Add a sort Typew of non-Kan types

3 years ago · 842f55db1b
--- a/src/Elab.hs
+++ b/src/Elab.hs
@ -64,7 +64,7 @@ check env (P.Lam s b) expected = do
 pure (PathI (quote a) (quote x) (quote y) s bd)

 check env (P.Let v t d b) expected = do
 ty <- check env t VType
 ty <- check env t VTypeω
 let ty' = eval env ty
 d <- check env d ty'
 let d' = eval env d
@ -84,7 +84,7 @@ check env (P.Partial fs) ty = do
 let ourFaces = Systems.faces formula
 extentFaces = Systems.faces extent

 unless (formula == extent) $
 unless (toDNF formula == toDNF extent) $
 throwIO $ IncompleteSystem formula extent

 let range = formulaToTm $ toDNF formula
@ -164,21 +164,35 @@ infer env (P.App f x) = do
 pure (PathP (quote a) (quote ai0) (quote ai1) fun arg, a @@ arg')

 infer env (P.Pi s d r) = do
 dom <- check env d VType
 (dom, ty) <- infer env d
 case ty of
 VType -> pure VType
 VTypeω -> pure VTypeω
 _ -> throwIO . UnifyError $ NotSort ty
 let d' = eval env dom
 rng <- check env { names = Map.insert s (d', VVar s) (names env) } r VType
 pure (Pi s dom rng, VType)
 (rng, rng_t) <- infer env { names = Map.insert s (d', VVar s) (names env) } r
 case ty of
 VType -> pure VType
 VTypeω -> pure VTypeω
 _ -> throwIO . UnifyError $ NotSort ty
 pure (Pi s dom rng, rng_t)

 infer env (P.Sigma s d r) = do
 dom <- check env d VType
 (dom, ty) <- infer env d
 rng_t <-
 case ty of
 VType -> pure VType
 VTypeω -> pure VTypeω
 _ -> throwIO . UnifyError $ NotSort ty
 let d' = eval env dom
 rng <- check env { names = Map.insert s (d', VVar s) (names env) } r VType
 pure (Sigma s dom rng, VType)
 rng <- check env { names = Map.insert s (d', VVar s) (names env) } r rng_t
 pure (Sigma s dom rng, rng_t)

 infer env P.Type = pure (Type, VType)
 infer env P.I = pure (I, VType)
 infer env P.I0 = pure (I0, VI)
 infer env P.I1 = pure (I1, VI)
 infer env P.Type = pure (Type, VType)
 infer env P.Typeω = pure (Typeω, VTypeω)
 infer env P.I = pure (I, VTypeω)
 infer env P.I0 = pure (I0, VI)
 infer env P.I1 = pure (I1, VI)

 infer env (P.Cut e t) = do
 t <- check env t VType
@ -211,7 +225,7 @@ infer env P.PartialT = do
 Lam "A" Type $
 Partial (Var "r") (Var "A")
 , VPi "I" VI \i ->
 VPi "A" VType (const VType))
 VPi "A" VType (const VTypeω))

 infer env P.Comp = do
 let u_t a r = VPi "i" VI \i -> VPartial r (a @@ i)
@ -244,7 +258,7 @@ infer env (P.INot x) = (, VI) . INot <$> check env x VI
 infer env P.Lam{} = error "can't infer type for lambda"

 infer env (P.Let v t d b) = do
 ty <- check env t VType
 ty <- check env t VTypeω
 let ty' = eval env ty
 d <- check env d ty'
 let d' = eval env d
@ -285,4 +299,4 @@ checkFormula env (P.Is1 x) =
 Nothing -> throwIO (NotInScope x)

 index_t :: Value
 index_t = VPi "_" VI (const VType)
 index_t = VPi "_" VI (const VTypeω)
--- a/src/Eval.hs
+++ b/src/Eval.hs
@ -49,6 +49,7 @@ VNe hd xs @@ vl = VNe hd (PApp vl:xs)
 VLam _ _ k @@ vl = k vl
 VEqGlued a b @@ vl = VEqGlued (a @@ vl) (b @@ vl)
 VOfSub a phi u0 x @@ vl = x @@ vl
 VSystem fs @@ vl = mapVSystem (VSystem fs) (@@ vl)
 f @@ _ = error $ "can't apply argument to " ++ show f

 proj1 :: Value -> Value
@ -81,7 +82,7 @@ pathp env p x y (VNe hd sp) i =
 pathp env p x y (VOfSub _ _ _ v) i = pathp env p x y v i

 comp :: Env -> Value -> Formula -> Value -> Value -> Value
 comp env a@(VLam ivar VI fam) phi u a0 = go (fam undefined) phi u a0 where
 comp env a@(VLam ivar VI fam) phi u a0 = go (fam (VVar "woopsie")) phi u a0 where
 i = VVar ivar
 stuck :: Value
 stuck = maybeAddEq $ VComp a (toValue phi) u a0
@ -96,14 +97,14 @@ comp env a@(VLam ivar VI fam) phi u a0 = go (fam undefined) phi u a0 where
 go VPi{} phi u a0 =
 let
 dom x = let VPi _ d _ = fam x in d
 rng x = let VPi _ d _ = fam x in d
 rng x = let VPi _ _ r = fam x in r

 ai1 = dom VI0
 y' i y = fill env i (dom . inot . fam) P.Bot (VSystem emptySystem) y
 y' i y = fill env i (dom . inot) P.Bot (VSystem emptySystem) y
 ybar i y = y' (inot i) y
 in VLam "x" ai1 \arg ->
 comp env
 (VLam ivar VI (\i -> rng (ybar i arg)))
 (VLam ivar VI (\i -> rng i (ybar i arg)))
 phi
 (VLam "i" VI \i -> mapVSystem (u @@ i) (@@ ybar i arg)) 
 (a0 @@ ybar VI0 arg)
@ -138,8 +139,10 @@ comp env a@(VLam ivar VI fam) phi u a0 = go (fam undefined) phi u a0 where
 let
 VSystem (FMap sys) = p @@ v
 sys' = fmap (flip (pathp env ai0 u0 v0) j) sys
 in mkVSystem $ Map.fromList [(phi, mapVSystem (p @@ v) (flip (pathp env ai0 u0 v0) j))
 , (notFormula jc, u' v), (jc, v' v)])
 in mkVSystem $ Map.fromList [ (phi, mapVSystem (p @@ v) (flip (pathp env ai0 u0 v0) j))
 , (notFormula jc, u' v)
 , (jc, v' v)
 ])
 (pathp env (ai0 @@ VI0) u0 v0 p0 j)

 go a P.Top u a0 = u @@ VI1
@ -250,6 +253,7 @@ data UnifyError
 | NotPiType Value
 | NotPartialType Formula Value
 | NotSigmaType Value
 | NotSort Value
 deriving (Show, Typeable, Exception)

 unify :: Env -> Value -> Value -> IO ()
@ -326,6 +330,9 @@ unify env vl (VSystem fs)
 | ((_, vl'):_) <- Map.toList (Map.filterWithKey (\f _ -> isTrue (toValue' env f)) (getSystem fs))
 = unify env vl' vl

 unify env VType VTypeω = pure ()
 unify env VTypeω VTypeω = pure ()

 unify env x y =
 case sameCube env x y of
 Just True -> pure ()
@ -418,7 +425,7 @@ fill :: Env
 fill env i a phi u a0 =
 comp env
 (VLam "j" VI \j -> a (i `iand` j))
 (phi `P.Or` ifc)
 (phi `P.Or` notFormula ifc)
 (VLam "j" VI \j ->
 mkVSystem (Map.fromList [ (phi, uiand j)
 , (notFormula ifc, a0) ]))
--- a/src/Main.hs
+++ b/src/Main.hs
@ -67,7 +67,7 @@ main = do

 repl :: IO ()
 repl = runInputT defaultSettings (go (Env mempty)) where
 go env = getInputLine "λ " >>= \case
 go env = getInputLine "> " >>= \case
 Just i | ":sq " `isPrefixOf` i -> do
 case parseString body (replicate 4 ' ' ++ drop 4 i) of
 Right exp -> 
@ -84,7 +84,7 @@ repl = runInputT defaultSettings (go (Env mempty)) where
 Right (Assume vs) ->
 let
 loop env ((v, t):vs) = do
 tm <- liftIO $ check env t VType
 tm <- liftIO $ check env t VTypeω
 let ty = eval env tm
 loop env{ names = Map.insert v (ty, VVar v) (names env) } vs
 loop env [] = go env
--- a/src/Presyntax.hs
+++ b/src/Presyntax.hs
@ -14,6 +14,7 @@ data Exp

 | Pi String Exp Exp
 | Type
 | Typeω

 | I
 | I0 | I1
--- a/src/Presyntax/Lexer.hs
+++ b/src/Presyntax/Lexer.hs
@ -12,6 +12,7 @@ data TokenClass
 | Tok_lambda

 | Tok_type
 | Tok_typeω
 | Tok_path
 | Tok_phi
 | Tok_sub
@ -178,6 +179,7 @@ lexString = go 0 0 0 where

 finishIdent c
 | T.pack "Type" == c = Tok_type
 | T.pack "Typeω" == c = Tok_typeω
 | T.pack "Path" == c = Tok_path
 | T.pack "Partial" == c = Tok_phi
 | T.pack "Sub" == c = Tok_sub
--- a/src/Syntax.hs
+++ b/src/Syntax.hs
@ -1,3 +1,4 @@
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE PatternSynonyms #-}
 module Syntax where
@ -19,7 +20,7 @@ data Term
 | Let String Term Term Term

 | Pi String Term Term
 | Type
 | Type | Typeω

 | I
 | I0 | I1
@ -110,6 +111,7 @@ instance Show Term where
 in showBinder (Pi v d r)

 Type -> showString "Type"
 Typeω -> showString "Typeω"
 I -> showChar 'I'
 I0 -> showString "i0"
 I1 -> showString "i1"
@ -129,9 +131,11 @@ instance Show Term where
 Path a x y -> showsPrec p (App (App (App (Var "Path") a) x) y)
 Sub a x y -> showsPrec p (App (App (App (Var "Sub") a) x) y)
 Partial r a -> showsPrec p (App (App (Var "Partial") r) a)
 Comp a phi u a0 -> showsPrec p (foldl App (Var "comp") [a, phi, u, a0])
 InclSub _a _phi _u0 a0 -> showsPrec p a0

 Comp a I0 (Lam _ I (System (FMap (Map.null -> True)))) a0 -> showsPrec p (foldl App (Var "transp") [a, a0])
 Comp a phi u a0 -> showsPrec p (foldl App (Var "comp") [a, phi, u, a0])

 PathI a x y s b -> showParen (p >= fun_prec) $
 showString ("λ " ++ s ++ " -> ")
 . shows b
@ -163,7 +167,7 @@ data Value
 = VNe String [Proj]
 | VLam String Value (Value -> Value)
 | VPi String Value (Value -> Value)
 | VType
 | VType | VTypeω
 | VI | VI0 | VI1
 | VEqGlued Value Value -- e which is def. eq. to e'
 | VPair Value Value
@ -207,10 +211,11 @@ quote = go mempty where
 let n = rename s scope
 in Sigma n (go scope d) (go (Set.insert n scope) (r (VVar n)))

 go scope VType = Type
 go scope VI0 = I0
 go scope VI1 = I1
 go scope VI = I
 go _ VType = Type
 go _ VI0 = I0
 go _ VI1 = I1
 go _ VI = I
 go _ VTypeω = Typeω

 go scope (VIAnd x y) = IAnd (go scope x) (go scope y)
 go scope (VIOr x y) = IOr (go scope x) (go scope y)