consts in consts_code Isar commands are now referred to by usual term syntax
authorhaftmann
Thu May 10 10:22:17 2007 +0200 (2007-05-10)
changeset 22921475ff421a6a3
parent 22920 0dbcb73bf9bf
child 22922 66baa75eae06
consts in consts_code Isar commands are now referred to by usual term syntax
NEWS
doc-src/HOL/HOL.tex
doc-src/IsarRef/logics.tex
src/HOL/Code_Generator.thy
src/HOL/Extraction/Higman.thy
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Integ/Numeral.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/ExecutableRat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/MicroJava/J/JListExample.thy
src/HOL/MicroJava/JVM/JVMListExample.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/recfun_codegen.ML
src/Pure/Tools/codegen_consts.ML
src/Pure/codegen.ML
     1.1 --- a/NEWS	Thu May 10 10:21:50 2007 +0200
     1.2 +++ b/NEWS	Thu May 10 10:22:17 2007 +0200
     1.3 @@ -68,20 +68,23 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* code generator: consts in 'consts_code' Isar commands are now referred
     1.8 +  to by usual term syntax (including optional type annotations).
     1.9 +
    1.10  * code generator: 
    1.11 -  - Isar "definition"s and primitive instance definitions are added explicitly
    1.12 -    to the table of defining equations
    1.13 +  - Isar 'definition's, 'constdef's and primitive instance definitions are added
    1.14 +    explicitly to the table of defining equations
    1.15    - primitive definitions are not used as defining equations by default any longer
    1.16    - defining equations are now definitly restricted to meta "==" and object
    1.17          equality "="
    1.18    - HOL theories have been adopted accordingly
    1.19  
    1.20  * class_package.ML offers a combination of axclasses and locales to
    1.21 -achieve Haskell-like type classes in Isabelle. See
    1.22 +achieve Haskell-like type classes in Isabelle.  See
    1.23  HOL/ex/Classpackage.thy for examples.
    1.24  
    1.25  * Yet another code generator framework allows to generate executable
    1.26 -code for ML and Haskell (including "class"es). A short usage sketch:
    1.27 +code for ML and Haskell (including "class"es).  A short usage sketch:
    1.28  
    1.29      internal compilation:
    1.30          code_gen <list of constants (term syntax)> (SML #)
     2.1 --- a/doc-src/HOL/HOL.tex	Thu May 10 10:21:50 2007 +0200
     2.2 +++ b/doc-src/HOL/HOL.tex	Thu May 10 10:22:17 2007 +0200
     2.3 @@ -1441,7 +1441,12 @@
     2.4  If the formula involves explicit quantifiers, \texttt{arith_tac} may take
     2.5  super-exponential time and space.
     2.6  
     2.7 -If \texttt{arith_tac} fails, try to find relevant arithmetic results in
the library.  The theories \texttt{Nat} and \texttt{NatArith} contain
theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
Theory \texttt{Divides} contains theorems about \texttt{div} and
\texttt{mod}.  Use Proof General's \emph{find} button (or other search
facilities) to locate them.
     2.8 +If \texttt{arith_tac} fails, try to find relevant arithmetic results in
     2.9 +the library.  The theories \texttt{Nat} and \texttt{NatArith} contain
    2.10 +theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
    2.11 +Theory \texttt{Divides} contains theorems about \texttt{div} and
    2.12 +\texttt{mod}.  Use Proof General's \emph{find} button (or other search
    2.13 +facilities) to locate them.
    2.14  
    2.15  \index{nat@{\textit{nat}} type|)}
    2.16  
    2.17 @@ -2793,12 +2798,14 @@
    2.18  \begin{rail}
    2.19  constscode : 'consts_code' (codespec +);
    2.20  
    2.21 -codespec : name ( '::' type) ? template attachment ?;
    2.22 +codespec : const template attachment ?;
    2.23  
    2.24  typescode : 'types_code' (tycodespec +);
    2.25  
    2.26  tycodespec : name template attachment ?;
    2.27  
    2.28 +const : term;
    2.29 +
    2.30  template: '(' string ')';
    2.31  
    2.32  attachment: 'attach' modespec ? verblbrace text verbrbrace;
    2.33 @@ -2859,8 +2866,8 @@
    2.34  are immediately executable, may be associated with a piece of ML
    2.35  code manually using the \ttindex{consts_code} command
    2.36  (see Fig.~\ref{fig:HOL:codegen-configuration}).
    2.37 -It takes a list whose elements consist of a constant name, together
    2.38 -with an optional type constraint (to account for overloading), and a
    2.39 +It takes a list whose elements consist of a constant (given in usual term syntax
    2.40 +-- an explicit type constraint accounts for overloading), and a
    2.41  mixfix template describing the ML code. The latter is very much the
    2.42  same as the mixfix templates used when declaring new constants.
    2.43  The most notable difference is that terms may be included in the ML
     3.1 --- a/doc-src/IsarRef/logics.tex	Thu May 10 10:21:50 2007 +0200
     3.2 +++ b/doc-src/IsarRef/logics.tex	Thu May 10 10:22:17 2007 +0200
     3.3 @@ -730,12 +730,14 @@
     3.4  
     3.5  'consts\_code' (codespec +);
     3.6  
     3.7 -codespec : name ( '::' type) ? template attachment ?;
     3.8 +codespec : const template attachment ?;
     3.9  
    3.10  'types\_code' (tycodespec +);
    3.11  
    3.12  tycodespec : name template attachment ?;
    3.13  
    3.14 +const: term;
    3.15 +
    3.16  template: '(' string ')';
    3.17  
    3.18  attachment: 'attach' modespec ? verblbrace text verbrbrace;
     4.1 --- a/src/HOL/Code_Generator.thy	Thu May 10 10:21:50 2007 +0200
     4.2 +++ b/src/HOL/Code_Generator.thy	Thu May 10 10:22:17 2007 +0200
     4.3 @@ -39,7 +39,7 @@
     4.4    "Not"     ("not")
     4.5    "op |"    ("(_ orelse/ _)")
     4.6    "op &"    ("(_ andalso/ _)")
     4.7 -  "HOL.If"      ("(if _/ then _/ else _)")
     4.8 +  "If"      ("(if _/ then _/ else _)")
     4.9  
    4.10  setup {*
    4.11  let
     5.1 --- a/src/HOL/Extraction/Higman.thy	Thu May 10 10:21:50 2007 +0200
     5.2 +++ b/src/HOL/Extraction/Higman.thy	Thu May 10 10:22:17 2007 +0200
     5.3 @@ -333,8 +333,8 @@
     5.4  *}
     5.5  
     5.6  consts_code
     5.7 -  arbitrary :: "LT"  ("({* L0 [] [] *})")
     5.8 -  arbitrary :: "TT"  ("({* T0 A [] [] [] R0 *})")
     5.9 +  "arbitrary :: LT"  ("({* L0 [] [] *})")
    5.10 +  "arbitrary :: TT"  ("({* T0 A [] [] [] R0 *})")
    5.11  
    5.12  code_module Higman
    5.13  contains
     6.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Thu May 10 10:21:50 2007 +0200
     6.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Thu May 10 10:22:17 2007 +0200
     6.3 @@ -293,7 +293,7 @@
     6.4  
     6.5  
     6.6  consts_code
     6.7 -  arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
     6.8 +  "arbitrary :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
     6.9  
    6.10  definition
    6.11    arbitrary_nat_pair :: "nat \<times> nat" where
     7.1 --- a/src/HOL/Integ/Numeral.thy	Thu May 10 10:21:50 2007 +0200
     7.2 +++ b/src/HOL/Integ/Numeral.thy	Thu May 10 10:22:17 2007 +0200
     7.3 @@ -667,18 +667,17 @@
     7.4  *}
     7.5  
     7.6  consts_code
     7.7 -  "HOL.zero" :: "int"                ("0")
     7.8 -  "HOL.one" :: "int"                 ("1")
     7.9 -  "HOL.uminus" :: "int => int"       ("~")
    7.10 -  "HOL.plus" :: "int => int => int"  ("(_ +/ _)")
    7.11 -  "HOL.times" :: "int => int => int" ("(_ */ _)")
    7.12 -  "Orderings.less" :: "int => int => bool" ("(_ </ _)")
    7.13 -  "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
    7.14 -  "neg"                              ("(_ < 0)")
    7.15 +  "0 :: int"                   ("0")
    7.16 +  "1 :: int"                   ("1")
    7.17 +  "uminus :: int => int"       ("~")
    7.18 +  "op + :: int => int => int"  ("(_ +/ _)")
    7.19 +  "op * :: int => int => int"  ("(_ */ _)")
    7.20 +  "op \<le> :: int => int => bool" ("(_ <=/ _)")
    7.21 +  "op < :: int => int => bool" ("(_ </ _)")
    7.22  
    7.23  quickcheck_params [default_type = int]
    7.24  
    7.25 -(* setup continues in theory Presburger *)
    7.26 +(*setup continues in theory Presburger*)
    7.27  
    7.28  hide (open) const Pls Min B0 B1 succ pred
    7.29  
     8.1 --- a/src/HOL/Lambda/WeakNorm.thy	Thu May 10 10:21:50 2007 +0200
     8.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Thu May 10 10:22:17 2007 +0200
     8.3 @@ -488,8 +488,8 @@
     8.4  subsection {* Generating executable code *}
     8.5  
     8.6  consts_code
     8.7 -  arbitrary :: "'a"       ("(error \"arbitrary\")")
     8.8 -  arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
     8.9 +  "arbitrary :: 'a"       ("(error \"arbitrary\")")
    8.10 +  "arbitrary :: 'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
    8.11  
    8.12  code_module Norm
    8.13  contains
     9.1 --- a/src/HOL/Library/EfficientNat.thy	Thu May 10 10:21:50 2007 +0200
     9.2 +++ b/src/HOL/Library/EfficientNat.thy	Thu May 10 10:22:17 2007 +0200
     9.3 @@ -170,7 +170,7 @@
     9.4  *}
     9.5  
     9.6  consts_code
     9.7 -  "HOL.zero" :: nat ("0")
     9.8 +  "0 \<Colon> nat" ("0")
     9.9    Suc ("(_ + 1)")
    9.10  
    9.11  text {*
    10.1 --- a/src/HOL/Library/ExecutableRat.thy	Thu May 10 10:21:50 2007 +0200
    10.2 +++ b/src/HOL/Library/ExecutableRat.thy	Thu May 10 10:22:17 2007 +0200
    10.3 @@ -140,13 +140,13 @@
    10.4  consts_code
    10.5    div_zero ("(raise/ (Fail/ \"Division by zero\"))")
    10.6    Fract ("({*erat_of_quotient*} (_) (_))")
    10.7 -  HOL.zero :: rat ("({*Rat True 0 1*})")
    10.8 -  HOL.one :: rat ("({*Rat True 1 1*})")
    10.9 -  HOL.plus :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   10.10 -  HOL.uminus :: "rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")
   10.11 -  HOL.times :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   10.12 -  HOL.inverse :: "rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")
   10.13 -  Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   10.14 -  "op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   10.15 +  "0 \<Colon> rat" ("({*Rat True 0 1*})")
   10.16 +  "1 \<Colon> rat" ("({*Rat True 1 1*})")
   10.17 +  "plus \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   10.18 +  "uminus \<Colon> rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")
   10.19 +  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   10.20 +  "inverse \<Colon> rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")
   10.21 +  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   10.22 +  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   10.23  
   10.24  end
    11.1 --- a/src/HOL/Library/ExecutableSet.thy	Thu May 10 10:21:50 2007 +0200
    11.2 +++ b/src/HOL/Library/ExecutableSet.thy	Thu May 10 10:22:17 2007 +0200
    11.3 @@ -343,19 +343,18 @@
    11.4  subsubsection {* const serializations *}
    11.5  
    11.6  consts_code
    11.7 -  "{}"      ("[]")
    11.8 -  "insert"  ("{*insertl*}")
    11.9 -  "op Un"   ("{*unionl*}")
   11.10 -  "op Int"  ("{*intersect*}")
   11.11 -  "minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
   11.12 -            ("{*flip subtract*}")
   11.13 -  "image"   ("{*map_distinct*}")
   11.14 -  "Union"   ("{*unions*}")
   11.15 -  "Inter"   ("{*intersects*}")
   11.16 -  "UNION"   ("{*map_union*}")
   11.17 -  "INTER"   ("{*map_inter*}")
   11.18 -  "Ball"    ("{*Blall*}")
   11.19 -  "Bex"     ("{*Blex*}")
   11.20 -  "filter_set" ("{*filter*}")
   11.21 +  "{}" ("{*[]*}")
   11.22 +  insert ("{*insertl*}")
   11.23 +  "op \<union>" ("{*unionl*}")
   11.24 +  "op \<inter>" ("{*intersect*}")
   11.25 +  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
   11.26 +  image ("{*map_distinct*}")
   11.27 +  Union ("{*unions*}")
   11.28 +  Inter ("{*intersects*}")
   11.29 +  UNION ("{*map_union*}")
   11.30 +  INTER ("{*map_inter*}")
   11.31 +  Ball ("{*Blall*}")
   11.32 +  Bex ("{*Blex*}")
   11.33 +  filter_set ("{*filter*}")
   11.34  
   11.35  end
    12.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Thu May 10 10:21:50 2007 +0200
    12.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Thu May 10 10:22:17 2007 +0200
    12.3 @@ -73,8 +73,8 @@
    12.4  *}
    12.5  
    12.6    "arbitrary" ("(raise Match)")
    12.7 -  "arbitrary" :: "val" ("{* Unit *}")
    12.8 -  "arbitrary" :: "cname" ("\"\"")
    12.9 +  "arbitrary :: val" ("{* Unit *}")
   12.10 +  "arbitrary :: cname" ("\"\"")
   12.11  
   12.12    "Object" ("\"Object\"")
   12.13    "list_name" ("\"list\"")
    13.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu May 10 10:21:50 2007 +0200
    13.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu May 10 10:22:17 2007 +0200
    13.3 @@ -102,8 +102,8 @@
    13.4  *}
    13.5  
    13.6    "arbitrary" ("(raise Match)")
    13.7 -  "arbitrary" :: "val" ("{* Unit *}")
    13.8 -  "arbitrary" :: "cname" ("{* Object *}")
    13.9 +  "arbitrary :: val" ("{* Unit *}")
   13.10 +  "arbitrary :: cname" ("{* Object *}")
   13.11  
   13.12    "list_nam" ("\"list\"")
   13.13    "test_nam" ("\"test\"")
    14.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu May 10 10:21:50 2007 +0200
    14.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu May 10 10:22:17 2007 +0200
    14.3 @@ -285,12 +285,12 @@
    14.4     (c as Const (s, T), ts) =>
    14.5       (case DatatypePackage.datatype_of_case thy s of
    14.6          SOME {index, descr, ...} =>
    14.7 -          if is_some (get_assoc_code thy s T) then NONE else
    14.8 +          if is_some (get_assoc_code thy (s, T)) then NONE else
    14.9            SOME (pretty_case thy defs gr dep module brack
   14.10              (#3 (the (AList.lookup op = descr index))) c ts)
   14.11        | NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of
   14.12          (SOME {index, descr, ...}, (_, U as Type _)) =>
   14.13 -          if is_some (get_assoc_code thy s T) then NONE else
   14.14 +          if is_some (get_assoc_code thy (s, T)) then NONE else
   14.15            let val SOME args = AList.lookup op =
   14.16              (#3 (the (AList.lookup op = descr index))) s
   14.17            in
   14.18 @@ -305,7 +305,7 @@
   14.19        (case DatatypePackage.get_datatype thy s of
   14.20           NONE => NONE
   14.21         | SOME {descr, ...} =>
   14.22 -           if isSome (get_assoc_type thy s) then NONE else
   14.23 +           if is_some (get_assoc_type thy s) then NONE else
   14.24             let
   14.25               val (gr', ps) = foldl_map
   14.26                 (invoke_tycodegen thy defs dep module false) (gr, Ts);
    15.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu May 10 10:21:50 2007 +0200
    15.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu May 10 10:22:17 2007 +0200
    15.3 @@ -617,7 +617,7 @@
    15.4  
    15.5  fun inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
    15.6      (Const ("Collect", Type (_, [_, Type (_, [U])])), [u]) => (case strip_comb u of
    15.7 -        (Const (s, T), ts) => (case (get_clauses thy s, get_assoc_code thy s T) of
    15.8 +        (Const (s, T), ts) => (case (get_clauses thy s, get_assoc_code thy (s, T)) of
    15.9            (SOME (names, thyname, k, intrs), NONE) =>
   15.10              let val (gr', call_p) = mk_ind_call thy defs gr dep module true
   15.11                s T (ts @ [Term.dummy_pattern U]) names thyname k intrs
   15.12 @@ -628,7 +628,7 @@
   15.13          | _ => NONE)
   15.14        | _ => NONE)
   15.15    | (Const (s, T), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of
   15.16 -      NONE => (case (get_clauses thy s, get_assoc_code thy s T) of
   15.17 +      NONE => (case (get_clauses thy s, get_assoc_code thy (s, T)) of
   15.18          (SOME (names, thyname, k, intrs), NONE) =>
   15.19            if length ts < k then NONE else SOME
   15.20              (let val (gr', call_p) = mk_ind_call thy defs gr dep module false
    16.1 --- a/src/HOL/Tools/recfun_codegen.ML	Thu May 10 10:21:50 2007 +0200
    16.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Thu May 10 10:22:17 2007 +0200
    16.3 @@ -151,7 +151,7 @@
    16.4    end;
    16.5  
    16.6  fun recfun_codegen thy defs gr dep module brack t = (case strip_comb t of
    16.7 -    (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy s T) of
    16.8 +    (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of
    16.9         (([], _), _) => NONE
   16.10       | (_, SOME _) => NONE
   16.11       | ((eqns, thyname), NONE) =>
    17.1 --- a/src/Pure/Tools/codegen_consts.ML	Thu May 10 10:21:50 2007 +0200
    17.2 +++ b/src/Pure/Tools/codegen_consts.ML	Thu May 10 10:22:17 2007 +0200
    17.3 @@ -8,13 +8,14 @@
    17.4  
    17.5  signature CODEGEN_CONSTS =
    17.6  sig
    17.7 -  type const = string * string option (* constant name, possibly instance *)
    17.8 +  type const = string * string option (*constant name, possibly instance*)
    17.9    val const_ord: const * const -> order
   17.10    val eq_const: const * const -> bool
   17.11    structure Consttab: TABLE
   17.12    val const_of_cexpr: theory -> string * typ -> const
   17.13    val string_of_typ: theory -> typ -> string
   17.14    val string_of_const: theory -> const -> string
   17.15 +  val read_bare_const: theory -> string -> string * typ
   17.16    val read_const: theory -> string -> const
   17.17    val read_const_exprs: theory -> (const list -> const list)
   17.18      -> string list -> const list
   17.19 @@ -72,14 +73,16 @@
   17.20  
   17.21  (* reading constants as terms and wildcards pattern *)
   17.22  
   17.23 -fun read_const thy raw_t =
   17.24 +fun read_bare_const thy raw_t =
   17.25    let
   17.26      val t = Sign.read_term thy raw_t;
   17.27    in case try dest_Const t
   17.28 -   of SOME c_ty => const_of_cexpr thy c_ty
   17.29 +   of SOME c_ty => c_ty
   17.30      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   17.31    end;
   17.32  
   17.33 +fun read_const thy = const_of_cexpr thy o read_bare_const thy;
   17.34 +
   17.35  local
   17.36  
   17.37  fun consts_of thy some_thyname =
    18.1 --- a/src/Pure/codegen.ML	Thu May 10 10:21:50 2007 +0200
    18.2 +++ b/src/Pure/codegen.ML	Thu May 10 10:22:17 2007 +0200
    18.3 @@ -35,13 +35,13 @@
    18.4      (string * string) list * codegr
    18.5    val generate_code_i: theory -> string list -> string -> (string * term) list ->
    18.6      (string * string) list * codegr
    18.7 -  val assoc_consts: (xstring * string option * (term mixfix list *
    18.8 -    (string * string) list)) list -> theory -> theory
    18.9 -  val assoc_consts_i: (xstring * typ option * (term mixfix list *
   18.10 -    (string * string) list)) list -> theory -> theory
   18.11 -  val assoc_types: (xstring * (typ mixfix list *
   18.12 -    (string * string) list)) list -> theory -> theory
   18.13 -  val get_assoc_code: theory -> string -> typ ->
   18.14 +  val assoc_const: string * (term mixfix list *
   18.15 +    (string * string) list) -> theory -> theory
   18.16 +  val assoc_const_i: (string * typ) * (term mixfix list *
   18.17 +    (string * string) list) -> theory -> theory
   18.18 +  val assoc_type: xstring * (typ mixfix list *
   18.19 +    (string * string) list) -> theory -> theory
   18.20 +  val get_assoc_code: theory -> string * typ ->
   18.21      (term mixfix list * (string * string) list) option
   18.22    val get_assoc_type: theory -> string ->
   18.23      (typ mixfix list * (string * string) list) option
   18.24 @@ -384,46 +384,34 @@
   18.25  
   18.26  (**** associate constants with target language code ****)
   18.27  
   18.28 -fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) =>
   18.29 +fun gen_assoc_const prep_const (raw_const, syn) thy =
   18.30    let
   18.31      val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   18.32        CodegenData.get thy;
   18.33 -    val cname = Sign.intern_const thy s;
   18.34 +    val (cname, T) = prep_const thy raw_const;
   18.35    in
   18.36 -    (case Sign.const_type thy cname of
   18.37 -       SOME T =>
   18.38 -         let val T' = (case tyopt of
   18.39 -                NONE => T
   18.40 -              | SOME ty =>
   18.41 -                  let val U = prep_type thy ty
   18.42 -                  in if Type.raw_instance (U, T) then U
   18.43 -                    else error ("Illegal type constraint for constant " ^ cname)
   18.44 -                  end)
   18.45 -         in
   18.46 -           if num_args_of (fst syn) > length (binder_types T') then
   18.47 -             error ("More arguments than in corresponding type of " ^ s)
   18.48 -           else (case AList.lookup (op =) consts (cname, T') of
   18.49 -             NONE => CodegenData.put {codegens = codegens,
   18.50 -               tycodegens = tycodegens,
   18.51 -               consts = ((cname, T'), syn) :: consts,
   18.52 -               types = types, attrs = attrs, preprocs = preprocs,
   18.53 -               modules = modules, test_params = test_params} thy
   18.54 -           | SOME _ => error ("Constant " ^ cname ^ " already associated with code"))
   18.55 -         end
   18.56 -     | _ => error ("Not a constant: " ^ s))
   18.57 -  end) (thy, xs);
   18.58 +    if num_args_of (fst syn) > length (binder_types T) then
   18.59 +      error ("More arguments than in corresponding type of " ^ cname)
   18.60 +    else case AList.lookup (op =) consts (cname, T) of
   18.61 +      NONE => CodegenData.put {codegens = codegens,
   18.62 +        tycodegens = tycodegens,
   18.63 +        consts = ((cname, T), syn) :: consts,
   18.64 +        types = types, attrs = attrs, preprocs = preprocs,
   18.65 +        modules = modules, test_params = test_params} thy
   18.66 +    | SOME _ => error ("Constant " ^ cname ^ " already associated with code")
   18.67 +  end;
   18.68  
   18.69 -val assoc_consts_i = gen_assoc_consts (K I);
   18.70 -val assoc_consts = gen_assoc_consts Sign.read_typ;
   18.71 +val assoc_const_i = gen_assoc_const (K I);
   18.72 +val assoc_const = gen_assoc_const CodegenConsts.read_bare_const;
   18.73  
   18.74  
   18.75  (**** associate types with target language types ****)
   18.76  
   18.77 -fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) =>
   18.78 +fun assoc_type (s, syn) thy =
   18.79    let
   18.80      val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   18.81        CodegenData.get thy;
   18.82 -    val tc = Sign.intern_type thy s
   18.83 +    val tc = Sign.intern_type thy s;
   18.84    in
   18.85      case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
   18.86        SOME (Type.LogicalType i, _) =>
   18.87 @@ -436,7 +424,7 @@
   18.88              preprocs = preprocs, modules = modules, test_params = test_params} thy
   18.89          | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
   18.90      | _ => error ("Not a type constructor: " ^ s)
   18.91 -  end) (thy, xs);
   18.92 +  end;
   18.93  
   18.94  fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy);
   18.95  
   18.96 @@ -581,7 +569,7 @@
   18.97  fun is_instance thy T1 T2 =
   18.98    Sign.typ_instance thy (T1, Logic.legacy_varifyT T2);
   18.99  
  18.100 -fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) =>
  18.101 +fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
  18.102    s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
  18.103  
  18.104  fun get_aux_code xs = map_filter (fn (m, code) =>
  18.105 @@ -734,7 +722,7 @@
  18.106          in SOME (gr'', mk_app brack (Pretty.str s) ps) end
  18.107  
  18.108      | Const (s, T) =>
  18.109 -      (case get_assoc_code thy s T of
  18.110 +      (case get_assoc_code thy (s, T) of
  18.111           SOME (ms, aux) =>
  18.112             let val i = num_args_of ms
  18.113             in if length ts < i then
  18.114 @@ -1111,7 +1099,7 @@
  18.115     | _ => error ("Malformed annotation: " ^ quote s));
  18.116  
  18.117  val _ = Context.add_setup
  18.118 -  (assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
  18.119 +  (fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
  18.120       [("term_of",
  18.121         "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
  18.122        ("test",
  18.123 @@ -1139,19 +1127,19 @@
  18.124    OuterSyntax.command "types_code"
  18.125    "associate types with target language types" K.thy_decl
  18.126      (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
  18.127 -     (fn xs => Toplevel.theory (fn thy => assoc_types
  18.128 -       (map (fn ((name, mfx), aux) => (name, (parse_mixfix
  18.129 -         (Sign.read_typ thy) mfx, aux))) xs) thy)));
  18.130 +     (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
  18.131 +       (fn ((name, mfx), aux) => (name, (parse_mixfix
  18.132 +         (Sign.read_typ thy) mfx, aux)))) xs thy)));
  18.133  
  18.134  val assoc_constP =
  18.135    OuterSyntax.command "consts_code"
  18.136    "associate constants with target language code" K.thy_decl
  18.137      (Scan.repeat1
  18.138 -       (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --|
  18.139 +       (P.term --|
  18.140          P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
  18.141 -     (fn xs => Toplevel.theory (fn thy => assoc_consts
  18.142 -       (map (fn (((name, optype), mfx), aux) =>
  18.143 -         (name, optype, (parse_mixfix (Sign.read_term thy) mfx, aux))) xs) thy)));
  18.144 +     (fn xs => Toplevel.theory (fn thy => fold (assoc_const o 
  18.145 +       (fn ((const, mfx), aux) =>
  18.146 +         (const, (parse_mixfix (Sign.read_term thy) mfx, aux)))) xs thy)));
  18.147  
  18.148  fun parse_code lib =
  18.149    Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --