{-|
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
(Int -> RErasure -> ShowS)
-> (RErasure -> String) -> ([RErasure] -> ShowS) -> Show RErasure
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
(Int -> RPlicity -> ShowS)
-> (RPlicity -> String) -> ([RPlicity] -> ShowS) -> Show RPlicity
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
(Int -> RFunArg -> ShowS)
-> (RFunArg -> String) -> ([RFunArg] -> ShowS) -> Show RFunArg
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
(Int -> RTyDecl -> ShowS)
-> (RTyDecl -> String) -> ([RTyDecl] -> ShowS) -> Show RTyDecl
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
(Int -> RTyConArg -> ShowS)
-> (RTyConArg -> String)
-> ([RTyConArg] -> ShowS)
-> Show RTyConArg
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
(Int -> RCtorArg -> ShowS)
-> (RCtorArg -> String) -> ([RCtorArg] -> ShowS) -> Show RCtorArg
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
(Int -> RDatatype -> ShowS)
-> (RDatatype -> String)
-> ([RDatatype] -> ShowS)
-> Show RDatatype
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 RErased = [ArgOpt
InaccessibleArg]
rArgOpts _ = []

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

data RFunClause a = RMkFunClause a a
                  | RMkImpossibleClause a
                  deriving Int -> RFunClause a -> ShowS
[RFunClause a] -> ShowS
RFunClause a -> String
(Int -> RFunClause a -> ShowS)
-> (RFunClause a -> String)
-> ([RFunClause a] -> ShowS)
-> Show (RFunClause a)
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
[RFunDefn a] -> ShowS
RFunDefn a -> String
(Int -> RFunDefn a -> ShowS)
-> (RFunDefn a -> String)
-> ([RFunDefn a] -> ShowS)
-> Show (RFunDefn a)
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 n :: String
n = Name -> [String] -> Name
sNS (String -> Name
sUN String
n) ["Reflection", "Language"]

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

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

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

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

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

reifyPair :: (Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyPair :: (Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyPair left :: Term -> ElabD a
left right :: Term -> ElabD b
right (App _ (App _ (App _ (App _ (P _ n :: Name
n _) _) _) x :: Term
x) y :: Term
y)
  | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pairCon = (a -> b -> (a, b)) -> ElabD a -> ElabD b -> ElabD (a, b)
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 left :: Term -> ElabD a
left right :: Term -> ElabD b
right tm :: Term
tm = String -> ElabD (a, b)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> ElabD (a, b)) -> String -> ElabD (a, b)
forall a b. (a -> b) -> a -> b
$ "Not a pair: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm

reifyList :: (Term -> ElabD a) -> Term -> ElabD [a]
reifyList :: (Term -> ElabD a) -> Term -> ElabD [a]
reifyList getElt :: Term -> ElabD a
getElt lst :: Term
lst =
  case Term -> Maybe [Term]
unList Term
lst of
    Nothing -> String -> ElabD [a]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Couldn't reify a list"
    Just xs :: [Term]
xs -> (Term -> ElabD a) -> [Term] -> ElabD [a]
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 -> StateT (ElabState EState) TC [ErrorReportPart]
reifyReportParts errs :: Term
errs =
  case Term -> Maybe [Term]
unList Term
errs of
    Nothing -> String -> StateT (ElabState EState) TC [ErrorReportPart]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Failed to reify errors"
    Just errs' :: [Term]
errs' ->
      let parts :: Either Err [ErrorReportPart]
parts = (Term -> Either Err ErrorReportPart)
-> [Term] -> Either Err [ErrorReportPart]
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
err -> String -> StateT (ElabState EState) TC [ErrorReportPart]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT (ElabState EState) TC [ErrorReportPart])
-> String -> StateT (ElabState EState) TC [ErrorReportPart]
forall a b. (a -> b) -> a -> b
$ "Couldn't reify \"Fail\" tactic - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
err
        Right errs'' :: [ErrorReportPart]
errs'' ->
          [ErrorReportPart] -> StateT (ElabState EState) TC [ErrorReportPart]
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 _ _ _)
        | (P _ f :: Name
f _, args :: [Term]
args) <- Term -> (Term, [Term])
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 _ n :: Name
n _)
        | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
reflm "Erased" = Term -> ElabD Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
forall n. TT n
Erased
reifyTT t :: Term
t@(P _ n :: Name
n _)
        | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
reflm "Impossible" = Term -> ElabD Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
forall n. TT n
Impossible
reifyTT t :: Term
t = String -> ElabD Term
forall (m :: * -> *) a. MonadFail m => String -> m a
fail ("Unknown reflection term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
t)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

reifyTTUExp :: Term -> ElabD UExp
reifyTTUExp :: Term -> StateT (ElabState EState) TC UExp
reifyTTUExp t :: Term
t@(App _ _ _)
  = case Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t of
      (P _ f :: Name
f _, [Constant (Str str :: String
str), Constant (I i :: Int
i)])
           | Name
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
reflm "UVar" -> UExp -> StateT (ElabState EState) TC UExp
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> StateT (ElabState EState) TC UExp)
-> UExp -> StateT (ElabState EState) TC UExp
forall a b. (a -> b) -> a -> b
$ String -> Int -> UExp
UVar String
str Int
i
      (P _ f :: Name
f _, [Constant (I i :: Int
i)])
           | Name
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
reflm "UVal" -> UExp -> StateT (ElabState EState) TC UExp
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> StateT (ElabState EState) TC UExp)
-> UExp -> StateT (ElabState EState) TC UExp
forall a b. (a -> b) -> a -> b
$ Int -> UExp
UVal Int
i
      _ -> String -> StateT (ElabState EState) TC UExp
