src/HOL/ex/CodeEmbed.thy
author haftmann
Wed Dec 27 19:10:03 2006 +0100 (2006-12-27 ago)
changeset 21912 ff45788e7bf9
parent 21757 093ca3efb132
permissions -rw-r--r--
dropped section header
haftmann@20400
     1
(*  ID:         $Id$
haftmann@20400
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@20400
     3
*)
haftmann@20400
     4
haftmann@20400
     5
header {* Embedding (a subset of) the Pure term algebra in HOL *}
haftmann@20400
     6
haftmann@20400
     7
theory CodeEmbed
haftmann@20400
     8
imports Main MLString
haftmann@20400
     9
begin
haftmann@20400
    10
haftmann@20400
    11
subsection {* Definitions *}
haftmann@20400
    12
haftmann@20400
    13
types vname = ml_string;
haftmann@20400
    14
types "class" = ml_string;
haftmann@20400
    15
types sort = "class list"
haftmann@20400
    16
haftmann@20400
    17
datatype "typ" =
haftmann@20400
    18
    Type ml_string "typ list" (infix "{\<struct>}" 120)
haftmann@20400
    19
  | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
haftmann@20400
    20
haftmann@20400
    21
abbreviation
wenzelm@21404
    22
  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115) where
haftmann@20400
    23
  "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
wenzelm@21404
    24
abbreviation
wenzelm@21404
    25
  Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115) where
haftmann@20400
    26
  "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
haftmann@20400
    27
haftmann@20400
    28
datatype "term" =
haftmann@20400
    29
    Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112)
haftmann@20400
    30
  | Fix   vname "typ" (infix ":\<epsilon>" 112)
haftmann@20400
    31
  | App   "term" "term" (infixl "\<bullet>" 110)
haftmann@20400
    32
haftmann@20400
    33
abbreviation
wenzelm@21404
    34
  Apps :: "term \<Rightarrow> term list \<Rightarrow> term"  (infixl "{\<bullet>}" 110) where
haftmann@20400
    35
  "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
haftmann@20400
    36
haftmann@20400
    37
haftmann@20400
    38
subsection {* ML interface *}
haftmann@20400
    39
haftmann@20400
    40
ML {*
haftmann@20400
    41
structure Embed =
haftmann@20400
    42
struct
haftmann@20400
    43
haftmann@20400
    44
local
haftmann@20400
    45
  val thy = the_context ();
haftmann@20400
    46
  val const_Type = Sign.intern_const thy "Type";
haftmann@20400
    47
  val const_TFix = Sign.intern_const thy "TFix";
haftmann@20400
    48
  val const_Const = Sign.intern_const thy "Const";
haftmann@20400
    49
  val const_App = Sign.intern_const thy "App";
haftmann@20400
    50
  val const_Fix = Sign.intern_const thy "Fix";
haftmann@20400
    51
in
haftmann@20400
    52
  val typ_vname = Type (Sign.intern_type thy "vname", []);
haftmann@20400
    53
  val typ_class = Type (Sign.intern_type thy "class", []);
haftmann@20400
    54
  val typ_sort = Type (Sign.intern_type thy "sort", []);
haftmann@20400
    55
  val typ_typ = Type (Sign.intern_type thy "typ", []);
haftmann@20400
    56
  val typ_term = Type (Sign.intern_type thy "term", []);
wenzelm@21757
    57
  val term_sort = HOLogic.mk_list typ_class o map MLString.term_ml_string;
haftmann@20400
    58
  fun term_typ f (Type (tyco, tys)) =
haftmann@21455
    59
        Const (const_Type, MLString.typ_ml_string --> HOLogic.listT typ_typ --> typ_typ)
wenzelm@21757
    60
          $ MLString.term_ml_string tyco $ HOLogic.mk_list typ_typ (map (term_typ f) tys)
haftmann@20400
    61
    | term_typ f (TFree v) =
haftmann@20400
    62
        f v;
haftmann@20400
    63
  fun term_term f g (Const (c, ty)) =
haftmann@20400
    64
        Const (const_Const, MLString.typ_ml_string --> typ_typ --> typ_term)
haftmann@20400
    65
          $ MLString.term_ml_string c $ g ty
haftmann@20400
    66
    | term_term f g (t1 $ t2) =
haftmann@20400
    67
        Const (const_App, typ_term --> typ_term --> typ_term)
haftmann@20400
    68
          $ term_term f g t1 $ term_term f g t2
haftmann@20400
    69
    | term_term f g (Free v) = f v;
haftmann@20400
    70
end;
haftmann@20400
    71
haftmann@20400
    72
end;
haftmann@20400
    73
*}
haftmann@20400
    74
haftmann@20400
    75
haftmann@20400
    76
subsection {* Code serialization setup *}
haftmann@20400
    77
haftmann@20453
    78
code_type "typ" and "term"
haftmann@21113
    79
  (SML "Term.typ" and "Term.term")
haftmann@20400
    80
haftmann@20453
    81
code_const Type and TFix
haftmann@20453
    82
  and Const and App and Fix
haftmann@20453
    83
  (SML "Term.Type (_, _)" and "Term.TFree (_, _)"
haftmann@20453
    84
    and "Term.Const (_, _)" and "Term.$ (_, _)" and "Term.Free (_, _)")
haftmann@20400
    85
haftmann@21079
    86
code_reserved SML Term
haftmann@21079
    87
haftmann@20400
    88
end