src/Pure/Isar/spec_parse.ML
author wenzelm
Thu, 26 Mar 2009 18:59:25 +0100
changeset 30726 67388cc4ccb4
parent 30720 6d8dcfb264dc
child 33287 0f99569d23e1
permissions -rw-r--r--
locale_expression: mandatory as parameter; misc tuning and simplifications of parsers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/spec_parse.ML
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     3
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     4
Parsers for complex specifications.
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     5
*)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     6
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     7
signature SPEC_PARSE =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     8
sig
29312
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
     9
  val attrib: Attrib.src parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    10
  val attribs: Attrib.src list parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    11
  val opt_attribs: Attrib.src list parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    12
  val thm_name: string -> Attrib.binding parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    13
  val opt_thm_name: string -> Attrib.binding parser
30481
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    14
  val spec: (Attrib.binding * string) parser
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    15
  val specs: (Attrib.binding * string list) parser
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    16
  val alt_specs: (Attrib.binding * string) list parser
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    17
  val where_alt_specs: (Attrib.binding * string) list parser
29312
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    18
  val xthm: (Facts.ref * Attrib.src list) parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    19
  val xthms1: (Facts.ref * Attrib.src list) list parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    20
  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    21
  val locale_mixfix: mixfix parser
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29360
diff changeset
    22
  val locale_fixes: (binding * string option * mixfix) list parser
29312
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    23
  val locale_insts: (string option list * (Attrib.binding * string) list) parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    24
  val class_expr: string list parser
30726
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
    25
  val locale_expression: bool -> Expression.expression parser
29312
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    26
  val locale_keyword: string parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    27
  val context_element: Element.context parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    28
  val statement: (Attrib.binding * (string * string list) list) list parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    29
  val general_statement: (Element.context list * Element.statement) parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    30
  val statement_keyword: string parser
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    31
end;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    32
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    33
structure SpecParse: SPEC_PARSE =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    34
struct
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    35
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    36
structure P = OuterParse;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    37
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    38
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    39
(* theorem specifications *)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    40
27816
0dfed2f2822a unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27378
diff changeset
    41
val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src;
24014
d3873741678d attribs: not cut (!!!);
wenzelm
parents: 24013
diff changeset
    42
val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    43
val opt_attribs = Scan.optional attribs [];
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    44
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27816
diff changeset
    45
fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27816
diff changeset
    46
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    47
fun opt_thm_name s =
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28722
diff changeset
    48
  Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
1de908189869 cleaned up binding module and related code
haftmann
parents: 28722
diff changeset
    49
    Attrib.empty_binding;
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    50
30481
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    51
val spec = opt_thm_name ":" -- P.prop;
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    52
val specs = opt_thm_name ":" -- Scan.repeat1 P.prop;
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    53
30481
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    54
val alt_specs =
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    55
  P.enum1 "|" (spec --| Scan.option (Scan.ahead (P.name || P.$$$ "[") -- P.!!! (P.$$$ "|")));
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    56
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    57
val where_alt_specs = P.where_ |-- P.!!! alt_specs;
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    58
24013
3063a756611d xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents: 23919
diff changeset
    59
val xthm =
26361
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    60
  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
7946f459c6c8 Facts.Named: include position;
wenzelm
parents: 26336
diff changeset
    61
  (P.alt_string >> Facts.Fact ||
27816
0dfed2f2822a unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27378
diff changeset
    62
    P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
24013
3063a756611d xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents: 23919
diff changeset
    63
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    64
val xthms1 = Scan.repeat1 xthm;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    65
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    66
val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    67
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    68
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    69
(* locale and context elements *)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    70
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    71
val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    72
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    73
val locale_fixes =
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27816
diff changeset
    74
  P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    75
    >> (single o P.triple1) ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    76
  P.params >> map Syntax.no_syn) >> flat;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    77
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    78
val locale_insts =
22658
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22104
diff changeset
    79
  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
30726
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
    80
  -- Scan.optional (P.where_ |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    81
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    82
local
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    83
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    84
val loc_element =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    85
  P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    86
  P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    87
    >> Element.Constrains ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    88
  P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp))
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    89
    >> Element.Assumes ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    90
  P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp))
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    91
    >> Element.Defines ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    92
  P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    93
    >> (curry Element.Notes "");
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    94
24869
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
    95
fun plus1_unless test scan =
25999
f8bcd311d501 added ::: / @@@ scanner combinators;
wenzelm
parents: 25094
diff changeset
    96
  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    97
30726
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
    98
fun prefix mandatory =
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
    99
  P.name -- (P.$$$ "!" >> K true || P.$$$ "?" >> K false || Scan.succeed mandatory) --| P.$$$ ":";
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   100
30726
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
   101
val instance = P.where_ |--
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
   102
  P.and_list1 (P.name -- (P.$$$ "=" |-- P.term)) >> Expression.Named ||
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
   103
  Scan.repeat1 (P.maybe P.term) >> Expression.Positional;
29033
721529248e31 Enable keyword 'structure' in for clause of locale expression.
ballarin
parents: 28965
diff changeset
   104
24869
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   105
in
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   106
28722
bdb694e18bf8 Minor cleanup.
ballarin
parents: 28710
diff changeset
   107
val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
bdb694e18bf8 Minor cleanup.
ballarin
parents: 28710
diff changeset
   108
   P.$$$ "defines" || P.$$$ "notes";
bdb694e18bf8 Minor cleanup.
ballarin
parents: 28710
diff changeset
   109
bdb694e18bf8 Minor cleanup.
ballarin
parents: 28710
diff changeset
   110
val class_expr = plus1_unless locale_keyword P.xname;
24869
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   111
30726
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
   112
fun locale_expression mandatory =
29033
721529248e31 Enable keyword 'structure' in for clause of locale expression.
ballarin
parents: 28965
diff changeset
   113
  let
30720
wenzelm
parents: 30513
diff changeset
   114
    val expr2 = P.xname;
30726
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
   115
    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
30720
wenzelm
parents: 30513
diff changeset
   116
      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
wenzelm
parents: 30513
diff changeset
   117
    val expr0 = plus1_unless locale_keyword expr1;
29033
721529248e31 Enable keyword 'structure' in for clause of locale expression.
ballarin
parents: 28965
diff changeset
   118
  in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
721529248e31 Enable keyword 'structure' in for clause of locale expression.
ballarin
parents: 28965
diff changeset
   119
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   120
val context_element = P.group "context element" loc_element;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   121
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   122
end;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   123
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   124
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   125
(* statements *)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   126
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   127
val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   128
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   129
val obtain_case =
30726
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
   130
  P.parbinding -- (Scan.optional (P.simple_fixes --| P.where_) [] --
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   131
    (P.and_list1 (Scan.repeat1 P.prop) >> flat));
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   132
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   133
val general_statement =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   134
  statement >> (fn x => ([], Element.Shows x)) ||
28722
bdb694e18bf8 Minor cleanup.
ballarin
parents: 28710
diff changeset
   135
  Scan.repeat context_element --
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   136
   (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   137
    P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   138
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   139
val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   140
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   141
end;