--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/code_evaluation.ML Mon Sep 20 15:10:21 2010 +0200
@@ -0,0 +1,174 @@
+(* Title: HOL/Tools/code_evaluation.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Evaluation and reconstruction of terms in ML.
+*)
+
+signature CODE_EVALUATION =
+sig
+ val dynamic_value_strict: theory -> term -> term
+ val put_term: (unit -> term) -> Proof.context -> Proof.context
+ val tracing: string -> 'a -> 'a
+ val setup: theory -> theory
+end;
+
+structure Code_Evaluation : CODE_EVALUATION =
+struct
+
+(** term_of instances **)
+
+(* formal definition *)
+
+fun add_term_of tyco raw_vs thy =
+ let
+ val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
+ val ty = Type (tyco, map TFree vs);
+ val lhs = Const (@{const_name term_of}, ty --> @{typ term})
+ $ Free ("x", ty);
+ val rhs = @{term "undefined :: term"};
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+ fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
+ o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
+ in
+ thy
+ |> Class.instantiation ([tyco], vs, @{sort term_of})
+ |> `(fn lthy => Syntax.check_term lthy eq)
+ |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
+ |> snd
+ |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+ end;
+
+fun ensure_term_of (tyco, (raw_vs, _)) thy =
+ let
+ val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
+ andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
+ in if need_inst then add_term_of tyco raw_vs thy else thy end;
+
+
+(* code equations for datatypes *)
+
+fun mk_term_of_eq thy ty vs tyco (c, tys) =
+ let
+ val t = list_comb (Const (c, tys ---> ty),
+ map Free (Name.names Name.context "a" tys));
+ val (arg, rhs) =
+ pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
+ (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
+ val cty = Thm.ctyp_of thy ty;
+ in
+ @{thm term_of_anything}
+ |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
+ |> Thm.varifyT_global
+ end;
+
+fun add_term_of_code tyco raw_vs raw_cs thy =
+ let
+ val algebra = Sign.classes_of thy;
+ val vs = map (fn (v, sort) =>
+ (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
+ val ty = Type (tyco, map TFree vs);
+ val cs = (map o apsnd o map o map_atyps)
+ (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
+ val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+ val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
+ in
+ thy
+ |> Code.del_eqns const
+ |> fold Code.add_eqn eqs
+ end;
+
+fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
+ let
+ val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
+ in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
+
+
+(* code equations for abstypes *)
+
+fun mk_abs_term_of_eq thy ty vs tyco abs ty_rep proj =
+ let
+ val arg = Var (("x", 0), ty);
+ val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
+ (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
+ |> Thm.cterm_of thy;
+ val cty = Thm.ctyp_of thy ty;
+ in
+ @{thm term_of_anything}
+ |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
+ |> Thm.varifyT_global
+ end;
+
+fun add_abs_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
+ let
+ val algebra = Sign.classes_of thy;
+ val vs = map (fn (v, sort) =>
+ (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
+ val ty = Type (tyco, map TFree vs);
+ val ty_rep = map_atyps
+ (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
+ val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+ val eq = mk_abs_term_of_eq thy ty vs tyco abs ty_rep proj;
+ in
+ thy
+ |> Code.del_eqns const
+ |> Code.add_eqn eq
+ end;
+
+fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
+ let
+ val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
+ in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
+
+
+(** termifying syntax **)
+
+fun map_default f xs =
+ let val ys = map f xs
+ in if exists is_some ys
+ then SOME (map2 the_default xs ys)
+ else NONE
+ end;
+
+fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
+ if not (Term.has_abs t)
+ then if fold_aterms (fn Const _ => I | _ => K false) t true
+ then SOME (HOLogic.reflect_term t)
+ else error "Cannot termify expression containing variables"
+ else error "Cannot termify expression containing abstraction"
+ | subst_termify_app (t, ts) = case map_default subst_termify ts
+ of SOME ts' => SOME (list_comb (t, ts'))
+ | NONE => NONE
+and subst_termify (Abs (v, T, t)) = (case subst_termify t
+ of SOME t' => SOME (Abs (v, T, t'))
+ | NONE => NONE)
+ | subst_termify t = subst_termify_app (strip_comb t)
+
+fun check_termify ts ctxt = map_default subst_termify ts
+ |> Option.map (rpair ctxt)
+
+
+(** evaluation **)
+
+structure Evaluation = Proof_Data (
+ type T = unit -> term
+ fun init _ () = error "Evaluation"
+);
+val put_term = Evaluation.put;
+
+fun tracing s x = (Output.tracing s; x);
+
+fun dynamic_value_strict thy t = Code_Runtime.dynamic_value_strict (Evaluation.get, put_term, "Code_Evaluation.put_term")
+ thy NONE I (HOLogic.mk_term_of (fastype_of t) t) [];
+
+
+(** setup **)
+
+val setup =
+ Code.datatype_interpretation ensure_term_of
+ #> Code.abstype_interpretation ensure_term_of
+ #> Code.datatype_interpretation ensure_term_of_code
+ #> Code.abstype_interpretation ensure_abs_term_of_code
+ #> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
+ #> Value.add_evaluator ("code", dynamic_value_strict o ProofContext.theory_of);
+
+end;