Commits

maloneymr committed c6c94aa

Change ty to return Just Term, add tyof to find the type of a typeable term, add inhabits to demonstrate a term inhabits a type, add proof that 1+1=2

Comments (0)

Files changed (1)

 cTy "Refl" = Forall (Star 0) (Forall (Var 0) (Const "Eq" `App` Var 1 `App` Var 0 `App` Var 0))
 cTy _ = error "Undefined constant"
 
-ty :: Term -> Term    
+ty :: Term -> Maybe Term    
 ty = ty' []
 
-ty' :: Ctx -> Term -> Term
-ty' ctx (Star n) = Star (n+1)
-ty' ctx (Lam t b) = 
-    let ctx' = t : ctx in
-    Forall t (ty' ctx' b)
-ty' ctx (Forall t b) = 
-    let ctx' = t : ctx in
-    let Star tn = ty' ctx t in
-    let Star bn = ty' ctx' b in
-    if tn == bn then Star tn else error "Mismatched universes"
-ty' ctx (Var i) = ctx !! i
-ty' ctx (App f a) = 
-    let Forall t b = ty' ctx f in
-    let t' = ty' ctx a in
-    if t `eq` t' then norm (sub 0 a b) else error "Invalid argument to function"
-ty' ctx (Const name) = cTy name
+ty' :: Ctx -> Term -> Maybe Term
+ty' ctx (Star n) = Just $ Star (n+1)
+ty' ctx (Lam t b) = do
+    let ctx' = t : ctx 
+    bt <- ty' ctx' b
+    Just $ Forall t bt
+ty' ctx (Forall t b) = do
+    let ctx' = t : ctx 
+    case ty' ctx t of
+        Just (Star tn) -> case ty' ctx' b of
+            Just (Star bn) -> if tn == bn then Just $ Star tn else Nothing
+            otherwise -> Nothing
+        otherwise -> Nothing
+ty' ctx (Var i) = if i < length ctx then Just $ ctx !! i else Nothing
+ty' ctx (App f a) = do
+    ft <- ty' ctx f
+    case norm ft of 
+        Forall t b -> do
+                t' <- ty' ctx a
+                if norm t `eq` norm t' then Just $ sub 0 a b else Nothing
+        otherwise -> Nothing
+
+ty' ctx (Const name) = Just $ cTy name
+
+tyof x = let Just r = ty x in r
 
 star = Star 0
 idStar = Lam star (Var 0)
 
 p :: Term -> String
 p term = case ty term of
-    Const "Nat" -> show $ toInt $ norm term
-    otherwise -> "<" ++ show (ty $ norm term) ++ ">"
+    Nothing -> error "Typecheck failure"
+    Just (Const "Nat") -> show $ toInt $ norm term
+    otherwise -> let Just t = ty term  in "<" ++ show t ++ ">"
 
 toInt :: Term -> Int
 toInt t = 
                 
 toNat :: Int -> Term
 toNat 0 = Const "Zero"
-toNat n = App (Const "Succ") $ toNat (n -1)
+toNat n = App (Const "Succ") $ toNat (n -1)
+
+inhabits :: Term -> Term -> Bool 
+inhabits e t = 
+    let Just et = ty e in
+    let Just _ = ty t in -- error if it doesn't typecheck
+    norm et == norm t
+
+one = _succ `App` _zero
+two = _succ `App` one
+three = _succ `App` two
+
+onePlusOne = plus `App` (_succ `App` _zero) `App` (_succ `App` _zero) 
+onePlusOneEqualsTwo = Const "Eq" `App` Const "Nat" `App` onePlusOne `App` two
+proofThatOnePlusOneEqualsTwo = Const "Refl" `App` Const "Nat" `App` two
+
+onePlusOneEqualsThree = Const "Eq" `App` Const "Nat" `App` onePlusOne `App` three