Stefan pushed to branch main at Stefan / Typer

Commits: 10d4fafc by Maxim Bernard at 2024-10-29T18:10:32-04:00 Don't transform builtins' types into closed form.

* src/opslexp.ml: Add DB offset to `lmap`, and use it in `get_builtin` to shift all DB indices accordingly. Add context parameter to `get_builtin` (used to compute shift). Make necessary adaptations in `check` and `fv` now that builtin types aren't in closed form.

* src/lexp.ml: Make necessary adaptations in `mkSusp`, `push_susp` and `clean`.

* src/inverse_subst.ml: Make necessary adaptations in `apply_inv_subst`.

* src/builtin.ml: Remove `kind` parameter from `new_builtin_type` since it shouldn't be anything else than `type0` (especially with the hardcoded DB offset). Provide new argument to `add_builtin_cst`.

* src/elab.ml: Remove obsolete argument from `new_builtin_type` calls. Provide new argument to `add_builtin_cst`. Make necessary adaptations in `meta_to_var`, `sform_identifier`, `sform_built_in` and `default_ectx`. In `sform_built_in`, remove transformation to closed form.

- - - - -

5 changed files:

- src/builtin.ml - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml

Changes:

===================================== src/builtin.ml ===================================== @@ -131,21 +131,28 @@ let v2o_list v = in v2o_list [] v

-let new_builtin_type name kind = - let t = mkBuiltin ((dloc, name), kind) in - OL.add_builtin_cst name t; +let new_builtin_type name = + let t = mkBuiltin ((dloc, name), DB.type0) in + (* Although the current context may not be empty when adding this builtins, + * we still provide 0 as the type's DB offset, since `DB.type0` doesn't + * reference any var/metavar, so the offset doesn't matter. *) + OL.add_builtin_cst name 0 t; t

let register_builtin_csts () = - OL.add_builtin_cst "TypeLevel" DB.type_level; - OL.add_builtin_cst "TypeLevel_z" DB.level0; - OL.add_builtin_cst "Type" DB.type0; - OL.add_builtin_cst "Type0" DB.type0; - OL.add_builtin_cst "Type1" DB.type1; - OL.add_builtin_cst "Integer" DB.type_integer; - OL.add_builtin_cst "Float" DB.type_float; - OL.add_builtin_cst "String" DB.type_string; - OL.add_builtin_cst "Eq" DB.type_eq; - OL.add_builtin_cst "I" DB.type_interval + (* Although the current context may not be empty when adding these builtins, + * we still provide 0 as the types' DB offset, since none of these types + * reference any var/metavar, so the offset doesn't matter in these cases. *) + OL.add_builtin_cst "TypeLevel" 0 DB.type_level; + OL.add_builtin_cst "TypeLevel_z" 0 DB.level0; + OL.add_builtin_cst "Type" 0 DB.type0; + OL.add_builtin_cst "Type0" 0 DB.type0; + OL.add_builtin_cst "Type1" 0 DB.type1; + OL.add_builtin_cst "Integer" 0 DB.type_integer; + OL.add_builtin_cst "Int" 0 DB.type_int; + OL.add_builtin_cst "Float" 0 DB.type_float; + OL.add_builtin_cst "String" 0 DB.type_string; + OL.add_builtin_cst "Eq" 0 DB.type_eq; + OL.add_builtin_cst "I" 0 DB.type_interval

let _ = register_builtin_csts ()

===================================== src/elab.ml ===================================== @@ -118,15 +118,21 @@ type special_decl_forms_map =

let special_forms : special_forms_map ref = ref SMap.empty let special_decl_forms : special_decl_forms_map ref = ref SMap.empty -let type_special_form = BI.new_builtin_type "Special-Form" type0 -let type_special_decl_form = BI.new_builtin_type "Special-Decl-Form" type0 +let type_special_form = BI.new_builtin_type "Special-Form" +let type_special_decl_form = BI.new_builtin_type "Special-Decl-Form"

let add_special_form (name, func) = - OL.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); + (* Although the current context may not be empty when adding this builtins, + * we still provide 0 as the type's DB offset, since `type_special_form` + * doesn'treference any var/metavar, so the offset doesn't matter. *) + OL.add_builtin_cst name 0 (mkBuiltin ((dloc, name), type_special_form)); special_forms := SMap.add name func (!special_forms)

let add_special_decl_form (name, func) = - OL.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_decl_form)); + (* Although the current context may not be empty when adding this builtins, + * we still provide 0 as the type's DB offset, since `type_special_decl_form` + * doesn'treference any var/metavar, so the offset doesn't matter. *) + OL.add_builtin_cst name 0 (mkBuiltin ((dloc, name), type_special_decl_form)); special_decl_forms := SMap.add name func (!special_decl_forms)

let get_special_form name = @@ -494,7 +500,7 @@ let meta_to_var ids (e : lexp) = | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) | Sort (_, (StypeOmega | StypeLevel)) -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, loop o t) | Var (n,i) -> if i < o then e else mkVar (n, i + count) | Proj (l, lxp, lbl) -> mkProj (l, loop o lxp, lbl) | Susp (e, s) -> loop o (push_susp e s) @@ -642,7 +648,7 @@ and sform_identifier ctx loc sargs ot = when String.length name >= 1 && String.get name 0 == '#' -> if String.length name > 2 && String.get name 1 == '#' then let name = string_sub name 2 (String.length name) in - try let e = OL.get_builtin name in + try let e = OL.get_builtin (ectx_to_lctx ctx) name in (e, Inferred (OL.get_type (ectx_to_lctx ctx) e)) with | Not_found @@ -1639,16 +1645,16 @@ let sform_built_in ctx loc sargs ot = | true, [String (_, name)] -> (match ot with | Some ltp - (* FIXME: This `L.clean` is basically the last remaining use of the - * function. It's not indispensible, tho it might still be useful for + (* FIXME: This `L.clean` is one of the last remaining uses of the + * function. It's not indispensible, tho it might still be useful for * performance of type-inference (at least until we have proper - * memoization of push_susp and/or whnf). *) - -> let ltp' = Lexp.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in + * memoization of push_susp and/or whnf). *) + -> let ltp' = Lexp.clean ltp in let bi = mkBuiltin ((Sexp.location loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions) || List.mem name DB.builtin_axioms) then sexp_error (Sexp.location loc) {|Unknown built-in "%s"|} name; - OL.add_builtin_cst name bi; + OL.add_builtin_cst name (DB.get_size ctx) bi; (bi, Checked) | None -> error ~loc:(Sexp.location loc) "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) @@ -2065,7 +2071,7 @@ let default_ectx

(* Empty context *) let ectx = empty_elab_context in - let ectx = SMap.fold (fun key e ctx + let ectx = SMap.fold (fun key (_o, e) ctx -> if String.get key 0 = '-' then ctx else ctx_define ctx (dsinfo, Some key) e (OL.get_type (ectx_to_lctx ectx) e))

===================================== src/inverse_subst.ml ===================================== @@ -271,7 +271,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) | Sort (_l, (StypeOmega | StypeLevel)) -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, apply_inv_subst t s) | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) | Proj (l,lxp,lbl) -> mkProj (l, apply_inv_subst lxp s, lbl) | Susp (e, s') -> apply_inv_subst (push_susp e s') s