forall (m :: * -> *) a. MonadFail m => String -> m a
fail ("Unknown reflection type universe expression: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
t)
reifyTTUExp t :: Term
t = String -> StateT (ElabState EState) TC UExp
forall (m :: * -> *) a. MonadFail m => String -> m a
fail ("Unknown reflection type universe expression: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
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 funName :: String
funName args :: [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 n :: Name
n ty :: Raw
ty = do Name
n' <- Name -> ElabD Name
forall aux. Name -> Elab' aux Name
getNameFrom Name
n
                  Name -> Raw -> Elab' EState ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
n' Raw
ty
                  Name -> ElabD Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'

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

reflectFixity :: Fixity -> Raw
reflectFixity :: Fixity -> Raw
reflectFixity (Infixl  p :: Int
p) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (String -> Name
tacN "Infixl")) (Int -> Raw
intToReflectedNat Int
p)
reflectFixity (Infixr  p :: Int
p) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (String -> Name
tacN "Infixr")) (Int -> Raw
intToReflectedNat Int
p)
reflectFixity (InfixN  p :: Int
p) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (String -> Name
tacN "InfixN")) (Int -> Raw
intToReflectedNat Int
p)
reflectFixity (PrefixN p :: Int
p) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (String -> Name
tacN "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 -> Elab' EState ()
reflectTTQuotePattern unq :: [Name]
unq (P _ n :: Name
n _)
  | Name
n Name -> [Name] -> Bool
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 Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var Name
n) ; Elab' EState ()
forall aux. Elab' aux ()
solve
  | Bool
otherwise =
    do Name
tyannot <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN 0 "pTyAnnot") (Name -> Raw
Var (String -> Name
reflm "TT"))
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
tyannot  -- use a _ pattern here
       Name
nt <- Name -> ElabD Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN 0 "nt")
       Name -> Raw -> Elab' EState ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
nt (Name -> Raw
Var (String -> Name
reflm "NameType"))
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
nt       -- use a _ pattern here
       Name
n' <- Name -> ElabD Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN 0 "n")
       Name -> Raw -> Elab' EState ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
n' (Name -> Raw
Var (String -> Name
reflm "TTName"))
       Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall "P" [Name -> Raw
Var Name
nt, Name -> Raw
Var Name
n', Name -> Raw
Var Name
tyannot]
       Elab' EState ()
forall aux. Elab' aux ()
solve
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
focus Name
n'; Name -> Elab' EState ()
reflectNameQuotePattern Name
n
reflectTTQuotePattern unq :: [Name]
unq (V n :: Int
n)
  = do Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall "V" [Const -> Raw
RConstant (Int -> Const
I Int
n)]
       Elab' EState ()
forall aux. Elab' aux ()
solve
reflectTTQuotePattern unq :: [Name]
unq (Bind n :: Name
n b :: Binder Term
b x :: Term
x)
  = do Name
x' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN 0 "sc") (Name -> Raw
Var (String -> Name
reflm "TT"))
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
x'
       Name
b' <- Name -> ElabD Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN 0 "binder")
       Name -> Raw -> Elab' EState ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
b' (Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN "Binder") ["Reflection", "Language"]))
                      (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN "TT") ["Reflection", "Language"])))
       if Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Term -> [Name]
forall n. Eq n => TT n -> [n]
freeNames Term
x
         then do Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall "Bind"
                                 [Name -> Raw
reflectName Name
n,
                                  Name -> Raw
Var Name
b',
                                  Name -> Raw
Var Name
x']
                 Elab' EState ()
forall aux. Elab' aux ()
solve
         else do Name
any <- Name -> ElabD Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN 0 "anyName")
                 Name -> Raw -> Elab' EState ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
any (Name -> Raw
Var (String -> Name
reflm "TTName"))
                 Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
any
                 Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall "Bind"
                                 [Name -> Raw
Var Name
any,
                                  Name -> Raw
Var Name
b',
                                  Name -> Raw
Var Name
x']
                 Elab' EState ()
forall aux. Elab' aux ()
solve
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
focus Name
x'; [Name] -> Term -> Elab' EState ()
reflectTTQuotePattern [Name]
unq Term
x
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
focus Name
b'; ([Name] -> Term -> Elab' EState ())
-> Raw -> [Name] -> Binder Term -> Elab' EState ()
forall a.
([Name] -> a -> Elab' EState ())
-> Raw -> [Name] -> Binder a -> Elab' EState ()
reflectBinderQuotePattern [Name] -> Term -> Elab' EState ()
reflectTTQuotePattern (Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
reflm "TT") [Name]
unq Binder Term
b
reflectTTQuotePattern unq :: [Name]
unq (App _ f :: Term
f x :: Term
x)
  = do Name
f' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN 0 "f") (Name -> Raw
Var (String -> Name
reflm "TT")) ; Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
f'
       Name
x' <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN 0 "x") (Name -> Raw
Var (String -> Name
reflm "TT")) ; Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
x'
       Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall "App" [Name -> Raw
Var Name
f', Name -> Raw
Var Name
x']
       Elab' EState ()
forall aux. Elab' aux ()
solve
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
focus Name
f'; [Name] -> Term -> Elab' EState ()
reflectTTQuotePattern [Name]
unq Term
f
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
focus Name
x'; [Name] -> Term -> Elab' EState ()
reflectTTQuotePattern [Name]
unq Term
x
reflectTTQuotePattern unq :: [Name]
unq (Constant c :: Const
c)
  = do Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall "TConst" [Const -> Raw
reflectConstant Const
c]
       Elab' EState ()
forall aux. Elab' aux ()
solve
reflectTTQuotePattern unq :: [Name]
unq (Proj t :: Term
t i :: Int
i)
  = TC () -> Elab' EState ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> Elab' EState ())
