Commit d31f1ce5 authored by Tommaso Petrucciani's avatar Tommaso Petrucciani
Browse files

Merge branch 'cduce-next' into setvariants

# Conflicts:
#	types/type_tallying.ml
parents a1043ffe 8a3f269f
......@@ -53,7 +53,7 @@ DEPEND_OCAMLDEP = misc/q_symbol.cmo
ifeq ($(PROFILE), true)
CAMLOPT_P = ocamlopt -p
ifeq ($(NATIVE), false)
CAMLC_P = ocamlcp -p a
CAMLC_P = ocamlcp -p
SYNTAX_PARSER =
DEPEND_OCAMLDEP =
endif
......
......@@ -180,6 +180,7 @@ let argv args =
let main () =
at_exit (fun () -> Stats.dump Format.std_formatter);
Cduce_loc.set_viewport (Html.create false);
Sys.set_signal Sys.sigint (Sys.Signal_handle (fun _ -> exit 2));
match mode () with
| `Toplevel args ->
Cduce_config.init_all ();
......
let margin = ref ""
let increase_margin () = margin := !margin ^ " "
let decrease_margin () = margin := String.sub !margin 0 (max (String.length !margin - 2) 0)
let () = Format.pp_set_tags Format.err_formatter true
let _DEBUG = fun level ?(enter=false) ?(leave=false) fmt ->
let _DEBUG = fun level ?(enter=false) ?(leave=false) pp ->
let () =
if enter then begin
Format.eprintf "%s> Entering %s: @\n%!" !margin level;
increase_margin ()
end
else if leave then begin
decrease_margin();
Format.eprintf "\n%s< Leaving %s:@\n%!" !margin level;
end
if enter then
Format.eprintf "@[@{<%s>@\n@[<v 3> " level
in
Format.eprintf "%s" !margin;
Format.eprintf fmt
Format.kfprintf
(fun fmt ->
if leave then
Format.fprintf fmt "@]@\n@}@]@\n"
)
Format.err_formatter pp
......@@ -8,15 +8,15 @@ let pp_list ?(delim=("[","]")) ?(sep=",") f ppf l =
let rec aux ppf =
function
[] -> Format.fprintf ppf ""
| [ h ] -> Format.fprintf ppf "%a@ " f h
| h::t -> Format.fprintf ppf "%a%s@ %a" f h sep aux t
| [ h ] -> Format.fprintf ppf "%a" f h
| h::t -> Format.fprintf ppf "%a%s@,%a" f h sep aux t
in
match l with
[] -> Format.fprintf ppf "%s%s" od cd
|_ -> Format.fprintf ppf "%s@ %a%s" od aux l cd
|_ -> Format.fprintf ppf "%s@,%a@,%s" od aux l cd
let pp_pair ?(delim=("(", ")")) ?(sep=",") f1 f2 ppf (p1, p2) =
let od, cd = delim in
Format.fprintf ppf "%s%a%s@ %a%s" od f1 p1 sep f2 p2 cd
Format.fprintf ppf "%s%a%s@,%a%s" od f1 p1 sep f2 p2 cd
let cons x l = x :: l
......@@ -112,6 +112,7 @@ sig
val union : t -> t -> t
val inter : t -> t -> t
val add : Line.t -> t -> t
val filter : (Line.t -> bool) -> t -> t
end
=
struct
......@@ -240,8 +241,8 @@ let single (type a) (module V : VarType with type Atom.t = a) b v lpos lneg =
let t = cap (aux id lpos) (aux neg lneg) in
if b then neg t else t
let toplevel
(*
let toplevel_poly
(type a) (module V : VarType with type Atom.t = a)
delta norm_rec mem lpos lneg
=
......@@ -261,9 +262,11 @@ let toplevel
| true, false -> 1
| _ -> Var.compare v1 v2
in
_DEBUG "normrec_spec" "@[ Starting toplevel @]@\n%!";
_DEBUG "normrec_spec" "@[ Starting toplevel @]@\n";
let res =
match lpos, lneg with
match lpos, lneg with
| `
[], (`Var x)::neg ->
let t = single (module V) false x [] neg in
singleton x (t, any)
......@@ -285,12 +288,43 @@ let toplevel
singleton x (t, any)
| [ (`Atm _) as a ], [ ] ->
norm_rec delta mem V.(inj (atom a))
norm_rec delta mem V.(inj (atom a))
| _ -> assert false
in
_DEBUG "normrec_spec" "@[ Finished toplevel %a @]@\n%!" ConstrSet.print res;
_DEBUG "normrec_spec" "@[ Finished toplevel %a @]@\n" ConstrSet.print res;
res
*)
let toplevel
(type a) (module V : VarType with type Atom.t = a)
delta norm_rec mem lpos lneg
=
let split_vars l =
List.partition
(function `Atm _ -> true
| `Var v -> not (Var.Set.mem delta v)) l
in
let lpos_poly, lpos_mono = split_vars lpos in
let lneg_poly, lneg_mono = split_vars lneg in
match lpos_poly, lpos_mono, lneg_poly, lneg_mono with
[ (`Atm _) as a ], _, [], _ -> norm_rec delta mem V.(inj (atom a))
| ([] | [ `Atm _ ]), _, (`Var x) :: llneg_poly, _ ->
let t = single (module V) false x lpos (llneg_poly @ lneg_mono) in
ConstrSet.single_var x (t, any)
| (`Var x)::llpos_poly, _, [], _ ->
let t = single (module V) true x (llpos_poly @ lpos_mono) lneg in
ConstrSet.single_var x (empty, t)
| (`Var x)::llpos_poly, _, (`Var y)::llneg_poly, _ ->
if Var.compare x y < 0 then
let t = single (module V) true x (llpos_poly @ lpos_mono) lneg in
ConstrSet.single_var x (empty, t)
else
let t = single (module V) false y lpos (llneg_poly @ lneg_mono) in
ConstrSet.single_var y (t, any)
| _ -> assert false
let big_prod ?(delta=Var.Set.empty) f acc l =
List.fold_left (fun acc (pos,neg) ->
......@@ -308,7 +342,7 @@ let history = ref []
let rec norm delta mem t =
_DEBUG "normrec" ~enter:true
"@[norm (id=%i) delta=@[%a@] <mem> t=@[ %a @] @]@\n%!"
"@[norm (id=%i) delta=@[%a@] <mem> t=@[ %a @] @]@\n"
(let () =
history := (t, (incr counter;!counter)) :: !history
in
......@@ -318,13 +352,13 @@ let rec norm delta mem t =
(* If we find it in the global hashtable,
we are finished *)
let res = NormMemoHash.find memo_norm (t, delta) in
_DEBUG "normrec" "@[ - Result found in global table @]@\n%!";
_DEBUG "normrec" "@[ - Result found in global table @]@\n";
res
with
Not_found ->
try
let finished, cst = NormMemoHash.find mem (t, delta) in
_DEBUG "normrec" "@[ - Result found in local table, finished = %b @]@\n%!" finished;
_DEBUG "normrec" "@[ - Result found in local table, finished = %b @]@\n" finished;
if finished then cst else ConstrSet.sat
with
Not_found ->
......@@ -332,10 +366,10 @@ let rec norm delta mem t =
let res =
(* base cases *)
if is_empty t then begin
_DEBUG "normrec" "@[ - Empty type case @]@\n%!";
_DEBUG "normrec" "@[ - Empty type case @]@\n";
ConstrSet.sat
end else if no_var t then begin
_DEBUG "normrec" "@[ - No var case @]@\n%!";
_DEBUG "normrec" "@[ - No var case @]@\n";
ConstrSet.unsat
end else if is_var t then begin
let (v,p) = Variable.extract t in
......@@ -348,12 +382,12 @@ let rec norm delta mem t =
ConstrSet.single_var v (if p then (empty, empty) else (any, any))
end
end else begin (* type is not empty and is not a variable *)
_DEBUG "normrec" "@[ - Inductive case:@]@\n%!";
_DEBUG "normrec" "@[ - Inductive case:@]@\n";
let mem = NormMemoHash.add mem (t,delta) (false, ConstrSet.sat); mem in
let t = Iter.simplify t in
let aux (module V : VarType) t acc =
_DEBUG "normrec"
" @[ - Before %a constraints: %a, remaining: %a @]@\n%!"
" @[ - Before %a constraints: %a, remaining: %a @]@\n"
pp_type_kind V.kind ConstrSet.print acc
Print.pp_type V.(inj (proj t));
......@@ -362,16 +396,17 @@ let rec norm delta mem t =
(toplevel (module V) delta (norm_dispatch V.kind) mem)
acc
V.(get (proj t)) *)
if ConstrSet.is_unsat acc then acc else
fold_prod (module V) (toplevel (module V) delta (norm_dispatch V.kind) mem)
acc V.(proj t)
in
_DEBUG "normrec"
" @[ - After %a constraints: %a @]@\n%!"
" @[ - After %a constraints: %a @]@\n"
pp_type_kind V.kind ConstrSet.print res;
res
in
let acc = Iter.fold aux t ConstrSet.sat in
_DEBUG "normrec" "@]@\n%!";
_DEBUG "normrec" "@]@\n";
acc
end
......@@ -380,7 +415,7 @@ let rec norm delta mem t =
end
in
_DEBUG "normrec" ~leave:true
"@[norm delta=@[%a@] <mem> t=@[ %a @] result=@[%a@] %a@]@\n%!"
"@[norm delta=@[%a@] <mem> t=@[ %a @] result=@[%a@] %a@]@\n"
Var.Set.print delta
Print.pp_type t
ConstrSet.print res
......@@ -482,14 +517,21 @@ and pp_arr x = Utils.pp_pair Print.pp_node Print.pp_node x
and pp_arrl x = Utils.pp_list pp_arr x
and pp_parrl x = Utils.pp_pair pp_arrl pp_arrl ~delim:("<",">") x
and simplify_cs_ delta mem m =
ConstrSet.filter (fun line ->
Line.for_all (fun v (inf, sup) ->
not (ConstrSet.is_unsat (norm delta mem (diff inf sup)))) line)
m
and simplify_cs delta mem m = m
and norm_arrow delta mem t =
let rec norm_arrow pos neg =
_DEBUG "norm_arrow_rec" ~enter:true "@[ norm_arrow_rec @[%a@] and @[%a@]@]@\n%!"
_DEBUG "norm_arrow_rec" ~enter:true "@[ norm_arrow_rec @[%a@] and @[%a@]@]@\n"
pp_arrl pos
pp_arrl neg;
match neg with
|[] -> ConstrSet.unsat
|(t1,t2) :: n ->
if is_empty (descr t1) then ConstrSet.sat else
let t1 = descr t1 and t2 = descr t2 in
let con1 = norm delta mem t1 in (* [t1] *)
let con2 = aux t1 (diff any t2) pos in
......@@ -498,7 +540,7 @@ and norm_arrow delta mem t =
ConstrSet.union (ConstrSet.union con1 con2) con0
in
_DEBUG "norm_arrow_rec" ~leave:true
"@[ norm_arrow_rec @[%a@] and @[%a@] result=@[%a@]@]@\n%!"
"@[ norm_arrow_rec @[%a@] and @[%a@] result=@[%a@]@]@\n"
pp_arrl pos
pp_arrl neg
ConstrSet.print res
......@@ -512,31 +554,44 @@ and norm_arrow delta mem t =
let t1s1 = diff t1 (descr s1) in
let acc1 = cap acc (descr s2) in
let con1 = norm delta mem t1s1 in (* [t1 \ s1] *)
let con1 = simplify_cs delta mem con1 in
let con10 = aux t1s1 acc p in
let con10 = simplify_cs delta mem con10 in
let con2 = norm delta mem acc1 in (* [(Any \ t2) ^ s2] *)
let con2 = simplify_cs delta mem con2 in
let con20 = aux t1 acc1 p in
let con20 = simplify_cs delta mem con20 in
let con11 = ConstrSet.union con1 con10 in
let con22 = ConstrSet.union con2 con20 in
ConstrSet.inter con11 con22
in
_DEBUG "norm_arrow" ~enter:true "@[norm_arrow delta=@[%a] mem t=@[%a@]@]@\n%!"
_DEBUG "norm_arrow" ~enter:true "@[<v 2>norm_arrow@ delta=@[%a@]@ mem@ t=@[%a@]@]@\n"
Var.Set.print delta
Print.pp_type t;
let t_arrow = VarArrow.leafconj (VarArrow.proj t) in
(* let dnf = Pair.get t in
_DEBUG "norm_arrow" (
Format.eprintf
"@[normarrow: @[%a@]@]\n%!"
"@[normarrow: @[%a@]@]\n"
(Utils.pp_list pp_parrl) dnf);
big_prod norm_arrow ConstrSet.sat (dnf) *)
(*let res =
fold_prod (module Pair) norm_arrow ConstrSet.sat t_arrow
in*)
let constrs = Pair.fold (fun (pos, neg) acc -> (norm_arrow pos neg)::acc) t_arrow [] in
_DEBUG "norm_arrow" "@[intermediate constraints:@\n%a@\n@]@\n%!"
_DEBUG "norm_arrow" "@[intermediate constraints:@\n%a@\n@]@\n"
(Utils.pp_list ~sep:",\n " ConstrSet.print) constrs;
let res = List.fold_left ConstrSet.inter ConstrSet.sat constrs in
_DEBUG "norm_arrow" ~leave:true "@[norm_arrow delta=@[%a] mem t=@[%a@] result=@[%a]@]@\n%!"
let res =
List.fold_left (fun acc cs ->
let nacc = ConstrSet.inter acc cs in
simplify_cs delta mem nacc)
ConstrSet.sat constrs
in
_DEBUG "norm_arrow" ~leave:true "@[<v 2>norm_arrow@ delta=@[%a@]@ mem@ t=@[%a@]@ result=@[%a]@]@\n"
Var.Set.print delta
Print.pp_type t
ConstrSet.print res;
......@@ -545,22 +600,30 @@ and norm_arrow delta mem t =
let norm delta t =
_DEBUG "norm" ~enter:true "@[norm delta=@[%a@] t=@[%a@] @]@\n%!"
_DEBUG "norm" ~enter:true "@[norm delta=@[%a@] t=@[%a@] @]@\n"
Var.Set.print delta Print.pp_type t;
let res =
try NormMemoHash.find memo_norm (t,delta)
with Not_found -> begin
let res = norm delta (NormMemoHash.create 17) t in
let mem = (NormMemoHash.create 17) in
let res = norm delta mem t in
let res = simplify_cs delta mem res in
NormMemoHash.add memo_norm (t,delta) res; res
end
in
_DEBUG "norm" ~leave:true "@[norm delta=@[%a@] t=@[ %a @] result=@[%a@] @]@\n%!"
_DEBUG "norm" ~leave:true "@[norm delta=@[%a@] t=@[ %a @] result=@[%a@] @]@\n"
Var.Set.print delta Print.pp_type t ConstrSet.print res;
res
module TypeCache =
module TypeCache =
struct
module Dset = (* Set.Make(Descr) *) struct type t = descr list let mem e l = List.exists (Types.equiv e) l let add e l = if mem e l then l else e :: l let empty = [] end
module Dset = struct
type t = descr list
let empty = []
let mem e l = List.exists (Types.equiv e) l
let add e l = if mem e l then l else e::l
end
(*Set.Make(Descr) *)
type t = Dset.t * unit Cache.cache
let empty = Dset.empty, Cache.emp
let mem t (dset, cache) =
......@@ -576,13 +639,14 @@ let norm delta t =
end
exception UnSatConstr of string
exception Found of descr
let rec merge delta cache m =
let saturate x =
let cache = TypeCache.add x cache in
let n = norm delta x in
if ConstrSet.is_unsat n then (_DEBUG "mergerec" "%a is unsat because of %a@\n"
Line.print m Print.pp_type x);
let c1 = ConstrSet.inter (ConstrSet.singleton m) n in
let c2 =
ConstrSet.fold (fun m1 acc ->
......@@ -606,7 +670,11 @@ let rec merge delta cache m =
_DEBUG "merge" ~leave:true "@[merge delta=@[%a@] res=@[%a@] @]@\n%!"
Var.Set.print delta ConstrSet.print res; res
let merge delta m = merge delta TypeCache.empty m
let merge delta m =
let res = merge delta TypeCache.empty m in
_DEBUG "merge" "@[merge delta=@[%a@] m=@[ %a @] result=@[%a@] @]@\n"
Var.Set.print delta Line.print m ConstrSet.print res;
res
let solve delta s =
let add_eq alpha s t acc =
......@@ -633,7 +701,7 @@ let solve delta s =
let solve delta s =
let res = solve delta s in
_DEBUG "solve" "Calling solve (%a, %a), got %a@\n%!"
_DEBUG "solve" "Calling solve (%a, %a), got %a@\n"
Var.Set.print delta ConstrSet.print s
pp_sl res;
res
......@@ -669,9 +737,7 @@ let unify (eq_set : Descr.t Var.Map.map) =
Subst.print eq_set Subst.print accu Subst.print res;
res
in
let res = loop eq_set Var.Map.empty in
_DEBUG "unify" "%!";
res
loop eq_set Var.Map.empty
exception Step1Fail
......@@ -679,7 +745,7 @@ exception Step2Fail
let tallying delta l =
_DEBUG "tallying" ~enter:true
"@[tallying delta=@[%a@] l=@[ %a @] @]@\n%!"
"@[tallying delta=@[%a@] l=@[ %a @] @]@\n"
Var.Set.print delta
(Utils.pp_list (Utils.pp_pair Print.pp_type Print.pp_type)) l;
let n =
......@@ -690,15 +756,15 @@ let tallying delta l =
else ConstrSet.inter acc (norm delta d)
) ConstrSet.sat l
in
_DEBUG "tallying" " @[tallying:after norm, contraints=@[ %a @] @]@\n%!" ConstrSet.print n;
_DEBUG "tallying" " @[tallying:after norm, contraints=@[ %a @] @]@\n" ConstrSet.print n;
if ConstrSet.is_unsat n then raise Step1Fail else
let m =
ConstrSet.fold (fun c acc -> (solve delta (merge delta c)) @ acc) n []
in
_DEBUG "tallying" " @[tallying:after solve, contraints=@[ %a @] @]@\n%!" pp_sl m;
_DEBUG "tallying" " @[tallying:after solve, contraints=@[ %a @] @]@\n" pp_sl m;
if m == [] then raise Step2Fail;
let res = List.map unify m in
_DEBUG "tallying" " @[tallying:after unify, solutions=@[ %a @] @]@\n%!" pp_sl res;
_DEBUG "tallying" " @[tallying:after unify, solutions=@[ %a @] @]@\n" pp_sl res;
_DEBUG "tallying" ~leave:true "";
res
......@@ -819,7 +885,7 @@ exception FoundApply of t * int * int * Descr.t Var.Map.map list
s @@ sigma_i < t @@ sigma_j for all i \in I, j \in J *)
let apply_raw delta s t =
_DEBUG "apply_raw" " @[Entering apply_raw (delta:@[%a@], @[%a@], @[%a@])@\n%!"
_DEBUG "apply_raw" " @[Entering apply_raw (delta:@[%a@], @[%a@], @[%a@])@\n"
Var.Set.print delta
Print.pp_type s
Print.pp_type t
......@@ -871,7 +937,7 @@ let apply_raw delta s t =
tallying i i;
loop (i+1)
with FoundApply (res, i, j, sl) ->
_DEBUG "apply_raw" " Leaving apply_raw (delta:@[%a@], @[%a@], @[%a@]) = @[%a@], @[%a@] @]@\n%!"
_DEBUG "apply_raw" " Leaving apply_raw (delta:@[%a@], @[%a@], @[%a@]) = @[%a@], @[%a@] @]@\n"
Var.Set.print delta
Print.pp_type s
Print.pp_type t
......
......@@ -1867,6 +1867,7 @@ let all_tlv = Variable.all_tlv
let has_tlv = Variable.has_tlv
let collect_vars = Variable.collect_vars
let all_vars = Variable.all_vars
let collect_vars = Variable.collect_vars
let extract_variable = Variable.extract_variable
let is_closed = Variable.is_closed
......@@ -2365,16 +2366,20 @@ module Print = struct
(* arrows *)
let u_acc =
(List.map (fun (p,n) ->
let p = List.fold_left (fun acc (t,s) ->
if is_empty (descr t) then acc else
(prepare (descr t), prepare (descr s)) :: acc) [] p
in
let n = List.rev_map (fun (t,s) ->
(prepare (descr t), prepare (descr s))) n
in
(Arrows (p,n))
) (Pair.get (VarArrow.(leafconj (proj tt))))) @ u_acc
List.fold_left (fun acc (p,n) ->
try
let p = List.fold_left (fun acc (t,s) ->
if is_empty (descr t) then acc else
(prepare (descr t), prepare (descr s)) :: acc) [] p
in
let n = List.rev_map (fun (t,s) ->
if is_empty (descr t) then raise Not_found;
(prepare (descr t), prepare (descr s))) n
in
(Arrows (p,n))::acc
with
Not_found -> acc)
u_acc (Pair.get (VarArrow.(leafconj (proj tt))))
in
(* records *)
......
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