modernized and more uniform style
authorhaftmann
Fri Jan 09 08:36:59 2015 +0100 (2015-01-09)
changeset 59323468bd3aedfa1
parent 59322 8ccecf1415b0
child 59324 f5f9993a168d
modernized and more uniform style
src/HOL/Library/code_test.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/value.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_target.ML
src/Tools/Code_Generator.thy
     1.1 --- a/src/HOL/Library/code_test.ML	Thu Jan 08 18:23:29 2015 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Fri Jan 09 08:36:59 2015 +0100
     1.3 @@ -571,16 +571,15 @@
     1.4      "compile test cases to target languages, execute them and report results"
     1.5        (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
     1.6  
     1.7 -val _ = Context.>> (Context.map_theory (
     1.8 -  fold add_driver
     1.9 -    [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
    1.10 -     (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
    1.11 -     (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
    1.12 -     (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
    1.13 -     (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
    1.14 -     (scalaN, (evaluate_in_scala, Code_Scala.target))]
    1.15 -    #> fold (fn target => Value.add_evaluator (target, eval_term target))
    1.16 -      [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]
    1.17 -    ))
    1.18 +val _ = Theory.setup (fold add_driver
    1.19 +  [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
    1.20 +   (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
    1.21 +   (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
    1.22 +   (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
    1.23 +   (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
    1.24 +   (scalaN, (evaluate_in_scala, Code_Scala.target))]
    1.25 +  #> fold (fn target => Value.add_evaluator (target, eval_term target))
    1.26 +    [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]);
    1.27 +
    1.28  end
    1.29  
     2.1 --- a/src/HOL/Tools/code_evaluation.ML	Thu Jan 08 18:23:29 2015 +0100
     2.2 +++ b/src/HOL/Tools/code_evaluation.ML	Fri Jan 09 08:36:59 2015 +0100
     2.3 @@ -134,11 +134,11 @@
     2.4  
     2.5  (* setup *)
     2.6  
     2.7 -val _ = Context.>> (Context.map_theory
     2.8 +val _ = Theory.setup
     2.9    (Code.datatype_interpretation ensure_term_of
    2.10    #> Code.abstype_interpretation ensure_term_of
    2.11    #> Code.datatype_interpretation ensure_term_of_code
    2.12 -  #> Code.abstype_interpretation ensure_abs_term_of_code));
    2.13 +  #> Code.abstype_interpretation ensure_abs_term_of_code);
    2.14  
    2.15  
    2.16  (** termifying syntax **)
     3.1 --- a/src/HOL/Tools/value.ML	Thu Jan 08 18:23:29 2015 +0100
     3.2 +++ b/src/HOL/Tools/value.ML	Fri Jan 09 08:36:59 2015 +0100
     3.3 @@ -74,7 +74,7 @@
     3.4      (opt_evaluator -- opt_modes -- Parse.term
     3.5        >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
     3.6  
     3.7 -val _ = Context.>> (Context.map_theory
     3.8 +val _ = Theory.setup
     3.9    (Thy_Output.antiquotation @{binding value}
    3.10      (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    3.11      (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
    3.12 @@ -82,7 +82,6 @@
    3.13          [style (value_maybe_select some_name context t)]))
    3.14    #> add_evaluator ("simp", Code_Simp.dynamic_value)
    3.15    #> add_evaluator ("nbe", Nbe.dynamic_value)
    3.16 -  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict))
    3.17 -);
    3.18 +  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict));
    3.19  
    3.20  end;
     4.1 --- a/src/Tools/Code/code_haskell.ML	Thu Jan 08 18:23:29 2015 +0100
     4.2 +++ b/src/Tools/Code/code_haskell.ML	Fri Jan 09 08:36:59 2015 +0100
     4.3 @@ -9,7 +9,6 @@
     4.4    val language_params: string
     4.5    val target: string
     4.6    val print_numeral: string -> int -> string
     4.7 -  val setup: theory -> theory
     4.8  end;
     4.9  
    4.10  structure Code_Haskell : CODE_HASKELL =
    4.11 @@ -493,13 +492,8 @@
    4.12  
    4.13  (** Isar setup **)
    4.14  
    4.15 -val _ =
    4.16 -  Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
    4.17 -    (Parse.term -- Parse.name >> (fn (raw_bind, target) =>
    4.18 -      Toplevel.theory (add_monad target raw_bind)));
    4.19 -
    4.20 -val setup =
    4.21 -  Code_Target.add_language
    4.22 +val _ = Theory.setup
    4.23 +  (Code_Target.add_language
    4.24      (target, { serializer = serializer, literals = literals,
    4.25        check = { env_var = "ISABELLE_GHC", make_destination = I,
    4.26          make_command = fn module_name =>
    4.27 @@ -519,6 +513,11 @@
    4.28      ]
    4.29    #> fold (Code_Target.add_reserved target) prelude_import_unqualified
    4.30    #> fold (Code_Target.add_reserved target o fst) prelude_import_unqualified_constr
    4.31 -  #> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr;
    4.32 +  #> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr);
    4.33 +
    4.34 +val _ =
    4.35 +  Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
    4.36 +    (Parse.term -- Parse.name >> (fn (raw_bind, target) =>
    4.37 +      Toplevel.theory (add_monad target raw_bind)));
    4.38  
    4.39  end; (*struct*)
     5.1 --- a/src/Tools/Code/code_ml.ML	Thu Jan 08 18:23:29 2015 +0100
     5.2 +++ b/src/Tools/Code/code_ml.ML	Fri Jan 09 08:36:59 2015 +0100
     5.3 @@ -8,7 +8,6 @@
     5.4  sig
     5.5    val target_SML: string
     5.6    val target_OCaml: string
     5.7 -  val setup: theory -> theory
     5.8  end;
     5.9  
    5.10  structure Code_ML : CODE_ML =
    5.11 @@ -860,8 +859,8 @@
    5.12      print_typ (INFX (1, R)) ty2
    5.13    );
    5.14  
    5.15 -val setup =
    5.16 -  Code_Target.add_language
    5.17 +val _ = Theory.setup
    5.18 +  (Code_Target.add_language
    5.19      (target_SML, { serializer = serializer_sml, literals = literals_sml,
    5.20        check = { env_var = "ISABELLE_PROCESS",
    5.21          make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
    5.22 @@ -887,6 +886,6 @@
    5.23        "sig", "struct", "then", "to", "true", "try", "type", "val",
    5.24        "virtual", "when", "while", "with"
    5.25      ]
    5.26 -  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
    5.27 +  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]);
    5.28  
    5.29  end; (*struct*)
     6.1 --- a/src/Tools/Code/code_preproc.ML	Thu Jan 08 18:23:29 2015 +0100
     6.2 +++ b/src/Tools/Code/code_preproc.ML	Fri Jan 09 08:36:59 2015 +0100
     6.3 @@ -280,8 +280,8 @@
     6.4    type T = string list option;
     6.5    val empty = SOME [];
     6.6    val extend = I;
     6.7 -  fun merge (NONE, d2) = NONE
     6.8 -    | merge (d1, NONE) = NONE
     6.9 +  fun merge (NONE, _) = NONE
    6.10 +    | merge (_, NONE) = NONE
    6.11      | merge (SOME cs1, SOME cs2) = SOME (Library.merge (op =) (cs1, cs2));
    6.12  );
    6.13  
    6.14 @@ -567,21 +567,26 @@
    6.15  
    6.16  (** setup **)
    6.17  
    6.18 -val _ =
    6.19 +val _ = Theory.setup (
    6.20    let
    6.21      fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    6.22      fun add_del_attribute_parser process =
    6.23        Attrib.add_del (mk_attribute (process Simplifier.add_simp))
    6.24          (mk_attribute (process Simplifier.del_simp));
    6.25    in
    6.26 -    Context.>> (Context.map_theory
    6.27 -      (Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold)
    6.28 -        "preprocessing equations for code generator"
    6.29 -      #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post)
    6.30 -        "postprocessing equations for code generator"
    6.31 -      #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev)
    6.32 -        "post- and preprocessing equations for code generator"))
    6.33 -  end;
    6.34 +    Attrib.setup @{binding code_unfold} (add_del_attribute_parser process_unfold)
    6.35 +      "preprocessing equations for code generator"
    6.36 +    #> Attrib.setup @{binding code_post} (add_del_attribute_parser process_post)
    6.37 +      "postprocessing equations for code generator"
    6.38 +    #> Attrib.setup @{binding code_abbrev} (add_del_attribute_parser process_abbrev)
    6.39 +      "post- and preprocessing equations for code generator"
    6.40 +    #> Attrib.setup @{binding code_preproc_trace}
    6.41 +      ((Scan.lift (Args.$$$ "off" >> K trace_none)
    6.42 +      || (Scan.lift (Args.$$$ "only" |-- Args.colon |-- Scan.repeat1 Parse.term))
    6.43 +         >> trace_only_ext
    6.44 +      || Scan.succeed trace_all)
    6.45 +      >> (Thm.declaration_attribute o K)) "tracing of the code generator preprocessor"
    6.46 +  end);
    6.47  
    6.48  val _ =
    6.49    Outer_Syntax.command @{command_spec "print_codeproc"} "print code preprocessor setup"
     7.1 --- a/src/Tools/Code/code_scala.ML	Thu Jan 08 18:23:29 2015 +0100
     7.2 +++ b/src/Tools/Code/code_scala.ML	Fri Jan 09 08:36:59 2015 +0100
     7.3 @@ -8,7 +8,6 @@
     7.4  sig
     7.5    val target: string
     7.6    val case_insensitive: bool Config.T;
     7.7 -  val setup: theory -> theory
     7.8  end;
     7.9  
    7.10  structure Code_Scala : CODE_SCALA =
    7.11 @@ -423,8 +422,8 @@
    7.12  
    7.13  (** Isar setup **)
    7.14  
    7.15 -val setup =
    7.16 -  Code_Target.add_language
    7.17 +val _ = Theory.setup
    7.18 +  (Code_Target.add_language
    7.19      (target, { serializer = serializer, literals = literals,
    7.20        check = { env_var = "SCALA_HOME",
    7.21          make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
    7.22 @@ -446,6 +445,6 @@
    7.23      ]
    7.24    #> fold (Code_Target.add_reserved target) [
    7.25        "apply", "sys", "scala", "BigInt", "Nil", "List"
    7.26 -    ];
    7.27 +    ]);
    7.28  
    7.29  end; (*struct*)
     8.1 --- a/src/Tools/Code/code_simp.ML	Thu Jan 08 18:23:29 2015 +0100
     8.2 +++ b/src/Tools/Code/code_simp.ML	Fri Jan 09 08:36:59 2015 +0100
     8.3 @@ -14,7 +14,6 @@
     8.4      -> Proof.context -> conv
     8.5    val static_tac: { ctxt: Proof.context, simpset: simpset option, consts: string list }
     8.6      -> Proof.context -> int -> tactic
     8.7 -  val setup: theory -> theory
     8.8    val trace: bool Config.T
     8.9  end;
    8.10  
    8.11 @@ -86,10 +85,10 @@
    8.12  fun dynamic_value ctxt =
    8.13    snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of (Proof_Context.theory_of ctxt);
    8.14  
    8.15 -val setup =
    8.16 -  Method.setup @{binding code_simp}
    8.17 +val _ = Theory.setup 
    8.18 +  (Method.setup @{binding code_simp}
    8.19      (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac)))
    8.20 -    "simplification with code equations";
    8.21 +    "simplification with code equations");
    8.22  
    8.23  
    8.24  (* evaluation with static code context *)
     9.1 --- a/src/Tools/Code/code_target.ML	Thu Jan 08 18:23:29 2015 +0100
     9.2 +++ b/src/Tools/Code/code_target.ML	Fri Jan 09 08:36:59 2015 +0100
     9.3 @@ -55,8 +55,6 @@
     9.4    val add_reserved: string -> string -> theory -> theory
     9.5  
     9.6    val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
     9.7 -
     9.8 -  val setup: theory -> theory
     9.9  end;
    9.10  
    9.11  structure Code_Target : CODE_TARGET =
    9.12 @@ -492,15 +490,15 @@
    9.13  
    9.14  in
    9.15  
    9.16 -val antiq_setup =
    9.17 -  Thy_Output.antiquotation @{binding code_stmts}
    9.18 +val _ = Theory.setup
    9.19 +  (Thy_Output.antiquotation @{binding code_stmts}
    9.20      (parse_const_terms --
    9.21        Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
    9.22        -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
    9.23      (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
    9.24          present_code ctxt (mk_cs ctxt)
    9.25            (maps (fn f => f ctxt) mk_stmtss)
    9.26 -          target_name some_width "Example" []);
    9.27 +          target_name some_width "Example" []));
    9.28  
    9.29  end;
    9.30  
    9.31 @@ -673,9 +671,4 @@
    9.32      | NONE => error ("Bad directive " ^ quote cmd_expr)
    9.33    end;
    9.34  
    9.35 -
    9.36 -(** theory setup **)
    9.37 -
    9.38 -val setup = antiq_setup;
    9.39 -
    9.40  end; (*struct*)
    10.1 --- a/src/Tools/Code_Generator.thy	Thu Jan 08 18:23:29 2015 +0100
    10.2 +++ b/src/Tools/Code_Generator.thy	Fri Jan 09 08:36:59 2015 +0100
    10.3 @@ -16,15 +16,6 @@
    10.4  
    10.5  ML_file "~~/src/Tools/cache_io.ML"
    10.6  ML_file "~~/src/Tools/Code/code_preproc.ML"
    10.7 -
    10.8 -attribute_setup code_preproc_trace = {*
    10.9 -  (Scan.lift (Args.$$$ "off" >> K Code_Preproc.trace_none)
   10.10 -  || (Scan.lift (Args.$$$ "only" |-- Args.colon |-- Scan.repeat1 Parse.term))
   10.11 -       >> Code_Preproc.trace_only_ext
   10.12 -  || Scan.succeed Code_Preproc.trace_all)
   10.13 -  >> (Thm.declaration_attribute o K)
   10.14 -*} "tracing of the code generator preprocessor"
   10.15 -
   10.16  ML_file "~~/src/Tools/Code/code_symbol.ML"
   10.17  ML_file "~~/src/Tools/Code/code_thingol.ML"
   10.18  ML_file "~~/src/Tools/Code/code_simp.ML"
   10.19 @@ -35,14 +26,6 @@
   10.20  ML_file "~~/src/Tools/Code/code_haskell.ML"
   10.21  ML_file "~~/src/Tools/Code/code_scala.ML"
   10.22  
   10.23 -setup {*
   10.24 -  Code_Simp.setup
   10.25 -  #> Code_Target.setup
   10.26 -  #> Code_ML.setup
   10.27 -  #> Code_Haskell.setup
   10.28 -  #> Code_Scala.setup
   10.29 -*}
   10.30 -
   10.31  code_datatype "TYPE('a\<Colon>{})"
   10.32  
   10.33  definition holds :: "prop" where