Stefan pushed to branch main at Stefan / Typer
Commits: f72f5e81 by Stefan Monnier at 2023-07-18T20:00:45-04:00 Move definition of some types to `builtins.typer`
Allow the use of `Built-in` to define types. Doesn't work for types like `Eq` or `Float` which are used internally in the typing rules, but works for most other types introduced for built-in functions.
* btl/builtins.typer (Int, Sexp, IO, Elab_Context, Array, FileHandle, Ref) (DataconsLabel, Heap): Define here.
* src/builtin.ml (register_builtin_types): Delete function. (type_arrow_0): Delete var. (register_builtin_csts): Don't register `Elab_Context`.
* src/debruijn.ml (type_elabctx, type_int): Delete vars. (builtin_axioms): New var.
* src/elab.ml (sform_built_in): Accept built-ins without a function if they're listed in `DB.builtin_axioms`.
* src/env.ml (value_string_with_type): Use `OL.conv_builtin_p` instead to avoid referring to `DB.type_eq`.
* src/heap.ml (type_datacons_label, type_heap): Delete vars. (register_builtins): Don't register them.
* src/opslexp (type_dummy): New var. Use it instead of `DB.type_int` when returning a dummy type after a type error.
- - - - -
7 changed files:
- btl/builtins.typer - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/env.ml - src/heap.ml - src/opslexp.ml
Changes:
===================================== btl/builtins.typer ===================================== @@ -124,6 +124,8 @@ Bool = typecons (Bool) (true) (false); true = datacons Bool true; false = datacons Bool false;
+Int = Built-in "Int" : Type; + %% Basic operators Int_+ = Built-in "Int.+" : Int -> Int -> Int; Int_- = Built-in "Int.-" : Int -> Int -> Int; @@ -199,6 +201,7 @@ String_eq = Built-in "String.=" : String -> String -> Bool; String_concat = Built-in "String.concat" : String -> String -> String; String_sub = Built-in "String.sub" : String -> Int -> Int -> String;
+Sexp = Built-in "Sexp" : Type; Sexp_eq = Built-in "Sexp.=" : Sexp -> Sexp -> Bool;
%% @@ -206,6 +209,9 @@ Sexp_eq = Built-in "Sexp.=" : Sexp -> Sexp -> Bool; %% Returns the same Sexp in the IO monad %% but also print the Sexp to standard output %% +IO : Type -> Type; +IO = Built-in "IO"; + Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp;
%% ----------------------------------------------------- @@ -251,10 +257,16 @@ Sexp_dispatch = Built-in "Sexp.dispatch"; %% %% Parse a block using the grammar in the passed context %% + +Elab_Context = Built-in "Elab_Context" : Type; + Reader_parse = Built-in "Reader.parse" : Elab_Context -> Sexp -> List Sexp;
%%%% Array (without IO, but they could be added easily)
+Array : Type_ ?l -> Type_ ?l; +Array = Built-in "Array"; + %% %% Takes an index, a new value and an array %% Returns a copy of the array with the element @@ -324,6 +336,8 @@ IO_run = Built-in "IO.run";
%% File monad
+FileHandle = Built-in "FileHandle" : Type; + %% Define operations on file handle. File_open = Built-in "File.open" : String -> String -> IO FileHandle; File_stdout = Built-in "File.stdout" : Unit -> FileHandle; @@ -341,6 +355,9 @@ Sys_exit = Built-in "Sys.exit" : Int -> IO Unit; %% Ref = typecons (Ref (a : Type)) (Ref a); %%
+Ref : Type_ ?l -> Type_ ?l; +Ref = Built-in "Ref"; + %% %% Takes a value %% Returns a value modifiable in the IO monad @@ -489,25 +506,29 @@ Test_neq = Built-in "Test.neq"; %% Given a string, return an opaque DataconsLabel that identifies a data %% constructor. %% -datacons-label<-string : String -> ##DataconsLabel; + +DataconsLabel = Built-in "DataconsLabel" : Type; +Heap = Built-in "Heap" : Type -> Type; + +datacons-label<-string : String -> DataconsLabel; datacons-label<-string = Built-in "datacons-label<-string";
-Heap_unsafe-alloc : Int -> ##Heap Int; +Heap_unsafe-alloc : Int -> Heap Int; Heap_unsafe-alloc = Built-in "Heap.alloc";
-Heap_unsafe-free : Int -> ##Heap Unit; +Heap_unsafe-free : Int -> Heap Unit; Heap_unsafe-free = Built-in "Heap.free";
-Heap_unsafe-export : Int -> ##Heap ?t; +Heap_unsafe-export : Int -> Heap ?t; Heap_unsafe-export = Built-in "Heap.export";
-Heap_unsafe_store_header : Int -> ##DataconsLabel -> ##Heap Unit; +Heap_unsafe_store_header : Int -> DataconsLabel -> Heap Unit; Heap_unsafe_store_header = Built-in "Heap.store-header";
-Heap_unsafe-store-cell : Int -> Int -> ?t -> ##Heap Unit; +Heap_unsafe-store-cell : Int -> Int -> ?t -> Heap Unit; Heap_unsafe-store-cell = Built-in "Heap.store-cell";
-Heap_unsafe-load-cell : Int -> Int -> ##Heap ?t; +Heap_unsafe-load-cell : Int -> Int -> Heap ?t; Heap_unsafe-load-cell = Built-in "Heap.load-cell";
%%% builtins.typer ends here.
===================================== src/builtin.ml ===================================== @@ -142,24 +142,10 @@ let register_builtin_csts () = 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) - -let register_builtin_types () = - let _ = new_builtin_type "Sexp" DB.type0 in - let _ = new_builtin_type "IO" type_arrow_0 in - let _ = new_builtin_type "Ref" type_arrow_0 in - let _ = new_builtin_type "Array" type_arrow_0 in - let _ = new_builtin_type "FileHandle" DB.type0 in - () - -let _ = register_builtin_csts (); - register_builtin_types () +let _ = register_builtin_csts ()
===================================== src/debruijn.ml ===================================== @@ -123,11 +123,13 @@ let level2 = mkSortLevel (mkSLsucc level1) let type0 = mkSort (dsinfo, Stype level0) let type1 = mkSort (dsinfo, Stype level1) let type2 = mkSort (dsinfo, Stype level2) -let type_int = mkBuiltin ((dloc, "Int"), type0) let type_integer = mkBuiltin ((dloc, "Integer"), type0) let type_float = mkBuiltin ((dloc, "Float"), type0) let type_string = mkBuiltin ((dloc, "String"), type0) -let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) + +(* FIXME: This definition of `Eq` should preferably be in `builtins.typer`, + * but we need `type_eq` when to hande `Case` expressions in + * elab/conv_p/check! :-( *) let type_eq_type = let lv = (dsinfo, Some "l") in let tv = (dsinfo, Some "t") in @@ -142,6 +144,11 @@ let type_eq_type = mkSort (dsinfo, Stype (mkVar (lv, 3))))))) let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type)
+let builtin_axioms = + ["Int"; "Elab_Context"; "IO"; "Ref"; "Sexp"; "Array"; "FileHandle"; + (* From `healp.ml`. *) + "Heap"; "DataconsLabel"] + (* FIXME: Is this the best way to do this? Originally, I wanted to * define this in Typer and then reference it from OCaml code. *)
===================================== src/elab.ml ===================================== @@ -1602,7 +1602,8 @@ let sform_built_in ctx loc sargs ot = * memoization of push_susp and/or whnf). *) -> let ltp' = Lexp.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in let bi = mkBuiltin ((Sexp.location loc, name), ltp') in - if not (SMap.mem name (!EV.builtin_functions)) then + 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; (bi, Checked)
===================================== src/env.ml ===================================== @@ -177,13 +177,14 @@ let value_string_with_type v ltype ctx = | Call (_, e, args) -> let e' = OL.lexp_whnf e ctx in (match args with - (* Pretty print identity types *) - | [_l; (_, t); (_, left); (_, right)] when OL.conv_p ctx e' DB.type_eq - -> sprintf "%s = %s [ %s ]" - (Lexp.to_string left) - (Lexp.to_string right) - (Lexp.to_string t) - | _ -> value_string v) + (* Pretty print identity types *) + | [_l; (_, t); (_, left); (_, right)] + when OL.conv_builtin_p ctx e' "Eq" + -> sprintf "%s = %s [ %s ]" + (Lexp.to_string left) + (Lexp.to_string right) + (Lexp.to_string t) + | _ -> value_string v) | _ -> value_string v in get_string ltype ctx
===================================== src/heap.ml ===================================== @@ -20,10 +20,8 @@
(** A heap of Typer objects that can be partially initialized. *)
-open Builtin open Env open Eval -open Lexp
module IMap = Util.IMap module OL = Opslexp @@ -40,8 +38,6 @@ let error ~(loc : location) ?print_action fmt =
let dloc = Util.dummy_location let type0 = Debruijn.type0 -let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) -let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0)
let next_free_address : addr ref = ref 1
@@ -142,8 +138,6 @@ let heap_load_cell : builtin_function = | _ -> error ~loc "`Heap.store-cell` expects [Int; Int]"
let register_builtins () = - 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 ===================================== @@ -158,6 +158,7 @@ let lexp_close lctx e = * Oh well! *) mkSusp e (lctx_to_subst lctx)
+let type_dummy = DB.type_integer
(** Reduce to weak head normal form. * WHNF implies: @@ -676,7 +677,7 @@ and check'' erased ctx e = | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _, _)) -> (log_tc_error ~loc:(Lexp.location e) "Unsupported immediate value!"; - DB.type_int) + type_dummy) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) -> let t = check erased ctx e in @@ -991,11 +992,11 @@ and check'' erased ctx e = with | Not_found -> log_tc_error ~loc:(Sexp.location l) {|Constructor "%s" does not exist|} name; - DB.type_int) + type_dummy) | _ -> log_tc_error ~loc:(Lexp.location e) "Cons of a non-inductive type: %s" (Lexp.to_string t); - DB.type_int) + type_dummy) | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> let e = push_susp e s in @@ -1135,7 +1136,7 @@ and get_type ctx e = | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_integer | Imm (String (_, _)) -> DB.type_string - | Imm (Block (_, _) | Symbol _ | Node (_, _, _)) -> DB.type_int + | Imm (Block (_, _) | Symbol _ | Node (_, _, _)) -> type_dummy | Builtin (_, t) -> t | SortLevel _ -> DB.type_level | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e))) @@ -1279,8 +1280,8 @@ and get_type ctx e = -> mkArrow (l, P.Aerasable, vd, atype, buildtype fargs) in buildtype fargs - with Not_found -> DB.type_int) - | _ -> DB.type_int) + with Not_found -> type_dummy) + | _ -> type_dummy) | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> get_type ctx (push_susp e s)
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f72f5e81a6773eb89c27efa7b5c71057cb...
Afficher les réponses par date