src/HOL/Tools/value.ML
author wenzelm
Mon, 03 Nov 2014 14:50:27 +0100
changeset 58893 9e0ecb66d6a7
parent 58100 f54a8a4134d3
child 59323 468bd3aedfa1
permissions -rw-r--r--
eliminated unused int_only flag (see also c12484a27367); just proper commands;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56927
4044a7d1720f hardcoded nbe and sml into value command
haftmann
parents: 56926
diff changeset
     1
(*  Title:      HOL/Tools/value.ML
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
     3
58100
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
     4
Generic value command for arbitrary evaluators, with default using nbe or SML.
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
     5
*)
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
     6
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
     7
signature VALUE =
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
     8
sig
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
     9
  val value: Proof.context -> term -> term
58100
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    10
  val value_select: string -> Proof.context -> term -> term
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    11
  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    12
  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    13
end;
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    14
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    15
structure Value : VALUE =
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    16
struct
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    17
58100
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    18
fun default_value ctxt t =
56927
4044a7d1720f hardcoded nbe and sml into value command
haftmann
parents: 56926
diff changeset
    19
  if null (Term.add_frees t [])
4044a7d1720f hardcoded nbe and sml into value command
haftmann
parents: 56926
diff changeset
    20
  then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
4044a7d1720f hardcoded nbe and sml into value command
haftmann
parents: 56926
diff changeset
    21
    SOME t' => t'
4044a7d1720f hardcoded nbe and sml into value command
haftmann
parents: 56926
diff changeset
    22
  | NONE => Nbe.dynamic_value ctxt t
4044a7d1720f hardcoded nbe and sml into value command
haftmann
parents: 56926
diff changeset
    23
  else Nbe.dynamic_value ctxt t;
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    24
58100
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    25
structure Evaluator = Theory_Data
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    26
(
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    27
  type T = (string * (Proof.context -> term -> term)) list;
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    28
  val empty = [("default", default_value)];
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    29
  val extend = I;
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    30
  fun merge data : T = AList.merge (op =) (K true) data;
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    31
)
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    32
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    33
val add_evaluator = Evaluator.map o AList.update (op =);
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    34
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    35
fun value_select name ctxt =
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    36
  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    37
   of NONE => error ("No such evaluator: " ^ name)
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    38
    | SOME f => f ctxt;
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    39
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    40
fun value ctxt =
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    41
  let
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    42
    val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    43
  in
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    44
    if null evaluators
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    45
    then error "No evaluators"
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    46
    else (snd o snd o split_last) evaluators ctxt
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    47
  end;
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    48
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    49
fun value_maybe_select some_name =
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    50
  case some_name
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    51
    of NONE => value
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    52
     | SOME name => value_select name;
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    53
  
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    54
fun value_cmd some_name modes raw_t state =
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    55
  let
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    56
    val ctxt = Toplevel.context_of state;
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    57
    val t = Syntax.read_term ctxt raw_t;
58100
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    58
    val t' = value_maybe_select some_name ctxt t;
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    59
    val ty' = Term.type_of t';
31218
fa54c1e614df fixed typo
haftmann
parents: 29288
diff changeset
    60
    val ctxt' = Variable.auto_fixes t' ctxt;
37146
f652333bbf8e renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents: 36960
diff changeset
    61
    val p = Print_Mode.with_modes modes (fn () =>
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    62
      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    63
        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    64
  in Pretty.writeln p end;
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    65
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 33522
diff changeset
    66
val opt_modes =
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 43619
diff changeset
    67
  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    68
58100
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    69
val opt_evaluator =
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    70
  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    71
  
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 33522
diff changeset
    72
val _ =
58893
9e0ecb66d6a7 eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents: 58100
diff changeset
    73
  Outer_Syntax.command @{command_spec "value"} "evaluate and print term"
58100
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    74
    (opt_evaluator -- opt_modes -- Parse.term
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    75
      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    76
56926
aaea99edc040 modernized setups
haftmann
parents: 56925
diff changeset
    77
val _ = Context.>> (Context.map_theory
aaea99edc040 modernized setups
haftmann
parents: 56925
diff changeset
    78
  (Thy_Output.antiquotation @{binding value}
58100
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    79
    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    80
    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
43612
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    81
      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
58100
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    82
        [style (value_maybe_select some_name context t)]))
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    83
  #> add_evaluator ("simp", Code_Simp.dynamic_value)
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    84
  #> add_evaluator ("nbe", Nbe.dynamic_value)
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    85
  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict))
f54a8a4134d3 restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents: 56975
diff changeset
    86
);
43612
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    87
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    88
end;