git.iko.soy/Idris-dev
on master help sign in
Allow DSLs to be applied with $

Given a DSL stlc with the usual definition, in the past it was necessary to write stlc (\x => x) because stlc $ \x => x didn't work. This makes that happen. This is especially nice for DSLs that include do-blocks.

commit2e93a50f05062ab81b85e3775f64136e9fcaa07d authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 5 Mar 2015, 13:43 (12 years ago) parent32171ed
3 files changed+15−10
compare with master
unifiedsplit
CHANGELOG+2−1 src/Idris/DSL.hs+12−2 src/Idris/ParseExpr.hs+1−7
CHANGELOG+2−1
@@ -19,7 +19,8 @@ New in 0.9.17:
1919 Specifically, the rewritten lambda, pi, and let binders will now get
2020 an extra argument of type TTName. This allows more understandable
2121 dynamic errors in DSL code and more readable code generation results.
22−
22+* DSL notation can now be applied with $
23+
2324New in 0.9.16:
2425--------------
2526* Inductive-inductive definitions are now supported (i.e. simultaneously
src/Idris/DSL.hs+12−2
@@ -2,6 +2,8 @@
22
33module Idris.DSL where
44
5+import Data.Generics.Uniplate.Data (transform)
6+
57import Idris.AbsSyntax
68
79import Idris.Core.TT
@@ -13,9 +15,17 @@ import Debug.Trace
1315debindApp :: SyntaxInfo -> PTerm -> PTerm
1416debindApp syn t = debind (dsl_bind (dsl_info syn)) t
1517
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+
1626desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
17−desugar syn i t = let t' = expandDo (dsl_info syn) t in
18− t' -- addImpl i t'
27+desugar syn i t = let t' = expandDo (dsl_info syn) t
28+ in dslify syn i t'
1929
2030mkTTName :: FC -> Name -> PTerm
2131mkTTName fc n =
src/Idris/ParseExpr.hs+1−7
@@ -554,14 +554,8 @@ app syn = do f <- simpleExpr syn
554554 args <- many (do notEndApp; arg syn)
555555 case args of
556556 [] -> return f
557− _ -> return (dslify i (PApp fc f args)))
557+ _ -> return (PApp fc f args))
558558 <?> "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
565559
566560{-| Parses a function argument
567561@