Commit 6dce4b88 authored by Pietro Abate's avatar Pietro Abate
Browse files

Merge branch 'master' into propagate

Conflicts:
	tests/lambda/src/printer.ml
	types/patterns.ml
parents b9aa225f e18e076b
......@@ -198,11 +198,11 @@ and compile_branches env (brs : Typed.branches) =
* 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 *)
let t, _, d = br.Typed.br_pat.Patterns.descr in
let t, fv, d = br.Typed.br_pat.Patterns.descr in
let fv, d = incr Patterns.counter;
let freshname = "pat" ^ (string_of_int !Patterns.counter) ^ ":x" in
let fv = (Patterns.fv br.Typed.br_pat) @ [!Patterns.counter, freshname] in
fv, Patterns.Cap((Types.any, fv, Patterns.Capture(!Patterns.counter, freshname)), (t, [], d))
let fv = fv @ [!Patterns.counter, freshname] in
fv, Patterns.Cap((Types.any, fv, Patterns.Capture(!Patterns.counter, freshname)), (t, 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
......
......@@ -48,7 +48,15 @@ Int } ,{ `$A = [ Char* ]
`$A & Int | Char | Atom | (Any,Any) | <(Any) (Any)>Any | Arrow),{}))",
"fun pair x : ('A[{}] * 'B[{}]) : 'A[{}] -> match x : ('A[{}] * 'B[{}]) with | (z : 'A[{}], y : 'B[{}]) -> z";
"Test CDuce.runtime.poly.match_abstr failed", "Apply(,)",
"Test CDuce.runtime.poly.match_abstr failed", "Apply(Match(Abstraction(Dummy,,,,Sel(,(`$A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow -> `$A & Int |
Char |
Atom |
(Any,Any) |
<(Any) (Any)>Any |
Arrow),{})), {accept_chars=false; brs_disp=<disp>; brs_rhs=[| (2, TVar(Local(0),Comp({},{ { `$A =
Int
} }))) |]; brs_stack_pos=0}),Const(3))",
"(match (fun f x : 'A[{}] : 'A[{}] -> x) : ('A[{}] -> 'A[{}]) with | y : ('A[{}] -> 'A[{}]) -> y[{A/Int}]).3";
......
......@@ -229,10 +229,22 @@ and pp_lambda ppf =
| Var v -> Format.fprintf ppf "Var(%a)" pp_vloc v
| TVar (v,sigma) -> Format.fprintf ppf "TVar(%a,%a)" pp_vloc v pp_lambda_sigma sigma
| Apply (e1,e2) -> Format.fprintf ppf "Apply(%a,%a)" pp_lambda e1 pp_lambda e2
| Abstraction (va, l, b, i, true, sigma, v) -> Format.fprintf ppf "PolyAbstraction(%a,,,,%a,%a)" pp_vloc_array va pp_lambda_sigma sigma pp_vloc v
| Abstraction (va, l, b, i, false, sigma, v) -> Format.fprintf ppf "Abstraction(%a,,,,%a,%a)" pp_vloc_array va pp_lambda_sigma sigma pp_vloc v
| Abstraction (va, l, b, i, true, sigma) -> Format.fprintf ppf "PolyAbstraction(%a,,,,%a)" pp_vloc_array va pp_sigma sigma
| Abstraction (va, l, b, i, false, sigma) -> Format.fprintf ppf "Abstraction(%a,,,,%a)" pp_vloc_array va pp_sigma sigma
| Check(_) -> Format.fprintf ppf "Check"
| Const(v) -> Format.fprintf ppf "Const(%a)" pp_value v
| Pair(e1, e2) -> Format.fprintf ppf "Pair(%a, %a)" pp_lambda e1 pp_lambda e2
| String(_) -> Format.fprintf ppf "String"
| Match(e, brs) -> Format.fprintf ppf "Match(%a, %a)" pp_lambda e pp_lbranches brs
| _ -> ()
and pp_lbranches ppf brs =
let open Lambda in
Format.fprintf ppf "{accept_chars=%b; brs_disp=<disp>; brs_rhs=[| %a |]; brs_stack_pos=%d}" brs.brs_accept_chars pp_patrhs brs.brs_rhs brs.brs_stack_pos
and pp_patrhs ppf arr =
Array.iter (function | Auto_pat.Match(i, e) -> Format.fprintf ppf "(%d, %a)" i pp_lambda e | _ -> ()) arr
let print_to_string f x =
let b = Buffer.create 1024 in
let ppf = Format.formatter_of_buffer b in
......
......@@ -336,7 +336,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;
r
let filter t p =
......@@ -370,10 +370,13 @@ x=(1,2)
| Cup ((a1,_,_) as p1,p2) ->
approx_var seen p2 (Types.diff t a1)
(approx_var seen p1 (Types.cap t a1) xs)
| Cap ((_,fv1,_) as p1,((_,fv2,_) as p2)) ->
IdSet.cup
| Cap ((_,fv1,d1) as p1,((_,fv2,d2) as p2)) ->
(match d1 with
| Capture(_, name) when Str.string_match (Str.regexp "pat[0-9]+:") name 0 ->
(match d2 with | Constr _ -> fv2 | _ -> approx_var seen p2 t xs)
| _ -> IdSet.cup
(approx_var seen p1 t (IdSet.cap fv1 xs))
(approx_var seen p2 t (IdSet.cap fv2 xs))
(approx_var seen p2 t (IdSet.cap fv2 xs)))
| Capture _ ->
xs
| Constant (_,c) ->
......@@ -389,7 +392,6 @@ 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