src/Pure/Isar/spec_parse.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29601 93553f7c722f
child 30481 de003023c302
permissions -rw-r--r--
use long names for old-style fold combinators;
     1 (*  Title:      Pure/Isar/spec_parse.ML
     2     Author:     Makarius
     3 
     4 Parsers for complex specifications.
     5 *)
     6 
     7 signature SPEC_PARSE =
     8 sig
     9   type token = OuterParse.token
    10   type 'a parser = 'a OuterParse.parser
    11   val attrib: Attrib.src parser
    12   val attribs: Attrib.src list parser
    13   val opt_attribs: Attrib.src list parser
    14   val thm_name: string -> Attrib.binding parser
    15   val opt_thm_name: string -> Attrib.binding parser
    16   val spec: (Attrib.binding * string list) parser
    17   val named_spec: (Attrib.binding * string list) parser
    18   val spec_name: ((binding * string) * Attrib.src list) parser
    19   val spec_opt_name: ((binding * string) * Attrib.src list) parser
    20   val xthm: (Facts.ref * Attrib.src list) parser
    21   val xthms1: (Facts.ref * Attrib.src list) list parser
    22   val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
    23   val locale_mixfix: mixfix parser
    24   val locale_fixes: (binding * string option * mixfix) list parser
    25   val locale_insts: (string option list * (Attrib.binding * string) list) parser
    26   val class_expr: string list parser
    27   val locale_expression: Expression.expression parser
    28   val locale_keyword: string parser
    29   val context_element: Element.context parser
    30   val statement: (Attrib.binding * (string * string list) list) list parser
    31   val general_statement: (Element.context list * Element.statement) parser
    32   val statement_keyword: string parser
    33   val specification:
    34     (binding * ((Attrib.binding * string list) list * (binding * string option) list)) list parser
    35 end;
    36 
    37 structure SpecParse: SPEC_PARSE =
    38 struct
    39 
    40 structure P = OuterParse;
    41 type token = P.token;
    42 type 'a parser = 'a P.parser;
    43 
    44 
    45 (* theorem specifications *)
    46 
    47 val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src;
    48 val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
    49 val opt_attribs = Scan.optional attribs [];
    50 
    51 fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
    52 
    53 fun opt_thm_name s =
    54   Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
    55     Attrib.empty_binding;
    56 
    57 val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
    58 val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
    59 
    60 val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    61 val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    62 
    63 val xthm =
    64   P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
    65   (P.alt_string >> Facts.Fact ||
    66     P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    67 
    68 val xthms1 = Scan.repeat1 xthm;
    69 
    70 val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
    71 
    72 
    73 (* locale and context elements *)
    74 
    75 val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
    76 
    77 val locale_fixes =
    78   P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
    79     >> (single o P.triple1) ||
    80   P.params >> map Syntax.no_syn) >> flat;
    81 
    82 val locale_insts =
    83   Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
    84   -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
    85 
    86 local
    87 
    88 val loc_element =
    89   P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
    90   P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
    91     >> Element.Constrains ||
    92   P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp))
    93     >> Element.Assumes ||
    94   P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp))
    95     >> Element.Defines ||
    96   P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
    97     >> (curry Element.Notes "");
    98 
    99 fun plus1_unless test scan =
   100   scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
   101 
   102 val rename = P.name -- Scan.option P.mixfix;
   103 
   104 val prefix = P.name -- Scan.optional (P.$$$ "!" >> K true) false --| P.$$$ ":";
   105 val named = P.name -- (P.$$$ "=" |-- P.term);
   106 val position = P.maybe P.term;
   107 val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
   108   Scan.repeat1 position >> Expression.Positional;
   109 
   110 in
   111 
   112 val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
   113    P.$$$ "defines" || P.$$$ "notes";
   114 
   115 val class_expr = plus1_unless locale_keyword P.xname;
   116 
   117 val locale_expression =
   118   let
   119     fun expr2 x = P.xname x;
   120     fun expr1 x = (Scan.optional prefix ("", false) -- expr2 --
   121       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
   122     fun expr0 x = (plus1_unless locale_keyword expr1) x;
   123   in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
   124 
   125 val context_element = P.group "context element" loc_element;
   126 
   127 end;
   128 
   129 
   130 (* statements *)
   131 
   132 val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
   133 
   134 val obtain_case =
   135   P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
   136     (P.and_list1 (Scan.repeat1 P.prop) >> flat));
   137 
   138 val general_statement =
   139   statement >> (fn x => ([], Element.Shows x)) ||
   140   Scan.repeat context_element --
   141    (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
   142     P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
   143 
   144 val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
   145 
   146 
   147 (* specifications *)
   148 
   149 val specification = P.enum1 "|" (P.parbinding -- (P.and_list1 spec -- P.for_simple_fixes));
   150 
   151 end;