Stefan pushed to branch master at Stefan / Typer

Commits: b0866ba1 by Stefan Monnier at 2016-09-19T17:52:08-04:00 * src/debruijn.ml (lexp_context): Rename from env_type.

- - - - -

3 changed files:

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

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -37,7 +37,6 @@ open Lexp module L = Lexp open Myers open Fmt -(*open Typecheck env_elem and env_type *)

module S = Subst

@@ -62,7 +61,7 @@ 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 env_type = env_elem myers +type lexp_context = env_elem myers

type db_idx = int (* DeBruijn index. *) type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *) @@ -75,10 +74,10 @@ type senv_type = senv_length * scope

(* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) -type elab_context = senv_type * env_type * property_env +type elab_context = senv_type * lexp_context * property_env

(* Extract the lexp context from the context used during elaboration. *) -let ectx_to_lctx (ectx : elab_context) : env_type = +let ectx_to_lctx (ectx : elab_context) : lexp_context = let (_, lctx, _) = ectx in lctx

(* internal definitions @@ -87,7 +86,7 @@ let ectx_to_lctx (ectx : elab_context) : env_type = let _make_scope = StringMap.empty let _make_senv_type = (0, _make_scope) let _make_myers = nil -let _get_env(ctx: elab_context): env_type = let (_, ev, _) = ctx in ev +let _get_env(ctx: elab_context): lexp_context = let (_, ev, _) = ctx in ev

(* Public methods: DO USE * ---------------------------------- *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -911,7 +911,7 @@ and print_lexp_ctx (ctx : elab_context) =

(* it is annoying to print according to StringMap order *) (* let's use myers list order *) - let rec extract_names (lst: env_type) acc = + let rec extract_names (lst: lexp_context) acc = match lst with | Mnil-> acc | Mcons (hd, tl, _, _) ->

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -41,14 +41,12 @@ let conv_erase = true (* If true, conv ignores erased terms. *)

(* Lexp context *)

-type lexp_context = DB.env_type - -let lookup_type (ctx : lexp_context) vref = +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 : lexp_context) vref = +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))) @@ -133,7 +131,7 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let rec lexp_whnf e (ctx : lexp_context) = match e with +let rec lexp_whnf e (ctx : DB.lexp_context) = match e with (* | Let (_, defs, body) -> FIXME!! Need recursive substitutions! *) | Var v -> (match lookup_value ctx v with | None -> e

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