git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1979 from david-christiansen/dsl-dollars
b56f5c1David Christiansen
CHANGELOG+2−1
compare with master
unifiedsplit
@@ -19,7 +19,8 @@ New in 0.9.17:
19 Specifically, the rewritten lambda, pi, and let binders will now get
19 Specifically, the rewritten lambda, pi, and let binders will now get
20 an extra argument of type TTName. This allows more understandable
20 an extra argument of type TTName. This allows more understandable
21 dynamic errors in DSL code and more readable code generation results.
21 dynamic errors in DSL code and more readable code generation results.
22−
22+* DSL notation can now be applied with $
23+
23New in 0.9.16:
24New in 0.9.16:
24--------------
25--------------
25* Inductive-inductive definitions are now supported (i.e. simultaneously
26* Inductive-inductive definitions are now supported (i.e. simultaneously
src/Idris/DSL.hs+12−2
@@ -2,6 +2,8 @@
2
2
3module Idris.DSL where
3module Idris.DSL where
4
4
5+import Data.Generics.Uniplate.Data (transform)
6+
5import Idris.AbsSyntax
7import Idris.AbsSyntax
6
8
7import Idris.Core.TT
9import Idris.Core.TT
@@ -13,9 +15,17 @@ import Debug.Trace
13debindApp :: SyntaxInfo -> PTerm -> PTerm
15debindApp :: SyntaxInfo -> PTerm -> PTerm
14debindApp syn t = debind (dsl_bind (dsl_info syn)) t
16debindApp syn t = debind (dsl_bind (dsl_info syn)) t
15
17
18+dslify :: SyntaxInfo -> IState -> PTerm -> PTerm
19+dslify syn i = transform dslifyApp
20+ where
21+ dslifyApp (PApp fc (PRef _ f) [a])
22+ | [d] <- lookupCtxt f (idris_dsls i)
23+ = desugar (syn { dsl_info = d }) i (getTm a)
24+ dslifyApp t = t
25+
16desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
26desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
17−desugar syn i t = let t' = expandDo (dsl_info syn) t in
27+desugar syn i t = let t' = expandDo (dsl_info syn) t
18− t' -- addImpl i t'
28+ in dslify syn i t'
19
29
20mkTTName :: FC -> Name -> PTerm
30mkTTName :: FC -> Name -> PTerm
21mkTTName fc n =
31mkTTName fc n =
src/Idris/ParseExpr.hs+1−7
@@ -554,14 +554,8 @@ app syn = do f <- simpleExpr syn
554 args <- many (do notEndApp; arg syn)
554 args <- many (do notEndApp; arg syn)
555 case args of
555 case args of
556 [] -> return f
556 [] -> return f
557− _ -> return (dslify i (PApp fc f args)))
557+ _ -> return (PApp fc f args))
558 <?> "function application"
558 <?> "function application"
559− where
560− dslify :: IState -> PTerm -> PTerm
561− dslify i (PApp fc (PRef _ f) [a])
562− | [d] <- lookupCtxt f (idris_dsls i)
563− = desugar (syn { dsl_info = d }) i (getTm a)
564− dslify i t = t
565
559
566{-| Parses a function argument
560{-| Parses a function argument
567@
561@