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