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