(*  Title:      Pure/Isar/spec_parse.ML

     Author:     Makarius

 Parsers for complex specifications.

 *)

 signature SPEC_PARSE =

 sig

   val attrib: Attrib.src parser

   val attribs: Attrib.src list parser

   val opt_attribs: Attrib.src list parser

   val thm_name: string -> Attrib.binding parser

   val opt_thm_name: string -> Attrib.binding parser

   val spec: (Attrib.binding * string) parser

   val specs: (Attrib.binding * string list) parser

   val alt_specs: (Attrib.binding * string) list parser

   val where_alt_specs: (Attrib.binding * string) list parser

   val xthm: (Facts.ref * Attrib.src list) parser

   val xthms1: (Facts.ref * Attrib.src list) list parser

   val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser

   val constdecl: (binding * string option * mixfix) parser

   val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser

   val locale_mixfix: mixfix parser

   val locale_fixes: (binding * string option * mixfix) list parser

   val locale_insts: (string option list * (Attrib.binding * string) list) parser

   val class_expr: string list parser

   val locale_expression: bool -> Expression.expression parser

   val locale_keyword: string parser

   val context_element: Element.context parser

   val statement: (Attrib.binding * (string * string list) list) list parser

   val general_statement: (Element.context list * Element.statement) parser

   val statement_keyword: string parser

 end;

 structure SpecParse: SPEC_PARSE =

 struct

 (* theorem specifications *)

 val attrib =

   Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)

   >> Args.src;

 val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";

 val opt_attribs = Scan.optional attribs [];

 fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;

 fun opt_thm_name s =

   Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)

     Attrib.empty_binding;

 val spec = opt_thm_name ":" -- Parse.prop;

 val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;

 val alt_specs =

   Parse.enum1 "|"

     (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));

 val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;

 val xthm =

   Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||

   (Parse.alt_string >> Facts.Fact ||

     Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;

 val xthms1 = Scan.repeat1 xthm;

 val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);

 (* basic constant specifications *)

 val constdecl =

   Parse.binding --

     (Parse.where_ >> K (NONE, NoSyn) ||

       Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||

       Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))

   >> Parse.triple2;

 val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);

 (* locale and context elements *)

 val locale_mixfix =

   Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||

   Parse.mixfix;

 val locale_fixes =

   Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix

     >> (single o Parse.triple1) ||

   Parse.params >> map Syntax.no_syn) >> flat;

 val locale_insts =

   Scan.optional

     (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --

   Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];

 local

 val loc_element =

   Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||

   Parse.$$$ "constrains" |--

     Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))

     >> Element.Constrains ||

   Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))

     >> Element.Assumes ||

   Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))

     >> Element.Defines ||

   Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))

     >> (curry Element.Notes "");

 fun plus1_unless test scan =

   scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));

 fun prefix mandatory =

   Parse.name --

     (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|

     Parse.$$$ ":";

 val instance = Parse.where_ |--

   Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||

   Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;

 in

 val locale_keyword =

   Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||

   Parse.$$$ "defines" || Parse.$$$ "notes";

 val class_expr = plus1_unless locale_keyword Parse.xname;

 fun locale_expression mandatory =

   let

     val expr2 = Parse.xname;

     val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --

       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));

     val expr0 = plus1_unless locale_keyword expr1;

   in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;

 val context_element = Parse.group "context element" loc_element;

 end;

 (* statements *)

 val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);

 val obtain_case =

   Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --

     (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));

 val general_statement =

   statement >> (fn x => ([], Element.Shows x)) ||

   Scan.repeat context_element --

    (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||

     Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);

 val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";

 end;