git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1621 from trillioneyes/repl-definitions

Repl definitions

commit8e265509a1c611f26cc4e22e66963b59f0457981 authorEdwin Brady <edwin.brady@gmail.com> dateSun 12 Oct 2014, 13:39 (12 years ago) parent72b9e951c8c27e
3 files changed+32−14
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+8−1 src/Idris/Parser.hs+21−12 src/Idris/REPL.hs+3−1
src/Idris/AbsSyntaxTree.hs+8−1
@@ -29,7 +29,7 @@ import qualified Data.Map as M
2929import Data.Either
3030import qualified Data.Set as S
3131import Data.Word (Word)
32−import Data.Maybe (fromMaybe)
32+import Data.Maybe (fromMaybe, mapMaybe)
3333import Data.Traversable (Traversable)
3434import Data.Foldable (Foldable)
3535
@@ -974,6 +974,11 @@ deriving instance NFData SynContext
974974
975975data Syntax = Rule [SSymbol] PTerm SynContext
976976 deriving Show
977+
978+syntaxNames :: Syntax -> [Name]
979+syntaxNames (Rule syms _ _) = mapMaybe ename syms
980+ where ename (Keyword n) = Just n
981+ ename _ = Nothing
977982{-!
978983deriving instance Binary Syntax
979984deriving instance NFData Syntax
@@ -985,6 +990,8 @@ data SSymbol = Keyword Name
985990 | Expr Name
986991 | SimpleExpr Name
987992 deriving Show
993+
994+
988995{-!
989996deriving instance Binary SSymbol
990997deriving instance NFData SSymbol
src/Idris/Parser.hs+21−12
@@ -216,19 +216,28 @@ decl' syn = fixity
216216-}
217217syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
218218syntaxDecl syn = do s <- syntaxRule syn
219− i <- get
220− let rs = syntax_rules i
221− let ns = syntax_keywords i
222− let ibc = ibc_write i
223− let ks = map show (names s)
224− put (i { syntax_rules = s : rs,
225− syntax_keywords = ks ++ ns,
226− ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
219+ i <- get
220+ put (i `addSyntax` s)
227221 fc <- getFC
228− return (PSyntax fc s)
229− where names (Rule syms _ _) = mapMaybe ename syms
230− ename (Keyword n) = Just n
231− ename _ = Nothing
222+ return (PSyntax fc s)
223+
224+-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
225+addSyntax :: IState -> Syntax -> IState
226+addSyntax i s = i { syntax_rules = s : rs,
227+ syntax_keywords = ks ++ ns,
228+ ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc }
229+ where rs = syntax_rules i
230+ ns = syntax_keywords i
231+ ibc = ibc_write i
232+ ks = map show (syntaxNames s)
233+
234+-- | Like 'addSyntax', but no effect on the IBC.
235+addReplSyntax :: IState -> Syntax -> IState
236+addReplSyntax i s = i { syntax_rules = s : rs,
237+ syntax_keywords = ks ++ ns }
238+ where rs = syntax_rules i
239+ ns = syntax_keywords i
240+ ks = map show (syntaxNames s)
232241
233242{- | Parses a syntax extension declaration
234243
src/Idris/REPL.hs+3−1
@@ -744,7 +744,9 @@ process fn (NewDefn decls) = do
744744 defineName (PFix fc fixity strs : defns) = do
745745 fmodifyState idris_fixities (map (Fix fixity) strs ++)
746746 unless (null defns) $ defineName defns
747− defineName (PSyntax{}:_) = tclift $ tfail (Msg "That kind of declaration is not supported. If you feel it should be supported, please submit an issue at https://github.com/idris-lang/Idris-dev.")
747+ defineName (PSyntax _ syntax:_) = do
748+ i <- get
749+ put (addReplSyntax i syntax)
748750 defineName decls = do
749751 elabDecls toplevel (map fixClauses decls)
750752 setReplDefined (getName (head decls))