generic value command
authorhaftmann
Tue Sep 16 09:21:22 2008 +0200 (2008-09-16)
changeset 2822777221ee0f7b9
parent 28226 97c530dc8aca
child 28228 7ebe8dc06cbb
generic value command
NEWS
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/ex/Eval_Examples.thy
src/Pure/IsaMakefile
src/Pure/Tools/ROOT.ML
src/Pure/Tools/value.ML
src/Pure/codegen.ML
src/Tools/nbe.ML
     1.1 --- a/NEWS	Mon Sep 15 20:51:58 2008 +0200
     1.2 +++ b/NEWS	Tue Sep 16 09:21:22 2008 +0200
     1.3 @@ -63,6 +63,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOL/Main: command "value" now integrates different evaluation mechanisms.
     1.8 +The result of the first successful evaluation mechanism is printed.
     1.9 +In square brackets a particular named evaluation mechanisms may be specified
    1.10 +(currently, [SML], [code] or [nbe]).  See further HOL/ex/Eval_Examples.thy.
    1.11 +
    1.12  * HOL/Orderings: class "wellorder" moved here, with explicit induction
    1.13  rule "less_induct" as assumption.  For instantiation of "wellorder" by
    1.14  means of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.
     2.1 --- a/src/HOL/HOL.thy	Mon Sep 15 20:51:58 2008 +0200
     2.2 +++ b/src/HOL/HOL.thy	Tue Sep 16 09:21:22 2008 +0200
     2.3 @@ -1711,6 +1711,7 @@
     2.4    #> Code_ML.setup
     2.5    #> Code_Haskell.setup
     2.6    #> Nbe.setup
     2.7 +  #> Codegen.setup
     2.8  *}
     2.9  
    2.10  lemma [code func]:
     3.1 --- a/src/HOL/IsaMakefile	Mon Sep 15 20:51:58 2008 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Tue Sep 16 09:21:22 2008 +0200
     3.3 @@ -184,6 +184,7 @@
     3.4    ROOT.ML \
     3.5    Arith_Tools.thy \
     3.6    ATP_Linkup.thy \
     3.7 +  Code_Eval.thy \
     3.8    Complex/Complex_Main.thy \
     3.9    Complex/Complex.thy \
    3.10    Complex/Fundamental_Theorem_Algebra.thy \
    3.11 @@ -210,6 +211,7 @@
    3.12    Library/GCD.thy \
    3.13    Library/Order_Relation.thy \
    3.14    Library/Parity.thy \
    3.15 +  Library/RType.thy \
    3.16    Library/Univ_Poly.thy \
    3.17    List.thy \
    3.18    Main.thy \
    3.19 @@ -301,7 +303,7 @@
    3.20    Library/List_lexord.thy Library/Commutative_Ring.thy			\
    3.21    Library/comm_ring.ML Library/Coinductive_List.thy			\
    3.22    Library/AssocList.thy		\
    3.23 -  Library/Binomial.thy Library/Eval.thy Library/Eval_Witness.thy	\
    3.24 +  Library/Binomial.thy Library/Eval_Witness.thy	\
    3.25    Library/Code_Index.thy Library/Code_Char.thy				\
    3.26    Library/Code_Char_chr.thy Library/Code_Integer.thy			\
    3.27    Library/Code_Message.thy			\
     4.1 --- a/src/HOL/ex/Eval_Examples.thy	Mon Sep 15 20:51:58 2008 +0200
     4.2 +++ b/src/HOL/ex/Eval_Examples.thy	Tue Sep 16 09:21:22 2008 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Small examples for evaluation mechanisms *}
     4.5  
     4.6  theory Eval_Examples
     4.7 -imports Eval "~~/src/HOL/Real/Rational"
     4.8 +imports Code_Eval "~~/src/HOL/Real/Rational"
     4.9  begin
    4.10  
    4.11  text {* evaluation oracle *}
    4.12 @@ -35,44 +35,44 @@
    4.13  text {* term evaluation *}
    4.14  
    4.15  value "(Suc 2 + 1) * 4"
    4.16 -value (code) "(Suc 2 + 1) * 4"
    4.17 -value (SML) "(Suc 2 + 1) * 4"
    4.18 -value ("normal_form") "(Suc 2 + 1) * 4"
    4.19 +value [code] "(Suc 2 + 1) * 4"
    4.20 +value [SML] "(Suc 2 + 1) * 4"
    4.21 +value [nbe] "(Suc 2 + 1) * 4"
    4.22  
    4.23  value "(Suc 2 + Suc 0) * Suc 3"
    4.24 -value (code) "(Suc 2 + Suc 0) * Suc 3"
    4.25 -value (SML) "(Suc 2 + Suc 0) * Suc 3"
    4.26 -value ("normal_form") "(Suc 2 + Suc 0) * Suc 3"
    4.27 +value [code] "(Suc 2 + Suc 0) * Suc 3"
    4.28 +value [SML] "(Suc 2 + Suc 0) * Suc 3"
    4.29 +value [nbe] "(Suc 2 + Suc 0) * Suc 3"
    4.30  
    4.31  value "nat 100"
    4.32 -value (code) "nat 100"
    4.33 -value (SML) "nat 100"
    4.34 -value ("normal_form") "nat 100"
    4.35 +value [code] "nat 100"
    4.36 +value [SML] "nat 100"
    4.37 +value [nbe] "nat 100"
    4.38  
    4.39  value "(10\<Colon>int) \<le> 12"
    4.40 -value (code) "(10\<Colon>int) \<le> 12"
    4.41 -value (SML) "(10\<Colon>int) \<le> 12"
    4.42 -value ("normal_form") "(10\<Colon>int) \<le> 12"
    4.43 +value [code] "(10\<Colon>int) \<le> 12"
    4.44 +value [SML] "(10\<Colon>int) \<le> 12"
    4.45 +value [nbe] "(10\<Colon>int) \<le> 12"
    4.46  
    4.47  value "max (2::int) 4"
    4.48 -value (code) "max (2::int) 4"
    4.49 -value (SML) "max (2::int) 4"
    4.50 -value ("normal_form") "max (2::int) 4"
    4.51 +value [code] "max (2::int) 4"
    4.52 +value [SML] "max (2::int) 4"
    4.53 +value [nbe] "max (2::int) 4"
    4.54  
    4.55  value "of_int 2 / of_int 4 * (1::rat)"
    4.56 -value (code) "of_int 2 / of_int 4 * (1::rat)"
    4.57 -value (SML) "of_int 2 / of_int 4 * (1::rat)"
    4.58 -value ("normal_form") "of_int 2 / of_int 4 * (1::rat)"
    4.59 +value [code] "of_int 2 / of_int 4 * (1::rat)"
    4.60 +value [SML] "of_int 2 / of_int 4 * (1::rat)"
    4.61 +value [nbe] "of_int 2 / of_int 4 * (1::rat)"
    4.62  
    4.63  value "[]::nat list"
    4.64 -value (code) "[]::nat list"
    4.65 -value (SML) "[]::nat list"
    4.66 -value ("normal_form") "[]::nat list"
    4.67 +value [code] "[]::nat list"
    4.68 +value [SML] "[]::nat list"
    4.69 +value [nbe] "[]::nat list"
    4.70  
    4.71  value "[(nat 100, ())]"
    4.72 -value (code) "[(nat 100, ())]"
    4.73 -value (SML) "[(nat 100, ())]"
    4.74 -value ("normal_form") "[(nat 100, ())]"
    4.75 +value [code] "[(nat 100, ())]"
    4.76 +value [SML] "[(nat 100, ())]"
    4.77 +value [nbe] "[(nat 100, ())]"
    4.78  
    4.79  
    4.80  text {* a fancy datatype *}
    4.81 @@ -85,8 +85,8 @@
    4.82      Cair 'a 'b
    4.83  
    4.84  value "Shift (Cair (4::nat) [Suc 0])"
    4.85 -value (code) "Shift (Cair (4::nat) [Suc 0])"
    4.86 -value (SML) "Shift (Cair (4::nat) [Suc 0])"
    4.87 -value ("normal_form") "Shift (Cair (4::nat) [Suc 0])"
    4.88 +value [code] "Shift (Cair (4::nat) [Suc 0])"
    4.89 +value [SML] "Shift (Cair (4::nat) [Suc 0])"
    4.90 +value [nbe] "Shift (Cair (4::nat) [Suc 0])"
    4.91  
    4.92  end
     5.1 --- a/src/Pure/IsaMakefile	Mon Sep 15 20:51:58 2008 +0200
     5.2 +++ b/src/Pure/IsaMakefile	Tue Sep 16 09:21:22 2008 +0200
     5.3 @@ -72,7 +72,7 @@
     5.4    Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML	\
     5.5    Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML		\
     5.6    Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML	\
     5.7 -  Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML			\
     5.8 +  Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML Tools/value.ML	\
     5.9    Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML	\
    5.10    assumption.ML axclass.ML codegen.ML config.ML conjunction.ML		\
    5.11    consts.ML context.ML conv.ML defs.ML display.ML drule.ML envir.ML	\
     6.1 --- a/src/Pure/Tools/ROOT.ML	Mon Sep 15 20:51:58 2008 +0200
     6.2 +++ b/src/Pure/Tools/ROOT.ML	Tue Sep 16 09:21:22 2008 +0200
     6.3 @@ -4,6 +4,7 @@
     6.4  Miscellaneous tools and packages for Pure Isabelle.
     6.5  *)
     6.6  
     6.7 +use "value.ML";
     6.8  use "named_thms.ML";
     6.9  use "isabelle_process.ML";
    6.10  
    6.11 @@ -12,4 +13,3 @@
    6.12  
    6.13  (*derived theory and proof elements*)
    6.14  use "invoke.ML";
    6.15 -
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/Tools/value.ML	Tue Sep 16 09:21:22 2008 +0200
     7.3 @@ -0,0 +1,67 @@
     7.4 +(*  Title:      Pure/Tools/value.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Florian Haftmann, TU Muenchen
     7.7 +
     7.8 +Value command for different evaluators.
     7.9 +*)
    7.10 +
    7.11 +signature VALUE =
    7.12 +sig
    7.13 +  val value: Proof.context -> term -> term
    7.14 +  val value_select: string -> Proof.context -> term -> term
    7.15 +  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
    7.16 +  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
    7.17 +end;
    7.18 +
    7.19 +structure Value : VALUE =
    7.20 +struct
    7.21 +
    7.22 +structure Evaluator = TheoryDataFun(
    7.23 +  type T = (string * (Proof.context -> term -> term)) list;
    7.24 +  val empty = [];
    7.25 +  val copy = I;
    7.26 +  val extend = I;
    7.27 +  fun merge pp = AList.merge (op =) (K true);
    7.28 +)
    7.29 +
    7.30 +val add_evaluator = Evaluator.map o AList.update (op =);
    7.31 +
    7.32 +fun value_select name ctxt =
    7.33 +  case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name
    7.34 +   of NONE => error ("No such evaluator: " ^ name)
    7.35 +    | SOME f => f ctxt;
    7.36 +
    7.37 +fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.theory_of ctxt)
    7.38 +  in if null evaluators then error "No evaluators"
    7.39 +  else let val (evaluators, (_, evaluator)) = split_last evaluators
    7.40 +    in case get_first (fn (_, f) => try (f ctxt) t) evaluators
    7.41 +     of SOME t' => t'
    7.42 +      | NONE => evaluator ctxt t
    7.43 +  end end;
    7.44 +
    7.45 +fun value_cmd some_name modes raw_t state =
    7.46 +  let
    7.47 +    val ctxt = Toplevel.context_of state;
    7.48 +    val t = Syntax.read_term ctxt raw_t;
    7.49 +    val t' = case some_name
    7.50 +     of NONE => value ctxt t
    7.51 +      | SOME name => value_select name ctxt t;
    7.52 +    val ty' = Term.type_of t';
    7.53 +    val ctxt' = Variable.auto_fixes t ctxt;
    7.54 +    val p = PrintMode.with_modes modes (fn () =>
    7.55 +      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    7.56 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    7.57 +  in Pretty.writeln p end;
    7.58 +
    7.59 +local structure P = OuterParse and K = OuterKeyword in
    7.60 +
    7.61 +val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
    7.62 +
    7.63 +val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
    7.64 +  (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
    7.65 +    >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
    7.66 +        (value_cmd some_name modes t)));
    7.67 +
    7.68 +end; (*local*)
    7.69 +
    7.70 +end;
     8.1 --- a/src/Pure/codegen.ML	Mon Sep 15 20:51:58 2008 +0200
     8.2 +++ b/src/Pure/codegen.ML	Tue Sep 16 09:21:22 2008 +0200
     8.3 @@ -96,6 +96,8 @@
     8.4    val del_nodes: string list -> codegr -> codegr
     8.5    val map_node: string -> (node -> node) -> codegr -> codegr
     8.6    val new_node: string * node -> codegr -> codegr
     8.7 +
     8.8 +  val setup: theory -> theory
     8.9  end;
    8.10  
    8.11  structure Codegen : CODEGEN =
    8.12 @@ -154,7 +156,7 @@
    8.13  
    8.14  type nametab = (string * string) Symtab.table * unit Symtab.table;
    8.15  
    8.16 -fun merge_nametabs ((tab, used), (tab', used')) =
    8.17 +fun merge_nametabs ((tab, used) : nametab, (tab', used')) =
    8.18    (Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used'));
    8.19  
    8.20  type node =
    8.21 @@ -232,7 +234,7 @@
    8.22    fun merge _
    8.23      ({codegens = codegens1, tycodegens = tycodegens1,
    8.24        consts = consts1, types = types1,
    8.25 -      preprocs = preprocs1, modules = modules1, test_params = test_params1},
    8.26 +      preprocs = preprocs1, modules = modules1, test_params = test_params1} : T,
    8.27       {codegens = codegens2, tycodegens = tycodegens2,
    8.28        consts = consts2, types = types2,
    8.29        preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
    8.30 @@ -347,14 +349,6 @@
    8.31        end)
    8.32    in add_preprocessor prep end;
    8.33  
    8.34 -val _ = Context.>>
    8.35 -  (let
    8.36 -    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    8.37 -  in
    8.38 -    Context.map_theory (Code.add_attribute ("unfold", Scan.succeed (mk_attribute
    8.39 -      (fn thm => add_unfold thm #> Code.add_inline thm))))
    8.40 -  end);
    8.41 -
    8.42  
    8.43  (**** associate constants with target language code ****)
    8.44  
    8.45 @@ -784,11 +778,6 @@
    8.46                   (add_edge (node_id, dep) gr'', p module''))
    8.47             end);
    8.48  
    8.49 -val _ = Context.>> (Context.map_theory
    8.50 - (add_codegen "default" default_codegen #>
    8.51 -  add_tycodegen "default" default_tycodegen));
    8.52 -
    8.53 -
    8.54  fun mk_tuple [p] = p
    8.55    | mk_tuple ps = Pretty.block (str "(" ::
    8.56        List.concat (separate [str ",", Pretty.brk 1] (map single ps)) @
    8.57 @@ -804,7 +793,7 @@
    8.58  
    8.59  fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
    8.60  
    8.61 -fun add_to_module name s = AList.map_entry (op =) name (suffix s);
    8.62 +fun add_to_module name s = AList.map_entry (op =) (name : string) (suffix s);
    8.63  
    8.64  fun output_code gr module xs =
    8.65    let
    8.66 @@ -1023,8 +1012,6 @@
    8.67      else state
    8.68    end;
    8.69  
    8.70 -val _ = Context.>> (Specification.add_theorem_hook test_goal');
    8.71 -
    8.72  
    8.73  (**** Evaluator for terms ****)
    8.74  
    8.75 @@ -1053,18 +1040,6 @@
    8.76      in !eval_result end;
    8.77    in e () end;
    8.78  
    8.79 -fun print_evaluated_term s = Toplevel.keep (fn state =>
    8.80 -  let
    8.81 -    val ctxt = Toplevel.context_of state;
    8.82 -    val thy = ProofContext.theory_of ctxt;
    8.83 -    val t = eval_term thy (Syntax.read_term ctxt s);
    8.84 -    val T = Term.type_of t;
    8.85 -  in
    8.86 -    Pretty.writeln
    8.87 -      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
    8.88 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
    8.89 -  end);
    8.90 -
    8.91  exception Evaluation of term;
    8.92  
    8.93  fun evaluation_oracle (thy, Evaluation t) =
    8.94 @@ -1072,10 +1047,7 @@
    8.95  
    8.96  fun evaluation_conv ct =
    8.97    let val thy = Thm.theory_of_cterm ct
    8.98 -  in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation (Thm.term_of ct)) end;
    8.99 -
   8.100 -val _ = Context.>> (Context.map_theory
   8.101 -  (Theory.add_oracle ("evaluation", evaluation_oracle)));
   8.102 +  in Thm.invoke_oracle_i thy "HOL.evaluation" (thy, Evaluation (Thm.term_of ct)) end;
   8.103  
   8.104  
   8.105  (**** Interface ****)
   8.106 @@ -1156,6 +1128,15 @@
   8.107             else map_modules (Symtab.update (module, gr)) thy)
   8.108       end));
   8.109  
   8.110 +val setup = add_codegen "default" default_codegen
   8.111 +  #> add_tycodegen "default" default_tycodegen
   8.112 +  #> Theory.add_oracle ("evaluation", evaluation_oracle)
   8.113 +  #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of)
   8.114 +  #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
   8.115 +       (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)));
   8.116 +
   8.117 +val _ = Context.>> (Specification.add_theorem_hook test_goal');
   8.118 +
   8.119  val _ =
   8.120    OuterSyntax.command "code_library"
   8.121      "generates code for terms (one structure for each theory)" K.thy_decl
   8.122 @@ -1195,10 +1176,6 @@
   8.123          (get_test_params (Toplevel.theory_of st), [])) g [] |>
   8.124        pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
   8.125  
   8.126 -val _ =
   8.127 -  OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
   8.128 -    (P.term >> (Toplevel.no_timing oo print_evaluated_term));
   8.129 -
   8.130  end;
   8.131  
   8.132  val auto_quickcheck = Codegen.auto_quickcheck;
     9.1 --- a/src/Tools/nbe.ML	Mon Sep 15 20:51:58 2008 +0200
     9.2 +++ b/src/Tools/nbe.ML	Tue Sep 16 09:21:22 2008 +0200
     9.3 @@ -454,7 +454,8 @@
     9.4    let val ctxt = Toplevel.context_of state
     9.5    in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
     9.6  
     9.7 -val setup = Theory.add_oracle ("norm", norm_oracle);
     9.8 +val setup = Theory.add_oracle ("norm", norm_oracle)
     9.9 +  #> Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
    9.10  
    9.11  local structure P = OuterParse and K = OuterKeyword in
    9.12  
    9.13 @@ -462,7 +463,7 @@
    9.14  
    9.15  val _ =
    9.16    OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
    9.17 -    (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd));
    9.18 +    (opt_modes -- P.term >> (Toplevel.keep o norm_print_term_cmd));
    9.19  
    9.20  end;
    9.21