Setepenre pushed to branch master at Stefan / Typer
Commits: cee10e51 by Pierre Delaunay at 2016-11-29T14:10:27-05:00 Little modifications
- - - - - af1634f0 by Pierre Delaunay at 2016-11-29T14:11:03-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - d760340d by Pierre Delaunay at 2016-12-01T03:49:10-05:00 Merge branch 'master' of gitlab.com:monnier/typer
- - - - - d63348a8 by Pierre Delaunay at 2016-12-01T05:41:23-05:00 * src/eval.ml: fixed trace issue - when function calls were evaluated arguments trace evaluation was not kept which made trace very short and not representative of the work that has been made by the interpreter.
* src/lexp.ml: added missing `lexp_name` cases and removed catch-all case
- - - - -
5 changed files:
- samples/dependent.typer - samples/inductive.typer - src/eval.ml - src/lexp.ml - tests/eval_test.ml
Changes:
===================================== samples/dependent.typer ===================================== --- a/samples/dependent.typer +++ b/samples/dependent.typer @@ -1,5 +1,9 @@
-Reify = inductive_ (Reify (a : Type)) (RInt (a = Int)) (RFloat (a = Float)) (RString (a = String)); +Reify = inductive_ (Reify (a : Type)) + (RInt (a = Int)) + (RFloat (a = Float)) + (RString (a = String)); + RInt = inductive-cons Reify RInt; RFloat = inductive-cons Reify RFloat; RString = inductive-cons Reify RString; @@ -18,11 +22,11 @@ get-type x = case x
% Here to-int : (a : Type) ≡> (r : (Reify a)) => (x : a) -> Int; -to-int = lambda a ≡> lambda r = lambda x -> case a +to-int = lambda a ≡> lambda r => lambda x -> case a | RInt => x | RFloat => float-to-int x | RString => string-to-int x;
-a = to-int (a := Float2) (2.0); -b = to-int (a := String2) "2"; -c = to-int (a := Int2) 2; \ No newline at end of file +%a = to-int (a := Float2) (2.0); +%b = to-int (a := String2) "2"; +%c = to-int (a := Int2) 2;
===================================== samples/inductive.typer ===================================== --- a/samples/inductive.typer +++ b/samples/inductive.typer @@ -71,7 +71,6 @@ type-impl = lambda (x : List Sexp) -> (cons (a := Sexp) name ctor) in
% Create a forward declaration in case the declaration is recursive - % let fdecl = make-ann type-name (symbol_ "Type") in let decl = make-decl type-name inductive in
% Add constructors @@ -85,7 +84,6 @@ type-impl = lambda (x : List Sexp) -> in for-each ctor (nil (a := Sexp)) in
% return decls - % cons (a := Sexp) fdecl % Forward declaration (cons (a := Sexp) decl % inductive type declaration ctors); % constructor declarations
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -72,6 +72,8 @@ let append_typer_trace trace (expr : elexp) = let r = (a, expr::b) in _global_eval_trace := r; r
+let get_trace () = !_global_eval_trace + let rec_depth trace = let (a, b) = trace in List.length b @@ -243,8 +245,6 @@ let write_impl loc depth args_val = 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 : eval_debug_info): (value_type) =
let trace = append_eval_trace trace lxp in @@ -281,12 +281,15 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type eval inst nctx
(* Function call *) - | Call (f, args) - (* FIXME: Add the trace only once we enter the function? *) - -> let ntrace = append_typer_trace trace lxp in - eval_call (elexp_location f) ntrace - (_eval f ctx ntrace) - (List.map (fun e -> _eval e ctx ntrace) args) + | Call (f, args) -> + (* we need to keep the trace from f and args evaluation + * else the trace will be truncated. + * we use _global_eval_trace to keep in memory previous steps *) + let ef = _eval f ctx trace in + let eargs = (List.map (fun e -> _eval e ctx (get_trace ())) args) in + eval_call (elexp_location f) f (get_trace ()) + ef + eargs
(* Case *) | Case (loc, target, pat, dflt) @@ -302,7 +305,8 @@ and eval_var ctx lxp v = elexp_fatal loc lxp ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ")
-and eval_call loc i f args = +(* unef: unevaluated function (to make the trace readable) *) +and eval_call loc unef i f args = match f, args with (* return result of eval *) | _, [] -> f @@ -315,8 +319,10 @@ and eval_call loc i f args = | (v::vs, Lambda ((_, x), e)) (* "Uncurry" on the fly. *) -> bindargs e vs (add_rte_variable (Some x) v ctx) - | ([], _) -> _eval e ctx i - | _ -> eval_call loc i (_eval e ctx i) vs in + | ([], _) -> + let trace = append_typer_trace i unef in + _eval e ctx trace + | _ -> eval_call loc unef i (_eval e ctx i) vs in bindargs e vs (add_rte_variable (Some x) v ctx)
| Vbuiltin (name), args @@ -326,8 +332,8 @@ and eval_call loc i f args = builtin loc i args (* Fast common case. *) else if nargs > arity then let rec split n vs acc = match (n, vs) with - | 0, _ -> let v = eval_call loc i f (List.rev acc) in - eval_call loc i v vs + | 0, _ -> let v = eval_call loc unef i f (List.rev acc) in + eval_call loc unef i v vs | _, (v::vs) -> split (n - 1) vs (v::acc) | _ -> error loc "Impossible!" in split nargs args [] @@ -417,10 +423,12 @@ and _eval_decls (decls: (vdef * elexp) list) (* Builtin Implementation (Some require eval) *)
and bind_impl loc depth args_val = + let trace_dum = (Var ((loc, "<dummy>"), -1)) in + match args_val with | [Vcommand (cmd); callback] -> (* bind returns another Vcommand *) - Vcommand (fun () -> eval_call loc depth callback [cmd ()]) + Vcommand (fun () -> eval_call loc trace_dum depth callback [cmd ()]) | _ -> error loc "Wrong number of args or wrong first arg value in `bind`"
and run_io loc depth args_val = @@ -503,7 +511,7 @@ and print_typer_trace trace = print_typer_trace' b
and print_trace title trace default = - (* If no trace is provided take the most revent one *) + (* If no trace is provided take the most recent one *) let trace = match trace with | Some trace -> trace | None -> default in
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -341,7 +341,9 @@ let lexp_name e = | Susp _ -> "Susp" | Builtin (_, _, None) -> "Builtin" | Builtin _ -> "AttributeTable" - | _ -> "lexp_to_string: not implemented" + | Metavar _ -> "Metavar" + | Sort _ -> "Sort" + | SortLevel _ -> "SortLevel"
(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp =
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -351,9 +351,9 @@ let _ = test_eval_eqv_named lambda (z : Int) -> x * y + z;"
"fun 2 1; - %fun (z := 1) (y := 2)" + fun 2 1"
- "3%; 3" + "3; 3"
(* run all tests *)
View it on GitLab: https://gitlab.com/monnier/typer/compare/133a2261c1981cf4344a2be3ad47e6ee55b...