-> (String -> TC ()) -> String -> Elab' EState ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> (String -> Err) -> String -> TC ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
InternalMsg (String -> Elab' EState ()) -> String -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$
      "Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuotePattern unq :: [Name]
unq Erased
  = do Name
erased <- Name -> Raw -> ElabD Name
claimTy (Int -> String -> Name
sMN 0 "erased") (Name -> Raw
Var (String -> Name
reflm "TT"))
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
erased
       Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var Name
erased)
reflectTTQuotePattern unq :: [Name]
unq Impossible
  = TC () -> Elab' EState ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> Elab' EState ())
-> (String -> TC ()) -> String -> Elab' EState ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> (String -> Err) -> String -> TC ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
InternalMsg (String -> Elab' EState ()) -> String -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$
      "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuotePattern unq :: [Name]
unq (Inferred t :: Term
t)
  = TC () -> Elab' EState ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> Elab' EState ())
-> (String -> TC ()) -> String -> Elab' EState ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> (String -> Err) -> String -> TC ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
InternalMsg (String -> Elab' EState ()) -> String -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$
      "Phase error! The Inferred constructor is for coverage checking only and should not have been reflected during elaboration."
reflectTTQuotePattern unq :: [Name]
unq (TType exp :: UExp
exp)
  = do Name
ue <- Name -> ElabD Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN 0 "uexp")
       Name -> Raw -> Elab' EState ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
ue (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN "TTUExp") ["Reflection", "Language"]))
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
ue
       Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall "TType" [Name -> Raw
Var Name
ue]
       Elab' EState ()
forall aux. Elab' aux ()
solve
reflectTTQuotePattern unq :: [Name]
unq (UType u :: Universe
u)
  = do Name
uH <- Name -> ElabD Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN 0 "someUniv")
       Name -> Raw -> Elab' EState ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
uH (Name -> Raw
Var (String -> Name
reflm "Universe"))
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
uH
       Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall "UType" [Name -> Raw
Var Name
uH]
       Elab' EState ()
forall aux. Elab' aux ()
solve
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
focus Name
uH
       Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var (String -> Name
reflm (case Universe
u of
                           NullType -> "NullType"
                           UniqueType -> "UniqueType"
                           AllTypes -> "AllTypes")))
       Elab' EState ()
forall aux. Elab' aux ()
solve

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

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

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

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

reflectNameType :: NameType -> Raw
reflectNameType :: NameType -> Raw
reflectNameType (NameType
Bound) = Name -> Raw
Var (String -> Name
reflm "Bound")
reflectNameType (NameType
Ref) = Name -> Raw
Var (String -> Name
reflm "Ref")
reflectNameType (DCon x :: Int
x y :: Int
y _)
  = String -> [Raw] -> Raw
reflCall "DCon" [Const -> Raw
RConstant (Int -> Const
I Int
x), Const -> Raw
RConstant (Int -> Const
I Int
y)] -- FIXME: Uniqueness!
reflectNameType (TCon x :: Int
x y :: Int
y)
  = String -> [Raw] -> Raw
reflCall "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 s :: Text
s)
  = String -> [Raw] -> Raw
reflCall "UN" [Const -> Raw
RConstant (String -> Const
Str (Text -> String
str Text
s))]
reflectName (NS n :: Name
n ns :: [Text]
ns)
  = String -> [Raw] -> Raw
reflCall "NS" [ Name -> Raw
reflectName Name
n
                  , (String -> Raw -> Raw) -> Raw -> [String] -> Raw
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ n :: String
n s :: Raw
s ->
                             Raw -> [Raw] -> Raw
raw_apply ( Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ Name -> [String] -> Name
sNS (String -> Name
sUN "::") ["List", "Prelude"] )
                                       [ Const -> Raw
RConstant Const
StrType, Const -> Raw
RConstant (String -> Const
Str String
n), Raw
s ])
                             ( Raw -> [Raw] -> Raw
raw_apply ( Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ Name -> [String] -> Name
sNS (String -> Name
sUN "Nil") ["List", "Prelude"] )
                                         [ Const -> Raw
RConstant Const
StrType ])
                             ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
str [Text]
ns)
                  ]
reflectName (MN i :: Int
i n :: Text
n)
  = String -> [Raw] -> Raw
reflCall "MN" [Const -> Raw
RConstant (Int -> Const
I Int
i), Const -> Raw
RConstant (String -> Const
Str (Text -> String
str Text
n))]
reflectName (SN sn :: SpecialName
sn) = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (String -> Name
reflm "SN")) [SpecialName -> Raw
reflectSpecialName SpecialName
sn]
reflectName (SymRef _) = String -> Raw
forall a. HasCallStack => String -> a
error "The impossible happened: symbol table ref survived IBC loading"

reflectSpecialName :: SpecialName -> Raw
reflectSpecialName :: SpecialName -> Raw
reflectSpecialName (WhereN i :: Int
i n1 :: Name
n1 n2 :: Name
n2) =
  String -> [Raw] -> Raw
reflCall "WhereN" [Const -> Raw
RConstant (Int -> Const
I Int
i), Name -> Raw
reflectName Name
n1, Name -> Raw
reflectName Name
n2]
reflectSpecialName (WithN i :: Int
i n :: Name
n) = String -> [Raw] -> Raw
reflCall "WithN" [ Const -> Raw
RConstant (Int -> Const
I Int
i)
                                                  , Name -> Raw
reflectName Name
n
                                                  ]
reflectSpecialName (ImplementationN impl :: Name
impl ss :: [Text]
ss) =
  String -> [Raw] -> Raw
reflCall "ImplementationN" [ Name -> Raw
reflectName Name
impl
                             , Raw -> [Raw] -> Raw
mkList (Const -> Raw
RConstant Const
StrType) ([Raw] -> Raw) -> [Raw] -> Raw
forall a b. (a -> b) -> a -> b
$
                                 (Text -> Raw) -> [Text] -> [Raw]
forall a b. (a -> b) -> [a] -> [b]
map (Const -> Raw
RConstant (Const -> Raw) -> (Text -> Const) -> Text -> Raw
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Const
Str (String -> Const) -> (Text -> String) -> Text -> Const
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack) [Text]
ss
                             ]
