src/Tools/value.ML
author traytel
Thu Sep 29 09:37:59 2011 +0200 (2011-09-29)
changeset 45102 7bb89635eb51
parent 43619 3803869014aa
child 46949 94aa7b81bcf6
permissions -rw-r--r--
correct coercion generation in case of unknown map functions
     1 (*  Title:      Tools/value.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Generic value command for arbitrary evaluators.
     5 *)
     6 
     7 signature VALUE =
     8 sig
     9   val value: Proof.context -> term -> term
    10   val value_select: string -> Proof.context -> term -> term
    11   val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
    12   val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
    13   val setup : theory -> theory
    14 end;
    15 
    16 structure Value : VALUE =
    17 struct
    18 
    19 structure Evaluator = Theory_Data
    20 (
    21   type T = (string * (Proof.context -> term -> term)) list;
    22   val empty = [];
    23   val extend = I;
    24   fun merge data : T = AList.merge (op =) (K true) data;
    25 )
    26 
    27 val add_evaluator = Evaluator.map o AList.update (op =);
    28 
    29 fun value_select name ctxt =
    30   case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
    31    of NONE => error ("No such evaluator: " ^ name)
    32     | SOME f => f ctxt;
    33 
    34 fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
    35   in if null evaluators then error "No evaluators"
    36   else let val (evaluators, (_, evaluator)) = split_last evaluators
    37     in case get_first (fn (_, f) => try (f ctxt) t) evaluators
    38      of SOME t' => t'
    39       | NONE => evaluator ctxt t
    40   end end;
    41 
    42 fun value_maybe_select some_name =
    43   case some_name
    44     of NONE => value
    45      | SOME name => value_select name;
    46   
    47 fun value_cmd some_name modes raw_t state =
    48   let
    49     val ctxt = Toplevel.context_of state;
    50     val t = Syntax.read_term ctxt raw_t;
    51     val t' = value_maybe_select some_name ctxt t;
    52     val ty' = Term.type_of t';
    53     val ctxt' = Variable.auto_fixes t' ctxt;
    54     val p = Print_Mode.with_modes modes (fn () =>
    55       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    56         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    57   in Pretty.writeln p end;
    58 
    59 val opt_modes =
    60   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
    61 
    62 val opt_evaluator =
    63   Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]")
    64   
    65 val _ =
    66   Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
    67     (opt_evaluator -- opt_modes -- Parse.term
    68       >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
    69           (value_cmd some_name modes t)));
    70 
    71 val antiq_setup =
    72   Thy_Output.antiquotation @{binding value}
    73     (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    74     (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
    75       (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
    76         [style (value_maybe_select some_name context t)]));
    77 
    78 val setup = antiq_setup;
    79 
    80 end;