git.iko.soy/Idris-dev
on master help sign in
Careful when expanding dsl notation
b8b447fEdwin Brady
src/Idris/DSL.hs+8−11
compare with master
unifiedsplit
@@ -53,23 +53,20 @@ mkTTName fc n =
53expandSugar :: DSL -> PTerm -> PTerm
53expandSugar :: DSL -> PTerm -> PTerm
54expandSugar dsl (PLam fc n nfc ty tm)
54expandSugar dsl (PLam fc n nfc ty tm)
55 | Just lam <- dsl_lambda dsl
55 | Just lam <- dsl_lambda dsl
56− = let sc = PApp fc lam [ pexp (mkTTName fc n)
56+ = PApp fc lam [ pexp (mkTTName fc n)
57− , pexp (var dsl n tm 0)]
57+ , pexp (expandSugar dsl (var dsl n tm 0))]
58− in expandSugar dsl sc
59expandSugar dsl (PLam fc n nfc ty tm) = PLam fc n nfc (expandSugar dsl ty) (expandSugar dsl tm)
58expandSugar dsl (PLam fc n nfc ty tm) = PLam fc n nfc (expandSugar dsl ty) (expandSugar dsl tm)
60expandSugar dsl (PLet fc n nfc ty v tm)
59expandSugar dsl (PLet fc n nfc ty v tm)
61 | Just letb <- dsl_let dsl
60 | Just letb <- dsl_let dsl
62− = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)
61+ = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)
63− , pexp v
62+ , pexp (expandSugar dsl v)
64− , pexp (var dsl n tm 0)]
63+ , pexp (expandSugar dsl (var dsl n tm 0))]
65− in expandSugar dsl sc
66expandSugar dsl (PLet fc n nfc ty v tm) = PLet fc n nfc (expandSugar dsl ty) (expandSugar dsl v) (expandSugar dsl tm)
64expandSugar dsl (PLet fc n nfc ty v tm) = PLet fc n nfc (expandSugar dsl ty) (expandSugar dsl v) (expandSugar dsl tm)
67expandSugar dsl (PPi p n fc ty tm)
65expandSugar dsl (PPi p n fc ty tm)
68 | Just pi <- dsl_pi dsl
66 | Just pi <- dsl_pi dsl
69− = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)
67+ = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)
70− , pexp ty
68+ , pexp (expandSugar dsl ty)
71− , pexp (var dsl n tm 0)]
69+ , pexp (expandSugar dsl (var dsl n tm 0))]
72− in expandSugar dsl sc
73expandSugar dsl (PPi p n fc ty tm) = PPi p n fc (expandSugar dsl ty) (expandSugar dsl tm)
70expandSugar dsl (PPi p n fc ty tm) = PPi p n fc (expandSugar dsl ty) (expandSugar dsl tm)
74expandSugar dsl (PApp fc t args) = PApp fc (expandSugar dsl t)
71expandSugar dsl (PApp fc t args) = PApp fc (expandSugar dsl t)
75 (map (fmap (expandSugar dsl)) args)
72 (map (fmap (expandSugar dsl)) args)