src/HOL/ex/CodeEmbed.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeEmbed.thy	Mon Aug 21 11:02:39 2006 +0200
@@ -0,0 +1,91 @@
+(*  ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Embedding (a subset of) the Pure term algebra in HOL *}
+
+theory CodeEmbed
+imports Main MLString
+begin
+
+section {* Embedding (a subset of) the Pure term algebra in HOL *}
+
+
+subsection {* Definitions *}
+
+types vname = ml_string;
+types "class" = ml_string;
+types sort = "class list"
+
+datatype "typ" =
+    Type ml_string "typ list" (infix "{\<struct>}" 120)
+  | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
+
+abbreviation
+  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115)
+  "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
+  Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115)
+  "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
+
+datatype "term" =
+    Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112)
+  | Fix   vname "typ" (infix ":\<epsilon>" 112)
+  | App   "term" "term" (infixl "\<bullet>" 110)
+
+abbreviation
+  Apps :: "term \<Rightarrow> term list \<Rightarrow> term"  (infixl "{\<bullet>}" 110)
+  "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
+
+
+subsection {* ML interface *}
+
+ML {*
+structure Embed =
+struct
+
+local
+  val thy = the_context ();
+  val const_Type = Sign.intern_const thy "Type";
+  val const_TFix = Sign.intern_const thy "TFix";
+  val const_Const = Sign.intern_const thy "Const";
+  val const_App = Sign.intern_const thy "App";
+  val const_Fix = Sign.intern_const thy "Fix";
+in
+  val typ_vname = Type (Sign.intern_type thy "vname", []);
+  val typ_class = Type (Sign.intern_type thy "class", []);
+  val typ_sort = Type (Sign.intern_type thy "sort", []);
+  val typ_typ = Type (Sign.intern_type thy "typ", []);
+  val typ_term = Type (Sign.intern_type thy "term", []);
+  val term_sort = HOList.term_list typ_class MLString.term_ml_string;
+  fun term_typ f (Type (tyco, tys)) =
+        Const (const_Type, MLString.typ_ml_string --> HOList.typ_list typ_typ --> typ_typ)
+          $ MLString.term_ml_string tyco $ HOList.term_list typ_typ (term_typ f) tys
+    | term_typ f (TFree v) =
+        f v;
+  fun term_term f g (Const (c, ty)) =
+        Const (const_Const, MLString.typ_ml_string --> typ_typ --> typ_term)
+          $ MLString.term_ml_string c $ g ty
+    | term_term f g (t1 $ t2) =
+        Const (const_App, typ_term --> typ_term --> typ_term)
+          $ term_term f g t1 $ term_term f g t2
+    | term_term f g (Free v) = f v;
+end;
+
+end;
+*}
+
+
+subsection {* Code serialization setup *}
+
+code_typapp
+  "typ"  ml (target_atom "Term.typ")
+  "term" ml (target_atom "Term.term")
+
+code_constapp
+  Type  ml ("Term.Type (_, _)")
+  TFix  ml ("Term.TFree (_, _)")
+  Const ml ("Term.Const (_, _)")
+  App   ml ("Term.$ (_, _)")
+  Fix   ml ("Term.Free (_, _)")
+
+end
\ No newline at end of file