diff options
Diffstat (limited to 'src/full/Agda/TypeChecking/Monad/Base.hs')
| -rw-r--r-- | src/full/Agda/TypeChecking/Monad/Base.hs | 759 |
1 files changed, 586 insertions, 173 deletions
diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs index b225c01..6dba507 100644 --- a/src/full/Agda/TypeChecking/Monad/Base.hs +++ b/src/full/Agda/TypeChecking/Monad/Base.hs @@ -1,16 +1,7 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-} @@ -22,7 +13,7 @@ import qualified Control.Concurrent as C import qualified Control.Exception as E import Control.Monad.State import Control.Monad.Reader -import Control.Monad.Writer +import Control.Monad.Writer hiding ((<>)) import Control.Monad.Trans.Maybe import Control.Applicative hiding (empty) @@ -36,8 +27,9 @@ import Data.Map (Map) import qualified Data.Map as Map -- hiding (singleton, null, empty) import Data.Set (Set) import qualified Data.Set as Set -- hiding (singleton, null, empty) +import Data.Semigroup (Semigroup, Monoid, (<>), mempty, mappend, Any(..)) import Data.Typeable (Typeable) -import Data.Foldable +import Data.Foldable (Foldable) import Data.Traversable import Data.IORef @@ -53,6 +45,8 @@ import qualified Agda.Syntax.Abstract as A import Agda.Syntax.Abstract (AllNames) import Agda.Syntax.Internal as I import Agda.Syntax.Internal.Pattern () +import Agda.Syntax.Internal.Generic (TermLike(..)) +import Agda.Syntax.Parser (PM(..), ParseWarning, runPMIO) import Agda.Syntax.Treeless (Compiled) import Agda.Syntax.Fixity import Agda.Syntax.Position @@ -61,8 +55,8 @@ import qualified Agda.Syntax.Info as Info import Agda.TypeChecking.CompiledClause import Agda.TypeChecking.Positivity.Occurrence +import Agda.TypeChecking.Free.Lazy (Free'(freeVars'), bind', bind) -import Agda.Interaction.Exceptions -- import {-# SOURCE #-} Agda.Interaction.FindFile import Agda.Interaction.Options import Agda.Interaction.Response @@ -70,13 +64,13 @@ import Agda.Interaction.Response import Agda.Interaction.Highlighting.Precise (CompressedFile, HighlightingInfo) -import qualified Agda.Compiler.JS.Syntax as JS import qualified Agda.Compiler.UHC.Pragmas.Base as CR import Agda.Utils.Except ( Error(strMsg) , ExceptT , MonadError(catchError, throwError) + , runExceptT ) import Agda.Utils.Benchmark (MonadBench(..)) @@ -85,12 +79,14 @@ import Agda.Utils.HashMap (HashMap) import qualified Agda.Utils.HashMap as HMap import Agda.Utils.Hash import Agda.Utils.Lens +import Agda.Utils.List import Agda.Utils.ListT import Agda.Utils.Monad import Agda.Utils.Null import Agda.Utils.Permutation -import Agda.Utils.Pretty +import Agda.Utils.Pretty hiding ((<>)) import Agda.Utils.Singleton +import Agda.Utils.Functor #include "undefined.h" import Agda.Utils.Impossible @@ -115,32 +111,35 @@ instance Show TCState where show _ = "TCSt{}" data PreScopeState = PreScopeState - { stPreTokens :: CompressedFile -- from lexer + { stPreTokens :: !CompressedFile -- from lexer -- ^ Highlighting info for tokens (but not those tokens for -- which highlighting exists in 'stSyntaxInfo'). - , stPreImports :: Signature -- XX populated by scopec hecker + , stPreImports :: !Signature -- XX populated by scopec hecker -- ^ Imported declared identifiers. -- Those most not be serialized! - , stPreImportedModules :: Set ModuleName -- imports logic - , stPreModuleToSource :: ModuleToSource -- imports - , stPreVisitedModules :: VisitedModules -- imports - , stPreScope :: ScopeInfo + , stPreImportedModules :: !(Set ModuleName) -- imports logic + , stPreModuleToSource :: !ModuleToSource -- imports + , stPreVisitedModules :: !VisitedModules -- imports + , stPreScope :: !ScopeInfo -- generated by scope checker, current file: which modules you have, public definitions, current file, maps concrete names to abstract names. - , stPrePatternSyns :: A.PatternSynDefns + , stPrePatternSyns :: !A.PatternSynDefns -- ^ Pattern synonyms of the current file. Serialized. - , stPrePatternSynImports :: A.PatternSynDefns + , stPrePatternSynImports :: !A.PatternSynDefns -- ^ Imported pattern synonyms. Must not be serialized! - , stPrePragmaOptions :: PragmaOptions + , stPrePragmaOptions :: !PragmaOptions -- ^ Options applying to the current file. @OPTIONS@ -- pragmas only affect this field. - , stPreImportedBuiltins :: BuiltinThings PrimFun - , stPreHaskellImports :: Set String + , stPreImportedBuiltins :: !(BuiltinThings PrimFun) + , stPreImportedDisplayForms :: !DisplayForms + -- ^ Display forms added by someone else to imported identifiers + , stPreImportedInstanceDefs :: !InstanceTable + , stPreHaskellImports :: !(Set String) -- ^ Imports that should be generated by the compiler / MAlonzo -- (this includes imports from imported modules). - , stPreHaskellImportsUHC :: Set String + , stPreHaskellImportsUHC :: !(Set String) -- ^ Imports that should be generated by the compiler / UHC backend -- (this includes imports from imported modules). - , stPreHaskellCode :: [String] + , stPreHaskellCode :: ![String] -- ^ Inline Haskell code that should be inserted by the GHC backend , stPreFreshInteractionId :: !InteractionId } @@ -148,48 +147,61 @@ data PreScopeState = PreScopeState type DisambiguatedNames = IntMap A.QName data PostScopeState = PostScopeState - { stPostSyntaxInfo :: CompressedFile + { stPostSyntaxInfo :: !CompressedFile -- ^ Highlighting info. , stPostDisambiguatedNames :: !DisambiguatedNames -- ^ Disambiguation carried out by the type checker. -- Maps position of first name character to disambiguated @'A.QName'@ -- for each @'A.AmbiguousQName'@ already passed by the type checker. - , stPostMetaStore :: MetaStore - , stPostInteractionPoints :: InteractionPoints -- scope checker first - , stPostAwakeConstraints :: Constraints - , stPostSleepingConstraints :: Constraints - , stPostDirty :: Bool -- local + , stPostMetaStore :: !MetaStore + , stPostInteractionPoints :: !InteractionPoints -- scope checker first + , stPostSolvedInteractionPoints :: !InteractionPoints + -- ^ Interaction points that have been filled by a give or solve action. + , stPostAwakeConstraints :: !Constraints + , stPostSleepingConstraints :: !Constraints + , stPostDirty :: !Bool -- local -- ^ Dirty when a constraint is added, used to prevent pointer update. -- Currently unused. - , stPostOccursCheckDefs :: Set QName -- local + , stPostOccursCheckDefs :: !(Set QName) -- local -- ^ Definitions to be considered during occurs check. -- Initialized to the current mutual block before the check. -- During occurs check, we remove definitions from this set -- as soon we have checked them. - , stPostSignature :: Signature + , stPostSignature :: !Signature -- ^ Declared identifiers of the current file. -- These will be serialized after successful type checking. + , stPostModuleParameters :: !ModuleParamDict + -- ^ TODO: can these be moved into the @TCEnv@? , stPostImportsDisplayForms :: !DisplayForms -- ^ Display forms we add for imported identifiers - , stPostImportedDisplayForms :: !DisplayForms - -- ^ Display forms added by someone else to imported identifiers - , stPostCurrentModule :: Maybe ModuleName + , stPostCurrentModule :: !(Maybe ModuleName) -- ^ The current module is available after it has been type -- checked. - , stPostInstanceDefs :: TempInstanceTable - , stPostStatistics :: Statistics + , stPostInstanceDefs :: !TempInstanceTable + , stPostStatistics :: !Statistics -- ^ Counters to collect various statistics about meta variables etc. -- Only for current file. - , stPostMutualBlocks :: Map MutualId (Set QName) - , stPostLocalBuiltins :: BuiltinThings PrimFun - , stPostFreshMetaId :: MetaId - , stPostFreshMutualId :: MutualId - , stPostFreshCtxId :: CtxId - , stPostFreshProblemId :: ProblemId - , stPostFreshInt :: Int - , stPostFreshNameId :: NameId + , stPostTCWarnings :: ![TCWarning] + , stPostMutualBlocks :: !(Map MutualId MutualBlock) + , stPostLocalBuiltins :: !(BuiltinThings PrimFun) + , stPostFreshMetaId :: !MetaId + , stPostFreshMutualId :: !MutualId + , stPostFreshCtxId :: !CtxId + , stPostFreshProblemId :: !ProblemId + , stPostFreshInt :: !Int + , stPostFreshNameId :: !NameId } +-- | A mutual block of names in the signature. +data MutualBlock = MutualBlock + { mutualInfo :: Info.MutualInfo + -- ^ The original info of the mutual block. + , mutualNames :: Set QName + } deriving (Show, Eq) + +instance Null MutualBlock where + empty = MutualBlock empty empty + -- | A part of the state which is not reverted when an error is thrown -- or the state is reset. data PersistentTCState = PersistentTCSt @@ -266,6 +278,8 @@ initPreScopeState = PreScopeState , stPrePatternSynImports = Map.empty , stPrePragmaOptions = defaultInteractionOptions , stPreImportedBuiltins = Map.empty + , stPreImportedDisplayForms = HMap.empty + , stPreImportedInstanceDefs = Map.empty , stPreHaskellImports = Set.empty , stPreHaskellImportsUHC = Set.empty , stPreHaskellCode = [] @@ -278,16 +292,18 @@ initPostScopeState = PostScopeState , stPostDisambiguatedNames = IntMap.empty , stPostMetaStore = Map.empty , stPostInteractionPoints = Map.empty + , stPostSolvedInteractionPoints = Map.empty , stPostAwakeConstraints = [] , stPostSleepingConstraints = [] , stPostDirty = False , stPostOccursCheckDefs = Set.empty , stPostSignature = emptySignature + , stPostModuleParameters = Map.empty , stPostImportsDisplayForms = HMap.empty - , stPostImportedDisplayForms = HMap.empty , stPostCurrentModule = Nothing - , stPostInstanceDefs = (Map.empty , []) + , stPostInstanceDefs = (Map.empty , Set.empty) , stPostStatistics = Map.empty + , stPostTCWarnings = [] , stPostMutualBlocks = Map.empty , stPostLocalBuiltins = Map.empty , stPostFreshMetaId = 0 @@ -403,6 +419,12 @@ stInteractionPoints f s = f (stPostInteractionPoints (stPostScopeState s)) <&> \x -> s {stPostScopeState = (stPostScopeState s) {stPostInteractionPoints = x}} +stSolvedInteractionPoints :: Lens' InteractionPoints TCState +stSolvedInteractionPoints f s = + f (stPostSolvedInteractionPoints (stPostScopeState s)) <&> + \ x -> s {stPostScopeState = (stPostScopeState s) + {stPostSolvedInteractionPoints = x}} + stAwakeConstraints :: Lens' Constraints TCState stAwakeConstraints f s = f (stPostAwakeConstraints (stPostScopeState s)) <&> @@ -428,6 +450,11 @@ stSignature f s = f (stPostSignature (stPostScopeState s)) <&> \x -> s {stPostScopeState = (stPostScopeState s) {stPostSignature = x}} +stModuleParameters :: Lens' (ModuleParamDict) TCState +stModuleParameters f s = + f (stPostModuleParameters (stPostScopeState s)) <&> + \x -> s {stPostScopeState = (stPostScopeState s) {stPostModuleParameters = x}} + stImportsDisplayForms :: Lens' DisplayForms TCState stImportsDisplayForms f s = f (stPostImportsDisplayForms (stPostScopeState s)) <&> @@ -435,14 +462,19 @@ stImportsDisplayForms f s = stImportedDisplayForms :: Lens' DisplayForms TCState stImportedDisplayForms f s = - f (stPostImportedDisplayForms (stPostScopeState s)) <&> - \x -> s {stPostScopeState = (stPostScopeState s) {stPostImportedDisplayForms = x}} + f (stPreImportedDisplayForms (stPreScopeState s)) <&> + \x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedDisplayForms = x}} stCurrentModule :: Lens' (Maybe ModuleName) TCState stCurrentModule f s = f (stPostCurrentModule (stPostScopeState s)) <&> \x -> s {stPostScopeState = (stPostScopeState s) {stPostCurrentModule = x}} +stImportedInstanceDefs :: Lens' InstanceTable TCState +stImportedInstanceDefs f s = + f (stPreImportedInstanceDefs (stPreScopeState s)) <&> + \x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedInstanceDefs = x}} + stInstanceDefs :: Lens' TempInstanceTable TCState stInstanceDefs f s = f (stPostInstanceDefs (stPostScopeState s)) <&> @@ -453,7 +485,12 @@ stStatistics f s = f (stPostStatistics (stPostScopeState s)) <&> \x -> s {stPostScopeState = (stPostScopeState s) {stPostStatistics = x}} -stMutualBlocks :: Lens' (Map MutualId (Set QName)) TCState +stTCWarnings :: Lens' [TCWarning] TCState +stTCWarnings f s = + f (stPostTCWarnings (stPostScopeState s)) <&> + \x -> s {stPostScopeState = (stPostScopeState s) {stPostTCWarnings = x}} + +stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState stMutualBlocks f s = f (stPostMutualBlocks (stPostScopeState s)) <&> \x -> s {stPostScopeState = (stPostScopeState s) {stPostMutualBlocks = x}} @@ -595,6 +632,11 @@ type ModuleToSource = Map TopLevelModuleName AbsolutePath type SourceToModule = Map AbsolutePath TopLevelModuleName -- | Creates a 'SourceToModule' map based on 'stModuleToSource'. +-- +-- O(n log n). +-- +-- For a single reverse lookup in 'stModuleToSource', +-- rather use 'lookupModuleFromSourse'. sourceToModule :: TCM SourceToModule sourceToModule = @@ -603,6 +645,14 @@ sourceToModule = . Map.toList <$> use stModuleToSource +-- | Lookup an 'AbsolutePath' in 'sourceToModule'. +-- +-- O(n). + +lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName) +lookupModuleFromSource f = + fmap fst . List.find ((f ==) . snd) . Map.toList <$> use stModuleToSource + --------------------------------------------------------------------------- -- ** Interface --------------------------------------------------------------------------- @@ -686,12 +736,18 @@ iFullHash i = combineHashes $ iSourceHash i : List.map snd (iImportedModules i) -- ** Closure --------------------------------------------------------------------------- -data Closure a = Closure { clSignature :: Signature - , clEnv :: TCEnv - , clScope :: ScopeInfo - , clValue :: a - } - deriving (Typeable) +data Closure a = Closure + { clSignature :: Signature + , clEnv :: TCEnv + , clScope :: ScopeInfo + , clModuleParameters :: ModuleParamDict + -- ^ Since module parameters are currently stored in 'TCState' + -- not in 'TCEnv', we save them here. + -- The map contains for each 'ModuleName' @M@ with module telescope @Γ_M@ + -- a substitution @Γ ⊢ ρ_M : Γ_M@ from the current context @Γ = envContext (clEnv)@. + , clValue :: a + } + deriving (Typeable, Functor, Foldable) instance Show a => Show (Closure a) where show cl = "Closure " ++ show (clValue cl) @@ -704,7 +760,8 @@ buildClosure x = do env <- ask sig <- use stSignature scope <- use stScope - return $ Closure sig env scope x + pars <- use stModuleParameters + return $ Closure sig env scope pars x --------------------------------------------------------------------------- -- ** Constraints @@ -758,6 +815,38 @@ instance HasRange Constraint where getRange (FindInScope x cands) = getRange x -} +instance Free' Constraint c where + freeVars' c = + case c of + ValueCmp _ t u v -> freeVars' (t, (u, v)) + ElimCmp _ t u es es' -> freeVars' ((t, u), (es, es')) + TypeCmp _ t t' -> freeVars' (t, t') + TelCmp _ _ _ tel tel' -> freeVars' (tel, tel') + SortCmp _ s s' -> freeVars' (s, s') + LevelCmp _ l l' -> freeVars' (l, l') + UnBlock _ -> mempty + Guarded c _ -> freeVars' c + IsEmpty _ t -> freeVars' t + CheckSizeLtSat u -> freeVars' u + FindInScope _ _ cs -> freeVars' cs + +instance TermLike Constraint where + foldTerm f = \case + ValueCmp _ t u v -> foldTerm f (t, u, v) + ElimCmp _ t u es es' -> foldTerm f (t, u, es, es') + TypeCmp _ t t' -> foldTerm f (t, t') + LevelCmp _ l l' -> foldTerm f (l, l') + IsEmpty _ t -> foldTerm f t + CheckSizeLtSat u -> foldTerm f u + TelCmp _ _ _ tel1 tel2 -> __IMPOSSIBLE__ -- foldTerm f (tel1, tel2) -- Not yet implemented + SortCmp _ s1 s2 -> __IMPOSSIBLE__ -- foldTerm f (s1, s2) -- Not yet implemented + UnBlock _ -> __IMPOSSIBLE__ -- mempty -- Not yet implemented + Guarded c _ -> __IMPOSSIBLE__ -- foldTerm c -- Not yet implemented + FindInScope _ _ cs -> __IMPOSSIBLE__ -- Not yet implemented + traverseTerm f c = __IMPOSSIBLE__ -- Not yet implemented + traverseTermM f c = __IMPOSSIBLE__ -- Not yet implemented + + data Comparison = CmpEq | CmpLeq deriving (Eq, Typeable) @@ -811,6 +900,22 @@ dirToCmp cont DirGeq = flip $ cont CmpLeq data Open a = OpenThing { openThingCtxIds :: [CtxId], openThing :: a } deriving (Typeable, Show, Functor) +instance Decoration Open where + traverseF f (OpenThing cxt x) = OpenThing cxt <$> f x + +data Local a = Local ModuleName a -- ^ Local to a given module, the value + -- should have module parameters as free variables. + | Global a -- ^ Global value, should be closed. + deriving (Typeable, Show, Functor, Foldable, Traversable) + +isGlobal :: Local a -> Bool +isGlobal Global{} = True +isGlobal Local{} = False + +instance Decoration Local where + traverseF f (Local m x) = Local m <$> f x + traverseF f (Global x) = Global <$> f x + --------------------------------------------------------------------------- -- * Judgements -- @@ -871,7 +976,6 @@ data Frozen data MetaInstantiation = InstV [Arg String] Term -- ^ solved by term (abstracted over some free variables) - | InstS Term -- ^ solved by @Lam .. Sort s@ | Open -- ^ unsolved | OpenIFS -- ^ open, to be instantiated as "implicit from scope" | BlockedConst Term -- ^ solution blocked by unsolved constraints @@ -894,7 +998,6 @@ data TypeCheckingProblem instance Show MetaInstantiation where show (InstV tel t) = "InstV " ++ show tel ++ " (" ++ show t ++ ")" - show (InstS s) = "InstS (" ++ show s ++ ")" show Open = "Open" show OpenIFS = "OpenIFS" show (BlockedConst t) = "BlockedConst (" ++ show t ++ ")" @@ -984,6 +1087,9 @@ getMetaRelevance = envRelevance . getMetaEnv data InteractionPoint = InteractionPoint { ipRange :: Range -- ^ The position of the interaction point. , ipMeta :: Maybe MetaId -- ^ The meta variable, if any, holding the type etc. + , ipClause:: IPClause + -- ^ The clause of the interaction point (if any). + -- Used for case splitting. } instance Eq InteractionPoint where (==) = (==) `on` ipMeta @@ -991,6 +1097,19 @@ instance Eq InteractionPoint where (==) = (==) `on` ipMeta -- | Data structure managing the interaction points. type InteractionPoints = Map InteractionId InteractionPoint +-- | Which clause is an interaction point located in? +data IPClause = IPClause + { ipcQName :: QName -- ^ The name of the function. + , ipcClauseNo :: Int -- ^ The number of the clause of this function. + , ipcClause :: A.RHS -- ^ The original AST clause rhs. + } + | IPNoClause -- ^ The interaction point is not in the rhs of a clause. + +instance Eq IPClause where + IPNoClause == IPNoClause = True + IPClause x i _ == IPClause x' i' _ = x == x' && i == i' + _ == _ = False + --------------------------------------------------------------------------- -- ** Signature --------------------------------------------------------------------------- @@ -1020,7 +1139,7 @@ sigRewriteRules f s = type Sections = Map ModuleName Section type Definitions = HashMap QName Definition type RewriteRuleMap = HashMap QName RewriteRules -type DisplayForms = HashMap QName [Open DisplayForm] +type DisplayForms = HashMap QName [LocalDisplayForm] data Section = Section { _secTelescope :: Telescope } deriving (Typeable, Show) @@ -1049,25 +1168,29 @@ emptySignature = Sig Map.empty HMap.empty HMap.empty data DisplayForm = Display { dfFreeVars :: Nat -- ^ Number @n@ of free variables in 'dfRHS'. - , dfPats :: [Term] + , dfPats :: Elims -- ^ Left hand side patterns, where @var 0@ stands for a pattern -- variable. There should be @n@ occurrences of @var0@ in -- 'dfPats'. + -- The 'ArgInfo' is ignored in these patterns. , dfRHS :: DisplayTerm -- ^ Right hand side, with @n@ free variables. } deriving (Typeable, Show) +type LocalDisplayForm = Local DisplayForm + -- | A structured presentation of a 'Term' for reification into -- 'Abstract.Syntax'. data DisplayTerm - = DWithApp DisplayTerm [DisplayTerm] Args - -- ^ @(f vs | ws) us@. + = DWithApp DisplayTerm [DisplayTerm] Elims + -- ^ @(f vs | ws) es@. -- The first 'DisplayTerm' is the parent function @f@ with its args @vs@. -- The list of 'DisplayTerm's are the with expressions @ws@. - -- The 'Args' are additional arguments @us@ - -- (possible in case the with-application is of function type). - | DCon ConHead [Arg DisplayTerm] + -- The 'Elims' are additional arguments @es@ + -- (possible in case the with-application is of function type) + -- or projections (if it is of record type). + | DCon ConHead ConInfo [Arg DisplayTerm] -- ^ @c vs@. | DDef QName [Elim' DisplayTerm] -- ^ @d vs@. @@ -1077,8 +1200,18 @@ data DisplayTerm -- ^ @v@. deriving (Typeable, Show) +instance Free' DisplayForm c where + freeVars' (Display n ps t) = bind (freeVars' ps) `mappend` bind' n (freeVars' t) + +instance Free' DisplayTerm c where + freeVars' (DWithApp t ws es) = freeVars' (t, (ws, es)) + freeVars' (DCon _ _ vs) = freeVars' vs + freeVars' (DDef _ es) = freeVars' es + freeVars' (DDot v) = freeVars' v + freeVars' (DTerm v) = freeVars' v + -- | By default, we have no display form. -defaultDisplayForm :: QName -> [Open DisplayForm] +defaultDisplayForm :: QName -> [LocalDisplayForm] defaultDisplayForm c = [] defRelevance :: Definition -> Relevance @@ -1086,15 +1219,16 @@ defRelevance = argInfoRelevance . defArgInfo -- | Non-linear (non-constructor) first-order pattern. data NLPat - = PVar (Maybe CtxId) !Int - -- ^ Matches anything (modulo non-linearity). + = PVar (Maybe CtxId) !Int [Arg Int] + -- ^ Matches anything (modulo non-linearity) that only contains bound + -- variables that occur in the given arguments. | PWild -- ^ Matches anything (e.g. irrelevant terms). | PDef QName PElims -- ^ Matches @f es@ | PLam ArgInfo (Abs NLPat) -- ^ Matches @λ x → t@ - | PPi (Dom (Type' NLPat)) (Abs (Type' NLPat)) + | PPi (Dom NLPType) (Abs NLPType) -- ^ Matches @(x : A) → B@ | PBoundVar {-# UNPACK #-} !Int PElims -- ^ Matches @x es@ where x is a lambda-bound variable @@ -1103,14 +1237,20 @@ data NLPat deriving (Typeable, Show) type PElims = [Elim' NLPat] +data NLPType = NLPType + { nlpTypeLevel :: NLPat -- always PWild or PVar (with all bound variables in scope) + , nlpTypeUnEl :: NLPat + } deriving (Typeable, Show) + type RewriteRules = [RewriteRule] -- | Rewrite rules can be added independently from function clauses. data RewriteRule = RewriteRule - { rewName :: QName -- ^ Name of rewrite rule @q : Γ → lhs ≡ rhs@ + { rewName :: QName -- ^ Name of rewrite rule @q : Γ → f ps ≡ rhs@ -- where @≡@ is the rewrite relation. , rewContext :: Telescope -- ^ @Γ@. - , rewLHS :: NLPat -- ^ @Γ ⊢ lhs : t@. + , rewHead :: QName -- ^ @f@. + , rewPats :: PElims -- ^ @Γ ⊢ ps : t@. , rewRHS :: Term -- ^ @Γ ⊢ rhs : t@. , rewType :: Type -- ^ @Γ ⊢ t@. } @@ -1166,7 +1306,7 @@ data Definition = Defn -- 23, 3 -- 27, 1 - , defDisplay :: [Open DisplayForm] + , defDisplay :: [LocalDisplayForm] , defMutual :: MutualId , defCompiledRep :: CompiledRepresentation , defInstance :: Maybe QName @@ -1174,10 +1314,15 @@ data Definition = Defn , defCopy :: Bool -- ^ Has this function been created by a module -- instantiation? + , defMatchable :: Bool + -- ^ Is the def matched against in a rewrite rule? , theDef :: Defn } deriving (Typeable, Show) +theDefLens :: Lens' Defn Definition +theDefLens f d = f (theDef d) <&> \ df -> d { theDef = df } + -- | Create a definition with sensible defaults. defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition defaultDefn info x t def = Defn @@ -1191,13 +1336,14 @@ defaultDefn info x t def = Defn , defCompiledRep = noCompiledRep , defInstance = Nothing , defCopy = False + , defMatchable = False , theDef = def } type HaskellCode = String type HaskellType = String type EpicCode = String -type JSCode = JS.Exp +type JSCode = String data HaskellRepresentation = HsDefn HaskellType HaskellCode @@ -1240,19 +1386,21 @@ data ExtLamInfo = ExtLamInfo -- | Additional information for projection 'Function's. data Projection = Projection - { projProper :: Maybe QName - -- ^ @Nothing@ if only projection-like, @Just q@ if record projection, - -- where @q@ is the original projection name - -- (current name could be from module app). - , projFromType :: QName - -- ^ Type projected from. Record type if @projProper = Just{}@. + { projProper :: Bool + -- ^ @False@ if only projection-like, @True@ if record projection. + , projOrig :: QName + -- ^ The original projection name + -- (current name could be from module application). + , projFromType :: Arg QName + -- ^ Type projected from. Record type if @projProper = Just{}@. Also + -- stores @ArgInfo@ of the principal argument. , projIndex :: Int -- ^ Index of the record argument. -- Start counting with 1, because 0 means that -- it is already applied to the record value. -- This can happen in module instantiation, but -- then either the record value is @var 0@, or @funProjection == Nothing@. - , projDropPars :: Term + , projLams :: ProjLams -- ^ Term @t@ to be be applied to record parameters and record value. -- The parameters will be dropped. -- In case of a proper projection, a postfix projection application @@ -1260,22 +1408,56 @@ data Projection = Projection -- (Invariant: the number of abstractions equals 'projIndex'.) -- In case of a projection-like function, just the function symbol -- is returned as 'Def': @t = \ pars -> f@. - , projArgInfo :: ArgInfo - -- ^ The info of the principal (record) argument. } deriving (Typeable, Show) -data EtaEquality = Specified !Bool | Inferred !Bool deriving (Typeable,Show) +-- | Abstractions to build projection function (dropping parameters). +newtype ProjLams = ProjLams { getProjLams :: [Arg ArgName] } + deriving (Typeable, Show, Null) + +-- | Building the projection function (which drops the parameters). +projDropPars :: Projection -> ProjOrigin -> Term +-- Proper projections: +projDropPars (Projection True d _ _ lams) o = + case initLast $ getProjLams lams of + Nothing -> Def d [] + Just (pars, Arg i y) -> + let core = Lam i $ Abs y $ Var 0 [Proj o d] in + List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) core pars +-- Projection-like functions: +projDropPars (Projection False _ _ _ lams) o | null lams = __IMPOSSIBLE__ +projDropPars (Projection False d _ _ lams) o = + List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) (Def d []) $ init $ getProjLams lams + +-- | The info of the principal (record) argument. +projArgInfo :: Projection -> ArgInfo +projArgInfo (Projection _ _ _ _ lams) = + maybe __IMPOSSIBLE__ getArgInfo $ lastMaybe $ getProjLams lams + +-- | Should a record type admit eta-equality? +data EtaEquality + = Specified !Bool -- ^ User specifed 'eta-equality' or 'no-eta-equality' + | Inferred !Bool -- ^ Positivity checker inferred whether eta is safe/ + deriving (Typeable, Show, Eq) etaEqualityToBool :: EtaEquality -> Bool etaEqualityToBool (Specified b) = b etaEqualityToBool (Inferred b) = b +-- | Make sure we do not overwrite a user specification. setEtaEquality :: EtaEquality -> Bool -> EtaEquality setEtaEquality e@Specified{} _ = e setEtaEquality _ b = Inferred b +data FunctionFlag + = FunStatic -- ^ Should calls to this function be normalised at compile-time? + | FunInline -- ^ Should calls to this function be inlined by the compiler? + | FunMacro -- ^ Is this function a macro? + deriving (Typeable, Eq, Ord, Enum, Show) + data Defn = Axiom -- ^ Postulate. + | AbstractDefn + -- ^ Returned by 'getConstInfo' if definition is abstract. | Function { funClauses :: [Clause] , funCompiled :: Maybe CompiledClauses @@ -1298,12 +1480,7 @@ data Defn = Axiom -- it is already applied to the record. (Can happen in module -- instantiation.) This information is used in the termination -- checker. - , funStatic :: Bool - -- ^ Should calls to this function be normalised at compile-time? - , funInline :: Bool - -- ^ Should calls to this function be inlined by the compiler? - , funSmashable :: Bool - -- ^ Are we allowed to smash this function? + , funFlags :: Set FunctionFlag , funTerminates :: Maybe Bool -- ^ Has this function been termination checked? Did it pass? , funExtLam :: Maybe ExtLamInfo @@ -1332,7 +1509,6 @@ data Defn = Axiom , recClause :: Maybe Clause , recConHead :: ConHead -- ^ Constructor name and fields. , recNamedCon :: Bool - , recConType :: Type -- ^ The record constructor's type. (Includes record parameters.) , recFields :: [Arg QName] , recTel :: Telescope -- ^ The record field telescope. (Includes record parameters.) -- Note: @TelV recTel _ == telView' recConType@. @@ -1352,6 +1528,7 @@ data Defn = Axiom , conData :: QName -- ^ Name of datatype or record type. , conAbstr :: IsAbstract , conInd :: Induction -- ^ Inductive or coinductive? + , conErased :: [Bool] -- ^ Which arguments are erased at runtime (computed during compilation to treeless) } | Primitive { primAbstr :: IsAbstract @@ -1379,15 +1556,27 @@ emptyFunction = Function , funAbstr = ConcreteDef , funDelayed = NotDelayed , funProjection = Nothing - , funStatic = False - , funInline = False - , funSmashable = True + , funFlags = Set.empty , funTerminates = Nothing , funExtLam = Nothing , funWith = Nothing , funCopatternLHS = False } +funFlag :: FunctionFlag -> Lens' Bool Defn +funFlag flag f def@Function{ funFlags = flags } = + f (Set.member flag flags) <&> + \ b -> def{ funFlags = (if b then Set.insert else Set.delete) flag flags } +funFlag _ f def = f False <&> const def + +funStatic, funInline, funMacro :: Lens' Bool Defn +funStatic = funFlag FunStatic +funInline = funFlag FunInline +funMacro = funFlag FunMacro + +isMacro :: Defn -> Bool +isMacro = (^. funMacro) + -- | Checking whether we are dealing with a function yet to be defined. isEmptyFunction :: Defn -> Bool isEmptyFunction def = @@ -1396,7 +1585,7 @@ isEmptyFunction def = _ -> False isCopatternLHS :: [Clause] -> Bool -isCopatternLHS = List.any (List.any (isJust . A.isProjP) . clausePats) +isCopatternLHS = List.any (List.any (isJust . A.isProjP) . namedClausePats) recCon :: Defn -> QName recCon Record{ recConHead } = conName recConHead @@ -1428,10 +1617,13 @@ instance Null Simplification where empty = NoSimplification null = (== NoSimplification) +instance Semigroup Simplification where + YesSimplification <> _ = YesSimplification + NoSimplification <> s = s + instance Monoid Simplification where mempty = NoSimplification - mappend YesSimplification _ = YesSimplification - mappend NoSimplification s = s + mappend = (<>) data Reduced no yes = NoReduction no | YesReduction Simplification yes deriving (Typeable, Functor) @@ -1522,16 +1714,10 @@ defNonterminating :: Definition -> Bool defNonterminating Defn{theDef = Function{funTerminates = Just False}} = True defNonterminating _ = False --- | Beware when using this function on a @def@ obtained with @getConstInfo q@! --- If the identifier @q@ is abstract, 'getConstInfo' will turn its @def@ into --- an 'Axiom' and you always get 'ConcreteDef', paradoxically. --- Use it in 'IgnoreAbstractMode', like this: --- @ --- a <- ignoreAbstractMode $ defAbstract <$> getConstInfo q --- @ defAbstract :: Definition -> IsAbstract defAbstract d = case theDef d of Axiom{} -> ConcreteDef + AbstractDefn{} -> AbstractDef Function{funAbstr = a} -> a Datatype{dataAbstr = a} -> a Record{recAbstr = a} -> a @@ -1582,7 +1768,7 @@ data Call = CheckClause Type A.SpineClause | IsTypeCall A.Expr Sort | IsType_ A.Expr | InferVar Name - | InferDef Range QName + | InferDef QName | CheckArguments Range [NamedArg A.Expr] Type Type | CheckDataDef Range Name [A.LamBinding] [A.Constructor] | CheckRecDef Range Name [A.LamBinding] [A.Constructor] @@ -1641,7 +1827,7 @@ instance HasRange Call where getRange (IsTypeCall e s) = getRange e getRange (IsType_ e) = getRange e getRange (InferVar x) = getRange x - getRange (InferDef _ f) = getRange f + getRange (InferDef f) = getRange f getRange (CheckArguments r _ _ _) = r getRange (CheckDataDef i _ _ _) = getRange i getRange (CheckRecDef i _ _ _) = getRange i @@ -1667,7 +1853,7 @@ instance HasRange Call where -- | The instance table is a @Map@ associating to every name of -- record/data type/postulate its list of instances -type InstanceTable = Map QName [QName] +type InstanceTable = Map QName (Set QName) -- | When typechecking something of the following form: -- @@ -1677,7 +1863,7 @@ type InstanceTable = Map QName [QName] -- -- it's not yet known where to add @x@, so we add it to a list of -- unresolved instances and we'll deal with it later. -type TempInstanceTable = (InstanceTable , [QName]) +type TempInstanceTable = (InstanceTable , Set QName) --------------------------------------------------------------------------- -- ** Builtin things @@ -1744,6 +1930,18 @@ ifTopLevelAndHighlightingLevelIs l m = do -- * Type checking environment --------------------------------------------------------------------------- +data ModuleParameters = ModuleParams + { mpSubstitution :: Substitution + -- ^ @Δ ⊢ σ : Γ@ for a @module M Γ@ where @Δ@ is the current context @envContext@. + } deriving (Typeable, Show) + +defaultModuleParameters :: ModuleParameters +defaultModuleParameters = ModuleParams IdS + +type ModuleParamDict = Map ModuleName ModuleParameters + -- ^ The map contains for each 'ModuleName' @M@ with module telescope @Γ_M@ + -- a substitution @Γ ⊢ ρ_M : Γ_M@ from the current context @Γ = envContext (clEnv)@. + data TCEnv = TCEnv { envContext :: Context , envLetBindings :: LetBindings @@ -1775,24 +1973,20 @@ data TCEnv = -- Other value: @Relevant@, then only relevant decls. are avail. , envDisplayFormsEnabled :: Bool -- ^ Sometimes we want to disable display forms. - , envReifyInteractionPoints :: Bool - -- ^ should we try to recover interaction points when reifying? - -- disabled when generating types for with functions - , envEtaContractImplicit :: Bool - -- ^ it's safe to eta contract implicit lambdas as long as we're - -- not going to reify and retypecheck (like when doing with - -- abstraction) , envRange :: Range , envHighlightingRange :: Range -- ^ Interactive highlighting uses this range rather -- than 'envRange'. + , envClause :: IPClause + -- ^ What is the current clause we are type-checking? + -- Will be recorded in interaction points in this clause. , envCall :: Maybe (Closure Call) -- ^ what we're doing at the moment , envHighlightingLevel :: HighlightingLevel -- ^ Set to 'None' when imported modules are -- type-checked. , envHighlightingMethod :: HighlightingMethod - , envModuleNestingLevel :: Integer + , envModuleNestingLevel :: !Int -- ^ This number indicates how far away from the -- top-level module Agda has come when chasing -- modules. The level of a given module is not @@ -1822,12 +2016,20 @@ data TCEnv = -- No by default. -- Yes for rewriting feature. , envPrintDomainFreePi :: Bool - -- ^ When True types will be omitted from printed pi types if they - -- can be inferred + -- ^ When @True@, types will be omitted from printed pi types if they + -- can be inferred. + , envPrintMetasBare :: Bool + -- ^ When @True@, throw away meta numbers and meta elims. + -- This is used for reifying terms for feeding into the + -- user's source code, e.g., for the interaction tactics @solveAll@. , envInsideDotPattern :: Bool -- ^ Used by the scope checker to make sure that certain forms -- of expressions are not used inside dot patterns: extended -- lambdas and let-expressions. + , envUnquoteFlags :: UnquoteFlags + , envInstanceDepth :: !Int + -- ^ Until we get a termination checker for instance search (#1743) we + -- limit the search depth to ensure termination. } deriving (Typeable) @@ -1855,10 +2057,9 @@ initEnv = TCEnv { envContext = [] -- definition (which sets 'AbstractMode'). , envRelevance = Relevant , envDisplayFormsEnabled = True - , envReifyInteractionPoints = True - , envEtaContractImplicit = True , envRange = noRange , envHighlightingRange = noRange + , envClause = IPNoClause , envCall = Nothing , envHighlightingLevel = None , envHighlightingMethod = Indirect @@ -1870,12 +2071,125 @@ initEnv = TCEnv { envContext = [] , envAllowedReductions = allReductions , envCompareBlocked = False , envPrintDomainFreePi = False + , envPrintMetasBare = False , envInsideDotPattern = False + , envUnquoteFlags = defaultUnquoteFlags + , envInstanceDepth = 0 } disableDestructiveUpdate :: TCM a -> TCM a disableDestructiveUpdate = local $ \e -> e { envAllowDestructiveUpdate = False } +data UnquoteFlags = UnquoteFlags + { _unquoteNormalise :: Bool } + deriving (Typeable) + +defaultUnquoteFlags :: UnquoteFlags +defaultUnquoteFlags = UnquoteFlags + { _unquoteNormalise = False } + +unquoteNormalise :: Lens' Bool UnquoteFlags +unquoteNormalise f e = f (_unquoteNormalise e) <&> \ x -> e { _unquoteNormalise = x } + +eUnquoteNormalise :: Lens' Bool TCEnv +eUnquoteNormalise = eUnquoteFlags . unquoteNormalise + +-- * e-prefixed lenses +------------------------------------------------------------------------ + +eContext :: Lens' Context TCEnv +eContext f e = f (envContext e) <&> \ x -> e { envContext = x } + +eLetBindings :: Lens' LetBindings TCEnv +eLetBindings f e = f (envLetBindings e) <&> \ x -> e { envLetBindings = x } + +eCurrentModule :: Lens' ModuleName TCEnv +eCurrentModule f e = f (envCurrentModule e) <&> \ x -> e { envCurrentModule = x } + +eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv +eCurrentPath f e = f (envCurrentPath e) <&> \ x -> e { envCurrentPath = x } + +eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv +eAnonymousModules f e = f (envAnonymousModules e) <&> \ x -> e { envAnonymousModules = x } + +eImportPath :: Lens' [C.TopLevelModuleName] TCEnv +eImportPath f e = f (envImportPath e) <&> \ x -> e { envImportPath = x } + +eMutualBlock :: Lens' (Maybe MutualId) TCEnv +eMutualBlock f e = f (envMutualBlock e) <&> \ x -> e { envMutualBlock = x } + +eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv +eTerminationCheck f e = f (envTerminationCheck e) <&> \ x -> e { envTerminationCheck = x } + +eSolvingConstraints :: Lens' Bool TCEnv +eSolvingConstraints f e = f (envSolvingConstraints e) <&> \ x -> e { envSolvingConstraints = x } + +eCheckingWhere :: Lens' Bool TCEnv +eCheckingWhere f e = f (envCheckingWhere e) <&> \ x -> e { envCheckingWhere = x } + +eAssignMetas :: Lens' Bool TCEnv +eAssignMetas f e = f (envAssignMetas e) <&> \ x -> e { envAssignMetas = x } + +eActiveProblems :: Lens' [ProblemId] TCEnv +eActiveProblems f e = f (envActiveProblems e) <&> \ x -> e { envActiveProblems = x } + +eAbstractMode :: Lens' AbstractMode TCEnv +eAbstractMode f e = f (envAbstractMode e) <&> \ x -> e { envAbstractMode = x } + +eRelevance :: Lens' Relevance TCEnv +eRelevance f e = f (envRelevance e) <&> \ x -> e { envRelevance = x } + +eDisplayFormsEnabled :: Lens' Bool TCEnv +eDisplayFormsEnabled f e = f (envDisplayFormsEnabled e) <&> \ x -> e { envDisplayFormsEnabled = x } + +eRange :: Lens' Range TCEnv +eRange f e = f (envRange e) <&> \ x -> e { envRange = x } + +eHighlightingRange :: Lens' Range TCEnv +eHighlightingRange f e = f (envHighlightingRange e) <&> \ x -> e { envHighlightingRange = x } + +eCall :: Lens' (Maybe (Closure Call)) TCEnv +eCall f e = f (envCall e) <&> \ x -> e { envCall = x } + +eHighlightingLevel :: Lens' HighlightingLevel TCEnv +eHighlightingLevel f e = f (envHighlightingLevel e) <&> \ x -> e { envHighlightingLevel = x } + +eHighlightingMethod :: Lens' HighlightingMethod TCEnv +eHighlightingMethod f e = f (envHighlightingMethod e) <&> \ x -> e { envHighlightingMethod = x } + +eModuleNestingLevel :: Lens' Int TCEnv +eModuleNestingLevel f e = f (envModuleNestingLevel e) <&> \ x -> e { envModuleNestingLevel = x } + +eAllowDestructiveUpdate :: Lens' Bool TCEnv +eAllowDestructiveUpdate f e = f (envAllowDestructiveUpdate e) <&> \ x -> e { envAllowDestructiveUpdate = x } + +eExpandLast :: Lens' ExpandHidden TCEnv +eExpandLast f e = f (envExpandLast e) <&> \ x -> e { envExpandLast = x } + +eAppDef :: Lens' (Maybe QName) TCEnv +eAppDef f e = f (envAppDef e) <&> \ x -> e { envAppDef = x } + +eSimplification :: Lens' Simplification TCEnv +eSimplification f e = f (envSimplification e) <&> \ x -> e { envSimplification = x } + +eAllowedReductions :: Lens' AllowedReductions TCEnv +eAllowedReductions f e = f (envAllowedReductions e) <&> \ x -> e { envAllowedReductions = x } + +eCompareBlocked :: Lens' Bool TCEnv +eCompareBlocked f e = f (envCompareBlocked e) <&> \ x -> e { envCompareBlocked = x } + +ePrintDomainFreePi :: Lens' Bool TCEnv +ePrintDomainFreePi f e = f (envPrintDomainFreePi e) <&> \ x -> e { envPrintDomainFreePi = x } + +eInsideDotPattern :: Lens' Bool TCEnv +eInsideDotPattern f e = f (envInsideDotPattern e) <&> \ x -> e { envInsideDotPattern = x } + +eUnquoteFlags :: Lens' UnquoteFlags TCEnv +eUnquoteFlags f e = f (envUnquoteFlags e) <&> \ x -> e { envUnquoteFlags = x } + +eInstanceDepth :: Lens' Int TCEnv +eInstanceDepth f e = f (envInstanceDepth e) <&> \ x -> e { envInstanceDepth = x } + --------------------------------------------------------------------------- -- ** Context --------------------------------------------------------------------------- @@ -1904,7 +2218,16 @@ data AbstractMode = AbstractMode -- ^ Abstract things in the current module can be accessed. | ConcreteMode -- ^ No abstract things can be accessed. | IgnoreAbstractMode -- ^ All abstract things can be accessed. - deriving (Typeable, Show) + deriving (Typeable, Show, Eq) + +aDefToMode :: IsAbstract -> AbstractMode +aDefToMode AbstractDef = AbstractMode +aDefToMode ConcreteDef = ConcreteMode + +aModeToDef :: AbstractMode -> IsAbstract +aModeToDef AbstractMode = AbstractDef +aModeToDef ConcreteMode = ConcreteDef +aModeToDef _ = __IMPOSSIBLE__ --------------------------------------------------------------------------- -- ** Insertion of implicit arguments @@ -1926,27 +2249,52 @@ data ExplicitToInstance data Candidate = Candidate { candidateTerm :: Term , candidateType :: Type , candidateEti :: ExplicitToInstance + , candidateOverlappable :: Bool } deriving (Show) +instance Free' Candidate c where + freeVars' (Candidate t u _ _) = freeVars' (t, u) --------------------------------------------------------------------------- --- * Type checking errors +-- * Type checking warnings (aka non-fatal errors) --------------------------------------------------------------------------- --- Occurence of a name in a datatype definition -data Occ = OccCon { occDatatype :: QName - , occConstructor :: QName - , occPosition :: OccPos - } - | OccClause { occFunction :: QName - , occClause :: Int - , occPosition :: OccPos - } - deriving (Show) +-- | A non-fatal error is an error which does not prevent us from +-- checking the document further and interacting with the user. + +-- We keep the state for termination issues, positivity issues and +-- unsolved constraints from when we encountered the warning so that +-- we can print it later +data Warning = + TerminationIssue [TerminationError] + | NotStrictlyPositive QName OccursWhere + | UnsolvedMetaVariables [Range] -- ^ Do not use directly with 'warning' + | UnsolvedInteractionMetas [Range] -- ^ Do not use directly with 'warning' + | UnsolvedConstraints Constraints + -- ^ Do not use directly with 'warning' + | OldBuiltin String String + -- ^ In `OldBuiltin old new`, the BUILTIN old has been replaced by new + | EmptyRewritePragma + -- ^ If the user wrote just @{-# REWRITE #-}@. + | ParseWarning ParseWarning + deriving Show + +data TCWarning + = TCWarning + { tcWarningState :: TCState + -- ^ The state in which the warning was raised. + , tcWarningClosure :: Closure Warning + -- ^ The warning and the environment in which it was raised. + } + deriving Show -data OccPos = NonPositively | ArgumentTo Nat QName - deriving (Show) +tcWarning :: TCWarning -> Warning +tcWarning = clValue . tcWarningClosure + +--------------------------------------------------------------------------- +-- * Type checking errors +--------------------------------------------------------------------------- -- | Information about a call. @@ -2083,13 +2431,13 @@ data TypeError | CannotEliminateWithPattern (NamedArg A.Pattern) Type | TooManyArgumentsInLHS Type | WrongNumberOfConstructorArguments QName Nat Nat - | ShouldBeEmpty Type [Pattern] + | ShouldBeEmpty Type [DeBruijnPattern] | ShouldBeASort Type -- ^ The given type should have been a sort. | ShouldBePi Type -- ^ The given type should have been a pi. | ShouldBeRecordType Type - | ShouldBeRecordPattern Pattern + | ShouldBeRecordPattern DeBruijnPattern | NotAProjectionPattern (NamedArg A.Pattern) | NotAProperTerm | SetOmegaNotValidType @@ -2137,7 +2485,7 @@ data TypeError | TooManyFields QName [C.Name] | DuplicateFields [C.Name] | DuplicateConstructors [C.Name] - | WithOnFreeVariable A.Expr + | WithOnFreeVariable A.Expr Term | UnexpectedWithPatterns [A.Pattern] | WithClausePatternMismatch A.Pattern Pattern | FieldOutsideRecord @@ -2146,8 +2494,8 @@ data TypeError -- TODO: Remove some of the constructors in this section, now that -- the SplitError constructor has been added? | IncompletePatternMatching Term [Elim] -- can only happen if coverage checking is switched off - | CoverageFailure QName [[Arg DeBruijnPattern]] - | UnreachableClauses QName [[Arg DeBruijnPattern]] + | CoverageFailure QName [[NamedArg DeBruijnPattern]] + | UnreachableClauses QName [[NamedArg DeBruijnPattern]] | CoverageCantSplitOn QName Telescope Args Args | CoverageCantSplitIrrelevantType Type | CoverageCantSplitType Type @@ -2160,13 +2508,11 @@ data TypeError | UnificationStuck Telescope [Term] [Term] | SplitError SplitError -- Positivity errors - | NotStrictlyPositive QName [Occ] + | TooManyPolarities QName Integer -- Import errors | LocalVsImportedModuleClash ModuleName - | UnsolvedMetas [Range] - | UnsolvedConstraints Constraints | SolvedButOpenHoles - -- ^ Some interaction points (holes) have not be filled by user. + -- ^ Some interaction points (holes) have not been filled by user. -- There are not 'UnsolvedMetas' since unification solved them. -- This is an error, since interaction points are never filled -- without user interaction. @@ -2174,6 +2520,8 @@ data TypeError | FileNotFound C.TopLevelModuleName [AbsolutePath] | OverlappingProjects AbsolutePath C.TopLevelModuleName C.TopLevelModuleName | AmbiguousTopLevelModuleName C.TopLevelModuleName [AbsolutePath] + | ModuleNameUnexpected C.TopLevelModuleName C.TopLevelModuleName + -- ^ Found module name, expected module name. | ModuleNameDoesntMatchFileName C.TopLevelModuleName [AbsolutePath] | ClashingFileNamesFor ModuleName [AbsolutePath] | ModuleDefinedInOtherFile C.TopLevelModuleName AbsolutePath AbsolutePath @@ -2201,6 +2549,7 @@ data TypeError -- definition, but it wasn't of the form @m Delta@. | NotAnExpression C.Expr | NotAValidLetBinding D.NiceDeclaration + | NotValidBeforeField D.NiceDeclaration | NothingAppliedToHiddenArg C.Expr | NothingAppliedToInstanceArg C.Expr -- Pattern synonym errors @@ -2223,6 +2572,7 @@ data TypeError | IFSNoCandidateInScope Type -- Reflection errors | UnquoteFailed UnquoteError + | DeBruijnIndexOutOfScope Nat Telescope [Name] -- Safe flag errors | SafeFlagPostulate C.Name | SafeFlagPragma [String] @@ -2230,9 +2580,14 @@ data TypeError | SafeFlagTerminating | SafeFlagPrimTrustMe | SafeFlagNoPositivityCheck + | SafeFlagPolarity -- Language option errors | NeedOptionCopatterns | NeedOptionRewriting + -- Failure associated to warnings + | NonFatalErrors [TCWarning] + -- Instance search errors + | InstanceSearchDepthExhausted Term Type Int deriving (Typeable, Show) -- | Distinguish error message when parsing lhs or pattern synonym, resp. @@ -2248,11 +2603,19 @@ instance Error TypeError where -- | Type-checking errors. -data TCErr = TypeError TCState (Closure TypeError) - | Exception Range Doc - | IOException Range E.IOException - | PatternErr -- TCState -- ^ for pattern violations - {- AbortAssign TCState -- ^ used to abort assignment to meta when there are instantiations -- UNUSED -} +data TCErr + = TypeError + { tcErrState :: TCState + -- ^ The state in which the error was raised. + , tcErrClosErr :: Closure TypeError + -- ^ The environment in which the error as raised plus the error. + } + | Exception Range Doc + | IOException Range E.IOException + | PatternErr + -- ^ The exception which is usually caught. + -- Raised for pattern violations during unification ('assignV') + -- but also in other situations where we want to backtrack. deriving (Typeable) instance Error TCErr where @@ -2263,14 +2626,12 @@ instance Show TCErr where show (Exception r d) = show r ++ ": " ++ render d show (IOException r e) = show r ++ ": " ++ show e show PatternErr{} = "Pattern violation (you shouldn't see this)" - {- show (AbortAssign _) = "Abort assignment (you shouldn't see this)" -- UNUSED -} instance HasRange TCErr where getRange (TypeError _ cl) = envRange $ clEnv cl getRange (Exception r _) = r getRange (IOException r _) = r getRange PatternErr{} = noRange - {- getRange (AbortAssign s) = noRange -- UNUSED -} instance E.Exception TCErr @@ -2297,16 +2658,29 @@ mapRedEnvSt f g (ReduceEnv e s) = ReduceEnv (f e) (g s) newtype ReduceM a = ReduceM { unReduceM :: ReduceEnv -> a } -- deriving (Functor, Applicative, Monad) +fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b +fmapReduce f (ReduceM m) = ReduceM $ \ e -> f $! m e +{-# INLINE fmapReduce #-} + +apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b +apReduce (ReduceM f) (ReduceM x) = ReduceM $ \ e -> f e $! x e +{-# INLINE apReduce #-} + +bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b +bindReduce (ReduceM m) f = ReduceM $ \ e -> unReduceM (f $! m e) e +{-# INLINE bindReduce #-} + instance Functor ReduceM where - fmap f (ReduceM m) = ReduceM $ \ e -> f $! m e + fmap = fmapReduce instance Applicative ReduceM where pure x = ReduceM (const x) - ReduceM f <*> ReduceM x = ReduceM $ \ e -> f e $! x e + (<*>) = apReduce instance Monad ReduceM where return = pure - ReduceM m >>= f = ReduceM $ \ e -> unReduceM (f $! m e) e + (>>=) = bindReduce + (>>) = (*>) instance ReadTCState ReduceM where getTCState = ReduceM redSt @@ -2369,6 +2743,16 @@ instance MonadError TCErr (TCMT IO) where writeIORef r $ oldState { stPersistentState = stPersistentState newState } unTCM (h err) r e +-- | Parse monad + +runPM :: PM a -> TCM a +runPM m = do + (res, ws) <- runPMIO m + mapM_ (warning . ParseWarning) ws + case res of + Left e -> throwError (Exception (getRange e) (pretty e)) + Right a -> return a + -- | Interaction monad. type IM = TCMT (Haskeline.InputT IO) @@ -2491,11 +2875,9 @@ instance MonadIO m => MonadIO (TCMT m) where x <- m x `seq` return x where - wrap r m = failOnException handleException - $ E.catch m (handleIOException r) + wrap r m = E.catch m (handleIOException r) handleIOException r e = E.throwIO $ IOException r e - handleException r s = E.throwIO $ Exception r s -- | We store benchmark statistics in an IORef. -- This enables benchmarking pure computation, see @@ -2510,9 +2892,12 @@ instance Null (TCM Doc) where null = __IMPOSSIBLE__ -- | Short-cutting disjunction forms a monoid. +instance Semigroup (TCM Any) where + ma <> mb = Any <$> do (getAny <$> ma) `or2M` (getAny <$> mb) + instance Monoid (TCM Any) where mempty = return mempty - ma `mappend` mb = Any <$> do (getAny <$> ma) `or2M` (getAny <$> mb) + mappend = (<>) patternViolation :: TCM a patternViolation = throwError PatternErr @@ -2523,6 +2908,10 @@ internalError s = typeError $ InternalError s genericError :: MonadTCM tcm => String -> tcm a genericError = typeError . GenericError +{-# SPECIALIZE genericDocError :: Doc -> TCM a #-} +genericDocError :: MonadTCM tcm => Doc -> tcm a +genericDocError = typeError . GenericDocError + {-# SPECIALIZE typeError :: TypeError -> TCM a #-} typeError :: MonadTCM tcm => TypeError -> tcm a typeError err = liftTCM $ throwError =<< typeError_ err @@ -2531,6 +2920,16 @@ typeError err = liftTCM $ throwError =<< typeError_ err typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr typeError_ err = liftTCM $ TypeError <$> get <*> buildClosure err +{-# SPECIALIZE warning_ :: Warning -> TCM TCWarning #-} +warning_ :: MonadTCM tcm => Warning -> tcm TCWarning +warning_ w = liftTCM $ TCWarning <$> get <*> buildClosure w + +{-# SPECIALIZE warning :: Warning -> TCM () #-} +warning :: MonadTCM tcm => Warning -> tcm () +warning w = do + tcwarn <- warning_ w + stTCWarnings %= (tcwarn :) + -- | Running the type checking monad (most general form). {-# SPECIALIZE runTCM :: TCEnv -> TCState -> TCM a -> IO (a, TCState) #-} runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState) @@ -2614,15 +3013,15 @@ instance KillRange Section where killRange (Section tel) = killRange1 Section tel instance KillRange Definition where - killRange (Defn ai name t pols occs displ mut compiled inst copy def) = - killRange11 Defn ai name t pols occs displ mut compiled inst copy def + killRange (Defn ai name t pols occs displ mut compiled inst copy ma def) = + killRange11 Defn ai name t pols occs displ mut compiled inst copy ma def -- TODO clarify: Keep the range in the defName field? instance KillRange CtxId where killRange (CtxId x) = killRange1 CtxId x instance KillRange NLPat where - killRange (PVar x y) = killRange1 PVar x y + killRange (PVar x y z) = killRange3 PVar x y z killRange (PWild) = PWild killRange (PDef x y) = killRange2 PDef x y killRange (PLam x y) = killRange2 PLam x y @@ -2630,9 +3029,12 @@ instance KillRange NLPat where killRange (PBoundVar x y) = killRange2 PBoundVar x y killRange (PTerm x) = killRange1 PTerm x +instance KillRange NLPType where + killRange (NLPType s a) = killRange2 NLPType s a + instance KillRange RewriteRule where - killRange (RewriteRule q gamma lhs rhs t) = - killRange5 RewriteRule q gamma lhs rhs t + killRange (RewriteRule q gamma f es rhs t) = + killRange6 RewriteRule q gamma f es rhs t instance KillRange CompiledRepresentation where killRange = id @@ -2644,15 +3046,19 @@ instance KillRange EtaEquality where instance KillRange ExtLamInfo where killRange = id +instance KillRange FunctionFlag where + killRange = id + instance KillRange Defn where killRange def = case def of Axiom -> Axiom - Function cls comp tt inv mut isAbs delayed proj static inline smash term extlam with cop -> - killRange15 Function cls comp tt inv mut isAbs delayed proj static inline smash term extlam with cop + AbstractDefn -> __IMPOSSIBLE__ -- only returned by 'getConstInfo'! + Function cls comp tt inv mut isAbs delayed proj flags term extlam with copat -> + killRange13 Function cls comp tt inv mut isAbs delayed proj flags term extlam with copat Datatype a b c d e f g h i j -> killRange10 Datatype a b c d e f g h i j - Record a b c d e f g h i j k l -> killRange12 Record a b c d e f g h i j k l - Constructor a b c d e -> killRange5 Constructor a b c d e + Record a b c d e f g h i j k -> killRange11 Record a b c d e f g h i j k + Constructor a b c d e f -> killRange6 Constructor a b c d e f Primitive a b c d -> killRange4 Primitive a b c d instance KillRange MutualId where @@ -2668,13 +3074,20 @@ instance KillRange TermHead where killRange (ConsHead q) = ConsHead $ killRange q instance KillRange Projection where - killRange (Projection a b c d e) = killRange4 Projection a b c d e + killRange (Projection a b c d e) = killRange5 Projection a b c d e + +instance KillRange ProjLams where + killRange = id instance KillRange a => KillRange (Open a) where killRange = fmap killRange +instance KillRange a => KillRange (Local a) where + killRange (Local a b) = killRange2 Local a b + killRange (Global a) = killRange1 Global a + instance KillRange DisplayForm where - killRange (Display n vs dt) = killRange3 Display n vs dt + killRange (Display n es dt) = killRange3 Display n es dt instance KillRange Polarity where killRange = id @@ -2682,8 +3095,8 @@ instance KillRange Polarity where instance KillRange DisplayTerm where killRange dt = case dt of - DWithApp dt dts args -> killRange3 DWithApp dt dts args - DCon q dts -> killRange2 DCon q dts + DWithApp dt dts es -> killRange3 DWithApp dt dts es + DCon q ci dts -> killRange3 DCon q ci dts DDef q dts -> killRange2 DDef q dts DDot v -> killRange1 DDot v DTerm v -> killRange1 DTerm v |