sigma test file

full/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 Lennart Hurkens Equal
+	List NatChurch Product1 Lennart Hurkens Equal Sigma
 
 # TODO_FAIL are tests that *should* fail but currently pass.
 TODO_FAIL=

full/pi/Sigma.pi

@@ -1,5 +1,7 @@
 module Sigma where
 
+-- Defining projection terms using pattern matching
+
 fst : (A:Type) -> (B:A -> Type) -> { x : A | B x } -> A
 fst = \A B x . let (y,z) = x in y 
 

full/src/PrettyPrint.hs

@@ -471,6 +471,9 @@ instance Display Term where
 
   display t
     | Just i <- isNumeral t = display i
+  display (TyCon n [Arg Rel a,Arg Rel (Lam Rel bnd)]) 
+    | n == sigmaName = do
+      display (TySigma a bnd)
   display (TyCon n args) = do
     p <- ask prec
     dn <- display n

main/Makefile

@@ -1,11 +1,11 @@
 SOURCES=TypeCheck.hs PrettyPrint.hs LayoutToken.hs Parser.hs Syntax.hs Environment.hs Modules.hs Arbitrary.hs Equal.hs 
 TEST_VERSION1 = Lec1.pi 
-TEST_VERSION2 = $(TEST_VERSION1) Lec2.pi Hw1.pi Hw2.pi NatChurch.pi
+TEST_VERSION2 = $(TEST_VERSION1) Lec2.pi Hw1.pi Hw2.pi NatChurch.pi Sigma.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 Fix.pi Lennart.pi Hurkens.pi Equal.pi
 SRCS=$(addprefix src/,$(SOURCES)) app/Main.hs test/Main.hs
 
-EXTRA=LICENSE README.md pi-forall.cabal stack.yaml
+EXTRA=LICENSE README.md pi-forall.cabal stack.yaml 
 
 VERSION1=$(addprefix ../version1/,$(SRCS)) $(addprefix ../version1/pi/,$(TEST_VERSION1)) ../version1/pi/Hw1.pi $(EXTRA)
 VERSION2=$(addprefix ../version2/,$(SRCS)) $(addprefix ../version2/pi/,$(TEST_VERSION2)) $(EXTRA)

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 Lennart Hurkens Equal
+	List NatChurch Product1 Lennart Hurkens Equal Sigma
 
 # TODO_FAIL are tests that *should* fail but currently pass.
 TODO_FAIL=

version2/pi/Sigma.pi

@@ -1,5 +1,7 @@
 module Sigma where
 
+-- Defining projection terms using pattern matching
+
 fst : (A:Type) -> (B:A -> Type) -> { x : A | B x } -> A
 fst = \A B x . let (y,z) = x in y 
 

version3/pi/Sigma.pi

@@ -1,5 +1,7 @@
 module Sigma where
 
+-- Defining projection terms using pattern matching
+
 fst : (A:Type) -> (B:A -> Type) -> { x : A | B x } -> A
 fst = \A B x . let (y,z) = x in y