packages feed

Agda-2.3.2.2: src/prototyping/eval/Syntax.hs

module Syntax where

import Data.Map (Map)

type Name = String

data Exp = Var Int
	 | Con Name
	 | Def Name
	 | App Exp Exp
	 | Lam Exp

data Pat = ConP Name [Pat]
	 | VarP
	 | WildP

data Clause = Clause [Pat] Exp

type Sig = Map Name [Clause]

data LamView = NoLam Exp
	     | Lams Int Exp

data AppView = Apps Exp [Exp]

lamView :: Exp -> LamView
lamView (Lam v) = lam $ lamView v
    where
	lam (NoLam v)  = Lams 1 v
	lam (Lams n v) = Lams (n + 1) v
lamView v	= NoLam v

appView :: Exp -> AppView
appView (App u v) = appView u `app` v
    where
	app (Apps u vs) v = Apps u (vs ++ [v])
appView v	  = Apps v []

apps :: Exp -> [Exp] -> Exp
apps = foldl App