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