reflectSpecialName (ParentN n :: Name
n s :: Text
s) =
  String -> [Raw] -> Raw
reflCall "ParentN" [Name -> Raw
reflectName Name
n, Const -> Raw
RConstant (String -> Const
Str (Text -> String
T.unpack Text
s))]
reflectSpecialName (MethodN n :: Name
n) =
  String -> [Raw] -> Raw
reflCall "MethodN" [Name -> Raw
reflectName Name
n]
reflectSpecialName (CaseN fc :: FC'
fc n :: Name
n) =
  String -> [Raw] -> Raw
reflCall "CaseN" [FC -> Raw
reflectFC (FC' -> FC
unwrapFC FC'
fc), Name -> Raw
reflectName Name
n]
reflectSpecialName (ImplementationCtorN n :: Name
n) =
  String -> [Raw] -> Raw
reflCall "ImplementationCtorN" [Name -> Raw
reflectName Name
n]
reflectSpecialName (MetaN parent :: Name
parent meta :: Name
meta) =
  String -> [Raw] -> Raw
reflCall "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 -> Elab' EState ()
reflectNameQuotePattern n :: Name
n@(UN s :: Text
s)
  = do Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ Name -> Raw
reflectName Name
n
       Elab' EState ()
forall aux. Elab' aux ()
solve
reflectNameQuotePattern n :: Name
n@(NS _ _)
  = do Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ Name -> Raw
reflectName Name
n
       Elab' EState ()
forall aux. Elab' aux ()
solve
reflectNameQuotePattern (MN _ n :: Text
n)
  = do Name
i <- Name -> ElabD Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN 0 "mnCounter")
       Name -> Raw -> Elab' EState ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
i (Const -> Raw
RConstant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITNative)))
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
i
       Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> Elab' EState ()) -> Raw -> Elab' EState ()
forall a b. (a -> b) -> a -> b
$ String -> [Raw] -> Raw
reflCall "MN" [Name -> Raw
Var Name
i, Const -> Raw
RConstant (String -> Const
Str (String -> Const) -> String -> Const
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
n)]
       Elab' EState ()
forall aux. Elab' aux ()
solve
reflectNameQuotePattern _ -- for all other names, match any
  = do Name
nameHole <- Name -> ElabD Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN 0 "name")
       Name -> Raw -> Elab' EState ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
nameHole (Name -> Raw
Var (String -> Name
reflm "TTName"))
       Name -> Elab' EState ()
forall aux. Name -> Elab' aux ()
movelast Name
nameHole
       Raw -> Elab' EState ()
forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var Name
nameHole)
       Elab' EState ()
forall aux. Elab' aux ()
solve

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

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

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

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

reflectUExp :: UExp -> Raw
reflectUExp :: UExp -> Raw
reflectUExp (UVar ns :: String
ns i :: Int
i) = String -> [Raw] -> Raw
reflCall "UVar" [Const -> Raw
RConstant (String -> Const
Str String
ns), Const -> Raw
RConstant (Int -> Const
I Int
i)]
reflectUExp (UVal i :: Int
i) = String -> [Raw] -> Raw
reflCall "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 = ((Name, Binder Term) -> Raw -> Raw)
-> Raw -> [(Name, Binder Term)] -> Raw
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name, Binder Term) -> Raw -> Raw
consToEnvList Raw
emptyEnvList ([(Name, Binder Term)] -> Raw)
-> (Env -> [(Name, Binder Term)]) -> Env -> Raw
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> [(Name, Binder Term)]
forall a b1 b2. [(a, b1, b2)] -> [(a, b2)]
envBinders
  where
    consToEnvList :: (Name, Binder Term) -> Raw -> Raw
    consToEnvList :: (Name, Binder Term) -> Raw -> Raw
consToEnvList (n :: Name
n, b :: Binder Term
b) l :: Raw
l
      = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN "::") ["List", "Prelude"]))
                  [ Raw
envTupleType
                  , Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var Name
pairCon) [ (Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
reflm "TTName")
                                            , (Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
reflm "Binder")
                                                    (Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
reflm "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 "Nil") ["List", "Prelude"]))
                             [Raw
envTupleType]

-- Reflected environments don't get the RigCount (for the moment, at least)
reifyEnv :: Term -> ElabD Env
reifyEnv :: Term -> ElabD Env
reifyEnv tm :: Term
tm = do [(Name, Binder Term)]
preEnv <- (Term -> ElabD (Name, Binder Term))
-> Term -> ElabD [(Name, Binder Term)]
forall a. (Term -> ElabD a) -> Term -> ElabD [a]
reifyList ((Term -> ElabD Name)
-> (Term -> ElabD (Binder Term))
-> Term
-> ElabD (Name, Binder Term)
forall a b.
(Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyPair Term -> ElabD Name
reifyTTName ((Term -> ElabD Term) -> Name -> Term -> ElabD (Binder Term)
forall a. (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinder Term -> ElabD Term
reifyTT (String -> Name
reflm "TT"))) Term
tm
                 Env -> ElabD Env
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> ElabD Env) -> Env -> ElabD Env
forall a b. (a -> b) -> a -> b
$ ((Name, Binder Term) -> (Name, RigCount, Binder Term))
-> [(Name, Binder Term)] -> Env
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n, b :: 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 True  = Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN "True") ["Bool", "Prelude"])
rawBool False = Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN "False") ["Bool", "Prelude"])

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

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

