Stefan pushed to branch main at Stefan / Typer

Commits: 5d8e2879 by Stefan Monnier at 2023-07-17T22:03:39-04:00 Move Eq.eqs definition to builtins.typer

Defining `eq_eq` in `debruijn.ml` was cumbersome. Replace both uses of it (one in `mk_eq_witness` and one in `eq_cast_whnf`) to use a different way to refer to `Eq.eq`. This makes use of `lmap` which is like `predef` except it's filled "on the go" so it's available already during `builtin.typer`.

* btl/builtins.typer (Eq_eq): Define it like other built-ins!

* src/builtin.ml (lmap, add_builtin_cst): Move to Opslexp.

* src/debruijn.ml (eq_eq): Delete.

* src/elab.ml (sform_identifier, default_ectx): Adjust to new `lmap`.

* src/opslexp.ml (lmap, add_builtin_cst): Move from Builtin. Simplify the map to only hold the lexps and not their type (the type is trivial to extract from the builtin anyway). (conv_builtin_p): New function. (eq_cast_whnf): Use it. (get_builtin): New function. (mk_eq_witness): Use it.

- - - - -

6 changed files:

- btl/builtins.typer - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/heap.ml - src/opslexp.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -1,6 +1,6 @@ %%% builtins.typer --- Initialize the builtin functions

-%% Copyright (C) 2011-2020 Free Software Foundation, Inc. +%% Copyright (C) 2011-2023 Free Software Foundation, Inc. %% %% Author: Pierre Delaunay pierre.delaunay@hec.ca %% Keywords: languages, lisp, dependent types. @@ -60,7 +60,7 @@ I_not i = case i Eq_eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> (f : I ≡> t) ≡> Eq (f (_ := i0)) (f (_ := i1)); -Eq_eq = ##Eq.eq; +Eq_eq = Built-in "Eq.eq";

Eq_uneq : (l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) => (y : t)

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

-(* Map of lexp builtin elements accessible via (## <name>). *) -let lmap = ref (SMap.empty : (lexp * ltype) SMap.t) - -let add_builtin_cst (name : string) (e : lexp) - = let map = !lmap in - assert (not (SMap.mem name map)); - let t = OL.check Myers.nil e in - lmap := SMap.add name (e, t) map - let new_builtin_type name kind = let t = mkBuiltin ((dloc, name), kind) in - add_builtin_cst name t; + OL.add_builtin_cst name t; t

let register_builtin_csts () = - add_builtin_cst "TypeLevel" DB.type_level; - add_builtin_cst "TypeLevel_z" DB.level0; - add_builtin_cst "Type" DB.type0; - add_builtin_cst "Type0" DB.type0; - add_builtin_cst "Type1" DB.type1; - add_builtin_cst "Int" DB.type_int; - add_builtin_cst "Integer" DB.type_integer; - add_builtin_cst "Float" DB.type_float; - add_builtin_cst "String" DB.type_string; - add_builtin_cst "Elab_Context" DB.type_elabctx; - add_builtin_cst "Eq" DB.type_eq; - add_builtin_cst "Eq.eq" DB.eq_eq; - add_builtin_cst "I" DB.type_interval + 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 "Int" DB.type_int; + 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 "Elab_Context" DB.type_elabctx; + OL.add_builtin_cst "Eq" DB.type_eq; + OL.add_builtin_cst "I" DB.type_interval

let type_arrow_0 = mkArrow (dsinfo, Anormal, (dsinfo, None), DB.type0, DB.type0)

===================================== src/debruijn.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2022 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -161,28 +161,6 @@ let type_interval let interval_i0 = mkCons (type_interval, (dloc, "i0")) let interval_i1 = mkCons (type_interval, (dloc, "i1"))

-let eq_eq = - (* Variables for the type level, type and the function (I -> ?A) *) - let lv = (dsinfo, Some "l") in - let tv = (dsinfo, Some "t") in - let fv = (dsinfo, Some "f") in - mkBuiltin ((dloc, "Eq.eq"), - mkArrow (dsinfo, Aerasable, lv, - type_level, - mkArrow (dsinfo, Aerasable, tv, - mkSort (dsinfo, Stype (mkVar (lv, 0))), - mkArrow (dsinfo, Aerasable, fv, - mkArrow (dsinfo, Aerasable, (dsinfo, None), - type_interval, - mkVar (tv, 1)), - mkCall (dsinfo, type_eq, - [Aerasable, mkVar (lv, 2); - Aerasable, mkVar (tv, 1); - Anormal, mkCall (dsinfo, mkVar (fv, 0), - [Aerasable, interval_i0]); - Anormal, mkCall (dsinfo, mkVar (fv, 0), - [Aerasable, interval_i1])]))))) - (* easier to debug with type annotations *) type env_elem = (vname * varbind * ltype) type lexp_context = env_elem M.myers

===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2022 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -121,11 +121,11 @@ 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 add_special_form (name, func) = - BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); + OL.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); special_forms := SMap.add name func (!special_forms)

