# HG changeset patch
# User haftmann
# Date 1160751166 -7200
# Node ID 19d7f07b0fa397b22ff8f011fa053bbbe11282d4
# Parent  7fe928722821491454cd5cc9a1f2e50658f4e025
added codegen2 example

diff -r 7fe928722821 -r 19d7f07b0fa3 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Fri Oct 13 15:01:34 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Fri Oct 13 16:52:46 2006 +0200
@@ -579,4 +579,75 @@
 val ct2' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}
 
+text {*
+The same story again for code next generation.
+*}
+
+code_gen
+  type_NF (SML -) (SML _)
+
+ML {*
+structure Norm = ROOT.WeakNorm;
+structure Type = ROOT.Type;
+structure Lambda = ROOT.Lambda;
+
+fun nat_of_int 0 = ROOT.IntDef.Zero_nat
+  | nat_of_int n = ROOT.IntDef.Succ_nat (nat_of_int (n-1));
+
+fun int_of_nat ROOT.IntDef.Zero_nat = 0
+  | int_of_nat (ROOT.IntDef.Succ_nat n) = 1 + int_of_nat n;
+
+fun dBtype_of_typ (Type ("fun", [T, U])) =
+      Type.Fun (dBtype_of_typ T, dBtype_of_typ U)
+  | dBtype_of_typ (TFree (s, _)) = (case explode s of
+        ["'", a] => Type.Atom (nat_of_int (ord a - 97))
+      | _ => error "dBtype_of_typ: variable name")
+  | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
+
+fun dB_of_term (Bound i) = Lambda.Var (nat_of_int i)
+  | dB_of_term (t $ u) = Lambda.App (dB_of_term t, dB_of_term u)
+  | dB_of_term (Abs (_, _, t)) = Lambda.Abs (dB_of_term t)
+  | dB_of_term _ = error "dB_of_term: bad term";
+
+fun term_of_dB Ts (Type ("fun", [T, U])) (Lambda.Abs dBt) =
+      Abs ("x", T, term_of_dB (T :: Ts) U dBt)
+  | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
+and term_of_dB' Ts (Lambda.Var n) = Bound (int_of_nat n)
+  | term_of_dB' Ts (Lambda.App (dBt, dBu)) =
+      let val t = term_of_dB' Ts dBt
+      in case fastype_of1 (Ts, t) of
+          Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
+        | _ => error "term_of_dB: function type expected"
+      end
+  | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
+
+fun typing_of_term Ts e (Bound i) =
+      Norm.Var (e, nat_of_int i, dBtype_of_typ (nth Ts i))
+  | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
+        Type ("fun", [T, U]) => Norm.App_1 (e, dB_of_term t,
+          dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
+          typing_of_term Ts e t, typing_of_term Ts e u)
+      | _ => error "typing_of_term: function type expected")
+  | typing_of_term Ts e (Abs (s, T, t)) =
+      let val dBT = dBtype_of_typ T
+      in Norm.Abs_1 (e, dBT, dB_of_term t,
+        dBtype_of_typ (fastype_of1 (T :: Ts, t)),
+        typing_of_term (T :: Ts) (Type.shift e ROOT.IntDef.Zero_nat dBT) t)
+      end
+  | typing_of_term _ _ _ = error "typing_of_term: bad term";
+
+fun dummyf _ = error "dummy";
+*}
+
+ML {*
+val ct1 = rd "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))";
+val (dB1, _) = ROOT.WeakNorm.type_NF (typing_of_term [] dummyf (term_of ct1));
+val ct1' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct1)) dB1);
+
+val ct2 = rd
+  "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))";
+val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
+val ct2' = cterm_of thy (term_of_dB [] (#T (rep_cterm ct2)) dB2);
+*}
+
 end