ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 03:34:13 +03:00
Code Issues Projects Releases Wiki Activity

Added top-level %runElab support

Browse Source 
Now, %runElab also works in a declaration context, eliminating the need
for a useless definition of type () when running for side effects.
This commit is contained in:
David Raymond Christiansen 2015-08-21 15:08:27 -07:00
parent fbb201c5ff
commit ab63941a04
15 changed files with 124 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
CHANGELOG
View File

@ -27,6 +27,8 @@ New in 0.9.19:
* Some improvements in interactive editing, particularly in lifting out
definitions and proof search.
* Moved System.Interactive, along with getArgs to the Prelude.
* Major improvements to reflected elaboration scripts, including the ability to run
them in a declaration context and many bug fixes.
New in 0.9.18:
--------------

1
idris.cabal
View File

@ -799,6 +799,7 @@ Library
, Idris.Elab.Class
, Idris.Elab.Instance
, Idris.Elab.Provider
, Idris.Elab.RunElab
, Idris.Elab.Transform
, Idris.Elab.Value
, Idris.Elab.Term

27
src/Idris/AbsSyntaxTree.hs
View File

@ -622,41 +622,41 @@ type ProvideWhat = ProvideWhat' PTerm
-- datatypes and typeclasses.
data PDecl' t
= PFix FC Fixity [String] -- ^ Fixity declaration
| PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)
| PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)
| PPostulate Bool -- external def if true
(Docstring (Either Err PTerm)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location
(Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location
| PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
| PCAF FC Name t -- ^ Top level constant
| PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
| PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
| PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
| PNamespace String FC [PDecl' t]
-- ^ New namespace, where FC is accurate location of the
-- namespace in the file
| PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
| PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
Name -- Record name
FC -- Record name precise location
[(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
[(Name, Docstring (Either Err PTerm))] -- Param Docs
[((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields
[(Name, Docstring (Either Err t))] -- Param Docs
[((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
(Maybe (Name, FC)) -- Optional constructor name and location
(Docstring (Either Err PTerm)) -- Constructor doc
(Docstring (Either Err t)) -- Constructor doc
SyntaxInfo -- Constructor SyntaxInfo
-- ^ Record declaration
| PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
| PClass (Docstring (Either Err t)) SyntaxInfo FC
[(Name, t)] -- constraints
Name -- class name
FC -- accurate location of class name
[(Name, FC, t)] -- parameters and precise locations
[(Name, Docstring (Either Err PTerm))] -- parameter docstrings
[(Name, Docstring (Either Err t))] -- parameter docstrings
[(Name, FC)] -- determining parameters and precise locations
[PDecl' t] -- declarations
(Maybe (Name, FC)) -- instance constructor name and location
(Docstring (Either Err PTerm)) -- instance constructor docs
(Docstring (Either Err t)) -- instance constructor docs
-- ^ Type class: arguments are documentation, syntax info, source location, constraints,
-- class name, class name location, parameters, method declarations, optional constructor name
| PInstance
(Docstring (Either Err PTerm)) -- Instance docs
[(Name, Docstring (Either Err PTerm))] -- Parameter docs
(Docstring (Either Err t)) -- Instance docs
[(Name, Docstring (Either Err t))] -- Parameter docs
SyntaxInfo
FC [(Name, t)] -- constraints
Name -- class
@ -672,9 +672,10 @@ data PDecl' t
| PSyntax FC Syntax -- ^ Syntax definition
| PMutual FC [PDecl' t] -- ^ Mutual block
| PDirective Directive -- ^ Compiler directive.
| PProvider (Docstring (Either Err PTerm)) SyntaxInfo FC FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term. The second FC is precise highlighting location.
| PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term. The second FC is precise highlighting location.
| PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
-- bool is True, lhs and rhs must be convertible
| PRunElabDecl FC t
deriving Functor
{-!
deriving instance Binary PDecl'

3
src/Idris/Core/Binary.hs
View File

@ -186,6 +186,8 @@ instance Binary a => Binary (Err' a) where
put f
put (NoValidAlts ns) = do putWord8 41
put ns
put (RunningElabScript e) = do putWord8 42
put e
get = do i <- getWord8
case i of
@ -256,6 +258,7 @@ instance Binary a => Binary (Err' a) where
40 -> do x <- get ; y <- get
return $ UnknownImplicit x y
41 -> fmap NoValidAlts get
42 -> fmap RunningElabScript get
_ -> error "Corrupted binary data for Err'"
----- Generated by 'derive'

1
src/Idris/Core/DeepSeq.hs
View File

@ -111,6 +111,7 @@ instance NFData Err where
rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
rnf (ElabScriptStuck x1) = rnf x1 `seq` ()
rnf (RunningElabScript x1) = rnf x1 `seq` ()
instance NFData ErrorReportPart where
rnf (TextPart x1) = rnf x1 `seq` ()

26
src/Idris/Core/Elaborate.hs
View File

@ -104,16 +104,24 @@ initNextNameFrom ns = do ES (p, a) s e <- get
maxName m (_ : xs) = maxName m xs
maxName m [] = m + 1
-- | Transform the error returned by an elaboration script, preserving
-- location information and proof search failure messages.
transformErr :: (Err -> Err) -> Elab' aux a -> Elab' aux a
transformErr f elab = do s <- get
case runStateT elab s of
OK (a, s') -> do put s'
return $! a
Error e -> lift $ Error (rewriteErr e)
where
rewriteErr (At f e) = At f (rewriteErr e)
rewriteErr (ProofSearchFail e) = ProofSearchFail (rewriteErr e)
rewriteErr e = f e
errAt :: String -> Name -> Elab' aux a -> Elab' aux a
errAt thing n elab = do s <- get
case runStateT elab s of
OK (a, s') -> do put s'
return $! a
Error e -> lift $ Error (rewriteErr e)
where
rewriteErr (At f e) = At f (rewriteErr e)
rewriteErr (ProofSearchFail e) = ProofSearchFail (rewriteErr e)
rewriteErr e = Elaborating thing n e
errAt thing n = transformErr (Elaborating thing n)
erun :: FC -> Elab' aux a -> Elab' aux a
erun f elab = do s <- get

1
src/Idris/Core/TT.hs
View File

@ -291,6 +291,7 @@ data Err' t
| ElabScriptDebug [ErrorReportPart] t [(Name, t, [(Name, Binder t)])]
-- ^ User-specified message, proof term, goals with context (first goal is focused)
| ElabScriptStuck t
| RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script
deriving (Eq, Functor, Data, Typeable)
type Err = Err' Term

2
src/Idris/DeepSeq.hs
View File

@ -196,6 +196,8 @@ instance (NFData t) => NFData (PDecl' t) where
rnf x5 `seq` rnf x6 `seq` ()
rnf (PTransform x1 x2 x3 x4)
= rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
rnf (PRunElabDecl x1 x2)
= rnf x1 `seq` rnf x2 `seq` ()
instance NFData t => NFData (ProvideWhat' t) where
rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()

2
src/Idris/Delaborate.hs
View File

@ -482,6 +482,8 @@ pprintErr' i (ElabScriptDebug msg tm holes) =
pprintErr' i (ElabScriptStuck tm) =
text "Can't run" <+> pprintTT [] tm <+> text "as an elaborator script." <$>
text "Is it a stuck term?"
pprintErr' i (RunningElabScript e) =
text "While running an elaboration script, the following error occurred" <> colon <$> pprintErr' i e
showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation
showPart ist (TextPart str) = fillSep . map text . words $ str

49
src/Idris/Elab/RunElab.hs Normal file
View File

@ -0,0 +1,49 @@
module Idris.Elab.RunElab (elabRunElab) where
import Idris.Elab.Term
import Idris.Elab.Value (elabVal)
import Idris.AbsSyntax
import Idris.Error
import Idris.Core.Elaborate hiding (Tactic (..))
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)
elabScriptTy :: Type
elabScriptTy = App Complete (P Ref (sNS (sUN "Elab") ["Elab", "Reflection", "Language"]) Erased)
(P Ref unitTy Erased)
mustBeElabScript :: Type -> Idris ()
mustBeElabScript ty =
do ctxt <- getContext
case converts ctxt [] ty elabScriptTy of
OK _ -> return ()
Error e -> ierror e
elabRunElab :: ElabInfo -> FC -> PTerm -> Idris ()
elabRunElab info fc script' =
do -- First elaborate the script itself
(script, scriptTy) <- elabVal info ERHS script'
mustBeElabScript scriptTy
ist <- getIState
ctxt <- getContext
(ElabResult tyT' defer is ctxt' newDecls highlights, log) <-
tclift $ elaborate ctxt (idris_datatypes ist) (sMN 0 "toplLevelElab") elabScriptTy initEState
(transformErr RunningElabScript
(erun fc (do tm <- runElabAction ist fc [] script [] --TODO namespace from parser
EState is _ impls highlights <- getAux
ctxt <- get_context
let ds = [] -- todo
log <- getLog
return (ElabResult tm ds (map snd is) ctxt impls highlights))))
setContext ctxt'
processTacticDecls info newDecls
sendHighlighting highlights

4
src/Idris/ElabDecls.hs
View File

@ -29,6 +29,7 @@ import Idris.Elab.Record
import Idris.Elab.Class
import Idris.Elab.Instance
import Idris.Elab.Provider
import Idris.Elab.RunElab
import Idris.Elab.Transform
import Idris.Elab.Value
@ -265,4 +266,7 @@ elabDecl' what info (PProvider doc syn fc nfc provWhat n)
elabDecl' what info (PTransform fc safety old new)
= do elabTransform info fc safety old new
return ()
elabDecl' what info (PRunElabDecl fc script)
= do elabRunElab info fc script
return ()
elabDecl' _ _ _ = return () -- skipped this time

6
src/Idris/IBC.hs
View File

@ -1262,6 +1262,9 @@ instance (Binary t) => Binary (PDecl' t) where
put x2
put x3
put x4
PRunElabDecl x1 x2 -> do putWord8 17
put x1
put x2
get
= do i <- getWord8
case i of
@ -1371,6 +1374,9 @@ instance (Binary t) => Binary (PDecl' t) where
x3 <- get
x4 <- get
return (PTransform x1 x2 x3 x4)
17 -> do x1 <- get
x2 <- get
return (PRunElabDecl x1 x2)
_ -> error "Corrupted binary data for PDecl'"
instance Binary t => Binary (ProvideWhat' t) where

18
src/Idris/Parser.hs
View File

@ -179,6 +179,7 @@ Decl ::=
| Provider
| Transform
| Import!
| RunElabDecl
;
@
-}
@ -231,6 +232,7 @@ decl' syn = fixity
<|> fnDecl' syn
<|> data_ syn
<|> record syn
<|> runElabDecl syn
<?> "declaration"
{- | Parses a syntax extension declaration (and adds the rule to parser state)
@ -1232,6 +1234,22 @@ transform syn = do try (lchar '%' *> reserved "transform")
return [PTransform fc False l r]
<?> "transform"
{- | Parses a top-level reflected elaborator script
@
RunElabDecl ::= '%' 'runElab' Expr
@
-}
runElabDecl :: SyntaxInfo -> IdrisParser PDecl
runElabDecl syn =
do kwFC <- try (do fc <- getFC
lchar '%'
fc' <- reservedFC "runElab"
return (spanFC fc fc'))
script <- expr syn <?> "elaborator script"
highlightP kwFC AnnKeyword
return $ PRunElabDecl kwFC script
<?> "top-level elaborator script"
{- * Loading and parsing -}
{- | Parses an expression from input -}

4
test/meta003/BadDef.idr
View File

@ -8,5 +8,5 @@ mkN n = NS (UN n) ["BadDef"]
mkBadDef1 : Elab ()
mkBadDef1 = do declareType $ Declare (mkN "bad1") [] `(() -> ())
defineFunction $ DefineFun (mkN "bad1") [MkFunClause `(():()) `("hi")]
runBad1 : ()
runBad1 = %runElab (mkBadDef1 *> search)
%runElab mkBadDef1

4
test/meta003/expected
View File

@ -1,5 +1,5 @@
BadDef.idr:12:9:
When checking right hand side of runBad1:
BadDef.idr:12:1-9:
While running an elaboration script, the following error occurred:
Type mismatch between
()
and