Juillet 2023 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][quotient-types] 7 commits: Implement `Quotient` formation
by James Tan Juan Whei (＠jamestjw) 24 Aoû '23

24 Aoû '23

James Tan Juan Whei pushed to branch quotient-types at Stefan / Typer Commits: 61d01f99 by James Tan at 2023-07-19T22:16:16-04:00 Implement `Quotient` formation - - - - - 1282e0ba by James Tan at 2023-07-19T22:16:16-04:00 Implement `Quotient` introduction - - - - - 00341dfd by James Tan at 2023-07-19T22:16:17-04:00 Implement `Quotient` elimination - - - - - 55c38d85 by James Tan at 2023-07-19T22:16:17-04:00 Implement `Eq` constructor for `Quotient` - - - - - aa04cc68 by James Tan at 2023-07-19T22:16:17-04:00 Improve unification scheme for SLlub (l1, l2) when l1 ≃ l2 - - - - - d00058fa by James Tan at 2023-07-26T19:34:39-04:00 Implement `qcase` macro - Facilitates `Quotient` elimination - - - - - 48982943 by James Tan at 2023-07-26T19:34:40-04:00 Write some proofs about quotient types - - - - - 12 changed files: - btl/builtins.typer - btl/pervasive.typer - + btl/qcase.typer - + samples/qcase_test.typer - + samples/quotient.typer - + samples/quotient_lib.typer - src/debruijn.ml - src/env.ml - src/eval.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -531,4 +531,42 @@ 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"; + +%% 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. ===================================== 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,284 @@ +%% 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 bounded in `e1`, and `a`, `a'`, `r` and `i` are +%% bounded 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 (Integer->Int 0) body Sexp_error; + elim_fn_sexp = List_nth (Integer->Int 1) body Sexp_error; + elim_compat_sexp = List_nth (Integer->Int 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) (Integer->Int 2)) + then + let + e = List_nth (Integer->Int 0) xs Sexp_error; + e_type = List_nth (Integer->Int 1) xs Sexp_error; + extract_type sexp sexps = + if (is_sym sexp "_/_") + then + %% (_/_ A R ) + %% |___| |___| + %% | | + %% a r + let + a = List_nth (Integer->Int 0) sexps Sexp_error; + r = List_nth (Integer->Int 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) (Integer->Int 2))) + then + let + %% (_=>_ (Quotient_in a) e1 ) + %% |_____________| |_________| + %% | | + %% qin fn_body + qin_sexp = List_nth (Integer->Int 0) sexps Sexp_error; + fn_body_sexp = List_nth (Integer->Int 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) + (Integer->Int 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) + (Integer->Int 2))) + then + let + %% (_=>_ (Quotient_eq a a' r i) p ) + %% |____________________| |__________| + %% | | + %% qeq proof_exp + qeq_sexp = List_nth (Integer->Int 0) sexps Sexp_error; + proof_exp_sexp = List_nth (Integer->Int 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 exactly + %% 4 arguments, also ensure that identifier are symbols + %% TODO: Make it possible to omit the `i`, in which case + %% we expect p to be an equality proof. + if (and (is_sym sexp "Quotient_eq") + (and %% We allow the last parameter `i` to be omitted + (or (Int_eq (List_length sexps) (Integer->Int 3)) + (Int_eq (List_length sexps) (Integer->Int 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) (Integer->Int 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 (Integer->Int 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/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,116 @@ +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; + +%% `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 ===================================== samples/quotient_lib.typer ===================================== @@ -0,0 +1,129 @@ +%%%%% 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) -> + (x : 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) -> + (x : 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? +%% 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,7 +145,7 @@ let type_eq_type = let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) let builtin_axioms = - ["Int"; "Elab_Context"; "IO"; "Ref"; "Sexp"; "Array"; "FileHandle"; + ["Int"; "Elab_Context"; "IO"; "Ref"; "Sexp"; "Array"; "FileHandle"; "Quotient"; (* From `healp.ml`. *) "Heap"; "DataconsLabel"] ===================================== src/env.ml ===================================== @@ -184,7 +184,12 @@ let value_string_with_type v ltype ctx = (Lexp.to_string left) (Lexp.to_string right) (Lexp.to_string t) - | _ -> value_string v) + | [_; _; (_, 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 ===================================== @@ -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/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 ===================================== 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,28 @@ 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/bfbff550912f1de9c0b1d61e494c2ac7… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/bfbff550912f1de9c0b1d61e494c2ac7… You're receiving this email because of your account on gitlab.com.

