eliminated type Args.T;
authorwenzelm
Fri Mar 13 21:25:15 2009 +0100 (2009-03-13)
changeset 305131796b8ea88aa
parent 30512 17b2aad869fa
child 30514 9455ecc7796d
eliminated type Args.T;
pervasive types 'a parser and 'a context_parser;
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/splitter.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/code.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/spec_parse.ML
src/Pure/Isar/value_parse.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/Thy/thy_output.ML
src/Pure/simplifier.ML
src/Tools/code/code_target.ML
src/Tools/eqsubst.ML
     1.1 --- a/src/Provers/blast.ML	Fri Mar 13 21:24:21 2009 +0100
     1.2 +++ b/src/Provers/blast.ML	Fri Mar 13 21:25:15 2009 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4                   uwrappers: (string * wrapper) list,
     1.5                   safe0_netpair: netpair, safep_netpair: netpair,
     1.6                   haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
     1.7 -  val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
     1.8 +  val cla_modifiers: Method.modifier parser list
     1.9    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    1.10    end;
    1.11  
     2.1 --- a/src/Provers/clasimp.ML	Fri Mar 13 21:24:21 2009 +0100
     2.2 +++ b/src/Provers/clasimp.ML	Fri Mar 13 21:25:15 2009 +0100
     2.3 @@ -62,8 +62,8 @@
     2.4    val iff_add: attribute
     2.5    val iff_add': attribute
     2.6    val iff_del: attribute
     2.7 -  val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
     2.8 -  val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
     2.9 +  val iff_modifiers: Method.modifier parser list
    2.10 +  val clasimp_modifiers: Method.modifier parser list
    2.11    val clasimp_setup: theory -> theory
    2.12  end;
    2.13  
     3.1 --- a/src/Provers/classical.ML	Fri Mar 13 21:24:21 2009 +0100
     3.2 +++ b/src/Provers/classical.ML	Fri Mar 13 21:25:15 2009 +0100
     3.3 @@ -146,7 +146,7 @@
     3.4    val haz_elim: int option -> attribute
     3.5    val haz_intro: int option -> attribute
     3.6    val rule_del: attribute
     3.7 -  val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
     3.8 +  val cla_modifiers: Method.modifier parser list
     3.9    val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
    3.10    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    3.11    val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
     4.1 --- a/src/Provers/splitter.ML	Fri Mar 13 21:24:21 2009 +0100
     4.2 +++ b/src/Provers/splitter.ML	Fri Mar 13 21:25:15 2009 +0100
     4.3 @@ -39,7 +39,7 @@
     4.4    val Delsplits       : thm list -> unit
     4.5    val split_add: attribute
     4.6    val split_del: attribute
     4.7 -  val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
     4.8 +  val split_modifiers : Method.modifier parser list
     4.9    val setup: theory -> theory
    4.10  end;
    4.11  
     5.1 --- a/src/Pure/Isar/args.ML	Fri Mar 13 21:24:21 2009 +0100
     5.2 +++ b/src/Pure/Isar/args.ML	Fri Mar 13 21:25:15 2009 +0100
     5.3 @@ -7,69 +7,66 @@
     5.4  
     5.5  signature ARGS =
     5.6  sig
     5.7 -  type T = OuterLex.token
     5.8 +  type token = OuterLex.token
     5.9    type src
    5.10 -  val src: (string * T list) * Position.T -> src
    5.11 -  val dest_src: src -> (string * T list) * Position.T
    5.12 +  val src: (string * token list) * Position.T -> src
    5.13 +  val dest_src: src -> (string * token list) * Position.T
    5.14    val pretty_src: Proof.context -> src -> Pretty.T
    5.15    val map_name: (string -> string) -> src -> src
    5.16    val morph_values: morphism -> src -> src
    5.17    val maxidx_values: src -> int -> int
    5.18    val assignable: src -> src
    5.19    val closure: src -> src
    5.20 -  val context: Context.generic * T list -> Context.proof * (Context.generic * T list)
    5.21 -  val theory: Context.generic * T list -> Context.theory * (Context.generic * T list)
    5.22 -  val $$$ : string -> T list -> string * T list
    5.23 -  val add: T list -> string * T list
    5.24 -  val del: T list -> string * T list
    5.25 -  val colon: T list -> string * T list
    5.26 -  val query: T list -> string * T list
    5.27 -  val bang: T list -> string * T list
    5.28 -  val query_colon: T list -> string * T list
    5.29 -  val bang_colon: T list -> string * T list
    5.30 -  val parens: (T list -> 'a * T list) -> T list -> 'a * T list
    5.31 -  val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
    5.32 -  val mode: string -> 'a * T list -> bool * ('a * T list)
    5.33 -  val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
    5.34 -  val name_source: T list -> string * T list
    5.35 -  val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
    5.36 -  val name: T list -> string * T list
    5.37 -  val binding: T list -> binding * T list
    5.38 -  val alt_name: T list -> string * T list
    5.39 -  val symbol: T list -> string * T list
    5.40 -  val liberal_name: T list -> string * T list
    5.41 -  val var: T list -> indexname * T list
    5.42 -  val internal_text: T list -> string * T list
    5.43 -  val internal_typ: T list -> typ * T list
    5.44 -  val internal_term: T list -> term * T list
    5.45 -  val internal_fact: T list -> thm list * T list
    5.46 -  val internal_attribute: T list -> (morphism -> attribute) * T list
    5.47 -  val named_text: (string -> string) -> T list -> string * T list
    5.48 -  val named_typ: (string -> typ) -> T list -> typ * T list
    5.49 -  val named_term: (string -> term) -> T list -> term * T list
    5.50 -  val named_fact: (string -> thm list) -> T list -> thm list * T list
    5.51 -  val named_attribute: (string -> morphism -> attribute) -> T list ->
    5.52 -    (morphism -> attribute) * T list
    5.53 -  val typ_abbrev: Context.generic * T list -> typ * (Context.generic * T list)
    5.54 -  val typ: Context.generic * T list -> typ * (Context.generic * T list)
    5.55 -  val term: Context.generic * T list -> term * (Context.generic * T list)
    5.56 -  val term_abbrev: Context.generic * T list -> term * (Context.generic * T list)
    5.57 -  val prop: Context.generic * T list -> term * (Context.generic * T list)
    5.58 -  val tyname: Context.generic * T list -> string * (Context.generic * T list)
    5.59 -  val const: Context.generic * T list -> string * (Context.generic * T list)
    5.60 -  val const_proper: Context.generic * T list -> string * (Context.generic * T list)
    5.61 -  val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
    5.62 -  val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
    5.63 -    -> ((int -> tactic) -> tactic) * ('a * T list)
    5.64 -  val parse: OuterLex.token list -> T list * OuterLex.token list
    5.65 -  val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
    5.66 -  val attribs: (string -> string) -> T list -> src list * T list
    5.67 -  val opt_attribs: (string -> string) -> T list -> src list * T list
    5.68 -  val thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
    5.69 -  val opt_thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
    5.70 -  val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
    5.71 -  val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
    5.72 -    src -> Proof.context -> 'a * Proof.context
    5.73 +  val context: Proof.context context_parser
    5.74 +  val theory: theory context_parser
    5.75 +  val $$$ : string -> string parser
    5.76 +  val add: string parser
    5.77 +  val del: string parser
    5.78 +  val colon: string parser
    5.79 +  val query: string parser
    5.80 +  val bang: string parser
    5.81 +  val query_colon: string parser
    5.82 +  val bang_colon: string parser
    5.83 +  val parens: ('a parser) -> 'a parser
    5.84 +  val bracks: ('a parser) -> 'a parser
    5.85 +  val mode: string -> bool context_parser
    5.86 +  val maybe: 'a parser -> 'a option parser
    5.87 +  val name_source: string parser
    5.88 +  val name_source_position: (SymbolPos.text * Position.T) parser
    5.89 +  val name: string parser
    5.90 +  val binding: binding parser
    5.91 +  val alt_name: string parser
    5.92 +  val symbol: string parser
    5.93 +  val liberal_name: string parser
    5.94 +  val var: indexname parser
    5.95 +  val internal_text: string parser
    5.96 +  val internal_typ: typ parser
    5.97 +  val internal_term: term parser
    5.98 +  val internal_fact: thm list parser
    5.99 +  val internal_attribute: (morphism -> attribute) parser
   5.100 +  val named_text: (string -> string) -> string parser
   5.101 +  val named_typ: (string -> typ) -> typ parser
   5.102 +  val named_term: (string -> term) -> term parser
   5.103 +  val named_fact: (string -> thm list) -> thm list parser
   5.104 +  val named_attribute: (string -> morphism -> attribute) -> (morphism -> attribute) parser
   5.105 +  val typ_abbrev: typ context_parser
   5.106 +  val typ: typ context_parser
   5.107 +  val term: term context_parser
   5.108 +  val term_abbrev: term context_parser
   5.109 +  val prop: term context_parser
   5.110 +  val tyname: string context_parser
   5.111 +  val const: string context_parser
   5.112 +  val const_proper: string context_parser
   5.113 +  val bang_facts: thm list context_parser
   5.114 +  val goal_spec: ((int -> tactic) -> tactic) -> ((int -> tactic) -> tactic) context_parser
   5.115 +  val parse: token list parser
   5.116 +  val parse1: (string -> bool) -> token list parser
   5.117 +  val attribs: (string -> string) -> src list parser
   5.118 +  val opt_attribs: (string -> string) -> src list parser
   5.119 +  val thm_name: (string -> string) -> string -> (binding * src list) parser
   5.120 +  val opt_thm_name: (string -> string) -> string -> (binding * src list) parser
   5.121 +  val syntax: string -> 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   5.122 +  val context_syntax: string -> 'a context_parser -> src -> Proof.context -> 'a * Proof.context
   5.123  end;
   5.124  
   5.125  structure Args: ARGS =
   5.126 @@ -78,13 +75,13 @@
   5.127  structure T = OuterLex;
   5.128  structure P = OuterParse;
   5.129  
   5.130 +type token = T.token;
   5.131 +
   5.132  
   5.133  
   5.134  (** datatype src **)
   5.135  
   5.136 -type T = T.token;
   5.137 -
   5.138 -datatype src = Src of (string * T list) * Position.T;
   5.139 +datatype src = Src of (string * token list) * Position.T;
   5.140  
   5.141  val src = Src;
   5.142  fun dest_src (Src src) = src;
     6.1 --- a/src/Pure/Isar/attrib.ML	Fri Mar 13 21:24:21 2009 +0100
     6.2 +++ b/src/Pure/Isar/attrib.ML	Fri Mar 13 21:25:15 2009 +0100
     6.3 @@ -24,14 +24,13 @@
     6.4      (('c * 'att list) * ('d * 'att list) list) list
     6.5    val crude_closure: Proof.context -> src -> src
     6.6    val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
     6.7 -  val syntax: (Context.generic * Args.T list ->
     6.8 -    attribute * (Context.generic * Args.T list)) -> src -> attribute
     6.9 +  val syntax: attribute context_parser -> src -> attribute
    6.10    val no_args: attribute -> src -> attribute
    6.11    val add_del_args: attribute -> attribute -> src -> attribute
    6.12 -  val thm_sel: Args.T list -> Facts.interval list * Args.T list
    6.13 -  val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
    6.14 -  val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
    6.15 -  val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
    6.16 +  val thm_sel: Facts.interval list parser
    6.17 +  val thm: thm context_parser
    6.18 +  val thms: thm list context_parser
    6.19 +  val multi_thm: thm list context_parser
    6.20    val print_configs: Proof.context -> unit
    6.21    val internal: (morphism -> attribute) -> src
    6.22    val register_config: Config.value Config.T -> theory -> theory
     7.1 --- a/src/Pure/Isar/code.ML	Fri Mar 13 21:24:21 2009 +0100
     7.2 +++ b/src/Pure/Isar/code.ML	Fri Mar 13 21:25:15 2009 +0100
     7.3 @@ -44,7 +44,7 @@
     7.4    val postprocess_conv: theory -> cterm -> thm
     7.5    val postprocess_term: theory -> term -> term
     7.6  
     7.7 -  val add_attribute: string * (Args.T list -> attribute * Args.T list) -> theory -> theory
     7.8 +  val add_attribute: string * attribute parser -> theory -> theory
     7.9  
    7.10    val print_codesetup: theory -> unit
    7.11  end;
    7.12 @@ -83,7 +83,7 @@
    7.13  (** code attributes **)
    7.14  
    7.15  structure CodeAttr = TheoryDataFun (
    7.16 -  type T = (string * (Args.T list -> attribute * Args.T list)) list;
    7.17 +  type T = (string * attribute parser) list;
    7.18    val empty = [];
    7.19    val copy = I;
    7.20    val extend = I;
     8.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Mar 13 21:24:21 2009 +0100
     8.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 13 21:25:15 2009 +0100
     8.3 @@ -9,7 +9,6 @@
     8.4  
     8.5  signature OUTER_SYNTAX =
     8.6  sig
     8.7 -  type 'a parser = 'a OuterParse.parser
     8.8    val command: string -> string -> OuterKeyword.T ->
     8.9      (Toplevel.transition -> Toplevel.transition) parser -> unit
    8.10    val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
     9.1 --- a/src/Pure/Isar/spec_parse.ML	Fri Mar 13 21:24:21 2009 +0100
     9.2 +++ b/src/Pure/Isar/spec_parse.ML	Fri Mar 13 21:25:15 2009 +0100
     9.3 @@ -6,8 +6,6 @@
     9.4  
     9.5  signature SPEC_PARSE =
     9.6  sig
     9.7 -  type token = OuterParse.token
     9.8 -  type 'a parser = 'a OuterParse.parser
     9.9    val attrib: Attrib.src parser
    9.10    val attribs: Attrib.src list parser
    9.11    val opt_attribs: Attrib.src list parser
    9.12 @@ -36,8 +34,6 @@
    9.13  struct
    9.14  
    9.15  structure P = OuterParse;
    9.16 -type token = P.token;
    9.17 -type 'a parser = 'a P.parser;
    9.18  
    9.19  
    9.20  (* theorem specifications *)
    10.1 --- a/src/Pure/Isar/value_parse.ML	Fri Mar 13 21:24:21 2009 +0100
    10.2 +++ b/src/Pure/Isar/value_parse.ML	Fri Mar 13 21:25:15 2009 +0100
    10.3 @@ -6,7 +6,6 @@
    10.4  
    10.5  signature VALUE_PARSE =
    10.6  sig
    10.7 -  type 'a parser = 'a OuterParse.parser
    10.8    val comma: 'a parser -> 'a parser
    10.9    val equal: 'a parser -> 'a parser
   10.10    val parens: 'a parser -> 'a parser
   10.11 @@ -20,7 +19,6 @@
   10.12  struct
   10.13  
   10.14  structure P = OuterParse;
   10.15 -type 'a parser = 'a P.parser;
   10.16  
   10.17  
   10.18  (* syntax utilities *)
    11.1 --- a/src/Pure/ML/ml_antiquote.ML	Fri Mar 13 21:24:21 2009 +0100
    11.2 +++ b/src/Pure/ML/ml_antiquote.ML	Fri Mar 13 21:25:15 2009 +0100
    11.3 @@ -6,15 +6,11 @@
    11.4  
    11.5  signature ML_ANTIQUOTE =
    11.6  sig
    11.7 -  val macro: string ->
    11.8 -    (Context.generic * Args.T list -> Proof.context * (Context.generic * Args.T list)) -> unit
    11.9 +  val macro: string -> Proof.context context_parser -> unit
   11.10    val variant: string -> Proof.context -> string * Proof.context
   11.11 -  val inline: string ->
   11.12 -    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
   11.13 -  val declaration: string -> string ->
   11.14 -    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
   11.15 -  val value: string ->
   11.16 -    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
   11.17 +  val inline: string -> string context_parser -> unit
   11.18 +  val declaration: string -> string -> string context_parser -> unit
   11.19 +  val value: string -> string context_parser -> unit
   11.20  end;
   11.21  
   11.22  structure ML_Antiquote: ML_ANTIQUOTE =
    12.1 --- a/src/Pure/ML/ml_context.ML	Fri Mar 13 21:24:21 2009 +0100
    12.2 +++ b/src/Pure/ML/ml_context.ML	Fri Mar 13 21:25:15 2009 +0100
    12.3 @@ -27,8 +27,7 @@
    12.4    type antiq =
    12.5      {struct_name: string, background: Proof.context} ->
    12.6        (Proof.context -> string * string) * Proof.context
    12.7 -  val add_antiq: string ->
    12.8 -    (Position.T -> Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) -> unit
    12.9 +  val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
   12.10    val trace: bool ref
   12.11    val eval_wrapper: (string -> unit) * (string -> 'a) -> bool -> Position.T -> string -> unit
   12.12    val eval: bool -> Position.T -> string -> unit
   12.13 @@ -157,9 +156,7 @@
   12.14  
   12.15  local
   12.16  
   12.17 -val global_parsers = ref (Symtab.empty:
   12.18 -  (Position.T -> Context.generic * Args.T list -> antiq * (Context.generic * Args.T list))
   12.19 -    Symtab.table);
   12.20 +val global_parsers = ref (Symtab.empty: (Position.T -> antiq context_parser) Symtab.table);
   12.21  
   12.22  in
   12.23  
    13.1 --- a/src/Pure/Thy/thy_output.ML	Fri Mar 13 21:24:21 2009 +0100
    13.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Mar 13 21:25:15 2009 +0100
    13.3 @@ -18,8 +18,7 @@
    13.4    val print_antiquotations: unit -> unit
    13.5    val boolean: string -> bool
    13.6    val integer: string -> int
    13.7 -  val antiquotation: string ->
    13.8 -    (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    13.9 +  val antiquotation: string -> 'a context_parser ->
   13.10      ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
   13.11    datatype markup = Markup | MarkupEnv | Verbatim
   13.12    val modes: string list ref
    14.1 --- a/src/Pure/simplifier.ML	Fri Mar 13 21:24:21 2009 +0100
    14.2 +++ b/src/Pure/simplifier.ML	Fri Mar 13 21:25:15 2009 +0100
    14.3 @@ -73,11 +73,10 @@
    14.4    val def_simproc_i: {name: string, lhss: term list,
    14.5      proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    14.6      local_theory -> local_theory
    14.7 -  val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    14.8 -  val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
    14.9 -  val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   14.10 -  val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
   14.11 -    -> theory -> theory
   14.12 +  val cong_modifiers: Method.modifier parser list
   14.13 +  val simp_modifiers': Method.modifier parser list
   14.14 +  val simp_modifiers: Method.modifier parser list
   14.15 +  val method_setup: Method.modifier parser list -> theory -> theory
   14.16    val easy_setup: thm -> thm list -> theory -> theory
   14.17  end;
   14.18  
    15.1 --- a/src/Tools/code/code_target.ML	Fri Mar 13 21:24:21 2009 +0100
    15.2 +++ b/src/Tools/code/code_target.ML	Fri Mar 13 21:25:15 2009 +0100
    15.3 @@ -26,7 +26,7 @@
    15.4      -> (Path.T option -> 'a -> unit)
    15.5      -> ('a -> string * string option list)
    15.6      -> 'a -> serialization
    15.7 -  val serialize: theory -> string -> string option -> Args.T list
    15.8 +  val serialize: theory -> string -> string option -> OuterLex.token list
    15.9      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
   15.10    val serialize_custom: theory -> string * (serializer * literals)
   15.11      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
   15.12 @@ -106,7 +106,7 @@
   15.13  
   15.14  type serializer =
   15.15    string option                         (*module name*)
   15.16 -  -> Args.T list                        (*arguments*)
   15.17 +  -> OuterLex.token list                (*arguments*)
   15.18    -> (string -> string)                 (*labelled_name*)
   15.19    -> string list                        (*reserved symbols*)
   15.20    -> (string * Pretty.T) list           (*includes*)
    16.1 --- a/src/Tools/eqsubst.ML	Fri Mar 13 21:24:21 2009 +0100
    16.2 +++ b/src/Tools/eqsubst.ML	Fri Mar 13 21:25:15 2009 +0100
    16.3 @@ -109,8 +109,8 @@
    16.4         searchinfo -> Term.term -> match Seq.seq Seq.seq
    16.5  
    16.6      (* syntax tools *)
    16.7 -    val ith_syntax : Args.T list -> int list * Args.T list
    16.8 -    val options_syntax : Args.T list -> bool * Args.T list
    16.9 +    val ith_syntax : int list parser
   16.10 +    val options_syntax : bool parser
   16.11  
   16.12      (* Isar level hooks *)
   16.13      val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method