src/HOL/Tools/code_evaluation.ML
author haftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 41075 4bed56dc95fb
parent 40726 16dcfedc4eb7
child 41184 5c6f44d22f51
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
     1 (*  Title:      HOL/Tools/code_evaluation.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Evaluation and reconstruction of terms in ML.
     5 *)
     6 
     7 signature CODE_EVALUATION =
     8 sig
     9   val dynamic_value: theory -> term -> term option
    10   val dynamic_value_strict: theory -> term -> term
    11   val dynamic_value_exn: theory -> term -> term Exn.result
    12   val static_value: theory -> string list -> typ list -> term -> term option
    13   val static_value_strict: theory -> string list -> typ list -> term -> term
    14   val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
    15   val dynamic_eval_conv: conv
    16   val static_eval_conv: theory -> string list -> typ list -> conv
    17   val put_term: (unit -> term) -> Proof.context -> Proof.context
    18   val tracing: string -> 'a -> 'a
    19   val setup: theory -> theory
    20 end;
    21 
    22 structure Code_Evaluation : CODE_EVALUATION =
    23 struct
    24 
    25 (** term_of instances **)
    26 
    27 (* formal definition *)
    28 
    29 fun add_term_of tyco raw_vs thy =
    30   let
    31     val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    32     val ty = Type (tyco, map TFree vs);
    33     val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    34       $ Free ("x", ty);
    35     val rhs = @{term "undefined :: term"};
    36     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    37     fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    38       o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    39   in
    40     thy
    41     |> Class.instantiation ([tyco], vs, @{sort term_of})
    42     |> `(fn lthy => Syntax.check_term lthy eq)
    43     |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    44     |> snd
    45     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    46   end;
    47 
    48 fun ensure_term_of (tyco, (raw_vs, _)) thy =
    49   let
    50     val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    51       andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    52   in if need_inst then add_term_of tyco raw_vs thy else thy end;
    53 
    54 
    55 (* code equations for datatypes *)
    56 
    57 fun mk_term_of_eq thy ty (c, (_, tys)) =
    58   let
    59     val t = list_comb (Const (c, tys ---> ty),
    60       map Free (Name.names Name.context "a" tys));
    61     val (arg, rhs) =
    62       pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    63         (t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    64     val cty = Thm.ctyp_of thy ty;
    65   in
    66     @{thm term_of_anything}
    67     |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    68     |> Thm.varifyT_global
    69   end;
    70 
    71 fun add_term_of_code tyco raw_vs raw_cs thy =
    72   let
    73     val algebra = Sign.classes_of thy;
    74     val vs = map (fn (v, sort) =>
    75       (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
    76     val ty = Type (tyco, map TFree vs);
    77     val cs = (map o apsnd o apsnd o map o map_atyps)
    78       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    79     val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    80     val eqs = map (mk_term_of_eq thy ty) cs;
    81  in
    82     thy
    83     |> Code.del_eqns const
    84     |> fold Code.add_eqn eqs
    85   end;
    86 
    87 fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
    88   let
    89     val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    90   in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
    91 
    92 
    93 (* code equations for abstypes *)
    94 
    95 fun mk_abs_term_of_eq thy ty abs ty_rep proj =
    96   let
    97     val arg = Var (("x", 0), ty);
    98     val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
    99       (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
   100       |> Thm.cterm_of thy;
   101     val cty = Thm.ctyp_of thy ty;
   102   in
   103     @{thm term_of_anything}
   104     |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
   105     |> Thm.varifyT_global
   106   end;
   107 
   108 fun add_abs_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
   109   let
   110     val algebra = Sign.classes_of thy;
   111     val vs = map (fn (v, sort) =>
   112       (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
   113     val ty = Type (tyco, map TFree vs);
   114     val ty_rep = map_atyps
   115       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
   116     val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   117     val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
   118  in
   119     thy
   120     |> Code.del_eqns const
   121     |> Code.add_eqn eq
   122   end;
   123 
   124 fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, (_, ty)), (proj, _)))) thy =
   125   let
   126     val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   127   in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
   128 
   129 
   130 (** termifying syntax **)
   131 
   132 fun map_default f xs =
   133   let val ys = map f xs
   134   in if exists is_some ys
   135     then SOME (map2 the_default xs ys)
   136     else NONE
   137   end;
   138 
   139 fun subst_termify_app (Const (@{const_name termify}, _), [t]) =
   140       if not (Term.has_abs t)
   141       then if fold_aterms (fn Const _ => I | _ => K false) t true
   142         then SOME (HOLogic.reflect_term t)
   143         else error "Cannot termify expression containing variables"
   144       else error "Cannot termify expression containing abstraction"
   145   | subst_termify_app (t, ts) = case map_default subst_termify ts
   146      of SOME ts' => SOME (list_comb (t, ts'))
   147       | NONE => NONE
   148 and subst_termify (Abs (v, T, t)) = (case subst_termify t
   149      of SOME t' => SOME (Abs (v, T, t'))
   150       | NONE => NONE)
   151   | subst_termify t = subst_termify_app (strip_comb t) 
   152 
   153 fun check_termify ts ctxt = map_default subst_termify ts
   154   |> Option.map (rpair ctxt)
   155 
   156 
   157 (** evaluation **)
   158 
   159 structure Evaluation = Proof_Data (
   160   type T = unit -> term
   161   fun init _ () = error "Evaluation"
   162 );
   163 val put_term = Evaluation.put;
   164 val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");
   165 
   166 fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
   167 
   168 fun term_of_const_for thy = AxClass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
   169 
   170 fun gen_dynamic_value dynamic_value thy t =
   171   dynamic_value cookie thy NONE I (mk_term_of t) [];
   172 
   173 val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
   174 val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
   175 val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
   176 
   177 fun gen_static_value static_value thy consts Ts =
   178   static_value cookie thy NONE I (union (op =) (map (term_of_const_for thy) Ts) consts)
   179   o mk_term_of;
   180 
   181 val static_value = gen_static_value Code_Runtime.static_value;
   182 val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
   183 val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
   184 
   185 fun certify_eval thy value conv ct =
   186   let
   187     val t = Thm.term_of ct;
   188     val T = fastype_of t;
   189     val mk_eq = Thm.mk_binop (Thm.cterm_of thy (Const ("==", T --> T --> propT)));
   190   in case value t
   191    of NONE => Thm.reflexive ct
   192     | SOME t' => conv (mk_eq ct (Thm.cterm_of thy t')) RS @{thm eq_eq_TrueD}
   193         handle THM _ =>
   194           error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
   195   end;
   196 
   197 val dynamic_eval_conv = Conv.tap_thy
   198   (fn thy => certify_eval thy (dynamic_value thy) Code_Runtime.dynamic_holds_conv);
   199 
   200 fun static_eval_conv thy consts Ts =
   201   let
   202     val eqs = "==" :: @{const_name HOL.eq} ::
   203       map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
   204         (*assumes particular code equations for "==" etc.*)
   205   in
   206     certify_eval thy (static_value thy consts Ts)
   207       (Code_Runtime.static_holds_conv thy (union (op =) eqs consts))
   208   end;
   209 
   210 
   211 (** diagnostic **)
   212 
   213 fun tracing s x = (Output.tracing s; x);
   214 
   215 
   216 (** setup **)
   217 
   218 val setup =
   219   Code.datatype_interpretation ensure_term_of
   220   #> Code.abstype_interpretation ensure_term_of
   221   #> Code.datatype_interpretation ensure_term_of_code
   222   #> Code.abstype_interpretation ensure_abs_term_of_code
   223   #> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
   224   #> Value.add_evaluator ("code", dynamic_value_strict o ProofContext.theory_of);
   225 
   226 end;