Commit 4eeac845 authored by Kim Nguyễn's avatar Kim Nguyễn

Remove debugging code.

parent 6d75d13d
......@@ -137,70 +137,6 @@ module BoolChars : BoolVar.S with
module BoolAbstracts : BoolVar.S with
type s = Abstracts.t = BoolVar.Make(Abstracts)
(* module TLV = struct *)
(* module Set = struct *)
(* include Set.Make( *)
(* struct *)
(* type t = (Var.var * bool) *)
(* let compare (v1,p1) (v2,p2) = *)
(* let c = Var.compare v1 v2 in *)
(* if c == 0 then *)
(* if p1 == p2 then 0 *)
(* else if p1 then 1 else -1 *)
(* else c *)
(* end) *)
(* let pp_aux ppf pp_elem s = *)
(* let f ppf = function *)
(* |(v,true) -> Format.fprintf ppf "%a" pp_elem v *)
(* |(v,false) -> Format.fprintf ppf "~ %a" pp_elem v *)
(* in *)
(* Utils.pp_list ~sep:";" ~delim:("{","}") f ppf (elements s) *)
(* let dump ppf s = pp_aux ppf Var.dump s *)
(* let pp ppf s = pp_aux ppf Var.pp s *)
(* let printf = pp Format.std_formatter *)
(* end *)
(* (\* tlv : top level variables *)
(* * fv : all free variables in the subtree *\) *)
(* type t = { tlv : Set.t ; fv : Var.Set.t; isvar : bool } *)
(* let empty = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false } *)
(* let any = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false } *)
(* let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; isvar = true } *)
(* (\* return the max of top level variables *\) *)
(* let max x = Set.max_elt x.tlv *)
(* let pair x y = { *)
(* tlv = Set.empty ; *)
(* fv = Var.Set.union x.fv y.fv ; *)
(* isvar = false *)
(* } *)
(* let record x = { *)
(* tlv = Set.empty ; *)
(* fv = x.fv ; *)
(* isvar = false *)
(* } *)
(* (\* 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 no_variables t = (Var.Set.cardinal t.fv = 0) && (Set.cardinal t.tlv = 0) *)
(* let has_toplevel t = Set.cardinal t.tlv > 0 *)
(* let pp ppf x = Set.pp ppf x.tlv *)
(* let dump ppf x = Format.fprintf ppf "<fv = %a ; tlv = %a>" Var.Set.dump x.fv Set.dump x.tlv *)
(* let printf = pp Format.std_formatter *)
(* let mem v x = Set.mem v x.tlv *)
(* end *)
module rec Descr :
sig
(* each kind is represented as a union of itersection of types
......@@ -3284,61 +3220,41 @@ 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
if DescrSet.mem t mem || is_empty t then CS.sat
else if is_var t then begin
(* if there is only one variable then is it A <= 0 or 1 <= A *)
if is_var t then begin
debug_norm "It's a variable " ;
let (v,p) = extract_variable t in
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
if Var.Set.mem v delta then CS.unsat
else
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 *)
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 =
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
let acc = aux single_times normpair acc (BoolPair.get t.times) in
let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
end else if no_var t then CS.unsat
else begin
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 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
let acc = aux single_times normpair acc (BoolPair.get t.times) in
let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
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 !!! *)
let res = aux single_record normrec acc (BoolRec.get t.record) in
let res =
CS.S.filter
(fun m -> CS.M.for_all (fun v (s, t) -> not (Var.Set.mem v delta) ||
let x = var v in subtype s x && subtype x t
let res = aux single_record normrec acc (BoolRec.get t.record) in
let res = (* Simplify the constraints on that type *)
CS.S.filter
(fun m -> CS.M.for_all (fun v (s, t) -> not (Var.Set.mem v delta) ||
let x = var v in subtype s x && subtype x t
) m)
res
in
debug_norm "Type (%a) yielded constraints: %a@\n%!"
Print.pp_type t CS.pp_s res; res
res
in
res
end
......@@ -3542,7 +3458,6 @@ module Tallying = struct
else CS.prod delta acc (norm delta d)
) CS.sat l
in
debug_norm "First step gave constraints: %a@\n%!" CS.pp_s n;
if Pervasives.(n = CS.unsat) then raise Step1Fail else
let m =
CS.S.fold (fun c acc ->
......@@ -3658,7 +3573,6 @@ let squaresubtype delta s t =
in
set ai i ss;
tallying i;
if i == 2 then raise (Tallying.UnSatConstr "Gave up");
loop (i+1)
with FoundSquareSub sl -> sl
in
......@@ -3710,7 +3624,6 @@ let apply_raw delta s t =
tallying i j;
done;
tallying i i;
if i == 2 then raise (Tallying.UnSatConstr "Gave up");
loop (i+1)
with FoundApply (res, i, j, sl) -> sl, get ai i, get aj j, res
in
......
......@@ -812,15 +812,6 @@ 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 ->
......@@ -887,14 +878,6 @@ 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 *)
......@@ -908,9 +891,6 @@ 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
......@@ -991,13 +971,9 @@ 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) ->
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
......@@ -1008,7 +984,6 @@ 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
......@@ -1017,12 +992,8 @@ and type_check' loc env ed constr precise = match ed with
(* s [_delta dom(t) *)
try Types.squareapply env.delta t1 t2
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