dc3f0f9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

added dsl blocks

dc3f0f9Edwin Brady15 years ago

idris.cabal+1−1

compare with master

unifiedsplit

@@ -61,7 +61,7 @@ Executable idris

61 Idris.Delaborate, Idris.Primitives, Idris.Imports,

62 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

63 Idris.Coverage, Idris.IBC, Idris.Unlit,

64− Idris.DataOpts, Idris.Transforms,

64+ Idris.DataOpts, Idris.Transforms, Idris.DSL,

66 Paths_idris

samples/interp.idr+15−7

@@ -30,6 +30,12 @@ using (G : Vect Ty n)

30 Expr G c

31 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

32 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

33+

34+ dsl expr

35+ lambda = Lam

36+ variable = Var

37+ index_first = stop

38+ index_next = pop

34 interp : Env G -> {static} Expr G t -> interpTy t

40 interp : Env G -> {static} Expr G t -> interpTy t

35 interp env (Var i) = lookup i env

41 interp env (Var i) = lookup i env

@@ -39,28 +45,29 @@ using (G : Vect Ty n)

39 interp env (Op op x y) = op (interp env x) (interp env y)

45 interp env (Op op x y) = op (interp env x) (interp env y)

40 interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e)

46 interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e)

41 interp env (Bind v f) = interp env (f (interp env v))

47 interp env (Bind v f) = interp env (f (interp env v))

42−

48+

43 eId : Expr G (TyFun TyInt TyInt)

49 eId : Expr G (TyFun TyInt TyInt)

44− eId = Lam (Var stop)

50+ eId = expr (\x => x)

46 eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))

52 eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))

47− eTEST = Lam (Lam (Var (pop stop)))

53+ eTEST = expr (\x, y => y)

49 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

55 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

50− eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))))

56+ eAdd = expr (\x, y => Op (+) x y)

52-- eDouble : Expr G (TyFun TyInt TyInt)

58-- eDouble : Expr G (TyFun TyInt TyInt)

53-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))

59-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))

55 eDouble : Expr G (TyFun TyInt TyInt)

61 eDouble : Expr G (TyFun TyInt TyInt)

56− eDouble = Lam (App (App eAdd (Var stop)) (Var stop))

62+ eDouble = expr (\x => App (App eAdd x) (Var stop))

58 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

64 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

59 app = \f, a => App f a

65 app = \f, a => App f a

61 eFac : Expr G (TyFun TyInt TyInt)

67 eFac : Expr G (TyFun TyInt TyInt)

62− eFac = Lam (If (Op (==) (Var stop) (Val 0))

68+ eFac = expr (\x => If (Op (==) x (Val 0))

69+ (Val 1)

63− (Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)))

70+ (Op (*) (app eFac (Op (-) x (Val 1))) x))

65 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

72 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

@@ -70,6 +77,7 @@ using (G : Vect Ty n)

70 (\y => Bind (App eDouble (Val x))

77 (\y => Bind (App eDouble (Val x))

71 (\z => App (App eAdd (Val y)) (Val z))))))

78 (\z => App (App eAdd (Val y)) (Val z))))))

80+

73test : Int

81test : Int

74test = interp [] eProg 2 2

82test = interp [] eProg 2 2

src/Idris/AbsSyntax.hs+21−11

