git.iko.soy/Idris-dev
on master help sign in
Named lambda,let,pi in dsl block
commit3b5790caf955ae56d4aaf12c40ea85c3db8ebd0b authorChetan Taralekar <chetant@gmail.com> dateSun 1 Mar 2015, 22:34 (12 years ago) parent5475fe3
6 files changed+51−13
compare with master
unifiedsplit
src/Idris/DSL.hs+28−6 test/dsl001/test001.idr+4−1 test/dsl002/Resimp.idr+6−1 test/dsl003/DSLPi.idr+8−2 test/sourceLocation001/SourceLoc.idr+3−1 test/sourceLocation001/expected+2−2
src/Idris/DSL.hs+28−6
@@ -17,21 +17,43 @@ desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
1717desugar syn i t = let t' = expandDo (dsl_info syn) t in
1818 t' -- addImpl i t'
1919
20+mkTTName :: FC -> Name -> PTerm
21+mkTTName fc n =
22+ let mkList fc [] = PRef fc (sNS (sUN "Nil") ["List", "Prelude"])
23+ mkList fc (x:xs) = PApp fc (PRef fc (sNS (sUN "::") ["List", "Prelude"]))
24+ [ pexp (stringC x)
25+ , pexp (mkList fc xs)]
26+ stringC = PConstant . Str . str
27+ intC = PConstant . I
28+ reflm n = sNS (sUN n) ["Reflection", "Language"]
29+ in case n of
30+ UN nm -> PApp fc (PRef fc (reflm "UN")) [ pexp (stringC nm)]
31+ NS nm ns -> PApp fc (PRef fc (reflm "NS")) [ pexp (mkTTName fc nm)
32+ , pexp (mkList fc ns)]
33+ MN i nm -> PApp fc (PRef fc (reflm "MN")) [ pexp (intC i)
34+ , pexp (stringC nm)]
35+ otherwise -> PRef fc $ reflm "NErased"
36+
2037expandDo :: DSL -> PTerm -> PTerm
2138expandDo dsl (PLam fc n ty tm)
2239 | Just lam <- dsl_lambda dsl
23− = let sc = PApp fc lam [pexp (var dsl n tm 0)] in
24− expandDo dsl sc
40+ = let sc = PApp fc lam [ pexp (mkTTName fc n)
41+ , pexp (var dsl n tm 0)]
42+ in expandDo dsl sc
2543expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)
2644expandDo dsl (PLet fc n ty v tm)
2745 | Just letb <- dsl_let dsl
28− = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in
29− expandDo dsl sc
46+ = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)
47+ , pexp v
48+ , pexp (var dsl n tm 0)]
49+ in expandDo dsl sc
3050expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
3151expandDo dsl (PPi p n ty tm)
3252 | Just pi <- dsl_pi dsl
33− = let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in
34− expandDo dsl sc
53+ = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)
54+ , pexp ty
55+ , pexp (var dsl n tm 0)]
56+ in expandDo dsl sc
3557expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
3658expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
3759 (map (fmap (expandDo dsl)) args)
test/dsl001/test001.idr+4−1
@@ -35,8 +35,11 @@ using (G : Vect n Ty)
3535 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
3636 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
3737
38+ lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)
39+ lam_ _ = Lam
40+
3841 dsl expr
39− lambda = Lam
42+ lambda = lam_
4043 variable = Var
4144 index_first = stop
4245 index_next = pop
test/dsl002/Resimp.idr+6−1
@@ -156,6 +156,11 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)
156156 = interp env v (\env', v' => do n <- v'
157157 interp env' (f n) k)
158158
159+ let_ : _ -> Creator (interpTy a) ->
160+ Res (a :: gam) (Val () :: gam') (R t) ->
161+ Res gam gam' (R t)
162+ let_ _ = Let
163+
159164-- run : {static} Res [] [] (R t) -> IO t
160165-- run prog = interp [] prog (\env, res => res)
161166
@@ -163,7 +168,7 @@ syntax run [prog] = interp [] prog (\env, res => res)
163168
164169dsl res
165170 variable = id
166− let = Let
171+ let = let_
167172 index_first = stop
168173 index_next = pop
169174
test/dsl003/DSLPi.idr+8−2
@@ -5,8 +5,11 @@ import Data.Vect
55
66data Ty = BOOL | INT | UNIT | ARR Ty Ty
77
8+arr_ : _ -> Ty -> Ty -> Ty
9+arr_ _ = ARR
10+
811dsl simple_type
9− pi = ARR
12+ pi = arr_
1013
1114test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)
1215test1 = Refl
@@ -25,8 +28,11 @@ using (vars : Vect n Ty)
2528 implicit exprSpec : Expr vars BOOL -> Spec vars
2629 exprSpec = ItHolds
2730
31+ forall_ : _ -> (t : Ty) -> Spec (t :: vars) -> Spec vars
32+ forall_ _ = ForAll
33+
2834dsl specs
29− pi = ForAll
35+ pi = forall_
3036 variable = Var
3137 index_first = FZ
3238 index_next = FS
test/sourceLocation001/SourceLoc.idr+3−1
@@ -54,6 +54,8 @@ using (ctxt : Vect n Ty)
5454 run (App f x) env = !(run f env) !(run x env)
5555 run (Die {loc}) _ = Left loc
5656
57+ lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')
58+ lam_ _ = Lam
5759
5860exec : Tm [] t -> IO ()
5961exec tm = case run tm [] of
@@ -64,7 +66,7 @@ dsl lang
6466 variable = Var
6567 index_first = FZ
6668 index_next = FS
67− lambda = Lam
69+ lambda = lam_
6870
6971testTerm1 : Tm [] (Arr U U)
7072testTerm1 = lang (\x=>Die)
test/sourceLocation001/expected+2−2
@@ -3,9 +3,9 @@ FileLoc "SourceLoc.idr" (16, 11) (16, 11)
33Testing using inline tactics
44FileLoc "SourceLoc.idr" (20, 17) (20, 17)
55Testing using metavariable with later definition
6−FileLoc "SourceLoc.idr" (96, 16) (96, 16)
6+FileLoc "SourceLoc.idr" (98, 16) (98, 16)
77-----------------------
88Success!
9−Error at FileLoc "SourceLoc.idr" (70, 23) (70, 23)
9+Error at FileLoc "SourceLoc.idr" (72, 23) (72, 23)
1010Success!
1111Success!