include "vect.idr";

-- 'using' means that inside this block, if G is used it is added as
-- an implicit argument with the given type. The type checker isn't
-- clever enough to work this out...

using (G:Vect Ty n) {

  -- Types: integers and functions.

  data Ty = TyInt | TyFun Ty Ty;

  -- Translate a representation of a type into an Idris type.

  interpTy : Ty -> #;
  interpTy TyInt = Int;
  interpTy (TyFun A T) = interpTy A -> interpTy T;

  -- Expressions are indexed by their type, and the types of variables
  -- in scope. Variables are de Bruijn indexed, represented by a Fin n
  -- (i.e. a natural number bounded by n).

  -- Expr can be read as a description of the typing rules for the language.

  data Expr : (Vect Ty n) -> Ty -> # where
     Var : (i:Fin n) -> Expr G (vlookup i G)
   | Val : (x:Int) -> Expr G TyInt
   | Lam : Expr (A::G) T -> Expr G (TyFun A T)
   | App : Expr G (TyFun A T) -> Expr G A -> Expr G T
   | Op : (Int -> Int -> Int) -> Expr G TyInt -> Expr G TyInt -> Expr G TyInt;

  -- When we evaluate Expr, we'll need to know the values in scope, as
  -- well as their types. Env is an environment, indexed over the
  -- types in scope.

  data Env : (Vect Ty n) -> # where
     Empty : (Env VNil)
   | Extend : (res:interpTy T) -> (Env G) -> 
	      (Env (T :: G));

  envLookup : (i:Fin n) -> (Env G) -> (interpTy (vlookup i G));
  envLookup fO (Extend t env) = t;
  envLookup (fS i) (Extend t env) = envLookup i env;

  -- interp translates an Expr into an Idris expression of the
  -- appropriate type. It therefore evaluates the expression by using
  -- Idris' evaluator.
    
  interp : Env G -> Expr G T -> interpTy T;
  interp env (Var i) = envLookup i env;
  interp env (Val x) = x;
  interp env (Lam scope) = \x => interp (Extend x env) scope;
  interp env (App f a) = interp env f (interp env a);
  interp env (Op op l r) = op (interp env l) (interp env r);
   

  -- Some test functions:
  -- 1. Add two inputs.

  test : Expr G (TyFun TyInt (TyFun TyInt TyInt));
  test = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));

  -- 2. Double a value by calling 'test'.

  double : Expr G (TyFun TyInt TyInt);
  double = Lam (App (App test (Var fO)) (Var fO));

}

runDouble : Expr VNil TyInt;
runDouble = App double (Val 21);



-- Specialise test and double:

testS = \x, y => interp Empty test x y %spec;
  %freeze test; 
  %transform interp ?G test ?x ?y => testS ?x ?y;

-- The 'freeze' and 'transform' mean that when specialising functions
-- which use 'test', we'll convert call to interp test to calls to
-- testS. So we're controlling inlining (i.e., stopping it where we
-- don't want it).

doubleS = \x => interp Empty double x %spec;