James Tan Juan Whei pushed to branch quotient-types 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.

- - - - - 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.

- - - - - 6ea6caae by Stefan Monnier at 2023-07-18T20:03:41-04:00 test/env_tests.ml: Adjust to last change

- - - - - 28335684 by James Tan at 2023-07-19T02:01:32-04:00 Implement `Quotient` formation

- - - - - 4c832100 by James Tan at 2023-07-19T02:07:14-04:00 Implement `Quotient` introduction

- - - - - 946ac2f1 by James Tan at 2023-07-19T02:07:16-04:00 Implement `Quotient` elimination

- - - - - 5894ed22 by James Tan at 2023-07-19T02:07:16-04:00 Implement `Eq` constructor for `Quotient`

- - - - - bfbff550 by James Tan at 2023-07-19T02:07:16-04:00 Improve unification scheme for SLlub (l1, l2) when l1 ≃ l2

- - - - -

11 changed files:

- btl/builtins.typer - + samples/quotient.typer - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/env.ml - src/eval.ml - src/heap.ml - src/opslexp.ml - src/unification.ml - tests/env_test.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) @@ -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,67 @@ 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";

+ +%% +%% Quotient types +%% +%% Quotient : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> +%% (R : A -> A -> Type_ l2) -> Type_ (TypeLevel_⊔ l1 l2) +%% +Quotient_in : ?A -> Quotient ?A ?R; +Quotient_in = Built-in "Quotient.in"; + +%% FIXME: We want to be able to say the following +%% Quotient_eq : (a : ?) ≡> (a' : ?) ≡> (p : ?R a a') ≡> +%% Eq (Quotient_in (R := R?) a) +%% (Quotient_in (R := R?) a'); +%% But we running into the following issue for now: +%% "Bug in the elaboration of a repeated metavar!" +Quotient_eq : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> + (R : A -> A -> Type_ l2) ≡> + (a : A) ≡> (a' : A) ≡> (p : R a a') -> + Eq (Quotient_in (R := R) a) + (Quotient_in (R := R) a'); +Quotient_eq = Built-in "Quotient.eq"; + +%% FIXME: We want to be able to say the following +%% Quotient_elim : (f : ?A -> ?B) -> +%% (p : (a : ?) -> (a' : ?) -> ?R a a' -> Eq (f a) (f a')) ≡> +%% (q : Quotient ?A ?R) -> +%% ?B; +%% Same issue as above +Quotient_elim : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (l3 : TypeLevel) ≡> + (A : Type_ l1) ≡> (B : Type_ l2) ≡> + (R : A -> A -> Type_ l3) ≡> + (f : A -> B) -> + (p : (a : A) -> (a' : A) -> R a a' -> Eq (f a) (f a')) ≡> + (q : Quotient A R) -> + B; +Quotient_elim = Built-in "Quotient.elim"; + %%% builtins.typer ends here.

