{-|
Module      : Idris.Reflection
Description : Code related to Idris's reflection system. This module contains quoters and unquoters along with some supporting datatypes.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE CPP, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
module Idris.Reflection (RConstructorDefn(..), RDataDefn(..),RFunArg(..),
                         RFunClause(..), RFunDefn(..), RTyDecl(..),
                         buildDatatypes, buildFunDefns, envTupleType, fromTTMaybe,
                         getArgs, mkList, rawList, rawPair, rawPairTy, reflect,
                         reflectArg, reflectDatatype, reflectEnv, reflectErr,
                         reflectFC, reflectFixity, reflectFunDefn, reflectList,
                         reflectName, reflectNameType, reflectRaw,
                         reflectRawQuotePattern, reflectRawQuote, reflectTTQuote,
                         reflectTTQuotePattern, reflm, reify, reifyBool, reifyEnv,
                         reifyFunDefn, reifyList, reifyRDataDefn, reifyRaw,
                         reifyReportPart, reifyReportParts, reifyTT, reifyTTName,
                         reifyTyDecl, rFunArgToPArg, tacN
                         ) where

import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
                             movelast, runElab, solve)
import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact,
                            lookupTyExact)
import Idris.Core.TT

import Idris.AbsSyntaxTree (ArgOpt(..), ElabD, Fixity(..), IState(idris_datatypes, idris_implicits, idris_patdefs, tt_ctxt),
                            PArg, PArg'(..), PTactic, PTactic'(..), PTerm(..),
                            initEState, pairCon, pairTy)
import Idris.Delaborate (delab)

import Control.Monad (liftM, liftM2, liftM4)
import Control.Monad.State.Strict (lift)
import Data.List (findIndex, (\\))
import Data.Maybe (catMaybes)
import qualified Data.Text as T

data RErasure = RErased | RNotErased deriving Int -> RErasure -> ShowS
[RErasure] -> ShowS
RErasure -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RErasure] -> ShowS
$cshowList :: [RErasure] -> ShowS
show :: RErasure -> String
$cshow :: RErasure -> String
showsPrec :: Int -> RErasure -> ShowS
$cshowsPrec :: Int -> RErasure -> ShowS
Show

data RPlicity = RExplicit | RImplicit | RConstraint deriving Int -> RPlicity -> ShowS
[RPlicity] -> ShowS
RPlicity -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RPlicity] -> ShowS
$cshowList :: [RPlicity] -> ShowS
show :: RPlicity -> String
$cshow :: RPlicity -> String
showsPrec :: Int -> RPlicity -> ShowS
$cshowsPrec :: Int -> RPlicity -> ShowS
Show

data RFunArg = RFunArg { RFunArg -> Name
argName    :: Name
                       , RFunArg -> Raw
argTy      :: Raw
                       , RFunArg -> RPlicity
argPlicity :: RPlicity
                       , RFunArg -> RErasure
erasure    :: RErasure
                       }
  deriving Int -> RFunArg -> ShowS
[RFunArg] -> ShowS
RFunArg -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RFunArg] -> ShowS
$cshowList :: [RFunArg] -> ShowS
show :: RFunArg -> String
$cshow :: RFunArg -> String
showsPrec :: Int -> RFunArg -> ShowS
$cshowsPrec :: Int -> RFunArg -> ShowS
Show

data RTyDecl = RDeclare Name [RFunArg] Raw deriving Int -> RTyDecl -> ShowS
[RTyDecl] -> ShowS
RTyDecl -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RTyDecl] -> ShowS
$cshowList :: [RTyDecl] -> ShowS
show :: RTyDecl -> String
$cshow :: RTyDecl -> String
showsPrec :: Int -> RTyDecl -> ShowS
$cshowsPrec :: Int -> RTyDecl -> ShowS
Show

data RTyConArg = RParameter RFunArg
               | RIndex     RFunArg
  deriving Int -> RTyConArg -> ShowS
[RTyConArg] -> ShowS
RTyConArg -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RTyConArg] -> ShowS
$cshowList :: [RTyConArg] -> ShowS
show :: RTyConArg -> String
$cshow :: RTyConArg -> String
showsPrec :: Int -> RTyConArg -> ShowS
$cshowsPrec :: Int -> RTyConArg -> ShowS
Show

data RCtorArg = RCtorParameter RFunArg | RCtorField RFunArg deriving Int -> RCtorArg -> ShowS
[RCtorArg] -> ShowS
RCtorArg -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RCtorArg] -> ShowS
$cshowList :: [RCtorArg] -> ShowS
show :: RCtorArg -> String
$cshow :: RCtorArg -> String
showsPrec :: Int -> RCtorArg -> ShowS
$cshowsPrec :: Int -> RCtorArg -> ShowS
Show

data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RCtorArg], Raw)] deriving Int -> RDatatype -> ShowS
[RDatatype] -> ShowS
RDatatype -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RDatatype] -> ShowS
$cshowList :: [RDatatype] -> ShowS
show :: RDatatype -> String
$cshow :: RDatatype -> String
showsPrec :: Int -> RDatatype -> ShowS
$cshowsPrec :: Int -> RDatatype -> ShowS
Show

data RConstructorDefn = RConstructor Name [RFunArg] Raw

data RDataDefn = RDefineDatatype Name [RConstructorDefn]

rArgOpts :: RErasure -> [ArgOpt]
rArgOpts :: RErasure -> [ArgOpt]
rArgOpts RErasure
RErased = [ArgOpt
InaccessibleArg]
rArgOpts RErasure
_ = []

rFunArgToPArg :: RFunArg -> PArg
rFunArgToPArg :: RFunArg -> PArg
rFunArgToPArg (RFunArg Name
n Raw
_ RPlicity
RExplicit RErasure
e) = forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
0 (RErasure -> [ArgOpt]
rArgOpts RErasure
e) Name
n PTerm
Placeholder
rFunArgToPArg (RFunArg Name
n Raw
_ RPlicity
RImplicit RErasure
e) = forall t. Int -> Bool -> [ArgOpt] -> Name -> t -> PArg' t
PImp Int
0 Bool
False (RErasure -> [ArgOpt]
rArgOpts RErasure
e) Name
n PTerm
Placeholder
rFunArgToPArg (RFunArg Name
n Raw
_ RPlicity
RConstraint RErasure
e) = forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PConstraint Int
0 (RErasure -> [ArgOpt]
rArgOpts RErasure
e) Name
n PTerm
Placeholder

data RFunClause a = RMkFunClause a a
                  | RMkImpossibleClause a
                  deriving Int -> RFunClause a -> ShowS
forall a. Show a => Int -> RFunClause a -> ShowS
forall a. Show a => [RFunClause a] -> ShowS
forall a. Show a => RFunClause a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RFunClause a] -> ShowS
$cshowList :: forall a. Show a => [RFunClause a] -> ShowS
show :: RFunClause a -> String
$cshow :: forall a. Show a => RFunClause a -> String
showsPrec :: Int -> RFunClause a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> RFunClause a -> ShowS
Show

data RFunDefn a = RDefineFun Name [RFunClause a] deriving Int -> RFunDefn a -> ShowS
forall a. Show a => Int -> RFunDefn a -> ShowS
forall a. Show a => [RFunDefn a] -> ShowS
forall a. Show a => RFunDefn a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RFunDefn a] -> ShowS
$cshowList :: forall a. Show a => [RFunDefn a] -> ShowS
show :: RFunDefn a -> String
$cshow :: forall a. Show a => RFunDefn a -> String
showsPrec :: Int -> RFunDefn a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> RFunDefn a -> ShowS
Show

-- | Prefix a name with the "Language.Reflection" namespace
reflm :: String -> Name
reflm :: String -> Name
reflm String
n = Name -> [String] -> Name
sNS (String -> Name
sUN String
n) [String
"Reflection", String
"Language"]

-- | Prefix a name with the "Language.Reflection.Elab" namespace
tacN :: String -> Name
tacN :: String -> Name
tacN String
str = Name -> [String] -> Name
sNS (String -> Name
sUN String
str) [String
"Elab", String
"Reflection", String
"Language"]

