use unbound's instantiate

full/README.md

@@ -16,7 +16,7 @@ each other.
 Installation
 ----------
 
-  Compiling pi-forall requires GHC and cabal or stack
+  Compiling pi-forall requires GHC and stack
 
   Recommended tools (see links for instructions):
 
@@ -48,6 +48,19 @@ Each implementation has the following structure:
 
 ```
 
+To build each version, go to that directory and type:
+
+```
+stack build
+```
+
+and to typecheck a source file:
+
+```
+stack exec -- pi-forall <sourcefile>
+```
+
+
 Acknowledgement
 ---------------
 

full/pi/Equality.pi

@@ -99,7 +99,7 @@ k = \ [A][x] p .
 k2 : [A:Type] -> [x:A] -> [P : (x = x) -> Type] -> P Refl -> (h:x = x) -> P h
 k2 = \ [A][x][P] d h . subst d by h
 
--- here's another version of j
+-- here's j
 -- https://ncatlab.org/nlab/show/identity+type#ExplicitDefinition
 
 j : [A:Type]
@@ -108,10 +108,10 @@ j : [A:Type]
   -> (x:A) -> (y:A) -> (p : x = y) -> C x y p
 j = \[A][C] t x y p . subst (t x) by p
 
--- Can we use this version of j to derive k ? 
--- I don't think so. At least not without some 
--- form of heterogenous equality
+-- Can't derive k from j 
 
+{- -- Doesn't type check
 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
+-}

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 products to TypeCheck.hs in 'version1'
+-- for booleans and sigma types to TypeCheck.hs in 'version1'
 
 -- prelude operations on boolean values
 

full/pi/Hw2.pi

@@ -20,7 +20,7 @@ neg = \ A . ( (A) -> void )
 not : Bool -> Bool 
 not = \ x . if x then False else True
 
--- to be or not to be, that is the question
+-- show that true is not false
 
 not_not_equal : (b : Bool) -> (b = not b) -> void
 not_not_equal = \b pf. 
@@ -31,7 +31,7 @@ not_false_then_true : (b : Bool) -> neg (b = False) -> b = True
 not_false_then_true = \b nb. 
   if b then Refl else nb Refl (b = True) 
 
--- showing that decidable equality for booleans is correct.
+-- show that decidable equality for booleans is correct.
 
 eq_bool : Bool -> Bool -> Bool
 eq_bool = \x y. if x then y else not y

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

full/src/Equal.hs

@@ -187,7 +187,7 @@ whnf (App t1 t2) = do
   nf <- whnf t1 
   case nf of 
     (Lam ep  bnd) -> do
-      whnf (Unbound.substBind bnd (unArg t2) )
+      whnf (Unbound.instantiate bnd [unArg t2] )
     _ -> do
       return (App nf t2)
 
@@ -201,8 +201,7 @@ whnf (LetPair a bnd) = do
   nf <- whnf a 
   case nf of 
     Prod b1 c -> do
-      ((x,y), body) <- Unbound.unbind bnd
-      whnf (Unbound.substs [(x, b1), (y, c)] body)
+      whnf (Unbound.instantiate bnd [b1, c])
     _ -> return (LetPair nf bnd)
 
 -- ignore/remove type annotations and source positions when normalizing  
@@ -211,7 +210,7 @@ whnf (Pos _ tm) = whnf tm
 
 whnf (Let rhs bnd)  = do
   -- (x,body) <- Unbound.unbind bnd
-  whnf (Unbound.substBind bnd rhs)  
+  whnf (Unbound.instantiate bnd [rhs])  
 whnf (Subst tm pf) = do
   pf' <- whnf pf
   case pf' of 

full/src/Syntax.hs

@@ -401,7 +401,7 @@ instance Unbound.Alpha SourcePos where
   acompare' _ _ _ = EQ
 
 -- Substitutions ignore source positions
-instance Unbound.Subst b SourcePos where subst _ _ = id; substs _ = id; substPat _ _ = id
+instance Unbound.Subst b SourcePos where subst _ _ = id; substs _ = id; substBvs _ _ = id
 
 -- Internally generated source positions
 internalPos :: SourcePos

full/src/TypeCheck.hs

@@ -83,7 +83,7 @@ tcTerm (App t1 t2) Nothing = do
   -- if the argument is Irrelevant, resurrect the context
   (if ep1 == Irr then Env.extendCtx (Demote Rel) else id) $ 
     checkType (unArg t2) tyA
-  return (Unbound.substBind bnd (unArg t2))
+  return (Unbound.instantiate bnd [unArg t2])
 
 
 -- i-ann

full/stack.yaml

@@ -6,7 +6,7 @@ packages:
 
 extra-deps:
 - git: [email protected]:lambdageek/unbound-generics.git
-  commit: 04f940740d95aecd105fd87ed9f49ee0b81da408 
+  commit: a2a558058012b09bb313b3eb03cddb734fcf4a98
 
 
 flags: {}

main/pi/Equality.pi

@@ -99,7 +99,7 @@ k = \ [A][x] p .
 k2 : [A:Type] -> [x:A] -> [P : (x = x) -> Type] -> P Refl -> (h:x = x) -> P h
 k2 = \ [A][x][P] d h . subst d by h
 
--- here's another version of j
+-- here's j
 -- https://ncatlab.org/nlab/show/identity+type#ExplicitDefinition
 
 j : [A:Type]
@@ -108,11 +108,9 @@ j : [A:Type]
   -> (x:A) -> (y:A) -> (p : x = y) -> C x y p
 j = \[A][C] t x y p . subst (t x) by p
 
--- Can we use this version of j to derive k ? 
--- I don't think so. At least not without some 
--- form of heterogenous equality
+-- Can't derive k from j 
 
-{- -- Don't work, and I don't think it ever will.
+{- -- Doesn't type check
 k' : [A:Type] -> (x:A) -> (p : x = x) -> (p = Refl)
 k' = \ [A] x p . 
       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 products to TypeCheck.hs in 'version1'
+-- for booleans and sigma types to TypeCheck.hs in 'version1'
 
 -- prelude operations on boolean values
 

main/pi/Hw2.pi

@@ -20,7 +20,7 @@ neg = \ A . ( (A) -> void )
 not : Bool -> Bool 
 not = \ x . if x then False else True
 
--- to be or not to be, that is the question
+-- show that true is not false
 
 not_not_equal : (b : Bool) -> (b = not b) -> void
 not_not_equal = {- SOLN DATA -} \b pf. 
@@ -31,7 +31,7 @@ not_false_then_true : (b : Bool) -> neg (b = False) -> b = True
 not_false_then_true = {- SOLN DATA -} \b nb. 
   if b then Refl else nb Refl (b = True) {- STUBWITH TRUSTME -}
 
--- showing that decidable equality for booleans is correct.
+-- show that decidable equality for booleans is correct.
 
 eq_bool : Bool -> Bool -> Bool
 eq_bool = \x y. if x then y else not y

version1/README.md

@@ -16,7 +16,7 @@ each other.
 Installation
 ----------
 
-  Compiling pi-forall requires GHC and cabal or stack
+  Compiling pi-forall requires GHC and stack
 
   Recommended tools (see links for instructions):
 
@@ -48,6 +48,19 @@ Each implementation has the following structure:
 
 ```
 
