Commit 28b75cf5 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Do not call Arrow.apply since the types bound to the variable Gamma will be...

Do not call Arrow.apply since the types bound to the variable Gamma will be the result of the application.
parent 1d82d5dc
...@@ -1972,9 +1972,9 @@ struct ...@@ -1972,9 +1972,9 @@ struct
Print.assign_name t; Print.assign_name t;
t;; t;;
let trace msg = let trace msg =
(* output_string stderr (msg ^ "\n"); (* output_string stderr (msg ^ "\n");
flush stderr *) flush stderr *)
();; ();;
let print_to_string f = let print_to_string f =
...@@ -2511,7 +2511,7 @@ struct ...@@ -2511,7 +2511,7 @@ struct
* position with any *) * position with any *)
let substituterec t alpha = let substituterec t alpha =
let subst x d = let subst x d =
if Var.equal d alpha then x if Var.equal d alpha then x
else var d else var d
in in
if no_var t then t if no_var t then t
...@@ -2557,9 +2557,9 @@ struct ...@@ -2557,9 +2557,9 @@ struct
| (b1, v1) :: ll -> (b1==b && v1==v) || (memq_pair key ll) | (b1, v1) :: ll -> (b1==b && v1==v) || (memq_pair key ll)
in in
let memo = ref [] in let memo = ref [] in
(* we memoize based on the pair (pos, v), since v can occur both (* we memoize based on the pair (pos, v), since v can occur both
* positively and negatively. and we want to manage the variables * positively and negatively. and we want to manage the variables
* differently in both cases *) * differently in both cases *)
let rec aux pos v = let rec aux pos v =
if not (memq_pair (pos,v) !memo) then if not (memq_pair (pos,v) !memo) then
let () = memo := (pos,v) :: !memo in let () = memo := (pos,v) :: !memo in
...@@ -3198,8 +3198,8 @@ let apply_raw s t = ...@@ -3198,8 +3198,8 @@ let apply_raw s t =
Queue.add (aux (0,lazy(s)) (1,lazy(Positive.substitutefree t)) s t) q; Queue.add (aux (0,lazy(s)) (1,lazy(Positive.substitutefree t)) s t) q;
let result = ref ([],(any,any)) in let result = ref ([],(any,any)) in
let counter = ref 0 in let counter = ref 0 in
(* I removed the condition to stop at the first solution since, (* I removed the condition to stop at the first solution since,
at least for map even it is only partial *) at least for map even it is only partial *)
while not(Queue.is_empty q) do while not(Queue.is_empty q) do
try try
incr counter; (* don't know about termination... *) incr counter; (* don't know about termination... *)
...@@ -3221,13 +3221,17 @@ let apply_full s t = ...@@ -3221,13 +3221,17 @@ let apply_full s t =
cap tacc (List.fold_left (fun tacc subst -> cap tacc (List.fold_left (fun tacc subst ->
Positive.substitute tacc subst) t constr_lst)) any subst_lst Positive.substitute tacc subst) t constr_lst)) any subst_lst
in in
let arr = Arrow.get ss in (*let arr = Arrow.get ss in
let res = Arrow.apply arr (tt) in let res = Arrow.apply arr (tt) in *)
let ss = Positive.clean_type ss in let ss = Positive.clean_type ss in
let tt = Positive.clean_type tt in let tt = Positive.clean_type tt in
let res = Positive.clean_type res in (*let res = Positive.clean_type res in *)
Format.printf "sl = %a\nfunction type = %a\nargument type = %a\nresult type = %a\n\n%!" let res2 = List.fold_left
Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res; res (fun acc l -> cap acc (snd (List.find (fun (`Var v, _) -> 0 == String.compare v.Var.id "Gamma") l))) any subst_lst
in
let res2 = Positive.clean_type res2 in
Format.printf "sl = %a\nfunction type = %a\nargument type = %a\nresult type = %a\n%!"
Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res2; res2
let apply s t = fst (apply_raw s t) let apply s t = fst (apply_raw s t)
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