make the files/notes agree

doc/pi.ott

@@ -335,6 +335,7 @@ G |- b : A
 --------------------------- ::  app
 G |- a b : B [ b / x ]
 
+
 G |- a : A    
 G |- A = B
 ------------ :: conv

doc/weirich.bib

@@ -1,3 +1,16 @@
+@techreport{Coc,
+  TITLE = {{The calculus of constructions}},
+  AUTHOR = {Coquand, T. and Huet, G{\'e}rard},
+  URL = {https://hal.inria.fr/inria-00076024},
+  NUMBER = {RR-0530},
+  INSTITUTION = {{INRIA}},
+  YEAR = {1986},
+  MONTH = May,
+  PDF = {https://hal.inria.fr/inria-00076024/file/RR-0530.pdf},
+  HAL_ID = {inria-00076024},
+  HAL_VERSION = {v1},
+}
+
 @inproceedings{idris2,
   author    = {Edwin C. Brady},
   editor    = {Anders M{\o}ller and

full/pi/Hw1.pi

@@ -1,7 +1,7 @@
 module Hw1 where
 
 -- HW #1: get this file to type check by adding typing rules
--- for booleans and let expressions to TypeCheck.hs in 'version1'
+-- for booleans and products to TypeCheck.hs in 'version1'
 
 -- prelude operations on boolean values
 
@@ -18,7 +18,7 @@ eq_bool : Bool -> Bool -> Bool
 eq_bool = \ b1 b2 . 
   if b1 then b2 else (not b2)  
 
--- sigma types
+--- sigma types
 
 double : (A:Type) -> (x : A) -> { x : A | A }
 double = \A x. (x,x) 

full/pi/Lec1.pi

@@ -18,22 +18,17 @@ idT = (x:Type) -> x -> x
 selfapp : idT -> idT
 selfapp = (\x.x : (idT -> idT) -> (idT -> idT)) (\x.x)
 
--- some Church encodings: booleans
+-- Church encoding: booleans
 
-bool : Type 
-bool = (A:Type) -> A -> A -> A 
-
-true : bool
+true : (A:Type) -> A -> A -> A 
 true = \A x y. x
 
-false : bool
+false : (A:Type) -> A -> A -> A 
 false = \A x y. y
 
-cond : bool -> (x:Type) -> x -> x -> x
+cond : ((A:Type) -> A -> A -> A) -> (x:Type) -> x -> x -> x
 cond = \ b . b 
 
-
-
 -- void type
 
 void : Type
@@ -42,10 +37,31 @@ void = (x:Type) -> x
 -- inhabited by diverging term
 
 loop : (x:Type) -> x
-loop = loop
+loop = \x. loop x
 
 -- unit type 
 
 unit : Type
 unit = (x:Type) -> x -> x
 
+-- this code only type checks with a definition of type equality that 
+-- includes beta-equivalence/definitions (i.e. >= version2)
+
+-- Church encoding of simply-typed pairs
+{-
+
+pair : Type -> Type -> Type
+pair = \p. \q. (c: Type) -> (p -> q -> c) -> c
+
+prod : (p:Type) -> (q:Type) -> p -> q -> pair p q
+prod = \p.\q. \x.\y. \c. \f. f x y
+
+proj1 : (p:Type) -> (q:Type) -> pair p q -> p
+proj1  = \p. \q. \a. a p (\x.\y.x)
+
+proj2 : (p:Type) -> (q:Type) -> pair p q -> q
+proj2  = \p. \q. \a. a q (\x.\y.y)
+
+swap : (p:Type) -> (q:Type) -> pair p q -> pair q p
+swap = \p. \q. \a. prod q p (proj2 p q a) (proj1 p q a)
+-}

full/pi/Lec2.pi

@@ -1,24 +1,5 @@
 module Lec2 where
 
--- this code only type checks with a definition of type equality that 
--- includes definition unfolding and beta-equivalence
-
--- logical "and"
-
-and : Type -> Type -> Type
-and = \p. \q. (c: Type) -> (p -> q -> c) -> c
-
-conj : (p:Type) -> (q:Type) -> p -> q -> and p q
-conj = \p.\q. \x.\y. \c. \f. f x y
-
-proj1 : (p:Type) -> (q:Type) -> and p q -> p
-proj1  = \p. \q. \a. a p (\x.\y.x)
-
-proj2 : (p:Type) -> (q:Type) -> and p q -> q
-proj2  = \p. \q. \a. a q (\x.\y.y)
-
-and_commutes : (p:Type) -> (q:Type) -> and p q -> and q p
-and_commutes = \p. \q. \a. conj q p (proj2 p q a) (proj1 p q a)
 
 -- "large eliminations" 
 
@@ -46,7 +27,9 @@ z2 = True
 -- context-dependent. In otherwords, it should add new 
 -- definitions to the context in the true/false branches
 -- when the scrutinee is a variable
+-- (i.e. >= version3)
 
+{- 
 not : Bool -> Bool 
 not = \x. if x then False else True
 
@@ -55,6 +38,7 @@ bar = \b. if b then () else True
 
 barnot : (b : Bool) -> T (not b) 
 barnot = \b. if b then False else ()
+-}
 
 -- projections for sigma types
 

full/pi/NatChurch.pi

@@ -71,13 +71,13 @@ scott_three = scott_s (scott_s (scott_s scott_z))
 scott_pred : scott_nat -> scott_nat
 scott_pred = TRUSTME
 
-test1 : scott_pred scott_two = scott_one
-test1 = TRUSTME -- replace with Refl
+testNC1 : scott_pred scott_two = scott_one
+testNC1 = TRUSTME -- replace with Refl
 
 -- Now write plus: with Scott encoded nats, note that you need to use recursion.
 
 scott_plus : scott_nat -> scott_nat -> scott_nat 
 scott_plus = TRUSTME
 
-test2 : scott_plus scott_one scott_two = scott_three
-test2 = TRUSTME -- replace with Refl
+testNC2 : scott_plus scott_one scott_two = scott_three
+testNC2 = TRUSTME -- replace with Refl

main/Makefile

@@ -2,7 +2,7 @@ SOURCES=TypeCheck.hs PrettyPrint.hs LayoutToken.hs Parser.hs Syntax.hs Environme
 TEST_VERSION1 = Lec1.pi 
 TEST_VERSION2 = $(TEST_VERSION1) Lec2.pi Hw1.pi Hw2.pi NatChurch.pi
 TEST_VERSION3 = $(TEST_VERSION2) Lec3.pi
-TEST_FULL=Makefile $(TEST_VERSION3) Logic.pi Equality.pi Product.pi Nat.pi Fin.pi FinHw.pi Vec.pi BoolLib.pi List.pi Lambda.pi Lambda0.pi Lambda1.pi Lambda2.pi BoolLib.pi Lec4.pi Product1.pi
+TEST_FULL=Makefile $(TEST_VERSION3) Logic.pi Equality.pi Product.pi Nat.pi Fin.pi FinHw.pi Vec.pi BoolLib.pi List.pi Lambda.pi Lambda0.pi Lambda1.pi Lambda2.pi BoolLib.pi Lec4.pi Product1.pi Lennart.pi
 SRCS=$(addprefix src/,$(SOURCES)) app/Main.hs test/Main.hs
 
 EXTRA=LICENSE README.md pi-forall.cabal stack.yaml

main/pi/Equality.pi

@@ -112,6 +112,8 @@ j = \[A][C] t x y p . subst (t x) by p
 -- I don't think so. At least not without some 
 -- form of heterogenous equality
 
+{- -- Don't work, and I don't think it ever will.
 k' : [A:Type] -> (x:A) -> (p : x = x) -> (p = Refl)
 k' = \ [A] x p . 
-      j [A] [\ x y p . p = Refl] x x Refl
+      j [A] [\ x y p . p = Refl] x x Refl
+-}

main/pi/Hw1.pi

@@ -1,7 +1,7 @@
 module Hw1 where
 
 -- HW #1: get this file to type check by adding typing rules
--- for booleans and let expressions to TypeCheck.hs in 'version1'
+-- for booleans and products to TypeCheck.hs in 'version1'
 
 -- prelude operations on boolean values
 
@@ -18,7 +18,7 @@ eq_bool : Bool -> Bool -> Bool
 eq_bool = \ b1 b2 . 
   if b1 then b2 else (not b2)  
 
--- sigma types
+--- sigma types
 
 double : (A:Type) -> (x : A) -> { x : A | A }
 double = \A x. (x,x) 

main/pi/Lec1.pi

@@ -18,24 +18,17 @@ idT = (x:Type) -> x -> x
 selfapp : idT -> idT
 selfapp = (\x.x : (idT -> idT) -> (idT -> idT)) (\x.x)
 
-{- SOLN EQUAL -}
+-- Church encoding: booleans
 
--- some Church encodings: booleans
-
-bool : Type 
-bool = (A:Type) -> A -> A -> A 
-
-true : bool
+true : (A:Type) -> A -> A -> A 
 true = \A x y. x
 
-false : bool
+false : (A:Type) -> A -> A -> A 
 false = \A x y. y
 
-cond : bool -> (x:Type) -> x -> x -> x
+cond : ((A:Type) -> A -> A -> A) -> (x:Type) -> x -> x -> x
 cond = \ b . b 
 
-{- STUBWITH -}
-
 -- void type
 
 void : Type
@@ -44,10 +37,31 @@ void = (x:Type) -> x
 -- inhabited by diverging term
 
 loop : (x:Type) -> x
-loop = loop
+loop = \x. loop x
 
 -- unit type 
 
 unit : Type
 unit = (x:Type) -> x -> x
 
+-- this code only type checks with a definition of type equality that 
+-- includes beta-equivalence/definitions (i.e. >= version2)
+
+-- Church encoding of simply-typed pairs
+{-
+
+pair : Type -> Type -> Type
+pair = \p. \q. (c: Type) -> (p -> q -> c) -> c
+
+prod : (p:Type) -> (q:Type) -> p -> q -> pair p q
+prod = \p.\q. \x.\y. \c. \f. f x y
+
+proj1 : (p:Type) -> (q:Type) -> pair p q -> p
+proj1  = \p. \q. \a. a p (\x.\y.x)
+
+proj2 : (p:Type) -> (q:Type) -> pair p q -> q
+proj2  = \p. \q. \a. a q (\x.\y.y)
+
+swap : (p:Type) -> (q:Type) -> pair p q -> pair q p
+swap = \p. \q. \a. prod q p (proj2 p q a) (proj1 p q a)
+-}

main/pi/Lec2.pi

@@ -1,24 +1,5 @@
 module Lec2 where
 
--- this code only type checks with a definition of type equality that 
--- includes definition unfolding and beta-equivalence
-
--- logical "and"
-
-and : Type -> Type -> Type
-and = \p. \q. (c: Type) -> (p -> q -> c) -> c
-
-conj : (p:Type) -> (q:Type) -> p -> q -> and p q
-conj = \p.\q. \x.\y. \c. \f. f x y
-
-proj1 : (p:Type) -> (q:Type) -> and p q -> p
-proj1  = \p. \q. \a. a p (\x.\y.x)
-
-proj2 : (p:Type) -> (q:Type) -> and p q -> q
-proj2  = \p. \q. \a. a q (\x.\y.y)
-
-and_commutes : (p:Type) -> (q:Type) -> and p q -> and q p
-and_commutes = \p. \q. \a. conj q p (proj2 p q a) (proj1 p q a)
 
 -- "large eliminations" 
 
@@ -46,7 +27,9 @@ z2 = True
 -- context-dependent. In otherwords, it should add new 
 -- definitions to the context in the true/false branches
 -- when the scrutinee is a variable
+-- (i.e. >= version3)
 
+{- 
 not : Bool -> Bool 
 not = \x. if x then False else True
 
@@ -55,6 +38,7 @@ bar = \b. if b then () else True
 
 barnot : (b : Bool) -> T (not b) 
 barnot = \b. if b then False else ()
+-}
 
 -- projections for sigma types
 

main/pi/Makefile

@@ -16,7 +16,7 @@ SHELL=/bin/bash
 PASS=Logic Equality Product Nat Fin Vec BoolLib Hw1 Hw2 FinHw \
     Lambda Lambda0 Lambda1 Lambda2 \
 	Lec1 Lec2 Lec3 Lec4 \
-	List NatChurch Product1
+	List NatChurch Product1 Lennart
 
 # TODO_FAIL are tests that *should* fail but currently pass.
 TODO_FAIL=

main/pi/NatChurch.pi

@@ -71,13 +71,13 @@ scott_three = scott_s (scott_s (scott_s scott_z))
 scott_pred : scott_nat -> scott_nat
 scott_pred = TRUSTME
 
-test1 : scott_pred scott_two = scott_one
-test1 = TRUSTME -- replace with Refl
+testNC1 : scott_pred scott_two = scott_one
+testNC1 = TRUSTME -- replace with Refl
 
 -- Now write plus: with Scott encoded nats, note that you need to use recursion.
 
 scott_plus : scott_nat -> scott_nat -> scott_nat 
 scott_plus = TRUSTME
 
-test2 : scott_plus scott_one scott_two = scott_three
-test2 = TRUSTME -- replace with Refl
+testNC2 : scott_plus scott_one scott_two = scott_three
+testNC2 = TRUSTME -- replace with Refl

version1/pi/Hw1.pi

@@ -1,7 +1,7 @@
 module Hw1 where
 
 -- HW #1: get this file to type check by adding typing rules
--- for booleans and let expressions to TypeCheck.hs in 'version1'
+-- for booleans and products to TypeCheck.hs in 'version1'
 
 -- prelude operations on boolean values
 
@@ -18,7 +18,7 @@ eq_bool : Bool -> Bool -> Bool
 eq_bool = \ b1 b2 . 
   if b1 then b2 else (not b2)  
 
--- sigma types
+--- sigma types
 
 double : (A:Type) -> (x : A) -> { x : A | A }
 double = \A x. (x,x)