src/Pure/Isar/parse_spec.ML
author wenzelm
Sun Nov 28 20:03:19 2010 +0100 (2010-11-28)
changeset 40793 d21aedaa91e7
parent 36955 226fb165833e
child 40800 330eb65c9469
permissions -rw-r--r--
added Parse.literal_fact with proper inner_syntax markup (source position);
tuned;
     1 (*  Title:      Pure/Isar/parse_spec.ML
     2     Author:     Makarius
     3 
     4 Parsers for complex specifications.
     5 *)
     6 
     7 signature PARSE_SPEC =
     8 sig
     9   val attrib: Attrib.src parser
    10   val attribs: Attrib.src list parser
    11   val opt_attribs: Attrib.src list parser
    12   val thm_name: string -> Attrib.binding parser
    13   val opt_thm_name: string -> Attrib.binding parser
    14   val spec: (Attrib.binding * string) parser
    15   val specs: (Attrib.binding * string list) parser
    16   val alt_specs: (Attrib.binding * string) list parser
    17   val where_alt_specs: (Attrib.binding * string) list parser
    18   val xthm: (Facts.ref * Attrib.src list) parser
    19   val xthms1: (Facts.ref * Attrib.src list) list parser
    20   val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
    21   val constdecl: (binding * string option * mixfix) parser
    22   val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) 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: bool -> 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 end;
    34 
    35 structure Parse_Spec: PARSE_SPEC =
    36 struct
    37 
    38 (* theorem specifications *)
    39 
    40 val attrib =
    41   Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
    42   >> Args.src;
    43 
    44 val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
    45 val opt_attribs = Scan.optional attribs [];
    46 
    47 fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
    48 
    49 fun opt_thm_name s =
    50   Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
    51     Attrib.empty_binding;
    52 
    53 val spec = opt_thm_name ":" -- Parse.prop;
    54 val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
    55 
    56 val alt_specs =
    57   Parse.enum1 "|"
    58     (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
    59 
    60 val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
    61 
    62 val xthm =
    63   Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
    64   (Parse.literal_fact >> Facts.Fact ||
    65     Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    66 
    67 val xthms1 = Scan.repeat1 xthm;
    68 
    69 val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
    70 
    71 
    72 (* basic constant specifications *)
    73 
    74 val constdecl =
    75   Parse.binding --
    76     (Parse.where_ >> K (NONE, NoSyn) ||
    77       Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
    78       Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
    79   >> Parse.triple2;
    80 
    81 val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
    82 
    83 
    84 (* locale and context elements *)
    85 
    86 val locale_mixfix =
    87   Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
    88   Parse.mixfix;
    89 
    90 val locale_fixes =
    91   Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
    92     >> (single o Parse.triple1) ||
    93   Parse.params >> map Syntax.no_syn) >> flat;
    94 
    95 val locale_insts =
    96   Scan.optional
    97     (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
    98   Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
    99 
   100 local
   101 
   102 val loc_element =
   103   Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
   104   Parse.$$$ "constrains" |--
   105     Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
   106     >> Element.Constrains ||
   107   Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
   108     >> Element.Assumes ||
   109   Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
   110     >> Element.Defines ||
   111   Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
   112     >> (curry Element.Notes "");
   113 
   114 fun plus1_unless test scan =
   115   scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
   116 
   117 fun prefix mandatory =
   118   Parse.name --
   119     (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
   120     Parse.$$$ ":";
   121 
   122 val instance = Parse.where_ |--
   123   Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
   124   Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
   125 
   126 in
   127 
   128 val locale_keyword =
   129   Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   130   Parse.$$$ "defines" || Parse.$$$ "notes";
   131 
   132 val class_expr = plus1_unless locale_keyword Parse.xname;
   133 
   134 fun locale_expression mandatory =
   135   let
   136     val expr2 = Parse.xname;
   137     val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
   138       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
   139     val expr0 = plus1_unless locale_keyword expr1;
   140   in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
   141 
   142 val context_element = Parse.group "context element" loc_element;
   143 
   144 end;
   145 
   146 
   147 (* statements *)
   148 
   149 val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
   150 
   151 val obtain_case =
   152   Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
   153     (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
   154 
   155 val general_statement =
   156   statement >> (fn x => ([], Element.Shows x)) ||
   157   Scan.repeat context_element --
   158    (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
   159     Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
   160 
   161 val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
   162 
   163 end;
   164