rawList :: Raw -> [Raw] -> Raw
rawList :: Raw -> [Raw] -> Raw
rawList ty :: Raw
ty = (Raw -> Raw -> Raw) -> Raw -> [Raw] -> Raw
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 t1 :: Raw
t1 t2 :: 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 (a :: Raw
a, b :: Raw
b) (x :: Raw
x, y :: 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 a :: Raw
a b :: Raw
b c :: 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 (a :: Raw
a, b :: Raw
b, c :: Raw
c) (x :: Raw
x, y :: Raw
y, z :: 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 ctxt :: [(Name, Term)]
ctxt = Raw -> [Raw] -> Raw
rawList (Raw -> Raw -> Raw
rawPairTy  (Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
reflm "TTName") (Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
reflm "TT"))
                           (((Name, Term) -> Raw) -> [(Name, Term)] -> [Raw]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: Name
n, t :: Term
t) -> ((Raw, Raw) -> (Raw, Raw) -> Raw
rawPair (Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
reflm "TTName", Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
reflm "TT")
                                                      (Name -> Raw
reflectName Name
n, Term -> Raw
reflect Term
t)))
                                [(Name, Term)]
ctxt)

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

-- | Reflect a file context
reflectFC :: FC -> Raw
reflectFC :: FC -> Raw
reflectFC fc :: FC
fc = Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var (String -> Name
reflm "FileLoc"))
                         [ Const -> Raw
RConstant (String -> Const
Str (FC -> String
fc_fname FC
fc))
                         , Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var Name
pairCon) ([Raw] -> Raw) -> [Raw] -> Raw
forall a b. (a -> b) -> a -> b
$
                             [Raw
intTy, Raw
intTy] [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++
                             (Int -> Raw) -> [Int] -> [Raw]
forall a b. (a -> b) -> [a] -> [b]
map (Const -> Raw
RConstant (Const -> Raw) -> (Int -> Const) -> Int -> Raw
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I)
                                 [ (Int, Int) -> Int
forall a b. (a, b) -> a
fst (FC -> (Int, Int)
fc_start FC
fc)
                                 , (Int, Int) -> Int
forall a b. (a, b) -> b
snd (FC -> (Int, Int)
fc_start FC
fc)
                                 ]
                         , Raw -> [Raw] -> Raw
raw_apply (Name -> Raw
Var Name
pairCon) ([Raw] -> Raw) -> [Raw] -> Raw
forall a b. (a -> b) -> a -> b
$
                             [Raw
intTy, Raw
intTy] [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++
                             (Int -> Raw) -> [Int] -> [Raw]
forall a b. (a -> b) -> [a] -> [b]
map (Const -> Raw
RConstant (Const -> Raw) -> (Int -> Const) -> Int -> Raw
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I)
                                 [ (Int, Int) -> Int
forall a b. (a, b) -> a
fst (FC -> (Int, Int)
fc_end FC
fc)
                                 , (Int, Int) -> Int
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 -> StateT (ElabState EState) TC FC
reifyFC tm :: Term
tm
  | (P (DCon _ _ _) cn :: Name
cn _, [Constant (Str fn :: String
fn), st :: Term
st, end :: Term
end]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm
  , Name
cn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
reflm "FileLoc" = String -> (Int, Int) -> (Int, Int) -> FC
FC String
fn ((Int, Int) -> (Int, Int) -> FC)
-> StateT (ElabState EState) TC (Int, Int)
-> StateT (ElabState EState) TC ((Int, Int) -> FC)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> ElabD Int)
-> (Term -> ElabD Int)
-> Term
-> StateT (ElabState EState) TC (Int, Int)
forall a b.
(Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyPair Term -> ElabD Int
reifyInt Term -> ElabD Int
reifyInt Term
st StateT (ElabState EState) TC ((Int, Int) -> FC)
-> StateT (ElabState EState) TC (Int, Int)
-> StateT (ElabState EState) TC FC
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> ElabD Int)
-> (Term -> ElabD Int)
-> Term
-> StateT (ElabState EState) TC (Int, Int)
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 = String -> StateT (ElabState EState) TC FC
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT (ElabState EState) TC FC)
-> String -> StateT (ElabState EState) TC FC
forall a b. (a -> b) -> a -> b
$ "Not a source location: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
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 _ (App _ (P (DCon _ _ _) (NS (UN just :: Text
just) _) _) ty :: Term
ty) tm :: Term
tm)
  | Text
just Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Just" = Term -> Maybe Term
forall a. a -> Maybe a
Just Term
tm
fromTTMaybe x :: Term
x          = Maybe Term
forall a. Maybe a
Nothing

reflErrName :: String -> Name
reflErrName :: String -> Name
reflErrName n :: String
n = Name -> [String] -> Name
sNS (String -> Name
sUN String
n) ["Errors", "Reflection", "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 _ (P (DCon _ _ _) n :: Name
n _) (Constant (Str msg :: String
msg))) | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
reflm "TextPart" =
    ErrorReportPart -> Either Err ErrorReportPart
forall a b. b -> Either a b
Right (String -> ErrorReportPart
TextPart String
msg)
reifyReportPart (App _ (P (DCon _ _ _) n :: Name
n _) ttn :: Term
ttn)
  | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
reflm "NamePart" =
    case EState -> ElabD Name -> ProofState -> TC (Name, ElabState EState)
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 0 "hole") String
internalNS Context
initContext Ctxt TypeInfo
forall k a. Map k a
emptyContext 0 Term
forall n. TT n
Erased) of
      Error e :: Err
e -> Err -> Either Err ErrorReportPart
forall a b. a -> Either a b
Left (Err -> Either Err ErrorReportPart)
-> (String -> Err) -> String -> Either Err ErrorReportPart
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
InternalMsg (String -> Either Err ErrorReportPart)
-> String -> Either Err ErrorReportPart
forall a b. (a -> b) -> a -> b
$
       "could not reify name term " String -> ShowS
forall a. [a] -> [a] -> [a]
++
       Term -> String
forall a. Show a => a -> String
show Term
ttn String -> ShowS
forall a. [a] -> [a] -> [a]
++
       " when reflecting an error:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
e
      OK (n' :: Name
n', _)-> ErrorReportPart -> Either Err ErrorReportPart
forall a b. b -> Either a b
Right (ErrorReportPart -> Either Err ErrorReportPart)
-> ErrorReportPart -> Either Err ErrorReportPart
forall a b. (a -> b) -> a -> b
$ Name -> ErrorReportPart
NamePart Name
n'
reifyReportPart (App _ (P (DCon _ _ _) n :: Name
n _) tm :: Term
tm)
  | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
reflm "TermPart" =
  case EState -> ElabD Term -> ProofState -> TC (Term, ElabState EState)
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 0 "hole") String
internalNS Context
initContext Ctxt TypeInfo
forall k a. Map k a
emptyContext 0 Term
forall n. TT n
Erased) of
    Error e :: Err
e -> Err -> Either Err ErrorReportPart
forall a b. a -> Either a b
Left (Err -> Either Err ErrorReportPart)
-> (String -> Err) -> String -> Either Err ErrorReportPart
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
InternalMsg (String -> Either Err ErrorReportPart)
-> String -> Either Err ErrorReportPart
forall a b. (a -> b) -> a -> b
$
      "could not reify reflected term " String -> ShowS
forall a. [a] -> [a] -> [a]
++
      Term -> String
forall a. Show a => a -> String
show Term
tm String -> ShowS
forall a. [a] -> [a] -> [a]
++
      " when reflecting an error:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
e
    OK (tm' :: Term
tm', _) -> ErrorReportPart -> Either Err ErrorReportPart
forall a b. b -> Either a b
Right (ErrorReportPart -> Either Err ErrorReportPart)
-> ErrorReportPart -> Either Err ErrorReportPart
forall a b. (a -> b) -> a -> b
$ Term -> ErrorReportPart
TermPart Term
tm'
reifyReportPart (App _ (P (DCon _ _ _) n :: Name
n _) tm :: Term
tm)
  | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
reflm "RawPart" =
  case EState
-> StateT (ElabState EState) TC Raw
-> ProofState
-> TC (Raw, ElabState EState)
forall aux a.
aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
runElab EState
initEState (Term -> StateT (ElabState EState) TC Raw
reifyRaw Term
tm) (Name
-> String -> Context -> Ctxt TypeInfo -> Int -> Term -> ProofState
initElaborator (Int -> String -> Name
sMN 0 "hole") String
internalNS Context
initContext Ctxt TypeInfo
forall k a. Map k a
emptyContext 0 Term
forall n. TT n
Erased) of
    Error e :: Err
e -> Err -> Either Err ErrorReportPart
forall a b. a -> Either a b
Left (Err -> Either Err ErrorReportPart)
-> (String -> Err) -> String -> Either Err ErrorReportPart
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
InternalMsg (String -> Either Err ErrorReportPart)
-> String -> Either Err ErrorReportPart
forall a b. (a -> b) -> a -> b
$
      "could not reify reflected raw term " String -> ShowS
forall a. [a] -> [a] -> [a]
++
      Term -> String
forall a. Show a => a -> String
show Term
tm String -> ShowS
forall a. [a] -> [a] -> [a]
++
      " when reflecting an error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
e
    OK (tm' :: Raw
tm', _) -> ErrorReportPart -> Either Err ErrorReportPart
forall a b. b -> Either a b
Right (ErrorReportPart -> Either Err ErrorReportPart)
-> ErrorReportPart -> Either Err ErrorReportPart
forall a b. (a -> b) -> a -> b
$ Raw -> ErrorReportPart
RawPart Raw
tm'
reifyReportPart (App _ (P (DCon _ _ _) n :: Name
n _) tm :: Term
tm)
  | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
reflm "SubReport" =
  case Term -> Maybe [Term]
unList Term
tm of
    Just xs :: [Term]
xs -> do [ErrorReportPart]
subParts <- (Term -> Either Err ErrorReportPart)
-> [Term] -> Either Err [ErrorReportPart]
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
                  ErrorReportPart -> Either Err ErrorReportPart
forall a b. b -> Either a b
Right ([ErrorReportPart] -> ErrorReportPart
SubReport [ErrorReportPart]
subParts)
    Nothing -> Err -> Either Err ErrorReportPart
forall a b. a -> Either a b
Left (Err -> Either Err ErrorReportPart)
-> (String -> Err) -> String -> Either Err ErrorReportPart
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
InternalMsg (String -> Either Err ErrorReportPart)
-> String -> Either Err ErrorReportPart
forall a b. (a -> b) -> a -> b
$ "could not reify subreport " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm
reifyReportPart x :: Term
x = Err -> Either Err ErrorReportPart
forall a b. a -> Either a b
Left (Err -> Either Err ErrorReportPart)
-> (String -> Err) -> String -> Either Err ErrorReportPart
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
InternalMsg (String -> Either Err ErrorReportPart)
-> String -> Either Err ErrorReportPart
forall a b. (a -> b) -> a -> b
$ "could not reify " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
x

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

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

reifyRFunArg :: Term -> ElabD RFunArg
reifyRFunArg :: Term -> ElabD RFunArg
reifyRFunArg (App _ (App _ (App _ (App _ (P (DCon _ _ _) n :: Name
n _) argN :: Term
argN) argTy :: Term
argTy) argPl :: Term
argPl) argE :: Term
argE)
  | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
tacN "MkFunArg" = (Name -> Raw -> RPlicity -> RErasure -> RFunArg)
-> ElabD Name
-> StateT (ElabState EState) TC Raw
-> ElabD RPlicity
-> ElabD RErasure
-> ElabD RFunArg
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 -> StateT (ElabState EState) TC Raw
reifyRaw Term
argTy)
                             (Term -> ElabD RPlicity
reifyPlicity Term
argPl)
                             (Term -> ElabD RErasure
reifyErasure Term
argE)
reifyRFunArg aTm :: Term
aTm = String -> ElabD RFunArg
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> ElabD RFunArg) -> String -> ElabD RFunArg
forall a b. (a -> b) -> a -> b
$ "Couldn't reify " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
aTm String -> ShowS
forall a. [a] -> [a] -> [a]
++ " as an RArg."

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

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

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