3 3

Bug - Types inductifs avec des paramètres dépendants
by James Juan Whei Tan 23 Jul '23

23 Jul '23

Salut, Je vous montre le problème lié aux types inductifs que j’ai mentionné hier. On définit d’abord le type `Sigma` Sigma = typecons (Sigma (l1 ::: TypeLevel) (l2 ::: TypeLevel) (A : Type_ l1) (B : A -> Type_ l2)) (sigma (fst : A) (snd : B fst)); sigma = datacons Sigma sigma; Mais quand il s’agit de construire une expression de ce type, on se retrouve dans l’obligation de fournir la valeur de `B` explicitement lors de la construction même si l’information se trouve déjà dans l’annotation de type. up : Sigma Unit (lambda _ -> Unit);; up = sigma (B := lambda _ -> Unit) unit unit; %% ça ne marche plus si on enlève l’argument B Si on enlève le B, on obtient l’erreur "Context expected: (?B↑0 unit) but expression has type: Unit”. J’ai investigué un tout petit peu, mais malheureusement j’ai pas pu trouver la source de ce problème. J’ai rencontré un autre problème avec les indices de Debruijn quand j’écrivais cette preuve HoTT_isContr A = Sigma A (lambda (x : A) -> ((y : A) -> Eq x y)); isContrΠ : (A : Type_ ?) ≡> (B : A -> Type_ ?) ≡> (h : (x : A) -> HoTT_isContr (B x)) -> HoTT_isContr ((x : A) -> B x); isContrΠ h = sigma (A := (x : A) -> B x) (B := (lambda (x : ((x : A) -> B x)) -> ((y : ((x : A) -> B x)) -> Eq x y))) (lambda x -> case (h x) | sigma bx p => bx) (lambda f -> Eq_eq (f := lambda i ≡> lambda x -> case (h x) | sigma bx p => Eq_uneq (p := p (f x)) (i := i))); qui donnait l’erreur [X] Fatal :(DEBRUIJN) DeBruijn index 2 refers to wrong name. Expected: " %gensym% no 42 “ got " %gensym% no 39 “ On rencontre ce problème quand on est dans la branche du 2e `case` dans le code. Mon hypothèse est que le `bx` n’est pas égal à l’autre `bx` dans le 1er `case`, et puisque ce que renvoit le 2e `case` dépend de ce qui est renvoyé dans l’autre, ça devient un problème. La bonne nouvelle c’est que j’ai réussi à contourner le problème en remplaçant les deux `case ` par des appels à des fonctions auxiliaires. pr1 : Sigma ?A ?B -> ?A; pr1 s = case s | sigma a _ => a; pr2 : (s : Sigma ?A ?B) -> ?B (pr1 s); pr2 = lambda _ _ A B ≡> lambda s -> case s | sigma a b => let branch=s : Eq (sigma (A := A) (B := B) a b) s; branch=s = ##DeBruijn 0; res : B (pr1 s); res = Eq_cast (p := branch=s) (f := lambda x -> B (pr1 x)) b; in res; isContrΠ : (A : Type_ ?) ≡> (B : A -> Type_ ?) ≡> (h : (x : A) -> HoTT_isContr (B x)) -> HoTT_isContr ((x : A) -> B x); isContrΠ = lambda _ _ A B ≡> lambda h -> sigma (A := (x : A) -> B x) (B := (lambda (x : ((x : A) -> B x)) -> ((y : ((x : A) -> B x)) -> Eq x y))) (lambda x -> pr1 (h x)) (lambda g -> Eq_eq (f := lambda i ≡> lambda x -> Eq_uneq (p := (pr2 (h x)) (g x)) (i := i))); A première vue, c’est peut-être lié à un problème similaire dans `hurkens.typer` (regardez la ligne 87). Pour faciliter la reproduction de ces bugs, j’ai attaché en pièce jointe un fichier qui contient tout le code que j’ai montré ci-dessus. James

2 3

Re: [Typer] Implémentation du type Interval
by Stefan Monnier 19 Jul '23

19 Jul '23

> Désolé pour le retard je l’avais complètement oublié, je viens de > créer une branche qui s’appelle `cubical-equality`. Merci. Je l'ai divisé en quelques commit plus ou moins indépendants et je l'ai poussé sur `main`. Stefan

2 5

[Git][monnier/typer][quotient-types] 8 commits: Move Eq.eqs definition to builtins.typer
by James Tan Juan Whei (＠jamestjw) 19 Jul '23

