git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1979 from david-christiansen/dsl-dollars

Allow DSLs to be applied with $

commitb56f5c17f2698a0e8cc9747f893bca37300fe76f authorDavid Christiansen <david@davidchristiansen.dk> dateThu 5 Mar 2015, 15:33 (12 years ago) parent32171ed2e93a50
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@