Commit 802f291e authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Improve the debugging infrastructre.

parent 6c4f2a3a
......@@ -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 :
......
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.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
let x : (('c -> 'c) & ('b -> 'b) & ('a -> 'a)) = fun ('aa -> 'aa; 'bb -> 'bb ; 'cc -> 'cc ) x -> x ;;
......@@ -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
This diff is collapsed.
open Ident
open Encodings
open Debug
let count = ref 0
let () =
......@@ -114,6 +115,7 @@ 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
......@@ -1849,6 +1851,13 @@ 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
......@@ -3255,14 +3264,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 (Format.eprintf " - for type %a pos: %a, neg: %a, all: %a, tlv: %a, delta: %a@\n"
_DEBUG "clean_type" " - 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 =
......@@ -3288,8 +3297,8 @@ struct
let clean_type delta t =
let res = clean_type delta t in
DEBUG clean_type (Format.eprintf "@[ Calling clean_type(%a,@, %a) = %a@]@\n%!"
Var.Set.print delta Print.pp_type t Print.pp_type res);
_DEBUG "clean_type" "@[ Calling clean_type(%a,@, %a) = %a@]@\n%!"
Var.Set.print delta Print.pp_type t Print.pp_type res;
res
......
......@@ -203,6 +203,7 @@ end
module Variable : sig
val extract : t -> Var.t * bool
val variance : Var.t -> t -> [ `Positive | `Negative | `Invariant | `Absent ]
end
module Subst : sig
......@@ -368,7 +369,8 @@ 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
......@@ -16,11 +18,10 @@ 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 = x.id - y.id in
if c == 0 then Ident.U.compare x.name y.name
let c = Ident.U.compare x.name y.name in
if c == 0 then x.id - y.id
else
c
else c
......@@ -44,8 +45,10 @@ 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 (Format.fprintf ppf "_%i_%a" x.id print_kind x.kind)
_DEBUG "var_ident" "_%i_%a" x.id print_kind x.kind
end
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
......@@ -1270,9 +1271,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 (Format.eprintf "Typechecking function %s @[%a@] against expected type @[%a@] delta = @[%a@]@\n%!"
_DEBUG "typecheck_arrow" "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 _ ->
......@@ -1358,7 +1359,7 @@ and type_check' loc env ed constr precise = match ed with
end
end
in
DEBUG typer_apply (Format.eprintf "@[<hov 2> Typing function application:@\n\
_DEBUG "typer_apply" "@[<hov 2> Typing function application:@\n\
delta: %a@\n\
function: %a@\n\
argument: %a@\n\
......@@ -1368,7 +1369,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