--- a/src/HOL/HOLCF/Tools/cont_consts.ML Tue Oct 22 12:28:32 2024 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Tue Oct 22 12:41:20 2024 +0200
@@ -16,44 +16,19 @@
structure Cont_Consts: CONT_CONSTS =
struct
-(* type cfun *)
-
fun count_cfun \<^Type>\<open>cfun _ B\<close> = count_cfun B + 1
| count_cfun _ = 0
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 c1 c2 n mx =
- let
- val xs = Name.invent Name.context "xa" n
- val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant c1, Ast.Constant c2)
- in
- [Syntax.Parse_Print_Rule
- (Ast.mk_appl (Ast.Constant c1) (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 c2))] @
- (case mx of
- Infix _ => [extra_parse_rule]
- | Infixl _ => [extra_parse_rule]
- | Infixr _ => [extra_parse_rule]
- | _ => [])
- end
-
-
-(* add_consts *)
+ | change_cfun _ T = raise TYPE ("cont_consts: change_cfun", [T], [])
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 (_, _, Binder _) = false
| is_cont_const (b, T, mx) =
let
val n = Mixfix.mixfix_args thy_ctxt mx handle ERROR msg =>
@@ -65,8 +40,15 @@
val c = Sign.full_name thy b
val c1 = Lexicon.mark_syntax c
val c2 = Lexicon.mark_const c
- val n = Mixfix.mixfix_args thy_ctxt mx
- in ((b, T, NoSyn), (c1, change_cfun n T, mx), trans_rules c1 c2 n mx) end
+ val xs = Name.invent Name.context "xa" (Mixfix.mixfix_args thy_ctxt mx)
+ val trans_rules =
+ Syntax.Parse_Print_Rule
+ (Ast.mk_appl (Ast.Constant c1) (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 c2)) ::
+ (if Mixfix.is_infix mx then [Syntax.Parse_Rule (Ast.Constant c1, Ast.Constant c2)] else [])
+ in ((b, T, NoSyn), (c1, change_cfun (length xs) T, mx), trans_rules) end
val decls = map (fn (b, T, mx) => (b, prep_typ thy T, mx)) raw_decls
val (cont_decls, normal_decls) = List.partition is_cont_const decls