Commit 251e2287 authored by Pietro Abate's avatar Pietro Abate
Browse files

Merge branch 'master-merge' into typing-test

parents b75572c5 cb63b921
......@@ -181,13 +181,23 @@ and compile_branches env (brs : Typed.branches) =
(* p_i / t_i -> br.Typed.br_pat / br.Typed.br_type
* p_i / t_i is used here to add elements to env.gamma *)
and compile_branch env br =
(* We add a fresh variable "pat<nb>:x" for each pattern
TODO: Add a fresh variable for cap too. *)
(* We add a fresh variable "pat<nb>:x" for each pattern (except Constr) *)
let t, _, d = br.Typed.br_pat.Patterns.descr in
let fv = match d with
| Patterns.Constr(_) | Patterns.Cap(_) -> Patterns.fv br.Typed.br_pat
| _ -> incr Patterns.counter; (Patterns.fv br.Typed.br_pat)
@ [!Patterns.counter, "pat" ^ (string_of_int !Patterns.counter) ^ ":x"] in
let fv, d = match d with
| Patterns.Constr(_) -> Patterns.fv br.Typed.br_pat, d
| Patterns.Cap((t1, _, d1), (t2, _, d2)) -> incr Patterns.counter;
let fv = (Patterns.fv br.Typed.br_pat)
@ [!Patterns.counter, "pat" ^ (string_of_int !Patterns.counter) ^ ":x"] in
fv, Patterns.Cap((t1, fv, d1), (t2, fv, d2))
| Patterns.Cup((t1, _, d1), (t2, _, d2)) -> incr Patterns.counter;
let fv = (Patterns.fv br.Typed.br_pat)
@ [!Patterns.counter, "pat" ^ (string_of_int !Patterns.counter) ^ ":x"] in
fv, Patterns.Cup((t1, fv, d1), (t2, fv, d2))
| _ -> incr Patterns.counter;
let fv = (Patterns.fv br.Typed.br_pat)
@ [!Patterns.counter, "pat" ^ (string_of_int !Patterns.counter) ^ ":x"] in
fv, d
in
let pat = { br.Typed.br_pat with Patterns.descr=(t,fv,d); Patterns.fv=fv } in
let env = List.fold_left enter_local env fv in
let m = Patterns.filter (Types.descr (Patterns.accept pat)) pat in
......
......@@ -101,10 +101,10 @@ let rec _to_typed env l expr =
and make_sigma s =
let rec aux2 acc = function
| (name, ptype) :: rest ->
aux2 ((Var.mk name, type_of_ptype ptype) :: acc) rest
aux2 (Types.Tallying.CS.E.add (Var.mk name) (type_of_ptype ptype) acc) rest
| [] -> acc in
let rec aux acc = function
| l :: rest -> aux (acc @ [aux2 [] l]) rest
| l :: rest -> aux (acc @ [aux2 Types.Tallying.CS.E.empty l]) rest
| [] -> acc in
aux [] s
......
......@@ -27,8 +27,9 @@ let tests_poly_abstr = [
"fun f x : Int : Int -> 2";
"Test CDuce.lambda.poly.identity failed",
"Abstraction(Dummy,,,,Sel(,([ Char* ] | Int -> [ Char* ] | Int),Comp({},{ { (`$A/
Int) } ,{ (`$A/[ Char* ]) } })))",
"Abstraction(Dummy,,,,Sel(,([ Char* ] | Int -> [ Char* ] | Int),Comp({},{ { `$A =
Int } ,{ `$A = [ Char* ]
} })))",
"(fun f x : 'A[{A/Int},{A/String}] : 'A[{A/Int},{A/String}] -> x) [{A/Int},{A/String}]";
"Test CDuce.runtime.poly.tail failed",
......
......@@ -26,12 +26,12 @@ let rec pp_typed ppf e =
pp_typed_aux e
and pp_typedsigma ppf =
let rec aux ppf = function
| (v, t) :: rest -> Format.fprintf ppf "(%a, %a)" Var.dump v Types.Print.print t
| [] -> Format.fprintf ppf "" in
let rec aux ppf s = Types.Tallying.CS.E.iter
(fun k v -> Format.fprintf ppf "(%a, %a)" Var.dump k Types.Print.print v) s
in
function
| s :: rest -> Format.fprintf ppf "[%a, %a]" aux s pp_typedsigma rest
| [] -> Format.fprintf ppf ""
| [] -> ()
and pp_typed_aux ppf e =
match e.Typed.exp_descr with
......
......@@ -338,7 +338,7 @@ and filter_node t p : Types.Positive.v id_map =
let res = IdMap.map_from_slist (fun _ -> Types.Positive.forward ()) fv in
memo_filter := MemoFilter.add (t,p) res !memo_filter;
let r = filter_descr t (descr p) in
IdMap.collide Types.Positive.define res r;
(* IdMap.collide Types.Positive.define res r;*) (* Had to comment this to add fresh variables for patterns *)
r
let filter t p =
......@@ -391,6 +391,7 @@ x=(1,2)
(approx_var_node seen q1 (pi1 ~kind:`XML t) xs)
(approx_var_node seen q2 (pi2 ~kind:`XML t) xs)
| Record _ -> IdSet.empty
| Constr _ -> xs (* Needed to add fresh variables to patterns *)
| _ -> assert false
and approx_var_node seen q t xs =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment