Setepenre pushed to branch master at Stefan / Typer
Commits: be8035b0 by Pierre Delaunay at 2016-10-06T16:10:24-04:00 Updated formating primitive to output a string instead of printing things. This was modified to allow them to be used when writing error messages
Changes to be committed: * src/fmt.ml * src/util.ml - new function (loc_string), changed (print_loc) to (loc_print) for consistency with what is done elsewhere.
- - - - - 2ae5a5ce by Pierre Delaunay at 2016-10-10T16:45:19-04:00 * src/lparse.ml - Updated calltrace system. Eval and Lparse can use the same trace. - Added new debug_message primitive to help print helpful messages. Debugging info is provided as strings and not printed anymore which mean we can create messages we want without constraints. - elab trace is passed to eval when expanding macros.
* src/eval.ml - Moved evaluated builtin function from (src/builtin.ml) to (src/eval.ml)
* src/opslexp.ml - new type (pexporlexp)
* src/elexp.ml - removed old debug_message
* src/REPL.ml * src/debug.ml * src/debug_util.ml - updated to reflect modification
- - - - - 8c6311a9 by Pierre Delaunay at 2016-10-10T16:51:13-04:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - -
10 changed files:
- src/REPL.ml - src/builtin.ml - src/debug.ml - src/debug_util.ml - src/elexp.ml - src/eval.ml - src/fmt.ml - src/lparse.ml - src/opslexp.ml - src/util.ml
Changes:
===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -183,6 +183,7 @@ let _help_msg = %who (%w) : print runtime environment %info (%i) : print elaboration environment %calltrace (%ct): print call trace of last call + %elabtrace (%et): print elaboration trace %readfile : read a Typer file %help (%h) : print help " @@ -217,7 +218,8 @@ let rec repl i clxp rctx = | "%help" | "%h" -> (print_string _help_msg; repl clxp rctx) | "%who" | "%w" -> (print_rte_ctx rctx; repl clxp rctx) | "%info" | "%i" -> (print_lexp_ctx (ectx_to_lctx clxp); repl clxp rctx) - | "%calltrace" | "%ct" -> (print_eval_trace (); repl clxp rctx) + | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) + | "%elabtrace" | "%et" -> (print_lexp_trace None; repl clxp rctx)
(* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> (
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -38,7 +38,6 @@ open Lexp
open Debruijn open Env (* get_rte_variable *) -open Printf
let builtin_error loc msg = msg_error "BUILT-IN" loc msg; @@ -123,41 +122,6 @@ let type_int = Builtin((dloc, "Int"), type0) let type_float = Builtin((dloc, "Float"), type0) let type_string = Builtin((dloc, "String"), type0)
-(* Builtin of builtin * string * ltype *) -let _generic_binary_iop name f loc (depth: int) (args_val: value_type list) - (ctx: runtime_env) = - - let l, r = match args_val with - | [l; r] -> l, r - | _ -> builtin_error loc (name ^ " expects 2 Integers arguments") in - - match l, r with - | Vint(v), Vint(w) -> Vint(f v w) - | _ -> - value_print l; print_string " "; value_print r; - builtin_error loc (name ^ " expects Integers as arguments") - -let iadd_impl = _generic_binary_iop "Integer::add" (fun a b -> a + b) -let isub_impl = _generic_binary_iop "Integer::sub" (fun a b -> a - b) -let imult_impl = _generic_binary_iop "Integer::mult" (fun a b -> a * b) -let idiv_impl = _generic_binary_iop "Integer::div" (fun a b -> a / b) - - -(* loc is given by the compiler *) -let none_fun : (location -> int -> value_type list -> runtime_env -> value_type) - = (fun loc args_val ctx -> - builtin_error loc "Requested Built-in was not implemented") - -let make_symbol loc depth args_val ctx = - (* symbol is a simple string *) - let lxp = match args_val with - | [r] -> r - | _ -> builtin_error loc ("symbol_ expects 1 argument") in - - match lxp with - | Vstring(str) -> Vsexp(Symbol(loc, str)) - | _ -> builtin_error loc ("symbol_ expects one string as argument") -
(* lexp Imm list *) let olist2tlist_lexp lst ctx = @@ -187,107 +151,6 @@ let rec tlist2olist acc expr = value_print expr; builtin_error dloc "List conversion failure'"
-let make_node loc depth args_val ctx = - - let op, tlist = match args_val with - | [Vsexp(op); lst] -> op, lst - | op::_ -> - builtin_error loc - ("node_ expects one 'Sexp' got " ^ (value_name op)) - | _ -> typer_unreachable "-" in - - (* value_print tlist; print_string "\n"; *) - - let args = tlist2olist [] tlist in - - let s = List.map (fun g -> match g with - | Vsexp(sxp) -> sxp - (* eval transform sexp into those... *) - | Vint (i) -> Integer(dloc, i) - | Vstring (s) -> String(dloc, s) - | _ -> - print_rte_ctx ctx; - print_string (value_name g); print_string "\n"; - value_print g; print_string "\n"; - builtin_error loc ("node_ expects 'List Sexp' second as arguments")) args in - - Vsexp(Node(op, s)) - -let make_string loc depth args_val ctx = - let lxp = match args_val with - | [r] -> r - | _ -> builtin_error loc ("string_ expects 1 argument") in - - match lxp with - | Vstring(str) -> Vsexp(String(loc, str)) - | _ -> builtin_error loc ("string_ expects one string as argument") - -let make_integer loc depth args_val ctx = - let lxp = match args_val with - | [r] -> r - | _ -> builtin_error loc ("integer_ expects 1 argument") in - - match lxp with - | Vint(str) -> Vsexp(Integer(loc, str)) - | _ -> builtin_error loc ("integer_ expects one string as argument") - -let make_float loc depth args_val ctx = Vdummy -let make_block loc depth args_val ctx = Vdummy - -let ttrue = Vcons((dloc, "True"), []) -let tfalse = Vcons((dloc, "False"), []) -let btyper b = if b then ttrue else tfalse - -let string_eq loc depth args_val ctx = - match args_val with - | [Vstring(s1); Vstring(s2)] -> btyper (s1 = s2) - | _ -> builtin_error loc "string_eq expects 2 strings" - -let int_eq loc depth args_val ctx = - match args_val with - | [Vint(s1); Vint(s2)] -> btyper (s1 = s2) - | _ -> builtin_error loc "int_eq expects 2 integer" - -let sexp_eq loc depth args_val ctx = - match args_val with - | [Vsexp (s1); Vsexp (s2)] -> btyper (sexp_equal s1 s2) - | _ -> builtin_error loc "sexp_eq expects 2 sexp" - -let open_impl loc depth args_val ctx = - - let file, mode = match args_val with - | [Vstring(file_name); Vstring(mode)] -> file_name, mode - | _ -> builtin_error loc "open expects 2 strings" in - - (* open file *) (* return a file handle *) - Vcommand(fun () -> - match mode with - | "r" -> Vin(open_in file) - | "w" -> Vout(open_out file) - | _ -> builtin_error loc "wrong open mode") - -let read_impl loc depth args_val ctx = - - let channel = match args_val with - | [Vin(c); _] -> c - | _ -> - List.iter (fun v -> value_print v; print_string "\n") args_val; - builtin_error loc "read expects an in_channel" in - - let line = input_line channel in - Vstring(line) - -let write_impl loc depth args_val ctx = - - let channel, msg = match args_val with - | [Vout(c); Vstring(msg)] -> c, msg - | _ -> - List.iter (fun v -> value_print v) args_val; - builtin_error loc "read expects an out_channel" in - - fprintf channel "%s" msg; - Vdummy - let is_lbuiltin idx ctx = let bsize = 1 in let csize = get_size ctx in @@ -332,8 +195,6 @@ let has_attribute_impl loc largs ctx ftype =
let b = has_property ctx (vi, vn) (ai, an) in
- - let rvar = if b then get_predef "True" ctx else get_predef "False" ctx in rvar, (get_predef "Bool" ctx)
===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -50,7 +50,7 @@ let rec debug_pretokens_print pretoken = print_string " "; let print_info msg loc = print_string msg; - print_string "["; print_loc loc; print_string "]\t" in + print_string "["; loc_print loc; print_string "]\t" in
match pretoken with | Preblock(loc, pts,_) @@ -73,7 +73,7 @@ let rec debug_pretokens_print_all pretokens = let rec debug_sexp_print sexp = let print_info msg loc = print_string msg; - print_string "["; print_loc loc; print_string "]\t" in + print_string "["; loc_print loc; print_string "]\t" in match sexp with | Epsilon -> print_string "Epsilon " (* "ε" *) @@ -117,7 +117,7 @@ let debug_pexp_print ptop = let l = pexp_location ptop in let print_info msg loc pex = print_string msg; print_string "["; - print_loc loc; + loc_print loc; print_string "]\t"; pexp_print pex in match ptop with @@ -135,23 +135,23 @@ let debug_pexp_print ptop = (*| _ -> print_info "Not Impl " l ptop *)
let debug_pexp_decls decls = - let print_loc l = print_string "["; print_loc l; print_string "] " in + let loc_print l = print_string "["; loc_print l; print_string "] " in
List.iter (fun e -> print_string " ";
let _ = match e with | Pexpr ((l, name), pxp) -> - lalign_print_string (pexp_string pxp) 15; - print_loc l; print_string " = "; pexp_print pxp + lalign_print_string (pexp_name pxp) 15; + loc_print l; print_string " = "; pexp_print pxp
| Ptype ((l, name), ptp) -> - lalign_print_string (pexp_string ptp) 15; - print_loc l; print_string " : "; pexp_print ptp + lalign_print_string (pexp_name ptp) 15; + loc_print l; print_string " : "; pexp_print ptp
| Pmcall((l, op), args) -> lalign_print_string "Macro Decls" 15; - print_loc l; sexp_print (Node(Symbol(l, op), args)) in + loc_print l; sexp_print (Node(Symbol(l, op), args)) in
print_string "\n")
@@ -172,8 +172,8 @@ let debug_lexp_decls decls = let ((loc, name), lxp, ltp) = e in
print_string " "; - lalign_print_string (lexp_string lxp) 15; - print_string "["; print_loc loc; print_string "]"; + lalign_print_string (lexp_name lxp) 15; + print_string "["; loc_print loc; print_string "]";
let str = _lexp_str_decls (!debug_ppctx) [e] in
===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -388,9 +388,9 @@ let main () = ) merged));
(* debug lexp parsing once merged *) - let lexps, nctx = try _lexp_decls pexps octx 0 + let lexps, nctx = try lexp_p_decls pexps octx with e -> - print_lexp_trace (); + print_lexp_trace None; internal_error "Fail" in
(* use the new way of parsing expr *) @@ -442,7 +442,7 @@ let main () = with e -> print_string reset; print_rte_ctx (!_global_eval_ctx); - print_eval_trace (); + print_eval_trace None; raise e) in print_string reset;
===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -136,8 +136,3 @@ and elexp_string lxp = "inductive_ " ^ s
| Type -> "Type " - -(* Print Lexp name followed by the lexp in itself, finally throw an exception *) -let elexp_debug_message loc lxp message = - elexp_fatal loc (message ^ "\n" ^ (elexp_name lxp) ^ ": " ^ (elexp_string lxp) ^ "\n"); -
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -42,9 +42,20 @@ open Builtin open Grammar open Debruijn open Env +open Printf (* IO Monad *) module OL = Opslexp
+(* Print a message that look like this: + * + * [X] Fatal [Ln 8, cl 6] EVAL MESSAGE + * > type_namae: type_string *) + +let debug_msg error_type type_name type_string loc expr message = + let msg = message ^ "\n" ^ + " > " ^ (type_name expr) ^ ": " ^ (type_string expr) ^ "\n" in + error_type loc msg + (* eval error are always fatal *) let eval_error loc msg = msg_error "EVAL" loc msg; @@ -63,20 +74,163 @@ let _builtin_lookup = ref SMap.empty
(* Print value name followed by the value in itself, finally throw an exception *) let value_debug_message loc vxp message = - print_string "\n"; - print_string (value_name vxp); print_string ": "; value_print vxp; print_string "\n"; - eval_fatal loc message + debug_msg eval_fatal value_name value_string loc vxp message + +let elexp_debug_message loc elxp message = + debug_msg eval_fatal elexp_name elexp_string loc elxp message + +(* + * Builtins + *) +let none_fun : (location -> OL.pexporlexp list -> value_type list -> runtime_env -> value_type) + = (fun loc args_val ctx -> + eval_error loc "Requested Built-in was not implemented") + +(* Builtin of builtin * string * ltype *) +let _generic_binary_iop name f loc (depth : OL.pexporlexp list) + (args_val: value_type list) (ctx: runtime_env) = + + let l, r = match args_val with + | [l; r] -> l, r + | _ -> builtin_error loc (name ^ " expects 2 Integers arguments") in + + match l, r with + | Vint(v), Vint(w) -> Vint(f v w) + | _ -> + value_print l; print_string " "; value_print r; + builtin_error loc (name ^ " expects Integers as arguments") + +let iadd_impl = _generic_binary_iop "Integer::add" (fun a b -> a + b) +let isub_impl = _generic_binary_iop "Integer::sub" (fun a b -> a - b) +let imult_impl = _generic_binary_iop "Integer::mult" (fun a b -> a * b) +let idiv_impl = _generic_binary_iop "Integer::div" (fun a b -> a / b) + +let make_symbol loc depth args_val ctx = + (* symbol is a simple string *) + let lxp = match args_val with + | [r] -> r + | _ -> builtin_error loc ("symbol_ expects 1 argument") in + + match lxp with + | Vstring(str) -> Vsexp(Symbol(loc, str)) + | _ -> builtin_error loc ("symbol_ expects one string as argument") + +let make_node loc depth args_val ctx = + + let op, tlist = match args_val with + | [Vsexp(op); lst] -> op, lst + | op::_ -> + builtin_error loc + ("node_ expects one 'Sexp' got " ^ (value_name op)) + | _ -> typer_unreachable "-" in + + (* value_print tlist; print_string "\n"; *) + + let args = tlist2olist [] tlist in + + let s = List.map (fun g -> match g with + | Vsexp(sxp) -> sxp + (* eval transform sexp into those... *) + | Vint (i) -> Integer(dloc, i) + | Vstring (s) -> String(dloc, s) + | _ -> + print_rte_ctx ctx; + print_string (value_name g); print_string "\n"; + value_print g; print_string "\n"; + builtin_error loc ("node_ expects 'List Sexp' second as arguments")) args in + + Vsexp(Node(op, s)) + +let make_string loc depth args_val ctx = + let lxp = match args_val with + | [r] -> r + | _ -> builtin_error loc ("string_ expects 1 argument") in + + match lxp with + | Vstring(str) -> Vsexp(String(loc, str)) + | _ -> builtin_error loc ("string_ expects one string as argument") + +let make_integer loc depth args_val ctx = + let lxp = match args_val with + | [r] -> r + | _ -> builtin_error loc ("integer_ expects 1 argument") in + + match lxp with + | Vint(str) -> Vsexp(Integer(loc, str)) + | _ -> builtin_error loc ("integer_ expects one string as argument") + +let make_float loc depth args_val ctx = Vdummy +let make_block loc depth args_val ctx = Vdummy + +let ttrue = Vcons((dloc, "True"), []) +let tfalse = Vcons((dloc, "False"), []) +let btyper b = if b then ttrue else tfalse + +let string_eq loc depth args_val ctx = + match args_val with + | [Vstring(s1); Vstring(s2)] -> btyper (s1 = s2) + | _ -> builtin_error loc "string_eq expects 2 strings" + +let int_eq loc depth args_val ctx = + match args_val with + | [Vint(s1); Vint(s2)] -> btyper (s1 = s2) + | _ -> builtin_error loc "int_eq expects 2 integer" + +let sexp_eq loc depth args_val ctx = + match args_val with + | [Vsexp (s1); Vsexp (s2)] -> btyper (sexp_equal s1 s2) + | _ -> builtin_error loc "sexp_eq expects 2 sexp" + +let open_impl loc depth args_val ctx = + + let file, mode = match args_val with + | [Vstring(file_name); Vstring(mode)] -> file_name, mode + | _ -> builtin_error loc "open expects 2 strings" in + + (* open file *) (* return a file handle *) + Vcommand(fun () -> + match mode with + | "r" -> Vin(open_in file) + | "w" -> Vout(open_out file) + | _ -> builtin_error loc "wrong open mode") + +let read_impl loc depth args_val ctx = + + let channel = match args_val with + | [Vin(c); _] -> c + | _ -> + List.iter (fun v -> value_print v; print_string "\n") args_val; + builtin_error loc "read expects an in_channel" in + + let line = input_line channel in + Vstring(line) + +let write_impl loc depth args_val ctx = + + let channel, msg = match args_val with + | [Vout(c); Vstring(msg)] -> c, msg + | _ -> + List.iter (fun v -> value_print v) args_val; + builtin_error loc "read expects an out_channel" in + + fprintf channel "%s" msg; + Vdummy
(* This is an internal definition * 'i' is the recursion depth used to print the call trace *) -let rec _eval lxp (ctx : Env.runtime_env) i: (value_type) = +let rec _eval lxp (ctx : Env.runtime_env) trace: (value_type) = + + let trace = ((OL.Elexp lxp)::trace) in let tloc = elexp_location lxp in + let eval lxp ctx = _eval lxp ctx trace in
- (if i > (!_eval_max_recursion_depth) then + (if (List.length trace) > (!_eval_max_recursion_depth) then eval_fatal tloc "Recursion Depth exceeded");
- _global_eval_ctx := ctx; (* Allow us to print the latest used environment *) - _global_eval_trace := (i, tloc, lxp)::!_global_eval_trace; + (* Save current trace in a global variable. If an error occur, + we will be able to retrieve the most recent trace and context *) + _global_eval_ctx := ctx; + _global_eval_trace := trace;
match lxp with (* Leafs *) @@ -96,15 +250,15 @@ let rec _eval lxp (ctx : Env.runtime_env) i: (value_type) = (* Nodes *) (* ---------------- *) | Let(_, decls, inst) -> - let nctx = _eval_decls decls ctx i in - _eval inst nctx (i + 1) + let nctx = _eval_decls decls ctx trace in + eval inst nctx
(* Function call *) - | Call (lname, args) -> eval_call ctx i lname args + | Call (lname, args) -> eval_call ctx trace lname args
(* Case *) | Case (loc, target, pat, dflt) - -> (eval_case ctx i loc target pat dflt) + -> (eval_case ctx trace loc target pat dflt)
| Type -> Vcons((tloc, "Unit"), [])
@@ -112,17 +266,18 @@ let rec _eval lxp (ctx : Env.runtime_env) i: (value_type) = and get_predef_eval name ctx = let r = (get_rte_size ctx) - !builtin_size in let v = mkSusp (get_predef_raw name) (S.shift r) in - _eval (OL.erase_type v) ctx 0 + _eval (OL.erase_type v) ctx []
and eval_var ctx lxp v = let ((loc, name), idx) = v in try get_rte_variable (Some name) (idx) ctx with e -> - eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ") + elexp_debug_message loc lxp + ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ")
and eval_call ctx i lname eargs = let loc = elexp_location lname in - let f = _eval lname ctx (i + 1) in + let f = _eval lname ctx i in
(* standard function *) let rec eval_call f args ctx = @@ -134,26 +289,26 @@ and eval_call ctx i lname eargs = (* we add an argument to the closure *) | Closure (n, lxp, ctx), hd::tl -> let nctx = add_rte_variable (Some n) hd ctx in - let ret = _eval lxp nctx (i + 1) in + let ret = _eval lxp nctx i in eval_call ret tl nctx
| Vbuiltin (str), args -> (* lookup the built-in implementation and call it *) - (get_builtin_impl str loc) loc (i + 1) args ctx + (get_builtin_impl str loc) loc i args ctx
(* return result of eval *) | _, [] -> f
- | _ -> debug_msg (value_print f); - eval_error loc "Cannot eval function" in + | _ -> + value_debug_message loc f "Cannot eval function" in
(* eval function here *) - let args = List.map (fun e -> _eval e ctx (i + 1)) eargs in + let args = List.map (fun e -> _eval e ctx i) eargs in eval_call f args ctx
and eval_case ctx i loc target pat dflt = (* Eval target *) - let v = _eval target ctx (i + 1) in + let v = _eval target ctx i in
(* extract constructor name and arguments *) let ctor_name, args = match v with @@ -178,21 +333,22 @@ and eval_case ctx i loc target pat dflt = | [], [] -> nctx in
let nctx = fold2 ctx pat_args args in - _eval exp nctx (i + 1) + _eval exp nctx i
(* Run default *) with Not_found -> (match dflt with - | Some lxp -> _eval lxp ctx (i + 1) + | Some lxp -> _eval lxp ctx i | _ -> eval_error loc "Match Failure")
and build_arg_list args ctx i = (* _eval every args *) - let arg_val = List.map (fun (k, e) -> _eval e ctx (i + 1)) args in + let arg_val = List.map (fun (k, e) -> _eval e ctx i) args in
(* Add args inside context *) List.fold_left (fun c v -> add_rte_variable None v c) ctx arg_val
-and eval_decls decls ctx = _eval_decls decls ctx 0 +and eval_decls decls ctx = _eval_decls decls ctx [] + and _eval_decls (decls: (vdef * elexp) list) (ctx: runtime_env) i: runtime_env =
@@ -203,7 +359,7 @@ and _eval_decls (decls: (vdef * elexp) list) add_rte_variable (Some name) Vdummy ctx) ctx decls in
List.iteri (fun idx ((_, name), lxp) -> - let v = _eval lxp nctx (i + 1) in + let v = _eval lxp nctx i in let offset = n - idx in ignore (set_rte_variable offset (Some name) v nctx)) decls;
@@ -237,7 +393,7 @@ and typer_builtins_impl = [ ("write" , write_impl); ]
-and bind_impl loc depth args_val ctx = +and bind_impl loc (depth : OL.pexporlexp list) args_val ctx =
let io, cb = match args_val with | [io; callback] -> io, callback @@ -307,7 +463,7 @@ and get_builtin_impl str loc = (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args ctx = - let eval a b = _eval a b 1 in + let eval a b = _eval a b [] in let sxp, nd, sym, str, it, flt, blk, rctx = match args with | [sxp; Closure(_, nd, rctx); Closure(_, sym, _); Closure(_, str, _); Closure(_, it, _); @@ -317,9 +473,7 @@ and sexp_dispatch loc depth args ctx =
let sxp = match sxp with | Vsexp(sxp) -> sxp - | _ -> debug_msg ( print_string "\n"; - value_print sxp; print_string "\n"); - eval_error loc "sexp_dispatch expects a Sexp as 1st arg" in + | _ -> value_debug_message loc sxp "sexp_dispatch expects a Sexp as 1st arg" in
match sxp with | Node (op, s) ->( @@ -348,12 +502,43 @@ and print_eval_result i lxp = print_string "] >> "; value_print lxp; print_string "\n";
+and print_trace2 title trace default = + (* If no trace is provided take the most revent one *) + let trace = match trace with + | Some trace -> trace + | None -> default in + + (* Trace is upside down by default *) + let trace = List.rev trace in + + (* Now eval trace and lparse trace are the same *) + let print_trace = (fun type_name type_string type_loc i expr -> + (* Print location info *) + print_string (" [" ^ (loc_string (type_loc expr)) ^ "] "); + + (* Print call trace visualization *) + Fmt._print_ct_tree i; print_string "+- "; + + (* Print element *) + print_string ((type_name expr) ^ ": " ^ (type_string expr) ^ "\n") + ) in + + let lexp_trace = print_trace pexp_name pexp_string pexp_location in + let elexp_trace = print_trace elexp_name elexp_string elexp_location in + + (* Print the trace*) + print_string (Fmt.make_title title); + print_string (Fmt.make_sep '-'); + let _ = List.iteri (fun i expr -> + match expr with + | OL.Pexp p -> lexp_trace i p + | OL.Elexp e -> elexp_trace i e) trace in + print_string (Fmt.make_sep '=')
-and print_eval_trace () = - print_trace " EVAL TRACE " 50 elexp_name elexp_print !_global_eval_trace +and print_eval_trace trace = + print_trace2 " EVAL TRACE " trace !_global_eval_trace
-let eval lxp ctx = - _eval lxp ctx 1 +let eval lxp ctx = _eval lxp ctx []
let debug_eval lxp ctx = try @@ -361,7 +546,7 @@ let debug_eval lxp ctx = eval lxp ctx with e -> ( print_rte_ctx (!_global_eval_ctx); - print_eval_trace (); + print_eval_trace None; raise e)
(* Eval a list of lexp *)
===================================== src/fmt.ml ===================================== --- a/src/fmt.ml +++ b/src/fmt.ml @@ -31,8 +31,8 @@ * ---------------------------------------------------------------------------*)
(* Compute the number of character needed to print an integer*) -let str_size_int value = - (int_of_float (log10 (float value))) + 1 +let str_size_int v = + (int_of_float (log10 (float v))) + 1
(* print n char 'c' *) let rec make_line c n = String.make n c @@ -42,56 +42,54 @@ let cut_int (v:int) (start:int) (len:int): int = 0
(* RALIGN * ----------------------- *) -let ralign_generic get_size print_str print_elem cut_elem elem col = +let ralign_generic get_size elem_string cut_elem elem col = let n = get_size elem in - if n > col then - print_elem (cut_elem elem 0 col) - else begin - print_str (make_line ' ' (col - n)); - print_elem elem; end + if n > col then elem_string (cut_elem elem 0 col) + else (make_line ' ' (col - n)) ^ (elem_string elem)
-let ralign_print_string = - ralign_generic String.length print_string print_string String.sub +let ralign_string = + ralign_generic String.length (fun s -> s) String.sub
-let ralign_print_int = - ralign_generic str_size_int print_string print_int cut_int +let ralign_int = + ralign_generic str_size_int string_of_int cut_int
+let ralign_print_int i c = print_string (ralign_int i c) +let ralign_print_string s c = print_string (ralign_string s c)
(* LALIGN * ----------------------- *) -let lalign_generic get_size print_str print_elem cut_elem elem col = +let lalign_generic get_size elem_string cut_elem elem col = let n = get_size elem in - if n > col then - print_elem (cut_elem elem 0 col) - else begin - print_elem elem; - print_str (make_line ' ' (col - n)); end + if n > col then elem_string (cut_elem elem 0 col) + else (elem_string elem) ^ (make_line ' ' (col - n))
-let lalign_print_string = - lalign_generic String.length print_string print_string String.sub +let lalign_string = + lalign_generic String.length (fun s -> s) String.sub
-let lalign_print_int = - lalign_generic str_size_int print_string print_int cut_int +let lalign_int = + lalign_generic str_size_int string_of_int cut_int + +let lalign_print_int i c = print_string (lalign_int i c) +let lalign_print_string s c = print_string (lalign_string s c)
(* CALIGN * ----------------------- *) -let calign_generic get_size print_str print_elem cut_elem elem col = +let calign_generic get_size elem_string cut_elem elem col = let n = get_size elem in let p = n mod 2 in let sep_n = (col - n) / 2 in
- if n > col then - print_elem (cut_elem elem 0 col) - else begin - print_str (make_line ' ' sep_n); - print_elem elem; - print_str (make_line ' ' (sep_n + p)); end + if n > col then elem_string (cut_elem elem 0 col) + else (make_line ' ' sep_n) ^ (elem_string elem) ^ (make_line ' ' (sep_n + p)) + +let calign_string = + calign_generic String.length (fun s -> s) String.sub
-let calign_print_string = - calign_generic String.length print_string print_string String.sub +let calign_int = + calign_generic str_size_int string_of_int cut_int
-let calign_print_int = - calign_generic str_size_int print_string print_int cut_int +let calign_print_int i c = print_string (calign_int i c) +let calign_print_string s c = print_string (calign_string s c)
(* Table Printing helper *) let make_title title =
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -56,6 +56,7 @@ module SU = Subst let make_var name index loc = Var(((loc, name), index))
+(* dummies *) let dlxp = type0 let dltype = type0 let dloc = dummy_location @@ -71,9 +72,10 @@ let btl_folder = ref "./btl/"
(* Print Lexp name followed by the lexp in itself, finally throw an exception *) let lexp_debug_message loc lxp message = - print_string "\n"; - print_string (lexp_string lxp); print_string ": "; lexp_print lxp; print_string "\n"; - lexp_fatal loc message + debug_msg lexp_fatal lexp_name lexp_string loc lxp message + +let pexp_debug_message loc lxp message = + debug_msg lexp_fatal pexp_name pexp_string loc lxp message
let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = @@ -175,16 +177,16 @@ let build_var name ctx = let type0_idx = senv_lookup name ctx in Var((dloc, name), type0_idx)
-let rec lexp_p_infer (p : pexp) (ctx : elab_context): lexp * ltype = - _lexp_p_infer p ctx 1 - -and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = +let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype =
- let lexp_infer p ctx = _lexp_p_infer p ctx (i + 1) in + let trace = ((OL.Pexp p)::trace) in let tloc = pexp_location p in + let lexp_infer p ctx = _lexp_p_infer p ctx trace in
+ (* Save current trace in a global variable. If an error occur, + we will be able to retrieve the most recent trace and context *) _global_lexp_ctx := ctx; - _global_lexp_trace := (i, tloc, p)::!_global_lexp_trace; + _global_lexp_trace := trace;
match p with (* Block/String/Integer/Float *) @@ -213,9 +215,9 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =
(* Let, Variable declaration + local scope *) | Plet(loc, decls, body) -> - let decls, nctx = _lexp_decls decls ctx i in + let decls, nctx = _lexp_decls decls ctx trace in let bdy, ltp = lexp_infer body nctx in - (lexp_let_decls decls bdy nctx i), ltp + (lexp_let_decls decls bdy nctx trace), ltp
(* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) -> @@ -233,7 +235,7 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = (* (arg_kind * pvar * pexp option) list *) let formal = List.map (fun (kind, var, opxp) -> let ltp, _ = match opxp with - | Some pxp -> _lexp_p_infer pxp !nctx (i + 1) + | Some pxp -> _lexp_p_infer pxp !nctx trace | None -> dltype, dltype in
nctx := env_extend !nctx var Variable ltp; @@ -248,7 +250,7 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = * (not always type0). *) type0 (List.rev formal) in
- let map_ctor = lexp_parse_inductive ctors nctx i in + let map_ctor = lexp_parse_inductive ctors nctx trace in let v = Inductive(tloc, label, formal, map_ctor) in v, ltp
@@ -267,7 +269,7 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = Lambda(kind, var, ltp, lbody), lambda_type
| Pcall (fname, _args) -> - lexp_call fname _args ctx i + lexp_call fname _args ctx trace
(* Pcons *) | Pcons(t, sym) -> @@ -315,14 +317,13 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =
(* Pcase: we can infer iff `patterns` is not empty *) | Pcase (loc, target, patterns) -> - lexp_case None (loc, target, patterns) ctx i + lexp_case None (loc, target, patterns) ctx trace
| Phastype (_, pxp, ptp) -> let ltp, _ = lexp_infer ptp ctx in - (_lexp_p_check pxp ltp ctx (i + 1)), ltp + (_lexp_p_check pxp ltp ctx trace), ltp
- | _ -> pexp_print p; print_string "\n"; - lexp_fatal tloc "Unhandled Pexp" + | _ -> pexp_debug_message tloc p "Unhandled Pexp"
and lexp_let_decls decls (body: lexp) ctx i = @@ -331,56 +332,48 @@ and lexp_let_decls decls (body: lexp) ctx i = List.fold_left (fun lxp decls -> Let(dloc, decls, lxp)) body decls
-and lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context): lexp = - _lexp_p_check p t ctx 1 +and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp =
-and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) i: lexp = + let trace = ((OL.Pexp p)::trace) in let tloc = pexp_location p in + let lexp_infer p ctx = _lexp_p_infer p ctx trace in + let lexp_check p ltp ctx = _lexp_p_check p ltp ctx trace in
+ (* Safe current trace in a global variable. If an error occur, + we will be able to retrieve the most recent trace and context *) _global_lexp_ctx := ctx; - _global_lexp_trace := (i, tloc, p)::!_global_lexp_trace; + _global_lexp_trace := trace;
match p with (* This case cannot be inferred *) | Plambda (kind, var, None, body) ->( (* Read var type from the provided type *) let ltp, lbtp = match nosusp t with - | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp - | _ -> lexp_error tloc "Type does not match"; dltype, dltype in + | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp + | expr -> + lexp_debug_message tloc expr "Expected Type Arrow ( _ -> _ )" in
let nctx = env_extend ctx var Variable ltp in - let lbody = _lexp_p_check body lbtp nctx (i + 1) in + let lbody = lexp_check body lbtp nctx in
Lambda(kind, var, ltp, lbody))
(* This is mostly for the case where no branches are provided *) | Pcase (loc, target, patterns) -> - let lxp, _ = lexp_case (Some t) (loc, target, patterns) ctx i in + let lxp, _ = lexp_case (Some t) (loc, target, patterns) ctx trace in lxp
(* handle pcall here * ) | Pcall (fname, _args) -> *)
- | _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in - e (* - match e with - (* Built-in is a dummy function with no type. We cannot check - * Built-in *) - | Builtin _ -> e - | _ -> - (if OL.conv_p inferred_t t then () else debug_msg ( - print_string "1 exp "; lexp_print e; print_string "\n"; - print_string "2 inf "; lexp_print inferred_t; print_string "\n"; - print_string "3 Ann "; lexp_print t; print_string "\n"; - lexp_warning tloc "Type Mismatch inferred != Annotation")); - e*) + | _ -> let (e, inferred_t) = lexp_infer p ctx in e
(* Lexp.case cam be checked and inferred *) and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = (* FIXME: check if case is exhaustive *) (* Helpers *) - let lexp_infer p ctx = _lexp_p_infer p ctx (i + 1) in
+ let lexp_infer p ctx = _lexp_p_infer p ctx i in let rtype = ref rtype in
let type_check ltp = @@ -407,7 +400,7 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = (* Read patterns one by one *) let fold_fun (merged, dflt) (pat, exp) = (* Create pattern context *) - let (name, iloc, arg), nctx = lexp_read_pattern pat exp tlxp ctx in + let (name, iloc, arg), nctx = lexp_read_pattern pat exp tlxp ctx i in
(* parse using pattern context *) let exp, ltp = lexp_infer exp nctx in @@ -442,10 +435,13 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = and lexp_call (func: pexp) (sargs: sexp list) ctx i = let loc = pexp_location func in
+ let lexp_infer p ctx = _lexp_p_infer p ctx i in + let lexp_check p ltp ctx = _lexp_p_check p ltp ctx i in + let from_lctx ctx = try (from_lctx ctx) with e ->( lexp_error loc "Could not convert lexp context into rte context"; - print_eval_trace (); + print_eval_trace None; raise e) in
(* Vanilla : sqr is inferred and (lambda x -> x * x) is returned @@ -454,7 +450,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = * Anonymous : lambda *)
(* retrieve function's body (sqr 3) sqr is a Pvar() *) - let body, ltp = _lexp_p_infer func ctx (i + 1) in + let body, ltp = lexp_infer func ctx in let ltp = nosusp ltp in
let rec handle_fun_args largs sargs ltp = match sargs with @@ -465,7 +461,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | Arrow (ak, Some (_, aname'), arg_type, _, ret_type) when aname = aname' -> let parg = pexp_parse sarg in - let larg = _lexp_p_check parg arg_type ctx i in + let larg = lexp_check parg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) | _ -> lexp_fatal (sexp_location sarg) @@ -483,11 +479,10 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = lexp_fatal (sexp_location sarg) "Expected non-explicit arg" | t -> - lexp_print t; print_string "\n"; print_lexp_ctx (ectx_to_lctx ctx); - lexp_fatal (sexp_location sarg) - ("Explicit arg `" ^ sexp_string sarg - ^ "` to non-function (type = " ^ lexp_string ltp ^ ")")) in + lexp_debug_message (sexp_location sarg) t + ("Explicit arg `" ^ sexp_string sarg ^ + "` to non-function (type = " ^ lexp_string ltp ^ ")")) in
let handle_funcall () = (* Here we use lexp_whnf on actual code, but it's OK @@ -502,7 +497,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
| true, [String (_, str); stp] -> let ptp = pexp_parse stp in - let ltp, _ = _lexp_p_infer ptp ctx (i + 1) in + let ltp, _ = lexp_infer ptp ctx in Builtin((loc, str), ltp), ltp
| true, _ -> @@ -519,7 +514,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = Call (body, List.rev largs), ret_type in
let handle_macro_call () = - let sxp = match lexp_expand_macro body sargs ctx with + let sxp = match lexp_expand_macro body sargs ctx i with | Vsexp(sxp) -> sxp (* Those are sexp converted by the eval function *) | Vint(i) -> Integer(dloc, i) @@ -529,7 +524,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = value_debug_message loc v "Macro_ expects '(List Sexp) -> Sexp'" in
let pxp = pexp_parse sxp in - _lexp_p_infer pxp ctx (i + 1) in + lexp_infer pxp ctx in
(* This is the builtin Macro type *) let macro_type, macro_disp = match get_predef_option "Macro" ctx with @@ -557,7 +552,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | _ -> handle_funcall ()
(* Read a pattern and create the equivalent representation *) -and lexp_read_pattern pattern exp target ctx: +and lexp_read_pattern pattern exp target ctx trace: ((string * location * (arg_kind * vdef option) list) * elab_context) =
match pattern with @@ -585,7 +580,7 @@ and lexp_read_pattern pattern exp target ctx:
| Ppatcons (ctor, args) -> (* Get cons argument types. *) - let lctor, _ = lexp_p_infer ctor ctx in + let lctor, _ = _lexp_p_infer ctor ctx trace in match OL.lexp_whnf lctor (ectx_to_lctx ctx) with | Cons (it, (loc, cons_name)) -> let cons_args = match OL.lexp_whnf it (ectx_to_lctx ctx) with @@ -657,7 +652,7 @@ and lexp_read_pattern_args args (args_type : lexp list) ctx:
(* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx i = - let lexp_parse p ctx = _lexp_p_infer p ctx (i + 1) in + let lexp_parse p ctx = _lexp_p_infer p ctx i in
let make_args (args:(arg_kind * pvar option * pexp) list) ctx : (arg_kind * vdef option * ltype) list = @@ -680,7 +675,7 @@ and lexp_parse_inductive ctors ctx i =
(* Macro declaration handling, return a list of declarations * to be processed *) -and lexp_expand_macro macro_funct sargs ctx = +and lexp_expand_macro macro_funct sargs ctx trace =
(* Build the function to be called *) let macro_expand = get_predef "expand_macro_" ctx in @@ -691,9 +686,9 @@ and lexp_expand_macro macro_funct sargs ctx = let rctx = from_lctx ctx in
(* eval macro *) - _global_eval_trace := []; - let vxp = try eval emacro rctx - with e -> print_eval_trace (); raise e in + _global_eval_trace := trace; + let vxp = try _eval emacro rctx trace + with e -> print_eval_trace None; raise e in (* Return results *) (* Vint/Vstring/Vfloat might need to be converted to sexp *) vxp @@ -716,7 +711,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = | Var((_, "add-attribute"), _) ->( (* Builtin macro *) let pargs = List.map pexp_parse sargs in - let largs = _lexp_parse_all pargs ctx 0 in + let largs = _lexp_parse_all pargs ctx [] in
(* extract info *) let var, att, fn = match largs with @@ -730,7 +725,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = [], ctx)
| _ ->( - let ret = lexp_expand_macro body sargs ctx in + let ret = lexp_expand_macro body sargs ctx [] in
(* convert typer list to ocaml *) let decls = tlist2olist [] ret in @@ -747,7 +742,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = lexp_fatal loc "Macro not found"
(* Parse let declaration *) -and lexp_p_decls decls ctx = _lexp_decls decls ctx 0 +and lexp_p_decls decls ctx = _lexp_decls decls ctx []
and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) @@ -757,7 +752,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (fun ((_, vname) as v, pexp, ltp) map -> let i = senv_lookup vname nctx in let adjusted_ltp = push_susp ltp (S.shift (i + 1)) in - IntMap.add i (v, lexp_p_check pexp adjusted_ltp nctx, ltp) + IntMap.add i (v, _lexp_p_check pexp adjusted_ltp nctx [], ltp) map) defs IntMap.empty in let decls = List.rev (List.map (fun (_, d) -> d) (IntMap.bindings declmap)) in @@ -781,7 +776,7 @@ and lexp_decls_1 [], [], nctx
| Ptype ((l, vname) as v, ptp) :: pdecls - -> let (ltp, lsort) = lexp_p_infer ptp nctx in + -> let (ltp, lsort) = _lexp_p_infer ptp nctx [] in if SMap.mem vname pending_decls then (lexp_error l ("Variable `" ^ vname ^ "` declared twice!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) @@ -799,7 +794,7 @@ and lexp_decls_1 when SMap.is_empty pending_decls -> assert (pending_defs == []); assert (ectx == nctx); - let (lexp, ltp) = lexp_p_infer pexp nctx in + let (lexp, ltp) = _lexp_p_infer pexp nctx [] in (* Lexp decls are always recursive, so we have to shift by 1 to account * for the extra var (ourselves). *) [(v, push_susp lexp (S.shift 1), ltp)], pdecls, @@ -845,22 +840,21 @@ and _lexp_decls pdecls ctx i: ((vdef * lexp * ltype) list list * elab_context) = decls :: declss, nnctx
and lexp_decls_toplevel decls ctx = - _lexp_decls decls ctx 1 + _lexp_decls decls ctx []
and _lexp_parse_all (p: pexp list) (ctx: elab_context) i : lexp list =
let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with | [] -> (List.rev acc) - | pe :: plst -> let lxp, _ = _lexp_p_infer pe ctx (i + 1) in + | pe :: plst -> let lxp, _ = _lexp_p_infer pe ctx i in (loop plst ctx (lxp::acc)) in
(loop p ctx [])
-and print_lexp_trace () = - print_trace " LEXP TRACE " 50 pexp_string pexp_print !_global_lexp_trace - +and print_lexp_trace (trace : (OL.pexporlexp list) option) = + print_trace2 " ELAB TRACE " trace !_global_lexp_trace (* Only print var info *) and lexp_print_var_info ctx = let ((m, _), env, _) = ctx in @@ -879,8 +873,14 @@ and lexp_print_var_info ctx = print_string "\n") done
+(* Those call reinitialize the calltrace *) +let lexp_parse_all p ctx = _lexp_parse_all p ctx [] + +let lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context): lexp = + _lexp_p_check p t ctx []
-let lexp_parse_all p ctx = _lexp_parse_all p ctx 1 +let lexp_p_infer (p : pexp) (ctx : elab_context): lexp * ltype = + _lexp_p_infer p ctx []
(* Default context with builtin types
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -460,3 +460,9 @@ and clean_map cases = (l, (clean_arg_list args), (erase_type expr))) cases
+(* Custom type to make trace uniform between lparse and eval *) +type pexporlexp = + | Pexp of P.pexp + | Elexp of E.elexp + +
===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -44,12 +44,10 @@ type vref = vdef * db_index type bottom = | B_o_t_t_o_m_ of bottom
(* print debug info *) -let print_loc (loc: location) = - (*print_string loc.file; *) (* Printing the file is too much*) - print_string "ln "; - Fmt.ralign_print_int loc.line 3; - print_string ", cl "; - Fmt.ralign_print_int loc.column 3 +let loc_string loc = + "Ln " ^ (Fmt.ralign_int loc.line 3) ^ ", cl " ^ (Fmt.ralign_int loc.column 3) + +let loc_print loc = print_string (loc_string loc)
(* * -1 - Nothing (* During testing we may want to produce errors *) @@ -77,17 +75,16 @@ let typer_unreachable s = raise (Unreachable_error s) * | ------------------------------------------------ *)
+ + + (* File is not printed because currently we parse only one file... *) (* Section is the name of the compilation step [for debugging] *) (* 'prerr' output is ugly *) let msg_message lvl kind section (loc: location) msg = if lvl <= !_typer_verbose then( - print_string (" " ^ kind); - print_string " ["; print_loc loc; print_string "] "; - Fmt.lalign_print_string section 8; - print_string (" " ^ msg); - print_newline ()) else () - + let info = " " ^ kind ^ " [" ^ loc_string loc ^ "] " ^ (Fmt.lalign_string section 8) in + print_string (info ^ " " ^ msg ^ "\n")) else ()
let msg_fatal s l m = msg_message 0 "[X] Fatal " s l m; @@ -115,7 +112,7 @@ let print_trace name max elem_to_string print_elem trace =
let racc = List.rev trace in Fmt.print_last max racc (fun j (i, l, g) -> - print_string " ["; print_loc l; print_string "] "; + print_string " ["; loc_print l; print_string "] "; Fmt._print_ct_tree i; print_string "+- "; print_string (elem_to_string g); print_string ": "; print_elem g; print_string "\n");
View it on GitLab: https://gitlab.com/monnier/typer/compare/b57544ca2b8497fbd6c1783690cc5565537...
Afficher les réponses par date