@@ -40,6 +40,7 @@ data IState = IState { tt_ctxt :: Context,

40 idris_implicits :: Ctxt [PArg],

41 idris_statics :: Ctxt [Bool],

42 idris_classes :: Ctxt ClassInfo,

43+ idris_dsls :: Ctxt DSL,

43 idris_optimisation :: Ctxt OptInfo,

44 idris_optimisation :: Ctxt OptInfo,

44 idris_datatypes :: Ctxt TypeInfo,

45 idris_datatypes :: Ctxt TypeInfo,

45 idris_patdefs :: Ctxt [(Term, Term)], -- not exported

46 idris_patdefs :: Ctxt [(Term, Term)], -- not exported

@@ -70,6 +71,7 @@ data IBCWrite = IBCFix FixDecl

70 | IBCImp Name

71 | IBCImp Name

71 | IBCStatic Name

72 | IBCStatic Name

72 | IBCClass Name

73 | IBCClass Name

74+ | IBCDSL Name

73 | IBCData Name

75 | IBCData Name

74 | IBCOpt Name

76 | IBCOpt Name

75 | IBCSyntax Syntax

77 | IBCSyntax Syntax

@@ -83,7 +85,7 @@ data IBCWrite = IBCFix FixDecl

83 deriving Show

85 deriving Show

85idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

87idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

86− emptyContext emptyContext emptyContext

88+ emptyContext emptyContext emptyContext emptyContext

87 "" defaultOpts 6 [] [] [] [] [] [] [] []

89 "" defaultOpts 6 [] [] [] [] [] [] [] []

88 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

90 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

@@ -372,6 +374,7 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

372 [t] -- parameters

374 [t] -- parameters

373 t -- full instance type

375 t -- full instance type

374 [PDecl' t]

376 [PDecl' t]

377+ | PDSL Name (DSL' t)

375 | PSyntax FC Syntax

378 | PSyntax FC Syntax

376 | PDirective (Idris ())

379 | PDirective (Idris ())

377 deriving Functor

380 deriving Functor

@@ -558,16 +561,22 @@ deriving instance Binary TypeInfo

558

561

559-- Syntactic sugar info

562-- Syntactic sugar info

560

563

561−data DSL = DSL { dsl_bind :: PTerm,

564+data DSL' t = DSL { dsl_bind :: t,

562− dsl_return :: PTerm,

565+ dsl_return :: t,

563− dsl_apply :: PTerm,

566+ dsl_apply :: t,

564− dsl_pure :: PTerm,

567+ dsl_pure :: t,

568+ dsl_var :: Maybe t,

565− index_first :: Maybe PTerm,

569+ index_first :: Maybe t,

566− index_next :: Maybe PTerm,

570+ index_next :: Maybe t,

567− dsl_lambda :: Maybe PTerm,

571+ dsl_lambda :: Maybe t,

568− dsl_let :: Maybe PTerm

572+ dsl_let :: Maybe t

569− }

573+ }

570− deriving Show

574+ deriving (Show, Functor)

575+{-!

576+deriving instance Binary DSL'

577+!-}

578+

579+type DSL = DSL' PTerm

571

580

572data SynContext = PatternSyntax | TermSyntax | AnySyntax

581data SynContext = PatternSyntax | TermSyntax | AnySyntax

573 deriving Show

582 deriving Show

@@ -598,6 +607,7 @@ initDSL = DSL (PRef f (UN ">>="))

598 Nothing

607 Nothing

599 Nothing

608 Nothing

600 Nothing

609 Nothing

610+ Nothing

601 where f = FC "(builtin)" 0

611 where f = FC "(builtin)" 0

602

612

603data SyntaxInfo = Syn { using :: [(Name, PTerm)],

613data SyntaxInfo = Syn { using :: [(Name, PTerm)],

src/Idris/DSL.hsnew file+105

@@ -0,0 +1,105 @@

1+{-# LANGUAGE PatternGuards #-}

3+module Idris.DSL where

5+import Idris.AbsSyntax

6+import Paths_idris

8+import Core.CoreParser

9+import Core.TT

10+import Core.Evaluate

11+

12+desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

13+desugar syn i t = let t' = expandDo (dsl_info syn) t in

14+ t' -- addImpl i t'

15+

16+expandDo :: DSL -> PTerm -> PTerm

17+expandDo dsl (PLam n ty tm)

18+ | Just lam <- dsl_lambda dsl

19+ = let sc = PApp (FC "(dsl)" 0) lam [pexp (var dsl n tm 0)] in

20+ expandDo dsl sc

21+expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

22+expandDo dsl (PLet n ty v tm)

23+ | Just letb <- dsl_let dsl

24+ = let sc = PApp (FC "(dsl)" 0) letb [pexp v, pexp (var dsl n tm 0)] in

25+ expandDo dsl sc

26+expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

27+expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

28+expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

29+ (map (fmap (expandDo dsl)) args)

30+expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

31+ (map (pmap (expandDo dsl)) opts)

32+expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)

33+expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

34+ (expandDo dsl r)

35+expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)

36+expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

37+expandDo dsl (PReturn fc) = dsl_return dsl

38+expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

39+ where

40+ block b [DoExp fc tm] = tm

41+ block b [a] = PElabError "Last statement in do block must be an expression"

42+ block b (DoBind fc n tm : rest)

43+ = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]

44+ block b (DoBindP fc p tm : rest)

45+ = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder

46+ (PCase fc (PRef fc (MN 0 "bpat"))

47+ [(p, block b rest)]))]

48+ block b (DoLet fc n ty tm : rest)

49+ = PLet n ty tm (block b rest)

50+ block b (DoLetP fc p tm : rest)

51+ = PCase fc tm [(p, block b rest)]

52+ block b (DoExp fc tm : rest)

53+ = PApp fc b

54+ [pexp tm,

55+ pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

56+ block b _ = PElabError "Invalid statement in do block"

57+

58+expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

59+expandDo dsl t = t

60+

61+var :: DSL -> Name -> PTerm -> Int -> PTerm

62+var dsl n t i = v' i t where

63+ v' i (PRef fc x) | x == n =

64+ case dsl_var dsl of

65+ Nothing -> PElabError "No 'variable' defined in dsl"

66+ Just v -> PApp fc v [pexp (mkVar fc i)]

67+ v' i (PLam n ty sc)

68+ | Nothing <- dsl_lambda dsl

69+ = PLam n ty (v' i sc)

70+ | otherwise = PLam n (v' i ty) (v' (i + 1) sc)

71+ v' i (PLet n ty val sc)

72+ | Nothing <- dsl_let dsl

73+ = PLet n (v' i ty) (v' i val) (v' i sc)

74+ | otherwise = PLet n (v' i ty) (v' i val) (v' (i + 1) sc)

75+ v' i (PPi p n ty sc) = PPi p n (v' i ty) (v' i sc)

76+ v' i (PTyped l r) = PTyped (v' i l) (v' i r)

77+ v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

78+ v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

79+ v' i (PEq f l r) = PEq f (v' i l) (v' i r)

80+ v' i (PPair f l r) = PPair f (v' i l) (v' i r)

81+ v' i (PDPair f l t r) = PDPair f (v' i l) (v' i t) (v' i r)

82+ v' i (PAlternative as) = PAlternative $ map (v' i) as

83+ v' i (PHidden t) = PHidden (v' i t)

84+ v' i (PIdiom f t) = PIdiom f (v' i t)

85+ v' i t = t

86+

87+ mkVar fc 0 = case index_first dsl of

88+ Nothing -> PElabError "No index_first defined"

89+ Just f -> f

90+ mkVar fc n = case index_next dsl of

91+ Nothing -> PElabError "No index_next defined"

92+ Just f -> PApp fc f [pexp (mkVar fc (n-1))]

93+

94+unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm

95+unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in

96+ mkap (getFn e)

97+ where

98+ getFn (PApp fc f args) = (PApp fc pure [pexp f], args)

99+ getFn f = (f, [])

100+

101+ mkap (f, []) = f

102+ mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as)

