degeneralized value command into HOL
authorhaftmann
Fri May 09 08:13:36 2014 +0200 (2014-05-09)
changeset 56925601edd9a6859
parent 56924 2f94c9a50f06
child 56926 aaea99edc040
degeneralized value command into HOL
src/HOL/Code_Evaluation.thy
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/value.ML
src/Tools/Code_Generator.thy
src/Tools/nbe.ML
src/Tools/value.ML
     1.1 --- a/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:36 2014 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:36 2014 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  theory Code_Evaluation
     1.6  imports Typerep Limited_Sequence
     1.7 +keywords "value" :: diag
     1.8  begin
     1.9  
    1.10  subsection {* Term representation *}
    1.11 @@ -162,6 +163,17 @@
    1.12    constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing"
    1.13  
    1.14  
    1.15 +subsection {* Interactive evaluation *}
    1.16 +
    1.17 +ML_file "~~/src/HOL/Tools/value.ML"
    1.18 +
    1.19 +setup {*
    1.20 +  Value.setup
    1.21 +  #> Value.add_evaluator ("nbe", Nbe.dynamic_value)
    1.22 +  #> Value.add_evaluator ("code", Code_Evaluation.dynamic_value_strict)
    1.23 +*}
    1.24 +
    1.25 +
    1.26  subsection {* Generic reification *}
    1.27  
    1.28  ML_file "~~/src/HOL/Tools/reification.ML"
     2.1 --- a/src/HOL/Tools/code_evaluation.ML	Fri May 09 08:13:36 2014 +0200
     2.2 +++ b/src/HOL/Tools/code_evaluation.ML	Fri May 09 08:13:36 2014 +0200
     2.3 @@ -228,7 +228,6 @@
     2.4    #> Code.abstype_interpretation ensure_term_of
     2.5    #> Code.datatype_interpretation ensure_term_of_code
     2.6    #> Code.abstype_interpretation ensure_abs_term_of_code
     2.7 -  #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify)
     2.8 -  #> Value.add_evaluator ("code", dynamic_value_strict);
     2.9 +  #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify);
    2.10  
    2.11  end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/value.ML	Fri May 09 08:13:36 2014 +0200
     3.3 @@ -0,0 +1,79 @@
     3.4 +(*  Title:      Tools/value.ML
     3.5 +    Author:     Florian Haftmann, TU Muenchen
     3.6 +
     3.7 +Generic value command for arbitrary evaluators.
     3.8 +*)
     3.9 +
    3.10 +signature VALUE =
    3.11 +sig
    3.12 +  val value: Proof.context -> term -> term
    3.13 +  val value_select: string -> Proof.context -> term -> term
    3.14 +  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
    3.15 +  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
    3.16 +  val setup : theory -> theory
    3.17 +end;
    3.18 +
    3.19 +structure Value : VALUE =
    3.20 +struct
    3.21 +
    3.22 +structure Evaluator = Theory_Data
    3.23 +(
    3.24 +  type T = (string * (Proof.context -> term -> term)) list;
    3.25 +  val empty = [];
    3.26 +  val extend = I;
    3.27 +  fun merge data : T = AList.merge (op =) (K true) data;
    3.28 +)
    3.29 +
    3.30 +val add_evaluator = Evaluator.map o AList.update (op =);
    3.31 +
    3.32 +fun value_select name ctxt =
    3.33 +  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
    3.34 +   of NONE => error ("No such evaluator: " ^ name)
    3.35 +    | SOME f => f ctxt;
    3.36 +
    3.37 +fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
    3.38 +  in if null evaluators then error "No evaluators"
    3.39 +  else let val (evaluators, (_, evaluator)) = split_last evaluators
    3.40 +    in case get_first (fn (_, f) => try (f ctxt) t) evaluators
    3.41 +     of SOME t' => t'
    3.42 +      | NONE => evaluator ctxt t
    3.43 +  end end;
    3.44 +
    3.45 +fun value_maybe_select some_name =
    3.46 +  case some_name
    3.47 +    of NONE => value
    3.48 +     | SOME name => value_select name;
    3.49 +  
    3.50 +fun value_cmd some_name modes raw_t state =
    3.51 +  let
    3.52 +    val ctxt = Toplevel.context_of state;
    3.53 +    val t = Syntax.read_term ctxt raw_t;
    3.54 +    val t' = value_maybe_select some_name ctxt t;
    3.55 +    val ty' = Term.type_of t';
    3.56 +    val ctxt' = Variable.auto_fixes t' ctxt;
    3.57 +    val p = Print_Mode.with_modes modes (fn () =>
    3.58 +      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    3.59 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    3.60 +  in Pretty.writeln p end;
    3.61 +
    3.62 +val opt_modes =
    3.63 +  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
    3.64 +
    3.65 +val opt_evaluator =
    3.66 +  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
    3.67 +  
    3.68 +val _ =
    3.69 +  Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
    3.70 +    (opt_evaluator -- opt_modes -- Parse.term
    3.71 +      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
    3.72 +
    3.73 +val antiq_setup =
    3.74 +  Thy_Output.antiquotation @{binding value}
    3.75 +    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    3.76 +    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
    3.77 +      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
    3.78 +        [style (value_maybe_select some_name context t)]));
    3.79 +
    3.80 +val setup = antiq_setup;
    3.81 +
    3.82 +end;
     4.1 --- a/src/Tools/Code_Generator.thy	Fri May 09 08:13:36 2014 +0200
     4.2 +++ b/src/Tools/Code_Generator.thy	Fri May 09 08:13:36 2014 +0200
     4.3 @@ -7,14 +7,13 @@
     4.4  theory Code_Generator
     4.5  imports Pure
     4.6  keywords
     4.7 -  "value" "print_codeproc" "code_thms" "code_deps" :: diag and
     4.8 +  "print_codeproc" "code_thms" "code_deps" :: diag and
     4.9    "export_code" "code_identifier" "code_printing" "code_reserved"
    4.10      "code_monad" "code_reflect" :: thy_decl and
    4.11    "datatypes" "functions" "module_name" "file" "checking"
    4.12    "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
    4.13  begin
    4.14  
    4.15 -ML_file "~~/src/Tools/value.ML"
    4.16  ML_file "~~/src/Tools/cache_io.ML"
    4.17  ML_file "~~/src/Tools/Code/code_preproc.ML"
    4.18  ML_file "~~/src/Tools/Code/code_symbol.ML"
    4.19 @@ -28,8 +27,7 @@
    4.20  ML_file "~~/src/Tools/Code/code_scala.ML"
    4.21  
    4.22  setup {*
    4.23 -  Value.setup
    4.24 -  #> Code_Preproc.setup
    4.25 +  Code_Preproc.setup
    4.26    #> Code_Simp.setup
    4.27    #> Code_Target.setup
    4.28    #> Code_ML.setup
    4.29 @@ -66,7 +64,6 @@
    4.30  
    4.31  ML_file "~~/src/Tools/Code/code_runtime.ML"
    4.32  ML_file "~~/src/Tools/nbe.ML"
    4.33 -setup Nbe.setup
    4.34  
    4.35  hide_const (open) holds
    4.36  
     5.1 --- a/src/Tools/nbe.ML	Fri May 09 08:13:36 2014 +0200
     5.2 +++ b/src/Tools/nbe.ML	Fri May 09 08:13:36 2014 +0200
     5.3 @@ -24,7 +24,6 @@
     5.4    val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
     5.5    val trace: bool Unsynchronized.ref
     5.6  
     5.7 -  val setup: theory -> theory
     5.8    val add_const_alias: thm -> theory -> theory
     5.9  end;
    5.10  
    5.11 @@ -617,9 +616,4 @@
    5.12        (fn program => fn _ => K (eval_term ctxt (compile true ctxt program)));
    5.13    in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
    5.14  
    5.15 -
    5.16 -(** setup **)
    5.17 -
    5.18 -val setup = Value.add_evaluator ("nbe", dynamic_value);
    5.19 -
    5.20  end;
     6.1 --- a/src/Tools/value.ML	Fri May 09 08:13:36 2014 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,79 +0,0 @@
     6.4 -(*  Title:      Tools/value.ML
     6.5 -    Author:     Florian Haftmann, TU Muenchen
     6.6 -
     6.7 -Generic value command for arbitrary evaluators.
     6.8 -*)
     6.9 -
    6.10 -signature VALUE =
    6.11 -sig
    6.12 -  val value: Proof.context -> term -> term
    6.13 -  val value_select: string -> Proof.context -> term -> term
    6.14 -  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
    6.15 -  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
    6.16 -  val setup : theory -> theory
    6.17 -end;
    6.18 -
    6.19 -structure Value : VALUE =
    6.20 -struct
    6.21 -
    6.22 -structure Evaluator = Theory_Data
    6.23 -(
    6.24 -  type T = (string * (Proof.context -> term -> term)) list;
    6.25 -  val empty = [];
    6.26 -  val extend = I;
    6.27 -  fun merge data : T = AList.merge (op =) (K true) data;
    6.28 -)
    6.29 -
    6.30 -val add_evaluator = Evaluator.map o AList.update (op =);
    6.31 -
    6.32 -fun value_select name ctxt =
    6.33 -  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
    6.34 -   of NONE => error ("No such evaluator: " ^ name)
    6.35 -    | SOME f => f ctxt;
    6.36 -
    6.37 -fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
    6.38 -  in if null evaluators then error "No evaluators"
    6.39 -  else let val (evaluators, (_, evaluator)) = split_last evaluators
    6.40 -    in case get_first (fn (_, f) => try (f ctxt) t) evaluators
    6.41 -     of SOME t' => t'
    6.42 -      | NONE => evaluator ctxt t
    6.43 -  end end;
    6.44 -
    6.45 -fun value_maybe_select some_name =
    6.46 -  case some_name
    6.47 -    of NONE => value
    6.48 -     | SOME name => value_select name;
    6.49 -  
    6.50 -fun value_cmd some_name modes raw_t state =
    6.51 -  let
    6.52 -    val ctxt = Toplevel.context_of state;
    6.53 -    val t = Syntax.read_term ctxt raw_t;
    6.54 -    val t' = value_maybe_select some_name ctxt t;
    6.55 -    val ty' = Term.type_of t';
    6.56 -    val ctxt' = Variable.auto_fixes t' ctxt;
    6.57 -    val p = Print_Mode.with_modes modes (fn () =>
    6.58 -      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    6.59 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    6.60 -  in Pretty.writeln p end;
    6.61 -
    6.62 -val opt_modes =
    6.63 -  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
    6.64 -
    6.65 -val opt_evaluator =
    6.66 -  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
    6.67 -  
    6.68 -val _ =
    6.69 -  Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
    6.70 -    (opt_evaluator -- opt_modes -- Parse.term
    6.71 -      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
    6.72 -
    6.73 -val antiq_setup =
    6.74 -  Thy_Output.antiquotation @{binding value}
    6.75 -    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    6.76 -    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
    6.77 -      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
    6.78 -        [style (value_maybe_select some_name context t)]));
    6.79 -
    6.80 -val setup = antiq_setup;
    6.81 -
    6.82 -end;