src/HOL/Code_Eval.thy
author haftmann
Fri Jan 02 08:12:46 2009 +0100 (2009-01-02)
changeset 29332 edc1e2a56398
parent 28965 1de908189869
child 29575 41d604e59e93
permissions -rw-r--r--
named code theorem for Fract_norm
     1 (*  Title:      HOL/Code_Eval.thy
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 header {* Term evaluation using the generic code generator *}
     7 
     8 theory Code_Eval
     9 imports Plain Typerep
    10 begin
    11 
    12 subsection {* Term representation *}
    13 
    14 subsubsection {* Terms and class @{text term_of} *}
    15 
    16 datatype "term" = dummy_term
    17 
    18 definition Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" where
    19   "Const _ _ = dummy_term"
    20 
    21 definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
    22   "App _ _ = dummy_term"
    23 
    24 code_datatype Const App
    25 
    26 class term_of = typerep +
    27   fixes term_of :: "'a \<Rightarrow> term"
    28 
    29 lemma term_of_anything: "term_of x \<equiv> t"
    30   by (rule eq_reflection) (cases "term_of x", cases t, simp)
    31 
    32 ML {*
    33 structure Eval =
    34 struct
    35 
    36 fun mk_term f g (Const (c, ty)) =
    37       @{term Const} $ Message_String.mk c $ g ty
    38   | mk_term f g (t1 $ t2) =
    39       @{term App} $ mk_term f g t1 $ mk_term f g t2
    40   | mk_term f g (Free v) = f v
    41   | mk_term f g (Bound i) = Bound i
    42   | mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t);
    43 
    44 fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t;
    45 
    46 end;
    47 *}
    48 
    49 
    50 subsubsection {* @{text term_of} instances *}
    51 
    52 setup {*
    53 let
    54   fun add_term_of_def ty vs tyco thy =
    55     let
    56       val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    57         $ Free ("x", ty);
    58       val rhs = @{term "undefined \<Colon> term"};
    59       val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    60       fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    61         o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    62     in
    63       thy
    64       |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
    65       |> `(fn lthy => Syntax.check_term lthy eq)
    66       |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    67       |> snd
    68       |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    69       |> LocalTheory.exit_global
    70     end;
    71   fun interpretator (tyco, (raw_vs, _)) thy =
    72     let
    73       val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    74       val constrain_sort =
    75         curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
    76       val vs = (map o apsnd) constrain_sort raw_vs;
    77       val ty = Type (tyco, map TFree vs);
    78     in
    79       thy
    80       |> Typerep.perhaps_add_def tyco
    81       |> not has_inst ? add_term_of_def ty vs tyco
    82     end;
    83 in
    84   Code.type_interpretation interpretator
    85 end
    86 *}
    87 
    88 setup {*
    89 let
    90   fun mk_term_of_eq ty vs tyco (c, tys) =
    91     let
    92       val t = list_comb (Const (c, tys ---> ty),
    93         map Free (Name.names Name.context "a" tys));
    94     in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term
    95       (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty)))
    96       (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort)))) t)
    97     end;
    98   fun prove_term_of_eq ty eq thy =
    99     let
   100       val cty = Thm.ctyp_of thy ty;
   101       val (arg, rhs) = pairself (Thm.cterm_of thy) eq;
   102       val thm = @{thm term_of_anything}
   103         |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
   104         |> Thm.varifyT;
   105     in
   106       thy
   107       |> Code.add_eqn thm
   108     end;
   109   fun interpretator (tyco, (raw_vs, raw_cs)) thy =
   110     let
   111       val constrain_sort =
   112         curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
   113       val vs = (map o apsnd) constrain_sort raw_vs;
   114       val cs = (map o apsnd o map o map_atyps)
   115         (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs;
   116       val ty = Type (tyco, map TFree vs);
   117       val eqs = map (mk_term_of_eq ty vs tyco) cs;
   118       val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   119     in
   120       thy
   121       |> Code.del_eqns const
   122       |> fold (prove_term_of_eq ty) eqs
   123     end;
   124 in
   125   Code.type_interpretation interpretator
   126 end
   127 *}
   128 
   129 
   130 subsubsection {* Code generator setup *}
   131 
   132 lemmas [code del] = term.recs term.cases term.size
   133 lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
   134 
   135 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
   136 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
   137 lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
   138 
   139 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
   140     (let (n, m) = nibble_pair_of_char c
   141   in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   142     (Code_Eval.term_of n)) (Code_Eval.term_of m))"
   143   by (subst term_of_anything) rule 
   144 
   145 code_type "term"
   146   (SML "Term.term")
   147 
   148 code_const Const and App
   149   (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)")
   150 
   151 code_const "term_of \<Colon> message_string \<Rightarrow> term"
   152   (SML "Message'_String.mk")
   153 
   154 
   155 subsection {* Evaluation setup *}
   156 
   157 ML {*
   158 signature EVAL =
   159 sig
   160   val mk_term: ((string * typ) -> term) -> (typ -> term) -> term -> term
   161   val eval_ref: (unit -> term) option ref
   162   val eval_term: theory -> term -> term
   163 end;
   164 
   165 structure Eval : EVAL =
   166 struct
   167 
   168 open Eval;
   169 
   170 val eval_ref = ref (NONE : (unit -> term) option);
   171 
   172 fun eval_term thy t =
   173   t 
   174   |> Eval.mk_term_of (fastype_of t)
   175   |> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t [])
   176   |> Code.postprocess_term thy;
   177 
   178 end;
   179 *}
   180 
   181 setup {*
   182   Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
   183 *}
   184 
   185 
   186 subsubsection {* Syntax *}
   187 
   188 print_translation {*
   189 let
   190   val term = Const ("<TERM>", dummyT);
   191   fun tr1' [_, _] = term;
   192   fun tr2' [] = term;
   193 in
   194   [(@{const_syntax Const}, tr1'),
   195     (@{const_syntax App}, tr1'),
   196     (@{const_syntax dummy_term}, tr2')]
   197 end
   198 *}
   199 
   200 hide const dummy_term
   201 hide (open) const Const App
   202 hide (open) const term_of
   203 
   204 end