src/HOL/Tools/code_evaluation.ML

Factored out ML into separate file

(*  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;