-- | Reify tactics from their reflected representation
reify :: IState -> Term -> ElabD PTactic
reify :: IState -> Term -> ElabD PTactic
reify IState
_ (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Intros" = forall (m :: * -> *) a. Monad m => a -> m a
return forall t. PTactic' t
Intros
reify IState
_ (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Trivial" = forall (m :: * -> *) a. Monad m => a -> m a
return forall t. PTactic' t
Trivial
reify IState
_ (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Implementation" = forall (m :: * -> *) a. Monad m => a -> m a
return forall t. PTactic' t
TCImplementation
reify IState
_ (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Solve" = forall (m :: * -> *) a. Monad m => a -> m a
return forall t. PTactic' t
Solve
reify IState
_ (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Compute" = forall (m :: * -> *) a. Monad m => a -> m a
return forall t. PTactic' t
Compute
reify IState
_ (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Skip" = forall (m :: * -> *) a. Monad m => a -> m a
return forall t. PTactic' t
Skip
reify IState
_ (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"SourceFC" = forall (m :: * -> *) a. Monad m => a -> m a
return forall t. PTactic' t
SourceFC
reify IState
_ (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Unfocus" = forall (m :: * -> *) a. Monad m => a -> m a
return forall t. PTactic' t
Unfocus
reify IState
ist t :: Term
t@(App AppStatus Name
_ Term
_ Term
_)
          | (P NameType
_ Name
f Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t = IState -> Name -> [Term] -> ElabD PTactic
reifyApp IState
ist Name
f [Term]
args
reify IState
_ Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown tactic " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)

reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
reifyApp IState
ist Name
t [Term
l, Term
r] | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Try" = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall t. PTactic' t -> PTactic' t -> PTactic' t
Try (IState -> Term -> ElabD PTactic
reify IState
ist Term
l) (IState -> Term -> ElabD PTactic
reify IState
ist Term
r)
reifyApp IState
_ Name
t [Constant (I Int
i)]
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Search" = forall (m :: * -> *) a. Monad m => a -> m a
return (forall t.
Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic' t
ProofSearch Bool
True Bool
True Int
i forall a. Maybe a
Nothing [] [])
reifyApp IState
_ Name
t [Term
x]
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Refine" = do Name
n <- Term -> ElabD Name
reifyTTName Term
x
                                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> [Bool] -> PTactic' t
Refine Name
n []
reifyApp IState
ist Name
t [Term
n, Term
ty] | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Claim" = do Name
n' <- Term -> ElabD Name
reifyTTName Term
n
                                                 Term
goal <- Term -> ElabD Term
reifyTT Term
ty
                                                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> t -> PTactic' t
Claim Name
n' (IState -> Term -> PTerm
delab IState
ist Term
goal)
reifyApp IState
ist Name
t [Term
l, Term
r] | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Seq" = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall t. PTactic' t -> PTactic' t -> PTactic' t
TSeq (IState -> Term -> ElabD PTactic
reify IState
ist Term
l) (IState -> Term -> ElabD PTactic
reify IState
ist Term
r)
reifyApp IState
ist Name
t [Constant (Str String
n), Term
x]
             | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"GoalType" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. String -> PTactic' t -> PTactic' t
GoalType String
n) (IState -> Term -> ElabD PTactic
reify IState
ist Term
x)
reifyApp IState
_ Name
t [Term
n] | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Intro" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. [Name] -> PTactic' t
Intro forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[])) (Term -> ElabD Name
reifyTTName Term
n)
reifyApp IState
ist Name
t [Term
t']
             | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ApplyTactic" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. t -> PTactic' t
ApplyTactic forall b c a. (b -> c) -> (a -> b) -> a -> c
. IState -> Term -> PTerm
delab IState
ist) (Term -> ElabD Term
reifyTT Term
t')
reifyApp IState
ist Name
t [Term
t']
             | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Reflect" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. t -> PTactic' t
Reflect forall b c a. (b -> c) -> (a -> b) -> a -> c
. IState -> Term -> PTerm
delab IState
ist) (Term -> ElabD Term
reifyTT Term
t')
reifyApp IState
ist Name
t [Term
t']
             | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ByReflection" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. t -> PTactic' t
ByReflection forall b c a. (b -> c) -> (a -> b) -> a -> c
. IState -> Term -> PTerm
delab IState
ist) (Term -> ElabD Term
reifyTT Term
t')
reifyApp IState
_ Name
t [Term
t']
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Fill" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. t -> PTactic' t
Fill forall b c a. (b -> c) -> (a -> b) -> a -> c
. Raw -> PTerm
PQuote) (Term -> ElabD Raw
reifyRaw Term
t')
reifyApp IState
ist Name
t [Term
t']
             | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Exact" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. t -> PTactic' t
Exact forall b c a. (b -> c) -> (a -> b) -> a -> c
. IState -> Term -> PTerm
delab IState
ist) (Term -> ElabD Term
reifyTT Term
t')
reifyApp IState
ist Name
t [Term
x]
             | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Focus" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall t. Name -> PTactic' t
Focus (Term -> ElabD Name
reifyTTName Term
x)
reifyApp IState
ist Name
t [Term
t']
             | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Rewrite" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall t. t -> PTactic' t
Rewrite forall b c a. (b -> c) -> (a -> b) -> a -> c
. IState -> Term -> PTerm
delab IState
ist) (Term -> ElabD Term
reifyTT Term
t')
reifyApp IState
ist Name
t [Term
n, Term
t']
             | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"LetTac" = do Name
n'  <- Term -> ElabD Name
reifyTTName Term
n
                                        Term
t'' <- Term -> ElabD Term
reifyTT Term
t'
                                        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> t -> PTactic' t
LetTac Name
n' (IState -> Term -> PTerm
delab IState
ist Term
t')
reifyApp IState
ist Name
t [Term
n, Term
tt', Term
t']
             | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"LetTacTy" = do Name
n'   <- Term -> ElabD Name
reifyTTName Term
n
                                          Term
tt'' <- Term -> ElabD Term
reifyTT Term
tt'
                                          Term
t''  <- Term -> ElabD Term
reifyTT Term
t'
                                          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> t -> t -> PTactic' t
LetTacTy Name
n' (IState -> Term -> PTerm
delab IState
ist Term
tt'') (IState -> Term -> PTerm
delab IState
ist Term
t'')
reifyApp IState
ist Name
t [Term
errs]
             | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Fail" = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. [ErrorReportPart] -> PTactic' t
TFail (Term -> ElabD [ErrorReportPart]
reifyReportParts Term
errs)
reifyApp IState
_ Name
f [Term]
args = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown tactic " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name
f, [Term]
args)) -- shouldn't happen

reifyBool :: Term -> ElabD Bool
reifyBool :: Term -> ElabD Bool
reifyBool (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN String
"True") [String
"Bool", String
"Prelude"] = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                    | Name
n forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN String
"False") [String
"Bool", String
"Prelude"] = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
reifyBool Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Not a Boolean: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm

reifyInt :: Term -> ElabD Int
reifyInt :: Term -> ElabD Int
reifyInt (Constant (I Int
i)) = forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
reifyInt Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Not an Int: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm

reifyPair :: (Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyPair :: forall a b.
(Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyPair Term -> ElabD a
left Term -> ElabD b
right (App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (P NameType
_ Name
n Term
_) Term
_) Term
_) Term
x) Term
y)
  | Name
n forall a. Eq a => a -> a -> Bool
== Name
pairCon = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (Term -> ElabD a
left Term
x) (Term -> ElabD b
right Term
y)
reifyPair Term -> ElabD a
left Term -> ElabD b
right Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Not a pair: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm

reifyList :: (Term -> ElabD a) -> Term -> ElabD [a]
reifyList :: forall a. (Term -> ElabD a) -> Term -> ElabD [a]
reifyList Term -> ElabD a
getElt Term
lst =
  case Term -> Maybe [Term]
unList Term
lst of
    Maybe [Term]
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Couldn't reify a list"
    Just [Term]
xs -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> ElabD a
getElt [Term]
xs

reifyReportParts :: Term -> ElabD [ErrorReportPart]
reifyReportParts :: Term -> ElabD [ErrorReportPart]
reifyReportParts Term
errs =
  case Term -> Maybe [Term]
unList Term
errs of
    Maybe [Term]
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Failed to reify errors"
    Just [Term]
errs' ->
      let parts :: Either Err [ErrorReportPart]
parts = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> Either Err ErrorReportPart
reifyReportPart [Term]
errs' in
      case Either Err [ErrorReportPart]
parts of
        Left Err
err -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify \"Fail\" tactic - " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Err
err
        Right [ErrorReportPart]
errs'' ->
          forall (m :: * -> *) a. Monad m => a -> m a
return [ErrorReportPart]
errs''

-- | Reify terms from their reflected representation
reifyTT :: Term -> ElabD Term
reifyTT :: Term -> ElabD Term
reifyTT t :: Term
t@(App AppStatus Name
_ Term
_ Term
_)
        | (P NameType
_ Name
f Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t = Name -> [Term] -> ElabD Term
reifyTTApp Name
f [Term]
args
reifyTT t :: Term
t@(P NameType
_ Name
n Term
_)
        | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Erased" = forall (m :: * -> *) a. Monad m => a -> m a
return forall n. TT n
Erased
reifyTT t :: Term
t@(P NameType
_ Name
n Term
_)
        | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Impossible" = forall (m :: * -> *) a. Monad m => a -> m a
return forall n. TT n
Impossible
reifyTT Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection term: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)

reifyTTApp :: Name -> [Term] -> ElabD Term
reifyTTApp :: Name -> [Term] -> ElabD Term
reifyTTApp Name
t [Term
nt, Term
n, Term
x]
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"P" = do NameType
nt' <- Term -> ElabD NameType
reifyTTNameType Term
nt
                                 Name
n'  <- Term -> ElabD Name
reifyTTName Term
n
                                 Term
x'  <- Term -> ElabD Term
reifyTT Term
x
                                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. NameType -> n -> TT n -> TT n
P NameType
nt' Name
n' Term
x'
reifyTTApp Name
t [Constant (I Int
i)]
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"V" = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. Int -> TT n
V Int
i
reifyTTApp Name
t [Term
n, Term
b, Term
x]
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Bind" = do Name
n' <- Term -> ElabD Name
reifyTTName Term
n
                                    Binder Term
b' <- forall a. (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinder Term -> ElabD Term
reifyTT (String -> Name
reflm String
"TT") Term
b
                                    Term
x' <- Term -> ElabD Term
reifyTT Term
x
                                    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' Binder Term
b' Term
x'
reifyTTApp Name
t [Term
f, Term
x]
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"App" = do Term
f' <- Term -> ElabD Term
reifyTT Term
f
                                   Term
x' <- Term -> ElabD Term
reifyTT Term
x
                                   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. AppStatus n -> TT n -> TT n -> TT n
App forall n. AppStatus n
Complete Term
f' Term
x'
reifyTTApp Name
t [Term
c]
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"TConst" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall n. Const -> TT n
Constant (Term -> ElabD Const
reifyTTConst Term
c)
reifyTTApp Name
t [Term
t', Constant (I Int
i)]
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Proj" = do Term
t'' <- Term -> ElabD Term
reifyTT Term
t'
                                    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. TT n -> Int -> TT n
Proj Term
t'' Int
i
reifyTTApp Name
t [Term
tt]
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"TType" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall n. UExp -> TT n
TType (Term -> ElabD UExp
reifyTTUExp Term
tt)
reifyTTApp Name
t [Term
tt]
           | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"UType" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall n. Universe -> TT n
UType (Term -> ElabD Universe
reifyUniverse Term
tt)
reifyTTApp Name
t [Term]
args = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection term: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name
t, [Term]
args))

reifyUniverse :: Term -> ElabD Universe
reifyUniverse :: Term -> ElabD Universe
reifyUniverse (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"AllTypes" = forall (m :: * -> *) a. Monad m => a -> m a
return Universe
AllTypes
                        | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"UniqueType" = forall (m :: * -> *) a. Monad m => a -> m a
return Universe
UniqueType
                        | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"NullType" = forall (m :: * -> *) a. Monad m => a -> m a
return Universe
NullType
reifyUniverse Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection universe: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm)

-- | Reify raw terms from their reflected representation
reifyRaw :: Term -> ElabD Raw
reifyRaw :: Term -> ElabD Raw
reifyRaw t :: Term
t@(App AppStatus Name
_ Term
_ Term
_)
         | (P NameType
_ Name
f Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t = Name -> [Term] -> ElabD Raw
reifyRawApp Name
f [Term]
args
reifyRaw t :: Term
t@(P NameType
_ Name
n Term
_)
         | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"RType" = forall (m :: * -> *) a. Monad m => a -> m a
return Raw
RType
reifyRaw Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection raw term in reifyRaw: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)

reifyRawApp :: Name -> [Term] -> ElabD Raw
reifyRawApp :: Name -> [Term] -> ElabD Raw
reifyRawApp Name
t [Term
n]
            | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Var" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Name -> Raw
Var (Term -> ElabD Name
reifyTTName Term
n)
reifyRawApp Name
t [Term
n, Term
b, Term
x]
            | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"RBind" = do Name
n' <- Term -> ElabD Name
reifyTTName Term
n
                                      Binder Raw
b' <- forall a. (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinder Term -> ElabD Raw
reifyRaw (String -> Name
reflm String
"Raw") Term
b
                                      Raw
x' <- Term -> ElabD Raw
reifyRaw Term
x
                                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> Binder Raw -> Raw -> Raw
RBind Name
n' Binder Raw
b' Raw
x'
reifyRawApp Name
t [Term
f, Term
x]
            | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"RApp" = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Raw -> Raw -> Raw
RApp (Term -> ElabD Raw
reifyRaw Term
f) (Term -> ElabD Raw
reifyRaw Term
x)
reifyRawApp Name
t [Term
c]
            | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"RConstant" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Const -> Raw
RConstant (Term -> ElabD Const
reifyTTConst Term
c)
reifyRawApp Name
t [Term]
args = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection raw term in reifyRawApp: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name
t, [Term]
args))

reifyTTName :: Term -> ElabD Name
reifyTTName :: Term -> ElabD Name
reifyTTName Term
t
            | (P NameType
_ Name
f Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t = Name -> [Term] -> ElabD Name
reifyTTNameApp Name
f [Term]
args
reifyTTName Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection term name: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)

reifyTTNameApp :: Name -> [Term] -> ElabD Name
reifyTTNameApp :: Name -> [Term] -> ElabD Name
reifyTTNameApp Name
t [Constant (Str String
n)]
               | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"UN" = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> Name
sUN String
n
reifyTTNameApp Name
t [Term
n, Term
ns]
               | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"NS" = do Name
n'  <- Term -> ElabD Name
reifyTTName Term
n
                                      [String]
ns' <- Term -> ElabD [String]
reifyTTNamespace Term
ns
                                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> [String] -> Name
sNS Name
n' [String]
ns'
reifyTTNameApp Name
t [Constant (I Int
i), Constant (Str String
n)]
               | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"MN" = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> String -> Name
sMN Int
i String
n
reifyTTNameApp Name
t [Term
sn]
               | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"SN"
               , (P NameType
_ Name
f Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
sn = SpecialName -> Name
SN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [Term] -> ElabD SpecialName
reifySN Name
f [Term]
args
  where reifySN :: Name -> [Term] -> ElabD SpecialName
        reifySN :: Name -> [Term] -> ElabD SpecialName
reifySN Name
t [Constant (I Int
i), Term
n1, Term
n2]
                | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"WhereN" = Int -> Name -> Name -> SpecialName
WhereN Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD Name
reifyTTName Term
n1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ElabD Name
reifyTTName Term
n2
        reifySN Name
t [Constant (I Int
i), Term
n]
                | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"WithN" = Int -> Name -> SpecialName
WithN Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD Name
reifyTTName Term
n
        reifySN Name
t [Term
n, Term
ss]
                | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ImplementationN" =
                  case Term -> Maybe [Term]
unList Term
ss of
                    Maybe [Term]
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't reify ImplementationN strings"
                    Just [Term]
ss' -> Name -> [Text] -> SpecialName
ImplementationN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD Name
reifyTTName Term
n forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
                                 forall (f :: * -> *) a. Applicative f => a -> f a
pure [String -> Text
T.pack String
s | Constant (Str String
s) <- [Term]
ss']
        reifySN Name
t [Term
n, Constant (Str String
s)]
                | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ParentN" =
                  Name -> Text -> SpecialName
ParentN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD Name
reifyTTName Term
n forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Text
T.pack String
s)
        reifySN Name
t [Term
n]
                | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"MethodN" =
                  Name -> SpecialName
MethodN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD Name
reifyTTName Term
n
        reifySN Name
t [Term
fc, Term
n]
                | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"CaseN" =
                  FC' -> Name -> SpecialName
CaseN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FC -> FC'
FC' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD FC
reifyFC Term
fc) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ElabD Name
reifyTTName Term
n
        reifySN Name
t [Term
n]
                | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ImplementationCtorN" =
                  Name -> SpecialName
ImplementationCtorN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD Name
reifyTTName Term
n
        reifySN Name
t [Term
n1, Term
n2]
                | Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"MetaN" =
                  Name -> Name -> SpecialName
MetaN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD Name
reifyTTName Term
n1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ElabD Name
reifyTTName Term
n2
        reifySN Name
t [Term]
args = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Can't reify special name " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
t forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Term]
args
reifyTTNameApp Name
t [Term]
args = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection term name: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name
t, [Term]
args))

reifyTTNamespace :: Term -> ElabD [String]
reifyTTNamespace :: Term -> ElabD [String]
reifyTTNamespace t :: Term
t@(App AppStatus Name
_ Term
_ Term
_)
  = case forall n. TT n -> (TT n, [TT n])
unApply Term
t of
      (P NameType
_ Name
f Term
_, [Constant Const
StrType])
           | Name
f forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN String
"Nil") [String
"List", String
"Prelude"] -> forall (m :: * -> *) a. Monad m => a -> m a
return []
      (P NameType
_ Name
f Term
_, [Constant Const
StrType, Constant (Str String
n), Term
ns])
           | Name
f forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN String
"::")  [String
"List", String
"Prelude"] -> forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (String
nforall a. a -> [a] -> [a]
:) (Term -> ElabD [String]
reifyTTNamespace Term
ns)
      (Term, [Term])
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection namespace arg: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)
reifyTTNamespace Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection namespace arg: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)

reifyTTNameType :: Term -> ElabD NameType
reifyTTNameType :: Term -> ElabD NameType
reifyTTNameType t :: Term
t@(P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Bound" = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ NameType
Bound
reifyTTNameType t :: Term
t@(P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Ref" = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ NameType
Ref
reifyTTNameType t :: Term
t@(App AppStatus Name
_ Term
_ Term
_)
  = case forall n. TT n -> (TT n, [TT n])
unApply Term
t of
      (P NameType
_ Name
f Term
_, [Constant (I Int
tag), Constant (I Int
num)])
           | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"DCon" -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Int -> Bool -> NameType
DCon Int
tag Int
num Bool
False -- FIXME: Uniqueness!
           | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"TCon" -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Int -> NameType
TCon Int
tag Int
num
      (Term, [Term])
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection name type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)
reifyTTNameType Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection name type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)

reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinder :: forall a. (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinder Term -> ElabD a
reificator Name
binderType t :: Term
t@(App AppStatus Name
_ Term
_ Term
_)
  = case forall n. TT n -> (TT n, [TT n])
unApply Term
t of
     (P NameType
_ Name
f Term
_, Term
bt:[Term]
args) | Term -> Raw
forget Term
bt forall a. Eq a => a -> a -> Bool
== Name -> Raw
Var Name
binderType
       -> forall a. (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
reifyTTBinderApp Term -> ElabD a
reificator Name
f [Term]
args
     (Term, [Term])
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Mismatching binder reflection: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)
reifyTTBinder Term -> ElabD a
_ Name
_ Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection binder: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)

reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
reifyTTBinderApp :: forall a. (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
reifyTTBinderApp Term -> ElabD a
reif Name
f [Term
t]
                      | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Lam" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall b. RigCount -> b -> Binder b
Lam RigCount
RigW) (Term -> ElabD a
reif Term
t)
reifyTTBinderApp Term -> ElabD a
reif Name
f [Term
t, Term
k]
                      | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Pi" = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing) (Term -> ElabD a
reif Term
t) (Term -> ElabD a
reif Term
k)
reifyTTBinderApp Term -> ElabD a
reif Name
f [Term
x, Term
y]
                      | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Let" = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (forall b. RigCount -> b -> b -> Binder b
Let RigCount
RigW) (Term -> ElabD a
reif Term
x) (Term -> ElabD a
reif Term
y)
reifyTTBinderApp Term -> ElabD a
reif Name
f [Term
t]
                      | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Hole" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall b. b -> Binder b
Hole (Term -> ElabD a
reif Term
t)
reifyTTBinderApp Term -> ElabD a
reif Name
f [Term
t]
                      | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"GHole" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall b. Int -> [Name] -> b -> Binder b
GHole Int
0 []) (Term -> ElabD a
reif Term
t)
reifyTTBinderApp Term -> ElabD a
reif Name
f [Term
x, Term
y]
                      | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Guess" = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall b. b -> b -> Binder b
Guess (Term -> ElabD a
reif Term
x) (Term -> ElabD a
reif Term
y)
reifyTTBinderApp Term -> ElabD a
reif Name
f [Term
t]
                      | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"PVar" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall b. RigCount -> b -> Binder b
PVar RigCount
RigW) (Term -> ElabD a
reif Term
t)
reifyTTBinderApp Term -> ElabD a
reif Name
f [Term
t]
                      | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"PVTy" = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall b. b -> Binder b
PVTy (Term -> ElabD a
reif Term
t)
reifyTTBinderApp Term -> ElabD a
_ Name
f [Term]
args = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection binder: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name
f, [Term]
args))

reifyTTConst :: Term -> ElabD Const
reifyTTConst :: Term -> ElabD Const
reifyTTConst (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"StrType"  = forall (m :: * -> *) a. Monad m => a -> m a
return Const
StrType
reifyTTConst (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"VoidType" = forall (m :: * -> *) a. Monad m => a -> m a
return Const
VoidType
reifyTTConst (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Forgot"   = forall (m :: * -> *) a. Monad m => a -> m a
return Const
Forgot
reifyTTConst t :: Term
t@(App AppStatus Name
_ Term
_ Term
_)
             | (P NameType
_ Name
f Term
_, [Term
arg]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t   = Name -> Term -> ElabD Const
reifyTTConstApp Name
f Term
arg
reifyTTConst Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection constant: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)

reifyTTConstApp :: Name -> Term -> ElabD Const
reifyTTConstApp :: Name -> Term -> ElabD Const
reifyTTConstApp Name
f Term
aty
                | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"AType" = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ArithTy -> Const
AType (Term -> ElabD ArithTy
reifyArithTy Term
aty)
reifyTTConstApp Name
f (Constant c :: Const
c@(I Int
_))
                | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"I"   = forall (m :: * -> *) a. Monad m => a -> m a
return Const
c
reifyTTConstApp Name
f (Constant c :: Const
c@(BI Integer
_))
                | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"BI"  = forall (m :: * -> *) a. Monad m => a -> m a
return Const
c
reifyTTConstApp Name
f (Constant c :: Const
c@(Fl Double
_))
                | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Fl"  = forall (m :: * -> *) a. Monad m => a -> m a
return Const
c
reifyTTConstApp Name
f (Constant c :: Const
c@(Ch Char
_))
                | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Ch"  = forall (m :: * -> *) a. Monad m => a -> m a
return Const
c
reifyTTConstApp Name
f (Constant c :: Const
c@(Str String
_))
                | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Str" = forall (m :: * -> *) a. Monad m => a -> m a
return Const
c
reifyTTConstApp Name
f (Constant c :: Const
c@(B8 Word8
_))
                | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"B8"  = forall (m :: * -> *) a. Monad m => a -> m a
return Const
c
reifyTTConstApp Name
f (Constant c :: Const
c@(B16 Word16
_))
                | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"B16" = forall (m :: * -> *) a. Monad m => a -> m a
return Const
c
reifyTTConstApp Name
f (Constant c :: Const
c@(B32 Word32
_))
                | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"B32" = forall (m :: * -> *) a. Monad m => a -> m a
return Const
c
reifyTTConstApp Name
f (Constant c :: Const
c@(B64 Word64
_))
                | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"B64" = forall (m :: * -> *) a. Monad m => a -> m a
return Const
c
reifyTTConstApp Name
f v :: Term
v@(P NameType
_ Name
_ Term
_) =
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Err -> TC a
tfail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
      String
"Can't reify the variable " forall a. [a] -> [a] -> [a]
++
      forall a. Show a => a -> String
show Term
v forall a. [a] -> [a] -> [a]
++
      String
" as a constant, because its value is not statically known."
reifyTTConstApp Name
f Term
arg = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection constant: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name
f, Term
arg))

reifyArithTy :: Term -> ElabD ArithTy
reifyArithTy :: Term -> ElabD ArithTy
reifyArithTy (App AppStatus Name
_ (P NameType
_ Name
n Term
_) Term
intTy) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ATInt"    = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IntTy -> ArithTy
ATInt (Term -> ElabD IntTy
reifyIntTy Term
intTy)
reifyArithTy (P NameType
_ Name
n Term
_)               | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ATDouble" = forall (m :: * -> *) a. Monad m => a -> m a
return ArithTy
ATFloat
reifyArithTy Term
x = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Couldn't reify reflected ArithTy: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
x)

reifyNativeTy :: Term -> ElabD NativeTy
reifyNativeTy :: Term -> ElabD NativeTy
reifyNativeTy (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"IT8"  = forall (m :: * -> *) a. Monad m => a -> m a
return NativeTy
IT8
reifyNativeTy (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"IT16" = forall (m :: * -> *) a. Monad m => a -> m a
return NativeTy
IT16
reifyNativeTy (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"IT32" = forall (m :: * -> *) a. Monad m => a -> m a
return NativeTy
IT32
reifyNativeTy (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"IT64" = forall (m :: * -> *) a. Monad m => a -> m a
return NativeTy
IT64
reifyNativeTy Term
x = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify reflected NativeTy " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
x

reifyIntTy :: Term -> ElabD IntTy
reifyIntTy :: Term -> ElabD IntTy
reifyIntTy (App AppStatus Name
_ (P NameType
_ Name
n Term
_) Term
nt) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ITFixed" = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NativeTy -> IntTy
ITFixed (Term -> ElabD NativeTy
reifyNativeTy Term
nt)
reifyIntTy (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ITNative" = forall (m :: * -> *) a. Monad m => a -> m a
return IntTy
ITNative
reifyIntTy (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ITBig" = forall (m :: * -> *) a. Monad m => a -> m a
return IntTy
ITBig
reifyIntTy (P NameType
_ Name
n Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"ITChar" = forall (m :: * -> *) a. Monad m => a -> m a
return IntTy
ITChar
reifyIntTy Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"The term " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++ String
" is not a reflected IntTy"

reifyTTUExp :: Term -> ElabD UExp
reifyTTUExp :: Term -> ElabD UExp
reifyTTUExp t :: Term
t@(App AppStatus Name
_ Term
_ Term
_)
  = case forall n. TT n -> (TT n, [TT n])
unApply Term
t of
      (P NameType
_ Name
f Term
_, [Constant (Str String
str), Constant (I Int
i)])
           | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"UVar" -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> Int -> UExp
UVar String
str Int
i
      (P NameType
_ Name
f Term
_, [Constant (I Int
i)])
           | Name
f forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"UVal" -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> UExp
UVal Int
i
      (Term, [Term])
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection type universe expression: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)
reifyTTUExp Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown reflection type universe expression: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t)

-- | Create a reflected call to a named function/constructor
reflCall :: String -> [Raw] -> Raw
reflCall :: String -> [Raw] -> Raw
reflCall String
funName [Raw]
args
  = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (String -> Name
reflm String
funName)) [Raw]
args

-- | Lift a term into its Language.Reflection.TT representation
reflect :: Term -> Raw
reflect :: Term -> Raw
reflect = [Name] -> Term -> Raw
reflectTTQuote []

-- | Lift a term into its Language.Reflection.Raw representation
reflectRaw :: Raw -> Raw
reflectRaw :: Raw -> Raw
reflectRaw = [Name] -> Raw -> Raw
reflectRawQuote []

claimTy :: Name -> Raw -> ElabD Name
claimTy :: Name -> Raw -> ElabD Name
claimTy Name
n Raw
ty = do Name
n' <- forall aux. Name -> Elab' aux Name
getNameFrom Name
n
                  forall aux. Name -> Raw -> Elab' aux ()
claim Name
n' Raw
ty
                  forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'

intToReflectedNat :: Int -> Raw
intToReflectedNat :: Int -> Raw
intToReflectedNat Int
i = if Int
i forall a. Ord a => a -> a -> Bool
<= Int
0
                        then Name -> Raw
Var (String -> Name
natN String
"Z")
                        else Raw -> Raw -> Raw
RApp (Name -> Raw
Var (String -> Name
natN String
"S")) (Int -> Raw
intToReflectedNat (Int
i forall a. Num a => a -> a -> a
- Int
1))
  where natN :: String -> Name
        natN :: String -> Name
natN String
n = Name -> [String] -> Name
sNS (String -> Name
sUN String
n) [String
"Nat", String
"Prelude"]

reflectFixity :: Fixity -> Raw
reflectFixity :: Fixity -> Raw
reflectFixity (Infixl  Int
p) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (String -> Name
tacN String
"Infixl")) (Int -> Raw
intToReflectedNat Int
p)
reflectFixity (Infixr  Int
p) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (String -> Name
tacN String
"Infixr")) (Int -> Raw
intToReflectedNat Int
p)
reflectFixity (InfixN  Int
p) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (String -> Name
tacN String
"InfixN")) (Int -> Raw
intToReflectedNat Int
p)
reflectFixity (PrefixN Int
p) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (String -> Name
tacN String
"PrefixN")) (Int -> Raw
intToReflectedNat Int
p)

-- | Convert a reflected term to a more suitable form for pattern-matching.
-- In particular, the less-interesting bits are elaborated to _ patterns. This
-- happens to NameTypes, universe levels, names that are bound but not used,
-- and the type annotation field of the P constructor.
reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
reflectTTQuotePattern [Name]
unq (P NameType
_ Name
n Term
_)
  | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
unq = -- the unquoted names have been claimed as TT already - just use them
    do forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var Name
n) ; forall aux. Elab' aux ()
solve
  | Bool
otherwise =
    do Name
tyannot <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"pTyAnnot") (Name -> Raw
Var (String -> Name
reflm String
"TT"))
       forall aux. Name -> Elab' aux ()
movelast Name
tyannot  -- use a _ pattern here
       Name
nt <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"nt")
       forall aux. Name -> Raw -> Elab' aux ()
claim Name
nt (Name -> Raw
Var (String -> Name
reflm String
"NameType"))
       forall aux. Name -> Elab' aux ()
movelast Name
nt       -- use a _ pattern here
       Name
n' <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"n")
       forall aux. Name -> Raw -> Elab' aux ()
claim Name
n' (Name -> Raw
Var (String -> Name
reflm String
"TTName"))
       forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"P" [Name -> Raw
Var Name
nt, Name -> Raw
Var Name
n', Name -> Raw
Var Name
tyannot]
       forall aux. Elab' aux ()
solve
       forall aux. Name -> Elab' aux ()
focus Name
n'; Name -> ElabD ()
reflectNameQuotePattern Name
n
reflectTTQuotePattern [Name]
unq (V Int
n)
  = do forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"V" [Const -> Raw
RConstant (Int -> Const
I Int
n)]
       forall aux. Elab' aux ()
solve
reflectTTQuotePattern [Name]
unq (Bind Name
n Binder Term
b Term
x)
  = do Name
x' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"sc") (Name -> Raw
Var (String -> Name
reflm String
"TT"))
       forall aux. Name -> Elab' aux ()
movelast Name
x'
       Name
b' <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"binder")
       forall aux. Name -> Raw -> Elab' aux ()
claim Name
b' (Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Binder") [String
"Reflection", String
"Language"]))
                      (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"TT") [String
"Reflection", String
"Language"])))
       if Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall n. Eq n => TT n -> [n]
freeNames Term
x
         then do forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"Bind"
                                 [Name -> Raw
reflectName Name
n,
                                  Name -> Raw
Var Name
b',
                                  Name -> Raw
Var Name
x']
                 forall aux. Elab' aux ()
solve
         else do Name
any <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"anyName")
                 forall aux. Name -> Raw -> Elab' aux ()
claim Name
any (Name -> Raw
Var (String -> Name
reflm String
"TTName"))
                 forall aux. Name -> Elab' aux ()
movelast Name
any
                 forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"Bind"
                                 [Name -> Raw
Var Name
any,
                                  Name -> Raw
Var Name
b',
                                  Name -> Raw
Var Name
x']
                 forall aux. Elab' aux ()
solve
       forall aux. Name -> Elab' aux ()
focus Name
x'; [Name] -> Term -> ElabD ()
reflectTTQuotePattern [Name]
unq Term
x
       forall aux. Name -> Elab' aux ()
focus Name
b'; forall a.
([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()
reflectBinderQuotePattern [Name] -> Term -> ElabD ()
reflectTTQuotePattern (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TT") [Name]
unq Binder Term
b
reflectTTQuotePattern [Name]
unq (App AppStatus Name
_ Term
f Term
x)
  = do Name
f' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"f") (Name -> Raw
Var (String -> Name
reflm String
"TT")) ; forall aux. Name -> Elab' aux ()
movelast Name
f'
       Name
x' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"x") (Name -> Raw
Var (String -> Name
reflm String
"TT")) ; forall aux. Name -> Elab' aux ()
movelast Name
x'
       forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"App" [Name -> Raw
Var Name
f', Name -> Raw
Var Name
x']
       forall aux. Elab' aux ()
solve
       forall aux. Name -> Elab' aux ()
focus Name
f'; [Name] -> Term -> ElabD ()
reflectTTQuotePattern [Name]
unq Term
f
       forall aux. Name -> Elab' aux ()
focus Name
x'; [Name] -> Term -> ElabD ()
reflectTTQuotePattern [Name]
unq Term
x
reflectTTQuotePattern [Name]
unq (Constant Const
c)
  = do forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"TConst" [Const -> Raw
reflectConstant Const
c]
       forall aux. Elab' aux ()
solve
reflectTTQuotePattern [Name]
unq (Proj Term
t Int
i)
  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Err -> TC a
tfail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
InternalMsg forall a b. (a -> b) -> a -> b
$
      String
"Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuotePattern [Name]
unq Term
Erased
  = do Name
erased <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"erased") (Name -> Raw
Var (String -> Name
reflm String
"TT"))
       forall aux. Name -> Elab' aux ()
movelast Name
erased
       forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var Name
erased)
reflectTTQuotePattern [Name]
unq Term
Impossible
  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Err -> TC a
tfail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
InternalMsg forall a b. (a -> b) -> a -> b
$
      String
"Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuotePattern [Name]
unq (Inferred Term
t)
  = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Err -> TC a
tfail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
InternalMsg forall a b. (a -> b) -> a -> b
$
      String
"Phase error! The Inferred constructor is for coverage checking only and should not have been reflected during elaboration."
reflectTTQuotePattern [Name]
unq (TType UExp
exp)
  = do Name
ue <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"uexp")
       forall aux. Name -> Raw -> Elab' aux ()
