Commit 7b5be392 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Second part of the debugging infrastructure.

parent 38cf7a58
......@@ -51,14 +51,14 @@ SYNTAX_PARSER = -syntax camlp4o $(SYNTAX:%=-ppopt %)
CAMLC_P = ocamlc -g
DEPEND_OCAMLDEP = misc/q_symbol.cmo
ifeq ($(PROFILE), true)
CAMLOPT_P = ocamlopt -p -inline 100
CAMLOPT_P = ocamlopt -p
ifeq ($(NATIVE), false)
CAMLC_P = ocamlcp -p a
SYNTAX_PARSER =
DEPEND_OCAMLDEP =
endif
else
CAMLOPT_P = ocamlopt -inline 100
CAMLOPT_P = ocamlopt
endif
OPT = -warn-error FPSXY
......@@ -72,8 +72,11 @@ ifeq ($(INTERFACE), true)
endif
ifneq ($(strip $(DEBUG)),)
OPT += -g
OPT += -g
SYNTAX += -symbol cduce_debug=\"$(DEBUG)\"
CAMLOPT_P += -inline 0
else
CAMLOPT_P += -inline 100
endif
ifeq ($(BIN_ANNOT), true)
......@@ -181,7 +184,7 @@ DIRS := $(DIRS_DEPEND) $(OCAMLIFACE)
# Objects to build
OBJECTS = \
driver/cduce_config.cmo misc/stats.cmo misc/custom.cmo misc/hBig_int.cmo misc/encodings.cmo \
misc/debug.cmo driver/cduce_config.cmo misc/stats.cmo misc/custom.cmo misc/hBig_int.cmo misc/encodings.cmo \
misc/upool.cmo misc/pretty.cmo misc/ns.cmo misc/imap.cmo misc/html.cmo misc/utils.cmo \
\
types/compunit.cmo types/sortedList.cmo types/ident.cmo types/var.cmo types/bool.cmo \
......
misc/debug.cmo :
misc/debug.cmx :
driver/cduce_config.cmo : driver/cduce_config.cmi
driver/cduce_config.cmx : driver/cduce_config.cmi
misc/stats.cmo : misc/stats.cmi
......@@ -29,11 +31,11 @@ types/ident.cmo : misc/utils.cmo types/sortedList.cmi misc/ns.cmi \
types/ident.cmx : misc/utils.cmx types/sortedList.cmx misc/ns.cmx \
misc/encodings.cmx
types/var.cmo : misc/utils.cmo types/sortedList.cmi types/ident.cmo \
misc/custom.cmo types/var.cmi
misc/debug.cmo misc/custom.cmo types/var.cmi
types/var.cmx : misc/utils.cmx types/sortedList.cmx types/ident.cmx \
misc/custom.cmx types/var.cmi
types/bool.cmo : types/var.cmi misc/custom.cmo types/bool.cmi
types/bool.cmx : types/var.cmx misc/custom.cmx types/bool.cmi
misc/debug.cmx misc/custom.cmx types/var.cmi
types/bool.cmo : types/var.cmi misc/utils.cmo misc/custom.cmo types/bool.cmi
types/bool.cmx : types/var.cmx misc/utils.cmx misc/custom.cmx types/bool.cmi
types/intervals.cmo : misc/hBig_int.cmi types/intervals.cmi
types/intervals.cmx : misc/hBig_int.cmx types/intervals.cmi
types/chars.cmo : misc/custom.cmo types/chars.cmi
......@@ -46,22 +48,22 @@ types/normal.cmo : types/normal.cmi
types/normal.cmx : types/normal.cmi
types/types.cmo : types/var.cmi misc/utils.cmo misc/stats.cmi \
types/sortedList.cmi misc/pretty.cmi misc/ns.cmi types/normal.cmi \
types/intervals.cmi types/ident.cmo misc/encodings.cmi misc/custom.cmo \
types/compunit.cmi types/chars.cmi types/bool.cmi types/atoms.cmi \
types/types.cmi
types/intervals.cmi types/ident.cmo misc/encodings.cmi misc/debug.cmo \
misc/custom.cmo types/compunit.cmi types/chars.cmi types/bool.cmi \
types/atoms.cmi types/types.cmi
types/types.cmx : types/var.cmx misc/utils.cmx misc/stats.cmx \
types/sortedList.cmx misc/pretty.cmx misc/ns.cmx types/normal.cmx \
types/intervals.cmx types/ident.cmx misc/encodings.cmx misc/custom.cmx \
types/compunit.cmx types/chars.cmx types/bool.cmx types/atoms.cmx \
types/types.cmi
types/intervals.cmx types/ident.cmx misc/encodings.cmx misc/debug.cmx \
misc/custom.cmx types/compunit.cmx types/chars.cmx types/bool.cmx \
types/atoms.cmx types/types.cmi
compile/auto_pat.cmo : types/types.cmi types/ident.cmo types/chars.cmi \
types/atoms.cmi compile/auto_pat.cmi
compile/auto_pat.cmx : types/types.cmx types/ident.cmx types/chars.cmx \
types/atoms.cmx compile/auto_pat.cmi
types/type_tallying.cmo : types/var.cmi misc/utils.cmo types/types.cmi \
misc/custom.cmo types/type_tallying.cmi
misc/debug.cmo misc/custom.cmo types/bool.cmi types/type_tallying.cmi
types/type_tallying.cmx : types/var.cmx misc/utils.cmx types/types.cmx \
misc/custom.cmx types/type_tallying.cmi
misc/debug.cmx misc/custom.cmx types/bool.cmx types/type_tallying.cmi
types/sequence.cmo : types/types.cmi misc/custom.cmo types/chars.cmi \
types/atoms.cmi types/sequence.cmi
types/sequence.cmx : types/types.cmx misc/custom.cmx types/chars.cmx \
......@@ -199,15 +201,15 @@ types/externals.cmx : parser/cduce_loc.cmx types/externals.cmi
typing/typer.cmo : types/var.cmi misc/utils.cmo types/types.cmi \
typing/typepat.cmi typing/typed.cmo types/type_tallying.cmi \
types/sequence.cmi schema/schema_validator.cmi types/patterns.cmi \
misc/ns.cmi types/ident.cmo types/externals.cmi types/compunit.cmi \
types/chars.cmi parser/cduce_loc.cmi types/builtin_defs.cmi \
types/atoms.cmi parser/ast.cmo typing/typer.cmi
misc/ns.cmi types/ident.cmo types/externals.cmi misc/debug.cmo \
types/compunit.cmi types/chars.cmi parser/cduce_loc.cmi \
types/builtin_defs.cmi types/atoms.cmi parser/ast.cmo typing/typer.cmi
typing/typer.cmx : types/var.cmx misc/utils.cmx types/types.cmx \
typing/typepat.cmx typing/typed.cmx types/type_tallying.cmx \
types/sequence.cmx schema/schema_validator.cmx types/patterns.cmx \
misc/ns.cmx types/ident.cmx types/externals.cmx types/compunit.cmx \
types/chars.cmx parser/cduce_loc.cmx types/builtin_defs.cmx \
types/atoms.cmx parser/ast.cmx typing/typer.cmi
misc/ns.cmx types/ident.cmx types/externals.cmx misc/debug.cmx \
types/compunit.cmx types/chars.cmx parser/cduce_loc.cmx \
types/builtin_defs.cmx types/atoms.cmx parser/ast.cmx typing/typer.cmi
compile/compile.cmo : types/var.cmi runtime/value.cmi misc/upool.cmi \
types/types.cmi typing/typer.cmi typing/typed.cmo types/type_tallying.cmi \
types/patterns.cmi misc/ns.cmi compile/lambda.cmi misc/imap.cmi \
......@@ -355,15 +357,15 @@ driver/run.cmx : runtime/value.cmx parser/ulexer.cmx misc/stats.cmx \
driver/cduce_js_runtime.cmo : driver/cduce_config.cmi driver/cduce.cmi
driver/cduce_js_runtime.cmx : driver/cduce_config.cmx driver/cduce.cmx
driver/cducetop_js_runtime.cmo : driver/librarian.cmi \
driver/cduce_config.cmi driver/cduce.cmi
plugins/jsoo_plugin.cmi driver/cduce_config.cmi driver/cduce.cmi
driver/cducetop_js_runtime.cmx : driver/librarian.cmx \
driver/cduce_config.cmx driver/cduce.cmx
plugins/jsoo_plugin.cmx driver/cduce_config.cmx driver/cduce.cmx
driver/cduceeditor_js_runtime.cmo : parser/ulexer.cmi driver/librarian.cmi \
types/ident.cmo parser/cduce_loc.cmi driver/cduce_config.cmi \
driver/cduce.cmi
plugins/jsoo_plugin.cmi types/ident.cmo parser/cduce_loc.cmi \
driver/cduce_config.cmi driver/cduce.cmi
driver/cduceeditor_js_runtime.cmx : parser/ulexer.cmx driver/librarian.cmx \
types/ident.cmx parser/cduce_loc.cmx driver/cduce_config.cmx \
driver/cduce.cmx
plugins/jsoo_plugin.cmx types/ident.cmx parser/cduce_loc.cmx \
driver/cduce_config.cmx driver/cduce.cmx
driver/start.cmo : driver/run.cmo
driver/start.cmx : driver/run.cmx
driver/examples.cmo :
......
......@@ -38,7 +38,7 @@ let define s =
end
EXTEND Caml_syntax.Gram
GLOBAL: Caml_syntax.str_item Caml_syntax.expr;
GLOBAL: Caml_syntax.str_item Caml_syntax.sig_item Caml_syntax.expr;
Caml_syntax.str_item: FIRST
[ [ "ifdef"; c = UIDENT; "then"; e1 = SELF;
......@@ -50,21 +50,33 @@ EXTEND Caml_syntax.Gram
"else"; e2 = SELF ->
if List.mem_assoc c !symbols then e2 else e1
| "ifndef"; c = UIDENT; "then"; e1 = SELF ->
if List.mem_assoc c !symbols then <:str_item<>> else e1
if List.mem_assoc c !symbols then <:str_item<>> else e1
| "let" ; "_DEBUG"; "="; e = Caml_syntax.expr ->
let var = <:patt< $lid:"_DEBUG"$ >> in
let binding = <:binding< $var$ = $e$>> in
<:str_item<value $binding$>>
] ];
Caml_syntax.sig_item: FIRST
[ [ "val" ; "_DEBUG" ; ":"; t = Caml_syntax.ctyp ->
<:sig_item< value $lid:"_DEBUG"$ : $t$ >> ] ];
Caml_syntax.expr: BEFORE "simple"
[ [
"DEBUG" ; x = OPT [ x = LIDENT -> x ]; "("; e = Caml_syntax.expr; ")" ->
let flag =
match x with
None -> ""
| Some s -> s
in
"_DEBUG" ; flag = STRING ; e = Caml_syntax.expr LEVEL "apply" ->
let _debug = <:expr<$lid:"_DEBUG"$>> in
let _flag = <:expr<$str:flag$>> in
let rec inject e =
match e with
<:expr< $e1$ $e2$ >> -> let ee = inject e1 in <:expr< $ee$ $e2$>>
| _ -> <:expr< $_debug$ $_flag$ $e$ >>
in
if !debug && (flag = "" || List.exists (fun s -> s = "all" || s = flag) !debug_symbols) then
e
inject e
else <:expr< () >>
]
]
];
END
......
......@@ -14,3 +14,9 @@ let pp_list ?(delim=("[","]")) ?(sep=",") f ppf l =
match l with
[] -> Format.fprintf ppf "%s%s" od 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
let cons x l = x :: l
......@@ -130,3 +130,4 @@ let is_finite m =
let compute ~empty ~full ~cup ~cap ~diff ~atom b = assert false
let get _ = assert false
let iter _ = assert false
let fold _ = assert false
......@@ -15,6 +15,7 @@ sig
include Custom.T
val get: t -> (elem list * elem list) list
val fold : ((elem list * elem list) -> 'a -> 'a) -> t -> 'a -> 'a
val empty : t
val full : t
......@@ -128,21 +129,22 @@ struct
| c -> [ fun ppf -> print f ppf c ]
let rec get_aux rev accu pos neg = function
let rec get_aux f rev accu pos neg = function
| True ->
let x =
if rev then (List.rev pos, List.rev neg)
else (pos,neg)
in x :: accu
in f x accu
| False -> accu
| Split (_,x, p,i,n) ->
(*OPT: can avoid creating this list cell when pos or neg =False *)
let accu = get_aux rev accu (x::pos) neg p in
let accu = get_aux rev accu pos (x::neg) n in
let accu = get_aux rev accu pos neg i in
let accu = get_aux f rev accu (x::pos) neg p in
let accu = get_aux f rev accu pos (x::neg) n in
let accu = get_aux f rev accu pos neg i in
accu
let get x = get_aux false [] [] [] x
let get x = get_aux Utils.cons false [] [] [] x
let fold f t acc = get_aux f false acc [] [] t
let rec get' accu pos neg = function
| True -> (pos,neg) :: accu
......@@ -370,7 +372,8 @@ struct
let h = compute_hash v a False False in
(Split (h,`Var v, a, False, False) :> t )
let get x = get_aux true [] [] [] x
let get x = get_aux Utils.cons true [] [] [] x
let fold f t acc = get_aux f true acc [] [] t
let leafconj x =
let rec aux accu = function
......
......@@ -8,7 +8,7 @@ sig
include Custom.T
val get: t -> (elem list * elem list) list
val fold : ((elem list * elem list) -> 'a -> 'a) -> t -> 'a -> 'a
val empty : t
val full : t
val cup : t -> t -> t
......
......@@ -165,3 +165,4 @@ let trivially_disjoint = disjoint
let compute ~empty ~full ~cup ~cap ~diff ~atom b = assert false
let get _ = assert false
let iter _ = assert false
let fold _ = assert false
......@@ -404,3 +404,4 @@ let trivially_disjoint = disjoint
let compute ~empty ~full ~cup ~cap ~diff ~atom b = assert false
let get _ = assert false
let iter _ = assert false
let fold _ = assert false
......@@ -231,6 +231,8 @@ let toplevel
| true, false -> 1
| _ -> Var.compare v1 v2
in
_DEBUG "normrec_spec" "@[ Starting toplevel @]@\n%!";
let res =
match lpos, lneg with
[], (`Var x)::neg ->
let t = single (module V) false x [] neg in
......@@ -252,37 +254,47 @@ let toplevel
let t = single (module V) false x lpos neg in
singleton x (t, any)
| [ (`Atm _) as a ], [ ] -> norm_rec delta mem V.(inj (atom a))
| [ (`Atm _) as a ], [ ] ->
norm_rec delta mem V.(inj (atom a))
| _ -> assert false
in
_DEBUG "normrec_spec" "@[ Finished toplevel %a @]@\n%!" ConstrSet.print res;
res
let big_prod f acc l =
let big_prod ?(delta=Var.Set.empty) f acc l =
List.fold_left (fun acc (pos,neg) ->
ConstrSet.inter acc (f pos neg)
ConstrSet.inter acc (f pos neg)
) acc l
let fold_prod (type e) (type b) ?(delta=Var.Set.empty) (module B : Bool.S with type elem = e and type t = b) f acc t =
B.fold (fun (pos, neg) acc -> ConstrSet.inter acc (f pos neg)) t acc
module NormMemoHash = Hashtbl.Make(Custom.Pair(Descr)(Var.Set))
let memo_norm = NormMemoHash.create 17
let counter = ref 0
let history = ref []
let rec norm delta mem t =
DEBUG normrec (
Format.eprintf
" @[Entering norm rec(%a):@\n" Print.pp_type t);
_DEBUG "normrec" ~enter:true
"@[norm (id=%i) delta=@[%a@] <mem> t=@[ %a @] @]@\n%!"
(let () =
history := (t, (incr counter;!counter)) :: !history
in
!counter) Var.Set.print delta Print.pp_type t;
let res =
try
(* If we find it in the global hashtable,
we are finished *)
let res = NormMemoHash.find memo_norm (t, delta) in
DEBUG normrec (Format.eprintf
"@[ - 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 (Format.eprintf
"@[ - 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 ->
......@@ -290,39 +302,46 @@ let rec norm delta mem t =
let res =
(* base cases *)
if is_empty t then begin
DEBUG normrec (Format.eprintf "@[ - Empty type case @]@\n");
_DEBUG "normrec" "@[ - Empty type case @]@\n%!";
ConstrSet.sat
end else if no_var t then begin
DEBUG normrec (Format.eprintf "@[ - No var case @]@\n");
ConstrSet.unsat
_DEBUG "normrec" "@[ - No var case @]@\n%!";
ConstrSet.unsat
end else if is_var t then begin
let (v,p) = Variable.extract t in
if Var.Set.mem delta v then begin
DEBUG normrec (Format.eprintf "@[ - Monomorphic var case @]@\n");
_DEBUG "normrec" "@[ - Monomorphic var case @]@\n";
ConstrSet.unsat (* if it is monomorphic, unsat *)
end else begin
DEBUG normrec (Format.eprintf "@[ - Polymorphic var case @]@\n");
_DEBUG "normrec" "@[ - Polymorphic var case @]@\n";
(* otherwise, create a single constraint according to its polarity *)
ConstrSet.singleton v (if p then (empty, empty) else (any, any))
end
end else begin (* type is not empty and is not a variable *)
DEBUG normrec (Format.eprintf "@[ - 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%!"
pp_type_kind V.kind ConstrSet.print acc
Print.pp_type V.(inj (proj t));
let res =
big_prod
(*big_prod
(toplevel (module V) delta (norm_dispatch V.kind) mem)
acc
V.(get (proj t))
V.(get (proj t)) *)
fold_prod (module V) (toplevel (module V) delta (norm_dispatch V.kind) mem)
acc V.(proj t)
in
DEBUG normrec
(Format.eprintf "@[ - After %a constraints: %a @]@\n"
pp_type_kind V.kind ConstrSet.print res);
_DEBUG "normrec"
" @[ - 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 (Format.eprintf "@]@\n");
_DEBUG "normrec" "@]@\n%!";
acc
end
......@@ -330,11 +349,20 @@ let rec norm delta mem t =
NormMemoHash.replace mem (t, delta) (true,res); res
end
in
DEBUG normrec (Format.eprintf
"Leaving norm rec(%a) = %a@]@\n%!"
Print.pp_type t
ConstrSet.print res
);
_DEBUG "normrec" ~leave:true
"@[norm delta=@[%a@] <mem> t=@[ %a @] result=@[%a@] %a@]@\n%!"
Var.Set.print delta
Print.pp_type t
ConstrSet.print res
(fun ppf h ->
let _, c = List.hd !h in
Format.fprintf ppf "end of call %i, " c;
h := List.tl !h;
match !h with
[] -> Format.fprintf ppf "no more pending types"
| (tt,i) :: _ -> Format.fprintf ppf "pending type (id=%i) is %a" i Print.pp_type tt)
history
;
res
and norm_dispatch k =
......@@ -382,7 +410,8 @@ and norm_pair (module V : VarType with type Atom.t = Pair.t) delta mem t =
ConstrSet.(union (union con1 con2) con0)
in
let t = V.leafconj (V.proj t) in
big_prod norm_prod ConstrSet.sat (Pair.get t)
(*big_prod norm_prod ConstrSet.sat (Pair.get t) *)
fold_prod (module Pair) norm_prod ConstrSet.sat t
and norm_rec delta mem t =
let norm_rec_array ((oleft,left),rights) =
......@@ -403,9 +432,9 @@ and norm_rec delta mem t =
in
let t = VarRec.leafconj (VarRec.proj t) in
List.fold_left (fun acc (_,p,n) ->
if ConstrSet.is_unsat acc then acc else ConstrSet.inter acc (norm_rec_array (p,n))
ConstrSet.inter acc (norm_rec_array (p,n))
) ConstrSet.sat (get_record t)
(* arrow(p,{t1 -> t2}) = [t1] v arrow'(t1,any \ t2,p)
* arrow'(t1,acc,{s1 -> s2} v p) =
* ([t1\s1] v arrow'(t1\s1,acc,p)) ^
......@@ -419,8 +448,15 @@ and norm_rec delta mem t =
* P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
*)
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 norm_arrow delta mem t =
let rec norm_arrow pos neg =
_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 ->
......@@ -428,31 +464,69 @@ and norm_arrow delta mem t =
let con1 = norm delta mem t1 in (* [t1] *)
let con2 = aux t1 (diff any t2) pos in
let con0 = norm_arrow pos n in
ConstrSet.union (ConstrSet.union con1 con2) con0
and aux t1 acc = function
let res =
ConstrSet.union (ConstrSet.union con1 con2) con0
in
_DEBUG "norm_arrow_rec" ~leave:true
"@[ norm_arrow_rec @[%a@] and @[%a@] result=@[%a@]@]@\n%!"
pp_arrl pos
pp_arrl neg
ConstrSet.print res
;
res
and aux t1 acc l =
match l with
|[] -> ConstrSet.unsat
|(s1,s2) :: p ->
let t1s1 = diff t1 (descr s1) in
let acc1 = cap acc (descr s2) in
let con1 = norm delta mem t1s1 in (* [t1 \ s1] *)
let con2 = norm delta mem acc1 in (* [(Any \ t2) ^ s2] *)
let con10 = aux t1s1 acc p in
let con2 = norm delta mem acc1 in (* [(Any \ t2) ^ s2] *)
let con20 = aux t1 acc1 p in
let con11 = ConstrSet.union con1 con10 in
let con22 = ConstrSet.union con2 con20 in
ConstrSet.inter con11 con22
in
let t = VarArrow.leafconj (VarArrow.proj t) in
big_prod norm_arrow ConstrSet.sat (Pair.get t)
_DEBUG "norm_arrow" ~enter:true "@[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%!"
(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%!"
(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%!"
Var.Set.print delta
Print.pp_type t
ConstrSet.print res;
res
let norm delta t =
try NormMemoHash.find memo_norm (t,delta)
with Not_found -> begin
let res = norm delta (NormMemoHash.create 17) t in
NormMemoHash.add memo_norm (t,delta) res; res
end
_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
NormMemoHash.add memo_norm (t,delta) res; res
end
in
_DEBUG "norm" ~leave:true "@[norm delta=@[%a@] t=@[ %a @] result=@[%a@] @]@\n%!"
Var.Set.print delta Print.pp_type t ConstrSet.print res;
res
(* merge needs delta because it calls norm recursively *)
let rec merge delta cache m =
......@@ -508,46 +582,44 @@ let solve delta s =
let solve delta s =
let res = solve delta s in
DEBUG solve (Format.eprintf "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);
pp_sl res;
res
let () = Format.pp_set_margin Format.err_formatter 200
let unify (eq_set : Descr.t Var.Map.map) =
let rec loop eq_set accu =
DEBUG unify
(Format.eprintf "@[<hov 2> Entering unify_loop @[(%a, %a)@]@\n"
Subst.print eq_set Subst.print accu);
_DEBUG "unify"
"@[<hov 2> Entering unify_loop @[(%a, %a)@]@\n"
Subst.print eq_set Subst.print accu;
let res =
if Var.Map.is_empty eq_set then accu else
begin
let (alpha, t), eq_set' = Var.Map.remove_min eq_set in
DEBUG unify (Format.eprintf
_DEBUG "unify"
"@[<hov 2>- Choosing equation @[%a = %a@]@]@\n"
Var.print alpha Types.Print.pp_type t);
Var.print alpha Types.Print.pp_type t;
let x = Subst.solve_rectype t alpha in
DEBUG unify (Format.eprintf
"@[<hov 2>- Solving equation @[%a = %a@]@]@\n"
Var.print alpha Types.Print.pp_type x);
_DEBUG "unify" "@[<hov 2>- Solving equation @[%a = %a@]@]@\n"
Var.print alpha Types.Print.pp_type x;
let eq_set' =
Var.Map.map (fun s -> Subst.single s (alpha,x)) eq_set'
in
let sigma = loop eq_set' (Var.Map.replace alpha x accu) in
let t_alpha = Subst.full x sigma in
DEBUG unify (Format.eprintf
"@[<hov 2>- Applying substitution @[%a@] to @[%a@], @[<hov 4>got %a@]@]@\n"
Subst.print sigma Print.pp_type x Print.pp_type t_alpha);
_DEBUG "unify" "@[<hov 2>- Applying substitution @[%a@] to @[%a@], @[<hov 4>got %a@]@]@\n"
Subst.print sigma Print.pp_type x Print.pp_type t_alpha;
Var.Map.replace alpha t_alpha sigma
end
in
DEBUG unify (Format.eprintf "Leaving unify_loop @[(%a, %a)@], @[<hov 4>got %a@]@]@\n"
Subst.print eq_set Subst.print accu Subst.print res);
_DEBUG "unify" "Leaving unify_loop @[(%a, %a)@], @[<hov 4>got %a@]@]@\n"
Subst.print eq_set Subst.print accu Subst.print res;
res
in
let res = loop eq_set Var.Map.empty in
DEBUG unify (Format.(pp_print_flush err_formatter ()));
_DEBUG "unify" "%!";
res
......@@ -555,14 +627,19 @@ exception Step1Fail
exception Step2Fail
let tallying delta l =
_DEBUG "tallying" ~enter:true
"@[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 =
List.fold_left (fun acc (s,t) ->
let d = diff s t in
let d = Iter.simplify (diff s t) in