2
{-# LANGUAGE FlexibleInstances #-}
3
{-# LANGUAGE PatternGuards #-}
4
{-# LANGUAGE TypeSynonymInstances #-}
6
module Agda.TypeChecking.Unquote where
8
import Control.Applicative
9
import Control.Monad.State (evalState, get, put)
10
import Control.Monad.Writer (execWriterT, tell)
11
import Control.Monad.Trans (lift)
14
import Data.Maybe (fromMaybe)
15
import Data.Traversable (traverse)
17
import Agda.Syntax.Common
18
import Agda.Syntax.Internal as I
19
import Agda.Syntax.Literal
20
import Agda.Syntax.Position
21
import Agda.Syntax.Translation.InternalToAbstract
23
import Agda.TypeChecking.CompiledClause
24
import Agda.TypeChecking.Datatypes ( getConHead )
25
import Agda.TypeChecking.DropArgs
26
import Agda.TypeChecking.Free
27
import Agda.TypeChecking.Level
28
import Agda.TypeChecking.Monad
29
import Agda.TypeChecking.Monad.Builtin
30
import Agda.TypeChecking.Monad.Exception
31
import Agda.TypeChecking.Pretty
32
import Agda.TypeChecking.Reduce
33
import Agda.TypeChecking.Reduce.Monad
34
import Agda.TypeChecking.Substitute
36
import Agda.Utils.Except
37
import Agda.Utils.Impossible
38
import Agda.Utils.Monad ( ifM )
39
import Agda.Utils.Permutation ( Permutation(Perm) )
40
import Agda.Utils.String ( Str(Str), unStr )
41
import Agda.Utils.VarSet (VarSet)
42
import qualified Agda.Utils.VarSet as Set
44
#include "undefined.h"
46
agdaTermType :: TCM Type
47
agdaTermType = El (mkType 0) <$> primAgdaTerm
50
qNameType = El (mkType 0) <$> primQName
52
type UnquoteM = ExceptionT UnquoteError TCM
54
runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError a)
55
runUnquoteM = runExceptionT
57
isCon :: ConHead -> TCM Term -> UnquoteM Bool
58
isCon con tm = do t <- lift tm
59
case ignoreSharing t of
60
Con con' _ -> return (con == con')
63
{-unquoteFailedGeneric :: String -> UnquoteM a
64
unquoteFailedGeneric msg = typeError . GenericError $ "Unable to unquote the " ++ msg
66
unquoteFailed :: String -> String -> Term -> TCM a
67
unquoteFailed kind msg t = do doc <- prettyTCM t
68
unquoteFailedGeneric $ "term (" ++ show doc ++ ") of type " ++ kind ++ ".\nReason: " ++ msg ++ "."
71
unquote :: Term -> UnquoteM a
73
unquoteH :: Unquote a => I.Arg Term -> UnquoteM a
74
unquoteH a | isHidden a && isRelevant a =
76
unquoteH a = throwException $ BadVisibility "hidden" a
78
unquoteN :: Unquote a => I.Arg Term -> UnquoteM a
79
unquoteN a | notHidden a && isRelevant a =
81
unquoteN a = throwException $ BadVisibility "visible" a
83
choice :: Monad m => [(m Bool, m a)] -> m a -> m a
85
choice ((mb, mx) : mxs) dflt = ifM mb mx $ choice mxs dflt
87
ensureDef :: QName -> UnquoteM QName
89
i <- (theDef <$> getConstInfo x) `catchError` \_ -> return Axiom -- for recursive unquoteDecl
92
def <- lift $ prettyTCM =<< primAgdaTermDef
93
con <- lift $ prettyTCM =<< primAgdaTermCon
94
throwException $ ConInsteadOfDef x (show def) (show con)
97
ensureCon :: QName -> UnquoteM QName
99
i <- (theDef <$> getConstInfo x) `catchError` \_ -> return Axiom -- for recursive unquoteDecl
101
Constructor{} -> return x
103
def <- lift $ prettyTCM =<< primAgdaTermDef
104
con <- lift $ prettyTCM =<< primAgdaTermCon
105
throwException $ DefInsteadOfCon x (show def) (show con)
107
pickName :: Type -> String
112
Def d _ | c:_ <- show (qnameName d),
113
isAlpha c -> [toLower c]
116
instance Unquote I.ArgInfo where
119
case ignoreSharing t of
122
[(c `isCon` primArgArgInfo, ArgInfo <$> unquoteN h <*> unquoteN r <*> return [])]
124
Con c _ -> __IMPOSSIBLE__
125
_ -> throwException $ NotAConstructor "ArgInfo" t
127
instance Unquote a => Unquote (I.Arg a) where
130
case ignoreSharing t of
133
[(c `isCon` primArgArg, Arg <$> unquoteN info <*> unquoteN x)]
135
Con c _ -> __IMPOSSIBLE__
136
_ -> throwException $ NotAConstructor "Arg" t
138
-- Andreas, 2013-10-20: currently, post-fix projections are not part of the
140
instance Unquote a => Unquote (Elim' a) where
141
unquote t = Apply <$> unquote t
143
instance Unquote Integer where
146
case ignoreSharing t of
147
Lit (LitInt _ n) -> return n
148
_ -> throwException $ NotALiteral "Integer" t
150
instance Unquote Double where
153
case ignoreSharing t of
154
Lit (LitFloat _ x) -> return x
155
_ -> throwException $ NotALiteral "Float" t
157
instance Unquote Char where
160
case ignoreSharing t of
161
Lit (LitChar _ x) -> return x
162
_ -> throwException $ NotALiteral "Char" t
164
instance Unquote Str where
167
case ignoreSharing t of
168
Lit (LitString _ x) -> return (Str x)
169
_ -> throwException $ NotALiteral "String" t
171
instance Unquote a => Unquote [a] where
174
case ignoreSharing t of
177
[(c `isCon` primCons, (:) <$> unquoteN x <*> unquoteN xs)]
181
[(c `isCon` primNil, return [])]
183
Con c _ -> __IMPOSSIBLE__
184
_ -> throwException $ NotAConstructor "List" t
186
instance Unquote Hiding where
189
case ignoreSharing t of
192
[(c `isCon` primHidden, return Hidden)
193
,(c `isCon` primInstance, return Instance)
194
,(c `isCon` primVisible, return NotHidden)]
196
Con c vs -> __IMPOSSIBLE__
197
_ -> throwException $ NotAConstructor "Hiding" t
199
instance Unquote Relevance where
202
case ignoreSharing t of
205
[(c `isCon` primRelevant, return Relevant)
206
,(c `isCon` primIrrelevant, return Irrelevant)]
208
Con c vs -> __IMPOSSIBLE__
209
_ -> throwException $ NotAConstructor "Relevance" t
211
instance Unquote QName where
214
case ignoreSharing t of
215
Lit (LitQName _ x) -> return x
216
_ -> throwException $ NotALiteral "QName" t
218
instance Unquote ConHead where
219
unquote t = lift . getConHead =<< ensureCon =<< unquote t
221
instance Unquote a => Unquote (Abs a) where
222
unquote t = Abs "_" <$> unquote t
224
instance Unquote Sort where
227
case ignoreSharing t of
230
[(c `isCon` primAgdaSortUnsupported, pure $ Type $ Max [Plus 0 $ UnreducedLevel $ hackReifyToMeta])]
234
[(c `isCon` primAgdaSortSet, Type <$> unquoteN u)
235
,(c `isCon` primAgdaSortLit, Type . levelMax . (:[]) . ClosedLevel <$> unquoteN u)]
237
Con c _ -> __IMPOSSIBLE__
238
_ -> throwException $ NotAConstructor "Sort" t
240
instance Unquote Level where
241
unquote l = Max . (:[]) . Plus 0 . UnreducedLevel <$> unquote l
243
instance Unquote Type where
246
case ignoreSharing t of
249
[(c `isCon` primAgdaTypeEl, El <$> unquoteN s <*> unquoteN u)]
251
Con c _ -> __IMPOSSIBLE__
252
_ -> throwException $ NotAConstructor "Type" t
254
instance Unquote Literal where
257
case ignoreSharing t of
260
[ (c `isCon` primAgdaLitNat, LitInt noRange <$> unquoteN x)
261
, (c `isCon` primAgdaLitFloat, LitFloat noRange <$> unquoteN x)
262
, (c `isCon` primAgdaLitChar, LitChar noRange <$> unquoteN x)
263
, (c `isCon` primAgdaLitString, LitString noRange . unStr <$> unquoteN x)
264
, (c `isCon` primAgdaLitQName, LitQName noRange <$> unquoteN x) ]
266
Con c _ -> __IMPOSSIBLE__
267
_ -> throwException $ NotAConstructor "Literal" t
269
instance Unquote Term where
272
case ignoreSharing t of
275
[(c `isCon` primAgdaTermUnsupported, pure hackReifyToMeta)]
280
[ (c `isCon` primAgdaTermSort, Sort <$> unquoteN x)
281
, (c `isCon` primAgdaTermLit, Lit <$> unquoteN x) ]
286
[ (c `isCon` primAgdaTermVar, Var <$> (fromInteger <$> unquoteN x) <*> unquoteN y)
287
, (c `isCon` primAgdaTermCon, Con <$> unquoteN x <*> unquoteN y)
288
, (c `isCon` primAgdaTermDef, Def <$> (ensureDef =<< unquoteN x) <*> unquoteN y)
289
, (c `isCon` primAgdaTermLam, Lam <$> (flip setHiding defaultArgInfo <$> unquoteN x) <*> unquoteN y)
290
, (c `isCon` primAgdaTermPi, mkPi <$> (domFromArg <$> unquoteN x) <*> unquoteN y)
291
, (c `isCon` primAgdaTermExtLam, mkExtLam <$> unquoteN x <*> unquoteN y) ]
295
mkPi a (Abs _ b) = Pi a (Abs x b)
296
where x | 0 `freeIn` b = pickName (unDom a)
298
mkPi _ NoAbs{} = __IMPOSSIBLE__
300
Con{} -> __IMPOSSIBLE__
301
Lit{} -> __IMPOSSIBLE__
302
_ -> throwException $ NotAConstructor "Term" t
304
instance Unquote Pattern where
307
case ignoreSharing t of
310
[ (c `isCon` primAgdaPatVar, pure (VarP "x"))
311
, (c `isCon` primAgdaPatAbsurd, pure (VarP "()"))
312
, (c `isCon` primAgdaPatDot, pure (DotP hackReifyToMeta))
316
[ (c `isCon` primAgdaPatProj, ProjP <$> unquoteN x)
317
, (c `isCon` primAgdaPatLit, LitP <$> unquoteN x) ]
321
[ (c `isCon` primAgdaPatCon, flip ConP Nothing <$> unquoteN x <*> (map (fmap unnamed) <$> unquoteN y)) ]
323
Con c _ -> __IMPOSSIBLE__
324
_ -> throwException $ NotAConstructor "Pattern" t
326
data UnquotedFunDef = UnQFun Type [Clause]
328
instance Unquote Clause where
331
case ignoreSharing t of
334
[ (c `isCon` primAgdaClauseAbsurd, mkClause Nothing <$> unquoteN x) ]
338
[ (c `isCon` primAgdaClauseClause, checkClause =<< mkClause . Just <$> unquoteN y <*> unquoteN x) ]
340
Con c _ -> __IMPOSSIBLE__
341
_ -> throwException $ NotAConstructor "Clause" t
343
mkClause :: Maybe Term -> [I.Arg Pattern] -> I.Clause
345
Clause { clauseRange = noRange
346
, clauseTel = dummyTel n'
347
, clausePerm = Perm n vs
348
, namedClausePats = ps
349
, clauseBody = mkBody n b
350
, clauseType = Nothing }
352
ps = map (fmap unnamed) ps0
353
n = vars True ps -- with dot patterns
354
n' = vars False ps -- without dot patterns
355
dummyTel 0 = EmptyTel
356
dummyTel n = ExtendTel (defaultDom typeDontCare) (Abs "x" $ dummyTel (n - 1))
357
mkBody 0 b = maybe NoBody Body b
358
mkBody n b = Bind $ Abs "x" $ mkBody (n - 1) b
359
vars d ps = sum $ map (vars' d . namedArg) ps
360
vars' d (ConP _ _ ps) = vars d ps
362
vars' d DotP{} = if d then 1 else 0
366
vs = evalState (execWriterT $ mapM_ (computePerm . namedArg) ps) 0
367
next = do n <- get; put (n + 1); return n
369
computePerm (ConP _ _ ps) = mapM_ (computePerm . namedArg) ps
370
computePerm VarP{} = tell . (:[]) =<< next
371
computePerm DotP{} = () <$ next
372
computePerm LitP{} = return ()
373
computePerm ProjP{} = return ()
375
checkClause :: I.Clause -> UnquoteM I.Clause
376
checkClause cl@Clause{ clausePerm = Perm n vs , clauseBody = body } = do
377
let freevs = allVars $ freeVars $ fromMaybe __IMPOSSIBLE__ $ getBody body
378
propervs = Set.fromList $ map ((n-1)-) vs
379
dottedvs = Set.difference (Set.fromList [0..n-1]) propervs
380
offending = Set.intersection freevs dottedvs
381
Agda.TypeChecking.Monad.reportSDoc "tc.unquote.clause.dotvars" 30 $ vcat
382
[ text $ "checkClause "
383
, nest 2 $ text $ "free vars: " ++ show freevs
384
, nest 2 $ text $ "dotted vars: " ++ show dottedvs
385
, nest 2 $ text $ "offending vars: " ++ show offending
387
if Set.null offending
389
else throwException $ RhsUsesDottedVar (Set.toList offending) t
391
instance Unquote UnquotedFunDef where
394
case ignoreSharing t of
397
[ (c `isCon` primAgdaFunDefCon, UnQFun <$> unquoteN x <*> unquoteN y) ]
399
Con c _ -> __IMPOSSIBLE__
400
_ -> throwException $ NotAConstructor "Pattern" t
402
reifyUnquoted :: Reify a e => a -> TCM e
403
reifyUnquoted = nowReifyingUnquoted . disableDisplayForms . withShowAllArguments . reify
added
removed
src/full/Agda/TypeChecking/Unquote.hs