claim Name
ue (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"TTUExp") [String
"Reflection", String
"Language"]))
       forall aux. Name -> Elab' aux ()
movelast Name
ue
       forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"TType" [Name -> Raw
Var Name
ue]
       forall aux. Elab' aux ()
solve
reflectTTQuotePattern [Name]
unq (UType Universe
u)
  = do Name
uH <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"someUniv")
       forall aux. Name -> Raw -> Elab' aux ()
claim Name
uH (Name -> Raw
Var (String -> Name
reflm String
"Universe"))
       forall aux. Name -> Elab' aux ()
movelast Name
uH
       forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"UType" [Name -> Raw
Var Name
uH]
       forall aux. Elab' aux ()
solve
       forall aux. Name -> Elab' aux ()
focus Name
uH
       forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var (String -> Name
reflm (case Universe
u of
                           Universe
NullType -> String
"NullType"
                           Universe
UniqueType -> String
"UniqueType"
                           Universe
AllTypes -> String
"AllTypes")))
       forall aux. Elab' aux ()
solve

reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
reflectRawQuotePattern [Name]
unq (Var Name
n)
  -- the unquoted names already have types, just use them
  | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
unq = do forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var Name
n); forall aux. Elab' aux ()
solve
  | Bool
otherwise = do forall aux. Raw -> Elab' aux ()
fill (String -> [Raw] -> Raw
reflCall String
"Var" [Name -> Raw
reflectName Name
n]); forall aux. Elab' aux ()
solve
reflectRawQuotePattern [Name]
unq (RBind Name
n Binder Raw
b Raw
sc) =
  do Name
scH <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"sc")
     forall aux. Name -> Raw -> Elab' aux ()
claim Name
scH (Name -> Raw
Var (String -> Name
reflm String
"Raw"))
     forall aux. Name -> Elab' aux ()
movelast Name
scH
     Name
bH <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"binder")
     forall aux. Name -> Raw -> Elab' aux ()
claim Name
bH (Raw -> Raw -> Raw
RApp (Name -> Raw
Var (String -> Name
reflm String
"Binder"))
                    (Name -> Raw
Var (String -> Name
reflm String
"Raw")))
     if Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Raw -> [Name]
freeNamesR Raw
sc
        then do forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"RBind" [Name -> Raw
reflectName Name
n,
                                         Name -> Raw
Var Name
bH,
                                         Name -> Raw
Var Name
scH]
                forall aux. Elab' aux ()
solve
        else do Name
any <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"anyName")
                forall aux. Name -> Raw -> Elab' aux ()
claim Name
any (Name -> Raw
Var (String -> Name
reflm String
"TTName"))
                forall aux. Name -> Elab' aux ()
movelast Name
any
                forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"RBind" [Name -> Raw
Var Name
any, Name -> Raw
Var Name
bH, Name -> Raw
Var Name
scH]
                forall aux. Elab' aux ()
solve
     forall aux. Name -> Elab' aux ()
focus Name
scH; [Name] -> Raw -> ElabD ()
reflectRawQuotePattern [Name]
unq Raw
sc
     forall aux. Name -> Elab' aux ()
focus Name
bH; forall a.
([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()
reflectBinderQuotePattern [Name] -> Raw -> ElabD ()
reflectRawQuotePattern (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"Raw") [Name]
unq Binder Raw
b
  where freeNamesR :: Raw -> [Name]
freeNamesR (Var Name
n) = [Name
n]
        freeNamesR (RBind Name
n (Let RigCount
rc Raw
t Raw
v) Raw
body) = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Raw -> [Name]
freeNamesR Raw
v,
                                                         Raw -> [Name]
freeNamesR Raw
body forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n],
                                                         Raw -> [Name]
freeNamesR Raw
t]
        freeNamesR (RBind Name
n Binder Raw
b Raw
body) = Raw -> [Name]
freeNamesR (forall b. Binder b -> b
binderTy Binder Raw
b) forall a. [a] -> [a] -> [a]
++
                                      (Raw -> [Name]
freeNamesR Raw
body forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n])
        freeNamesR (RApp Raw
f Raw
x) = Raw -> [Name]
freeNamesR Raw
f forall a. [a] -> [a] -> [a]
++ Raw -> [Name]
freeNamesR Raw
x
        freeNamesR Raw
RType = []
        freeNamesR (RUType Universe
_) = []
        freeNamesR (RConstant Const
_) = []
reflectRawQuotePattern [Name]
unq (RApp Raw
f Raw
x) =
  do Name
fH <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"f")
     forall aux. Name -> Raw -> Elab' aux ()
claim Name
fH (Name -> Raw
Var (String -> Name
reflm String
"Raw"))
     forall aux. Name -> Elab' aux ()
movelast Name
fH
     Name
xH <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"x")
     forall aux. Name -> Raw -> Elab' aux ()
claim Name
xH (Name -> Raw
Var (String -> Name
reflm String
"Raw"))
     forall aux. Name -> Elab' aux ()
movelast Name
xH
     forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"RApp" [Name -> Raw
Var Name
fH, Name -> Raw
Var Name
xH]
     forall aux. Elab' aux ()
solve
     forall aux. Name -> Elab' aux ()
focus Name
fH; [Name] -> Raw -> ElabD ()
reflectRawQuotePattern [Name]
unq Raw
f
     forall aux. Name -> Elab' aux ()
focus Name
xH; [Name] -> Raw -> ElabD ()
reflectRawQuotePattern [Name]
unq Raw
x
reflectRawQuotePattern [Name]
unq Raw
RType =
  do forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var (String -> Name
reflm String
"RType"))
     forall aux. Elab' aux ()
solve
reflectRawQuotePattern [Name]
unq (RUType Universe
univ) =
  do Name
uH <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"universe")
     forall aux. Name -> Raw -> Elab' aux ()
claim Name
uH (Name -> Raw
Var (String -> Name
reflm String
"Universe"))
     forall aux. Name -> Elab' aux ()
movelast Name
uH
     forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"RUType" [Name -> Raw
Var Name
uH]
     forall aux. Elab' aux ()
solve
     forall aux. Name -> Elab' aux ()
focus Name
uH; forall aux. Raw -> Elab' aux ()
fill (Universe -> Raw
reflectUniverse Universe
univ); forall aux. Elab' aux ()
solve
reflectRawQuotePattern [Name]
unq (RConstant Const
c) =
  do Name
cH <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"const")
     forall aux. Name -> Raw -> Elab' aux ()
claim Name
cH (Name -> Raw
Var (String -> Name
reflm String
"Constant"))
     forall aux. Name -> Elab' aux ()
movelast Name
cH
     forall aux. Raw -> Elab' aux ()
fill (String -> [Raw] -> Raw
reflCall String
"RConstant" [Name -> Raw
Var Name
cH]); forall aux. Elab' aux ()
solve
     forall aux. Name -> Elab' aux ()
focus Name
cH
     forall aux. Raw -> Elab' aux ()
fill (Const -> Raw
reflectConstant Const
c); forall aux. Elab' aux ()
solve

reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()
reflectBinderQuotePattern :: forall a.
([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()
reflectBinderQuotePattern [Name] -> a -> ElabD ()
q Raw
ty [Name]
unq (Lam RigCount
_ a
t)
   = do Name
t' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"ty") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
t'
        forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"Lam" [Raw
ty, Name -> Raw
Var Name
t']
        forall aux. Elab' aux ()
solve
        forall aux. Name -> Elab' aux ()
focus Name
t'; [Name] -> a -> ElabD ()
q [Name]
unq a
t
reflectBinderQuotePattern [Name] -> a -> ElabD ()
q Raw
ty [Name]
unq (Pi RigCount
_ Maybe ImplicitInfo
_ a
t a
k)
   = do Name
t' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"ty") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
t'
        Name
k' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"k") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
k';
        forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"Pi" [Raw
ty, Name -> Raw
Var Name
t', Name -> Raw
Var Name
k']
        forall aux. Elab' aux ()
solve
        forall aux. Name -> Elab' aux ()
focus Name
t'; [Name] -> a -> ElabD ()
q [Name]
unq a
t
reflectBinderQuotePattern [Name] -> a -> ElabD ()
q Raw
ty [Name]
unq (Let RigCount
rc a
x a
y)
   = do Name
x' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"ty") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
x';
        Name
y' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"v")Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
y';
        forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"Let" [Raw
ty, Name -> Raw
Var Name
x', Name -> Raw
Var Name
y']
        forall aux. Elab' aux ()
solve
        forall aux. Name -> Elab' aux ()
focus Name
x'; [Name] -> a -> ElabD ()
q [Name]
unq a
x
        forall aux. Name -> Elab' aux ()
focus Name
y'; [Name] -> a -> ElabD ()
q [Name]
unq a
y
reflectBinderQuotePattern [Name] -> a -> ElabD ()
q Raw
ty [Name]
unq (NLet a
x a
y)
   = do Name
x' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"ty") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
x'
        Name
y' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"v") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
y'
        forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"Let" [Raw
ty, Name -> Raw
Var Name
x', Name -> Raw
Var Name
y']
        forall aux. Elab' aux ()
solve
        forall aux. Name -> Elab' aux ()
focus Name
x'; [Name] -> a -> ElabD ()
q [Name]
unq a
x
        forall aux. Name -> Elab' aux ()
focus Name
y'; [Name] -> a -> ElabD ()
q [Name]
unq a
y
reflectBinderQuotePattern [Name] -> a -> ElabD ()
q Raw
ty [Name]
unq (Hole a
t)
   = do Name
t' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"ty") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
t'
        forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"Hole" [Raw
ty, Name -> Raw
Var Name
t']
        forall aux. Elab' aux ()
solve
        forall aux. Name -> Elab' aux ()
focus Name
t'; [Name] -> a -> ElabD ()
q [Name]
unq a
t
reflectBinderQuotePattern [Name] -> a -> ElabD ()
q Raw
ty [Name]
unq (GHole Int
_ [Name]
_ a
t)
   = do Name
t' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"ty") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
t'
        forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"GHole" [Raw
ty, Name -> Raw
Var Name
t']
        forall aux. Elab' aux ()
solve
        forall aux. Name -> Elab' aux ()
focus Name
t'; [Name] -> a -> ElabD ()
q [Name]
unq a
t
reflectBinderQuotePattern [Name] -> a -> ElabD ()
q Raw
ty [Name]
unq (Guess a
x a
y)
   = do Name
x' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"ty") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
x'
        Name
y' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"v") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
y'
        forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"Guess" [Raw
ty, Name -> Raw
Var Name
x', Name -> Raw
Var Name
y']
        forall aux. Elab' aux ()
solve
        forall aux. Name -> Elab' aux ()
focus Name
x'; [Name] -> a -> ElabD ()
q [Name]
unq a
x
        forall aux. Name -> Elab' aux ()
focus Name
y'; [Name] -> a -> ElabD ()
q [Name]
unq a
y
reflectBinderQuotePattern [Name] -> a -> ElabD ()
q Raw
ty [Name]
unq (PVar RigCount
_ a
t)
   = do Name
t' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"ty") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
t'
        forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"PVar" [Raw
ty, Name -> Raw
Var Name
t']
        forall aux. Elab' aux ()
solve
        forall aux. Name -> Elab' aux ()
focus Name
t'; [Name] -> a -> ElabD ()
q [Name]
unq a
t
reflectBinderQuotePattern [Name] -> a -> ElabD ()
q Raw
ty [Name]
unq (PVTy a
t)
   = do Name
t' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN Int
0 String
"ty") Raw
ty; forall aux. Name -> Elab' aux ()
movelast Name
t'
        forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"PVTy" [Raw
ty, Name -> Raw
Var Name
t']
        forall aux. Elab' aux ()
solve
        forall aux. Name -> Elab' aux ()
focus Name
t'; [Name] -> a -> ElabD ()
q [Name]
unq a
t

reflectUniverse :: Universe -> Raw
reflectUniverse :: Universe -> Raw
reflectUniverse Universe
u =
  (Name -> Raw
Var (String -> Name
reflm (case Universe
u of
                 Universe
NullType -> String
"NullType"
                 Universe
UniqueType -> String
"UniqueType"
                 Universe
AllTypes -> String
"AllTypes")))

-- | Create a reflected TT term, but leave refs to the provided name intact
reflectTTQuote :: [Name] -> Term -> Raw
reflectTTQuote :: [Name] -> Term -> Raw
reflectTTQuote [Name]
unq (P NameType
nt Name
n Term
t)
  | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
unq = Name -> Raw
Var Name
n
  | Bool
otherwise = String -> [Raw] -> Raw
reflCall String
"P" [NameType -> Raw
reflectNameType NameType
nt, Name -> Raw
reflectName Name
n, [Name] -> Term -> Raw
reflectTTQuote [Name]
unq Term
t]
reflectTTQuote [Name]
unq (V Int
n)
  = String -> [Raw] -> Raw
reflCall String
"V" [Const -> Raw
RConstant (Int -> Const
I Int
n)]
reflectTTQuote [Name]
unq (Bind Name
n Binder Term
b Term
x)
  = String -> [Raw] -> Raw
reflCall String
"Bind" [Name -> Raw
reflectName Name
n, forall a. ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
reflectBinderQuote [Name] -> Term -> Raw
reflectTTQuote (String -> Name
reflm String
"TT") [Name]
unq Binder Term
b, [Name] -> Term -> Raw
reflectTTQuote [Name]
unq Term
x]
reflectTTQuote [Name]
unq (App AppStatus Name
_ Term
f Term
x)
  = String -> [Raw] -> Raw
reflCall String
"App" [[Name] -> Term -> Raw
reflectTTQuote [Name]
unq Term
f, [Name] -> Term -> Raw
reflectTTQuote [Name]
unq Term
x]
reflectTTQuote [Name]
unq (Constant Const
c)
  = String -> [Raw] -> Raw
reflCall String
"TConst" [Const -> Raw
reflectConstant Const
c]
reflectTTQuote [Name]
unq (TType UExp
exp) = String -> [Raw] -> Raw
reflCall String
"TType" [UExp -> Raw
reflectUExp UExp
exp]
reflectTTQuote [Name]
unq (UType Universe
u) = String -> [Raw] -> Raw
reflCall String
"UType" [Universe -> Raw
reflectUniverse Universe
u]
reflectTTQuote [Name]
_   (Proj Term
_ Int
_) =
  forall a. HasCallStack => String -> a
error String
"Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuote [Name]
unq Term
Erased = Name -> Raw
Var (String -> Name
reflm String
"Erased")
reflectTTQuote [Name]
_   Term
Impossible =
  forall a. HasCallStack => String -> a
error String
"Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuote [Name]
_   (Inferred Term
tm) =
  forall a. HasCallStack => String -> a
error String
"Phase error! The Inferred constructor is for coverage checking only and should not have been reflected during elaboration."

reflectRawQuote :: [Name] -> Raw -> Raw
reflectRawQuote :: [Name] -> Raw -> Raw
reflectRawQuote [Name]
unq (Var Name
n)
  | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
unq = Name -> Raw
Var Name
n
  | Bool
otherwise = String -> [Raw] -> Raw
reflCall String
"Var" [Name -> Raw
reflectName Name
n]
reflectRawQuote [Name]
unq (RBind Name
n Binder Raw
b Raw
r) =
  String -> [Raw] -> Raw
reflCall String
"RBind" [Name -> Raw
reflectName Name
n, forall a. ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
reflectBinderQuote [Name] -> Raw -> Raw
reflectRawQuote (String -> Name
reflm String
"Raw") [Name]
unq Binder Raw
b, [Name] -> Raw -> Raw
reflectRawQuote [Name]
unq Raw
r]
reflectRawQuote [Name]
unq (RApp Raw
f Raw
x) =
  String -> [Raw] -> Raw
reflCall String
"RApp" [[Name] -> Raw -> Raw
reflectRawQuote [Name]
unq Raw
f, [Name] -> Raw -> Raw
reflectRawQuote [Name]
unq Raw
x]
reflectRawQuote [Name]
unq Raw
RType = Name -> Raw
Var (String -> Name
reflm String
"RType")
reflectRawQuote [Name]
unq (RUType Universe
u) =
  String -> [Raw] -> Raw
reflCall String
"RUType" [Universe -> Raw
reflectUniverse Universe
u]
reflectRawQuote [Name]
unq (RConstant Const
cst) = String -> [Raw] -> Raw
reflCall String
"RConstant" [Const -> Raw
reflectConstant Const
cst]

reflectNameType :: NameType -> Raw
reflectNameType :: NameType -> Raw
reflectNameType (NameType
Bound) = Name -> Raw
Var (String -> Name
reflm String
"Bound")
reflectNameType (NameType
Ref) = Name -> Raw
Var (String -> Name
reflm String
"Ref")
reflectNameType (DCon Int
x Int
y Bool
_)
  = String -> [Raw] -> Raw
reflCall String
"DCon" [Const -> Raw
RConstant (Int -> Const
I Int
x), Const -> Raw
RConstant (Int -> Const
I Int
y)] -- FIXME: Uniqueness!
reflectNameType (TCon Int
x Int
y)
  = String -> [Raw] -> Raw
reflCall String
"TCon" [Const -> Raw
RConstant (Int -> Const
I Int
x), Const -> Raw
RConstant (Int -> Const
I Int
y)]

reflectName :: Name -> Raw
reflectName :: Name -> Raw
reflectName (UN Text
s)
  = String -> [Raw] -> Raw
reflCall String
"UN" [Const -> Raw
RConstant (String -> Const
Str (Text -> String
str Text
s))]
reflectName (NS Name
n [Text]
ns)
  = String -> [Raw] -> Raw
reflCall String
"NS" [ Name -> Raw
reflectName Name
n
                  , forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ String
n Raw
s ->
                             Raw -> [Raw] -> Raw
raw_apply ( Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ Name -> [String] -> Name
sNS (String -> Name
sUN String
"::") [String
"List", String
"Prelude"] )
                                       [ Const -> Raw
RConstant Const
StrType, Const -> Raw
RConstant (String -> Const
Str String
n), Raw
s ])
                             ( Raw -> [Raw] -> Raw
raw_apply ( Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ Name -> [String] -> Name
sNS (String -> Name
sUN String
"Nil") [String
"List", String
"Prelude"] )
                                         [ Const -> Raw
RConstant Const
StrType ])
                             (forall a b. (a -> b) -> [a] -> [b]
map Text -> String
str [Text]
ns)
                  ]
reflectName (MN Int
i Text
n)
  = String -> [Raw] -> Raw
reflCall String
"MN" [Const -> Raw
RConstant (Int -> Const
I Int
i), Const -> Raw
RConstant (String -> Const
Str (Text -> String
str Text
n))]
reflectName (SN SpecialName
sn) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (String -> Name
reflm String
"SN")) [SpecialName -> Raw
reflectSpecialName SpecialName
sn]
reflectName (SymRef Int
_) = forall a. HasCallStack => String -> a
error String
"The impossible happened: symbol table ref survived IBC loading"

reflectSpecialName :: SpecialName -> Raw
reflectSpecialName :: SpecialName -> Raw
reflectSpecialName (WhereN Int
i Name
n1 Name
n2) =
  String -> [Raw] -> Raw
reflCall String
"WhereN" [Const -> Raw
RConstant (Int -> Const
I Int
i), Name -> Raw
reflectName Name
n1, Name -> Raw
reflectName Name
n2]
reflectSpecialName (WithN Int
i Name
n) = String -> [Raw] -> Raw
reflCall String
"WithN" [ Const -> Raw
RConstant (Int -> Const
I Int
i)
                                                  , Name -> Raw
reflectName Name
n
                                                  ]
reflectSpecialName (ImplementationN Name
impl [Text]
ss) =
  String -> [Raw] -> Raw
reflCall String
"ImplementationN" [ Name -> Raw
reflectName Name
impl
                             , Raw -> [Raw] -> Raw
mkList (Const -> Raw
RConstant Const
StrType) forall a b. (a -> b) -> a -> b
$
                                 forall a b. (a -> b) -> [a] -> [b]
map (Const -> Raw
RConstant forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Const
Str forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack) [Text]
ss
                             ]
reflectSpecialName (ParentN Name
n Text
s) =
  String -> [Raw] -> Raw
reflCall String
"ParentN" [Name -> Raw
reflectName Name
n, Const -> Raw
RConstant (String -> Const
Str (Text -> String
T.unpack Text
s))]
reflectSpecialName (MethodN Name
n) =
  String -> [Raw] -> Raw
reflCall String
"MethodN" [Name -> Raw
reflectName Name
n]
reflectSpecialName (CaseN FC'
fc Name
n) =
  String -> [Raw] -> Raw
reflCall String
"CaseN" [FC -> Raw
reflectFC (FC' -> FC
unwrapFC FC'
fc), Name -> Raw
reflectName Name
n]
reflectSpecialName (ImplementationCtorN Name
n) =
  String -> [Raw] -> Raw
reflCall String
"ImplementationCtorN" [Name -> Raw
reflectName Name
n]
reflectSpecialName (MetaN Name
parent Name
meta) =
  String -> [Raw] -> Raw
reflCall String
"MetaN" [Name -> Raw
reflectName Name
parent, Name -> Raw
reflectName Name
meta]

-- | Elaborate a name to a pattern.  This means that NS and UN will be intact.
-- MNs corresponding to will care about the string but not the number.  All
-- others become _.
reflectNameQuotePattern :: Name -> ElabD ()
reflectNameQuotePattern :: Name -> ElabD ()
reflectNameQuotePattern n :: Name
n@(UN Text
s)
  = do forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ Name -> Raw
reflectName Name
n
       forall aux. Elab' aux ()
solve
reflectNameQuotePattern n :: Name
n@(NS Name
_ [Text]
_)
  = do forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ Name -> Raw
reflectName Name
n
       forall aux. Elab' aux ()
solve
reflectNameQuotePattern (MN Int
_ Text
n)
  = do Name
i <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"mnCounter")
       forall aux. Name -> Raw -> Elab' aux ()
claim Name
i (Const -> Raw
RConstant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITNative)))
       forall aux. Name -> Elab' aux ()
movelast Name
i
       forall aux. Raw -> Elab' aux ()
fill forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall String
"MN" [Name -> Raw
Var Name
i, Const -> Raw
RConstant (String -> Const
Str forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
n)]
       forall aux. Elab' aux ()
solve
reflectNameQuotePattern Name
_ -- for all other names, match any
  = do Name
nameHole <- forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"name")
       forall aux. Name -> Raw -> Elab' aux ()
claim Name
nameHole (Name -> Raw
Var (String -> Name
reflm String
"TTName"))
       forall aux. Name -> Elab' aux ()
movelast Name
nameHole
       forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var Name
nameHole)
       forall aux. Elab' aux ()
solve

reflectBinder :: Binder Term -> Raw
reflectBinder :: Binder Term -> Raw
reflectBinder = forall a. ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
reflectBinderQuote [Name] -> Term -> Raw
reflectTTQuote (String -> Name
reflm String
"TT") []

reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
reflectBinderQuote :: forall a. ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
reflectBinderQuote [Name] -> a -> Raw
q Name
ty [Name]
unq (Lam RigCount
_ a
t)
   = String -> [Raw] -> Raw
reflCall String
"Lam" [Name -> Raw
Var Name
ty, [Name] -> a -> Raw
q [Name]
unq a
t]
reflectBinderQuote [Name] -> a -> Raw
q Name
ty [Name]
unq (Pi RigCount
_ Maybe ImplicitInfo
_ a
t a
k)
   = String -> [Raw] -> Raw
reflCall String
"Pi" [Name -> Raw
Var Name
ty, [Name] -> a -> Raw
q [Name]
unq a
t, [Name] -> a -> Raw
q [Name]
unq a
k]
reflectBinderQuote [Name] -> a -> Raw
q Name
ty [Name]
unq (Let RigCount
rc a
x a
y)
   = String -> [Raw] -> Raw
reflCall String
"Let" [Name -> Raw
Var Name
ty, [Name] -> a -> Raw
q [Name]
unq a
x, [Name] -> a -> Raw
q [Name]
unq a
y]
reflectBinderQuote [Name] -> a -> Raw
q Name
ty [Name]
unq (NLet a
x a
y)
   = String -> [Raw] -> Raw
reflCall String
"Let" [Name -> Raw
Var Name
ty, [Name] -> a -> Raw
q [Name]
unq a
x, [Name] -> a -> Raw
q [Name]
unq a
y]
reflectBinderQuote [Name] -> a -> Raw
q Name
ty [Name]
unq (Hole a
t)
   = String -> [Raw] -> Raw
reflCall String
"Hole" [Name -> Raw
Var Name
ty, [Name] -> a -> Raw
q [Name]
unq a
t]
reflectBinderQuote [Name] -> a -> Raw
q Name
ty [Name]
unq (GHole Int
_ [Name]
_ a
t)
   = String -> [Raw] -> Raw
reflCall String
"GHole" [Name -> Raw
Var Name
ty, [Name] -> a -> Raw
q [Name]
unq a
t]
reflectBinderQuote [Name] -> a -> Raw
q Name
ty [Name]
unq (Guess a
x a
y)
   = String -> [Raw] -> Raw
reflCall String
"Guess" [Name -> Raw
Var Name
ty, [Name] -> a -> Raw
q [Name]
unq a
x, [Name] -> a -> Raw
q [Name]
unq a
y]
reflectBinderQuote [Name] -> a -> Raw
q Name
ty [Name]
unq (PVar RigCount
_ a
t)
   = String -> [Raw] -> Raw
reflCall String
"PVar" [Name -> Raw
Var Name
ty, [Name] -> a -> Raw
q [Name]
unq a
t]
reflectBinderQuote [Name] -> a -> Raw
q Name
ty [Name]
unq (PVTy a
t)
   = String -> [Raw] -> Raw
reflCall String
"PVTy" [Name -> Raw
Var Name
ty, [Name] -> a -> Raw
q [Name]
unq a
t]

mkList :: Raw -> [Raw] -> Raw
mkList :: Raw -> [Raw] -> Raw
mkList Raw
ty []      = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Nil") [String
"List", String
"Prelude"])) Raw
ty
mkList Raw
ty (Raw
x:[Raw]
xs) = Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"::") [String
"List", String
"Prelude"])) Raw
ty)
                              Raw
x)
                        (Raw -> [Raw] -> Raw
mkList Raw
ty [Raw]
xs)

