src/Pure/Isar/parse_spec.ML
author wenzelm
Mon Nov 14 16:52:19 2011 +0100 (2011-11-14 ago)
changeset 45488 6d71d9e52369
parent 44357 5f5649ac8235
child 45592 8baa0b7f3f66
permissions -rw-r--r--
pass positions for named targets, for formal links in the document model;
     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 = Parse.position (Parse.liberal_name -- Parse.!!! Args.parse) >> Args.src;
    41 val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
    42 val opt_attribs = Scan.optional attribs [];
    43 
    44 fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
    45 
    46 fun opt_thm_name s =
    47   Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
    48     Attrib.empty_binding;
    49 
    50 val spec = opt_thm_name ":" -- Parse.prop;
    51 val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
    52 
    53 val alt_specs =
    54   Parse.enum1 "|"
    55     (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
    56 
    57 val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
    58 
    59 val xthm =
    60   Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
    61   (Parse.literal_fact >> Facts.Fact ||
    62     Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    63 
    64 val xthms1 = Scan.repeat1 xthm;
    65 
    66 val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
    67 
    68 
    69 (* basic constant specifications *)
    70 
    71 val constdecl =
    72   Parse.binding --
    73     (Parse.where_ >> K (NONE, NoSyn) ||
    74       Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
    75       Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
    76   >> Parse.triple2;
    77 
    78 val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
    79 
    80 
    81 (* locale and context elements *)
    82 
    83 val locale_mixfix =
    84   Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
    85   Parse.mixfix;
    86 
    87 val locale_fixes =
    88   Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
    89     >> (single o Parse.triple1) ||
    90   Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
    91 
    92 val locale_insts =
    93   Scan.optional
    94     (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
    95   Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
    96 
    97 local
    98 
    99 val loc_element =
   100   Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
   101   Parse.$$$ "constrains" |--
   102     Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
   103     >> Element.Constrains ||
   104   Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
   105     >> Element.Assumes ||
   106   Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
   107     >> Element.Defines ||
   108   Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
   109     >> (curry Element.Notes "");
   110 
   111 fun plus1_unless test scan =
   112   scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
   113 
   114 fun prefix mandatory =
   115   Parse.name --
   116     (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
   117     Parse.$$$ ":";
   118 
   119 val instance = Parse.where_ |--
   120   Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
   121   Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
   122 
   123 in
   124 
   125 val locale_keyword =
   126   Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   127   Parse.$$$ "defines" || Parse.$$$ "notes";
   128 
   129 val class_expr = plus1_unless locale_keyword Parse.xname;
   130 
   131 fun locale_expression mandatory =
   132   let
   133     val expr2 = Parse.xname;
   134     val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
   135       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
   136     val expr0 = plus1_unless locale_keyword expr1;
   137   in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
   138 
   139 val context_element = Parse.group (fn () => "context element") loc_element;
   140 
   141 end;
   142 
   143 
   144 (* statements *)
   145 
   146 val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
   147 
   148 val obtain_case =
   149   Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
   150     (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
   151 
   152 val general_statement =
   153   statement >> (fn x => ([], Element.Shows x)) ||
   154   Scan.repeat context_element --
   155    (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
   156     Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
   157 
   158 val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
   159 
   160 end;
   161