===================================== src/lexp.ml ===================================== @@ -345,7 +345,7 @@ let rec mkSusp e s = * it just seemed like a good idea to do it eagerly when it's easy. *) match lexp_lexp' e with | Imm _ -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, mkSusp t s) | Susp (e, s') -> mkSusp_memo e (scompose s' s) | Var (l,v) -> slookup s l v | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s, vd) @@ -443,8 +443,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> mkSortLevel (mkSLlub' (push_susp e1 s, push_susp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (_, _) -> e - | Builtin _ -> e - + | Builtin (sym, t) -> mkBuiltin (sym, mkSusp t s) | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let rec loop s defs = match defs with @@ -512,7 +511,7 @@ let clean e = -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) | Sort (_, _) -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, clean s t) | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty)

===================================== src/opslexp.ml ===================================== @@ -131,28 +131,21 @@ let rec lctx_to_subst lctx = (List.rev defs) in L.scompose s2 s1

-(* Map of lexp builtin elements accessible via (## <name>). *) -let lmap = ref (SMap.empty : lexp SMap.t) - -let add_builtin_cst (name : string) (e : lexp) +(* Map of lexp builtin elements accessible via (## <name>). + * Values are pairs consisting of : + * - the type's De Bruijn offset (i.e. the context's size when the builtin + * was added) + * - the builtin's type *) +let lmap = ref (SMap.empty : (S.db_offset * lexp) SMap.t) + +let add_builtin_cst (name : string) (offset : S.db_offset) (e : lexp) = let map = !lmap in assert (not (SMap.mem name map)); - lmap := SMap.add name e map - -let get_builtin (name) = SMap.find name !lmap - -(* Take an expression `e` that is "closed" relatively to context lctx - * and return an equivalent expression valid in the empty context. - * By "closed" I mean that it only refers to elements of the context which - * are LetDef. *) -let lexp_close lctx e = - (* There are many different ways to skin this cat. - * This is definitely not the best one: - * - it inlines all the definitions everywhere they're used - * - It turns the lctx (of O(log N) access time) into a subst - * (of O(N) access time) - * Oh well! *) - mkSusp e (lctx_to_subst lctx) + lmap := SMap.add name (offset, e) map + +let get_builtin (ctx : lexp_context) (name) = + let (offset, btl) = SMap.find name !lmap in + mkSusp btl (S.shift ((M.length ctx) - offset))

let type_dummy = DB.type_integer

@@ -568,7 +561,7 @@ and mk_eq_witness sinfo e ctx = | _ -> Log.internal_error "" in (* FIXME: Doesn't `e` need a "shift" here? *) let fn = mkLambda (Aerasable, (sinfo, None), etype, e) in - mkCall (sinfo, get_builtin "Eq.eq", + mkCall (sinfo, get_builtin ctx "Eq.eq", [Aerasable, elevel; Aerasable, etype; Anormal, fn]) @@ -711,7 +704,7 @@ and check'' erased ctx e = * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t) - -> let _ = check_type DB.set_empty Myers.nil t in + -> let _ = check_type erased ctx t in t (* FIXME: Check recursive references. *) | Var (((loc, name), idx) as v) @@ -1065,7 +1058,7 @@ and fv (e : lexp) : (db_set * mv_set) = | SortLevel (SLlub (e1, e2)) -> fv_union (fv e1) (fv e2) | Sort (_, Stype e) -> fv e | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty - | Builtin _ -> fv_empty + | Builtin (_, t) -> fv t | Var (_, i) -> (DB.set_singleton i, mv_set_empty) | Proj (_, lxp, _) -> fv lxp | Susp (e, s) -> fv (push_susp e s)

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/10d4fafcb572a8cbe9ec22ecad2436dee0...