1 2module Agda.TypeChecking.Monad.Builtin 3 ( module Agda.TypeChecking.Monad.Builtin 4 , module Agda.Syntax.Builtin -- The names are defined here. 5 ) where 6 7import qualified Control.Monad.Fail as Fail 8 9import Control.Monad.Except 10import Control.Monad.Reader 11import Control.Monad.State 12import Control.Monad.Trans.Identity (IdentityT) 13import Control.Monad.Trans.Maybe 14import Control.Monad.Writer 15 16import qualified Data.Map as Map 17import Data.Function ( on ) 18 19import Agda.Syntax.Common 20import Agda.Syntax.Position 21import Agda.Syntax.Literal 22import Agda.Syntax.Builtin 23import Agda.Syntax.Internal as I 24import Agda.TypeChecking.Monad.Base 25-- import Agda.TypeChecking.Functions -- LEADS TO IMPORT CYCLE 26import Agda.TypeChecking.Substitute 27 28import Agda.Utils.ListT 29import Agda.Utils.Monad 30import Agda.Utils.Maybe 31import Agda.Utils.Tuple 32 33import Agda.Utils.Impossible 34 35class ( Functor m 36 , Applicative m 37 , Fail.MonadFail m 38 ) => HasBuiltins m where 39 getBuiltinThing :: String -> m (Maybe (Builtin PrimFun)) 40 41 default getBuiltinThing :: (MonadTrans t, HasBuiltins n, t n ~ m) => String -> m (Maybe (Builtin PrimFun)) 42 getBuiltinThing = lift . getBuiltinThing 43 44instance HasBuiltins m => HasBuiltins (ExceptT e m) 45instance HasBuiltins m => HasBuiltins (IdentityT m) 46instance HasBuiltins m => HasBuiltins (ListT m) 47instance HasBuiltins m => HasBuiltins (MaybeT m) 48instance HasBuiltins m => HasBuiltins (ReaderT e m) 49instance HasBuiltins m => HasBuiltins (StateT s m) 50instance (HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m) 51 52deriving instance HasBuiltins m => HasBuiltins (BlockT m) 53 54instance MonadIO m => HasBuiltins (TCMT m) where 55 getBuiltinThing b = liftM2 mplus (Map.lookup b <$> useTC stLocalBuiltins) 56 (Map.lookup b <$> useTC stImportedBuiltins) 57 58-- If Agda is changed so that the type of a literal can belong to an 59-- inductive family (with at least one index), then the implementation 60-- of split' in Agda.TypeChecking.Coverage should be changed. 61 62litType 63 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) 64 => Literal -> m Type 65litType = \case 66 LitNat n -> do 67 _ <- primZero 68 when (n > 0) $ void $ primSuc 69 el <$> primNat 70 LitWord64 _ -> el <$> primWord64 71 LitFloat _ -> el <$> primFloat 72 LitChar _ -> el <$> primChar 73 LitString _ -> el <$> primString 74 LitQName _ -> el <$> primQName 75 LitMeta _ _ -> el <$> primAgdaMeta 76 where 77 el t = El (mkType 0) t 78 79setBuiltinThings :: BuiltinThings PrimFun -> TCM () 80setBuiltinThings b = stLocalBuiltins `setTCLens` b 81 82bindBuiltinName :: String -> Term -> TCM () 83bindBuiltinName b x = do 84 builtin <- getBuiltinThing b 85 case builtin of 86 Just (Builtin y) -> typeError $ DuplicateBuiltinBinding b y x 87 Just (Prim _) -> typeError $ NoSuchBuiltinName b 88 Nothing -> stLocalBuiltins `modifyTCLens` Map.insert b (Builtin x) 89 90bindPrimitive :: String -> PrimFun -> TCM () 91bindPrimitive b pf = do 92 builtin <- getBuiltinThing b 93 case builtin of 94 Just (Builtin _) -> typeError $ NoSuchPrimitiveFunction b 95 Just (Prim x) -> typeError $ (DuplicatePrimitiveBinding b `on` primFunName) x pf 96 Nothing -> stLocalBuiltins `modifyTCLens` Map.insert b (Prim pf) 97 98getBuiltin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) 99 => String -> m Term 100getBuiltin x = 101 fromMaybeM (typeError $ NoBindingForBuiltin x) $ getBuiltin' x 102 103getBuiltin' :: HasBuiltins m => String -> m (Maybe Term) 104getBuiltin' x = do 105 builtin <- getBuiltinThing x 106 case builtin of 107 Just (Builtin t) -> return $ Just $ killRange t 108 _ -> return Nothing 109 110getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun) 111getPrimitive' x = (getPrim =<<) <$> getBuiltinThing x 112 where 113 getPrim (Prim pf) = return pf 114 getPrim _ = Nothing 115 116getPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) 117 => String -> m PrimFun 118getPrimitive x = 119 fromMaybeM (typeError $ NoSuchPrimitiveFunction x) $ getPrimitive' x 120 121getPrimitiveTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) 122 => String -> m Term 123getPrimitiveTerm x = (`Def` []) . primFunName <$> getPrimitive x 124 125getPrimitiveTerm' :: HasBuiltins m => String -> m (Maybe Term) 126getPrimitiveTerm' x = fmap (`Def` []) <$> getPrimitiveName' x 127 128getTerm' :: HasBuiltins m => String -> m (Maybe Term) 129getTerm' x = mplus <$> getBuiltin' x <*> getPrimitiveTerm' x 130 131getName' :: HasBuiltins m => String -> m (Maybe QName) 132getName' x = mplus <$> getBuiltinName' x <*> getPrimitiveName' x 133 134-- | @getTerm use name@ looks up @name@ as a primitive or builtin, and 135-- throws an error otherwise. 136-- The @use@ argument describes how the name is used for the sake of 137-- the error message. 138getTerm :: (HasBuiltins m) => String -> String -> m Term 139getTerm use name = flip fromMaybeM (getTerm' name) $ 140 return $! throwImpossible (ImpMissingDefinitions [name] use) 141 142 143-- | Rewrite a literal to constructor form if possible. 144constructorForm :: HasBuiltins m => Term -> m Term 145constructorForm v = do 146 let pZero = fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinZero 147 pSuc = fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSuc 148 constructorForm' pZero pSuc v 149 150constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term 151constructorForm' pZero pSuc v = 152 case v of 153 Lit (LitNat n) 154 | n == 0 -> pZero 155 | n > 0 -> (`apply1` Lit (LitNat $ n - 1)) <$> pSuc 156 | otherwise -> pure v 157 _ -> pure v 158 159--------------------------------------------------------------------------- 160-- * The names of built-in things 161--------------------------------------------------------------------------- 162 163primInteger, primIntegerPos, primIntegerNegSuc, 164 primFloat, primChar, primString, primUnit, primUnitUnit, primBool, primTrue, primFalse, 165 primSigma, 166 primList, primNil, primCons, primIO, primNat, primSuc, primZero, primMaybe, primNothing, primJust, 167 primPath, primPathP, primInterval, primIZero, primIOne, primPartial, primPartialP, 168 primIMin, primIMax, primINeg, 169 primIsOne, primItIsOne, primIsOne1, primIsOne2, primIsOneEmpty, 170 primSub, primSubIn, primSubOut, 171 primTrans, primHComp, 172 primId, primConId, primIdElim, 173 primEquiv, primEquivFun, primEquivProof, 174 primTranspProof, 175 primGlue, prim_glue, prim_unglue, 176 prim_glueU, prim_unglueU, 177 primFaceForall, 178 primNatPlus, primNatMinus, primNatTimes, primNatDivSucAux, primNatModSucAux, 179 primNatEquality, primNatLess, 180 -- Machine words 181 primWord64, 182 primSizeUniv, primSize, primSizeLt, primSizeSuc, primSizeInf, primSizeMax, 183 primInf, primSharp, primFlat, 184 primEquality, primRefl, 185 primRewrite, -- Name of rewrite relation 186 primLevel, primLevelZero, primLevelSuc, primLevelMax, 187 primLockUniv, 188 primSet, primProp, primSetOmega, primStrictSet, primSSetOmega, 189 primFromNat, primFromNeg, primFromString, 190 -- builtins for reflection: 191 primQName, primArgInfo, primArgArgInfo, primArg, primArgArg, primAbs, primAbsAbs, primAgdaTerm, primAgdaTermVar, 192 primAgdaTermLam, primAgdaTermExtLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi, 193 primAgdaTermSort, primAgdaTermLit, primAgdaTermUnsupported, primAgdaTermMeta, 194 primAgdaErrorPart, primAgdaErrorPartString, primAgdaErrorPartTerm, primAgdaErrorPartName, 195 primHiding, primHidden, primInstance, primVisible, 196 primRelevance, primRelevant, primIrrelevant, 197 primQuantity, primQuantity0, primQuantityω, 198 primModality, primModalityConstructor, 199 primAssoc, primAssocLeft, primAssocRight, primAssocNon, 200 primPrecedence, primPrecRelated, primPrecUnrelated, 201 primFixity, primFixityFixity, 202 primAgdaLiteral, primAgdaLitNat, primAgdaLitWord64, primAgdaLitFloat, primAgdaLitString, primAgdaLitChar, primAgdaLitQName, primAgdaLitMeta, 203 primAgdaSort, primAgdaSortSet, primAgdaSortLit, primAgdaSortProp, primAgdaSortPropLit, primAgdaSortInf, primAgdaSortUnsupported, 204 primAgdaDefinition, primAgdaDefinitionFunDef, primAgdaDefinitionDataDef, primAgdaDefinitionRecordDef, 205 primAgdaDefinitionPostulate, primAgdaDefinitionPrimitive, primAgdaDefinitionDataConstructor, 206 primAgdaClause, primAgdaClauseClause, primAgdaClauseAbsurd, 207 primAgdaPattern, primAgdaPatCon, primAgdaPatVar, primAgdaPatDot, 208 primAgdaPatLit, primAgdaPatProj, 209 primAgdaPatAbsurd, 210 primAgdaMeta, 211 primAgdaTCM, primAgdaTCMReturn, primAgdaTCMBind, primAgdaTCMUnify, 212 primAgdaTCMTypeError, primAgdaTCMInferType, primAgdaTCMCheckType, 213 primAgdaTCMNormalise, primAgdaTCMReduce, 214 primAgdaTCMCatchError, primAgdaTCMGetContext, primAgdaTCMExtendContext, primAgdaTCMInContext, 215 primAgdaTCMFreshName, primAgdaTCMDeclareDef, primAgdaTCMDeclarePostulate, primAgdaTCMDefineFun, 216 primAgdaTCMGetType, primAgdaTCMGetDefinition, 217 primAgdaTCMQuoteTerm, primAgdaTCMUnquoteTerm, primAgdaTCMQuoteOmegaTerm, 218 primAgdaTCMBlockOnMeta, primAgdaTCMCommit, primAgdaTCMIsMacro, 219 primAgdaTCMWithNormalisation, primAgdaTCMDebugPrint, primAgdaTCMWithReconsParams, 220 primAgdaTCMOnlyReduceDefs, primAgdaTCMDontReduceDefs, 221 primAgdaTCMNoConstraints, 222 primAgdaTCMRunSpeculative, 223 primAgdaTCMExec 224 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term 225 226primInteger = getBuiltin builtinInteger 227primIntegerPos = getBuiltin builtinIntegerPos 228primIntegerNegSuc = getBuiltin builtinIntegerNegSuc 229primFloat = getBuiltin builtinFloat 230primChar = getBuiltin builtinChar 231primString = getBuiltin builtinString 232primBool = getBuiltin builtinBool 233primSigma = getBuiltin builtinSigma 234primUnit = getBuiltin builtinUnit 235primUnitUnit = getBuiltin builtinUnitUnit 236primTrue = getBuiltin builtinTrue 237primFalse = getBuiltin builtinFalse 238primList = getBuiltin builtinList 239primNil = getBuiltin builtinNil 240primCons = getBuiltin builtinCons 241primMaybe = getBuiltin builtinMaybe 242primNothing = getBuiltin builtinNothing 243primJust = getBuiltin builtinJust 244primIO = getBuiltin builtinIO 245primId = getBuiltin builtinId 246primConId = getBuiltin builtinConId 247primIdElim = getPrimitiveTerm builtinIdElim 248primPath = getBuiltin builtinPath 249primPathP = getBuiltin builtinPathP 250primInterval = getBuiltin builtinInterval 251primIZero = getBuiltin builtinIZero 252primIOne = getBuiltin builtinIOne 253primIMin = getPrimitiveTerm builtinIMin 254primIMax = getPrimitiveTerm builtinIMax 255primINeg = getPrimitiveTerm builtinINeg 256primPartial = getPrimitiveTerm "primPartial" 257primPartialP = getPrimitiveTerm "primPartialP" 258primIsOne = getBuiltin builtinIsOne 259primItIsOne = getBuiltin builtinItIsOne 260primTrans = getPrimitiveTerm builtinTrans 261primHComp = getPrimitiveTerm builtinHComp 262primEquiv = getBuiltin builtinEquiv 263primEquivFun = getBuiltin builtinEquivFun 264primEquivProof = getBuiltin builtinEquivProof 265primTranspProof = getBuiltin builtinTranspProof 266prim_glueU = getPrimitiveTerm builtin_glueU 267prim_unglueU = getPrimitiveTerm builtin_unglueU 268primGlue = getPrimitiveTerm builtinGlue 269prim_glue = getPrimitiveTerm builtin_glue 270prim_unglue = getPrimitiveTerm builtin_unglue 271primFaceForall = getPrimitiveTerm builtinFaceForall 272primIsOne1 = getBuiltin builtinIsOne1 273primIsOne2 = getBuiltin builtinIsOne2 274primIsOneEmpty = getBuiltin builtinIsOneEmpty 275primSub = getBuiltin builtinSub 276primSubIn = getBuiltin builtinSubIn 277primSubOut = getPrimitiveTerm builtinSubOut 278primNat = getBuiltin builtinNat 279primSuc = getBuiltin builtinSuc 280primZero = getBuiltin builtinZero 281primNatPlus = getBuiltin builtinNatPlus 282primNatMinus = getBuiltin builtinNatMinus 283primNatTimes = getBuiltin builtinNatTimes 284primNatDivSucAux = getBuiltin builtinNatDivSucAux 285primNatModSucAux = getBuiltin builtinNatModSucAux 286primNatEquality = getBuiltin builtinNatEquals 287primNatLess = getBuiltin builtinNatLess 288primWord64 = getBuiltin builtinWord64 289primSizeUniv = getBuiltin builtinSizeUniv 290primSize = getBuiltin builtinSize 291primSizeLt = getBuiltin builtinSizeLt 292primSizeSuc = getBuiltin builtinSizeSuc 293primSizeInf = getBuiltin builtinSizeInf 294primSizeMax = getBuiltin builtinSizeMax 295primInf = getBuiltin builtinInf 296primSharp = getBuiltin builtinSharp 297primFlat = getBuiltin builtinFlat 298primEquality = getBuiltin builtinEquality 299primRefl = getBuiltin builtinRefl 300primRewrite = getBuiltin builtinRewrite 301primLevel = getBuiltin builtinLevel 302primLevelZero = getBuiltin builtinLevelZero 303primLevelSuc = getBuiltin builtinLevelSuc 304primLevelMax = getBuiltin builtinLevelMax 305primSet = getBuiltin builtinSet 306primProp = getBuiltin builtinProp 307primSetOmega = getBuiltin builtinSetOmega 308primLockUniv = getPrimitiveTerm builtinLockUniv 309primSSetOmega = getBuiltin builtinSSetOmega 310primStrictSet = getBuiltin builtinStrictSet 311primFromNat = getBuiltin builtinFromNat 312primFromNeg = getBuiltin builtinFromNeg 313primFromString = getBuiltin builtinFromString 314primQName = getBuiltin builtinQName 315primArg = getBuiltin builtinArg 316primArgArg = getBuiltin builtinArgArg 317primAbs = getBuiltin builtinAbs 318primAbsAbs = getBuiltin builtinAbsAbs 319primAgdaSort = getBuiltin builtinAgdaSort 320primHiding = getBuiltin builtinHiding 321primHidden = getBuiltin builtinHidden 322primInstance = getBuiltin builtinInstance 323primVisible = getBuiltin builtinVisible 324primRelevance = getBuiltin builtinRelevance 325primRelevant = getBuiltin builtinRelevant 326primIrrelevant = getBuiltin builtinIrrelevant 327primQuantity = getBuiltin builtinQuantity 328primQuantity0 = getBuiltin builtinQuantity0 329primQuantityω = getBuiltin builtinQuantityω 330primModality = getBuiltin builtinModality 331primModalityConstructor = getBuiltin builtinModalityConstructor 332primAssoc = getBuiltin builtinAssoc 333primAssocLeft = getBuiltin builtinAssocLeft 334primAssocRight = getBuiltin builtinAssocRight 335primAssocNon = getBuiltin builtinAssocNon 336primPrecedence = getBuiltin builtinPrecedence 337primPrecRelated = getBuiltin builtinPrecRelated 338primPrecUnrelated = getBuiltin builtinPrecUnrelated 339primFixity = getBuiltin builtinFixity 340primFixityFixity = getBuiltin builtinFixityFixity 341primArgInfo = getBuiltin builtinArgInfo 342primArgArgInfo = getBuiltin builtinArgArgInfo 343primAgdaSortSet = getBuiltin builtinAgdaSortSet 344primAgdaSortLit = getBuiltin builtinAgdaSortLit 345primAgdaSortProp = getBuiltin builtinAgdaSortProp 346primAgdaSortPropLit = getBuiltin builtinAgdaSortPropLit 347primAgdaSortInf = getBuiltin builtinAgdaSortInf 348primAgdaSortUnsupported = getBuiltin builtinAgdaSortUnsupported 349primAgdaTerm = getBuiltin builtinAgdaTerm 350primAgdaTermVar = getBuiltin builtinAgdaTermVar 351primAgdaTermLam = getBuiltin builtinAgdaTermLam 352primAgdaTermExtLam = getBuiltin builtinAgdaTermExtLam 353primAgdaTermDef = getBuiltin builtinAgdaTermDef 354primAgdaTermCon = getBuiltin builtinAgdaTermCon 355primAgdaTermPi = getBuiltin builtinAgdaTermPi 356primAgdaTermSort = getBuiltin builtinAgdaTermSort 357primAgdaTermLit = getBuiltin builtinAgdaTermLit 358primAgdaTermUnsupported = getBuiltin builtinAgdaTermUnsupported 359primAgdaTermMeta = getBuiltin builtinAgdaTermMeta 360primAgdaErrorPart = getBuiltin builtinAgdaErrorPart 361primAgdaErrorPartString = getBuiltin builtinAgdaErrorPartString 362primAgdaErrorPartTerm = getBuiltin builtinAgdaErrorPartTerm 363primAgdaErrorPartName = getBuiltin builtinAgdaErrorPartName 364primAgdaLiteral = getBuiltin builtinAgdaLiteral 365primAgdaLitNat = getBuiltin builtinAgdaLitNat 366primAgdaLitWord64 = getBuiltin builtinAgdaLitWord64 367primAgdaLitFloat = getBuiltin builtinAgdaLitFloat 368primAgdaLitChar = getBuiltin builtinAgdaLitChar 369primAgdaLitString = getBuiltin builtinAgdaLitString 370primAgdaLitQName = getBuiltin builtinAgdaLitQName 371primAgdaLitMeta = getBuiltin builtinAgdaLitMeta 372primAgdaPattern = getBuiltin builtinAgdaPattern 373primAgdaPatCon = getBuiltin builtinAgdaPatCon 374primAgdaPatVar = getBuiltin builtinAgdaPatVar 375primAgdaPatDot = getBuiltin builtinAgdaPatDot 376primAgdaPatLit = getBuiltin builtinAgdaPatLit 377primAgdaPatProj = getBuiltin builtinAgdaPatProj 378primAgdaPatAbsurd = getBuiltin builtinAgdaPatAbsurd 379primAgdaClause = getBuiltin builtinAgdaClause 380primAgdaClauseClause = getBuiltin builtinAgdaClauseClause 381primAgdaClauseAbsurd = getBuiltin builtinAgdaClauseAbsurd 382primAgdaDefinitionFunDef = getBuiltin builtinAgdaDefinitionFunDef 383primAgdaDefinitionDataDef = getBuiltin builtinAgdaDefinitionDataDef 384primAgdaDefinitionRecordDef = getBuiltin builtinAgdaDefinitionRecordDef 385primAgdaDefinitionDataConstructor = getBuiltin builtinAgdaDefinitionDataConstructor 386primAgdaDefinitionPostulate = getBuiltin builtinAgdaDefinitionPostulate 387primAgdaDefinitionPrimitive = getBuiltin builtinAgdaDefinitionPrimitive 388primAgdaDefinition = getBuiltin builtinAgdaDefinition 389primAgdaMeta = getBuiltin builtinAgdaMeta 390primAgdaTCM = getBuiltin builtinAgdaTCM 391primAgdaTCMReturn = getBuiltin builtinAgdaTCMReturn 392primAgdaTCMBind = getBuiltin builtinAgdaTCMBind 393primAgdaTCMUnify = getBuiltin builtinAgdaTCMUnify 394primAgdaTCMTypeError = getBuiltin builtinAgdaTCMTypeError 395primAgdaTCMInferType = getBuiltin builtinAgdaTCMInferType 396primAgdaTCMCheckType = getBuiltin builtinAgdaTCMCheckType 397primAgdaTCMNormalise = getBuiltin builtinAgdaTCMNormalise 398primAgdaTCMReduce = getBuiltin builtinAgdaTCMReduce 399primAgdaTCMCatchError = getBuiltin builtinAgdaTCMCatchError 400primAgdaTCMGetContext = getBuiltin builtinAgdaTCMGetContext 401primAgdaTCMExtendContext = getBuiltin builtinAgdaTCMExtendContext 402primAgdaTCMInContext = getBuiltin builtinAgdaTCMInContext 403primAgdaTCMFreshName = getBuiltin builtinAgdaTCMFreshName 404primAgdaTCMDeclareDef = getBuiltin builtinAgdaTCMDeclareDef 405primAgdaTCMDeclarePostulate = getBuiltin builtinAgdaTCMDeclarePostulate 406primAgdaTCMDefineFun = getBuiltin builtinAgdaTCMDefineFun 407primAgdaTCMGetType = getBuiltin builtinAgdaTCMGetType 408primAgdaTCMGetDefinition = getBuiltin builtinAgdaTCMGetDefinition 409primAgdaTCMQuoteTerm = getBuiltin builtinAgdaTCMQuoteTerm 410primAgdaTCMQuoteOmegaTerm = getBuiltin builtinAgdaTCMQuoteOmegaTerm 411primAgdaTCMUnquoteTerm = getBuiltin builtinAgdaTCMUnquoteTerm 412primAgdaTCMBlockOnMeta = getBuiltin builtinAgdaTCMBlockOnMeta 413primAgdaTCMCommit = getBuiltin builtinAgdaTCMCommit 414primAgdaTCMIsMacro = getBuiltin builtinAgdaTCMIsMacro 415primAgdaTCMWithNormalisation = getBuiltin builtinAgdaTCMWithNormalisation 416primAgdaTCMWithReconsParams = getBuiltin builtinAgdaTCMWithReconsParams 417primAgdaTCMDebugPrint = getBuiltin builtinAgdaTCMDebugPrint 418primAgdaTCMOnlyReduceDefs = getBuiltin builtinAgdaTCMOnlyReduceDefs 419primAgdaTCMDontReduceDefs = getBuiltin builtinAgdaTCMDontReduceDefs 420primAgdaTCMNoConstraints = getBuiltin builtinAgdaTCMNoConstraints 421primAgdaTCMRunSpeculative = getBuiltin builtinAgdaTCMRunSpeculative 422primAgdaTCMExec = getBuiltin builtinAgdaTCMExec 423 424-- | The coinductive primitives. 425 426data CoinductionKit = CoinductionKit 427 { nameOfInf :: QName 428 , nameOfSharp :: QName 429 , nameOfFlat :: QName 430 } 431 432-- | Tries to build a 'CoinductionKit'. 433 434coinductionKit' :: TCM CoinductionKit 435coinductionKit' = do 436 Def inf _ <- primInf 437 Def sharp _ <- primSharp 438 Def flat _ <- primFlat 439 return $ CoinductionKit 440 { nameOfInf = inf 441 , nameOfSharp = sharp 442 , nameOfFlat = flat 443 } 444 445coinductionKit :: TCM (Maybe CoinductionKit) 446coinductionKit = tryMaybe coinductionKit' 447 448-- | Sort primitives. 449 450data SortKit = SortKit 451 { nameOfSet :: QName 452 , nameOfProp :: QName 453 , nameOfSSet :: QName 454 , nameOfSetOmega :: IsFibrant -> QName 455 } 456 457sortKit :: HasBuiltins m => m SortKit 458sortKit = do 459 Def set _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSet 460 Def prop _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinProp 461 Def setomega _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSetOmega 462 Def sset _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinStrictSet 463 Def ssetomega _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSSetOmega 464 return $ SortKit 465 { nameOfSet = set 466 , nameOfProp = prop 467 , nameOfSSet = sset 468 , nameOfSetOmega = \case 469 IsFibrant -> setomega 470 IsStrict -> ssetomega 471 } 472 473 474------------------------------------------------------------------------ 475-- * Path equality 476------------------------------------------------------------------------ 477 478getPrimName :: Term -> QName 479getPrimName ty = do 480 let lamV (Lam i b) = mapFst (getHiding i :) $ lamV (unAbs b) 481 lamV (Pi _ b) = lamV (unEl $ unAbs b) 482 lamV v = ([], v) 483 case lamV ty of 484 (_, Def path _) -> path 485 (_, Con nm _ _) -> conName nm 486 (_, Var 0 [Proj _ l]) -> l 487 (_, t) -> __IMPOSSIBLE__ 488 489getBuiltinName', getPrimitiveName' :: HasBuiltins m => String -> m (Maybe QName) 490getBuiltinName' n = fmap getPrimName <$> getBuiltin' n 491getPrimitiveName' n = fmap primFunName <$> getPrimitive' n 492 493isPrimitive :: HasBuiltins m => String -> QName -> m Bool 494isPrimitive n q = (Just q ==) <$> getPrimitiveName' n 495 496intervalView' :: HasBuiltins m => m (Term -> IntervalView) 497intervalView' = do 498 iz <- getBuiltinName' builtinIZero 499 io <- getBuiltinName' builtinIOne 500 imax <- getPrimitiveName' "primIMax" 501 imin <- getPrimitiveName' "primIMin" 502 ineg <- getPrimitiveName' "primINeg" 503 return $ \ t -> 504 case t of 505 Def q es -> 506 case es of 507 [Apply x,Apply y] | Just q == imin -> IMin x y 508 [Apply x,Apply y] | Just q == imax -> IMax x y 509 [Apply x] | Just q == ineg -> INeg x 510 _ -> OTerm t 511 Con q _ [] | Just (conName q) == iz -> IZero 512 | Just (conName q) == io -> IOne 513 _ -> OTerm t 514 515intervalView :: HasBuiltins m => Term -> m IntervalView 516intervalView t = do 517 f <- intervalView' 518 return (f t) 519 520intervalUnview :: HasBuiltins m => IntervalView -> m Term 521intervalUnview t = do 522 f <- intervalUnview' 523 return (f t) 524 525intervalUnview' :: HasBuiltins m => m (IntervalView -> Term) 526intervalUnview' = do 527 iz <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIZero -- should it be a type error instead? 528 io <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIOne 529 imin <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' "primIMin" 530 imax <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' "primIMax" 531 ineg <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' "primINeg" 532 return $ \ v -> case v of 533 IZero -> iz 534 IOne -> io 535 IMin x y -> apply imin [x,y] 536 IMax x y -> apply imax [x,y] 537 INeg x -> apply ineg [x] 538 OTerm t -> t 539 540------------------------------------------------------------------------ 541-- * Path equality 542------------------------------------------------------------------------ 543 544-- | Check whether the type is actually an path (lhs ≡ rhs) 545-- and extract lhs, rhs, and their type. 546-- 547-- Precondition: type is reduced. 548 549pathView :: HasBuiltins m => Type -> m PathView 550pathView t0 = do 551 view <- pathView' 552 return $ view t0 553 554pathView' :: HasBuiltins m => m (Type -> PathView) 555pathView' = do 556 mpath <- getBuiltinName' builtinPath 557 mpathp <- getBuiltinName' builtinPathP 558 return $ \ t0@(El s t) -> 559 case t of 560 Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ] 561 | Just path' == mpath, Just path <- mpathp -> PathType s path level (lam_i <$> typ) lhs rhs 562 where lam_i = Lam defaultArgInfo . NoAbs "_" 563 Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ] 564 | Just path' == mpathp, Just path <- mpathp -> PathType s path level typ lhs rhs 565 _ -> OType t0 566 567-- | Non dependent Path 568idViewAsPath :: HasBuiltins m => Type -> m PathView 569idViewAsPath t0@(El s t) = do 570 mid <- fmap getPrimName <$> getBuiltin' builtinId 571 mpath <- fmap getPrimName <$> getBuiltin' builtinPath 572 case mid of 573 Just path | isJust mpath -> case t of 574 Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ] 575 | path' == path -> return $ PathType s (fromJust mpath) level typ lhs rhs 576 _ -> return $ OType t0 577 _ -> return $ OType t0 578 579boldPathView :: Type -> PathView 580boldPathView t0@(El s t) = do 581 case t of 582 Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ] 583 -> PathType s path' level typ lhs rhs 584 _ -> OType t0 585 586-- | Revert the 'PathView'. 587-- 588-- Postcondition: type is reduced. 589 590pathUnview :: PathView -> Type 591pathUnview (OType t) = t 592pathUnview (PathType s path l t lhs rhs) = 593 El s $ Def path $ map Apply [l, t, lhs, rhs] 594 595------------------------------------------------------------------------ 596-- * Builtin equality 597------------------------------------------------------------------------ 598 599-- | Get the name of the equality type. 600primEqualityName :: TCM QName 601-- primEqualityName = getDef =<< primEquality -- LEADS TO IMPORT CYCLE 602primEqualityName = do 603 eq <- primEquality 604 -- Andreas, 2014-05-17 moved this here from TC.Rules.Def 605 -- Don't know why up to 2 hidden lambdas need to be stripped, 606 -- but I left the code in place. 607 -- Maybe it was intended that equality could be declared 608 -- in three different ways: 609 -- 1. universe and type polymorphic 610 -- 2. type polymorphic only 611 -- 3. monomorphic. 612 let lamV (Lam i b) = mapFst (getHiding i :) $ lamV (unAbs b) 613 lamV v = ([], v) 614 return $ case lamV eq of 615 (_, Def equality _) -> equality 616 _ -> __IMPOSSIBLE__ 617 618-- | Check whether the type is actually an equality (lhs ≡ rhs) 619-- and extract lhs, rhs, and their type. 620-- 621-- Precondition: type is reduced. 622 623equalityView :: Type -> TCM EqualityView 624equalityView t0@(El s t) = do 625 equality <- primEqualityName 626 case t of 627 Def equality' es | equality' == equality -> do 628 let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es 629 let n = length vs 630 unless (n >= 3) __IMPOSSIBLE__ 631 let (pars, [ typ , lhs, rhs ]) = splitAt (n-3) vs 632 return $ EqualityType s equality pars typ lhs rhs 633 _ -> return $ OtherType t0 634 635-- | Revert the 'EqualityView'. 636-- 637-- Postcondition: type is reduced. 638 639equalityUnview :: EqualityView -> Type 640equalityUnview (OtherType t) = t 641equalityUnview (IdiomType t) = t 642equalityUnview (EqualityType s equality l t lhs rhs) = 643 El s $ Def equality $ map Apply (l ++ [t, lhs, rhs]) 644 645-- | Primitives with typechecking constrants. 646constrainedPrims :: [String] 647constrainedPrims = 648 [ builtinConId 649 , builtinPOr 650 , builtinComp 651 , builtinHComp 652 , builtinTrans 653 , builtin_glue 654 , builtin_glueU 655 ] 656 657getNameOfConstrained :: HasBuiltins m => String -> m (Maybe QName) 658getNameOfConstrained s = do 659 unless (s `elem` constrainedPrims) __IMPOSSIBLE__ 660 getName' s 661