# HG changeset patch
# User wenzelm
# Date 1729592102 -7200
# Node ID e8030f7b13861b7704da6d80b666f308b61a17db
# Parent  2157039256d3cc8eecc783e39025bd585abb0ba5
misc tuning and clarification;

diff -r 2157039256d3 -r e8030f7b1386 src/HOL/HOLCF/Tools/cont_consts.ML
--- a/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Oct 22 12:03:46 2024 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Oct 22 12:15:02 2024 +0200
@@ -1,7 +1,9 @@
 (*  Title:      HOL/HOLCF/Tools/cont_consts.ML
-    Author:     Tobias Mayr, David von Oheimb, and Markus Wenzel
+    Author:     Tobias Mayr
+    Author:     David von Oheimb
+    Author:     Makarius
 
-HOLCF version of consts: handle continuous function types in mixfix
+HOLCF version of 'consts' command: handle continuous function types in mixfix
 syntax.
 *)
 
@@ -14,23 +16,28 @@
 structure Cont_Consts: CONT_CONSTS =
 struct
 
+(* type cfun *)
 
-(* misc utils *)
+fun count_cfun \<^Type>\<open>cfun _ B\<close> = count_cfun B + 1
+  | count_cfun _ = 0
 
-fun change_arrow 0 T = T
-  | change_arrow n (Type (_, [S, T])) = \<^Type>\<open>fun S \<open>change_arrow (n - 1) T\<close>\<close>
-  | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], [])
+fun change_cfun 0 T = T
+  | change_cfun n \<^Type>\<open>cfun A B\<close> = \<^Type>\<open>fun A \<open>change_cfun (n - 1) B\<close>\<close>
+  | change_cfun _ T = raise TYPE ("cont_consts: change_arrow", [T], [])
+
+
+(* translations *)
 
 fun trans_rules name2 name1 n mx =
   let
-    val vnames = Name.invent Name.context "a" n
+    val xs = Name.invent Name.context "xa" n
     val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1)
   in
     [Syntax.Parse_Print_Rule
-      (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames),
-        fold (fn a => fn t =>
-            Ast.mk_appl (Ast.Constant \<^const_syntax>\<open>Rep_cfun\<close>) [t, Ast.Variable a])
-          vnames (Ast.Constant name1))] @
+      (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable xs),
+        fold (fn x => fn t =>
+            Ast.mk_appl (Ast.Constant \<^const_syntax>\<open>Rep_cfun\<close>) [t, Ast.Variable x])
+          xs (Ast.Constant name1))] @
     (case mx of
       Infix _ => [extra_parse_rule]
     | Infixl _ => [extra_parse_rule]
@@ -39,58 +46,42 @@
   end
 
 
-(* transforming infix/mixfix declarations of constants with type ...->...
-   a declaration of such a constant is transformed to a normal declaration with
-   an internal name, the same type, and nofix. Additionally, a purely syntactic
-   declaration with the original name, type ...=>..., and the original mixfix
-   is generated and connected to the other declaration via some translation.
-*)
-fun transform thy (c, T, mx) =
-  let
-    val thy_ctxt = Proof_Context.init_global thy
-    fun syntax b = Lexicon.mark_const (Sign.full_bname thy b)
-    val c1 = Binding.name_of c
-    val c2 = c1 ^ "_cont_syntax"
-    val n = Mixfix.mixfix_args thy_ctxt mx
-  in
-    ((c, T, NoSyn),
-      (Binding.name c2, change_arrow n T, mx),
-      trans_rules (syntax c2) (syntax c1) n mx)
-  end
-
-fun cfun_arity (Type (n, [_, T])) = if n = \<^type_name>\<open>cfun\<close> then 1 + cfun_arity T else 0
-  | cfun_arity _ = 0
-
-fun is_contconst _ (_, _, NoSyn) = false
-  | is_contconst _ (_, _, Binder _) = false    (* FIXME ? *)
-  | is_contconst thy (c, T, mx) =
-      let
-        val thy_ctxt = Proof_Context.init_global thy
-        val n = Mixfix.mixfix_args thy_ctxt mx handle ERROR msg =>
-          cat_error msg ("in mixfix annotation for " ^ Binding.print c)
-      in cfun_arity T >= n end
-
-
 (* add_consts *)
 
-local
-
 fun gen_add_consts prep_typ raw_decls thy =
   let
+    val thy_ctxt = Proof_Context.init_global thy
+
+    fun is_cont_const (_, _, NoSyn) = false
+      | is_cont_const (_, _, Binder _) = false    (* FIXME ? *)
+      | is_cont_const (c, T, mx) =
+          let
+            val n = Mixfix.mixfix_args thy_ctxt mx handle ERROR msg =>
+              cat_error msg ("in mixfix annotation for " ^ Binding.print c)
+          in count_cfun T >= n end
+
+    fun transform (c, T, mx) =
+      let
+        fun syntax b = Lexicon.mark_const (Sign.full_bname thy b)
+        val c1 = Binding.name_of c
+        val c2 = c1 ^ "_cont_syntax"
+        val n = Mixfix.mixfix_args thy_ctxt mx
+      in
+        ((c, T, NoSyn),
+          (Binding.name c2, change_cfun n T, mx),
+          trans_rules (syntax c2) (syntax c1) n mx)
+      end
+
     val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls
-    val (contconst_decls, normal_decls) = List.partition (is_contconst thy) decls
-    val transformed_decls = map (transform thy) contconst_decls
+    val (cont_decls, normal_decls) = List.partition is_cont_const decls
+    val transformed_decls = map transform cont_decls
   in
     thy
     |> Sign.add_consts (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
     |> Sign.add_trrules (maps #3 transformed_decls)
   end
 
-in
-
 val add_consts = gen_add_consts Sign.certify_typ
 val add_consts_cmd = gen_add_consts Syntax.read_typ_global
 
 end
-
-end