Stefan pushed to branch master at Stefan / Typer
Commits: ad319791 by Stefan Monnier at 2016-09-14T14:49:44-04:00 Type check values added via env_extend
* src/debruijn.ml (elab_context): New name. (ectx_to_lctx): New function. (ectx_extend_rec): New function. (env_extend): Use 0 as db_offset since these are non-recursive.
* src/lparse.ml (_shift_glob): Remove. (senv_lookup): Don't redefine. (ctx_define): New function. (lexp_call): Update to new arg type of lexp_whnf. (lexp_read_pattern): Use ctx_define. (_lexp_rec_decl.tctx): Rename `expr` -> `decl` since it's a declaration. (default_lctx): Use ctx_define.
* src/opslexp.ml (lookup_type, lookup_value): Move earlier. (conv_p'): Use structural equality for sorts. (lexp_whnf): Don't use elab_context since this is also used elsewhere.
- - - - -
3 changed files:
- src/debruijn.ml - src/lparse.ml - src/opslexp.ml
Changes:
===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -61,6 +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 db_idx = int (* DeBruijn index. *) @@ -72,7 +73,14 @@ 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 + * a lexp context plus some side info. *) type lexp_context = senv_type * env_type * property_env +type elab_context = lexp_context + +(* Extract the lexp context from the context used during elaboration. *) +let ectx_to_lctx (ectx : elab_context) : env_type = + let (_, lctx, _) = ectx in lctx
(* internal definitions * ---------------------------------- *) @@ -107,9 +115,20 @@ let env_extend (ctx: lexp_context) (def: vdef) (v: varbind) (t: lexp) = debruijn_warning loc ("Variable Shadowing " ^ name); with Not_found -> ()); let nmap = StringMap.add name n map in - (* FIXME: Why a db_offset of 1? *) - ((n + 1, nmap), cons (1, Some def, v, t) env, f) - + ((n + 1, nmap), cons (0, Some def, v, t) env, f) + +let ectx_extend_rec (ctx: elab_context) (defs: (vdef * lexp * ltype) list) = + List.fold_left + (fun (ctx, recursion_offset) (def, e, t) -> + let (loc, name) = def in + let ((n, map), env, f) = ctx in + (try let _ = senv_lookup name ctx in + debruijn_warning loc ("Variable Shadowing " ^ name); + with Not_found -> ()); + let nmap = StringMap.add name n map in + ((n + 1, nmap), cons (recursion_offset, Some def, LetDef e, t) env, f), + recursion_offset - 1) + (ctx, List.length defs) defs
let _name_error loc estr str = if estr = str then () else
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -67,7 +67,6 @@ let lexp_fatal = msg_fatal "LPARSE" let _global_lexp_ctx = ref make_lexp_context let _global_lexp_trace = ref [] let _parsing_internals = ref false -let _shift_glob = ref 0 let btl_folder = ref "./btl/"
(* merged declaration, allow us to process declaration in multiple pass *) @@ -84,6 +83,22 @@ let _type_shift tp i = | Var(v, idx) -> Var(v, idx) | expr -> expr
+let ctx_define (ctx: lexp_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 + else + (print_string "¡¡ctx_define error!!\n"; + lexp_print lxp; + print_string " !: "; + lexp_print ltype; + print_string "\nbecause\n"; + lexp_print (OL.check cctx lxp); + print_string " != "; + lexp_print ltype; + print_string "\n"; + lexp_fatal (let (l,_) = var in l) "TC error") + (* The main job of lexp (currently) is to determine variable name (index) * and to regroup type specification with their variable * @@ -124,10 +139,6 @@ let build_var name ctx = let type0_idx = senv_lookup name ctx in Var((dloc, name), type0_idx)
-(* shift all variables by an offset *) -let senv_lookup name ctx = - senv_lookup name ctx + !_shift_glob - let rec lexp_p_infer (p : pexp) (ctx : lexp_context): lexp * ltype = _lexp_p_infer p ctx 1
@@ -413,7 +424,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | [] -> largs, ltp | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs (* Explicit-implicit argument. *) - -> (match OL.lexp_whnf ltp ctx with + -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) with | Arrow (ak, Some (_, aname'), arg_type, _, ret_type) when aname = aname' -> let parg = pexp_parse sarg in @@ -424,7 +435,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = "Explicit arg to non-function") | sarg :: sargs (* Process Argument *) - -> (match OL.lexp_whnf ltp ctx with + -> (match OL.lexp_whnf ltp (ectx_to_lctx ctx) with | Arrow (Aexplicit, _, arg_type, _, ret_type) -> let parg = pexp_parse sarg in let larg = _lexp_p_check parg arg_type ctx i in @@ -442,7 +453,7 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let handle_funcall () = (* Here we use lexp_whnf on actual code, but it's OK * because we only use the result when it's a "predefined constant". *) - match OL.lexp_whnf body ctx with + match OL.lexp_whnf body (ectx_to_lctx ctx) with | Builtin((_, "Built-in"), _) -> ( (* ------ SPECIAL ------ *) @@ -555,13 +566,13 @@ and lexp_read_pattern pattern exp target ctx: (* name is defined but is not a constructor *) (* it technically could be ... (expr option) *) (* What about Var -> Cons ? *) - | _ -> let nctx = env_extend ctx var (LetDef target) dltype in + | _ -> let nctx = ctx_define ctx var target dltype in (name, loc, []), nctx)
(* would it not make a default match too? *) with Not_found -> (* Create a variable containing target *) - let nctx = env_extend ctx var (LetDef target) dltype in + let nctx = ctx_define ctx var target dltype in (name, loc, []), nctx)
| Ppatcons (ctor_name, args) -> @@ -821,7 +832,7 @@ and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * lexp_context) = (List.rev !all), ctx
and _lexp_rec_decl decls ctx i = - (* parse a groupe of mutually recursive definition + (* parse a group of mutually recursive definitions * i.e let decl parsing *)
(* to compute recursive offset *) @@ -829,8 +840,8 @@ and _lexp_rec_decl decls ctx i = let lst = ref [] in
(* add all elements to the environment *) - let tctx = List.fold_left (fun vctx expr -> - match expr with + let tctx = List.fold_left (fun vctx decl -> + match decl with | Ldecl((l, s), _, None) -> env_extend vctx (l, s) ForwardRef dltype
@@ -842,9 +853,9 @@ and _lexp_rec_decl decls ctx i = lexp_fatal dloc "use lexp_decl_macro to parse macro decls") ctx decls in
let i = ref 0 in - let ctx = List.fold_left (fun vctx expr -> + let ctx = List.fold_left (fun vctx decl -> i := !i + 1; - match expr with + match decl with (* lexp infer *) | Ldecl ((l, s), Some pxp, None) -> let lxp, ltp = lexp_p_infer pxp vctx in @@ -991,11 +1002,11 @@ let default_lctx, default_rctx =
(* Empty context *) let lctx = make_lexp_context in - let lctx = env_extend lctx (dloc, "Type1") (LetDef type1) type2 in - let lctx = env_extend lctx (dloc, "Type") (LetDef type0) type1 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. *) let lxp = Builtin((dloc, "Built-in"), type0) in - let lctx = env_extend lctx (dloc, "Built-in") (LetDef lxp) type0 in + let lctx = ctx_define lctx (dloc, "Built-in") lxp type0 in
(* Read BTL files *) let pres = prelex_file (!btl_folder ^ "types.typer") in
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -39,6 +39,21 @@ module DB = Debruijn
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 (_, i) = vref in + let (_, _, _, t) = Myers.nth i ctx in + mkSusp t (S.shift (i + 1)) + +let lookup_value (ctx : 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 + (********* Testing if two types are "convertible" aka "equivalent" *********)
let rec conv_arglist_p s1 s2 args1 args2 : bool = @@ -56,7 +71,7 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 | (SortLevel (sl1), SortLevel (sl2)) -> sl1 == sl2 - | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 + | (Sort (_, s1), Sort (_, s2)) -> s1 = s2 | (Builtin ((_, s1), _), Builtin ((_, s2), _)) -> s1 == s2 (* BEWARE: When we'll make expand let-defined vars here, we'll have to * be careful not to introduce infinite-recursion. *) @@ -118,9 +133,9 @@ 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 = match e with +let rec lexp_whnf e (ctx : lexp_context) = match e with (* | Let (_, defs, body) -> FIXME!! Need recursive substitutions! *) - | Var v -> (match DB.env_lookup_expr ctx v with + | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! * IOW the risk of inf-looping should only show up when doing @@ -168,17 +183,6 @@ let rec lexp_whnf e ctx = match e with (********* Testing if a lexp is properly typed *********)
-let lookup_type ctx vref = - let (_, i) = vref in - let (_, _, _, t) = Myers.nth i ctx in - mkSusp t (S.shift (i + 1)) - -let lookup_value ctx 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 assert_type e t t' = if conv_p t t' then () else U.msg_error "TC" (lexp_location e) "Type mismatch"; () @@ -202,7 +206,7 @@ let rec check ctx e = match e with | Imm (Float (_, _)) -> B.type_float | Imm (Integer (_, _)) -> B.type_int - | Imm (Epsilon|Block (_, _, _)|Symbol _|String (_, _)|Node (_, _)) + | Imm (Epsilon | Block (_, _, _) | Symbol _ | String (_, _) | Node (_, _)) -> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; B.type_int) | SortLevel (_) -> B.type_level
View it on GitLab: https://gitlab.com/monnier/typer/commit/ad3197914f08a88922451d90e90802687395...