Core-3 grammar

(* Core-3 overlay on Core-2/Core-1/Core-0.
   Append proof-declaration and intent-declaration to
   implementation-top-level-declaration. Append proof-interface-declaration
   and intent-declaration to generated-interface-top-level-declaration. Replace effect only;
   preserve the six domain alternatives and their numeric tags.
   New words are contextual in these productions, not new old-edition keywords.
   qualified-name, visibility, identifier, string-literal, decimal-digit,
   and type are inherited. Free English remains outside the grammar.
   Every example using a declaration fragment assumes an enclosing module. *)

effect = "io" | "alloc" | "time" | "random" | "reflect" | "unsafe"
       | "abort" | "compute" | "state" | "flow" | "optimize"
       | "hardware" | "physics" | "intent" ;

proof-declaration = visibility , "proof" , "namespace" , qualified-name ,
                    "{" , { proof-item } , "}" ;
proof-interface-declaration = visibility , "proof" , "namespace" , qualified-name ,
                             "{" , { proof-interface-item } , "}" ;
proof-item = proof-universe | proof-definition | proof-axiom | proof-inductive
           | proof-verification | proof-extraction ;
proof-interface-item = proof-universe | proof-signature | proof-axiom
                     | proof-inductive ;
proof-universe = "universe" , identifier , { "," , identifier } , ";" ;
proof-level-parameters = "<" , identifier , { "," , identifier } , ">" ;
proof-profile-list = "using" , "(" ,
    [ string-literal , { "," , string-literal } ] , ")" ;
proof-definition-header = ( "define" | "opaque" | "theorem" ) , identifier ,
    [ proof-level-parameters ] , ":" , proof-term , proof-profile-list ;
proof-definition = proof-definition-header , "=" , proof-term , ";" ;
proof-signature = proof-definition-header , ";" ;
proof-axiom = "axiom" , identifier , [ proof-level-parameters ] , ":" ,
              proof-term , "profile" , string-literal , ";" ;
proof-inductive = "inductive" , identifier , [ proof-level-parameters ] ,
    { proof-binder } , ":" , proof-term , "{" ,
    { identifier , ":" , proof-term , ";" } , "}" ;
proof-verification = "verify" , identifier , ":" , proof-term ,
    "subject" , qualified-name , "model" , qualified-name ,
    "mode" , ( "partial" | "total" ) , proof-profile-list ,
    "by" , proof-term , ";" ;
proof-extraction = "extract" , identifier , "from" , qualified-name ,
    "contract" , qualified-name , ";" ;

proof-term = "forall" , proof-binder , { proof-binder } , "->" , proof-term
           | "fun" , proof-binder , { proof-binder } , "=>" , proof-term
           | "let" , proof-binder , "=" , proof-term , "in" , proof-term
           | proof-application ;
proof-binder = "(" , identifier , ":" , proof-term , ")" ;
proof-application = proof-atom ,
    { "(" , proof-term , { "," , proof-term } , ")" } ;
proof-atom = "Prop"
           | ( "Sort" | "Type" ) , "(" , proof-level , ")"
           | qualified-name , [ "<" , proof-level , { "," , proof-level } , ">" ]
           | "(" , proof-term , ")" ;
proof-level = proof-natural | identifier
            | "succ" , "(" , proof-level , ")"
            | ( "max" | "imax" ) , "(" , proof-level , "," , proof-level , ")" ;
proof-natural = decimal-digit , { decimal-digit } ;

intent-declaration = visibility , "intent" , identifier ,
    "(" , [ intent-parameter , { "," , intent-parameter } ] , ")" , "->" , type , effect-clause ,
    "{" , "authority" , string-literal , ";" ,
    "policy" , qualified-name , ";" ,
    intent-requirement , { intent-requirement } ,
    { intent-formalization } , "}" ;
intent-parameter = identifier , ":" , type ;
intent-requirement = "requirement" , identifier , ":" , string-literal , ";" ;
intent-formalization = "formalize" , identifier , "with" , qualified-name , ";" ;