1
1
-- {-# LANGUAGE CPP #-}
2
{-# LANGUAGE DeriveFoldable #-}
3
{-# LANGUAGE DeriveFunctor #-}
2
{-# LANGUAGE DeriveFoldable #-}
3
{-# LANGUAGE DeriveFunctor #-}
4
4
{-# LANGUAGE DeriveTraversable #-}
5
5
{-# LANGUAGE FlexibleInstances #-}
7
7
module Agda.TypeChecking.Rules.LHS.Problem where
9
import Control.Monad.Error
10
import Data.Monoid ( Monoid(mappend,mempty) )
9
import Prelude hiding (null)
11
11
import Data.Foldable
12
12
import Data.Traversable
19
19
import qualified Agda.Syntax.Abstract as A
21
21
import Agda.TypeChecking.Substitute as S
22
import Agda.TypeChecking.Pretty
22
import Agda.TypeChecking.Pretty hiding (empty)
24
import Agda.Utils.Except ( Error(noMsg, strMsg) )
25
import Agda.Utils.Null
24
26
import Agda.Utils.Permutation
26
28
type Substitution = [Maybe Term]
80
82
-- | The permutation should permute @allHoles@ of the patterns to correspond to
81
83
-- the abstract patterns in the problem.
82
type Problem = Problem' (Permutation, [I.NamedArg Pattern])
84
type Problem = Problem' (Permutation, [I.NamedArg Pattern])
83
85
type ProblemPart = Problem' ()
85
87
-- | User patterns that could not be given a type yet.
128
130
| LitFocus Literal OneHolePatterns Int Type
132
-- | Result of 'splitProblem': Determines position for the next split.
130
133
data SplitProblem
132
= Split ProblemPart [Name] (I.Arg Focus) (Abs ProblemPart)
133
-- ^ Split on constructor pattern.
134
-- The @[Name]@s give the as-bindings for the focus.
136
| SplitRest { splitProjection :: I.Arg QName, splitRestType :: Type }
137
-- ^ Split on projection pattern.
138
-- The projection could be belonging to an irrelevant record field.
135
= -- | Split on constructor pattern.
137
{ splitLPats :: ProblemPart
138
-- ^ The typed user patterns left of the split position.
139
-- Invariant: @'problemRest' == empty@.
140
, splitAsNames :: [Name]
141
-- ^ The as-bindings for the focus.
142
, splitFocus :: I.Arg Focus
143
-- ^ How to split the variable at the split position.
144
, splitRPats :: Abs ProblemPart
145
-- ^ The typed user patterns right of the split position.
148
| -- | Split on projection pattern.
150
{ splitProjection :: I.Arg QName
151
-- ^ The projection could be belonging to an irrelevant record field.
152
, splitRestType :: Type
155
-- | Put a typed pattern on the very left of a @SplitProblem@.
157
:: A.NamedArg A.Pattern -- ^ @p@ A pattern.
158
-> ArgName -- ^ @x@ The name of the argument (from its type).
159
-> I.Dom Type -- ^ @t@ Its type.
160
-> SplitProblem -- ^ The split problem, containing 'splitLPats' @ps;xs:ts@.
161
-> SplitProblem -- ^ The result, now containing 'splitLPats' @(p,ps);(x,xs):(t,ts)@.
162
consSplitProblem p x dom s@SplitRest{} = s
163
consSplitProblem p x dom s@Split{ splitLPats = ps } = s{ splitLPats = consProblem' ps }
165
consProblem' (Problem ps () tel pr) =
166
Problem (p:ps) () (ExtendTel dom $ Abs x tel) pr
183
211
noMsg = NothingToSplit
184
212
strMsg = SplitPanic
186
instance Monoid ProblemRest where
187
mempty = ProblemRest [] (defaultArg typeDontCare)
188
mappend pr (ProblemRest [] _) = pr
191
instance Monoid p => Monoid (Problem' p) where
192
mempty = Problem [] mempty EmptyTel mempty
193
Problem ps1 qs1 tel1 pr1 `mappend` Problem ps2 qs2 tel2 pr2 =
194
Problem (ps1 ++ ps2) (mappend qs1 qs2) (abstract tel1 tel2) (mappend pr1 pr2)
214
instance Null ProblemRest where
215
null = null . restPats
216
empty = ProblemRest { restPats = [], restType = defaultArg typeDontCare }
218
instance Null a => Null (Problem' a) where
219
null p = null (problemInPat p) && null (problemRest p)
220
empty = Problem empty empty empty empty
added
removed
src/full/Agda/TypeChecking/Rules/LHS/Problem.hs
