1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Fri Jan 19 22:08:12 2007 +0100
     1.3 @@ -0,0 +1,153 @@
     1.4 +(*  Title:      Pure/Isar/spec_parse.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Parsers for complex specifications.
     1.9 +*)
    1.10 +
    1.11 +signature SPEC_PARSE =
    1.12 +sig
    1.13 +  type token
    1.14 +  val attrib: OuterLex.token list -> Attrib.src * token list
    1.15 +  val attribs: token list -> Attrib.src list * token list
    1.16 +  val opt_attribs: token list -> Attrib.src list * token list
    1.17 +  val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
    1.18 +  val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
    1.19 +  val spec: token list -> ((bstring * Attrib.src list) * string list) * token list
    1.20 +  val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
    1.21 +  val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
    1.22 +  val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
    1.23 +  val xthm: token list -> (thmref * Attrib.src list) * token list
    1.24 +  val xthms1: token list -> (thmref * Attrib.src list) list * token list
    1.25 +  val name_facts: token list ->
    1.26 +    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
    1.27 +  val locale_mixfix: token list -> mixfix * token list
    1.28 +  val locale_fixes: token list -> (string * string option * mixfix) list * token list
    1.29 +  val locale_insts: token list -> string option list * token list
    1.30 +  val locale_expr: token list -> Locale.expr * token list
    1.31 +  val locale_expr_unless: (token list -> 'a * token list) ->
    1.32 +    token list -> Locale.expr * token list
    1.33 +  val locale_keyword: token list -> string * token list
    1.34 +  val locale_element: token list -> Element.context Locale.element * token list
    1.35 +  val context_element: token list -> Element.context * token list
    1.36 +  val statement: token list ->
    1.37 +    ((bstring * Attrib.src list) * (string * string list) list) list * token list
    1.38 +  val general_statement: token list ->
    1.39 +    (Element.context Locale.element list * Element.statement) * OuterLex.token list
    1.40 +  val statement_keyword: token list -> string * token list
    1.41 +  val specification: token list ->
    1.42 +    (string *
    1.43 +      (((bstring * Attrib.src list) * string list) list * (string * string option) list)) list *
    1.44 +    token list
    1.45 +end;
    1.46 +
    1.47 +structure SpecParse: SPEC_PARSE =
    1.48 +struct
    1.49 +
    1.50 +structure P = OuterParse;
    1.51 +type token = P.token;
    1.52 +
    1.53 +
    1.54 +(* theorem specifications *)
    1.55 +
    1.56 +val attrib = P.position ((P.keyword_sid || P.xname) -- P.!!! P.arguments) >> Args.src;
    1.57 +val attribs = P.$$$ "[" |-- P.!!! (P.list attrib --| P.$$$ "]");
    1.58 +val opt_attribs = Scan.optional attribs [];
    1.59 +
    1.60 +fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
    1.61 +fun opt_thm_name s =
    1.62 +  Scan.optional ((P.name -- opt_attribs || (attribs >> pair "")) --| P.$$$ s) ("", []);
    1.63 +
    1.64 +val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
    1.65 +val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
    1.66 +
    1.67 +val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    1.68 +val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    1.69 +
    1.70 +val thm_sel = P.$$$ "(" |-- P.list1
    1.71 + (P.nat --| P.minus -- P.nat >> PureThy.FromTo ||
    1.72 +  P.nat --| P.minus >> PureThy.From ||
    1.73 +  P.nat >> PureThy.Single) --| P.$$$ ")";
    1.74 +
    1.75 +val xthm = (P.alt_string >> Fact || P.xname -- thm_sel >> NameSelection || P.xname >> Name)
    1.76 +  -- opt_attribs;
    1.77 +val xthms1 = Scan.repeat1 xthm;
    1.78 +
    1.79 +val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
    1.80 +
    1.81 +
    1.82 +(* locale and context elements *)
    1.83 +
    1.84 +val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
    1.85 +
    1.86 +val locale_fixes =
    1.87 +  P.and_list1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
    1.88 +    >> (single o P.triple1) ||
    1.89 +  P.params >> map Syntax.no_syn) >> flat;
    1.90 +
    1.91 +val locale_insts =
    1.92 +  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];
    1.93 +
    1.94 +local
    1.95 +
    1.96 +val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    1.97 +   P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";
    1.98 +
    1.99 +val loc_element =
   1.100 +  P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
   1.101 +  P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
   1.102 +    >> Element.Constrains ||
   1.103 +  P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp))
   1.104 +    >> Element.Assumes ||
   1.105 +  P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp))
   1.106 +    >> Element.Defines ||
   1.107 +  P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
   1.108 +    >> (curry Element.Notes "");
   1.109 +
   1.110 +fun plus1 test scan =
   1.111 +  scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::;
   1.112 +
   1.113 +val rename = P.name -- Scan.option P.mixfix;
   1.114 +
   1.115 +fun expr test =
   1.116 +  let
   1.117 +    fun expr2 x = (P.xname >> Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
   1.118 +    and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Locale.Rename || expr2) x
   1.119 +    and expr0 x = (plus1 test expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
   1.120 +  in expr0 end;
   1.121 +in
   1.122 +
   1.123 +val locale_expr_unless = expr
   1.124 +val locale_expr = expr loc_keyword;
   1.125 +val locale_keyword = loc_keyword;
   1.126 +
   1.127 +val locale_element = P.group "locale element"
   1.128 +  (loc_element >> Locale.Elem || P.$$$ "includes" |-- P.!!! locale_expr >> Locale.Expr);
   1.129 +
   1.130 +val context_element = P.group "context element" loc_element;
   1.131 +
   1.132 +end;
   1.133 +
   1.134 +
   1.135 +(* statements *)
   1.136 +
   1.137 +val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
   1.138 +
   1.139 +val obtain_case =
   1.140 +  P.parname -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
   1.141 +    (P.and_list1 (Scan.repeat1 P.prop) >> flat));
   1.142 +
   1.143 +val general_statement =
   1.144 +  statement >> (fn x => ([], Element.Shows x)) ||
   1.145 +  Scan.repeat locale_element --
   1.146 +   (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
   1.147 +    P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
   1.148 +
   1.149 +val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
   1.150 +
   1.151 +
   1.152 +(* specifications *)
   1.153 +
   1.154 +val specification = P.enum1 "|" (P.parname -- (P.and_list1 spec -- P.for_simple_fixes));
   1.155 +
   1.156 +end;