src/Tools/value.ML

more general prover operations;

(*  Title:      Tools/value.ML
    Author:     Florian Haftmann, TU Muenchen

Generic value command for arbitrary evaluators.
*)

signature VALUE =
sig
  val value: Proof.context -> term -> term
  val value_select: string -> Proof.context -> term -> term
  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
  val setup : theory -> theory
end;

structure Value : VALUE =
struct

structure Evaluator = Theory_Data
(
  type T = (string * (Proof.context -> term -> term)) list;
  val empty = [];
  val extend = I;
  fun merge data : T = AList.merge (op =) (K true) data;
)

val add_evaluator = Evaluator.map o AList.update (op =);

fun value_select name ctxt =
  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
   of NONE => error ("No such evaluator: " ^ name)
    | SOME f => f ctxt;

fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
  in if null evaluators then error "No evaluators"
  else let val (evaluators, (_, evaluator)) = split_last evaluators
    in case get_first (fn (_, f) => try (f ctxt) t) evaluators
     of SOME t' => t'
      | NONE => evaluator ctxt t
  end end;

fun value_maybe_select some_name =
  case some_name
    of NONE => value
     | SOME name => value_select name;
  
fun value_cmd some_name modes raw_t state =
  let
    val ctxt = Toplevel.context_of state;
    val t = Syntax.read_term ctxt raw_t;
    val t' = value_maybe_select some_name ctxt t;
    val ty' = Term.type_of t';
    val ctxt' = Variable.auto_fixes t' ctxt;
    val p = Print_Mode.with_modes modes (fn () =>
      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
  in Pretty.writeln p end;

val opt_modes =
  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];

val opt_evaluator =
  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
  
val _ =
  Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
    (opt_evaluator -- opt_modes -- Parse.term
      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));

val antiq_setup =
  Thy_Output.antiquotation @{binding value}
    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
        [style (value_maybe_select some_name context t)]));

val setup = antiq_setup;

end;