src/Pure/Isar/spec_parse.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 33287 0f99569d23e1
child 36950 75b8f26f2f07
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
     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   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 SpecParse: SPEC_PARSE =
    36 struct
    37 
    38 structure P = OuterParse;
    39 
    40 
    41 (* theorem specifications *)
    42 
    43 val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src;
    44 val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
    45 val opt_attribs = Scan.optional attribs [];
    46 
    47 fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
    48 
    49 fun opt_thm_name s =
    50   Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
    51     Attrib.empty_binding;
    52 
    53 val spec = opt_thm_name ":" -- P.prop;
    54 val specs = opt_thm_name ":" -- Scan.repeat1 P.prop;
    55 
    56 val alt_specs =
    57   P.enum1 "|" (spec --| Scan.option (Scan.ahead (P.name || P.$$$ "[") -- P.!!! (P.$$$ "|")));
    58 
    59 val where_alt_specs = P.where_ |-- P.!!! alt_specs;
    60 
    61 val xthm =
    62   P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
    63   (P.alt_string >> Facts.Fact ||
    64     P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    65 
    66 val xthms1 = Scan.repeat1 xthm;
    67 
    68 val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
    69 
    70 
    71 (* basic constant specifications *)
    72 
    73 val constdecl =
    74   P.binding --
    75     (P.where_ >> K (NONE, NoSyn) ||
    76       P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
    77       Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
    78   >> P.triple2;
    79 
    80 val constdef = Scan.option constdecl -- (opt_thm_name ":" -- P.prop);
    81 
    82 
    83 (* locale and context elements *)
    84 
    85 val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
    86 
    87 val locale_fixes =
    88   P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
    89     >> (single o P.triple1) ||
    90   P.params >> map Syntax.no_syn) >> flat;
    91 
    92 val locale_insts =
    93   Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
    94   -- Scan.optional (P.where_ |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
    95 
    96 local
    97 
    98 val loc_element =
    99   P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
   100   P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
   101     >> Element.Constrains ||
   102   P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp))
   103     >> Element.Assumes ||
   104   P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp))
   105     >> Element.Defines ||
   106   P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
   107     >> (curry Element.Notes "");
   108 
   109 fun plus1_unless test scan =
   110   scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
   111 
   112 fun prefix mandatory =
   113   P.name -- (P.$$$ "!" >> K true || P.$$$ "?" >> K false || Scan.succeed mandatory) --| P.$$$ ":";
   114 
   115 val instance = P.where_ |--
   116   P.and_list1 (P.name -- (P.$$$ "=" |-- P.term)) >> Expression.Named ||
   117   Scan.repeat1 (P.maybe P.term) >> Expression.Positional;
   118 
   119 in
   120 
   121 val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
   122    P.$$$ "defines" || P.$$$ "notes";
   123 
   124 val class_expr = plus1_unless locale_keyword P.xname;
   125 
   126 fun locale_expression mandatory =
   127   let
   128     val expr2 = P.xname;
   129     val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
   130       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
   131     val expr0 = plus1_unless locale_keyword expr1;
   132   in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
   133 
   134 val context_element = P.group "context element" loc_element;
   135 
   136 end;
   137 
   138 
   139 (* statements *)
   140 
   141 val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
   142 
   143 val obtain_case =
   144   P.parbinding -- (Scan.optional (P.simple_fixes --| P.where_) [] --
   145     (P.and_list1 (Scan.repeat1 P.prop) >> flat));
   146 
   147 val general_statement =
   148   statement >> (fn x => ([], Element.Shows x)) ||
   149   Scan.repeat context_element --
   150    (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
   151     P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
   152 
   153 val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
   154 
   155 end;