src/Pure/Isar/parse_spec.ML
author wenzelm
Mon Nov 14 16:52:19 2011 +0100 (2011-11-14 ago)
changeset 45488 6d71d9e52369
parent 44357 5f5649ac8235
child 45592 8baa0b7f3f66
permissions -rw-r--r--
pass positions for named targets, for formal links in the document model;
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@40800
    40
val attrib = Parse.position (Parse.liberal_name -- Parse.!!! Args.parse) >> Args.src;
wenzelm@36950
    41
val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
wenzelm@22104
    42
val opt_attribs = Scan.optional attribs [];
wenzelm@22104
    43
wenzelm@36950
    44
fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
wenzelm@28083
    45
wenzelm@22104
    46
fun opt_thm_name s =
wenzelm@36950
    47
  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
haftmann@28965
    48
    Attrib.empty_binding;
wenzelm@22104
    49
wenzelm@36950
    50
val spec = opt_thm_name ":" -- Parse.prop;
wenzelm@36950
    51
val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
wenzelm@22104
    52
wenzelm@30481
    53
val alt_specs =
wenzelm@36950
    54
  Parse.enum1 "|"
wenzelm@36950
    55
    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
wenzelm@30481
    56
wenzelm@36950
    57
val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
wenzelm@22104
    58
wenzelm@24013
    59
val xthm =
wenzelm@36950
    60
  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
wenzelm@40793
    61
  (Parse.literal_fact >> Facts.Fact ||
wenzelm@36950
    62
    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
wenzelm@24013
    63
wenzelm@22104
    64
val xthms1 = Scan.repeat1 xthm;
wenzelm@22104
    65
wenzelm@36950
    66
val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
wenzelm@22104
    67
wenzelm@22104
    68
wenzelm@33287
    69
(* basic constant specifications *)
wenzelm@33287
    70
wenzelm@33287
    71
val constdecl =
wenzelm@36950
    72
  Parse.binding --
wenzelm@36950
    73
    (Parse.where_ >> K (NONE, NoSyn) ||
wenzelm@36950
    74
      Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
wenzelm@36950
    75
      Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
wenzelm@36950
    76
  >> Parse.triple2;
wenzelm@33287
    77
wenzelm@36950
    78
val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
wenzelm@33287
    79
wenzelm@33287
    80
wenzelm@22104
    81
(* locale and context elements *)
wenzelm@22104
    82
wenzelm@36950
    83
val locale_mixfix =
wenzelm@36950
    84
  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
wenzelm@36950
    85
  Parse.mixfix;
wenzelm@22104
    86
wenzelm@22104
    87
val locale_fixes =
wenzelm@36950
    88
  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
wenzelm@36950
    89
    >> (single o Parse.triple1) ||
wenzelm@42287
    90
  Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
wenzelm@22104
    91
wenzelm@22104
    92
val locale_insts =
wenzelm@36950
    93
  Scan.optional
wenzelm@36950
    94
    (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
wenzelm@36950
    95
  Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
wenzelm@22104
    96
wenzelm@22104
    97
local
wenzelm@22104
    98
wenzelm@22104
    99
val loc_element =
wenzelm@36950
   100
  Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
wenzelm@36950
   101
  Parse.$$$ "constrains" |--
wenzelm@36950
   102
    Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
wenzelm@22104
   103
    >> Element.Constrains ||
wenzelm@36950
   104
  Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
wenzelm@22104
   105
    >> Element.Assumes ||
wenzelm@36950
   106
  Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
wenzelm@22104
   107
    >> Element.Defines ||
wenzelm@36950
   108
  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
wenzelm@22104
   109
    >> (curry Element.Notes "");
wenzelm@22104
   110
wenzelm@24869
   111
fun plus1_unless test scan =
wenzelm@36950
   112
  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
wenzelm@22104
   113
wenzelm@30726
   114
fun prefix mandatory =
wenzelm@36950
   115
  Parse.name --
wenzelm@36950
   116
    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
wenzelm@36950
   117
    Parse.$$$ ":";
wenzelm@22104
   118
wenzelm@36950
   119
val instance = Parse.where_ |--
wenzelm@36950
   120
  Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
wenzelm@36950
   121
  Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
ballarin@29033
   122
wenzelm@24869
   123
in
wenzelm@24869
   124
wenzelm@36950
   125
val locale_keyword =
wenzelm@36950
   126
  Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
wenzelm@36950
   127
  Parse.$$$ "defines" || Parse.$$$ "notes";
ballarin@28722
   128
wenzelm@36950
   129
val class_expr = plus1_unless locale_keyword Parse.xname;
wenzelm@24869
   130
wenzelm@30726
   131
fun locale_expression mandatory =
ballarin@29033
   132
  let
wenzelm@36950
   133
    val expr2 = Parse.xname;
wenzelm@30726
   134
    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
wenzelm@30720
   135
      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
wenzelm@30720
   136
    val expr0 = plus1_unless locale_keyword expr1;
wenzelm@36950
   137
  in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
ballarin@29033
   138
wenzelm@44357
   139
val context_element = Parse.group (fn () => "context element") loc_element;
wenzelm@22104
   140
wenzelm@22104
   141
end;
wenzelm@22104
   142
wenzelm@22104
   143
wenzelm@22104
   144
(* statements *)
wenzelm@22104
   145
wenzelm@36950
   146
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
wenzelm@22104
   147
wenzelm@22104
   148
val obtain_case =
wenzelm@36950
   149
  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
wenzelm@36950
   150
    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
wenzelm@22104
   151
wenzelm@22104
   152
val general_statement =
wenzelm@22104
   153
  statement >> (fn x => ([], Element.Shows x)) ||
ballarin@28722
   154
  Scan.repeat context_element --
wenzelm@36950
   155
   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
wenzelm@36950
   156
    Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
wenzelm@22104
   157
wenzelm@36950
   158
val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
wenzelm@22104
   159
wenzelm@22104
   160
end;
wenzelm@36952
   161