From d7acfca7ca7e878d30c822233ea656bacdb6dc71 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Wed, 31 Mar 2021 18:55:35 -0300 Subject: [PATCH] implement composition for HITs --- intro.tt | 39 +++++++++++++-- src/Elab.hs | 10 +++- src/Elab/Eval.hs | 2 +- src/Elab/WiredIn.hs | 110 ++++++++++++++++++++++++++++------------- src/Main.hs | 9 ++-- src/Presyntax/Lexer.x | 19 ++++++- src/Presyntax/Parser.y | 24 +++++---- src/Syntax.hs | 6 +++ 8 files changed, 162 insertions(+), 57 deletions(-) diff --git a/intro.tt b/intro.tt index 3e4093c..6449b74 100644 --- a/intro.tt +++ b/intro.tt @@ -278,6 +278,9 @@ hcomp {A} {phi} u a0 = comp (\i -> A) {phi} u a0 transRefl : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p refl) p transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> y ]) (inS (p i)) (inot j) +transpFill : {A : Type} (x : A) -> Path x (transp (\i -> A) x) +transpFill {A} x i = fill (\i -> A) (\k []) (inS x) i + -- Reduction of composition --------------------------- -- @@ -623,11 +626,13 @@ notp = univalence (IsoToEquiv (not, involToIso not notInvol)) -- -- This follows from setting bottom := ∀ A, A. -bottom : Type -bottom = {A : Type} -> A +data bottom : Type where {} elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b -elimBottom P x = x +elimBottom P = \case {} + +absurd : {P : Type} -> bottom -> P +absurd = \case {} -- We prove that true != false by transporting along the path -- @@ -642,7 +647,7 @@ elimBottom P x = x -- and evaluate the if at either end. trueNotFalse : Path true false -> bottom -trueNotFalse p {A} = transp (\i -> if (Bool -> Bool) A (p i)) id +trueNotFalse p = transp (\i -> if (Bool -> Bool) bottom (p i)) id -- To be an h-Set is to have no "higher path information". Alternatively, -- @@ -823,6 +828,9 @@ helix = \case base -> Int loop i -> intPath i +loopP : Path base base +loopP i = loop i + winding : Path base base -> Int winding p = transp (\i -> helix (p i)) (pos zero) @@ -898,6 +906,9 @@ Susp_to_poSusp_to_Susp = \case unitEta : (x : Unit) -> Path x tt unitEta = \case tt -> refl +unitContr : isContr Unit +unitContr = (tt, \x -> sym (unitEta x)) + poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x poSusp_to_Susp_to_poSusp {A} = \case inl x -> cong inl (sym (unitEta x)) @@ -1023,4 +1034,22 @@ four : Int four = multInt two two sixteen : Int -sixteen = multInt four four \ No newline at end of file +sixteen = multInt four four + +isProp : Type -> Type +isProp A = (x : A) (y : A) -> Path x y + +data Sq (A : Type) : Type where + inc : A -> Sq A + sq i : (x : A) (y : A) -> Sq A [ (i = i0) -> inc x, (i = i1) -> inc y ] + +Sq_rec : {A : Type} {B : Type} + -> isProp B + -> (f : A -> B) + -> Sq A -> B +Sq_rec prop f = \case + inc x -> f x + sq x y i -> prop (f x) (f y) i + +hitTranspExample : Path (inc false) (inc true) +hitTranspExample i = transp (\i -> Sq (notp i)) (sq true false i) \ No newline at end of file diff --git a/src/Elab.hs b/src/Elab.hs index e8e74e7..e6e4aad 100644 --- a/src/Elab.hs +++ b/src/Elab.hs @@ -4,6 +4,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE EmptyCase #-} module Elab where import Control.Arrow (Arrow(first)) @@ -330,7 +331,11 @@ skipLams k = do (Lam P.Im n . ) <$> skipLams (k - 1) checkLetItems :: Map Text (Maybe (Name, NFType)) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a -checkLetItems _ [] cont = cont [] +checkLetItems map [] cont = do + for_ (Map.toList map) $ \case + (_, Nothing) -> pure () + (n, Just _) -> throwElab $ DeclaredUndefined (Bound n 0) + cont [] checkLetItems map (P.LetDecl v t:xs) cont = do t <- check t VTypeω t_nf <- eval t @@ -616,3 +621,6 @@ data UnsaturatedCon = UnsaturatedCon { theConstr :: Name } data NotACon = NotACon { theNotConstr :: Name } deriving (Show, Typeable) deriving anyclass (Exception) + +newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name } + deriving (Eq, Show, Exception) \ No newline at end of file diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs index e2a2af9..002bb0d 100644 --- a/src/Elab/Eval.hs +++ b/src/Elab/Eval.hs @@ -588,7 +588,7 @@ forceIO x = pure x force :: Value -> Value force = unsafePerformIO . forceIO -applProj :: Value -> Projection -> Value +applProj :: HasCallStack => 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 diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs index df561fb..302011d 100644 --- a/src/Elab/WiredIn.hs +++ b/src/Elab/WiredIn.hs @@ -302,10 +302,10 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = VNe (HData False _) args -> case force a0 of VNe (HCon con_type con_name) con_args -> - VNe (HCon con_type con_name) $ compConArgs (length args) (a @@) con_type con_args phi u + VNe (HCon con_type con_name) $ compConArgs makeSetFiller (length args) (a @@) con_type con_args phi u _ -> VComp a phi u (VInc (a @@ VI0) phi a0) - VNe (HData True _) args -> compHIT (length args) (a @@) phi u incA0 + VNe (HData True name) args -> compHIT name (length args) (a @@) phi u incA0 VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a)) sys@VSystem{} -> error $ "comp VSystem: " ++ show (prettyTm (quote sys)) @@ -328,50 +328,55 @@ forceAndGlue v = v@VGlueTy{} -> v y -> VGlueTy y VI1 (fun (const y)) (fun (const (idEquiv y))) -compHIT :: HasCallStack => Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value -compHIT 0 a phi u a0 = - case phi of +compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value +compHIT name n a phi u a0 = + case force phi of VI1 -> u @@ VI1 @@ VItIsOne - VI0 -> compOutS (a VI0) phi u a0 - _ -> VHComp (a VI0) phi u a0 -compHIT _ a phi u a0 = error $ unlines - [ "*** TODO: composition for HIT: " - , "domain = " ++ show (prettyTm (quote (zonk (fun a)))) - , "phi = " ++ show (prettyTm (quote (zonk phi))) - , "u = " ++ show (prettyTm (quote (zonk u))) - , "a0 = " ++ show (prettyTm (quote (zonk a0))) - ] - -compConArgs :: Int -> (NFEndp -> Value) -> Value -> Seq.Seq Projection -> NFEndp -> Value -> Seq.Seq Projection -compConArgs total_args fam = go total_args where + VI0 -> transHit name a VI0 (compOutS (a VI0) phi u a0) + x -> go n a x u a0 + where + go 0 a phi u a0 = VHComp (a VI0) phi u a0 + go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> squeezeHit name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (compOutS (a VI1) phi (u @@ VI1 @@ VItIsOne) a0)) + +compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value) + -> Int + -> (Value -> Value) + -> Value + -> Seq.Seq Projection + -> t1 -> t2 + -> Seq.Seq Projection +compConArgs makeFiller total_args fam = go total_args where go _ _ Seq.Empty _ _ = Seq.Empty go nargs (VPi p dom (Closure _ rng)) (PApp p' y Seq.:<| xs) phi u - | nargs > 0 = assert (p == p') $ go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u + | nargs > 0 = assert (p == p') $ + PApp p' (nthArg (total_args - nargs) (fam VI1)) Seq.:<| go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u | otherwise = assert (p == p') $ - let fill = makeFiller nargs dom phi u y + let fill = makeFiller typeArgument nargs dom phi u y in PApp p' (fill @@ VI1) Seq.:<| go (nargs - 1) (rng fill) xs phi u go _ _ _ _ _ = error $ "invalid constructor" - nthArg i (VNe hd s) = - case s Seq.!? i of - Just (PApp _ t) -> t - _ -> error $ "invalid " ++ show i ++ "th argument to data type " ++ show hd - nthArg i (VSystem vs) = VSystem (fmap (nthArg i) vs) - nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs)) - - makeFiller nth (VNe (HData _ n') args) phi u a0 - | n' == typeArgument = - fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0 - makeFiller _ _ _ _ a0 = fun (const a0) - - makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs - makeDomain _ = error "somebody smuggled something that smells" - smuggle x = VNe (HData False typeArgument) (Seq.singleton (PApp P.Ex x)) typeArgument = unsafePerformIO newName {-# NOINLINE typeArgument #-} +makeSetFiller :: Name -> Int -> Value -> NFEndp -> Value -> Value -> Value +makeSetFiller typeArgument nth (VNe (HData _ n') args) phi u a0 + | n' == typeArgument = + fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0 + where + makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs + makeDomain _ = error "somebody smuggled something that smells" +makeSetFiller _ _ _ _ _ a0 = fun (const a0) + +nthArg :: Int -> Value -> Value +nthArg i (VNe hd s) = + case s Seq.!? i of + Just (PApp _ t) -> t + _ -> error $ "invalid " ++ show i ++ "th argument to data type " ++ show hd +nthArg i (VSystem vs) = VSystem (fmap (nthArg i) vs) +nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs)) + compOutS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value compOutS a b c d = compOutS a b c (force d) where compOutS _ _hi _0 vl@VComp{} = vl @@ -462,6 +467,43 @@ contr a aC phi u = transp :: (NFEndp -> Value) -> Value -> Value transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0) +gtrans :: (NFEndp -> Value) -> NFEndp -> Value -> Value +gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (VInc (line VI0) VI0 a0) + +transHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> Value +transHit name line phi (VHComp _ psi u u0) = VHComp (line VI1) psi (system \i j -> transHit name line phi (u @@ i @@ j)) (transHit name line phi u0) +transHit name line phi (VNe (HCon con_type con_name) spine) | ourType = x' where + x' = VNe (HCon con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi () + (_, VNe hd (length -> nargs)) = unPi con_type + ourType = case hd of + HData True n' -> n' == name + _ -> False + +transHit name line phi (VNe (HPCon sys con_type con_name) spine) | ourType = x' where + x' = VNe (HPCon (mapVSystem rec sys) con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi () + rec = transHit name line phi + (_, VNe hd (length -> nargs)) = unPi con_type + ourType = case hd of + HData True n' -> n' == name + _ -> False + +transHit name line phi (VSystem xs) = mkVSystem (fmap (transHit name line phi) xs) +transHit _ line phi a0 = gtrans line phi a0 + +fillHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> NFEndp -> Value +fillHit name a phi a0 i = transHit name (\j -> a (iand i j)) (phi `ior` inot i) a0 where + +squeezeHit :: Name -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> NFEndp -> Value +squeezeHit name a phi x i = transHit name (\j -> a (ior i j)) (phi `ior` i) (x i) + +makeTransFiller :: Name -> Name -> p -> Value -> NFEndp -> () -> Value -> Value +makeTransFiller thedata typeArgument _ (VNe (HData _ n') args) phi () a0 + | n' == typeArgument = fun (fillHit thedata (makeDomain args) phi a0) + where + makeDomain (PApp _ x Seq.:<| xs) = \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs + makeDomain _ = error "somebody smuggled something that smells" +makeTransFiller _ _ _ _ _ _ a0 = fun (const a0) + makeEquiv :: Name -> Value -> Value makeEquiv var vne = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y) where diff --git a/src/Main.hs b/src/Main.hs index 78737e8..e298fe3 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -72,7 +72,7 @@ evalArgExpr env str = enterReplIn :: ElabEnv -> IO () enterReplIn env = runInputT defaultSettings (loop env') where - env' = env { commHook = putStrLn . show . prettyTm . quote } + env' = env { commHook = T.putStrLn . render . prettyTm . quote . zonk } loop :: ElabEnv -> InputT IO () loop env = do @@ -102,7 +102,7 @@ checkFiles files = runElab (go files ask) =<< emptyEnv where | otherwise -> let pos = fromJust (Map.lookup v (whereBound env)) - in withSpan (fst pos) (snd pos) $ throwElab $ DeclaredUndefined v + in withSpan (fst pos) (snd pos) $ throwElab $ Elab.DeclaredUndefined v _ -> pure () metas <- liftIO $ readIORef (unsolvedMetas env) @@ -182,7 +182,7 @@ displayExceptions lines = putStrLn $ "Unknown primitive: " ++ T.unpack x , Handler \(NotInScope x) -> do putStrLn $ "Variable not in scope: " ++ show (pretty x) - , Handler \(DeclaredUndefined n) -> do + , Handler \(Elab.DeclaredUndefined n) -> do putStrLn $ "Name declared but not defined: " ++ show (pretty n) ] @@ -212,9 +212,6 @@ squiggleUnder (Posn l c) (Posn l' c') file in T.unlines [ padding, line, padding <> squiggle ] | otherwise = T.unlines (take (l' - l) (drop l (T.lines file))) -newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name } - deriving (Eq, Show, Exception) - dumpTokens :: Alex () dumpTokens = do t <- alexMonadScan diff --git a/src/Presyntax/Lexer.x b/src/Presyntax/Lexer.x index 4020f03..8ba40da 100644 --- a/src/Presyntax/Lexer.x +++ b/src/Presyntax/Lexer.x @@ -7,6 +7,8 @@ import qualified Data.Text as T import Presyntax.Tokens +import Debug.Trace + } %wrapper "monadUserState-bytestring" @@ -38,7 +40,7 @@ tokens :- <0> \[ { always TokOSquare } <0> \) { always TokCParen } -<0> \} { always TokCBrace } +<0> \} { closeBrace } <0> \] { always TokCSquare } <0> \; { always TokSemi } @@ -71,6 +73,7 @@ tokens :- -- layout: indentation of the next token is context for offside rule { \n ; + \{ { openBrace } () { startLayout } } @@ -145,6 +148,20 @@ startLayout (AlexPn _ line col, _, _, _) _ = do else mapUserState $ \s -> s { layoutColumns = col:layoutColumns s } pure (Token TokLStart line col) +openBrace :: AlexInput -> Int64 -> Alex Token +openBrace (AlexPn _ line col, _, _, _) _ = do + popStartCode + mapUserState $ \s -> s { layoutColumns = minBound:layoutColumns s } + pure (Token TokOBrace line col) + +closeBrace :: AlexInput -> Int64 -> Alex Token +closeBrace (AlexPn _ line col, _, _, _) _ = do + ~(col':tail) <- layoutColumns <$> getUserState + if col' < 0 + then mapUserState $ \s -> s { layoutColumns = tail } + else pure () + pure (Token TokCBrace line col) + variableOrKeyword :: AlexAction Token variableOrKeyword (AlexPn _ l c, _, s, _) size = let text = T.decodeUtf8 (Lbs.toStrict (Lbs.take size s)) in diff --git a/src/Presyntax/Parser.y b/src/Presyntax/Parser.y index 006cbad..ede969f 100644 --- a/src/Presyntax/Parser.y +++ b/src/Presyntax/Parser.y @@ -1,5 +1,5 @@ { -{-# LANGUAGE FlexibleInstances, ViewPatterns #-} +{-# LANGUAGE FlexibleContexts, FlexibleInstances, ViewPatterns #-} module Presyntax.Parser where import qualified Data.Text as T @@ -81,7 +81,7 @@ Exp :: { Expr } Exp : '\\' LambdaList '->' Exp { span $1 $4 $ makeLams $2 $4 } | '\\' MaybeLambdaList '[' System ']' { span $1 $5 $ makeLams $2 $ LamSystem $4 } - | '\\' 'case' START CaseList END { span $1 $5 $ LamCase $4 } + | '\\' 'case' Block(CaseList) { span $1 $3 $ LamCase (thd $3) } | '(' var ':' Exp ')' ProdTail { span $1 $6 $ Pi Ex (getVar $2) $4 $6 } | '{' var ':' Exp '}' ProdTail { span $1 $6 $ Pi Im (getVar $2) $4 $6 } | ExpApp '->' Exp { span $1 $3 $ Pi Ex (T.singleton '_') $1 $3 } @@ -89,8 +89,7 @@ Exp | '(' var ':' Exp ')' '*' Exp { span $1 $7 $ Sigma (getVar $2) $4 $7 } | ExpApp '*' Exp { span $1 $3 $ Sigma (T.singleton '_') $1 $3 } - | 'let' START LetList END 'in' Exp { span $1 $6 $ Let $3 $6 } - | 'let' START LetList END Exp { span $1 $5 $ Let $3 $5 } + | 'let' Block(LetList) 'in' Exp { span $1 $4 $ Let (thd $2) $4 } | ExpApp { $1 } @@ -149,7 +148,8 @@ CaseItem :: { (Pattern, Expr) } : Pattern '->' Exp { ($1, $3) } CaseList :: { [(Pattern, Expr)] } - : CaseItem { [$1] } + : { [] } + | CaseItem { [$1] } | CaseItem Semis CaseList { $1:$3 } Pattern :: { Pattern } @@ -163,12 +163,14 @@ Statement :: { Statement } : VarList ':' Exp { spanSt $1 $3 $ Decl (thd $1) $3 } | var LhsList '=' Rhs { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) } | '{-#' Pragma '#-}' { spanSt $1 $3 $ $2 } - | 'postulate' START Postulates END { spanSt $1 $4 $ Postulate $3 } - | 'data' var Parameters ':' Exp 'where' START Constructors END - { spanSt $1 $9 $ Data (getVar $2) $3 $5 $8 } + + | 'postulate' Block(Postulates) { spanSt $1 $2 $ Postulate (thd $2) } + | 'data' var Parameters ':' Exp 'where' Block(Constructors) + { spanSt $1 $7 $ Data (getVar $2) $3 $5 (thd $7) } Constructors :: { [(Posn, Posn, Constructor)] } - : var ':' Exp { [(startPosn $1, endPosn $3, Point (getVar $1) $3)] } + : { [] } + | 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 @@ -250,6 +252,10 @@ FAtom :: { Formula } x -> parseError (x, ["i0", "i1"]) } +Block(p) + : START p END { (startPosn $1, endPosn $3, $2) } + | '{' p '}' { (startPosn $1, endPosn $3, $2) } + { lexer cont = alexMonadScan >>= cont diff --git a/src/Syntax.hs b/src/Syntax.hs index 0839188..4e531a7 100644 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -308,3 +308,9 @@ data Projection data Boundary = Boundary { getBoundaryNames :: [Name], getBoundaryMap :: Value } deriving (Eq, Show, Ord) + +unPi :: Value -> ([(Plicity, Value)], Value) +unPi (VPi p d (Closure n k)) = + let (a, x) = unPi (k (VVar n)) + in ((p, d):a, x) +unPi x = ([], x) \ No newline at end of file