Commit 75077fa0 authored by Pietro Abate's avatar Pietro Abate
Browse files

test

parent 06abcb05
let pretty (x : Int) : String = string_of x;;
let even2 (Int -> Bool; ('c\Int) -> ('c\Int))
| x & Int -> (x mod 2) = 0
| x -> x
;;
let even (Int -> Bool; ('a\Int) -> ('a\Int))
| x & Int -> (x mod 2) = 0
| x -> x
......
......@@ -8,7 +8,7 @@ let length (l : t( 'a ) ) : Int =
let hd (['a+] -> 'a) [el _*] -> el
let tl (t( 'a ) -> ['a*])
let tl (t( 'a ) -> t( 'a ))
| [] -> []
| [_; rest] -> rest
......
......@@ -2972,6 +2972,9 @@ module Tallying = struct
else c) map1 map2
let add delta v (inf, sup) map =
(*
let _ = Format.printf "%a <= %a <= %a@." Print.pp_type inf Var.pp v Print.pp_type sup in
*)
let new_i, new_s =
try
let old_i, old_s = VarMap.find v map in
......@@ -3191,7 +3194,35 @@ module Tallying = struct
else
if monov1 then 1 else -1
in
let remove l e =
List.filter (function
|`Var x -> not(Var.equal x e)
|`Atm _ -> true
) l
in
match (p,n) with
|([`Atm t], []) -> norm_rec (t,delta,mem)
|(pos,neg) ->
let ps =
List.fold_left (fun acc -> function
|(`Var x) ->
let t = single (true,x,remove pos x,neg) in
CS.union acc (CS.singleton (Pos (x,t)))
|`Atm _ -> acc
) CS.unsat pos
in
let ns =
List.fold_left (fun acc -> function
|(`Var x) ->
let t = single (false,x,pos,remove neg x) in
CS.union acc (CS.singleton (Neg (t, x)))
|`Atm _ -> assert false
) CS.unsat neg
in
CS.union ps ns
(*
|([], (`Var x)::neg) ->
let t = single (false,x,[],neg) in
CS.singleton (Neg (t, x))
......@@ -3214,6 +3245,7 @@ module Tallying = struct
|([`Atm t], []) -> norm_rec (t,delta,mem)
|_,_ -> assert false
*)
let big_prod delta f acc l =
List.fold_left (fun acc (pos,neg) ->
......@@ -3426,30 +3458,32 @@ module Tallying = struct
let unify e =
let rec aux sol e =
(* Format.printf "e = %a\n" CS.print_e e; *)
Format.eprintf "e = %a@.%!" CS.pp_e e;
if CS.E.is_empty e then sol
else begin
let (alpha,t) = CS.E.min_binding e in
(* Format.printf "Unify -> %a = %a\n" Var.pp alpha Print.pp_type t; *)
Format.eprintf "Choosing Binding %a = %a@.%!" Var.pp alpha Print.pp_type t;
let e1 = CS.E.remove alpha e in
(* Format.printf "e1 = %a\n" CS.print_e e1; *)
Format.printf "E\%a = %a@." Var.pp alpha CS.pp_e e1;
(* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
(* substituterec remove also all previously introduced fresh variables *)
let x = Positive.substituterec t alpha in
(* Format.printf "X = %a %a %a\n" Var.pp alpha Print.print x dump t; *)
Format.printf "X = %a@." Print.pp_type x;
let es =
CS.E.fold (fun beta s acc ->
CS.E.add beta (Positive.substitute s (alpha,x)) acc
) e1 CS.E.empty
in
(* Format.printf "es = %a\n" CS.print_e es; *)
aux ((CS.E.add alpha x sol)) es
Format.printf "E' = %a@." CS.pp_e es;
let sigma = aux ((CS.E.add alpha x sol)) es in
let talpha = CS.E.fold (fun v sub acc -> Positive.substitute acc (v,sub)) sigma x in
CS.E.add alpha talpha sigma
end
in
(* Format.printf "Begin e = %a\n" CS.print_e e; *)
Format.eprintf "Begin e = %a@." CS.pp_e e;
let r = aux CS.E.empty e in
(* Format.printf "r = %a\n" CS.print_e r; *)
Format.eprintf "r = %a@." CS.pp_e r;
r
exception Step1Fail
......@@ -3473,8 +3507,9 @@ module Tallying = struct
in
if CS.ES.is_empty m then raise Step2Fail else
let el =
CS.ES.fold (fun e acc -> CS.ES.add (unify e) acc ) m CS.ES.empty
CS.ES.fold (fun e acc -> Format.eprintf "aaaa\n%!" ; CS.ES.add (unify e) acc ) m CS.ES.empty
in
Format.eprintf "vvvv\n%!" ;
(CS.ES.elements el)
(* apply sigma to t *)
......@@ -3561,6 +3596,7 @@ let get a i = if i < 0 then any else (!a).(i)
exception FoundSquareSub of Tallying.CS.sl
let squaresubtype delta s t =
Format.eprintf "begin squareapply\n%!";
Tallying.NormMemoHash.clear Tallying.memo_norm;
let ai = ref [| |] in
let tallying i =
......@@ -3574,12 +3610,14 @@ let squaresubtype delta s t =
in
let rec loop i =
try
Format.eprintf "before clean\n%!";
let ss =
if i = 0 then s
else (cap (Positive.substitutefree delta s) (get ai (i-1)))
in
set ai i ss;
tallying i;
Format.eprintf "after clean\n%!";
loop (i+1)
with FoundSquareSub sl -> sl
in
......@@ -3593,6 +3631,7 @@ exception FoundApply of t * int * int * Tallying.CS.sl
(** find two sets of type substitutions I,J such that
s @@ sigma_i < t @@ sigma_j for all i \in I, j \in J *)
let apply_raw delta s t =
Format.eprintf "begin apply_raw\n%!";
Tallying.NormMemoHash.clear Tallying.memo_norm;
let vgamma = Var.mk "Gamma" in
let gamma = var vgamma in
......@@ -3605,6 +3644,7 @@ let apply_raw delta s t =
let s = get ai i in
let t = arrow (cons (get aj j)) cgamma in
let sl = Tallying.tallying delta [ (s,t) ] in
Format.eprintf "before clean\n%!";
let new_res =
Positive.clean_type delta (
List.fold_left (fun tacc si ->
......@@ -3612,10 +3652,11 @@ let apply_raw delta s t =
) any sl
)
in
Format.eprintf "after clean\n%!";
raise (FoundApply(new_res,i,j,sl))
with
Tallying.Step1Fail -> (assert (i == 0 && j == 0); raise (Tallying.UnSatConstr "apply_raw step1"))
| Tallying.Step2Fail -> () (* continue *)
| Tallying.Step2Fail -> Format.printf "Step2Fail@."; () (* continue *)
in
let rec loop i =
try
......@@ -3642,7 +3683,10 @@ let apply_raw delta s t =
loop 0
let apply_full delta s t =
let _,_,_,res = apply_raw delta s t in
let sl,_,_,res = apply_raw delta s t in
res
let squareapply delta s t = let s,_,_,res = apply_raw delta s t in (s,res)
let squareapply delta s t =
let sl,_,_,res = apply_raw delta s t in
let _ = Format.printf "Final Sub : %a@." Tallying.CS.pp_sl sl in
(sl,res)
......@@ -8,7 +8,8 @@ module V = struct
let check _ = ()
let is_fresh x = x.fr > 0
let fresh v = { v with fr = v.fr + 1 }
let freshcounter = ref 0
let fresh v = { v with fr = (incr freshcounter; !freshcounter) }
let mk id = { id = Ident.U.mk id; fr = 0 }
let id x = Ident.U.get_str x.id
......
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