b693b81 · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

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

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

28 definitions and proof search.

29* 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.

30

32

31New in 0.9.18:

33New in 0.9.18:

32--------------

34--------------

idris.cabal+1

@@ -803,6 +803,7 @@ Library

803 , Idris.Elab.Class

804 , Idris.Elab.Instance

805 , Idris.Elab.Provider

806+ , Idris.Elab.RunElab

806 , Idris.Elab.Transform

807 , Idris.Elab.Transform

807 , Idris.Elab.Value

808 , Idris.Elab.Value

808 , Idris.Elab.Term

809 , Idris.Elab.Term

src/Idris/AbsSyntaxTree.hs+14−13

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

622-- datatypes and typeclasses.

623data PDecl' t

624 = 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)

626 | 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

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

629 | 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.

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

632 | PNamespace String FC [PDecl' t]

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

634 -- namespace in the file

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

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

636 Name -- Record name

637 FC -- Record name precise location

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

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

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

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

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

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

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

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

643 SyntaxInfo -- Constructor SyntaxInfo

644 -- ^ Record declaration

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

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

646 [(Name, t)] -- constraints

647 Name -- class name

648 FC -- accurate location of class name

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

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

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

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

652 [PDecl' t] -- declarations

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

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

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

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

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

657 | PInstance

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

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

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

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

660 SyntaxInfo

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

662 Name -- class

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

672 | PSyntax FC Syntax -- ^ Syntax definition

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

674 | 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.

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

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

678+ | PRunElabDecl FC t

678 deriving Functor

679 deriving Functor

679{-!

680{-!

680deriving instance Binary PDecl'

681deriving instance Binary PDecl'

src/Idris/Core/Binary.hs+3

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

186 put f

187 put (NoValidAlts ns) = do putWord8 41

188 put ns

189+ put (RunningElabScript e) = do putWord8 42

190+ put e

189

191

190 get = do i <- getWord8

192 get = do i <- getWord8

191 case i of

193 case i of

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

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

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

257 return $ UnknownImplicit x y

259 return $ UnknownImplicit x y

258 41 -> fmap NoValidAlts get

260 41 -> fmap NoValidAlts get

261+ 42 -> fmap RunningElabScript get

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

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

260----- Generated by 'derive'

263----- Generated by 'derive'

261

264

src/Idris/Core/DeepSeq.hs+1

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

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

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

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

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

114

115

115instance NFData ErrorReportPart where

116instance NFData ErrorReportPart where

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

117 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

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

105 maxName m [] = m + 1

106

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+

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

122errAt :: 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+

117

125

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

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

119erun f elab = do s <- get

127erun f elab = do s <- get

src/Idris/Core/TT.hs+1

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

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

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

293 | ElabScriptStuck t

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

294 deriving (Eq, Functor, Data, Typeable)

295 deriving (Eq, Functor, Data, Typeable)

295

296

296type Err = Err' Term

297type Err = Err' Term

src/Idris/DeepSeq.hs+2

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

196 rnf x5 `seq` rnf x6 `seq` ()

197 rnf (PTransform x1 x2 x3 x4)

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

199+ rnf (PRunElabDecl x1 x2)

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

199

201

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

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

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

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

src/Idris/Delaborate.hs+6−2

@@ -289,7 +289,9 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

289 CantUnify _ (x_in', _) (y_in',_) _ _ _ | x_in == x_in' && y_in == y_in' -> empty

290 _ -> line <> line <> text "Specifically:" <>

291 indented (pprintErr' i e) <>

292− if (opt_errContext (idris_options i)) then showSc i sc else empty

292+ if (opt_errContext (idris_options i))

293+ then text "Unification failure" <$> showSc i sc

294+ else empty

293pprintErr' i (CantConvert x_in y_in env) =

295pprintErr' i (CantConvert x_in y_in env) =

294 let (x_ns, y_ns, nms) = renameMNs x_in y_in

296 let (x_ns, y_ns, nms) = renameMNs x_in y_in

295 (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))

297 (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))

@@ -300,7 +302,7 @@ pprintErr' i (CantConvert x_in y_in env) =

300 text "and" <>

302 text "and" <>

301 indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

303 indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

302 y)) <>

304 y)) <>

303− if (opt_errContext (idris_options i)) then line <> showSc i env else empty

305+ if (opt_errContext (idris_options i)) then line <> text "Conversion failure" <$> showSc i env else empty

