Problem with dsl specification

[Srdjan Stipic]

Hi.

I am trying to implement dsl specification

for the simple imperative language defined in Idrid excercises

(Lecture 2. problems 9 and 10).

http://www.cs.st-andrews.ac.uk/~eb/Idris/exercises.pdf

The specification of dsl is the following:

  dsl imp

    variable    = Var

    index_first = stop

    index_next  = pop

    let         = Let

  -- Problematic code start here --

  -- instance Num (Expr G TyInt) where

  --   (+) x y = Op (+) x y

  --   (-) x y = Op (-) x y

  --   (*) x y = Op (*) x y

  --   abs x = Val . fromInteger . abs

  --   fromInteger = Val . fromInteger

  -- Problematic code ens here --

When I run the program for idris repl, the program work correctly:

-- output starts here --

*./L2-imp> :r

Type checking ././L2-imp.idr

*./L2-imp> :exec

1

2

3

4

5

6

7

8

9

10

*./L2-imp> 

-- output ends here --

But hen I uncomment the problematic lines I get the following error in the idris repl:

-- output starts here --

➜  exercises git:(master) ✗ idris ./L2-imp.idr 

     ____    __     _                                          

    /  _/___/ /____(_)____                                     

    / // __  / ___/ / ___/     Version 0.9.7

  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      

 /___/\__,_/_/  /_/____/       Type :? for help                

Type checking ././L2-imp.idr

././L2-imp.idr:84:Can't convert Vect Ty n with Vect Ty n1

*./L2-imp> 

-- output ends here --

I was googling for the error message but I wasn't able to find the solution.

Please, can somebody explain me why I get this error message? (and how to fix it)

Thanks

Srdjan

P.S.

The source code of the program:

-- problematic lines are in the comments

module Main

data Ty = TyInt | TyBool | TyUnit | TyFun Ty Ty

interpTy : Ty -> Type

interpTy TyInt       = Int

interpTy TyBool      = Bool

interpTy TyUnit      = ()

interpTy (TyFun s t) = interpTy s -> interpTy t

using (G : Vect Ty n)

  data Env : Vect Ty n -> Type where

      Nil  : Env Nil

      (::) : interpTy a -> Env G -> Env (a :: G)

  data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where

      stop : HasType fO (t :: G) t

      pop  : HasType k G t -> HasType (fS k) (u :: G) t

  lookup : HasType i G t -> Env G -> interpTy t

  lookup stop    (x :: xs) = x

  lookup (pop k) (x :: xs) = lookup k xs

  total

  update : HasType i G t -> Env G -> interpTy t -> Env G

  update stop (x :: xs) a = a :: xs

  update (pop k) (x :: xs) a = x :: update k xs a

  data Expr : Vect Ty n -> Ty -> Type where

       Val : interpTy a -> Expr G a

       Var : HasType i G t -> Expr G t

       Op  : (interpTy a -> interpTy b -> interpTy c) ->

              Expr G a -> Expr G b -> Expr G c

  total

  eval : Env G -> Expr G t -> interpTy t

  eval env (Var i) = lookup i env

  eval env (Val x) = x

  eval env (Op op x y) = op (eval env x) (eval env y)

  infix 5 :=

  data Imp    : Vect Ty n -> Ty -> Type where

       Let    : Expr G t -> Imp (t :: G) u -> Imp G u

       (:=)   : HasType i G t -> Expr G t -> Imp G t

       Print  : Expr G TyInt -> Imp G TyUnit

       For    : Imp G i -> -- initialise

                Imp G TyBool -> -- test

                Imp G x -> -- increment

                Imp G t -> -- body

                Imp G TyUnit

       (>>=)  : Imp G a -> (interpTy a -> Imp G b) -> Imp G b

       Return : Expr G t -> Imp G t

  total

  interp : Env G -> Imp G t -> IO (interpTy t, Env G)

  interp env (For init test increment body) = do

    (_, env') <- interp env init

    (t, _) <- interp env' test

    if t then do (_, env'') <- interp env' body

                 interp env'' (For increment test increment body)

         else return ((), env')

  interp env (Let x t) = let a = eval env x in do

    (v, _) <- interp (a :: env) t

    return (v, env)

  interp env (x := k) = let a = eval env k in return (a, update x env a)

  interp env (Print k) = do putStrLn $ show $ eval env k; return ((), env)

  interp env (Return x) = return (eval env x, env)

  interp env (x >>= y) = do

    (a, env') <- interp env x

    interp env' (y a)

  dsl imp

    variable    = Var

    index_first = stop

    index_next  = pop

    let         = Let

  -- instance Num (Expr G TyInt) where

  --   (+) x y = Op (+) x y

  --   (-) x y = Op (-) x y

  --   (*) x y = Op (*) x y

  --   abs x = Val . fromInteger . abs

  --   fromInteger = Val . fromInteger

  -- count2 : Imp [] TyUnit

  -- count2 = do let x = 4

  -- count2 = imp (do let x = 0

  --                  For (x := 0) (x < 10) (x := x + 1)

  --                  (Print (x + 1)))

  count : Imp [] TyUnit

  count = Let (Val 4) (

          For (stop := (Val 0))

              (Return (Op (<) (Var stop) (Val (10))))

              (stop := (Op (+) (Var stop) (Val 1)))

              (Print (Op (+) (Var stop) (Val 1))))

  main : IO ()

  main = do interp [] count; return ()