src/Pure/Syntax/mixfix.ML
author wenzelm
Tue Mar 22 15:32:47 2011 +0100 (2011-03-22)
changeset 42052 34f1d2d81284
parent 37216 3165bc303f66
child 42130 e10e2cce85c8
permissions -rw-r--r--
statespace syntax: strip positions -- type constraints are unexpected here;
     1 (*  Title:      Pure/Syntax/mixfix.ML
     2     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3 
     4 Mixfix declarations, infixes, binders.
     5 *)
     6 
     7 signature MIXFIX0 =
     8 sig
     9   datatype mixfix =
    10     NoSyn |
    11     Mixfix of string * int list * int |
    12     Delimfix of string |
    13     Infix of string * int |
    14     Infixl of string * int |
    15     Infixr of string * int |
    16     Binder of string * int * int |
    17     Structure
    18   val binder_name: string -> string
    19 end;
    20 
    21 signature MIXFIX1 =
    22 sig
    23   include MIXFIX0
    24   val no_syn: 'a * 'b -> 'a * 'b * mixfix
    25   val pretty_mixfix: mixfix -> Pretty.T
    26   val mixfix_args: mixfix -> int
    27   val mixfixT: mixfix -> typ
    28   val make_type: int -> typ
    29 end;
    30 
    31 signature MIXFIX =
    32 sig
    33   include MIXFIX1
    34   val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext
    35   val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext
    36 end;
    37 
    38 structure Mixfix: MIXFIX =
    39 struct
    40 
    41 
    42 (** mixfix declarations **)
    43 
    44 datatype mixfix =
    45   NoSyn |
    46   Mixfix of string * int list * int |
    47   Delimfix of string |
    48   Infix of string * int |
    49   Infixl of string * int |
    50   Infixr of string * int |
    51   Binder of string * int * int |
    52   Structure;
    53 
    54 fun no_syn (x, y) = (x, y, NoSyn);
    55 
    56 
    57 (* pretty_mixfix *)
    58 
    59 local
    60 
    61 val quoted = Pretty.quote o Pretty.str;
    62 val keyword = Pretty.keyword;
    63 val parens = Pretty.enclose "(" ")";
    64 val brackets = Pretty.enclose "[" "]";
    65 val int = Pretty.str o string_of_int;
    66 
    67 in
    68 
    69 fun pretty_mixfix NoSyn = Pretty.str ""
    70   | pretty_mixfix (Mixfix (s, ps, p)) =
    71       parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
    72   | pretty_mixfix (Delimfix s) = parens [quoted s]
    73   | pretty_mixfix (Infix (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
    74   | pretty_mixfix (Infixl (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    75   | pretty_mixfix (Infixr (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    76   | pretty_mixfix (Binder (s, p1, p2)) =
    77       parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
    78   | pretty_mixfix Structure = parens [keyword "structure"];
    79 
    80 end;
    81 
    82 
    83 (* syntax specifications *)
    84 
    85 fun mixfix_args NoSyn = 0
    86   | mixfix_args (Mixfix (sy, _, _)) = Syn_Ext.mfix_args sy
    87   | mixfix_args (Delimfix sy) = Syn_Ext.mfix_args sy
    88   | mixfix_args (Infix (sy, _)) = 2 + Syn_Ext.mfix_args sy
    89   | mixfix_args (Infixl (sy, _)) = 2 + Syn_Ext.mfix_args sy
    90   | mixfix_args (Infixr (sy, _)) = 2 + Syn_Ext.mfix_args sy
    91   | mixfix_args (Binder _) = 1
    92   | mixfix_args Structure = 0;
    93 
    94 fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT
    95   | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT;
    96 
    97 
    98 (* syn_ext_types *)
    99 
   100 fun make_type n = replicate n Syn_Ext.typeT ---> Syn_Ext.typeT;
   101 
   102 fun syn_ext_types type_decls =
   103   let
   104     fun mk_infix sy ty t p1 p2 p3 = Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
   105 
   106     fun mfix_of (_, _, NoSyn) = NONE
   107       | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syn_Ext.Mfix (sy, ty, t, ps, p))
   108       | mfix_of (t, ty, Delimfix sy) = SOME (Syn_Ext.Mfix (sy, ty, t, [], Syn_Ext.max_pri))
   109       | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
   110       | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
   111       | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
   112       | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);  (* FIXME printable t (!?) *)
   113 
   114     fun check_args (_, ty, _) (SOME (mfix as Syn_Ext.Mfix (sy, _, _, _, _))) =
   115           if length (Term.binder_types ty) = Syn_Ext.mfix_args sy then ()
   116           else Syn_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
   117       | check_args _ NONE = ();
   118 
   119     val mfix = map mfix_of type_decls;
   120     val _ = map2 check_args type_decls mfix;
   121     val xconsts = map #1 type_decls;
   122   in Syn_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end;
   123 
   124 
   125 (* syn_ext_consts *)
   126 
   127 val binder_stamp = stamp ();
   128 val binder_name = suffix "_binder";
   129 
   130 fun syn_ext_consts is_logtype const_decls =
   131   let
   132     fun mk_infix sy ty c p1 p2 p3 =
   133       [Syn_Ext.Mfix ("op " ^ sy, ty, c, [], Syn_Ext.max_pri),
   134        Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
   135 
   136     fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
   137           [Type ("idts", []), ty2] ---> ty3
   138       | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
   139 
   140     fun mfix_of (_, _, NoSyn) = []
   141       | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syn_Ext.Mfix (sy, ty, c, ps, p)]
   142       | mfix_of (c, ty, Delimfix sy) = [Syn_Ext.Mfix (sy, ty, c, [], Syn_Ext.max_pri)]
   143       | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
   144       | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
   145       | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
   146       | mfix_of (c, ty, Binder (sy, p, q)) =
   147           [Syn_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
   148       | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c);   (* FIXME printable c (!?) *)
   149 
   150     fun binder (c, _, Binder _) = SOME (binder_name c, c)
   151       | binder _ = NONE;
   152 
   153     val mfix = maps mfix_of const_decls;
   154     val xconsts = map #1 const_decls;
   155     val binders = map_filter binder const_decls;
   156     val binder_trs = binders
   157       |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syn_Trans.mk_binder_tr);
   158     val binder_trs' = binders
   159       |> map (Syn_Ext.stamp_trfun binder_stamp o
   160           apsnd (K o Syn_Trans.non_typed_tr') o Syn_Trans.mk_binder_tr' o swap);
   161   in
   162     Syn_Ext.syn_ext' true is_logtype
   163       mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
   164   end;
   165 
   166 end;