(* some syntactic sugar for lambda terms a la Barendregt *) (* $Id: sugar.ml,v 1.1.1.1 2000/02/23 00:08:55 alamstei Exp $ *) open Lambda type sugarterm = | SVar of variable (* x *) | SApp of sugarterm * sugarterm (* MN *) | SAbs of variable * sugarterm (* \x.M *) | Numeral of int (* 'n' *) | Pair of sugarterm * sugarterm (* [M, N] *) | Ifthenelse of sugarterm * sugarterm * sugarterm (* if M then N else P *) | True | False | Proj1 of sugarterm (* Pi1 M *) | Proj2 of sugarterm (* Pi2 M *) | S of sugarterm (* Successor *) | P of sugarterm (* Predecessor *) | Zero of sugarterm (* Test for 0 *) | Y of sugarterm (* Fixpoint combinator used for defining recursive functions *) (* Y = \f.(\x.f(xx))(\x.f(xx)) *) let rec desugar sterm = match sterm with SVar(x) -> Var(x) | SApp(m, n) -> App((desugar m), (desugar n)) | SAbs(x, m) -> Abs(x, (desugar m)) | Numeral(n) -> if (n = 0) then let f = fresh() in Abs(f, Var(f)) else desugar (Pair(False, Numeral(n - 1))) | Pair(m, n) -> let f = fresh() in Abs(f, App(App(Var(f), desugar m), desugar n)) | Ifthenelse(m, n, p) -> App(App(desugar m, desugar n), desugar p) | True -> let f = fresh() in let g = fresh() in Abs(f, Abs(g, Var(f))) | False -> let f = fresh() in let g = fresh() in Abs(f, Abs(g, Var(g))) | Proj1(m) -> App(desugar m, desugar True) | Proj2(m) -> App(desugar m, desugar False) | S(m) -> let f = fresh() in App(Abs(f, desugar (Pair(False, SVar(f)))), desugar m) | P(m) -> let f = fresh() in App(Abs(f, App(Var(f), desugar False)), desugar m) | Zero(m) -> let f = fresh() in App(Abs(f, App(Var(f), desugar True)), desugar m) | Y(m) -> let f = fresh() in let f' = Var(f) in let g = fresh() in let g' = Var(g) in App(Abs(f, App(Abs(g, App(f', App(g', g'))), Abs(g, App(f', App(g', g'))))), desugar m) let rec convert term = match term with Var(x) -> SVar(x) | App(m, n) -> SApp(convert m, convert n) | Abs(x, m) -> SAbs(x, convert m)