Stefan pushed to branch main at Stefan / Typer

Commits: c88a9143 by James Tan at 2023-08-21T16:40:32-04:00 Implement `Quotient` formation

- - - - - 98dd1f53 by James Tan at 2023-08-21T17:58:12-04:00 Implement `Quotient` introduction

- - - - - 85c39685 by James Tan at 2023-08-21T18:58:26-04:00 Implement `Quotient` elimination

- - - - - 89c93f93 by James Tan at 2023-08-21T18:58:29-04:00 Implement `Eq` constructor for `Quotient`

- - - - - 69fdb2dd by James Tan at 2023-08-21T18:58:29-04:00 Improve unification scheme for SLlub (l1, l2) when l1 ≃ l2

- - - - - 7d9c88fc by James Tan at 2023-08-21T18:58:29-04:00 Implement `qcase` macro - Facilitates `Quotient` elimination

- - - - - ee5361fa by James Tan at 2023-08-21T18:58:29-04:00 Write some proofs about quotient types

- - - - - f84010df by James Tan at 2023-08-21T19:29:55-04:00 Add a proof that `Quotient` implies `funExt`

- - - - - a445e1d0 by Stefan Monnier at 2023-08-24T19:33:22-04:00 Fix the annoying "Bug in the elaboration of a repeated metavar"

There are still cases where it can happen, but they should hopefully be more "real" (i.e. cases where the two occurrences of the metavar are in different scopes).

* src/debruijn.ml (builtin_axioms): Shorten accordingly. (meta_scope): Keep track of the scope level in the metavar map.

* src/elab.ml (sform_identifier): Adjust accordingly.

- - - - - 965b1d0d by Stefan Monnier at 2023-08-24T19:37:56-04:00 Make type constructors more like normal/executable Builtins

* src/eval.ml (eval_call): When building closures for Builtins, build them one arg at a time, so it works even with very large values of `arity`. (quotient_type): Delete function. (type_constructor): New function. (register_builtin_functions): Use it for `IO/Ref/Array/Quotient`.

* src/heap.ml (register_builtins): Use it for `Heap`.

* src/debruijn.ml (builtin_axioms): Shorten accordingly.

- - - - - 476b8241 by Stefan Monnier at 2023-08-24T19:38:30-04:00 Minor simplifications for Quotient code

* btl/builtins.typer (Quotient_elim, Quotient_eq): Simplify the type annotation. (NormToQuotient): Make the base type implicit.

* btl/qcase.typer (qcase_impl): Remove redundant `Integer->Int`. Remove leftover `TODO`.

* samples/quotient.typer (Z): Adjust to new type of `NormToQuotient`. (q1=1): Simplify the type annotation.

- - - - -

15 changed files:

- btl/builtins.typer - btl/pervasive.typer - + btl/qcase.typer - samples/nat.typer - + samples/qcase_test.typer - + samples/quotient.typer - + samples/quotient_lib.typer - src/debruijn.ml - src/elab.ml - src/env.ml - src/eval.ml - src/heap.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -531,4 +531,31 @@ Heap_unsafe-store-cell = Built-in "Heap.store-cell"; Heap_unsafe-load-cell : Int -> Int -> Heap ?t; Heap_unsafe-load-cell = Built-in "Heap.load-cell";

