- tactical0 : [ [ t = tactical; SYMBOL "." -> t ] ];
- tactical: [
- [ IDENT "fail" -> return_tactical loc TacticAst.Fail
- | IDENT "do"; count = int; tac = tactical ->
- return_tactical loc (TacticAst.Do (count, tac))
- | IDENT "id" -> return_tactical loc TacticAst.IdTac
- | IDENT "repeat"; tac = tactical ->
- return_tactical loc (TacticAst.Repeat tac)
- | tactics = LIST0 tactical SEP SYMBOL ";" ->
- return_tactical loc (TacticAst.Seq tactics)
- | tac = tactical;
- PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
- return_tactical loc (TacticAst.Then (tac, tacs))
- | IDENT "tries";
- PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
- return_tactical loc (TacticAst.Tries tacs)
- | IDENT "try"; tac = tactical -> return_tactical loc (TacticAst.Try tac)
- | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
- | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
+ tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
+ tactical:
+ [ "sequence" LEFTA
+ [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
+ return_tactical loc (TacticAst.Seq tactics)
+ ]
+ | "then" NONA
+ [ tac = tactical;
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+ return_tactical loc (TacticAst.Then (tac, tacs))
+ ]
+ | "loops" RIGHTA
+ [ [ IDENT "do" | IDENT "Do" ]; count = int; tac = tactical ->
+ return_tactical loc (TacticAst.Do (count, tac))
+ | [ IDENT "repeat" | IDENT "Repeat" ]; tac = tactical ->
+ return_tactical loc (TacticAst.Repeat tac)
+ ]
+ | "simple" NONA
+ [ [ IDENT "tries" | IDENT "Tries" ];
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+ return_tactical loc (TacticAst.Tries tacs)
+ | [ IDENT "try" | IDENT "Try" ]; tac = NEXT ->
+ return_tactical loc (TacticAst.Try tac)
+ | [ IDENT "fail" | IDENT "Fail" ] -> return_tactical loc TacticAst.Fail
+ | [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac
+ | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
+ | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
+ ]
+ ];
+ 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))