2402885 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Generic syntax declarations (see prelude.idr for example)

commit24028852ed165388731f58094f805fbd9eb8c6e3 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 16 Oct 2011, 19:35 (15 years ago) parent12bd089

5 files changed+80−7

compare with master

unifiedsplit

lib/prelude.idr+6 src/Core/CoreParser.hs+1−1 src/Idris/AbsSyntax.hs+13−4 src/Idris/ElabDecls.hs+3−1 src/Idris/Parser.hs+57−1

lib/prelude.idr+6

@@ -5,6 +5,12 @@ import io;

66data Bool = False | True;

8+boolElim : (x:Bool) -> a -> a -> a;

9+boolElim True t e = t;

10+boolElim False t e = e;

11+

12+syntax if [test] then [t] else [e] = boolElim test t e;

13+

814infixl 5 ==, /=, ==.;

915infixl 6 <, <=, >, >=, <., <=., >., >=.;

1016infixl 7 <<, >>;

src/Core/CoreParser.hs+1−1

@@ -17,7 +17,7 @@ idrisDef = haskellDef {

1717 opStart = iOpStart,

1818 opLetter = iOpLetter,

1919 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>"],

20− reservedNames = ["let", "in", "data", "Set", "if", "then", "else",

20+ reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",

2121 "do", "dsl", "import",

2222 "infix", "infixl", "infixr", "prefix",

2323 "where", "forall", "syntax",

src/Idris/AbsSyntax.hs+13−4

@@ -30,11 +30,12 @@ data IState = IState { tt_ctxt :: Context,

3030 idris_options :: IOption,

3131 idris_name :: Int,

3232 idris_metavars :: [Name],

33+ syntax_rules :: [Syntax],

3334 imported :: [FilePath],

3435 idris_prims :: [(Name, ([E.Name], E.Term))]

3536 }

3637

37−idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] [] []

38+idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] [] [] []

3839

3940-- The monad for the main REPL - reading and processing files and updating

4041-- global state (hence the IO inner monad).

@@ -134,7 +135,7 @@ data PDecl' t = PFix Fixity [String] -- fixity declaration

