← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, Kiwamu Okabe, Iain Lane
  • Date: 2013-04-10 11:46:43 UTC
  • mfrom: (4.1.5 experimental)
  • Revision ID: package-import@ubuntu.com-20130410114643-prunhsz59f0fhrdn
Tags: 2.3.2-1
[ Kiwamu Okabe ]
* New patch: Extend haskell-src-exts dependency and fix type miss.

[ Iain Lane ]
* [dfbca48] Imported Upstream version 2.3.2
* [7746bcc] Remove all patches — all upstream.
* [2cdb691] Update build-deps to match control file
* [868ebf4] agda-mode no longer depends on haskell-mode or GHCi.
  Remove dependency and update .el file accordingly
* [9e0ba22] Add agda-bin package here, as the separate package has been
  removed
* [75a240f] agda-mode needs to depend on agda-bin
* [d290f95] Allow Quickcheck up to 2.7. Fix haskeline build-dep.
* [79190e6] Add missing geniplate and parallel BDs

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs
8
8
 
9
9
import Agda.TypeChecking.Monad
10
10
import Agda.TypeChecking.Substitute hiding (Substitution)
 
11
import qualified Agda.TypeChecking.Substitute as S (Substitution)
11
12
import Agda.TypeChecking.Free
12
13
import Agda.TypeChecking.Pretty
13
14
import Agda.TypeChecking.Reduce
14
15
import Agda.TypeChecking.Telescope
15
16
 
16
17
import Agda.TypeChecking.Rules.LHS.Problem
 
18
-- import Agda.TypeChecking.Rules.LHS.ProblemRest
17
19
import Agda.TypeChecking.Rules.LHS.Split ( asView )
18
20
 
 
21
import Agda.Utils.List
19
22
import Agda.Utils.Permutation
20
23
import Agda.Utils.Size
21
24
 
25
28
-- | Instantiate a telescope with a substitution. Might reorder the telescope.
26
29
--   @instantiateTel (Γ : Tel)(σ : Γ --> Γ) = Γσ~@
27
30
--   Monadic only for debugging purposes.
28
 
instantiateTel :: Substitution -> Telescope -> TCM (Telescope, Permutation, [Term], [Type])
 
31
instantiateTel :: Substitution -> Telescope -> TCM (Telescope, Permutation, S.Substitution, [Dom Type])
29
32
instantiateTel s tel = liftTCM $ do
30
33
 
31
34
  tel <- normalise tel
38
41
    ]
39
42
 
40
43
  -- Shrinking permutation (removing Justs) (and its complement, and reverse)
41
 
  let ps  = Perm (size s) [ i | (i, Nothing) <- zip [0..] $ reverse s ]
42
 
      psR = reverseP ps
43
 
      psC = Perm (size s) [ i | (i, Just _)  <- zip [0..] $ reverse s ]
 
44
  let n   = size s
 
45
      {- OLD CODE, leave as documentation
 
46
      ps  = Perm n [ i | (i, Nothing) <- zip [0..] $ reverse s ]
 
47
      psR = reverseP ps
 
48
      psC = Perm n [ i | (i, Just _)  <- zip [0..] $ reverse s ]
 
49
      -}
 
50
      deal (i, Nothing) = Left i
 
51
      deal (i, Just _ ) = Right i
 
52
      (is, isC) = mapEither deal $ zip [0..] $ reverse s
 
53
      ps  = Perm n is
 
54
      psR = reverseP ps
 
55
      psC = Perm n isC
44
56
 
45
57
  reportSDoc "tc.lhs.inst" 10 $ vcat
46
58
    [ nest 2 $ text $ "ps   = " ++ show ps
57
69
  -- rho : [Tm Γσ]Γ
58
70
  let rho = mkSubst s'
59
71
 
 
72
  reportSDoc "tc.lhs.inst" 15 $ nest 2 $
 
73
    text "rho = " <+> text (show rho)
 
74
 
60
75
  -- tel1 : [Type Γ]Γ
61
76
  let tel1   = flattenTel tel
62
77
      names1 = teleNames tel
67
82
    ]
68
83
 
