src/Pure/Isar/parse_spec.ML
changeset 36952 338c3f8229e4
parent 36950 75b8f26f2f07
child 36955 226fb165833e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/parse_spec.ML	Sat May 15 23:32:15 2010 +0200
     1.3 @@ -0,0 +1,167 @@
     1.4 +(*  Title:      Pure/Isar/parse_spec.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Parsers for complex specifications.
     1.8 +*)
     1.9 +
    1.10 +signature PARSE_SPEC =
    1.11 +sig
    1.12 +  val attrib: Attrib.src parser
    1.13 +  val attribs: Attrib.src list parser
    1.14 +  val opt_attribs: Attrib.src list parser
    1.15 +  val thm_name: string -> Attrib.binding parser
    1.16 +  val opt_thm_name: string -> Attrib.binding parser
    1.17 +  val spec: (Attrib.binding * string) parser
    1.18 +  val specs: (Attrib.binding * string list) parser
    1.19 +  val alt_specs: (Attrib.binding * string) list parser
    1.20 +  val where_alt_specs: (Attrib.binding * string) list parser
    1.21 +  val xthm: (Facts.ref * Attrib.src list) parser
    1.22 +  val xthms1: (Facts.ref * Attrib.src list) list parser
    1.23 +  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
    1.24 +  val constdecl: (binding * string option * mixfix) parser
    1.25 +  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
    1.26 +  val locale_mixfix: mixfix parser
    1.27 +  val locale_fixes: (binding * string option * mixfix) list parser
    1.28 +  val locale_insts: (string option list * (Attrib.binding * string) list) parser
    1.29 +  val class_expr: string list parser
    1.30 +  val locale_expression: bool -> Expression.expression parser
    1.31 +  val locale_keyword: string parser
    1.32 +  val context_element: Element.context parser
    1.33 +  val statement: (Attrib.binding * (string * string list) list) list parser
    1.34 +  val general_statement: (Element.context list * Element.statement) parser
    1.35 +  val statement_keyword: string parser
    1.36 +end;
    1.37 +
    1.38 +structure Parse_Spec: PARSE_SPEC =
    1.39 +struct
    1.40 +
    1.41 +(* theorem specifications *)
    1.42 +
    1.43 +val attrib =
    1.44 +  Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
    1.45 +  >> Args.src;
    1.46 +
    1.47 +val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
    1.48 +val opt_attribs = Scan.optional attribs [];
    1.49 +
    1.50 +fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
    1.51 +
    1.52 +fun opt_thm_name s =
    1.53 +  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
    1.54 +    Attrib.empty_binding;
    1.55 +
    1.56 +val spec = opt_thm_name ":" -- Parse.prop;
    1.57 +val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
    1.58 +
    1.59 +val alt_specs =
    1.60 +  Parse.enum1 "|"
    1.61 +    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
    1.62 +
    1.63 +val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
    1.64 +
    1.65 +val xthm =
    1.66 +  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
    1.67 +  (Parse.alt_string >> Facts.Fact ||
    1.68 +    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    1.69 +
    1.70 +val xthms1 = Scan.repeat1 xthm;
    1.71 +
    1.72 +val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
    1.73 +
    1.74 +
    1.75 +(* basic constant specifications *)
    1.76 +
    1.77 +val constdecl =
    1.78 +  Parse.binding --
    1.79 +    (Parse.where_ >> K (NONE, NoSyn) ||
    1.80 +      Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
    1.81 +      Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
    1.82 +  >> Parse.triple2;
    1.83 +
    1.84 +val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
    1.85 +
    1.86 +
    1.87 +(* locale and context elements *)
    1.88 +
    1.89 +val locale_mixfix =
    1.90 +  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
    1.91 +  Parse.mixfix;
    1.92 +
    1.93 +val locale_fixes =
    1.94 +  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
    1.95 +    >> (single o Parse.triple1) ||
    1.96 +  Parse.params >> map Syntax.no_syn) >> flat;
    1.97 +
    1.98 +val locale_insts =
    1.99 +  Scan.optional
   1.100 +    (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
   1.101 +  Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
   1.102 +
   1.103 +local
   1.104 +
   1.105 +val loc_element =
   1.106 +  Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
   1.107 +  Parse.$$$ "constrains" |--
   1.108 +    Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
   1.109 +    >> Element.Constrains ||
   1.110 +  Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
   1.111 +    >> Element.Assumes ||
   1.112 +  Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
   1.113 +    >> Element.Defines ||
   1.114 +  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
   1.115 +    >> (curry Element.Notes "");
   1.116 +
   1.117 +fun plus1_unless test scan =
   1.118 +  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
   1.119 +
   1.120 +fun prefix mandatory =
   1.121 +  Parse.name --
   1.122 +    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
   1.123 +    Parse.$$$ ":";
   1.124 +
   1.125 +val instance = Parse.where_ |--
   1.126 +  Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
   1.127 +  Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
   1.128 +
   1.129 +in
   1.130 +
   1.131 +val locale_keyword =
   1.132 +  Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   1.133 +  Parse.$$$ "defines" || Parse.$$$ "notes";
   1.134 +
   1.135 +val class_expr = plus1_unless locale_keyword Parse.xname;
   1.136 +
   1.137 +fun locale_expression mandatory =
   1.138 +  let
   1.139 +    val expr2 = Parse.xname;
   1.140 +    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
   1.141 +      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
   1.142 +    val expr0 = plus1_unless locale_keyword expr1;
   1.143 +  in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
   1.144 +
   1.145 +val context_element = Parse.group "context element" loc_element;
   1.146 +
   1.147 +end;
   1.148 +
   1.149 +
   1.150 +(* statements *)
   1.151 +
   1.152 +val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
   1.153 +
   1.154 +val obtain_case =
   1.155 +  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
   1.156 +    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
   1.157 +
   1.158 +val general_statement =
   1.159 +  statement >> (fn x => ([], Element.Shows x)) ||
   1.160 +  Scan.repeat context_element --
   1.161 +   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
   1.162 +    Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
   1.163 +
   1.164 +val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
   1.165 +
   1.166 +end;
   1.167 +
   1.168 +(*legacy alias*)
   1.169 +structure SpecParse = Parse_Spec;
   1.170 +