src/Pure/Isar/spec_parse.ML
author haftmann
Mon Jan 05 15:55:04 2009 +0100 (2009-01-05)
changeset 29360 a5be60c3674e
parent 29312 f369fb19146e
child 29581 b3b33e0298eb
permissions -rw-r--r--
locale -> old_locale, new_locale -> locale
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
  type token = OuterParse.token
wenzelm@29312
    10
  type 'a parser = 'a OuterParse.parser
wenzelm@29312
    11
  val attrib: Attrib.src parser
wenzelm@29312
    12
  val attribs: Attrib.src list parser
wenzelm@29312
    13
  val opt_attribs: Attrib.src list parser
wenzelm@29312
    14
  val thm_name: string -> Attrib.binding parser
wenzelm@29312
    15
  val opt_thm_name: string -> Attrib.binding parser
wenzelm@29312
    16
  val spec: (Attrib.binding * string list) parser
wenzelm@29312
    17
  val named_spec: (Attrib.binding * string list) parser
wenzelm@29312
    18
  val spec_name: ((Binding.T * string) * Attrib.src list) parser
wenzelm@29312
    19
  val spec_opt_name: ((Binding.T * string) * Attrib.src list) parser
wenzelm@29312
    20
  val xthm: (Facts.ref * Attrib.src list) parser
wenzelm@29312
    21
  val xthms1: (Facts.ref * Attrib.src list) list parser
wenzelm@29312
    22
  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
wenzelm@29312
    23
  val locale_mixfix: mixfix parser
wenzelm@29312
    24
  val locale_fixes: (Binding.T * 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
haftmann@29360
    27
  val locale_expr: Old_Locale.expr parser
wenzelm@29312
    28
  val locale_expression: Expression.expression parser
wenzelm@29312
    29
  val locale_keyword: string parser
wenzelm@29312
    30
  val context_element: Element.context parser
wenzelm@29312
    31
  val statement: (Attrib.binding * (string * string list) list) list parser
wenzelm@29312
    32
  val general_statement: (Element.context list * Element.statement) parser
wenzelm@29312
    33
  val statement_keyword: string parser
wenzelm@29312
    34
  val specification:
wenzelm@29312
    35
    (Binding.T * ((Attrib.binding * string list) list * (Binding.T * string option) list)) list parser
wenzelm@22104
    36
end;
wenzelm@22104
    37
wenzelm@22104
    38
structure SpecParse: SPEC_PARSE =
wenzelm@22104
    39
struct
wenzelm@22104
    40
wenzelm@22104
    41
structure P = OuterParse;
wenzelm@22104
    42
type token = P.token;
wenzelm@29312
    43
type 'a parser = 'a P.parser;
wenzelm@22104
    44
wenzelm@22104
    45
wenzelm@22104
    46
(* theorem specifications *)
wenzelm@22104
    47
wenzelm@27816
    48
val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src;
wenzelm@24014
    49
val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
wenzelm@22104
    50
val opt_attribs = Scan.optional attribs [];
wenzelm@22104
    51
wenzelm@28083
    52
fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
wenzelm@28083
    53
wenzelm@22104
    54
fun opt_thm_name s =
haftmann@28965
    55
  Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
haftmann@28965
    56
    Attrib.empty_binding;
wenzelm@22104
    57
wenzelm@22104
    58
val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
wenzelm@22104
    59
val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
wenzelm@22104
    60
wenzelm@22104
    61
val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
wenzelm@22104
    62
val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
wenzelm@22104
    63
wenzelm@24013
    64
val xthm =
wenzelm@26361
    65
  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
wenzelm@26361
    66
  (P.alt_string >> Facts.Fact ||
wenzelm@27816
    67
    P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
wenzelm@24013
    68
wenzelm@22104
    69
val xthms1 = Scan.repeat1 xthm;
wenzelm@22104
    70
wenzelm@22104
    71
val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
wenzelm@22104
    72
wenzelm@22104
    73
wenzelm@22104
    74
(* locale and context elements *)
wenzelm@22104
    75
wenzelm@22104
    76
val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
wenzelm@22104
    77
wenzelm@22104
    78
val locale_fixes =
wenzelm@28083
    79
  P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
wenzelm@22104
    80
    >> (single o P.triple1) ||
wenzelm@22104
    81
  P.params >> map Syntax.no_syn) >> flat;
wenzelm@22104
    82
wenzelm@22104
    83
val locale_insts =
ballarin@22658
    84
  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
ballarin@25094
    85
  -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
wenzelm@22104
    86
wenzelm@22104
    87
local
wenzelm@22104
    88
wenzelm@22104
    89
val loc_element =
wenzelm@22104
    90
  P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
wenzelm@22104
    91
  P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
wenzelm@22104
    92
    >> Element.Constrains ||
wenzelm@22104
    93
  P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp))
