summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Monad/Base.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Monad/Base.hs')
-rw-r--r--src/full/Agda/TypeChecking/Monad/Base.hs759
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