Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
  • SimonJ
  • add-proj
  • alice
  • case-unification
  • compiler-phase-simpl
  • dev/characterization
  • diagnostics_and_hover
  • feedback/graveline
  • gambit-compile-pervasives
  • gensym-without-spaces
  • instance-args
  • ja--elab-flamecharts
  • ja-barszcz
  • ja-perf
  • ja-refl
  • laurent/elab_cache
  • location-sinfo
  • main
  • master
  • misc-bugfixes
  • ocaml-toplevel
  • open-module
  • quot-types/normalisation
  • quot-types/rational
  • report/hmdup
  • report/itd
  • report/jfla-2019
  • report/ml-2017
  • report/tcvi
  • report/vincent-bonnevalle
  • residue-fix
  • residues-elab
  • sexp-case
  • simon--logging-overhaul
  • simon--pp-print-lctx
  • simon--pp-print-value
  • simon--remove-heap
  • simon--trace-evaluation-through-logging
  • there-can-be-only-one-inductive
  • tp/ift6172
  • trace-vs-diagnose
  • track-sexp-lexp
  • typer-lsp-server
43 results

Target

Select target project
  • monnier/typer
  • league/typer
  • jamestjw/typer
  • rdivyanshu/typer
  • jabarszcz/typer
  • JasonHuZS/typer
  • npereira97/typer
  • hannelita/typer
  • khaledPac/typer
  • shonfeder/typer
10 results
Select Git revision
  • SimonJ
  • add-proj
  • alice
  • case-unification
  • compiler-phase-simpl
  • dev/characterization
  • diagnostics_and_hover
  • feedback/graveline
  • gambit-compile-pervasives
  • gensym-without-spaces
  • instance-args
  • ja--elab-flamecharts
  • ja-barszcz
  • ja-perf
  • ja-refl
  • laurent/elab_cache
  • location-sinfo
  • main
  • master
  • misc-bugfixes
  • ocaml-toplevel
  • open-module
  • quot-types/normalisation
  • quot-types/rational
  • report/hmdup
  • report/itd
  • report/jfla-2019
  • report/ml-2017
  • report/tcvi
  • report/vincent-bonnevalle
  • residue-fix
  • residues-elab
  • sexp-case
  • simon--logging-overhaul
  • simon--pp-print-lctx
  • simon--pp-print-value
  • simon--remove-heap
  • simon--trace-evaluation-through-logging
  • there-can-be-only-one-inductive
  • tp/ift6172
  • trace-vs-diagnose
  • track-sexp-lexp
  • typer-lsp-server
