ab63941 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added top-level %runElab support

Now, %runElab also works in a declaration context, eliminating the need for a useless definition of type () when running for side effects.

commitab63941a040e53f8dd41318174d204c62ac7c4a5 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 21 Aug 2015, 15:08 (11 years ago) parentfbb201c

15 files changed+124−26

compare with master

unifiedsplit

CHANGELOG+2 idris.cabal+1 src/Idris/AbsSyntaxTree.hs+14−13 src/Idris/Core/Binary.hs+3 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/Elaborate.hs+17−9 src/Idris/Core/TT.hs+1 src/Idris/DeepSeq.hs+2 src/Idris/Delaborate.hs+2 src/Idris/Elab/RunElab.hs+49 src/Idris/ElabDecls.hs+4 src/Idris/IBC.hs+6 src/Idris/Parser.hs+18 test/meta003/BadDef.idr+2−2 test/meta003/expected+2−2

CHANGELOG+2

@@ -27,6 +27,8 @@ New in 0.9.19:

2727* Some improvements in interactive editing, particularly in lifting out

2828 definitions and proof search.

2929* Moved System.Interactive, along with getArgs to the Prelude.

30+* Major improvements to reflected elaboration scripts, including the ability to run

31+ them in a declaration context and many bug fixes.

3032

3133New in 0.9.18:

3234--------------

idris.cabal+1

@@ -799,6 +799,7 @@ Library

799799 , Idris.Elab.Class

800800 , Idris.Elab.Instance

801801 , Idris.Elab.Provider

802+ , Idris.Elab.RunElab

802803 , Idris.Elab.Transform

803804 , Idris.Elab.Value

804805 , Idris.Elab.Term

src/Idris/AbsSyntaxTree.hs+14−13

@@ -622,41 +622,41 @@ type ProvideWhat = ProvideWhat' PTerm

622622-- datatypes and typeclasses.

623623data PDecl' t

624624 = PFix FC Fixity [String] -- ^ Fixity declaration

625− | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)

625+ | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)

626626 | PPostulate Bool -- external def if true

627− (Docstring (Either Err PTerm)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location

627+ (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location

628628 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

629629 | PCAF FC Name t -- ^ Top level constant

630− | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

630+ | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

631631 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

632632 | PNamespace String FC [PDecl' t]

633633 -- ^ New namespace, where FC is accurate location of the

634634 -- namespace in the file

635− | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts

635+ | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts

636636 Name -- Record name

637637 FC -- Record name precise location

638638 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span

639− [(Name, Docstring (Either Err PTerm))] -- Param Docs

640− [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields

639+ [(Name, Docstring (Either Err t))] -- Param Docs

640+ [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields

641641 (Maybe (Name, FC)) -- Optional constructor name and location

642− (Docstring (Either Err PTerm)) -- Constructor doc

642+ (Docstring (Either Err t)) -- Constructor doc

643643 SyntaxInfo -- Constructor SyntaxInfo

644644 -- ^ Record declaration

645− | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC

645+ | PClass (Docstring (Either Err t)) SyntaxInfo FC

646646 [(Name, t)] -- constraints

647647 Name -- class name

648648 FC -- accurate location of class name

649649 [(Name, FC, t)] -- parameters and precise locations

650− [(Name, Docstring (Either Err PTerm))] -- parameter docstrings

650+ [(Name, Docstring (Either Err t))] -- parameter docstrings

651651 [(Name, FC)] -- determining parameters and precise locations

652652 [PDecl' t] -- declarations

653653 (Maybe (Name, FC)) -- instance constructor name and location

654− (Docstring (Either Err PTerm)) -- instance constructor docs

654+ (Docstring (Either Err t)) -- instance constructor docs

655655 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

656656 -- class name, class name location, parameters, method declarations, optional constructor name

657657 | PInstance

658− (Docstring (Either Err PTerm)) -- Instance docs

659− [(Name, Docstring (Either Err PTerm))] -- Parameter docs

658+ (Docstring (Either Err t)) -- Instance docs

659+ [(Name, Docstring (Either Err t))] -- Parameter docs

660660 SyntaxInfo

661661 FC [(Name, t)] -- constraints

662662 Name -- class

@@ -672,9 +672,10 @@ data PDecl' t

672672 | PSyntax FC Syntax -- ^ Syntax definition

673673 | PMutual FC [PDecl' t] -- ^ Mutual block

674674 | PDirective Directive -- ^ Compiler directive.

675− | 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.

675+ | 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.

676676 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

677677 -- bool is True, lhs and rhs must be convertible

678+ | PRunElabDecl FC t

678679 deriving Functor

679680{-!

680681deriving instance Binary PDecl'

src/Idris/Core/Binary.hs+3

@@ -186,6 +186,8 @@ instance Binary a => Binary (Err' a) where

186186 put f

187187 put (NoValidAlts ns) = do putWord8 41

188188 put ns

189+ put (RunningElabScript e) = do putWord8 42

190+ put e

189191

190192 get = do i <- getWord8

191193 case i of

@@ -256,6 +258,7 @@ instance Binary a => Binary (Err' a) where

256258 40 -> do x <- get ; y <- get

257259 return $ UnknownImplicit x y

258260 41 -> fmap NoValidAlts get

261+ 42 -> fmap RunningElabScript get

259262 _ -> error "Corrupted binary data for Err'"

260263----- Generated by 'derive'

261264

src/Idris/Core/DeepSeq.hs+1

@@ -111,6 +111,7 @@ instance NFData Err where

111111 rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

112112 rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

113113 rnf (ElabScriptStuck x1) = rnf x1 `seq` ()

114+ rnf (RunningElabScript x1) = rnf x1 `seq` ()

114115

115116instance NFData ErrorReportPart where

116117 rnf (TextPart x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+17−9

@@ -104,16 +104,24 @@ initNextNameFrom ns = do ES (p, a) s e <- get

104104 maxName m (_ : xs) = maxName m xs

105105 maxName m [] = m + 1

106106

107+

108+-- | Transform the error returned by an elaboration script, preserving

109+-- location information and proof search failure messages.

110+transformErr :: (Err -> Err) -> Elab' aux a -> Elab' aux a

111+transformErr f elab = do s <- get

112+ case runStateT elab s of

113+ OK (a, s') -> do put s'

114+ return $! a

115+ Error e -> lift $ Error (rewriteErr e)

116+

117+ where

118+ rewriteErr (At f e) = At f (rewriteErr e)

119+ rewriteErr (ProofSearchFail e) = ProofSearchFail (rewriteErr e)

120+ rewriteErr e = f e

121+

107122errAt :: String -> Name -> Elab' aux a -> Elab' aux a

108−errAt thing n elab = do s <- get

109− case runStateT elab s of

110− OK (a, s') -> do put s'

111− return $! a

112− Error e -> lift $ Error (rewriteErr e)

113− where

114− rewriteErr (At f e) = At f (rewriteErr e)

115− rewriteErr (ProofSearchFail e) = ProofSearchFail (rewriteErr e)

116− rewriteErr e = Elaborating thing n e

123+errAt thing n = transformErr (Elaborating thing n)

124+

117125

118126erun :: FC -> Elab' aux a -> Elab' aux a

119127erun f elab = do s <- get

src/Idris/Core/TT.hs+1

@@ -291,6 +291,7 @@ data Err' t

291291 | ElabScriptDebug [ErrorReportPart] t [(Name, t, [(Name, Binder t)])]

292292 -- ^ User-specified message, proof term, goals with context (first goal is focused)

293293 | ElabScriptStuck t

294+ | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script

294295 deriving (Eq, Functor, Data, Typeable)

295296

296297type Err = Err' Term

src/Idris/DeepSeq.hs+2

@@ -196,6 +196,8 @@ instance (NFData t) => NFData (PDecl' t) where

196196 rnf x5 `seq` rnf x6 `seq` ()

197197 rnf (PTransform x1 x2 x3 x4)

198198 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

199+ rnf (PRunElabDecl x1 x2)

200+ = rnf x1 `seq` rnf x2 `seq` ()

199201

200202instance NFData t => NFData (ProvideWhat' t) where

201203 rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()

src/Idris/Delaborate.hs+2

@@ -482,6 +482,8 @@ pprintErr' i (ElabScriptDebug msg tm holes) =

482482pprintErr' i (ElabScriptStuck tm) =

483483 text "Can't run" <+> pprintTT [] tm <+> text "as an elaborator script." <$>

484484 text "Is it a stuck term?"

485+pprintErr' i (RunningElabScript e) =

486+ text "While running an elaboration script, the following error occurred" <> colon <$> pprintErr' i e

485487

486488showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation

487489showPart ist (TextPart str) = fillSep . map text . words $ str

src/Idris/Elab/RunElab.hsnew file+49

@@ -0,0 +1,49 @@

1+module Idris.Elab.RunElab (elabRunElab) where

3+import Idris.Elab.Term

4+import Idris.Elab.Value (elabVal)

6+import Idris.AbsSyntax

7+import Idris.Error

9+import Idris.Core.Elaborate hiding (Tactic (..))

10+import Idris.Core.Evaluate

11+import Idris.Core.Execute

12+import Idris.Core.TT

13+import Idris.Core.Typecheck

14+

15+import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)

16+

17+elabScriptTy :: Type

18+elabScriptTy = App Complete (P Ref (sNS (sUN "Elab") ["Elab", "Reflection", "Language"]) Erased)

19+ (P Ref unitTy Erased)

20+

21+mustBeElabScript :: Type -> Idris ()

22+mustBeElabScript ty =

23+ do ctxt <- getContext

24+ case converts ctxt [] ty elabScriptTy of

25+ OK _ -> return ()

26+ Error e -> ierror e

27+

28+elabRunElab :: ElabInfo -> FC -> PTerm -> Idris ()

29+elabRunElab info fc script' =

30+ do -- First elaborate the script itself

31+ (script, scriptTy) <- elabVal info ERHS script'

32+ mustBeElabScript scriptTy

33+ ist <- getIState

34+ ctxt <- getContext

35+ (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-

36+ tclift $ elaborate ctxt (idris_datatypes ist) (sMN 0 "toplLevelElab") elabScriptTy initEState

37+ (transformErr RunningElabScript

38+ (erun fc (do tm <- runElabAction ist fc [] script [] --TODO namespace from parser

39+ EState is _ impls highlights <- getAux

40+ ctxt <- get_context

41+ let ds = [] -- todo

42+ log <- getLog

43+ return (ElabResult tm ds (map snd is) ctxt impls highlights))))

44+

45+

46+

47+ setContext ctxt'

48+ processTacticDecls info newDecls

49+ sendHighlighting highlights

src/Idris/ElabDecls.hs+4

@@ -29,6 +29,7 @@ import Idris.Elab.Record

2929import Idris.Elab.Class

3030import Idris.Elab.Instance

3131import Idris.Elab.Provider

32+import Idris.Elab.RunElab

3233import Idris.Elab.Transform

3334import Idris.Elab.Value

3435

@@ -265,4 +266,7 @@ elabDecl' what info (PProvider doc syn fc nfc provWhat n)

265266elabDecl' what info (PTransform fc safety old new)

266267 = do elabTransform info fc safety old new

267268 return ()

269+elabDecl' what info (PRunElabDecl fc script)

270+ = do elabRunElab info fc script

271+ return ()

268272elabDecl' _ _ _ = return () -- skipped this time

src/Idris/IBC.hs+6

@@ -1262,6 +1262,9 @@ instance (Binary t) => Binary (PDecl' t) where

12621262 put x2

12631263 put x3

12641264 put x4

1265+ PRunElabDecl x1 x2 -> do putWord8 17

1266+ put x1

1267+ put x2

12651268 get

12661269 = do i <- getWord8

12671270 case i of

@@ -1371,6 +1374,9 @@ instance (Binary t) => Binary (PDecl' t) where

13711374 x3 <- get

13721375 x4 <- get

13731376 return (PTransform x1 x2 x3 x4)

1377+ 17 -> do x1 <- get

1378+ x2 <- get

1379+ return (PRunElabDecl x1 x2)

13741380 _ -> error "Corrupted binary data for PDecl'"

13751381

13761382instance Binary t => Binary (ProvideWhat' t) where

src/Idris/Parser.hs+18

@@ -179,6 +179,7 @@ Decl ::=

179179 | Provider

180180 | Transform

181181 | Import!

182+ | RunElabDecl

182183 ;

183184@

184185-}

@@ -231,6 +232,7 @@ decl' syn = fixity

231232 <|> fnDecl' syn

232233 <|> data_ syn

233234 <|> record syn

235+ <|> runElabDecl syn

234236 <?> "declaration"

235237

236238{- | Parses a syntax extension declaration (and adds the rule to parser state)

@@ -1232,6 +1234,22 @@ transform syn = do try (lchar '%' *> reserved "transform")

12321234 return [PTransform fc False l r]

12331235 <?> "transform"

12341236

1237+{- | Parses a top-level reflected elaborator script

1238+

1239+@

1240+RunElabDecl ::= '%' 'runElab' Expr

1241+@

1242+-}

1243+runElabDecl :: SyntaxInfo -> IdrisParser PDecl

1244+runElabDecl syn =

1245+ do kwFC <- try (do fc <- getFC

1246+ lchar '%'

1247+ fc' <- reservedFC "runElab"

1248+ return (spanFC fc fc'))

1249+ script <- expr syn <?> "elaborator script"

1250+ highlightP kwFC AnnKeyword

1251+ return $ PRunElabDecl kwFC script

1252+ <?> "top-level elaborator script"

12351253

12361254{- * Loading and parsing -}

12371255{- | Parses an expression from input -}

test/meta003/BadDef.idr+2−2

@@ -8,5 +8,5 @@ mkN n = NS (UN n) ["BadDef"]

88mkBadDef1 : Elab ()

99mkBadDef1 = do declareType $ Declare (mkN "bad1") [] `(() -> ())

1010 defineFunction $ DefineFun (mkN "bad1") [MkFunClause `(():()) `("hi")]

11−runBad1 : ()

12−runBad1 = %runElab (mkBadDef1 *> search)

11+

12+%runElab mkBadDef1

test/meta003/expected+2−2

@@ -1,5 +1,5 @@

1−BadDef.idr:12:9:

2−When checking right hand side of runBad1:

1+BadDef.idr:12:1-9:

2+While running an elaboration script, the following error occurred:

33Type mismatch between

44 ()

55and