Stefan pushed to branch master at Stefan / Typer

Commits: e134b211 by Stefan Monnier at 2016-10-04T21:04:33-04:00 * src/eval.ml (from_lctx): Rewrite to obey the db_offset

* src/debruijn.ml (lexp_ctx_cons): Tighten the check.

* src/env.ml (value_type): Use runtime_env. (runtime_env): Drop the extra two integers. (env_cell): Make the var's name immutable. (get_rte_variable, get_rte_size, add_rte_variable, print_rte_ctx): Adjust accordingly. (set_rte_variable): Adjust and make return type be unit. (get_rte_size, is_free_var, rte_shift): Remove.

* src/myers.ml (fold_left, fold_right, map, iteri): New functions.

* tests/env_test.ml: Don't use the return value of set_rte_variable.

- - - - -

6 changed files:

- src/debruijn.ml - src/env.ml - src/eval.ml - src/lparse.ml - src/myers.ml - tests/env_test.ml

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -109,7 +109,12 @@ let lexp_ctx_cons (ctx : lexp_context) offset d v t = assert (offset >= 0 && (ctx = M.nil || let (previous_offset, _, _, _) = M.car ctx in - previous_offset >= 0 && previous_offset <= 1 + offset)); + previous_offset >= 0 (* General constraint. *) + (* Either `ctx` is self-standing (doesn't depend on us), + * or it depends on us (and maybe other bindings to come), in + * which case we have to depend on the exact same bindings. *) + && (previous_offset <= 1 + || previous_offset = 1 + offset))); M.cons (offset, d, v, t) ctx

let lctx_extend (ctx : lexp_context) (def: vdef) (v: varbind) (t: lexp) =

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -55,13 +55,17 @@ type value_type = | Vcons of symbol * value_type list | Vbuiltin of string | Vfloat of float - | Closure of string * elexp * (((string option * value_type) ref M.myers) * (int * int)) + | Closure of string * elexp * runtime_env | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vdummy | 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 = @@ -138,26 +142,16 @@ let value_name v = | Vout _ -> "Vout" | Vcommand _ -> "Vcommand"

-(* Runtime Environ *) -type env_cell = (string option * value_type) ref -type runtime_env = (env_cell M.myers) * (int * int) - -let make_runtime_ctx = (M.nil, (0, 0)) +let make_runtime_ctx = M.nil

-let get_rte_size (ctx: runtime_env): int = let (l, _) = ctx in M.length l - -let is_free_var idx ctx = - let (l, (osize, _)) = ctx in - let tsize = (get_rte_size ctx) - osize in - if idx > tsize then true else false +let get_rte_size (ctx: runtime_env): int = M.length ctx

let get_rte_variable (name: string option) (idx: int) - (ctx: runtime_env): value_type = - let (l, _) = ctx in + (ctx: runtime_env): value_type = try ( - let ref_cell = (M.nth idx l) in - let (tn, x) = !ref_cell in - match (tn, name) with + let (defname, ref_cell) = (M.nth idx ctx) in + let x = !ref_cell in + match (defname, name) with | (Some n1, Some n2) -> ( if n1 = n2 then x @@ -172,34 +166,21 @@ let get_rte_variable (name: string option) (idx: int) env_error dloc ("Variable lookup failure. Var: "" ^ n ^ "" idx: " ^ (str_idx idx))

-let rte_shift vref ctx = - let (_, (osize, _)) = ctx in (* number of variable declared outside *) - let csize = get_rte_size ctx in (* current size *) - let offset = csize - osize in - let ((loc, name), idx) = vref in - (* check if variable is free *) - let offset = if idx > offset then offset else 0 in - (* shift idx *) - idx + offset - -let add_rte_variable name (x: value_type) (ctx: runtime_env): runtime_env = - let (l, b) = ctx in - let lst = (M.cons (ref (name, x)) l) in - (lst, b) +let add_rte_variable name (x: value_type) (ctx: runtime_env) + : runtime_env = + let valcell = ref x in + M.cons (name, valcell) ctx

-let set_rte_variable idx name (lxp: value_type) ctx = - let (l, _) = ctx in - let ref_cell = (M.nth idx l) in - let (n, _) = !ref_cell in +let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = + let (n, ref_cell) = (M.nth idx ctx) in

- match (n, name) with - | Some n1, Some n2 -> - if (n1 != n2) then - env_error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) - else( - ref_cell := (name, lxp); ctx) + (match (n, name) with + | Some n1, Some n2 -> + if (n1 != n2) then + env_error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) + | _ -> ());

- | _ -> ref_cell := (name, lxp); ctx + ref_cell := v

(* This function is used when we enter a new scope *) @@ -260,14 +241,14 @@ let print_myers_list l print_fun = print_string (make_sep '=')

let print_rte_ctx (ctx: runtime_env) = - let (l, b) = ctx in - print_myers_list l - (fun x -> - let (n, g) = !x in - let _ = + print_myers_list + ctx + (fun (n, vref) -> + let g = !vref in + let _ = match n with - | Some m -> lalign_print_string m 12; print_string " | " - | None -> print_string (make_line ' ' 12); print_string " | " in + | 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")

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -64,7 +64,7 @@ let _builtin_lookup = ref SMap.empty

(* This is an internal definition * 'i' is the recursion depth used to print the call trace *) -let rec _eval lxp ctx i: (value_type) = +let rec _eval lxp (ctx : Env.runtime_env) i: (value_type) = let tloc = elexp_location lxp in

(if i > (!_eval_max_recursion_depth) then @@ -204,9 +204,9 @@ and _eval_decls (decls: (vdef * elexp) list) add_rte_variable (Some name) Vdummy ctx) ctx decls in

List.iteri (fun idx ((_, name), lxp) -> - let lxp = _eval lxp nctx (i + 1) in + let v = _eval lxp nctx (i + 1) in let offset = n - idx in - ignore (set_rte_variable offset (Some name) lxp nctx)) decls; + ignore (set_rte_variable offset (Some name) v nctx)) decls;

nctx and eval_decls_toplevel (decls: (vdef * elexp) list list) ctx = @@ -371,34 +371,44 @@ let eval_all lxps rctx silent = List.map (fun g -> evalfun g rctx) lxps

-let maybe s = match s with Some v -> v | _ -> "" - -(* build a rctx from a lctx, rm is used to ignore the last 'rm' elements *) -let from_lctx (ctx: elab_context) rm: runtime_env = - let ((n, _), env, _) = ctx in - let n = n - 1 in - let rctx = ref make_runtime_ctx in - - (* FIXME: Why not use Myers.map (Myers.nthcdr) ? *) - for i = 0 to (n - rm) do - let name, exp = match (Myers.nth (n - i) env) with - | (_, Some (_, name), LetDef exp, _) -> Some name, Some exp - | (_, Some (_, name), _, _) -> Some name, None - | _ -> None, None in - - let vxp = match exp with - | Some lxp -> - let octx = add_rte_variable name Vdummy (!rctx) in - let lxp = (OL.erase_type lxp) in - (try (eval lxp octx) - with e -> elexp_print lxp; - print_string "\n"; raise e) - - (* Happen once *) - | None -> eval_warning dloc ("Unable to eval expr: " ^ (maybe name)); - Vdummy in - - rctx := add_rte_variable name vxp (!rctx) - done; - - !rctx +let varname s = match s with Some (_, v) -> v | _ -> "<anon>" + +(* build a rctx from a lctx. *) +let from_lctx (ctx: elab_context): runtime_env = + let (_, lctx, _) = ctx in + let rctx : runtime_env + = M.map (fun (_, oname, _, _) + -> (match (oname : symbol option) with + | Some (_, name) -> Some name + | _ -> None), + ref Vdummy) + lctx in + + (* Then fill each slot in turn. *) + let _, evals + = M.fold_left + (fun (i, evals) (o, oname, def, _) + -> match def with + | LetDef lxp + -> (let elxp = OL.erase_type lxp in + let (_, valcell) = M.nth i rctx in + let octx = M.nthcdr (i - o + 1) rctx in + (i + 1, (valcell, elxp, octx) :: evals)) + | _ + (* 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 `" + ^ varname oname ^ "`"); + (i + 1, evals)) + (0, []) lctx in + (* The evaluations have to be done "from the end of the list". *) + List.iter (fun (valcell, elxp, octx) + -> try valcell := eval elxp octx + with e -> (* print_lexp_ctx (ectx_to_lctx ctx); *) + print_string "eval-in-from_lctx failed on: "; + (* lexp_print lxp; print_string "\nerased to: "; *) + elexp_print elxp; + print_string "\n"; raise e) + evals; + + rctx

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -497,7 +497,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let args = [(Aexplicit, body); (Aexplicit, (olist2tlist_lexp sargs ctx))] in let macro = Call(macro_expand, args) in let emacro = OL.erase_type macro in - let rctx = (from_lctx ctx 0) in + let rctx = from_lctx ctx in

_global_eval_trace := [];

@@ -721,7 +721,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = let arg = olist2tlist_lexp sargs ctx in let lxp = Call(lxp, [(Aexplicit, arg)]) in let elexp = OL.erase_type lxp in - let rctx = (from_lctx ctx 0) in + let rctx = from_lctx ctx in

(* get a list of declaration *) let decls = eval elexp rctx in

===================================== src/myers.ml ===================================== --- a/src/myers.ml +++ b/src/myers.ml @@ -112,3 +112,15 @@ let rec findcdr p l = | Mcons (x, _, _, _) when p x -> last | Mcons (_, l1, _, l2) -> findcdr2 (Some l) l1 l2 in findcdr1 None l + +let rec fold_left f i l = match l with + | Mnil -> i + | Mcons (x, l, _, _) -> fold_left f (f i x) l + +let rec fold_right f l i = match l with + | Mnil -> i + | Mcons (x, l, _, _) -> f x (fold_right f l i) + +let map f l = fold_right (fun x l' -> cons (f x) l') l nil + +let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l

===================================== tests/env_test.ml ===================================== --- a/tests/env_test.ml +++ b/tests/env_test.ml @@ -61,9 +61,11 @@ let _ = (add_test "ENV" "Set Variables" (fun () ->

print_rte_ctx rctx;

- let rctx, _ = List.fold_left (fun (ctx, idx) (n, _, v) -> - ((set_rte_variable idx n (Vdummy) ctx), idx - 1)) - (rctx, n) var in + let rctx, _ = List.fold_left + (fun (ctx, idx) (n, _, v) -> + (set_rte_variable idx n (Vdummy) ctx); + (ctx, idx - 1)) + (rctx, n) var in

print_rte_ctx rctx;

View it on GitLab: https://gitlab.com/monnier/typer/commit/e134b2115e1a7b25f9b70574130d27d94b79...