===================================== samples/quotient.typer ===================================== @@ -0,0 +1,99 @@ +Nat : Type; + +type Nat + | zero + | succ Nat; + +_-_ : Nat -> Nat -> Nat; +_-_ x y = case x + | zero => zero + | succ m => case y + | zero => x + | succ n => m - n; + +NatPair = Pair Nat Nat; + +fst p = case p + | pair m _ => m; + +snd p = case p + | pair _ n => n; + +normaliseZ : NatPair -> NatPair; +normaliseZ np = case np + | pair m n => pair (m - n) (n - m); + +equalZ : NatPair -> NatPair -> Type; +equalZ x1 x2 = Eq (normaliseZ x1) (normaliseZ x2); + +%% +%% See definitions of `Quotient` in `builtins.typer` +%% + +%% FIXME: We shouldn't get this error +%% "Requested Built-in "Quotient" does not exist" +%% Z = Quotient NatPair equalZ; + +%% +%% Quotient.eq +%% +%% Proof that quotiented elements are equal when +%% the base elements themselves are related in +%% the underlying type. +𝟙-𝟘 : Quotient NatPair equalZ; +𝟙-𝟘 = Quotient_in (pair (succ zero) zero); + +𝟚-𝟙 : Quotient NatPair equalZ; +𝟚-𝟙 = Quotient_in (pair (succ (succ zero)) (succ zero)); + +𝟙=𝟙 : Eq (t := Quotient NatPair equalZ) 𝟙-𝟘 𝟚-𝟙; +𝟙=𝟙 = Quotient_eq + (R := equalZ) + (a := pair (succ zero) zero) + (a' := pair (succ (succ zero)) (succ zero)) + Eq_refl; + +%% +%% Quotient.elim +%% +%% Elimination of quotients requires a proof that +%% the equality between quotients is respected +NatToInt : Nat -> Int; +NatToInt n = case n + | zero => 0 + | succ n' => 1 + NatToInt n'; + +NatPairToInt' : NatPair -> Int; +NatPairToInt' np = case np + | pair x y => + (case x + | zero => (NatToInt y) * -1 + | succ _ => NatToInt x); + +NatPairToInt : NatPair -> Int; +NatPairToInt np = NatPairToInt' (normaliseZ np); + +%% Proof that NatPairToInt respects the quotient Z +NatPairToIntCompat : (a : NatPair) -> (a' : NatPair) -> + (p : equalZ a a') -> + Eq (NatPairToInt a) (NatPairToInt a'); +NatPairToIntCompat _ _ p = Eq_eq (f := lambda i ≡> + NatPairToInt' (Eq_uneq (p := p) (i := i))); + +%% FIXME: Explicitly providing a value for R should unnecessary, +%% this should be inferred based on the type of `q`. This is +%% because we do not handle residuals during unification for now. +Z_To_Int : Quotient NatPair equalZ -> Int; +Z_To_Int q = Quotient_elim (R := equalZ) NatPairToInt (p := NatPairToIntCompat) q; + +neg2_Z : Quotient NatPair equalZ; +neg2_Z = Quotient_in (pair (succ zero) (succ (succ (succ zero)))); + +neg2_Int : Int; +neg2_Int = Z_To_Int neg2_Z; + +%% FIXME: This could work if we add a reduction rule +%% neg2_refl : Eq neg2_Int (-2 : Int); +%% neg2_refl = Eq_refl; + +%% TODO: Define Quotient NatPair equalZ ≃ Int

===================================== src/builtin.ml ===================================== @@ -131,45 +131,22 @@ 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 - -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 () + 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; + OL.add_builtin_cst "Quotient" DB.type_quotient + +let _ = register_builtin_csts ()

===================================== 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. @@ -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. *) @@ -161,27 +168,30 @@ 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])]))))) +let type_quotient_type = + let lv1 = (dsinfo, Some "l1") in + let lv2 = (dsinfo, Some "l2") in + let tv = (dsinfo, Some "A") in + let rv = (dsinfo, Some "R") in + let rtype = mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 0), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 1), + mkSort (dsinfo, Stype (mkVar (lv2, 3))))) in + mkArrow (dsinfo, Aerasable, lv1, + type_level, + mkArrow (dsinfo, Aerasable, lv2, + type_level, + mkArrow (dsinfo, Anormal, tv, + mkSort (dsinfo, Stype (mkVar (lv1, 1))), + mkArrow (dsinfo, Anormal, rv, + rtype, + mkSort (dsinfo, Stype + (mkSortLevel + (mkSLlub' (mkVar (lv1, 3), + mkVar (lv2, 2))))))))) + +let type_quotient = mkBuiltin ((dloc, "Quotient"), type_quotient_type)

(* easier to debug with type annotations *) type env_elem = (vname * varbind * ltype)

===================================== 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; @@ -1602,9 +1602,10 @@ 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; - 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 +2021,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/env.ml ===================================== @@ -177,12 +177,15 @@ 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) + (* 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) + | [_; _; (_, t); (_, r)] when OL.conv_p ctx e' DB.type_quotient + -> sprintf "(Quotient.in %s %s)" (Lexp.to_string t) (Lexp.to_string r) | _ -> value_string v) | _ -> value_string v in get_string ltype ctx

===================================== src/eval.ml ===================================== @@ -1027,6 +1027,18 @@ let typelevel_lub loc (_depth : eval_debug_info) (args_val: value_type list) = | [Vint v1; Vint v2] -> Vint(max v1 v2) | _ -> error loc ("`Typlevel.⊔` expects 2 TypeLevel argument2")

+let quotient_elim loc depth args = + let trace_dum = (Var ((epsilon (loc), None), -1)) in + match args with + | [(Closure _) as f; q] -> + eval_call loc trace_dum depth f [q] + | _ -> error loc "Quotient.elim expects 2 arguments" + +let quotient_eq loc _ args = + match args with + | [_] -> Vundefined + | _ -> error loc "Quotient.eq expects 1 argument" + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -1084,6 +1096,9 @@ let register_builtin_functions () = ("Test.false" , test_false,2); ("Test.eq" , test_eq,3); ("Test.neq" , test_neq,3); + ("Quotient.in" , nop_fun, 1); + ("Quotient.eq" , quotient_eq, 1); + ("Quotient.elim" , quotient_elim, 2); ] let _ = register_builtin_functions ()

===================================== 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. @@ -20,12 +20,11 @@

(** 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

type location = Source.Location.t type symbol = Sexp.symbol @@ -39,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

@@ -141,8 +138,6 @@ 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; 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 @@ -148,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: @@ -283,11 +294,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 +555,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]) @@ -659,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 @@ -974,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 @@ -1118,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))) @@ -1262,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)