reflectConstant :: Const -> Raw
reflectConstant :: Const -> Raw
reflectConstant c :: Const
c@(I  Int
_) = String -> [Raw] -> Raw
reflCall String
"I"  [Const -> Raw
RConstant Const
c]
reflectConstant c :: Const
c@(BI Integer
_) = String -> [Raw] -> Raw
reflCall String
"BI" [Const -> Raw
RConstant Const
c]
reflectConstant c :: Const
c@(Fl Double
_) = String -> [Raw] -> Raw
reflCall String
"Fl" [Const -> Raw
RConstant Const
c]
reflectConstant c :: Const
c@(Ch Char
_) = String -> [Raw] -> Raw
reflCall String
"Ch" [Const -> Raw
RConstant Const
c]
reflectConstant c :: Const
c@(Str String
_) = String -> [Raw] -> Raw
reflCall String
"Str" [Const -> Raw
RConstant Const
c]
reflectConstant c :: Const
c@(B8 Word8
_) = String -> [Raw] -> Raw
reflCall String
"B8" [Const -> Raw
RConstant Const
c]
reflectConstant c :: Const
c@(B16 Word16
_) = String -> [Raw] -> Raw
reflCall String
"B16" [Const -> Raw
RConstant Const
c]
reflectConstant c :: Const
c@(B32 Word32
_) = String -> [Raw] -> Raw
reflCall String
"B32" [Const -> Raw
RConstant Const
c]
reflectConstant c :: Const
c@(B64 Word64
_) = String -> [Raw] -> Raw
reflCall String
"B64" [Const -> Raw
RConstant Const
c]
reflectConstant (AType (ATInt IntTy
ITNative)) = String -> [Raw] -> Raw
reflCall String
"AType" [String -> [Raw] -> Raw
reflCall String
"ATInt" [Name -> Raw
Var (String -> Name
reflm String
"ITNative")]]
reflectConstant (AType (ATInt IntTy
ITBig)) = String -> [Raw] -> Raw
reflCall String
"AType" [String -> [Raw] -> Raw
reflCall String
"ATInt" [Name -> Raw
Var (String -> Name
reflm String
"ITBig")]]
reflectConstant (AType ArithTy
ATFloat) = String -> [Raw] -> Raw
reflCall String
"AType" [Name -> Raw
Var (String -> Name
reflm String
"ATDouble")]
reflectConstant (AType (ATInt IntTy
ITChar)) = String -> [Raw] -> Raw
reflCall String
"AType" [String -> [Raw] -> Raw
reflCall String
"ATInt" [Name -> Raw
Var (String -> Name
reflm String
"ITChar")]]
reflectConstant Const
StrType = Name -> Raw
Var (String -> Name
reflm String
"StrType")
reflectConstant (AType (ATInt (ITFixed NativeTy
IT8)))  = String -> [Raw] -> Raw
reflCall String
"AType" [String -> [Raw] -> Raw
reflCall String
"ATInt" [String -> [Raw] -> Raw
reflCall String
"ITFixed" [Name -> Raw
Var (String -> Name
reflm String
"IT8")]]]
reflectConstant (AType (ATInt (ITFixed NativeTy
IT16))) = String -> [Raw] -> Raw
reflCall String
"AType" [String -> [Raw] -> Raw
reflCall String
"ATInt" [String -> [Raw] -> Raw
reflCall String
"ITFixed" [Name -> Raw
Var (String -> Name
reflm String
"IT16")]]]
reflectConstant (AType (ATInt (ITFixed NativeTy
IT32))) = String -> [Raw] -> Raw
reflCall String
"AType" [String -> [Raw] -> Raw
reflCall String
"ATInt" [String -> [Raw] -> Raw
reflCall String
"ITFixed" [Name -> Raw
Var (String -> Name
reflm String
"IT32")]]]
reflectConstant (AType (ATInt (ITFixed NativeTy
IT64))) = String -> [Raw] -> Raw
reflCall String
"AType" [String -> [Raw] -> Raw
reflCall String
"ATInt" [String -> [Raw] -> Raw
reflCall String
"ITFixed" [Name -> Raw
Var (String -> Name
reflm String
"IT64")]]]
reflectConstant Const
VoidType = Name -> Raw
Var (String -> Name
reflm String
"VoidType")
reflectConstant Const
Forgot = Name -> Raw
Var (String -> Name
reflm String
"Forgot")
reflectConstant Const
WorldType = Name -> Raw
Var (String -> Name
reflm String
"WorldType")
reflectConstant Const
TheWorld = Name -> Raw
Var (String -> Name
reflm String
"TheWorld")

reflectUExp :: UExp -> Raw
reflectUExp :: UExp -> Raw
reflectUExp (UVar String
ns Int
i) = String -> [Raw] -> Raw
reflCall String
"UVar" [Const -> Raw
RConstant (String -> Const
Str String
ns), Const -> Raw
RConstant (Int -> Const
I Int
i)]
reflectUExp (UVal Int
i) = String -> [Raw] -> Raw
reflCall String
"UVal" [Const -> Raw
RConstant (Int -> Const
I Int
i)]

-- | Reflect the environment of a proof into a List (TTName, Binder TT)
reflectEnv :: Env -> Raw
reflectEnv :: Env -> Raw
reflectEnv = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name, Binder Term) -> Raw -> Raw
consToEnvList Raw
emptyEnvList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {b1} {b2}. [(a, b1, b2)] -> [(a, b2)]
envBinders
  where
    consToEnvList :: (Name, Binder Term) -> Raw -> Raw
    consToEnvList :: (Name, Binder Term) -> Raw -> Raw
consToEnvList (Name
n, Binder Term
b) Raw
l
      = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"::") [String
"List", String
"Prelude"]))
                  [ Raw
envTupleType
                  , Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var Name
pairCon) [ (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TTName")
                                            , (Raw -> Raw -> Raw
RApp (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"Binder")
                                                    (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TT"))
                                            , Name -> Raw
reflectName Name
n
                                            , Binder Term -> Raw
reflectBinder Binder Term
b
                                            ]
                  , Raw
l
                  ]

    emptyEnvList :: Raw
    emptyEnvList :: Raw
emptyEnvList = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Nil") [String
"List", String
"Prelude"]))
                             [Raw
envTupleType]

-- Reflected environments don't get the RigCount (for the moment, at least)
reifyEnv :: Term -> ElabD Env
reifyEnv :: Term -> ElabD Env
reifyEnv Term
tm = do [(Name, Binder Term)]
preEnv <- forall a. (Term -> ElabD a) -> Term -> ElabD [a]
reifyList (forall a b.
(Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyPair Term -> ElabD Name
reifyTTName (forall a. (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinder Term -> ElabD Term
reifyTT (String -> Name
reflm String
"TT"))) Term
tm
                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Binder Term
b) -> (Name
n, RigCount
RigW, Binder Term
b)) [(Name, Binder Term)]
preEnv

-- | Reflect an error into the internal datatype of Idris -- TODO
rawBool :: Bool -> Raw
rawBool :: Bool -> Raw
rawBool Bool
True  = Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"True") [String
"Bool", String
"Prelude"])
rawBool Bool
False = Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"False") [String
"Bool", String
"Prelude"])

rawNil :: Raw -> Raw
rawNil :: Raw -> Raw
rawNil Raw
ty = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Nil") [String
"List", String
"Prelude"])) [Raw
ty]

rawCons :: Raw -> Raw -> Raw -> Raw
rawCons :: Raw -> Raw -> Raw -> Raw
rawCons Raw
ty Raw
hd Raw
tl = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"::") [String
"List", String
"Prelude"])) [Raw
ty, Raw
hd, Raw
tl]

rawList :: Raw -> [Raw] -> Raw
rawList :: Raw -> [Raw] -> Raw
rawList Raw
ty = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Raw -> Raw -> Raw -> Raw
rawCons Raw
ty) (Raw -> Raw
rawNil Raw
ty)

rawPairTy :: Raw -> Raw -> Raw
rawPairTy :: Raw -> Raw -> Raw
rawPairTy Raw
t1 Raw
t2 = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var Name
pairTy) [Raw
t1, Raw
t2]

rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
rawPair (Raw
a, Raw
b) (Raw
x, Raw
y) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var Name
pairCon) [Raw
a, Raw
b, Raw
x, Raw
y]

-- | Idris tuples nest to the right
rawTripleTy :: Raw -> Raw -> Raw -> Raw
rawTripleTy :: Raw -> Raw -> Raw -> Raw
rawTripleTy Raw
a Raw
b Raw
c = Raw -> Raw -> Raw
rawPairTy Raw
a (Raw -> Raw -> Raw
rawPairTy Raw
b Raw
c)

rawTriple :: (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw
rawTriple :: (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw
rawTriple (Raw
a, Raw
b, Raw
c) (Raw
x, Raw
y, Raw
z) = (Raw, Raw) -> (Raw, Raw) -> Raw
rawPair (Raw
a, Raw -> Raw -> Raw
rawPairTy Raw
b Raw
c) (Raw
x, (Raw, Raw) -> (Raw, Raw) -> Raw
rawPair (Raw
b, Raw
c) (Raw
y, Raw
z))

reflectCtxt :: [(Name, Type)] -> Raw
reflectCtxt :: [(Name, Term)] -> Raw
reflectCtxt [(Name, Term)]
ctxt = Raw -> [Raw] -> Raw
rawList (Raw -> Raw -> Raw
rawPairTy  (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TTName") (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TT"))
                           (forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
t) -> ((Raw, Raw) -> (Raw, Raw) -> Raw
rawPair (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TTName", Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TT")
                                                      (Name -> Raw
reflectName Name
n, Term -> Raw
reflect Term
t)))
                                [(Name, Term)]
ctxt)

reflectErr :: Err -> Raw
reflectErr :: Err -> Raw
reflectErr (Msg String
msg) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"Msg") [Const -> Raw
RConstant (String -> Const
Str String
msg)]
reflectErr (InternalMsg String
msg) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"InternalMsg") [Const -> Raw
RConstant (String -> Const
Str String
msg)]
reflectErr (CantUnify Bool
b (Term
t1,Maybe Provenance
_) (Term
t2,Maybe Provenance
_) Err
e [(Name, Term)]
ctxt Int
i) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"CantUnify")
            [ Bool -> Raw
rawBool Bool
b
            , Term -> Raw
reflect Term
t1
            , Term -> Raw
reflect Term
t2
            , Err -> Raw
reflectErr Err
e
            , [(Name, Term)] -> Raw
reflectCtxt [(Name, Term)]
ctxt
            , Const -> Raw
RConstant (Int -> Const
I Int
i)]
reflectErr (InfiniteUnify Name
n Term
tm [(Name, Term)]
ctxt) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"InfiniteUnify")
            [ Name -> Raw
reflectName Name
n
            , Term -> Raw
reflect Term
tm
            , [(Name, Term)] -> Raw
reflectCtxt [(Name, Term)]
ctxt
            ]
reflectErr (CantConvert Term
t Term
t' [(Name, Term)]
ctxt) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"CantConvert")
            [ Term -> Raw
reflect Term
t
            , Term -> Raw
reflect Term
t'
            , [(Name, Term)] -> Raw
reflectCtxt [(Name, Term)]
ctxt
            ]
reflectErr (CantSolveGoal Term
t [(Name, Term)]
ctxt) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"CantSolveGoal")
            [ Term -> Raw
reflect Term
t
            , [(Name, Term)] -> Raw
reflectCtxt [(Name, Term)]
ctxt
            ]
reflectErr (UnifyScope Name
n Name
n' Term
t [(Name, Term)]
ctxt) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"UnifyScope")
            [ Name -> Raw
reflectName Name
n
            , Name -> Raw
reflectName Name
n'
            , Term -> Raw
reflect Term
t
            , [(Name, Term)] -> Raw
reflectCtxt [(Name, Term)]
ctxt
            ]
reflectErr (CantInferType String
str) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"CantInferType") [Const -> Raw
RConstant (String -> Const
Str String
str)]
reflectErr (NonFunctionType Term
t Term
t') =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"NonFunctionType") [Term -> Raw
reflect Term
t, Term -> Raw
reflect Term
t']
reflectErr (NotEquality Term
t Term
t') =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"NotEquality") [Term -> Raw
reflect Term
t, Term -> Raw
reflect Term
t']
reflectErr (TooManyArguments Name
n) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"TooManyArguments") [Name -> Raw
reflectName Name
n]
reflectErr (CantIntroduce Term
t) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"CantIntroduce") [Term -> Raw
reflect Term
t]
reflectErr (NoSuchVariable Name
n) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"NoSuchVariable") [Name -> Raw
reflectName Name
n]
reflectErr (WithFnType Term
t) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"WithFnType") [Term -> Raw
reflect Term
t]
reflectErr (CantMatch Term
t) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"CantMatch") [Term -> Raw
reflect Term
t]
reflectErr (NoTypeDecl Name
n) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"NoTypeDecl") [Name -> Raw
reflectName Name
n]
reflectErr (NotInjective Term
t1 Term
t2 Term
t3) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"NotInjective")
            [ Term -> Raw
reflect Term
t1
            , Term -> Raw
reflect Term
t2
            , Term -> Raw
reflect Term
t3
            ]
reflectErr (CantResolve Bool
_ Term
t Err
more)
   = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"CantResolve") [Term -> Raw
reflect Term
t, Err -> Raw
reflectErr Err
more]
reflectErr (InvalidTCArg Name
n Term
t) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"InvalidTCArg") [Name -> Raw
reflectName Name
n, Term -> Raw
reflect Term
t]
reflectErr (CantResolveAlts [Name]
ss) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"CantResolveAlts")
            [Raw -> [Raw] -> Raw
rawList (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TTName") (forall a b. (a -> b) -> [a] -> [b]
map Name -> Raw
reflectName [Name]
ss)]
reflectErr (IncompleteTerm Term
t) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"IncompleteTerm") [Term -> Raw
reflect Term
t]
reflectErr (UniverseError FC
fc UExp
ue (Int, Int)
old (Int, Int)
new [ConstraintFC]
tys) =
  -- NB: loses information, but OK because this is not likely to be rewritten
  Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"UniverseError"
reflectErr Err
ProgramLineComment = Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"ProgramLineComment"
reflectErr (Inaccessible Name
n) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"Inaccessible") [Name -> Raw
reflectName Name
n]
reflectErr (UnknownImplicit Name
n Name
f) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"UnknownImplicit") [Name -> Raw
reflectName Name
n, Name -> Raw
reflectName Name
f]
reflectErr (NonCollapsiblePostulate Name
n) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"NonCollabsiblePostulate") [Name -> Raw
reflectName Name
n]
reflectErr (AlreadyDefined Name
n) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"AlreadyDefined") [Name -> Raw
reflectName Name
n]
reflectErr (ProofSearchFail Err
e) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"ProofSearchFail") [Err -> Raw
reflectErr Err
e]
reflectErr (NoRewriting Term
l Term
r Term
tm) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"NoRewriting") [Term -> Raw
reflect Term
l, Term -> Raw
reflect Term
r, Term -> Raw
reflect Term
tm]
reflectErr (ProviderError String
str) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"ProviderError") [Const -> Raw
RConstant (String -> Const
Str String
str)]
reflectErr (LoadingFailed String
str Err
err) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflErrName String
"LoadingFailed") [Const -> Raw
RConstant (String -> Const
Str String
str)]
reflectErr Err
x = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Msg") [String
"Errors", String
"Reflection", String
"Language"])) [Const -> Raw
RConstant forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Const
Str forall a b. (a -> b) -> a -> b
$ String
"Default reflection: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Err
x]

