← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Quote.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Quote.hs
1
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE FlexibleInstances #-}
 
3
{-# LANGUAGE TypeSynonymInstances #-}
2
4
 
3
5
module Agda.TypeChecking.Quote where
4
6
 
5
7
import Control.Applicative
6
8
 
 
9
import Data.Maybe (fromMaybe)
 
10
 
7
11
import Agda.Syntax.Position
8
12
import Agda.Syntax.Literal
9
 
import Agda.Syntax.Internal
 
13
import Agda.Syntax.Internal as I
10
14
import Agda.Syntax.Common
11
15
 
 
16
import {-# SOURCE #-} Agda.TypeChecking.Datatypes
12
17
import Agda.TypeChecking.Monad
13
18
import Agda.TypeChecking.Monad.Builtin
14
19
import Agda.TypeChecking.Reduce
15
20
import Agda.TypeChecking.Pretty
16
21
import Agda.TypeChecking.Substitute
17
22
 
 
23
import Agda.Utils.Monad
 
24
 
18
25
#include "../undefined.h"
19
26
import Agda.Utils.Impossible
20
27
 
28
35
  nil <- primNil
29
36
  cons <- primCons
30
37
  arg <- primArgArg
 
38
  arginfo <- primArgArgInfo
31
39
  var <- primAgdaTermVar
32
40
  lam <- primAgdaTermLam
33
41
  def <- primAgdaTermDef
52
60
      quoteRelevance NonStrict  = relevant
53
61
      quoteRelevance Forced     = relevant
54
62
      quoteRelevance UnusedArg  = relevant
 
63
      quoteColors _ = nil -- TODO guilhem
 
64
      quoteArgInfo (ArgInfo h r cs) = arginfo @@ quoteHiding h
 
65
                                              @@ quoteRelevance r
 
66
                                --              @@ quoteColors cs
55
67
      quoteLit (LitInt   _ n)   = iterate suc zero !! fromIntegral n
56
68
      quoteLit _                = unsupported
57
69
      -- We keep no ranges in the quoted term, so the equality on terms
59
71
      quoteSortLevelTerm (Max [])              = setLit @@ Lit (LitInt noRange 0)
60
72
      quoteSortLevelTerm (Max [ClosedLevel n]) = setLit @@ Lit (LitInt noRange n)
61
73
      quoteSortLevelTerm (Max [Plus 0 (NeutralLevel v)]) = set @@ quote v
62
 
      quoteSortLevelTerm _                     = unsupported
 
74
      quoteSortLevelTerm _                     = unsupportedSort
63
75
      quoteSort (Type t)    = quoteSortLevelTerm t
64
76
      quoteSort Prop        = unsupportedSort
65
77
      quoteSort Inf         = unsupportedSort
67
79
      quoteType (El s t) = el @@ quoteSort s @@ quote t
68
80
      list [] = nil
69
81
      list (a : as) = cons @@ a @@ list as
70
 
      zero = con @@ quoteName z @@ nil
71
 
      suc n = con @@ quoteName s @@ list [arg @@ visible @@ relevant @@ n]
72
 
      quoteDom q (Dom h r t) = arg @@ quoteHiding h @@ quoteRelevance r @@ q t
73
 
      quoteArg q (Arg h r t) = arg @@ quoteHiding h @@ quoteRelevance r @@ q t
 
82
      zero = con @@ quoteConName z @@ nil
 
83
      suc n = con @@ quoteConName s @@ list [arg @@ quoteArgInfo defaultArgInfo @@ n]
 
84
      quoteDom q (Dom info t) = arg @@ quoteArgInfo info @@ q t
 
85
      quoteArg q (Arg info t) = arg @@ quoteArgInfo info @@ q t
74
86
      quoteArgs ts = list (map (quoteArg quote) ts)
75
 
      quote (Var n ts) = var @@ Lit (LitInt noRange $ fromIntegral n) @@ quoteArgs ts
76
 
      quote (Lam h t) = lam @@ quoteHiding h @@ quote (absBody t)
77
 
      quote (Def x ts) = def @@ quoteName x @@ quoteArgs ts
78
 
      quote (Con x ts) = con @@ quoteName x @@ quoteArgs ts
79
 
      quote (Pi t u) = pi @@ quoteDom quoteType t
80
 
                          @@ quoteType (absBody u)
81
 
      quote (Level _) = unsupported
82
 
      quote (Lit lit) = quoteLit lit
83
 
      quote (Sort s)  = sort @@ quoteSort s
84
 
      quote (Shared p) = quote $ derefPtr p
85
 
      quote MetaV{}   = unsupported
86
 
      quote DontCare{} = unsupported -- could be exposed at some point but we have to take care
 
87
      quote v =
 
88
        case unSpine v of
 
89
          (Var n es)   ->
 
90
             let ts = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
 
91
             in  var @@ Lit (LitInt noRange $ fromIntegral n) @@ quoteArgs ts
 
92
          (Lam info t) -> lam @@ quoteHiding (getHiding info) @@ quote (absBody t)
 
93
          (Def x es)   ->
 
94
             let ts = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
 
95
             in  def @@ quoteName x @@ quoteArgs ts
 
96
          (Con x ts)   -> con @@ quoteConName x @@ quoteArgs ts
 
97
          (Pi t u)     -> pi @@ quoteDom quoteType t
 
98
                        @@ quoteType (absBody u)
 
99
          (Level _)    -> unsupported
 
100
          (Lit lit)    -> quoteLit lit
 
101
          (Sort s)     -> sort @@ quoteSort s
 
102
          (Shared p)   -> quote $ derefPtr p
 
103
          MetaV{}      -> unsupported
 
104
          DontCare{}   -> unsupported -- could be exposed at some point but we have to take care
87
105
  return (quote, quoteType)
88
106
 
89
107
quoteName :: QName -> Term
90
108
quoteName x = Lit (LitQName noRange x)
91
109
 
 
110
quoteConName :: ConHead -> Term
 
111
quoteConName = quoteName . conName
 
112
 
92
113
quoteTerm :: Term -> TCM Term
93
114
quoteTerm v = ($v) . fst <$> quotingKit
94
115
 
101
122
qNameType :: TCM Type
102
123
qNameType = El (mkType 0) <$> primQName
103
124
 
104
 
isCon :: QName -> TCM Term -> TCM Bool
 
125
isCon :: ConHead -> TCM Term -> TCM Bool
105
126
isCon con tm = do t <- tm
106
127
                  case ignoreSharing t of
107
128
                    Con con' _ -> return (con == con')
117
138
class Unquote a where
118
139
  unquote :: Term -> TCM a
119
140
 
120
 
unquoteH :: Unquote a => Arg Term -> TCM a
121
 
unquoteH (Arg Hidden Relevant x) = unquote x
122
 
unquoteH _                       = unquoteFailedGeneric "argument. It should be `hidden'."
 
141
unquoteH :: Unquote a => I.Arg Term -> TCM a
 
142
unquoteH a | isHidden a && isRelevant a =
 
143
    unquote $ unArg a
 
144
unquoteH _ = unquoteFailedGeneric "argument. It should be `hidden'."
123
145
 
124
 
unquoteN :: Unquote a => Arg Term -> TCM a
125
 
unquoteN (Arg NotHidden Relevant x) = unquote x
126
 
unquoteN _                          = unquoteFailedGeneric "argument. It should be `visible'"
 
146
unquoteN :: Unquote a => I.Arg Term -> TCM a
 
147
unquoteN a | notHidden a && isRelevant a =
 
148
    unquote $ unArg a
 
149
unquoteN _ = unquoteFailedGeneric "argument. It should be `visible'"
127
150
 
128
151
choice :: Monad m => [(m Bool, m a)] -> m a -> m a
129
152
choice [] dflt = dflt
130
 
choice ((mb, mx) : mxs) dflt = do b <- mb
131
 
                                  if b then mx else choice mxs dflt
132
 
 
133
 
instance Unquote a => Unquote (Arg a) where
134
 
  unquote t = do
135
 
    t <- reduce t
136
 
    case ignoreSharing t of
137
 
      Con c [hid,rel,x] -> do
138
 
        choice
139
 
          [(c `isCon` primArgArg, Arg <$> unquoteN hid <*> unquoteN rel <*> unquoteN x)]
140
 
          (unquoteFailed "Arg" "arity 3 and not the `arg' constructor" t)
141
 
      _ -> unquoteFailed "Arg" "not of arity 3" t
 
153
choice ((mb, mx) : mxs) dflt = ifM mb mx $ choice mxs dflt
 
154
 
 
155
instance Unquote I.ArgInfo where
 
156
  unquote t = do
 
157
    t <- reduce t
 
158
    case ignoreSharing t of
 
159
      Con c [h,r] -> do
 
160
        choice
 
161
          [(c `isCon` primArgArgInfo, ArgInfo <$> unquoteN h <*> unquoteN r <*> return [])]
 
162
          (unquoteFailed "ArgInfo" "arity 2 and not the `arginfo' constructor" t)
 
163
      _ -> unquoteFailed "ArgInfo" "not of arity 2" t
 
164
 
 
165
instance Unquote a => Unquote (I.Arg a) where
 
166
  unquote t = do
 
167
    t <- reduce t
 
168
    case ignoreSharing t of
 
169
      Con c [info,x] -> do
 
170
        choice
 
171
          [(c `isCon` primArgArg, Arg <$> unquoteN info <*> unquoteN x)]
 
172
          (unquoteFailed "Arg" "arity 2 and not the `arg' constructor" t)
 
173
      _ -> unquoteFailed "Arg" "not of arity 2" t
 
174
 
 
175
-- Andreas, 2013-10-20: currently, post-fix projections are not part of the
 
176
-- quoted syntax.
 
177
instance Unquote a => Unquote (Elim' a) where
 
178
  unquote t = Apply <$> unquote t
142
179
 
143
180
instance Unquote Integer where
144
181
  unquote t = do
195
232
      Lit (LitQName _ x) -> return x
196
233
      _                  -> unquoteFailed "QName" "not a literal qname value" t
197
234
 
 
235
instance Unquote ConHead where
 
236
  unquote t = getConHead =<< unquote t
 
237
 
198
238
instance Unquote a => Unquote (Abs a) where
199
 
  unquote t = do x <- freshNoName_
200
 
                 Abs (show x) <$> unquote t
 
239
  unquote t = do x <- freshNoName_ -- Andreas, 2014-07-11 This is pointless, as it does NOT generate a name suggestion.
 
240
                 Abs (nameToArgName x) <$> unquote t
201
241
 
202
242
instance Unquote Sort where
203
243
  unquote t = do
246
286
          [(c `isCon` primAgdaTermVar, Var <$> (fromInteger <$> unquoteN x) <*> unquoteN y)
247
287
          ,(c `isCon` primAgdaTermCon, Con <$> unquoteN x <*> unquoteN y)
248
288
          ,(c `isCon` primAgdaTermDef, Def <$> unquoteN x <*> unquoteN y)
249
 
          ,(c `isCon` primAgdaTermLam, Lam <$> unquoteN x <*> unquoteN y)
 
289
          ,(c `isCon` primAgdaTermLam, Lam <$> (flip setHiding defaultArgInfo <$> unquoteN x) <*> unquoteN y)
250
290
          ,(c `isCon` primAgdaTermPi,  Pi  <$> (domFromArg <$> unquoteN x) <*> unquoteN y)]
251
291
          (unquoteFailed "Term" "arity 2 and none of Var, Con, Def, Lam, Pi" t)
252
292