19 Jul '23

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(a)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(a)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(a)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(a)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/a68c3a6aa15a0575f08ca0d386208720… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a68c3a6aa15a0575f08ca0d386208720… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] test/env_tests.ml: Adjust to last change
by Stefan (＠monnier) 19 Jul '23

19 Jul '23

Stefan pushed to branch main at Stefan / Typer Commits: 6ea6caae by Stefan Monnier at 2023-07-18T20:03:41-04:00 test/env_tests.ml: Adjust to last change - - - - - 1 changed file: - tests/env_test.ml Changes: ===================================== 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/-/commit/6ea6caae3d7a7e7619ade47cbc8fc58c1… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6ea6caae3d7a7e7619ade47cbc8fc58c1… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] Move definition of some types to `builtins.typer`
by Stefan (＠monnier) 19 Jul '23

19 Jul '23

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/f72f5e81a6773eb89c27efa7b5c71057c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f72f5e81a6773eb89c27efa7b5c71057c… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] Move Eq.eqs definition to builtins.typer
by Stefan (＠monnier) 18 Jul '23

18 Jul '23

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(a)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(a)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(a)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(a)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/5d8e2879f991e5ed879e4c47f0e6ba724… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/5d8e2879f991e5ed879e4c47f0e6ba724… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch cubical-equality
by Stefan (＠monnier) 17 Jul '23

17 Jul '23

Stefan deleted branch cubical-equality at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] 5 commits: * btl/pervasive.typer (id): Rename from `I`
by Stefan (＠monnier) 14 Jul '23

14 Jul '23

