src/Pure/Isar/spec_parse.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 33287 0f99569d23e1
child 36950 75b8f26f2f07
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm@22104
     1
(*  Title:      Pure/Isar/spec_parse.ML
wenzelm@22104
     2
    Author:     Makarius
wenzelm@22104
     3
wenzelm@22104
     4
Parsers for complex specifications.
wenzelm@22104
     5
*)
wenzelm@22104
     6
wenzelm@22104
     7
signature SPEC_PARSE =
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@22104
    35
structure SpecParse: SPEC_PARSE =
wenzelm@22104
    36
struct
wenzelm@22104
    37
wenzelm@22104
    38
structure P = OuterParse;
wenzelm@22104
    39
wenzelm@22104
    40
wenzelm@22104
    41
(* theorem specifications *)
wenzelm@22104
    42
wenzelm@27816
    43
val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src;
wenzelm@24014
    44
val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
wenzelm@22104
    45
val opt_attribs = Scan.optional attribs [];
wenzelm@22104
    46
wenzelm@28083
    47
fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
wenzelm@28083
    48
wenzelm@22104
    49
fun opt_thm_name s =
haftmann@28965
    50
  Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
haftmann@28965
    51
    Attrib.empty_binding;
wenzelm@22104
    52
wenzelm@30481
    53
val spec = opt_thm_name ":" -- P.prop;
wenzelm@30481
    54
val specs = opt_thm_name ":" -- Scan.repeat1 P.prop;
wenzelm@22104
    55
wenzelm@30481
    56
val alt_specs =
wenzelm@30481
    57
  P.enum1 "|" (spec --| Scan.option (Scan.ahead (P.name || P.$$$ "[") -- P.!!! (P.$$$ "|")));
wenzelm@30481
    58
wenzelm@30481
    59
val where_alt_specs = P.where_ |-- P.!!! alt_specs;
wenzelm@22104
    60
wenzelm@24013
    61
val xthm =
wenzelm@26361
    62
  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
wenzelm@26361
    63
  (P.alt_string >> Facts.Fact ||
wenzelm@27816
    64
    P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
wenzelm@24013
    65
wenzelm@22104
    66
val xthms1 = Scan.repeat1 xthm;
wenzelm@22104
    67
wenzelm@22104
    68
val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
wenzelm@22104
    69
wenzelm@22104
    70
wenzelm@33287
    71
(* basic constant specifications *)
wenzelm@33287
    72
wenzelm@33287
    73
val constdecl =
wenzelm@33287
    74
  P.binding --
wenzelm@33287
    75
    (P.where_ >> K (NONE, NoSyn) ||
wenzelm@33287
    76
      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
wenzelm@33287
    77
      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
wenzelm@33287
    78
  >> P.triple2;
wenzelm@33287
    79
wenzelm@33287
    80
val constdef = Scan.option constdecl -- (opt_thm_name ":" -- P.prop);
wenzelm@33287
    81
wenzelm@33287
    82
wenzelm@22104
    83
(* locale and context elements *)
wenzelm@22104
    84
wenzelm@22104
    85
val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
wenzelm@22104
    86
wenzelm@22104
    87
val locale_fixes =
wenzelm@28083
    88
  P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
wenzelm@22104
    89
    >> (single o P.triple1) ||
wenzelm@22104
    90
  P.params >> map Syntax.no_syn) >> flat;
wenzelm@22104
    91
wenzelm@22104
    92
val locale_insts =
ballarin@22658
    93
  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
wenzelm@30726
    94
  -- Scan.optional (P.where_ |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
wenzelm@22104
    95
wenzelm@22104
    96
local
wenzelm@22104
    97
wenzelm@22104
    98
val loc_element =
wenzelm@22104
    99
  P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
wenzelm@22104
   100
  P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
wenzelm@22104
   101
    >> Element.Constrains ||
wenzelm@22104
   102
  P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp))
wenzelm@22104
   103
    >> Element.Assumes ||
wenzelm@22104
   104
  P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp))
wenzelm@22104
   105
    >> Element.Defines ||
wenzelm@22104
   106
  P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
wenzelm@22104
   107
    >> (curry Element.Notes "");
wenzelm@22104
   108
wenzelm@24869
   109
fun plus1_unless test scan =
wenzelm@25999
   110
  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
wenzelm@22104
   111
wenzelm@30726
   112
fun prefix mandatory =
wenzelm@30726
   113
  P.name -- (P.$$$ "!" >> K true || P.$$$ "?" >> K false || Scan.succeed mandatory) --| P.$$$ ":";
wenzelm@22104
   114
wenzelm@30726
   115
val instance = P.where_ |--
wenzelm@30726
   116
  P.and_list1 (P.name -- (P.$$$ "=" |-- P.term)) >> Expression.Named ||
wenzelm@30726
   117
  Scan.repeat1 (P.maybe P.term) >> Expression.Positional;
ballarin@29033
   118
wenzelm@24869
   119
in
wenzelm@24869
   120
ballarin@28722
   121
val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
ballarin@28722
   122
   P.$$$ "defines" || P.$$$ "notes";
ballarin@28722
   123
ballarin@28722
   124
val class_expr = plus1_unless locale_keyword P.xname;
wenzelm@24869
   125
wenzelm@30726
   126
fun locale_expression mandatory =
ballarin@29033
   127
  let
wenzelm@30720
   128
    val expr2 = P.xname;
wenzelm@30726
   129
    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
wenzelm@30720
   130
      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
wenzelm@30720
   131
    val expr0 = plus1_unless locale_keyword expr1;
ballarin@29033
   132
  in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
ballarin@29033
   133
wenzelm@22104
   134
val context_element = P.group "context element" loc_element;
wenzelm@22104
   135
wenzelm@22104
   136
end;
wenzelm@22104
   137
wenzelm@22104
   138
wenzelm@22104
   139
(* statements *)
wenzelm@22104
   140
wenzelm@22104
   141
val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
wenzelm@22104
   142
wenzelm@22104
   143
val obtain_case =
wenzelm@30726
   144
  P.parbinding -- (Scan.optional (P.simple_fixes --| P.where_) [] --
wenzelm@22104
   145
    (P.and_list1 (Scan.repeat1 P.prop) >> flat));
wenzelm@22104
   146
wenzelm@22104
   147
val general_statement =
wenzelm@22104
   148
  statement >> (fn x => ([], Element.Shows x)) ||
ballarin@28722
   149
  Scan.repeat context_element --
wenzelm@22104
   150
   (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
wenzelm@22104
   151
    P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
wenzelm@22104
   152
wenzelm@22104
   153
val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
wenzelm@22104
   154
wenzelm@22104
   155
end;