ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 03:34:13 +03:00
Code Issues Projects Releases Wiki Activity

Named lambda,let,pi in dsl block

Browse Source
This commit is contained in:
Chetan Taralekar 2015-03-01 22:34:17 -06:00
parent 5475fe3dae
commit 3b5790caf9
6 changed files with 51 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
src/Idris/DSL.hs
View File

@ -17,21 +17,43 @@ desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
desugar syn i t = let t' = expandDo (dsl_info syn) t in
t' -- addImpl i t'
mkTTName :: FC -> Name -> PTerm
mkTTName fc n =
let mkList fc [] = PRef fc (sNS (sUN "Nil") ["List", "Prelude"])
mkList fc (x:xs) = PApp fc (PRef fc (sNS (sUN "::") ["List", "Prelude"]))
[ pexp (stringC x)
, pexp (mkList fc xs)]
stringC = PConstant . Str . str
intC = PConstant . I
reflm n = sNS (sUN n) ["Reflection", "Language"]
in case n of
UN nm -> PApp fc (PRef fc (reflm "UN")) [ pexp (stringC nm)]
NS nm ns -> PApp fc (PRef fc (reflm "NS")) [ pexp (mkTTName fc nm)
, pexp (mkList fc ns)]
MN i nm -> PApp fc (PRef fc (reflm "MN")) [ pexp (intC i)
, pexp (stringC nm)]
otherwise -> PRef fc $ reflm "NErased"
expandDo :: DSL -> PTerm -> PTerm
expandDo dsl (PLam fc n ty tm)
| Just lam <- dsl_lambda dsl
= let sc = PApp fc lam [pexp (var dsl n tm 0)] in
expandDo dsl sc
= let sc = PApp fc lam [ pexp (mkTTName fc n)
, pexp (var dsl n tm 0)]
in expandDo dsl sc
expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)
expandDo dsl (PLet fc n ty v tm)
| Just letb <- dsl_let dsl
= let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in
expandDo dsl sc
= let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)
, pexp v
, pexp (var dsl n tm 0)]
in expandDo dsl sc
expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
expandDo dsl (PPi p n ty tm)
| Just pi <- dsl_pi dsl
= let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in
expandDo dsl sc
= let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)
, pexp ty
, pexp (var dsl n tm 0)]
in expandDo dsl sc
expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
(map (fmap (expandDo dsl)) args)

5
test/dsl001/test001.idr
View File

@ -35,8 +35,11 @@ using (G : Vect n Ty)
If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)
lam_ _ = Lam
dsl expr
lambda = Lam
lambda = lam_
variable = Var
index_first = stop
index_next = pop

7
test/dsl002/Resimp.idr
View File

@ -156,6 +156,11 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)
= interp env v (\env', v' => do n <- v'
interp env' (f n) k)
let_ : _ -> Creator (interpTy a) ->
Res (a :: gam) (Val () :: gam') (R t) ->
Res gam gam' (R t)
let_ _ = Let
-- run : {static} Res [] [] (R t) -> IO t
-- run prog = interp [] prog (\env, res => res)
@ -163,7 +168,7 @@ syntax run [prog] = interp [] prog (\env, res => res)
dsl res
variable = id
let = Let
let = let_
index_first = stop
index_next = pop

10
test/dsl003/DSLPi.idr
View File

@ -5,8 +5,11 @@ import Data.Vect
data Ty = BOOL | INT | UNIT | ARR Ty Ty
arr_ : _ -> Ty -> Ty -> Ty
arr_ _ = ARR
dsl simple_type
pi = ARR
pi = arr_
test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)
test1 = Refl
@ -25,8 +28,11 @@ using (vars : Vect n Ty)
implicit exprSpec : Expr vars BOOL -> Spec vars
exprSpec = ItHolds
forall_ : _ -> (t : Ty) -> Spec (t :: vars) -> Spec vars
forall_ _ = ForAll
dsl specs
pi = ForAll
pi = forall_
variable = Var
index_first = FZ
index_next = FS

4
test/sourceLocation001/SourceLoc.idr
View File

@ -54,6 +54,8 @@ using (ctxt : Vect n Ty)
run (App f x) env = !(run f env) !(run x env)
run (Die {loc}) _ = Left loc
lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')
lam_ _ = Lam
exec : Tm [] t -> IO ()
exec tm = case run tm [] of
@ -64,7 +66,7 @@ dsl lang
variable = Var
index_first = FZ
index_next = FS
lambda = Lam
lambda = lam_
testTerm1 : Tm [] (Arr U U)
testTerm1 = lang (\x=>Die)

4
test/sourceLocation001/expected
View File

@ -3,9 +3,9 @@ FileLoc "SourceLoc.idr" (16, 11) (16, 11)
Testing using inline tactics
FileLoc "SourceLoc.idr" (20, 17) (20, 17)
Testing using metavariable with later definition
FileLoc "SourceLoc.idr" (96, 16) (96, 16)
FileLoc "SourceLoc.idr" (98, 16) (98, 16)
-----------------------
Success!
Error at FileLoc "SourceLoc.idr" (70, 23) (70, 23)
Error at FileLoc "SourceLoc.idr" (72, 23) (72, 23)
Success!
Success!