-- | Reflect a file context
reflectFC :: FC -> Raw
reflectFC :: FC -> Raw
reflectFC FC
fc = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (String -> Name
reflm String
"FileLoc"))
                         [ Const -> Raw
RConstant (String -> Const
Str (FC -> String
fc_fname FC
fc))
                         , Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var Name
pairCon) forall a b. (a -> b) -> a -> b
$
                             [Raw
intTy, Raw
intTy] forall a. [a] -> [a] -> [a]
++
                             forall a b. (a -> b) -> [a] -> [b]
map (Const -> Raw
RConstant forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I)
                                 [ forall a b. (a, b) -> a
fst (FC -> (Int, Int)
fc_start FC
fc)
                                 , forall a b. (a, b) -> b
snd (FC -> (Int, Int)
fc_start FC
fc)
                                 ]
                         , Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var Name
pairCon) forall a b. (a -> b) -> a -> b
$
                             [Raw
intTy, Raw
intTy] forall a. [a] -> [a] -> [a]
++
                             forall a b. (a -> b) -> [a] -> [b]
map (Const -> Raw
RConstant forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I)
                                 [ forall a b. (a, b) -> a
fst (FC -> (Int, Int)
fc_end FC
fc)
                                 , forall a b. (a, b) -> b
snd (FC -> (Int, Int)
fc_end FC
fc)
                                 ]
                         ]
  where intTy :: Raw
intTy = Const -> Raw
RConstant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITNative))

reifyFC :: Term -> ElabD FC
reifyFC :: Term -> ElabD FC
reifyFC Term
tm
  | (P (DCon Int
_ Int
_ Bool
_) Name
cn Term
_, [Constant (Str String
fn), Term
st, Term
end]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
tm
  , Name
cn forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"FileLoc" = String -> (Int, Int) -> (Int, Int) -> FC
FC String
fn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b.
(Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyPair Term -> ElabD Int
reifyInt Term -> ElabD Int
reifyInt Term
st forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a b.
(Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyPair Term -> ElabD Int
reifyInt Term -> ElabD Int
reifyInt Term
end
  | Bool
otherwise = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Not a source location: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm

fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
fromTTMaybe :: Term -> Maybe Term
fromTTMaybe (App AppStatus Name
_ (App AppStatus Name
_ (P (DCon Int
_ Int
_ Bool
_) (NS (UN Text
just) [Text]
_) Term
_) Term
ty) Term
tm)
  | Text
just forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Just" = forall a. a -> Maybe a
Just Term
tm
fromTTMaybe Term
x          = forall a. Maybe a
Nothing

reflErrName :: String -> Name
reflErrName :: String -> Name
reflErrName String
n = Name -> [String] -> Name
sNS (String -> Name
sUN String
n) [String
"Errors", String
"Reflection", String
"Language"]

-- | Attempt to reify a report part from TT to the internal
-- representation. Not in Idris or ElabD monads because it should be usable
-- from either.
reifyReportPart :: Term -> Either Err ErrorReportPart
reifyReportPart :: Term -> Either Err ErrorReportPart
reifyReportPart (App AppStatus Name
_ (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_) (Constant (Str String
msg))) | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"TextPart" =
    forall a b. b -> Either a b
Right (String -> ErrorReportPart
TextPart String
msg)
reifyReportPart (App AppStatus Name
_ (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_) Term
ttn)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"NamePart" =
    case forall aux a.
aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
runElab EState
initEState (Term -> ElabD Name
reifyTTName Term
ttn) (Name
-> String -> Context -> Ctxt TypeInfo -> Int -> Term -> ProofState
initElaborator (Int -> String -> Name
sMN Int
0 String
"hole") String
internalNS Context
initContext forall {k} {a}. Map k a
emptyContext Int
0 forall n. TT n
Erased) of
      Error Err
e -> forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
InternalMsg forall a b. (a -> b) -> a -> b
$
       String
"could not reify name term " forall a. [a] -> [a] -> [a]
++
       forall a. Show a => a -> String
show Term
ttn forall a. [a] -> [a] -> [a]
++
       String
" when reflecting an error:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Err
e
      OK (Name
n', ElabState EState
_)-> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ Name -> ErrorReportPart
NamePart Name
n'
reifyReportPart (App AppStatus Name
_ (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_) Term
tm)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"TermPart" =
  case forall aux a.
aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
runElab EState
initEState (Term -> ElabD Term
reifyTT Term
tm) (Name
-> String -> Context -> Ctxt TypeInfo -> Int -> Term -> ProofState
initElaborator (Int -> String -> Name
sMN Int
0 String
"hole") String
internalNS Context
initContext forall {k} {a}. Map k a
emptyContext Int
0 forall n. TT n
Erased) of
    Error Err
e -> forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
InternalMsg forall a b. (a -> b) -> a -> b
$
      String
"could not reify reflected term " forall a. [a] -> [a] -> [a]
++
      forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++
      String
" when reflecting an error:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Err
e
    OK (Term
tm', ElabState EState
_) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ Term -> ErrorReportPart
TermPart Term
tm'
reifyReportPart (App AppStatus Name
_ (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_) Term
tm)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"RawPart" =
  case forall aux a.
aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
runElab EState
initEState (Term -> ElabD Raw
reifyRaw Term
tm) (Name
-> String -> Context -> Ctxt TypeInfo -> Int -> Term -> ProofState
initElaborator (Int -> String -> Name
sMN Int
0 String
"hole") String
internalNS Context
initContext forall {k} {a}. Map k a
emptyContext Int
0 forall n. TT n
Erased) of
    Error Err
e -> forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
InternalMsg forall a b. (a -> b) -> a -> b
$
      String
"could not reify reflected raw term " forall a. [a] -> [a] -> [a]
++
      forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++
      String
" when reflecting an error: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Err
e
    OK (Raw
tm', ElabState EState
_) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ Raw -> ErrorReportPart
RawPart Raw
tm'
reifyReportPart (App AppStatus Name
_ (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_) Term
tm)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"SubReport" =
  case Term -> Maybe [Term]
unList Term
tm of
    Just [Term]
xs -> do [ErrorReportPart]
subParts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> Either Err ErrorReportPart
reifyReportPart [Term]
xs
                  forall a b. b -> Either a b
Right ([ErrorReportPart] -> ErrorReportPart
SubReport [ErrorReportPart]
subParts)
    Maybe [Term]
Nothing -> forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
InternalMsg forall a b. (a -> b) -> a -> b
$ String
"could not reify subreport " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm
reifyReportPart Term
x = forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
InternalMsg forall a b. (a -> b) -> a -> b
$ String
"could not reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
x

reifyErasure :: Term -> ElabD RErasure
reifyErasure :: Term -> ElabD RErasure
reifyErasure (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"Erased" = forall (m :: * -> *) a. Monad m => a -> m a
return RErasure
RErased
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"NotErased" = forall (m :: * -> *) a. Monad m => a -> m a
return RErasure
RNotErased
reifyErasure Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Can't reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++ String
" as erasure info."

reifyPlicity :: Term -> ElabD RPlicity
reifyPlicity :: Term -> ElabD RPlicity
reifyPlicity (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"Explicit" = forall (m :: * -> *) a. Monad m => a -> m a
return RPlicity
RExplicit
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"Implicit" = forall (m :: * -> *) a. Monad m => a -> m a
return RPlicity
RImplicit
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"Constraint" = forall (m :: * -> *) a. Monad m => a -> m a
return RPlicity
RConstraint
reifyPlicity Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++ String
" as RPlicity."

reifyRFunArg :: Term -> ElabD RFunArg
reifyRFunArg :: Term -> ElabD RFunArg
reifyRFunArg (App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_) Term
argN) Term
argTy) Term
argPl) Term
argE)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"MkFunArg" = forall (m :: * -> *) a1 a2 a3 a4 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
liftM4 Name -> Raw -> RPlicity -> RErasure -> RFunArg
RFunArg
                             (Term -> ElabD Name
reifyTTName Term
argN)
                             (Term -> ElabD Raw
reifyRaw Term
argTy)
                             (Term -> ElabD RPlicity
reifyPlicity Term
argPl)
                             (Term -> ElabD RErasure
reifyErasure Term
argE)
reifyRFunArg Term
aTm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
aTm forall a. [a] -> [a] -> [a]
++ String
" as an RArg."

reifyTyDecl :: Term -> ElabD RTyDecl
reifyTyDecl :: Term -> ElabD RTyDecl
reifyTyDecl (App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_) Term
tyN) Term
args) Term
ret)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"Declare" =
  do Name
tyN'  <- Term -> ElabD Name
reifyTTName Term
tyN
     [RFunArg]
args' <- case Term -> Maybe [Term]
unList Term
args of
                Maybe [Term]
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
args forall a. [a] -> [a] -> [a]
++ String
" as an arglist."
                Just [Term]
xs -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> ElabD RFunArg
reifyRFunArg [Term]
xs
     Raw
ret'  <- Term -> ElabD Raw
reifyRaw Term
ret
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> [RFunArg] -> Raw -> RTyDecl
RDeclare Name
tyN' [RFunArg]
args' Raw
ret'
reifyTyDecl Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++ String
" as a type declaration."

reifyFunDefn :: Term -> ElabD (RFunDefn Raw)
reifyFunDefn :: Term -> ElabD (RFunDefn Raw)
reifyFunDefn (App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (P NameType
_ Name
n Term
_) (P NameType
_ Name
t Term
_)) Term
fnN) Term
clauses)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"DefineFun" Bool -> Bool -> Bool
&& Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Raw" =
  do Name
fnN' <- Term -> ElabD Name
reifyTTName Term
fnN
     [RFunClause Raw]
clauses' <- case Term -> Maybe [Term]
unList Term
clauses of
                   Maybe [Term]
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
clauses forall a. [a] -> [a] -> [a]
++ String
" as a clause list"
                   Just [Term]
cs -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> ElabD (RFunClause Raw)
reifyC [Term]
cs
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Name -> [RFunClause a] -> RFunDefn a
RDefineFun Name
fnN' [RFunClause Raw]
clauses'
  where reifyC :: Term -> ElabD (RFunClause Raw)
        reifyC :: Term -> ElabD (RFunClause Raw)
reifyC (App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_) (P NameType
_ Name
t Term
_)) Term
lhs) Term
rhs)
          | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"MkFunClause" Bool -> Bool -> Bool
&& Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Raw" = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. a -> a -> RFunClause a
RMkFunClause
                                             (Term -> ElabD Raw
reifyRaw Term
lhs)
                                             (Term -> ElabD Raw
reifyRaw Term
rhs)
        reifyC (App AppStatus Name
_ (App AppStatus Name
_ (P (DCon Int
_ Int
_ Bool
_) Name
n Term
_) (P NameType
_ Name
t Term
_)) Term
lhs)
          | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"MkImpossibleClause" Bool -> Bool -> Bool
&& Name
t forall a. Eq a => a -> a -> Bool
== String -> Name
reflm String
"Raw" = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> RFunClause a
RMkImpossibleClause forall a b. (a -> b) -> a -> b
$ Term -> ElabD Raw
reifyRaw Term
lhs
        reifyC Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++ String
" as a clause."
reifyFunDefn Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++ String
" as a function declaration."

reifyRConstructorDefn :: Term -> ElabD RConstructorDefn
reifyRConstructorDefn :: Term -> ElabD RConstructorDefn
reifyRConstructorDefn (App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (P NameType
_ Name
n Term
_) Term
cn) Term
args) Term
retTy)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"Constructor", Just [Term]
args' <- Term -> Maybe [Term]
unList Term
args
  = Name -> [RFunArg] -> Raw -> RConstructorDefn
RConstructor forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD Name
reifyTTName Term
cn forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> ElabD RFunArg
reifyRFunArg [Term]
args' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> ElabD Raw
reifyRaw Term
retTy
reifyRConstructorDefn Term
aTm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
aTm forall a. [a] -> [a] -> [a]
++ String
" as an RConstructorDefn"

reifyRDataDefn :: Term -> ElabD RDataDefn
reifyRDataDefn :: Term -> ElabD RDataDefn
reifyRDataDefn (App AppStatus Name
_ (App AppStatus Name
_ (P NameType
_ Name
n Term
_) Term
tyn) Term
ctors)
  | Name
n forall a. Eq a => a -> a -> Bool
== String -> Name
tacN String
"DefineDatatype", Just [Term]
ctors' <- Term -> Maybe [Term]
unList Term
ctors
  = Name -> [RConstructorDefn] -> RDataDefn
RDefineDatatype forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD Name
reifyTTName Term
tyn forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> ElabD RConstructorDefn
reifyRConstructorDefn [Term]
ctors'
reifyRDataDefn Term
aTm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Couldn't reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
aTm forall a. [a] -> [a] -> [a]
++ String
" as an RDataDefn"

envTupleType :: Raw
envTupleType :: Raw
envTupleType
  = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var Name
pairTy) [ (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TTName")
                           , (Raw -> Raw -> Raw
RApp (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"Binder") (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TT"))
                           ]

reflectList :: Raw -> [Raw] -> Raw
reflectList :: Raw -> [Raw] -> Raw
reflectList Raw
ty []     = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Nil") [String
"List", String
"Prelude"])) Raw
ty
reflectList Raw
ty (Raw
x:[Raw]
xs) = Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"::") [String
"List", String
"Prelude"])) Raw
ty)
                                   Raw
x)
                             (Raw -> [Raw] -> Raw
reflectList Raw
ty [Raw]
xs)

-- | Apply Idris's implicit info to get a signature. The [PArg] should
-- come from a lookup in idris_implicits on IState.
getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)
getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)
getArgs []     Raw
r = ([], Raw
r)
getArgs (PArg
a:[PArg]
as) (RBind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Raw
ty Raw
_) Raw
sc) =
  let ([RFunArg]
args, Raw
res) = [PArg] -> Raw -> ([RFunArg], Raw)
getArgs [PArg]
as Raw
sc
      erased :: RErasure
erased = if ArgOpt
InaccessibleArg forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall t. PArg' t -> [ArgOpt]
argopts PArg
a then RErasure
RErased else RErasure
RNotErased
      arg' :: RFunArg
arg' = case PArg
a of
               PImp {} -> Name -> Raw -> RPlicity -> RErasure -> RFunArg
RFunArg Name
n Raw
ty RPlicity
RImplicit RErasure
erased
               PExp {} -> Name -> Raw -> RPlicity -> RErasure -> RFunArg
