1
{-# LANGUAGE CPP, TupleSections #-}
3
module Agda.TypeChecking.Rules.LHS.ProblemRest where
5
import Control.Applicative
9
import Agda.Syntax.Common
10
import Agda.Syntax.Position
11
import Agda.Syntax.Info
12
import Agda.Syntax.Internal
13
import qualified Agda.Syntax.Abstract as A
15
import Agda.TypeChecking.Monad
16
import Agda.TypeChecking.Pretty
17
import Agda.TypeChecking.Reduce
18
import Agda.TypeChecking.Telescope
19
import Agda.TypeChecking.Implicit
20
import Agda.TypeChecking.Substitute
21
import Agda.TypeChecking.Pretty
23
import Agda.TypeChecking.Rules.LHS.Problem
24
import Agda.TypeChecking.Rules.LHS.Implicit
26
import Agda.Utils.Size
27
import Agda.Utils.Permutation
29
#include "../../../undefined.h"
30
import Agda.Utils.Impossible
34
-- | Rename the variables in a telescope using the names from a given pattern
35
useNamesFromPattern :: [NamedArg A.Pattern] -> Telescope -> Telescope
36
useNamesFromPattern ps = telFromList . zipWith ren (toPats ps ++ repeat dummy) . telToList
38
dummy = A.WildP __IMPOSSIBLE__
39
ren (A.VarP x) (Dom NotHidden r (_, a)) = Dom NotHidden r (show x, a)
40
ren A.PatternSynP{} _ = __IMPOSSIBLE__ -- ensure there are no syns left
44
-- | Are there any untyped user patterns left?
45
noProblemRest :: Problem -> Bool
46
noProblemRest (Problem _ _ _ (ProblemRest ps _)) = null ps
48
-- | Get the type of clause. Only valid if 'noProblemRest'.
49
typeFromProblem :: Problem -> Type
50
typeFromProblem (Problem _ _ _ (ProblemRest _ a)) = a
52
-- | Construct an initial 'split' 'Problem' from user patterns.
53
problemFromPats :: [NamedArg A.Pattern] -- ^ The user patterns.
54
-> Type -- ^ The type the user patterns eliminate.
55
-> TCM Problem -- ^ The initial problem constructed from the user patterns.
56
problemFromPats ps a = do
57
TelV tel0' b0 <- telView a
58
-- For the initial problem, do not insert trailing implicits.
59
-- This has the effect of not including trailing hidden domains in the problem telescope.
60
-- In all later call to insertImplicitPatterns, we can then use ExpandLast.
61
ps <- insertImplicitPatterns DontExpandLast ps tel0'
62
-- unless (size tel0' >= size ps) $ typeError $ TooManyArgumentsInLHS a
63
let tel0 = useNamesFromPattern ps tel0'
64
(as, bs) = splitAt (size ps) $ telToList tel0
65
(ps1,ps2) = splitAt (size as) ps
66
gamma = telFromList as
67
b = telePi (telFromList bs) b0
68
-- now (gamma -> b) = a and |gamma| = |ps1|
69
pr = ProblemRest ps2 b
70
-- patterns ps2 eliminate type b
72
-- internal patterns start as all variables
73
ips = map (argFromDom . fmap (VarP . fst)) as
75
-- the initial problem for starting the splitting
76
problem = Problem ps1 (idP $ size ps1, ips) gamma pr
77
reportSDoc "tc.lhs.problem" 10 $
78
vcat [ text "checking lhs -- generated an initial split problem:"
80
[ text "ps =" <+> fsep (map prettyA ps)
81
, text "a =" <+> prettyTCM a
82
, text "a' =" <+> prettyTCM (telePi tel0 b0)
83
, text "a'' =" <+> prettyTCM (telePi tel0' b0)
84
, text "xs =" <+> text (show $ map (fst . unDom) as)
85
, text "tel0 =" <+> prettyTCM tel0
86
, text "b0 =" <+> prettyTCM b0
87
, text "gamma =" <+> prettyTCM gamma
88
, text "b =" <+> addCtxTel gamma (prettyTCM b)
94
todoProblemRest :: ProblemRest
95
todoProblemRest = mempty
98
-- | Try to move patterns from the problem rest into the problem.
99
-- Possible if type of problem rest has been updated to a function type.
100
updateProblemRest_ :: Problem -> TCM (Nat, Problem)
101
updateProblemRest_ p@(Problem _ _ _ (ProblemRest [] _)) = return (0, p)
102
updateProblemRest_ p@(Problem ps0 (perm0@(Perm n0 is0), qs0) tel0 (ProblemRest ps a)) = do
103
TelV tel' b0 <- telView a
105
EmptyTel -> return (0, p) -- no progress
106
ExtendTel{} -> do -- a did reduce to a pi-type
107
ps <- insertImplicitPatterns DontExpandLast ps tel'
108
let tel = useNamesFromPattern ps tel'
109
(as, bs) = splitAt (size ps) $ telToList tel
110
(ps1,ps2) = splitAt (size as) ps
111
tel1 = telFromList $ telToList tel0 ++ as
112
b = telePi (telFromList bs) b0
113
pr = ProblemRest ps2 b
114
qs1 = map (argFromDom . fmap (VarP . fst)) as
116
perm1 = liftP n perm0 -- IS: Perm (n0 + n) $ is0 ++ [n0..n0+n-1]
117
return $ (n,) $ Problem (ps0 ++ ps1) (perm1, raise n qs0 ++ qs1) tel1 pr
119
updateProblemRest :: LHSState -> TCM LHSState
120
updateProblemRest st@LHSState { lhsProblem = p } = do
121
(n, p') <- updateProblemRest_ p
122
if (n == 0) then return st else do
126
, lhsSubst = applySubst tau (lhsSubst st)
127
, lhsDPI = applySubst tau (lhsDPI st)
128
, lhsAsB = applySubst tau (lhsAsB st)
added
removed
src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
