Stefan pushed to branch master at Stefan / Typer

Commits: 9bb74c93 by Stefan Monnier at 2016-09-29T00:10:31-04:00 * src/opslexp.ml (lookup_type, lookup_value): Move to debruijn.ml

* src/debruijn.ml (_get_env): Remove functions. (env_lookup_by_index, print_lexp_ctx): Change ctx type. (lctx_lookup): Rename from _env_lookup; change ctx type. (lctx_lookup_type, lctx_lookup_value): Move from opslexp.ml; use lctx_lookup. (env_lookup_type, env_lookup_expr): Use them.

- - - - -

5 changed files:

- src/REPL.ml - src/debruijn.ml - src/debug_util.ml - src/lparse.ml - src/opslexp.ml

Changes:

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -216,7 +216,7 @@ let rec repl i clxp rctx = | "%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 clxp; repl clxp rctx) + | "%info" | "%i" -> (print_lexp_ctx (ectx_to_lctx clxp); repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace (); repl clxp rctx)

(* command with arguments *)

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -89,7 +89,6 @@ let ectx_to_lctx (ectx : elab_context) : lexp_context = let _make_scope = StringMap.empty let _make_senv_type = (0, _make_scope) let _make_myers = M.nil -let _get_env(ctx: elab_context): lexp_context = let (_, ev, _) = ctx in ev

(* Public methods: DO USE * ---------------------------------- *) @@ -158,12 +157,12 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = recursion_offset - 1) (ctx, List.length defs) defs

-let env_lookup_by_index index (ctx: elab_context): env_elem = - (Myers.nth index (_get_env ctx)) +let env_lookup_by_index index (ctx: lexp_context): env_elem = + Myers.nth index ctx

(* Print context *) -let print_lexp_ctx (ctx : elab_context) = - let ((n, map), env, f) = ctx in +let print_lexp_ctx (ctx : lexp_context) = + let n = M.length ctx in

print_string (make_title " LEXP CONTEXT ");

@@ -187,15 +186,12 @@ let print_lexp_ctx (ctx : elab_context) = | _ -> "" in extract_names tl (name::acc) in

- let ord = extract_names env [] in + let ord = extract_names ctx [] in

let rec _print idx ord = match ord with | [] -> () | hd::tl ->( - let idx2 = StringMap.find hd map in - - (if idx2 != idx then ());

print_string " | "; lalign_print_string hd 10; print_string " | "; lalign_print_int (n - idx - 1) 7; @@ -243,11 +239,10 @@ let _name_error loc estr str ctx =

(* generic lookup *) -let _env_lookup ctx (v: vref): env_elem = - let ((dv_size, _), info_env, _) = ctx in +let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = let ((loc, ename), dbi) = v in

- try(let ret = (Myers.nth dbi info_env) in + try(let ret = (Myers.nth dbi ctx) in let _ = match ret with | (_, Some (_, name), _, _) -> (* Check if names match *) @@ -259,17 +254,23 @@ let _env_lookup ctx (v: vref): env_elem = Not_found -> debruijn_error loc "DeBruijn index out of bounds!"

+ +let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = + let (_, i) = vref in + let (_, _, _, t) = lctx_lookup ctx vref in + mkSusp t (S.shift (i + 1)) + +let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option = + let (_, i) = vref in + match lctx_lookup ctx vref with + | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) + | _ -> None + let env_lookup_type ctx (v : vref): lexp = - let (_, idx) = v in - let (_, _, _, ltp) = _env_lookup ctx v in - mkSusp ltp (S.shift (idx + 0)) + lctx_lookup_type (ectx_to_lctx ctx) v

let env_lookup_expr ctx (v : vref): lexp option = - let (_, idx) = v in - let (r, _, lxp, _) = _env_lookup ctx v in - match lxp with - | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r))) - | _ -> None + lctx_lookup_value (ectx_to_lctx ctx) v

(* replace an expression by another *) (* Most of the time it should be O(1) but it can be O(n) *)

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -345,7 +345,7 @@ let main () = debug_lexp_decls flexps; print_string "\n"));

(if (get_p_option "lctx") then( - print_lexp_ctx nctx; print_string "\n")); + print_lexp_ctx (ectx_to_lctx nctx); print_string "\n"));

let clean_lxp = List.map OL.clean_decls lexps in

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -433,7 +433,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = "Expected non-explicit arg" | t -> lexp_print t; print_string "\n"; - print_lexp_ctx ctx; + print_lexp_ctx (ectx_to_lctx ctx); lexp_fatal (sexp_location sarg) "Explicit arg to non-function") in

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -45,16 +45,8 @@ let impredicative_erase = true (* Allows erasable args to be impredicative. *)

(* Lexp context *)

-let lookup_type (ctx : DB.lexp_context) vref = - let (_, i) = vref in - let (_, _, _, t) = Myers.nth i ctx in - mkSusp t (S.shift (i + 1)) - -let lookup_value (ctx : DB.lexp_context) vref = - let (_, i) = vref in - match Myers.nth i ctx with - | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) - | _ -> None +let lookup_type = DB.lctx_lookup_type +let lookup_value = DB.lctx_lookup_value

(********* Testing if two types are "convertible" aka "equivalent" *********)

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