RFunArg Name
n Raw
ty RPlicity
RExplicit RErasure
erased
               PConstraint {} -> Name -> Raw -> RPlicity -> RErasure -> RFunArg
RFunArg Name
n Raw
ty RPlicity
RConstraint RErasure
erased
               PTacImplicit {} -> Name -> Raw -> RPlicity -> RErasure -> RFunArg
RFunArg Name
n Raw
ty RPlicity
RImplicit RErasure
erased
  in (RFunArg
arg'forall a. a -> [a] -> [a]
:[RFunArg]
args, Raw
res)
getArgs [PArg]
_ Raw
r = ([], Raw
r)

unApplyRaw :: Raw -> (Raw, [Raw])
unApplyRaw :: Raw -> (Raw, [Raw])
unApplyRaw Raw
tm = [Raw] -> Raw -> (Raw, [Raw])
ua [] Raw
tm
  where
    ua :: [Raw] -> Raw -> (Raw, [Raw])
ua [Raw]
args (RApp Raw
f Raw
a) = [Raw] -> Raw -> (Raw, [Raw])
ua (Raw
aforall a. a -> [a] -> [a]
:[Raw]
args) Raw
f
    ua [Raw]
args Raw
t         = (Raw
t, [Raw]
args)

-- | Build the reflected function definition(s) that correspond(s) to
-- a provided unqualified name
buildFunDefns :: IState -> Name -> [RFunDefn Term]
buildFunDefns :: IState -> Name -> [RFunDefn Term]
buildFunDefns IState
ist Name
n =
  [ forall {a}. Name -> [([(a, TT a)], TT a, TT a)] -> RFunDefn (TT a)
mkFunDefn Name
name [([(Name, Term)], Term, Term)]
clauses
  | (Name
name, ([([(Name, Term)], Term, Term)]
clauses, [PTerm]
_)) <- forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n forall a b. (a -> b) -> a -> b
$ IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
ist
  ]

  where mkFunDefn :: Name -> [([(a, TT a)], TT a, TT a)] -> RFunDefn (TT a)
mkFunDefn Name
name [([(a, TT a)], TT a, TT a)]
clauses = forall a. Name -> [RFunClause a] -> RFunDefn a
RDefineFun Name
name (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. ([(a, TT a)], TT a, TT a) -> RFunClause (TT a)
mkFunClause [([(a, TT a)], TT a, TT a)]
clauses)

        mkFunClause :: ([(a, TT a)], TT a, TT a) -> RFunClause (TT a)
mkFunClause ([], TT a
lhs, TT a
Impossible) = forall a. a -> RFunClause a
RMkImpossibleClause TT a
lhs
        mkFunClause ([], TT a
lhs, TT a
rhs) = forall a. a -> a -> RFunClause a
RMkFunClause TT a
lhs TT a
rhs
        mkFunClause (((a
n, TT a
ty) : [(a, TT a)]
ns), TT a
lhs, TT a
rhs) = ([(a, TT a)], TT a, TT a) -> RFunClause (TT a)
mkFunClause ([(a, TT a)]
ns, TT a -> TT a
bind TT a
lhs, TT a -> TT a
bind TT a
rhs) where
          bind :: TT a -> TT a
bind TT a
Impossible = forall n. TT n
Impossible
          bind TT a
tm = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind a
n (forall b. RigCount -> b -> Binder b
PVar RigCount
RigW TT a
ty) TT a
tm

-- | Build the reflected datatype definition(s) that correspond(s) to
-- a provided unqualified name
buildDatatypes :: IState -> Name -> [RDatatype]
buildDatatypes :: IState -> Name -> [RDatatype]
buildDatatypes IState
ist Name
n =
  forall a. [Maybe a] -> [a]
catMaybes [ Name -> TypeInfo -> Maybe RDatatype
mkDataType Name
dn TypeInfo
ti
            | (Name
dn, TypeInfo
ti) <- forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n Ctxt TypeInfo
datatypes
            ]
  where datatypes :: Ctxt TypeInfo
datatypes = IState -> Ctxt TypeInfo
idris_datatypes IState
ist
        ctxt :: Context
ctxt      = IState -> Context
tt_ctxt IState
ist
        impls :: Ctxt [PArg]
impls     = IState -> Ctxt [PArg]
idris_implicits IState
ist

        ctorSig :: [Int] -> Name -> Maybe (Name, [RCtorArg], Raw)
ctorSig [Int]
params Name
cn = do Raw
cty <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Raw
forget (Name -> Context -> Maybe Term
lookupTyExact Name
cn Context
ctxt)
                               [PArg]
argInfo <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
cn Ctxt [PArg]
impls
                               let ([RFunArg]
args, Raw
res) = [PArg] -> Raw -> ([RFunArg], Raw)
getArgs [PArg]
argInfo Raw
cty
                               forall (m :: * -> *) a. Monad m => a -> m a
return (Name
cn, [RFunArg] -> Raw -> [Int] -> [RCtorArg]
ctorArgsStatus [RFunArg]
args Raw
res [Int]
params, Raw
res)

        argPos :: Name -> [RFunArg] -> Raw -> Maybe Int
argPos Name
n [] Raw
res = Name -> Raw -> Maybe Int
findPos Name
n Raw
res
          where findPos :: Name -> Raw -> Maybe Int
findPos Name
n Raw
app = case Raw -> (Raw, [Raw])
unApplyRaw Raw
app of
                                  (Raw
_, [Raw]
argL) -> forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex (forall a. Eq a => a -> a -> Bool
== Name -> Raw
Var Name
n) [Raw]
argL
        argPos Name
n (RFunArg
arg:[RFunArg]
args) Raw
res = if Name
n forall a. Eq a => a -> a -> Bool
== RFunArg -> Name
argName RFunArg
arg
                                     then forall a. Maybe a
Nothing
                                     else Name -> [RFunArg] -> Raw -> Maybe Int
argPos Name
n [RFunArg]
args Raw
res

        ctorArgsStatus :: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
        ctorArgsStatus :: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
ctorArgsStatus [] Raw
_ [Int]
_ = []
        ctorArgsStatus (RFunArg
arg:[RFunArg]
args) Raw
res [Int]
params =
          case Name -> [RFunArg] -> Raw -> Maybe Int
argPos (RFunArg -> Name
argName RFunArg
arg) [RFunArg]
args Raw
res of
            Maybe Int
Nothing -> RFunArg -> RCtorArg
RCtorField RFunArg
arg forall a. a -> [a] -> [a]
: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
ctorArgsStatus [RFunArg]
args Raw
res [Int]
params
            Just Int
i -> if Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
params
                         then RFunArg -> RCtorArg
RCtorParameter RFunArg
arg forall a. a -> [a] -> [a]
: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
ctorArgsStatus [RFunArg]
args Raw
res [Int]
params
                         else RFunArg -> RCtorArg
RCtorField RFunArg
arg forall a. a -> [a] -> [a]
: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
ctorArgsStatus [RFunArg]
args Raw
res [Int]
params

        mkDataType :: Name -> TypeInfo -> Maybe RDatatype
mkDataType Name
name (TI {param_pos :: TypeInfo -> [Int]
param_pos = [Int]
params, con_names :: TypeInfo -> [Name]
con_names = [Name]
constrs}) =
          do (TyDecl (TCon Int
_ Int
_) Term
ty) <- Name -> Context -> Maybe Def
lookupDefExact Name
name Context
ctxt
             [PArg]
implInfo <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
name Ctxt [PArg]
impls
             let ([RTyConArg]
tcargs, Raw
tcres) = [Int] -> [PArg] -> Raw -> ([RTyConArg], Raw)
getTCArgs [Int]
params [PArg]
implInfo (Term -> Raw
forget Term
ty)
             [(Name, [RCtorArg], Raw)]
ctors <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Int] -> Name -> Maybe (Name, [RCtorArg], Raw)
ctorSig [Int]
params) [Name]
constrs
             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name
-> [RTyConArg] -> Raw -> [(Name, [RCtorArg], Raw)] -> RDatatype
RDatatype Name
name [RTyConArg]
tcargs Raw
tcres [(Name, [RCtorArg], Raw)]
ctors

        getTCArgs :: [Int] -> [PArg] -> Raw -> ([RTyConArg], Raw)
        getTCArgs :: [Int] -> [PArg] -> Raw -> ([RTyConArg], Raw)
getTCArgs [Int]
params [PArg]
implInfo Raw
tcTy =
          let ([RFunArg]
args, Raw
res) = [PArg] -> Raw -> ([RFunArg], Raw)
getArgs [PArg]
implInfo Raw
tcTy
          in ([RFunArg] -> Int -> [RTyConArg]
tcArg [RFunArg]
args Int
0, Raw
res)
            where tcArg :: [RFunArg] -> Int -> [RTyConArg]
tcArg [] Int
_ = []
                  tcArg (RFunArg
arg:[RFunArg]
args) Int
i | Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
params = RFunArg -> RTyConArg
RParameter RFunArg
arg forall a. a -> [a] -> [a]
: [RFunArg] -> Int -> [RTyConArg]
tcArg [RFunArg]
args (Int
iforall a. Num a => a -> a -> a
+Int
1)
                                     | Bool
otherwise       = RFunArg -> RTyConArg
RIndex RFunArg
arg forall a. a -> [a] -> [a]
: [RFunArg] -> Int -> [RTyConArg]
tcArg [RFunArg]
args (Int
iforall a. Num a => a -> a -> a
+Int
1)


reflectErasure :: RErasure -> Raw
reflectErasure :: RErasure -> Raw
reflectErasure RErasure
RErased    = Name -> Raw
Var (String -> Name
tacN String
"Erased")
reflectErasure RErasure
RNotErased = Name -> Raw
Var (String -> Name
tacN String
"NotErased")

reflectPlicity :: RPlicity -> Raw
reflectPlicity :: RPlicity -> Raw
reflectPlicity RPlicity
RExplicit = Name -> Raw
Var (String -> Name
tacN String
"Explicit")
reflectPlicity RPlicity
RImplicit = Name -> Raw
Var (String -> Name
tacN String
"Implicit")
reflectPlicity RPlicity
RConstraint = Name -> Raw
Var (String -> Name
tacN String
"Constraint")

reflectArg :: RFunArg -> Raw
reflectArg :: RFunArg -> Raw
reflectArg (RFunArg Name
n Raw
ty RPlicity
plic RErasure
erasure) =
  Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"MkFunArg") (Name -> Raw
reflectName Name
n))
                   (Raw -> Raw
reflectRaw Raw
ty))
              (RPlicity -> Raw
reflectPlicity RPlicity
plic))
       (RErasure -> Raw
reflectErasure RErasure
erasure)

reflectCtorArg :: RCtorArg -> Raw
reflectCtorArg :: RCtorArg -> Raw
reflectCtorArg (RCtorParameter RFunArg
arg) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"CtorParameter") (RFunArg -> Raw
reflectArg RFunArg
arg)
reflectCtorArg (RCtorField RFunArg
arg) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"CtorField") (RFunArg -> Raw
reflectArg RFunArg
arg)

reflectDatatype :: RDatatype -> Raw
reflectDatatype :: RDatatype -> Raw
reflectDatatype (RDatatype Name
tyn [RTyConArg]
tyConArgs Raw
tyConRes [(Name, [RCtorArg], Raw)]
constrs) =
  Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"MkDatatype") [ Name -> Raw
reflectName Name
tyn
                                      , Raw -> [Raw] -> Raw
rawList (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"TyConArg") (forall a b. (a -> b) -> [a] -> [b]
map RTyConArg -> Raw
reflectConArg [RTyConArg]
tyConArgs)
                                      , Raw -> Raw
reflectRaw Raw
tyConRes
                                      , Raw -> [Raw] -> Raw
rawList (Raw -> Raw -> Raw -> Raw
rawTripleTy (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TTName")
                                                             (Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"List") [String
"List", String
"Prelude"]))
                                                                   (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"CtorArg"))
                                                             (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"Raw"))
                                                [ (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw
rawTriple ((Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TTName")
                                                            ,(Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN String
"List") [String
"List", String
"Prelude"]))
                                                                   (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"CtorArg"))
                                                            ,(Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"Raw"))
                                                            (Name -> Raw
reflectName Name
cn
                                                            ,Raw -> [Raw] -> Raw
rawList (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"CtorArg")
                                                                     (forall a b. (a -> b) -> [a] -> [b]
map RCtorArg -> Raw
reflectCtorArg [RCtorArg]
cargs)
                                                            ,Raw -> Raw
reflectRaw Raw
cty)
                                                | (Name
cn, [RCtorArg]
cargs, Raw
cty) <- [(Name, [RCtorArg], Raw)]
constrs
                                                ]
                                      ]
  where reflectConArg :: RTyConArg -> Raw
reflectConArg (RParameter RFunArg
a) =
          Raw -> Raw -> Raw
RApp (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"TyConParameter") (RFunArg -> Raw
reflectArg RFunArg
a)
        reflectConArg (RIndex RFunArg
a) =
          Raw -> Raw -> Raw
RApp (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"TyConIndex") (RFunArg -> Raw
reflectArg RFunArg
a)

reflectFunClause :: RFunClause Term -> Raw
reflectFunClause :: RFunClause Term -> Raw
reflectFunClause (RMkFunClause Term
lhs Term
rhs)    = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"MkFunClause")
                                                     forall a b. (a -> b) -> a -> b
$ (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TT") forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Term -> Raw
reflect [ Term
lhs, Term
rhs ]

reflectFunClause (RMkImpossibleClause Term
lhs) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"MkImpossibleClause")
                                                       [ Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TT", Term -> Raw
reflect Term
lhs ]

reflectFunDefn :: RFunDefn Term -> Raw
reflectFunDefn :: RFunDefn Term -> Raw
reflectFunDefn (RDefineFun Name
name [RFunClause Term]
clauses) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"DefineFun")
                                                     [ Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TT"
                                                     , Name -> Raw
reflectName Name
name
                                                     , Raw -> [Raw] -> Raw
rawList (Raw -> Raw -> Raw
RApp (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
tacN String
"FunClause")
                                                                     (Name -> Raw
Var forall a b. (a -> b) -> a -> b
$ String -> Name
reflm String
"TT"))
                                                               (forall a b. (a -> b) -> [a] -> [b]
map RFunClause Term -> Raw
reflectFunClause [RFunClause Term]
clauses)
                                                     ]