103+

104+unIdiom ap pure fc e = PApp fc pure [pexp e]

105+

src/Idris/ElabDecls.hs+6

@@ -3,6 +3,7 @@

3module Idris.ElabDecls where

5import Idris.AbsSyntax

6+import Idris.DSL

6import Idris.Error

7import Idris.Error

7import Idris.Delaborate

8import Idris.Delaborate

8import Idris.Imports

9import Idris.Imports

@@ -623,6 +624,11 @@ elabDecl' info (PInstance s f cs n ps t ds)

623elabDecl' info (PRecord s f tyn ty cn cty)

624elabDecl' info (PRecord s f tyn ty cn cty)

624 = do iLOG $ "Elaborating record " ++ show tyn

625 = do iLOG $ "Elaborating record " ++ show tyn

625 elabRecord info s f tyn ty cn cty

626 elabRecord info s f tyn ty cn cty

627+elabDecl' info (PDSL n dsl)

628+ = do i <- get

629+ put (i { idris_dsls = addDef n dsl (idris_dsls i) })

630+ addIBC (IBCDSL n)

631+

626elabDecl' info (PDirective i) = i

632elabDecl' info (PDirective i) = i

627

633

628elabCaseBlock info d@(PClauses f o n ps)

634elabCaseBlock info d@(PClauses f o n ps)