+%% +%% Quotient types +%% +Quotient = Built-in "Quotient" : (l1 : TypeLevel) ≡> (l2 : TypeLevel) + ≡> (A : Type_ l1) -> (R : A -> A -> Type_ l2) + -> Type_ (_∪_ l1 l2); + +Quotient_in : ?A -> Quotient ?A ?R; +Quotient_in = Built-in "Quotient.in"; + +Quotient_elim : (f : ?A -> ?B) + -> (p : (a : ?) -> (a' : ?) -> ?R a a' -> Eq (f a) (f a')) + ≡> (q : Quotient ?A ?R) -> ?B; +Quotient_elim = Built-in "Quotient.elim"; + +%% FIXME: We want to be able to say the following +%% Quotient_eq : (p : ?R ?a ?a') +%% ≡> Eq (Quotient_in (R := ?R) ?a) (Quotient_in (R := ?R) ?a'); +Quotient_eq : (R : ? -> ? -> ?) + ≡> R ?a ?a' + -> Eq (Quotient_in (R := R) ?a) (Quotient_in (R := R) ?a'); +Quotient_eq = Built-in "Quotient.eq"; + +%% Definition of a quotient type by using a normalisation function +%% NormToQuotient : (?A -> ?A) -> Type; +NormToQuotient f = Quotient ? (lambda a -> lambda a' -> Eq (f a) (f a')); + %%% builtins.typer ends here.

===================================== btl/pervasive.typer ===================================== @@ -690,6 +690,9 @@ depelim = load "btl/depelim.typer"; case_as_return_ = depelim.case_as_return_; case_return_ = depelim.case_return_;

+define-operator "qcase" () 42; +qcase_ = let lib = load "btl/qcase.typer" in lib.qcase_macro; + %%%% Unit tests function for doing file

%% It's hard to do a primitive which execute test file

===================================== btl/qcase.typer ===================================== @@ -0,0 +1,281 @@ +%% Qcase macro +%% Make the syntax cleaner for quotient eliminations +%% +%% qcase (e : A / R) +%% | Quotient_in a => e1 +%% | Quotient_eq a a' r i => e2 +%% +%% `a` is bound in `e1`, and `a`, `a'`, `r` and `i` are +%% bound in `e2`. `i` can only be used in an erasable manner. +%% +%% TODO: The annotation is necessary for now, as we need the `R` +%% However, we should make it optional. +is_sym : Sexp -> String -> Bool; +is_sym sexp s = + let + kfalse = K false; + in + Sexp_dispatch sexp + (lambda _ _ -> false) % Nodes + (String_eq s) % Symbol + kfalse % String + kfalse % Integer + kfalse % Float + kfalse; % List of Sexp +%% (build_explicit_arg "name" sexp) yields a +%% (name := sexp) Sexp +build_explicit_arg : String -> Sexp -> Sexp; +build_explicit_arg s sexp = Sexp_node (Sexp_symbol "_:=_") + (cons (Sexp_symbol s) + (cons sexp nil)); +qcase_impl = lambda (sexps : List Sexp) -> + %% For the same example that was given above, we expect + %% `sexps` to represent the following: + %% (_|_ (_:_ e (_/_ A R)) + %% (_=>_ (Quotient_in a) e1) + %% (_=>_ (Quotient_eq a a' r i) e2)) + %% Node : [(_|_ (_:_ e (_/_ A R)) (_=>_ (Qin a) e1) (_=>_ (Qeq a a' r i) e2))] + let + %% (_|_ (_:_ e (_/_ A R)) (_=>_ (Qin a) e1) (_=>_ (Qeq a a' r i) e2)) + head = List_head Sexp_error sexps; + knil = K nil; + kerr = K Sexp_error; + get-list : Sexp -> List Sexp; + get-list node = Sexp_dispatch node + (lambda op lst -> lst) % Nodes + knil % Symbol + knil % String + knil % Integer + knil % Float + knil; % List of Sexp + %% List of: + %% (_:_ e (_/_ A R)) + %% (_=>_ (Qin a) e1) + %% (_=>_ (Qeq a a' r i) e2) + body = get-list head; + elim_targ_sexp = List_nth 0 body Sexp_error; + elim_fn_sexp = List_nth 1 body Sexp_error; + elim_compat_sexp = List_nth 2 body Sexp_error; + %% Triple of the expression to eliminate, the underlying type A + %% and the relation R + %% A and R are optional + elim_expr_details : Triplet Sexp (Option Sexp) (Option Sexp); + elim_expr_details = + let + kerr = K (triplet Sexp_error none none); + extract_from_annotated_e : Sexp -> List Sexp -> + Triplet Sexp (Option Sexp) (Option Sexp); + extract_from_annotated_e _ xs = + if (Int_eq (List_length xs) 2) + then + let + e = List_nth 0 xs Sexp_error; + e_type = List_nth 1 xs Sexp_error; + extract_type sexp sexps = + if (is_sym sexp "_/_") + then + %% (_/_ A R ) + %% |___| |___| + %% | | + %% a r + let + a = List_nth 0 sexps Sexp_error; + r = List_nth 1 sexps Sexp_error; + in + triplet e (some a) (some r) + else + triplet e (some Sexp_error) (some Sexp_error); + kerr' = K (triplet e (some Sexp_error) (some Sexp_error)); + in + Sexp_dispatch e_type + extract_type % Nodes + kerr' % Symbol + kerr' % String + kerr' % Integer + kerr' % Float + kerr' % List of Sexp + else + triplet Sexp_error none none; + extract_targ_from_node : Sexp -> List Sexp -> + Triplet Sexp (Option Sexp) (Option Sexp); + extract_targ_from_node x xs = + %% Check if annotation is present + if (is_sym x "_:_") + then + %% Dissect the sexp to extract, the e, A and R + extract_from_annotated_e x xs + else + %% No annotation was given, return the entire + %% expresson as the elimination target + triplet x none none; + in + Sexp_dispatch elim_targ_sexp + extract_targ_from_node % Nodes + (lambda _ -> triplet elim_targ_sexp + none none) % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr; % List of Sexp + %% The function (`f`) argument + elim_fn : Sexp; + elim_fn = + let + extract_fn : Sexp -> List Sexp -> Sexp; + extract_fn sexp sexps = + %% Check that branch is well formed + if (and (is_sym sexp "_=>_") (Int_eq (List_length sexps) 2)) + then + let + %% (_=>_ (Quotient_in a) e1 ) + %% |_____________| |_________| + %% | | + %% qin fn_body + qin_sexp = List_nth 0 sexps Sexp_error; + fn_body_sexp = List_nth 1 sexps Sexp_error; + bound_var : Sexp; + bound_var = + let + extract_var head args = if (and (is_sym head "Quotient_in") + (Int_eq (List_length args) + 1)) + then + List_head Sexp_error args + else + %% FIXME: Might be good to have + %% a better way to report this + Sexp_error; + in + Sexp_dispatch qin_sexp + extract_var % Nodes + kerr % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr; % List of Sexp + in + Sexp_node (Sexp_symbol "lambda_->_") + (cons bound_var + (cons fn_body_sexp nil)) + else Sexp_error; + in + Sexp_dispatch elim_fn_sexp + extract_fn % Nodes + kerr % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr; % List of Sexp + %% The proof (`p`) argument + elim_compat : Sexp; + elim_compat = + let + extract_proof : Sexp -> List Sexp -> Sexp; + extract_proof sexp sexps = + %% Check that branch is well formed + if (and (is_sym sexp "_=>_") (Int_eq (List_length sexps) + 2)) + then + let + %% (_=>_ (Quotient_eq a a' r i) p ) + %% |____________________| |__________| + %% | | + %% qeq proof_exp + qeq_sexp = List_nth 0 sexps Sexp_error; + proof_exp_sexp = List_nth 1 sexps Sexp_error; + is_symbol : Sexp -> Bool; + is_symbol sexp = + let + ktrue = K true; + kfalse = K false; + in + Sexp_dispatch sexp + (K kfalse) % Nodes + ktrue % Symbol + kfalse % String + kfalse % Integer + kfalse % Float + kfalse; % List of Sexp + build_proof : Sexp -> List Sexp -> Sexp; + build_proof sexp sexps = + %% Check that the right identifier is used with + %% 3 or 4 arguments, also ensure that identifier are symbols + if (and (is_sym sexp "Quotient_eq") + (and %% We allow the last parameter `i` to be omitted + (or (Int_eq (List_length sexps) 3) + (Int_eq (List_length sexps) 4)) + (List_foldl (lambda acc sexp -> + and acc (is_symbol sexp)) + true sexps))) + then + let + mklambda : Sexp -> Sexp -> Sexp; + mklambda param body = + Sexp_node (Sexp_symbol "lambda_->_") + (cons param (cons body nil)); + proof_fn = + if (Int_eq (List_length sexps) 3) + then + %% `i` is absent, i.e. we expect to be provided + %% with an equality proof. + %% We want to convert Quotient_eq a a' r => e + %% to (lambda a a' r -> e) + quote (uquote (List_foldr mklambda + sexps proof_exp_sexp)) + else + %% Handle the case where `i` is present + %% We have to construct an equality proof + %% from what was given + %% We want to convert Quotient_eq a a' r i => e + %% to (lambda a a' r -> Eq_eq (f := lambda i ≡> e)) + let + erasable_param = List_nth 3 sexps Sexp_error; + proof_fn_params = + List_reverse (List_tail (List_reverse sexps nil)) + nil; + eq = quote (Eq_eq (f := + lambda (uquote erasable_param) ≡> + (uquote proof_exp_sexp))); + in + quote (uquote (List_foldr mklambda + proof_fn_params eq)); + in + build_explicit_arg "p" proof_fn + else + Sexp_error; + in + Sexp_dispatch qeq_sexp + build_proof % Nodes + kerr % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr % List of Sexp + else + Sexp_error; + in + Sexp_dispatch elim_compat_sexp + extract_proof % Nodes + kerr % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr; % List of Sexp + qelim_args : List Sexp; + qelim_args = case elim_expr_details + | triplet e a r => + let + res = (cons elim_fn + (cons elim_compat + (cons e nil))); + res' = (case r + | none => res + | some r' => + (cons (build_explicit_arg "R" r') res)); + in + res'; + qelim_sexp = Sexp_node (Sexp_symbol "Quotient_elim") + qelim_args; + in + IO_return qelim_sexp; +qcase_macro = macro qcase_impl;

===================================== samples/nat.typer ===================================== @@ -14,6 +14,13 @@ plus = lambda (x : Nat) -> lambda (y : Nat) -> case x | zero => y | succ z => succ (plus z y);

+minus : Nat -> Nat -> Nat; +minus = lambda (x : Nat) -> lambda (y : Nat) -> case x + | zero => zero + | succ m => case y + | zero => x + | succ n => minus m n; + one = succ zero; two = succ one; three = succ two;

===================================== samples/qcase_test.typer ===================================== @@ -0,0 +1,50 @@ +%% Defining a total relation on Unit +R : Unit -> Unit -> Type; +R u1 u2 = Unit; + +inQ : Quotient Unit R; +inQ = Quotient_in (); + +e1 : Unit; +e1 = qcase (inQ : Unit / R) + | Quotient_in a => () + | Quotient_eq a a' r i => (); + +e2 : Unit; +e2 = qcase (inQ : Unit / R) + | Quotient_in a => () + | Quotient_eq a a' r => Eq_refl; + +e3 : Unit; +e3 = qcase inQ + | Quotient_in a => () + | Quotient_eq a a' r i => (); + +e4 : Unit; +e4 = qcase inQ + | Quotient_in a => () + | Quotient_eq a a' r => Eq_refl; + +test-elim-to-unit = do { + Test_info "QCASE" "elimination to Unit"; + + r0 <- Test_eq "annotated elim to `Unit` with explicit `I`" e1 (); + r1 <- Test_eq "annotated elim to `Unit` without `I`" e2 (); + r2 <- Test_eq "unannotated elim to `Unit` with explicit `I`" e3 (); + r3 <- Test_eq "unannotated elim to `Unit` without `I`" e4 (); + + success <- IO_return (and (and (and r0 r1) r2) r3); + + if success then + (Test_info "QCASE" "elimination to Unit succeeded") + else + (Test_warning "QCASE" "elimination to Unit failed"); + + IO_return success; +}; + +exec-test = do { + b1 <- test-elim-to-unit; + + IO_return b1; +};

===================================== samples/quotient.typer ===================================== @@ -0,0 +1,141 @@ +%%%% Definitions of `Nat` +nat-lib = load "samples/nat.typer"; +Nat = nat-lib.Nat; +zero = nat-lib.zero; +succ = nat-lib.succ; +Nat_- = nat-lib.minus; +NatToInt = nat-lib.to-num; + +NatPair = Pair Nat Nat; + +normaliseZ : NatPair -> NatPair; +normaliseZ np = case np + | pair m n => pair (Nat_- m n) (Nat_- n m); + +%% FIXME: Ideally, we shouldn't need to define this separately as this should +%% be taken care of by `NormToQuotient`. However, for now we still to +%% explicitly pass this as a value of R to most `Quotient` functions as it +%% cannot be inferred. +equalZ : NatPair -> NatPair -> Type; +equalZ x1 x2 = Eq (normaliseZ x1) (normaliseZ x2); + +Z = NormToQuotient normaliseZ; + +%% +%% Quotient.eq +%% +%% Proof that quotiented elements are equal when the base elements themselves +%% are related in the underlying type. + +q1-0 : Quotient NatPair equalZ; +q1-0 = Quotient_in (pair (succ zero) zero); + +q2-1 : Quotient NatPair equalZ; +q2-1 = Quotient_in (pair (succ (succ zero)) (succ zero)); + +q1=1 : Eq q1-0 q2-1; +q1=1 = 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. + +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; + +%% `qcase` macro to facilitate elimination +Z_To_Int' : Quotient NatPair equalZ -> Int; +Z_To_Int' q = + %% The annotation is optional, but is necessary in + %% this case, since the propagation of type + %% information is insufficient the way things are now. + qcase (q : NatPair / equalZ) + | Quotient_in a => NatPairToInt a + | Quotient_eq a a' r i => NatPairToInt' (Eq_uneq (p := r) (i := i)); + +%% Omitting the `i` parameter by providing an equality proof on the RHS +Z_To_Int'' : Quotient NatPair equalZ -> Int; +Z_To_Int'' q = + qcase (q : NatPair / equalZ) + | Quotient_in a => NatPairToInt a + | Quotient_eq a a' r => NatPairToIntCompat a a' r; + +%% TODO: Define Quotient NatPair equalZ ≃ Int + +elim_β : (A : Type_ ?) ≡> (B : Type_ ?) + ≡> (R : A -> A -> Type_ ?) + ≡> (f : A -> B) + -> (p : (a : A) -> (a' : A) -> R a a' -> Eq (f a) (f a')) + -> (a : A) -> Eq (Quotient_elim (R := R) f + (p := p) (Quotient_in (R := R) a)) + (f a); +elim_β f p a = Eq_refl; + +%% +%% Proof that the existence of Quotient types implies functional extensionality +%% + +funext : (A : Type_ ?) -> (B : A -> Type_ ?) + -> (f1 : (a : A) -> B a) -> (f2 : (a : A) -> B a) + -> (h : (a : A) -> Eq (f1 a) (f2 a)) -> Eq f1 f2; +funext A B f1 f2 h = + let + fn_type = (a : A) -> B a; + %% This relation can be easily shown to be an equivalence relation + %% by leveraging the properties of the `Eq` type. + equiv_rel : (f1 : fn_type) -> (f1 : fn_type) -> Type_ ?; + equiv_rel f1 f2 = ((a : A) -> Eq (f1 a) (f2 a)); + extfun = Quotient fn_type equiv_rel; + extfun_app : (f : extfun) -> fn_type; + extfun_app f a = Quotient_elim (R := equiv_rel) + (f := lambda f -> f a) + (p := lambda f1 f2 r -> r a) f; + sound : Eq (Quotient_in (R := equiv_rel) f1) + (Quotient_in (R := equiv_rel) f2); + sound = Quotient_eq (R := equiv_rel) (a := f1) (a' := f2) h; + %% The two terms reduce to f1 and f2 respectively by + %% 1. Leveraging the fact that elim_β holds definitionally + %% 2. The η-equivalence of functions + res : Eq (extfun_app (Quotient_in (R := equiv_rel) f1)) + (extfun_app (Quotient_in (R := equiv_rel) f2)); + %% FIXME: Loading `samples/hott.typer` causes the following error + %% [X] Fatal :(internal) lub of two SLsucc + %% Hence, the definition of `Eq_cong` is inlined for now + res = Eq_eq (f := lambda i ≡> extfun_app (Eq_uneq (p := sound) (i := i))); + in + res;

===================================== samples/quotient_lib.typer ===================================== @@ -0,0 +1,123 @@ +%%%%% Prelude %%%%%% + +%% FIXME : Loading hott.typer doesn't work for some reason +%% due to "[X] Fatal :(internal) lub of two SLsucc" +%% Some definitions will be duplicated for now + +Eq_funext : (f : ? -> ?) => (g : ? -> ?) => ((x : ?) -> Eq (f x) (g x)) + -> Eq f g; +Eq_funext p = Eq_eq (f := lambda i ≡> lambda x -> Eq_uneq (p := p x) (i := i)); + +HoTT_isProp P = (x : P) -> (y : P) -> Eq x y; + +HoTT_isSet A = (x : A) -> (y : A) -> HoTT_isProp (Eq x y); + +HoTT_isContr = typecons (HoTT_isContr (l ::: TypeLevel) + (A : Type_ l)) + (isContr (a : A) ((a' : A) -> Eq a a')); +isContr = datacons HoTT_isContr isContr; + +%%%%% Prelude END %%%%%% + +%% TODO: Prove dependent version of this after we introduce +%% dependent elim, which will be more interesting and more +%% worthwhile +recProp : (A : Type_ ?) ≡> (B : Type_ ?) + ≡> (R : A -> A -> Type_ ?) ≡> (p : HoTT_isProp B) + -> (f : A -> B) -> Quotient A R -> B; +recProp = lambda _ _ _ _ _ R ≡> + lambda p f x -> + Quotient_elim (R := R) f (p := lambda a a' r -> p (f a) (f a')) x; + +%% Again, this is not very interesting, unlike its dependent +%% counterpart. +recContr : (A : Type_ ?) ≡> (B : Type_ ?) + ≡> (R : A -> A -> Type_ ?) + ≡> (p : HoTT_isContr B) + -> Quotient A R -> B; +recContr = lambda _ _ _ _ _ R ≡> + lambda p x -> case p + | isContr a f => Quotient_elim (R := R) + (lambda _ -> a) + (p := lambda a a' r -> Eq_refl) + x; + +%% FIXME: Quotient_elim should be named Quotient_rec? +%% This definition requires dependent elimination of `Quotient` +%% +%% rec2 : (A : Type_ ?) ≡> (B : Type_ ?) ≡> (C : Type_ ?) +%% ≡> (R : A -> A -> Type_ ?) ≡> (S : B -> B -> Type_ ?) +%% ≡> (C_isSet : HoTT_isSet C) +%% -> (f : A -> B -> C) +%% -> ((a : A) -> (b : A) -> (c : B) -> R a b -> Eq (f a c) (f b c)) +%% -> ((a : A) -> (b : B) -> (c : B) -> S b c -> Eq (f a b) (f a c)) +%% -> Quotient A R -> Quotient B S -> C; +%% rec2 = lambda _ _ _ _ _ A B C R S ≡> +%% lambda C_isSet f feql feqr -> +%% Quotient_elim (R := R) +%% (lambda a -> +%% lambda b -> Quotient_elim (R := S) (f a) +%% (p := feqr a) b) +%% (p := lambda a a' r -> +%% let +%% eqf : (b : B) -> Eq (f a b) (f a' b); +%% eqf b = feql a a' b r; +%% eqf' : Eq (f a) (f a'); +%% eqf' = Eq_funext (f := f a) (g := f a') eqf; +%% p : (x : Quotient B S) -> +%% HoTT_isProp (Eq (Quotient_elim (R := S) (f a) +%% (p := feqr a) x) +%% (Quotient_elim (R := S) (f a') +%% (p := feqr a') x)); +%% p x = C_isSet (Quotient_elim (R := S) (f a) +%% (p := feqr a) x) +%% (Quotient_elim (R := S) (f a') +%% (p := feqr a') x); +%% res : (x : Quotient B S) -> +%% (Eq (Quotient_elim (R := S) (f a) +%% (p := feqr a) x) +%% (Quotient_elim (R := S) (f a') +%% (p := feqr a') x)); +%% res x = Quotient_elim (A := B) +%% %% FIXME: We need depelim here +%% (B := Eq (f a b) (f a' b)) +%% (R := S) +%% eqf +%% (p := lambda u v s -> +%% Eq_eq (f := lambda i ≡> +%% p (Eq_uneq (p := Quotient_eq (R := S) s) (i := i)) +%% (eqf u) (eqf v))) +%% x; +%% in +%% Eq_funext (f := Quotient_elim (R := S) (f a) +%% (p := feqr a)) +%% (g := Quotient_elim (R := S) (f a') +%% (p := feqr a')) +%% res); + +%% Lemma 6.10.2 in HoTT book, to prove this we need to +%% apply propositional truncation on SurjectiveQuotientProof. +%% type SurjectiveQuotientProof (A : ?) (x : Quotient A ?R) +%% | surjectiveQuotientProof (a : A) (Eq (Quotient_in a) x); +%% Quotient_in_surjective : (x : Quotient ?A ?R) -> ||SurjectiveQuotientProof ?A ?R x||₁; + +%% Given a proof that a unary operation preserves the underlying +%% relation, we can apply the operation to the quotiented type. +quotUnaryOp : (A : Type_ ?) + ≡> (R : A -> A -> Type_ ?) + ≡> (op : A -> A) + -> ((a : A) -> (a' : A) -> R a a' -> R (op a) (op a')) + -> Quotient A R -> Quotient A R; +quotUnaryOp = lambda _ _ A R ≡> + lambda op h x -> + let + opPreservesQuotient : (a : A) -> (a' : A) -> R a a' -> + Eq (t := Quotient A R) + (Quotient_in (op a)) + (Quotient_in (op a')); + opPreservesQuotient a a' r = Quotient_eq (R := R) (h a a' r); + in + Quotient_elim (R := R) + (lambda a -> Quotient_in (op a)) + (p := opPreservesQuotient) + x;

===================================== src/debruijn.ml ===================================== @@ -145,9 +145,9 @@ let type_eq_type = 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"] + ["Int"; "Elab_Context"; "Sexp"; "FileHandle"; + (* From `heap.ml`. *) + "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. @@ -183,7 +183,7 @@ type lctx_length = db_ridx type meta_scope = scope_level (* Integer identifying a level. *) * lctx_length (* Length of ctx when the scope is added. *) - * (meta_id SMap.t ref) (* Metavars already known in this scope. *) + * ((meta_id * scope_level) SMap.t ref) (* Metavars already known in this scope. *)

type typeclass_ctx = (ltype * lctx_length) list (* the list of type classes *)

===================================== src/elab.ml ===================================== @@ -651,22 +651,15 @@ and sform_identifier ctx loc sargs ot = let subst = S.shift ctx_shift in let (_, _, rmmap) = ectx_get_scope ctx in if not (name = "") && SMap.mem name (!rmmap) then - let idx = SMap.find name (!rmmap) in - match (metavar_lookup idx) with - | MVar (sl',_,_) - -> if sl = sl' then - (mkMetavar (idx, subst, (loc, Some name)), Lazy) - else - (* FIXME: The variable is from another scope_level! It - means that `subst` is not the right substitution for - the metavar! *) - fatal ~loc:(Sexp.location loc) ("Bug in the elaboration of a metavar" - ^^ " repeated at a different scope level!") - | MVal _ - -> (* FIXME: We face the same problem as above, but here, - the situation is worse, we don't even know the scope - level! *) - fatal ~loc:(Sexp.location loc) "Bug in the elaboration of a repeated metavar!" + let (idx, sl') = SMap.find name (!rmmap) in + if sl = sl' then + (mkMetavar (idx, subst, (loc, Some name)), Lazy) + else + (* FIXME: The variable is from another scope_level! It + means that `subst` is not the right substitution for + the metavar! *) + fatal ~loc:(Sexp.location loc) ("Bug in the elaboration of a metavar" + ^^ " repeated at a different scope level!") else let t = match ot with | None -> newMetatype octx sl loc @@ -679,7 +672,7 @@ and sform_identifier ctx loc sargs ot = match lexp_lexp' mv with | Metavar (idx, _, _) -> idx | _ -> fatal ~loc:(Sexp.location loc) "newMetavar returned a non-Metavar" in - rmmap := SMap.add name idx (!rmmap)); + rmmap := SMap.add name (idx, sl) (!rmmap)); (mv, match ot with Some _ -> Checked | None -> Lazy)

(* Normal identifier. *)

===================================== src/env.ml ===================================== @@ -184,6 +184,11 @@ let value_string_with_type v ltype ctx = (Lexp.to_string left) (Lexp.to_string right) (Lexp.to_string t) + | [_; _; (_, t); (_, r)] + when OL.conv_builtin_p ctx e' "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 ===================================== @@ -535,12 +535,8 @@ and eval_call loc unef i f args = if n >= 0 then (Var (vdummy, n))::buildargs (n - 1) else [] in - let rec buildbody n = - if n > 0 then - Lambda (vdummy, buildbody (n - 1)) - else Call (Builtin (dloc, name), buildargs (arity - 1)) in Closure (vdummy, - buildbody (arity - nargs - 1), + Call (Builtin (dloc, name), buildargs (List.length args)), buildctx args Myers.nil)

with @@ -1027,6 +1023,17 @@ 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")

+(* Dummy "implementation" of a type constructor. *) +let type_constructor loc _ _args = + error loc "No implementation of the construction of this type" + +let quotient_elim loc depth args = + let trace_dum = (Var ((epsilon (loc), None), -1)) in + match args with + | [f; q] -> + eval_call loc trace_dum depth f [q] + | _ -> error loc "Quotient.elim expects 2 arguments" + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -1048,6 +1055,7 @@ let register_builtin_functions () = ("Float->String" , float_to_string, 1); ("Int->String" , int_to_string, 1); ("Integer->String", integer_to_string, 1); + ("IO" , type_constructor, max_int); ("IO.bind" , io_bind, 2); ("IO.return" , io_return, 1); ("IO.run" , io_run, 2); @@ -1059,6 +1067,7 @@ let register_builtin_functions () = ("Eq.eq" , arity0_fun, 0); ("Eq.uneq" , eq_uneq, 2); ("Y" , y_operator, 1); + ("Ref" , type_constructor, max_int); ("Ref.make" , ref_make, 1); ("Ref.read" , ref_read, 1); ("Ref.write" , ref_write, 2); @@ -1070,6 +1079,7 @@ let register_builtin_functions () = ("Elab.is-arg-erasable", is_arg_erasable, 3); ("Elab.nth-arg" , nth_arg, 3); ("Elab.arg-pos" , arg_pos, 3); + ("Array" , type_constructor, max_int); ("Array.append" , array_append,2); ("Array.create" , array_create,2); ("Array.length" , array_length,1); @@ -1084,6 +1094,10 @@ let register_builtin_functions () = ("Test.false" , test_false,2); ("Test.eq" , test_eq,3); ("Test.neq" , test_neq,3); + ("Quotient" , type_constructor, max_int); + ("Quotient.in" , nop_fun, 1); + ("Quotient.eq" , nop_fun, 1); + ("Quotient.elim" , quotient_elim, 2); ] let _ = register_builtin_functions ()

===================================== src/heap.ml ===================================== @@ -138,6 +138,7 @@ let heap_load_cell : builtin_function = | _ -> error ~loc "`Heap.store-cell` expects [Int; Int]"

let register_builtins () = + add_builtin_function "Heap" Eval.type_constructor max_int; 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 ===================================== @@ -304,7 +304,9 @@ 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_builtin_p ctx eq "Eq.eq" + | Call (_, eq, _) + when conv_builtin_p ctx eq "Eq.eq" || + conv_builtin_p ctx eq "Quotient.eq" -> Some (fx, rest) | _ -> None) | _ -> None @@ -319,12 +321,23 @@ and eq_uneq_whnf ctx args = else None | _ -> None

+and quotient_elim_whnf ctx args = + match args with + | _l1 :: _l2 :: _l3 :: _A :: _R :: _P :: (_, f) :: (_, _p) :: (_, q) :: rest + -> (match lexp'_whnf q ctx with + | Call (_, qin, [_; _; _; _; (_, e)]) + when conv_builtin_p ctx qin "Quotient.in" + -> Some (mkCall (dsinfo, f, [Anormal, e]), rest) + | _ -> None) + | _ -> None + and register_reducible_builtins () = reducible_builtins := List.fold_right (fun (n, f) m -> SMap.add n f m) [ ("Eq.cast", eq_cast_whnf); - ("Eq.uneq", eq_uneq_whnf) + ("Eq.uneq", eq_uneq_whnf); + ("Quotient.elim", quotient_elim_whnf) ] !reducible_builtins

(** A very naive implementation of sets of pairs of lexps. *)

===================================== 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/elab_test.ml ===================================== @@ -180,7 +180,7 @@ unify (f Z (S Z)) (f (S Z) Z); |}

let _ = add_elab_test_decl - "WHNF of Eq.cast" + "WHNF of Eq.cast (applied to Eq.eq)" {| x = (4 : Int); y = x; @@ -192,6 +192,27 @@ test : Eq (Eq_cast (p := p) (f := lambda _ -> Unit) ()) (); test = Eq_refl; |}

+let _ = add_elab_test_decl + "WHNF of Eq.cast (applied to Quotient.eq)" + {| +totalRel : Unit -> Unit -> Type; +totalRel u1 u2 = Unit; + +unitQ : Quotient Unit totalRel; +unitQ = Quotient_in unit; + +unitQ' = unitQ; + +unitQ=unitQ' : Eq (t := Quotient Unit totalRel) unitQ unitQ'; +unitQ=unitQ' = Quotient_eq (R := totalRel) + (a := unit) + (a' := unit) + unit; + +test : Eq (Eq_cast (p := unitQ=unitQ') (f := lambda _ -> Unit) ()) (); +test = Eq_refl; + |} + let _ = add_elab_test_decl "Decidable at the type level" {|

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