Setepenre pushed to branch master at Stefan / Typer
Commits: 5496ae2c by Pierre Delaunay at 2016-10-12T02:10:14-04:00 * new file: samples/error.typer - Erroneous typer code to test out error messages
* src/lparse.ml * src/eval.ml: - tinking with error messages: replaced lexp_error/debruijn_error/eval_fatal/... by simple error/fatal/warning/... - added typer call trace - removed `reset_eval_trace`
* added new functions - value_fatal/elexp_fatal/pexp_fatal/pexp_warning/etc.. Those print an error message then print the expression causing the error. Example:
% [Ln 45, cl 12] ./samples/error.typer % [!] Error LPARSE Lambda require type annotation % > Plambda: (lambda_->_ n n) % > Root: (lambda_->_ n n)
* src/util.ml - removed unused print_trace (old code)
* src/opslexp.ml - Added `pol_string` and `pol_name`
* src/debruijn.ml * src/env.ml - `print_rte_ctx` and `print_lexp_ctx` skip builtins (shorter dump) `dump_rte_ctx` and `dump_lexp_ctx`can be used to print the whole context
* src/REPL.ml - added %typertrace option - `%who` and `%info` use print_..._ctx - `%who all` and `%info all` use dump_..._ctx
- - - - -
15 changed files:
- + samples/error.typer - samples/nat.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/util.ml - tests/eval_test.ml - tests/macro_test.ml
Changes:
===================================== samples/error.typer ===================================== --- /dev/null +++ b/samples/error.typer @@ -0,0 +1,112 @@ +%(* +% * Typer Compiler +% * +% * --------------------------------------------------------------------------- +% * +% * Copyright (C) 2011-2016 Free Software Foundation, Inc. +% * +% * Author: Pierre Delaunay pierre.delaunay@hec.ca +% * Keywords: languages, lisp, dependent types. +% * +% * This file is part of Typer. +% * +% * Typer is free software; you can redistribute it and/or modify it under the +% * terms of the GNU General Public License as published by the Free Software +% * Foundation, either version 3 of the License, or (at your option) any +% * later version. +% * +% * Typer is distributed in the hope that it will be useful, but WITHOUT ANY +% * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +% * FOR A PARTICULAR PURPOSE. See the GNU General Public License for +% * more details. +% * +% * You should have received a copy of the GNU General Public License along +% * with this program. If not, see http://www.gnu.org/licenses/. +% * +% * --------------------------------------------------------------------------- +% * +% * Description: +% * Erroneous typer code to test out error messages +% * Fatal errors are at the end of the file +%* +% * --------------------------------------------------------------------------- *) + +% [!] Error [Ln 10, cl 29] LPARSE The variable: "b" was not declared +% > Pvar: b +% > Root: + +a = lambda (n : Int) -> n + b; +v = (a 2); + +% [!] Error [Ln 14, cl 12] LPARSE Lambda require type annotation +% > Plambda: (lambda_->_ n n) +% > Root: + +m = lambda n -> n; + +% [!] Error [Ln 27, cl 28] LPARSE Constructor "cons3" does not exist +% > inductive_: (inductive_ e (cons1) (cons2 Int)) +% > Root: + +idt = inductive_ (idt) (cons1) (cons2 Int); +cons1 = inductive-cons idt cons1; +cons2 = inductive-cons idt cons2; +cons3 = inductive-cons idt cons3; + +% [!] Error [Ln 32, cl 28] LPARSE Not an Inductive Type +% > Builtin: Int +% > Root: + +cons4 = inductive-cons Int cons3; + +% /!\ Warning [Ln 70, cl 17] LPARSE Pattern cons2 is a duplicate. It will override previous pattern. + +fun2 : idt -> Int; +fun2 n = case n + | cons1 => 1 + | cons2 i => 2 + | cons2 j => 3; + +% [X] Fatal [Ln 77, cl 12] LPARSE Explicit arg `2` to non-function (type = Int) +% > Builtin: Int +% > Root: + +% h = fun2 1 2; + +% [X] Fatal [Ln 6, cl 6] LPARSE Macro_ expects `(List Sexp) -> Sexp` +% > Vcons: (cons 2 (nil)) +% > Root: n + +% m = Macro_ (lambda (n : Int) -> n); +% v = (m 2); + +% [X] Fatal [Ln 43, cl 5] LPARSE Expected Type Arrow ( _ -> _ ) +% > Var: Int +% > Root: + +% fun : Int; +% fun n = n + 2; + + +% [!] Error [Ln 0, cl 0] LPARSE Error while type-checking +% > lambda: (lambda_->_ (_:_ n idt) (case_ n (_=>_ cons1 1) (_=>_ cons2c ""))) +% > Root: +% [!] Error [Ln 87, cl 1] LPARSE `fun4` defined but not declared! +% [!] Error [Ln 86, cl 1] LPARSE Variable `fun4` declared but not defined! + +% idtb = inductive_ (idtb) (cons1b) (cons2b Int); +% cons1b = inductive-cons idtb cons1b; +% cons2b = inductive-cons idtb cons2b; + +% fun4 : idt -> Int; +% fun4 n = case n +% | cons1 => 1 +% | cons2c => 2; + + +% [!] Error [Ln 73, cl 16] TC Unsupported immediate value! + +% fun3 : idt -> Int; +% fun3 n = case n +% | cons1 => 1 +% | cons2 i => "AB"; \ No newline at end of file
===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -32,4 +32,4 @@ even = lambda (n : Nat) -> case n a = odd one; b = even one; c = odd two; -d = even two; \ No newline at end of file +d = even two;
===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -182,8 +182,9 @@ let _help_msg = " %quit (%q) : leave REPL %who (%w) : print runtime environment %info (%i) : print elaboration environment - %calltrace (%ct): print call trace of last call + %calltrace (%ct): print eval trace of last call %elabtrace (%et): print elaboration trace + %typertrace (%tt): print typer trace %readfile : read a Typer file %help (%h) : print help " @@ -216,10 +217,9 @@ let rec repl i clxp rctx = (* Check special keywords *) | "%quit" | "%q" -> () | "%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 None; repl clxp rctx) - | "%elabtrace" | "%et" -> (print_lexp_trace None; repl clxp rctx) + | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) + | "%elabtrace" | "%et" -> (print_lexp_trace None; repl clxp rctx) + | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx)
(* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( @@ -227,6 +227,17 @@ let rec repl i clxp rctx = | "%readfile"::args -> let (i, clxp, rctx) = readfiles args (i, clxp, rctx) false in repl clxp rctx; + | "%who"::args | "%w"::args -> ( + let _ = match args with + | ["all"] -> dump_rte_ctx rctx + | _ -> print_rte_ctx rctx in + repl clxp rctx) + | "%info"::args | "%i"::args -> ( + let _ = match args with + | ["all"] -> dump_lexp_ctx (ectx_to_lctx clxp) + | _ -> print_lexp_ctx (ectx_to_lctx clxp) in + repl clxp rctx) + | cmd::_ -> ieval_error dloc (" "" ^ cmd ^ "" is not a correct repl command"); repl clxp rctx
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -39,12 +39,8 @@ open Lexp open Debruijn open Env (* get_rte_variable *)
-let builtin_error loc msg = - msg_error "BUILT-IN" loc msg; - raise (internal_error msg) - -let builtin_warning loc msg = - msg_warning "BUILT-IN" loc msg +let error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg) +let warning loc msg = msg_warning "BUILT-IN" loc msg
type predef_table = (lexp option ref) SMap.t
@@ -59,8 +55,6 @@ let predef_name = [ "expand_macro_"; ]
-let builtin_size = ref 0 - let default_predef_map : predef_table = (* add predef name, expr will be populated when parsing *) List.fold_left (fun m name -> @@ -71,7 +65,7 @@ let predef_map = ref default_predef_map let get_predef_raw (name: string) : lexp = match !(SMap.find name (!predef_map)) with | Some exp -> exp - | None -> builtin_error dloc ("""^ name ^ "" was not predefined") + | None -> error dloc ("""^ name ^ "" was not predefined")
let get_predef_option (name: string) ctx = let r = (get_size ctx) - !builtin_size - 0 in @@ -149,7 +143,7 @@ let rec tlist2olist acc expr = | _ -> print_string (value_name expr); print_string "\n"; value_print expr; - builtin_error dloc "List conversion failure'" + error dloc "List conversion failure'"
let is_lbuiltin idx ctx = let bsize = 1 in @@ -170,12 +164,12 @@ let get_attribute_impl loc largs ctx ftype =
let (vi, vn), (ai, an) = match largs with | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an) - | _ -> builtin_error loc "get-attribute expects two arguments" in + | _ -> error loc "get-attribute expects two arguments" in
let lxp = get_property ctx (vi, vn) (ai, an) in let ltype = match env_lookup_expr ctx ((loc, an), ai) with | Some ltp -> ltp - | None -> builtin_error loc "not expression available" in + | None -> error loc "not expression available" in
lxp, ltype
@@ -183,7 +177,7 @@ let new_attribute_impl loc largs ctx ftype =
let eltp = match largs with | [eltp] -> eltp - | _ -> builtin_warning loc "new-attribute expects one argument"; type0 in + | _ -> warning loc "new-attribute expects one argument"; type0 in
eltp, ftype
@@ -191,7 +185,7 @@ let has_attribute_impl loc largs ctx ftype =
let (vi, vn), (ai, an) = match largs with | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an) - | _ -> builtin_error loc "has-attribute expects two arguments" in + | _ -> error loc "has-attribute expects two arguments" in
let b = has_property ctx (vi, vn) (ai, an) in
@@ -202,11 +196,11 @@ let declexpr_impl loc largs ctx ftype =
let (vi, vn) = match largs with | [Var((_, vn), vi)] -> (vi, vn) - | _ -> builtin_error loc "declexpr expects one argument" in + | _ -> error loc "declexpr expects one argument" in
let lxp = match env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> lxp - | None -> builtin_error loc "no expr available" in + | None -> error loc "no expr available" in let ltp = env_lookup_type ctx ((loc, vn), vi) in (* FIXME: Unused? *) lxp, ftype
@@ -215,7 +209,7 @@ let decltype_impl loc largs ctx ftype =
let (vi, vn) = match largs with | [Var((_, vn), vi)] -> (vi, vn) - | _ -> builtin_error loc "decltype expects one argument" in + | _ -> error loc "decltype expects one argument" in
let ltype = env_lookup_type ctx ((loc, vn), vi) in (* mkSusp prop (S.shift (var_i + 1)) *) @@ -241,7 +235,7 @@ let macro_impl_map : macromap =
let get_macro_impl loc name = try SMap.find name macro_impl_map - with Not_found -> builtin_error loc ("Builtin macro" ^ name ^ " not found") + with Not_found -> error loc ("Builtin macro" ^ name ^ " not found")
let is_builtin_macro name = try let _ = SMap.find name macro_impl_map in true
===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -40,8 +40,8 @@ open Fmt
module S = Subst
-let debruijn_error l m = msg_error "DEBRUIJN" l m; internal_error m -let debruijn_warning = msg_warning "DEBRUIJN" +let error l m = msg_error "DEBRUIJN" l m; internal_error m +let warning = msg_warning "DEBRUIJN"
(* Type definitions * ---------------------------------- *) @@ -60,7 +60,6 @@ type property_env = property_elem PropertyMap.t
(* easier to debug with type annotations *) type env_elem = (int * vdef option * varbind * ltype) -(* FIXME: This is the *lexp context*. *) type lexp_context = env_elem M.myers
type db_idx = int (* DeBruijn index. *) @@ -124,7 +123,7 @@ let env_extend_rec r (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in let ((n, map), env, f) = ctx in (try let _ = senv_lookup name ctx in - debruijn_warning loc ("Variable Shadowing " ^ name); + warning loc ("Variable Shadowing " ^ name); with Not_found -> ()); let nmap = SMap.add name n map in ((n + 1, nmap), @@ -161,29 +160,29 @@ let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx
(* Print context *) -let print_lexp_ctx (ctx : lexp_context) = - let n = M.length ctx in +let print_lexp_ctx_n (ctx : lexp_context) start = + let n = (M.length ctx) - 1 in
print_string (make_title " LEXP CONTEXT ");
make_rheader [ (Some ('l', 7), "INDEX"); - (Some ('l', 10), "NAME"); (Some ('l', 4), "OFF"); - (Some ('l', 40), "VALUE:TYPE")]; + (Some ('l', 10), "NAME"); + (Some ('l', 42), "VALUE:TYPE")];
print_string (make_sep '-');
(* it is annoying to print according to SMap order *) (* let's use myers list order *) let rec extract_names (lst: lexp_context) acc = - match lst with - | M.Mnil -> acc - | M.Mcons (hd, tl, _, _) -> - let name = match hd with - | (_, Some (_, name), _, _) -> name - | _ -> "" in - extract_names tl (name::acc) in + let names = ref [] in + for i = start to n do + let name = match (M.nth (n - i) lst) with + | (_, Some (_, name), _, _) -> name + | _ -> "" in + names := name::!names + done; !names in
let ord = extract_names ctx [] in
@@ -195,7 +194,7 @@ let print_lexp_ctx (ctx : lexp_context) = print_string " | "; lalign_print_int (n - idx - 1) 7; print_string " | ";
- let ptr_str = "" in (*" | | | | " in *) + let ptr_str = " | | | | " in
try let r, name, exp, tp = match env_lookup_by_index (n - idx - 1) ctx with @@ -204,32 +203,40 @@ let print_lexp_ctx (ctx : lexp_context) = | (r, _, _, tp) -> r, "", None, tp in
(* Print env Info *) - lalign_print_string name 10; (* name must match *) + lalign_print_int r 4; print_string " | "; - lalign_print_int r 4; + lalign_print_string name 10; (* name must match *) print_string " | ";
- let _ = (match exp with + let _ = match exp with | None -> print_string "<var>" - | Some exp -> lexp_print exp) - (* let str = _lexp_to_str (!debug_ppctx) exp in + | Some exp -> ( + let str = _lexp_to_str (!debug_ppctx) exp in let str = (match str_split str '\n' with - | hd::tl -> print_string (hd ^ "\n"); tl + | hd::tl -> print_string hd; tl | _ -> []) in
- List.iter (fun elem -> - print_string (ptr_str ^ elem ^ "\n")) str) *)in + List.iter (fun elem -> + print_string ("\n" ^ ptr_str ^ elem)) str) in
- print_string (ptr_str ^ ": "); lexp_print tp; print_string "\n"; + print_string (": "); lexp_print tp; print_string "\n";
_print (idx + 1) tl
with Not_found -> (print_string "Not_found |\n"; _print (idx + 1) tl)) in
- _print 0 ord; print_string (make_sep '=') + _print (start - 1) ord; print_string (make_sep '=')
+(* Only print user defined variables *) +let print_lexp_ctx (ctx : lexp_context) = + print_lexp_ctx_n ctx !L.builtin_size + +(* Dump the whole context *) +let dump_lexp_ctx (ctx : lexp_context) = + print_lexp_ctx_n ctx 0 + (* generic lookup *) let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = let ((loc, ename), dbi) = v in @@ -240,7 +247,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = (* Check if names match *) if not (ename = name) then (print_lexp_ctx ctx; - debruijn_error loc ("DeBruijn index " + error loc ("DeBruijn index " ^ string_of_int dbi ^ " refers to wrong name. " ^ "Expected: `" ^ ename @@ -249,7 +256,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem =
ret) with - Not_found -> debruijn_error loc ("DeBruijn index " + Not_found -> error loc ("DeBruijn index " ^ string_of_int dbi ^ " out of bounds!")
@@ -303,14 +310,13 @@ let get_property ctx (var_i, var_n) (att_i, att_n): lexp = (* /!\ input index are reversed or not ? I think not so I shift them *) let pmap = try PropertyMap.find (n - var_i, var_n) property_map with Not_found -> - debruijn_error dummy_location ("Variable "" ^ var_n ^ "" does not have any properties") in + error dummy_location ("Variable "" ^ var_n ^ "" does not have any properties") in
let prop = try PropertyMap.find (n - att_i, att_n) pmap with Not_found -> - debruijn_error dummy_location ("Property "" ^ att_n ^ "" not found") in + error dummy_location ("Property "" ^ att_n ^ "" not found") in mkSusp prop (S.shift (var_i + 1))
- let has_property ctx (var_i, var_n) (att_i, att_n): bool = let (a, b, property_map) = ctx in let n = get_size ctx in
===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -250,9 +250,9 @@ let lexp_detect_recursive pdecls = let ptp = (match (!pending) with | Ldecl(_, _, ptp)::[] -> ptp (* we already checked that len(pending) == 1*) - | Ldecl(_, _, ptp)::_ -> lexp_fatal l "Unreachable" - | [] -> lexp_fatal l "Unreachable" - | Lmcall _ :: _ -> lexp_fatal l "Unreachable") in + | Ldecl(_, _, ptp)::_ -> typer_unreachable "Unreachable" + | [] -> typer_unreachable "Unreachable" + | Lmcall _ :: _ -> typer_unreachable "Unreachable") in
(* add declaration to merged decl *) merged := Ldecl((l, s), Some pxp, ptp)::(!merged); @@ -280,7 +280,7 @@ let lexp_detect_recursive pdecls = merged := Ldecl((l, s), Some pxp, (Some ptp))::!merged;
(* s should be unique *) - | _ -> lexp_error l "declaration must be unique") in + | _ -> error l "declaration must be unique") in
(* element is not pending anymore *) pending := lst; @@ -388,10 +388,13 @@ let main () = ) merged));
(* debug lexp parsing once merged *) + print_string yellow; let lexps, nctx = try lexp_p_decls pexps octx with e -> + print_string reset; print_lexp_trace None; - internal_error "Fail" in + raise e in + print_string reset;
(* use the new way of parsing expr *) let ctx = nctx in
===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -42,9 +42,6 @@ type label = symbol
module SMap = U.SMap
-let elexp_warning = U.msg_warning "ELEXP" -let elexp_fatal = U.msg_fatal "ELEXP" - type elexp = | Imm of sexp
===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -37,18 +37,15 @@ open Sexp
open Elexp module M = Myers +module L = Lexp
let dloc = dummy_location
-let env_error loc msg = - msg_error "ENV" loc msg; - raise (internal_error msg) - -let env_warning loc msg = msg_warning "ENV" loc msg +let error loc msg = msg_error "ENV" loc msg; raise (internal_error msg) +let warning loc msg = msg_warning "ENV" loc msg
let str_idx idx = "[" ^ (string_of_int idx) ^ "]"
- type value_type = | Vint of int | Vstring of string @@ -62,12 +59,11 @@ type value_type = | Vin of in_channel | Vout of out_channel | Vcommand of (unit -> value_type) + (* Runtime Environ *) and env_cell = (string option * (value_type ref)) and runtime_env = env_cell M.myers
- - let rec value_equal a b = match a, b with | Vint(i1), Vint(i2) -> i1 = i2 @@ -78,11 +74,10 @@ let rec value_equal a b = | Vin (c1), Vin(c2) -> c1 = c2 | Vout (c1), Vout(c2) -> c2 = c2 | Vcommand (f1), Vcommand(f2)-> f1 = f2 - | Vdummy, Vdummy -> - env_warning dloc "Vdummy"; true + | Vdummy, Vdummy -> warning dloc "Vdummy"; true
| Closure(s1, b1, ctx1), Closure(s2, b2, ctx2) -> - env_warning dloc "Closure"; + warning dloc "Closure"; if (s1 != s2) then false else true
| Vcons((_, ct1), a1), Vcons((_, ct2), a2) -> @@ -131,7 +126,7 @@ let rec value_string v = | Vint i -> string_of_int i | Vfloat f -> string_of_float f | Vsexp s -> sexp_string s - | Closure (s, elexp, _) -> "(" ^ s ^ (elexp_string elexp) ^ ")" + | Closure (s, elexp, _) -> "(lambda " ^ s ^ " -> " ^ (elexp_string elexp) ^ ")" | Vcons ((_, s), lst) -> let args = List.fold_left (fun str v -> (str ^ " " ^ (value_string v))) "" lst in @@ -153,14 +148,14 @@ let get_rte_variable (name: string option) (idx: int) if n1 = n2 then x else ( - env_error dloc + error dloc ("Variable lookup failure. Expected: "" ^ n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "" got "" ^ n1 ^ """)))
| _ -> x) with Not_found -> let n = match name with Some n -> n | None -> "" in - env_error dloc ("Variable lookup failure. Var: "" ^ + error dloc ("Variable lookup failure. Var: "" ^ n ^ "" idx: " ^ (str_idx idx))
let add_rte_variable name (x: value_type) (ctx: runtime_env) @@ -174,44 +169,11 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = (match (n, name) with | Some n1, Some n2 -> if (n1 != n2) then - env_error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) + error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) | _ -> ());
ref_cell := v
- -(* This function is used when we enter a new scope *) -(* it saves the size of the environment before temp var are added *) -(* it allow us to remove temporary variables when we enter a new scope * ) -let local_ctx ctx = - let (l, (_, _)) = ctx in - let osize = M.length l in - (l, (osize, 0)) - -let select_n (ctx: runtime_env) n: runtime_env = - let (l, a) = ctx in - let r = ref nil in - let s = (M.length l) - 1 in - - for i = 0 to n - 1 do - r := (M.cons (M.nth (s - i) l) (!r)); - done; - - ((!r), a) - -(* This removes temporary variables from the environment *) -(* and create a clean context free of function arguments *) -let temp_ctx (ctx: runtime_env): runtime_env = - let (l, (osize, _)) = ctx in - let tsize = M.length l in - (* Check if temporary variables are present *) - if tsize != osize then( - (* remove them - print_string "temp ctx was useful\n"; *) - (select_n ctx osize)) - else - ctx *) - (* Select the n first variable present in the env *) let nfirst_rte_var n ctx = let rec loop i acc = @@ -221,15 +183,14 @@ let nfirst_rte_var n ctx = List.rev acc in loop 0 []
-let print_myers_list l print_fun = +let print_myers_list l print_fun start = let n = (M.length l) - 1 in - print_string (make_title " ENVIRONMENT "); make_rheader [(None, "INDEX"); (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")]; print_string (make_sep '-');
- for i = 0 to n do + for i = start to n do print_string " | "; ralign_print_int (n - i) 5; print_string " | "; @@ -237,7 +198,7 @@ let print_myers_list l print_fun = done; print_string (make_sep '=')
-let print_rte_ctx (ctx: runtime_env) = +let print_rte_ctx_n (ctx: runtime_env) start = print_myers_list ctx (fun (n, vref) -> @@ -247,5 +208,13 @@ let print_rte_ctx (ctx: runtime_env) = | Some m -> lalign_print_string m 12; print_string " | " | None -> print_string (make_line ' ' 12); print_string " | " in
- value_print g; print_string "\n") + value_print g; print_string "\n") start + +(* Only print user defined variables *) +let print_rte_ctx ctx = + (* FIXME: harcoded -3, runtime_env has 3 variables missing *) + print_rte_ctx_n ctx (!L.builtin_size - 3)
+(* Dump the whole context *) +let dump_rte_ctx ctx = + print_rte_ctx_n ctx 0
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -46,59 +46,88 @@ 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 *) +type eval_debug_info = OL.pexporlexp list * elexp list + +let dloc = dummy_location +let _global_eval_trace = ref ([], []) +let _global_eval_ctx = ref make_runtime_ctx +let _eval_max_recursion_depth = ref 255 +let _builtin_lookup = ref SMap.empty + +let append_eval_trace trace (expr : elexp) = + let (a, b) = trace in + let r = (OL.Elexp expr)::a, b in + _global_eval_trace := r; r
-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 +let append_typer_trace trace (expr : elexp) = + let (a, b) = trace in + let r = (a, expr::b) in + _global_eval_trace := r; r + +let rec_depth trace = + let (a, b) = trace in + List.length b
(* eval error are always fatal *) -let eval_error loc msg = +let error loc msg = msg_error "EVAL" loc msg; + flush stdout; raise (internal_error msg)
-let eval_fatal = msg_fatal "EVAL" +let fatal = msg_fatal "EVAL" +let warning = msg_warning "EVAL"
-let dloc = dummy_location -let eval_warning = msg_warning "EVAL" +(* Print a message that look like this: + * + * [Ln 8, cl 6] ./samples/error.typer + * [X] Fatal EVAL MESSAGE + * > .... + * > .... + * + *)
-let _global_eval_trace = ref [] -let _global_eval_ctx = ref make_runtime_ctx -let _eval_max_recursion_depth = ref 255 -let reset_eval_trace () = _global_eval_trace := [] -let _builtin_lookup = ref SMap.empty +let debug_messages error_type loc message messages = + let msg = List.fold_left (fun str msg -> + str ^ "\n > " ^ msg) message messages in + error_type loc (msg ^ "\n") + +let root_string () = + match !_global_eval_trace with + | [], _ -> "" + | e::_, _ -> OL.pol_string e + +let debug_message error_type type_name type_string loc expr message = + debug_messages error_type loc + message [ + (type_name expr) ^ ": " ^ (type_string expr); + "Root: " ^ (root_string ()); + ]
(* Print value name followed by the value in itself, finally throw an exception *) -let value_debug_message loc vxp message = - debug_msg eval_fatal value_name value_string loc vxp message +let value_fatal = debug_message fatal value_name value_string +let value_error = debug_message error value_name value_string +let elexp_fatal = debug_message fatal elexp_name elexp_string
-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") +let none_fun : (location -> eval_debug_info -> value_type list -> runtime_env -> value_type) + = (fun loc args_val ctx -> error loc "Requested Built-in was not implemented")
(* Builtin of builtin * string * ltype *) -let _generic_binary_iop name f loc (depth : OL.pexporlexp list) +let _generic_binary_iop name f loc (depth : eval_debug_info) (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 + | _ -> 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") + debug_messages fatal loc (name ^ " expects Integers as arguments") [ + "(" ^ name ^ " " ^ (value_string l) ^ " " ^ (value_string r) ^ ")";]
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) @@ -109,19 +138,17 @@ 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 + | _ -> 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") + | _ -> value_error loc lxp "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)) + | op::_ -> value_error loc op "node_ expects one 'Sexp' got: " | _ -> typer_unreachable "-" in
(* value_print tlist; print_string "\n"; *) @@ -135,29 +162,27 @@ let make_node loc depth args_val ctx = | 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 + value_error loc g "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 + | _ -> 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") + | _ -> value_error loc lxp "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 + | _ -> 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") + | _ -> value_error loc lxp "integer_ expects one string as argument"
let make_float loc depth args_val ctx = Vdummy let make_block loc depth args_val ctx = Vdummy @@ -169,30 +194,30 @@ 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" + | _ -> 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" + | _ -> 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" + | _ -> 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 + | _ -> 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") + | _ -> error loc "wrong open mode")
let read_impl loc depth args_val ctx =
@@ -200,7 +225,7 @@ let read_impl loc depth args_val ctx = | [Vin(c); _] -> c | _ -> List.iter (fun v -> value_print v; print_string "\n") args_val; - builtin_error loc "read expects an in_channel" in + error loc "read expects an in_channel" in
let line = input_line channel in Vstring(line) @@ -211,21 +236,21 @@ let write_impl loc depth args_val ctx = | [Vout(c); Vstring(msg)] -> c, msg | _ -> List.iter (fun v -> value_print v) args_val; - builtin_error loc "read expects an out_channel" in + 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) trace: (value_type) = +let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) =
- let trace = ((OL.Elexp lxp)::trace) in + let trace = append_eval_trace trace lxp in let tloc = elexp_location lxp in let eval lxp ctx = _eval lxp ctx trace in
- (if (List.length trace) > (!_eval_max_recursion_depth) then - eval_fatal tloc "Recursion Depth exceeded"); + (if (rec_depth trace) > (!_eval_max_recursion_depth) then + fatal tloc "Recursion Depth exceeded");
(* Save current trace in a global variable. If an error occur, we will be able to retrieve the most recent trace and context *) @@ -254,7 +279,8 @@ let rec _eval lxp (ctx : Env.runtime_env) trace: (value_type) = eval inst nctx
(* Function call *) - | Call (lname, args) -> eval_call ctx trace lname args + | Call (lname, args) -> + eval_call ctx (append_typer_trace trace lxp) lname args
(* Case *) | Case (loc, target, pat, dflt) @@ -266,13 +292,13 @@ let rec _eval lxp (ctx : Env.runtime_env) trace: (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 [] + _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 -> - elexp_debug_message loc lxp + elexp_fatal loc lxp ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ")
and eval_call ctx i lname eargs = @@ -300,7 +326,7 @@ and eval_call ctx i lname eargs = | _, [] -> f
| _ -> - value_debug_message loc f "Cannot eval function" in + value_fatal loc f "Cannot eval function" in
(* eval function here *) let args = List.map (fun e -> _eval e ctx i) eargs in @@ -313,7 +339,7 @@ and eval_case ctx i loc target pat dflt = (* extract constructor name and arguments *) let ctor_name, args = match v with | Vcons((_, cname), args) -> cname, args - | _ -> elexp_debug_message loc target "Target is not a Constructor" in + | _ -> elexp_fatal loc target "Target is not a Constructor" in
(* Get working pattern *) try let (_, pat_args, exp) = SMap.find ctor_name pat in @@ -327,8 +353,8 @@ and eval_case ctx i loc target pat dflt = | (None)::pats, arg::args -> fold2 nctx pats args (* Errors: those should not happen but they might *) (* List.fold2 would complain. we print more info *) - | _::_, [] -> eval_warning loc "a) Eval::Case Pattern Error"; nctx - | [], _::_ -> eval_warning loc "b) Eval::Case Pattern Error"; nctx + | _::_, [] -> warning loc "a) Eval::Case Pattern Error"; nctx + | [], _::_ -> warning loc "b) Eval::Case Pattern Error"; nctx (* Normal case *) | [], [] -> nctx in
@@ -338,7 +364,7 @@ and eval_case ctx i loc target pat dflt = (* Run default *) with Not_found -> (match dflt with | Some lxp -> _eval lxp ctx i - | _ -> eval_error loc "Match Failure") + | _ -> error loc "Match Failure")
and build_arg_list args ctx i = (* _eval every args *) @@ -347,8 +373,6 @@ and build_arg_list args ctx i = (* 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 [] - and _eval_decls (decls: (vdef * elexp) list) (ctx: runtime_env) i: runtime_env =
@@ -364,10 +388,6 @@ and _eval_decls (decls: (vdef * elexp) list) ignore (set_rte_variable offset (Some name) v nctx)) decls;
nctx -and eval_decls_toplevel (decls: (vdef * elexp) list list) ctx = - (* Add toplevel decls function *) - List.fold_left (fun ctx decls -> - eval_decls decls ctx) ctx decls
(* -------------------------------------------------------------------------- *) (* Builtin Implementation (Some require eval) *) @@ -393,23 +413,23 @@ and typer_builtins_impl = [ ("write" , write_impl); ]
-and bind_impl loc (depth : OL.pexporlexp list) args_val ctx = +and bind_impl loc depth args_val ctx =
let io, cb = match args_val with | [io; callback] -> io, callback - | _ -> eval_error loc "bind expects two arguments" in + | _ -> error loc "bind expects two arguments" in
(* build Vcommand from io function *) let cmd = match io with | Vcommand (cmd) -> cmd - | _ -> eval_error loc "bind first arguments must be a monad" in + | _ -> error loc "bind first arguments must be a monad" in
(* bind returns another Vcommand *) Vcommand (fun () -> (* get callback *) let body, ctx = match cb with | Closure(_, body, ctx) -> body, ctx - | _ -> eval_error loc "A Closure was expected" in + | _ -> error loc "A Closure was expected" in
(* run given command *) let underlying = cmd () in @@ -424,11 +444,11 @@ and run_io loc depth args_val ctx =
let io, ltp = match args_val with | [io; ltp] -> io, ltp - | _ -> eval_error loc "run-io expects 2 arguments" in + | _ -> error loc "run-io expects 2 arguments" in
let cmd = match io with | Vcommand (cmd) -> cmd - | _ -> eval_error loc "run-io expects a monad as first argument" in + | _ -> error loc "run-io expects a monad as first argument" in
(* run given command *) let _ = cmd () in @@ -439,7 +459,7 @@ and run_io loc depth args_val ctx = and typer_eval loc depth args ctx = let arg = match args with | [a] -> a - | _ -> eval_error loc "eval_ expects a single argument" in + | _ -> error loc "eval_ expects a single argument" in (* I need to be able to lexp sexp but I don't have lexp ctx *) match arg with (* Nodes that can be evaluated *) @@ -457,23 +477,23 @@ and get_builtin_impl str loc =
try SMap.find str !_builtin_lookup with Not_found -> - eval_error loc ("Requested Built-in "" ^ str ^ "" does not exist") + error loc ("Requested Built-in "" ^ str ^ "" does not exist")
(* Sexp -> (Sexp -> List Sexp -> Sexp) -> (String -> Sexp) -> (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args ctx = - let eval a b = _eval a b [] in + let eval a b = _eval a b depth in let sxp, nd, sym, str, it, flt, blk, rctx = match args with | [sxp; Closure(_, nd, rctx); Closure(_, sym, _); Closure(_, str, _); Closure(_, it, _); Closure(_, flt, _); Closure(_, blk, _)] -> sxp, nd, sym, str, it, flt, blk, rctx - | _ -> eval_error loc "sexp_dispatch expects 7 arguments" in + | _ -> error loc "sexp_dispatch expects 7 arguments" in
let sxp = match sxp with | Vsexp(sxp) -> sxp - | _ -> value_debug_message loc sxp "sexp_dispatch expects a Sexp as 1st arg" in + | _ -> value_fatal loc sxp "sexp_dispatch expects a Sexp as 1st arg" in
match sxp with | Node (op, s) ->( @@ -481,7 +501,7 @@ and sexp_dispatch loc depth args ctx = let rctx = add_rte_variable None (olist2tlist_rte s) rctx in match eval nd rctx with | Closure(_, nd, _) -> eval nd rctx - | _ -> eval_error loc "Node has 2 arguments") + | _ -> error loc "Node has 2 arguments")
| Symbol (_ , s) -> eval sym (add_rte_variable None (Vstring(s)) rctx) @@ -493,7 +513,7 @@ and sexp_dispatch loc depth args ctx = eval flt (add_rte_variable None (Vfloat(f)) rctx) (* | Block (_ , s, _) -> eval blk (add_rte_variable None (olist2tlist_rte s)) *) - | _ -> eval_error loc "sexp_dispatch error" + | _ -> error loc "sexp_dispatch error"
(* -------------------------------------------------------------------------- *) and print_eval_result i lxp = @@ -502,7 +522,27 @@ and print_eval_result i lxp = print_string "] >> "; value_print lxp; print_string "\n";
-and print_trace2 title trace default = +and print_typer_trace' trace = + + let trace = List.rev trace in + + print_string (Fmt.make_title "Typer Trace"); + print_string (Fmt.make_sep '-'); + + let _ = List.iteri (fun i expr -> + print_string " "; + Fmt._print_ct_tree i; print_string "+- "; + print_string ((elexp_string expr) ^ "\n")) trace in + + print_string (Fmt.make_sep '=') + +and print_typer_trace trace = + match trace with + | Some t -> print_typer_trace' t + | None -> let (a, b) = !_global_eval_trace in + print_typer_trace' b + +and print_trace title trace default = (* If no trace is provided take the most revent one *) let trace = match trace with | Some trace -> trace @@ -536,19 +576,26 @@ and print_trace2 title trace default = print_string (Fmt.make_sep '=')
and print_eval_trace trace = - print_trace2 " EVAL TRACE " trace !_global_eval_trace + let (a, b) = !_global_eval_trace in + print_trace " EVAL TRACE " trace a
-let eval lxp ctx = _eval lxp ctx [] +let eval lxp ctx = _eval lxp ctx ([], [])
let debug_eval lxp ctx = - try - _global_eval_trace := []; - eval lxp ctx + try eval lxp ctx with e -> ( print_rte_ctx (!_global_eval_ctx); print_eval_trace None; raise e)
+ +let eval_decls decls ctx = _eval_decls decls ctx ([], []) + +let eval_decls_toplevel (decls: (vdef * elexp) list list) ctx = + (* Add toplevel decls function *) + List.fold_left (fun ctx decls -> + eval_decls decls ctx) ctx decls + (* Eval a list of lexp *) let eval_all lxps rctx silent = let evalfun = if silent then eval else debug_eval in @@ -581,7 +628,7 @@ let from_lctx (ctx: elab_context): runtime_env = | _ (* FIXME: We should stop right here if this variable is * actually used (e.g. if this type's variable is ∀t.t). *) - -> eval_warning dloc ("No definition to compute the value of `" + -> warning dloc ("No definition to compute the value of `" ^ varname oname ^ "`"); (i + 1, evals)) (0, []) lctx in
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -105,6 +105,8 @@ type varbind = | ForwardRef | LetDef of lexp
+let builtin_size = ref 0 + (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -583,9 +585,9 @@ let lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp))
type print_context = (bool * int * bool * bool * bool * bool* int)
-let pretty_ppctx = ref (true , 0, true, false, true, 4, true) -let compact_ppctx = ref (false, 0, true, false, true, 4, false) -let debug_ppctx = ref (false, 0, true, true , false, 4, true) +let pretty_ppctx = ref (true , 0, true, false, true, 2, true) +let compact_ppctx = ref (false, 0, true, false, true, 2, false) +let debug_ppctx = ref (false, 0, true, true , false, 2, true)
let rec lexp_print e = _lexp_print (!debug_ppctx) e and _lexp_print ctx e = print_string (_lexp_to_str ctx e)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -61,28 +61,41 @@ let dlxp = type0 let dltype = type0 let dloc = dummy_location
-let lexp_warning = msg_warning "LPARSE" -let lexp_error = msg_error "LPARSE" -let lexp_fatal = msg_fatal "LPARSE" - let _global_lexp_ctx = ref make_elab_context let _global_lexp_trace = ref [] let _parsing_internals = ref false 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 = - debug_msg lexp_fatal lexp_name lexp_string loc lxp message +let warning = msg_warning "LPARSE" +let error = msg_error "LPARSE" +let fatal = msg_fatal "LPARSE"
-let pexp_debug_message loc lxp message = - debug_msg lexp_fatal pexp_name pexp_string loc lxp message +let root_string () = + match !_global_lexp_trace with + | [] -> "" + | e::_ -> OL.pol_string e
+(* Print Lexp name followed by the lexp in itself, finally throw an exception *) +let debug_message error_type type_name type_string loc expr message = + debug_messages error_type loc + message [ + (type_name expr) ^ ": " ^ (type_string expr); + "Root: " ^ (root_string ()); + ] + +let lexp_fatal = debug_message fatal lexp_name lexp_string +let lexp_warning = debug_message warning lexp_name lexp_string +let lexp_error = debug_message error lexp_name lexp_string +let pexp_fatal = debug_message fatal pexp_name pexp_string +let pexp_error = debug_message error pexp_name pexp_string +let value_fatal = debug_message fatal value_name value_string
let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = match OL.lexp_whnf lsort (ectx_to_lctx ctx) with | Sort (_, _) -> () (* All clear! *) - | _ -> lexp_error l ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_string ltp) + | _ -> lexp_error l ltp + ("Type of `" ^ name ^ "` is not a proper type: " + ^ lexp_string ltp)
let elab_check_proper_type (ctx : elab_context) ltp v = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp @@ -94,28 +107,22 @@ let elab_check_proper_type (ctx : elab_context) ltp v =
let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in + let loc = lexp_location lxp in + let ltype' = try OL.check lctx lxp - with e -> - print_string "Error while type-checking:\n"; - lexp_print lxp; - print_string "\nIn context:\n"; - print_lexp_ctx (ectx_to_lctx ctx); - raise e in + with e -> + lexp_error dloc lxp "Error while type-checking"; + print_lexp_ctx (ectx_to_lctx ctx); + raise e in (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is * convertible to `Type_0`, because it doesn't have access to lctx. *) if true (* OL.conv_p ltype ltype' *) then elab_check_proper_type ctx ltype var else - (print_string "¡¡ctx_define error!!\n"; - lexp_print lxp; - print_string " !: "; - lexp_print ltype; - print_string "\nbecause\n"; - lexp_print (OL.check lctx lxp); - print_string " != "; - lexp_print ltype; - print_string "\n"; - lexp_fatal (let (l,_) = var in l) "TC error") + (debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ + (lexp_string lxp) ^ "!: " ^ (lexp_string ltype); + " because"; + (lexp_string (OL.check lctx lxp)) ^ "!= " ^ (lexp_string ltype);])
let ctx_define (ctx: elab_context) var lxp ltype = elab_check_def ctx var lxp ltype; @@ -190,13 +197,13 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype =
match p with (* Block/String/Integer/Float *) - | Pimm value -> (Imm(value), - match value with + | Pimm v -> (Imm(v), + match v with | Integer _ -> type_int | Float _ -> type_float | String _ -> type_string; - | _ -> lexp_error tloc "Could not find type"; - pexp_print p; print_string "\n"; dltype) + | _ -> pexp_error tloc p "Could not find type"; + dltype)
(* Symbol i.e identifier *) | Pvar (loc, name) ->( @@ -209,7 +216,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = lxp, ltp (* Return Macro[22] *)
with Not_found -> - (lexp_error loc ("The variable: "" ^ name ^ "" was not declared"); + (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); (* Error recovery. The -1 index will raise an error later on *) (make_var name (-1) loc), dltype))
@@ -259,7 +266,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = let ltp, _ = match optype with | Some ptype -> lexp_infer ptype ctx (* This case must have been lexp_p_check *) - | None -> lexp_error tloc "Lambda require type annotation"; + | None -> pexp_error tloc p "Lambda require type annotation"; dltype, dltype in
let nctx = env_extend ctx var Variable ltp in @@ -278,14 +285,14 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype =
(* Get constructor args *) let formal, args = match OL.lexp_whnf idt (ectx_to_lctx ctx) with - | Inductive(_, _, formal, ctor_def) -> ( + | Inductive(_, _, formal, ctor_def) as lxp -> ( try formal, (SMap.find cname ctor_def) with Not_found -> - lexp_error loc + lexp_error loc lxp ("Constructor "" ^ cname ^ "" does not exist"); [], [])
- | _ -> lexp_error loc "Not an Inductive Type"; [], [] in + | lxp -> lexp_error loc lxp "Not an Inductive Type"; [], [] in
(* build Arrow type *) let target = if formal = [] then @@ -323,7 +330,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = let ltp, _ = lexp_infer ptp ctx in (_lexp_p_check pxp ltp ctx trace), ltp
- | _ -> pexp_debug_message tloc p "Unhandled Pexp" + | _ -> pexp_fatal tloc p "Unhandled Pexp"
and lexp_let_decls decls (body: lexp) ctx i = @@ -351,7 +358,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = let ltp, lbtp = match nosusp t with | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | expr -> - lexp_debug_message tloc expr "Expected Type Arrow ( _ -> _ )" in + lexp_fatal tloc expr "Expected Type Arrow ( _ -> _ )" in
let nctx = env_extend ctx var Variable ltp in let lbody = lexp_check body lbtp nctx in @@ -384,8 +391,8 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = | None -> rtype := (Some ltp); true in
let uniqueness_warn name = - lexp_warning loc ("Pattern " ^ name ^ " is a duplicate." ^ - " It will override previous pattern.") in + warning loc ("Pattern " ^ name ^ " is a duplicate." ^ + " It will override previous pattern.") in
let check_uniqueness loc name map = try let _ = SMap.find name map in uniqueness_warn name @@ -409,7 +416,7 @@ and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i =
(* Check ltp type. Must be similar to rtype *) (if type_check ltp then () - else lexp_error iloc "Branch return type mismatch"); + else lexp_error iloc ltp "Branch return type mismatch");
if name = "_" then ( (if dflt != None then uniqueness_warn name); @@ -440,9 +447,10 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
let from_lctx ctx = try (from_lctx ctx) with e ->( - lexp_error loc "Could not convert lexp context into rte context"; - print_eval_trace None; - raise e) in + debug_messages error loc + "Could not convert lexp context into rte context" []; + print_eval_trace None; + raise e) in
(* Vanilla : sqr is inferred and (lambda x -> x * x) is returned * Macro : sqr is returned @@ -464,8 +472,9 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = 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) - ("Explicit arg `" ^ aname ^ "` to non-function (type = " ^ lexp_string ltp ^ ")")) + | _ -> fatal (sexp_location sarg) + ("Explicit arg `" ^ aname ^ "` to non-function " ^ + "(type = " ^ (lexp_string ltp) ^ ")")) | sarg :: sargs (* Process Argument *) -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) with @@ -474,15 +483,16 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let larg = _lexp_p_check parg arg_type ctx i in handle_fun_args ((Aexplicit, larg) :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) - | Arrow _ as t -> lexp_print t; print_string "\n"; - sexp_print sarg; print_string "\n"; - lexp_fatal (sexp_location sarg) - "Expected non-explicit arg" + | Arrow _ as t -> + debug_messages fatal (sexp_location sarg) "Expected non-explicit arg" [ + "ltype : " ^ (lexp_string t); + "s-exp arg: " ^ (sexp_string sarg);] + | t -> - print_lexp_ctx (ectx_to_lctx ctx); - lexp_debug_message (sexp_location sarg) t - ("Explicit arg `" ^ sexp_string sarg ^ - "` to non-function (type = " ^ lexp_string ltp ^ ")")) in + print_lexp_ctx (ectx_to_lctx ctx); + lexp_fatal (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 @@ -500,12 +510,10 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let ltp, _ = lexp_infer ptp ctx in Builtin((loc, str), ltp), ltp
- | true, _ -> - lexp_error loc "Wrong Usage of "Built-in""; + | true, _ -> error loc "Wrong Usage of `Built-in`"; dlxp, dltype
- | false, _ -> - lexp_error loc "Use of "Built-in" in user code"; + | false, _ -> error loc "Use of `Built-in` in user code"; dlxp, dltype)
| _ -> @@ -521,7 +529,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | Vstring(s) -> String(dloc, s) | Vfloat(f) -> Float(dloc, f) | v -> - value_debug_message loc v "Macro_ expects '(List Sexp) -> Sexp'" in + value_fatal loc v "Macro_ expects `(List Sexp) -> Sexp`" in
let pxp = pexp_parse sxp in lexp_infer pxp ctx in @@ -584,16 +592,13 @@ and lexp_read_pattern pattern exp target ctx trace: 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 - | Inductive(_, _, _, map) + | Inductive(_, (_, label), _, map) -> (try SMap.find cons_name map with Not_found - -> lexp_warning loc - ("`" ^ lexp_string (it) - ^ "` does not hold a `" + -> warning loc ("`" ^ (lexp_string it) ^ "` does not hold a `" ^ cons_name ^ "` constructor"); []) - | it -> lexp_fatal loc - ("`" ^ lexp_string (it) - ^ "` is not an inductive type!") in + | it -> fatal loc + ("`" ^ (lexp_string it) ^ "` is not an inductive type!") in
(* FIXME: Don't remove them, add them without names! *) (* FIXME: Add support for explicit-implicit fields! *) @@ -609,9 +614,9 @@ and lexp_read_pattern pattern exp target ctx trace: (* read pattern args *) let args, nctx = lexp_read_pattern_args args cons_args ctx in (cons_name, loc, args), nctx - | _ -> lexp_warning (pexp_location ctor) - ("Invalid constructor `" - ^ (pexp_string ctor) ^ "`"); + | _ -> warning (pexp_location ctor) + ("Invalid constructor `" ^ (pexp_string ctor) ^ "`"); + ("_", pexp_location ctor, []), ctx
(* Read patterns inside a constructor *) @@ -629,7 +634,7 @@ and lexp_read_pattern_args args (args_type : lexp list) ctx: let args_type = if length_type != length_pat then make_list dltype length_pat else args_type in
- (if length_type != length_pat then lexp_warning dloc "Size Mismatch"); + (if length_type != length_pat then warning dloc "Size Mismatch");
let rec loop args args_type acc ctx = match args, args_type with @@ -644,7 +649,7 @@ and lexp_read_pattern_args args (args_type : lexp list) ctx: let nctx = env_extend ctx var Variable ltp in let nacc = (Aexplicit, Some var)::acc in loop tl type_tl nacc nctx - | _ -> lexp_error dloc "Constructor inside a Constructor"; + | _ -> error dloc "Constructor inside a Constructor"; loop tl type_tl ((Aexplicit, None)::acc) ctx) | _ -> typer_unreachable "unreachable branch"
@@ -686,8 +691,7 @@ and lexp_expand_macro macro_funct sargs ctx trace = let rctx = from_lctx ctx in
(* eval macro *) - _global_eval_trace := trace; - let vxp = try _eval emacro rctx 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 *) @@ -704,7 +708,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = let body, mfun = match lxp with | Some (Call(_, [(_, lxp)]) as e) -> e, lxp | Some lxp -> lxp, lxp - | None -> lexp_fatal loc "expression does not exist" in + | None -> fatal loc "expression does not exist" in
(* Special Form *) match mfun with @@ -716,7 +720,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = (* extract info *) let var, att, fn = match largs with | [Var((_, vn), vi); Var((_, an), ai); fn] -> (vi, vn), (ai, an), fn - | _ -> lexp_fatal loc "add-attribute expects 3 args" in + | _ -> fatal loc "add-attribute expects 3 args" in
let ctx = add_property ctx var att fn in
@@ -734,12 +738,12 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = let decls = List.map (fun g -> match g with | Vsexp(sxp) -> sxp - | _ -> value_debug_message loc g "Macro expects sexp list") decls in + | _ -> value_fatal loc g "Macro expects sexp list") decls in
(* read as pexp_declaraton *) pexp_decls_all decls, ctx) with _ -> - lexp_fatal loc "Macro not found" + fatal loc ("Macro `" ^ mname ^ "`not found")
(* Parse let declaration *) and lexp_p_decls decls ctx = _lexp_decls decls ctx [] @@ -770,7 +774,7 @@ and lexp_decls_1 match pdecls with | [] -> (if not (SMap.is_empty pending_decls) then let (s, (l, _)) = SMap.choose pending_decls in - lexp_error l ("Variable `" ^ s ^ "` declared but not defined!") + error l ("Variable `" ^ s ^ "` declared but not defined!") else assert (pending_defs == [])); [], [], nctx @@ -778,11 +782,11 @@ and lexp_decls_1 | Ptype ((l, vname) as v, ptp) :: pdecls -> let (ltp, lsort) = _lexp_p_infer ptp nctx [] in if SMap.mem vname pending_decls then - (lexp_error l ("Variable `" ^ vname ^ "` declared twice!"); + (error l ("Variable `" ^ vname ^ "` declared twice!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) else if List.exists (fun ((_, vname'), _, _) -> vname = vname') pending_defs then - (lexp_error l ("Variable `" ^ vname ^ "` already defined!"); + (error l ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) else (elab_check_sort nctx lsort v ltp; lexp_decls_1 pdecls ectx @@ -811,7 +815,7 @@ and lexp_decls_1 lexp_decls_1 pdecls ectx nctx pending_decls pending_defs
with Not_found -> - lexp_error l ("`" ^ vname ^ "` defined but not declared!"); + error l ("`" ^ vname ^ "` defined but not declared!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs)
| Pmcall ((l, _) as v, sargs) :: pdecls @@ -830,7 +834,7 @@ and lexp_decls_1 lexp_decls_1 (List.append pdecls' pdecls) ectx nctx' pending_decls pending_defs)
- else lexp_fatal l "Context changed in already changed context") + else fatal l "Context changed in already changed context")
and _lexp_decls pdecls ctx i: ((vdef * lexp * ltype) list list * elab_context) = @@ -854,7 +858,8 @@ and _lexp_parse_all (p: pexp list) (ctx: elab_context) i : lexp list =
and print_lexp_trace (trace : (OL.pexporlexp list) option) = - print_trace2 " ELAB TRACE " trace !_global_lexp_trace + print_trace " ELAB TRACE " trace !_global_lexp_trace + (* Only print var info *) and lexp_print_var_info ctx = let ((m, _), env, _) = ctx in @@ -924,12 +929,11 @@ let default_lctx, default_rctx = (* -- DONE -- *) lctx with e -> - lexp_warning dloc "Predef not found"; + warning dloc "Predef not found"; lctx in let rctx = make_runtime_ctx in let rctx = eval_decls_toplevel (List.map OL.clean_decls d) rctx in - _global_eval_trace := []; - lctx, rctx + lctx, rctx
(* String Parsing * --------------------------------------------------------- *)
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -466,3 +466,10 @@ type pexporlexp = | Elexp of E.elexp
+let pol_string xp = match xp with + | Pexp p -> P.pexp_string p + | Elexp e -> E.elexp_string e + +let pol_name xp = match xp with + | Pexp p -> P.pexp_name p + | Elexp e -> E.elexp_name e \ No newline at end of file
===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -65,29 +65,21 @@ let internal_error s = raise (Internal_error s) exception Unreachable_error of string let typer_unreachable s = raise (Unreachable_error s)
-(* Multi line error message ? - * - * | [X] Fatal SECTION [ln 12, cl 12: FILE.typer] - * | >> typer_dump = something; - * | >> - * | >> My Error message is on multiple line - * | >> multiple line - * | ------------------------------------------------ - *) - - - - -(* 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( - let info = " " ^ kind ^ " [" ^ loc_string loc ^ "] " ^ (Fmt.lalign_string section 8) in - print_string (info ^ " " ^ msg ^ "\n")) else () + let info = + " [" ^ loc_string loc ^ "] " ^ loc.file ^ "\n" ^ + " " ^ kind ^ " " ^ (Fmt.lalign_string section 8) ^ " " ^ msg ^ "\n" in + print_string info) 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; + flush stdout; internal_error m
let msg_error = msg_message 1 "[!] Error " @@ -102,24 +94,6 @@ let not_implemented_error () = internal_error "not implemented"
let string_implode chars = String.concat "" (List.map (String.make 1) chars)
-let print_trace name max elem_to_string print_elem trace = - print_string (Fmt.make_title name); - - let n = List.length trace in - print_string " size = "; print_int n; - print_string (" max_printed = " ^ (string_of_int max) ^ "\n"); - print_string (Fmt.make_sep '-'); - - let racc = List.rev trace in - Fmt.print_last max racc (fun j (i, l, g) -> - 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"); - - print_string (Fmt.make_sep '=') - - let opt_map f x = match x with None -> None | Some x -> Some (f x)
let str_split str sep =
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -48,7 +48,6 @@ let rctx = default_rctx *) let test_eval_eqv_named name decl run res = add_test "EVAL" name (fun () -> - reset_eval_trace (); let rctx, lctx = eval_decl_str decl lctx rctx in
let erun = eval_expr_str run lctx rctx in (* evaluated run expr *) @@ -253,9 +252,8 @@ let _ = test_eval_eqv attr_decl "True"
(* This makes sure contexts are reinitialized between calls - * i.e the context should not grow * ) + * i.e the context should not grow *) let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> - reset_eval_trace (); _typer_verbose := (-1);
let code = " @@ -276,10 +274,9 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> success () else failure ()) -)) *) +))
let _ = (add_test "EVAL" "Monads" (fun () -> - reset_eval_trace ();
let dcode = " c = bind (a := Type) (b := Type) (open "./_build/w_file.txt" "w")
===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -43,7 +43,6 @@ let lctx = default_lctx let rctx = default_rctx
let _ = (add_test "MACROS" "macros base" (fun () -> - reset_eval_trace ();
(* define 'lambda x -> x * x' using macros *) let dcode = " @@ -67,8 +66,6 @@ let _ = (add_test "MACROS" "macros base" (fun () ->
let _ = (add_test "MACROS" "macros decls" (fun () -> - reset_eval_trace (); - let dcode = " decls-impl = lambda (x : List Sexp) -> cons(a := Sexp) (node_ (symbol_ "_=_")
View it on GitLab: https://gitlab.com/monnier/typer/commit/5496ae2c19527caf00905cce277ce17a7356...