src/Idris/ElabTerm.hs+7

@@ -1,6 +1,9 @@

1+{-# LANGUAGE PatternGuards #-}

1module Idris.ElabTerm where

3module Idris.ElabTerm where

3import Idris.AbsSyntax

5import Idris.AbsSyntax

6+import Idris.DSL

5import Core.Elaborate hiding (Tactic(..))

8import Core.Elaborate hiding (Tactic(..))

6import Core.TT

9import Core.TT

@@ -191,6 +194,10 @@ elab ist info pattern tcgen fn tm

191-- elabE True ty

194-- elabE True ty

192-- focus valn

195-- focus valn

193-- elabE True val

196-- elabE True val

197+-- elab' ina (PApp fc (PRef _ dsl) [arg])

198+-- | [d] <- lookupCtxt Nothing dsl (idris_dsls ist)

199+-- = let dsl' = expandDo d (getTm arg) in

200+-- trace (show dsl') $ elab' ina dsl'

194 elab' ina (PApp fc (PRef _ f) args')

201 elab' ina (PApp fc (PRef _ f) args')

195 = do let args = {- case lookupCtxt f (inblock info) of

202 = do let args = {- case lookupCtxt f (inblock info) of

196 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

203 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

src/Idris/IBC.hs+41−4

@@ -22,7 +22,7 @@ import System.Directory

22import Paths_idris

24ibcVersion :: Word8

25−ibcVersion = 9

25+ibcVersion = 10

27data IBCFile = IBCFile { ver :: Word8,

28 sourcefile :: FilePath,

@@ -31,6 +31,7 @@ data IBCFile = IBCFile { ver :: Word8,

31 ibc_fixes :: [FixDecl],

32 ibc_statics :: [(Name, [Bool])],

33 ibc_classes :: [(Name, ClassInfo)],

34+ ibc_dsls :: [(Name, DSL)],

34 ibc_datatypes :: [(Name, TypeInfo)],

35 ibc_datatypes :: [(Name, TypeInfo)],

35 ibc_optimise :: [(Name, OptInfo)],

36 ibc_optimise :: [(Name, OptInfo)],

36 ibc_syntax :: [Syntax],

37 ibc_syntax :: [Syntax],

@@ -45,7 +46,7 @@ deriving instance Binary IBCFile

45!-}

46!-}

47initIBC :: IBCFile

48initIBC :: IBCFile

48−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] []

49+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

50loadIBC :: FilePath -> Idris ()

51loadIBC :: FilePath -> Idris ()

51loadIBC fp = do iLOG $ "Loading ibc " ++ fp

52loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -84,6 +85,10 @@ ibc i (IBCClass n) f

84 = case lookupCtxt Nothing n (idris_classes i) of

85 = case lookupCtxt Nothing n (idris_classes i) of

85 [v] -> return f { ibc_classes = (n,v): ibc_classes f }

86 [v] -> return f { ibc_classes = (n,v): ibc_classes f }

86 _ -> fail "IBC write failed"

87 _ -> fail "IBC write failed"

88+ibc i (IBCDSL n) f

89+ = case lookupCtxt Nothing n (idris_dsls i) of

90+ [v] -> return f { ibc_dsls = (n,v): ibc_dsls f }

91+ _ -> fail "IBC write failed"

87ibc i (IBCData n) f

92ibc i (IBCData n) f

88 = case lookupCtxt Nothing n (idris_datatypes i) of

93 = case lookupCtxt Nothing n (idris_datatypes i) of

89 [v] -> return f { ibc_datatypes = (n,v): ibc_datatypes f }

94 [v] -> return f { ibc_datatypes = (n,v): ibc_datatypes f }

@@ -116,6 +121,7 @@ process i fn

116 pFixes (ibc_fixes i)

121 pFixes (ibc_fixes i)

117 pStatics (ibc_statics i)

122 pStatics (ibc_statics i)

118 pClasses (ibc_classes i)

123 pClasses (ibc_classes i)

124+ pDSLs (ibc_dsls i)

119 pDatatypes (ibc_datatypes i)

125 pDatatypes (ibc_datatypes i)

120 pOptimise (ibc_optimise i)

126 pOptimise (ibc_optimise i)

121 pSyntax (ibc_syntax i)

127 pSyntax (ibc_syntax i)

@@ -174,6 +180,13 @@ pClasses cs = mapM_ (\ (n, c) ->

174 = addDef n c (idris_classes i) }))

