src/Tools/value.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46961 5c6955f487e5
child 51658 21c10672633b
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37744
3daaf23b9ab4 tuned titles
haftmann
parents: 37146
diff changeset
     1
(*  Title:      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
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28227
diff changeset
     4
Generic value command for arbitrary evaluators.
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
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    10
  val value_select: string -> Proof.context -> term -> term
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    11
  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    12
  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
43612
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    13
  val setup : theory -> theory
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    14
end;
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    15
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    16
structure Value : VALUE =
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    17
struct
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    18
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 31218
diff changeset
    19
structure Evaluator = Theory_Data
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 31218
diff changeset
    20
(
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    21
  type T = (string * (Proof.context -> term -> term)) list;
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    22
  val empty = [];
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    23
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 31218
diff changeset
    24
  fun merge data : T = AList.merge (op =) (K true) data;
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    25
)
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    26
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    27
val add_evaluator = Evaluator.map o AList.update (op =);
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    28
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    29
fun value_select name ctxt =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 37744
diff changeset
    30
  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    31
   of NONE => error ("No such evaluator: " ^ name)
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    32
    | SOME f => f ctxt;
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    33
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 37744
diff changeset
    34
fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    35
  in if null evaluators then error "No evaluators"
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    36
  else let val (evaluators, (_, evaluator)) = split_last evaluators
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    37
    in case get_first (fn (_, f) => try (f ctxt) t) evaluators
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    38
     of SOME t' => t'
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    39
      | NONE => evaluator ctxt t
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    40
  end end;
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    41
43612
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    42
fun value_maybe_select some_name =
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    43
  case some_name
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    44
    of NONE => value
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    45
     | SOME name => value_select name;
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    46
  
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    47
fun value_cmd some_name modes raw_t state =
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    48
  let
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    49
    val ctxt = Toplevel.context_of state;
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    50
    val t = Syntax.read_term ctxt raw_t;
43612
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    51
    val t' = value_maybe_select some_name ctxt t;
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    52
    val ty' = Term.type_of t';
31218
fa54c1e614df fixed typo
haftmann
parents: 29288
diff changeset
    53
    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
    54
    val p = Print_Mode.with_modes modes (fn () =>
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    55
      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    56
        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    57
  in Pretty.writeln p end;
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    58
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 33522
diff changeset
    59
val opt_modes =
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 43619
diff changeset
    60
  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    61
43612
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    62
val opt_evaluator =
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 43619
diff changeset
    63
  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
43612
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    64
  
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 33522
diff changeset
    65
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
    66
  Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
43612
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    67
    (opt_evaluator -- opt_modes -- Parse.term
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 33522
diff changeset
    68
      >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 33522
diff changeset
    69
          (value_cmd some_name modes t)));
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    70
43612
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    71
val antiq_setup =
43619
3803869014aa proper @{binding} antiquotations (relevant for formal references);
wenzelm
parents: 43612
diff changeset
    72
  Thy_Output.antiquotation @{binding value}
43612
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    73
    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    74
    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    75
      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    76
        [style (value_maybe_select some_name context t)]));
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    77
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    78
val setup = antiq_setup;
c32144b8baba adding a value antiquotation
bulwahn
parents: 42361
diff changeset
    79
28227
77221ee0f7b9 generic value command
haftmann
parents:
diff changeset
    80
end;