packages feed

Agda-2.3.2.2: src/core/Exp.hs

module Exp where

import Val

-- we use de Bruijn indexes

data Exp =
      ELam Exp
    | EApp Int [Exp]

    | ESet
    | EFun Exp Exp

    | Efun Int [(Name,Int,Exp)]       -- body of a definition

type Env = [Val]

update :: Env -> Val -> Env
update env u = u:env

getRef 0 (u:us) = u
getRef (n+1) (u:us) = getRef n us
getRef 0 [] = error "getRef"  -- this should never occur after scope analysis

eval :: Env -> Exp -> Val
eval env (ELam e)= Lam (\ u -> eval (update env u) e)
eval env (EApp n us) = apps (getRef n env) (map (eval env) us)
eval env ESet = Set
eval env (EFun a1 a2) =
 Fun (eval env a1) (\ u -> eval (update env u) a2)
eval env e = error "eval"

get s [] = error ("get " ++ s)     -- should never occur
get s ((s1,u):us) = if s == s1 then u else get s us

evalBody :: Env -> Val -> Exp -> Val

evalBody env v (ELam e) = Lam (\ u -> evalBody (update env u) (app v u) e)
evalBody env v (Efun k nes) =
 Lam f
  where
        f (App (Const c _) us) = apps (get c nvs) (drop k us)
        f w = app v w
        nvs = map (\ (c,_,e) -> (c,eval env e)) nes
evalBody env v e = eval env e