134135 | PClauses Name [PClause' t] -- pattern clause

135136 | PData (PData' t) -- data declaration

136137 | PParams [(Name, PTerm)] [PDecl' t] -- params block

137− | PImport String

138+ | PSyntax Syntax

138139 deriving Functor

139140

140141data PClause' t = PClause Name t t [PDecl]

@@ -160,7 +161,7 @@ declared (PTy n t) = [n]

160161declared (PClauses n _) = [] -- not a declaration

161162declared (PData (PDatadecl n _ ts)) = n : map fst ts

162163declared (PParams _ ds) = concatMap declared ds

163−declared (PImport _) = []

164+-- declared (PImport _) = []

164165

165166-- High level language terms

166167--

@@ -198,6 +199,13 @@ data DSL = DSL { dsl_bind :: Name,

198199 dsl_return :: Name }

199200 deriving Show

200201

202+data Syntax = Rule [SSymbol] PTerm

203+ deriving Show

204+

205+data SSymbol = Keyword Name

206+ | Expr Name

207+ deriving Show

208+

201209initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])

202210

203211data SyntaxInfo = Syn { using :: [(Name, PTerm)],

@@ -458,5 +466,6 @@ dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

458466dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)

459467dumpDecl (PData d) = showDImp True d

460468dumpDecl (PParams ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

461−dumpDecl (PImport i) = "import " ++ i

469+dumpDecl (PSyntax syn) = "syntax " ++ show syn

470+-- dumpDecl (PImport i) = "import " ++ i

462471

src/Idris/ElabDecls.hs+3−1

@@ -152,6 +152,7 @@ elabDecl :: ElabInfo -> PDecl -> Idris ()

152152elabDecl info d = idrisCatch (elabDecl' info d) (\e -> iputStrLn (report e))

153153

154154elabDecl' info (PFix _ _) = return () -- nothing to elaborate

155+elabDecl' info (PSyntax p) = return () -- nothing to elaborate

155156elabDecl' info (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n

156157 elabType info n ty

157158elabDecl' info (PData d) = do iLOG $ "Elaborating " ++ show (d_name d)

@@ -247,7 +248,8 @@ elab info pattern tm = do elab' tm

247248 elab' (PApp f [arg])

248249 = do simple_app (elab' f) (elab' (getTm arg))

249250 solve

250− elab' Placeholder = fail $ "Can't deal with a placeholder here"

251+ elab' Placeholder = do (h : hs) <- get_holes

252+ movelast h

251253 elab' (PMetavar n) = do attack; defer n; solve

252254 elab' (PElabError e) = fail e

253255 elab' x = fail $ "Not implemented " ++ show x

src/Idris/Parser.hs+57−1

@@ -16,6 +16,7 @@ import qualified Text.ParserCombinators.Parsec.Token as PTok

1616import Data.List

1717import Control.Monad.State

1818import Debug.Trace

19+import Data.Maybe

1920

2021type TokenParser a = PTok.TokenParser a

2122

@@ -143,6 +144,29 @@ pDecl' syn

143144 = try pFixity

144145 <|> pFunDecl' syn

145146 <|> try (pData syn)

147+ <|> try (pSyntaxDecl syn)

148+

149+pSyntaxDecl :: SyntaxInfo -> IParser PDecl

150+pSyntaxDecl syn

151+ = do s <- pSyntaxRule syn

152+ i <- getState

153+ setState (i { syntax_rules = s : syntax_rules i })

154+ return (PSyntax s)

155+

156+pSyntaxRule :: SyntaxInfo -> IParser Syntax

157+pSyntaxRule syn

158+ = do reserved "syntax"

159+ syms <- many1 pSynSym

160+ lchar '='

161+ tm <- pExpr syn

162+ lchar ';'

163+ return (Rule syms tm)

164+

165+pSynSym :: IParser SSymbol

166+pSynSym = try (do lchar '['; n <- iName; lchar ']'

167+ return (Expr n))

168+ <|> do n <- iName

169+ return (Keyword n)

146170

147171pFunDecl' :: SyntaxInfo -> IParser PDecl

148172pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn

@@ -200,12 +224,44 @@ pExpr syn = do i <- getState

200224

201225pExpr' :: SyntaxInfo -> IParser PTerm

202226pExpr' syn

203− = try (pApp syn)

227+ = try (do i <- getState

228+ pExtensions syn (syntax_rules i))

229+ <|> try (pApp syn)

204230 <|> pSimpleExpr syn

205231 <|> try (pLambda syn)

206232 <|> try (pPi syn)

207233 <|> try (pDoBlock syn)

208234

235+pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm

236+pExtensions syn rules = choice (map (pExt syn) rules)

237+

238+pExt :: SyntaxInfo -> Syntax -> IParser PTerm

239+pExt syn (Rule ssym ptm)

240+ = do smap <- mapM pSymbol ssym

241+ return (update (mapMaybe id smap) ptm) -- updated with smap

242+ where

243+ pSymbol (Keyword n) = do reserved (show n); return Nothing

244+ pSymbol (Expr n) = do tm <- pSimpleExpr syn

245+ return $ Just (n, tm)

246+ dropn n [] = []

247+ dropn n ((x,t) : xs) | n == x = xs

248+ | otherwise = (x,t):dropn n xs

249+

250+ update ns (PRef n) = case lookup n ns of

251+ Just t -> t

252+ _ -> PRef n

253+ update ns (PLam n ty sc) = PLam n (update ns ty) (update (dropn n ns) sc)

254+ update ns (PPi p n ty sc) = PPi p n (update ns ty) (update (dropn n ns) sc)

255+ update ns (PLet n ty val sc) = PLet n (update ns ty) (update ns val)

256+ (update (dropn n ns) sc)

257+ update ns (PApp t args) = PApp (update ns t) (map (fmap (update ns)) args)

258+ update ns (PPair l r) = PPair (update ns l) (update ns r)

259+ update ns (PHidden t) = PHidden (update ns t)

260+ update ns (PDoBlock ds) = PDoBlock $ upd ns ds

261+ where upd ns (DoExp t : ds) = DoExp (update ns t) : upd ns ds

262+ upd ns (DoBind n t : ds) = DoBind n (update ns t) : upd (dropn n ns) ds

263+ upd ns (DoLet n t : ds) = DoLet n (update ns t) : upd (dropn n ns) ds

264+

209265pfName = try iName

210266 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])

211267