src/HOL/Library/Eval.thy
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 24381 560e8ecdf633
child 24508 c8b82fec6447
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
     1 (*  Title:      HOL/Library/Eval.thy
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 header {* A simple term evaluation mechanism *}
     7 
     8 theory Eval
     9 imports Main Pure_term
    10 begin
    11 
    12 subsection {* @{text typ_of} class *}
    13 
    14 class typ_of =
    15   fixes typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
    16 
    17 ML {*
    18 structure TypOf =
    19 struct
    20 
    21 val class_typ_of = Sign.intern_class @{theory} "typ_of";
    22 
    23 fun term_typ_of_type ty =
    24   Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
    25     $ Logic.mk_type ty;
    26 
    27 fun mk_typ_of_def ty =
    28   let
    29     val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
    30       $ Free ("x", Term.itselfT ty)
    31     val rhs = Pure_term.mk_typ (fn v => term_typ_of_type (TFree v)) ty
    32   in Logic.mk_equals (lhs, rhs) end;
    33 
    34 end;
    35 *}
    36 
    37 instance itself :: (typ_of) typ_of
    38   "typ_of T \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
    39 
    40 instance "prop" :: typ_of
    41   "typ_of T \<equiv> STR ''prop'' {\<struct>} []" ..
    42 
    43 instance int :: typ_of
    44   "typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
    45 
    46 setup {*
    47 let
    48   fun mk arities _ thy =
    49     (maps (fn (tyco, asorts, _) => [(("", []), TypOf.mk_typ_of_def
    50       (Type (tyco,
    51         map TFree (Name.names Name.context "'a" asorts))))]) arities, thy);
    52   fun hook specs =
    53     DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
    54       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    55       [TypOf.class_typ_of] mk ((K o K) (fold (Code.add_func true)))
    56 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    57 *}
    58 
    59 
    60 subsection {* @{text term_of} class *}
    61 
    62 class term_of = typ_of +
    63   constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
    64   fixes term_of :: "'a \<Rightarrow> term"
    65 
    66 ML {*
    67 structure TermOf =
    68 struct
    69 
    70 local
    71   fun term_term_of ty =
    72     Const (@{const_name term_of}, ty --> @{typ term});
    73 in
    74   val class_term_of = Sign.intern_class @{theory} "term_of";
    75   fun mk_terms_of_defs vs (tyco, cs) =
    76     let
    77       val dty = Type (tyco, map TFree vs);
    78       fun mk_eq c =
    79         let
    80           val lhs : term = term_term_of dty $ c;
    81           val rhs : term = Pure_term.mk_term
    82             (fn (v, ty) => term_term_of ty $ Free (v, ty))
    83             (Pure_term.mk_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c
    84         in
    85           HOLogic.mk_eq (lhs, rhs)
    86         end;
    87     in map mk_eq cs end;
    88   fun mk_term_of t =
    89     term_term_of (Term.fastype_of t) $ t;
    90 end;
    91 
    92 end;
    93 *}
    94 
    95 setup {*
    96 let
    97   fun thy_note ((name, atts), thms) =
    98     PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
    99   fun thy_def ((name, atts), t) =
   100     PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
   101   fun mk arities css _ thy =
   102     let
   103       val (_, asorts, _) :: _ = arities;
   104       val vs = Name.names Name.context "'a" asorts;
   105       val defs = map (TermOf.mk_terms_of_defs vs) css;
   106       val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs;
   107     in
   108       thy
   109       |> PrimrecPackage.gen_primrec thy_note thy_def "" defs'
   110       |> snd
   111     end;
   112   fun hook specs =
   113     if (fst o hd) specs = (fst o dest_Type) @{typ typ} then I
   114     else
   115       DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
   116       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   117       [TermOf.class_term_of] ((K o K o pair) []) mk
   118 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
   119 *}
   120 
   121 abbreviation
   122   intT :: "typ"
   123 where
   124   "intT \<equiv> STR ''IntDef.int'' {\<struct>} []"
   125 
   126 abbreviation
   127   bitT :: "typ"
   128 where
   129   "bitT \<equiv> STR ''Numeral.bit'' {\<struct>} []"
   130 
   131 function
   132   mk_int :: "int \<Rightarrow> term"
   133 where
   134   "mk_int k = (if k = 0 then STR ''Numeral.Pls'' \<Colon>\<subseteq> intT
   135     else if k = -1 then STR ''Numeral.Min'' \<Colon>\<subseteq> intT
   136     else let (l, m) = divAlg (k, 2)
   137   in STR ''Numeral.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
   138     (if m = 0 then STR ''Numeral.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Numeral.bit.B1'' \<Colon>\<subseteq> bitT))"
   139 by pat_completeness auto
   140 termination by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
   141 
   142 instance int :: term_of
   143   "term_of k \<equiv> STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k" ..
   144 
   145 
   146 text {* Adaption for @{typ ml_string}s *}
   147 
   148 lemmas [code func, code func del] = term_of_ml_string_def
   149 
   150 
   151 subsection {* Evaluation infrastructure *}
   152 
   153 ML {*
   154 signature EVAL =
   155 sig
   156   val eval_ref: term option ref
   157   val eval_conv: cterm -> thm
   158   val eval_print: (cterm -> thm) -> Proof.context -> term -> unit
   159   val eval_print_cmd: (cterm -> thm) -> string -> Toplevel.state -> unit
   160 end;
   161 
   162 structure Eval =
   163 struct
   164 
   165 val eval_ref = ref (NONE : term option);
   166 
   167 end;
   168 *}
   169 
   170 oracle eval_oracle ("term * CodeThingol.code * (CodeThingol.typscheme * CodeThingol.iterm) * cterm") =
   171 {* fn thy => fn (t0, code, ((vs, ty), t), ct) => 
   172 let
   173   val _ = (Term.map_types o Term.map_atyps) (fn _ =>
   174     error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
   175     t0;
   176 in Logic.mk_equals (t0, CodeTarget.eval_term thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) []) end;
   177 *}
   178 
   179 ML {*
   180 structure Eval : EVAL =
   181 struct
   182 
   183 open Eval;
   184 
   185 fun eval_invoke thy t0 code vs_ty_t _ ct = eval_oracle thy (t0, code, vs_ty_t, ct);
   186 
   187 fun eval_conv ct =
   188   let
   189     val thy = Thm.theory_of_cterm ct;
   190     val ct' = (Thm.cterm_of thy o TermOf.mk_term_of o Thm.term_of) ct;
   191   in
   192     CodePackage.eval_term thy
   193       (eval_invoke thy (Thm.term_of ct)) ct'
   194   end;
   195 
   196 fun eval_print conv ctxt t =
   197   let
   198     val thy = ProofContext.theory_of ctxt;
   199     val ct = Thm.cterm_of thy t;
   200     val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
   201     val ty = Term.type_of t';
   202     val p = 
   203       Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
   204         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)];
   205   in Pretty.writeln p end;
   206 
   207 fun eval_print_cmd conv raw_t state =
   208   let
   209     val ctxt = Toplevel.context_of state;
   210     val t = ProofContext.read_term ctxt raw_t;
   211     val thy = ProofContext.theory_of ctxt;
   212     val ct = Thm.cterm_of thy t;
   213     val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
   214     val ty = Term.type_of t';
   215     val p = 
   216       Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
   217         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)];
   218   in Pretty.writeln p end;
   219 
   220 end;
   221 *}
   222 
   223 ML {*
   224 val valueP =
   225   OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
   226     ((OuterParse.opt_keyword "overloaded" -- OuterParse.term)
   227       >> (fn (b, t) => Toplevel.no_timing o Toplevel.keep
   228            (Eval.eval_print_cmd (if b then Eval.eval_conv else Codegen.evaluation_conv) t)));
   229 
   230 val _ = OuterSyntax.add_parsers [valueP];
   231 *}
   232 
   233 end