reifyRDataDefn :: Term -> ElabD RDataDefn
reifyRDataDefn :: Term -> ElabD RDataDefn
reifyRDataDefn (App _ (App _ (P _ n :: Name
n _) tyn :: Term
tyn) ctors :: Term
ctors)
  | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
tacN "DefineDatatype", Just ctors' :: [Term]
ctors' <- Term -> Maybe [Term]
unList Term
ctors
  = Name -> [RConstructorDefn] -> RDataDefn
RDefineDatatype (Name -> [RConstructorDefn] -> RDataDefn)
-> ElabD Name
-> StateT (ElabState EState) TC ([RConstructorDefn] -> RDataDefn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ElabD Name
reifyTTName Term
tyn StateT (ElabState EState) TC ([RConstructorDefn] -> RDataDefn)
-> StateT (ElabState EState) TC [RConstructorDefn]
-> ElabD RDataDefn
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> ElabD RConstructorDefn)
-> [Term] -> StateT (ElabState EState) TC [RConstructorDefn]
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 aTm :: Term
aTm = String -> ElabD RDataDefn
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> ElabD RDataDefn) -> String -> ElabD RDataDefn
forall a b. (a -> b) -> a -> b
$ "Couldn't reify " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
aTm String -> ShowS
forall a. [a] -> [a] -> [a]
++ " as an RDataDefn"

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

