idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 10:18:23 +03:00
Code Issues Projects Releases Wiki Activity

In reflection, check now takes a concrete type

Browse Source 
So the type of Elab now gives the expected type that's being elaborated
to, meaning that we can run 'check' in the middle of scripts and use the
result.
This commit is contained in:
Edwin Brady 2020-06-02 22:41:37 +01:00
parent ff4282f886
commit 2a75731916
9 changed files with 36 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -14,8 +14,8 @@ data Elab : Type -> Type where
LogMsg : Nat -> String -> Elab ()
LogTerm : Nat -> String -> TTImp -> Elab ()
-- Check a TTImp term against the current goal type
Check : TTImp -> Elab TT
-- Elaborate a TTImp term to a concrete value
Check : {expected : Type} -> TTImp -> Elab expected
-- Get the current goal type, if known
-- (it might need to be inferred from the solution)
Goal : Elab (Maybe TTImp)
@ -73,9 +73,8 @@ logGoal n msg
Nothing => pure ()
Just t => logTerm n msg t
-- Check a TTImp term against the current goal type
export
check : TTImp -> Elab TT
check : {expected : Type} -> TTImp -> Elab expected
check = Check
export

27
src/TTImp/Elab/RunElab.idr
View File

@ -75,7 +75,16 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp
pure $ !(reify defs str') ++ ": " ++
show (the RawImp !(reify defs tm'))
scriptRet ()
elabCon defs "Check" [ttimp] = evalClosure defs ttimp -- to be reified
elabCon defs "Check" [exp, ttimp]
= do exp' <- evalClosure defs exp
ttimp' <- evalClosure defs ttimp
tidx <- resolveName (UN "[elaborator script]")
e <- newRef EST (initEState tidx env)
(checktm, _) <- runDelays 0 $
check top (initElabInfo InExpr) nest env !(reify defs ttimp')
(Just (glueBack defs env exp'))
empty <- clearDefs defs
nf empty env checktm
elabCon defs "Goal" []
= do let Just gty = exp
| Nothing => nfOpts withAll defs env
@ -138,17 +147,23 @@ checkRunElab : {vars : _} ->
FC -> RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkRunElab rig elabinfo nest env fc script exp
= do defs <- get Ctxt
= do expected <- mkExpected exp
defs <- get Ctxt
when (not (isExtension ElabReflection defs)) $
throw (GenericMsg fc "%language ElabReflection not enabled")
let n = NS ["Reflection", "Language"] (UN "Elab")
let ttn = reflectiontt "TT"
tt <- getCon fc defs ttn
elabtt <- appCon fc defs n [tt]
elabtt <- appCon fc defs n [expected]
(stm, sty) <- runDelays 0 $
check rig elabinfo nest env script (Just (gnf env elabtt))
defs <- get Ctxt -- checking might have resolved some holes
ntm <- elabScript fc nest env
!(nfOpts withAll defs env stm) exp
!(nfOpts withAll defs env stm) (Just (gnf env expected))
defs <- get Ctxt -- might have updated as part of the script
check rig elabinfo nest env !(reify defs ntm) exp
pure (!(quote defs env ntm), gnf env expected)
where
mkExpected : Maybe (Glued vars) -> Core (Term vars)
mkExpected (Just ty) = pure !(getTerm ty)
mkExpected Nothing
= do nm <- genName "scriptTy"
metaVar fc erased env nm (TType fc)

2
tests/idris2/reflection002/expected
View File

@ -1,5 +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)))
cube = \x => mult x (mult x (mult x 1))
Main> 27
Main> Bye for now!

2
tests/idris2/reflection002/power.idr
View File

@ -7,7 +7,7 @@ powerFn Z = `(const 1)
powerFn (S k) = `(\x => mult x (~(powerFn k) x))
%macro
power : Nat -> Elab TT
power : Nat -> Elab (Nat -> Nat)
power n = check (powerFn n)
cube : Nat -> Nat

2
tests/idris2/reflection003/expected
View File

@ -12,4 +12,4 @@ Error during reflection: Still not trying
refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1:
Error during reflection: Undefined name
refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1:
Error during reflection: failed after generating Main.{plus:5817}
Error during reflection: failed after generating Main.{plus:5841}

8
tests/idris2/reflection003/refprims.idr
View File

@ -2,7 +2,7 @@ import Language.Reflection
%language ElabReflection
logPrims : Elab TT
logPrims : Elab a
logPrims
= do ns <- getType `{{ (++) }}
traverse (\ (n, ty) =>
@ -10,7 +10,7 @@ logPrims
logTerm 0 "Type" ty) ns
fail "Not really trying"
logDataCons : Elab TT
logDataCons : Elab a
logDataCons
= do [(n, _)] <- getType `{{ Nat }}
| _ => fail "Ambiguous name"
@ -18,7 +18,7 @@ logDataCons
logMsg 0 ("Constructors: " ++ show !(getCons n))
fail "Still not trying"
logBad : Elab TT
logBad : Elab a
logBad
= do [(n, _)] <- getType `{{ DoesntExist }}
| [] => fail "Undefined name"
@ -27,7 +27,7 @@ logBad
logMsg 0 ("Constructors: " ++ show !(getCons n))
fail "Still not trying"
tryGenSym : Elab TT
tryGenSym : Elab a
tryGenSym
= do n <- genSym "plus"
ns <- inCurrentNS n

2
tests/idris2/reflection004/refdecl.idr
View File

@ -2,7 +2,7 @@ import Language.Reflection
%language ElabReflection
logDecls : TTImp -> Elab TT
logDecls : TTImp -> Elab (Int -> Int)
logDecls v
= do declare [IClaim EmptyFC MW Public []
(MkTy EmptyFC `{{ Main.foo }}

4
tests/idris2/reflection005/expected
View File

@ -1,9 +1,9 @@
1/1: Building refdecl (refdecl.idr)
refdecl.idr:13:16--14:1:While processing right hand side of bad at refdecl.idr:13:1--14:1:
When unifying Elab () and Elab TT
When unifying Elab () and Elab a
Mismatch between:
()
and
TT
a
Main> 9400
Main> Bye for now!

4
tests/idris2/reflection006/refleq.idr
View File

@ -2,7 +2,7 @@ import Language.Reflection
%language ElabReflection
solveReflected : TTImp -> Elab TT
solveReflected : TTImp -> Elab any
solveReflected `(Builtin.Equal {a=_} {b=_} ~(left) ~(right))
= do logTerm 0 "Left" left
logTerm 0 "Right" right
@ -12,7 +12,7 @@ solveReflected g
fail "I don't know how to prove this"
%macro
prove : Elab TT
prove : Elab any
prove
= do env <- localVars
Just g <- goal