@@ -53,23 +53,20 @@ mkTTName fc n =
5353expandSugar :: DSL -> PTerm -> PTerm
5454expandSugar dsl (PLam fc n nfc ty tm)
5555 | Just lam <- dsl_lambda dsl
56− = let sc = PApp fc lam [ pexp (mkTTName fc n)
57− , pexp (var dsl n tm 0)]
58− in expandSugar dsl sc
56+ = PApp fc lam [ pexp (mkTTName fc n)
57+ , pexp (expandSugar dsl (var dsl n tm 0))]
5958expandSugar dsl (PLam fc n nfc ty tm) = PLam fc n nfc (expandSugar dsl ty) (expandSugar dsl tm)
6059expandSugar dsl (PLet fc n nfc ty v tm)
6160 | Just letb <- dsl_let dsl
62− = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)
63− , pexp v
64− , pexp (var dsl n tm 0)]
65− in expandSugar dsl sc
61+ = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)
62+ , pexp (expandSugar dsl v)
63+ , pexp (expandSugar dsl (var dsl n tm 0))]
6664expandSugar dsl (PLet fc n nfc ty v tm) = PLet fc n nfc (expandSugar dsl ty) (expandSugar dsl v) (expandSugar dsl tm)
6765expandSugar dsl (PPi p n fc ty tm)
6866 | Just pi <- dsl_pi dsl
69− = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)
70− , pexp ty
71− , pexp (var dsl n tm 0)]
72− in expandSugar dsl sc
67+ = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)
68+ , pexp (expandSugar dsl ty)
69+ , pexp (expandSugar dsl (var dsl n tm 0))]
7370expandSugar dsl (PPi p n fc ty tm) = PPi p n fc (expandSugar dsl ty) (expandSugar dsl tm)
7471expandSugar dsl (PApp fc t args) = PApp fc (expandSugar dsl t)
7572 (map (fmap (expandSugar dsl)) args)