idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-07 08:18:12 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #210 from edwinb/elab-reflection

Browse Source 
Initial steps to elaborator reflection
This commit is contained in:
Edwin Brady 2020-05-31 15:06:50 +01:00 committed by GitHub
commit 54119bc4e2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
16 changed files with 646 additions and 419 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
idris2.ipkg
View File

@ -121,6 +121,7 @@ modules =
TTImp.Elab.Quote, TTImp.Elab.Quote,
TTImp.Elab.Record, TTImp.Elab.Record,
TTImp.Elab.Rewrite, TTImp.Elab.Rewrite,
TTImp.Elab.RunElab,
TTImp.Elab.Term, TTImp.Elab.Term,
TTImp.Elab.Utils, TTImp.Elab.Utils,
TTImp.Impossible, TTImp.Impossible,

35
libs/base/Language/Reflection.idr
View File

@ -3,12 +3,18 @@ module Language.Reflection
import public Language.Reflection.TT import public Language.Reflection.TT
import public Language.Reflection.TTImp import public Language.Reflection.TTImp
public export export
data Elab : Type -> Type where data Elab : Type -> Type where
Pure : a -> Elab a Pure : a -> Elab a
Bind : Elab a -> (a -> Elab b) -> Elab b Bind : Elab a -> (a -> Elab b) -> Elab b
LogMsg : Nat -> String -> Elab ()
LogTerm : Nat -> String -> TTImp -> Elab ()
Check : TTImp -> Elab a -- Check a TTImp term against the current goal type
Check : TTImp -> Elab TT
-- Get the current goal type, if known
-- (it might need to be inferred from the solution)
Goal : Elab (Maybe TTImp)
mutual mutual
export export
@ -26,3 +32,28 @@ mutual
export export
Monad Elab where Monad Elab where
(>>=) = Bind (>>=) = Bind
export
logMsg : Nat -> String -> Elab ()
logMsg = LogMsg
export
logTerm : Nat -> String -> TTImp -> Elab ()
logTerm = LogTerm
export
logGoal : Nat -> String -> Elab ()
logGoal n msg
= do g <- Goal
case g of
Nothing => pure ()
Just t => logTerm n msg t
-- Check a TTImp term against the current goal type
export
check : TTImp -> Elab TT
check = Check
export
goal : Elab (Maybe TTImp)
goal = Goal

5
libs/base/Language/Reflection/TT.idr
View File

@ -55,6 +55,10 @@ data IsVar : Name -> Nat -> List Name -> Type where
public export public export
data LazyReason = LInf | LLazy | LUnknown data LazyReason = LInf | LLazy | LUnknown
export
data TT : Type where [external]
{-
-- Type checked terms in the core TT -- Type checked terms in the core TT
public export public export
data TT : List Name -> Type where data TT : List Name -> Type where
@ -73,6 +77,7 @@ data TT : List Name -> Type where
PrimVal : FC -> Constant -> TT vars PrimVal : FC -> Constant -> TT vars
Erased : FC -> TT vars Erased : FC -> TT vars
TType : FC -> TT vars TType : FC -> TT vars
-}
public export public export
data TotalReq = Total | CoveringOnly | PartialOK data TotalReq = Total | CoveringOnly | PartialOK

2
libs/base/Language/Reflection/TTImp.idr
View File

@ -1,6 +1,6 @@
module Language.Reflection.TTImp module Language.Reflection.TTImp
import Language.Reflection.TT import public Language.Reflection.TT
-- Unchecked terms and declarations in the intermediate language -- Unchecked terms and declarations in the intermediate language
mutual mutual

6
src/Core/Options.idr
View File

@ -82,11 +82,15 @@ record PrimNames where
fromCharName : Maybe Name fromCharName : Maybe Name
public export public export
data LangExt = Borrowing -- not yet implemented data LangExt
= ElabReflection
| Borrowing -- not yet implemented
export export
Eq LangExt where Eq LangExt where
ElabReflection == ElabReflection = True
Borrowing == Borrowing = True Borrowing == Borrowing = True
_ == _ = False
-- Other options relevant to the current session (so not to be saved in a TTC) -- Other options relevant to the current session (so not to be saved in a TTC)
public export public export

206
src/Core/Reflect.idr
View File

@ -126,8 +126,11 @@ Reflect Double where
export export
Reify Bool where Reify Bool where
reify defs (NDCon _ (NS _ (UN "True")) _ _ _) = pure True reify defs val@(NDCon _ n _ _ _)
reify defs (NDCon _ (NS _ (UN "False")) _ _ _) = pure False = case !(full (gamma defs) n) of
NS _ (UN "True") => pure True
NS _ (UN "False") => pure False
_ => cantReify val "Bool"
reify defs val = cantReify val "Bool" reify defs val = cantReify val "Bool"
export export
@ -137,11 +140,13 @@ Reflect Bool where
export export
Reify Nat where Reify Nat where
reify defs (NDCon _ (NS _ (UN "Z")) _ _ _) reify defs val@(NDCon _ n _ _ args)
= pure Z = case (!(full (gamma defs) n), args) of
reify defs (NDCon _ (NS _ (UN "S")) _ _ [k]) (NS _ (UN "Z"), _) => pure Z
= do k' <- reify defs !(evalClosure defs k) (NS _ (UN "S"), [k])
=> do k' <- reify defs !(evalClosure defs k)
pure (S k') pure (S k')
_ => cantReify val "Nat"
reify defs val = cantReify val "Nat" reify defs val = cantReify val "Nat"
export export
@ -153,12 +158,14 @@ Reflect Nat where
export export
Reify a => Reify (List a) where Reify a => Reify (List a) where
reify defs (NDCon _ (NS _ (UN "Nil")) _ _ _) reify defs val@(NDCon _ n _ _ args)
= pure [] = case (!(full (gamma defs) n), args) of
reify defs (NDCon _ (NS _ (UN "::")) _ _ [_, x, xs]) (NS _ (UN "Nil"), _) => pure []
= do x' <- reify defs !(evalClosure defs x) (NS _ (UN "::"), [_, x, xs])
=> do x' <- reify defs !(evalClosure defs x)
xs' <- reify defs !(evalClosure defs xs) xs' <- reify defs !(evalClosure defs xs)
pure (x' :: xs') pure (x' :: xs')
_ => cantReify val "List"
reify defs val = cantReify val "List" reify defs val = cantReify val "List"
export export
@ -171,11 +178,13 @@ Reflect a => Reflect (List a) where
export export
Reify a => Reify (Maybe a) where Reify a => Reify (Maybe a) where
reify defs (NDCon _ (NS _ (UN "Nothing")) _ _ _) reify defs val@(NDCon _ n _ _ args)
= pure Nothing = case (!(full (gamma defs) n), args) of
reify defs (NDCon _ (NS _ (UN "Just")) _ _ [_, x]) (NS _ (UN "Nothing"), _) => pure Nothing
= do x' <- reify defs !(evalClosure defs x) (NS _ (UN "Just"), [_, x])
=> do x' <- reify defs !(evalClosure defs x)
pure (Just x') pure (Just x')
_ => cantReify val "Maybe"
reify defs val = cantReify val "Maybe" reify defs val = cantReify val "Maybe"
export export
@ -187,10 +196,13 @@ Reflect a => Reflect (Maybe a) where
export export
(Reify a, Reify b) => Reify (a, b) where (Reify a, Reify b) => Reify (a, b) where
reify defs (NDCon _ (NS _ (UN "MkPair")) _ _ [_, _, x, y]) reify defs val@(NDCon _ n _ _ [_, _, x, y])
= do x' <- reify defs !(evalClosure defs x) = case (!(full (gamma defs) n)) of
NS _ (UN "MkPair")
=> do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
pure (x', y') pure (x', y')
_ => cantReify val "Pair"
reify defs val = cantReify val "Pair" reify defs val = cantReify val "Pair"
export export
@ -202,17 +214,20 @@ export
export export
Reify Name where Reify Name where
reify defs (NDCon _ (NS _ (UN "UN")) _ _ [str]) reify defs val@(NDCon _ n _ _ args)
= do str' <- reify defs !(evalClosure defs str) = case (!(full (gamma defs) n), args) of
(NS _ (UN "UN"), [str])
=> do str' <- reify defs !(evalClosure defs str)
pure (UN str') pure (UN str')
reify defs (NDCon _ (NS _ (UN "MN")) _ _ [str, i]) (NS _ (UN "MN"), [str, i])
= do str' <- reify defs !(evalClosure defs str) => do str' <- reify defs !(evalClosure defs str)
i' <- reify defs !(evalClosure defs i) i' <- reify defs !(evalClosure defs i)
pure (MN str' i') pure (MN str' i')
reify defs (NDCon _ (NS _ (UN "NS")) _ _ [ns, n]) (NS _ (UN "NS"), [ns, n])
= do ns' <- reify defs !(evalClosure defs ns) => do ns' <- reify defs !(evalClosure defs ns)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (NS ns' n') pure (NS ns' n')
_ => cantReify val "Name"
reify defs val = cantReify val "Name" reify defs val = cantReify val "Name"
export export
@ -232,18 +247,19 @@ Reflect Name where
export export
Reify NameType where Reify NameType where
reify defs (NDCon _ (NS _ (UN "Bound")) _ _ _) reify defs val@(NDCon _ n _ _ args)
= pure Bound = case (!(full (gamma defs) n), args) of
reify defs (NDCon _ (NS _ (UN "Func")) _ _ _) (NS _ (UN "Bound"), _) => pure Bound
= pure Func (NS _ (UN "Func"), _) => pure Func
reify defs (NDCon _ (NS _ (UN "DataCon")) _ _ [t,i]) (NS _ (UN "DataCon"), [t,i])
= do t' <- reify defs !(evalClosure defs t) => do t' <- reify defs !(evalClosure defs t)
i' <- reify defs !(evalClosure defs i) i' <- reify defs !(evalClosure defs i)
pure (DataCon t' i') pure (DataCon t' i')
reify defs (NDCon _ (NS _ (UN "TyCon")) _ _ [t,i]) (NS _ (UN "TyCon"), [t,i])
= do t' <- reify defs !(evalClosure defs t) => do t' <- reify defs !(evalClosure defs t)
i' <- reify defs !(evalClosure defs i) i' <- reify defs !(evalClosure defs i)
pure (TyCon t' i') pure (TyCon t' i')
_ => cantReify val "NameType"
reify defs val = cantReify val "NameType" reify defs val = cantReify val "NameType"
export export
@ -261,35 +277,38 @@ Reflect NameType where
export export
Reify Constant where Reify Constant where
reify defs (NDCon _ (NS _ (UN "I")) _ _ [x]) reify defs val@(NDCon _ n _ _ args)
= do x' <- reify defs !(evalClosure defs x) = case (!(full (gamma defs) n), args) of
(NS _ (UN "I"), [x])
=> do x' <- reify defs !(evalClosure defs x)
pure (I x') pure (I x')
reify defs (NDCon _ (NS _ (UN "BI")) _ _ [x]) (NS _ (UN "BI"), [x])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (BI x') pure (BI x')
reify defs (NDCon _ (NS _ (UN "Str")) _ _ [x]) (NS _ (UN "Str"), [x])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (Str x') pure (Str x')
reify defs (NDCon _ (NS _ (UN "Ch")) _ _ [x]) (NS _ (UN "Ch"), [x])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (Ch x') pure (Ch x')
reify defs (NDCon _ (NS _ (UN "Db")) _ _ [x]) (NS _ (UN "Db"), [x])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (Db x') pure (Db x')
reify defs (NDCon _ (NS _ (UN "WorldVal")) _ _ []) (NS _ (UN "WorldVal"), [])
= pure WorldVal => pure WorldVal
reify defs (NDCon _ (NS _ (UN "IntType")) _ _ []) (NS _ (UN "IntType"), [])
= pure IntType => pure IntType
reify defs (NDCon _ (NS _ (UN "IntegerType")) _ _ []) (NS _ (UN "IntegerType"), [])
= pure IntegerType => pure IntegerType
reify defs (NDCon _ (NS _ (UN "StringType")) _ _ []) (NS _ (UN "StringType"), [])
= pure StringType => pure StringType
reify defs (NDCon _ (NS _ (UN "CharType")) _ _ []) (NS _ (UN "CharType"), [])
= pure CharType => pure CharType
reify defs (NDCon _ (NS _ (UN "DoubleType")) _ _ []) (NS _ (UN "DoubleType"), [])
= pure DoubleType => pure DoubleType
reify defs (NDCon _ (NS _ (UN "WorldType")) _ _ []) (NS _ (UN "WorldType"), [])
= pure WorldType => pure WorldType
_ => cantReify val "Constant"
reify defs val = cantReify val "Constant" reify defs val = cantReify val "Constant"
export export
@ -326,12 +345,12 @@ Reflect Constant where
export export
Reify Visibility where Reify Visibility where
reify defs (NDCon _ (NS _ (UN "Private")) _ _ []) reify defs val@(NDCon _ n _ _ _)
= pure Private = case !(full (gamma defs) n) of
reify defs (NDCon _ (NS _ (UN "Export")) _ _ []) NS _ (UN "Private") => pure Private
= pure Export NS _ (UN "Export") => pure Export
reify defs (NDCon _ (NS _ (UN "Public")) _ _ []) NS _ (UN "Public") => pure Public
= pure Public _ => cantReify val "Visibility"
reify defs val = cantReify val "Visibility" reify defs val = cantReify val "Visibility"
export export
@ -342,12 +361,12 @@ Reflect Visibility where
export export
Reify TotalReq where Reify TotalReq where
reify defs (NDCon _ (NS _ (UN "Total")) _ _ []) reify defs val@(NDCon _ n _ _ _)
= pure Total = case !(full (gamma defs) n) of
reify defs (NDCon _ (NS _ (UN "CoveringOnly")) _ _ []) NS _ (UN "Total") => pure Total
= pure CoveringOnly NS _ (UN "CoveringOnly") => pure CoveringOnly
reify defs (NDCon _ (NS _ (UN "PartialOK")) _ _ []) NS _ (UN "PartialOK") => pure PartialOK
= pure PartialOK _ => cantReify val "TotalReq"
reify defs val = cantReify val "TotalReq" reify defs val = cantReify val "TotalReq"
export export
@ -358,12 +377,12 @@ Reflect TotalReq where
export export
Reify RigCount where Reify RigCount where
reify defs (NDCon _ (NS _ (UN "M0")) _ _ []) reify defs val@(NDCon _ n _ _ _)
= pure erased = case !(full (gamma defs) n) of
reify defs (NDCon _ (NS _ (UN "M1")) _ _ []) NS _ (UN "M0") => pure erased
= pure linear NS _ (UN "M1") => pure linear
reify defs (NDCon _ (NS _ (UN "MW")) _ _ []) NS _ (UN "MW") => pure top
= pure top _ => cantReify val "Count"
reify defs val = cantReify val "Count" reify defs val = cantReify val "Count"
export export
@ -376,12 +395,15 @@ Reflect RigCount where
export export
Reify t => Reify (PiInfo t) where Reify t => Reify (PiInfo t) where
reify defs (NDCon _ (NS _ (UN "ImplicitArg")) _ _ []) reify defs val@(NDCon _ n _ _ args)
= pure Implicit = case (!(full (gamma defs) n), args) of
reify defs (NDCon _ (NS _ (UN "ExplicitArg")) _ _ []) (NS _ (UN "ImplicitArg"), _) => pure Implicit
= pure Explicit (NS _ (UN "ExplicitArg"), _) => pure Explicit
reify defs (NDCon _ (NS _ (UN "AutoImplicit")) _ _ []) (NS _ (UN "AutoImplicit"), _) => pure AutoImplicit
= pure AutoImplicit (NS _ (UN "DefImplicit"), [t])
=> do t' <- reify defs !(evalClosure defs t)
pure (DefImplicit t')
_ => cantReify val "PiInfo"
reify defs val = cantReify val "PiInfo" reify defs val = cantReify val "PiInfo"
export export
@ -395,12 +417,12 @@ Reflect t => Reflect (PiInfo t) where
export export
Reify LazyReason where Reify LazyReason where
reify defs (NDCon _ (NS _ (UN "LInf")) _ _ []) reify defs val@(NDCon _ n _ _ _)
= pure LInf = case !(full (gamma defs) n) of
reify defs (NDCon _ (NS _ (UN "LLazy")) _ _ []) NS _ (UN "LInf") => pure LInf
= pure LLazy NS _ (UN "LLazy") => pure LLazy
reify defs (NDCon _ (NS _ (UN "LUnknown")) _ _ []) NS _ (UN "LUnknown") => pure LUnknown
= pure LUnknown _ => cantReify val "LazyReason"
reify defs val = cantReify val "LazyReason" reify defs val = cantReify val "LazyReason"
export export
@ -411,13 +433,15 @@ Reflect LazyReason where
export export
Reify FC where Reify FC where
reify defs (NDCon _ (NS _ (UN "MkFC")) _ _ [fn, start, end]) reify defs val@(NDCon _ n _ _ args)
= do fn' <- reify defs !(evalClosure defs fn) = case (!(full (gamma defs) n), args) of
(NS _ (UN "MkFC"), [fn, start, end])
=> do fn' <- reify defs !(evalClosure defs fn)
start' <- reify defs !(evalClosure defs start) start' <- reify defs !(evalClosure defs start)
end' <- reify defs !(evalClosure defs start) end' <- reify defs !(evalClosure defs end)
pure (MkFC fn' start' end') pure (MkFC fn' start' end')
reify defs (NDCon _ (NS _ (UN "EmptyFC")) _ _ []) (NS _ (UN "EmptyFC"), _) => pure EmptyFC
= pure EmptyFC _ => cantReify val "FC"
reify defs val = cantReify val "FC" reify defs val = cantReify val "FC"
export export
@ -429,9 +453,12 @@ Reflect FC where
appCon fc defs (reflectiontt "MkFC") [fn', start', end'] appCon fc defs (reflectiontt "MkFC") [fn', start', end']
reflect fc defs env EmptyFC = getCon fc defs (reflectiontt "EmptyFC") reflect fc defs env EmptyFC = getCon fc defs (reflectiontt "EmptyFC")
{-
-- Reflection of well typed terms: We don't reify terms because that involves -- Reflection of well typed terms: We don't reify terms because that involves
-- type checking, but we can reflect them -- type checking, but we can reflect them
-- TODO: Do we need this? Fix reify if we do.
export export
Reflect (IsVar name idx vs) where Reflect (IsVar name idx vs) where
reflect fc defs env First reflect fc defs env First
@ -513,3 +540,4 @@ Reflect (Term vs) where
appCon fc defs (reflectiontt "TType") appCon fc defs (reflectiontt "TType")
[Erased fc False, tfc'] [Erased fc False, tfc']
reflect fc defs env val = cantReflect fc "Term" reflect fc defs env val = cantReflect fc "Term"
-}

9
src/Idris/Parser.idr
View File

@ -401,6 +401,11 @@ mutual
symbol "|]" symbol "|]"
end <- location end <- location
pure (PIdiom (MkFC fname start end) e) pure (PIdiom (MkFC fname start end) e)
<|> do start <- location
pragma "runElab"
e <- expr pdef fname indents
end <- location
pure (PRunElab (MkFC fname start end) e)
<|> do start <- location <|> do start <- location
pragma "logging" pragma "logging"
lvl <- intLit lvl <- intLit
@ -1035,7 +1040,9 @@ onoff
extension : Rule LangExt extension : Rule LangExt
extension extension
= do exactIdent "Borrowing" = do exactIdent "ElabReflection"
pure ElabReflection
<|> do exactIdent "Borrowing"
pure Borrowing pure Borrowing
totalityOpt : Rule TotalReq totalityOpt : Rule TotalReq

2
src/Parser/Lexer/Source.idr
View File

@ -174,7 +174,7 @@ reservedSymbols : List String
reservedSymbols reservedSymbols
= symbols ++ = symbols ++
["%", "\\", ":", "=", "|", "|||", "<-", "->", "=>", "?", "!", ["%", "\\", ":", "=", "|", "|||", "<-", "->", "=>", "?", "!",
"&", "**", ".."] "&", "**", "..", "~"]
fromHexLit : String -> Integer fromHexLit : String -> Integer
fromHexLit str fromHexLit str

106
src/TTImp/Elab/RunElab.idr Normal file
View File

@ -0,0 +1,106 @@
module TTImp.Elab.RunElab
import Core.Context
import Core.Core
import Core.Env
import Core.GetType
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.Reflect
import Core.Unify
import Core.TT
import Core.Value
import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.Reflect
import TTImp.TTImp
import TTImp.Unelab
elabScript : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
FC -> ElabInfo -> NestedNames vars ->
Env Term vars -> NF vars -> Maybe (Glued vars) ->
Core (NF vars)
elabScript fc elabinfo nest env (NDCon nfc nm t ar args) exp
= do defs <- get Ctxt
fnm <- toFullNames nm
case fnm of
NS ["Reflection", "Language"] (UN n)
=> elabCon defs n args
_ => failWith defs
where
failWith : Defs -> Core a
failWith defs
= do defs <- get Ctxt
empty <- clearDefs defs
throw (BadRunElab fc env !(quote empty env (NDCon nfc nm t ar args)))
scriptRet : Reflect a => a -> Core (NF vars)
scriptRet tm
= do defs <- get Ctxt
nfOpts withAll defs env !(reflect fc defs env tm)
elabCon : Defs -> String -> List (Closure vars) -> Core (NF vars)
elabCon defs "Pure" [_,val] = evalClosure defs val
elabCon defs "Bind" [_,_,act,k]
= do act' <- elabScript fc elabinfo nest env
!(evalClosure defs act) exp
case !(evalClosure defs k) of
NBind _ x (Lam _ _ _) sc =>
elabScript fc elabinfo nest env
!(sc defs (toClosure withAll env
!(quote defs env act'))) exp
_ => failWith defs
elabCon defs "LogMsg" [lvl, str]
= do lvl' <- evalClosure defs lvl
logC !(reify defs lvl') $
do str' <- evalClosure defs str
reify defs str'
scriptRet ()
elabCon defs "LogTerm" [lvl, str, tm]
= do lvl' <- evalClosure defs lvl
logC !(reify defs lvl') $
do str' <- evalClosure defs str
tm' <- evalClosure defs tm
pure $ !(reify defs str') ++ ": " ++
show (the RawImp !(reify defs tm'))
scriptRet ()
elabCon defs "Check" [ttimp] = evalClosure defs ttimp -- to be reified
elabCon defs "Goal" []
= do let Just gty = exp
| Nothing => nfOpts withAll defs env
!(reflect fc defs env (the (Maybe RawImp) Nothing))
ty <- getTerm gty
scriptRet (Just !(unelabNoSugar env ty))
elabCon defs n args = failWith defs
elabScript fc elabinfo nest env script exp
= do defs <- get Ctxt
empty <- clearDefs defs
throw (BadRunElab fc env !(quote empty env script))
export
checkRunElab : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkRunElab rig elabinfo nest env fc script exp
= do defs <- get Ctxt
when (not (isExtension ElabReflection defs)) $
throw (GenericMsg fc "%language ElabReflection not enabled")
(stm, sty) <- runDelays 0 $
check rig elabinfo nest env script Nothing
defs <- get Ctxt -- checking might have resolved some holes
ntm <- elabScript fc elabinfo nest env
!(nfOpts withAll defs env stm) exp
defs <- get Ctxt -- might have updated as part of the script
check rig elabinfo nest env !(reify defs ntm) exp

3
src/TTImp/Elab/Term.idr
View File

@ -28,6 +28,7 @@ import TTImp.Elab.Prim
import TTImp.Elab.Quote import TTImp.Elab.Quote
import TTImp.Elab.Record import TTImp.Elab.Record
import TTImp.Elab.Rewrite import TTImp.Elab.Rewrite
import TTImp.Elab.RunElab
import TTImp.Reflect import TTImp.Reflect
import TTImp.TTImp import TTImp.TTImp
@ -182,7 +183,7 @@ checkTerm rig elabinfo nest env (IQuoteDecl fc tm) exp
checkTerm rig elabinfo nest env (IUnquote fc tm) exp checkTerm rig elabinfo nest env (IUnquote fc tm) exp
= throw (GenericMsg fc "Can't escape outside a quoted term") = throw (GenericMsg fc "Can't escape outside a quoted term")
checkTerm rig elabinfo nest env (IRunElab fc tm) exp checkTerm rig elabinfo nest env (IRunElab fc tm) exp
= throw (GenericMsg fc "RunElab not implemented yet") = checkRunElab rig elabinfo nest env fc tm exp
checkTerm {vars} rig elabinfo nest env (IPrimVal fc c) exp checkTerm {vars} rig elabinfo nest env (IPrimVal fc c) exp
= do let (cval, cty) = checkPrim {vars} fc c = do let (cval, cty) = checkPrim {vars} fc c
checkExp rig elabinfo env fc cval (gnf env cty) exp checkExp rig elabinfo env fc cval (gnf env cty) exp

323
src/TTImp/Reflect.idr
View File

@ -13,13 +13,14 @@ import TTImp.TTImp
export export
Reify BindMode where Reify BindMode where
reify defs (NDCon _ (NS _ (UN "PI")) _ _ [c]) reify defs val@(NDCon _ n _ _ args)
= do c' <- reify defs !(evalClosure defs c) = case (!(full (gamma defs) n), args) of
(NS _ (UN "PI"), [c])
=> do c' <- reify defs !(evalClosure defs c)
pure (PI c') pure (PI c')
reify defs (NDCon _ (NS _ (UN "PATTERN")) _ _ _) (NS _ (UN "PATTERN"), _) => pure PATTERN
= pure PATTERN (NS _ (UN "NONE"), _) => pure NONE
reify defs (NDCon _ (NS _ (UN "NONE")) _ _ _) _ => cantReify val "BindMode"
= pure NONE
reify deva val = cantReify val "BindMode" reify deva val = cantReify val "BindMode"
export export
@ -34,10 +35,11 @@ Reflect BindMode where
export export
Reify UseSide where Reify UseSide where
reify defs (NDCon _ (NS _ (UN "UseLeft")) _ _ _) reify defs val@(NDCon _ n _ _ args)
= pure UseLeft = case (!(full (gamma defs) n), args) of
reify defs (NDCon _ (NS _ (UN "UseRight")) _ _ _) (NS _ (UN "UseLeft"), _) => pure UseLeft
= pure UseRight (NS _ (UN "UseRight"), _) => pure UseRight
_ => cantReify val "UseSide"
reify defs val = cantReify val "UseSide" reify defs val = cantReify val "UseSide"
export export
@ -49,18 +51,15 @@ Reflect UseSide where
export export
Reify DotReason where Reify DotReason where
reify defs (NDCon _ (NS _ (UN "NonLinearVar")) _ _ _) reify defs val@(NDCon _ n _ _ args)
= pure NonLinearVar = case (!(full (gamma defs) n), args) of
reify defs (NDCon _ (NS _ (UN "VarApplied")) _ _ _) (NS _ (UN "NonLinearVar"), _) => pure NonLinearVar
= pure VarApplied (NS _ (UN "VarApplied"), _) => pure VarApplied
reify defs (NDCon _ (NS _ (UN "NotConstructor")) _ _ _) (NS _ (UN "NotConstructor"), _) => pure NotConstructor
= pure NotConstructor (NS _ (UN "ErasedArg"), _) => pure ErasedArg
reify defs (NDCon _ (NS _ (UN "ErasedArg")) _ _ _) (NS _ (UN "UserDotted"), _) => pure UserDotted
= pure ErasedArg (NS _ (UN "UnknownDot"), _) => pure UnknownDot
reify defs (NDCon _ (NS _ (UN "UserDotted")) _ _ _) _ => cantReify val "DotReason"
= pure UserDotted
reify defs (NDCon _ (NS _ (UN "UnknownDot")) _ _ _)
= pure UnknownDot
reify defs val = cantReify val "DotReason" reify defs val = cantReify val "DotReason"
export export
@ -81,323 +80,347 @@ Reflect DotReason where
mutual mutual
export export
Reify RawImp where Reify RawImp where
reify defs (NDCon _ (NS _ (UN "IVar")) _ _ [fc, n]) reify defs val@(NDCon _ n _ _ args)
= do fc' <- reify defs !(evalClosure defs fc) = case (!(full (gamma defs) n), args) of
(NS _ (UN "IVar"), [fc, n])
=> do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (IVar fc' n') pure (IVar fc' n')
reify defs (NDCon _ (NS _ (UN "IPi")) _ _ [fc, c, p, mn, aty, rty]) (NS _ (UN "IPi"), [fc, c, p, mn, aty, rty])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
c' <- reify defs !(evalClosure defs c) c' <- reify defs !(evalClosure defs c)
p' <- reify defs !(evalClosure defs p) p' <- reify defs !(evalClosure defs p)
mn' <- reify defs !(evalClosure defs mn) mn' <- reify defs !(evalClosure defs mn)
aty' <- reify defs !(evalClosure defs aty) aty' <- reify defs !(evalClosure defs aty)
rty' <- reify defs !(evalClosure defs rty) rty' <- reify defs !(evalClosure defs rty)
pure (IPi fc' c' p' mn' aty' rty') pure (IPi fc' c' p' mn' aty' rty')
reify defs (NDCon _ (NS _ (UN "ILam")) _ _ [fc, c, p, mn, aty, lty]) (NS _ (UN "ILam"), [fc, c, p, mn, aty, lty])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
c' <- reify defs !(evalClosure defs c) c' <- reify defs !(evalClosure defs c)
p' <- reify defs !(evalClosure defs p) p' <- reify defs !(evalClosure defs p)
mn' <- reify defs !(evalClosure defs mn) mn' <- reify defs !(evalClosure defs mn)
aty' <- reify defs !(evalClosure defs aty) aty' <- reify defs !(evalClosure defs aty)
lty' <- reify defs !(evalClosure defs lty) lty' <- reify defs !(evalClosure defs lty)
pure (ILam fc' c' p' mn' aty' lty') pure (ILam fc' c' p' mn' aty' lty')
reify defs (NDCon _ (NS _ (UN "ILet")) _ _ [fc, c, n, ty, val, sc]) (NS _ (UN "ILet"), [fc, c, n, ty, val, sc])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
c' <- reify defs !(evalClosure defs c) c' <- reify defs !(evalClosure defs c)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
ty' <- reify defs !(evalClosure defs ty) ty' <- reify defs !(evalClosure defs ty)
val' <- reify defs !(evalClosure defs val) val' <- reify defs !(evalClosure defs val)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
pure (ILet fc' c' n' ty' val' sc') pure (ILet fc' c' n' ty' val' sc')
reify defs (NDCon _ (NS _ (UN "ICase")) _ _ [fc, sc, ty, cs]) (NS _ (UN "ICase"), [fc, sc, ty, cs])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
ty' <- reify defs !(evalClosure defs ty) ty' <- reify defs !(evalClosure defs ty)
cs' <- reify defs !(evalClosure defs cs) cs' <- reify defs !(evalClosure defs cs)
pure (ICase fc' sc' ty' cs') pure (ICase fc' sc' ty' cs')
reify defs (NDCon _ (NS _ (UN "ILocal")) _ _ [fc, ds, sc]) (NS _ (UN "ILocal"), [fc, ds, sc])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
ds' <- reify defs !(evalClosure defs ds) ds' <- reify defs !(evalClosure defs ds)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
pure (ILocal fc' ds' sc') pure (ILocal fc' ds' sc')
reify defs (NDCon _ (NS _ (UN "IUpdate")) _ _ [fc, ds, sc]) (NS _ (UN "IUpdate"), [fc, ds, sc])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
ds' <- reify defs !(evalClosure defs ds) ds' <- reify defs !(evalClosure defs ds)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
pure (IUpdate fc' ds' sc') pure (IUpdate fc' ds' sc')
reify defs (NDCon _ (NS _ (UN "IApp")) _ _ [fc, f, a]) (NS _ (UN "IApp"), [fc, f, a])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f) f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a) a' <- reify defs !(evalClosure defs a)
pure (IApp fc' f' a') pure (IApp fc' f' a')
reify defs (NDCon _ (NS _ (UN "IImplicitApp")) _ _ [fc, f, m, a]) (NS _ (UN "IImplicitApp"), [fc, f, m, a])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f) f' <- reify defs !(evalClosure defs f)
m' <- reify defs !(evalClosure defs m) m' <- reify defs !(evalClosure defs m)
a' <- reify defs !(evalClosure defs a) a' <- reify defs !(evalClosure defs a)
pure (IImplicitApp fc' f' m' a') pure (IImplicitApp fc' f' m' a')
reify defs (NDCon _ (NS _ (UN "IWithApp")) _ _ [fc, f, a]) (NS _ (UN "IWithApp"), [fc, f, a])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f) f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a) a' <- reify defs !(evalClosure defs a)
pure (IWithApp fc' f' a') pure (IWithApp fc' f' a')
reify defs (NDCon _ (NS _ (UN "ISearch")) _ _ [fc, d]) (NS _ (UN "ISearch"), [fc, d])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
d' <- reify defs !(evalClosure defs d) d' <- reify defs !(evalClosure defs d)
pure (ISearch fc' d') pure (ISearch fc' d')
reify defs (NDCon _ (NS _ (UN "IAlternative")) _ _ [fc, t, as]) (NS _ (UN "IAlternative"), [fc, t, as])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
as' <- reify defs !(evalClosure defs as) as' <- reify defs !(evalClosure defs as)
pure (IAlternative fc' t' as') pure (IAlternative fc' t' as')
reify defs (NDCon _ (NS _ (UN "IRewrite")) _ _ [fc, t, sc]) (NS _ (UN "IRewrite"), [fc, t, sc])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
pure (IRewrite fc' t' sc') pure (IRewrite fc' t' sc')
reify defs (NDCon _ (NS _ (UN "IBindHere")) _ _ [fc, t, sc]) (NS _ (UN "IBindHere"), [fc, t, sc])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
sc' <- reify defs !(evalClosure defs sc) sc' <- reify defs !(evalClosure defs sc)
pure (IBindHere fc' t' sc') pure (IBindHere fc' t' sc')
reify defs (NDCon _ (NS _ (UN "IBindVar")) _ _ [fc, n]) (NS _ (UN "IBindVar"), [fc, n])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (IBindVar fc' n') pure (IBindVar fc' n')
reify defs (NDCon _ (NS _ (UN "IAs")) _ _ [fc, s, n, t]) (NS _ (UN "IAs"), [fc, s, n, t])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
s' <- reify defs !(evalClosure defs s) s' <- reify defs !(evalClosure defs s)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IAs fc' s' n' t') pure (IAs fc' s' n' t')
reify defs (NDCon _ (NS _ (UN "IMustUnify")) _ _ [fc, r, t]) (NS _ (UN "IMustUnify"), [fc, r, t])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
r' <- reify defs !(evalClosure defs r) r' <- reify defs !(evalClosure defs r)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IMustUnify fc' r' t') pure (IMustUnify fc' r' t')
reify defs (NDCon _ (NS _ (UN "IDelayed")) _ _ [fc, r, t]) (NS _ (UN "IDelayed"), [fc, r, t])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
r' <- reify defs !(evalClosure defs r) r' <- reify defs !(evalClosure defs r)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IDelayed fc' r' t') pure (IDelayed fc' r' t')
reify defs (NDCon _ (NS _ (UN "IDelay")) _ _ [fc, t]) (NS _ (UN "IDelay"), [fc, t])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IDelay fc' t') pure (IDelay fc' t')
reify defs (NDCon _ (NS _ (UN "IForce")) _ _ [fc, t]) (NS _ (UN "IForce"), [fc, t])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IForce fc' t') pure (IForce fc' t')
reify defs (NDCon _ (NS _ (UN "IQuote")) _ _ [fc, t]) (NS _ (UN "IQuote"), [fc, t])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IQuote fc' t') pure (IQuote fc' t')
reify defs (NDCon _ (NS _ (UN "IQuoteDecl")) _ _ [fc, t]) (NS _ (UN "IQuoteDecl"), [fc, t])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IQuoteDecl fc' t') pure (IQuoteDecl fc' t')
reify defs (NDCon _ (NS _ (UN "IUnquote")) _ _ [fc, t]) (NS _ (UN "IUnquote"), [fc, t])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IUnquote fc' t') pure (IUnquote fc' t')
reify defs (NDCon _ (NS _ (UN "IPrimVal")) _ _ [fc, t]) (NS _ (UN "IPrimVal"), [fc, t])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IPrimVal fc' t') pure (IPrimVal fc' t')
reify defs (NDCon _ (NS _ (UN "IType")) _ _ [fc]) (NS _ (UN "IType"), [fc])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
pure (IType fc') pure (IType fc')
reify defs (NDCon _ (NS _ (UN "IHole")) _ _ [fc, n]) (NS _ (UN "IHole"), [fc, n])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (IHole fc' n') pure (IHole fc' n')
reify defs (NDCon _ (NS _ (UN "Implicit")) _ _ [fc, n]) (NS _ (UN "Implicit"), [fc, n])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
n' <- reify defs !(evalClosure defs n) n' <- reify defs !(evalClosure defs n)
pure (Implicit fc' n') pure (Implicit fc' n')
reify defs (NDCon _ (NS _ (UN "IWithUnambigNames")) _ _ [fc, ns, t]) (NS _ (UN "IWithUnambigNames"), [fc, ns, t])
= do fc' <- reify defs !(evalClosure defs fc) => do fc' <- reify defs !(evalClosure defs fc)
ns' <- reify defs !(evalClosure defs ns) ns' <- reify defs !(evalClosure defs ns)
t' <- reify defs !(evalClosure defs t) t' <- reify defs !(evalClosure defs t)
pure (IWithUnambigNames fc' ns' t') pure (IWithUnambigNames fc' ns' t')
_ => cantReify val "TTImp"
reify defs val = cantReify val "TTImp" reify defs val = cantReify val "TTImp"
export export
Reify IFieldUpdate where Reify IFieldUpdate where
reify defs (NDCon _ (NS _ (UN "ISetField")) _ _ [x, y]) reify defs val@(NDCon _ n _ _ args)
= do x' <- reify defs !(evalClosure defs x) = case (!(full (gamma defs) n), args) of
(NS _ (UN "ISetField"), [x, y])
=> do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
pure (ISetField x' y') pure (ISetField x' y')
reify defs (NDCon _ (NS _ (UN "ISetFieldApp")) _ _ [x, y]) (NS _ (UN "ISetFieldApp"), [x, y])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
pure (ISetFieldApp x' y') pure (ISetFieldApp x' y')
_ => cantReify val "IFieldUpdate"
reify defs val = cantReify val "IFieldUpdate" reify defs val = cantReify val "IFieldUpdate"
export export
Reify AltType where Reify AltType where
reify defs (NDCon _ (NS _ (UN "FirstSuccess")) _ _ _) reify defs val@(NDCon _ n _ _ args)
= pure FirstSuccess = case (!(full (gamma defs) n), args) of
reify defs (NDCon _ (NS _ (UN "Unique")) _ _ _) (NS _ (UN "FirstSuccess"), _)
= pure Unique => pure FirstSuccess
reify defs (NDCon _ (NS _ (UN "UniqueDefault")) _ _ [x]) (NS _ (UN "Unique"), _)
= do x' <- reify defs !(evalClosure defs x) => pure Unique
(NS _ (UN "UniqueDefault"), [x])
=> do x' <- reify defs !(evalClosure defs x)
pure (UniqueDefault x') pure (UniqueDefault x')
_ => cantReify val "AltType"
reify defs val = cantReify val "AltType" reify defs val = cantReify val "AltType"
export export
Reify FnOpt where Reify FnOpt where
reify defs (NDCon _ (NS _ (UN "Inline")) _ _ _) reify defs val@(NDCon _ n _ _ args)
= pure Inline = case (!(full (gamma defs) n), args) of
reify defs (NDCon _ (NS _ (UN "TCInline")) _ _ _) (NS _ (UN "Inline"), _) => pure Inline
= pure TCInline (NS _ (UN "TCInline"), _) => pure TCInline
reify defs (NDCon _ (NS _ (UN "Hint")) _ _ [x]) (NS _ (UN "Hint"), [x])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (Hint x') pure (Hint x')
reify defs (NDCon _ (NS _ (UN "GlobalHint")) _ _ [x]) (NS _ (UN "GlobalHint"), [x])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (GlobalHint x') pure (GlobalHint x')
reify defs (NDCon _ (NS _ (UN "ExternFn")) _ _ _) (NS _ (UN "ExternFn"), _) => pure ExternFn
= pure ExternFn (NS _ (UN "ForeignFn"), [x])
reify defs (NDCon _ (NS _ (UN "ForeignFn")) _ _ [x]) => do x' <- reify defs !(evalClosure defs x)
= do x' <- reify defs !(evalClosure defs x)
pure (ForeignFn x') pure (ForeignFn x')
reify defs (NDCon _ (NS _ (UN "Invertible")) _ _ _) (NS _ (UN "Invertible"), _) => pure Invertible
= pure Invertible (NS _ (UN "Totality"), [x])
reify defs (NDCon _ (NS _ (UN "Totality")) _ _ [x]) => do x' <- reify defs !(evalClosure defs x)
= do x' <- reify defs !(evalClosure defs x)
pure (Totality x') pure (Totality x')
reify defs (NDCon _ (NS _ (UN "Macro")) _ _ _) (NS _ (UN "Macro"), _) => pure Macro
= pure Macro (NS _ (UN "SpecArgs"), [x])
reify defs (NDCon _ (NS _ (UN "SpecArgs")) _ _ [x]) => do x' <- reify defs !(evalClosure defs x)
= do x' <- reify defs !(evalClosure defs x)
pure (SpecArgs x') pure (SpecArgs x')
_ => cantReify val "FnOpt"
reify defs val = cantReify val "FnOpt" reify defs val = cantReify val "FnOpt"
export export
Reify ImpTy where Reify ImpTy where
reify defs (NDCon _ (NS _ (UN "MkTy")) _ _ [x,y,z]) reify defs val@(NDCon _ n _ _ args)
= do x' <- reify defs !(evalClosure defs x) = case (!(full (gamma defs) n), args) of
(NS _ (UN "MkTy"), [x,y,z])
=> do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (MkImpTy x' y' z') pure (MkImpTy x' y' z')
_ => cantReify val "ITy"
reify defs val = cantReify val "ITy" reify defs val = cantReify val "ITy"
export export
Reify DataOpt where Reify DataOpt where
reify defs (NDCon _ (NS _ (UN "SearchBy")) _ _ [x]) reify defs val@(NDCon _ n _ _ args)
= do x' <- reify defs !(evalClosure defs x) = case (!(full (gamma defs) n), args) of
(NS _ (UN "SearchBy"), [x])
=> do x' <- reify defs !(evalClosure defs x)
pure (SearchBy x') pure (SearchBy x')
reify defs (NDCon _ (NS _ (UN "NoHints")) _ _ _) (NS _ (UN "NoHints"), _) => pure NoHints
= pure NoHints (NS _ (UN "UniqueSearch"), _) => pure UniqueSearch
reify defs (NDCon _ (NS _ (UN "UniqueSearch")) _ _ _) (NS _ (UN "External"), _) => pure External
= pure UniqueSearch (NS _ (UN "NoNewtype"), _) => pure NoNewtype
reify defs (NDCon _ (NS _ (UN "External")) _ _ _) _ => cantReify val "DataOpt"
= pure External
reify defs (NDCon _ (NS _ (UN "NoNewtype")) _ _ _)
= pure NoNewtype
reify defs val = cantReify val "DataOpt" reify defs val = cantReify val "DataOpt"
export export
Reify ImpData where Reify ImpData where
reify defs (NDCon _ (NS _ (UN "MkData")) _ _ [v,w,x,y,z]) reify defs val@(NDCon _ n _ _ args)
= do v' <- reify defs !(evalClosure defs v) = case (!(full (gamma defs) n), args) of
(NS _ (UN "MkData"), [v,w,x,y,z])
=> do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w) w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (MkImpData v' w' x' y' z') pure (MkImpData v' w' x' y' z')
reify defs (NDCon _ (NS _ (UN "MkLater")) _ _ [x,y,z]) (NS _ (UN "MkLater"), [x,y,z])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (MkImpLater x' y' z') pure (MkImpLater x' y' z')
_ => cantReify val "Data"
reify defs val = cantReify val "Data" reify defs val = cantReify val "Data"
export export
Reify IField where Reify IField where
reify defs (NDCon _ (NS _ (UN "MkIField")) _ _ [v,w,x,y,z]) reify defs val@(NDCon _ n _ _ args)
= do v' <- reify defs !(evalClosure defs v) = case (!(full (gamma defs) n), args) of
(NS _ (UN "MkIField"), [v,w,x,y,z])
=> do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w) w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (MkIField v' w' x' y' z') pure (MkIField v' w' x' y' z')
_ => cantReify val "IField"
reify defs val = cantReify val "IField" reify defs val = cantReify val "IField"
export export
Reify ImpRecord where Reify ImpRecord where
reify defs (NDCon _ (NS _ (UN "MkRecord")) _ _ [v,w,x,y,z]) reify defs val@(NDCon _ n _ _ args)
= do v' <- reify defs !(evalClosure defs v) = case (!(full (gamma defs) n), args) of
(NS _ (UN "MkRecord"), [v,w,x,y,z])
=> do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w) w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (MkImpRecord v' w' x' y' z') pure (MkImpRecord v' w' x' y' z')
_ => cantReify val "Record"
reify defs val = cantReify val "Record" reify defs val = cantReify val "Record"
export export
Reify ImpClause where Reify ImpClause where
reify defs (NDCon _ (NS _ (UN "PatClause")) _ _ [x,y,z]) reify defs val@(NDCon _ n _ _ args)
= do x' <- reify defs !(evalClosure defs x) = case (!(full (gamma defs) n), args) of
(NS _ (UN "PatClause"), [x,y,z])
=> do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (PatClause x' y' z') pure (PatClause x' y' z')
reify defs (NDCon _ (NS _ (UN "WithClause")) _ _ [w,x,y,z]) (NS _ (UN "WithClause"), [w,x,y,z])
= do w' <- reify defs !(evalClosure defs w) => do w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (WithClause w' x' y' [] z') pure (WithClause w' x' y' [] z')
reify defs (NDCon _ (NS _ (UN "ImpossibleClause")) _ _ [x,y]) (NS _ (UN "ImpossibleClause"), [x,y])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
pure (ImpossibleClause x' y') pure (ImpossibleClause x' y')
_ => cantReify val "Clause"
reify defs val = cantReify val "Clause" reify defs val = cantReify val "Clause"
export export
Reify ImpDecl where Reify ImpDecl where
reify defs (NDCon _ (NS _ (UN "IClaim")) _ _ [v,w,x,y,z]) reify defs val@(NDCon _ n _ _ args)
= do v' <- reify defs !(evalClosure defs v) = case (!(full (gamma defs) n), args) of
(NS _ (UN "IClaim"), [v,w,x,y,z])
=> do v' <- reify defs !(evalClosure defs v)
w' <- reify defs !(evalClosure defs w) w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (IClaim v' w' x' y' z') pure (IClaim v' w' x' y' z')
reify defs (NDCon _ (NS _ (UN "IData")) _ _ [x,y,z]) (NS _ (UN "IData"), [x,y,z])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (IData x' y' z') pure (IData x' y' z')
reify defs (NDCon _ (NS _ (UN "IDef")) _ _ [x,y,z]) (NS _ (UN "IDef"), [x,y,z])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (IDef x' y' z') pure (IDef x' y' z')
reify defs (NDCon _ (NS _ (UN "IParameters")) _ _ [x,y,z]) (NS _ (UN "IParameters"), [x,y,z])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (IParameters x' y' z') pure (IParameters x' y' z')
reify defs (NDCon _ (NS _ (UN "IRecord")) _ _ [x,y,z]) (NS _ (UN "IRecord"), [x,y,z])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (IRecord x' Nothing y' z') pure (IRecord x' Nothing y' z')
reify defs (NDCon _ (NS _ (UN "INamespace")) _ _ [w,x,y]) (NS _ (UN "INamespace"), [w,x,y])
= do w' <- reify defs !(evalClosure defs w) => do w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
pure (INamespace w' x' y') pure (INamespace w' x' y')
reify defs (NDCon _ (NS _ (UN "ITransform")) _ _ [w,x,y,z]) (NS _ (UN "ITransform"), [w,x,y,z])
= do w' <- reify defs !(evalClosure defs w) => do w' <- reify defs !(evalClosure defs w)
x' <- reify defs !(evalClosure defs x) x' <- reify defs !(evalClosure defs x)
y' <- reify defs !(evalClosure defs y) y' <- reify defs !(evalClosure defs y)
z' <- reify defs !(evalClosure defs z) z' <- reify defs !(evalClosure defs z)
pure (ITransform w' x' y' z') pure (ITransform w' x' y' z')
reify defs (NDCon _ (NS _ (UN "ILog")) _ _ [x]) (NS _ (UN "ILog"), [x])
= do x' <- reify defs !(evalClosure defs x) => do x' <- reify defs !(evalClosure defs x)
pure (ILog x') pure (ILog x')
_ => cantReify val "Decl"
reify defs val = cantReify val "Decl" reify defs val = cantReify val "Decl"
mutual mutual

2
tests/Main.idr
View File

@ -86,7 +86,7 @@ idrisTests
-- Records, access and dependent update -- Records, access and dependent update
"record001", "record002", "record003", "record004", "record001", "record002", "record003", "record004",
-- Quotation and reflection -- Quotation and reflection
"reflection001", "reflection001", "reflection002",
-- Miscellaneous regressions -- Miscellaneous regressions
"reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007", "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
"reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014", "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",

5
tests/idris2/reflection002/expected Normal file
View File

@ -0,0 +1,5 @@
1/1: Building power (power.idr)
Main> Main.cube : Nat -> Nat
cube = \x => mult x (mult x (mult x (const (fromInteger 1) x)))
Main> 27
Main> Bye for now!

3
tests/idris2/reflection002/input Normal file
View File

@ -0,0 +1,3 @@
:printdef cube
cube 3
:q

10
tests/idris2/reflection002/power.idr Normal file
View File

@ -0,0 +1,10 @@
import Language.Reflection
%language ElabReflection
powerFn : Nat -> TTImp
powerFn Z = `(const 1)
powerFn (S k) = `(\x => mult x (~(powerFn k) x))
cube : Nat -> Nat
cube = %runElab check (powerFn 3)

3
tests/idris2/reflection002/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-banner power.idr < input
rm -rf build