3
module Agda.TypeChecking.Rules.LHS.Instantiate where
5
import Agda.Syntax.Common
6
import Agda.Syntax.Internal
7
import qualified Agda.Syntax.Abstract as A
9
import Agda.TypeChecking.Monad
10
import Agda.TypeChecking.Substitute
11
import Agda.TypeChecking.Free
12
import Agda.TypeChecking.Pretty
13
import Agda.TypeChecking.Reduce
14
import Agda.TypeChecking.Telescope
16
import Agda.TypeChecking.Rules.LHS.Problem
17
import Agda.TypeChecking.Rules.LHS.Split ( asView )
19
import Agda.Utils.Permutation
20
import Agda.Utils.Size
22
#include "../../../undefined.h"
23
import Agda.Utils.Impossible
25
-- | Instantiate a telescope with a substitution. Might reorder the telescope.
26
-- @instantiateTel (Γ : Tel)(σ : Γ --> Γ) = Γσ~@
27
-- Monadic only for debugging purposes.
28
instantiateTel :: MonadTCM tcm => Substitution -> Telescope -> tcm (Telescope, Permutation, [Term], [Type])
29
instantiateTel s tel = liftTCM $ do
31
reportSDoc "tc.lhs.inst" 10 $ sep
32
[ text "instantiateTel "
33
, nest 2 $ fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) s
34
, nest 2 $ prettyTCM tel
37
-- Shrinking permutation (removing Justs) (and its complement, and reverse)
38
let ps = Perm (size s) [ i | (i, Nothing) <- zip [0..] $ reverse s ]
40
psC = Perm (size s) [ i | (i, Just _) <- zip [0..] $ reverse s ]
42
reportS "tc.lhs.inst" 10 $ unlines
44
, "psR = " ++ show psR
45
, "psC = " ++ show psC
48
-- s' : Substitution Γσ
51
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
52
text "s' =" <+> fsep (punctuate comma $ map (maybe (text "_") prettyTCM) s')
58
let tel1 = flattenTel tel
59
names1 = teleNames tel
61
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
62
text "tel1 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel1)
65
let tel2 = substs rho tel1
67
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
68
text "tel2 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel2)
71
tel3 <- instantiateFull $ permute ps tel2
72
let names3 = permute ps names1
74
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
75
text "tel3 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel3)
77
-- p : Permutation (Γσ -> Γσ~)
78
let p = reorderTel tel3
80
reportSLn "tc.lhs.inst" 10 $ "p = " ++ show p
82
-- rho' : [Term Γσ~]Γσ
83
let rho' = renaming (reverseP p)
85
-- tel4 : [Type Γσ~]Γσ~
86
let tel4 = substs rho' (permute p tel3)
87
names4 = permute p names3
89
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
90
text "tel4 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel4)
93
let tel5 = unflattenTel names4 tel4
95
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
96
text "tel5 =" <+> prettyTCM tel5
98
-- remember the types of the instantiations
99
-- itypes : [Type Γσ~]Γ*
100
let itypes = substs rho' $ permute psC $ map unArg tel2
102
return (tel5, composeP p ps, substs rho' rho, itypes)
105
-- Turn a Substitution ([Maybe Term]) into a substitution ([Term])
106
-- (The result is an infinite list)
107
mkSubst :: [Maybe Term] -> [Term]
109
where s' = s ++ repeat Nothing
110
rho i (Nothing : s) = Var i [] : rho (i + 1) s
111
rho i (Just u : s) = u : rho i s
112
rho _ [] = __IMPOSSIBLE__
114
-- | Produce a nice error message when splitting failed
115
nothingToSplitError :: Problem -> TCM a
116
nothingToSplitError (Problem ps _ tel) = splitError ps tel
118
splitError [] EmptyTel = __IMPOSSIBLE__
119
splitError (_:_) EmptyTel = __IMPOSSIBLE__
120
splitError [] ExtendTel{} = __IMPOSSIBLE__
121
splitError (p : ps) (ExtendTel a tel)
122
| isBad p = traceCall (CheckPattern (strip p) EmptyTel (unArg a)) $ case strip p of
123
A.DotP _ e -> typeError $ UninstantiatedDotPattern e
124
p -> typeError $ IlltypedPattern p (unArg a)
125
| otherwise = underAbstraction a tel $ \tel -> splitError ps tel
127
strip = snd . asView . namedThing . unArg
128
isBad p = case strip p of
added
removed
src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs
