rendered paste body val tc = " app(abs(emptyEnv:->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))). app( abs(extendEnv:->(->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))),->(Char,->(mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))),->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))))). app(app(fix(abs(f:->(->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))),->(mu(y.Variant(Tru:Unit, Fls:Unit, Zero:Unit, Var:Char, Abs:Record(var:Char, tp:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))), t:y), App:Record(fun:y, arg:y), If:Record(cond:y, thn:y, els:y), Succ:y, Pred:y, IsZero:y, Fix: y, None:Unit )),mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))).abs(env:->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))).abs(tm:mu(y.Variant(Tru:Unit, Fls:Unit, Zero:Unit, Var:Char, Abs:Record(var:Char, tp:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))), t:y), App:Record(fun:y, arg:y), If:Record(cond:y, thn:y, els:y), Succ:y, Pred:y, IsZero:y, Fix: y, None:Unit )).case tm of Tru=v => tag(Boolean=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Fls=v => tag(Boolean=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Zero=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Var=v => app(env, v) | Abs=v => ( case app(app(f, app(app(app(extendEnv, env),project(v.var)),project(v.tp)) ), project(v.t)) of Boolean=vv => tag (Arrow=record(fun=project(v.tp), arg=tag(Boolean=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))) as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Nat=vv => tag (Arrow=record(fun=project(v.tp), arg=tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))) as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Arrow=vv => tag (Arrow=record(fun=project(v.tp), arg=tag(Arrow=vv as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))) as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | None=vv => tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) esac ) | App=v => ( case app(app(f,env), project(v.fun)) of Arrow=vv => if =(project(vv.fun), app(app(f,env), project(v.arg))) then project(vv.arg) else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) fi | Boolean=vv => tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Nat=vv => tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | None=vv => tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) esac ) | If=v => if =(app(app(f,env),project(v.cond)), tag(Boolean=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))) then ( if =(app(app(f,env),project(v.thn)), app(f,project(v.els))) then app(app(f,env),project(v.thn)) else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) fi ) else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) fi | Succ=v => if =(app(app(f,env),v), tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))) then tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) fi | Pred=v => if =(app(app(f,env),v), tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))) then tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) fi | Fix=v => ( case v of Abs=v => if =(app(app(f,env), project(v.t)), project(v.tp)) then project(v.tp) else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) fi | Tru=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Fls=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Abs=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | App=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | If=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Succ=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Pred=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) | Fix=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) esac ) esac )))), emptyEnv), tag(App=record(fun=tag(Abs=record(var='a', tp=tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))), t=tag(Var='a' as mu(y.Variant(Tru:Unit, Fls:Unit, Zero:Unit, Var:Char, Abs:Record(var:Char, tp:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))), t:y), App:Record(fun:y, arg:y), If:Record(cond:y, thn:y, els:y), Succ:y, Pred:y, IsZero:y, Fix: y, None:Unit ))) ) as mu(y.Variant(Tru:Unit, Fls:Unit, Zero:Unit, Var:Char, Abs:Record(var:Char, tp:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))), t:y), App:Record(fun:y, arg:y), If:Record(cond:y, thn:y, els:y), Succ:y, Pred:y, IsZero:y, Fix: y, None:Unit ))), arg=tag(Zero=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))) as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) ) ), abs(oldEnv:->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))). abs(s:Char. abs(n:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))). abs(sprime:Char. if =(s,sprime) then n else app(oldEnv,sprime) fi ) ) ) ) ) ), abs(s:Char.tag(none = # as mu(y.Variant(Tru:Unit, Fls:Unit, Zero:Unit, Var:Char, Abs:Record(var:Char, tp:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))), t:y), App:Record(fun:y, arg:y), If:Record(cond:y, thn:y, els:y), Succ:y, Pred:y, IsZero:y, Fix: y, None:Unit )))) ) "
val tcm = ps tc