@@ -1,6 +1,9 @@
1+{-# LANGUAGE PatternGuards #-}
2+
13module Idris.Parser where
24
35import Idris.AbsSyntax
6+import Idris.DSL
47import Idris.Imports
58import Idris.Error
69import Idris.ElabDecls
@@ -310,6 +313,7 @@ pDecl syn = do notEndBlock
310313 <|> pNamespace syn
311314 <|> pClass syn
312315 <|> pInstance syn
316+ <|> do d <- pDSL syn; return [d]
313317 <|> pDirective
314318 <|> try (do reserved "import"
315319 fp <- identifier
@@ -728,7 +732,13 @@ pApp syn = do f <- pSimpleExpr syn
728732 fc <- pfc
729733 args <- many1 (do notEndApp
730734 pArg syn)
731− return (PApp fc f args)
735+ i <- getState
736+ return (dslify i $ PApp fc f args)
737+ where
738+ dslify i (PApp fc (PRef _ f) [a])
739+ | [d] <- lookupCtxt Nothing f (idris_dsls i)
740+ = desugar (syn { dsl_info = d }) i (getTm a)
741+ dslify i t = t
732742
733743pArg :: SyntaxInfo -> IParser PArg
734744pArg syn = try (pImplicitArg syn)
@@ -979,6 +989,45 @@ pSimpleCon syn
979989 pSimpleExpr syn)
980990 return (cn, args, fc)
981991
992+--------- DSL syntax overloading ---------
993+
994+pDSL :: SyntaxInfo -> IParser PDecl
995+pDSL syn = do reserved "dsl"; n <- pfName
996+ open_block; push_indent
997+ bs <- many1 (do notEndBlock
998+ b <- pOverload syn
999+ pKeepTerminator
1000+ return b)
1001+ pop_indent; close_block
1002+ let dsl = mkDSL bs (dsl_info syn)
1003+ checkDSL dsl
1004+ i <- getState
1005+ setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
1006+ return (PDSL n dsl)
1007+ where mkDSL bs dsl = let var = lookup "variable" bs
1008+ first = lookup "index_first" bs
1009+ next = lookup "index_next" bs
1010+ leto = lookup "let" bs
1011+ lambda = lookup "lambda" bs in
1012+ initDSL { dsl_var = var,
1013+ index_first = first,
1014+ index_next = next,
1015+ dsl_lambda = lambda,
1016+ dsl_let = leto }
1017+
1018+checkDSL :: DSL -> IParser ()
1019+checkDSL dsl = return ()
1020+
1021+pOverload :: SyntaxInfo -> IParser (String, PTerm)
1022+pOverload syn = do o <- identifier <|> do reserved "let"; return "let"
1023+ if (not (o `elem` overloadable))
1024+ then fail $ show o ++ " is not an overloading"
1025+ else do
1026+ lchar '='
1027+ t <- pExpr syn
1028+ return (o, t)
1029+ where overloadable = ["let","lambda","index_first","index_next","variable"]
1030+
9821031--------- Pattern match clauses ---------
9831032
9841033pPattern :: SyntaxInfo -> IParser PDecl
@@ -1193,55 +1242,3 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
11931242 imp = do lchar '?'; return False
11941243 <|> do lchar '_'; return True
11951244
1196−desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
1197−desugar syn i t = let t' = expandDo (dsl_info syn) t in
1198− t' -- addImpl i t'
1199−
1200−expandDo :: DSL -> PTerm -> PTerm
1201−expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)
1202−expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
1203−expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
1204−expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
1205− (map (fmap (expandDo dsl)) args)
1206−expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)
1207− (map (pmap (expandDo dsl)) opts)
1208−expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)
1209−expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)
1210− (expandDo dsl r)
1211−expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)
1212−expandDo dsl (PHidden t) = PHidden (expandDo dsl t)
1213−expandDo dsl (PReturn fc) = dsl_return dsl
1214−expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds
1215− where
1216− block b [DoExp fc tm] = tm
1217− block b [a] = PElabError "Last statement in do block must be an expression"
1218− block b (DoBind fc n tm : rest)
1219− = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]
1220− block b (DoBindP fc p tm : rest)
1221− = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder
1222− (PCase fc (PRef fc (MN 0 "bpat"))
1223− [(p, block b rest)]))]
1224− block b (DoLet fc n ty tm : rest)
1225− = PLet n ty tm (block b rest)
1226− block b (DoLetP fc p tm : rest)
1227− = PCase fc tm [(p, block b rest)]
1228− block b (DoExp fc tm : rest)
1229− = PApp fc b
1230− [pexp tm,
1231− pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]
1232− block b _ = PElabError "Invalid statement in do block"
1233−expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
1234−expandDo dsl t = t
1235−
1236−unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
1237−unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in
1238− mkap (getFn e)
1239− where
1240− getFn (PApp fc f args) = (PApp fc pure [pexp f], args)
1241− getFn f = (f, [])
1242−
1243− mkap (f, []) = f
1244− mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as)
1245−
1246−unIdiom ap pure fc e = PApp fc pure [pexp e]
1247−