SECTIONS WORKING!!!
This commit is contained in:
parent
640354bb45
commit
23f1432817
8 changed files with 299 additions and 296 deletions
|
|
@ -131,14 +131,6 @@ def inv_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i)
|
|||
def inv_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_r G op e a (i a) :=
|
||||
and_elim_r (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a);
|
||||
|
||||
section Groups
|
||||
variable G : *;
|
||||
variable op : binop G;
|
||||
hypothesis Hgroup : group G op e i;
|
||||
|
||||
def left_inv_unique
|
||||
end Groups
|
||||
|
||||
def left_inv_unique (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a b : G) (h : inv_l G op e a b) : eq G b (i a) :=
|
||||
-- b = b * e
|
||||
-- = b * (a * a^-1)
|
||||
|
|
|
|||
|
|
@ -115,101 +115,107 @@ def eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :
|
|||
|
||||
-- Some logic theorems
|
||||
|
||||
-- ~(A ∨ B) => ~A ∧ ~B
|
||||
def de_morgan1 (A B : *) (h : not (or A B)) : and (not A) (not B) :=
|
||||
and_intro (not A) (not B)
|
||||
(fun (a : A) => h (or_intro_l A B a))
|
||||
(fun (b : B) => h (or_intro_r A B b));
|
||||
section Theorems
|
||||
|
||||
-- ~A ∧ ~B => ~(A ∨ B)
|
||||
def de_morgan2 (A B : *) (h : and (not A) (not B)) : not (or A B) :=
|
||||
fun (contra : or A B) =>
|
||||
or_elim A B false contra
|
||||
(and_elim_l (not A) (not B) h)
|
||||
(and_elim_r (not A) (not B) h);
|
||||
variable (A B C : *);
|
||||
|
||||
-- ~A ∨ ~B => ~(A ∧ B)
|
||||
def de_morgan3 (A B : *) (h : or (not A) (not B)) : not (and A B) :=
|
||||
fun (contra : and A B) =>
|
||||
or_elim (not A) (not B) false h
|
||||
(fun (na : not A) => na (and_elim_l A B contra))
|
||||
(fun (nb : not B) => nb (and_elim_r A B contra));
|
||||
-- ~(A ∨ B) => ~A ∧ ~B
|
||||
def de_morgan1 (h : not (or A B)) : and (not A) (not B) :=
|
||||
and_intro (not A) (not B)
|
||||
(fun (a : A) => h (or_intro_l A B a))
|
||||
(fun (b : B) => h (or_intro_r A B b));
|
||||
|
||||
-- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
|
||||
-- ~A ∧ ~B => ~(A ∨ B)
|
||||
def de_morgan2 (h : and (not A) (not B)) : not (or A B) :=
|
||||
fun (contra : or A B) =>
|
||||
or_elim A B false contra
|
||||
(and_elim_l (not A) (not B) h)
|
||||
(and_elim_r (not A) (not B) h);
|
||||
|
||||
-- A ∧ B => B ∧ A
|
||||
def and_comm (A B : *) (h : and A B) : and B A :=
|
||||
and_intro B A
|
||||
(and_elim_r A B h)
|
||||
(and_elim_l A B h);
|
||||
-- ~A ∨ ~B => ~(A ∧ B)
|
||||
def de_morgan3 (h : or (not A) (not B)) : not (and A B) :=
|
||||
fun (contra : and A B) =>
|
||||
or_elim (not A) (not B) false h
|
||||
(fun (na : not A) => na (and_elim_l A B contra))
|
||||
(fun (nb : not B) => nb (and_elim_r A B contra));
|
||||
|
||||
-- A ∨ B => B ∨ A
|
||||
def or_comm (A B : *) (h : or A B) : or B A :=
|
||||
or_elim A B (or B A) h
|
||||
(fun (a : A) => or_intro_r B A a)
|
||||
(fun (b : B) => or_intro_l B A b);
|
||||
-- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
|
||||
|
||||
-- A ∧ (B ∧ C) => (A ∧ B) ∧ C
|
||||
def and_assoc_l (A B C : *) (h : and A (and B C)) : and (and A B) C :=
|
||||
let (a := (and_elim_l A (and B C) h))
|
||||
(bc := (and_elim_r A (and B C) h))
|
||||
(b := (and_elim_l B C bc))
|
||||
(c := (and_elim_r B C bc))
|
||||
in
|
||||
and_intro (and A B) C (and_intro A B a b) c
|
||||
end;
|
||||
-- A ∧ B => B ∧ A
|
||||
def and_comm (h : and A B) : and B A :=
|
||||
and_intro B A
|
||||
(and_elim_r A B h)
|
||||
(and_elim_l A B h);
|
||||
|
||||
-- (A ∧ B) ∧ C => A ∧ (B ∧ C)
|
||||
def and_assoc_r (A B C : *) (h : and (and A B) C) : and A (and B C) :=
|
||||
let (ab := and_elim_l (and A B) C h)
|
||||
(a := and_elim_l A B ab)
|
||||
(b := and_elim_r A B ab)
|
||||
(c := and_elim_r (and A B) C h)
|
||||
in
|
||||
and_intro A (and B C) a (and_intro B C b c)
|
||||
end;
|
||||
-- A ∨ B => B ∨ A
|
||||
def or_comm (h : or A B) : or B A :=
|
||||
or_elim A B (or B A) h
|
||||
(fun (a : A) => or_intro_r B A a)
|
||||
(fun (b : B) => or_intro_l B A b);
|
||||
|
||||
-- A ∨ (B ∨ C) => (A ∨ B) ∨ C
|
||||
def or_assoc_l (A B C : *) (h : or A (or B C)) : or (or A B) C :=
|
||||
or_elim A (or B C) (or (or A B) C) h
|
||||
(fun (a : A) => or_intro_l (or A B) C (or_intro_l A B a))
|
||||
(fun (g : or B C) =>
|
||||
or_elim B C (or (or A B) C) g
|
||||
(fun (b : B) => or_intro_l (or A B) C (or_intro_r A B b))
|
||||
(fun (c : C) => or_intro_r (or A B) C c));
|
||||
-- A ∧ (B ∧ C) => (A ∧ B) ∧ C
|
||||
def and_assoc_l (h : and A (and B C)) : and (and A B) C :=
|
||||
let (a := (and_elim_l A (and B C) h))
|
||||
(bc := (and_elim_r A (and B C) h))
|
||||
(b := (and_elim_l B C bc))
|
||||
(c := (and_elim_r B C bc))
|
||||
in
|
||||
and_intro (and A B) C (and_intro A B a b) c
|
||||
end;
|
||||
|
||||
-- (A ∨ B) ∨ C => A ∨ (B ∨ C)
|
||||
def or_assoc_r (A B C : *) (h : or (or A B) C) : or A (or B C) :=
|
||||
or_elim (or A B) C (or A (or B C)) h
|
||||
(fun (g : or A B) =>
|
||||
or_elim A B (or A (or B C)) g
|
||||
(fun (a : A) => or_intro_l A (or B C) a)
|
||||
(fun (b : B) => or_intro_r A (or B C) (or_intro_l B C b)))
|
||||
(fun (c : C) => or_intro_r A (or B C) (or_intro_r B C c));
|
||||
-- (A ∧ B) ∧ C => A ∧ (B ∧ C)
|
||||
def and_assoc_r (h : and (and A B) C) : and A (and B C) :=
|
||||
let (ab := and_elim_l (and A B) C h)
|
||||
(a := and_elim_l A B ab)
|
||||
(b := and_elim_r A B ab)
|
||||
(c := and_elim_r (and A B) C h)
|
||||
in
|
||||
and_intro A (and B C) a (and_intro B C b c)
|
||||
end;
|
||||
|
||||
-- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
|
||||
def and_distrib_l_or (A B C : *) (h : and A (or B C)) : or (and A B) (and A C) :=
|
||||
or_elim B C (or (and A B) (and A C)) (and_elim_r A (or B C) h)
|
||||
(fun (b : B) => or_intro_l (and A B) (and A C)
|
||||
(and_intro A B (and_elim_l A (or B C) h) b))
|
||||
(fun (c : C) => or_intro_r (and A B) (and A C)
|
||||
(and_intro A C (and_elim_l A (or B C) h) c));
|
||||
-- A ∨ (B ∨ C) => (A ∨ B) ∨ C
|
||||
def or_assoc_l (h : or A (or B C)) : or (or A B) C :=
|
||||
or_elim A (or B C) (or (or A B) C) h
|
||||
(fun (a : A) => or_intro_l (or A B) C (or_intro_l A B a))
|
||||
(fun (g : or B C) =>
|
||||
or_elim B C (or (or A B) C) g
|
||||
(fun (b : B) => or_intro_l (or A B) C (or_intro_r A B b))
|
||||
(fun (c : C) => or_intro_r (or A B) C c));
|
||||
|
||||
-- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
|
||||
def and_factor_l_or (A B C : *) (h : or (and A B) (and A C)) : and A (or B C) :=
|
||||
or_elim (and A B) (and A C) (and A (or B C)) h
|
||||
(fun (ab : and A B) => and_intro A (or B C)
|
||||
(and_elim_l A B ab)
|
||||
(or_intro_l B C (and_elim_r A B ab)))
|
||||
(fun (ac : and A C) => and_intro A (or B C)
|
||||
(and_elim_l A C ac)
|
||||
(or_intro_r B C (and_elim_r A C ac)));
|
||||
-- (A ∨ B) ∨ C => A ∨ (B ∨ C)
|
||||
def or_assoc_r (h : or (or A B) C) : or A (or B C) :=
|
||||
or_elim (or A B) C (or A (or B C)) h
|
||||
(fun (g : or A B) =>
|
||||
or_elim A B (or A (or B C)) g
|
||||
(fun (a : A) => or_intro_l A (or B C) a)
|
||||
(fun (b : B) => or_intro_r A (or B C) (or_intro_l B C b)))
|
||||
(fun (c : C) => or_intro_r A (or B C) (or_intro_r B C c));
|
||||
|
||||
-- Thanks Quinn!
|
||||
-- A ∨ B => ~B => A
|
||||
def disj_syllog (A B : *) (nb : not B) (hor : or A B) : A :=
|
||||
or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A);
|
||||
-- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
|
||||
def and_distrib_l_or (h : and A (or B C)) : or (and A B) (and A C) :=
|
||||
or_elim B C (or (and A B) (and A C)) (and_elim_r A (or B C) h)
|
||||
(fun (b : B) => or_intro_l (and A B) (and A C)
|
||||
(and_intro A B (and_elim_l A (or B C) h) b))
|
||||
(fun (c : C) => or_intro_r (and A B) (and A C)
|
||||
(and_intro A C (and_elim_l A (or B C) h) c));
|
||||
|
||||
-- (A => B) => ~B => ~A
|
||||
def contrapositive (A B : *) (f : A -> B) (nb : not B) : not A :=
|
||||
fun (a : A) => nb (f a);
|
||||
-- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
|
||||
def and_factor_l_or (h : or (and A B) (and A C)) : and A (or B C) :=
|
||||
or_elim (and A B) (and A C) (and A (or B C)) h
|
||||
(fun (ab : and A B) => and_intro A (or B C)
|
||||
(and_elim_l A B ab)
|
||||
(or_intro_l B C (and_elim_r A B ab)))
|
||||
(fun (ac : and A C) => and_intro A (or B C)
|
||||
(and_elim_l A C ac)
|
||||
(or_intro_r B C (and_elim_r A C ac)));
|
||||
|
||||
-- Thanks Quinn!
|
||||
-- A ∨ B => ~B => A
|
||||
def disj_syllog (nb : not B) (hor : or A B) : A :=
|
||||
or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A);
|
||||
|
||||
-- (A => B) => ~B => ~A
|
||||
def contrapositive (f : A -> B) (nb : not B) : not A :=
|
||||
fun (a : A) => nb (f a);
|
||||
|
||||
end Theorems
|
||||
|
|
|
|||
|
|
@ -155,73 +155,72 @@ def suc_or_zero : forall (n : nat), szc n :=
|
|||
-- satisfying 1 and 2. From there we will, with much effort, prove that R is
|
||||
-- actually a function satisfying the equations we want it to.
|
||||
|
||||
section RecursiveDefs
|
||||
|
||||
variable (A : *) (z : A) (fS : nat -> A -> A);
|
||||
|
||||
-- {{{ Defining R
|
||||
-- Here is condition 1 formally expressed in perga.
|
||||
def cond1 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
|
||||
Q zero z;
|
||||
def cond1 (Q : nat -> A -> *) := Q zero z;
|
||||
|
||||
-- Likewise for condition 2.
|
||||
def cond2 (A : *) (z : A) (fS : nat -> A -> A) (Q : nat -> A -> *) :=
|
||||
def cond2 (Q : nat -> A -> *) :=
|
||||
forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);
|
||||
|
||||
-- From here we can define R.
|
||||
def rec_rel (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
|
||||
forall (Q : nat -> A -> *), cond1 A z fS Q -> cond2 A z fS Q -> Q x y;
|
||||
def rec_rel (x : nat) (y : A) :=
|
||||
forall (Q : nat -> A -> *), cond1 Q -> cond2 Q -> Q x y;
|
||||
-- }}}
|
||||
|
||||
-- {{{ R is total
|
||||
def total (A B : *) (R : A -> B -> *) := forall (a : A), exists B (R a);
|
||||
|
||||
def rec_rel_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel A z fS) :=
|
||||
fun (Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) => h1;
|
||||
def rec_rel_cond1 : cond1 rec_rel :=
|
||||
fun (Q : nat -> A -> *) (h1 : cond1 Q) (h2 : cond2 Q) => h1;
|
||||
|
||||
def rec_rel_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel A z fS) :=
|
||||
fun (n : nat) (y : A) (h : rec_rel A z fS n y)
|
||||
(Q : nat -> A -> *) (h1 : cond1 A z fS Q) (h2 : cond2 A z fS Q) =>
|
||||
def rec_rel_cond2 : cond2 rec_rel :=
|
||||
fun (n : nat) (y : A) (h : rec_rel n y)
|
||||
(Q : nat -> A -> *) (h1 : cond1 Q) (h2 : cond2 Q) =>
|
||||
h2 n y (h Q h1 h2);
|
||||
|
||||
def rec_rel_total (A : *) (z : A) (fS : nat -> A -> A) : total nat A (rec_rel A z fS) :=
|
||||
let (R := rec_rel A z fS)
|
||||
def rec_rel_total : total nat A rec_rel :=
|
||||
let (R := rec_rel)
|
||||
(P (x : nat) := exists A (R x))
|
||||
(c1 := cond1 A z fS)
|
||||
(c2 := cond2 A z fS)
|
||||
in
|
||||
nat_ind P
|
||||
(exists_intro A (R zero) z (rec_rel_cond1 A z fS))
|
||||
(exists_intro A (R zero) z rec_rel_cond1)
|
||||
(fun (n : nat) (IH : P n) =>
|
||||
exists_elim A (P (suc n)) (R n) IH
|
||||
(fun (y0 : A) (hy : R n y0) =>
|
||||
exists_intro A (R (suc n)) (fS n y0) (rec_rel_cond2 A z fS n y0 hy)))
|
||||
exists_intro A (R (suc n)) (fS n y0) (rec_rel_cond2 n y0 hy)))
|
||||
end;
|
||||
|
||||
-- }}}
|
||||
|
||||
-- {{{ Defining R2
|
||||
def alt_cond1 (A : *) (z : A) (x : nat) (y : A) :=
|
||||
def alt_cond1 (x : nat) (y : A) :=
|
||||
and (eq nat x zero) (eq A y z);
|
||||
|
||||
def cond_y2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A)
|
||||
def cond_y2 (x : nat) (y : A)
|
||||
(x2 : nat) (y2 : A) :=
|
||||
and (eq A y (fS x2 y2)) (rec_rel A z fS x2 y2);
|
||||
and (eq A y (fS x2 y2)) (rec_rel x2 y2);
|
||||
|
||||
def cond_x2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) (x2 : nat) :=
|
||||
and (pred x x2) (exists A (cond_y2 A z fS x y x2));
|
||||
def cond_x2 (x : nat) (y : A) (x2 : nat) :=
|
||||
and (pred x x2) (exists A (cond_y2 x y x2));
|
||||
|
||||
def alt_cond2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
|
||||
exists nat (cond_x2 A z fS x y);
|
||||
def alt_cond2 (x : nat) (y : A) := exists nat (cond_x2 x y);
|
||||
|
||||
def rec_rel_alt (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :=
|
||||
or (alt_cond1 A z x y) (alt_cond2 A z fS x y);
|
||||
def rec_rel_alt (x : nat) (y : A) := or (alt_cond1 x y) (alt_cond2 x y);
|
||||
-- }}}
|
||||
|
||||
-- {{{ R = R2
|
||||
|
||||
-- {{{ R2 ⊆ R
|
||||
def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
|
||||
rec_rel_alt A z fS x y -> rec_rel A z fS x y :=
|
||||
let (R := rec_rel A z fS)
|
||||
(R2 := rec_rel_alt A z fS)
|
||||
(ac1 := alt_cond1 A z x y)
|
||||
(ac2 := alt_cond2 A z fS x y)
|
||||
def R2_sub_R (x : nat) (y : A) : rec_rel_alt x y -> rec_rel x y :=
|
||||
let (R := rec_rel)
|
||||
(R2 := rec_rel_alt)
|
||||
(ac1 := alt_cond1 x y)
|
||||
(ac2 := alt_cond2 x y)
|
||||
in
|
||||
fun (h : R2 x y) =>
|
||||
or_elim ac1 ac2 (R x y) h
|
||||
|
|
@ -229,13 +228,13 @@ def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
|
|||
let
|
||||
(x0 := and_elim_l (eq nat x zero) (eq A y z) case1)
|
||||
(yz := and_elim_r (eq nat x zero) (eq A y z) case1)
|
||||
(a1 := (eq_sym A y z yz) (R zero) (rec_rel_cond1 A z fS))
|
||||
(a1 := (eq_sym A y z yz) (R zero) rec_rel_cond1)
|
||||
in
|
||||
(eq_sym nat x zero x0) (fun (n : nat) => R n y) a1
|
||||
end)
|
||||
(fun (case2 : ac2) =>
|
||||
let (h1 := cond_x2 A z fS x y)
|
||||
(h2 := cond_y2 A z fS x y)
|
||||
let (h1 := cond_x2 x y)
|
||||
(h2 := cond_y2 x y)
|
||||
in
|
||||
exists_elim nat (R x y) h1 case2
|
||||
(fun (x2 : nat) (hx2 : h1 x2) =>
|
||||
|
|
@ -246,7 +245,7 @@ def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
|
|||
(fun (y2 : A) (hy2 : h2 x2 y2) =>
|
||||
let (hpreim := and_elim_l (eq A y (fS x2 y2)) (R x2 y2) hy2)
|
||||
(hR := and_elim_r (eq A y (fS x2 y2)) (R x2 y2) hy2)
|
||||
(a1 := rec_rel_cond2 A z fS x2 y2 hR)
|
||||
(a1 := rec_rel_cond2 x2 y2 hR)
|
||||
(a2 := (eq_sym A y (fS x2 y2) hpreim) (R (suc x2)) a1)
|
||||
in
|
||||
(eq_sym nat x (suc x2) hpred) (fun (n : nat) => R n y) a2
|
||||
|
|
@ -257,41 +256,36 @@ def R2_sub_R (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
|
|||
-- }}}
|
||||
|
||||
-- {{{ R ⊆ R2
|
||||
def R2_cond1 (A : *) (z : A) (fS : nat -> A -> A) : cond1 A z fS (rec_rel_alt A z fS) :=
|
||||
or_intro_l (alt_cond1 A z zero z) (alt_cond2 A z fS zero z)
|
||||
def R2_cond1 : cond1 rec_rel_alt :=
|
||||
or_intro_l (alt_cond1 zero z) (alt_cond2 zero z)
|
||||
(and_intro (eq nat zero zero) (eq A z z)
|
||||
(eq_refl nat zero)
|
||||
(eq_refl A z));
|
||||
|
||||
def R2_cond2 (A : *) (z : A) (fS : nat -> A -> A) : cond2 A z fS (rec_rel_alt A z fS) :=
|
||||
let (R := rec_rel A z fS)
|
||||
(R2 := rec_rel_alt A z fS)
|
||||
def R2_cond2 : cond2 rec_rel_alt :=
|
||||
let (R := rec_rel)
|
||||
(R2 := rec_rel_alt)
|
||||
in
|
||||
fun (x2 : nat) (y2 : A) (h : R2 x2 y2) =>
|
||||
let (x := suc x2)
|
||||
(y := fS x2 y2)
|
||||
(cx2 := cond_x2 A z fS x y)
|
||||
(cy2 := cond_y2 A z fS x y x2)
|
||||
(cx2 := cond_x2 x y)
|
||||
(cy2 := cond_y2 x y x2)
|
||||
in
|
||||
or_intro_r (alt_cond1 A z x y) (alt_cond2 A z fS x y)
|
||||
or_intro_r (alt_cond1 x y) (alt_cond2 x y)
|
||||
(exists_intro nat cx2 x2
|
||||
(and_intro (pred x x2) (exists A cy2)
|
||||
(eq_refl nat x)
|
||||
(exists_intro A cy2 y2
|
||||
(and_intro (eq A y y) (R x2 y2)
|
||||
(eq_refl A y)
|
||||
(R2_sub_R A z fS x2 y2 h)))))
|
||||
(R2_sub_R x2 y2 h)))))
|
||||
end
|
||||
end;
|
||||
|
||||
def R_sub_R2 (A : *) (z : A) (fS : nat -> A -> A) (x : nat) (y : A) :
|
||||
rec_rel A z fS x y -> rec_rel_alt A z fS x y :=
|
||||
let (R := rec_rel A z fS)
|
||||
(R2 := rec_rel_alt A z fS)
|
||||
in
|
||||
fun (h : R x y) =>
|
||||
h R2 (R2_cond1 A z fS) (R2_cond2 A z fS)
|
||||
end;
|
||||
|
||||
def R_sub_R2 (x : nat) (y : A) : rec_rel x y -> rec_rel_alt x y :=
|
||||
fun (h : rec_rel x y) => h rec_rel_alt R2_cond1 R2_cond2;
|
||||
-- }}}
|
||||
|
||||
-- }}}
|
||||
|
|
@ -303,13 +297,12 @@ def fl_in (A B : *) (R : A -> B -> *) (x : A) := forall (y1 y2 : B),
|
|||
|
||||
def fl (A B : *) (R : A -> B -> *) := forall (x : A), fl_in A B R x;
|
||||
|
||||
def R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
|
||||
rec_rel_alt A z fS zero y -> eq A y z :=
|
||||
let (R2 := rec_rel_alt A z fS)
|
||||
(ac1 := alt_cond1 A z zero y)
|
||||
(ac2 := alt_cond2 A z fS zero y)
|
||||
(cx2 := cond_x2 A z fS zero y)
|
||||
(cy2 := cond_y2 A z fS zero y)
|
||||
def R2_zero (y : A) : rec_rel_alt zero y -> eq A y z :=
|
||||
let (R2 := rec_rel_alt)
|
||||
(ac1 := alt_cond1 zero y)
|
||||
(ac2 := alt_cond2 zero y)
|
||||
(cx2 := cond_x2 zero y)
|
||||
(cy2 := cond_y2 zero y)
|
||||
in fun (h : R2 zero y) =>
|
||||
or_elim ac1 ac2 (eq A y z) h
|
||||
(fun (case1 : ac1) => and_elim_r (eq nat zero zero) (eq A y z) case1)
|
||||
|
|
@ -321,14 +314,13 @@ def R2_zero (A : *) (z : A) (fS : nat -> A -> A) (y : A) :
|
|||
(eq A y z)))
|
||||
end;
|
||||
|
||||
def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
|
||||
rec_rel_alt A z fS (suc x2) y -> exists A (cond_y2 A z fS (suc x2) y x2) :=
|
||||
let (R2 := rec_rel_alt A z fS)
|
||||
def R2_suc (x2 : nat) (y : A) : rec_rel_alt (suc x2) y -> exists A (cond_y2 (suc x2) y x2) :=
|
||||
let (R2 := rec_rel_alt)
|
||||
(x := suc x2)
|
||||
(ac1 := alt_cond1 A z x y)
|
||||
(ac2 := alt_cond2 A z fS x y)
|
||||
(cx2 := cond_x2 A z fS x y)
|
||||
(cy2 := cond_y2 A z fS x y)
|
||||
(ac1 := alt_cond1 x y)
|
||||
(ac2 := alt_cond2 x y)
|
||||
(cx2 := cond_x2 x y)
|
||||
(cy2 := cond_y2 x y)
|
||||
(goal := exists A (cy2 x2))
|
||||
in
|
||||
fun (h : R2 x y) =>
|
||||
|
|
@ -347,31 +339,31 @@ def R2_suc (A : *) (z : A) (fS : nat -> A -> A) (x2 : nat) (y : A) :
|
|||
end))
|
||||
end;
|
||||
|
||||
def R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A z fS) :=
|
||||
let (R := rec_rel A z fS)
|
||||
(R2 := rec_rel_alt A z fS)
|
||||
def R2_functional : fl nat A rec_rel_alt :=
|
||||
let (R := rec_rel)
|
||||
(R2 := rec_rel_alt)
|
||||
(f_in := fl_in nat A R2)
|
||||
in nat_ind f_in
|
||||
(fun (y1 y2 : A) (h1 : R2 zero y1) (h2 : R2 zero y2) =>
|
||||
eq_trans A y1 z y2
|
||||
(R2_zero A z fS y1 h1)
|
||||
(eq_sym A y2 z (R2_zero A z fS y2 h2)))
|
||||
(R2_zero y1 h1)
|
||||
(eq_sym A y2 z (R2_zero y2 h2)))
|
||||
(fun (x2 : nat) (IH : f_in x2) (y1 y2 : A) (h1 : R2 (suc x2) y1) (h2 : R2 (suc x2) y2) =>
|
||||
let (x := suc x2)
|
||||
(cy1 := cond_y2 A z fS x y1 x2)
|
||||
(cy2 := cond_y2 A z fS x y2 x2)
|
||||
(cy1 := cond_y2 x y1 x2)
|
||||
(cy2 := cond_y2 x y2 x2)
|
||||
(goal := eq A y1 y2)
|
||||
in
|
||||
exists_elim A goal cy1 (R2_suc A z fS x2 y1 h1)
|
||||
exists_elim A goal cy1 (R2_suc x2 y1 h1)
|
||||
(fun (y12 : A) (h12 : cy1 y12) =>
|
||||
exists_elim A goal cy2 (R2_suc A z fS x2 y2 h2)
|
||||
exists_elim A goal cy2 (R2_suc x2 y2 h2)
|
||||
(fun (y22 : A) (h22 : cy2 y22) =>
|
||||
let (y1_preim := and_elim_l (eq A y1 (fS x2 y12)) (R x2 y12) h12)
|
||||
(y2_preim := and_elim_l (eq A y2 (fS x2 y22)) (R x2 y22) h22)
|
||||
(R_x2_y12 := and_elim_r (eq A y1 (fS x2 y12)) (R x2 y12) h12)
|
||||
(R_x2_y22 := and_elim_r (eq A y2 (fS x2 y22)) (R x2 y22) h22)
|
||||
(R2_x2_y12 := R_sub_R2 A z fS x2 y12 R_x2_y12)
|
||||
(R2_x2_y22 := R_sub_R2 A z fS x2 y22 R_x2_y22)
|
||||
(R2_x2_y12 := R_sub_R2 x2 y12 R_x2_y12)
|
||||
(R2_x2_y22 := R_sub_R2 x2 y22 R_x2_y22)
|
||||
(y12_y22 := IH y12 y22 R2_x2_y12 R2_x2_y22)
|
||||
in
|
||||
eq_trans A y1 (fS x2 y12) y2
|
||||
|
|
@ -383,21 +375,16 @@ def R2_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel_alt A
|
|||
end)
|
||||
end;
|
||||
|
||||
def R_functional (A : *) (z : A) (fS : nat -> A -> A) : fl nat A (rec_rel A z fS) :=
|
||||
let (R := rec_rel A z fS)
|
||||
(sub := R_sub_R2 A z fS)
|
||||
in
|
||||
fun (n : nat) (y1 y2 : A) (h1 : R n y1) (h2 : R n y2) =>
|
||||
R2_functional A z fS n y1 y2 (sub n y1 h1) (sub n y2 h2)
|
||||
end;
|
||||
def R_functional : fl nat A rec_rel :=
|
||||
fun (n : nat) (y1 y2 : A) (h1 : rec_rel n y1) (h2 : rec_rel n y2) =>
|
||||
R2_functional n y1 y2 (R_sub_R2 n y1 h1) (R_sub_R2 n y2 h2);
|
||||
|
||||
-- }}}
|
||||
|
||||
-- {{{ Actually defining the function
|
||||
|
||||
def rec_def (A : *) (z : A) (fS : nat -> A -> A) (x : nat) : A :=
|
||||
exists_elim A A (rec_rel A z fS x) (rec_rel_total A z fS x)
|
||||
(fun (y : A) (_ : rec_rel A z fS x y) => y);
|
||||
def rec_def (x : nat) : A :=
|
||||
exists_elim A A (rec_rel x) (rec_rel_total x) (fun (y : A) (_ : rec_rel x y) => y);
|
||||
|
||||
-- }}}
|
||||
|
||||
|
|
@ -415,39 +402,30 @@ axiom definite_description (A : *) (P : A -> *) (h : exists A P) :
|
|||
P (exists_elim A A P h (fun (x : A) (_ : P x) => x));
|
||||
|
||||
-- Now we can use this axiom to prove that R n (rec_def n).
|
||||
def rec_def_sat (A : *) (z : A) (fS : nat -> A -> A) (x : nat) : rec_rel A z fS x (rec_def A z fS x) :=
|
||||
definite_description A (rec_rel A z fS x) (rec_rel_total A z fS x);
|
||||
def rec_def_sat (x : nat) : rec_rel x (rec_def x) :=
|
||||
definite_description A (rec_rel x) (rec_rel_total x);
|
||||
|
||||
def eq1 (A : *) (z : A) (f : nat -> A) := eq A (f zero) z;
|
||||
def eq1 (f : nat -> A) := eq A (f zero) z;
|
||||
|
||||
def eq2 (A : *) (z : A) (fS : nat -> A -> A) (f : nat -> A) := forall (n : nat), eq A (f (suc n)) (fS n (f n));
|
||||
def eq2 (f : nat -> A) := forall (n : nat), eq A (f (suc n)) (fS n (f n));
|
||||
|
||||
-- f zero = z
|
||||
def rec_def_sat_zero (A : *) (z : A) (fS : nat -> A -> A) : eq1 A z (rec_def A z fS) :=
|
||||
let (f := rec_def A z fS) in
|
||||
R_functional A z fS zero (f zero) z
|
||||
(rec_def_sat A z fS zero)
|
||||
(rec_rel_cond1 A z fS)
|
||||
end;
|
||||
def rec_def_sat_zero : eq1 rec_def := R_functional zero (rec_def zero) z (rec_def_sat zero) rec_rel_cond1;
|
||||
|
||||
-- f n = y -> f (suc n) = fS n y
|
||||
def rec_def_sat_suc (A : *) (z : A) (fS : nat -> A -> A) : eq2 A z fS (rec_def A z fS) :=
|
||||
def rec_def_sat_suc : eq2 rec_def :=
|
||||
fun (n : nat) =>
|
||||
let (R := rec_rel A z fS)
|
||||
(f := rec_def A z fS)
|
||||
(y := f n)
|
||||
(Rf := rec_def_sat A z fS)
|
||||
(RSnfy := rec_rel_cond2 A z fS n y (Rf n))
|
||||
let (y := rec_def n)
|
||||
(RSnfy := rec_rel_cond2 n y (rec_def_sat n))
|
||||
in
|
||||
R_functional A z fS (suc n) (f (suc n)) (fS n y) (Rf (suc n)) RSnfy
|
||||
R_functional (suc n) (rec_def (suc n)) (fS n y) (rec_def_sat (suc n)) RSnfy
|
||||
end;
|
||||
|
||||
-- }}}
|
||||
|
||||
-- {{{ The function satisfying these equations is unique
|
||||
|
||||
def rec_def_unique (A : *) (z : A) (fS : nat -> A -> A) (f g : nat -> A)
|
||||
(h1f : eq1 A z f) (h2f : eq2 A z fS f) (h1g : eq1 A z g) (h2g : eq2 A z fS g)
|
||||
def rec_def_unique (fS : nat -> A -> A) (f g : nat -> A) (h1f : eq1 f) (h2f : eq2 f) (h1g : eq1 g) (h2g : eq2 g)
|
||||
: forall (n : nat), eq A (f n) (g n) :=
|
||||
nat_ind (fun (n : nat) => eq A (f n) (g n))
|
||||
-- base case: f 0 = g 0
|
||||
|
|
@ -470,6 +448,8 @@ def rec_def_unique (A : *) (z : A) (fS : nat -> A -> A) (f g : nat -> A)
|
|||
|
||||
-- }}}
|
||||
|
||||
end RecursiveDefs
|
||||
|
||||
-- }}}
|
||||
|
||||
-- Now we can safely define addition.
|
||||
|
|
|
|||
|
|
@ -2,29 +2,25 @@
|
|||
|
||||
module Elaborator where
|
||||
|
||||
import Control.Monad.Except
|
||||
import Data.List (elemIndex, lookup)
|
||||
import Data.List.NonEmpty ((<|))
|
||||
import Errors (Error (..), Result)
|
||||
import qualified Data.Set as S
|
||||
import Expr (Expr)
|
||||
import qualified Expr as E
|
||||
import IR (IRDef (..), IRExpr, IRProgram)
|
||||
import IR (IRDef (..), IRExpr, IRProgram, IRSectionDef (..))
|
||||
import qualified IR as I
|
||||
import Relude.Extra.Lens
|
||||
|
||||
type Binders = [Text]
|
||||
|
||||
data SectionContext = SectionContext
|
||||
{ sectionDefs :: [(Text, [Text])] -- name and list of variables it depends on
|
||||
{ sectionDefs :: [(Text, [(Text, IRExpr)])] -- name and list of variables and their types it depends on
|
||||
, sectionVars :: [(Text, IRExpr)] -- variables and their types
|
||||
}
|
||||
|
||||
type ElabMonad = State SectionContext
|
||||
|
||||
lookupDefInCtxt :: Text -> SectionContext -> Maybe [(Text, IRExpr)]
|
||||
lookupDefInCtxt def (SectionContext defs vars) = mapMaybe helper <$> lookup def defs
|
||||
where
|
||||
helper dep = (dep,) <$> dep `lookup` vars
|
||||
lookupDefInCtxt def (SectionContext defs _) = lookup def defs
|
||||
|
||||
-- looks up a definition in the context and gives a list of the variables and
|
||||
-- their types that it depends on
|
||||
|
|
@ -38,7 +34,7 @@ lookupVarInCtxt var = lookup var . sectionVars
|
|||
lookupVar :: Text -> ElabMonad (Maybe IRExpr)
|
||||
lookupVar var = lookupVarInCtxt var <$> get
|
||||
|
||||
sectionDefsL :: Lens' SectionContext [(Text, [Text])]
|
||||
sectionDefsL :: Lens' SectionContext [(Text, [(Text, IRExpr)])]
|
||||
sectionDefsL = lens sectionDefs setter
|
||||
where
|
||||
setter ctxt newDefs = ctxt{sectionDefs = newDefs}
|
||||
|
|
@ -51,16 +47,29 @@ sectionVarsL = lens sectionVars setter
|
|||
saveState :: ElabMonad a -> ElabMonad a
|
||||
saveState action = get >>= (action <*) . put
|
||||
|
||||
elabSection :: Text -> [IRDef] -> ElabMonad [IRDef]
|
||||
debugIRExpr :: IRExpr -> String
|
||||
debugIRExpr = E.prettyS . elaborate
|
||||
|
||||
debugIRDef :: IRDef -> String
|
||||
debugIRDef (Def name (Just ty) body) = "def " ++ toString name ++ " : " ++ debugIRExpr ty ++ " := " ++ debugIRExpr body ++ ";"
|
||||
debugIRDef (Def name Nothing body) = "def " ++ toString name ++ " := " ++ debugIRExpr body ++ ";"
|
||||
debugIRDef (Axiom name typ) = "axiom " ++ toString name ++ " : " ++ debugIRExpr typ ++ ";"
|
||||
|
||||
debugIRSectionDef :: IRSectionDef -> String
|
||||
debugIRSectionDef (Variable name typ) = "variable " ++ toString name ++ " : " ++ debugIRExpr typ ++ ";"
|
||||
debugIRSectionDef (Section name _) = "section " ++ toString name ++ ";"
|
||||
debugIRSectionDef (IRDef def) = debugIRDef def
|
||||
|
||||
elabSection :: Text -> [IRSectionDef] -> ElabMonad [IRDef]
|
||||
elabSection _name contents = saveState $ concat <$> forM contents elabDef
|
||||
|
||||
elabProgram :: IRProgram -> IRProgram
|
||||
elabProgram :: IRProgram -> [IRDef]
|
||||
elabProgram prog = evalState (elabSection "" prog) (SectionContext [] [])
|
||||
|
||||
pushVariable :: Text -> IRExpr -> SectionContext -> SectionContext
|
||||
pushVariable name ty (SectionContext defs vars) = SectionContext defs ((name, ty) : vars)
|
||||
|
||||
pushDefinition :: Text -> [Text] -> SectionContext -> SectionContext
|
||||
pushDefinition :: Text -> [(Text, IRExpr)] -> SectionContext -> SectionContext
|
||||
pushDefinition name defVars (SectionContext defs vars) = SectionContext ((name, defVars) : defs) vars
|
||||
|
||||
removeName :: Text -> ElabMonad ()
|
||||
|
|
@ -68,39 +77,53 @@ removeName name = do
|
|||
modify $ over sectionDefsL (filter ((/= name) . fst))
|
||||
modify $ over sectionVarsL (filter ((/= name) . fst))
|
||||
|
||||
extendVars :: Set (Text, IRExpr) -> ElabMonad (Set (Text, IRExpr))
|
||||
extendVars vars = do
|
||||
vars' <- foldr S.union S.empty <$> traverse (usedVars . snd) (S.toList vars)
|
||||
if vars' `S.isSubsetOf` vars
|
||||
then pure vars
|
||||
else extendVars (vars `S.union` vars')
|
||||
|
||||
organize :: Set (Text, IRExpr) -> ElabMonad [(Text, IRExpr)]
|
||||
organize found = do
|
||||
vars <- gets sectionVars
|
||||
pure $ reverse [var | var <- vars, var `S.member` found]
|
||||
|
||||
-- find all the section variables used in an expression
|
||||
usedVars :: IRExpr -> ElabMonad [(Text, IRExpr)]
|
||||
usedVars (I.Var name) = maybe [] (pure . (name,)) <$> lookupVar name
|
||||
usedVars I.Star = pure []
|
||||
usedVars (I.Level _) = pure []
|
||||
usedVars (I.App m n) = (++) <$> usedVars m <*> usedVars n
|
||||
usedVars :: IRExpr -> ElabMonad (Set (Text, IRExpr))
|
||||
usedVars (I.Var name) = do
|
||||
varDeps <- maybe S.empty (S.singleton . (name,)) <$> lookupVar name
|
||||
defDeps <- maybe S.empty S.fromList <$> lookupDef name
|
||||
pure $ varDeps `S.union` defDeps
|
||||
usedVars I.Star = pure S.empty
|
||||
usedVars (I.Level _) = pure S.empty
|
||||
usedVars (I.App m n) = S.union <$> usedVars m <*> usedVars n
|
||||
usedVars (I.Abs name ty ascr body) = saveState $ do
|
||||
ty' <- usedVars ty
|
||||
ascr' <- traverse usedVars ascr
|
||||
removeName name
|
||||
((ty' ++ (ascr' ?: [])) ++) <$> usedVars body
|
||||
S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
|
||||
usedVars (I.Pi name ty ascr body) = saveState $ do
|
||||
ty' <- usedVars ty
|
||||
ascr' <- traverse usedVars ascr
|
||||
removeName name
|
||||
((ty' ++ (ascr' ?: [])) ++) <$> usedVars body
|
||||
S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
|
||||
usedVars (I.Let name ascr value body) = saveState $ do
|
||||
ty' <- usedVars value
|
||||
ascr' <- traverse usedVars ascr
|
||||
removeName name
|
||||
((ty' ++ (ascr' ?: [])) ++) <$> usedVars body
|
||||
S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
|
||||
|
||||
-- traverse the body of a definition, adding the necessary section arguments to
|
||||
-- any definitions made within the section
|
||||
traverseBody :: IRExpr -> ElabMonad IRExpr
|
||||
traverseBody (I.Var name) = do
|
||||
deps <- lookupDef name
|
||||
case deps of
|
||||
mdeps <- lookupDef name
|
||||
case mdeps of
|
||||
Nothing -> pure $ I.Var name
|
||||
Just [] -> pure $ I.Var name
|
||||
Just ((top, _) : rest) -> pure $ foldr (I.App . I.Var . fst) (I.Var top) rest
|
||||
Just deps -> pure $ foldl' (\acc newVar -> I.App acc (I.Var $ fst newVar)) (I.Var name) deps
|
||||
traverseBody I.Star = pure I.Star
|
||||
traverseBody e@(I.Level _) = pure e
|
||||
traverseBody (I.Level k) = pure $ I.Level k
|
||||
traverseBody (I.App m n) = I.App <$> traverseBody m <*> traverseBody n
|
||||
traverseBody (I.Abs name ty ascr body) = saveState $ do
|
||||
ty' <- traverseBody ty
|
||||
|
|
@ -113,8 +136,8 @@ traverseBody (I.Pi name ty ascr body) = saveState $ do
|
|||
removeName name
|
||||
I.Pi name ty' ascr' <$> traverseBody body
|
||||
traverseBody (I.Let name ascr value body) = saveState $ do
|
||||
value' <- traverseBody value
|
||||
ascr' <- traverse traverseBody ascr
|
||||
value' <- traverseBody value
|
||||
removeName name
|
||||
I.Let name ascr' value' <$> traverseBody body
|
||||
|
||||
|
|
@ -130,53 +153,55 @@ generalizeType = foldr mkPi
|
|||
generalizeVal :: IRExpr -> [(Text, IRExpr)] -> IRExpr
|
||||
generalizeVal = foldr mkAbs
|
||||
|
||||
elabDef :: IRDef -> ElabMonad [IRDef]
|
||||
elabDef (Def name ty body) = do
|
||||
tyVars <- fromMaybe [] <$> traverse usedVars ty
|
||||
elabDef :: IRSectionDef -> ElabMonad [IRDef]
|
||||
elabDef (IRDef (Def name ty body)) = do
|
||||
tyVars <- fromMaybe S.empty <$> traverse usedVars ty
|
||||
bodyVars <- usedVars body
|
||||
let totalVars = tyVars ++ bodyVars
|
||||
modify $ pushDefinition name (map fst totalVars)
|
||||
pure [Def name (flip generalizeType totalVars <$> ty) (generalizeVal body totalVars)]
|
||||
elabDef (Axiom name ty) = do
|
||||
vars <- usedVars ty
|
||||
modify $ pushDefinition name (map fst vars)
|
||||
totalVars <- extendVars (tyVars `S.union` bodyVars) >>= organize
|
||||
newBody <- traverseBody body
|
||||
newType <- traverse traverseBody ty
|
||||
modify $ pushDefinition name totalVars
|
||||
pure [Def name (flip generalizeType totalVars <$> newType) (generalizeVal newBody totalVars)]
|
||||
elabDef (IRDef (Axiom name ty)) = do
|
||||
vars <- usedVars ty >>= extendVars >>= organize
|
||||
modify $ pushDefinition name vars
|
||||
pure [Axiom name (generalizeType ty vars)]
|
||||
elabDef (Section name contents) = saveState $ elabSection name contents
|
||||
elabDef (Variable name ty) = [] <$ modify' (pushVariable name ty)
|
||||
|
||||
-- saveBinders :: State Binders a -> State Binders a
|
||||
-- saveBinders action = do
|
||||
-- binders <- get
|
||||
-- res <- action
|
||||
-- put binders
|
||||
-- pure res
|
||||
--
|
||||
-- elaborate :: IRExpr -> Expr
|
||||
-- elaborate ir = evalState (elaborate' ir) []
|
||||
-- where
|
||||
-- elaborate' :: IRExpr -> State Binders Expr
|
||||
-- elaborate' (I.Var n) = do
|
||||
-- binders <- get
|
||||
-- pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
|
||||
-- elaborate' I.Star = pure E.Star
|
||||
-- elaborate' (I.Level level) = pure $ E.Level level
|
||||
-- elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
|
||||
-- elaborate' (I.Abs x t a b) = saveBinders $ do
|
||||
-- t' <- elaborate' t
|
||||
-- a' <- traverse elaborate' a
|
||||
-- modify (x :)
|
||||
-- E.Abs x t' a' <$> elaborate' b
|
||||
-- elaborate' (I.Pi x t a b) = saveBinders $ do
|
||||
-- t' <- elaborate' t
|
||||
-- a' <- traverse elaborate' a
|
||||
-- modify (x :)
|
||||
-- E.Pi x t' a' <$> elaborate' b
|
||||
-- elaborate' (I.Let name Nothing val body) = saveBinders $ do
|
||||
-- val' <- elaborate' val
|
||||
-- modify (name :)
|
||||
-- E.Let name Nothing val' <$> elaborate' body
|
||||
-- elaborate' (I.Let name (Just ty) val body) = saveBinders $ do
|
||||
-- val' <- elaborate' val
|
||||
-- ty' <- elaborate' ty
|
||||
-- modify (name :)
|
||||
-- E.Let name (Just ty') val' <$> elaborate' body
|
||||
saveBinders :: State Binders a -> State Binders a
|
||||
saveBinders action = do
|
||||
binders <- get
|
||||
res <- action
|
||||
put binders
|
||||
pure res
|
||||
|
||||
elaborate :: IRExpr -> Expr
|
||||
elaborate ir = evalState (elaborate' ir) []
|
||||
where
|
||||
elaborate' :: IRExpr -> State Binders Expr
|
||||
elaborate' (I.Var n) = do
|
||||
binders <- get
|
||||
pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
|
||||
elaborate' I.Star = pure E.Star
|
||||
elaborate' (I.Level level) = pure $ E.Level level
|
||||
elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
|
||||
elaborate' (I.Abs x t a b) = saveBinders $ do
|
||||
t' <- elaborate' t
|
||||
a' <- traverse elaborate' a
|
||||
modify (x :)
|
||||
E.Abs x t' a' <$> elaborate' b
|
||||
elaborate' (I.Pi x t a b) = saveBinders $ do
|
||||
t' <- elaborate' t
|
||||
a' <- traverse elaborate' a
|
||||
modify (x :)
|
||||
E.Pi x t' a' <$> elaborate' b
|
||||
elaborate' (I.Let name Nothing val body) = saveBinders $ do
|
||||
val' <- elaborate' val
|
||||
modify (name :)
|
||||
E.Let name Nothing val' <$> elaborate' body
|
||||
elaborate' (I.Let name (Just ty) val body) = saveBinders $ do
|
||||
val' <- elaborate' val
|
||||
ty' <- elaborate' ty
|
||||
modify (name :)
|
||||
E.Let name (Just ty') val' <$> elaborate' body
|
||||
|
|
|
|||
|
|
@ -143,12 +143,12 @@ helper k e@(Pi{}) = if k > 2 then parenthesize res else res
|
|||
where
|
||||
(params, body) = collectPis e
|
||||
grouped = showParamGroup <$> groupParams params
|
||||
res = "∏ " <> unwords grouped <> " . " <> pretty body
|
||||
res = "∏ " <> unwords grouped <> " , " <> pretty body
|
||||
helper k e@(Abs{}) = if k >= 1 then parenthesize res else res
|
||||
where
|
||||
(params, body) = collectLambdas e
|
||||
grouped = showParamGroup <$> groupParams params
|
||||
res = "λ " <> unwords grouped <> " . " <> pretty body
|
||||
res = "λ " <> unwords grouped <> " => " <> pretty body
|
||||
helper _ e@(Let{}) = res
|
||||
where
|
||||
(binds, body) = collectLets e
|
||||
|
|
|
|||
22
lib/IR.hs
22
lib/IR.hs
|
|
@ -30,6 +30,18 @@ data IRExpr
|
|||
}
|
||||
deriving (Show, Eq, Ord)
|
||||
|
||||
data IRSectionDef
|
||||
= Section
|
||||
{ sectionName :: Text
|
||||
, sectionContents :: [IRSectionDef]
|
||||
}
|
||||
| Variable
|
||||
{ variableName :: Text
|
||||
, variableType :: IRExpr
|
||||
}
|
||||
| IRDef IRDef
|
||||
deriving (Show, Eq, Ord)
|
||||
|
||||
data IRDef
|
||||
= Def
|
||||
{ defName :: Text
|
||||
|
|
@ -40,14 +52,6 @@ data IRDef
|
|||
{ axiomName :: Text
|
||||
, axiomAscription :: IRExpr
|
||||
}
|
||||
| Section
|
||||
{ sectionName :: Text
|
||||
, sectionContents :: [IRDef]
|
||||
}
|
||||
| Variable
|
||||
{ variableName :: Text
|
||||
, variableType :: IRExpr
|
||||
}
|
||||
deriving (Show, Eq, Ord)
|
||||
|
||||
type IRProgram = [IRDef]
|
||||
type IRProgram = [IRSectionDef]
|
||||
|
|
|
|||
|
|
@ -176,14 +176,12 @@ pAxiom = lexeme $ label "axiom" $ do
|
|||
eat ";"
|
||||
pure $ Axiom ident ascription
|
||||
|
||||
pVariable :: Parser IRDef
|
||||
pVariable :: Parser [IRSectionDef]
|
||||
pVariable = lexeme $ label "variable declaration" $ do
|
||||
eat "variable" <|> eat "hypothesis"
|
||||
ident <- pIdentifier
|
||||
params <- pManyParams
|
||||
ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription
|
||||
vars <- pManyParams
|
||||
eat ";"
|
||||
pure $ Variable ident ascription
|
||||
pure $ uncurry Variable <$> vars
|
||||
|
||||
pDef :: Parser IRDef
|
||||
pDef = lexeme $ label "definition" $ do
|
||||
|
|
@ -196,20 +194,20 @@ pDef = lexeme $ label "definition" $ do
|
|||
eat ";"
|
||||
pure $ Def ident ascription $ foldr (mkAbs Nothing) body params
|
||||
|
||||
pSection :: Parser IRDef
|
||||
pSection :: Parser IRSectionDef
|
||||
pSection = lexeme $ label "section" $ do
|
||||
eat "section"
|
||||
secLabel <- pIdentifier
|
||||
body <- many pIRDef
|
||||
body <- concat <$> many pIRDef
|
||||
eat "end"
|
||||
void $ lexeme $ chunk secLabel
|
||||
pure $ Section secLabel body
|
||||
|
||||
pIRDef :: Parser IRDef
|
||||
pIRDef = pAxiom <|> pDef <|> pVariable <|> pSection
|
||||
pIRDef :: Parser [IRSectionDef]
|
||||
pIRDef = (pure . IRDef <$> pAxiom) <|> (pure . IRDef <$> pDef) <|> pVariable <|> (pure <$> pSection)
|
||||
|
||||
pIRProgram :: Parser IRProgram
|
||||
pIRProgram = skipSpace >> some pIRDef
|
||||
pIRProgram = skipSpace >> concat <$> some pIRDef
|
||||
|
||||
parserWrapper :: Parser a -> String -> Text -> Either String a
|
||||
parserWrapper p filename input = first errorBundlePretty $ runParser p filename input
|
||||
|
|
@ -218,7 +216,7 @@ parseProgram :: String -> Text -> Either String IRProgram
|
|||
parseProgram = parserWrapper pIRProgram
|
||||
|
||||
parseDef :: String -> Text -> Either String IRDef
|
||||
parseDef = parserWrapper pIRDef
|
||||
parseDef = parserWrapper (pAxiom <|> pDef)
|
||||
|
||||
parseExpr :: String -> Text -> Either String IRExpr
|
||||
parseExpr = parserWrapper pIRExpr
|
||||
|
|
|
|||
|
|
@ -36,14 +36,12 @@ handleDef (Def name (Just irTy) irBody) = do
|
|||
where
|
||||
body = elaborate irBody
|
||||
ty = elaborate irTy
|
||||
handleDef (Variable name ty) = undefined
|
||||
handleDef (Section name contents) = undefined
|
||||
|
||||
evalDef :: Env -> IRDef -> Result Env
|
||||
evalDef = flip (execStateT . handleDef)
|
||||
|
||||
handleProgram :: Env -> IRProgram -> Result Env
|
||||
handleProgram env = flip execStateT env . mapM_ handleDef
|
||||
handleProgram env = flip execStateT env . mapM_ handleDef . elabProgram
|
||||
|
||||
handleAndParseProgram :: Env -> String -> Text -> Either String Env
|
||||
handleAndParseProgram env filename input = (first toString . handleProgram env) =<< parseProgram filename input
|
||||
|
|
|
|||
Loading…
Reference in a new issue