idris-lang/Idris-dev — pull request #1303 by david-christiansen (2014-06-09 21:41:22+00:00)
Title: Add pi to overridable syntax in DSL blocks

Example, from the tests:
````
module DSLPi

data Ty = BOOL | INT | UNIT | ARR Ty Ty

dsl simple_type
pi = ARR

test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)
test1 = refl

using (vars : Vect n Ty)
infix 2 ===

data Expr : Vect n Ty -> Ty -> Type where
Var : (i : Fin n) -> Expr vars (index i vars)
(===) : Expr vars t -> Expr vars t -> Expr vars BOOL

data Spec : Vect n Ty -> Type where
ForAll : (t : Ty) -> Spec (t :: vars) -> Spec vars
ItHolds : Expr vars BOOL -> Spec vars

implicit exprSpec : Expr vars BOOL -> Spec vars
exprSpec = ItHolds

dsl specs
pi = ForAll
variable = Var
index_first = fZ
index_next = fS

test2 : Spec []
test2 = specs ((x, y : INT) -> x === y)

test3 : Spec []
test3 = ForAll INT . ForAll INT . ItHolds $ Var (fS fZ) === Var fZ

test4 : test2 = test3
test4 = refl
````