43 results
Show changes
Commits on Source (22)
Show whitespace changes
Inline Side-by-side
Showing
with 1310 additions and 83 deletions
btl/builtins.typer
View file @ 53990bc7
......@@ -49,36 +49,99 @@ Void = typecons Void;
i0 = datacons I i0;
i1 = datacons I i1;
%% Operations on the Interval are built-ins in order to enforce some
%% definitional equalities.
I_not : I -> I;
I_not i = case i
| i0 => i1
| i1 => i0;
I_not = Built-in "I.not";
I_meet : I -> I -> I;
I_meet = Built-in "I.meet";
%% Inspired by Cubical Agda, with the difference that we
%% return A r
%% The Cubical Agda definition:
%% transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1
%% This way, we avoid the peculiarity of having to have
%% side conditions on `A` based on the value of `r`.
I_transp : (A : I ≡> Type_ ?) ≡> (r : I) ≡>
A (_ := i0) -> A (_ := I_not r);
I_transp = Built-in "I.transp";
%% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l
%% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l
%% Heq : (l : TypeLevel) ≡> (t1 : Type_ l) ≡> (t2 : Type_ l)
%% ≡> t1 -> t2 -> Type_ l
Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l;
Eq = lambda _ ≡> lambda _ ≡> lambda x -> lambda y ->
Heq x y;
Heq_eq : (l : TypeLevel) ≡> (t : I ≡> Type_ l) ≡> (f : (i : I) ≡> t (_ := i))
≡> Heq (f (_ := i0)) (f (_ := i1));
Heq_eq = Built-in "Heq.eq";
Eq_eq : (l : TypeLevel) ≡> (t : Type_ l)
≡> (f : I ≡> t)
≡> Eq (f (_ := i0)) (f (_ := i1));
Eq_eq = Built-in "Eq.eq";
≡> Eq (t := t) (f (_ := i0)) (f (_ := i1));
Eq_eq = lambda _ ≡> lambda t ≡> lambda f ≡>
Heq_eq (t := lambda _ ≡> t) (f := f);
Heq_uneq : (l : TypeLevel) ≡> (t : I ≡> Type_ l)
≡> (x : t (_ := i0)) => (y : t (_ := i1))
=> (p : Heq x y) ≡> (i : I) ≡> t (_ := i);
Heq_uneq = Built-in "Heq.uneq";
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_uneq = lambda _ ≡> lambda t ≡>
lambda _ => lambda _ =>
lambda p ≡> lambda i ≡>
Heq_uneq (t := lambda _ ≡> t) (p := p) (i := i);
Heq_refl : (A : ?) ≡> (B : A -> ?)
≡> (x : A) ≡> (y : B x) ≡> Heq y y;
Heq_refl = lambda _ ≡> lambda _ ≡> lambda A ≡> lambda B ≡>
lambda x ≡> lambda y ≡>
Heq_eq
(t := lambda _ ≡> B x)
(f := lambda _ ≡> y);
Eq_refl : (l : TypeLevel) ≡> (t : Type_ l)
≡> (x : t) ≡> Eq x x;
Eq_refl = lambda _ ≡> lambda _ ≡> lambda x
≡> Eq_eq (f := lambda _ ≡> x);
Eq_refl = lambda _ ≡> lambda _ ≡> lambda x ≡>
Eq_eq (f := lambda _ ≡> x);
%% Note: This works too, but we use the simpler
%% definition.
%% Eq_refl = lambda _ ≡> lambda t ≡> lambda x ≡>
%% Heq_refl
%% (A := t)
%% (B := lambda _ -> t)
%% (x := x) (y := x);
%% FIXME: Hmm the type of `f` implies that `x` and `y` are of the same type,
%% contrary to what is suggested by `Heq`. This implies that it is sufficient
%% to define Eq_cast
%% Heq_cast : (x : ?) ≡> (y : ?)
%% ≡> (p : Heq x y)
%% ≡> (f : I ≡> ? -> ?)
%% ≡> f (_ := i0) x -> f (_ := i1) y;
%% Heq_cast = Built-in "Heq.cast";
Eq_cast : (x : ?) ≡> (y : ?)
≡> (p : Eq x y)
≡> (f : ? -> ?)
≡> f x -> f y;
%% FIXME: I'd like to just say:
%% Eq_cast : Eq ?x ?y ≡> ?f ?x -> ?f ?y;
Eq_cast = Built-in "Eq.cast";
Eq_cast : (x : ?) ≡> (y : ?) ≡> (p : Eq x y) ≡> (f : ? -> ?)
≡> f x -> f y;
Eq_cast = lambda _ ≡> lambda _ ≡> %% Two level variables
lambda A ≡> %% Type of x and y
lambda x ≡> lambda y ≡>
lambda p ≡> lambda f ≡>
lambda fx ->
I_transp (A := lambda i ≡> f (Heq_uneq
(t := lambda _ ≡> A)
(p := p) (i := i)))
(r := i0) fx;
%% Commutativity of equality!
%% FIXME: I'd like to just say:
......@@ -92,6 +155,12 @@ Eq_comm p = Eq_eq (f := lambda i ≡> Eq_uneq (p := p) (i := I_not i));
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;
Eq_cong : (x : ?A) => (y : ?A) =>
(f : ?A -> ?) -> (p : Eq x y)
-> Eq (f x) (f y);
Eq_cong = lambda f -> lambda p ->
Eq_eq (f := lambda i ≡> f (Eq_uneq (p := p) (i := i)));
%% General recursion!!
%% Whether this breaks consistency or not is a good question.
%% The basic idea is the following:
......@@ -531,4 +600,125 @@ 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";
%%%% Integer axioms
Integer_1≠0 = Built-in "Integer.1!=0" : Eq (t := Integer) 1 0 -> Void;
Integer_+-comm : (x : Integer) -> (y : Integer) -> Eq (Integer_+ x y) (Integer_+ y x);
Integer_+-comm = Built-in "Integer.+-comm";
Integer_*-comm : (x : Integer) -> (y : Integer) -> Eq (Integer_* x y) (Integer_* y x);
Integer_*-comm = Built-in "Integer.*-comm";
Integer_*-assoc : (x : Integer) -> (y : Integer) -> (z : Integer) ->
Eq (Integer_* x (Integer_* y z)) (Integer_* (Integer_* x y) z);
Integer_*-assoc = Built-in "Integer.*-assoc";
%%
%% (x + y) · z ≡ x · z + y · z
%%
Integer_*DistL+ : (x : Integer) -> (y : Integer) -> (z : Integer) ->
Eq (Integer_* (Integer_+ x y) z)
(Integer_+ (Integer_* x z) (Integer_* y z));
Integer_*DistL+ = Built-in "Integer.*DistL+";
%%
%% x · y ≡ 0 → ¬ x ≡ 0 → y ≡ 0
%%
Integer_isIntegral : (x : Integer) -> (y : Integer) -> Eq (Integer_* x y) 0 ->
(Eq x 0 -> Void) -> Eq y 0;
Integer_isIntegral = Built-in "Integer.isIntegral";
%%%% Integer theorems
%%
%% Zero-product property of integers
%% (¬ x ≡ 0) → (¬ y ≡ 0) -> (¬ x · y ≡ 0)
%%
Integer_0-product : (x : Integer) -> (y : Integer) -> (Eq x 0 -> Void) ->
(Eq y 0 -> Void) -> (Eq (Integer_* x y) 0 -> Void);
Integer_0-product = lambda x -> lambda y ->
lambda x≠0 -> lambda y≠0 -> lambda xy≠0 ->
y≠0 (Integer_isIntegral x y xy≠0 x≠0);
%%
%% x · (y + z) ≡ x · y + x · z
%%
%% FIXME: It'd be much better to have some sort of operator to facilitate the
%% concatenation of equality proofs.
%% Also, the last 2 commutativity proofs could be combined if we had cong₂,
%% whose definition requires dependent paths.
Integer_*DistR+ : (x : Integer) -> (y : Integer) -> (z : Integer) ->
Eq (Integer_* x (Integer_+ y z))
(Integer_+ (Integer_* x y) (Integer_* x z));
Integer_*DistR+ = lambda x -> lambda y -> lambda z ->
Eq_trans (Integer_*-comm x (Integer_+ y z))
(Eq_trans (Integer_*DistL+ y z x)
(Eq_trans (Eq_cong (lambda e -> Integer_+ e (Integer_* z x))
(Integer_*-comm y x))
(Eq_cong (lambda e -> Integer_+ (Integer_* x y) e)
(Integer_*-comm z x))));
%%
%% 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_rec : (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 : (A : ?) ≡> (R : A -> A -> ?) ≡>
(P : Quotient A R -> ?) ≡>
(f : (a : A) -> (P (Quotient_in a))) ->
(p : (a : A) -> (a' : A) -> R a a' -> Heq (f a) (f a')) ≡>
(q : Quotient A R) -> P q;
Quotient_elim = Built-in "Quotient.elim";
%% FIXME: If we eta expand this, i.e. if we write
%% ... lambda q -> Quotient_elim ... f (p := p) q
%% We get a Debruijn index error in while defining `rec2` in `quotient_lib.typer`,
%% this shouldn't happen and should be further investigated!
Quotient_rec : (A : ?) ≡> (B : ?) ≡>
(R : A -> A -> ?) ≡>
(f : A -> B) ->
(p : (a : A) -> (a' : A) -> R a a' -> Eq (f a) (f a')) ≡>
(q : Quotient A R) ->
B;
Quotient_rec = lambda _ ≡> lambda _ ≡> lambda _ ≡>
lambda A ≡> lambda B ≡> lambda R ≡>
lambda f -> lambda p ≡>
Quotient_elim (R := R) (P := lambda _ -> B) f (p := p);
%% FIXME: This axiom is necessary if we want to eliminate 2 quotiented
%% expressions to produce another quotiented expression. For now, the
%% 'prop'-ness of `Quotient_eq` isn't verified during `Quotient` elimination,
%% because
%% 1. it makes `Quotient` elimination really troublesome, and
%% 2. I want to see if this changes/breaks anything.
Quotient_trunc : (A : ?) ≡> (R : A -> A -> ?) ≡>
(x : Quotient A R) ≡> (y : Quotient A R) ≡>
(p : Eq x y) -> (q : Eq x y) -> Eq p q;
Quotient_trunc = Built-in "Quotient.trunc";
%%% builtins.typer ends here.
btl/depelim.typer
View file @ 53990bc7
......@@ -76,7 +76,7 @@ case_as_return_impl args =
Sexp_node
arrow_sexp
(cons head_sexp
(cons (quote (##Eq\.cast
(cons (quote (Eq_cast
(x := uquote head_sexp)
(y := uquote target_sexp)
(p := ##DeBruijn 0)
......
btl/pervasive.typer
View file @ 53990bc7
......@@ -690,6 +690,26 @@ 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;
%%%% Equational reasoning
%% Function to do one step of equational reasoning
step-≡ : (x : ?A) -> (y : ?A) ≡> (z : ?A) ≡> Eq x y -> Eq y z -> Eq x z;
step-≡ _ p q = Eq_trans p q;
%% Function to conclude equational reasoning
qed : (x : ?A) -> Eq x x;
qed x = Eq_refl;
%% FIXME: Chosen somewhat arbitrarily for now
define-operator "==<" 45 40;
define-operator ">==" 40 42;
define-operator "∎" 43 ();
_==<_>==_ = step-≡;
_∎ = qed;
%%%% Unit tests function for doing file
%% It's hard to do a primitive which execute test file
......
btl/qcase.typer 0 → 100644
View file @ 53990bc7
%% 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_rec")
qelim_args;
in
IO_return qelim_sexp;
qcase_macro = macro qcase_impl;
btl/rational.typer 0 → 100644
View file @ 53990bc7
%%
%% Prelude
%%
quot_lib = load "samples/quotient_lib.typer";
Quotient_rec2 = quot_lib.rec2;
%% A hack to ensure that we have fully reduced expressions
ℤ𝟘 = 0 : Integer;
ℤ𝟙 = 1 : Integer;
ℤ−𝟙 = -1 : Integer;
%% This is defined to make the code in this module more readable.
%% Mirrors the precedence of the Int operators.
define-operator "ℤ+" 111 130;
define-operator "ℤ*" 142 155;
_ℤ+_ = Integer_+;
_ℤ*_ = Integer_*;
%%
%% Prelude END
%%
%% Type that will serve as the underlying type
%% of the Rational quotient
type ℤ×ℤ≠𝟘
| inR (z1 : Integer) (z2 : Integer) (Not (Eq z2 ℤ𝟘));
fst : ℤ×ℤ≠𝟘 -> Integer;
fst z
| inR z1 _ _ => z1;
snd : ℤ×ℤ≠𝟘 -> Integer;
snd z
| inR _ z2 _ => z2;
not_zero_proof : (z : ℤ×ℤ≠𝟘) -> Not (Eq (snd z) ℤ𝟘);
not_zero_proof z =
case z return (Not (Eq (snd z) ℤ𝟘))
| inR z1 z2 p => p;
%% Use functions to access individual components of the inductive type
%% to get better definitional equivalences.
equalℚ : ℤ×ℤ≠𝟘 -> ℤ×ℤ≠𝟘 -> Type_ ?;
equalℚ z1 z2 = Eq ((fst z1) ℤ* (snd z2)) ((snd z1) ℤ* (fst z2));
Rational : Type;
Rational = Quotient ℤ×ℤ≠𝟘 equalℚ;
Rational_isSet : (x : Rational) -> (y : Rational) -> (p : Eq x y) -> (q : Eq x y)
-> Eq p q;
Rational_isSet x y p q = Quotient_trunc (R := equalℚ) p q;
%% To construct an element of this quotient, we need to prove that some Integer != 0
%% We could add the following axioms
%%
%% Integer_1!=0 : Eq (t := Integer) 1 0 -> False;
%% Integer_-1!=0 : Eq (t := Integer) -1 0 -> False;
%% Integer_succ!=0 : (x : Integer) -> Not (Eq x 0) -> Not (Eq (Integer_+ x 1) 0);
%% Integer_pred!=0 : (x : Integer) -> Not (Eq x 0) -> Not (Eq (Integer_- x 1) 0);
%% While we are at it, these axioms seems good to have
%% Integer_x-1=x+-1 : (x : Integer) -> Eq (Integer_- x 1) (Integer_+ x -1);
%% Integer_x+1=x--1 : (x : Integer) -> Eq (Integer_+ x 1) (Integer_- x -1);
Rational_1 : Rational;
Rational_1 =
%% FIXME: Small hack to make it work, if we put
%% the literal `1` as the second arg, this doesn't
%% type check
Quotient_in (inR ℤ𝟙 ℤ𝟙 Integer_1≠0);
Rational_negate : Rational -> Rational;
Rational_negate x =
let
negate_fst : ℤ×ℤ≠𝟘 -> ℤ×ℤ≠𝟘;
negate_fst x = inR (ℤ−𝟙 ℤ* (fst x)) (snd x) (not_zero_proof x);
negate_compat : (a : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) ->
equalℚ a b -> equalℚ (negate_fst a) (negate_fst b);
negate_compat a b r =
(ℤ−𝟙 ℤ* (fst a)) ℤ* (snd b)
==< Eq_comm (Integer_*-assoc ℤ−𝟙 (fst a) (snd b)) >==
ℤ−𝟙 ℤ* ((fst a) ℤ* (snd b))
==< Eq_cong (lambda e -> ℤ−𝟙 ℤ* e) r >==
ℤ−𝟙 ℤ* ((snd a) ℤ* (fst b))
==< Integer_*-assoc ℤ−𝟙 (snd a) (fst b) >==
(ℤ−𝟙 ℤ* (snd a)) ℤ* (fst b)
==< Eq_cong (lambda e -> e ℤ* (fst b))
(Integer_*-comm ℤ−𝟙 (snd a)) >==
((snd a) ℤ* ℤ−𝟙) ℤ* (fst b)
==< Eq_comm (Integer_*-assoc (snd a) ℤ−𝟙 (fst b)) >==
(snd a) ℤ* (ℤ−𝟙 ℤ* (fst b)) ∎;
in
qcase (x : ℤ×ℤ≠𝟘 / equalℚ)
| Quotient_in a => Quotient_in (R := equalℚ) (negate_fst a)
| Quotient_eq a a' r => Quotient_eq (R := equalℚ)
(a := negate_fst a)
(a' := negate_fst a')
(negate_compat a a' r);
ℤ×ℤ+ : ℤ×ℤ≠𝟘 -> ℤ×ℤ≠𝟘 -> Rational;
ℤ×ℤ+ a b =
let
x1 = fst a; y1 = snd a; p1 = not_zero_proof a;
x2 = fst b; y2 = snd b; p2 = not_zero_proof b;
in
Quotient_in (inR ((x1 ℤ* y2) ℤ+ (x2 ℤ* y1))
(y1 ℤ* y2)
(Integer_0-product y1 y2 p1 p2));
ℤ×ℤ+-Comm : (a : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) -> Eq (ℤ×ℤ+ a b) (ℤ×ℤ+ b a);
ℤ×ℤ+-Comm a b =
let
x1 = fst a; y1 = snd a; p1 = not_zero_proof a;
x2 = fst b; y2 = snd b; p2 = not_zero_proof b;
compat =
(x1 ℤ* y2 ℤ+ x2 ℤ* y1) ℤ* (y2 ℤ* y1)
==< Eq_cong (lambda e -> (x1 ℤ* y2 ℤ+ x2 ℤ* y1) ℤ* e)
(Integer_*-comm y2 y1) >==
(x1 ℤ* y2 ℤ+ x2 ℤ* y1) ℤ* (y1 ℤ* y2)
==< Integer_*-comm (x1 ℤ* y2 ℤ+ x2 ℤ* y1) (y1 ℤ* y2) >==
y1 ℤ* y2 ℤ* (x1 ℤ* y2 ℤ+ x2 ℤ* y1)
==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* e)
(Integer_+-comm (x1 ℤ* y2) (x2 ℤ* y1)) >==
y1 ℤ* y2 ℤ* (x2 ℤ* y1 ℤ+ x1 ℤ* y2) ∎;
in
Quotient_eq (R := equalℚ)
(a := inR (x1 ℤ* y2 ℤ+ x2 ℤ* y1)
(y1 ℤ* y2)
(Integer_0-product y1 y2 p1 p2))
(a' := inR (x2 ℤ* y1 ℤ+ x1 ℤ* y2)
(y2 ℤ* y1)
(Integer_0-product y2 y1 p2 p1))
compat;
%% FIXME: This proof begs to be simplified
ℚ+_feql : (a : ℤ×ℤ≠𝟘) -> (a' : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) -> equalℚ a a'
-> Eq (ℤ×ℤ+ a b) (ℤ×ℤ+ a' b);
ℚ+_feql a a' b p =
let
x1 = fst a ; y1 = snd a ; p1 = not_zero_proof a;
x1' = fst a'; y1' = snd a'; p1' = not_zero_proof a';
x2 = fst b ; y2 = snd b ; p2 = not_zero_proof b;
compat =
(x1 ℤ* y2 ℤ+ x2 ℤ* y1) ℤ* (y1' ℤ* y2)
==< Integer_*DistL+ (x1 ℤ* y2) (x2 ℤ* y1) (y1' ℤ* y2) >==
(x1 ℤ* y2) ℤ* (y1' ℤ* y2) ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)
==< Eq_cong (lambda e -> e ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2))
(Integer_*-assoc (x1 ℤ* y2) y1' y2) >==
(x1 ℤ* y2) ℤ* y1' ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)
==< Eq_cong (lambda e -> e ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2))
(Eq_trans (Eq_comm (Integer_*-assoc x1 y2 y1'))
(Eq_trans (Eq_cong (lambda e -> x1 ℤ* e)
(Integer_*-comm y2 y1'))
(Integer_*-assoc x1 y1' y2))) >==
x1 ℤ* y1' ℤ* y2 ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)
==< Eq_cong (lambda e ->
e ℤ* y2 ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2))
p >==
y1 ℤ* x1' ℤ* y2 ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)
==< Eq_cong (lambda e -> e ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2))
(Eq_comm (Integer_*-assoc y1 x1' y2)) >==
y1 ℤ* (x1' ℤ* y2)ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)
==< Eq_cong (lambda e -> y1 ℤ* e ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2))
(Integer_*-comm x1' y2) >==
y1 ℤ* (y2 ℤ* x1') ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2)
==< Eq_cong (lambda e -> e ℤ* y2 ℤ+ (x2 ℤ* y1) ℤ* (y1' ℤ* y2))
(Integer_*-assoc y1 y2 x1') >==
y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ x2 ℤ* y1 ℤ* (y1' ℤ* y2)
==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ e ℤ* (y1' ℤ* y2))
(Integer_*-comm x2 y1) >==
y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* x2 ℤ* (y1' ℤ* y2)
==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* x2 ℤ* e)
(Integer_*-comm y1' y2) >==
y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* x2 ℤ* (y2 ℤ* y1')
==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ e)
(Integer_*-assoc (y1 ℤ* x2) y2 y1') >==
y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* x2 ℤ* y2 ℤ* y1'
==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ e ℤ* y1')
(Eq_comm (Integer_*-assoc y1 x2 y2)) >==
y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* (x2 ℤ* y2) ℤ* y1'
==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* e ℤ* y1')
(Integer_*-comm x2 y2) >==
y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* (y2 ℤ* x2) ℤ* y1'
==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ e ℤ* y1')
(Integer_*-assoc y1 y2 x2) >==
y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* y2 ℤ* x2 ℤ* y1'
==< Eq_cong (lambda e -> y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ e)
(Eq_comm (Integer_*-assoc (y1 ℤ* y2) x2 y1')) >==
y1 ℤ* y2 ℤ* x1' ℤ* y2 ℤ+ y1 ℤ* y2 ℤ* (x2 ℤ* y1')
==< Eq_cong (lambda e -> e ℤ+ y1 ℤ* y2 ℤ* (x2 ℤ* y1'))
(Eq_comm (Integer_*-assoc (y1 ℤ* y2) x1' y2)) >==
y1 ℤ* y2 ℤ* (x1' ℤ* y2) ℤ+ y1 ℤ* y2 ℤ* (x2 ℤ* y1')
==< Eq_comm (Integer_*DistR+ (y1 ℤ* y2) (x1' ℤ* y2) (x2 ℤ* y1')) >==
y1 ℤ* y2 ℤ* (x1' ℤ* y2 ℤ+ x2 ℤ* y1') ∎;
in
Quotient_eq (R := equalℚ)
(a := inR (x1 ℤ* y2 ℤ+ x2 ℤ* y1)
(y1 ℤ* y2)
(Integer_0-product y1 y2 p1 p2))
(a' := inR (x1' ℤ* y2 ℤ+ x2 ℤ* y1')
(y1' ℤ* y2)
(Integer_0-product y1' y2 p1' p2))
compat;
ℚ+_feqr : (a : ℤ×ℤ≠𝟘) -> (b : ℤ×ℤ≠𝟘) -> (b' : ℤ×ℤ≠𝟘) -> equalℚ b b'
-> Eq (ℤ×ℤ+ a b) (ℤ×ℤ+ a b');
ℚ+_feqr a b b' p = Eq_trans (ℤ×ℤ+-Comm a b)
(Eq_trans (ℚ+_feql b b' a p) (ℤ×ℤ+-Comm b' a));
Rational_+ : Rational -> Rational -> Rational;
Rational_+ a b =
Quotient_rec2 (R := equalℚ) (S := equalℚ)
Rational_isSet ℤ×ℤ+ ℚ+_feql ℚ+_feqr a b;
samples/equational_reasoning_test.typer 0 → 100644
View file @ 53990bc7
short : (x : ?A) -> (y : ?A) -> (p : Eq x y) -> Eq x y;
short x y p =
x ==< p >==
y ∎;
long : (x : ?A) -> (y : ?A) -> (z : ?A) -> (w : ?A) ->
(p : Eq x y) -> (q : Eq y z) -> (r : Eq z w) -> Eq x w;
long x y z w p q r =
x ==< p >==
y ==< q >==
z ==< r >==
w ∎;
samples/hott.typer
View file @ 53990bc7
......@@ -101,12 +101,6 @@ Eq_funext : (f : ? -> ?) => (g : ? -> ?) =>
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)))
......@@ -183,6 +177,11 @@ HoTT_isSet A = (x : A) -> (y : A) -> (p : Eq x y) -> (q : Eq x y) -> Eq p q;
%% encoding of classical `or` in type-theory, then it preserves `isProp`!
HoTT_isProp P = (x : P) -> (y : P) -> 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;
%% Provable without axioms:
%%
%% ¬¬¬A -> ¬A
......@@ -202,9 +201,16 @@ Weak_double_negation nnna a = nnna (lambda na -> na a);
%% Propositional truncation: ||A|| is equivalent to A but is a mere proposition.
%% One way to approximate could be:
Propositional_truncation A = (P : ?) ≡> HoTT_isProp P ≡> (A -> P) -> P;
propositional_truncation : ?A -> Propositional_truncation ?A;
propositional_truncation a f = f a;
%% FIXME: The below definition makes the importation of this module fail!
%% Field type (ℓ : ##TypeLevel
%% => (ℓ : ##TypeLevel
%% ≡> (A : (##Type_ ℓ)
%% -> (##Type_
%% (##TypeLevel.∪ (##TypeLevel.succ ℓ)
%% (##TypeLevel.∪ ℓ ℓ)))))) is not a Type! (##Type_ω)
%% Propositional_truncation A = (P : ?) ≡> HoTT_isProp P ≡> (A -> P) -> P;
%% propositional_truncation : ?A -> Propositional_truncation ?A;
%% propositional_truncation a f = f a;
......
samples/qcase_test.typer 0 → 100644
View file @ 53990bc7
%% 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 → 100644
View file @ 53990bc7
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"
ℤ = Quotient NatPair equalZ;
%%
%% Quotient.eq
%%
%% Proof that quotiented elements are equal when
%% the base elements themselves are related in
%% the underlying type.
𝟙-𝟘 : ℤ;
𝟙-𝟘 = Quotient_in (pair (succ zero) zero);
𝟚-𝟙 : ℤ;
𝟚-𝟙 = Quotient_in (pair (succ (succ zero)) (succ zero));
𝟙=𝟙 : Eq 𝟙-𝟘 𝟚-𝟙;
𝟙=𝟙 = 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 : ℤ -> Int;
Z_To_Int q = Quotient_rec (R := equalZ) NatPairToInt (p := NatPairToIntCompat) q;
neg2_Z : ℤ;
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' : ℤ -> 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'' : ℤ -> 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 ℤ ≃ Int
samples/quotient_lib.typer 0 → 100644
View file @ 53990bc7
%%%%% Prelude %%%%%%
HoTT_lib = load "samples/hott.typer";
Eq_funext = HoTT_lib.Eq_funext;
HoTT_isProp = HoTT_lib.HoTT_isProp;
HoTT_isSet = HoTT_lib.HoTT_isSet;
HoTT_isContr = HoTT_lib.HoTT_isContr;
isContr = HoTT_lib.isContr;
%%%%% Prelude END %%%%%%
%% This function constructs the lid of this square:
%%
%% x y
%% --------------
%% | |
%% | |
%% | | p
%% | |
%% | |
%% --------------
%% x l transp_x
%%
%% We first produce a path that corresponds to the base of this square (named `l`
%% in the code). Then by doing what we would normally do to 'concatenate' `l` and
%% `p`, i.e. the same way we traditionally prove transitivity, we obtain the lid
%% of this square.
toPathOver : (A : I ≡> Type_ ?) ≡> (x : A (_ := i0)) => (y : A (_ := i1)) =>
%% Proof that transporting `x` from `A i0` to `A i1`
%% is equal to `y`
Eq (Eq_cast (p := Eq_eq (f := A))
(f := id) x) y ->
Heq x y;
toPathOver = lambda _ A ≡> lambda x y => lambda p ->
%% We want a function that will return `x` when passed `i0`
%% and `y` when passed `i1`.
let
l : Heq x (Eq_cast (p := Eq_eq (f := A)) (f := id) x);
%% Making use of the funny definition of `transp`!
l = Heq_eq (t := A)
(f := lambda i ≡>
I_transp (A := (lambda j ≡> A (_ := I_meet i j)))
(r := I_not i) x);
in
Eq_cast
(x := (Eq_cast (p := Eq_eq (f := A)) (f := id) x))
(y := y)
(p := p) (f := lambda y' -> Heq x y') l;
elimProp : (A : Type_ ?) ≡>
(R : A -> A -> Type_ ?) ≡>
(P : Quotient A R -> Type_ ?) ≡>
(prop : (x : Quotient A R) -> HoTT_isProp (P x)) ->
(f : (x : A) -> P (Quotient_in x)) ->
(x : Quotient A R) -> P x;
elimProp = lambda _ _ _ A R P ≡> lambda prop f ->
Quotient_elim
(R := R) (P := P) f
(p := lambda a a' r ->
%% Want to return f a = f a'
let
a=a' : Eq (t := Quotient A R) (Quotient_in a) (Quotient_in a');
a=a' = Quotient_eq (R := R) (a := a) (a' := a') r;
fa=fa' : Heq (f a) (f a');
fa=fa' = toPathOver
(A := lambda i ≡> P (Eq_uneq (p := a=a') (i := i)))
(prop (Quotient_in a')
(Eq_cast (p := a=a') (f := P) (f a))
(f a'));
in
fa=fa');
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_rec (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_rec (R := R)
(lambda _ -> a)
(p := lambda a a' r -> Eq_refl)
x;
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_rec (R := R)
(lambda a -> lambda b ->
Quotient_rec (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;
p : (x : Quotient B S) ->
HoTT_isProp (Eq (Quotient_rec (R := S) (f a) (p := feqr a) x)
(Quotient_rec (R := S) (f a') (p := feqr a') x));
p x = C_isSet (Quotient_rec (R := S) (f a) (p := feqr a) x)
(Quotient_rec (R := S) (f a') (p := feqr a') x);
compat : (x : Quotient B S) ->
(Eq (Quotient_rec (R := S) (f a) (p := feqr a) x)
(Quotient_rec (R := S) (f a') (p := feqr a') x));
compat x = elimProp (R := S)
(P := lambda x ->
(Eq (Quotient_rec (R := S) (f a) (p := feqr a) x)
(Quotient_rec (R := S) (f a') (p := feqr a') x)))
p eqf x;
in
Eq_funext (f := Quotient_rec (R := S) (f a) (p := feqr a))
(g := Quotient_rec (R := S) (f a') (p := feqr a'))
compat);
%% Model propositional truncation using a quotient type!
%% We are essentially defining a relation where every element
%% of P is related to every other element of P.
%% FIXME: Unification errors occur when we make this universe polymorphic!?
PropTrunc : (P : Type) -> Type;
PropTrunc P = Quotient P (lambda p1 p2 -> Unit);
%% FIXME: Hmm I think we won't be able to do this unless equality
%% between `Quotient`s is a `Prop`
%% squash : (x : PropTrunc ?P) -> (y : PropTrunc ?P) -> Eq x y;
%% squash x y = ?;
%% Lemma 6.10.2 in HoTT book, to prove this we need to
%% apply propositional truncation on SurjectiveQuotientProof.
%% FIXME: Why is the unification of the levels not working?
%% type SurjectiveQuotientProof (l1 ::: TypeLevel)
%% (l2 ::: TypeLevel)
%% (A : Type_ l1) (R : A -> A -> Type_ l2)
%% (x : Quotient A R) : Type_ ?
%% | surjectiveQuotientProof (a : A) (Eq (Quotient_in (R := R) a) x);
SurjectiveQuotientProof = typecons (SurjectiveQuotientProof (l1 ::: TypeLevel)
(l2 ::: TypeLevel)
(A : Type_ l1)
(R : A -> A -> Type_ l2)
(x : Quotient A R))
(surjectiveQuotientProof (a : A) (Eq (Quotient_in (R := R) a) x));
surjectiveQuotientProof = datacons SurjectiveQuotientProof surjectiveQuotientProof;
%% FIXME: This should be made universe polymorphic, but this is contingent upon the
%% truncation type itself being polymorphic. We need to implement `squash` to complete
%% this proof.
%% Quotient_in_surjective : (A : Type) -> (R : A -> A -> Type) -> (x : Quotient A R)
%% -> PropTrunc (SurjectiveQuotientProof A R x);
%% Quotient_in_surjective = ?
%% 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_rec (R := R)
(lambda a -> Quotient_in (op a))
(p := opPreservesQuotient)
x;
src/builtin.ml
View file @ 53990bc7
......@@ -145,7 +145,7 @@ let register_builtin_csts () =
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 "Heq" DB.type_heq;
OL.add_builtin_cst "I" DB.type_interval
let _ = register_builtin_csts ()
src/debruijn.ml
View file @ 53990bc7
......@@ -130,24 +130,32 @@ let type_string = mkBuiltin ((dloc, "String"), 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 type_heq_type =
let lv = (dsinfo, Some "l") in
let tv = (dsinfo, Some "t") in
let tv1 = (dsinfo, Some "t1") in
let tv2 = (dsinfo, Some "t2") in
mkArrow (dsinfo, Aerasable, lv,
type_level,
mkArrow (dsinfo, Aerasable, tv,
mkArrow (dsinfo, Aerasable, tv1,
mkSort (dsinfo, Stype (mkVar (lv, 0))),
mkArrow (dsinfo, Aerasable, tv2,
mkSort (dsinfo, Stype (mkVar (lv, 1))),
mkArrow (dsinfo, Anormal, (dsinfo, None),
mkVar (tv, 0),
mkVar (tv1, 1),
mkArrow (dsinfo, Anormal, (dsinfo, None),
mkVar (tv, 1),
mkSort (dsinfo, Stype (mkVar (lv, 3)))))))
let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type)
mkVar (tv2, 1),
mkSort (dsinfo,
Stype (mkVar (lv, 4))))))))
let type_heq = mkBuiltin ((dloc, "Heq"), type_heq_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"]
"Heap"; "DataconsLabel";
(* Integer axioms *)
"Integer.1!=0"; "Integer.+-comm"; "Integer.*-comm"; "Integer.*-assoc";
"Integer.*DistL+"; "Integer.isIntegral"]
(* 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
View file @ 53990bc7
......@@ -868,9 +868,9 @@ and unify_or_error lctx lxp ?lxp_name expect actual =
| ((ck, _ctx, t1, t2)::_)
-> lexp_error
(Lexp.location lxp) lxp
({|Type mismatch%s! Context expected:\n%s|}
^^ {|\nbut %s has type:\n %s\n|}
^^ {|can't unify:\n %s\nwith:\n %s|})
("Type mismatch%s! Context expected:\n%s"
^^ "\nbut %s has type:\n %s\n"
^^ "can't unify:\n %s\nwith:\n %s")
(match ck with
| Unif.CKimpossible -> ""
| Unif.CKresidual -> " (residue)")
......@@ -979,8 +979,9 @@ and check_case rtype (loc, target, ppatterns) ctx =
let tlxp' = shift_to_extended_ctx nctx tlxp in
let tltp' = shift_to_extended_ctx nctx tltp in
let tlvl' = shift_to_extended_ctx nctx tlvl in
let eqty = mkCall (loc, DB.type_eq,
let eqty = mkCall (loc, DB.type_heq,
[(Aerasable, tlvl'); (* Typelevel *)
(Aerasable, tltp'); (* Inductive type *)
(Aerasable, tltp'); (* Inductive type *)
(Anormal, head_lexp); (* Lexp of the branch head *)
(Anormal, tlxp')]) (* Target lexp *)
......
src/env.ml
View file @ 53990bc7
......@@ -178,12 +178,18 @@ let value_string_with_type v ltype ctx =
let e' = OL.lexp_whnf e ctx in
(match args with
(* Pretty print identity types *)
| [_l; (_, t); (_, left); (_, right)]
when OL.conv_builtin_p ctx e' "Eq"
| [_l; (_, t); (_, _t2); (_, left); (_, right)]
when OL.conv_builtin_p ctx e' "Heq"
-> sprintf "%s = %s [ %s ]"
(* TODO: Print something different when t1 != t2? *)
(Lexp.to_string left)
(Lexp.to_string right)
(Lexp.to_string t)
| [_; _; (_, t); (_, r)]
when OL.conv_builtin_p ctx e' "Quotient"
-> sprintf "(Quotient.in %s %s)"
(Lexp.to_string t)
(Lexp.to_string r)
| _ -> value_string v)
| _ -> value_string v
in get_string ltype ctx
......
src/eval.ml
View file @ 53990bc7
......@@ -766,9 +766,9 @@ let y_operator loc _depth args =
let arity0_fun loc _ _ = error loc "Called a 0-arity function!?"
let eq_uneq loc _ vs = match vs with
let heq_uneq loc _ vs = match vs with
| [x; _y] -> x
| _ -> error loc "Eq_uneq takes 2 arguments"
| _ -> error loc "Heq_uneq takes 2 arguments"
let nop_fun loc _ vs = match vs with
| [v] -> v
......@@ -1027,6 +1027,46 @@ 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_type loc _ args =
match args with
| [_; _] -> Vundefined
| _ -> error loc "Quotient expects 2 arguments"
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 quotient_trunc loc _ args =
match args with
| [_; _] -> Vundefined
| _ -> error loc "Quotient.trunc expects 1 argument"
let interval_meet loc _ args =
match args with
| [Vcons (sym1, _) as x; Vcons (sym2, _) as y] ->
(match (Sym.name sym1, Sym.name sym2) with
| "i0", _ -> x
| "i1", _ -> y
| _ -> error loc "Unexpected arguments passed to I.meet")
| _ -> error loc "I.meet expects 2 arguments"
let interval_not loc _ args =
match args with
| [Vcons (sym, _)] ->
(match Sym.name sym with
| "i0" -> Vcons ((dloc, "i1"), [])
| "i1" -> Vcons ((dloc, "i0"), [])
| _ -> error loc "Unexpected argument passed to I.not")
| _ -> error loc "I.not expects 1 argument"
let register_builtin_functions () =
List.iter (fun (name, f, arity) -> add_builtin_function name f arity)
[
......@@ -1055,9 +1095,9 @@ let register_builtin_functions () =
("File.open" , file_open, 2);
("File.read" , file_read, 2);
("File.write" , file_write, 2);
("Eq.cast" , nop_fun, 1);
("Eq.eq" , arity0_fun, 0);
("Eq.uneq" , eq_uneq, 2);
("Heq.cast" , nop_fun, 1);
("Heq.eq" , arity0_fun, 0);
("Heq.uneq" , heq_uneq, 2);
("Y" , y_operator, 1);
("Ref.make" , ref_make, 1);
("Ref.read" , ref_read, 1);
......@@ -1084,6 +1124,14 @@ let register_builtin_functions () =
("Test.false" , test_false,2);
("Test.eq" , test_eq,3);
("Test.neq" , test_neq,3);
("Quotient" , quotient_type, 2);
("Quotient.in" , nop_fun, 1);
("Quotient.eq" , quotient_eq, 1);
("Quotient.trunc", quotient_trunc, 2);
("Quotient.elim" , quotient_elim, 2);
("I.transp" , nop_fun, 1);
("I.meet" , interval_meet, 2);
("I.not" , interval_not, 1);
]
let _ = register_builtin_functions ()
......
src/lexp.ml
View file @ 53990bc7
......@@ -347,8 +347,8 @@ let mkSLlub' (e1, e2) =
| (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l
| (SortLevel SLz, e) | (e, SortLevel SLz)
-> Log.log_fatal ~section:"internal" "lub of SLz with %S" (lexp_head (hc e))
| (SortLevel (SLsucc _), SortLevel (SLsucc _))
-> Log.log_fatal ~section:"internal" "lub of two SLsucc"
| (SortLevel (SLsucc e1), SortLevel (SLsucc e2))
-> SLsucc (mkSortLevel (SLlub (e1, e2)))
| ((SortLevel _ | Var _ | Metavar _ | Susp _),
(SortLevel _ | Var _ | Metavar _ | Susp _))
-> SLlub (e1, e2)
......
src/opslexp.ml
View file @ 53990bc7
......@@ -300,16 +300,7 @@ and conv_builtin_p ctx e name =
| 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_builtin_p ctx eq "Eq.eq"
-> Some (fx, rest)
| _ -> None)
| _ -> None
and eq_uneq_whnf ctx args =
and heq_uneq_whnf ctx args =
match args with
| _l :: _t :: (_, x) :: (_, y) :: _p :: (_, i) :: rest
-> if conv_p ctx i DB.interval_i0
......@@ -319,12 +310,72 @@ and eq_uneq_whnf ctx args =
else None
| _ -> None
and interval_transp_whnf _ctx args =
match args with
| _l :: _a :: _r :: (_, a_i0) :: rest
-> Some (a_i0, rest)
| _ -> None
and interval_meet_whnf ctx args =
match args with
| (_, x) :: (_, y) :: rest
->
(* i0 ∧ x = i0 *)
if conv_p ctx x DB.interval_i0
then Some (DB.interval_i0, rest)
(* i1 ∧ y = y *)
else if conv_p ctx x DB.interval_i1
then Some (y, rest)
(* y ∧ i0 = i0 *)
else if conv_p ctx y DB.interval_i0
then Some (DB.interval_i0, rest)
(* x ∧ i1 = x *)
else if conv_p ctx y DB.interval_i1
then Some (x, rest)
(* x ∧ x = x *)
else if conv_p ctx x y
then Some(x, rest)
else None
| _ -> None
and interval_not_whnf ctx args =
match args with
| (_, x) :: rest
->
(* ~ i0 ≡ i1 *)
if conv_p ctx x DB.interval_i0
then Some (DB.interval_i1, rest)
(* ~ i1 ≡ i0 *)
else if conv_p ctx x DB.interval_i1
then Some (DB.interval_i0, rest)
else
(* ~ (~ i) ≡ i*)
(match lexp'_whnf x ctx with
| Call (_, fn, [_, y])
when conv_builtin_p ctx fn "I.not"
-> Some (y, rest)
| _ -> None)
| _ -> None
and quotient_elim_whnf ctx args =
match args with
| _l1 :: _l2 :: _l3 :: _A :: _R :: _P :: (_, f) :: (_, _p) :: (_, q) :: rest
-> (match lexp'_whnf q ctx with
| Call (_, qin, [_; _; _; _; (_, e)])
when conv_builtin_p ctx qin "Quotient.in"
-> Some (mkCall (dsinfo, f, [Anormal, e]), rest)
| _ -> None)
| _ -> None
and register_reducible_builtins () =
reducible_builtins :=
List.fold_right
(fun (n, f) m -> SMap.add n f m) [
("Eq.cast", eq_cast_whnf);
("Eq.uneq", eq_uneq_whnf)
("Heq.uneq", heq_uneq_whnf);
("I.transp", interval_transp_whnf);
("I.meet", interval_meet_whnf);
("I.not", interval_not_whnf);
("Quotient.elim", quotient_elim_whnf)
] !reducible_builtins
(** A very naive implementation of sets of pairs of lexps. *)
......@@ -484,8 +535,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
let tlxp = mkSusp target subst in
let tltp = mkSusp etype subst in
let tlvl = mkSusp elvl subst in
let eqty = mkCall (dsinfo, DB.type_eq,
let eqty = mkCall (dsinfo, DB.type_heq,
[(Pexp.Aerasable, tlvl); (* Typelevel *)
(Pexp.Aerasable, tltp); (* Inductive type *)
(Pexp.Aerasable, tltp); (* Inductive type *)
(Pexp.Anormal, hlxp); (* Lexp of the branch head *)
(Pexp.Anormal, tlxp)]) in (* Target lexp *)
......@@ -559,11 +611,11 @@ and mk_eq_witness sinfo e ctx =
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, get_builtin "Eq.eq",
let t = mkLambda (Pexp.Aerasable, (dsinfo, None), DB.type_interval, etype) in
let fn = mkLambda (Pexp.Aerasable, (dsinfo, None), DB.type_interval, e) in
mkCall (sinfo, get_builtin "Heq.eq",
[Pexp.Aerasable, elevel;
Pexp.Aerasable, etype;
Pexp.Aerasable, t;
Pexp.Anormal, fn])
(********* Testing if a lexp is properly typed *********)
......@@ -907,8 +959,9 @@ and check'' erased ctx e =
let tlxp = mkSusp e subst in
let tltp = mkSusp etype subst in
let tlvl = mkSusp elvl subst in
let eqty = mkCall (l, DB.type_eq,
let eqty = mkCall (l, DB.type_heq,
[(Pexp.Aerasable, tlvl); (* Typelevel *)
(Pexp.Aerasable, tltp); (* Inductive type *)
(Pexp.Aerasable, tltp); (* Inductive type *)
(Pexp.Anormal, hlxp); (* Lexp of the branch head *)
(Pexp.Anormal, tlxp)]) in (* Target lexp *)
......
src/unification.ml
View file @ 53990bc7
......@@ -249,13 +249,11 @@ and unify' (e1: lexp) (e2: lexp)
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'
(* Do lambdas first in case eta expansion helps unification. *)
| (Lambda _, _) -> unify_lambda msl e1' e2' ctx vs'
| (_, Lambda _) -> unify_lambda msl e2' e1' 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'
......@@ -266,8 +264,6 @@ and unify' (e1: lexp) (e2: lexp)
constraints. *)
| (_, Arrow _) -> unify_arrow msl e2' e1' ctx vs'
| (Arrow _, _) -> unify_arrow msl e1' e2' ctx vs'
| (_, Lambda _) -> unify_lambda msl e2' e1' ctx vs'
| (Lambda _, _) -> unify_lambda msl e1' e2' ctx vs'
| (_, Sort _) -> unify_sort msl e2' e1' ctx vs'
| (Sort _, _) -> unify_sort msl e1' e2' ctx vs'
| (_, SortLevel _) -> unify_sortlvl msl e2' e1' ctx vs'
......@@ -561,6 +557,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
View file @ 53990bc7
......@@ -154,7 +154,7 @@ unify =
lambda sxps ->
do {vname <- gensym ();
IO_return
(quote ((uquote vname) : (uquote (Sexp_node (Sexp_symbol "##Eq") sxps));
(quote ((uquote vname) : (uquote (Sexp_node (Sexp_symbol "Eq") sxps));
(uquote vname) = Eq_refl;
));
});
......@@ -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"
{|
......
tests/env_test.ml
View file @ 53990bc7
......@@ -73,9 +73,10 @@ let _ = (add_test "ENV" "Value Printer" (fun () ->
(mkArrow (dsinfo, Aerasable, (dsinfo, Some "l"),
DB.type_interval, DB.type_integer)),
"(lambda _ ≡> 42)");
((Vbuiltin "Eq.eq"),
(mkCall (dsinfo, DB.type_eq,
((Vbuiltin "Heq.eq"),
(mkCall (dsinfo, DB.type_heq,
[Aerasable, mkVar ((dsinfo, None), 2);
Aerasable, DB.type_integer;
Aerasable, DB.type_integer;
Anormal, mkVar ((dsinfo, Some "x"), 0);
Anormal, mkVar ((dsinfo, Some "y"), 0)])),
......