src/Pure/Isar/parse_spec.ML
author wenzelm
Mon May 17 10:20:55 2010 +0200 (2010-05-17)
changeset 36955 226fb165833e
parent 36952 338c3f8229e4
child 40793 d21aedaa91e7
permissions -rw-r--r--
centralized legacy aliases;
wenzelm@36952
     1
(*  Title:      Pure/Isar/parse_spec.ML
wenzelm@22104
     2
    Author:     Makarius
wenzelm@22104
     3
wenzelm@22104
     4
Parsers for complex specifications.
wenzelm@22104
     5
*)
wenzelm@22104
     6
wenzelm@36952
     7
signature PARSE_SPEC =
wenzelm@22104
     8
sig
wenzelm@29312
     9
  val attrib: Attrib.src parser
wenzelm@29312
    10
  val attribs: Attrib.src list parser
wenzelm@29312
    11
  val opt_attribs: Attrib.src list parser
wenzelm@29312
    12
  val thm_name: string -> Attrib.binding parser
wenzelm@29312
    13
  val opt_thm_name: string -> Attrib.binding parser
wenzelm@30481
    14
  val spec: (Attrib.binding * string) parser
wenzelm@30481
    15
  val specs: (Attrib.binding * string list) parser
wenzelm@30481
    16
  val alt_specs: (Attrib.binding * string) list parser
wenzelm@30481
    17
  val where_alt_specs: (Attrib.binding * string) list parser
wenzelm@29312
    18
  val xthm: (Facts.ref * Attrib.src list) parser
wenzelm@29312
    19
  val xthms1: (Facts.ref * Attrib.src list) list parser
wenzelm@29312
    20
  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
wenzelm@33287
    21
  val constdecl: (binding * string option * mixfix) parser
wenzelm@33287
    22
  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
wenzelm@29312
    23
  val locale_mixfix: mixfix parser
haftmann@29581
    24
  val locale_fixes: (binding * string option * mixfix) list parser
wenzelm@29312
    25
  val locale_insts: (string option list * (Attrib.binding * string) list) parser
wenzelm@29312
    26
  val class_expr: string list parser
wenzelm@30726
    27
  val locale_expression: bool -> Expression.expression parser
wenzelm@29312
    28
  val locale_keyword: string parser
wenzelm@29312
    29
  val context_element: Element.context parser
wenzelm@29312
    30
  val statement: (Attrib.binding * (string * string list) list) list parser
wenzelm@29312
    31
  val general_statement: (Element.context list * Element.statement) parser
wenzelm@29312
    32
  val statement_keyword: string parser
wenzelm@22104
    33
end;
wenzelm@22104
    34
wenzelm@36952
    35
structure Parse_Spec: PARSE_SPEC =
wenzelm@22104
    36
struct
wenzelm@22104
    37
wenzelm@22104
    38
(* theorem specifications *)
wenzelm@22104
    39
wenzelm@36950
    40
val attrib =
wenzelm@36950
    41
  Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
wenzelm@36950
    42
  >> Args.src;
wenzelm@36950
    43
wenzelm@36950
    44
val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
wenzelm@22104
    45
val opt_attribs = Scan.optional attribs [];
wenzelm@22104
    46
wenzelm@36950
    47
fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
wenzelm@28083
    48
wenzelm@22104
    49
fun opt_thm_name s =
wenzelm@36950
    50
  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
haftmann@28965
    51
    Attrib.empty_binding;
wenzelm@22104
    52
wenzelm@36950
    53
val spec = opt_thm_name ":" -- Parse.prop;
wenzelm@36950
    54
val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
wenzelm@22104
    55
wenzelm@30481
    56
val alt_specs =
wenzelm@36950
    57
  Parse.enum1 "|"
wenzelm@36950
    58
    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
wenzelm@30481
    59
wenzelm@36950
    60
val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
wenzelm@22104
    61
wenzelm@24013
    62
val xthm =
wenzelm@36950
    63
  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
