discontinued special treatment of structure Mixfix;
authorwenzelm
Fri Apr 08 14:20:57 2011 +0200 (2011-04-08)
changeset 42287d98eb048a2e4
parent 42286 24075ad39ca2
child 42288 2074b31650e6
discontinued special treatment of structure Mixfix;
eliminated slightly odd no_syn convenience;
src/HOL/HOLCF/Tools/cont_consts.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Orderings.thy
src/HOL/Set.thy
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/Pure/Isar/element.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syntax.ML
src/Pure/sign.ML
     1.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Fri Apr 08 14:05:31 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Fri Apr 08 14:20:57 2011 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4      fun syntax b = Syntax.mark_const (Sign.full_bname thy b)
     1.5      val c1 = Binding.name_of c
     1.6      val c2 = c1 ^ "_cont_syntax"
     1.7 -    val n = Syntax.mixfix_args mx
     1.8 +    val n = Mixfix.mixfix_args mx
     1.9    in
    1.10      ((c, T, NoSyn),
    1.11        (Binding.name c2, change_arrow n T, mx),
    1.12 @@ -64,7 +64,7 @@
    1.13    | is_contconst (_, _, Binder _) = false    (* FIXME ? *)
    1.14    | is_contconst (c, T, mx) =
    1.15        let
    1.16 -        val n = Syntax.mixfix_args mx handle ERROR msg =>
    1.17 +        val n = Mixfix.mixfix_args mx handle ERROR msg =>
    1.18            cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c))
    1.19        in cfun_arity T >= n end
    1.20  
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Apr 08 14:05:31 2011 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Apr 08 14:20:57 2011 +0200
     2.3 @@ -178,7 +178,7 @@
     2.4  
     2.5  (* Compatibility. *)
     2.6  
     2.7 -val string_of_mixfix = Pretty.string_of o Syntax.pretty_mixfix;
     2.8 +val string_of_mixfix = Pretty.string_of o Mixfix.pretty_mixfix;
     2.9  
    2.10  fun mk_syn thy c =
    2.11    if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
     3.1 --- a/src/HOL/Orderings.thy	Fri Apr 08 14:05:31 2011 +0200
     3.2 +++ b/src/HOL/Orderings.thy	Fri Apr 08 14:20:57 2011 +0200
     3.3 @@ -638,8 +638,8 @@
     3.4  
     3.5  print_translation {*
     3.6  let
     3.7 -  val All_binder = Syntax.binder_name @{const_syntax All};
     3.8 -  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
     3.9 +  val All_binder = Mixfix.binder_name @{const_syntax All};
    3.10 +  val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
    3.11    val impl = @{const_syntax HOL.implies};
    3.12    val conj = @{const_syntax HOL.conj};
    3.13    val less = @{const_syntax less};
     4.1 --- a/src/HOL/Set.thy	Fri Apr 08 14:05:31 2011 +0200
     4.2 +++ b/src/HOL/Set.thy	Fri Apr 08 14:20:57 2011 +0200
     4.3 @@ -231,8 +231,8 @@
     4.4  print_translation {*
     4.5  let
     4.6    val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
     4.7 -  val All_binder = Syntax.binder_name @{const_syntax All};
     4.8 -  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
     4.9 +  val All_binder = Mixfix.binder_name @{const_syntax All};
    4.10 +  val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
    4.11    val impl = @{const_syntax HOL.implies};
    4.12    val conj = @{const_syntax HOL.conj};
    4.13    val sbset = @{const_syntax subset};
     5.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Fri Apr 08 14:05:31 2011 +0200
     5.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Fri Apr 08 14:20:57 2011 +0200
     5.3 @@ -643,8 +643,7 @@
     5.4  *)
     5.5  val nums = (0 upto 10000);
     5.6  val nums' = (0 upto 3000);
     5.7 -val const_decls = map (fn i => Syntax.no_syn 
     5.8 -                                 ("const" ^ string_of_int i,Type ("nat",[]))) nums
     5.9 +val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums
    5.10  
    5.11  val consts = sort Term_Ord.fast_term_ord 
    5.12                (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
     6.1 --- a/src/HOL/Statespace/state_space.ML	Fri Apr 08 14:05:31 2011 +0200
     6.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Apr 08 14:20:57 2011 +0200
     6.3 @@ -344,8 +344,6 @@
     6.4  
     6.5  fun K_const T = Const ("StateFun.K_statefun",T --> T --> T);
     6.6  
     6.7 -val no_syn = #3 (Syntax.no_syn ((),()));
     6.8 -
     6.9  
    6.10  fun add_declaration name decl thy =
    6.11    thy
     7.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Apr 08 14:05:31 2011 +0200
     7.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Apr 08 14:20:57 2011 +0200
     7.3 @@ -47,10 +47,9 @@
     7.4        val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts)
     7.5      in
     7.6        Function.add_function
     7.7 -        (map (fn (name, T) =>
     7.8 -            Syntax.no_syn (Binding.conceal (Binding.name name), SOME T))
     7.9 -              (names ~~ Ts))
    7.10 -          (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
    7.11 +        (map (fn (name, T) => (Binding.conceal (Binding.name name), SOME T, NoSyn))
    7.12 +          (names ~~ Ts))
    7.13 +        (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
    7.14          Function_Common.default_config pat_completeness_auto
    7.15        #> snd
    7.16        #> Local_Theory.restore
     8.1 --- a/src/Pure/Isar/element.ML	Fri Apr 08 14:05:31 2011 +0200
     8.2 +++ b/src/Pure/Isar/element.ML	Fri Apr 08 14:20:57 2011 +0200
     8.3 @@ -169,7 +169,7 @@
     8.4      val prt_name_atts = pretty_name_atts ctxt;
     8.5  
     8.6      fun prt_mixfix NoSyn = []
     8.7 -      | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
     8.8 +      | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx];
     8.9  
    8.10      fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") ::
    8.11            Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
     9.1 --- a/src/Pure/Isar/generic_target.ML	Fri Apr 08 14:05:31 2011 +0200
     9.2 +++ b/src/Pure/Isar/generic_target.ML	Fri Apr 08 14:20:57 2011 +0200
     9.3 @@ -42,7 +42,7 @@
     9.4        ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
     9.5          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
     9.6          (if mx = NoSyn then ""
     9.7 -         else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx)));
     9.8 +         else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)));
     9.9        NoSyn);
    9.10  
    9.11  
    10.1 --- a/src/Pure/Isar/parse.ML	Fri Apr 08 14:05:31 2011 +0200
    10.2 +++ b/src/Pure/Isar/parse.ML	Fri Apr 08 14:20:57 2011 +0200
    10.3 @@ -305,7 +305,7 @@
    10.4  
    10.5  val fixes =
    10.6    and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
    10.7 -    params >> map Syntax.no_syn) >> flat;
    10.8 +    params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
    10.9  
   10.10  val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
   10.11  val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];
    11.1 --- a/src/Pure/Isar/parse_spec.ML	Fri Apr 08 14:05:31 2011 +0200
    11.2 +++ b/src/Pure/Isar/parse_spec.ML	Fri Apr 08 14:20:57 2011 +0200
    11.3 @@ -87,7 +87,7 @@
    11.4  val locale_fixes =
    11.5    Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
    11.6      >> (single o Parse.triple1) ||
    11.7 -  Parse.params >> map Syntax.no_syn) >> flat;
    11.8 +  Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
    11.9  
   11.10  val locale_insts =
   11.11    Scan.optional
    12.1 --- a/src/Pure/Isar/proof.ML	Fri Apr 08 14:05:31 2011 +0200
    12.2 +++ b/src/Pure/Isar/proof.ML	Fri Apr 08 14:20:57 2011 +0200
    12.3 @@ -566,7 +566,7 @@
    12.4  
    12.5  val write_cmd =
    12.6    gen_write (fn ctxt => fn (c, mx) =>
    12.7 -    (ProofContext.read_const ctxt false (Syntax.mixfixT mx) c, mx));
    12.8 +    (ProofContext.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
    12.9  
   12.10  end;
   12.11  
    13.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 08 14:05:31 2011 +0200
    13.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Apr 08 14:20:57 2011 +0200
    13.3 @@ -915,7 +915,7 @@
    13.4  (* variables *)
    13.5  
    13.6  fun declare_var (x, opt_T, mx) ctxt =
    13.7 -  let val T = (case opt_T of SOME T => T | NONE => Syntax.mixfixT mx)
    13.8 +  let val T = (case opt_T of SOME T => T | NONE => Mixfix.mixfixT mx)
    13.9    in ((x, T, mx), ctxt |> Variable.declare_constraints (Free (x, T))) end;
   13.10  
   13.11  local
   13.12 @@ -978,7 +978,7 @@
   13.13  local
   13.14  
   13.15  fun type_syntax (Type (c, args), mx) =
   13.16 -      SOME (Local_Syntax.Type, (Syntax.mark_type c, Syntax.make_type (length args), mx))
   13.17 +      SOME (Local_Syntax.Type, (Syntax.mark_type c, Mixfix.make_type (length args), mx))
   13.18    | type_syntax _ = NONE;
   13.19  
   13.20  fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
    14.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 14:05:31 2011 +0200
    14.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 14:20:57 2011 +0200
    14.3 @@ -4,7 +4,7 @@
    14.4  Mixfix declarations, infixes, binders.
    14.5  *)
    14.6  
    14.7 -signature MIXFIX0 =
    14.8 +signature BASIC_MIXFIX =
    14.9  sig
   14.10    datatype mixfix =
   14.11      NoSyn |
   14.12 @@ -15,22 +15,16 @@
   14.13      Infixr of string * int |
   14.14      Binder of string * int * int |
   14.15      Structure
   14.16 -  val binder_name: string -> string
   14.17  end;
   14.18  
   14.19 -signature MIXFIX1 =
   14.20 +signature MIXFIX =
   14.21  sig
   14.22 -  include MIXFIX0
   14.23 -  val no_syn: 'a * 'b -> 'a * 'b * mixfix
   14.24 +  include BASIC_MIXFIX
   14.25    val pretty_mixfix: mixfix -> Pretty.T
   14.26    val mixfix_args: mixfix -> int
   14.27    val mixfixT: mixfix -> typ
   14.28    val make_type: int -> typ
   14.29 -end;
   14.30 -
   14.31 -signature MIXFIX =
   14.32 -sig
   14.33 -  include MIXFIX1
   14.34 +  val binder_name: string -> string
   14.35    val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext
   14.36    val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext
   14.37  end;
   14.38 @@ -38,7 +32,6 @@
   14.39  structure Mixfix: MIXFIX =
   14.40  struct
   14.41  
   14.42 -
   14.43  (** mixfix declarations **)
   14.44  
   14.45  datatype mixfix =
   14.46 @@ -51,8 +44,6 @@
   14.47    Binder of string * int * int |
   14.48    Structure;
   14.49  
   14.50 -fun no_syn (x, y) = (x, y, NoSyn);
   14.51 -
   14.52  
   14.53  (* pretty_mixfix *)
   14.54  
   14.55 @@ -164,3 +155,7 @@
   14.56    end;
   14.57  
   14.58  end;
   14.59 +
   14.60 +structure Basic_Mixfix: BASIC_MIXFIX = Mixfix;
   14.61 +open Basic_Mixfix;
   14.62 +
    15.1 --- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 14:05:31 2011 +0200
    15.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 14:20:57 2011 +0200
    15.3 @@ -7,7 +7,6 @@
    15.4  
    15.5  signature BASIC_SYNTAX =
    15.6  sig
    15.7 -  include MIXFIX0
    15.8    include PRINTER0
    15.9  end;
   15.10  
   15.11 @@ -15,7 +14,6 @@
   15.12  sig
   15.13    include LEXICON0
   15.14    include SYN_EXT0
   15.15 -  include MIXFIX1
   15.16    include PRINTER0
   15.17    val positions_raw: Config.raw
   15.18    val positions: bool Config.T
   15.19 @@ -725,7 +723,7 @@
   15.20  
   15.21  (*export parts of internal Syntax structures*)
   15.22  val syntax_tokenize = tokenize;
   15.23 -open Lexicon Syn_Ext Mixfix Printer;
   15.24 +open Lexicon Syn_Ext Printer;
   15.25  val tokenize = syntax_tokenize;
   15.26  
   15.27  end;
   15.28 @@ -734,5 +732,4 @@
   15.29  open Basic_Syntax;
   15.30  
   15.31  forget_structure "Syn_Ext";
   15.32 -forget_structure "Mixfix";
   15.33  
    16.1 --- a/src/Pure/sign.ML	Fri Apr 08 14:05:31 2011 +0200
    16.2 +++ b/src/Pure/sign.ML	Fri Apr 08 14:20:57 2011 +0200
    16.3 @@ -334,7 +334,7 @@
    16.4  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    16.5    let
    16.6      fun type_syntax (b, n, mx) =
    16.7 -      (Syntax.mark_type (Name_Space.full_name naming b), Syntax.make_type n, mx);
    16.8 +      (Syntax.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
    16.9      val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
   16.10      val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
   16.11    in (naming, syn', tsig', consts) end);
   16.12 @@ -373,7 +373,7 @@
   16.13  fun type_notation add mode args =
   16.14    let
   16.15      fun type_syntax (Type (c, args), mx) =
   16.16 -          SOME (Syntax.mark_type c, Syntax.make_type (length args), mx)
   16.17 +          SOME (Syntax.mark_type c, Mixfix.make_type (length args), mx)
   16.18        | type_syntax _ = NONE;
   16.19    in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
   16.20