===================================== src/unification.ml ===================================== @@ -561,6 +561,10 @@ and unify_sortlvl (matching : scope_level option) -> (* FIXME: This SLlub representation needs to be * more "canonicalized" otherwise it's too restrictive! *) (unify' l11 l21 ctx vs matching)@(unify' l12 l22 ctx vs matching) + | SLlub (l1, l2), other | other, SLlub (l1, l2) + when OL.conv_p ctx l1 l2 + (* Arbitrarily selected `l1` over `l2` *) + -> unify' l1 (mkSortLevel other) ctx vs matching | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]

===================================== tests/env_test.ml ===================================== @@ -42,11 +42,11 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> if 10 <= (!global_verbose_lvl) then (

let var = [ - ((dsinfo, Some "a"), DB.type_int, (make_val "a")); - ((dsinfo, Some "b"), DB.type_int, (make_val "b")); - ((dsinfo, Some "c"), DB.type_int, (make_val "c")); - ((dsinfo, Some "d"), DB.type_int, (make_val "d")); - ((dsinfo, Some "e"), DB.type_int, (make_val "e")); + ((dsinfo, Some "a"), DB.type_integer, (make_val "a")); + ((dsinfo, Some "b"), DB.type_integer, (make_val "b")); + ((dsinfo, Some "c"), DB.type_integer, (make_val "c")); + ((dsinfo, Some "d"), DB.type_integer, (make_val "d")); + ((dsinfo, Some "e"), DB.type_integer, (make_val "e")); ] in

let n = (List.length var) - 1 in @@ -71,15 +71,15 @@ let _ = (add_test "ENV" "Value Printer" (fun () -> let open Lexp in let exps = [((Vint 42), (mkArrow (dsinfo, Aerasable, (dsinfo, Some "l"), - DB.type_interval, DB.type_int)), + DB.type_interval, DB.type_integer)), "(lambda _ ≡> 42)"); ((Vbuiltin "Eq.eq"), (mkCall (dsinfo, DB.type_eq, [Aerasable, mkVar ((dsinfo, None), 2); - Aerasable, DB.type_int; + Aerasable, DB.type_integer; Anormal, mkVar ((dsinfo, Some "x"), 0); Anormal, mkVar ((dsinfo, Some "y"), 0)])), - "x = y [ ##Int ]")] in + "x = y [ ##Integer ]")] in (* This test assumes that success = 0 and failure = -1 *) List.fold_left (fun res (v, ltype, expected)

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a68c3a6aa15a0575f08ca0d3862087202...