69
84
  -- tel2 : [Type Γσ]Γ
70
 
  let tel2 = substs rho tel1
 
85
  let tel2 = applySubst rho tel1
71
86
 
72
87
  reportSDoc "tc.lhs.inst" 15 $ nest 2 $
73
88
    text "tel2 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel2)
83
98
  p <- case reorderTel tel3 of
84
99
    Nothing -> inContext [] $ do
85
100
      xs <- mapM freshName_ names3
86
 
      addCtxs xs (Arg NotHidden Relevant prop) $ do
 
101
      addCtxs xs (Dom NotHidden Relevant prop) $ do
87
102
        err <- sep [ text "Recursive telescope in left hand side:"
88
103
                   , fsep [ parens (prettyTCM x <+> text ":" <+> prettyTCM t)
89
104
                          | (x, t) <- zip xs tel3 ]
97
112
  let rho' = renaming (reverseP p)
98
113
 
99
114
  -- tel4 : [Type Γσ~]Γσ~
100
 
  let tel4   = substs rho' (permute p tel3)
 
115
  let tel4   = applySubst rho' (permute p tel3)
101
116
      names4 = permute p names3
102
117
 
103
118
  reportSDoc "tc.lhs.inst" 15 $ nest 2 $
111
126
 
112
127
  -- remember the types of the instantiations
113
128
  -- itypes : [Type Γσ~]Γ*
114
 
  let itypes = substs rho' $ permute psC $ map unArg tel2
 
129
  let itypes = applySubst rho' $ permute psC tel2
115
130
 
116
 
  return (tel5, composeP p ps, substs rho' rho, itypes)
 
131
  return (tel5, composeP p ps, applySubst rho' rho, itypes)
117
132
  where
118
133
 
119
 
    -- Turn a Substitution ([Maybe Term]) into a substitution ([Term])
120
 
    -- (The result is an infinite list)
121
 
    mkSubst :: [Maybe Term] -> [Term]
 
134
    -- Turn a Substitution ([Maybe Term]) into a substitution (S.Substitution)
 
135
    mkSubst :: [Maybe Term] -> S.Substitution
122
136
    mkSubst s = rho 0 s'
123
 
      where s'  = s ++ repeat Nothing
124
 
            rho i (Nothing : s) = Var i [] : rho (i + 1) s
125
 
            rho i (Just u  : s) = u : rho i s
126
 
            rho _ []            = __IMPOSSIBLE__
 
137
      where s'  = s
 
138
            rho i (Nothing : s) = var i :# rho (i + 1) s
 
139
            rho i (Just u  : s) = u :# rho i s
 
140
            rho i []            = raiseS i
127
141
 
128
142
-- | Produce a nice error message when splitting failed
129
143
nothingToSplitError :: Problem -> TCM a
130
 
nothingToSplitError (Problem ps _ tel) = splitError ps tel
 
144
nothingToSplitError (Problem ps _ tel pr) = splitError ps tel
131
145
  where
132
146
    splitError []       EmptyTel    = __IMPOSSIBLE__
133
147
    splitError (_:_)    EmptyTel    = __IMPOSSIBLE__
134
148
    splitError []       ExtendTel{} = __IMPOSSIBLE__
135
149
    splitError (p : ps) (ExtendTel a tel)
136
 
      | isBad p   = traceCall (CheckPattern (strip p) EmptyTel (unArg a)) $ case strip p of
 
150
      | isBad p   = traceCall (CheckPattern (strip p) EmptyTel (unDom a)) $ case strip p of
137
151
          A.DotP _ e -> typeError $ UninstantiatedDotPattern e
138
 
          p          -> typeError $ IlltypedPattern p (unArg a)
 
152
          p          -> typeError $ IlltypedPattern p (unDom a)
139
153
      | otherwise = underAbstraction a tel $ \tel -> splitError ps tel
140
154
      where
141
 
        strip = snd . asView . namedThing . unArg
 
155
        strip = snd . asView . namedArg
142
156
        isBad p = case strip p of
143
157
          A.DotP _ _   -> True
144
158
          A.ConP _ _ _ -> True