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