let add_special_decl_form (name, func) = - BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_decl_form)); + OL.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_decl_form)); special_decl_forms := SMap.add name func (!special_decl_forms)

let get_special_form name = @@ -626,8 +626,8 @@ 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, t) = SMap.find name (! BI.lmap) in - (e, Inferred t) + try let e = OL.get_builtin name in + (e, Inferred (OL.get_type (ectx_to_lctx ctx) e)) with | Not_found -> sexp_error l {|Unknown builtin "%s"|} name; @@ -1604,7 +1604,7 @@ let sform_built_in ctx loc sargs ot = let bi = mkBuiltin ((Sexp.location loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error (Sexp.location loc) {|Unknown built-in "%s"|} name; - BI.add_builtin_cst name bi; + OL.add_builtin_cst name bi; (bi, Checked) | None -> error ~loc:(Sexp.location loc) "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) @@ -2020,29 +2020,30 @@ let default_ectx warning "Predef not found"; in

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

Heap.register_builtins (); (* read base file *) - let lctx = dynamic_bind parsing_internals true + let ectx = dynamic_bind parsing_internals true (fun () -> read_file (btl_folder ^ "/builtins.typer") - lctx) in - let _ = register_predefs lctx in + ectx) in + let _ = register_predefs ectx in

(* Does not work, not sure why let files = ["list.typer"; "quote.typer"; "type.typer"] in - let lctx = List.fold_left (fun lctx file_name -> - read_file (btl_folder ^ "/" ^ file_name) lctx) lctx files in *) + let ectx = List.fold_left (fun ectx file_name -> + read_file (btl_folder ^ "/" ^ file_name) ectx) ectx files in *)

- builtin_size := get_size lctx; + builtin_size := get_size ectx; let ectx = dynamic_bind in_pervasive true - (fun () -> read_file (btl_folder ^ "/pervasive.typer") lctx) in + (fun () -> read_file (btl_folder ^ "/pervasive.typer") ectx) in let ectx = DB.ectx_set_inst_def ectx true in let _ = sform_default_ectx := ectx in ectx

===================================== src/heap.ml ===================================== @@ -1,4 +1,4 @@ -(* Copyright (C) 2020, 2021 Free Software Foundation, Inc. +(* Copyright (C) 2020-2023 Free Software Foundation, Inc. * * Author: Simon Génier simon.genier@umontreal.ca * Keywords: languages, lisp, dependent types. @@ -26,6 +26,7 @@ open Eval open Lexp

module IMap = Util.IMap +module OL = Opslexp

type location = Source.Location.t type symbol = Sexp.symbol @@ -141,8 +142,8 @@ let heap_load_cell : builtin_function = | _ -> error ~loc "`Heap.store-cell` expects [Int; Int]"

let register_builtins () = - add_builtin_cst "DataconsLabel" type_datacons_label; - add_builtin_cst "Heap" type_heap; + OL.add_builtin_cst "DataconsLabel" type_datacons_label; + OL.add_builtin_cst "Heap" type_heap; add_builtin_function "datacons-label<-string" datacons_label_of_string 1; add_builtin_function "Heap.alloc" heap_alloc 1; add_builtin_function "Heap.free" heap_alloc 1;

===================================== src/opslexp.ml ===================================== @@ -135,6 +135,16 @@ 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) + = 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 @@ -283,11 +293,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = and lexp'_whnf e (ctx : DB.lexp_context) : lexp' = lexp_lexp' (lexp_whnf e ctx)

+and conv_builtin_p ctx e name = + (* FIXME: Maybe we could use `conv_p (get_builin name)` instead? *) + match lexp'_whnf e ctx with + | Builtin ((_, name'), _) -> name = name' + | _ -> false + and eq_cast_whnf ctx args = match args with | _l1 :: _l2 :: _t :: _x :: _y :: (_, p) :: _f :: (_, fx) :: rest -> (match lexp'_whnf p ctx with - | Call (_, eq, _) when conv_p ctx eq DB.eq_eq + | Call (_, eq, _) when conv_builtin_p ctx eq "Eq.eq" -> Some (fx, rest) | _ -> None) | _ -> None @@ -538,12 +554,13 @@ and conv_p (ctx : DB.lexp_context) e1 e2 else conv_p' ctx set_empty e1 e2

and mk_eq_witness sinfo e ctx = - let etype = get_type ctx e in (* FIXME we should not need get_type here *) + let etype = get_type ctx e in (* FIXME: we should not need get_type here. *) let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in + (* FIXME: Doesn't `e` need a "shift" here? *) let fn = mkLambda (Pexp.Aerasable, (sinfo, None), etype, e) in - mkCall (sinfo, DB.eq_eq, + mkCall (sinfo, get_builtin "Eq.eq", [Pexp.Aerasable, elevel; Pexp.Aerasable, etype; Pexp.Anormal, fn])

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/5d8e2879f991e5ed879e4c47f0e6ba724a...