Stefan pushed to branch master at Stefan / Typer

Commits: 1d2bbfca by Stefan Monnier at 2016-09-19T17:46:29-04:00 * src/debruijn.ml (elab_context): Rename from lexp_context.

- - - - -

7 changed files:

- src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/eval.ml - src/lexp.ml - src/lparse.ml

Changes:

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -127,7 +127,7 @@ let ierase_type (lexps: (ldecl list list * lexpr list)) = (List.map OL.clean_decls ldecls), (List.map OL.erase_type lexprs)

-let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * lexp_context) = +let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = let pdecls, pexprs = pexps in let ldecls, lctx = lexp_p_decls pdecls lctx in let lexprs = lexp_parse_all pexprs lctx in

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -363,7 +363,7 @@ let builtin_macro = [ ]

type macromap = - (location -> lexp list -> lexp_context -> lexp -> (lexp * lexp)) SMap.t + (location -> lexp list -> elab_context -> lexp -> (lexp * lexp)) SMap.t

let macro_impl_map : macromap = List.fold_left (fun map (name, funct) ->

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -73,10 +73,9 @@ type scope = db_ridx StringMap.t (* Map<String, db_ridx>*) type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope

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

(* Extract the lexp context from the context used during elaboration. *) let ectx_to_lctx (ectx : elab_context) : env_type = @@ -88,19 +87,19 @@ 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: lexp_context): env_type = let (_, ev, _) = ctx in ev +let _get_env(ctx: elab_context): env_type = let (_, ev, _) = ctx in ev

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

-let make_lexp_context = (_make_senv_type, _make_myers, PropertyMap.empty) +let make_elab_context = (_make_senv_type, _make_myers, PropertyMap.empty)

let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof

let get_size ctx = let ((n, _), _, _) = ctx in n

(* return its current DeBruijn index *) -let rec senv_lookup (name: string) (ctx: lexp_context): int = +let rec senv_lookup (name: string) (ctx: elab_context): int = let ((n, map), _, _) = ctx in let raw_idx = n - (StringMap.find name map) - 1 in (* if raw_idx > (n - csize) then @@ -108,7 +107,7 @@ let rec senv_lookup (name: string) (ctx: lexp_context): int = else *) raw_idx

-let env_extend (ctx: lexp_context) (def: vdef) (v: varbind) (t: lexp) = +let env_extend (ctx: elab_context) (def: vdef) (v: varbind) (t: lexp) = let (loc, name) = def in let ((n, map), env, f) = ctx in (try let _ = senv_lookup name ctx in @@ -165,7 +164,7 @@ let env_lookup_expr ctx (v : vref): lexp option = | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r))) | _ -> None

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

(* replace an expression by another *) @@ -204,7 +203,7 @@ let replace_by ctx name by =

let add_property ctx (var_i, var_n) (att_i, att_n) (prop: lexp) - : lexp_context = + : elab_context =

let (a, b, property_map) = ctx in let n = get_size ctx in

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

(* get typecheck context *) - let lctx_to_cctx (lctx: lexp_context) = + let lctx_to_cctx (lctx: elab_context) = let (_, env, _) = ctx in env in

(if (get_p_option "typecheck") then(

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -374,11 +374,12 @@ let eval_all lxps rctx silent = 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: lexp_context) rm: runtime_env = +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

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -767,9 +767,8 @@ and _lexp_to_str ctx exp = | Builtin ((_, name), _) -> name

| Sort (_, Stype lvl) -> (match lvl with - | SortLevel (SLn 0) -> "Type" - | SortLevel (SLn v) -> "Type" ^ (string_of_int v) - | _ -> "Type") + | SortLevel (SLn v) -> "Type_" ^ (string_of_int v) + | _ -> "Type_?")

| _ -> print_string "Printing Not Implemented"; "-- --"

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -64,7 +64,7 @@ let lexp_warning = msg_warning "LPARSE" let lexp_error = msg_error "LPARSE" let lexp_fatal = msg_fatal "LPARSE"

-let _global_lexp_ctx = ref make_lexp_context +let _global_lexp_ctx = ref make_elab_context let _global_lexp_trace = ref [] let _parsing_internals = ref false let btl_folder = ref "./btl/" @@ -83,7 +83,7 @@ let _type_shift tp i = | Var(v, idx) -> Var(v, idx) | expr -> expr