+To build each version, go to that directory and type:
+
+```
+stack build
+```
+
+and to typecheck a source file:
+
+```
+stack exec -- pi-forall <sourcefile>
+```
+
+
 Acknowledgement
 ---------------
 

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 products to TypeCheck.hs in 'version1'
+-- for booleans and sigma types to TypeCheck.hs in 'version1'
 
 -- prelude operations on boolean values
 

version1/src/Equal.hs

@@ -106,7 +106,7 @@ whnf (App t1 t2) = do
   nf <- whnf t1
   case nf of
     (Lam bnd) -> do
-      whnf (Unbound.substBind bnd t2)
+      whnf (Unbound.instantiate bnd [t2])
     _ -> do
       return (App nf t2)
 whnf (If t1 t2 t3) = do
@@ -118,8 +118,7 @@ whnf (LetPair a bnd) = do
   nf <- whnf a
   case nf of
     Prod b1 c -> do
-      ((x, y), body) <- Unbound.unbind bnd
-      whnf (Unbound.substs [(x, b1), (y, c)] body)
+      whnf (Unbound.instantiate bnd [b1, c])
     _ -> return (LetPair nf bnd)
 
 -- ignore/remove type annotations and source positions when normalizing

version1/src/Syntax.hs

@@ -243,7 +243,7 @@ instance Unbound.Alpha SourcePos where
   acompare' _ _ _ = EQ
 
 -- Substitutions ignore source positions
-instance Unbound.Subst b SourcePos where subst _ _ = id; substs _ = id; substPat _ _ = id
+instance Unbound.Subst b SourcePos where subst _ _ = id; substs _ = id; substBvs _ _ = id
 
 -- Internally generated source positions
 internalPos :: SourcePos

version1/src/TypeCheck.hs

@@ -67,7 +67,7 @@ tcTerm (App t1 t2) Nothing = do
       ensurePi ty = Env.err [DS "Expected a function type but found ", DD ty]
   (tyA, bnd) <- ensurePi ty1
   checkType t2 tyA
-  return (Unbound.substBind bnd t2)
+  return (Unbound.instantiate bnd [t2])
 
 -- i-ann
 tcTerm (Ann tm ty) Nothing = do
@@ -85,20 +85,12 @@ tcTerm TrustMe (Just ty) = return ty
 tcTerm TyUnit Nothing = return Type
 tcTerm LitUnit Nothing = return TyUnit
 -- i-bool