180 = addDef n c (idris_classes i) }))

175 cs

181 cs

176

182

183+pDSLs :: [(Name, DSL)] -> Idris ()

184+pDSLs cs = mapM_ (\ (n, c) ->

185+ do i <- getIState

186+ putIState (i { idris_dsls

187+ = addDef n c (idris_dsls i) }))

188+ cs

189+

177pDatatypes :: [(Name, TypeInfo)] -> Idris ()

190pDatatypes :: [(Name, TypeInfo)] -> Idris ()

178pDatatypes cs = mapM_ (\ (n, c) ->

191pDatatypes cs = mapM_ (\ (n, c) ->

179 do i <- getIState

192 do i <- getIState

@@ -568,7 +581,7 @@ instance Binary Accessibility where

568 _ -> error "Corrupted binary data for Accessibility"

581 _ -> error "Corrupted binary data for Accessibility"

569

582

570instance Binary IBCFile where

583instance Binary IBCFile where

571− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)

584+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17)

572 = do put x1

585 = do put x1

573 put x2

586 put x2

574 put x3

587 put x3

@@ -585,6 +598,7 @@ instance Binary IBCFile where

585 put x14

598 put x14

586 put x15

599 put x15

587 put x16

600 put x16

601+ put x17

588 get

602 get

589 = do x1 <- get

603 = do x1 <- get

590 if x1 == ibcVersion then

604 if x1 == ibcVersion then

@@ -603,7 +617,8 @@ instance Binary IBCFile where

603 x14 <- get

617 x14 <- get

604 x15 <- get

618 x15 <- get

605 x16 <- get

619 x16 <- get

620+ x17 <- get

606− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)

621+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17)

607 else return (initIBC { ver = x1 })

622 else return (initIBC { ver = x1 })

608

623

609instance Binary Fixity where

624instance Binary Fixity where

@@ -1024,6 +1039,28 @@ instance Binary Syntax where

1024 x3 <- get

1039 x3 <- get

1025 return (Rule x1 x2 x3)

1040 return (Rule x1 x2 x3)

1026

1041

