src/HOL/HOLCF/Tools/cont_consts.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Sat Nov 27 16:08:10 2010 -0800
@@ -0,0 +1,93 @@
+(*  Title:      HOLCF/Tools/cont_consts.ML
+    Author:     Tobias Mayr, David von Oheimb, and Markus Wenzel
+
+HOLCF version of consts: handle continuous function types in mixfix
+syntax.
+*)
+
+signature CONT_CONSTS =
+sig
+  val add_consts: (binding * typ * mixfix) list -> theory -> theory
+  val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory
+end;
+
+structure Cont_Consts: CONT_CONSTS =
+struct
+
+
+(* misc utils *)
+
+fun change_arrow 0 T = T
+  | change_arrow n (Type (_, [S, T])) = Type ("fun", [S, change_arrow (n - 1) T])
+  | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []);
+
+fun trans_rules name2 name1 n mx =
+  let
+    val vnames = Name.invents Name.context "a" n;
+    val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
+  in
+    [Syntax.ParsePrintRule
+      (Syntax.mk_appl (Constant name2) (map Variable vnames),
+        fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
+          vnames (Constant name1))] @
+    (case mx of
+      Infix _ => [extra_parse_rule]
+    | Infixl _ => [extra_parse_rule]
+    | Infixr _ => [extra_parse_rule]
+    | _ => [])
+  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
+    fun syntax b = Syntax.mark_const (Sign.full_bname thy b);
+    val c1 = Binding.name_of c;
+    val c2 = c1 ^ "_cont_syntax";
+    val n = Syntax.mixfix_args 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 cfun} then 1 + cfun_arity T else 0
+  | cfun_arity _ = 0;
+
+fun is_contconst (_, _, NoSyn) = false
+  | is_contconst (_, _, Binder _) = false    (* FIXME ? *)
+  | is_contconst (c, T, mx) =
+      let
+        val n = Syntax.mixfix_args mx handle ERROR msg =>
+          cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c));
+      in cfun_arity T >= n end;
+
+
+(* add_consts *)
+
+local
+
+fun gen_add_consts prep_typ raw_decls thy =
+  let
+    val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls;
+    val (contconst_decls, normal_decls) = List.partition is_contconst decls;
+    val transformed_decls = map (transform thy) contconst_decls;
+  in
+    thy
+    |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
+    |> Sign.add_trrules_i (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;