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