1042+instance (Binary t) => Binary (DSL' t) where

1043+ put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

1044+ = do put x1

1045+ put x2

1046+ put x3

1047+ put x4

1048+ put x5

1049+ put x6

1050+ put x7

1051+ put x8

1052+ put x9

1053+ get

1054+ = do x1 <- get

1055+ x2 <- get

1056+ x3 <- get

1057+ x4 <- get

1058+ x5 <- get

1059+ x6 <- get

1060+ x7 <- get

1061+ x8 <- get

1062+ x9 <- get

1063+ return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

1027

1064

1028instance Binary SSymbol where

1065instance Binary SSymbol where

1029 put x

1066 put x

src/Idris/Parser.hs+50−53

@@ -1,6 +1,9 @@

1+{-# LANGUAGE PatternGuards #-}

1module Idris.Parser where

3module Idris.Parser where

3import Idris.AbsSyntax

5import Idris.AbsSyntax

6+import Idris.DSL

4import Idris.Imports

7import Idris.Imports

5import Idris.Error

8import Idris.Error

6import Idris.ElabDecls

9import Idris.ElabDecls

@@ -310,6 +313,7 @@ pDecl syn = do notEndBlock

310 <|> pNamespace syn

313 <|> pNamespace syn

311 <|> pClass syn

314 <|> pClass syn

312 <|> pInstance syn

315 <|> pInstance syn

316+ <|> do d <- pDSL syn; return [d]

313 <|> pDirective

317 <|> pDirective

314 <|> try (do reserved "import"

318 <|> try (do reserved "import"

315 fp <- identifier

319 fp <- identifier

@@ -728,7 +732,13 @@ pApp syn = do f <- pSimpleExpr syn

728 fc <- pfc

732 fc <- pfc

729 args <- many1 (do notEndApp

733 args <- many1 (do notEndApp

730 pArg syn)

734 pArg syn)

735+ i <- getState

731− return (PApp fc f args)

736+ return (dslify i $ PApp fc f args)

737+ where

738+ dslify i (PApp fc (PRef _ f) [a])

739+ | [d] <- lookupCtxt Nothing f (idris_dsls i)

740+ = desugar (syn { dsl_info = d }) i (getTm a)

741+ dslify i t = t

732

742

733pArg :: SyntaxInfo -> IParser PArg

743pArg :: SyntaxInfo -> IParser PArg

734pArg syn = try (pImplicitArg syn)

744pArg syn = try (pImplicitArg syn)

@@ -979,6 +989,45 @@ pSimpleCon syn

979 pSimpleExpr syn)

989 pSimpleExpr syn)

980 return (cn, args, fc)

990 return (cn, args, fc)

981

991

992+--------- DSL syntax overloading ---------

993+

994+pDSL :: SyntaxInfo -> IParser PDecl

995+pDSL syn = do reserved "dsl"; n <- pfName

996+ open_block; push_indent

997+ bs <- many1 (do notEndBlock

998+ b <- pOverload syn

999+ pKeepTerminator

1000+ return b)

1001+ pop_indent; close_block

1002+ let dsl = mkDSL bs (dsl_info syn)

1003+ checkDSL dsl

1004+ i <- getState

1005+ setState (i { idris_dsls = addDef n dsl (idris_dsls i) })

1006+ return (PDSL n dsl)

1007+ where mkDSL bs dsl = let var = lookup "variable" bs

1008+ first = lookup "index_first" bs

1009+ next = lookup "index_next" bs

1010+ leto = lookup "let" bs

1011+ lambda = lookup "lambda" bs in

1012+ initDSL { dsl_var = var,

1013+ index_first = first,

1014+ index_next = next,

1015+ dsl_lambda = lambda,

1016+ dsl_let = leto }

1017+

1018+checkDSL :: DSL -> IParser ()

1019+checkDSL dsl = return ()

1020+

1021+pOverload :: SyntaxInfo -> IParser (String, PTerm)

1022+pOverload syn = do o <- identifier <|> do reserved "let"; return "let"

1023+ if (not (o `elem` overloadable))

1024+ then fail $ show o ++ " is not an overloading"

1025+ else do

1026+ lchar '='

1027+ t <- pExpr syn

1028+ return (o, t)

1029+ where overloadable = ["let","lambda","index_first","index_next","variable"]

1030+

982--------- Pattern match clauses ---------

1031--------- Pattern match clauses ---------

983

1032

984pPattern :: SyntaxInfo -> IParser PDecl

1033pPattern :: SyntaxInfo -> IParser PDecl

@@ -1193,55 +1242,3 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

1193 imp = do lchar '?'; return False

1242 imp = do lchar '?'; return False

1194 <|> do lchar '_'; return True

1243 <|> do lchar '_'; return True

1195

1244

1196−desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

1197−desugar syn i t = let t' = expandDo (dsl_info syn) t in

1198− t' -- addImpl i t'

1199−

1200−expandDo :: DSL -> PTerm -> PTerm

1201−expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

1202−expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

1203−expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

1204−expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

1205− (map (fmap (expandDo dsl)) args)

1206−expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

1207− (map (pmap (expandDo dsl)) opts)

1208−expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)

1209−expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

1210− (expandDo dsl r)

1211−expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)

