module Agda.TypeChecking.Monad.Signature where
import Prelude hiding (null)
import Control.Arrow (first, second, (***))
import Control.Applicative hiding (empty)
import Control.Monad.State
import Control.Monad.Reader
import Data.List hiding (null)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Monoid
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Abstract (Ren)
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Position
import qualified Agda.Compiler.JS.Parser as JS
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.Exception ( ExceptionT )
import Agda.TypeChecking.Monad.Mutual
import Agda.TypeChecking.Monad.Open
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.ProjectionLike
import Agda.Utils.Except ( Error )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Map as Map
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Size
import qualified Agda.Utils.HashMap as HMap
#include "undefined.h"
import Agda.Utils.Impossible
addConstant :: QName -> Definition -> TCM ()
addConstant q d = do
reportSLn "tc.signature" 20 $ "adding constant " ++ show q ++ " to signature"
tel <- getContextTelescope
let tel' = replaceEmptyName "r" $ killRange $ case theDef d of
Constructor{} -> fmap (setHiding Hidden) tel
_ -> tel
let d' = abstract tel' $ d { defName = q }
reportSLn "tc.signature" 30 $ "lambda-lifted definition = " ++ show d'
modifySignature $ updateDefinitions $ HMap.insertWith (+++) q d'
i <- currentOrFreshMutualBlock
setMutualBlock i q
where
new +++ old = new { defDisplay = defDisplay new ++ defDisplay old
, defInstance = defInstance new `mplus` defInstance old }
setTerminates :: QName -> Bool -> TCM ()
setTerminates q b = modifySignature $ updateDefinition q $ updateTheDef $ setT
where
setT def@Function{} = def { funTerminates = Just b }
setT def = def
modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
modifyFunClauses q f =
modifySignature $ updateDefinition q $ updateTheDef $ updateFunClauses f
addClauses :: QName -> [Clause] -> TCM ()
addClauses q cls = do
tel <- getContextTelescope
modifyFunClauses q (++ abstract tel cls)
addHaskellCode :: QName -> HaskellType -> HaskellCode -> TCM ()
addHaskellCode q hsTy hsDef = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addHs
where
addHs crep = crep { compiledHaskell = Just $ HsDefn hsTy hsDef }
addHaskellExport :: QName -> HaskellType -> String -> TCM ()
addHaskellExport q hsTy hsName = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addHs
where
addHs crep = crep { exportHaskell = Just (HsExport hsTy hsName)}
addHaskellType :: QName -> HaskellType -> TCM ()
addHaskellType q hsTy = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addHs
where
addHs crep = crep { compiledHaskell = Just $ HsType hsTy }
addEpicCode :: QName -> EpicCode -> TCM ()
addEpicCode q epDef = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addEp
where
addEp crep = crep { compiledEpic = Just epDef }
addJSCode :: QName -> String -> TCM ()
addJSCode q jsDef =
case JS.parse jsDef of
Left e ->
modifySignature $ updateDefinition q $ updateDefCompiledRep $ addJS (Just e)
Right s ->
typeError (CompilationError ("Failed to parse ECMAScript (..." ++ s ++ ") for " ++ show q))
where
addJS e crep = crep { compiledJS = e }
markStatic :: QName -> TCM ()
markStatic q = modifySignature $ updateDefinition q $ mark
where
mark def@Defn{theDef = fun@Function{}} =
def{theDef = fun{funStatic = True}}
mark def = def
unionSignatures :: [Signature] -> Signature
unionSignatures ss = foldr unionSignature emptySignature ss
where
unionSignature (Sig a b c) (Sig a' b' c') =
Sig (Map.union a a')
(HMap.union b b')
(HMap.unionWith mappend c c')
addSection :: ModuleName -> Nat -> TCM ()
addSection m fv = do
tel <- getContextTelescope
let sec = Section tel fv
modifySignature $ \sig -> sig { sigSections = Map.insert m sec $ sigSections sig }
lookupSection :: ModuleName -> TCM Telescope
lookupSection m = do
sig <- sigSections <$> getSignature
isig <- sigSections <$> getImportedSignature
return $ maybe EmptyTel secTelescope $ Map.lookup m sig `mplus` Map.lookup m isig
addDisplayForms :: QName -> TCM ()
addDisplayForms x = do
def <- getConstInfo x
args <- getContextArgs
add (drop (projectionArgs $ theDef def) args) x x []
where
add args top x vs0 = do
def <- getConstInfo x
let cs = defClauses def
isCopy = defCopy def
case cs of
[ Clause{ namedClausePats = pats, clauseBody = b } ]
| isCopy
, all (isVar . namedArg) pats
, Just (m, Def y es) <- strip (b `apply` vs0)
, Just vs <- mapM isApplyElim es -> do
let ps = raise 1 $ map unArg vs
df = Display 0 ps $ DTerm $ Def top $ map Apply args
reportSLn "tc.display.section" 20 $ "adding display form " ++ show y ++ " --> " ++ show top
++ "\n " ++ show df
addDisplayForm y df
add args top y vs
_ -> do
let reason = if not isCopy then "not a copy" else
case cs of
[] -> "no clauses"
_:_:_ -> "many clauses"
[ Clause{ clauseBody = b } ] -> case strip b of
Nothing -> "bad body"
Just (m, Def y es)
| m < length args -> "too few args"
| m > length args -> "too many args"
| otherwise -> "args=" ++ show args ++ " es=" ++ show es
Just (m, v) -> "not a def body"
reportSLn "tc.display.section" 30 $
"no display form from " ++ show x ++ " because " ++ reason
strip (Body v) = return (0, unSpine v)
strip NoBody = Nothing
strip (Bind b) = do
(n, v) <- strip $ absBody b
return (n + 1, ignoreSharing v)
isVar VarP{} = True
isVar _ = False
applySection
:: ModuleName
-> Telescope
-> ModuleName
-> Args
-> Ren QName
-> Ren ModuleName
-> TCM ()
applySection new ptel old ts rd rm = do
reportSLn "tc.mod.apply" 10 $ render $ vcat
[ text "applySection"
, text "new =" <+> text (show new)
, text "ptel =" <+> text (show ptel)
, text "old =" <+> text (show old)
, text "ts =" <+> text (show ts)
]
reportSLn "tc.mod.apply" 80 $ render $ vcat
[ text "arguments: " <+> text (show ts)
]
mapM_ (copyDef ts) rd
mapM_ (copySec ts) rm
mapM_ computePolarity (map snd rd)
where
copyName x = fromMaybe x $ lookup x rd
argsToUse new = do
let m = mnameFromList $ commonPrefix (mnameToList old) (mnameToList new)
reportSLn "tc.mod.apply" 80 $ "Common prefix: " ++ show m
let ms = tail . map mnameFromList . inits . mnameToList $ m
ps <- mapM (maybe 0 secFreeVars <.> getSection) ms
reportSLn "tc.mod.apply" 80 $ " params: " ++ show (zip ms ps)
return $ sum ps
copyDef :: Args -> (QName, QName) -> TCM ()
copyDef ts (x, y) = do
def <- getConstInfo x
np <- argsToUse (qnameModule x)
copyDef' np def
where
copyDef' np d = do
reportSLn "tc.mod.apply" 60 $ "making new def for " ++ show y ++ " from " ++ show x ++ " with " ++ show np ++ " args " ++ show abstr
reportSLn "tc.mod.apply" 80 $
"args = " ++ show ts' ++ "\n" ++
"old type = " ++ prettyShow (defType d) ++ "\n" ++
"new type = " ++ prettyShow t
addConstant y =<< nd y
makeProjection y
unless isCon $ whenJust inst $ \ c -> addNamedInstance y c
when (not isCon && size ptel == 0) $ do
addDisplayForms y
where
ts' = take np ts
t = defType d `apply` ts'
pol = defPolarity d `apply` ts'
occ = defArgOccurrences d `apply` ts'
inst = defInstance d
abstr = defAbstract d
nd :: QName -> TCM Definition
nd y = Defn (defArgInfo d) y t pol occ [] (1) noCompiledRep inst <$> def
oldDef = theDef d
isCon = case oldDef of { Constructor{} -> True ; _ -> False }
mutual = case oldDef of { Function{funMutual = m} -> m ; _ -> [] }
extlam = case oldDef of { Function{funExtLam = e} -> e ; _ -> Nothing }
with = case oldDef of { Function{funWith = w} -> copyName <$> w ; _ -> Nothing }
isVar0 t = case ignoreSharing $ unArg t of Var 0 [] -> True; _ -> False
proj = case oldDef of
Function{funProjection = Just p@Projection{projIndex = n}}
| size ts < n || (size ts == n && isVar0 (last ts))
-> Just $ p { projIndex = n size ts
, projDropPars = projDropPars p `apply` ts
}
_ -> Nothing
def =
case oldDef of
Constructor{ conPars = np, conData = d } -> return $
oldDef { conPars = np size ts'
, conData = copyName d
}
Datatype{ dataPars = np, dataCons = cs } -> return $
oldDef { dataPars = np size ts'
, dataClause = Just cl
, dataCons = map copyName cs
}
Record{ recPars = np, recConType = t, recTel = tel } -> return $
oldDef { recPars = np size ts'
, recClause = Just cl
, recConType = apply t ts
, recTel = apply tel ts
}
_ -> do
cc <- compileClauses Nothing [cl]
let newDef = Function
{ funClauses = [cl]
, funCompiled = Just $ cc
, funDelayed = NotDelayed
, funInv = NotInjective
, funMutual = mutual
, funAbstr = ConcreteDef
, funProjection = proj
, funStatic = False
, funCopy = True
, funTerminates = Just True
, funExtLam = extlam
, funWith = with
, funCopatternLHS = isCopatternLHS [cl]
}
reportSLn "tc.mod.apply" 80 $ "new def for " ++ show x ++ "\n " ++ show newDef
return newDef
head = case oldDef of
Function{funProjection = Just Projection{ projDropPars = f}}
-> f
_ -> Def x []
cl = Clause { clauseRange = getRange $ defClauses d
, clauseTel = EmptyTel
, clausePerm = idP 0
, namedClausePats = []
, clauseBody = Body $ head `apply` ts'
, clauseType = Just $ defaultArg t
}
copySec :: Args -> (ModuleName, ModuleName) -> TCM ()
copySec ts (x, y) = do
totalArgs <- argsToUse x
tel <- lookupSection x
ptel <- lookupSection $ mnameFromList $ init $ mnameToList x
let parentParams = size ptel
childParams = size tel parentParams
argsToChild = max 0 $ totalArgs parentParams
let fv = childParams argsToChild
reportSLn "tc.mod.apply" 80 $ "Copying section " ++ show x ++ " to " ++ show y
reportSLn "tc.mod.apply" 80 $ " free variables: " ++ show fv
reportSLn "tc.mod.apply" 80 $ " ts = " ++ show ts
reportSLn "tc.mod.apply" 80 $ " tel = " ++ show (map (second unEl . unDom) $ telToList tel)
reportSLn "tc.mod.apply" 80 $ " ptel = " ++ show (map (second unEl . unDom) $ telToList ptel)
reportSLn "tc.mod.apply" 80 $ " np = " ++ show totalArgs
addCtxTel (apply tel $ take totalArgs ts) $ addSection y fv
addDisplayForm :: QName -> DisplayForm -> TCM ()
addDisplayForm x df = do
d <- makeOpen df
let add = updateDefinition x $ \ def -> def{ defDisplay = d : defDisplay def }
modifyImportedSignature add
modifySignature add
canonicalName :: QName -> TCM QName
canonicalName x = do
def <- theDef <$> getConstInfo x
case def of
Constructor{conSrcCon = c} -> return $ conName c
Record{recClause = Just (Clause{ clauseBody = body })} -> canonicalName $ extract body
Datatype{dataClause = Just (Clause{ clauseBody = body })} -> canonicalName $ extract body
_ -> return x
where
extract NoBody = __IMPOSSIBLE__
extract (Body (Def x _)) = x
extract (Body (Shared p)) = extract (Body $ derefPtr p)
extract (Body _) = __IMPOSSIBLE__
extract (Bind b) = extract (unAbs b)
sameDef :: QName -> QName -> TCM (Maybe QName)
sameDef d1 d2 = do
c1 <- canonicalName d1
c2 <- canonicalName d2
if (c1 == c2) then return $ Just c1 else return Nothing
whatInduction :: QName -> TCM Induction
whatInduction c = do
def <- theDef <$> getConstInfo c
case def of
Datatype{ dataInduction = i } -> return i
Record{ recRecursive = False} -> return Inductive
Record{ recInduction = i } -> return $ fromMaybe Inductive i
Constructor{ conInd = i } -> return i
_ -> __IMPOSSIBLE__
singleConstructorType :: QName -> TCM Bool
singleConstructorType q = do
d <- theDef <$> getConstInfo q
case d of
Record {} -> return True
Constructor { conData = d } -> do
di <- theDef <$> getConstInfo d
return $ case di of
Record {} -> True
Datatype { dataCons = cs } -> length cs == 1
_ -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
class (Functor m, Applicative m, Monad m) => HasConstInfo m where
getConstInfo :: QName -> m Definition
getRewriteRulesFor :: QName -> m RewriteRules
defaultGetRewriteRulesFor :: (Monad m) => m TCState -> QName -> m RewriteRules
defaultGetRewriteRulesFor getTCState q = do
st <- getTCState
let sig = st^.stSignature
imp = st^.stImports
look s = HMap.lookup q $ sigRewriteRules s
return $ mconcat $ catMaybes [look sig, look imp]
instance HasConstInfo (TCMT IO) where
getRewriteRulesFor = defaultGetRewriteRulesFor get
getConstInfo q = join $ pureTCM $ \st env ->
let defs = sigDefinitions $ st^.stSignature
idefs = sigDefinitions $ st^.stImports
in case catMaybes [HMap.lookup q defs, HMap.lookup q idefs] of
[] -> fail $ "Unbound name: " ++ show q ++ " " ++ showQNameId q
[d] -> mkAbs env d
ds -> fail $ "Ambiguous name: " ++ show q
where
mkAbs env d
| treatAbstractly' q' env =
case makeAbstract d of
Just d -> return d
Nothing -> notInScope $ qnameToConcrete q
| otherwise = return d
where
q' = case theDef d of
Constructor{} -> dropLastModule q
_ -> q
dropLastModule q@QName{ qnameModule = m } =
q{ qnameModule = mnameFromList $ ifNull (mnameToList m) __IMPOSSIBLE__ init }
instance (HasConstInfo m, Error err) => HasConstInfo (ExceptionT err m) where
getConstInfo = lift . getConstInfo
getRewriteRulesFor = lift . getRewriteRulesFor
getConInfo :: MonadTCM tcm => ConHead -> tcm Definition
getConInfo = liftTCM . getConstInfo . conName
getPolarity :: QName -> TCM [Polarity]
getPolarity q = defPolarity <$> getConstInfo q
getPolarity' :: Comparison -> QName -> TCM [Polarity]
getPolarity' CmpEq q = map (composePol Invariant) <$> getPolarity q
getPolarity' CmpLeq q = getPolarity q
setPolarity :: QName -> [Polarity] -> TCM ()
setPolarity q pol = modifySignature $ updateDefinition q $ updateDefPolarity $ const pol
getArgOccurrence :: QName -> Nat -> TCM Occurrence
getArgOccurrence d i = do
def <- getConstInfo d
return $ case theDef def of
Constructor{} -> StrictPos
_ -> fromMaybe Mixed $ defArgOccurrences def !!! i
setArgOccurrences :: QName -> [Occurrence] -> TCM ()
setArgOccurrences d os = modifyArgOccurrences d $ const os
modifyArgOccurrences :: QName -> ([Occurrence] -> [Occurrence]) -> TCM ()
modifyArgOccurrences d f =
modifySignature $ updateDefinition d $ updateDefArgOccurrences f
getMutual :: QName -> TCM [QName]
getMutual d = do
def <- theDef <$> getConstInfo d
return $ case def of
Function { funMutual = m } -> m
Datatype { dataMutual = m } -> m
Record { recMutual = m } -> m
_ -> []
setMutual :: QName -> [QName] -> TCM ()
setMutual d m = modifySignature $ updateDefinition d $ updateTheDef $ \ def ->
case def of
Function{} -> def { funMutual = m }
Datatype{} -> def {dataMutual = m }
Record{} -> def { recMutual = m }
_ -> __IMPOSSIBLE__
mutuallyRecursive :: QName -> QName -> TCM Bool
mutuallyRecursive d d' = (d `elem`) <$> getMutual d'
getSection :: ModuleName -> TCM (Maybe Section)
getSection m = do
sig <- sigSections <$> getSignature
isig <- sigSections <$> getImportedSignature
return $ Map.lookup m sig <|> Map.lookup m isig
getSecFreeVars :: ModuleName -> TCM Nat
getSecFreeVars m = do
top <- currentModule
case top `isSubModuleOf` m || top == m of
True -> maybe 0 secFreeVars <$> getSection m
False -> return 0
getModuleFreeVars :: ModuleName -> TCM Nat
getModuleFreeVars m = sum <$> ((:) <$> getAnonymousVariables m <*> mapM getSecFreeVars ms)
where
ms = map mnameFromList . inits . mnameToList $ m
getDefFreeVars :: QName -> TCM Nat
getDefFreeVars q = getModuleFreeVars (qnameModule q)
freeVarsToApply :: QName -> TCM Args
freeVarsToApply x = genericTake <$> getDefFreeVars x <*> getContextArgs
instantiateDef :: Definition -> TCM Definition
instantiateDef d = do
vs <- freeVarsToApply $ defName d
verboseS "tc.sig.inst" 30 $ do
ctx <- getContext
m <- currentModule
reportSLn "tc.sig.inst" 30 $
"instDef in " ++ show m ++ ": " ++ show (defName d) ++ " " ++
unwords (map show . take (size vs) . reverse . map (fst . unDom) $ ctx)
return $ d `apply` vs
makeAbstract :: Definition -> Maybe Definition
makeAbstract d =
case defAbstract d of
ConcreteDef -> return d
AbstractDef -> do
def <- makeAbs $ theDef d
return d { defArgOccurrences = []
, defPolarity = []
, theDef = def
}
where
makeAbs Datatype {} = Just Axiom
makeAbs Function {} = Just Axiom
makeAbs Constructor{} = Nothing
makeAbs d@Record{} = Just Axiom
makeAbs d = Just d
inAbstractMode :: TCM a -> TCM a
inAbstractMode = local $ \e -> e { envAbstractMode = AbstractMode,
envAllowDestructiveUpdate = False }
inConcreteMode :: TCM a -> TCM a
inConcreteMode = local $ \e -> e { envAbstractMode = ConcreteMode }
ignoreAbstractMode :: MonadReader TCEnv m => m a -> m a
ignoreAbstractMode = local $ \e -> e { envAbstractMode = IgnoreAbstractMode,
envAllowDestructiveUpdate = False }
inConcreteOrAbstractMode :: QName -> TCM a -> TCM a
inConcreteOrAbstractMode q cont = do
a <- ignoreAbstractMode $ defAbstract <$> getConstInfo q
case a of
AbstractDef -> inAbstractMode cont
ConcreteDef -> inConcreteMode cont
treatAbstractly :: MonadReader TCEnv m => QName -> m Bool
treatAbstractly q = asks $ treatAbstractly' q
treatAbstractly' :: QName -> TCEnv -> Bool
treatAbstractly' q env = case envAbstractMode env of
ConcreteMode -> True
IgnoreAbstractMode -> False
AbstractMode -> not $ current == m || current `isSubModuleOf` m
where
current = dropAnon $ envCurrentModule env
m = dropAnon $ qnameModule q
dropAnon (MName ms) = MName $ reverse $ dropWhile isNoName $ reverse ms
typeOfConst :: QName -> TCM Type
typeOfConst q = defType <$> (instantiateDef =<< getConstInfo q)
relOfConst :: QName -> TCM Relevance
relOfConst q = defRelevance <$> getConstInfo q
colOfConst :: QName -> TCM [Color]
colOfConst q = defColors <$> getConstInfo q
sortOfConst :: QName -> TCM Sort
sortOfConst q =
do d <- theDef <$> getConstInfo q
case d of
Datatype{dataSort = s} -> return s
_ -> fail $ "Expected " ++ show q ++ " to be a datatype."
defPars :: Definition -> Int
defPars d = case theDef d of
Axiom{} -> 0
def@Function{} -> projectionArgs def
Datatype {dataPars = n} -> n
Record {recPars = n} -> n
Constructor{conPars = n} -> n
Primitive{} -> 0
droppedPars :: Definition -> Int
droppedPars d = case theDef d of
Axiom{} -> 0
def@Function{} -> projectionArgs def
Datatype {dataPars = _} -> 0
Record {recPars = _} -> 0
Constructor{conPars = n} -> n
Primitive{} -> 0
isProjection :: HasConstInfo m => QName -> m (Maybe Projection)
isProjection qn = isProjection_ . theDef <$> getConstInfo qn
isProjection_ :: Defn -> Maybe Projection
isProjection_ def =
case def of
Function { funProjection = result } -> result
_ -> Nothing
isProperProjection :: Defn -> Bool
isProperProjection d = caseMaybe (isProjection_ d) False $ \ isP ->
if projIndex isP <= 0 then False else isJust $ projProper isP
projectionArgs :: Defn -> Int
projectionArgs = maybe 0 (max 0 . pred . projIndex) . isProjection_
usesCopatterns :: QName -> TCM Bool
usesCopatterns q = do
d <- theDef <$> getConstInfo q
return $ case d of
Function{ funCopatternLHS = b } -> b
_ -> False
applyDef :: QName -> I.Arg Term -> TCM Term
applyDef f a = do
let fallback = return $ Def f [Apply a]
caseMaybeM (isProjection f) fallback $ \ isP -> do
if projIndex isP <= 0 then fallback else do
caseMaybe (projProper isP) fallback $ \ f' -> do
return $ unArg a `applyE` [Proj f']
getDefType :: QName -> Type -> TCM (Maybe Type)
getDefType f t = do
def <- getConstInfo f
let a = defType def
fallback = return $ Just a
caseMaybe (isProjection_ $ theDef def) fallback $
\ (Projection{ projIndex = n }) -> if n <= 0 then fallback else do
let npars | n == 0 = __IMPOSSIBLE__
| otherwise = n 1
case ignoreSharing $ unEl t of
Def d es -> do
flip (ifM $ eligibleForProjectionLike d) (return Nothing) $ do
let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims $ take npars es
return $ Just $ a `apply` pars
_ -> return Nothing