wenzelm@22104
    94
    >> Element.Assumes ||
wenzelm@22104
    95
  P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp))
wenzelm@22104
    96
    >> Element.Defines ||
wenzelm@22104
    97
  P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
wenzelm@22104
    98
    >> (curry Element.Notes "");
wenzelm@22104
    99
wenzelm@24869
   100
fun plus1_unless test scan =
wenzelm@25999
   101
  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
wenzelm@22104
   102
wenzelm@22104
   103
val rename = P.name -- Scan.option P.mixfix;
wenzelm@22104
   104
ballarin@29214
   105
val prefix = P.name -- Scan.optional (P.$$$ "!" >> K true) false --| P.$$$ ":";
ballarin@29033
   106
val named = P.name -- (P.$$$ "=" |-- P.term);
ballarin@29033
   107
val position = P.maybe P.term;
ballarin@29033
   108
val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
ballarin@29033
   109
  Scan.repeat1 position >> Expression.Positional;
ballarin@29033
   110
wenzelm@24869
   111
in
wenzelm@24869
   112
ballarin@28722
   113
val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
ballarin@28722
   114
   P.$$$ "defines" || P.$$$ "notes";
ballarin@28722
   115
ballarin@28722
   116
val class_expr = plus1_unless locale_keyword P.xname;
wenzelm@24869
   117
wenzelm@24869
   118
val locale_expr =
wenzelm@22104
   119
  let
haftmann@29360
   120
    fun expr2 x = (P.xname >> Old_Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
haftmann@29360
   121
    and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Old_Locale.Rename || expr2) x
haftmann@29360
   122
    and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Old_Locale.Merge es)) x;
wenzelm@22104
   123
  in expr0 end;
wenzelm@22104
   124
ballarin@29033
   125
val locale_expression =
ballarin@29033
   126
  let
ballarin@29033
   127
    fun expr2 x = P.xname x;
ballarin@29214
   128
    fun expr1 x = (Scan.optional prefix ("", false) -- expr2 --
ballarin@29033
   129
      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
ballarin@29033
   130
    fun expr0 x = (plus1_unless locale_keyword expr1) x;
ballarin@29033
   131
  in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
ballarin@29033
   132
wenzelm@22104
   133
val context_element = P.group "context element" loc_element;
wenzelm@22104
   134
wenzelm@22104
   135
end;
wenzelm@22104
   136
wenzelm@22104
   137
wenzelm@22104
   138
(* statements *)
wenzelm@22104
   139
wenzelm@22104
   140
val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
wenzelm@22104
   141
wenzelm@22104
   142
val obtain_case =
wenzelm@28083
   143
  P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
wenzelm@22104
   144
    (P.and_list1 (Scan.repeat1 P.prop) >> flat));
wenzelm@22104
   145
wenzelm@22104
   146
val general_statement =
wenzelm@22104
   147
  statement >> (fn x => ([], Element.Shows x)) ||
ballarin@28722
   148
  Scan.repeat context_element --
wenzelm@22104
   149
   (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
wenzelm@22104
   150
    P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
wenzelm@22104
   151
wenzelm@22104
   152
val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
wenzelm@22104
   153
wenzelm@22104
   154
wenzelm@22104
   155
(* specifications *)
wenzelm@22104
   156
wenzelm@28083
   157
val specification = P.enum1 "|" (P.parbinding -- (P.and_list1 spec -- P.for_simple_fixes));
wenzelm@22104
   158
wenzelm@22104
   159
end;