1212−expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

1213−expandDo dsl (PReturn fc) = dsl_return dsl

1214−expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

1215− where

1216− block b [DoExp fc tm] = tm

1217− block b [a] = PElabError "Last statement in do block must be an expression"

1218− block b (DoBind fc n tm : rest)

1219− = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]

1220− block b (DoBindP fc p tm : rest)

1221− = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder

1222− (PCase fc (PRef fc (MN 0 "bpat"))

1223− [(p, block b rest)]))]

1224− block b (DoLet fc n ty tm : rest)

1225− = PLet n ty tm (block b rest)

1226− block b (DoLetP fc p tm : rest)

1227− = PCase fc tm [(p, block b rest)]

1228− block b (DoExp fc tm : rest)

1229− = PApp fc b

1230− [pexp tm,

1231− pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

1232− block b _ = PElabError "Invalid statement in do block"

1233−expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

1234−expandDo dsl t = t

1235−

1236−unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm

1237−unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in

1238− mkap (getFn e)

1239− where

1240− getFn (PApp fc f args) = (PApp fc pure [pexp f], args)

1241− getFn f = (f, [])

1242−

1243− mkap (f, []) = f

1244− mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as)

1245−

1246−unIdiom ap pure fc e = PApp fc pure [pexp e]

1247−

test/test001/test001.idr+14−7

@@ -30,7 +30,13 @@ using (G : Vect Ty n) {

30 Expr G c

31 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

32 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

33−

33+

34+ dsl expr

35+ lambda = Lam

36+ variable = Var

37+ index_first = stop

38+ index_next = pop

39+

34 interp : Env G -> {static} Expr G t -> interpTy t

40 interp : Env G -> {static} Expr G t -> interpTy t

35 interp env (Var i) = lookup i env

41 interp env (Var i) = lookup i env

36 interp env (Val x) = x

42 interp env (Val x) = x

@@ -41,26 +47,27 @@ using (G : Vect Ty n) {

41 interp env (Bind v f) = interp env (f (interp env v))

47 interp env (Bind v f) = interp env (f (interp env v))

43 eId : Expr G (TyFun TyInt TyInt)

49 eId : Expr G (TyFun TyInt TyInt)

44− eId = Lam (Var stop)

50+ eId = expr (\x => x)

46 eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))

52 eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))

47− eTEST = Lam (Lam (Var (pop stop)))

53+ eTEST = expr (\x, y => y)

49 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

55 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

50− eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))))

56+ eAdd = expr (\x, y => Op (+) x y)

52-- eDouble : Expr G (TyFun TyInt TyInt)

58-- eDouble : Expr G (TyFun TyInt TyInt)

53-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))

59-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))

55 eDouble : Expr G (TyFun TyInt TyInt)

61 eDouble : Expr G (TyFun TyInt TyInt)

56− eDouble = Lam (App (App eAdd (Var stop)) (Var stop))

62+ eDouble = expr (\x => App (App eAdd x) (Var stop))

58 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

64 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

59 app = \f, a => App f a

65 app = \f, a => App f a

61 eFac : Expr G (TyFun TyInt TyInt)

67 eFac : Expr G (TyFun TyInt TyInt)

62− eFac = Lam (If (Op (==) (Var stop) (Val 0))

68+ eFac = expr (\x => If (Op (==) x (Val 0))

69+ (Val 1)

63− (Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)))

70+ (Op (*) (app eFac (Op (-) x (Val 1))) x))

65 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

72 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2