src/HOL/Tools/code_evaluation.ML
author haftmann
Mon Sep 20 15:25:32 2010 +0200 (2010-09-20)
changeset 39565 f4f87c6e2fad
parent 39564 acfd10e38e80
child 39567 5ee997fbe5cc
permissions -rw-r--r--
full palette of dynamic/static value(_strict/exn)
     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 put_term: (unit -> term) -> Proof.context -> Proof.context
    16   val tracing: string -> 'a -> 'a
    17   val setup: theory -> theory
    18 end;
    19 
    20 structure Code_Evaluation : CODE_EVALUATION =
    21 struct
    22 
    23 (** term_of instances **)
    24 
    25 (* formal definition *)
    26 
    27 fun add_term_of tyco raw_vs thy =
    28   let
    29     val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    30     val ty = Type (tyco, map TFree vs);
    31     val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    32       $ Free ("x", ty);
    33     val rhs = @{term "undefined :: term"};
    34     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    35     fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    36       o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    37   in
    38     thy
    39     |> Class.instantiation ([tyco], vs, @{sort term_of})
    40     |> `(fn lthy => Syntax.check_term lthy eq)
    41     |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    42     |> snd
    43     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    44   end;
    45 
    46 fun ensure_term_of (tyco, (raw_vs, _)) thy =
    47   let
    48     val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    49       andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    50   in if need_inst then add_term_of tyco raw_vs thy else thy end;
    51 
    52 
    53 (* code equations for datatypes *)
    54 
    55 fun mk_term_of_eq thy ty (c, tys) =
    56   let
    57     val t = list_comb (Const (c, tys ---> ty),
    58       map Free (Name.names Name.context "a" tys));
    59     val (arg, rhs) =
    60       pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    61         (t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    62     val cty = Thm.ctyp_of thy ty;
    63   in
    64     @{thm term_of_anything}
    65     |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
    66     |> Thm.varifyT_global
    67   end;
    68 
    69 fun add_term_of_code tyco raw_vs raw_cs thy =
    70   let
    71     val algebra = Sign.classes_of thy;
    72     val vs = map (fn (v, sort) =>
    73       (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
    74     val ty = Type (tyco, map TFree vs);
    75     val cs = (map o apsnd o map o map_atyps)
    76       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    77     val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    78     val eqs = map (mk_term_of_eq thy ty) cs;
    79  in
    80     thy
    81     |> Code.del_eqns const
    82     |> fold Code.add_eqn eqs
    83   end;
    84 
    85 fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
    86   let
    87     val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
    88   in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
    89 
    90 
    91 (* code equations for abstypes *)
    92 
    93 fun mk_abs_term_of_eq thy ty abs ty_rep proj =
    94   let
    95     val arg = Var (("x", 0), ty);
    96     val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
    97       (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
    98       |> Thm.cterm_of thy;
    99     val cty = Thm.ctyp_of thy ty;
   100   in
   101     @{thm term_of_anything}
   102     |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
   103     |> Thm.varifyT_global
   104   end;
   105 
   106 fun add_abs_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
   107   let
   108     val algebra = Sign.classes_of thy;
   109     val vs = map (fn (v, sort) =>
   110       (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
   111     val ty = Type (tyco, map TFree vs);
   112     val ty_rep = map_atyps
   113       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
   114     val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   115     val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
   116  in
   117     thy
   118     |> Code.del_eqns const
   119     |> Code.add_eqn eq
   120   end;
   121 
   122 fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
   123   let
   124     val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   125   in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
   126 
   127 
   128 (** termifying syntax **)
   129 
   130 fun map_default f xs =
   131   let val ys = map f xs
   132   in if exists is_some ys
   133     then SOME (map2 the_default xs ys)
   134     else NONE
   135   end;
   136 
   137 fun subst_termify_app (Const (@{const_name termify}, _), [t]) =
   138       if not (Term.has_abs t)
   139       then if fold_aterms (fn Const _ => I | _ => K false) t true
   140         then SOME (HOLogic.reflect_term t)
   141         else error "Cannot termify expression containing variables"
   142       else error "Cannot termify expression containing abstraction"
   143   | subst_termify_app (t, ts) = case map_default subst_termify ts
   144      of SOME ts' => SOME (list_comb (t, ts'))
   145       | NONE => NONE
   146 and subst_termify (Abs (v, T, t)) = (case subst_termify t
   147      of SOME t' => SOME (Abs (v, T, t'))
   148       | NONE => NONE)
   149   | subst_termify t = subst_termify_app (strip_comb t) 
   150 
   151 fun check_termify ts ctxt = map_default subst_termify ts
   152   |> Option.map (rpair ctxt)
   153 
   154 
   155 (** evaluation **)
   156 
   157 structure Evaluation = Proof_Data (
   158   type T = unit -> term
   159   fun init _ () = error "Evaluation"
   160 );
   161 val put_term = Evaluation.put;
   162 val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");
   163 
   164 fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
   165 
   166 fun term_of_const_for thy = AxClass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
   167 
   168 fun gen_dynamic_value dynamic_value thy t =
   169   dynamic_value cookie thy NONE I (mk_term_of t) [];
   170 
   171 val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
   172 val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
   173 val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
   174 
   175 fun gen_static_value static_value thy consts Ts =
   176   static_value cookie thy NONE I (union (op =) (map (term_of_const_for thy) Ts) consts)
   177   o mk_term_of;
   178 
   179 val static_value = gen_static_value Code_Runtime.static_value;
   180 val static_value_strict = gen_static_value Code_Runtime.static_value_strict;
   181 val static_value_exn = gen_static_value Code_Runtime.static_value_exn;
   182 
   183 
   184 (** diagnostic **)
   185 
   186 fun tracing s x = (Output.tracing s; x);
   187 
   188 
   189 (** setup **)
   190 
   191 val setup =
   192   Code.datatype_interpretation ensure_term_of
   193   #> Code.abstype_interpretation ensure_term_of
   194   #> Code.datatype_interpretation ensure_term_of_code
   195   #> Code.abstype_interpretation ensure_abs_term_of_code
   196   #> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
   197   #> Value.add_evaluator ("code", dynamic_value_strict o ProofContext.theory_of);
   198 
   199 end;