reflectList :: Raw -> [Raw] -> Raw
reflectList :: Raw -> [Raw] -> Raw
reflectList ty :: Raw
ty []     = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN "Nil") ["List", "Prelude"])) Raw
ty
reflectList ty :: Raw
ty (x :: Raw
x:xs :: [Raw]
xs) = Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> [String] -> Name
sNS (String -> Name
sUN "::") ["List", "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 []     r :: Raw
r = ([], Raw
r)
getArgs (a :: PArg
a:as :: [PArg]
as) (RBind n :: Name
n (Pi _ _ ty :: Raw
ty _) sc :: Raw
sc) =
  let (args :: [RFunArg]
args, res :: Raw
res) = [PArg] -> Raw -> ([RFunArg], Raw)
getArgs [PArg]
as Raw
sc
      erased :: RErasure
erased = if ArgOpt
InaccessibleArg ArgOpt -> [ArgOpt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PArg -> [ArgOpt]
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'RFunArg -> [RFunArg] -> [RFunArg]
forall a. a -> [a] -> [a]
:[RFunArg]
args, Raw
res)
getArgs _ r :: Raw
r = ([], Raw
r)

unApplyRaw :: Raw -> (Raw, [Raw])
unApplyRaw :: Raw -> (Raw, [Raw])
unApplyRaw tm :: Raw
tm = [Raw] -> Raw -> (Raw, [Raw])
ua [] Raw
tm
  where
    ua :: [Raw] -> Raw -> (Raw, [Raw])
ua args :: [Raw]
args (RApp f :: Raw
f a :: Raw
a) = [Raw] -> Raw -> (Raw, [Raw])
ua (Raw
aRaw -> [Raw] -> [Raw]
forall a. a -> [a] -> [a]
:[Raw]
args) Raw
f
    ua args :: [Raw]
args t :: 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 ist :: IState
ist n :: Name
n =
  [ Name -> [([(Name, Term)], Term, Term)] -> RFunDefn Term
forall a. Name -> [([(a, TT a)], TT a, TT a)] -> RFunDefn (TT a)
mkFunDefn Name
name [([(Name, Term)], Term, Term)]
clauses
  | (name :: Name
name, (clauses :: [([(Name, Term)], Term, Term)]
clauses, _)) <- Name
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
 -> [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))])
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))]
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
name clauses :: [([(a, TT a)], TT a, TT a)]
clauses = Name -> [RFunClause (TT a)] -> RFunDefn (TT a)
forall a. Name -> [RFunClause a] -> RFunDefn a
RDefineFun Name
name ((([(a, TT a)], TT a, TT a) -> RFunClause (TT a))
-> [([(a, TT a)], TT a, TT a)] -> [RFunClause (TT a)]
forall a b. (a -> b) -> [a] -> [b]
map ([(a, TT a)], TT a, TT a) -> RFunClause (TT a)
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 ([], lhs :: TT a
lhs, Impossible) = TT a -> RFunClause (TT a)
forall a. a -> RFunClause a
RMkImpossibleClause TT a
lhs
        mkFunClause ([], lhs :: TT a
lhs, rhs :: TT a
rhs) = TT a -> TT a -> RFunClause (TT a)
forall a. a -> a -> RFunClause a
RMkFunClause TT a
lhs TT a
rhs
        mkFunClause (((n :: a
n, ty :: TT a
ty) : ns :: [(a, TT a)]
ns), lhs :: TT a
lhs, rhs :: 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 Impossible = TT a
forall n. TT n
Impossible
          bind tm :: TT a
tm = a -> Binder (TT a) -> TT a -> TT a
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind a
n (RigCount -> TT a -> Binder (TT a)
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 ist :: IState
ist n :: Name
n =
  [Maybe RDatatype] -> [RDatatype]
forall a. [Maybe a] -> [a]
catMaybes [ Name -> TypeInfo -> Maybe RDatatype
mkDataType Name
dn TypeInfo
ti
            | (dn :: Name
dn, ti :: TypeInfo
ti) <- Name -> Ctxt TypeInfo -> [(Name, TypeInfo)]
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 params :: [Int]
params cn :: Name
cn = do Raw
cty <- (Term -> Raw) -> Maybe Term -> Maybe Raw
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 <- Name -> Ctxt [PArg] -> Maybe [PArg]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
cn Ctxt [PArg]
impls
                               let (args :: [RFunArg]
args, res :: Raw
res) = [PArg] -> Raw -> ([RFunArg], Raw)
getArgs [PArg]
argInfo Raw
cty
                               (Name, [RCtorArg], Raw) -> Maybe (Name, [RCtorArg], Raw)
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 n :: Name
n [] res :: Raw
res = Name -> Raw -> Maybe Int
findPos Name
n Raw
res
          where findPos :: Name -> Raw -> Maybe Int
findPos n :: Name
n app :: Raw
app = case Raw -> (Raw, [Raw])
unApplyRaw Raw
app of
                                  (_, argL :: [Raw]
argL) -> (Raw -> Bool) -> [Raw] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex (Raw -> Raw -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Raw
Var Name
n) [Raw]
argL
        argPos n :: Name
n (arg :: RFunArg
arg:args :: [RFunArg]
args) res :: Raw
res = if Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== RFunArg -> Name
argName RFunArg
arg
                                     then Maybe Int
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 [] _ _ = []
        ctorArgsStatus (arg :: RFunArg
arg:args :: [RFunArg]
args) res :: Raw
res params :: [Int]
params =
          case Name -> [RFunArg] -> Raw -> Maybe Int
argPos (RFunArg -> Name
argName RFunArg
arg) [RFunArg]
args Raw
res of
            Nothing -> RFunArg -> RCtorArg
RCtorField RFunArg
arg RCtorArg -> [RCtorArg] -> [RCtorArg]
forall a. a -> [a] -> [a]
: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
ctorArgsStatus [RFunArg]
args Raw
res [Int]
params
            Just i :: Int
i -> if Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
params
                         then RFunArg -> RCtorArg
RCtorParameter RFunArg
arg RCtorArg -> [RCtorArg] -> [RCtorArg]
forall a. a -> [a] -> [a]
: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
ctorArgsStatus [RFunArg]
args Raw
res [Int]
params
                         else RFunArg -> RCtorArg
RCtorField RFunArg
arg RCtorArg -> [RCtorArg] -> [RCtorArg]
forall a. a -> [a] -> [a]
: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
ctorArgsStatus [RFunArg]
args Raw
res [Int]
params

        mkDataType :: Name -> TypeInfo -> Maybe RDatatype
mkDataType name :: Name
name (TI {param_pos :: TypeInfo -> [Int]
param_pos = [Int]
params, con_names :: TypeInfo -> [Name]
con_names = [Name]
constrs}) =
          do (TyDecl (TCon _ _) ty :: Term
ty) <- Name -> Context -> Maybe Def
lookupDefExact Name
name Context
ctxt
             [PArg]
implInfo <- Name -> Ctxt [PArg] -> Maybe [PArg]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
name Ctxt [PArg]
impls
             let (tcargs :: [RTyConArg]
tcargs, tcres :: Raw
tcres) = [Int] -> [PArg] -> Raw -> ([RTyConArg], Raw)
getTCArgs [Int]
params [PArg]
implInfo (Term -> Raw
forget Term
ty)
             [(Name, [RCtorArg], Raw)]
ctors <- (Name -> Maybe (Name, [RCtorArg], Raw))
-> [Name] -> Maybe [(Name, [RCtorArg], Raw)]
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
             RDatatype -> Maybe RDatatype
forall (m :: * -> *) a. Monad m => a -> m a
return (RDatatype -> Maybe RDatatype) -> RDatatype -> Maybe RDatatype
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 params :: [Int]
params implInfo :: [PArg]
implInfo tcTy :: Raw
tcTy =
          let (args :: [RFunArg]
args, res :: Raw
res) = [PArg] -> Raw -> ([RFunArg], Raw)
getArgs [PArg]
implInfo Raw
tcTy
          in ([RFunArg] -> Int -> [RTyConArg]
tcArg [RFunArg]
args 0, Raw
res)
            where tcArg :: [RFunArg] -> Int -> [RTyConArg]
tcArg [] _ = []
                  tcArg (arg :: RFunArg
arg:args :: [RFunArg]
args) i :: Int
i | Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
params = RFunArg -> RTyConArg
RParameter RFunArg
arg RTyConArg -> [RTyConArg] -> [RTyConArg]
forall a. a -> [a] -> [a]
: [RFunArg] -> Int -> [RTyConArg]
tcArg [RFunArg]
args (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+1)
                                     | Bool
otherwise       = RFunArg -> RTyConArg
RIndex RFunArg
arg RTyConArg -> [RTyConArg] -> [RTyConArg]
forall a. a -> [a] -> [a]
: [RFunArg] -> Int -> [RTyConArg]
tcArg [RFunArg]
args (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+1)


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

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

reflectArg :: RFunArg -> Raw
reflectArg :: RFunArg -> Raw
reflectArg (RFunArg n :: Name
n ty :: Raw
ty plic :: RPlicity
plic erasure :: RErasure
erasure) =
  Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
tacN "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 arg :: RFunArg
arg) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
tacN "CtorParameter") (RFunArg -> Raw
reflectArg RFunArg
arg)
reflectCtorArg (RCtorField arg :: RFunArg
arg) = Raw -> Raw -> Raw
RApp (Name -> Raw
Var (Name -> Raw) -> Name -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Name
tacN "CtorField") (RFunArg -> Raw
reflectArg RFunArg
arg)

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

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

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

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