1
{-# LANGUAGE CPP, ExistentialQuantification, FlexibleContexts, Rank2Types,
2
TypeSynonymInstances, MultiParamTypeClasses, FlexibleInstances,
3
UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving,
4
DeriveFunctor, DeriveFoldable, DeriveTraversable
2
{-# LANGUAGE DeriveDataTypeable #-}
3
{-# LANGUAGE DeriveFoldable #-}
4
{-# LANGUAGE DeriveFunctor #-}
5
{-# LANGUAGE DeriveTraversable #-}
6
{-# LANGUAGE ExistentialQuantification #-}
7
{-# LANGUAGE FlexibleContexts #-}
8
{-# LANGUAGE FlexibleInstances #-}
9
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
10
{-# LANGUAGE MultiParamTypeClasses #-}
11
{-# LANGUAGE NamedFieldPuns #-}
12
{-# LANGUAGE Rank2Types #-}
13
{-# LANGUAGE ScopedTypeVariables #-}
14
{-# LANGUAGE TypeSynonymInstances #-}
15
{-# LANGUAGE UndecidableInstances #-}
6
17
module Agda.TypeChecking.Monad.Base where
19
import Control.Arrow ((***), first, second)
9
20
import qualified Control.Concurrent as C
10
21
import Control.DeepSeq
11
22
import Control.Exception as E
12
23
import Control.Monad.Error
13
24
import Control.Monad.State
14
25
import Control.Monad.Reader
26
import Control.Monad.Writer
27
import Control.Monad.Trans.Maybe
15
28
import Control.Applicative
16
30
import Data.Function
32
import qualified Data.List as List
18
33
import Data.Map as Map
19
34
import Data.Set as Set
20
35
import Data.Sequence as Seq
22
37
import Data.Foldable
23
38
import Data.Traversable
27
import Agda.Syntax.Common
41
import Agda.Syntax.Concrete (TopLevelModuleName)
42
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
43
import qualified Agda.Syntax.Common as Common
28
44
import qualified Agda.Syntax.Concrete as C
29
45
import qualified Agda.Syntax.Concrete.Definitions as D
30
46
import qualified Agda.Syntax.Abstract as A
31
import Agda.Syntax.Internal
47
import Agda.Syntax.Internal as I
32
48
import Agda.Syntax.Position
33
49
import Agda.Syntax.Scope.Base
34
import Agda.Utils.HashMap as HMap
36
51
import Agda.TypeChecking.CompiledClause
38
53
import Agda.Interaction.Exceptions
39
import {-# SOURCE #-} Agda.Interaction.FindFile
54
-- import {-# SOURCE #-} Agda.Interaction.FindFile
40
55
import Agda.Interaction.Options
41
import qualified Agda.Interaction.Highlighting.Range as R
42
56
import {-# SOURCE #-} Agda.Interaction.Response
43
(InteractionOutputCallback, defaultInteractionOutputCallback)
57
(InteractionOutputCallback, defaultInteractionOutputCallback, Response)
44
58
import Agda.Interaction.Highlighting.Precise
45
59
(CompressedFile, HighlightingInfo)
48
61
import qualified Agda.Compiler.JS.Syntax as JS
63
import Agda.TypeChecking.Monad.Base.Benchmark (Benchmark)
64
import qualified Agda.TypeChecking.Monad.Base.Benchmark as Benchmark
50
66
import Agda.Utils.FileName
51
67
import Agda.Utils.Fresh
52
import Agda.Utils.Monad
68
import Agda.Utils.HashMap as HMap
69
import Agda.Utils.Hash
53
70
import Agda.Utils.Permutation
54
71
import Agda.Utils.Pretty
55
72
import Agda.Utils.Time
112
128
data PersistentTCState = PersistentTCSt
113
129
{ stDecodedModules :: DecodedModules
114
130
, stPersistentOptions :: CommandLineOptions
115
-- ^ Options which apply to all files, unless overridden.
131
, stInteractionOutputCallback :: InteractionOutputCallback
132
-- ^ Callback function to call when there is a response
133
-- to give to the interactive frontend.
134
-- See the documentation of 'InteractionOutputCallback'.
135
, stBenchmark :: !Benchmark
136
-- ^ Structure to track how much CPU time was spent on which Agda phase.
137
-- Needs to be a strict field to avoid space leaks!
140
-- | Empty persistent state.
142
initPersistentState :: PersistentTCState
143
initPersistentState = PersistentTCSt
144
{ stPersistentOptions = defaultOptions
145
, stDecodedModules = Map.empty
146
, stInteractionOutputCallback = defaultInteractionOutputCallback
147
, stBenchmark = Benchmark.empty
118
150
data FreshThings =
162
-- | Empty state of type checker.
130
164
initState :: TCState
132
TCSt { stFreshThings = (Fresh 0 0 0 (NameId 0 0) 0 0 0) { fProblem = 1 }
133
, stMetaStore = Map.empty
134
, stSyntaxInfo = mempty
136
, stTermErrs = Seq.empty
137
, stInteractionPoints = Map.empty
138
, stAwakeConstraints = []
139
, stSleepingConstraints = []
141
, stOccursCheckDefs = Set.empty
142
, stSignature = emptySignature
143
, stImports = emptySignature
144
, stImportedModules = Set.empty
145
, stModuleToSource = Map.empty
146
, stVisitedModules = Map.empty
147
, stCurrentModule = Nothing
148
, stScope = emptyScopeInfo
149
, stPatternSyns = Map.empty
150
, stPatternSynImports = Map.empty
151
, stPragmaOptions = defaultInteractionOptions
152
, stStatistics = Map.empty
153
, stExtLambdaTele = Map.empty
154
, stMutualBlocks = Map.empty
155
, stLocalBuiltins = Map.empty
156
, stImportedBuiltins = Map.empty
157
, stHaskellImports = Set.empty
158
, stPersistent = PersistentTCSt
159
{ stPersistentOptions = defaultOptions
160
, stDecodedModules = Map.empty
162
, stInteractionOutputCallback = defaultInteractionOutputCallback
166
{ stFreshThings = (Fresh 0 0 0 (NameId 0 0) 0 0 0) { fProblem = 1 }
167
, stMetaStore = Map.empty
168
, stSyntaxInfo = mempty
170
, stTermErrs = Seq.empty
171
, stInteractionPoints = Map.empty
172
, stAwakeConstraints = []
173
, stSleepingConstraints = []
175
, stOccursCheckDefs = Set.empty
176
, stSignature = emptySignature
177
, stImports = emptySignature
178
, stImportedModules = Set.empty
179
, stModuleToSource = Map.empty
180
, stVisitedModules = Map.empty
181
, stCurrentModule = Nothing
182
, stScope = emptyScopeInfo
183
, stPatternSyns = Map.empty
184
, stPatternSynImports = Map.empty
185
, stPragmaOptions = defaultInteractionOptions
186
, stStatistics = Map.empty
187
, stMutualBlocks = Map.empty
188
, stLocalBuiltins = Map.empty
189
, stImportedBuiltins = Map.empty
190
, stHaskellImports = Set.empty
191
, stPersistent = initPersistentState
165
194
stBuiltinThings :: TCState -> BuiltinThings PrimFun
166
195
stBuiltinThings s = stLocalBuiltins s `Map.union` stImportedBuiltins s
234
282
type VisitedModules = Map C.TopLevelModuleName ModuleInfo
235
type DecodedModules = Map C.TopLevelModuleName (Interface, ClockTime)
283
type DecodedModules = Map C.TopLevelModuleName Interface
237
285
data Interface = Interface
238
{ iImportedModules :: [ModuleName]
239
, iModuleName :: ModuleName
240
, iScope :: Map ModuleName Scope
241
, iInsideScope :: ScopeInfo
242
, iSignature :: Signature
243
, iBuiltin :: BuiltinThings (String, QName)
244
, iHaskellImports :: Set String
245
-- ^ Haskell imports listed in
246
-- (transitively) imported modules are
247
-- not included here.
248
, iHighlighting :: HighlightingInfo
249
, iPragmaOptions :: [OptionsPragma]
250
-- ^ Pragma options set in the file.
251
, iPatternSyns :: A.PatternSynDefns
253
deriving (Typeable, Show)
286
{ iSourceHash :: Hash
287
-- ^ Hash of the source code.
288
, iImportedModules :: [(ModuleName, Hash)]
289
-- ^ Imported modules and their hashes.
290
, iModuleName :: ModuleName
291
-- ^ Module name of this interface.
292
, iScope :: Map ModuleName Scope
293
, iInsideScope :: ScopeInfo
294
-- ^ Scope after we loaded this interface.
295
-- Used in 'Agda.Interaction.BasicOps.AtTopLevel'
296
-- and 'Agda.Interaction.CommandLine.CommandLine.interactionLoop'.
297
, iSignature :: Signature
298
, iBuiltin :: BuiltinThings (String, QName)
299
, iHaskellImports :: Set String
300
-- ^ Haskell imports listed in
301
-- (transitively) imported modules are
302
-- not included here.
303
, iHighlighting :: HighlightingInfo
304
, iPragmaOptions :: [OptionsPragma]
305
-- ^ Pragma options set in the file.
306
, iPatternSyns :: A.PatternSynDefns
308
deriving (Typeable, Show)
310
-- | Combines the source hash and the (full) hashes of the imported modules.
311
iFullHash :: Interface -> Hash
312
iFullHash i = combineHashes $ iSourceHash i : List.map snd (iImportedModules i)
255
314
---------------------------------------------------------------------------
304
366
| FindInScope MetaId [(Term, Type)]
305
367
deriving (Typeable, Show)
369
instance HasRange Constraint where
370
getRange (IsEmpty r t) = r
372
{- no Range instances for Term, Type, Elm, Tele, Sort, Level, MetaId
373
getRange (ValueCmp cmp a u v) = getRange (a,u,v)
374
getRange (ElimCmp pol a v es es') = getRange (a,v,es,es')
375
getRange (TypeCmp cmp a b) = getRange (a,b)
376
getRange (TelCmp a b cmp tel tel') = getRange (a,b,tel,tel')
377
getRange (SortCmp cmp s s') = getRange (s,s')
378
getRange (LevelCmp cmp l l') = getRange (l,l')
379
getRange (UnBlock x) = getRange x
380
getRange (Guarded c pid) = getRange c
381
getRange (FindInScope x cands) = getRange x
307
384
data Comparison = CmpEq | CmpLeq
308
385
deriving (Eq, Typeable)
312
389
show CmpLeq = "=<"
391
-- | An extension of 'Comparison' to @>=@.
392
data CompareDirection = DirEq | DirLeq | DirGeq
393
deriving (Eq, Typeable)
395
instance Show CompareDirection where
400
-- | Embed 'Comparison' into 'CompareDirection'.
401
fromCmp :: Comparison -> CompareDirection
402
fromCmp CmpEq = DirEq
403
fromCmp CmpLeq = DirLeq
405
-- | Flip the direction of comparison.
406
flipCmp :: CompareDirection -> CompareDirection
407
flipCmp DirEq = DirEq
408
flipCmp DirLeq = DirGeq
409
flipCmp DirGeq = DirLeq
411
-- | Turn a 'Comparison' function into a 'CompareDirection' function.
413
-- Property: @dirToCmp f (fromCmp cmp) = f cmp@
414
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
415
dirToCmp cont DirEq = cont CmpEq
416
dirToCmp cont DirLeq = cont CmpLeq
417
dirToCmp cont DirGeq = flip $ cont CmpLeq
314
419
---------------------------------------------------------------------------
316
421
---------------------------------------------------------------------------
318
423
-- | A thing tagged with the context it came from.
319
data Open a = OpenThing [CtxId] a
424
data Open a = OpenThing { openThingCtxIds :: [CtxId], openThing :: a }
320
425
deriving (Typeable, Show, Functor)
322
427
---------------------------------------------------------------------------
458
577
getMetaRelevance :: MetaVariable -> Relevance
459
578
getMetaRelevance = envRelevance . getMetaEnv
580
getMetaColors :: MetaVariable -> [Color]
581
getMetaColors = envColors . getMetaEnv
461
583
---------------------------------------------------------------------------
462
584
-- ** Interaction meta variables
463
585
---------------------------------------------------------------------------
465
type InteractionPoints = Map InteractionId MetaId
467
newtype InteractionId = InteractionId Nat
468
deriving (Eq,Ord,Num,Integral,Real,Enum)
470
instance Show InteractionId where
471
show (InteractionId x) = "?" ++ show x
587
-- | Interaction points are created by the scope checker who sets the range.
588
-- The meta variable is created by the type checker and then hooked up to the
589
-- interaction point.
590
data InteractionPoint = InteractionPoint
591
{ ipRange :: Range -- ^ The position of the interaction point.
592
, ipMeta :: Maybe MetaId -- ^ The meta variable, if any, holding the type etc.
595
instance Eq InteractionPoint where (==) = (==) `on` ipMeta
597
-- | Data structure managing the interaction points.
598
type InteractionPoints = Map InteractionId InteractionPoint
473
600
---------------------------------------------------------------------------
497
624
emptySignature :: Signature
498
625
emptySignature = Sig Map.empty HMap.empty
500
data DisplayForm = Display Nat [Term] DisplayTerm
501
-- ^ The three arguments are:
503
-- * @n@: number of free variables;
505
-- * Patterns for arguments, one extra free var which
506
-- represents pattern vars. There should @n@ of them.
508
-- * Display form. @n@ free variables.
509
deriving (Typeable, Show)
511
data DisplayTerm = DWithApp [DisplayTerm] Args
512
| DCon QName [Arg DisplayTerm]
513
| DDef QName [Arg DisplayTerm]
516
deriving (Typeable, Show)
627
-- | A @DisplayForm@ is in essence a rewrite rule
631
-- for a defined symbol (could be a constructor as well) @q@.
632
-- The right hand side is a 'DisplayTerm' which is used to
633
-- 'reify' to a more readable 'Abstract.Syntax'.
635
-- The patterns @ts@ are just terms, but @var 0@ is interpreted
636
-- as a hole. Each occurrence of @var 0@ is a new hole (pattern var).
637
-- For each *occurrence* of @var0@ the rhs @dt@ has a free variable.
638
-- These are instantiated when matching a display form against a
639
-- term @q vs@ succeeds.
640
data DisplayForm = Display
642
-- ^ Number @n@ of free variables in 'dfRHS'.
644
-- ^ Left hand side patterns, where @var 0@ stands for a pattern
645
-- variable. There should be @n@ occurrences of @var0@ in
647
, dfRHS :: DisplayTerm
648
-- ^ Right hand side, with @n@ free variables.
650
deriving (Typeable, Show)
652
-- | A structured presentation of a 'Term' for reification into
653
-- 'Abstract.Syntax'.
655
= DWithApp DisplayTerm [DisplayTerm] Args
656
-- ^ @(f vs | ws) us@.
657
-- The first 'DisplayTerm' is the parent function @f@ with its args @vs@.
658
-- The list of 'DisplayTerm's are the with expressions @ws@.
659
-- The 'Args' are additional arguments @us@
660
-- (possible in case the with-application is of function type).
661
| DCon QName [Arg DisplayTerm]
663
| DDef QName [Arg DisplayTerm]
669
deriving (Typeable, Show)
671
-- | By default, we have no display form.
518
672
defaultDisplayForm :: QName -> [Open DisplayForm]
519
673
defaultDisplayForm c = []
675
defRelevance = argInfoRelevance . defArgInfo
676
defColors = argInfoColors . defArgInfo
521
678
data Definition = Defn
522
{ defRelevance :: Relevance -- ^ Some defs can be irrelevant (but not hidden).
679
{ defArgInfo :: ArgInfo -- ^ Hiding should not be used.
523
680
, defName :: QName
524
, defType :: Type -- ^ Type of the lifted definition.
681
, defType :: Type -- ^ Type of the lifted definition.
525
682
, defPolarity :: [Polarity]
526
683
, defArgOccurrences :: [Occurrence]
527
684
, defDisplay :: [Open DisplayForm]
575
749
instance NFData Occurrence
751
-- | Additional information for projection 'Function's.
752
data Projection = Projection
753
{ projProper :: Maybe QName
754
-- ^ @Nothing@ if only projection-like, @Just q@ if record projection,
755
-- where @q@ is the original projection name
756
-- (current name could be from module app).
757
, projFromType :: QName
758
-- ^ Type projected from. Record type if @projProper = Just{}@.
760
-- ^ Index of the record argument.
761
-- Start counting with 1, because 0 means that
762
-- it is already applied to the record.
763
-- (Can happen in module instantiation.)
764
, projDropPars :: Term
765
-- ^ Term @t@ to be be applied to record parameters and record value.
766
-- The parameters will be dropped.
767
-- In case of a proper projection, a postfix projection application
768
-- will be created: @t = \ pars r -> r .p@
769
-- In case of a projection-like function, just the function symbol
770
-- is returned as 'Def': @t = \ pars -> f@.
771
, projArgInfo :: I.ArgInfo
772
-- ^ The info of the principal (record) argument.
773
} deriving (Typeable, Show)
577
775
data Defn = Axiom
579
778
{ funClauses :: [Clause]
580
, funCompiled :: CompiledClauses
779
, funCompiled :: Maybe CompiledClauses
780
-- ^ 'Nothing' while function is still type-checked.
781
-- @Just cc@ after type and coverage checking and
782
-- translation to case trees.
581
783
, funInv :: FunctionInverse
582
{- MOVED to Definition
583
, funPolarity :: [Polarity]
584
, funArgOccurrences :: [Occurrence]
586
784
, funMutual :: [QName]
587
785
-- ^ Mutually recursive functions, @data@s and @record@s.
786
-- Does not include this function.
588
787
, funAbstr :: IsAbstract
589
788
, funDelayed :: Delayed
590
789
-- ^ Are the clauses of this definition delayed?
591
, funProjection :: Maybe (QName, Int)
790
, funProjection :: Maybe Projection
592
791
-- ^ Is it a record projection?
593
792
-- If yes, then return the name of the record type and index of
594
793
-- the record argument. Start counting with 1, because 0 means that
602
801
-- instantiation?
603
802
, funTerminates :: Maybe Bool
604
803
-- ^ Has this function been termination checked? Did it pass?
804
, funExtLam :: Maybe (Int,Int)
805
-- ^ Is this function generated from an extended lambda?
806
-- If yes, then return the number of hidden and non-hidden lambda-lifted arguments
807
, funWith :: Maybe QName
808
-- ^ Is this a generated with-function? If yes, then what's the
809
-- name of the parent function.
607
{ dataPars :: Nat -- nof parameters
608
, dataIxs :: Nat -- nof indices
609
, dataInduction :: Induction -- data or codata?
610
, dataClause :: (Maybe Clause) -- this might be in an instantiated module
611
, dataCons :: [QName] -- constructor names
812
{ dataPars :: Nat -- ^ Number of parameters.
813
, dataSmallPars :: Permutation -- ^ Parameters that are maybe small.
814
, dataNonLinPars :: Drop Permutation -- ^ Parameters that appear in indices.
815
, dataIxs :: Nat -- ^ Number of indices.
816
, dataInduction :: Induction -- ^ @data@ or @codata@ (legacy).
817
, dataClause :: (Maybe Clause) -- ^ This might be in an instantiated module.
818
, dataCons :: [QName] -- ^ Constructor names.
612
819
, dataSort :: Sort
614
, dataPolarity :: [Polarity]
615
, dataArgOccurrences :: [Occurrence]
617
, dataMutual :: [QName] -- ^ Mutually recursive functions, @data@s and @record@s.
820
, dataMutual :: [QName] -- ^ Mutually recursive functions, @data@s and @record@s. Does not include this data type.
618
821
, dataAbstr :: IsAbstract
621
824
{ recPars :: Nat -- ^ Number of parameters.
622
825
, recClause :: Maybe Clause
623
, recCon :: QName -- ^ Constructor name.
826
, recConHead :: ConHead -- ^ Constructor name and fields.
624
827
, recNamedCon :: Bool
625
, recConType :: Type -- ^ The record constructor's type.
626
, recFields :: [Arg A.QName]
627
, recTel :: Telescope -- ^ The record field telescope
629
, recPolarity :: [Polarity]
630
, recArgOccurrences :: [Occurrence]
632
, recMutual :: [QName] -- ^ Mutually recursive functions, @data@s and @record@s.
633
, recEtaEquality :: Bool -- ^ Eta-expand at this record type. @False@ for unguarded recursive records.
828
, recConType :: Type -- ^ The record constructor's type. (Includes record parameters.)
829
, recFields :: [Arg QName]
830
, recTel :: Telescope -- ^ The record field telescope. (Includes record parameters.)
831
-- Note: @TelV recTel _ == telView' recConType@.
832
-- Thus, @recTel@ is redundant.
833
, recMutual :: [QName] -- ^ Mutually recursive functions, @data@s and @record@s. Does not include this record.
834
, recEtaEquality :: Bool -- ^ Eta-expand at this record type. @False@ for unguarded recursive records and coinductive records.
634
835
, recInduction :: Induction -- ^ 'Inductive' or 'Coinductive'? Matters only for recursive records.
635
836
, recRecursive :: Bool -- ^ Recursive record. Implies @recEtaEquality = False@. Projections are not size-preserving.
636
837
, recAbstr :: IsAbstract
639
{ conPars :: Nat -- nof parameters
640
, conSrcCon :: QName -- original constructor (this might be in a module instance)
641
, conData :: QName -- name of datatype or record type
840
{ conPars :: Nat -- ^ Number of parameters.
841
, conSrcCon :: ConHead -- ^ Name of (original) constructor and fields. (This might be in a module instance.)
842
, conData :: QName -- ^ Name of datatype or record type.
642
843
, conAbstr :: IsAbstract
643
844
, conInd :: Induction -- ^ Inductive or coinductive?
646
847
{ primAbstr :: IsAbstract
647
848
, primName :: String
648
, primClauses :: Maybe [Clause]
649
-- ^ 'Nothing' for primitive functions, @'Just'
650
-- something@ for builtin functions.
849
, primClauses :: [Clause]
850
-- ^ 'null' for primitive functions, @not null@ for builtin functions.
651
851
, primCompiled :: Maybe CompiledClauses
652
-- ^ 'Nothing' for primitive functions, @'Just'
653
-- something@ for builtin functions.
852
-- ^ 'Nothing' for primitive functions,
853
-- @'Just' something@ for builtin functions.
655
855
-- ^ Primitive or builtin functions.
656
856
deriving (Typeable, Show)
858
-- | A template for creating 'Function' definitions, with sensible defaults.
859
emptyFunction :: Defn
860
emptyFunction = Function
862
, funCompiled = Nothing
863
, funInv = NotInjective
865
, funAbstr = ConcreteDef
866
, funDelayed = NotDelayed
867
, funProjection = Nothing
870
, funTerminates = Nothing
871
, funExtLam = Nothing
876
recCon :: Defn -> QName
877
recCon Record{ recConHead } = conName recConHead
878
recCon _ = __IMPOSSIBLE__
658
880
defIsRecord :: Defn -> Bool
659
881
defIsRecord Record{} = True
660
882
defIsRecord _ = False
667
889
newtype Fields = Fields [(C.Name, Type)]
668
890
deriving (Typeable)
670
data Reduced no yes = NoReduction no | YesReduction yes
892
-- | Did we encounter a simplifying reduction?
893
-- In terms of CIC, that would be a iota-reduction.
894
-- In terms of Agda, this is a constructor or literal
895
-- pattern that matched.
896
-- Just beta-reduction (substitution) or delta-reduction
897
-- (unfolding of definitions) does not count as simplifying?
899
data Simplification = YesSimplification | NoSimplification
900
deriving (Typeable, Eq, Show)
902
instance Monoid Simplification where
903
mempty = NoSimplification
904
mappend YesSimplification _ = YesSimplification
905
mappend NoSimplification s = s
907
data Reduced no yes = NoReduction no | YesReduction Simplification yes
671
908
deriving (Typeable, Functor)
673
data IsReduced = NotReduced | Reduced (Blocked ())
910
-- | Three cases: 1. not reduced, 2. reduced, but blocked, 3. reduced, not blocked.
913
| Reduced (Blocked ())
674
915
data MaybeReduced a = MaybeRed
675
916
{ isReduced :: IsReduced
676
917
, ignoreReduced :: a
678
919
deriving (Functor)
921
instance IsProjElim e => IsProjElim (MaybeReduced e) where
922
isProjElim = isProjElim . ignoreReduced
680
924
type MaybeReducedArgs = [MaybeReduced (Arg Term)]
925
type MaybeReducedElims = [MaybeReduced Elim]
682
927
notReduced :: a -> MaybeReduced a
683
928
notReduced x = MaybeRed NotReduced x
685
930
reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
686
931
reduced b = case fmap ignoreSharing <$> b of
687
NotBlocked (Arg _ _ (MetaV x _)) -> MaybeRed (Reduced $ Blocked x ()) v
688
_ -> MaybeRed (Reduced $ () <$ b) v
932
NotBlocked (Common.Arg _ (MetaV x _)) -> MaybeRed (Reduced $ Blocked x ()) v
933
_ -> MaybeRed (Reduced $ () <$ b) v
690
935
v = ignoreBlocking b
937
-- | Controlling 'reduce'.
938
data AllowedReduction
939
= ProjectionReductions -- ^ (Projection and) projection-like functions may be reduced.
940
| FunctionReductions -- ^ Functions which are not projections may be reduced.
941
| LevelReductions -- ^ Reduce @'Level'@ terms.
942
deriving (Show, Eq, Ord, Enum, Bounded)
944
type AllowedReductions = [AllowedReduction]
946
allReductions = [minBound..maxBound]
692
948
data PrimFun = PrimFun
693
949
{ primFunName :: QName
694
950
, primFunArity :: Arity
695
, primFunImplementation :: [Arg Term] -> TCM (Reduced MaybeReducedArgs Term)
951
, primFunImplementation :: [Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)
697
953
deriving (Typeable)
699
955
defClauses :: Definition -> [Clause]
700
956
defClauses Defn{theDef = Function{funClauses = cs}} = cs
701
defClauses Defn{theDef = Primitive{primClauses = Just cs}} = cs
957
defClauses Defn{theDef = Primitive{primClauses = cs}} = cs
702
958
defClauses Defn{theDef = Datatype{dataClause = Just c}} = [c]
703
959
defClauses Defn{theDef = Record{recClause = Just c}} = [c]
704
960
defClauses _ = []
706
962
defCompiled :: Definition -> Maybe CompiledClauses
707
defCompiled Defn{theDef = Function{funCompiled = cc}} = Just cc
963
defCompiled Defn{theDef = Function {funCompiled = mcc}} = mcc
708
964
defCompiled Defn{theDef = Primitive{primCompiled = mcc}} = mcc
709
965
defCompiled _ = Nothing
942
1206
-- doing speculative checking, like solve instance metas, or
943
1207
-- when updating might break abstraction, as is the case when
944
1208
-- checking abstract definitions.
1209
, envExpandLast :: ExpandHidden
1210
-- ^ When type-checking an alias f=e, we do not want
1211
-- to insert hidden arguments in the end, because
1212
-- these will become unsolved metas.
1213
, envAppDef :: Maybe QName
1214
-- ^ We are reducing an application of this function.
1215
-- (For debugging of incomplete matches only.)
1216
, envSimplification :: Simplification
1217
-- ^ Did we encounter a simplification (proper match)
1218
-- during the current reduction process?
1219
, envAllowedReductions :: AllowedReductions
1220
, envPrintDomainFreePi :: Bool
1221
-- ^ When True types will be omitted from printed pi types if they
1223
, envInsideDotPattern :: Bool
1224
-- ^ Used by the scope checker to make sure that certain forms
1225
-- of expressions are not used inside dot patterns: extended
1226
-- lambdas and let-expressions.
946
1228
deriving (Typeable)
956
1238
, envSolvingConstraints = False
957
1239
, envActiveProblems = [0]
958
1240
, envAssignMetas = True
959
, envAbstractMode = AbstractMode
1241
, envAbstractMode = ConcreteMode
1242
-- Andreas, 2013-02-21: This was 'AbstractMode' until now.
1243
-- However, top-level checks for mutual blocks, such as
1244
-- constructor-headedness, should not be able to look into
1245
-- abstract definitions unless abstract themselves.
1246
-- (See also discussion on issue 796.)
1247
-- The initial mode should be 'ConcreteMode', ensuring you
1248
-- can only look into abstract things in an abstract
1249
-- definition (which sets 'AbstractMode').
960
1250
, envRelevance = Relevant
961
1252
, envDisplayFormsEnabled = True
962
1253
, envReifyInteractionPoints = True
963
1254
, envEtaContractImplicit = True
964
1255
, envRange = noRange
965
1256
, envHighlightingRange = noRange
966
1257
, envCall = Nothing
968
1258
, envHighlightingLevel = None
969
1259
, envHighlightingMethod = Indirect
970
1260
, envModuleNestingLevel = -1
971
1261
, envAllowDestructiveUpdate = True
1262
, envExpandLast = ExpandLast
1263
, envAppDef = Nothing
1264
, envSimplification = NoSimplification
1265
, envAllowedReductions = allReductions
1266
, envPrintDomainFreePi = False
1267
, envInsideDotPattern = False
974
1270
---------------------------------------------------------------------------
1034
1332
-- | Information about a call.
1036
1334
data CallInfo = CallInfo
1037
{ callInfoRange :: Range
1038
-- ^ Range of the head identifier.
1039
, callInfoCall :: String
1040
-- ^ Formatted representation of the call.
1042
-- ('Doc' would perhaps be better here, but 'Doc' doesn't come
1043
-- with an 'Ord' instance.)
1044
} deriving (Eq, Ord, Typeable, Show)
1335
{ callInfoTarget :: QName
1336
-- ^ Target function name pretty-printed.
1337
, callInfoRange :: Range
1338
-- ^ Range of the target function.
1339
, callInfoCall :: Closure Term
1340
-- ^ To be formatted representation of the call.
1343
-- no Eq, Ord instances: too expensive! (see issues 851, 852)
1345
-- | We only 'show' the name of the callee.
1346
instance Show CallInfo where show = show . callInfoTarget
1348
instance Pretty CallInfo where pretty = text . show . callInfoTarget
1046
1350
-- | Information about a mutual block which did not pass the
1047
1351
-- termination checker.
1052
1356
-- automatically generated functions.)
1053
1357
, termErrCalls :: [CallInfo]
1054
1358
-- ^ The problematic call sites.
1055
} deriving (Typeable, Show, Eq)
1058
instance Eq TerminationError where
1059
(==) = (==) `on` termErrCalls
1359
} deriving (Typeable, Show)
1362
data SplitError = NotADatatype (Closure Type) -- ^ neither data type nor record
1363
| IrrelevantDatatype (Closure Type) -- ^ data type, but in irrelevant position
1364
| CoinductiveDatatype (Closure Type) -- ^ coinductive data type
1366
| NoRecordConstructor Type -- ^ record type, but no constructor
1368
| CantSplit QName Telescope Args Args [Term]
1369
| GenericSplitError String
1372
instance Error SplitError where
1374
strMsg = GenericSplitError
1063
1377
= InternalError String
1090
1402
-- ^ Indices (variables), index expressions (with
1091
1403
-- constructors applied to reconstructed parameters),
1093
| DoesNotConstructAnElementOf QName Term -- ^ constructor, type
1405
| CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]
1406
-- ^ Datatype, constructors.
1407
| DoesNotConstructAnElementOf QName Type -- ^ constructor, type
1094
1408
| DifferentArities
1095
1409
-- ^ Varying number of arguments for a function.
1096
| WrongHidingInLHS Type
1097
1411
-- ^ The left hand side of a function definition has a hidden argument
1098
1412
-- where a non-hidden was expected.
1099
1413
| WrongHidingInLambda Type
1100
1414
-- ^ Expected a non-hidden function and found a hidden lambda.
1101
1415
| WrongHidingInApplication Type
1102
1416
-- ^ A function is applied to a hidden argument where a non-hidden was expected.
1417
| WrongNamedArgument (I.NamedArg A.Expr)
1418
-- ^ A function is applied to a hidden named argument it does not have.
1103
1419
| WrongIrrelevanceInLambda Type
1104
1420
-- ^ Expected a relevant function and found an irrelevant lambda.
1421
| HidingMismatch Hiding Hiding
1422
-- ^ The given hiding does not correspond to the expected hiding.
1423
| RelevanceMismatch Relevance Relevance
1424
-- ^ The given relevance does not correspond to the expected relevane.
1425
| ColorMismatch [Color] [Color]
1426
-- ^ The given color does not correspond to the expected color.
1105
1427
| NotInductive Term
1106
1428
-- ^ The term does not correspond to an inductive data type.
1107
1429
| UninstantiatedDotPattern A.Expr
1108
1430
| IlltypedPattern A.Pattern Type
1431
| IllformedProjectionPattern A.Pattern
1432
| CannotEliminateWithPattern (A.NamedArg A.Pattern) Type
1109
1433
| TooManyArgumentsInLHS Type
1110
1434
| WrongNumberOfConstructorArguments QName Nat Nat
1111
1435
| ShouldBeEmpty Type [Pattern]
1115
1439
-- ^ The given type should have been a pi.
1116
1440
| ShouldBeRecordType Type
1117
1441
| ShouldBeRecordPattern Pattern
1442
| NotAProjectionPattern (A.NamedArg A.Pattern)
1118
1443
| NotAProperTerm
1119
1444
| SetOmegaNotValidType
1446
-- ^ This term is not a type expression.
1120
1447
| SplitOnIrrelevant A.Pattern (Dom Type)
1121
1448
| DefinitionIsIrrelevant QName
1122
1449
| VariableIsIrrelevant Name
1123
| UnequalLevel Comparison Term Term
1450
-- | UnequalLevel Comparison Term Term -- UNUSED
1124
1451
| UnequalTerms Comparison Term Term Type
1125
1452
| UnequalTypes Comparison Type Type
1126
| UnequalTelescopes Comparison Telescope Telescope
1453
-- | UnequalTelescopes Comparison Telescope Telescope -- UNUSED
1127
1454
| UnequalRelevance Comparison Term Term
1128
1455
-- ^ The two function types have different relevance.
1129
1456
| UnequalHiding Term Term
1130
1457
-- ^ The two function types have different hiding.
1458
| UnequalColors Term Term
1459
-- ^ The two function types have different color.
1131
1460
| UnequalSorts Sort Sort
1132
1461
| UnequalBecauseOfUniverseConflict Comparison Term Term
1133
1462
| HeterogeneousEquality Term Type Term Type
1266
1600
instance Exception TCErr
1602
-----------------------------------------------------------------------------
1603
-- * The reduce monad
1604
-----------------------------------------------------------------------------
1606
-- | Environment of the reduce monad.
1607
data ReduceEnv = ReduceEnv
1608
{ redEnv :: TCEnv -- ^ Read only access to environment.
1609
, redSt :: TCState -- ^ Read only access to state (signature, metas...).
1612
mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
1613
mapRedEnv f s = s { redEnv = f (redEnv s) }
1615
mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
1616
mapRedSt f s = s { redSt = f (redSt s) }
1618
mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv
1620
mapRedEnvSt f g (ReduceEnv e s) = ReduceEnv (f e) (g s)
1622
newtype ReduceM a = ReduceM { unReduceM :: Reader ReduceEnv a }
1623
deriving (Functor, Applicative, Monad)
1625
runReduceM :: ReduceM a -> TCM a
1629
return $ runReader (unReduceM m) (ReduceEnv e s)
1631
instance MonadReader TCEnv ReduceM where
1632
ask = redEnv <$> ReduceM ask
1633
local f = ReduceM . local (mapRedEnv f) . unReduceM
1268
1635
---------------------------------------------------------------------------
1269
1636
-- * Type checking monad transformer
1270
1637
---------------------------------------------------------------------------
1272
1639
newtype TCMT m a = TCM { unTCM :: IORef TCState -> TCEnv -> m a }
1641
-- TODO: make dedicated MonadTCEnv and MonadTCState service classes
1274
1643
instance MonadIO m => MonadReader TCEnv (TCMT m) where
1275
1644
ask = TCM $ \s e -> return e
1276
1645
local f (TCM m) = TCM $ \s e -> m s (f e)
1344
1729
returnTCMT :: MonadIO m => a -> TCMT m a
1345
1730
returnTCMT = \x -> TCM $ \_ _ -> return x
1346
{-# RULES "returnTCMT"
1347
returnTCMT = \x -> TCM $ \_ _ -> return x
1349
1731
{-# INLINE returnTCMT #-}
1350
{-# SPECIALIZE INLINE returnTCMT :: a -> TCM a #-}
1352
1733
bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
1353
1734
bindTCMT = \(TCM m) k -> TCM $ \r e -> m r e >>= \x -> unTCM (k x) r e
1354
{-# RULES "bindTCMT"
1355
bindTCMT = \(TCM m) k -> TCM $ \r e ->
1356
m r e >>= \x -> unTCM (k x) r e
1358
1735
{-# INLINE bindTCMT #-}
1359
{-# SPECIALIZE INLINE bindTCMT :: TCM a -> (a -> TCM b) -> TCM b #-}
1361
1737
thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b
1362
1738
thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e >> m2 r e
1363
{-# RULES "thenTCMT"
1364
thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e >> m2 r e
1366
1739
{-# INLINE thenTCMT #-}
1367
{-# SPECIALIZE INLINE thenTCMT :: TCM a -> TCM b -> TCM b #-}
1369
1741
instance MonadIO m => Functor (TCMT m) where
1370
1742
fmap = fmapTCMT
1372
1744
fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b
1373
1745
fmapTCMT = \f (TCM m) -> TCM $ \r e -> liftM f (m r e)
1374
{-# RULES "fmapTCMT"
1375
fmapTCMT = \f (TCM m) -> TCM $ \r e -> liftM f (m r e)
1377
1746
{-# INLINE fmapTCMT #-}
1378
{-# SPECIALIZE INLINE fmapTCMT :: (a -> b) -> TCM a -> TCM b #-}
1380
1748
instance MonadIO m => Applicative (TCMT m) where
1381
1749
pure = returnTCMT
1417
1781
throwError $ TypeError s cl
1419
runTCM :: TCMT IO a -> IO (Either TCErr a)
1420
runTCM m = (Right <$> runTCM' m) `E.catch` (return . Left)
1422
runTCM' :: MonadIO m => TCMT m a -> m a
1783
-- | Running the type checking monad (most general form).
1784
{-# SPECIALIZE runTCM :: TCEnv -> TCState -> TCM a -> IO (a, TCState) #-}
1785
runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)
1787
r <- liftIO $ newIORef s
1789
s <- liftIO $ readIORef r
1792
-- | Running the type checking monad on toplevel (with initial state).
1793
runTCMTop :: TCM a -> IO (Either TCErr a)
1794
runTCMTop m = (Right <$> runTCMTop' m) `E.catch` (return . Left)
1796
runTCMTop' :: MonadIO m => TCMT m a -> m a
1424
1798
r <- liftIO $ newIORef initState
1425
1799
unTCM m r initEnv
1801
-- | 'runSafeTCM' runs a safe 'TCM' action (a 'TCM' action which cannot fail)
1802
-- in the initial environment.
1804
runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
1805
runSafeTCM m st = runTCM initEnv st m `E.catch` (\ (e :: TCErr) -> __IMPOSSIBLE__)
1806
-- runSafeTCM m st = either__IMPOSSIBLE__ return <$> do
1807
-- -- Errors must be impossible.
1427
1814
-- | Runs the given computation in a separate thread, with /a copy/ of
1428
1815
-- the current state and environment.
added
removed
src/full/Agda/TypeChecking/Monad/Base.hs
