src/Pure/Isar/spec_parse.ML
author wenzelm
Sat Oct 06 16:50:09 2007 +0200 (2007-10-06)
changeset 24869 bad2b2be1f24
parent 24014 d3873741678d
child 25094 ba43514068fd
permissions -rw-r--r--
added class_expr;
tuned;
wenzelm@22104
     1
(*  Title:      Pure/Isar/spec_parse.ML
wenzelm@22104
     2
    ID:         $Id$
wenzelm@22104
     3
    Author:     Makarius
wenzelm@22104
     4
wenzelm@22104
     5
Parsers for complex specifications.
wenzelm@22104
     6
*)
wenzelm@22104
     7
wenzelm@22104
     8
signature SPEC_PARSE =
wenzelm@22104
     9
sig
wenzelm@22104
    10
  type token
wenzelm@22104
    11
  val attrib: OuterLex.token list -> Attrib.src * token list
wenzelm@22104
    12
  val attribs: token list -> Attrib.src list * token list
wenzelm@22104
    13
  val opt_attribs: token list -> Attrib.src list * token list
wenzelm@22104
    14
  val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
wenzelm@22104
    15
  val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
wenzelm@22104
    16
  val spec: token list -> ((bstring * Attrib.src list) * string list) * token list
wenzelm@22104
    17
  val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
wenzelm@22104
    18
  val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
wenzelm@22104
    19
  val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
wenzelm@22104
    20
  val xthm: token list -> (thmref * Attrib.src list) * token list
wenzelm@22104
    21
  val xthms1: token list -> (thmref * Attrib.src list) list * token list
wenzelm@22104
    22
  val name_facts: token list ->
wenzelm@22104
    23
    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
wenzelm@22104
    24
  val locale_mixfix: token list -> mixfix * token list
wenzelm@22104
    25
  val locale_fixes: token list -> (string * string option * mixfix) list * token list
wenzelm@24869
    26
  val locale_insts: token list -> (string option list * string list) * token list
wenzelm@24869
    27
  val class_expr: token list -> string list * token list
wenzelm@22104
    28
  val locale_expr: token list -> Locale.expr * token list
wenzelm@22104
    29
  val locale_keyword: token list -> string * token list
wenzelm@22104
    30
  val locale_element: token list -> Element.context Locale.element * token list
wenzelm@22104
    31
  val context_element: token list -> Element.context * token list
wenzelm@22104
    32
  val statement: token list ->
wenzelm@22104
    33
    ((bstring * Attrib.src list) * (string * string list) list) list * token list
wenzelm@22104
    34
  val general_statement: token list ->
wenzelm@22104
    35
    (Element.context Locale.element list * Element.statement) * OuterLex.token list
wenzelm@22104
    36
  val statement_keyword: token list -> string * token list
wenzelm@22104
    37
  val specification: token list ->
wenzelm@22104
    38
    (string *
wenzelm@22104
    39
      (((bstring * Attrib.src list) * string list) list * (string * string option) list)) list *
wenzelm@22104
    40
    token list
wenzelm@22104
    41
end;
wenzelm@22104
    42
wenzelm@22104
    43
structure SpecParse: SPEC_PARSE =
wenzelm@22104
    44
struct
wenzelm@22104
    45
wenzelm@22104
    46
structure P = OuterParse;
wenzelm@22104
    47
type token = P.token;
wenzelm@22104
    48
wenzelm@22104
    49
wenzelm@22104
    50
(* theorem specifications *)
wenzelm@22104
    51
wenzelm@22104
    52
val attrib = P.position ((P.keyword_sid || P.xname) -- P.!!! P.arguments) >> Args.src;
wenzelm@24014
    53
val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
wenzelm@22104
    54
val opt_attribs = Scan.optional attribs [];
wenzelm@22104
    55
wenzelm@22104
    56
fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
wenzelm@22104
    57
fun opt_thm_name s =
wenzelm@22104
    58
  Scan.optional ((P.name -- opt_attribs || (attribs >> pair "")) --| P.$$$ s) ("", []);
wenzelm@22104
    59
wenzelm@22104
    60
val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
wenzelm@22104
    61
val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
wenzelm@22104
    62
wenzelm@22104
    63
