Online SDPE in HOAS

fun PE (HAbs(f)) = HAbs(fn x => PE (f x))

| PE (HApp(e1, e2)) =

let val e1' = PE e1

val e2' = PE e2

in (case e1' of HAbs(f) => f e2'

| _ => HApp(e1', e2'))

end

| PE (HSym(s)) = HSym(s)

- let val e = HAbs(fn x =>

HApp(HAbs(fn y => y),

x))

in conv (PE e)

end;

> val it = Abs ("x1",Var "x1") : exp

Previous slide

Next slide

Back to first slide

View graphic version