wenzelm@36950
    64
  (Parse.alt_string >> Facts.Fact ||
wenzelm@36950
    65
    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
wenzelm@24013
    66
wenzelm@22104
    67
val xthms1 = Scan.repeat1 xthm;
wenzelm@22104
    68
wenzelm@36950
    69
val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
wenzelm@22104
    70
wenzelm@22104
    71
wenzelm@33287
    72
(* basic constant specifications *)
wenzelm@33287
    73
wenzelm@33287
    74
val constdecl =
wenzelm@36950
    75
  Parse.binding --
wenzelm@36950
    76
    (Parse.where_ >> K (NONE, NoSyn) ||
wenzelm@36950
    77
      Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
wenzelm@36950
    78
      Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
wenzelm@36950
    79
  >> Parse.triple2;
wenzelm@33287
    80
wenzelm@36950
    81
val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
wenzelm@33287
    82
wenzelm@33287
    83
wenzelm@22104
    84
(* locale and context elements *)
wenzelm@22104
    85
wenzelm@36950
    86
val locale_mixfix =
wenzelm@36950
    87
  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
wenzelm@36950
    88
  Parse.mixfix;
wenzelm@22104
    89
wenzelm@22104
    90
val locale_fixes =
wenzelm@36950
    91
  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
wenzelm@36950
    92
    >> (single o Parse.triple1) ||
wenzelm@36950
    93
  Parse.params >> map Syntax.no_syn) >> flat;
wenzelm@22104
    94
wenzelm@22104
    95
val locale_insts =
wenzelm@36950
    96
  Scan.optional
wenzelm@36950
    97
    (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
wenzelm@36950
    98
  Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
wenzelm@22104
    99
wenzelm@22104
   100
local
wenzelm@22104
   101
wenzelm@22104
   102
val loc_element =
wenzelm@36950
   103
  Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
wenzelm@36950
   104
  Parse.$$$ "constrains" |--
wenzelm@36950
   105
    Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
wenzelm@22104
   106
    >> Element.Constrains ||
wenzelm@36950
   107
  Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
wenzelm@22104
   108
    >> Element.Assumes ||
wenzelm@36950
   109
  Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
wenzelm@22104
   110
    >> Element.Defines ||
wenzelm@36950
   111
  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
wenzelm@22104
   112
    >> (curry Element.Notes "");
wenzelm@22104
   113
wenzelm@24869
   114
fun plus1_unless test scan =
wenzelm@36950
   115
  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
wenzelm@22104
   116
wenzelm@30726
   117
fun prefix mandatory =
wenzelm@36950
   118
  Parse.name --
wenzelm@36950
   119
    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
wenzelm@36950
   120
    Parse.$$$ ":";
wenzelm@22104
   121
wenzelm@36950
   122
val instance = Parse.where_ |--
wenzelm@36950
   123
  Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
wenzelm@36950
   124
  Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
ballarin@29033
   125
wenzelm@24869
   126
in
wenzelm@24869
   127
wenzelm@36950
   128
val locale_keyword =
wenzelm@36950
   129
  Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
wenzelm@36950
   130
  Parse.$$$ "defines" || Parse.$$$ "notes";
ballarin@28722
   131
wenzelm@36950
   132
val class_expr = plus1_unless locale_keyword Parse.xname;
wenzelm@24869
   133
wenzelm@30726
   134
fun locale_expression mandatory =
ballarin@29033
   135
  let
wenzelm@36950
   136
    val expr2 = Parse.xname;
wenzelm@30726
   137
    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
wenzelm@30720
   138
      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
wenzelm@30720
   139
    val expr0 = plus1_unless locale_keyword expr1;
wenzelm@36950
   140
  in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
ballarin@29033
   141
wenzelm@36950
   142
val context_element = Parse.group "context element" loc_element;
wenzelm@22104
   143
wenzelm@22104
   144
end;
wenzelm@22104
   145
wenzelm@22104
   146
wenzelm@22104
   147
(* statements *)
wenzelm@22104
   148
wenzelm@36950
   149
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
wenzelm@22104
   150
wenzelm@22104
   151
val obtain_case =
wenzelm@36950
   152
  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
wenzelm@36950
   153
    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
wenzelm@22104
   154
wenzelm@22104
   155
val general_statement =
wenzelm@22104
   156
  statement >> (fn x => ([], Element.Shows x)) ||
ballarin@28722
   157
  Scan.repeat context_element --
wenzelm@36950
   158
   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
wenzelm@36950
   159
    Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
wenzelm@22104
   160
wenzelm@36950
   161
val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
wenzelm@22104
   162
wenzelm@22104
   163
end;
wenzelm@36952
   164