304 where flagUnique (Bind n (Pi i t k@(UType u)) sc)

306 where flagUnique (Bind n (Pi i t k@(UType u)) sc)

305 = App Complete (P Ref (sUN (show u)) Erased)

307 = App Complete (P Ref (sUN (show u)) Erased)

306 (Bind n (Pi i (flagUnique t) k) (flagUnique sc))

308 (Bind n (Pi i (flagUnique t) k) (flagUnique sc))

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

480pprintErr' i (ElabScriptStuck tm) =

482pprintErr' i (ElabScriptStuck tm) =

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

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

482 text "Is it a stuck term?"

484 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

483

487

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

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

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

489showPart 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

2+

3+import Idris.Elab.Term

4+import Idris.Elab.Value (elabVal)

5+

6+import Idris.AbsSyntax

7+import Idris.Error

8+

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/Elab/Term.hs+7−3

@@ -1983,10 +1983,14 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1983 datatypes <- get_datatypes

1984 env <- get_env

1985 (_, ES (p, aux') _ _) <-

1986+ do (ES (current_p, _) _ _) <- get

1986− lift $ runElab aux (runElabAction ist fc [] script ns)

1987+ lift $ runElab aux (runElabAction ist fc [] script ns)

1987− (newProof recH ctxt datatypes goalTT)

1988+ ((newProof recH ctxt datatypes goalTT)

1989+ { nextname = nextname current_p})

1988 let tm_out = getProofTerm (pterm p)

1990 let tm_out = getProofTerm (pterm p)

1989− updateAux $ const aux'

1991+ do (ES (prf, _) s e) <- get

1992+ let p' = prf { nextname = nextname p }

1993+ put (ES (p', aux') s e)

1990 env' <- get_env

1994 env' <- get_env

1991 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out

1995 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out

1992 let (tm', ty') = (reflect tm, reflect ty)

1996 let (tm', ty') = (reflect tm, reflect ty)

src/Idris/ElabDecls.hs+4

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

29import Idris.Elab.Class

30import Idris.Elab.Instance

31import Idris.Elab.Provider

32+import Idris.Elab.RunElab

32import Idris.Elab.Transform

33import Idris.Elab.Transform

33import Idris.Elab.Value

34import Idris.Elab.Value

34

35

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

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

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

266 = do elabTransform info fc safety old new

267 = do elabTransform info fc safety old new

267 return ()

268 return ()

269+elabDecl' what info (PRunElabDecl fc script)

270+ = do elabRunElab info fc script

271+ return ()

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

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

src/Idris/IBC.hs+6

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

1262 put x2

1263 put x3

1264 put x4

1265+ PRunElabDecl x1 x2 -> do putWord8 17

1266+ put x1

1267+ put x2

1265 get

1268 get

1266 = do i <- getWord8

1269 = do i <- getWord8

1267 case i of

1270 case i of

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

1371 x3 <- get

1374 x3 <- get

1372 x4 <- get

1375 x4 <- get

1373 return (PTransform x1 x2 x3 x4)

1376 return (PTransform x1 x2 x3 x4)

1377+ 17 -> do x1 <- get

1378+ x2 <- get

1379+ return (PRunElabDecl x1 x2)

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

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

1375

1381

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

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

src/Idris/Parser.hs+18

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

179 | Provider

180 | Transform

181 | Import!

182+ | RunElabDecl

182 ;

183 ;

183@

184@

184-}

185-}

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

231 <|> fnDecl' syn

232 <|> fnDecl' syn

232 <|> data_ syn

233 <|> data_ syn

233 <|> record syn

234 <|> record syn

235+ <|> runElabDecl syn

234 <?> "declaration"

236 <?> "declaration"

235

237

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

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

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

1232 return [PTransform fc False l r]

1234 return [PTransform fc False l r]

1233 <?> "transform"

1235 <?> "transform"

1234

1236

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"

1235

1253

1236{- * Loading and parsing -}

1254{- * Loading and parsing -}

1237{- | Parses an expression from input -}

1255{- | Parses an expression from input -}

test/meta003/BadDef.idr+2−2

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

8mkBadDef1 : Elab ()

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

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

11−runBad1 : ()

11+

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

12+%runElab mkBadDef1

test/meta003/expected+2−2

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

1−BadDef.idr:12:9:

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

2−When checking right hand side of runBad1:

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

3Type mismatch between

4 ()

5and