+ theorem_flavour: [ (* all flavours but Goal *)
+ [ [ IDENT "definition" | IDENT "Definition" ] -> `Definition
+ | [ IDENT "fact" | IDENT "Fact" ] -> `Fact
+ | [ IDENT "lemma" | IDENT "Lemma" ] -> `Lemma
+ | [ IDENT "remark" | IDENT "Remark" ] -> `Remark
+ | [ IDENT "theorem" | IDENT "Theorem" ] -> `Theorem
+(* | [ IDENT "goal" | IDENT "Goal" ] -> `Goal *)
+ ]
+ ];
+ theorem_cmd: [
+ [ flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ];
+ SYMBOL "." ->
+ (loc, flavour, name, typ, body)
+ | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ];
+ SYMBOL "." ->
+ (loc, `Goal, None, typ, body)
+ ]
+ ];
+ proof_cmd: [ [ [ IDENT "proof" | IDENT "Proof" ]; SYMBOL "." -> loc ] ];
+ qed_cmd: [
+ [ [ IDENT "qed" | IDENT "Qed" ]; SYMBOL "." -> (loc, None)
+ | [ IDENT "save" | IDENT "Save" ]; name = IDENT; SYMBOL "." ->
+ (loc, Some name)
+ ]
+ ];
+ command: [
+ [ (loc', flavour, name, typ, body) = theorem_cmd ->
+ return_command loc (CommandAst.Theorem (loc', flavour, name, typ, body))
+ | (loc') = proof_cmd -> return_command loc (CommandAst.Proof loc')
+ | (loc, name) = qed_cmd -> return_command loc (CommandAst.Qed (loc, name))
+ ]
+ ];
+ script_entry: [
+ [ theorem = theorem_cmd;
+ proof = OPT [
+ proof_cmd; tacticals = LIST1 tactical0; qed = qed_cmd ->
+ (tacticals, qed)
+ ] ->
+ let (loc', flavour, name', typ, body_verbatim) = theorem in
+ let name'' =
+ match proof with
+ | None | Some (_, (_, None)) -> None
+ | Some (_, (_, Some name)) -> Some name
+ in
+ let name =
+ match (name', name'') with
+ | Some name, None -> name
+ | None, Some name -> name
+ | None, None ->
+ Stdpp.raise_with_loc loc (Failure "theorem's name is missing")
+ | Some name', Some name'' when name' <> name'' ->
+ Stdpp.raise_with_loc loc (Failure (sprintf
+ "theorem's name mismatch: %s <> %s" name' name''))
+ | Some name, _ -> name
+ in
+ let body =
+ match (body_verbatim, proof) with
+ | Some term, None -> CommandAst.Script.Verbatim (loc', term)
+ | None, Some (tacticals, (loc'', _)) ->
+ CommandAst.Script.Tactics (loc'', tacticals)
+ | Some _, Some _ ->
+ Stdpp.raise_with_loc loc (Failure (sprintf
+ "theorem %s has too many proofs" name))
+ | None, None ->
+ Stdpp.raise_with_loc loc (Failure (sprintf
+ "theorem %s has no proof" name))
+ in
+ return_script loc (CommandAst.Script.Theorem (flavour, name, typ, body))
+ ]
+ ];
+ script: [ [ entries = LIST0 script_entry; EOI -> entries ] ];