2402885 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Generic syntax declarations (see prelude.idr for example)

2402885Edwin Brady15 years ago

lib/prelude.idr+6

compare with master

unifiedsplit

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

6data 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+

8infixl 5 ==, /=, ==.;

14infixl 5 ==, /=, ==.;

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

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

10infixl 7 <<, >>;

16infixl 7 <<, >>;

src/Core/CoreParser.hs+1−1

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

17 opStart = iOpStart,

18 opLetter = iOpLetter,

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

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

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

21 "do", "dsl", "import",

22 "infix", "infixl", "infixr", "prefix",

23 "where", "forall", "syntax",

src/Idris/AbsSyntax.hs+13−4

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

30 idris_options :: IOption,

31 idris_name :: Int,

32 idris_metavars :: [Name],

33+ syntax_rules :: [Syntax],

33 imported :: [FilePath],

34 imported :: [FilePath],

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

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

35 }

36 }

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

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

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

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

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

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

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

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

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

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

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

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

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

137− | PImport String

138+ | PSyntax Syntax

138 deriving Functor

139 deriving Functor

139

140

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

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

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

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

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

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

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

162declared (PParams _ ds) = concatMap declared ds

163declared (PParams _ ds) = concatMap declared ds

163−declared (PImport _) = []

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

164

165

165-- High level language terms

166-- High level language terms

166--

167--

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

198 dsl_return :: Name }

199 dsl_return :: Name }

199 deriving Show

200 deriving Show

200

201

202+data Syntax = Rule [SSymbol] PTerm

203+ deriving Show

204+

205+data SSymbol = Keyword Name

206+ | Expr Name

207+ deriving Show

208+

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

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

202

210

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

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

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

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

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

459dumpDecl (PData d) = showDImp True d

467dumpDecl (PData d) = showDImp True d

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

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

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

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

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

462

471

src/Idris/ElabDecls.hs+3−1

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

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

153

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

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

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

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

156 elabType info n ty

157 elabType info n ty

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

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

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

247 elab' (PApp f [arg])

248 elab' (PApp f [arg])

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

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

249 solve

250 solve

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

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

252+ movelast h

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

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

252 elab' (PElabError e) = fail e

254 elab' (PElabError e) = fail e

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

255 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

16import Data.List

17import Control.Monad.State

18import Debug.Trace

19+import Data.Maybe

20type TokenParser a = PTok.TokenParser a

21type TokenParser a = PTok.TokenParser a

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

143 = try pFixity

144 = try pFixity

144 <|> pFunDecl' syn

145 <|> pFunDecl' syn

145 <|> try (pData syn)

146 <|> 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)

146

170

147pFunDecl' :: SyntaxInfo -> IParser PDecl

171pFunDecl' :: SyntaxInfo -> IParser PDecl

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

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

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

200

224

201pExpr' :: SyntaxInfo -> IParser PTerm

225pExpr' :: SyntaxInfo -> IParser PTerm

202pExpr' syn

226pExpr' syn

227+ = try (do i <- getState

228+ pExtensions syn (syntax_rules i))

203− = try (pApp syn)

229+ <|> try (pApp syn)

204 <|> pSimpleExpr syn

230 <|> pSimpleExpr syn

205 <|> try (pLambda syn)

231 <|> try (pLambda syn)

206 <|> try (pPi syn)

232 <|> try (pPi syn)

207 <|> try (pDoBlock syn)

233 <|> try (pDoBlock syn)

208

234

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+

209pfName = try iName

265pfName = try iName

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

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

211

267