src/Pure/Syntax/mixfix.ML
changeset 42288 2074b31650e6
parent 42287 d98eb048a2e4
child 42293 6cca0343ea48
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 14:20:57 2011 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 15:02:11 2011 +0200
     1.3 @@ -25,8 +25,8 @@
     1.4    val mixfixT: mixfix -> typ
     1.5    val make_type: int -> typ
     1.6    val binder_name: string -> string
     1.7 -  val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext
     1.8 -  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext
     1.9 +  val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
    1.10 +  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
    1.11  end;
    1.12  
    1.13  structure Mixfix: MIXFIX =
    1.14 @@ -74,11 +74,11 @@
    1.15  (* syntax specifications *)
    1.16  
    1.17  fun mixfix_args NoSyn = 0
    1.18 -  | mixfix_args (Mixfix (sy, _, _)) = Syn_Ext.mfix_args sy
    1.19 -  | mixfix_args (Delimfix sy) = Syn_Ext.mfix_args sy
    1.20 -  | mixfix_args (Infix (sy, _)) = 2 + Syn_Ext.mfix_args sy
    1.21 -  | mixfix_args (Infixl (sy, _)) = 2 + Syn_Ext.mfix_args sy
    1.22 -  | mixfix_args (Infixr (sy, _)) = 2 + Syn_Ext.mfix_args sy
    1.23 +  | mixfix_args (Mixfix (sy, _, _)) = Syntax_Ext.mfix_args sy
    1.24 +  | mixfix_args (Delimfix sy) = Syntax_Ext.mfix_args sy
    1.25 +  | mixfix_args (Infix (sy, _)) = 2 + Syntax_Ext.mfix_args sy
    1.26 +  | mixfix_args (Infixl (sy, _)) = 2 + Syntax_Ext.mfix_args sy
    1.27 +  | mixfix_args (Infixr (sy, _)) = 2 + Syntax_Ext.mfix_args sy
    1.28    | mixfix_args (Binder _) = 1
    1.29    | mixfix_args Structure = 0;
    1.30  
    1.31 @@ -88,29 +88,29 @@
    1.32  
    1.33  (* syn_ext_types *)
    1.34  
    1.35 -fun make_type n = replicate n Syn_Ext.typeT ---> Syn_Ext.typeT;
    1.36 +fun make_type n = replicate n Syntax_Ext.typeT ---> Syntax_Ext.typeT;
    1.37  
    1.38  fun syn_ext_types type_decls =
    1.39    let
    1.40 -    fun mk_infix sy ty t p1 p2 p3 = Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
    1.41 +    fun mk_infix sy ty t p1 p2 p3 = Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
    1.42  
    1.43      fun mfix_of (_, _, NoSyn) = NONE
    1.44 -      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syn_Ext.Mfix (sy, ty, t, ps, p))
    1.45 -      | mfix_of (t, ty, Delimfix sy) = SOME (Syn_Ext.Mfix (sy, ty, t, [], Syn_Ext.max_pri))
    1.46 +      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p))
    1.47 +      | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], Syntax_Ext.max_pri))
    1.48        | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
    1.49        | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
    1.50        | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
    1.51        | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);
    1.52  
    1.53 -    fun check_args (_, ty, _) (SOME (mfix as Syn_Ext.Mfix (sy, _, _, _, _))) =
    1.54 -          if length (Term.binder_types ty) = Syn_Ext.mfix_args sy then ()
    1.55 -          else Syn_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
    1.56 +    fun check_args (_, ty, _) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) =
    1.57 +          if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then ()
    1.58 +          else Syntax_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
    1.59        | check_args _ NONE = ();
    1.60  
    1.61      val mfix = map mfix_of type_decls;
    1.62      val _ = map2 check_args type_decls mfix;
    1.63      val xconsts = map #1 type_decls;
    1.64 -  in Syn_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end;
    1.65 +  in Syntax_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end;
    1.66  
    1.67  
    1.68  (* syn_ext_consts *)
    1.69 @@ -121,21 +121,21 @@
    1.70  fun syn_ext_consts is_logtype const_decls =
    1.71    let
    1.72      fun mk_infix sy ty c p1 p2 p3 =
    1.73 -      [Syn_Ext.Mfix ("op " ^ sy, ty, c, [], Syn_Ext.max_pri),
    1.74 -       Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
    1.75 +      [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], Syntax_Ext.max_pri),
    1.76 +       Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
    1.77  
    1.78      fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
    1.79            [Type ("idts", []), ty2] ---> ty3
    1.80        | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
    1.81  
    1.82      fun mfix_of (_, _, NoSyn) = []
    1.83 -      | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syn_Ext.Mfix (sy, ty, c, ps, p)]
    1.84 -      | mfix_of (c, ty, Delimfix sy) = [Syn_Ext.Mfix (sy, ty, c, [], Syn_Ext.max_pri)]
    1.85 +      | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)]
    1.86 +      | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], Syntax_Ext.max_pri)]
    1.87        | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
    1.88        | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
    1.89        | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
    1.90        | mfix_of (c, ty, Binder (sy, p, q)) =
    1.91 -          [Syn_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
    1.92 +          [Syntax_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
    1.93        | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c);
    1.94  
    1.95      fun binder (c, _, Binder _) = SOME (binder_name c, c)
    1.96 @@ -145,12 +145,12 @@
    1.97      val xconsts = map #1 const_decls;
    1.98      val binders = map_filter binder const_decls;
    1.99      val binder_trs = binders
   1.100 -      |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
   1.101 +      |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
   1.102      val binder_trs' = binders
   1.103 -      |> map (Syn_Ext.stamp_trfun binder_stamp o
   1.104 +      |> map (Syntax_Ext.stamp_trfun binder_stamp o
   1.105            apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
   1.106    in
   1.107 -    Syn_Ext.syn_ext' true is_logtype
   1.108 +    Syntax_Ext.syn_ext' true is_logtype
   1.109        mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
   1.110    end;
   1.111