src/Pure/Syntax/mixfix.ML
changeset 42288 2074b31650e6
parent 42287 d98eb048a2e4
child 42293 6cca0343ea48
--- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 14:20:57 2011 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 15:02:11 2011 +0200
@@ -25,8 +25,8 @@
   val mixfixT: mixfix -> typ
   val make_type: int -> typ
   val binder_name: string -> string
-  val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext
-  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext
+  val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
+  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
 end;
 
 structure Mixfix: MIXFIX =
@@ -74,11 +74,11 @@
 (* syntax specifications *)
 
 fun mixfix_args NoSyn = 0
-  | mixfix_args (Mixfix (sy, _, _)) = Syn_Ext.mfix_args sy
-  | mixfix_args (Delimfix sy) = Syn_Ext.mfix_args sy
-  | mixfix_args (Infix (sy, _)) = 2 + Syn_Ext.mfix_args sy
-  | mixfix_args (Infixl (sy, _)) = 2 + Syn_Ext.mfix_args sy
-  | mixfix_args (Infixr (sy, _)) = 2 + Syn_Ext.mfix_args sy
+  | mixfix_args (Mixfix (sy, _, _)) = Syntax_Ext.mfix_args sy
+  | mixfix_args (Delimfix sy) = Syntax_Ext.mfix_args sy
+  | mixfix_args (Infix (sy, _)) = 2 + Syntax_Ext.mfix_args sy
+  | mixfix_args (Infixl (sy, _)) = 2 + Syntax_Ext.mfix_args sy
+  | mixfix_args (Infixr (sy, _)) = 2 + Syntax_Ext.mfix_args sy
   | mixfix_args (Binder _) = 1
   | mixfix_args Structure = 0;
 
@@ -88,29 +88,29 @@
 
 (* syn_ext_types *)
 
-fun make_type n = replicate n Syn_Ext.typeT ---> Syn_Ext.typeT;
+fun make_type n = replicate n Syntax_Ext.typeT ---> Syntax_Ext.typeT;
 
 fun syn_ext_types type_decls =
   let
-    fun mk_infix sy ty t p1 p2 p3 = Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
+    fun mk_infix sy ty t p1 p2 p3 = Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
 
     fun mfix_of (_, _, NoSyn) = NONE
-      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syn_Ext.Mfix (sy, ty, t, ps, p))
-      | mfix_of (t, ty, Delimfix sy) = SOME (Syn_Ext.Mfix (sy, ty, t, [], Syn_Ext.max_pri))
+      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p))
+      | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], Syntax_Ext.max_pri))
       | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
       | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
       | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
       | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);
 
-    fun check_args (_, ty, _) (SOME (mfix as Syn_Ext.Mfix (sy, _, _, _, _))) =
-          if length (Term.binder_types ty) = Syn_Ext.mfix_args sy then ()
-          else Syn_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
+    fun check_args (_, ty, _) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) =
+          if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then ()
+          else Syntax_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
       | check_args _ NONE = ();
 
     val mfix = map mfix_of type_decls;
     val _ = map2 check_args type_decls mfix;
     val xconsts = map #1 type_decls;
-  in Syn_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end;
+  in Syntax_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end;
 
 
 (* syn_ext_consts *)
@@ -121,21 +121,21 @@
 fun syn_ext_consts is_logtype const_decls =
   let
     fun mk_infix sy ty c p1 p2 p3 =
-      [Syn_Ext.Mfix ("op " ^ sy, ty, c, [], Syn_Ext.max_pri),
-       Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
+      [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], Syntax_Ext.max_pri),
+       Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
 
     fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
           [Type ("idts", []), ty2] ---> ty3
       | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
 
     fun mfix_of (_, _, NoSyn) = []
-      | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syn_Ext.Mfix (sy, ty, c, ps, p)]
-      | mfix_of (c, ty, Delimfix sy) = [Syn_Ext.Mfix (sy, ty, c, [], Syn_Ext.max_pri)]
+      | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)]
+      | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], Syntax_Ext.max_pri)]
       | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
       | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
       | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
       | mfix_of (c, ty, Binder (sy, p, q)) =
-          [Syn_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
+          [Syntax_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
       | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c);
 
     fun binder (c, _, Binder _) = SOME (binder_name c, c)
@@ -145,12 +145,12 @@
     val xconsts = map #1 const_decls;
     val binders = map_filter binder const_decls;
     val binder_trs = binders
-      |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
+      |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
     val binder_trs' = binders
-      |> map (Syn_Ext.stamp_trfun binder_stamp o
+      |> map (Syntax_Ext.stamp_trfun binder_stamp o
           apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
   in
-    Syn_Ext.syn_ext' true is_logtype
+    Syntax_Ext.syn_ext' true is_logtype
       mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
   end;