diff --git a/intro.tt b/intro.tt index 69a934f..65e2fbd 100644 --- a/intro.tt +++ b/intro.tt @@ -293,6 +293,12 @@ transpFun : {A : Type} {B : Type} {C : Type} {D : Type} (p : Path A B) (q : Path (\x -> transp (\i -> q i) (f (transp (\i -> p (inot i)) x))) transpFun p q f = refl +-- transpDFun : {A : I -> Type} {B : (i : I) -> A i -> Type} +-- -> (f : (x : A i0) -> B i0 x) +-- -> Path (transp (\i -> (x : A i) -> B i x) f) +-- (\x -> transp (\i -> B i (fill (\j -> A (inot j)) (\k []) (inS x) (inot i))) (f (fill (\j -> A (inot j)) (\k []) (inS x) i1))) +-- transpDFun f = refl + -- When considering the more general case of a composition respecing sides, -- the outer transport becomes a composition. @@ -326,6 +332,9 @@ inverse eqv y = (eqv y) .1 .1 section : {A : Type} {B : Type} (f : A -> B) (eqv : isEquiv f) -> Path (\x -> f (inverse eqv x)) id section f eqv i y = (eqv y) .1 .2 i +contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> A +contr {A} {phi} p u = comp (\i -> A) {phi} (\i is1 -> p.2 (u is1) i) (inS (p.1)) + -- Proving that it's also a retraction is left as an exercise to the -- reader. We can package together a function and a proof that it's an -- equivalence to get a capital-E Equivalence. diff --git a/src/Elab.hs b/src/Elab.hs index a1408b7..0565b92 100644 --- a/src/Elab.hs +++ b/src/Elab.hs @@ -31,7 +31,7 @@ import Prettyprinter import Syntax.Pretty import Syntax -import Debug.Trace +import Syntax.Subst infer :: P.Expr -> ElabM (Term, NFType) infer (P.Span ex a b) = withSpan a b $ infer ex @@ -516,7 +516,7 @@ checkStatement (P.Data name tele retk constrs) k = markAsDef x e = e { definedNames = Set.insert x (definedNames e) } mkHead name - | any (\case { P.Path{} -> True; _ -> False}) constrs = HData True name + | any (\case { (_, _, P.Path{}) -> True; _ -> False}) constrs = HData True name | otherwise = HData False name checkTeleRetk allKan [] retk cont = do @@ -537,7 +537,7 @@ checkStatement (P.Data name tele retk constrs) k = checkCons _ _et [] k = k - checkCons n ret (P.Point x ty:xs) k = do + checkCons n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do t <- check ty VTypeω ty_nf <- eval t let @@ -548,7 +548,7 @@ checkStatement (P.Data name tele retk constrs) k = closed_nf <- eval closed defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons n ret xs k - checkCons n ret (P.Path name indices return faces:xs) k = do + checkCons n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do (con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do t <- check return VTypeω ty_nf <- eval t @@ -569,9 +569,12 @@ checkStatement (P.Data name tele retk constrs) k = faces <- envArgs args $ for faces \(f, t) -> do phi <- checkFormula f t <- check t ret - pure (quote phi, t) + pure (phi, (quote phi, t)) - system <- eval $ foldr (\x -> Lam P.Ex x) (System (Map.fromList faces)) (map (\(x, _, _) -> x) n' ++ map (\(x, _, _) -> x) args ++ indices) + system <- eval $ foldr (\x -> Lam P.Ex x) (System (Map.fromList (map snd faces))) (map (\(x, _, _) -> x) n' ++ map (\(x, _, _) -> x) args ++ indices) + + unify (foldr ior VI0 (map fst faces)) (totalProp indices) + `withNote` pretty "The formula determining the endpoints of a higher constructor must be a classical tautology" pure (ConName name 0 (length n') (length args + length indices), closed_nf, makePCon closed_nf mempty n' args indices system, Boundary indices system) defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons n ret xs k @@ -591,6 +594,9 @@ checkStatement (P.Data name tele retk constrs) k = makePCon cty sp [] ((nm, p, _):ys) zs sys con = VLam p $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp p a) [] ys zs (sys @@ a) con makePCon cty sp [] [] (nm:zs) sys con = VLam P.Ex $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp P.Ex a) [] [] zs (sys @@ a) con + totalProp (x:xs) = ior (inot (VVar x)) (VVar x) `ior` totalProp xs + totalProp [] = VI0 + evalFix :: Name -> NFType -> Term -> ElabM Value evalFix name nft term = do env <- ask diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs index 841d715..0dc4c3d 100644 --- a/src/Elab/Eval.hs +++ b/src/Elab/Eval.hs @@ -36,35 +36,12 @@ import Syntax import System.IO.Unsafe import {-# SOURCE #-} Elab.WiredIn -import Debug.Trace import Data.List (sortOn) +import Syntax.Subst eval :: Term -> ElabM Value eval t = asks (flip eval' t) -forceIO :: MonadIO m => Value -> m Value -forceIO mv@(VNe (HMeta (mvCell -> cell)) args) = do - solved <- liftIO $ readIORef cell - case solved of - Just vl -> forceIO (foldl applProj vl args) - Nothing -> pure mv -forceIO vl@(VSystem fs) = - case Map.lookup VI1 fs of - Just x -> forceIO x - Nothing -> pure vl -forceIO (GluedVl _ _ vl) = forceIO vl -forceIO (VComp line phi u a0) = comp <$> forceIO line <*> forceIO phi <*> pure u <*> pure a0 -forceIO x = pure x - -applProj :: Value -> Projection -> Value -applProj fun (PApp p arg) = vApp p fun arg -applProj fun (PIElim l x y i) = ielim l x y fun i -applProj fun (POuc a phi u) = outS a phi u fun -applProj fun PProj1 = vProj1 fun -applProj fun PProj2 = vProj2 fun - -force :: Value -> Value -force = unsafePerformIO . forceIO -- everywhere force zonkIO :: Value -> IO Value @@ -125,13 +102,6 @@ zonkSp (POuc a phi u) = POuc <$> zonkIO a <*> zonkIO phi <*> zonkIO u zonkSp PProj1 = pure PProj1 zonkSp PProj2 = pure PProj2 -mkVSystem :: Map.Map Value Value -> Value -mkVSystem vals = - let map' = Map.fromList (map (\(a, b) -> (force a, b)) (Map.toList vals)) in - case Map.lookup VI1 map' of - Just x -> x - Nothing -> VSystem (Map.filterWithKey (\k _ -> k /= VI0) map') - zonk :: Value -> Value zonk = unsafePerformIO . zonkIO @@ -232,35 +202,6 @@ evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', k):xs) evalCase _ rng sc xs = VCase (fun rng) sc xs -vApp :: HasCallStack => Plicity -> Value -> Value -> Value -vApp p (VLam p' k) arg - | p == p' = clCont k arg - | otherwise = error $ "wrong plicity " ++ show p ++ " vs " ++ show p' ++ " in app " ++ show (App p (quote (VLam p' k)) (quote arg)) -vApp p (VNe h sp) arg = VNe h (sp Seq.:|> PApp p arg) -vApp p (GluedVl h sp vl) arg = GluedVl h (sp Seq.:|> PApp p arg) (vApp p vl arg) -vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs) -vApp p (VInc (VPi _ _ (Closure _ r)) phi f) arg = VInc (r (vApp p f arg)) phi (vApp p f arg) -vApp _ x _ = error $ "can't apply " ++ show (prettyTm (quote x)) - -(@@) :: HasCallStack => Value -> Value -> Value -(@@) = vApp Ex -infixl 9 @@ - -vProj1 :: HasCallStack => Value -> Value -vProj1 (VPair a _) = a -vProj1 (VNe h sp) = VNe h (sp Seq.:|> PProj1) -vProj1 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj1) (vProj1 vl) -vProj1 (VSystem fs) = VSystem (fmap vProj1 fs) -vProj1 (VInc (VSigma a _) b c) = VInc a b (vProj1 c) -vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote x)) - -vProj2 :: HasCallStack => Value -> Value -vProj2 (VPair _ b) = b -vProj2 (VNe h sp) = VNe h (sp Seq.:|> PProj2) -vProj2 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj2) (vProj2 vl) -vProj2 (VSystem fs) = VSystem (fmap vProj2 fs) -vProj2 (VInc (VSigma _ (Closure _ r)) b c) = VInc (r (vProj1 c)) b (vProj2 c) -vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x)) data NotEqual = NotEqual Value Value deriving (Show, Typeable, Exception) @@ -386,7 +327,7 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where | otherwise = fail unify :: HasCallStack => Value -> Value -> ElabM () -unify a b = unify' a b -- `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b) +unify a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b) isConvertibleTo :: Value -> Value -> ElabM (Term -> Term) isConvertibleTo a b = isConvertibleTo (force a) (force b) where diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs index e3dfa83..1fa9ff4 100644 --- a/src/Elab/WiredIn.hs +++ b/src/Elab/WiredIn.hs @@ -25,7 +25,7 @@ import Syntax.Pretty (prettyTm) import Syntax import System.IO.Unsafe -import Debug.Trace (traceShowId, traceShow) +import Syntax.Subst wiType :: WiredIn -> NFType wiType WiType = VType @@ -211,16 +211,9 @@ outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v)) -- Composition comp :: NFLine -> NFEndp -> Value -> Value -> Value -comp a VI1 u _ - | not (isTyFam a) = u @@ VI1 @@ VItIsOne - where - isTyFam a = - case force (a @@ VI0) of - VType -> True - _ -> False - +comp _a VI1 u _a0 = u @@ VI1 @@ VItIsOne comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = - case force $ a @@ VVar (Bound (T.pack "i") 0) of + case force $ a @@ VVar (Bound (T.pack "i") (negate 1)) of VPi{} -> let plic i = let VPi p _ _ = force (a @@ i) in p @@ -240,10 +233,10 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = rng i = let VSigma _ (Closure _ r) = force (a @@ i) in r w i = fill (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) i - c1 = comp (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) + -- c1 = comp (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (VInc (rng VI0 (w VI0)) phi (vProj2 a0)) in - VPair c1 c2 + VPair (w VI1) c2 VPath{} -> let @@ -259,17 +252,16 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = , (inot j, u' i)])) (VInc (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j)) - VGlueTy{} -> + VGlueTy theBase thePhi theTypes theEquivs -> let b = u b0 = a0 - fam = a in let - base i = let VGlueTy base _ _ _ = forceAndGlue (fam @@ i) in base - phi i = let VGlueTy _ phi _ _ = forceAndGlue (fam @@ i) in phi - types i = let VGlueTy _ _ types _ = forceAndGlue (fam @@ i) in types - equivs i = let VGlueTy _ _ _ equivs = forceAndGlue (fam @@ i) in equivs + base i = substitute (Map.singleton (Bound "i" (negate 1)) i) theBase + phi i = substitute (Map.singleton (Bound "i" (negate 1)) i) thePhi + types i = substitute (Map.singleton (Bound "i" (negate 1)) i) theTypes + equivs i = substitute (Map.singleton (Bound "i" (negate 1)) i) theEquivs a i = fun \u -> unglue (base i) (phi i) (types i @@ u) (equivs i @@ u) (b @@ i @@ u) a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0 @@ -299,7 +291,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = in b1 VType -> VGlueTy a0 phi (fun \is1 -> u @@ VI1 @@ is1) - (fun \i -> mkVSystem (Map.fromList [(phi, makeEquiv (\i -> u @@ inot i @@ VItIsOne))])) + (fun \i -> mapVSystem makeEquiv (u @@ inot i @@ VItIsOne)) VNe (HData False _) args -> case force a0 of @@ -311,6 +303,10 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = _ -> VComp a phi u (VInc (a @@ VI0) phi a0) +mapVSystem :: (Value -> Value) -> Value -> Value +mapVSystem f (VSystem fs) = VSystem (fmap f fs) +mapVSystem f x = f x + forceAndGlue :: Value -> Value forceAndGlue v = case force v of @@ -357,17 +353,17 @@ compOutS :: NFSort -> NFEndp -> Value -> Value -> Value compOutS a b c d = compOutS a b c (force d) where compOutS _ _hi _0 vl@VComp{} = vl compOutS _ _hi _0 (VInc _ _ x) = x - compOutS _ _ _ v = v + compOutS a phi a0 v = outS a phi a0 v system :: (Value -> Value -> Value) -> Value -system k = fun \i -> fun \isone -> k i isone +system k = VLam P.Ex $ Closure (Bound "i" 0) \i -> VLam P.Ex $ Closure (Bound "phi" 0) \isone -> k i isone fill :: NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value fill a phi u a0 j = comp (line \i -> a @@ (i `iand` j)) (phi `ior` inot j) - (fun \i -> fun \isone -> mkVSystem (Map.fromList [ (phi, u @@ (i `iand` j) @@ isone) - , (inot j, a0)])) + (system \i isone -> mkVSystem (Map.fromList [ (phi, u @@ (i `iand` j) @@ isone) + , (inot j, outS a phi (u @@ VI0) a0)])) a0 hComp :: NFSort -> NFEndp -> Value -> Value -> Value @@ -440,9 +436,38 @@ contr a aC phi u = (system \i is1 -> ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i) (vProj1 aC) -makeEquiv :: (NFEndp -> Value) -> Value -makeEquiv line = comp (fun \i -> equiv a (line i)) VI0 (system \_ _ -> VSystem mempty) (idEquiv a) where - a = line VI0 +transp :: (NFEndp -> Value) -> Value -> Value +transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0) + +makeEquiv :: Value -> Value +makeEquiv line = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y) + where + a = line @@ VI0 + b = line @@ VI1 + + f = fun \x -> transp (line @@) x + g = fun \x -> transp ((line @@) . inot) x + u i = fun \x -> fill line VI0 (system \_ _ -> mkVSystem mempty) x i + v i = fun \x -> fill (fun ((line @@) . inot)) VI0 (system \_ _ -> mkVSystem mempty) x i + + fib y = VPair (g @@ y) (VLine b y (f @@ (g @@ y)) (fun (theta0 y VI1))) + theta0 y i j = fill line (ior j (inot j)) (system \i _ -> mkVSystem (Map.fromList [(j, v i @@ y), (inot j, u i @@ (g @@ y))])) (VInc a (ior j (inot j)) (g @@ y)) i + theta1 x beta y i j = + fill (fun ((line @@) . inot)) + (ior j (inot j)) + (system \i _ -> mkVSystem (Map.fromList [ (inot j, v (inot i) @@ y) + , (j, u (inot i) @@ x)])) + (VInc b (ior j (inot j)) (ielim b y (f @@ x) beta y)) + (inot i) + omega x beta y = theta1 x beta y VI0 + delta x beta y j k = comp line (ior k (ior (inot k) (ior j (inot j)))) + (system \i _ -> mkVSystem (Map.fromList [ (inot k, theta0 y i j) + , (k, theta1 x beta y i j) + , (inot j, v i @@ y) + , (j, u i @@ omega x beta y k)])) + (VInc a (ior k (ior (inot k) (ior j (inot j)))) (omega x beta y (iand j k))) + p x beta y = VLine (exists a \x -> VPath b y (f @@ x)) (fib y) (VPair x beta) $ fun \k -> + VPair (omega x beta y k) (VLine (VPath b y (f @@ x)) (vProj2 (fib y)) beta $ fun \j -> delta x beta y j k) idEquiv :: NFSort -> Value idEquiv a = VPair idfun idisequiv where @@ -453,4 +478,4 @@ idEquiv a = VPair idfun idisequiv where VLine (fun (const a)) y (vProj1 u) $ fun \j -> ielim (fun (const a)) y y (vProj2 u) (iand i j) - id_fiber y = VPair y (VLine a y y (fun (const y))) \ No newline at end of file + id_fiber y = VPair y (VLine a y y (fun (const y))) diff --git a/src/Elab/WiredIn.hs-boot b/src/Elab/WiredIn.hs-boot index 9b20dad..57cbe52 100644 --- a/src/Elab/WiredIn.hs-boot +++ b/src/Elab/WiredIn.hs-boot @@ -1,8 +1,9 @@ module Elab.WiredIn where -import Syntax import GHC.Stack.Types +import Syntax + wiType :: WiredIn -> NFType wiValue :: WiredIn -> NFType diff --git a/src/Presyntax/Parser.y b/src/Presyntax/Parser.y index d77ccce..006cbad 100644 --- a/src/Presyntax/Parser.y +++ b/src/Presyntax/Parser.y @@ -167,12 +167,12 @@ Statement :: { Statement } | 'data' var Parameters ':' Exp 'where' START Constructors END { spanSt $1 $9 $ Data (getVar $2) $3 $5 $8 } -Constructors :: { [Constructor] } - : var ':' Exp { [Point (getVar $1) $3] } - | var PatVarList ':' Exp '[' Faces ']' { [Path (getVar $1) (thd $2) $4 $6] } - | var ':' Exp Semis Constructors { Point (getVar $1) $3:$5 } +Constructors :: { [(Posn, Posn, Constructor)] } + : var ':' Exp { [(startPosn $1, endPosn $3, Point (getVar $1) $3)] } + | var PatVarList ':' Exp '[' Faces ']' { [(startPosn $1, endPosn $7, Path (getVar $1) (thd $2) $4 $6)] } + | var ':' Exp Semis Constructors { (startPosn $1, endPosn $3, Point (getVar $1) $3):$5 } | var PatVarList ':' Exp '[' Faces ']' Semis Constructors - { Path (getVar $1) (thd $2) $4 $6:$9 } + { (startPosn $1, endPosn $7, Path (getVar $1) (thd $2) $4 $6):$9 } Parameters :: { [(Text, Plicity, Expr)] } : {- empty -} { [] } diff --git a/src/Presyntax/Presyntax.hs b/src/Presyntax/Presyntax.hs index e5cd810..9a49b61 100644 --- a/src/Presyntax/Presyntax.hs +++ b/src/Presyntax/Presyntax.hs @@ -60,7 +60,7 @@ data Statement | ReplNf Expr -- REPL eval | ReplTy Expr -- REPL :t - | Data Text [(Text, Plicity, Expr)] Expr [Constructor] + | Data Text [(Text, Plicity, Expr)] Expr [(Posn, Posn, Constructor)] | SpanSt Statement Posn Posn deriving (Eq, Show, Ord) diff --git a/src/Syntax.hs b/src/Syntax.hs index 2cb7af7..fc23d66 100644 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -212,7 +212,7 @@ quoteWith names (GluedVl h sp (VLam p (Closure n k))) = quoteWith names (GluedVl h sp vl) | GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner) - | alwaysShort vl = quoteWith names vl + | True || alwaysShort vl = quoteWith names vl | otherwise = quoteWith names (VNe h sp) quoteWith names (VLam p (Closure n k)) = @@ -307,4 +307,4 @@ data Projection deriving (Eq, Show, Ord) data Boundary = Boundary { getBoundaryNames :: [Name], getBoundaryMap :: Value } - deriving (Eq, Show, Ord) \ No newline at end of file + deriving (Eq, Show, Ord) diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs index 3812da2..7accd4c 100644 --- a/src/Syntax/Pretty.hs +++ b/src/Syntax/Pretty.hs @@ -74,6 +74,8 @@ prettyTm = prettyTm . everywhere (mkT beautify) where prettyTm (IOr x y) = parens $ prettyTm x <+> operator (pretty "||") <+> prettyTm y prettyTm (INot x) = operator (pretty '~') <> prettyTm x + prettyTm (System (Map.null -> True)) = braces mempty + prettyTm (System xs) = braces (line <> indent 2 (vcat (punctuate comma (map go (Map.toList xs)))) <> line) where go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t @@ -92,7 +94,7 @@ prettyTm = prettyTm . everywhere (mkT beautify) where beautify (IElim _ _ _ f i) = App Ex f i beautify (PathIntro _ _ _ f) = f - beautify (App p (Lam p' v b) _) + beautify (App _ (Lam _ v b) _) | v `Set.notMember` freeVars b = beautify b beautify (IsOne phi) = toFun "IsOne" [phi] @@ -101,6 +103,9 @@ prettyTm = prettyTm . everywhere (mkT beautify) where beautify (Lam Ex v (App Ex f (Ref v'))) | v == v', v `Set.notMember` freeVars f = f + beautify (Comp a I0 (System (Map.null -> True)) a0) = toFun "transp" [a, a0] + beautify (Lam _ _ (Lam _ _ (System (Map.null -> True)))) = System mempty + beautify (Partial phi a) = toFun "Partial" [phi, a] beautify (PartialP phi a) = toFun "PartialP" [phi, a] beautify (Comp a phi u a0) = toFun "comp" [a, phi, u, a0] @@ -109,7 +114,9 @@ prettyTm = prettyTm . everywhere (mkT beautify) where beautify (Inc _ _ u) = toFun "inS" [u] beautify (Ouc a phi u u0) = toFun "outS" [a, phi, u, u0] - -- beautify (GlueTy a I1 _ _) = a + + + beautify (GlueTy a I1 _ _) = a beautify (GlueTy a b c d) = toFun "Glue" [a,b,c,d] beautify (Glue a b c d e f) = toFun "glue" [a,b,c,d,e,f] beautify (Unglue a b c d e) = toFun "unglue" [a,b,c,d,e]