val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
wenzelm@22104
    64
val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
wenzelm@22104
    65
wenzelm@22104
    66
val thm_sel = P.$$$ "(" |-- P.list1
wenzelm@22104
    67
 (P.nat --| P.minus -- P.nat >> PureThy.FromTo ||
wenzelm@22104
    68
  P.nat --| P.minus >> PureThy.From ||
wenzelm@22104
    69
  P.nat >> PureThy.Single) --| P.$$$ ")";
wenzelm@22104
    70
wenzelm@24013
    71
val xthm =
wenzelm@24013
    72
  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Name "") ||
wenzelm@24013
    73
  (P.alt_string >> Fact || P.xname -- thm_sel >> NameSelection || P.xname >> Name) -- opt_attribs;
wenzelm@24013
    74
wenzelm@22104
    75
val xthms1 = Scan.repeat1 xthm;
wenzelm@22104
    76
wenzelm@22104
    77
val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
wenzelm@22104
    78
wenzelm@22104
    79
wenzelm@22104
    80
(* locale and context elements *)
wenzelm@22104
    81
wenzelm@22104
    82
val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
wenzelm@22104
    83
wenzelm@22104
    84
val locale_fixes =
wenzelm@22104
    85
  P.and_list1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
wenzelm@22104
    86
    >> (single o P.triple1) ||
wenzelm@22104
    87
  P.params >> map Syntax.no_syn) >> flat;
wenzelm@22104
    88
wenzelm@22104
    89
val locale_insts =
ballarin@22658
    90
  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
ballarin@23919
    91
  -- Scan.optional (P.$$$ "where" |-- P.and_list1 P.term) [];
wenzelm@22104
    92
wenzelm@22104
    93
local
wenzelm@22104
    94
wenzelm@22104
    95
val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
wenzelm@22104
    96
   P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";
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@22104
   110
  scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::;
wenzelm@22104
   111
wenzelm@22104
   112
val rename = P.name -- Scan.option P.mixfix;
wenzelm@22104
   113
wenzelm@24869
   114
in
wenzelm@24869
   115
wenzelm@24869
   116
val class_expr = plus1_unless loc_keyword P.xname;
wenzelm@24869
   117
wenzelm@24869
   118
val locale_expr =
wenzelm@22104
   119
  let
wenzelm@22104
   120
    fun expr2 x = (P.xname >> Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
wenzelm@22104
   121
    and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Locale.Rename || expr2) x
wenzelm@24869
   122
    and expr0 x = (plus1_unless loc_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
wenzelm@22104
   123
  in expr0 end;
wenzelm@22104
   124
wenzelm@22104
   125
val locale_keyword = loc_keyword;
wenzelm@22104
   126
wenzelm@22104
   127
val locale_element = P.group "locale element"
wenzelm@22104
   128
  (loc_element >> Locale.Elem || P.$$$ "includes" |-- P.!!! locale_expr >> Locale.Expr);
wenzelm@22104
   129
wenzelm@22104
   130
val context_element = P.group "context element" loc_element;
wenzelm@22104
   131
wenzelm@22104
   132
end;
wenzelm@22104
   133
wenzelm@22104
   134
wenzelm@22104
   135
(* statements *)
wenzelm@22104
   136
wenzelm@22104
   137
val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
wenzelm@22104
   138
wenzelm@22104
   139
val obtain_case =
wenzelm@22104
   140
  P.parname -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
wenzelm@22104
   141
    (P.and_list1 (Scan.repeat1 P.prop) >> flat));
wenzelm@22104
   142
wenzelm@22104
   143
val general_statement =
wenzelm@22104
   144
  statement >> (fn x => ([], Element.Shows x)) ||
wenzelm@22104
   145
  Scan.repeat locale_element --
wenzelm@22104
   146
   (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
wenzelm@22104
   147
    P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
wenzelm@22104
   148
wenzelm@22104
   149
val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
wenzelm@22104
   150
wenzelm@22104
   151
wenzelm@22104
   152
(* specifications *)
wenzelm@22104
   153
wenzelm@22104
   154
val specification = P.enum1 "|" (P.parname -- (P.and_list1 spec -- P.for_simple_fixes));
wenzelm@22104
   155
wenzelm@22104
   156
end;