[Typer] [Git][monnier/typer][master] 2 commits: eval removes old temporary variables from ctx between function calls

Setepenre pushed to branch master at Stefan / Typer

Commits: cdec9d9a by Pierre Delaunay at 2016-03-23T23:37:17-04:00 eval removes old temporary variables from ctx between function calls

Changes to be committed: * src/debruijn.ml : rollback, old dbi were correct * src/eval.ml : - ctx is reinitialized between calls - new function debug_eval (equiv to old eval) - eval does not print call_trace and context if an error is raised * tests/eval_test.ml : test ctx reinit * tests/full_debug.ml: use debug_eval instead of eval

- - - - - bd7fd362 by Pierre Delaunay at 2016-03-23T23:47:47-04:00 All tests are passed - Recursion with case are working

Changes to be committed: * minor modifications

- - - - -

5 changed files:

- − samples/test__.typer - src/debruijn.ml - src/eval.ml - tests/eval_test.ml - tests/full_debug.ml

Changes:

===================================== samples/test__.typer deleted ===================================== --- a/samples/test__.typer +++ /dev/null @@ -1,61 +0,0 @@ - - - -%a = lambda x -> -% let a1 : Nat; a1 = 2; b1 : Nat; b1 = 3; in -% a1 + b1 + x -%; - -% main = (a 2) - - -a = 2; - -Nat = inductive_ (dNat) (zero) (succ Nat); - -zero = inductive-cons Nat zero; -succ = inductive-cons Nat succ; - -one = (succ zero); -two = (succ one); -three = (succ two); - -tonum = lambda x -> case x - | (succ y) => (1 + (tonum y)) - | _ => 0 -; - -x = zero; -% main = zero; => zero(Nat[1]) -% main = x; => succ(Nat[2]) - -main = (tonum one); - - - -%================================ CALL TRACE ================================ -% size = 6 -%---------------------------------------------------------------------------- -%|+- Call: (tonum[1] zero[6]) -%|:+- Var: zero[6] -%|:+- Lambda: lambda (x: unkwn) -> case x[0]: unkwn| succ y -> 1 + (tonum[4] y[0]); | zero -> 0; -%|:|+- Case: case x[0]: unkwn| succ y -> 1 + (tonum[4] y[0]); | zero -> 0; -%|:|:+- Var: x[0] -%|:|:+- Imm: 0 -%============================================================================ - -%================================ CALL TRACE ================================ -% size = 11 -%---------------------------------------------------------------------------- -%|+- Call: (tonum[2] x[1]) -%|:+- Var: x[1] -%|:+- Lambda: lambda (x: unkwn) -> case x[0]: unkwn| succ y -> 1 + (tonum[2] y[0]); | _ -> 0; -%|:|+- Case: case x[0]: unkwn| succ y -> 1 + (tonum[2] y[0]); | _ -> 0; -%|:|:+- Var: x[0] -%|:|:+- Var: zero[6] -%|:|:+- Call: 1 + (tonum[2] y[0]) -%|:|:|+- Imm: 1 -%|:|:|+- Call: (tonum[2] y[0]) -%|:|:|:+- Var: y[0] -%|:|:|:+- Var: zero[6] -%============================================================================

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -90,11 +90,11 @@ let temp_scope ctx bound = let (a, b, c) = ctx in (a, b, bound) (* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: lexp_context): int = let ((n, map), _, (csize, rof)) = ctx in - let raw_idx = n - (StringMap.find name map) - 1 in + let raw_idx = n - (StringMap.find name map) - 1 in (* if raw_idx > (n - csize) then raw_idx - rof (* Shift if the variable is not bound *) - else - raw_idx + else *) + raw_idx ;;

