Commit 58d89d58 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Revert "Improve the debugging infrastructre."

This reverts commit 802f291e.

This large merge commit makes the typing of some polymorphic variables buggy.
parent 576e9d76
......@@ -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
CAMLOPT_P = ocamlopt -p -inline 100
ifeq ($(NATIVE), false)
CAMLC_P = ocamlcp -p a
SYNTAX_PARSER =
DEPEND_OCAMLDEP =
endif
else
CAMLOPT_P = ocamlopt
CAMLOPT_P = ocamlopt -inline 100
endif
OPT = -warn-error FPSXY
......@@ -72,11 +72,8 @@ 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)
......@@ -184,7 +181,7 @@ DIRS := $(DIRS_DEPEND) $(OCAMLIFACE)
# Objects to build
OBJECTS = \
misc/debug.cmo driver/cduce_config.cmo misc/stats.cmo misc/custom.cmo misc/hBig_int.cmo misc/encodings.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
......@@ -31,11 +29,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/debug.cmo misc/custom.cmo types/var.cmi
misc/custom.cmo types/var.cmi
types/var.cmx : misc/utils.cmx types/sortedList.cmx types/ident.cmx \
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
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
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
......@@ -48,22 +46,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/debug.cmo \
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/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/debug.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/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/debug.cmo misc/custom.cmo types/bool.cmi types/type_tallying.cmi
misc/custom.cmo types/type_tallying.cmi
types/type_tallying.cmx : types/var.cmx misc/utils.cmx types/types.cmx \
misc/debug.cmx misc/custom.cmx types/bool.cmx types/type_tallying.cmi
misc/custom.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 \
......@@ -201,15 +199,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 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
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
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 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
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
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 \
......@@ -357,15 +355,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 \
plugins/jsoo_plugin.cmi driver/cduce_config.cmi driver/cduce.cmi
driver/cduce_config.cmi driver/cduce.cmi
driver/cducetop_js_runtime.cmx : driver/librarian.cmx \
plugins/jsoo_plugin.cmx driver/cduce_config.cmx driver/cduce.cmx
driver/cduce_config.cmx driver/cduce.cmx
driver/cduceeditor_js_runtime.cmo : parser/ulexer.cmi driver/librarian.cmi \
plugins/jsoo_plugin.cmi types/ident.cmo parser/cduce_loc.cmi \
driver/cduce_config.cmi driver/cduce.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 \
plugins/jsoo_plugin.cmx types/ident.cmx parser/cduce_loc.cmx \
driver/cduce_config.cmx driver/cduce.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 :
......
let margin = ref ""
let increase_margin () = margin := !margin ^ " "
let decrease_margin () = margin := String.sub !margin 0 (max (String.length !margin - 2) 0)
let _DEBUG = fun level ?(enter=false) ?(leave=false) fmt ->
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
in
Format.eprintf "%s" !margin;
Format.eprintf fmt
......@@ -38,7 +38,7 @@ let define s =
end
EXTEND Caml_syntax.Gram
GLOBAL: Caml_syntax.str_item Caml_syntax.sig_item Caml_syntax.expr;
GLOBAL: Caml_syntax.str_item Caml_syntax.expr;
Caml_syntax.str_item: FIRST
[ [ "ifdef"; c = UIDENT; "then"; e1 = SELF;
......@@ -50,33 +50,21 @@ 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
| "let" ; "_DEBUG"; "="; e = Caml_syntax.expr ->
let var = <:patt< $lid:"_DEBUG"$ >> in
let binding = <:binding< $var$ = $e$>> in
<:str_item<value $binding$>>
if List.mem_assoc c !symbols then <:str_item<>> else e1
] ];
Caml_syntax.sig_item: FIRST
[ [ "val" ; "_DEBUG" ; ":"; t = Caml_syntax.ctyp ->
<:sig_item< value $lid:"_DEBUG"$ : $t$ >> ] ];
Caml_syntax.expr: BEFORE "simple"
[ [
"_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
"DEBUG" ; x = OPT [ x = LIDENT -> x ]; "("; e = Caml_syntax.expr; ")" ->
let flag =
match x with
None -> ""
| Some s -> s
in
if !debug && (flag = "" || List.exists (fun s -> s = "all" || s = flag) !debug_symbols) then
inject e
e
else <:expr< () >>
]
]
];
END
......
......@@ -14,9 +14,3 @@ 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
let x : (('c -> 'c) & ('b -> 'b) & ('a -> 'a)) = fun ('aa -> 'aa; 'bb -> 'bb ; 'cc -> 'cc ) x -> x ;;
......@@ -130,4 +130,3 @@ 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,7 +15,6 @@ 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
......@@ -129,22 +128,21 @@ struct
| c -> [ fun ppf -> print f ppf c ]
let rec get_aux f rev accu pos neg = function
let rec get_aux rev accu pos neg = function
| True ->
let x =
if rev then (List.rev pos, List.rev neg)
else (pos,neg)
in f x accu
in 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 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
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
accu
let get x = get_aux Utils.cons false [] [] [] x
let fold f t acc = get_aux f false acc [] [] t
let get x = get_aux false [] [] [] x
let rec get' accu pos neg = function
| True -> (pos,neg) :: accu
......@@ -372,8 +370,7 @@ struct
let h = compute_hash v a False False in
(Split (h,`Var v, a, False, False) :> t )
let get x = get_aux Utils.cons true [] [] [] x
let fold f t acc = get_aux f true acc [] [] t
let get x = get_aux true [] [] [] x
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,4 +165,3 @@ 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,4 +404,3 @@ 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
This diff is collapsed.
open Ident
open Encodings
open Debug
let count = ref 0
let () =
......@@ -115,7 +114,6 @@ struct
let compute ~empty ~full ~cup ~cap ~diff ~atom b = assert false
let get _ = assert false
let iter _ = assert false
let fold _ = assert false
let full = any
......@@ -1851,13 +1849,6 @@ module Variable =
| _ -> raise (Invalid_argument "Variable.extract")
let extract_variable = extract
let variance v t =
let _,pos,neg, _ = collect_vars t in
match Var.Set.mem pos v, Var.Set.mem neg v with
true, false -> `Positive
| false,true -> `Negative
| true, true -> `Invariant
| false, false -> `Absent
end
......@@ -3264,14 +3255,14 @@ struct
let clean_type delta t =
if no_var t then t else
let _tlv,pos, neg, all = Variable.collect_vars t in
_DEBUG "clean_type" " - for type %a pos: %a, neg: %a, all: %a, tlv: %a, delta: %a@\n"
DEBUG clean_type (Format.eprintf " - for type %a pos: %a, neg: %a, all: %a, tlv: %a, delta: %a@\n"
Print.pp_type t
Var.Set.print pos
Var.Set.print neg
Var.Set.print all
Var.Set.print _tlv
Var.Set.print delta
;
);
let vars = Var.Set.diff all delta in
if Var.Set.is_empty vars then t else
let i_vars, s_vars =
......@@ -3297,8 +3288,8 @@ struct
let clean_type delta t =
let res = clean_type delta t in
_DEBUG "clean_type" "@[ Calling clean_type(%a,@, %a) = %a@]@\n%!"
Var.Set.print delta Print.pp_type t Print.pp_type res;
DEBUG clean_type (Format.eprintf "@[ Calling clean_type(%a,@, %a) = %a@]@\n%!"
Var.Set.print delta Print.pp_type t Print.pp_type res);
res
......
......@@ -203,7 +203,6 @@ end
module Variable : sig
val extract : t -> Var.t * bool
val variance : Var.t -> t -> [ `Positive | `Negative | `Invariant | `Absent ]
end
module Subst : sig
......@@ -369,8 +368,7 @@ val non_empty: t -> bool
val subtype : t -> t -> bool
val disjoint : t -> t -> bool
val equiv : t -> t -> bool
val trivially_disjoint : t -> t -> bool
(** intermediary representation for records *)
(*** TODO : SEAL OFF *)
......
open Debug
module V = struct
......@@ -18,10 +16,11 @@ module V = struct
Format.fprintf ppf "%a(%d_%a)" Ident.U.print t.name t.id print_kind t.kind
let compare x y =
let c = compare_kind x.kind y.kind in
if c == 0 then
let c = Ident.U.compare x.name y.name in
if c == 0 then x.id - y.id
let c = x.id - y.id in
if c == 0 then Ident.U.compare x.name y.name
else
c
else c
......@@ -45,10 +44,8 @@ module V = struct
let ident x = Ident.U.get_str x.name
let print ppf x =
begin
Format.fprintf ppf "'%a" Ident.U.print x.name;
_DEBUG "var_ident" "_%i_%a" x.id print_kind x.kind
end
DEBUG var_ident (Format.fprintf ppf "_%i_%a" x.id print_kind x.kind)
end
......
open Cduce_loc
open Ast
open Ident
open Debug
let (=) (x:int) y = x = y
let (<=) (x:int) y = x <= y
let (<) (x:int) y = x < y
......@@ -1271,9 +1270,9 @@ and type_check' loc env ed constr precise = match ed with
raise_loc loc (NonExhaustive (Types.diff t1 acc));
let t = type_check_branches loc env t1 [] a.fun_body Types.any true in
try
_DEBUG "typecheck_arrow" "Typechecking function %s @[%a@] against expected type @[%a@] delta = @[%a@]@\n%!"
DEBUG typecheck_arrow (Format.eprintf "Typechecking function %s @[%a@] against expected type @[%a@] delta = @[%a@]@\n%!"
(match a.fun_name with None -> "(anonymous)"
| Some s -> Ident.to_string s) Types.Print.pp_type t Types.Print.pp_type t2 Var.Set.print env.delta;
| Some s -> Ident.to_string s) Types.Print.pp_type t Types.Print.pp_type t2 Var.Set.print env.delta);
(Type_tallying.squaresubtype env.delta t t2)::tacc (* H_j *)
with
Type_tallying.UnSatConstr _ ->
......@@ -1359,7 +1358,7 @@ and type_check' loc env ed constr precise = match ed with
end
end
in
_DEBUG "typer_apply" "@[<hov 2> Typing function application:@\n\
DEBUG typer_apply (Format.eprintf "@[<hov 2> Typing function application:@\n\
delta: %a@\n\
function: %a@\n\
argument: %a@\n\
......@@ -1369,7 +1368,7 @@ substtitution: %a @]@\n%!"
Types.Print.pp_type t1
Types.Print.pp_type t2
Types.Print.pp_type res
Type_tallying.pp_sl sl;
Type_tallying.pp_sl sl);
let e = exp' loc ed in
e.exp_typ <- res;
(Subst(e,sl),verify loc res constr)
......
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