Commit 0f2c54a2 authored by Kim Nguyễn's avatar Kim Nguyễn

Debugging annotations.

parent 148cae0c
......@@ -187,9 +187,9 @@ module TLV = struct
}
(* true if it contains only one variable *)
let is_single t = t.isvar && (Var.Set.cardinal t.fv = 1) && (Set.cardinal t.tlv = 1)
let is_single t = t.isvar || ((Var.Set.cardinal t.fv = 1) && (Set.cardinal t.tlv = 1))
let no_variables t = (Var.Set.cardinal t.fv = 0) && (Set.cardinal t.tlv = 0)
let no_variables t = Var.Set.is_empty t.fv
let has_toplevel t = Set.cardinal t.tlv > 0
......@@ -2743,8 +2743,8 @@ module Positive = struct
with
Not_found ->
let node_t = forward () in
if no_var t then ty t
else
(*if no_var t then ty t
else *)
let () = DescrHash.add memo t node_t in
let descr_t =
decompose_kind Atom.any atom (BoolAtoms.get t.atoms)
......@@ -3156,19 +3156,27 @@ module Tallying = struct
type sl = sigma list
let singleton delta = function
|Pos (v,s) ->
if Var.Set.mem v delta then
(*if equal s any || equal (var v) s then *)S.singleton M.empty
(*else raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v))) *)
else
S.singleton (M.singleton v (empty,s))
|Neg (s,v) ->
if Var.Set.mem v delta then
(*if equal s any || equal (var v) s then *)S.singleton M.empty
(*else raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v))) *)
let singleton delta c =
let constr, do_check, t1, t2 =
match c with
|Pos (v,s) ->
if Var.Set.mem v delta then M.empty, true, (var v), s
else M.singleton v (empty,s), false, empty, empty
|Neg (s,v) ->
if Var.Set.mem v delta then M.empty, true, s, (var v)
else M.singleton v (s,any), false, empty, empty
in
let res = S.singleton constr in
if do_check then
if subtype t1 t2 then res
else
S.singleton (M.singleton v (s,any))
raise (UnSatConstr
(Format.sprintf
"Constraint (%s) <= (%s) on monomorphic variable failed"
(Utils.string_of_formatter Print.pp_type t1)
(Utils.string_of_formatter Print.pp_type t2)
))
else res
let pp_s = S.pp
let pp_m = M.pp
......@@ -3250,26 +3258,44 @@ module Tallying = struct
) acc l
(* norm generates a constraint set for the costraint t <= 0 *)
let debug_norm fmt =
if true then Format.eprintf fmt
else Format.ifprintf Format.err_formatter fmt
;;
let rec norm (t,delta,mem) =
debug_norm "Calling norm on input type %a : " Print.pp_type t;
(* if we already evaluated it, it is sat *)
if DescrSet.mem t mem || is_empty t then begin
debug_norm "It's Empty or found in memo, SAT@\n%!" ;
(*Format.printf "Sat for type %a\n%!" Print.print t; *)
CS.sat end
else begin
CS.sat
end else
(* if there is only one variable then is it A <= 0 or 1 <= A *)
if is_var t then
if is_var t then begin
debug_norm "It's a variable " ;
let (v,p) = TLV.max t.toplvars in
if Var.Set.mem v delta then CS.unsat
else
if Var.Set.mem v delta then begin
debug_norm "which is in delta, UNSAT@\n%!" ;
CS.unsat
end else
let () = debug_norm "which is not delta, ADDING SINGLETON CONSTRAINT@\n" in
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
CS.singleton delta s
(* if there are no vars, and it is not empty then unsat *)
else if (*no_var t*) Var.Set.subset t.toplvars.TLV.fv delta
then CS.unsat
else begin
end else
let () = debug_norm "is_var on type %a returned false!@\n%!" Print.pp_type t in
if no_var t (* Var.Set.subset t.toplvars.TLV.fv delta *)then begin
debug_norm "It does not have any variables, UNSAT@\n%!" ;
CS.unsat
end else begin
debug_norm "It is a complex type, adding to memo and recursing @\n%!";
let mem = DescrSet.add t mem in
let aux single norm_aux acc l = big_prod delta (toplevel delta single norm_aux mem) acc l in
let aux single norm_aux acc l =
let res = big_prod delta (toplevel delta single norm_aux mem) acc l
in
debug_norm " For type (%a) constraints where %a, are now %a@\n%!" Print.pp_type t CS.pp_s acc CS.pp_s res; res
in
let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
let acc = aux single_chars normchars acc (BoolChars.get t.chars) in
let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in
......@@ -3278,9 +3304,10 @@ module Tallying = struct
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
(* XXX normrec is not tested at all !!! *)
aux single_record normrec acc (BoolRec.get t.record)
let res = aux single_record normrec acc (BoolRec.get t.record) in
debug_norm "Type (%a) yielded constraints: %a@\n%!"
Print.pp_type t CS.pp_s res; res
end
end
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
* (s1,s2) \in N
......
......@@ -812,6 +812,15 @@ let let_decl env p e =
open Typed
let debug_env env =
Format.eprintf " Environment is:@\n%!";
Env.iter (fun s v ->
Format.eprintf " %s : " (Ident.to_string s);
match v with
EVal(_,_,t)| Val t -> Format.eprintf "%a@\n" Types.Print.pp_type t
| _ -> Format.eprintf "####@\n") env.ids;
Format.eprintf " Delta is: %a@\n%!" Var.Set.pp env.delta
let localize loc f x =
try f x with
| (Error _ | Constraint (_,_)) as exn ->
......@@ -878,6 +887,14 @@ and type_check' loc env ed constr precise = match ed with
(ed,verify loc (Types.cap te (Types.descr t)) constr)
| Abstraction a ->
let fun_name = match a.fun_name with
None -> "<anonymous>"
| Some f -> Ident.to_string f
in
Format.eprintf ">>> Typing the body of %s (line %a)@\n%!" fun_name Cduce_loc.print_loc (loc,`Full);
Format.eprintf "Env before is:@\n";
debug_env env;
let env = {
(* freshen type variables from the environment to avoid capture with
variables defined in the interface of a *)
......@@ -891,6 +908,9 @@ and type_check' loc env ed constr precise = match ed with
| x -> x)
env.ids }
in
Format.eprintf "Env after is:@\n";
debug_env env;
let t =
(* try Types.Arrow.check_strenghten a.fun_typ constr *)
try begin
......@@ -901,7 +921,7 @@ and type_check' loc env ed constr precise = match ed with
"but the interface of the abstraction is not compatible"
in
let env = match a.fun_name with
| None -> env
| None -> env
| Some f -> enter_value f a.fun_typ env
in
(* update \delta with all variables in t1 -> t2 *)
......@@ -971,9 +991,13 @@ and type_check' loc env ed constr precise = match ed with
(ed,localize loc (flatten (type_map loc env true e b) constr) precise)
| Apply (e1,e2) ->
let t1 = type_check env e1 Types.Arrow.any true in
let t1arrow = Types.Arrow.get t1 in
let t1 = Types.Positive.substitutefree env.delta t1 in
Format.eprintf "Typing application (%a)\n" Cduce_loc.print_loc (loc,`Full);
debug_env env;
let t1 = type_check env e1 Types.Arrow.any true in
Format.eprintf "Typechecked function type: %a@\n" Types.Print.pp_type t1;
let t1arrow = Types.Arrow.get t1 in
let t1 = Types.Positive.substitutefree env.delta t1 in
Format.eprintf "Refreshed function type: %a@\n" Types.Print.pp_type t1;
(* t [_delta 0 -> 1 *)
begin try
......@@ -984,6 +1008,7 @@ and type_check' loc env ed constr precise = match ed with
let dom = Types.Arrow.domain(t1arrow) in
let t2 = type_check env e2 Types.any true in
Format.eprintf "Typechecked argument type: %a@\n" Types.Print.pp_type t2;
let res =
if not (Types.no_var dom) ||
not (Types.no_var t2) then
......@@ -991,9 +1016,13 @@ and type_check' loc env ed constr precise = match ed with
let (sl,res) =
(* s [_delta dom(t) *)
try Types.squareapply env.delta t1 t2
with Types.Tallying.UnSatConstr _ ->
with Types.Tallying.UnSatConstr msg ->
Format.eprintf "Typing application failed with message: %s@\n" msg;
raise_loc loc (Constraint (t2,dom))
in
Format.eprintf "Found result type: %a (substitutions: %a)@\n%!"
Types.Print.pp_type res Types.Tallying.CS.pp_sl sl
;
res
else begin
(* Monomorphic case as before *)
......
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