src/HOL/Library/Eval.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 27368 9f90ac19e32b
child 27681 8cedebf55539
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
     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
    10   Plain
    11   RType
    12   Code_Index (* this theory is just imported for a term_of setup *)
    13 begin
    14 
    15 subsection {* Term representation *}
    16 
    17 subsubsection {* Terms and class @{text term_of} *}
    18 
    19 datatype "term" = dummy_term
    20 
    21 definition
    22   Const :: "message_string \<Rightarrow> rtype \<Rightarrow> term"
    23 where
    24   "Const _ _ = dummy_term"
    25 
    26 definition
    27   App :: "term \<Rightarrow> term \<Rightarrow> term"
    28 where
    29   "App _ _ = dummy_term"
    30 
    31 code_datatype Const App
    32 
    33 class term_of = rtype +
    34   fixes term_of :: "'a \<Rightarrow> term"
    35 
    36 lemma term_of_anything: "term_of x \<equiv> t"
    37   by (rule eq_reflection) (cases "term_of x", cases t, simp)
    38 
    39 ML {*
    40 structure Eval =
    41 struct
    42 
    43 fun mk_term f g (Const (c, ty)) =
    44       @{term Const} $ Message_String.mk c $ g ty
    45   | mk_term f g (t1 $ t2) =
    46       @{term App} $ mk_term f g t1 $ mk_term f g t2
    47   | mk_term f g (Free v) = f v
    48   | mk_term f g (Bound i) = Bound i
    49   | mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t);
    50 
    51 fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t;
    52 
    53 end;
    54 *}
    55 
    56 
    57 subsubsection {* @{text term_of} instances *}
    58 
    59 setup {*
    60 let
    61   fun add_term_of_def ty vs tyco thy =
    62     let
    63       val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    64         $ Free ("x", ty);
    65       val rhs = @{term "undefined \<Colon> term"};
    66       val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    67     in
    68       thy
    69       |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
    70       |> `(fn lthy => Syntax.check_term lthy eq)
    71       |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
    72       |> snd
    73       |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    74       |> LocalTheory.exit
    75       |> ProofContext.theory_of
    76     end;
    77   fun interpretator (tyco, (raw_vs, _)) thy =
    78     let
    79       val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    80       val constrain_sort =
    81         curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
    82       val vs = (map o apsnd) constrain_sort raw_vs;
    83       val ty = Type (tyco, map TFree vs);
    84     in
    85       thy
    86       |> RType.perhaps_add_def tyco
    87       |> not has_inst ? add_term_of_def ty vs tyco
    88     end;
    89 in
    90   Code.type_interpretation interpretator
    91 end
    92 *}
    93 
    94 setup {*
    95 let
    96   fun mk_term_of_eq ty vs tyco (c, tys) =
    97     let
    98       val t = list_comb (Const (c, tys ---> ty),
    99         map Free (Name.names Name.context "a" tys));
   100     in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term
   101       (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty)))
   102       (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))) t)
   103     end;
   104   fun prove_term_of_eq ty eq thy =
   105     let
   106       val cty = Thm.ctyp_of thy ty;
   107       val (arg, rhs) = pairself (Thm.cterm_of thy) eq;
   108       val thm = @{thm term_of_anything}
   109         |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
   110         |> Thm.varifyT;
   111     in
   112       thy
   113       |> Code.add_func thm
   114     end;
   115   fun interpretator (tyco, (raw_vs, raw_cs)) thy =
   116     let
   117       val constrain_sort =
   118         curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
   119       val vs = (map o apsnd) constrain_sort raw_vs;
   120       val cs = (map o apsnd o map o map_atyps)
   121         (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs;
   122       val ty = Type (tyco, map TFree vs);
   123       val eqs = map (mk_term_of_eq ty vs tyco) cs;
   124       val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   125     in
   126       thy
   127       |> Code.del_funcs const
   128       |> fold (prove_term_of_eq ty) eqs
   129     end;
   130 in
   131   Code.type_interpretation interpretator
   132 end
   133 *}
   134 
   135 
   136 subsubsection {* Code generator setup *}
   137 
   138 lemmas [code func del] = term.recs term.cases term.size
   139 lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
   140 
   141 lemma [code func, code func del]: "(term_of \<Colon> rtype \<Rightarrow> term) = term_of" ..
   142 lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
   143 lemma [code func, code func del]: "(term_of \<Colon> index \<Rightarrow> term) = term_of" ..
   144 lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
   145 
   146 code_type "term"
   147   (SML "Term.term")
   148 
   149 code_const Const and App
   150   (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)")
   151 
   152 code_const "term_of \<Colon> index \<Rightarrow> term"
   153   (SML "HOLogic.mk'_number/ HOLogic.indexT")
   154 
   155 code_const "term_of \<Colon> message_string \<Rightarrow> term"
   156   (SML "Message'_String.mk")
   157 
   158 
   159 subsubsection {* Syntax *}
   160 
   161 print_translation {*
   162 let
   163   val term = Const ("<TERM>", dummyT);
   164   fun tr1' [_, _] = term;
   165   fun tr2' [] = term;
   166 in
   167   [(@{const_syntax Const}, tr1'),
   168     (@{const_syntax App}, tr1'),
   169     (@{const_syntax dummy_term}, tr2')]
   170 end
   171 *}
   172 setup {*
   173   Sign.declare_const [] ("rterm_of", @{typ "'a \<Rightarrow> 'b"}, NoSyn)
   174   #> snd
   175 *}
   176 
   177 notation (output)
   178   rterm_of ("\<guillemotleft>_\<guillemotright>")
   179 
   180 locale (open) rterm_syntax =
   181   fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
   182 
   183 parse_translation {*
   184 let
   185   fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
   186     | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
   187 in
   188   [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)]
   189 end
   190 *}
   191 
   192 setup {*
   193 let
   194   val subst_rterm_of = Eval.mk_term
   195     (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v))
   196     (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort))));
   197   fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
   198     | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
   199         error ("illegal number of arguments for " ^ quote @{const_name rterm_of})
   200     | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts);
   201   fun subst_rterm_of'' t = 
   202     let
   203       val t' = subst_rterm_of' (strip_comb t);
   204     in if t aconv t'
   205       then NONE
   206       else SOME t'
   207     end;
   208   fun check_rterm_of ts ctxt =
   209     let
   210       val ts' = map subst_rterm_of'' ts;
   211     in if exists is_some ts'
   212       then SOME (map2 the_default ts ts', ctxt)
   213       else NONE
   214     end;
   215 in
   216   Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of)
   217 end;
   218 *}
   219 
   220 hide const dummy_term
   221 hide (open) const Const App
   222 hide (open) const term_of
   223 
   224 
   225 subsection {* Evaluation setup *}
   226 
   227 ML {*
   228 signature EVAL =
   229 sig
   230   val mk_term: ((string * typ) -> term) -> (typ -> term) -> term -> term
   231   val eval_ref: (unit -> term) option ref
   232   val eval_term: theory -> term -> term
   233   val evaluate: Proof.context -> term -> unit
   234   val evaluate': string -> Proof.context -> term -> unit
   235   val evaluate_cmd: string option -> string -> Toplevel.state -> unit
   236 end;
   237 
   238 structure Eval : EVAL =
   239 struct
   240 
   241 open Eval;
   242 
   243 val eval_ref = ref (NONE : (unit -> term) option);
   244 
   245 fun eval_term thy t =
   246   t 
   247   |> Eval.mk_term_of (fastype_of t)
   248   |> (fn t => CodeTarget.eval_term ("Eval.eval_ref", eval_ref) thy t [])
   249   |> Code.postprocess_term thy;
   250 
   251 val evaluators = [
   252   ("code", eval_term),
   253   ("SML", Codegen.eval_term),
   254   ("normal_form", Nbe.norm_term)
   255 ];
   256 
   257 fun gen_evaluate evaluators ctxt t =
   258   let
   259     val thy = ProofContext.theory_of ctxt;
   260     val (evls, evl) = split_last evaluators;
   261     val t' = case get_first (fn f => try (f thy) t) evls
   262      of SOME t' => t'
   263       | NONE => evl thy t;
   264     val ty' = Term.type_of t';
   265     val p = Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'),
   266       Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
   267       Pretty.quote (Syntax.pretty_typ ctxt ty')];
   268   in Pretty.writeln p end;
   269 
   270 val evaluate = gen_evaluate (map snd evaluators);
   271 
   272 fun evaluate' name = gen_evaluate
   273   [(the o AList.lookup (op =) evaluators) name];
   274 
   275 fun evaluate_cmd some_name raw_t state =
   276   let
   277     val ctxt = Toplevel.context_of state;
   278     val t = Syntax.read_term ctxt raw_t;
   279   in case some_name
   280    of NONE => evaluate ctxt t
   281     | SOME name => evaluate' name ctxt t
   282   end;
   283 
   284 end;
   285 *}
   286 
   287 ML {*
   288   OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
   289     (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
   290     -- OuterParse.term
   291       >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
   292            (Eval.evaluate_cmd some_name t)));
   293 *}
   294 
   295 end