src/HOL/Tools/code_evaluation.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 66330 dcb3e6bdc00a
child 67149 e61557884799
permissions -rw-r--r--
tuned;
     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: Proof.context -> term -> term option
    10   val dynamic_value_strict: Proof.context -> term -> term
    11   val dynamic_value_exn: Proof.context -> term -> term Exn.result
    12   val put_term: (unit -> term) -> Proof.context -> Proof.context
    13   val tracing: string -> 'a -> 'a
    14 end;
    15 
    16 structure Code_Evaluation : CODE_EVALUATION =
    17 struct
    18 
    19 (** term_of instances **)
    20 
    21 (* formal definition *)
    22 
    23 fun add_term_of_inst tyco thy =
    24   let
    25     val ((raw_vs, _), _) = Code.get_type thy tyco;
    26     val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    27     val ty = Type (tyco, map TFree vs);
    28     val lhs = Const (@{const_name term_of}, ty --> @{typ term})
    29       $ Free ("x", ty);
    30     val rhs = @{term "undefined :: term"};
    31     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    32     fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    33       o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    34   in
    35     thy
    36     |> Class.instantiation ([tyco], vs, @{sort term_of})
    37     |> `(fn lthy => Syntax.check_term lthy eq)
    38     |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
    39     |> snd
    40     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
    41   end;
    42 
    43 fun ensure_term_of_inst tyco thy =
    44   let
    45     val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of})
    46       andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
    47   in if need_inst then add_term_of_inst tyco thy else thy end;
    48 
    49 fun for_term_of_instance tyco vs f thy =
    50   let
    51     val algebra = Sign.classes_of thy;
    52   in
    53     case try (Sorts.mg_domain algebra tyco) @{sort term_of} of
    54       NONE => thy
    55     | SOME sorts => f tyco (map2 (fn (v, sort) => fn sort' =>
    56         (v, Sorts.inter_sort algebra (sort, sort'))) vs sorts) thy
    57   end;
    58 
    59 
    60 (* code equations for datatypes *)
    61 
    62 fun mk_term_of_eq thy ty (c, (_, tys)) =
    63   let
    64     val t = list_comb (Const (c, tys ---> ty),
    65       map Free (Name.invent_names Name.context "a" tys));
    66     val (arg, rhs) =
    67       apply2 (Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
    68         (t,
    69           map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t)
    70             (HOLogic.reflect_term t));
    71     val cty = Thm.global_ctyp_of thy ty;
    72   in
    73     @{thm term_of_anything}
    74     |> Thm.instantiate' [SOME cty] [SOME arg, SOME rhs]
    75     |> Thm.varifyT_global
    76   end;
    77 
    78 fun add_term_of_code_datatype tyco vs raw_cs thy =
    79   let
    80     val ty = Type (tyco, map TFree vs);
    81     val cs = (map o apsnd o apsnd o map o map_atyps)
    82       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    83     val eqs = map (mk_term_of_eq thy ty) cs;
    84  in
    85     thy
    86     |> Code.declare_default_eqns_global (map (rpair true) eqs)
    87   end;
    88 
    89 fun ensure_term_of_code_datatype (tyco, (vs, cs)) =
    90   for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code_datatype tyco vs cs);
    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.global_cterm_of thy;
   101     val cty = Thm.global_ctyp_of thy ty;
   102   in
   103     @{thm term_of_anything}
   104     |> Thm.instantiate' [SOME cty] [SOME (Thm.global_cterm_of thy arg), SOME rhs]
   105     |> Thm.varifyT_global
   106   end;
   107 
   108 fun add_term_of_code_abstype tyco vs abs raw_ty_rep projection thy =
   109   let
   110     val ty = Type (tyco, map TFree vs);
   111     val ty_rep = map_atyps
   112       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
   113     val eq = mk_abs_term_of_eq thy ty abs ty_rep projection;
   114  in
   115     thy
   116     |> Code.declare_default_eqns_global [(eq, true)]
   117   end;
   118 
   119 fun ensure_term_of_code_abstype (tyco, (vs, {abstractor = (abs, (_, ty)),
   120     projection, ...})) =
   121   for_term_of_instance tyco vs
   122     (fn tyco => fn vs => add_term_of_code_abstype tyco vs abs ty projection);
   123 
   124 
   125 (* setup *)
   126 
   127 val _ = Theory.setup
   128   (Code.type_interpretation ensure_term_of_inst
   129   #> Code.datatype_interpretation ensure_term_of_code_datatype
   130   #> Code.abstype_interpretation ensure_term_of_code_abstype);
   131 
   132 
   133 (** termifying syntax **)
   134 
   135 fun map_default f xs =
   136   let val ys = map f xs
   137   in if exists is_some ys
   138     then SOME (map2 the_default xs ys)
   139     else NONE
   140   end;
   141 
   142 fun subst_termify_app (Const (@{const_name termify}, _), [t]) =
   143       if not (Term.exists_subterm (fn Abs _ => true | _ => false) t)
   144       then if fold_aterms (fn Const _ => I | _ => K false) t true
   145         then SOME (HOLogic.reflect_term t)
   146         else error "Cannot termify expression containing variable"
   147       else error "Cannot termify expression containing abstraction"
   148   | subst_termify_app (t, ts) = case map_default subst_termify ts
   149      of SOME ts' => SOME (list_comb (t, ts'))
   150       | NONE => NONE
   151 and subst_termify (Abs (v, T, t)) = (case subst_termify t
   152      of SOME t' => SOME (Abs (v, T, t'))
   153       | NONE => NONE)
   154   | subst_termify t = subst_termify_app (strip_comb t) 
   155 
   156 fun check_termify ts = the_default ts (map_default subst_termify ts);
   157 
   158 val _ = Context.>> (Syntax_Phases.term_check 0 "termify" (K check_termify));
   159 
   160 
   161 (** evaluation **)
   162 
   163 structure Evaluation = Proof_Data
   164 (
   165   type T = unit -> term
   166   val empty: T = fn () => raise Fail "Evaluation"
   167   fun init _ = empty
   168 );
   169 val put_term = Evaluation.put;
   170 val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");
   171 
   172 fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
   173 
   174 fun gen_dynamic_value computation ctxt t =
   175   computation cookie ctxt NONE I (mk_term_of t) [];
   176 
   177 val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;
   178 val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
   179 val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
   180 
   181 
   182 (** diagnostic **)
   183 
   184 fun tracing s x = (Output.tracing s; x);
   185 
   186 end;