(* We first add variable into our map. Later on, we will add them into

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -48,12 +48,6 @@ let eval_error loc msg = let dloc = dummy_location let eval_warning = msg_warning "EVAL"

-type call_trace_type = (int * lexp) list -let global_trace = ref [] - -let add_call cll i = global_trace := (i, cll)::!global_trace - - let print_myers_list l print_fun = let n = (length l) - 1 in

@@ -70,6 +64,18 @@ let print_myers_list l print_fun = print_string (make_sep '='); ;;

+let print_rte_ctx ctx = + let (l, b) = ctx in + print_myers_list l + (fun (n, g) -> + let _ = + match n with + | Some m -> lalign_print_string m 12; print_string " | " + | None -> print_string (make_line ' ' 12); print_string " | " in + lexp_print g; print_string "\n") +;; + + let get_int lxp = match lxp with | Imm(Integer(_, l)) -> l @@ -77,43 +83,77 @@ let get_int lxp = ;;

(* Runtime Environ *) -type runtime_env = (string option * lexp) myers -let make_runtime_ctx = nil;; -let add_rte_variable name x l = (cons (name, x) l);; +type runtime_env = ((string option * lexp) myers) * (int * int) + +let make_runtime_ctx = (nil, (0, 0));;

-let get_rte_variable (*name: string option*) (idx: int) (l: runtime_env): lexp = - (* FIXME: Check that the variable's name is right! *) - let (tn, x) = (nth idx l) in x +let add_rte_variable name x ctx = + let (l, b) = ctx in + let lst = (cons (name, x) l) in + (lst, b);;

- (* +let get_rte_variable (name: string option) (idx: int) (ctx: runtime_env): lexp = + let (l, _) = ctx in + let (tn, x) = (nth idx l) in match (tn, name) with - | (Some n1, Some n2) -> - if n1 = n2 then x else (eval_error dloc - ("Variable lookup failure. Expected: " ^ n2 ^ " got " ^ n1); x) - | _ -> x (* can't check variable's name *) *) + | (Some n1, Some n2) -> ( + if n1 = n2 then + x + else ( + eval_error dloc + ("Variable lookup failure. Expected: "" ^ n2 ^ "" got "" ^ n1 ^ """))) + + | _ -> x (* can't check variable's name (call args do not have names) *) ;;

-let get_rte_size (l: runtime_env): int = length l;; +let get_rte_size (ctx: runtime_env): int = let (l, b) = ctx in length l;;

-let print_rte_ctx l = print_myers_list l - (fun (n, g) -> - let _ = - match n with - | Some m -> lalign_print_string m 12; print_string " | " - | None -> print_string (make_line ' ' 12); print_string " | " in - lexp_print g; print_string "\n") +(* This function is used when we enter a new scope *) +let local_ctx ctx = + let (l, _) = ctx in + let osize = length l in + (l, (osize, 0)) ;;

+let select_n ctx n = + let (l, a) = ctx in + let r = ref nil in + let s = (length l) - 1in + + for i = 0 to n - 1 do + r := (cons (nth (s - i) l) (!r)); + done; + + ((!r), a) + +let temp_ctx ctx = + let (l, (osize, _)) = ctx in + let tsize = length l in + (* Check if temporary variables are present *) + if tsize != osize then + (* remove temp var *) + (select_n ctx osize) + else + ctx +;;

let nfirst_rte_var n ctx = let rec loop i acc = if i < n then - loop (i + 1) ((get_rte_variable i ctx)::acc) + loop (i + 1) ((get_rte_variable None i ctx)::acc) else List.rev acc in loop 0 [] ;;

+type call_trace_type = (int * lexp) list + +let global_trace = ref [] +let global_env = ref (nil, (0, 0)) +let _eval_max_recursion_depth = ref 255 + +let add_call cll i = global_trace := (i, cll)::!global_trace + (* currently, we don't do much *) type value_type = lexp

@@ -121,10 +161,12 @@ type value_type = lexp * 'i' is the recursion depth used to print the call trace *) let rec _eval lxp ctx i: (value_type) =

- (if i > 255 then + (if i > (!_eval_max_recursion_depth) then raise (internal_error "Recursion Depth exceeded"));

add_call lxp i; + global_env := ctx; (* Allow us to print the latest used environment *) + match lxp with (* This is already a leaf *) | Imm(v) -> lxp @@ -132,18 +174,18 @@ let rec _eval lxp ctx i: (value_type) = (* Return a value stored in the environ *) | Var((loc, name), idx) as e -> begin (* find variable binding i.e we do not want a another variable *) - let rec var_crawling expr i k = + let rec var_crawling expr k = (if k > 255 then( lexp_print expr; print_string "\n"; flush stdout; raise (internal_error "Variable lookup failed"))); match expr with - | Var(_, j) -> - let p = (get_rte_variable (i + j) ctx) in - var_crawling p (i + j) (k + 1) + | Var((_, name2), j) -> + let p = (get_rte_variable (Some name2) j ctx) in + var_crawling p (k + 1) | _ -> expr in

try - (var_crawling e 0 0) + (var_crawling e 0) with Not_found -> print_string ("Variable: " ^ name ^ " was not found | "); @@ -154,11 +196,13 @@ let rec _eval lxp ctx i: (value_type) = | Let(_, decls, inst) -> (* First we _evaluate all declaration then we eval the instruction *) let nctx = build_ctx decls ctx i in - _eval inst nctx (i + 1) + _eval inst (local_ctx nctx) (i + 1)

(* Function call *) | Call (lname, args) -> ( - (* Try to extract name *) + (* create a clean environment *) + let clean_ctx = temp_ctx ctx in + let n = List.length args in match lname with (* Hardcoded functions *) @@ -170,9 +214,9 @@ let rec _eval lxp ctx i: (value_type) = | Var((_, name), _) when name = "_+_" -> let nctx = build_arg_list args ctx i in

- let l = get_int (get_rte_variable 0 nctx) in - let r = get_int (get_rte_variable 1 nctx) in - Imm(Integer(dloc, l + r)) + let l = get_int (get_rte_variable (None) 0 nctx) in + let r = get_int (get_rte_variable (None) 1 nctx) in + Imm(Integer(dloc, l + r))

(* _*_ is read as a single function with x args *) | Var((_, name), _) when name = "_*_" -> @@ -181,17 +225,23 @@ let rec _eval lxp ctx i: (value_type) = let vint = (nfirst_rte_var n nctx) in let varg = List.map (fun g -> get_int g) vint in let v = List.fold_left (fun a g -> a * g) 1 varg in - - Imm(Integer(dloc, v)) + Imm(Integer(dloc, v))

(* This is a named function call *) | Var((_, name), idx) -> - (* get function body *) - let body = get_rte_variable idx ctx in + (* get function body from current context *) + let body = get_rte_variable (Some name) idx ctx in

- (* Add args in the scope *) - let nctx = build_arg_list args ctx i in - _eval body nctx (i + 1) + (* _eval every args using current context *) + let arg_val = + List.map (fun (k, e) -> _eval e ctx (i + 1)) args in + + (* Add args inside our clean context *) + let clean_ctx = + List.fold_left (fun c v -> add_rte_variable None v c) + clean_ctx arg_val in + + _eval body clean_ctx (i + 1)

(* TODO Everything else *) (* Which includes a call to a lambda *) @@ -203,8 +253,11 @@ let rec _eval lxp ctx i: (value_type) = (* handle partial application i.e build a new lambda if Partial App *) | Lambda(_, vr, _, body) -> begin let (loc, name) = vr in - (* Get first arg *) - let value = (get_rte_variable 0 ctx) in + + (* This was redundant since we already pushed args + * when processing the call expression *) + (* Get first arg * ) + let value = (get_rte_variable (Some name) 0 ctx) in let nctx = add_rte_variable (Some name) value ctx in

(* Collapse nested lambdas. Returns body *) @@ -213,14 +266,14 @@ let rec _eval lxp ctx i: (value_type) = | Lambda(_, vr, _, body) -> let (loc, name) = vr in (* Get Variable from call context *) - let value = (get_rte_variable idx ctx) in + let value = (get_rte_variable (Some name) idx ctx) in (* Build lambda context *) let nctx = add_rte_variable (Some name) value nctx in (collapse body (idx + 1) nctx) | _ -> bd, nctx in

- let body, nctx = collapse body 1 nctx in - _eval body nctx (i + 1) end + let body, nctx = collapse body 1 nctx in*) + _eval body ctx (i + 1) end

(* Inductive is a type declaration. We have nothing to eval *) | Inductive (_, _, _, _) as e -> e @@ -234,16 +287,19 @@ let rec _eval lxp ctx i: (value_type) = (* Eval target *) let v = _eval target ctx (i + 1) in

+ let (_, (osize, _)) = ctx in + let csize = get_rte_size ctx in + let offset = csize - osize in + (* V must be a constructor Call *) let ctor_name, args = match v with | Call(lname, args) -> (match lname with | Var((_, ctor_name), _) -> ctor_name, args | _ -> eval_error loc "Target is not a Constructor" )

- | Cons((_, idx), (_, cname)) -> begin + | Cons(((_, vname), idx), (_, cname)) -> begin (* retrieve type definition *) - - let info = get_rte_variable idx ctx in + let info = get_rte_variable (Some vname) (idx + offset) ctx in let ctor_def = match info with | Inductive(_, _, _, c) -> c | _ -> eval_error loc "Not an Inductive Type" in @@ -275,6 +331,13 @@ let rec _eval lxp ctx i: (value_type) = else false in

+ (* if the argument is a reference to a variable its index need to be + * shifted *) + let arg_shift xp offset = + match xp with + | Var(a, idx) -> Var(a, idx + offset) + | _ -> xp in + (* Search for the working pattern *) let sol = SMap.filter is_true pat in if SMap.is_empty sol then @@ -283,12 +346,21 @@ let rec _eval lxp ctx i: (value_type) = (* Get working pattern *) let key, (_, pat_args, exp) = SMap.min_binding sol in

+ (* count the number of declared variables *) + let case_offset = List.fold_left (fun i g -> + match g with None -> i | _ -> i + 1) + 0 pat_args in + + let toffset = case_offset + offset in + (* build context *) - let nctx = List.fold_left2 (fun nctx pat cl -> + let nctx = List.fold_left2 (fun nctx pat arg -> match pat with | None -> nctx - | Some (_, (_, name)) -> let (_, xp) = cl in - add_rte_variable (Some name) xp nctx) + | Some (_, (_, name)) -> + let (_, xp) = arg in + let xp = (arg_shift xp toffset) in + add_rte_variable (Some name) xp nctx)

ctx pat_args args in (* eval body *) @@ -324,7 +396,8 @@ and eval_decls (decls: ((vdef * lexp * ltype) list)) let nctx = add_rte_variable (Some n) lxp ctx in loop tl nctx in

- loop decls ctx + let nctx = loop decls ctx in + (local_ctx nctx)

and print_eval_result i lxp = print_string " Out["; @@ -352,26 +425,34 @@ and print_call_trace () = ;;

let eval lxp ctx = + global_trace := []; + _eval lxp ctx 1 + +let debug_eval lxp ctx = try - _eval lxp ctx 1 + eval lxp ctx with e -> ( - print_rte_ctx ctx; + print_rte_ctx (!global_env); print_call_trace (); raise e) ;;

(* Eval a list of lexp *) -let eval_all lxps rctx = - global_trace := []; - List.map (fun g -> eval g rctx) lxps;; +let eval_all lxps rctx silent = + if silent then + List.map (fun g -> eval g rctx) lxps + else + List.map (fun g -> debug_eval g rctx) lxps;;

(* Eval String * ---------------------- *) -let eval_expr_str str lctx rctx = +let _eval_expr_str str lctx rctx silent = let lxps = lexp_expr_str str lctx in - (eval_all lxps rctx) + (eval_all lxps rctx silent) ;;

+let eval_expr_str str lctx rctx = _eval_expr_str str lctx rctx false + let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in (eval_decls lxps rctx), lctx

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -1,50 +1,51 @@ open Lparse (* add_def *) open Debruijn (* make_lexp_context *) open Eval (* make_rte_ctx *) -open Utest_lib +open Utest_lib +open Util +open Lexp

(* default environment *) let lctx = make_lexp_context let lctx = add_def "_+_" lctx let lctx = add_def "_*_" lctx -let rctx = make_runtime_ctx -let rctx = add_rte_variable (Some "_+_") dlxp rctx -let rctx = add_rte_variable (Some "_-_") dlxp rctx - - +let rctx = make_runtime_ctx +let rctx = add_rte_variable (Some "_+_") iop_binary rctx +let rctx = add_rte_variable (Some "_-_") iop_binary rctx + let _ = (add_test "EVAL" "Variable Cascade" (fun () -> - + let dcode = " - a = 10; - b = a; - c = b; + a = 10; + b = a; + c = b; d = c;" in - + let rctx, lctx = eval_decl_str dcode lctx rctx in - + let ecode = "d;" in - + let ret = eval_expr_str ecode lctx rctx in - + match ret with | [r] -> expect_equal_int (get_int r) 10 | _ -> failure ()) );; - - + + (* Let * ------------------------ *) - + let _ = (add_test "EVAL" "Let" (fun () -> (* Noise. Makes sure the correct variables are selected *) let dcode = " c = 3; e = 1; f = 2; d = 4;" in let rctx, lctx = eval_decl_str dcode lctx rctx in - + let ecode = " let a = 10; x = 50; y = 60; b = 20; in a + b;" in - + let ret = eval_expr_str ecode lctx rctx in (* Expect a single result *) match ret with @@ -59,7 +60,7 @@ let _ = (add_test "EVAL" "Let" (fun () -> let _ = (add_test "EVAL" "Lambda" (fun () -> (* Declare lambda *) let rctx, lctx = eval_decl_str "sqr = lambda x -> x * x;" lctx rctx in - + (* Eval defined lambda *) let ret = eval_expr_str "(sqr 4);" lctx rctx in (* Expect a single result *) @@ -72,11 +73,11 @@ let _ = (add_test "EVAL" "Lambda" (fun () -> let _ = (add_test "EVAL" "Nested Lambda" (fun () -> let code = " sqr = lambda x -> x * x; - cube = lambda x -> x * (sqr x); " in - + cube = lambda x -> x * (sqr x);" in + (* Declare lambda *) let rctx, lctx = eval_decl_str code lctx rctx in - + (* Eval defined lambda *) let ret = eval_expr_str "(cube 4);" lctx rctx in (* Expect a single result *) @@ -86,22 +87,42 @@ let _ = (add_test "EVAL" "Nested Lambda" (fun () -> ) ;;

+(* This makes sure contexts are reinitialized between calls + * i.e the context should not grow *) +let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> + let code = " + infinity = lambda beyond -> (infinity beyond);" in + + let rctx, lctx = eval_decl_str code lctx rctx in + + (* Expect throwing *) + try (* use the silent version as an error will be thrown *) + let _ = _eval_expr_str "(infinity 0);" lctx rctx true in + failure () + with + Internal_error m -> + if m = "Recursion Depth exceeded" then + success () + else + failure () +));; + (* Cases + Inductive types * ------------------------ *) - + let _ = (add_test "EVAL" "Case" (fun () -> (* Inductive type declaration + Noisy declarations *) let code = " i = 90;\n idt = inductive_ (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt);\n j = 100;\n - + d = 10;\n ctr0 = inductive-cons idt ctr0;\n e = 20;\n ctr1 = inductive-cons idt ctr1;\n f = 30;\n ctr2 = inductive-cons idt ctr2;\n g = 40;\n ctr3 = inductive-cons idt ctr2;\n h = 50;\n - + x = 1;\n a = (ctr1 (ctr2 ctr0));\n y = 2;\n b = (ctr2 (ctr2 ctr0));\n z = 3;\n @@ -111,17 +132,17 @@ let _ = (add_test "EVAL" "Case" (fun () -> | ctr1 l => 1\n | ctr2 l => 2\n | _ => 3;\n" in - + let rctx, lctx = eval_decl_str code lctx rctx in - + let rcode = "(test_fun a); (test_fun b); (test_fun c)"in - + (* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in (* Expect 3 results *) match ret with - | [a; b; c] -> - let t1 = expect_equal_int (get_int a) 1 in + | [a; b; c] -> + let t1 = expect_equal_int (get_int a) 1 in let t2 = expect_equal_int (get_int b) 2 in let t3 = expect_equal_int (get_int c) 3 in if t1 = 0 && t2 = 0 && t3 = 0 then @@ -138,28 +159,28 @@ let _ = (add_test "EVAL" "Recursive Call" (fun () -> let code = " a = 1;\n Nat = inductive_ (dNat) (zero) (succ Nat); b = 2;\n - + zero = inductive-cons Nat zero; c = 3;\n succ = inductive-cons Nat succ; d = 4;\n - + one = (succ zero); e = 5;\n two = (succ one); f = 6;\n three = (succ three); g = 7;\n

- tonum = lambda x -> case x + tonum = lambda x -> case x | (succ y) => (1 + (tonum y)) - | _ => 0;" in - + | zero => 0;" in + let rctx, lctx = eval_decl_str code lctx rctx in - - let rcode = "(tonum zero); (tonum zero); (tonum zero);"in - + + let rcode = "(tonum zero); (tonum one); (tonum two);"in + (* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in (* Expect a 3 results *) match ret with - | [a; b; c] -> - let t1 = expect_equal_int (get_int a) 0 in + | [a; b; c] -> + let t1 = expect_equal_int (get_int a) 0 in let t2 = expect_equal_int (get_int b) 1 in let t3 = expect_equal_int (get_int c) 2 in if t1 = 0 && t2 = 0 && t3 = 0 then

===================================== tests/full_debug.ml ===================================== --- a/tests/full_debug.ml +++ b/tests/full_debug.ml @@ -81,7 +81,7 @@ let arg_defs = [ add_p_option "sexp" (); add_p_option "pexp" (); add_p_option "lexp" ()), - " Print all compilation step with debug info"); + " Print all debug info"); ];;

let parse_args () = @@ -172,9 +172,9 @@ let main () = (* Push main args here if any *)

(* get main body *) - let body = (get_rte_variable main rctx) in + let body = (get_rte_variable (Some "main") main rctx) in (* eval main *) - let r = (eval body rctx) in + let r = (debug_eval body rctx) in print_eval_result 0 r

with

View it on GitLab: https://gitlab.com/monnier/typer/compare/aa416638d2073a688f3c9cb00e27bcbe9d5...