more conventional syntax for code_stmts antiquotation
authorhaftmann
Sun Jan 20 17:14:35 2019 +0000 (9 months ago)
changeset 696974d95261fab5a
parent 69696 9fd395ff57bc
child 69698 1a249d1c884b
more conventional syntax for code_stmts antiquotation
NEWS
src/Doc/Codegen/Foundations.thy
src/Doc/Codegen/Further.thy
src/Doc/Codegen/Refinement.thy
src/Tools/Code/code_target.ML
     1.1 --- a/NEWS	Sun Jan 20 21:26:15 2019 +0100
     1.2 +++ b/NEWS	Sun Jan 20 17:14:35 2019 +0000
     1.3 @@ -85,6 +85,9 @@
     1.4  proper module frame, nothing is added magically any longer.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Code generation: slightly more conventional syntax for
     1.8 +'code_stmts' antiquotation.  Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Simplified syntax setup for big operators under image. In rare
    1.11  situations, type conversions are not inserted implicitly any longer
    1.12  and need to be given explicitly. Auxiliary abbreviations INFIMUM,
     2.1 --- a/src/Doc/Codegen/Foundations.thy	Sun Jan 20 21:26:15 2019 +0100
     2.2 +++ b/src/Doc/Codegen/Foundations.thy	Sun Jan 20 17:14:35 2019 +0000
     2.3 @@ -191,7 +191,7 @@
     2.4  \<close>
     2.5  
     2.6  text %quote \<open>
     2.7 -  @{code_stmts dequeue (consts) dequeue (Haskell)}
     2.8 +  @{code_stmts dequeue constant: dequeue (Haskell)}
     2.9  \<close>
    2.10  
    2.11  text \<open>
    2.12 @@ -283,7 +283,7 @@
    2.13  \<close>
    2.14  
    2.15  text %quote \<open>
    2.16 -  @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
    2.17 +  @{code_stmts strict_dequeue constant: strict_dequeue (Haskell)}
    2.18  \<close>
    2.19  
    2.20  text \<open>
    2.21 @@ -325,7 +325,7 @@
    2.22  \<close>
    2.23  
    2.24  text %quote \<open>
    2.25 -  @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
    2.26 +  @{code_stmts strict_dequeue' constant: empty_queue strict_dequeue' (Haskell)}
    2.27  \<close>
    2.28  
    2.29  text \<open>
     3.1 --- a/src/Doc/Codegen/Further.thy	Sun Jan 20 21:26:15 2019 +0100
     3.2 +++ b/src/Doc/Codegen/Further.thy	Sun Jan 20 17:14:35 2019 +0000
     3.3 @@ -194,7 +194,7 @@
     3.4  \<close>
     3.5  
     3.6  text %quote \<open>
     3.7 -  @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
     3.8 +  @{code_stmts funpows constant: Nat.funpow funpows (Haskell)}
     3.9  \<close>
    3.10  
    3.11  
     4.1 --- a/src/Doc/Codegen/Refinement.thy	Sun Jan 20 21:26:15 2019 +0100
     4.2 +++ b/src/Doc/Codegen/Refinement.thy	Sun Jan 20 17:14:35 2019 +0000
     4.3 @@ -32,7 +32,7 @@
     4.4  \<close>
     4.5  
     4.6  text %quote \<open>
     4.7 -  @{code_stmts fib (consts) fib (Haskell)}
     4.8 +  @{code_stmts fib constant: fib (Haskell)}
     4.9  \<close>
    4.10  
    4.11  text \<open>
    4.12 @@ -69,7 +69,7 @@
    4.13  \<close>
    4.14  
    4.15  text %quote \<open>
    4.16 -  @{code_stmts fib (consts) fib fib_step (Haskell)}
    4.17 +  @{code_stmts fib constant: fib fib_step (Haskell)}
    4.18  \<close>
    4.19  
    4.20  
     5.1 --- a/src/Tools/Code/code_target.ML	Sun Jan 20 21:26:15 2019 +0100
     5.2 +++ b/src/Tools/Code/code_target.ML	Sun Jan 20 17:14:35 2019 +0000
     5.3 @@ -513,25 +513,29 @@
     5.4    check_code ctxt all_public
     5.5      (Code_Thingol.read_const_exprs ctxt raw_cs) seris;
     5.6  
     5.7 +val (constantK, type_constructorK, type_classK, class_relationK, class_instanceK, code_moduleK) =
     5.8 +  (\<^keyword>\<open>constant\<close>, \<^keyword>\<open>type_constructor\<close>, \<^keyword>\<open>type_class\<close>,
     5.9 +    \<^keyword>\<open>class_relation\<close>, \<^keyword>\<open>class_instance\<close>, \<^keyword>\<open>code_module\<close>);
    5.10 +
    5.11  local
    5.12  
    5.13  val parse_const_terms = Scan.repeat1 Args.term
    5.14    >> (fn ts => fn ctxt => map (Code.check_const (Proof_Context.theory_of ctxt)) ts);
    5.15  
    5.16 -fun parse_names category parse internalize mark_symbol =
    5.17 -  Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
    5.18 +fun parse_names keyword parse internalize mark_symbol =
    5.19 +  Scan.lift (keyword --| Args.colon) |-- Scan.repeat1 parse
    5.20    >> (fn xs => fn ctxt => map (mark_symbol o internalize ctxt) xs);
    5.21  
    5.22 -val parse_consts = parse_names "consts" Args.term
    5.23 +val parse_consts = parse_names constantK Args.term
    5.24    (Code.check_const o Proof_Context.theory_of) Constant;
    5.25  
    5.26 -val parse_types = parse_names "types" (Scan.lift Args.name)
    5.27 +val parse_types = parse_names type_constructorK (Scan.lift Args.name)
    5.28    (Sign.intern_type o Proof_Context.theory_of) Type_Constructor;
    5.29  
    5.30 -val parse_classes = parse_names "classes" (Scan.lift Args.name)
    5.31 +val parse_classes = parse_names type_classK (Scan.lift Args.name)
    5.32    (Sign.intern_class o Proof_Context.theory_of) Type_Class;
    5.33  
    5.34 -val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
    5.35 +val parse_instances = parse_names class_instanceK (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
    5.36    (fn ctxt => fn (raw_tyco, raw_class) =>
    5.37      let
    5.38        val thy = Proof_Context.theory_of ctxt;
    5.39 @@ -646,10 +650,6 @@
    5.40  
    5.41  (** Isar setup **)
    5.42  
    5.43 -val (constantK, type_constructorK, type_classK, class_relationK, class_instanceK, code_moduleK) =
    5.44 -  (\<^keyword>\<open>constant\<close>, \<^keyword>\<open>type_constructor\<close>, \<^keyword>\<open>type_class\<close>,
    5.45 -    \<^keyword>\<open>class_relation\<close>, \<^keyword>\<open>class_instance\<close>, \<^keyword>\<open>code_module\<close>);
    5.46 -
    5.47  local
    5.48  
    5.49  val parse_constants = constantK |-- Scan.repeat1 Parse.term >> map Constant;