summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/Builtin.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/Builtin.hs')
-rw-r--r--src/full/Agda/TypeChecking/Rules/Builtin.hs52
1 files changed, 35 insertions, 17 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/Builtin.hs b/src/full/Agda/TypeChecking/Rules/Builtin.hs
index 9b4a20a..1642962 100644
--- a/src/full/Agda/TypeChecking/Rules/Builtin.hs
+++ b/src/full/Agda/TypeChecking/Rules/Builtin.hs
@@ -1,7 +1,5 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TupleSections #-}
module Agda.TypeChecking.Rules.Builtin
( bindBuiltin
@@ -13,6 +11,8 @@ module Agda.TypeChecking.Rules.Builtin
import Control.Applicative hiding (empty)
import Control.Monad
+import Control.Monad.Reader (ask)
+import Control.Monad.State (get)
import Data.List (find)
import qualified Agda.Syntax.Abstract as A
@@ -102,7 +102,22 @@ coreBuiltins = map (\ (x, z) -> BuiltinInfo x z)
return (sort $ varSort 1))
[builtinRefl])
, (builtinHiding |-> BuiltinData tset [builtinHidden, builtinInstance, builtinVisible])
+ -- Relevance
, (builtinRelevance |-> BuiltinData tset [builtinRelevant, builtinIrrelevant])
+ , (builtinRelevant |-> BuiltinDataCons trelevance)
+ , (builtinIrrelevant |-> BuiltinDataCons trelevance)
+ -- Associativity
+ , builtinAssoc |-> BuiltinData tset [builtinAssocLeft, builtinAssocRight, builtinAssocNon]
+ , builtinAssocLeft |-> BuiltinDataCons tassoc
+ , builtinAssocRight |-> BuiltinDataCons tassoc
+ , builtinAssocNon |-> BuiltinDataCons tassoc
+ -- Precedence
+ , builtinPrecedence |-> BuiltinData tset [builtinPrecRelated, builtinPrecUnrelated]
+ , builtinPrecRelated |-> BuiltinDataCons (tint --> tprec)
+ , builtinPrecUnrelated |-> BuiltinDataCons tprec
+ -- Fixity
+ , builtinFixity |-> BuiltinData tset [builtinFixityFixity]
+ , builtinFixityFixity |-> BuiltinDataCons (tassoc --> tprec --> tfixity)
, (builtinRefl |-> BuiltinDataCons (hPi "a" (el primLevel) $
hPi "A" (return $ sort $ varSort 0) $
hPi "x" (El (varSort 1) <$> varM 0) $
@@ -136,8 +151,6 @@ coreBuiltins = map (\ (x, z) -> BuiltinInfo x z)
, (builtinHidden |-> BuiltinDataCons thiding)
, (builtinInstance |-> BuiltinDataCons thiding)
, (builtinVisible |-> BuiltinDataCons thiding)
- , (builtinRelevant |-> BuiltinDataCons trelevance)
- , (builtinIrrelevant |-> BuiltinDataCons trelevance)
, (builtinSizeUniv |-> builtinPostulate tSizeUniv) -- SizeUniv : SizeUniv
-- See comment on tSizeUniv: the following does not work currently.
-- , (builtinSizeUniv |-> builtinPostulate tSetOmega) -- SizeUniv : SetĪ‰
@@ -188,6 +201,7 @@ coreBuiltins = map (\ (x, z) -> BuiltinInfo x z)
, builtinAgdaTCMInferType |-> builtinPostulate (tterm --> tTCM_ primAgdaTerm)
, builtinAgdaTCMCheckType |-> builtinPostulate (tterm --> ttype --> tTCM_ primAgdaTerm)
, builtinAgdaTCMNormalise |-> builtinPostulate (tterm --> tTCM_ primAgdaTerm)
+ , builtinAgdaTCMReduce |-> builtinPostulate (tterm --> tTCM_ primAgdaTerm)
, builtinAgdaTCMCatchError |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tTCM 1 (varM 0) --> tTCM 1 (varM 0) --> tTCM 1 (varM 0))
, builtinAgdaTCMGetContext |-> builtinPostulate (tTCM_ (unEl <$> tlist (targ ttype)))
, builtinAgdaTCMExtendContext |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ targ ttype --> tTCM 1 (varM 0) --> tTCM 1 (varM 0))
@@ -201,6 +215,8 @@ coreBuiltins = map (\ (x, z) -> BuiltinInfo x z)
, builtinAgdaTCMUnquoteTerm |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tterm --> tTCM 1 (varM 0))
, builtinAgdaTCMBlockOnMeta |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tmeta --> tTCM 1 (varM 0))
, builtinAgdaTCMCommit |-> builtinPostulate (tTCM_ primUnit)
+ , builtinAgdaTCMIsMacro |-> builtinPostulate (tqname --> tTCM_ primBool)
+ , builtinAgdaTCMWithNormalisation |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tbool --> tTCM 1 (varM 0) --> tTCM 1 (varM 0))
]
where
(|->) = (,)
@@ -230,6 +246,7 @@ coreBuiltins = map (\ (x, z) -> BuiltinInfo x z)
tterm = el primAgdaTerm
terrorpart = el primAgdaErrorPart
tnat = el primNat
+ tint = el primInteger
tunit = el primUnit
tinteger = el primInteger
tfloat = el primFloat
@@ -241,6 +258,9 @@ coreBuiltins = map (\ (x, z) -> BuiltinInfo x z)
tbool = el primBool
thiding = el primHiding
trelevance = el primRelevance
+ tassoc = el primAssoc
+ tprec = el primPrecedence
+ tfixity = el primFixity
-- tcolors = el (list primAgdaTerm) -- TODO guilhem
targinfo = el primArgInfo
ttype = el primAgdaTerm
@@ -365,7 +385,7 @@ coreBuiltins = map (\ (x, z) -> BuiltinInfo x z)
suc n = s `apply1` n
choice = foldr1 (\x y -> x `catchError` \_ -> y)
xs <- mapM freshName_ xs
- addCtxs xs (domFromArg $ defaultArg nat) $ f apply1 zero suc (==) (===) choice
+ addContext (xs, domFromArg $ defaultArg nat) $ f apply1 zero suc (==) (===) choice
inductiveCheck :: String -> Int -> Term -> TCM ()
@@ -397,7 +417,7 @@ bindPostulatedName ::
String -> A.Expr -> (QName -> Definition -> TCM Term) -> TCM ()
bindPostulatedName builtin e m = do
q <- getName e
- def <- ignoreAbstractMode $ getConstInfo q
+ def <- getConstInfo q
case theDef def of
Axiom {} -> bindBuiltinName builtin =<< m q def
_ -> err
@@ -456,7 +476,7 @@ bindBuiltinUnit t = do
case def of
Record { recFields = [], recConHead = con } -> do
bindBuiltinName builtinUnit t
- bindBuiltinName builtinUnitUnit (Con con [])
+ bindBuiltinName builtinUnitUnit (Con con ConOSystem [])
_ -> genericError "Builtin UNIT must be a singleton record type"
bindBuiltinInfo :: BuiltinInfo -> A.Expr -> TCM ()
@@ -477,17 +497,17 @@ bindBuiltinInfo (BuiltinInfo s d) e = do
BuiltinDataCons t -> do
let name (Lam h b) = name (absBody b)
- name (Con c _) = Con c []
+ name (Con c ci _) = Con c ci []
name (Shared p) = name $ ignoreSharing (derefPtr p)
name _ = __IMPOSSIBLE__
e' <- checkExpr e =<< t
case e of
- A.Con _ -> return ()
+ A.Con{} -> return ()
_ -> typeError $ BuiltinMustBeConstructor s e
- let v@(Con h []) = name e'
+ let v@(Con h _ []) = name e'
c = conName h
when (s == builtinTrue) $ addHaskellCode c "Bool" "True"
when (s == builtinFalse) $ addHaskellCode c "Bool" "False"
@@ -521,7 +541,7 @@ bindBuiltinInfo (BuiltinInfo s d) e = do
"The argument to BUILTIN " ++ s ++ " must be a postulated name"
case e of
A.Def q -> do
- def <- ignoreAbstractMode $ getConstInfo q
+ def <- getConstInfo q
case theDef def of
Axiom {} -> do
builtinSizeHook s q t'
@@ -552,9 +572,7 @@ bindBuiltin b e = do
_ | Just i <- find ((b ==) . builtinName) coreBuiltins -> bindBuiltinInfo i e
_ -> typeError $ NoSuchBuiltinName b
where
- nowNat b = genericError $
- "Builtin " ++ b ++ " does no longer exist. " ++
- "It is now bound by BUILTIN " ++ builtinNat
+ nowNat b = warning $ OldBuiltin b builtinNat
isUntypedBuiltin :: String -> Bool
isUntypedBuiltin b = elem b [builtinFromNat, builtinFromNeg, builtinFromString]
@@ -563,8 +581,8 @@ bindUntypedBuiltin :: String -> A.Expr -> TCM ()
bindUntypedBuiltin b e =
case A.unScope e of
A.Def q -> bindBuiltinName b (Def q [])
- A.Proj q -> bindBuiltinName b (Def q [])
- e -> genericError $ "The argument to BUILTIN " ++ b ++ " must be a defined name"
+ A.Proj _ (AmbQ [q]) -> bindBuiltinName b (Def q [])
+ e -> genericError $ "The argument to BUILTIN " ++ b ++ " must be a defined unambiguous name"
-- | Bind a builtin thing to a new name.
bindBuiltinNoDef :: String -> A.QName -> TCM ()
@@ -580,7 +598,7 @@ bindBuiltinNoDef b q = do
-- Andreas, 2015-02-14
-- Special treatment of SizeUniv, should maybe be a primitive.
def | b == builtinSizeUniv = emptyFunction
- { funClauses = [ (empty :: Clause) { clauseBody = Body $ Sort sSizeUniv } ]
+ { funClauses = [ (empty :: Clause) { clauseBody = Just $ Sort sSizeUniv } ]
, funCompiled = Just (CC.Done [] $ Sort sSizeUniv)
, funTerminates = Just True
}