Stefan pushed to branch main at Stefan / Typer Commits: 269f8366 by Stefan Monnier at 2023-07-13T23:50:28-04:00 * btl/pervasive.typer (id): Rename from `I` - - - - - eac70cf3 by Stefan Monnier at 2023-07-14T00:48:31-04:00 Add the η rule, yay! - - - - - a4bd5195 by Stefan Monnier at 2023-07-14T00:48:41-04:00 Improve calling convention for builtin reductions - - - - - 3575175d by James Tan at 2023-07-14T00:48:41-04:00 Add implementation of `Eq` based on the `Interval` - - - - - 459aad06 by Stefan Monnier at 2023-07-14T00:50:51-04:00 Make the value printer take the type as arg - - - - - 17 changed files: - btl/builtins.typer - btl/case.typer - btl/pervasive.typer - btl/poly-lits.typer - debug_util.ml - samples/hott.typer - samples/unerase.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/env.ml - src/eval.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml - tests/env_test.ml - tests/eval_test.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -45,10 +45,32 @@ unit = datacons Unit unit; %% The empty type, with no constructors: nothing can have this type. Void = typecons Void; +%% I = typecons I i0 i1; +i0 = datacons I i0; +i1 = datacons I i1; + +I_not : I -> I; +I_not i = case i + | i0 => i1 + | i1 => i0; + %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l -Eq_refl : ((x : ?t) ≡> Eq x x); -Eq_refl = ##Eq\.refl; + +Eq_eq : (l : TypeLevel) ≡> (t : Type_ l) + ≡> (f : I ≡> t) + ≡> Eq (f (_ := i0)) (f (_ := i1)); +Eq_eq = ##Eq\.eq; + +Eq_uneq : (l : TypeLevel) ≡> (t : Type_ l) + ≡> (x : t) => (y : t) + => (p : Eq x y) ≡> (i : I) ≡> t; +Eq_uneq = Built-in "Eq.uneq"; + +Eq_refl : (l : TypeLevel) ≡> (t : Type_ l) + ≡> (x : t) ≡> Eq x x; +Eq_refl = lambda _ ≡> lambda _ ≡> lambda x + ≡> Eq_eq (f := lambda _ ≡> x); Eq_cast : (x : ?) ≡> (y : ?) ≡> (p : Eq x y) @@ -62,14 +84,13 @@ Eq_cast = Built-in "Eq.cast"; %% FIXME: I'd like to just say: %% Eq_comm : Eq ?x ?y -> Eq ?y ?x`; Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; -Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) - %% FIXME: The code is incorrectly accepted even - %% without this `(p := p)` because we just get a - %% metavar which remains uninstantiated and then - %% the definition gets ignored in the runtime - %% environment (see Eval.from_lctx). - (p := p) - Eq_refl; +Eq_comm p = Eq_eq (f := lambda i ≡> Eq_uneq (p := p) (i := I_not i)); + +%% FIXME: The below code is accepted even in the absence of `p := y=z`. +%% If `y=z` is taken to be unnecessary, this implies that we could define +%% Eq_broken_trans : Eq ?x ?y -> Eq ?x ?z; +Eq_trans : (x : ?t) ≡> (y : ?t) ≡> (z : ?t) ≡> Eq x y -> Eq y z -> Eq x z; +Eq_trans x=y = lambda y=z -> Eq_cast (p := y=z) (f := lambda x' -> Eq x x') x=y; %% General recursion!! %% Whether this breaks consistency or not is a good question. ===================================== btl/case.typer ===================================== @@ -200,7 +200,7 @@ kinds pat = let ctor-name : Sexp -> String; ctor-name pat = Sexp_dispatch pat (lambda s ss -> ctor-name s) - I strerr strerr strerr strerr; + id strerr strerr strerr strerr; in ctor-name pat; %% @@ -217,7 +217,7 @@ kinds pat = let %% str_of_sym : Sexp -> String; str_of_sym arg = Sexp_dispatch arg - (lambda _ _ -> "< error >") I strerr strerr strerr strerr; + (lambda _ _ -> "< error >") id strerr strerr strerr strerr; %% %% map function for all pattern's variables ===================================== btl/pervasive.typer ===================================== @@ -1,6 +1,6 @@ %%% pervasive --- Always available definitions -%% Copyright (C) 2011-2022 Free Software Foundation, Inc. +%% Copyright (C) 2011-2023 Free Software Foundation, Inc. %% %% Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> %% Keywords: languages, lisp, dependent types. @@ -187,7 +187,7 @@ List_empty xs = Int_eq (List_length xs) (Integer->Int 0); %%% Good 'ol combinators -I x = x; +id x = x; %% Use explicit erasable annotations since with an annotation like %% K : ?a -> ?b -> ?a; ===================================== btl/poly-lits.typer ===================================== @@ -18,7 +18,7 @@ typer-immediate = | _ => deflt); IntegerFromInteger : FromInteger Integer; -IntegerFromInteger = mkFromInteger I; +IntegerFromInteger = mkFromInteger id; IntFromInteger : FromInteger Int; IntFromInteger = mkFromInteger Integer->Int; ===================================== debug_util.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -177,7 +177,7 @@ let main () = let body = (get_rte_variable (dsinfo, Some "main") main rctx) in (* eval main *) - print_eval_result 1 body + print_eval_result 1 body None with Not_found -> () ===================================== samples/hott.typer ===================================== @@ -59,6 +59,71 @@ %% (x₁ : t(i := i₀)) (x₂ : t(i := i₁)) %% | Hrefl (p : Eq t₁ t₂) (Eq (coe p x₁) x₂); +%% Example usage of functions based on the Interval +%% type to define equalities +constantString : I ≡> Type; +constantString = lambda _ ≡> String; + +reflString : Eq String String; +reflString = Eq_eq (f := constantString); + +hello : String; +hello = Eq_cast (p := reflString) (f := lambda x -> x) "hello"; + +%% This doesn't work as `helloOrWorld`'s first argument is not erasable, +%% hence we can't prove obviously false equalities. +%% helloOrWorld : I -> String; +%% helloOrWorld s = case s +%% | i0 => "hello" +%% | i1 => "world"; +%% +%% hello=world : Eq "hello" "world"; +%% hello=world = Eq_eq helloOrWorld; + +constantString' : I ≡> Type; +constantString' = Eq_uneq (p := reflString); + +hello2 : Eq_uneq (p := reflString) (i := i0); +hello2 = "hello"; + +hello3 : constantString' (_ := i0); +hello3 = "hello"; + +hello4 : constantString' (_ := i1); +hello4 = "hello"; + +helloRefl : Eq "hello" hello; +helloRefl = Eq_refl; + +%% Functional extensionality +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)); + +%% Properties of the equality type +Eq_cong : (x : ?A) => (y : ?A) => + (f : ?A -> ?) -> (p : Eq x y) + -> Eq (f x) (f y); +Eq_cong f p = Eq_eq (f := lambda i ≡> f (Eq_uneq (p := p) (i := i))); + +%% This is necessary to prove Eq_comm_inv +notnot=id : (i : I) -> Eq i (I_not (I_not i)); +notnot=id i = case i return (Eq i (I_not (I_not i))) + | i0 => Eq_refl + | i1 => Eq_refl; + +%% FIXME: This should be provable, need to reduce `(Eq_comm (Eq_comm p))` to `p`. +%% It should be sufficient to add the following reduction: +%% Eq_uneq (Eq_eq f) i = f (_ := i) +%% and apply `notnot=id`. +%% Eq_comm_inv : (x : ?t) => (y : ?t) => (p : Eq x y) -> Eq (Eq_comm (Eq_comm p)) p; +%% Eq_comm_inv p = ?; + +%% FIXME: Similar to above. +%% Eq_cong_Id : (x : ?t) => (y : ?t) => (p : Eq x y) -> Eq (Eq_cong id p) p; +%% Eq_cong_Id p = ?; + %%%% Univalence %% type Equiv_function (f : ?A -> ?B) (g : ?A -> ?B) ===================================== samples/unerase.typer ===================================== @@ -1,4 +1,4 @@ %Eq_unerase : Eq ?x ?y ≡> Eq ?x ?y; Eq_unerase = - lambda x y (p : Eq x y) ≡> + lambda x y => lambda (p : Eq x y) ≡> Eq_cast (p := p) (f := Eq x) Eq_refl; ===================================== src/REPL.ml ===================================== @@ -1,6 +1,6 @@ (* REPL.ml --- Read Eval Print Loop (REPL) -Copyright (C) 2016-2021 Free Software Foundation, Inc. +Copyright (C) 2016-2023 Free Software Foundation, Inc. Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> @@ -141,13 +141,17 @@ let eval_interactive Elab.resolve_instances_and_generalize ctx lxp Elab.wrapLambda lxp in let lexprs = List.map (generalize_lexp ectx') lexprs in - List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs; + let ltypes = List.map (fun lexpr -> OL.check (ectx_to_lctx ectx') lexpr) lexprs in List.iter interactive#process_decls ldecls; Log.print_log (); let values = List.map interactive#eval_expr lexprs in - List.iter (Eval.print_eval_result i) values; + List.iter2 (fun v t -> + Eval.print_eval_result i + v + (Some (t, (ectx_to_lctx ectx')))) + values ltypes; Log.print_log (); ectx' ===================================== src/builtin.ml ===================================== @@ -157,7 +157,8 @@ let register_builtin_csts () = 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.refl" DB.eq_refl + 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) ===================================== src/debruijn.ml ===================================== @@ -141,23 +141,47 @@ let type_eq_type = mkVar (tv, 1), mkSort (dsinfo, Stype (mkVar (lv, 3))))))) let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) -let eq_refl = + +(* FIXME: Is this the best way to do this? Originally, I wanted to + * define this in Typer and then reference it from OCaml code. + *) +(* Defining the following: + * typecons I i0 i1 + *) +let type_interval + = mkInductive (dsinfo, (dloc, "I"), [], + List.fold_left (fun m name -> SMap.add name [] m) + SMap.empty + ["i0"; "i1"]) + +(* FIXME: Is this the best way to do this? Referencing such a definition + * in Typer will be a pain because it would depend on the location + * in the context. + *) +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 xv = (dsinfo, Some "x") in - mkBuiltin ((dloc, "Eq.refl"), - mkArrow (dsinfo, Aerasable, lv, - type_level, - mkArrow (dsinfo, Aerasable, tv, - mkSort (dsinfo, Stype (mkVar (lv, 0))), - mkArrow (dsinfo, Aerasable, xv, - mkVar (tv, 0), - mkCall (dsinfo, type_eq, - [Aerasable, mkVar (lv, 2); - Aerasable, mkVar (tv, 1); - Anormal, mkVar (xv, 0); - Anormal, mkVar (xv, 0)]))))) - + 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) ===================================== src/env.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018, 2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -31,12 +31,14 @@ * --------------------------------------------------------------------------- *) open Elexp +open Lexp open Fmt (* make_title, table util *) open Printf open Sexp module M = Myers module DB = Debruijn +module OL = Opslexp let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ENV" ?print_action ?loc fmt @@ -163,7 +165,35 @@ let rec value_string v = (fun str v -> (str^(value_string v)^";")) "" a) in ("["^(String.sub str 0 ((String.length str) - 1))^"]") ) -let value_print (vtp: value_type) = print_string (value_string vtp) +let value_string_with_type v ltype ctx = + (* Handle some special cases, and use the default + value string otherwise. *) + let rec get_string ltype ctx = + match lexp_lexp' (OL.lexp_whnf ltype ctx) with + | Arrow (_, Aerasable, _, _, ret_ltype) + (* Recurse on return type to handle chain of erasable arguments *) + -> let shifted_ret_ltype = push_susp ret_ltype (S.shift (-1)) in + sprintf "(lambda _ ≡> %s)" (get_string shifted_ret_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) + | _ -> value_string v + in get_string ltype ctx + +(* Caller may optionally provide additional type information + to allow the printer to produce a more informative output. *) +let value_print (vtp: value_type) (lexp_ctx: (lexp * DB.lexp_context) option) = + print_string (Option.fold + ~none:(value_string vtp) + ~some:(fun (ltype, ctx) -> value_string_with_type vtp ltype ctx) + lexp_ctx) let make_runtime_ctx = M.nil @@ -192,7 +222,7 @@ let print_rte_ctx_n (ctx: runtime_env) start = | (_, Some m) -> Printf.printf "%-12s | " m | _ -> print_string (make_line ' ' 12); print_string " | " in - value_print g; print_string "\n") start + value_print g None; print_string "\n") start (* Only print user defined variables *) let print_rte_ctx ctx = ===================================== src/eval.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018, 2020, 2021, 2022 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -404,7 +404,7 @@ let file_read loc _depth args_val = match args_val with * or actually pay attention to the second arg. *) | [Vin channel; Vint _n] -> Vstring (input_line channel) | _ -> error loc ~print_action:(fun _ -> - List.iter (fun v -> value_print v; print_newline ()) args_val; + List.iter (fun v -> value_print v None; print_newline ()) args_val; ) "File.read expects an in_channel. Actual arguments:" @@ -414,7 +414,7 @@ let file_write loc _depth args_val = match args_val with (* FIXME: This should be the unit value! *) Vundefined) | _ -> error loc ~print_action:(fun _ -> - List.iter (fun v -> value_print v; print_newline ()) args_val; + List.iter (fun v -> value_print v None; print_newline ()) args_val; ) "File.write expects an out_channel and a string. Actual arguments:" @@ -654,9 +654,9 @@ and sexp_dispatch loc depth args = eval_call blk [Vsexp b] (* -------------------------------------------------------------------------- *) -and print_eval_result i lxp = +and print_eval_result i lxp ltype = Printf.printf " Out[%02d] >> " i; - value_print lxp; + value_print lxp ltype; print_string "\n"; and print_typer_trace' trace = @@ -765,6 +765,11 @@ let y_operator loc _depth args = | _ -> error loc ("Y expects 1 (function) argument") let arity0_fun loc _ _ = error loc "Called a 0-arity function!?" + +let eq_uneq loc _ vs = match vs with + | [x; _y] -> x + | _ -> error loc "Eq_uneq takes 2 arguments" + let nop_fun loc _ vs = match vs with | [v] -> v | _ -> error loc "Wrong number of argument to nop" @@ -1050,8 +1055,9 @@ let register_builtin_functions () = ("File.open" , file_open, 2); ("File.read" , file_read, 2); ("File.write" , file_write, 2); - ("Eq.refl" , arity0_fun, 0); ("Eq.cast" , nop_fun, 1); + ("Eq.eq" , arity0_fun, 0); + ("Eq.uneq" , eq_uneq, 2); ("Y" , y_operator, 1); ("Ref.make" , ref_make, 1); ("Ref.read" , ref_read, 1); @@ -1083,8 +1089,7 @@ let _ = register_builtin_functions () let builtin_constant v loc _depth args_val = match args_val with (* FIXME: Dummy arg because we currently can't define a Builtin - * *constant* (except for cases like Eq.refl where the contant is not - * actually used). *) + * *constant*. *) | [_] -> v | _ -> error loc "Builtin almost-constant takes a unit argument" ===================================== src/opslexp.ml ===================================== @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps -Copyright (C) 2011-2022 Free Software Foundation, Inc. +Copyright (C) 2011-2023 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -63,7 +63,8 @@ module LMap let reducible_builtins = ref (SMap.empty : (DB.lexp_context -> (P.arg_kind * lexp) list (* The builtin's args *) - -> lexp option) SMap.t) + (* The reduction result and the remaining args *) + -> (lexp * (P.arg_kind * lexp) list) option) SMap.t) let log_tc_error ?print_action ?loc fmt = Log.log_error ~section:"TC" ?print_action ?loc fmt @@ -190,23 +191,18 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = lexp_whnf (mkCall (l, push_susp body (S.substitute (lexp_whnf arg ctx)), args)) ctx - | Call (l, f', xs1) -> mkCall (l, f', List.append xs1 xs) + | Call (l, f', xs1) -> lexp_whnf (mkCall (l, f', List.append xs1 xs)) ctx | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with - | Some f -> Option.value ~default:e (f ctx args) + | Some f -> Option.value ~default:e + (Option.map + (fun (e, args) -> + lexp_whnf (mkCall (l, e, args)) ctx) + (f ctx xs)) | None -> e) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> let e' = lexp_whnf e ctx in - let get_refl e = - 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 - mkCall (l, DB.eq_refl, - [Pexp.Aerasable, elevel; - Pexp.Aerasable, etype; - Pexp.Aerasable, e]) in let reduce it name aargs = let targs = match lexp'_whnf it ctx with | Inductive (_,_,fargs,_) -> fargs @@ -224,13 +220,13 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = (S.identity, targs) aargs in (* Substitute case Eq variable by the proof (Eq.refl l t e') *) - let subst = S.cons (get_refl e') subst in + let subst = S.cons (mk_eq_witness l e' ctx) subst in lexp_whnf (push_susp branch subst) ctx with | Not_found -> match default with | Some (_v,default) - -> let subst = S.cons (get_refl e') (S.substitute e') in + -> let subst = S.cons (mk_eq_witness l e' ctx) (S.substitute e') in lexp_whnf (push_susp default subst) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:(Sexp.location l) @@ -289,18 +285,29 @@ and lexp'_whnf e (ctx : DB.lexp_context) : lexp' = and eq_cast_whnf ctx args = match args with - | [_l; _t; _x; _y; (_, p); _f; (_, fx)] + | _l1 :: _l2 :: _t :: _x :: _y :: (_, p) :: _f :: (_, fx) :: rest -> (match lexp'_whnf p ctx with - | Call (_, refl, _) when conv_p ctx refl DB.eq_refl - -> Some (lexp_whnf fx ctx) + | Call (_, eq, _) when conv_p ctx eq DB.eq_eq + -> Some (fx, rest) | _ -> None) | _ -> None +and eq_uneq_whnf ctx args = + match args with + | _l :: _t :: (_, x) :: (_, y) :: _p :: (_, i) :: rest + -> if conv_p ctx i DB.interval_i0 + then Some (x, rest) + else if conv_p ctx i DB.interval_i1 + then Some (y, rest) + else 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.cast", eq_cast_whnf); + ("Eq.uneq", eq_uneq_whnf) ] !reducible_builtins (** A very naive implementation of sets of pairs of lexps. *) @@ -518,12 +525,29 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (* FIXME Should we use conversion on the terms of the substitution instead of syntactic equality? *) subst_eq s1 s2 + | (Lambda (a, l, t, _) as e', e'') | (e'', (Lambda (a, l, t, _) as e')) + (* Eta expansion of functions *) + -> let expansion = mkLambda (a, l, t, + mkCall (dsinfo, push_susp (hc e'') (S.shift 1), + [(a, mkVar ((dsinfo, None), 0))])) in + conv_p' ctx vs (hc e') expansion | (_, _) -> false and conv_p (ctx : DB.lexp_context) e1 e2 = if e1 == e2 then true 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 elevel = match lexp'_whnf (get_type ctx etype) ctx with + | Sort (_, Stype l) -> l + | _ -> Log.internal_error "" in + let fn = mkLambda (Pexp.Aerasable, (sinfo, None), etype, e) in + mkCall (sinfo, DB.eq_eq, + [Pexp.Aerasable, elevel; + Pexp.Aerasable, etype; + Pexp.Anormal, fn]) + (********* Testing if a lexp is properly typed *********) and mkSLlub ctx e1 e2 = ===================================== src/unification.ml ===================================== @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms -Copyright (C) 2016-2022 Free Software Foundation, Inc. +Copyright (C) 2016-2023 Free Software Foundation, Inc. Author: Vincent Bonnevalle <tiv.crb(a)gmail.com> @@ -248,7 +248,14 @@ and unify' (e1: lexp) (e2: lexp) be substituted with further reduction; 2. Calls, because they might become redexes; 3. Case expressions, for the same reason. *) + + (* FIXME: Does the order of these branches matter? If we can place + the Lambda branches above the Var branches, we can avoid + having to explicitly name the Lambda * Var pair for the + η expansion of Lambdas. *) + | (Lambda _, Var _) -> unify_lambda msl e1' e2' ctx vs' | (_, Var _) -> unify_var e2' e1' ctx + | (Var _, Lambda _) -> unify_lambda msl e2' e1' ctx vs' | (Var _, _) -> unify_var e1' e2' ctx | (_, Call _) -> unify_call msl e2' e1' ctx vs' | (Call _, _) -> unify_call msl e1' e2' ctx vs' @@ -298,7 +305,8 @@ and unify_arrow (matching : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs (** Unify a Lambda and a lexp if possible - Lambda , Lambda -> if var_kind = var_kind then UNIFY ltype & lxp else ERROR - - Lambda , _ -> Impossible + - Lambda , e -> UNIFY lambda with η expansion of e + - else -> Impossible *) and unify_lambda (matching : scope_level option) (lambda: lexp) (lxp: lexp) ctx vs = @@ -311,6 +319,12 @@ and unify_lambda (matching : scope_level option) (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs) matching) else [(CKimpossible, ctx, lambda, lxp)] + | (Lambda (arg_kind, arg, ltype, _), e) -> + (* η expansion of Lambda *) + let expansion = mkLambda (arg_kind, arg, ltype, + mkCall (dsinfo, push_susp (hc e) (S.shift 1), + [(arg_kind, mkVar ((dsinfo, None), 0))])) in + unify_lambda matching lambda expansion ctx vs | (_, _) -> [(CKimpossible, ctx, lambda, lxp)] (** Unify a Metavar and a lexp if possible ===================================== tests/elab_test.ml ===================================== @@ -1,6 +1,6 @@ (* elab_test.ml --- * - * Copyright (C) 2016-2017 Free Software Foundation, Inc. + * Copyright (C) 2016-2023 Free Software Foundation, Inc. * * Author: Vincent Bonnevalle <tiv.crb(a)gmail.com> * @@ -255,7 +255,20 @@ let _ = add_elab_test_decl "Check and instantiate implicit args when a type is given" {| test : Int -> ?a -> ?a; -test _ = I; +test _ = id; |} +let _ = add_elab_test_decl + "η expansion for Lambdas" + {| +succ : Int -> Int; +succ i = i + 1; + +p1 : Eq succ (lambda i -> succ i); +p1 = Eq_refl; + +p2 : Eq (lambda i -> succ i) succ; +p2 = Eq_refl; + |} + let _ = run_all () ===================================== tests/env_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -67,6 +67,26 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> print_rte_ctx rctx); success)) +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)), + "(lambda _ ≡> 42)"); + ((Vbuiltin "Eq.eq"), + (mkCall (dsinfo, DB.type_eq, + [Aerasable, mkVar ((dsinfo, None), 2); + Aerasable, DB.type_int; + Anormal, mkVar ((dsinfo, Some "x"), 0); + Anormal, mkVar ((dsinfo, Some "y"), 0)])), + "x = y [ ##Int ]")] in + (* This test assumes that success = 0 and failure = -1 *) + List.fold_left + (fun res (v, ltype, expected) + -> Int.min res + (expect_equal_str (value_string_with_type v ltype DB.empty_lctx) + expected)) + 0 exps)) (* run all tests *) let _ = run_all () ===================================== tests/eval_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -31,7 +31,6 @@ open Utest_lib open Eval (* reset_eval_trace *) -open Builtin open Env (* default environment *) @@ -510,7 +509,7 @@ let _ = test_eval_eqv_named implicitly = ?; Eq_unerase = - lambda x y (p : Eq x y) ≡> + lambda x y => lambda (p : Eq x y) ≡> Eq_cast (p := p) (f := Eq x) Eq_refl; exfalso (f : False) = ##case_ f; Not p = (contra : p) ≡> False; View it on GitLab: https://gitlab.com/monnier/typer/-/compare/9bdaed9bd6e4c0c74646fd75e28d1a7b… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/9bdaed9bd6e4c0c74646fd75e28d1a7b… You're receiving this email because of your account on gitlab.com.

1 0

Re: [Typer] pp_print
by Stefan Monnier 14 Jul '23

14 Jul '23

> Dans cette branche, j'escape les symboles et les noms de variable. > > https://gitlab.com/monnier/typer/-/compare/main...simon--escape-symbols > > Dites-moi si ça vous convient. LGTM, please push. sauf: c <> ' ' devrait être c > ' ' vu que Typer considère tous les charactères <= 32 comme du whitespace. Stefan

1 1