{-# LANGUAGE CPP #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE NondecreasingIndentation #-} -- ASR (2017-04-10). TODO: Is this option required by the final -- version of GHC 8.2.1 (it was required by the RC 1)? #if __GLASGOW_HASKELL__ >= 802 {-# OPTIONS -Wno-simplifiable-class-constraints #-} #endif {-| Primitive functions, such as addition on builtin integers. -} module Agda.TypeChecking.Primitive where import Control.Monad import Control.Monad.Reader (asks) import Control.Monad.Trans (lift) import Data.Char import Data.Either (partitionEithers) import Data.List (nub) import Data.Map (Map) import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set import Data.Maybe import Data.Monoid import Data.Traversable (traverse) import Data.Monoid (mempty) import Data.Word import Agda.Interaction.Options import qualified Agda.Interaction.Options.Lenses as Lens import Agda.Syntax.Position import Agda.Syntax.Common hiding (Nat) import Agda.Syntax.Internal import Agda.Syntax.Internal.Generic (TermLike(..)) import Agda.Syntax.Literal import Agda.Syntax.Concrete.Pretty () import Agda.Syntax.Fixity import Agda.TypeChecking.Monad hiding (getConstInfo, typeOfConst) import qualified Agda.TypeChecking.Monad as TCM import Agda.TypeChecking.Monad.Builtin import Agda.TypeChecking.Records import Agda.TypeChecking.Reduce import Agda.TypeChecking.Reduce.Monad as Reduce import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope import Agda.TypeChecking.Errors import Agda.TypeChecking.Functions import Agda.TypeChecking.Level import Agda.TypeChecking.Quote (QuotingKit, quoteTermWithKit, quoteTypeWithKit, quoteClauseWithKit, quotingKit) import Agda.TypeChecking.Pretty () -- instances only import Agda.TypeChecking.Names import Agda.TypeChecking.Warnings import Agda.Utils.Float import Agda.Utils.Functor import Agda.Utils.List import Agda.Utils.Maybe import Agda.Utils.Monad import Agda.Utils.Pretty (pretty, prettyShow) import Agda.Utils.Singleton import Agda.Utils.Size import Agda.Utils.String ( Str(Str), unStr ) import Agda.Utils.Tuple #include "undefined.h" import Agda.Utils.Impossible import Debug.Trace ------------------------------------------------------------------------ -- * Builtin Sigma ------------------------------------------------------------------------ data SigmaKit = SigmaKit { sigmaName :: QName , sigmaCon :: ConHead , sigmaFst :: QName , sigmaSnd :: QName } deriving (Eq,Show) getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit) getSigmaKit = do ms <- getBuiltinName' builtinSigma case ms of Nothing -> return Nothing Just sigma -> do def <- theDef <$> getConstInfo sigma case def of Record { recFields = [fst,snd], recConHead = con } -> do return . Just $ SigmaKit { sigmaName = sigma , sigmaCon = con , sigmaFst = unArg fst , sigmaSnd = unArg snd } _ -> __IMPOSSIBLE__ --------------------------------------------------------------------------- -- * Primitive functions --------------------------------------------------------------------------- data PrimitiveImpl = PrimImpl Type PrimFun -- Haskell type to Agda type newtype Nat = Nat { unNat :: Integer } deriving (Eq, Ord, Num, Enum, Real) -- In GHC > 7.8 deriving Integral causes an unnecessary toInteger -- warning. instance Integral Nat where toInteger = unNat quotRem (Nat a) (Nat b) = (Nat q, Nat r) where (q, r) = quotRem a b instance TermLike Nat where traverseTermM _ = pure foldTerm _ = mempty instance Show Nat where show = show . toInteger newtype Lvl = Lvl { unLvl :: Integer } deriving (Eq, Ord) instance Show Lvl where show = show . unLvl class PrimType a where primType :: a -> TCM Type instance (PrimType a, PrimType b) => PrimTerm (a -> b) where primTerm _ = unEl <$> (primType (undefined :: a) --> primType (undefined :: b)) instance PrimTerm a => PrimType a where primType _ = el $ primTerm (undefined :: a) class PrimTerm a where primTerm :: a -> TCM Term instance PrimTerm Integer where primTerm _ = primInteger instance PrimTerm Word64 where primTerm _ = primWord64 instance PrimTerm Bool where primTerm _ = primBool instance PrimTerm Char where primTerm _ = primChar instance PrimTerm Double where primTerm _ = primFloat instance PrimTerm Str where primTerm _ = primString instance PrimTerm Nat where primTerm _ = primNat instance PrimTerm Lvl where primTerm _ = primLevel instance PrimTerm QName where primTerm _ = primQName instance PrimTerm MetaId where primTerm _ = primAgdaMeta instance PrimTerm Type where primTerm _ = primAgdaTerm instance PrimTerm Fixity' where primTerm _ = primFixity instance PrimTerm a => PrimTerm [a] where primTerm _ = list (primTerm (undefined :: a)) instance PrimTerm a => PrimTerm (IO a) where primTerm _ = io (primTerm (undefined :: a)) -- From Agda term to Haskell value class ToTerm a where toTerm :: TCM (a -> Term) toTermR :: TCM (a -> ReduceM Term) toTermR = (pure .) <$> toTerm instance ToTerm Nat where toTerm = return $ Lit . LitNat noRange . toInteger instance ToTerm Word64 where toTerm = return $ Lit . LitWord64 noRange instance ToTerm Lvl where toTerm = return $ Level . Max . (:[]) . ClosedLevel . unLvl instance ToTerm Double where toTerm = return $ Lit . LitFloat noRange instance ToTerm Char where toTerm = return $ Lit . LitChar noRange instance ToTerm Str where toTerm = return $ Lit . LitString noRange . unStr instance ToTerm QName where toTerm = return $ Lit . LitQName noRange instance ToTerm MetaId where toTerm = do file <- getCurrentPath return $ Lit . LitMeta noRange file instance ToTerm Integer where toTerm = do pos <- primIntegerPos negsuc <- primIntegerNegSuc fromNat <- toTerm :: TCM (Nat -> Term) let intToTerm = fromNat . fromIntegral :: Integer -> Term let fromInt n | n >= 0 = apply pos [defaultArg $ intToTerm n] | otherwise = apply negsuc [defaultArg $ intToTerm (-n - 1)] return fromInt instance ToTerm Bool where toTerm = do true <- primTrue false <- primFalse return $ \b -> if b then true else false instance ToTerm Term where toTerm = do kit <- quotingKit; runReduceF (quoteTermWithKit kit) toTermR = do kit <- quotingKit; return (quoteTermWithKit kit) instance ToTerm Type where toTerm = do kit <- quotingKit; runReduceF (quoteTypeWithKit kit) toTermR = do kit <- quotingKit; return (quoteTypeWithKit kit) instance ToTerm ArgInfo where toTerm = do info <- primArgArgInfo vis <- primVisible hid <- primHidden ins <- primInstance rel <- primRelevant irr <- primIrrelevant return $ \ i -> info `applys` [ case getHiding i of NotHidden -> vis Hidden -> hid Instance{} -> ins , case getRelevance i of Relevant -> rel Irrelevant -> irr NonStrict -> rel ] instance ToTerm Fixity' where toTerm = (. theFixity) <$> toTerm instance ToTerm Fixity where toTerm = do lToTm <- toTerm aToTm <- toTerm fixity <- primFixityFixity return $ \ Fixity{fixityAssoc = a, fixityLevel = l} -> fixity `apply` [defaultArg (aToTm a), defaultArg (lToTm l)] instance ToTerm Associativity where toTerm = do lassoc <- primAssocLeft rassoc <- primAssocRight nassoc <- primAssocNon return $ \ a -> case a of NonAssoc -> nassoc LeftAssoc -> lassoc RightAssoc -> rassoc instance ToTerm PrecedenceLevel where toTerm = do (iToTm :: Integer -> Term) <- toTerm related <- primPrecRelated unrelated <- primPrecUnrelated return $ \ p -> case p of Unrelated -> unrelated Related n -> related `apply` [defaultArg $ iToTm n] -- | @buildList A ts@ builds a list of type @List A@. Assumes that the terms -- @ts@ all have type @A@. buildList :: TCM ([Term] -> Term) buildList = do nil' <- primNil cons' <- primCons let nil = nil' cons x xs = cons' `applys` [x, xs] return $ foldr cons nil instance ToTerm a => ToTerm [a] where toTerm = do mkList <- buildList fromA <- toTerm return $ mkList . map fromA -- From Haskell value to Agda term type FromTermFunction a = Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a) class FromTerm a where fromTerm :: TCM (FromTermFunction a) instance FromTerm Integer where fromTerm = do Con pos _ [] <- primIntegerPos Con negsuc _ [] <- primIntegerNegSuc toNat <- fromTerm :: TCM (FromTermFunction Nat) return $ \ v -> do b <- reduceB' v let v' = ignoreBlocking b arg = (<$ v') case unArg (ignoreBlocking b) of Con c ci [Apply u] | c == pos -> redBind (toNat u) (\ u' -> notReduced $ arg $ Con c ci [Apply $ ignoreReduced u']) $ \ n -> redReturn $ fromIntegral n | c == negsuc -> redBind (toNat u) (\ u' -> notReduced $ arg $ Con c ci [Apply $ ignoreReduced u']) $ \ n -> redReturn $ fromIntegral $ -n - 1 _ -> return $ NoReduction (reduced b) instance FromTerm Nat where fromTerm = fromLiteral $ \l -> case l of LitNat _ n -> Just $ fromInteger n _ -> Nothing instance FromTerm Word64 where fromTerm = fromLiteral $ \ case LitWord64 _ n -> Just n _ -> Nothing instance FromTerm Lvl where fromTerm = fromReducedTerm $ \l -> case l of Level (Max [ClosedLevel n]) -> Just $ Lvl n _ -> Nothing instance FromTerm Double where fromTerm = fromLiteral $ \l -> case l of LitFloat _ x -> Just x _ -> Nothing instance FromTerm Char where fromTerm = fromLiteral $ \l -> case l of LitChar _ c -> Just c _ -> Nothing instance FromTerm Str where fromTerm = fromLiteral $ \l -> case l of LitString _ s -> Just $ Str s _ -> Nothing instance FromTerm QName where fromTerm = fromLiteral $ \l -> case l of LitQName _ x -> Just x _ -> Nothing instance FromTerm MetaId where fromTerm = fromLiteral $ \l -> case l of LitMeta _ _ x -> Just x _ -> Nothing instance FromTerm Bool where fromTerm = do true <- primTrue false <- primFalse fromReducedTerm $ \t -> case t of _ | t =?= true -> Just True | t =?= false -> Just False | otherwise -> Nothing where a =?= b = a === b Def x [] === Def y [] = x == y Con x _ [] === Con y _ [] = x == y Var n [] === Var m [] = n == m _ === _ = False instance (ToTerm a, FromTerm a) => FromTerm [a] where fromTerm = do nil' <- primNil cons' <- primCons nil <- isCon nil' cons <- isCon cons' toA <- fromTerm fromA <- toTerm return $ mkList nil cons toA fromA where isCon (Lam _ b) = isCon $ absBody b isCon (Con c _ _)= return c isCon v = __IMPOSSIBLE__ mkList nil cons toA fromA t = do b <- reduceB' t let t = ignoreBlocking b let arg = (<$ t) case unArg t of Con c ci [] | c == nil -> return $ YesReduction NoSimplification [] Con c ci es | c == cons, Just [x,xs] <- allApplyElims es -> redBind (toA x) (\x' -> notReduced $ arg $ Con c ci (map Apply [ignoreReduced x',xs])) $ \y -> redBind (mkList nil cons toA fromA xs) (fmap $ \xs' -> arg $ Con c ci (map Apply [defaultArg $ fromA y, xs'])) $ \ys -> redReturn (y : ys) _ -> return $ NoReduction (reduced b) -- | Conceptually: @redBind m f k = either (return . Left . f) k =<< m@ redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b') redBind ma f k = do r <- ma case r of NoReduction x -> return $ NoReduction $ f x YesReduction _ y -> k y redReturn :: a -> ReduceM (Reduced a' a) redReturn = return . YesReduction YesSimplification fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a) fromReducedTerm f = return $ \t -> do b <- reduceB' t case f $ unArg (ignoreBlocking b) of Just x -> return $ YesReduction NoSimplification x Nothing -> return $ NoReduction (reduced b) fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a) fromLiteral f = fromReducedTerm $ \t -> case t of Lit lit -> f lit _ -> Nothing requireCubical :: TCM () requireCubical = do cubical <- optCubical <$> pragmaOptions unless cubical $ typeError $ GenericError "Missing option --cubical" primINeg' :: TCM PrimitiveImpl primINeg' = do requireCubical t <- elInf primInterval --> elInf primInterval return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ ts -> do case ts of [x] -> do unview <- intervalUnview' view <- intervalView' sx <- reduceB' x ix <- intervalView (unArg $ ignoreBlocking sx) let ineg :: Arg Term -> Arg Term ineg = fmap (unview . f . view) f ix = case ix of IZero -> IOne IOne -> IZero IMin x y -> IMax (ineg x) (ineg y) IMax x y -> IMin (ineg x) (ineg y) INeg x -> OTerm (unArg x) OTerm t -> INeg (Arg defaultArgInfo t) case ix of OTerm t -> return $ NoReduction [reduced sx] _ -> redReturn (unview $ f ix) _ -> __IMPOSSIBLE__ primDepIMin' :: TCM PrimitiveImpl primDepIMin' = do requireCubical t <- runNamesT [] $ nPi' "φ" (elInf $ cl primInterval) $ \ φ -> (pPi' "o" φ $ \ o -> elInf $ cl primInterval) --> elInf (cl primInterval) return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ ts -> do case ts of [x,y] -> do sx <- reduceB' x ix <- intervalView (unArg $ ignoreBlocking sx) itisone <- getTerm "primDepIMin" builtinItIsOne case ix of IZero -> redReturn =<< intervalUnview IZero IOne -> redReturn =<< (pure (unArg y) <@> pure itisone) _ -> do sy <- reduceB' y iy <- intervalView =<< reduce' =<< (pure (unArg $ ignoreBlocking sy) <@> pure itisone) case iy of IZero -> redReturn =<< intervalUnview IZero IOne -> redReturn (unArg $ ignoreBlocking sx) _ -> return $ NoReduction [reduced sx, reduced sy] _ -> __IMPOSSIBLE__ primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl primIBin unit absorber = do requireCubical t <- elInf primInterval --> elInf primInterval --> elInf primInterval return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ ts -> do case ts of [x,y] -> do sx <- reduceB' x ix <- intervalView (unArg $ ignoreBlocking sx) case ix of ix | ix ==% absorber -> redReturn =<< intervalUnview absorber ix | ix ==% unit -> return $ YesReduction YesSimplification (unArg y) _ -> do sy <- reduceB' y iy <- intervalView (unArg $ ignoreBlocking sy) case iy of iy | iy ==% absorber -> redReturn =<< intervalUnview absorber iy | iy ==% unit -> return $ YesReduction YesSimplification (unArg x) _ -> return $ NoReduction [reduced sx,reduced sy] _ -> __IMPOSSIBLE__ where (==%) IZero IZero = True (==%) IOne IOne = True (==%) _ _ = False primIMin' :: TCM PrimitiveImpl primIMin' = primIBin IOne IZero primIMax' :: TCM PrimitiveImpl primIMax' = primIBin IZero IOne imax :: HasBuiltins m => m Term -> m Term -> m Term imax x y = do x' <- x y' <- y intervalUnview (IMax (argN x') (argN y')) imin :: HasBuiltins m => m Term -> m Term -> m Term imin x y = do x' <- x y' <- y intervalUnview (IMin (argN x') (argN y')) -- ∀ {a}{c}{A : Set a}{x : A}(C : ∀ y → Id x y → Set c) → C x (conid i1 (\ i → x)) → ∀ {y} (p : Id x y) → C y p primIdJ :: TCM PrimitiveImpl primIdJ = do requireCubical t <- runNamesT [] $ hPi' "a" (el $ cl primLevel) $ \ a -> hPi' "c" (el $ cl primLevel) $ \ c -> hPi' "A" (sort . tmSort <$> a) $ \ bA -> hPi' "x" (el' a bA) $ \ x -> nPi' "C" (nPi' "y" (el' a bA) $ \ y -> (el' a $ cl primId <#> a <#> bA <@> x <@> y) --> (sort . tmSort <$> c)) $ \ bC -> (el' c $ bC <@> x <@> (cl primConId <#> a <#> bA <#> x <#> x <@> cl primIOne <@> lam "i" (\ _ -> x))) --> (hPi' "y" (el' a bA) $ \ y -> nPi' "p" (el' a $ cl primId <#> a <#> bA <@> x <@> y) $ \ p -> el' c $ bC <@> y <@> p) conidn <- getBuiltinName builtinConId conid <- primConId -- TODO make a kit return $ PrimImpl t $ primFun __IMPOSSIBLE__ 8 $ \ ts -> do unview <- intervalUnview' let imax x y = do x' <- x; y' <- y; pure $ unview (IMax (argN x') (argN y')) imin x y = do x' <- x; y' <- y; pure $ unview (IMin (argN x') (argN y')) ineg x = unview . INeg . argN <$> x mcomp <- getTerm' "primComp" case ts of [la,lc,a,x,c,d,y,eq] -> do seq <- reduceB' eq case unArg $ ignoreBlocking $ seq of (Def q [Apply la,Apply a,Apply x,Apply y,Apply phi,Apply p]) | Just q == conidn, Just comp <- mcomp -> do redReturn $ runNames [] $ do [lc,c,d,la,a,x,y,phi,p] <- mapM (open . unArg) [lc,c,d,la,a,x,y,phi,p] let w i = do [x,y,p,i] <- sequence [x,y,p,i] pure $ p `applyE` [IApply x y i] pure comp <#> (lam "i" $ \ _ -> lc) <@> (lam "i" $ \ i -> c <@> (w i) <@> (pure conid <#> la <#> a <#> x <#> (w i) <@> (phi `imax` ineg i) <@> (lam "j" $ \ j -> w $ imin i j))) <@> phi <@> (lam "i" $ \ _ -> nolam <$> d) -- TODO block <@> d _ -> return $ NoReduction $ map notReduced [la,lc,a,x,c,d,y] ++ [reduced seq] _ -> __IMPOSSIBLE__ primIdElim' :: TCM PrimitiveImpl primIdElim' = do requireCubical t <- runNamesT [] $ hPi' "a" (el $ cl primLevel) $ \ a -> hPi' "c" (el $ cl primLevel) $ \ c -> hPi' "A" (sort . tmSort <$> a) $ \ bA -> hPi' "x" (el' a bA) $ \ x -> nPi' "C" (nPi' "y" (el' a bA) $ \ y -> (el' a $ cl primId <#> a <#> bA <@> x <@> y) --> (sort . tmSort <$> c)) $ \ bC -> (nPi' "φ" (elInf $ cl primInterval) $ \ phi -> nPi' "y" (elInf $ cl primSub <#> a <@> bA <@> phi <@> (lam "o" $ const x)) $ \ y -> let pathxy = (cl primPath <#> a <@> bA <@> x <@> oucy) oucy = (cl primSubOut <#> a <#> bA <#> phi <#> (lam "o" $ const x) <@> y) reflx = (lam "o" $ \ _ -> lam "i" $ \ _ -> x) -- TODO Andrea, should block on o in nPi' "w" (elInf $ cl primSub <#> a <@> pathxy <@> phi <@> reflx) $ \ w -> let oucw = (cl primSubOut <#> a <#> pathxy <#> phi <#> reflx <@> w) in el' c $ bC <@> oucy <@> (cl primConId <#> a <#> bA <#> x <#> oucy <@> phi <@> oucw)) --> (hPi' "y" (el' a bA) $ \ y -> nPi' "p" (el' a $ cl primId <#> a <#> bA <@> x <@> y) $ \ p -> el' c $ bC <@> y <@> p) conid <- primConId sin <- primSubIn path <- primPath return $ PrimImpl t $ primFun __IMPOSSIBLE__ 8 $ \ ts -> do case ts of [a,c,bA,x,bC,f,y,p] -> do sp <- reduceB' p case unArg $ ignoreBlocking sp of Def q [Apply _a, Apply _bA, Apply _x, Apply _y, Apply phi , Apply w] -> do y' <- return $ sin `apply` [a,bA ,phi,argN $ unArg y] w' <- return $ sin `apply` [a,argN $ path `apply` [a,bA,x,y],phi,argN $ unArg w] redReturn $ unArg f `apply` [phi, defaultArg y', defaultArg w'] _ -> return $ NoReduction $ map notReduced [a,c,bA,x,bC,f,y] ++ [reduced sp] _ -> __IMPOSSIBLE__ primPOr :: TCM PrimitiveImpl primPOr = do requireCubical t <- runNamesT [] $ hPi' "a" (el $ cl primLevel) $ \ a -> nPi' "i" (elInf $ cl primInterval) $ \ i -> nPi' "j" (elInf $ cl primInterval) $ \ j -> hPi' "A" (pPi' "o" (imax i j) $ \o -> el' (cl primLevelSuc <@> a) (Sort . tmSort <$> a)) $ \ bA -> ((pPi' "i1" i $ \ i1 -> el' a $ bA <..> (cl primIsOne1 <@> i <@> j <@> i1))) --> ((pPi' "j1" j $ \ j1 -> el' a $ bA <..> (cl primIsOne2 <@> i <@> j <@> j1))) --> (pPi' "o" (imax i j) $ \ o -> el' a $ bA <..> o) return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ ts -> do case ts of [l,i,j,a,u,v] -> do si <- reduceB' i vi <- intervalView $ unArg $ ignoreBlocking si case vi of IOne -> redReturn (unArg u) IZero -> redReturn (unArg v) _ -> do sj <- reduceB' j vj <- intervalView $ unArg $ ignoreBlocking sj case vj of IOne -> redReturn (unArg v) IZero -> redReturn (unArg u) _ -> return $ NoReduction [notReduced l,reduced si,reduced sj,notReduced a,notReduced u,notReduced v] _ -> __IMPOSSIBLE__ primPartial' :: TCM PrimitiveImpl primPartial' = do requireCubical t <- runNamesT [] $ (hPi' "a" (el $ cl primLevel) $ \ a -> nPi' "φ" (elInf (cl primInterval)) $ \ _ -> nPi' "A" (sort . tmSort <$> a) $ \ bA -> return (sort $ Inf)) isOne <- primIsOne return $ PrimImpl t $ primFun __IMPOSSIBLE__ 3 $ \ ts -> do case ts of [l,phi,a] -> do (El s (Pi d b)) <- runNamesT [] $ do [l,a,phi] <- mapM (open . unArg) [l,a,phi] (elInf $ pure isOne <@> phi) --> el' l a redReturn $ Pi (setRelevance Irrelevant $ d { domFinite = True }) b _ -> __IMPOSSIBLE__ primPartialP' :: TCM PrimitiveImpl primPartialP' = do requireCubical t <- runNamesT [] $ (hPi' "a" (el $ cl primLevel) $ \ a -> nPi' "φ" (elInf (cl primInterval)) $ \ phi -> nPi' "A" (pPi' "o" phi $ \ _ -> el' (cl primLevelSuc <@> a) (Sort . tmSort <$> a)) $ \ bA -> return (sort $ Inf)) let toFinitePi :: Type -> Term toFinitePi (El _ (Pi d b)) = Pi (setRelevance Irrelevant $ d { domFinite = True }) b toFinitePi _ = __IMPOSSIBLE__ v <- runNamesT [] $ lam "a" $ \ l -> lam "φ" $ \ phi -> lam "A" $ \ a -> toFinitePi <$> nPi' "p" (elInf $ cl primIsOne <@> phi) (\ p -> el' l (a <@> p)) return $ PrimImpl t $ primFun __IMPOSSIBLE__ 0 $ \ _ -> redReturn v primSubOut' :: TCM PrimitiveImpl primSubOut' = do requireCubical t <- runNamesT [] $ hPi' "a" (el $ cl primLevel) $ \ a -> hPi' "A" (el' (cl primLevelSuc <@> a) (Sort . tmSort <$> a)) $ \ bA -> hPi' "φ" (elInf $ cl primInterval) $ \ phi -> hPi' "u" (elInf $ cl primPartial <#> a <@> phi <@> bA) $ \ u -> elInf (cl primSub <#> a <@> bA <@> phi <@> u) --> el' (Sort . tmSort <$> a) bA return $ PrimImpl t $ primFun __IMPOSSIBLE__ 5 $ \ ts -> do case ts of [a,bA,phi,u,x] -> do view <- intervalView' sphi <- reduceB' phi case view $ unArg $ ignoreBlocking sphi of IOne -> redReturn =<< (return (unArg u) <..> (getTerm builtinSubOut builtinItIsOne)) _ -> do sx <- reduceB' x mSubIn <- getBuiltinName' builtinSubIn case unArg $ ignoreBlocking $ sx of Def q [_,_,_, Apply t] | Just q == mSubIn -> redReturn (unArg t) _ -> return $ NoReduction $ map notReduced [a,bA] ++ [reduced sphi, notReduced u, reduced sx] _ -> __IMPOSSIBLE__ primIdFace' :: TCM PrimitiveImpl primIdFace' = do requireCubical t <- runNamesT [] $ hPi' "a" (el $ cl primLevel) $ \ a -> hPi' "A" (sort . tmSort <$> a) $ \ bA -> hPi' "x" (el' a bA) $ \ x -> hPi' "y" (el' a bA) $ \ y -> (el' a $ cl primId <#> a <#> bA <@> x <@> y) --> elInf (cl primInterval) return $ PrimImpl t $ primFun __IMPOSSIBLE__ 5 $ \ ts -> do case ts of [l,bA,x,y,t] -> do st <- reduceB' t mConId <- getName' builtinConId case unArg (ignoreBlocking st) of Def q [_,_,_,_, Apply phi,_] | Just q == mConId -> redReturn (unArg phi) _ -> return $ NoReduction $ map notReduced [l,bA,x,y] ++ [reduced st] _ -> __IMPOSSIBLE__ primIdPath' :: TCM PrimitiveImpl primIdPath' = do requireCubical t <- runNamesT [] $ hPi' "a" (el $ cl primLevel) $ \ a -> hPi' "A" (sort . tmSort <$> a) $ \ bA -> hPi' "x" (el' a bA) $ \ x -> hPi' "y" (el' a bA) $ \ y -> (el' a $ cl primId <#> a <#> bA <@> x <@> y) --> (el' a $ cl primPath <#> a <#> bA <@> x <@> y) return $ PrimImpl t $ primFun __IMPOSSIBLE__ 5 $ \ ts -> do case ts of [l,bA,x,y,t] -> do st <- reduceB' t mConId <- getName' builtinConId case unArg (ignoreBlocking st) of Def q [_,_,_,_,_,Apply w] | Just q == mConId -> redReturn (unArg w) _ -> return $ NoReduction $ map notReduced [l,bA,x,y] ++ [reduced st] _ -> __IMPOSSIBLE__ primTrans' :: TCM PrimitiveImpl primTrans' = do requireCubical t <- runNamesT [] $ hPi' "a" (elInf (cl primInterval) --> (el $ cl primLevel)) $ \ a -> nPi' "A" (nPi' "i" (elInf (cl primInterval)) $ \ i -> (sort . tmSort <$> (a <@> i))) $ \ bA -> nPi' "φ" (elInf $ cl primInterval) $ \ phi -> (el' (a <@> cl primIZero) (bA <@> cl primIZero) --> el' (a <@> cl primIOne) (bA <@> cl primIOne)) return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 4 $ \ ts nelims -> do primTransHComp DoTransp ts nelims primHComp' :: TCM PrimitiveImpl primHComp' = do requireCubical t <- runNamesT [] $ hPi' "a" (el $ cl primLevel) $ \ a -> hPi' "A" (sort . tmSort <$> a) $ \ bA -> hPi' "φ" (elInf $ cl primInterval) $ \ phi -> (nPi' "i" (elInf $ cl primInterval) $ \ i -> pPi' "o" phi $ \ _ -> el' a bA) --> (el' a bA --> el' a bA) return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 5 $ \ ts nelims -> do primTransHComp DoHComp ts nelims data TranspOrHComp = DoTransp | DoHComp deriving (Eq,Show) cmdToName :: TranspOrHComp -> String cmdToName DoTransp = builtinTrans cmdToName DoHComp = builtinHComp data FamilyOrNot a = IsFam {famThing :: a} | IsNot {famThing :: a} deriving (Eq,Show,Functor,Foldable,Traversable) instance Reduce a => Reduce (FamilyOrNot a) where reduceB' x = traverse id <$> traverse reduceB' x reduce' x = traverse reduce' x primTransHComp :: TranspOrHComp -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term) primTransHComp cmd ts nelims = do (l,bA,phi,u,u0) <- case (cmd,ts) of (DoTransp, [l,bA,phi, u0]) -> do -- u <- runNamesT [] $ do -- u0 <- open $ unArg u0 -- defaultArg <$> (ilam "o" $ \ _ -> u0) return $ (IsFam l,IsFam bA,phi,Nothing,u0) (DoHComp, [l,bA,phi,u,u0]) -> do -- [l,bA] <- runNamesT [] $ do -- forM [l,bA] $ \ a -> do -- let info = argInfo a -- a <- open $ unArg a -- Arg info <$> (lam "i" $ \ _ -> a) return $ (IsNot l,IsNot bA,phi,Just u,u0) _ -> __IMPOSSIBLE__ sphi <- reduceB' phi vphi <- intervalView $ unArg $ ignoreBlocking sphi let clP s = getTerm (cmdToName cmd) s -- WORK case vphi of IOne -> redReturn =<< case u of -- cmd == DoComp Just u -> runNamesT [] $ do u <- open (unArg u) u <@> clP builtinIOne <..> clP builtinItIsOne -- cmd == DoTransp Nothing -> return $ unArg u0 _ -> do let fallback' sc = do u' <- case u of -- cmd == DoComp Just u -> (:[]) <$> case vphi of IZero -> fmap (reduced . notBlocked . argN) . runNamesT [] $ do [l,c] <- mapM (open . unArg) [famThing l, ignoreBlocking sc] lam "i" $ \ i -> clP builtinIsOneEmpty <#> l <#> (ilam "o" $ \ _ -> c) _ -> return (notReduced u) -- cmd == DoTransp Nothing -> return [] return $ NoReduction $ [notReduced (famThing l), reduced sc, reduced sphi] ++ u' ++ [notReduced u0] sbA <- reduceB' bA t <- case unArg <$> ignoreBlocking sbA of IsFam (Lam _info t) -> Just . fmap IsFam <$> reduceB' (absBody t) IsFam _ -> return Nothing IsNot t -> return . Just . fmap IsNot $ (t <$ sbA) case t of Nothing -> fallback' (famThing <$> sbA) Just st -> do let fallback = fallback' (fmap famThing $ st *> sbA) t = ignoreBlocking st mGlue <- getPrimitiveName' builtinGlue mId <- getBuiltinName' builtinId pathV <- pathView' case famThing t of MetaV m _ -> fallback' (fmap famThing $ Blocked m () *> sbA) -- absName t instead of "i" Pi a b | nelims > 0 -> maybe fallback redReturn =<< compPi cmd "i" ((a,b) <$ t) (ignoreBlocking sphi) u u0 | otherwise -> fallback Sort (Type l) -> compSort cmd fallback phi u u0 (l <$ t) Def q [Apply la, Apply lb, Apply bA, Apply phi', Apply bT, Apply e] | Just q == mGlue -> do compGlue cmd phi u u0 ((la, lb, bA, phi', bT, e) <$ t) -- Path/PathP d | PathType _ _ _ bA x y <- pathV (El __DUMMY_SORT__ d) -> do if nelims > 0 then compPathP cmd sphi u u0 l ((bA, x, y) <$ t) else fallback Def q [Apply _ , Apply bA , Apply x , Apply y] | Just q == mId -> do maybe fallback return =<< compId cmd sphi u u0 l ((bA, x, y) <$ t) Def q es -> do info <- getConstInfo q let lam_i = Lam defaultArgInfo . Abs "i" case theDef info of r@Record{recComp = kit} | nelims > 0, Just as <- allApplyElims es, DoTransp <- cmd, Just transpR <- nameOfTransp kit -> if recPars r == 0 then redReturn $ unArg u0 else redReturn $ (Def transpR []) `apply` (map (fmap lam_i) as ++ [ignoreBlocking sphi,u0]) | nelims > 0, Just as <- allApplyElims es, DoHComp <- cmd, Just hCompR <- nameOfHComp kit -> redReturn $ (Def hCompR []) `apply` (as ++ [ignoreBlocking sphi,fromMaybe __IMPOSSIBLE__ u,u0]) | Just as <- allApplyElims es, [] <- recFields r -> compData False (recPars r) cmd l (as <$ t) sbA sphi u u0 Datatype{dataPars = pars, dataIxs = ixs, dataPathCons = pcons} | and [null pcons | DoHComp <- [cmd]], Just as <- allApplyElims es -> compData (not $ null $ pcons) (pars+ixs) cmd l (as <$ t) sbA sphi u u0 -- postulates with no arguments do not need to transport. Axiom{} | [] <- es, DoTransp <- cmd -> redReturn $ unArg u0 _ -> fallback _ -> fallback where compSort DoTransp fallback phi Nothing u0 (IsFam l) = do -- TODO should check l is constant redReturn $ unArg u0 compSort DoHComp fallback phi (Just u) u0 (IsNot l) = do let getTermLocal = getTerm (builtinHComp ++ " for Set") checkPrims <- all isJust <$> sequence [getTerm' builtinPathToEquiv, getTerm' builtinGlue] if not checkPrims then fallback else (redReturn =<<) . runNamesT [] $ do p2equiv <- getTermLocal builtinPathToEquiv tGlue <- getTermLocal builtinGlue tINeg <- getTermLocal builtinINeg io <- getTermLocal builtinIOne l <- open $ Level l [phi,e,u0] <- mapM (open . unArg) [phi,u,u0] let ineg r = pure tINeg <@> r pure tGlue <#> l <#> l <@> u0 <#> phi <@> (e <@> pure io) <@> ilam "o" (\ o -> pure p2equiv <#> (lam "i" $ \ i -> l) <@> (ilam "i" $ \ i -> e <@> ineg i <@> o)) compSort _ fallback phi u u0 _ = __IMPOSSIBLE__ compGlue DoHComp psi (Just u) u0 (IsNot (la, lb, bA, phi, bT, e)) = do let getTermLocal = getTerm $ (builtinHComp ++ " for " ++ builtinGlue) tPOr <- getTermLocal "primPOr" tIMax <- getTermLocal builtinIMax tIMin <- getTermLocal builtinIMin tINeg <- getTermLocal builtinINeg tHComp <- getTermLocal builtinHComp tEFun <- getTermLocal builtinEquivFun tglue <- getTermLocal builtin_glue tunglue <- getTermLocal builtin_unglue io <- getTermLocal builtinIOne (redReturn =<<) . runNamesT [] $ do [psi, u, u0] <- mapM (open . unArg) [psi, u, u0] [la, lb, bA, phi, bT, e] <- mapM (open . unArg) [la, lb, bA, phi, bT, e] let hfill la bA phi u u0 i = pure tHComp <#> la <#> bA <#> (pure tIMax <@> phi <@> (pure tINeg <@> i)) <@> (lam "j" $ \ j -> pure tPOr <#> la <@> phi <@> (pure tINeg <@> i) <@> (ilam "o" $ \ a -> bA) <@> (ilam "o" $ \ o -> u <@> (pure tIMin <@> i <@> j) <..> o) <@> (ilam "o" $ \ _ -> u0) ) <@> u0 tf i o = hfill lb (bT <..> o) psi u u0 i unglue g = pure tunglue <#> la <#> lb <#> bA <#> phi <#> bT <#> e <@> g a1 = pure tHComp <#> la <#> bA <#> (pure tIMax <@> psi <@> phi) <@> (lam "i" $ \ i -> pure tPOr <#> la <@> psi <@> phi <@> (ilam "_" $ \ _ -> bA) <@> (ilam "o" $ \ o -> unglue (u <@> i <..> o)) <@> (ilam "o" $ \ o -> pure tEFun <#> lb <#> la <#> (bT <..> o) <#> bA <@> (e <..> o) <@> tf i o) ) <@> (unglue u0) t1 = tf (pure io) pure tglue <#> la <#> lb <#> bA <#> phi <#> bT <#> e <@> (ilam "o" $ \ o -> t1 o) <@> a1 compGlue DoTransp psi Nothing u0 (IsFam (la, lb, bA, phi, bT, e)) = do let getTermLocal = getTerm $ (builtinTrans ++ " for " ++ builtinGlue) tPOr <- getTermLocal "primPOr" tIMax <- getTermLocal builtinIMax tIMin <- getTermLocal builtinIMin tINeg <- getTermLocal builtinINeg tHComp <- getTermLocal builtinHComp tTrans <- getTermLocal builtinTrans tForall <- getTermLocal builtinFaceForall tEFun <- getTermLocal builtinEquivFun tEProof <- getTermLocal builtinEquivProof tglue <- getTermLocal builtin_glue tunglue <- getTermLocal builtin_unglue io <- getTermLocal builtinIOne iz <- getTermLocal builtinIZero tLMax <- getTermLocal builtinLevelMax tPath <- getTermLocal builtinPath kit <- fromMaybe __IMPOSSIBLE__ <$> getSigmaKit (redReturn =<<) . runNamesT [] $ do let ineg j = pure tINeg <@> j imax i j = pure tIMax <@> i <@> j imin i j = pure tIMin <@> i <@> j -- First define a "ghcomp" version of gcomp. Normal comp looks like: -- -- comp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u ] (forward A 0 u0) -- -- So for "gcomp" we compute: -- -- gcomp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u, ~ phi -> forward A 0 u0 ] (forward A 0 u0) -- -- The point of this is that gcomp does not produce any empty -- systems (if phi = 0 it will reduce to "forward A 0 u". gcomp <- do let forward la bA r u = pure tTrans <#> (lam "i" $ \ i -> la <@> (i `imax` r)) <@> (lam "i" $ \ i -> bA <@> (i `imax` r)) <@> r <@> u return $ \ la bA phi u u0 -> pure tHComp <#> (la <@> pure io) <#> (bA <@> pure io) <#> imax phi (ineg phi) <@> (lam "i" $ \ i -> pure tPOr <#> (la <@> i) <@> phi <@> ineg phi <@> (ilam "o" $ \ a -> bA <@> i) <@> (ilam "o" $ \ o -> forward la bA i (u <@> i <..> o)) <@> (ilam "o" $ \ o -> forward la bA (pure iz) u0)) <@> forward la bA (pure iz) u0 let transpFill la bA phi u0 i = pure tTrans <#> (ilam "j" $ \ j -> la <@> imin i j) <@> (ilam "j" $ \ j -> bA <@> imin i j) <@> (imax phi (ineg i)) <@> u0 [psi,u0] <- mapM (open . unArg) [psi,u0] glue1 <- do g <- open $ (tglue `apply`) . map (setHiding Hidden) . map (subst 0 io) $ [la, lb, bA, phi, bT, e] return $ \ t a -> g <@> t <@> a unglue0 <- do ug <- open $ (tunglue `apply`) . map (setHiding Hidden) . map (subst 0 iz) $ [la, lb, bA, phi, bT, e] return $ \ a -> ug <@> a [la, lb, bA, phi, bT, e] <- mapM (\ a -> open . runNames [] $ (lam "i" $ const (pure $ unArg a))) [la, lb, bA, phi, bT, e] let tf i o = transpFill lb (lam "i" $ \ i -> bT <@> i <..> o) psi u0 i t1 o = tf (pure io) o a0 = unglue0 u0 -- compute "forall. phi" forallphi = pure tForall <@> phi -- a1 with gcomp a1 = gcomp la bA (imax psi forallphi) (lam "i" $ \ i -> pure tPOr <#> (la <@> i) <@> psi <@> forallphi <@> (ilam "o" $ \ a -> bA <@> i) <@> (ilam "o" $ \ _ -> a0) <@> (ilam "o" $ \ o -> pure tEFun <#> (lb <@> i) <#> (la <@> i) <#> (bT <@> i <..> o) <#> (bA <@> i) <@> (e <@> i <..> o) <@> (tf i o))) a0 max l l' = pure tLMax <@> l <@> l' sigCon x y = pure (Con (sigmaCon kit) ConOSystem []) <@> x <@> y w i o = pure tEFun <#> (lb <@> i) <#> (la <@> i) <#> (bT <@> i <..> o) <#> (bA <@> i) <@> (e <@> i <..> o) fiber la lb bA bB f b = (pure (Def (sigmaName kit) []) <#> la <#> lb <@> bA <@> (lam "a" $ \ a -> pure tPath <#> lb <#> bB <@> (f <@> a) <@> b)) -- We don't have to do anything special for "~ forall. phi" -- here (to implement "ghcomp") as it is taken care off by -- tEProof in t1'alpha below pe o = -- o : [ φ 1 ] pure tPOr <#> max (la <@> pure io) (lb <@> pure io) <@> psi <@> forallphi <@> (ilam "o" $ \ _ -> fiber (lb <@> pure io) (la <@> pure io) (bT <@> (pure io) <..> o) (bA <@> pure io) (w (pure io) o) a1) <@> (ilam "o" $ \ o -> sigCon u0 (lam "_" $ \ _ -> a1)) <@> (ilam "o" $ \ o -> sigCon (t1 o) (lam "_" $ \ _ -> a1)) -- "ghcomp" is implemented in the proof of tEProof -- (see src/data/lib/prim/Agda/Builtin/Cubical/Glue.agda) t1'alpha o = -- o : [ φ 1 ] pure tEProof <#> (lb <@> pure io) <#> (la <@> pure io) <@> (bT <@> pure io <..> o) <@> (bA <@> pure io) <@> (e <@> pure io <..> o) <@> a1 <@> forallphi <@> pe o -- TODO: optimize? t1' o = t1'alpha o <&> (`applyE` [Proj ProjSystem (sigmaFst kit)]) alpha o = t1'alpha o <&> (`applyE` [Proj ProjSystem (sigmaSnd kit)]) a1' = pure tHComp <#> (la <@> pure io) <#> (bA <@> pure io) <#> (imax (phi <@> pure io) psi) <@> (lam "j" $ \ j -> pure tPOr <#> (la <@> pure io) <@> (phi <@> pure io) <@> psi <@> (ilam "o" $ \ _ -> bA <@> pure io) <@> (ilam "o" $ \ o -> alpha o <@@> (w (pure io) o <@> t1' o,a1,j)) <@> (ilam "o" $ \ _ -> a1) ) <@> a1 glue1 (ilam "o" t1') a1' compGlue cmd phi u u0 _ = __IMPOSSIBLE__ compPi :: TranspOrHComp -> ArgName -> FamilyOrNot (Dom Type, Abs Type) -- Γ , i : I -> Arg Term -- Γ -> Maybe (Arg Term) -- Γ -> Arg Term -- Γ -> ReduceM (Maybe Term) compPi cmd t ab phi u u0 = do let getTermLocal = getTerm $ cmdToName cmd ++ " for function types" tTrans <- getTermLocal builtinTrans tHComp <- getTermLocal builtinHComp tINeg <- getTermLocal builtinINeg tIMax <- getTermLocal builtinIMax iz <- getTermLocal builtinIZero let toLevel' t = do s <- reduce $ getSort t case s of (Type l) -> return (Just l) _ -> return Nothing toLevel t = fromMaybe __IMPOSSIBLE__ <$> toLevel' t -- make sure the codomain has a level. caseMaybeM (toLevel' . absBody . snd . famThing $ ab) (return Nothing) $ \ _ -> do runNamesT [] $ do labA <- do let (x,f) = case ab of IsFam (a,_) -> (a, \ a -> runNames [] $ (lam "i" $ const (pure a))) IsNot (a,_) -> (a, id) lx <- toLevel' x caseMaybe lx (return Nothing) $ \ lx -> Just <$> mapM (open . f) [Level lx, unEl . unDom $ x] caseMaybe labA (return Nothing) $ \ [la,bA] -> Just <$> do [phi, u0] <- mapM (open . unArg) [phi, u0] u <- traverse open (unArg <$> u) glam (getArgInfo (fst $ famThing ab)) (absName $ snd $ famThing ab) $ \ u1 -> do case (cmd, ab, u) of (DoHComp, IsNot (a , b), Just u) -> do bT <- (raise 1 b `absApp`) <$> u1 let v = u1 pure tHComp <#> (Level <$> toLevel bT) <#> (pure $ unEl $ bT) <#> phi <@> (lam "i" $ \ i -> ilam "o" $ \ o -> gApply (getHiding a) (u <@> i <..> o) v) <@> (gApply (getHiding a) u0 v) (DoTransp, IsFam (a , b), Nothing) -> do let v i = do let iOrNot j = pure tIMax <@> i <@> (pure tINeg <@> j) pure tTrans <#> (lam "j" $ \ j -> la <@> iOrNot j) <@> (lam "j" $ \ j -> bA <@> iOrNot j) <@> (pure tIMax <@> phi <@> i) <@> u1 -- Γ , u1 : A[i1] , i : I bB v = (consS v $ liftS 1 $ raiseS 1) `applySubst` (absBody b {- Γ , i : I , x : A[i] -}) tLam = Lam defaultArgInfo bT <- bind "i" $ \ i -> bB <$> v i -- Γ , u1 : A[i1] (pure tTrans <#> (tLam <$> traverse (fmap Level . toLevel) bT) <@> (pure . tLam $ unEl <$> bT) <@> phi <@> gApply (getHiding a) u0 (v (pure iz))) (_,_,_) -> __IMPOSSIBLE__ compPathP cmd@DoHComp sphi (Just u) u0 (IsNot l) (IsNot (bA,x,y)) = do let getTermLocal = getTerm $ cmdToName cmd ++ " for path types" tHComp <- getTermLocal builtinHComp tINeg <- getTermLocal builtinINeg tIMax <- getTermLocal builtinIMax tOr <- getTermLocal "primPOr" let ineg j = pure tINeg <@> j imax i j = pure tIMax <@> i <@> j redReturn . runNames [] $ do [l,u,u0] <- mapM (open . unArg) [l,u,u0] phi <- open . unArg . ignoreBlocking $ sphi [bA, x, y] <- mapM (open . unArg) [bA, x, y] lam "j" $ \ j -> pure tHComp <#> l <#> (bA <@> j) <#> (phi `imax` (ineg j `imax` j)) <@> (lam "i'" $ \ i -> let or f1 f2 = pure tOr <#> l <@> f1 <@> f2 <#> (lam "_" $ \ _ -> bA <@> i) in or phi (ineg j `imax` j) <@> (ilam "o" $ \ o -> u <@> i <..> o <@@> (x, y, j)) -- a0 <@@> (x <@> i, y <@> i, j) <@> (or (ineg j) j <@> (ilam "_" $ const x) <@> (ilam "_" $ const y))) <@> (u0 <@@> (x, y, j)) compPathP cmd@DoTransp sphi Nothing u0 (IsFam l) (IsFam (bA,x,y)) = do -- Γ ⊢ l -- Γ, i ⊢ bA, x, y let getTermLocal = getTerm $ cmdToName cmd ++ " for path types" tINeg <- getTermLocal builtinINeg tIMax <- getTermLocal builtinIMax tOr <- getTermLocal "primPOr" iz <- getTermLocal builtinIZero io <- getTermLocal builtinIOne let ineg j = pure tINeg <@> j imax i j = pure tIMax <@> i <@> j comp <- do tHComp <- getTermLocal builtinHComp tTrans <- getTermLocal builtinTrans let forward la bA r u = pure tTrans <#> (lam "i" $ \ i -> la <@> (i `imax` r)) <@> (lam "i" $ \ i -> bA <@> (i `imax` r)) <@> r <@> u return $ \ la bA phi u u0 -> pure tHComp <#> (la <@> pure io) <#> (bA <@> pure io) <#> phi <@> (lam "i" $ \ i -> ilam "o" $ \ o -> forward la bA i (u <@> i <..> o)) <@> forward la bA (pure iz) u0 redReturn . runNames [] $ do [l,u0] <- mapM (open . unArg) [l,u0] phi <- open . unArg . ignoreBlocking $ sphi [bA, x, y] <- mapM (\ a -> open . runNames [] $ (lam "i" $ const (pure $ unArg a))) [bA, x, y] lam "j" $ \ j -> comp l (lam "i" $ \ i -> bA <@> i <@> j) (phi `imax` (ineg j `imax` j)) (lam "i'" $ \ i -> let or f1 f2 = pure tOr <#> l <@> f1 <@> f2 <#> (lam "_" $ \ _ -> bA <@> i <@> j) in or phi (ineg j `imax` j) <@> (ilam "o" $ \ o -> u0 <@@> (x <@> pure iz, y <@> pure iz, j)) <@> (or (ineg j) j <@> (ilam "_" $ const (x <@> i)) <@> (ilam "_" $ const (y <@> i)))) (u0 <@@> (x <@> pure iz, y <@> pure iz, j)) compPathP _ sphi u a0 _ _ = __IMPOSSIBLE__ compId cmd sphi u a0 l bA_x_y = do let getTermLocal = getTerm $ cmdToName cmd ++ " for " ++ builtinId unview <- intervalUnview' mConId <- getBuiltinName' builtinConId let isConId (Def q _) = Just q == mConId isConId _ = False sa0 <- reduceB' a0 -- wasteful to compute b even when cheaper checks might fail b <- case u of Nothing -> return True Just u -> allComponents unview (unArg . ignoreBlocking $ sphi) (unArg u) isConId case mConId of Just conid | isConId (unArg . ignoreBlocking $ sa0) , b -> (Just <$>) . (redReturn =<<) $ do tHComp <- getTermLocal builtinHComp tTrans <- getTermLocal builtinTrans tIMin <- getTermLocal "primDepIMin" tFace <- getTermLocal "primIdFace" tPath <- getTermLocal "primIdPath" tPathType <- getTermLocal builtinPath runNamesT [] $ do let irrInfo = setRelevance Irrelevant defaultArgInfo let io = pure $ unview IOne iz = pure $ unview IZero conId = pure $ Def conid [] l <- case l of IsFam l -> open . unArg $ l IsNot l -> do open (Lam defaultArgInfo $ NoAbs "_" $ unArg l) [p0] <- mapM (open . unArg) [a0] p <- case u of Just u -> do u <- open . unArg $ u return $ \ i o -> u <@> i <..> o Nothing -> do return $ \ i o -> p0 phi <- open . unArg . ignoreBlocking $ sphi [bA, x, y] <- case bA_x_y of IsFam (bA,x,y) -> mapM (\ a -> open . runNames [] $ (lam "i" $ const (pure $ unArg a))) [bA, x, y] IsNot (bA,x,y) -> forM [bA,x,y] $ \ a -> open (Lam defaultArgInfo $ NoAbs "_" $ unArg a) let eval DoTransp l bA phi _ u0 = pure tTrans <#> l <@> bA <@> phi <@> u0 eval DoHComp l bA phi u u0 = pure tHComp <#> (l <@> io) <#> (bA <@> io) <#> phi <@> u <@> u0 conId <#> (l <@> io) <#> (bA <@> io) <#> (x <@> io) <#> (y <@> io) <@> (pure tIMin <@> phi <@> (ilam "o" $ \ o -> pure tFace <#> (l <@> io) <#> (bA <@> io) <#> (x <@> io) <#> (y <@> io) <@> (p io o))) <@> (eval cmd l (lam "i" $ \ i -> pure tPathType <#> (l <@> i) <#> (bA <@> i) <@> (x <@> i) <@> (y <@> i)) phi (lam "i" $ \ i -> ilam "o" $ \ o -> pure tPath <#> (l <@> i) <#> (bA <@> i) <#> (x <@> i) <#> (y <@> i) <@> (p i o) ) (pure tPath <#> (l <@> iz) <#> (bA <@> iz) <#> (x <@> iz) <#> (y <@> iz) <@> p0) ) _ -> return $ Nothing allComponents unview phi u p = do let boolToI b = if b then unview IOne else unview IZero as <- decomposeInterval phi (and <$>) . forM as $ \ (bs,ts) -> do -- OPTIMIZE: stop at the first False let u' = listS (Map.toAscList $ Map.map boolToI bs) `applySubst` u t <- reduce2Lam u' return $! p t where reduce2Lam t = do t <- reduce' t case lam2Abs t of t -> Reduce.underAbstraction_ t $ \ t -> do t <- reduce' t case lam2Abs t of t -> Reduce.underAbstraction_ t reduce' where lam2Abs (Lam _ t) = t lam2Abs t = Abs "y" (raise 1 t `apply` [argN $ var 0]) compData False _ cmd@DoHComp (IsNot l) (IsNot ps) fsc sphi (Just u) a0 = do let getTermLocal = getTerm $ cmdToName cmd ++ " for data types" let sc = famThing <$> fsc tEmpty <- getTermLocal builtinIsOneEmpty constrForm <- do mz <- getTerm' builtinZero ms <- getTerm' builtinSuc return $ \ t -> fromMaybe t (constructorForm' mz ms t) su <- reduceB' u sa0 <- reduceB' a0 view <- intervalView' unview <- intervalUnview' let f = unArg . ignoreBlocking phi = f sphi u = f su a0 = f sa0 noRed = return $ NoReduction [notReduced l,reduced sc, reduced sphi, reduced su', reduced sa0] where su' = case view phi of IZero -> notBlocked $ argN $ runNames [] $ do [l,c] <- mapM (open . unArg) [l,ignoreBlocking sc] lam "i" $ \ i -> pure tEmpty <#> l <#> (ilam "o" $ \ _ -> c) _ -> su sameConHead h u = allComponents unview phi u $ \ t -> case constrForm t of Con h' _ _ -> h == h' _ -> False case constrForm a0 of Con h _ args -> do ifM (not <$> sameConHead h u) noRed $ do Constructor{ conComp = (cm,_) } <- theDef <$> getConstInfo (conName h) case nameOfHComp cm of Just hcompD -> redReturn $ Def hcompD [] `apply` (ps ++ map argN [phi,u,a0]) Nothing -> noRed _ -> noRed compData _ 0 DoTransp (IsFam l) (IsFam ps) fsc sphi Nothing a0 = redReturn $ unArg a0 compData isHIT _ cmd@DoTransp (IsFam l) (IsFam ps) fsc sphi Nothing a0 = do let getTermLocal = getTerm $ cmdToName cmd ++ " for data types" let sc = famThing <$> fsc mhcompName <- getName' builtinHComp constrForm <- do mz <- getTerm' builtinZero ms <- getTerm' builtinSuc return $ \ t -> fromMaybe t (constructorForm' mz ms t) sa0 <- reduceB' a0 let f = unArg . ignoreBlocking phi = f sphi a0 = f sa0 noRed = return $ NoReduction [notReduced l,reduced sc, reduced sphi, reduced sa0] let lam_i = Lam defaultArgInfo . Abs "i" case constrForm a0 of Con h _ args -> do Constructor{ conComp = (cm,_) } <- theDef <$> getConstInfo (conName h) case nameOfTransp cm of Just transpD -> redReturn $ Def transpD [] `apply` (map (fmap lam_i) ps ++ map argN [phi,a0]) Nothing -> noRed Def q es | isHIT, Just q == mhcompName, Just [_l0,_c0,psi,u,u0] <- allApplyElims es -> do let bC = ignoreBlocking sc hcomp <- getTermLocal builtinHComp transp <- getTermLocal builtinTrans io <- getTermLocal builtinIOne iz <- getTermLocal builtinIZero (redReturn =<<) . runNamesT [] $ do [l,bC,phi,psi,u,u0] <- mapM (open . unArg) [l,bC,ignoreBlocking sphi,psi,u,u0] -- hcomp (sc 1) [psi |-> transp sc phi u] (transp sc phi u0) pure hcomp <#> (l <@> pure io) <#> (bC <@> pure io) <#> psi <@> (lam "j" $ \ j -> ilam "o" $ \ o -> pure transp <#> l <@> bC <@> phi <@> (u <@> j <..> o)) <@> (pure transp <#> l <@> bC <@> phi <@> u0) _ -> noRed compData _ _ _ _ _ _ _ _ _ = __IMPOSSIBLE__ compPO = __IMPOSSIBLE__ primComp :: TCM PrimitiveImpl primComp = do requireCubical t <- runNamesT [] $ hPi' "a" (elInf (cl primInterval) --> (el $ cl primLevel)) $ \ a -> nPi' "A" (nPi' "i" (elInf (cl primInterval)) $ \ i -> (sort . tmSort <$> (a <@> i))) $ \ bA -> nPi' "φ" (elInf $ cl primInterval) $ \ phi -> (nPi' "i" (elInf $ cl primInterval) $ \ i -> pPi' "o" phi $ \ _ -> el' (a <@> i) (bA <@> i)) --> (el' (a <@> cl primIZero) (bA <@> cl primIZero) --> el' (a <@> cl primIOne) (bA <@> cl primIOne)) one <- primItIsOne io <- primIOne return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 5 $ \ ts nelims -> do case ts of [l,c,phi,u,a0] -> do sphi <- reduceB' phi vphi <- intervalView $ unArg $ ignoreBlocking sphi case vphi of IOne -> redReturn (unArg u `apply` [argN io, argN one]) _ -> do let getTermLocal = getTerm $ builtinComp tIMax <- getTermLocal builtinIMax tINeg <- getTermLocal builtinINeg tHComp <- getTermLocal builtinHComp tTrans <- getTermLocal builtinTrans iz <- getTermLocal builtinIZero (redReturn =<<) . runNamesT [] $ do comp <- do let ineg j = pure tINeg <@> j imax i j = pure tIMax <@> i <@> j let forward la bA r u = pure tTrans <#> (lam "i" $ \ i -> la <@> (i `imax` r)) <@> (lam "i" $ \ i -> bA <@> (i `imax` r)) <@> r <@> u return $ \ la bA phi u u0 -> pure tHComp <#> (la <@> pure io) <#> (bA <@> pure io) <#> phi <@> (lam "i" $ \ i -> ilam "o" $ \ o -> forward la bA i (u <@> i <..> o)) <@> forward la bA (pure iz) u0 [l,c,phi,u,a0] <- mapM (open . unArg) [l,c,phi,u,a0] comp l c phi u a0 _ -> __IMPOSSIBLE__ -- lookupS (listS [(x0,t0)..(xn,tn)]) xi = ti, assuming x0 < .. < xn. listS :: [(Int,Term)] -> Substitution listS ((i,t):ts) = singletonS i t `composeS` listS ts listS [] = IdS primGlue' :: TCM PrimitiveImpl primGlue' = do requireCubical -- Glue' : ∀ {l} (A : Set l) → ∀ φ → (T : Partial (Set a) φ) (f : (PartialP φ \ o → (T o) -> A)) -- ([f] : PartialP φ \ o → isEquiv (T o) A (f o)) → Set l t <- runNamesT [] $ (hPi' "la" (el $ cl primLevel) $ \ la -> hPi' "lb" (el $ cl primLevel) $ \ lb -> nPi' "A" (sort . tmSort <$> la) $ \ a -> hPi' "φ" (elInf $ cl primInterval) $ \ φ -> nPi' "T" (pPi' "o" φ $ \ o -> el' (cl primLevelSuc <@> lb) (Sort . tmSort <$> lb)) $ \ t -> (pPi' "o" φ $ \ o -> el' (cl primLevelMax <@> la <@> lb) $ cl primEquiv <#> lb <#> la <@> (t <@> o) <@> a) --> (sort . tmSort <$> lb)) view <- intervalView' one <- primItIsOne return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ts -> case ts of [la,lb,a,phi,t,e] -> do sphi <- reduceB' phi case view $ unArg $ ignoreBlocking $ sphi of IOne -> redReturn $ unArg t `apply` [argN one] _ -> return (NoReduction $ map notReduced [la,lb,a] ++ [reduced sphi] ++ map notReduced [t,e]) _ -> __IMPOSSIBLE__ prim_glue' :: TCM PrimitiveImpl prim_glue' = do requireCubical t <- runNamesT [] $ (hPi' "la" (el $ cl primLevel) $ \ la -> hPi' "lb" (el $ cl primLevel) $ \ lb -> hPi' "A" (sort . tmSort <$> la) $ \ a -> hPi' "φ" (elInf $ cl primInterval) $ \ φ -> hPi' "T" (pPi' "o" φ $ \ o -> el' (cl primLevelSuc <@> lb) (Sort . tmSort <$> lb)) $ \ t -> hPi' "e" (pPi' "o" φ $ \ o -> el' (cl primLevelMax <@> la <@> lb) $ cl primEquiv <#> lb <#> la <@> (t <@> o) <@> a) $ \ e -> (pPi' "o" φ $ \ o -> el' lb (t <@> o)) --> (el' la a --> el' lb (cl primGlue <#> la <#> lb <@> a <#> φ <@> t <@> e))) view <- intervalView' one <- primItIsOne return $ PrimImpl t $ primFun __IMPOSSIBLE__ 8 $ \ts -> case ts of [la,lb,bA,phi,bT,e,t,a] -> do sphi <- reduceB' phi case view $ unArg $ ignoreBlocking $ sphi of IOne -> redReturn $ unArg t `apply` [argN one] _ -> return (NoReduction $ map notReduced [la,lb,bA] ++ [reduced sphi] ++ map notReduced [bT,e,t,a]) _ -> __IMPOSSIBLE__ prim_unglue' :: TCM PrimitiveImpl prim_unglue' = do requireCubical t <- runNamesT [] $ (hPi' "la" (el $ cl primLevel) $ \ la -> hPi' "lb" (el $ cl primLevel) $ \ lb -> hPi' "A" (sort . tmSort <$> la) $ \ a -> hPi' "φ" (elInf $ cl primInterval) $ \ φ -> hPi' "T" (pPi' "o" φ $ \ o -> el' (cl primLevelSuc <@> lb) (Sort . tmSort <$> lb)) $ \ t -> hPi' "e" (pPi' "o" φ $ \ o -> el' (cl primLevelMax <@> la <@> lb) $ cl primEquiv <#> lb <#> la <@> (t <@> o) <@> a) $ \ e -> (el' lb (cl primGlue <#> la <#> lb <@> a <#> φ <@> t <@> e)) --> el' la a) view <- intervalView' one <- primItIsOne mglue <- getPrimitiveName' builtin_glue return $ PrimImpl t $ primFun __IMPOSSIBLE__ 7 $ \ts -> case ts of [la,lb,bA,phi,bT,e,b] -> do sphi <- reduceB' phi case view $ unArg $ ignoreBlocking $ sphi of IOne -> do let argOne = setRelevance Irrelevant $ argN one tEFun <- getTerm builtin_unglue builtinEquivFun redReturn $ tEFun `apply` [lb,la,argH $ unArg bT `apply` [argOne],bA, argN $ unArg e `apply` [argOne],b] _ -> do sb <- reduceB' b case unArg $ ignoreBlocking $ sb of Def q [Apply _,Apply _,Apply _,Apply _,Apply _,Apply _,Apply _,Apply a] | Just q == mglue -> redReturn $ unArg a _ -> return (NoReduction $ map notReduced [la,lb,bA] ++ [reduced sphi] ++ map notReduced [bT,e] ++ [reduced sb]) _ -> __IMPOSSIBLE__ -- TODO Andrea: keep reductions that happen under foralls? primFaceForall' :: TCM PrimitiveImpl primFaceForall' = do requireCubical t <- (elInf primInterval --> elInf primInterval) --> elInf primInterval return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ts -> case ts of [phi] -> do sphi <- reduceB' phi case unArg $ ignoreBlocking $ sphi of Lam _ t -> do t <- reduce' t case t of NoAbs _ t -> redReturn t Abs _ t -> maybe (return $ NoReduction [reduced sphi]) redReturn =<< toFaceMapsPrim t _ -> return (NoReduction [reduced sphi]) _ -> __IMPOSSIBLE__ where toFaceMapsPrim t = do view <- intervalView' unview <- intervalUnview' us' <- decomposeInterval t fr <- getTerm builtinFaceForall builtinFaceForall let v = view t us = [ map Left (Map.toList bsm) ++ map Right ts | (bsm,ts) <- us' , 0 `Map.notMember` bsm ] fm (i,b) = if b then var (i-1) else unview (INeg (argN (var $ i-1))) ffr t = fr `apply` [argN $ Lam defaultArgInfo $ Abs "i" t] r = Just $ foldr (\ x r -> unview (IMax (argN x) (argN r))) (unview IZero) (map (foldr (\ x r -> unview (IMin (argN (either fm ffr x)) (argN r))) (unview IOne)) us) -- traceSLn "cube.forall" 20 (unlines [show v, show us', show us, show r]) $ return $ case us' of [(m,[_])] | Map.null m -> Nothing v -> r decomposeInterval :: HasBuiltins m => Term -> m [(Map Int Bool,[Term])] decomposeInterval t = do xs <- decomposeInterval' t let isConsistent xs = all (\ xs -> Set.size xs == 1) . Map.elems $ xs -- optimize by not doing generate + filter return [ (Map.map (head . Set.toList) bsm,ts) | (bsm,ts) <- xs , isConsistent bsm ] decomposeInterval' :: HasBuiltins m => Term -> m [(Map Int (Set Bool),[Term])] decomposeInterval' t = do view <- intervalView' unview <- intervalUnview' let f :: IntervalView -> [[Either (Int,Bool) Term]] -- TODO handle primIMinDep -- TODO? handle forall f IZero = mzero f IOne = return [] f (IMin x y) = do xs <- (f . view . unArg) x; ys <- (f . view . unArg) y; return (xs ++ ys) f (IMax x y) = msum $ map (f . view . unArg) [x,y] f (INeg x) = map (either (\ (x,y) -> Left (x,not y)) (Right . unview . INeg . argN)) <$> (f . view . unArg) x f (OTerm (Var i [])) = return [Left (i,True)] f (OTerm t) = return [Right t] v = view t return [ (bsm,ts) | xs <- f v , let (bs,ts) = partitionEithers xs , let bsm = (Map.fromListWith Set.union . map (id -*- Set.singleton)) bs ] -- | @mkPrimInjective@ takes two Set0 @a@ and @b@ and a function @f@ of type -- @a -> b@ and outputs a primitive internalizing the fact that @f@ is injective. mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl mkPrimInjective a b qn = do -- Define the type eqName <- primEqualityName let lvl0 = Max [] let eq a t u = El (Type lvl0) <$> pure (Def eqName []) <#> pure (Level lvl0) <#> pure (unEl a) <@> t <@> u let f = pure (Def qn []) ty <- nPi "t" (pure a) $ nPi "u" (pure a) $ (eq b (f <@> varM 1) (f <@> varM 0)) --> (eq a ( varM 1) ( varM 0)) -- Get the constructor corresponding to BUILTIN REFL refl <- getRefl -- Implementation: when the equality argument reduces to refl so does the primitive. -- If the user want the primitive to reduce whenever the two values are equal (no -- matter whether the equality is refl), they can combine it with @eraseEquality@. return $ PrimImpl ty $ primFun __IMPOSSIBLE__ 3 $ \ ts -> do let t = fromMaybe __IMPOSSIBLE__ $ headMaybe ts let eq = unArg $ fromMaybe __IMPOSSIBLE__ $ lastMaybe ts eq' <- normalise' eq case eq' of Con{} -> redReturn $ refl t _ -> return $ NoReduction $ map notReduced ts primCharToNatInjective :: TCM PrimitiveImpl primCharToNatInjective = do char <- primType (undefined :: Char) nat <- primType (undefined :: Nat) toNat <- primFunName <$> getPrimitive "primCharToNat" mkPrimInjective char nat toNat primStringToListInjective :: TCM PrimitiveImpl primStringToListInjective = do string <- primType (undefined :: Str) chars <- primType (undefined :: String) toList <- primFunName <$> getPrimitive "primStringToList" mkPrimInjective string chars toList primWord64ToNatInjective :: TCM PrimitiveImpl primWord64ToNatInjective = do word <- primType (undefined :: Word64) nat <- primType (undefined :: Nat) toNat <- primFunName <$> getPrimitive "primWord64ToNat" mkPrimInjective word nat toNat getRefl :: TCM (Arg Term -> Term) getRefl = do -- BUILTIN REFL maybe a constructor with one (the principal) argument or only parameters. -- Get the ArgInfo of the principal argument of refl. con@(Con rf ci []) <- primRefl minfo <- fmap (setOrigin Inserted) <$> getReflArgInfo rf pure $ case minfo of Just ai -> Con rf ci . (:[]) . Apply . setArgInfo ai Nothing -> const con -- | @primEraseEquality : {a : Level} {A : Set a} {x y : A} -> x ≡ y -> x ≡ y@ primEraseEquality :: TCM PrimitiveImpl primEraseEquality = do -- primEraseEquality is incompatible with --without-K -- We raise an error warning if --safe is set and a mere warning otherwise whenM withoutKOption $ ifM (Lens.getSafeMode <$> commandLineOptions) {- then -} (warning SafeFlagWithoutKFlagPrimEraseEquality) {- else -} (warning WithoutKFlagPrimEraseEquality) -- Get the name and type of BUILTIN EQUALITY eq <- primEqualityName eqTy <- defType <$> getConstInfo eq -- E.g. @eqTy = eqTel → Set a@ where @eqTel = {a : Level} {A : Set a} (x y : A)@. TelV eqTel eqCore <- telView eqTy let eqSort = case unEl eqCore of Sort s -> s _ -> __IMPOSSIBLE__ -- Construct the type of primEraseEquality, e.g. -- @{a : Level} {A : Set a} {x y : A} → eq {a} {A} x y -> eq {a} {A} x y@. t <- let xeqy = pure $ El eqSort $ Def eq $ map Apply $ teleArgs eqTel in telePi_ (fmap hide eqTel) <$> (xeqy --> xeqy) -- Get the constructor corresponding to BUILTIN REFL refl <- getRefl -- The implementation of primEraseEquality: return $ PrimImpl t $ primFun __IMPOSSIBLE__ (1 + size eqTel) $ \ ts -> do let (u, v) = fromMaybe __IMPOSSIBLE__ $ last2 =<< initMaybe ts -- Andreas, 2013-07-22. -- Note that we cannot call the conversion checker here, -- because 'reduce' might be called in a context where -- some bound variables do not have a type (just __DUMMY_TYPE__), -- and the conversion checker for eliminations does not -- like this. -- We can only do untyped equality, e.g., by normalisation. (u', v') <- normalise' (u, v) if u' == v' then redReturn $ refl u else return $ NoReduction $ map notReduced ts -- | Get the 'ArgInfo' of the principal argument of BUILTIN REFL. -- -- Returns @Nothing@ for e.g. -- @ -- data Eq {a} {A : Set a} (x : A) : A → Set a where -- refl : Eq x x -- @ -- -- Returns @Just ...@ for e.g. -- @ -- data Eq {a} {A : Set a} : (x y : A) → Set a where -- refl : ∀ x → Eq x x -- @ getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo) getReflArgInfo rf = do def <- getConInfo rf TelV reflTel _ <- telView $ defType def return $ fmap getArgInfo $ headMaybe $ drop (conPars $ theDef def) $ telToList reflTel -- | Used for both @primForce@ and @primForceLemma@. genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl genPrimForce b ret = do let varEl s a = El (varSort s) <$> a varT s a = varEl s (varM a) varS s = pure $ sort $ varSort s t <- hPi "a" (el primLevel) $ hPi "b" (el primLevel) $ hPi "A" (varS 1) $ hPi "B" (varT 2 0 --> varS 1) b return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ ts -> case ts of [a, b, s, t, u, f] -> do u <- reduceB' u let isWHNF Blocked{} = return False isWHNF (NotBlocked _ u) = case unArg u of Lit{} -> return True Con{} -> return True Lam{} -> return True Pi{} -> return True Sort{} -> return True -- sorts and levels are considered whnf Level{} -> return True DontCare{} -> return True Def q _ -> do def <- theDef <$> getConstInfo q return $ case def of Datatype{} -> True Record{} -> True _ -> False MetaV{} -> return False Var{} -> return False Dummy s -> __IMPOSSIBLE_VERBOSE__ s ifM (isWHNF u) (redReturn $ ret (unArg f) (ignoreBlocking u)) (return $ NoReduction $ map notReduced [a, b, s, t] ++ [reduced u, notReduced f]) _ -> __IMPOSSIBLE__ primForce :: TCM PrimitiveImpl primForce = do let varEl s a = El (varSort s) <$> a varT s a = varEl s (varM a) varS s = pure $ sort $ varSort s genPrimForce (nPi "x" (varT 3 1) $ (nPi "y" (varT 4 2) $ varEl 4 $ varM 2 <@> varM 0) --> varEl 3 (varM 1 <@> varM 0)) $ \ f u -> apply f [u] primForceLemma :: TCM PrimitiveImpl primForceLemma = do let varEl s a = El (varSort s) <$> a varT s a = varEl s (varM a) varS s = pure $ sort $ varSort s refl <- primRefl force <- primFunName <$> getPrimitive "primForce" genPrimForce (nPi "x" (varT 3 1) $ nPi "f" (nPi "y" (varT 4 2) $ varEl 4 $ varM 2 <@> varM 0) $ varEl 4 $ primEquality <#> varM 4 <#> (varM 2 <@> varM 1) <@> (pure (Def force []) <#> varM 5 <#> varM 4 <#> varM 3 <#> varM 2 <@> varM 1 <@> varM 0) <@> (varM 0 <@> varM 1) ) $ \ _ _ -> refl mkPrimLevelZero :: TCM PrimitiveImpl mkPrimLevelZero = do t <- primType (undefined :: Lvl) return $ PrimImpl t $ primFun __IMPOSSIBLE__ 0 $ \_ -> redReturn $ Level $ Max [] mkPrimLevelSuc :: TCM PrimitiveImpl mkPrimLevelSuc = do t <- primType (id :: Lvl -> Lvl) return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ ~[a] -> do l <- levelView' $ unArg a redReturn $ Level $ levelSuc l mkPrimLevelMax :: TCM PrimitiveImpl mkPrimLevelMax = do t <- primType (max :: Op Lvl) return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ ~[a, b] -> do Max as <- levelView' $ unArg a Max bs <- levelView' $ unArg b redReturn $ Level $ levelMax $ as ++ bs mkPrimSetOmega :: TCM PrimitiveImpl mkPrimSetOmega = do let t = sort $ UnivSort Inf return $ PrimImpl t $ primFun __IMPOSSIBLE__ 0 $ \_ -> redReturn $ Sort Inf mkPrimFun1TCM :: (FromTerm a, ToTerm b, TermLike b) => TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl mkPrimFun1TCM mt f = do toA <- fromTerm fromB <- toTermR t <- mt return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ts -> case ts of [v] -> redBind (toA v) singleton $ \ x -> do b <- f x case firstMeta b of Just m -> return $ NoReduction [reduced (Blocked m v)] Nothing -> redReturn =<< fromB b _ -> __IMPOSSIBLE__ -- Tying the knot mkPrimFun1 :: (PrimType a, FromTerm a, PrimType b, ToTerm b) => (a -> b) -> TCM PrimitiveImpl mkPrimFun1 f = do toA <- fromTerm fromB <- toTerm t <- primType f return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ts -> case ts of [v] -> redBind (toA v) singleton $ \ x -> redReturn $ fromB $ f x _ -> __IMPOSSIBLE__ mkPrimFun2 :: ( PrimType a, FromTerm a, ToTerm a , PrimType b, FromTerm b , PrimType c, ToTerm c ) => (a -> b -> c) -> TCM PrimitiveImpl mkPrimFun2 f = do toA <- fromTerm fromA <- toTerm toB <- fromTerm fromC <- toTerm t <- primType f return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ts -> case ts of [v,w] -> redBind (toA v) (\v' -> [v', notReduced w]) $ \x -> redBind (toB w) (\w' -> [ reduced $ notBlocked $ Arg (argInfo v) (fromA x) , w']) $ \y -> redReturn $ fromC $ f x y _ -> __IMPOSSIBLE__ mkPrimFun4 :: ( PrimType a, FromTerm a, ToTerm a , PrimType b, FromTerm b, ToTerm b , PrimType c, FromTerm c, ToTerm c , PrimType d, FromTerm d , PrimType e, ToTerm e ) => (a -> b -> c -> d -> e) -> TCM PrimitiveImpl mkPrimFun4 f = do (toA, fromA) <- (,) <$> fromTerm <*> toTerm (toB, fromB) <- (,) <$> fromTerm <*> toTerm (toC, fromC) <- (,) <$> fromTerm <*> toTerm toD <- fromTerm fromE <- toTerm t <- primType f return $ PrimImpl t $ primFun __IMPOSSIBLE__ 4 $ \ts -> let argFrom fromX a x = reduced $ notBlocked $ Arg (argInfo a) (fromX x) in case ts of [a,b,c,d] -> redBind (toA a) (\a' -> a' : map notReduced [b,c,d]) $ \x -> redBind (toB b) (\b' -> [argFrom fromA a x, b', notReduced c, notReduced d]) $ \y -> redBind (toC c) (\c' -> [ argFrom fromA a x , argFrom fromB b y , c', notReduced d]) $ \z -> redBind (toD d) (\d' -> [ argFrom fromA a x , argFrom fromB b y , argFrom fromC c z , d']) $ \w -> redReturn $ fromE $ f x y z w _ -> __IMPOSSIBLE__ -- Type combinators infixr 4 --> infixr 4 .--> infixr 4 ..--> (-->), (.-->), (..-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type a --> b = garr id a b a .--> b = garr (const $ Irrelevant) a b a ..--> b = garr (const $ NonStrict) a b garr :: Monad tcm => (Relevance -> Relevance) -> tcm Type -> tcm Type -> tcm Type garr f a b = do a' <- a b' <- b return $ El (funSort (getSort a') (getSort b')) $ Pi (mapRelevance f $ defaultDom a') (NoAbs "_" b') gpi :: (MonadTCM tcm, MonadDebug tcm) => ArgInfo -> String -> tcm Type -> tcm Type -> tcm Type gpi info name a b = do a <- a let dom = defaultNamedArgDom info name a b <- addContext (name, dom) b let y = stringToArgName name return $ El (piSort (getSort a) (Abs y (getSort b))) (Pi dom (Abs y b)) hPi, nPi :: (MonadTCM tcm, MonadDebug tcm) => String -> tcm Type -> tcm Type -> tcm Type hPi = gpi $ setHiding Hidden defaultArgInfo nPi = gpi defaultArgInfo hPi', nPi' :: (MonadTCM tcm, MonadDebug tcm) => String -> NamesT tcm Type -> (NamesT tcm Term -> NamesT tcm Type) -> NamesT tcm Type hPi' s a b = hPi s a (bind' s b) nPi' s a b = nPi s a (bind' s b) pPi' :: (MonadTCM tcm, MonadDebug tcm) => String -> NamesT tcm Term -> (NamesT tcm Term -> NamesT tcm Type) -> NamesT tcm Type pPi' n phi b = toFinitePi <$> nPi' n (elInf $ cl (liftTCM primIsOne) <@> phi) b where toFinitePi :: Type -> Type toFinitePi (El s (Pi d b)) = El s $ Pi (setRelevance Irrelevant $ d { domFinite = True }) b toFinitePi _ = __IMPOSSIBLE__ el' :: Monad m => m Term -> m Term -> m Type el' l a = El <$> (tmSort <$> l) <*> a elInf :: Functor m => m Term -> m Type elInf t = (El Inf <$> t) nolam :: Term -> Term nolam = Lam defaultArgInfo . NoAbs "_" varM :: Monad tcm => Int -> tcm Term varM = return . var infixl 9 <@>, <#> gApply :: Monad tcm => Hiding -> tcm Term -> tcm Term -> tcm Term gApply h a b = gApply' (setHiding h defaultArgInfo) a b gApply' :: Monad tcm => ArgInfo -> tcm Term -> tcm Term -> tcm Term gApply' info a b = do x <- a y <- b return $ x `apply` [Arg info y] (<@>),(<#>),(<..>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term (<@>) = gApply NotHidden (<#>) = gApply Hidden (<..>) = gApply' (setRelevance Irrelevant defaultArgInfo) (<@@>) :: Monad tcm => tcm Term -> (tcm Term,tcm Term,tcm Term) -> tcm Term t <@@> (x,y,r) = do t <- t x <- x y <- y r <- r return $ t `applyE` [IApply x y r] list :: TCM Term -> TCM Term list t = primList <@> t io :: TCM Term -> TCM Term io t = primIO <@> t path :: TCM Term -> TCM Term path t = primPath <@> t el :: Functor tcm => tcm Term -> tcm Type el t = El (mkType 0) <$> t tset :: Monad tcm => tcm Type tset = return $ sort (mkType 0) sSizeUniv :: Sort sSizeUniv = mkType 0 -- Andreas, 2016-04-14 switching off SizeUniv, unfixing issue #1428 -- sSizeUniv = SizeUniv tSizeUniv :: Monad tcm => tcm Type tSizeUniv = tset -- Andreas, 2016-04-14 switching off SizeUniv, unfixing issue #1428 -- tSizeUniv = return $ El sSizeUniv $ Sort sSizeUniv -- Andreas, 2015-03-16 Since equality checking for types -- includes equality checking for sorts, we cannot put -- SizeUniv in Setω. (SizeUniv : Setω) == (_0 : suc _0) -- will first instantiate _0 := Setω, which is wrong. -- tSizeUniv = return $ El Inf $ Sort SizeUniv -- | Abbreviation: @argN = 'Arg' 'defaultArgInfo'@. argN :: e -> Arg e argN = Arg defaultArgInfo domN :: e -> Dom e domN = defaultDom -- | Abbreviation: @argH = 'hide' 'Arg' 'defaultArgInfo'@. argH :: e -> Arg e argH = Arg $ setHiding Hidden defaultArgInfo domH :: e -> Dom e domH = setHiding Hidden . defaultDom --------------------------------------------------------------------------- -- * The actual primitive functions --------------------------------------------------------------------------- type Op a = a -> a -> a type Fun a = a -> a type Rel a = a -> a -> Bool type Pred a = a -> Bool primitiveFunctions :: Map String (TCM PrimitiveImpl) primitiveFunctions = Map.fromList -- Ulf, 2015-10-28: Builtin integers now map to a datatype, and since you -- can define these functions (reasonably) efficiently using the primitive -- functions on natural numbers there's no need for them anymore. Keeping the -- show function around for convenience, and as a test case for a primitive -- function taking an integer. -- -- Integer functions -- [ "primIntegerPlus" |-> mkPrimFun2 ((+) :: Op Integer) -- , "primIntegerMinus" |-> mkPrimFun2 ((-) :: Op Integer) -- , "primIntegerTimes" |-> mkPrimFun2 ((*) :: Op Integer) -- , "primIntegerDiv" |-> mkPrimFun2 (div :: Op Integer) -- partial -- , "primIntegerMod" |-> mkPrimFun2 (mod :: Op Integer) -- partial -- , "primIntegerEquality" |-> mkPrimFun2 ((==) :: Rel Integer) -- , "primIntegerLess" |-> mkPrimFun2 ((<) :: Rel Integer) -- , "primIntegerAbs" |-> mkPrimFun1 (Nat . abs :: Integer -> Nat) -- , "primNatToInteger" |-> mkPrimFun1 (toInteger :: Nat -> Integer) [ "primShowInteger" |-> mkPrimFun1 (Str . show :: Integer -> Str) -- Natural number functions , "primNatPlus" |-> mkPrimFun2 ((+) :: Op Nat) , "primNatMinus" |-> mkPrimFun2 ((\x y -> max 0 (x - y)) :: Op Nat) , "primNatTimes" |-> mkPrimFun2 ((*) :: Op Nat) , "primNatDivSucAux" |-> mkPrimFun4 ((\k m n j -> k + div (max 0 $ n + m - j) (m + 1)) :: Nat -> Nat -> Nat -> Nat -> Nat) , "primNatModSucAux" |-> let aux :: Nat -> Nat -> Nat -> Nat -> Nat aux k m n j | n > j = mod (n - j - 1) (m + 1) | otherwise = k + n in mkPrimFun4 aux , "primNatEquality" |-> mkPrimFun2 ((==) :: Rel Nat) , "primNatLess" |-> mkPrimFun2 ((<) :: Rel Nat) -- Machine words , "primWord64ToNat" |-> mkPrimFun1 (fromIntegral :: Word64 -> Nat) , "primWord64FromNat" |-> mkPrimFun1 (fromIntegral :: Nat -> Word64) , "primWord64ToNatInjective" |-> primWord64ToNatInjective -- Level functions , "primLevelZero" |-> mkPrimLevelZero , "primLevelSuc" |-> mkPrimLevelSuc , "primLevelMax" |-> mkPrimLevelMax -- Sorts , "primSetOmega" |-> mkPrimSetOmega -- Floating point functions , "primNatToFloat" |-> mkPrimFun1 (fromIntegral :: Nat -> Double) , "primFloatPlus" |-> mkPrimFun2 ((+) :: Op Double) , "primFloatMinus" |-> mkPrimFun2 ((-) :: Op Double) , "primFloatTimes" |-> mkPrimFun2 ((*) :: Op Double) , "primFloatNegate" |-> mkPrimFun1 (negate :: Fun Double) , "primFloatDiv" |-> mkPrimFun2 ((/) :: Op Double) -- ASR (2016-09-29). We use bitwise equality for comparing Double -- because Haskell's Eq, which equates 0.0 and -0.0, allows to prove -- a contradiction (see Issue #2169). , "primFloatEquality" |-> mkPrimFun2 (floatEq :: Rel Double) , "primFloatLess" |-> mkPrimFun2 (floatLt :: Rel Double) , "primFloatNumericalEquality" |-> mkPrimFun2 ((==) :: Rel Double) , "primFloatNumericalLess" |-> mkPrimFun2 ((<) :: Rel Double) , "primFloatSqrt" |-> mkPrimFun1 (sqrt :: Double -> Double) , "primRound" |-> mkPrimFun1 (round :: Double -> Integer) , "primFloor" |-> mkPrimFun1 (floor :: Double -> Integer) , "primCeiling" |-> mkPrimFun1 (ceiling :: Double -> Integer) , "primExp" |-> mkPrimFun1 (exp :: Fun Double) , "primLog" |-> mkPrimFun1 (log :: Fun Double) , "primSin" |-> mkPrimFun1 (sin :: Fun Double) , "primCos" |-> mkPrimFun1 (cos :: Fun Double) , "primTan" |-> mkPrimFun1 (tan :: Fun Double) , "primASin" |-> mkPrimFun1 (asin :: Fun Double) , "primACos" |-> mkPrimFun1 (acos :: Fun Double) , "primATan" |-> mkPrimFun1 (atan :: Fun Double) , "primATan2" |-> mkPrimFun2 (atan2 :: Double -> Double -> Double) , "primShowFloat" |-> mkPrimFun1 (Str . show :: Double -> Str) -- Character functions , "primCharEquality" |-> mkPrimFun2 ((==) :: Rel Char) , "primIsLower" |-> mkPrimFun1 isLower , "primIsDigit" |-> mkPrimFun1 isDigit , "primIsAlpha" |-> mkPrimFun1 isAlpha , "primIsSpace" |-> mkPrimFun1 isSpace , "primIsAscii" |-> mkPrimFun1 isAscii , "primIsLatin1" |-> mkPrimFun1 isLatin1 , "primIsPrint" |-> mkPrimFun1 isPrint , "primIsHexDigit" |-> mkPrimFun1 isHexDigit , "primToUpper" |-> mkPrimFun1 toUpper , "primToLower" |-> mkPrimFun1 toLower , "primCharToNat" |-> mkPrimFun1 (fromIntegral . fromEnum :: Char -> Nat) , "primCharToNatInjective" |-> primCharToNatInjective , "primNatToChar" |-> mkPrimFun1 (toEnum . fromIntegral . (`mod` 0x110000) :: Nat -> Char) , "primShowChar" |-> mkPrimFun1 (Str . show . pretty . LitChar noRange) -- String functions , "primStringToList" |-> mkPrimFun1 unStr , "primStringToListInjective" |-> primStringToListInjective , "primStringFromList" |-> mkPrimFun1 Str , "primStringAppend" |-> mkPrimFun2 (\s1 s2 -> Str $ unStr s1 ++ unStr s2) , "primStringEquality" |-> mkPrimFun2 ((==) :: Rel Str) , "primShowString" |-> mkPrimFun1 (Str . show . pretty . LitString noRange . unStr) -- Other stuff , "primEraseEquality" |-> primEraseEquality -- This needs to be force : A → ((x : A) → B x) → B x rather than seq because of call-by-name. , "primForce" |-> primForce , "primForceLemma" |-> primForceLemma , "primQNameEquality" |-> mkPrimFun2 ((==) :: Rel QName) , "primQNameLess" |-> mkPrimFun2 ((<) :: Rel QName) , "primShowQName" |-> mkPrimFun1 (Str . prettyShow :: QName -> Str) , "primQNameFixity" |-> mkPrimFun1 (nameFixity . qnameName) , "primMetaEquality" |-> mkPrimFun2 ((==) :: Rel MetaId) , "primMetaLess" |-> mkPrimFun2 ((<) :: Rel MetaId) , "primShowMeta" |-> mkPrimFun1 (Str . prettyShow :: MetaId -> Str) , "primIMin" |-> primIMin' , "primIMax" |-> primIMax' , "primINeg" |-> primINeg' , "primPOr" |-> primPOr , "primComp" |-> primComp , builtinTrans |-> primTrans' , builtinHComp |-> primHComp' , "primIdJ" |-> primIdJ , "primPartial" |-> primPartial' , "primPartialP" |-> primPartialP' , builtinGlue |-> primGlue' , builtin_glue |-> prim_glue' , builtin_unglue |-> prim_unglue' , builtinFaceForall |-> primFaceForall' , "primDepIMin" |-> primDepIMin' , "primIdFace" |-> primIdFace' , "primIdPath" |-> primIdPath' , builtinIdElim |-> primIdElim' , builtinSubOut |-> primSubOut' ] where (|->) = (,) lookupPrimitiveFunction :: String -> TCM PrimitiveImpl lookupPrimitiveFunction x = fromMaybe (typeError $ NoSuchPrimitiveFunction x) (Map.lookup x primitiveFunctions) lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl) lookupPrimitiveFunctionQ q = do let s = case qnameName q of Name _ x _ _ _ -> prettyShow x PrimImpl t pf <- lookupPrimitiveFunction s return (s, PrimImpl t $ pf { primFunName = q }) getBuiltinName :: String -> TCM (Maybe QName) getBuiltinName b = do caseMaybeM (getBuiltin' b) (return Nothing) (Just <.> getName) where getName v = do v <- reduce v case unSpine $ v of Def x _ -> return x Con x _ _ -> return $ conName x Lam _ b -> getName $ unAbs b _ -> __IMPOSSIBLE__ isBuiltin :: QName -> String -> TCM Bool isBuiltin q b = (Just q ==) <$> getBuiltinName b