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