module Agda.TypeChecking.Quote where
import Control.Applicative
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
#include "../undefined.h"
import Agda.Utils.Impossible
quotingKit :: TCM ((Term -> Term), (Type -> Term))
quotingKit = do
hidden <- primHidden
instanceH <- primInstance
visible <- primVisible
relevant <- primRelevant
irrelevant <- primIrrelevant
nil <- primNil
cons <- primCons
arg <- primArgArg
var <- primAgdaTermVar
lam <- primAgdaTermLam
def <- primAgdaTermDef
con <- primAgdaTermCon
pi <- primAgdaTermPi
sort <- primAgdaTermSort
set <- primAgdaSortSet
setLit <- primAgdaSortLit
unsupportedSort <- primAgdaSortUnsupported
sucLevel <- primLevelSuc
lub <- primLevelMax
el <- primAgdaTypeEl
Con z _ <- ignoreSharing <$> primZero
Con s _ <- ignoreSharing <$> primSuc
unsupported <- primAgdaTermUnsupported
let t @@ u = apply t [defaultArg u]
quoteHiding Hidden = hidden
quoteHiding Instance = instanceH
quoteHiding NotHidden = visible
quoteRelevance Relevant = relevant
quoteRelevance Irrelevant = irrelevant
quoteRelevance NonStrict = relevant
quoteRelevance Forced = relevant
quoteRelevance UnusedArg = relevant
quoteLit (LitInt _ n) = iterate suc zero !! fromIntegral n
quoteLit _ = unsupported
quoteSortLevelTerm (Max []) = setLit @@ Lit (LitInt noRange 0)
quoteSortLevelTerm (Max [ClosedLevel n]) = setLit @@ Lit (LitInt noRange n)
quoteSortLevelTerm (Max [Plus 0 (NeutralLevel v)]) = set @@ quote v
quoteSortLevelTerm _ = unsupported
quoteSort (Type t) = quoteSortLevelTerm t
quoteSort Prop = unsupportedSort
quoteSort Inf = unsupportedSort
quoteSort DLub{} = unsupportedSort
quoteType (El s t) = el @@ quoteSort s @@ quote t
list [] = nil
list (a : as) = cons @@ a @@ list as
zero = con @@ quoteName z @@ nil
suc n = con @@ quoteName s @@ list [arg @@ visible @@ relevant @@ n]
quoteDom q (Dom h r t) = arg @@ quoteHiding h @@ quoteRelevance r @@ q t
quoteArg q (Arg h r t) = arg @@ quoteHiding h @@ quoteRelevance r @@ q t
quoteArgs ts = list (map (quoteArg quote) ts)
quote (Var n ts) = var @@ Lit (LitInt noRange $ fromIntegral n) @@ quoteArgs ts
quote (Lam h t) = lam @@ quoteHiding h @@ quote (absBody t)
quote (Def x ts) = def @@ quoteName x @@ quoteArgs ts
quote (Con x ts) = con @@ quoteName x @@ quoteArgs ts
quote (Pi t u) = pi @@ quoteDom quoteType t
@@ quoteType (absBody u)
quote (Level _) = unsupported
quote (Lit lit) = quoteLit lit
quote (Sort s) = sort @@ quoteSort s
quote (Shared p) = quote $ derefPtr p
quote MetaV{} = unsupported
quote DontCare{} = unsupported
return (quote, quoteType)
quoteName :: QName -> Term
quoteName x = Lit (LitQName noRange x)
quoteTerm :: Term -> TCM Term
quoteTerm v = ($v) . fst <$> quotingKit
quoteType :: Type -> TCM Term
quoteType v = ($v) . snd <$> quotingKit
agdaTermType :: TCM Type
agdaTermType = El (mkType 0) <$> primAgdaTerm
qNameType :: TCM Type
qNameType = El (mkType 0) <$> primQName
isCon :: QName -> TCM Term -> TCM Bool
isCon con tm = do t <- tm
case ignoreSharing t of
Con con' _ -> return (con == con')
_ -> return False
unquoteFailedGeneric :: String -> TCM a
unquoteFailedGeneric msg = typeError . GenericError $ "Unable to unquote the " ++ msg
unquoteFailed :: String -> String -> Term -> TCM a
unquoteFailed kind msg t = do doc <- prettyTCM t
unquoteFailedGeneric $ "term (" ++ show doc ++ ") of type " ++ kind ++ ".\nReason: " ++ msg ++ "."
class Unquote a where
unquote :: Term -> TCM a
unquoteH :: Unquote a => Arg Term -> TCM a
unquoteH (Arg Hidden Relevant x) = unquote x
unquoteH _ = unquoteFailedGeneric "argument. It should be `hidden'."
unquoteN :: Unquote a => Arg Term -> TCM a
unquoteN (Arg NotHidden Relevant x) = unquote x
unquoteN _ = unquoteFailedGeneric "argument. It should be `visible'"
choice :: Monad m => [(m Bool, m a)] -> m a -> m a
choice [] dflt = dflt
choice ((mb, mx) : mxs) dflt = do b <- mb
if b then mx else choice mxs dflt
instance Unquote a => Unquote (Arg a) where
unquote t = do
t <- reduce t
case ignoreSharing t of
Con c [hid,rel,x] -> do
choice
[(c `isCon` primArgArg, Arg <$> unquoteN hid <*> unquoteN rel <*> unquoteN x)]
(unquoteFailed "Arg" "arity 3 and not the `arg' constructor" t)
_ -> unquoteFailed "Arg" "not of arity 3" t
instance Unquote Integer where
unquote t = do
t <- reduce t
case ignoreSharing t of
Lit (LitInt _ n) -> return n
_ -> unquoteFailed "Integer" "not a literal integer" t
instance Unquote a => Unquote [a] where
unquote t = do
t <- reduce t
case ignoreSharing t of
Con c [x,xs] -> do
choice
[(c `isCon` primCons, (:) <$> unquoteN x <*> unquoteN xs)]
(unquoteFailed "List" "arity 2 and not the `∷' constructor" t)
Con c [] -> do
choice
[(c `isCon` primNil, return [])]
(unquoteFailed "List" "arity 0 and not the `[]' constructor" t)
_ -> unquoteFailed "List" "neither `[]' nor `∷'" t
instance Unquote Hiding where
unquote t = do
t <- reduce t
let err = unquoteFailed "Hiding" "neither `hidden' nor `visible'" t
case ignoreSharing t of
Con c [] -> do
choice
[(c `isCon` primHidden, return Hidden)
,(c `isCon` primInstance, return Instance)
,(c `isCon` primVisible, return NotHidden)]
err
Con c vs -> unquoteFailed "Hiding" "the value is a constructor, but its arity is not 0" t
_ -> err
instance Unquote Relevance where
unquote t = do
t <- reduce t
let err = unquoteFailed "Relevance" "neither `relevant' or `irrelevant'" t
case ignoreSharing t of
Con c [] -> do
choice
[(c `isCon` primRelevant, return Relevant)
,(c `isCon` primIrrelevant, return Irrelevant)]
err
Con c vs -> unquoteFailed "Relevance" "the value is a constructor, but its arity is not 0" t
_ -> err
instance Unquote QName where
unquote t = do
t <- reduce t
case ignoreSharing t of
Lit (LitQName _ x) -> return x
_ -> unquoteFailed "QName" "not a literal qname value" t
instance Unquote a => Unquote (Abs a) where
unquote t = do x <- freshNoName_
Abs (show x) <$> unquote t
instance Unquote Sort where
unquote t = do
t <- reduce t
case ignoreSharing t of
Con c [] -> do
choice
[(c `isCon` primAgdaSortUnsupported, unquoteFailed "Sort" "unsupported sort" t)]
(unquoteFailed "Sort" "arity 0 and not the `unsupported' constructor" t)
Con c [u] -> do
choice
[(c `isCon` primAgdaSortSet, Type <$> unquoteN u)
,(c `isCon` primAgdaSortLit, Type . levelMax . (:[]) . ClosedLevel <$> unquoteN u)]
(unquoteFailed "Sort" "arity 1 and not the `set' or the `lit' constructors" t)
_ -> unquoteFailed "Sort" "not of arity 0 nor 1" t
instance Unquote Level where
unquote l = Max . (:[]) . Plus 0 . UnreducedLevel <$> unquote l
instance Unquote Type where
unquote t = do
t <- reduce t
case ignoreSharing t of
Con c [s, u] -> do
choice
[(c `isCon` primAgdaTypeEl, El <$> unquoteN s <*> unquoteN u)]
(unquoteFailed "Type" "arity 2 and not the `el' constructor" t)
_ -> unquoteFailed "Type" "not of arity 2" t
instance Unquote Term where
unquote t = do
t <- reduce t
case ignoreSharing t of
Con c [] ->
choice
[(c `isCon` primAgdaTermUnsupported, unquoteFailed "Term" "unsupported term" t)]
(unquoteFailed "Term" "arity 0 and not the `unsupported' constructor" t)
Con c [x] -> do
choice
[(c `isCon` primAgdaTermSort, Sort <$> unquoteN x)]
(unquoteFailed "Term" "arity 1 and not the `sort' constructor" t)
Con c [x,y] ->
choice
[(c `isCon` primAgdaTermVar, Var <$> (fromInteger <$> unquoteN x) <*> unquoteN y)
,(c `isCon` primAgdaTermCon, Con <$> unquoteN x <*> unquoteN y)
,(c `isCon` primAgdaTermDef, Def <$> unquoteN x <*> unquoteN y)
,(c `isCon` primAgdaTermLam, Lam <$> unquoteN x <*> unquoteN y)
,(c `isCon` primAgdaTermPi, Pi <$> (domFromArg <$> unquoteN x) <*> unquoteN y)]
(unquoteFailed "Term" "arity 2 and none of Var, Con, Def, Lam, Pi" t)
Con{} -> unquoteFailed "Term" "neither arity 0 nor 1 nor 2" t
Lit{} -> unquoteFailed "Term" "unexpected literal" t
_ -> unquoteFailed "Term" "not a constructor" t