-let ctx_define (ctx: lexp_context) var lxp ltype = +let ctx_define (ctx: elab_context) var lxp ltype = let (_, cctx, _) = ctx in if OL.conv_p ltype (OL.check cctx lxp) then env_extend ctx var (LetDef lxp) ltype @@ -102,7 +102,7 @@ let ctx_define (ctx: lexp_context) var lxp ltype = (* The main job of lexp (currently) is to determine variable name (index) * and to regroup type specification with their variable * - * lexp_context is composed of two environment: senv and env. + * elab_context is composed of two environment: senv and env. * the senv environment is used to find the correct debruijn index * while the env environment is used to save variable information. * the env environment look a lot like the runtime environment that will be @@ -139,10 +139,10 @@ let build_var name ctx = let type0_idx = senv_lookup name ctx in Var((dloc, name), type0_idx)

-let rec lexp_p_infer (p : pexp) (ctx : lexp_context): lexp * ltype = +let rec lexp_p_infer (p : pexp) (ctx : elab_context): lexp * ltype = _lexp_p_infer p ctx 1

-and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = +and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =

let lexp_infer p ctx = _lexp_p_infer p ctx (i + 1) in let tloc = pexp_location p in @@ -292,10 +292,10 @@ and lexp_let_decls decls (body: lexp) ctx i = List.fold_left (fun lxp decls -> Let(dloc, decls, lxp)) body decls

-and lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context): lexp = +and lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context): lexp = _lexp_p_check p t ctx 1

-and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = +and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) i: lexp = let tloc = pexp_location p in

_global_lexp_ctx := ctx; @@ -550,7 +550,7 @@ and lexp_get_inductive_type loc ctor_name ctx : (string * lexp option) =

(* Read a pattern and create the equivalent representation *) and lexp_read_pattern pattern exp target ctx: - ((string * location * (arg_kind * vdef option) list) * lexp_context) = + ((string * location * (arg_kind * vdef option) list) * elab_context) =

match pattern with | Ppatany (loc) -> (* Catch all expression nothing to do *) @@ -605,7 +605,7 @@ and lexp_read_pattern pattern exp target ctx:

(* Read patterns inside a constructor *) and lexp_read_pattern_args args (args_type : lexp list) ctx: - (((arg_kind * vdef option) list) * lexp_context)= + (((arg_kind * vdef option) list) * elab_context)=

let length_type = List.length args_type in let length_pat = List.length args in @@ -667,7 +667,7 @@ and lexp_parse_inductive ctors ctx i =

(* Macro declaration handling, return a list of declarations * to be processed *) -and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = +and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = (* lookup for mname_ *) let idx = try senv_lookup mname ctx with Not_found -> @@ -809,7 +809,7 @@ and lexp_detect_recursive pdecls = (List.rev !decls)

-and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * lexp_context) = +and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * elab_context) = (* detect mutually recursive def and merge definition *) let decls = lexp_detect_recursive decls in let all = ref [] in @@ -884,7 +884,7 @@ and _lexp_rec_decl decls ctx i = and lexp_decls_toplevel decls ctx = _lexp_decls decls ctx 1

-and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list = +and _lexp_parse_all (p: pexp list) (ctx: elab_context) i : lexp list =

let rec loop (plst: pexp list) ctx (acc: lexp list) = match plst with @@ -895,7 +895,7 @@ and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list = (loop p ctx [])

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

print_string (make_title " LEXP CONTEXT "); @@ -1001,7 +1001,7 @@ let lexp_parse_all p ctx = _lexp_parse_all p ctx 1 let default_lctx, default_rctx =

(* Empty context *) - let lctx = make_lexp_context in + let lctx = make_elab_context in let lctx = ctx_define lctx (dloc, "Type1") type1 type2 in let lctx = ctx_define lctx (dloc, "Type") type0 type1 in (* FIXME: Add builtins directly here. *) @@ -1047,7 +1047,7 @@ let default_lctx, default_rctx =

(* Lexp helper *) let _lexp_expr_str (str: string) (tenv: token_env) - (grm: grammar) (limit: string option) (ctx: lexp_context) = + (grm: grammar) (limit: string option) (ctx: elab_context) = let pxps = _pexp_expr_str str tenv grm limit in lexp_parse_all pxps ctx

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