-tcTerm TyBool Nothing = return Type
+tcTerm TyBool Nothing = Env.err [DS "unimplemented"]
 -- i-true/false
-tcTerm (LitBool b) Nothing = return TyBool
+tcTerm (LitBool b) Nothing = Env.err [DS "unimplemented"]
 -- c-if
-tcTerm t@(If t1 t2 t3) mty = do
-  checkType t1 TyBool  
-  ty <- inferType t2 
-  checkType t3 ty
-  return ty
-tcTerm (Let rhs bnd) mty = do
-  ty <- inferType rhs
-  (x,body) <- Unbound.unbind bnd
-  Env.extendCtx (mkSig x ty) $ tcTerm body mty
-
+tcTerm t@(If t1 t2 t3) mty = Env.err [DS "unimplemented"]
+tcTerm (Let rhs bnd) mty = Env.err [DS "unimplemented"]
 tcTerm t@(Sigma tyA bnd) Nothing = Env.err [DS "unimplemented"]
 tcTerm t@(Prod a b) (Just ty) = Env.err [DS "unimplemented"]
 tcTerm t@(LetPair p bnd) (Just ty) = Env.err [DS "unimplemented"]

version1/stack.yaml

@@ -6,7 +6,7 @@ packages:
 
 extra-deps:
 - git: [email protected]:lambdageek/unbound-generics.git
-  commit: 04f940740d95aecd105fd87ed9f49ee0b81da408 
+  commit: a2a558058012b09bb313b3eb03cddb734fcf4a98
 
 
 flags: {}

version2/README.md

@@ -16,7 +16,7 @@ each other.
 Installation
 ----------
 
-  Compiling pi-forall requires GHC and cabal or stack
+  Compiling pi-forall requires GHC and stack
 
   Recommended tools (see links for instructions):
 
@@ -48,6 +48,19 @@ Each implementation has the following structure:
 
 ```
 
+To build each version, go to that directory and type:
+
+```
+stack build
+```
+
+and to typecheck a source file:
+
+```
+stack exec -- pi-forall <sourcefile>
+```
+
+
 Acknowledgement
 ---------------
 

version2/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 products to TypeCheck.hs in 'version1'
+-- for booleans and sigma types to TypeCheck.hs in 'version1'
 
 -- prelude operations on boolean values
 

version2/pi/Hw2.pi

@@ -19,7 +19,7 @@ neg = \ A . ( (A) -> void )
 not : Bool -> Bool 
 not = \ x . if x then False else True
 
--- to be or not to be, that is the question
+-- show that true is not false
 
 not_not_equal : (b : Bool) -> (b = not b) -> void
 not_not_equal = TRUSTME
@@ -28,7 +28,7 @@ not_not_equal = TRUSTME
 not_false_then_true : (b : Bool) -> neg (b = False) -> b = True
 not_false_then_true = TRUSTME
 
--- showing that decidable equality for booleans is correct.
+-- show that decidable equality for booleans is correct.
 
 eq_bool : Bool -> Bool -> Bool
 eq_bool = \x y. if x then y else not y

version2/src/Equal.hs

@@ -139,7 +139,7 @@ whnf (App t1 t2) = do
   nf <- whnf t1 
   case nf of 
     (Lam  bnd) -> do
-      whnf (Unbound.substBind bnd t2)
+      whnf (Unbound.instantiate bnd [t2])
     _ -> do
       return (App nf t2)
 
@@ -153,8 +153,7 @@ whnf (LetPair a bnd) = do
   nf <- whnf a 
   case nf of 
     Prod b1 c -> do
-      ((x,y), body) <- Unbound.unbind bnd
-      whnf (Unbound.substs [(x, b1), (y, c)] body)
+      whnf (Unbound.instantiate bnd [b1, c])
     _ -> return (LetPair nf bnd)
 
 -- ignore/remove type annotations and source positions when normalizing  
@@ -163,7 +162,7 @@ whnf (Pos _ tm) = whnf tm
 
 whnf (Let rhs bnd)  = do
   -- (x,body) <- Unbound.unbind bnd
-  whnf (Unbound.substBind bnd rhs)  
+  whnf (Unbound.instantiate bnd [rhs])  
 whnf (Subst tm pf) = do
   pf' <- whnf pf
   case pf' of 

version2/src/Syntax.hs

@@ -266,7 +266,7 @@ instance Unbound.Alpha SourcePos where
   acompare' _ _ _ = EQ
 
 -- Substitutions ignore source positions
-instance Unbound.Subst b SourcePos where subst _ _ = id; substs _ = id; substPat _ _ = id
+instance Unbound.Subst b SourcePos where subst _ _ = id; substs _ = id; substBvs _ _ = id
 
 -- Internally generated source positions
 internalPos :: SourcePos