diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 160 |
1 files changed, 160 insertions, 0 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 new file mode 100644 index 000000000..3f1087c67 --- /dev/null +++ b/parsing/g_proofs.ml4 @@ -0,0 +1,160 @@ + +(* $Id$ *) + +open Pcoq +open Pp +open Tactic +open Util +open Vernac + +(* Proof commands *) +GEXTEND Gram + GLOBAL: command ne_constrarg_list; + + destruct_location : + [ [ IDENT "Conclusion" -> <:ast< (CONCL)>> + | IDENT "Discardable"; "Hypothesis" -> <:ast< (DiscardableHYP)>> + | "Hypothesis" -> <:ast< (PreciousHYP)>> ]] + ; + ne_constrarg_list: + [ [ l = LIST1 constrarg -> l ] ] + ; + opt_identarg_list: + [ [ -> [] + | ":"; l = LIST1 identarg -> l ] ] + ; + vrec_clause: + [ [ name=identarg; it=LIST1 input_fun; ":="; body=tactic_expr -> + <:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ] + ; + command: + [ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >> + | IDENT "Goal"; "." -> <:ast< (GOAL) >> + | "Proof"; "." -> <:ast< (GOAL) >> + | IDENT "Abort"; "." -> <:ast< (ABORT) >> + | "Qed"; "." -> <:ast< (SaveNamed) >> + | IDENT "Save"; "." -> <:ast< (SaveNamed) >> + | IDENT "Defined"; "." -> <:ast< (DefinedNamed) >> + | IDENT "Save"; IDENT "Remark"; id = identarg; "." -> + <:ast< (SaveAnonymousRmk $id) >> + | IDENT "Save"; IDENT "Theorem"; id = identarg; "." -> + <:ast< (SaveAnonymousThm $id) >> + | IDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymousThm $id) >> + | IDENT "Suspend"; "." -> <:ast< (SUSPEND) >> + | IDENT "Resume"; "." -> <:ast< (RESUME) >> + | IDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >> + | IDENT "Abort"; IDENT "All"; "." -> <:ast< (ABORTALL) >> + | IDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >> + | IDENT "Restart"; "." -> <:ast< (RESTART) >> + | "Proof"; c = constrarg; "." -> <:ast< (PROOF $c) >> + | IDENT "Undo"; "." -> <:ast< (UNDO 1) >> + | IDENT "Undo"; n = numarg; "." -> <:ast< (UNDO $n) >> + | IDENT "Show"; n = numarg; "." -> <:ast< (SHOW $n) >> + | IDENT "Show"; IDENT "Implicits"; n = numarg; "." -> + <:ast< (SHOWIMPL $n) >> + | IDENT "Focus"; "." -> <:ast< (FOCUS) >> + | IDENT "Focus"; n = numarg; "." -> <:ast< (FOCUS $n) >> + | IDENT "Unfocus"; "." -> <:ast< (UNFOCUS) >> + | IDENT "Show"; "." -> <:ast< (SHOW) >> + | IDENT "Show"; IDENT "Implicits"; "." -> <:ast< (SHOWIMPL) >> + | IDENT "Show"; IDENT "Node"; "." -> <:ast< (ShowNode) >> + | IDENT "Show"; IDENT "Script"; "." -> <:ast< (ShowScript) >> + | IDENT "Show"; IDENT "Existentials"; "." -> <:ast< (ShowEx) >> + | IDENT "Existential"; n = numarg; ":="; c = constrarg; "." -> + <:ast< (EXISTENTIAL $n $c) >> + | IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":"; + c2 = Constr.constr; "." -> + <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >> + | IDENT "Existential"; n = numarg; ":"; c2 = Constr.constr; ":="; + c1 = Constr.constr; "." -> + <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >> + | IDENT "Explain"; "Proof"; l = numarg_list; "." -> + <:ast< (ExplainProof ($LIST $l)) >> + | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list; "." -> + <:ast< (ExplainProofTree ($LIST $l)) >> + | IDENT "Go"; n = numarg; "." -> <:ast< (Go $n) >> + | IDENT "Go"; IDENT "top"; "." -> <:ast< (Go "top") >> + | IDENT "Go"; IDENT "prev"; "." -> <:ast< (Go "prev") >> + | IDENT "Go"; IDENT "next"; "." -> <:ast< (Go "next") >> + | IDENT "Show"; "Proof"; "." -> <:ast< (ShowProof) >> + | IDENT "Guarded"; "." -> <:ast< (CheckGuard) >> + | IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >> + | IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >> + +(* Tactic Definition *) + + |IDENT "Tactic"; "Definition"; name=identarg; ":="; body=Tactic.tactic; + "." -> <:ast<(TACDEF $name (AST $body))>> + |IDENT "Tactic"; "Definition"; name=identarg; largs=LIST1 input_fun; + ":="; body=Tactic.tactic; "." -> + <:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>> + |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause ; "." -> + (match vc with + Coqast.Node(_,"RECCLAUSE",nme::tl) -> + <:ast<(TACDEF $nme (AST (REC $vc)))>> + |_ -> + anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">]) + |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause; + IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." -> + let nvcl= + List.fold_right + (fun e b -> match e with + Coqast.Node(_,"RECCLAUSE",nme::_) -> + nme::<:ast<(AST (REC $e))>>::b + |_ -> + anomalylabstrm "Gram.vernac" [<'sTR + "Not a correct RECCLAUSE">]) (vc::vcl) [] + in + <:ast<(TACDEF ($LIST $nvcl))>> + +(* Hints for Auto and EAuto *) + + | IDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":="; + IDENT "Resolve"; c = constrarg; "." -> + <:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>> + + | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":="; + IDENT "Immediate"; c = constrarg; "." -> + <:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>> + + | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":="; + IDENT "Unfold"; c = identarg; "." -> + <:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>> + + | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":="; + IDENT "Constructors"; c = identarg; "." -> + <:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>> + + | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":="; + IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg; "." -> + <:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames)) + $n $c (TACTIC $tac))>> + + | IDENT "Hints"; IDENT "Resolve"; l = ne_identarg_list; + dbnames = opt_identarg_list; "." -> + <:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >> + + | IDENT "Hints"; IDENT "Immediate"; l = ne_identarg_list; + dbnames = opt_identarg_list; "." -> + <:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >> + + | IDENT "Hints"; IDENT "Unfold"; l = ne_identarg_list; + dbnames = opt_identarg_list; "." -> + <:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >> + + | IDENT "HintDestruct"; + dloc = destruct_location; + na = identarg; + hyptyp = constrarg; + pri = numarg; + tac = Prim.astact; "." -> + <:ast< (HintDestruct $na (AST $dloc) $hyptyp $pri (AST $tac))>> + + | n = numarg; ":"; tac = tacarg; "." -> + <:ast< (SOLVE $n (TACTIC $tac)) >> + +(*This entry is not commented, only for debug*) + | IDENT "PrintConstr"; com = constrarg; "." -> + <:ast< (PrintConstr $com)>> + ] ]; + END |