src/HOL/Library/Eval.thy
author haftmann
Tue Dec 18 14:37:00 2007 +0100 (2007-12-18)
changeset 25691 8f8d83af100a
parent 25666 f46ed5b333fd
child 25763 474f8ba9dfa9
permissions -rw-r--r--
switched from PreList to ATP_Linkup
     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 ATP_Linkup 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 fun mk ty =
    22   Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
    23     $ Logic.mk_type ty;
    24 
    25 end
    26 *}
    27 
    28 setup {*
    29 let
    30   fun define_typ_of ty lthy =
    31     let
    32       val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
    33         $ Free ("T", Term.itselfT ty);
    34       val rhs = Pure_term.mk_typ (fn v => TypOf.mk (TFree v)) ty;
    35       val eq = Syntax.check_term lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
    36     in lthy |> Specification.definition (NONE, (("", []), eq)) end;
    37   fun interpretator tyco thy =
    38     let
    39       val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of};
    40       val ty = Type (tyco, map TFree (Name.names Name.context "'a" sorts));
    41     in
    42       thy
    43       |> TheoryTarget.instantiation ([tyco], sorts, @{sort typ_of})
    44       |> define_typ_of ty
    45       |> snd
    46       |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    47       |> LocalTheory.exit
    48       |> ProofContext.theory_of
    49     end;
    50 in TypedefPackage.interpretation interpretator end
    51 *}
    52 
    53 instantiation "prop" :: typ_of
    54 begin
    55 
    56 definition 
    57   "typ_of (T\<Colon>prop itself) = Type (STR ''prop'') []"
    58 
    59 instance ..
    60 
    61 end
    62 
    63 instantiation itself :: (typ_of) typ_of
    64 begin
    65 
    66 definition
    67   "typ_of (T\<Colon>'a itself itself) = Type (STR ''itself'') [typ_of TYPE('a\<Colon>typ_of)]"
    68 
    69 instance ..
    70 
    71 end
    72 
    73 instantiation set :: (typ_of) typ_of
    74 begin
    75  
    76 definition
    77   "typ_of (T\<Colon>'a set itself) = Type (STR ''set'') [typ_of TYPE('a\<Colon>typ_of)]"
    78 
    79 instance ..
    80 
    81 end
    82 
    83 
    84 subsection {* @{text term_of} class *}
    85 
    86 class term_of = typ_of +
    87   constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ"
    88   fixes term_of :: "'a \<Rightarrow> term"
    89 
    90 ML {*
    91 structure TermOf =
    92 struct
    93 
    94 local
    95   fun term_term_of ty =
    96     Const (@{const_name term_of}, ty --> @{typ term});
    97 in
    98   val class_term_of = Sign.intern_class @{theory} "term_of";
    99   fun mk_terms_of_defs vs (tyco, cs) =
   100     let
   101       val dty = Type (tyco, map TFree vs);
   102       fun mk_eq c =
   103         let
   104           val lhs : term = term_term_of dty $ c;
   105           val rhs : term = Pure_term.mk_term
   106             (fn (v, ty) => term_term_of ty $ Free (v, ty))
   107             (Pure_term.mk_typ (fn (v, sort) => TypOf.mk (TFree (v, sort)))) c
   108         in
   109           HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   110         end;
   111     in map mk_eq cs end;
   112   fun mk_term_of t =
   113     term_term_of (Term.fastype_of t) $ t;
   114 end;
   115 
   116 end;
   117 *}
   118 
   119 setup {*
   120 let
   121   fun thy_note ((name, atts), thms) =
   122     PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
   123   fun thy_def ((name, atts), t) =
   124     PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
   125   fun prep_dtyp thy vs tyco =
   126     let
   127       val (_, cs) = DatatypePackage.the_datatype_spec thy tyco;
   128       val prep_typ = map_atyps (fn TFree (v, sort) =>
   129         TFree (v, (the o AList.lookup (op =) vs) v));
   130       fun prep_c (c, tys) = list_comb (Const (c, tys ---> Type (tyco, map TFree vs)),
   131         map Free (Name.names Name.context "a" tys));
   132     in (tyco, map (prep_c o (apsnd o map) prep_typ) cs) end;
   133   fun prep thy tycos =
   134     let
   135       val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
   136       val tyco = hd tycos;
   137       val (vs_proto, _) = DatatypePackage.the_datatype_spec thy tyco;
   138       val all_typs = maps (maps snd o snd o DatatypePackage.the_datatype_spec thy) tycos;
   139       fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #>
   140             fold add_tycos tys
   141         | add_tycos _ = I;
   142       val dep_tycos = [] |> fold add_tycos all_typs |> subtract (op =) tycos;
   143       val sorts = map (inter_sort o snd) vs_proto;
   144       val vs = map fst vs_proto ~~ sorts;
   145       val css = map (prep_dtyp thy vs) tycos;
   146       val defs = map (TermOf.mk_terms_of_defs vs) css;
   147     in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos
   148         andalso not (tycos = [@{type_name typ}])
   149       then SOME (sorts, defs)
   150       else NONE
   151     end;
   152   fun prep' ctxt proto_eqs =
   153     let
   154       val eqs as eq :: _ = map (Syntax.check_term ctxt) proto_eqs;
   155       val (Free (v, ty), _) =
   156         (strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
   157     in ((v, SOME ty, NoSyn), map (pair ("", [])) eqs) end;
   158   fun primrec primrecs ctxt =
   159     let
   160       val (fixes, eqnss) = split_list (map (prep' ctxt) primrecs);
   161     in PrimrecPackage.add_primrec fixes (flat eqnss) ctxt end;
   162   fun interpretator tycos thy = case prep thy tycos
   163    of SOME (sorts, defs) =>
   164       thy
   165       |> TheoryTarget.instantiation (tycos, sorts, @{sort term_of})
   166       |> primrec defs
   167       |> snd
   168       |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   169       |> LocalTheory.exit
   170       |> ProofContext.theory_of
   171     | NONE => thy;
   172   in DatatypePackage.interpretation interpretator end
   173 *}
   174 
   175 abbreviation (in pure_term_syntax) (input)
   176   intT :: "typ"
   177 where
   178   "intT \<equiv> Type (STR ''IntDef.int'') []"
   179 
   180 abbreviation (in pure_term_syntax) (input)
   181   bitT :: "typ"
   182 where
   183   "bitT \<equiv> Type (STR ''Numeral.bit'') []"
   184 
   185 function (in pure_term_syntax)
   186   mk_int :: "int \<Rightarrow> term"
   187 where
   188   "mk_int k = (if k = 0 then STR ''Numeral.Pls'' \<Colon>\<subseteq> intT
   189     else if k = -1 then STR ''Numeral.Min'' \<Colon>\<subseteq> intT
   190     else let (l, m) = divAlg (k, 2)
   191   in STR ''Numeral.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
   192     (if m = 0 then STR ''Numeral.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Numeral.bit.B1'' \<Colon>\<subseteq> bitT))"
   193 by pat_completeness auto
   194 termination (in pure_term_syntax)
   195 by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
   196 
   197 declare pure_term_syntax.mk_int.simps [code func]
   198 
   199 definition (in pure_term_syntax)
   200   "term_of_int_aux k = STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
   201 
   202 declare pure_term_syntax.term_of_int_aux_def [code func]
   203 
   204 instantiation int :: term_of
   205 begin
   206 
   207 definition
   208   "term_of = pure_term_syntax.term_of_int_aux"
   209 
   210 instance ..
   211 
   212 end
   213 
   214 
   215 text {* Adaption for @{typ message_string}s *}
   216 
   217 lemmas [code func del] = term_of_message_string.simps
   218 
   219 
   220 subsection {* Evaluation infrastructure *}
   221 
   222 ML {*
   223 signature EVAL =
   224 sig
   225   val eval_ref: (unit -> term) option ref
   226   val eval_term: theory -> term -> term
   227   val evaluate: Proof.context -> term -> unit
   228   val evaluate': string -> Proof.context -> term -> unit
   229   val evaluate_cmd: string option -> Toplevel.state -> unit
   230 end;
   231 
   232 structure Eval =
   233 struct
   234 
   235 val eval_ref = ref (NONE : (unit -> term) option);
   236 
   237 fun eval_invoke thy code ((_, ty), t) deps _ =
   238   CodeTarget.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
   239 
   240 fun eval_term thy =
   241   TermOf.mk_term_of
   242   #> CodePackage.eval_term thy (eval_invoke thy)
   243   #> Code.postprocess_term thy;
   244 
   245 val evaluators = [
   246   ("code", eval_term),
   247   ("SML", Codegen.eval_term),
   248   ("normal_form", Nbe.norm_term)
   249 ];
   250 
   251 fun gen_evaluate evaluators ctxt t =
   252   let
   253     val thy = ProofContext.theory_of ctxt;
   254     val (evls, evl) = split_last evaluators;
   255     val t' = case get_first (fn f => try (f thy) t) evls
   256      of SOME t' => t'
   257       | NONE => evl thy t;
   258     val ty' = Term.type_of t';
   259     val p = Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'),
   260       Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
   261       Pretty.quote (Syntax.pretty_typ ctxt ty')];
   262   in Pretty.writeln p end;
   263 
   264 val evaluate = gen_evaluate (map snd evaluators);
   265 
   266 fun evaluate' name = gen_evaluate
   267   [(the o AList.lookup (op =) evaluators) name];
   268 
   269 fun evaluate_cmd some_name raw_t state =
   270   let
   271     val ctxt = Toplevel.context_of state;
   272     val t = Syntax.read_term ctxt raw_t;
   273   in case some_name
   274    of NONE => evaluate ctxt t
   275     | SOME name => evaluate' name ctxt t
   276   end;
   277 
   278 end;
   279 *}
   280 
   281 ML {*
   282   OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
   283     (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
   284     -- OuterParse.term
   285       >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
   286            (Eval.evaluate_cmd some_name t)));
   287 *}
   288 
   289 end