diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 526 |
1 files changed, 526 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 new file mode 100644 index 0000000000..740498fad1 --- /dev/null +++ b/parsing/g_vernac.ml4 @@ -0,0 +1,526 @@ + +(* $Id$ *) + +open Pcoq + +open Tactic + +GEXTEND Gram + simple_tactic: + [ [ LIDENT "ML"; s = Prim.string -> <:ast< (MLTACTIC $s) >> ] ] + ; +END + +open Vernac + +GEXTEND Gram + vernac: LAST + [ [ tac = tacarg; "." -> <:ast< (SOLVE 1 (TACTIC $tac)) >> ] ] + ; +END + +GEXTEND Gram + tacarg: + [ [ tcl = Tactic.tactic_com_list -> tcl ] ] + ; + theorem_body_line: + [ [ n = numarg; ":"; tac = tacarg; "." -> + <:ast< (VERNACCALL {SOLVE} $n (TACTIC $tac)) >> + | tac = tacarg; "." -> <:ast< (VERNACCALL {SOLVE} 1 (TACTIC $tac)) >> + ] ] + ; + theorem_body_line_list: + [ [ t = theorem_body_line -> [t] + | t = theorem_body_line; l = theorem_body_line_list -> t :: l ] ] + ; + theorem_body: + [ [ l = theorem_body_line_list -> + <:ast< (VERNACARGLIST ($LIST $l)) >> ] ] + ; + destruct_location : + [ [ LIDENT "Conclusion" -> <:ast< (CONCL)>> + | LIDENT "Discardable"; "Hypothesis" -> <:ast< (DiscardableHYP)>> + | "Hypothesis" -> <:ast< (PreciousHYP)>> ]] + ; + ne_comarg_list: + [ [ l = LIST1 comarg -> l ] ] + ; + + opt_identarg_list: + [ [ -> [] + | ":"; l = LIST1 identarg -> l ] ] + ; + + finite_tok: + [ [ "Inductive" -> <:ast< "Inductive" >> + | "CoInductive" -> <:ast< "CoInductive" >> ] ] + ; + block_old_style: + [ [ ind = oneind_old_style; "with"; indl = block_old_style -> ind :: indl + | ind = oneind_old_style -> [ind] ] ] + ; + oneind_old_style: + [ [ id = identarg; ":"; c = comarg; ":="; lidcom = lidcom -> + <:ast< (VERNACARGLIST $id $c $lidcom) >> ] ] + ; + block: + [ [ ind = oneind; "with"; indl = block -> ind :: indl + | ind = oneind -> [ind] ] ] + ; + oneind: + [ [ id = identarg; indpar = indpar; ":"; c = comarg; ":="; lidcom = lidcom + -> <:ast< (VERNACARGLIST $id $c $indpar $lidcom) >> ] ] + ; + onerec: + [ [ id = identarg; "["; idl = ne_binder_semi_list; "]"; ":"; c = comarg; + ":="; def = comarg -> + <:ast< (VERNACARGLIST $id (BINDERLIST ($LIST $idl)) $c $def) >> ] ] + ; + specifrec: + [ [ rec_ = onerec; "with"; recl = specifrec -> rec_ :: recl + | rec_ = onerec -> [rec_] ] ] + ; + onecorec: + [ [ id = identarg; ":"; c = comarg; ":="; def = comarg -> + <:ast< (VERNACARGLIST $id $c $def) >> ] ] + ; + specifcorec: + [ [ corec = onecorec; "with"; corecl = specifcorec -> corec :: corecl + | corec = onecorec -> [corec] ] ] + ; + rec_constr: + [ [ c = Vernac.identarg -> <:ast< (VERNACARGLIST $c) >> + | -> <:ast< (VERNACARGLIST) >> ] ] + ; + record_tok: + [ [ LIDENT "Record" -> <:ast< "Record" >> + | LIDENT "Structure" -> <:ast< "Structure" >> ] ] + ; + field: + [ [ id = identarg; ":"; c = Command.command -> + <:ast< (VERNACARGLIST "" $id (COMMAND $c)) >> + | id = identarg; ":>"; c = Command.command -> + <:ast< (VERNACARGLIST "COERCION" $id (COMMAND $c)) >> ] ] + ; + nefields: + [ [ idc = field; ";"; fs = nefields -> idc :: fs + | idc = field -> [idc] ] ] + ; + fields: + [ [ fs = nefields -> <:ast< (VERNACARGLIST ($LIST $fs)) >> + | -> <:ast< (VERNACARGLIST) >> ] ] + ; + onescheme: + [ [ id = identarg; ":="; dep = dep; c = comarg; LIDENT "Sort"; + s = sortdef -> + <:ast< (VERNACARGLIST $id $dep $c (COMMAND $s)) >> ] ] + ; + specifscheme: + [ [ rec_ = onescheme; "with"; recl = specifscheme -> rec_ :: recl + | rec_ = onescheme -> [rec_] ] ] + ; + dep: + [ [ LIDENT "Induction"; LIDENT "for" -> <:ast< "DEP" >> + | LIDENT "Minimality"; LIDENT "for" -> <:ast< "NODEP" >> ] ] + ; + ne_binder_semi_list: + [ [ id = binder; ";"; idl = ne_binder_semi_list -> id :: idl + | id = binder -> [id] ] ] + ; + indpar: + [ [ "["; bl = ne_binder_semi_list; "]" -> + <:ast< (BINDERLIST ($LIST $bl)) >> + | -> <:ast< (BINDERLIST) >> ] ] + ; + sortdef: + [ [ "Set" -> <:ast< (PROP {Pos}) >> + | "Prop" -> <:ast< (PROP {Null}) >> + | "Type" -> <:ast< (TYPE) >> ] ] + ; + thm_tok: + [ [ "Theorem" -> <:ast< "THEOREM" >> + | LIDENT "Lemma" -> <:ast< "LEMMA" >> + | LIDENT "Fact" -> <:ast< "FACT" >> + | LIDENT "Remark" -> <:ast< "REMARK" >> ] ] + ; + + def_tok: + [ [ "Definition" -> <:ast< "DEFINITION" >> + | LIDENT "Local" -> <:ast< "LOCAL" >> + | "@"; "Definition" -> <:ast< "OBJECT" >> + | "@"; LIDENT "Local" -> <:ast< "LOBJECT" >> + | "@"; LIDENT "Coercion" -> <:ast< "OBJCOERCION" >> + | "@"; LIDENT "Local"; LIDENT "Coercion" -> <:ast< "LOBJCOERCION" >> + | LIDENT "SubClass" -> <:ast< "SUBCLASS" >> + | LIDENT "Local"; LIDENT "SubClass" -> <:ast< "LSUBCLASS" >> ] ] + ; + import_tok: + [ [ LIDENT "Import" -> <:ast< "IMPORT" >> + | LIDENT "Export" -> <:ast< "EXPORT" >> + | -> <:ast< "IMPORT" >> ] ] + ; + specif_tok: + [ [ LIDENT "Implementation" -> <:ast< "IMPLEMENTATION" >> + | LIDENT "Specification" -> <:ast< "SPECIFICATION" >> + | -> <:ast< "UNSPECIFIED" >> ] ] + ; + hyp_tok: + [ [ "Hypothesis" -> <:ast< "HYPOTHESIS" >> + | "Variable" -> <:ast< "VARIABLE" >> ] ] + ; + hyps_tok: + [ [ LIDENT "Hypotheses" -> <:ast< "HYPOTHESES" >> + | LIDENT "Variables" -> <:ast< "VARIABLES" >> ] ] + ; + param_tok: + [ [ "Axiom" -> <:ast< "AXIOM" >> + | "Parameter" -> <:ast< "PARAMETER" >> ] ] + ; + params_tok: + [ [ LIDENT "Parameters" -> <:ast< "PARAMETERS" >> ] ] + ; + binder: + [ [ idl = ne_identarg_comma_list; ":"; c = Command.command -> + <:ast< (BINDER $c ($LIST $idl)) >> ] ] + ; + idcom: + [ [ id = LIDENT; ":"; c = Command.command -> + <:ast< (BINDER $c ($VAR $id)) >> ] ] + ; + ne_lidcom: + [ [ idc = idcom; "|"; l = ne_lidcom -> idc :: l + | idc = idcom -> [idc] ] ] + ; + lidcom: + [ [ l = ne_lidcom -> <:ast< (BINDERLIST ($LIST $l)) >> + | "|"; l = ne_lidcom -> <:ast< (BINDERLIST ($LIST $l)) >> + | -> <:ast< (BINDERLIST) >> ] ] + ; + END + +GEXTEND Gram + vernac: + (* Definition, Goal *) + [ [ thm = thm_tok; id = identarg; ":"; c = comarg; "." -> + <:ast< (StartProof $thm $id $c) >> + | thm = thm_tok; id = identarg; ":"; c = comarg; ":="; "Proof"; + tb = theorem_body; "Qed"; "." -> + <:ast< (TheoremProof $thm $id $c $tb) >> + + | def = def_tok; s = identarg; ":"; c1 = Command.command; "." -> + <:ast< (StartProof $def $s (COMMAND $c1)) >> + | def = def_tok; s = identarg; ":="; c1 = Command.command; "." -> + <:ast< (DEFINITION $def $s (COMMAND $c1)) >> + | def = def_tok; s = identarg; ":="; c1 = Command.command; ":"; + c2 = Command.command; "." -> + <:ast< (DEFINITION $def $s (COMMAND (CAST $c1 $c2))) >> + | def = def_tok; s = identarg; ":"; c1 = Command.command; ":="; + c2 = Command.command; "." -> + <:ast< (DEFINITION $def $s (COMMAND (CAST $c2 $c1))) >> + +(* CP / Juillet 99 + Ajout de la possibilite d'appliquer une regle de reduction au + corps d'une definition + Definition t := Eval red in term +*) + + | def = def_tok; s = identarg; ":="; + LIDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Command.command; "." -> + <:ast< (DEFINITION $def $s (COMMAND $c1) (TACTIC_ARG (REDEXP $r))) >> + | def = def_tok; s = identarg; ":="; + LIDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Command.command; ":"; + c2 = Command.command; "." -> + <:ast< (DEFINITION $def $s + (COMMAND (CAST $c1 $c2)) (TACTIC_ARG (REDEXP $r))) >> + | def = def_tok; s = identarg; ":"; c1 = Command.command; ":="; + LIDENT "Eval"; r = Tactic.red_tactic; "in"; + c2 = Command.command; "." -> + <:ast< (DEFINITION $def $s (COMMAND (CAST $c2 $c1)) + (TACTIC_ARG (REDEXP $r))) >> + +(* Papageno / Février 99 + Ajout du racourci "Definition x [c:nat] := t" pour + "Definition x := [c:nat]t" *) + + | def = def_tok; s = identarg; "["; id1 = LIDENT; ":"; + c = Command.command; t = definition_tail; "." -> + <:ast< (DEFINITION $def $s (COMMAND (LAMBDA $c [$id1]$t))) >> + + | def = def_tok; s = identarg; "["; id1 = LIDENT; ","; + idl = Command.ne_ident_comma_list; ":"; c = Command.command; + t = definition_tail; "." -> + <:ast< (DEFINITION $def $s (COMMAND + (LAMBDALIST $c [$id1]($SLAM $idl $t)))) >> + + + | hyp = hyp_tok; bl = ne_binder_semi_list; "." -> + <:ast< (VARIABLE $hyp (BINDERLIST ($LIST $bl))) >> + | hyp = hyps_tok; bl = ne_binder_semi_list; "." -> + <:ast< (VARIABLE $hyp (BINDERLIST ($LIST $bl))) >> + | hyp = param_tok; bl = ne_binder_semi_list; "." -> + <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >> + | hyp = params_tok; bl = ne_binder_semi_list; "." -> + <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >> + | LIDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]"; + ":="; c = comarg; "." -> + <:ast< (ABSTRACTION $id $c ($LIST $l)) >> + | f = finite_tok; "Set"; id = identarg; indpar = indpar; ":="; + lidcom = lidcom; "." -> + <:ast< (ONEINDUCTIVE $f $id (COMMAND (PROP {Pos})) $indpar + $lidcom) >> + | f = finite_tok; "Type"; id = identarg; indpar = indpar; ":="; + lidcom = lidcom; "." -> + <:ast< (ONEINDUCTIVE $f $id (COMMAND (TYPE)) $indpar $lidcom) >> + | f = finite_tok; "Prop"; id = identarg; indpar = indpar; ":="; + lidcom = lidcom; "." -> + <:ast< (ONEINDUCTIVE $f $id (COMMAND (PROP {Null})) $indpar + $lidcom) >> + | f = finite_tok; indl = block; "." -> + <:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >> + + | record_tok; name = identarg; ps = indpar; ":"; s = sortdef; ":="; + c = rec_constr; "{"; fs = fields; "}"; "." -> + <:ast< (RECORD "" $name $ps (COMMAND $s) $c $fs) >> + | record_tok; ">"; name = identarg; ps = indpar; ":"; s = sortdef; ":="; + c = rec_constr; "{"; fs = fields; "}"; "." -> + <:ast< (RECORD "COERCION" $name $ps (COMMAND $s) $c $fs) >> + + | LIDENT "Mutual"; "["; bl = ne_binder_semi_list; "]" ; f = finite_tok; + indl = block_old_style; "." -> + <:ast< (OLDMUTUALINDUCTIVE (BINDERLIST ($LIST $bl)) $f + (VERNACARGLIST ($LIST $indl))) >> + | LIDENT "Mutual"; f = finite_tok; indl = block; "." -> + <:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >> + | "Fixpoint"; recs = specifrec; "." -> + <:ast< (MUTUALRECURSIVE (VERNACARGLIST ($LIST $recs))) >> + | "CoFixpoint"; corecs = specifcorec; "." -> + <:ast< (MUTUALCORECURSIVE (VERNACARGLIST ($LIST $corecs))) >> + | LIDENT "Scheme"; schemes = specifscheme; "." -> + <:ast< (INDUCTIONSCHEME (VERNACARGLIST ($LIST $schemes))) >> + ] ]; + + + definition_tail: + [ [ ";"; idl = Command.ne_ident_comma_list; + ":"; c = Command.command; c2 = definition_tail -> + <:ast< (LAMBDALIST $c ($SLAM $idl $c2)) >> + | "]"; ":"; ty = Command.command; ":=" ; c = Command.command -> + <:ast< (CAST $c $ty) >> + | "]"; ":="; c = Command.command -> c + ] ]; + + END + +(* State management *) +GEXTEND Gram + vernac: + [ [ + LIDENT "Save"; LIDENT "State"; id = identarg; "." -> + <:ast< (SaveState $id "") >> + | LIDENT "Save"; LIDENT "State"; id = identarg; s = stringarg; "." -> + <:ast< (SaveState $id $s) >> + | LIDENT "Write"; LIDENT "States"; id = identarg; "." -> + <:ast< (WriteStates $id) >> + | LIDENT "Write"; LIDENT "States"; id = stringarg; "." -> + <:ast< (WriteStates $id) >> + | LIDENT "Restore"; LIDENT "State"; id = identarg; "." -> + <:ast< (RestoreState $id) >> + | LIDENT "Remove"; LIDENT "State"; id = identarg; "." -> + <:ast< (RemoveState $id) >> + | LIDENT "Reset"; LIDENT "after"; id = identarg; "." -> + <:ast< (ResetAfter $id) >> + | LIDENT "Reset"; LIDENT "Initial"; "." -> <:ast< (ResetInitial) >> + | LIDENT "Reset"; LIDENT "Section"; id = identarg; "." -> + <:ast< (ResetSection $id) >> + | LIDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >> + +(* Modules and Sections *) + + | LIDENT "Read"; LIDENT "Module"; id = identarg; "." -> + <:ast< (ReadModule $id) >> + | LIDENT "Require"; import = import_tok; specif = specif_tok; + id = identarg; "." -> <:ast< (Require $import $specif $id) >> + | LIDENT "Require"; import = import_tok; specif = specif_tok; + id = identarg; filename = stringarg; "." -> + <:ast< (RequireFrom $import $specif $id $filename) >> + | LIDENT "Section"; id = identarg; "." -> <:ast< (BeginSection $id) >> + | LIDENT "Chapter"; id = identarg; "." -> <:ast< (BeginSection $id) >> + | LIDENT "Module"; id = identarg; "." -> <:ast< (BeginModule $id) >> + | LIDENT "Begin"; LIDENT "Silent"; "." -> <:ast< (BeginSilent) >> + | LIDENT "End"; LIDENT "Silent"; "." -> <:ast< (EndSilent) >> + | LIDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >> + | LIDENT "Declare"; LIDENT "ML"; LIDENT "Module"; + l = ne_stringarg_list; "." -> <:ast< (DeclareMLModule ($LIST $l)) >> + | LIDENT "Import"; id = identarg; "." -> <:ast< (ImportModule $id) >> + (* Transparent and Opaque *) + | LIDENT "Transparent"; l = ne_identarg_list; "." -> + <:ast< (TRANSPARENT ($LIST $l)) >> + | LIDENT "Opaque"; l = ne_identarg_list; "." -> + <:ast< (OPAQUE ($LIST $l)) >> + + (* Extraction *) + | LIDENT "Extraction"; id = identarg; "." -> + <:ast< (PrintExtractId $id) >> + | LIDENT "Extraction"; "." -> <:ast< (PrintExtract) >> + +(* Grammar extensions, Coercions, Implicits *) + + | LIDENT "Coercion"; s = identarg; ":="; c1 = Command.command; "." -> + <:ast< (DEFINITION "COERCION" $s (COMMAND $c1)) >> + | LIDENT "Coercion"; s = identarg; ":="; c1 = Command.command; ":"; + c2 = Command.command; "." -> + <:ast< (DEFINITION "COERCION" $s (COMMAND (CAST $c1 $c2))) >> + | LIDENT "Coercion"; LIDENT "Local"; s = identarg; ":="; + c1 = Command.command; "." -> + <:ast< (DEFINITION "LCOERCION" $s (COMMAND $c1)) >> + | LIDENT "Coercion"; LIDENT "Local"; s = identarg; ":="; + c1 = Command.command; ":"; c2 = Command.command; "." -> + <:ast< (DEFINITION "LCOERCION" $s (COMMAND (CAST $c1 $c2))) >> + + + | LIDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg; + "." -> <:ast< (SyntaxMacro $id $com) >> + | LIDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg; + "|"; n = numarg; "." -> <:ast< (SyntaxMacro $id $com $n) >> + | LIDENT "Print"; "Grammar"; uni = identarg; ent = identarg; "." -> + <:ast< (PrintGrammar $uni $ent) >> + | LIDENT "Identity"; LIDENT "Coercion"; LIDENT "Local"; f = identarg; + ":"; c = identarg; ">->"; d = identarg; "." -> + <:ast< (COERCION "LOCAL" "IDENTITY" $f $c $d) >> + | LIDENT "Identity"; LIDENT "Coercion"; f = identarg; ":"; + c = identarg; ">->"; d = identarg; "." -> + <:ast< (COERCION "" "IDENTITY" $f $c $d) >> + | LIDENT "Coercion"; LIDENT "Local"; f = identarg; ":"; c = identarg; + ">->"; d = identarg; "." -> + <:ast< (COERCION "LOCAL" "" $f $c $d) >> + | LIDENT "Coercion"; f = identarg; ":"; c = identarg; ">->"; + d = identarg; "." -> <:ast< (COERCION "" "" $f $c $d) >> + | LIDENT "Class"; LIDENT "Local"; c = identarg; "." -> + <:ast< (CLASS "LOCAL" $c) >> + | LIDENT "Class"; c = identarg; "." -> <:ast< (CLASS "" $c) >> + | LIDENT "Implicit"; LIDENT "Arguments"; LIDENT "On"; "." -> + <:ast< (IMPLICIT_ARGS_ON) >> + | LIDENT "Implicit"; LIDENT "Arguments"; LIDENT "Off"; "." -> + <:ast< (IMPLICIT_ARGS_OFF) >> + | LIDENT "Implicits"; id = identarg; "["; l = numarg_list; "]"; "." -> + <:ast< (IMPLICITS "" $id ($LIST $l)) >> + | LIDENT "Implicits"; id = identarg; "." -> + <:ast< (IMPLICITS "Auto" $id) >> + ] ]; + END + +(* Proof commands *) +GEXTEND Gram + vernac: + [ [ LIDENT "Goal"; c = comarg; "." -> <:ast< (GOAL $c) >> + | LIDENT "Goal"; "." -> <:ast< (GOAL) >> + | "Proof"; "." -> <:ast< (GOAL) >> + | LIDENT "Abort"; "." -> <:ast< (ABORT) >> + | "Qed"; "." -> <:ast< (SaveNamed) >> + | LIDENT "Save"; "." -> <:ast< (SaveNamed) >> + | LIDENT "Defined"; "." -> <:ast< (DefinedNamed) >> + | LIDENT "Save"; LIDENT "Remark"; id = identarg; "." -> + <:ast< (SaveAnonymousRmk $id) >> + | LIDENT "Save"; LIDENT "Theorem"; id = identarg; "." -> + <:ast< (SaveAnonymousThm $id) >> + | LIDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymousThm $id) >> + | LIDENT "Suspend"; "." -> <:ast< (SUSPEND) >> + | LIDENT "Resume"; "." -> <:ast< (RESUME) >> + | LIDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >> + | LIDENT "Abort"; LIDENT "All"; "." -> <:ast< (ABORTALL) >> + | LIDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >> + | LIDENT "Restart"; "." -> <:ast< (RESTART) >> + | "Proof"; c = comarg; "." -> <:ast< (PROOF $c) >> + | LIDENT "Undo"; "." -> <:ast< (UNDO 1) >> + | LIDENT "Undo"; n = numarg; "." -> <:ast< (UNDO $n) >> + | LIDENT "Show"; n = numarg; "." -> <:ast< (SHOW $n) >> + | LIDENT "Show"; LIDENT "Implicits"; n = numarg; "." -> + <:ast< (SHOWIMPL $n) >> + | LIDENT "Focus"; "." -> <:ast< (FOCUS) >> + | LIDENT "Focus"; n = numarg; "." -> <:ast< (FOCUS $n) >> + | LIDENT "Unfocus"; "." -> <:ast< (UNFOCUS) >> + | LIDENT "Show"; "." -> <:ast< (SHOW) >> + | LIDENT "Show"; LIDENT "Implicits"; "." -> <:ast< (SHOWIMPL) >> + | LIDENT "Show"; LIDENT "Node"; "." -> <:ast< (ShowNode) >> + | LIDENT "Show"; LIDENT "Script"; "." -> <:ast< (ShowScript) >> + | LIDENT "Show"; LIDENT "Existentials"; "." -> <:ast< (ShowEx) >> + | LIDENT "Existential"; n = numarg; ":="; c = Command.command; "." -> + <:ast< (EXISTENTIAL $n (COMMAND $c)) >> + | LIDENT "Existential"; n = numarg; ":="; c1 = Command.command; ":"; + c2 = Command.command; "." -> + <:ast< (EXISTENTIAL $n (COMMAND (CAST $c1 $c2))) >> + | LIDENT "Existential"; n = numarg; ":"; c2 = Command.command; ":="; + c1 = Command.command; "." -> + <:ast< (EXISTENTIAL $n (COMMAND (CAST $c1 $c2))) >> + | LIDENT "Explain"; "Proof"; l = numarg_list; "." -> + <:ast< (ExplainProof ($LIST $l)) >> + | LIDENT "Explain"; "Proof"; LIDENT "Tree"; l = numarg_list; "." -> + <:ast< (ExplainProofTree ($LIST $l)) >> + | LIDENT "Go"; n = numarg; "." -> <:ast< (Go $n) >> + | LIDENT "Go"; LIDENT "top"; "." -> <:ast< (Go "top") >> + | LIDENT "Go"; LIDENT "prev"; "." -> <:ast< (Go "prev") >> + | LIDENT "Go"; LIDENT "next"; "." -> <:ast< (Go "next") >> + | LIDENT "Show"; "Proof"; "." -> <:ast< (ShowProof) >> + | LIDENT "Guarded"; "." -> <:ast< (CheckGuard) >> + | LIDENT "Show"; LIDENT "Tree"; "." -> <:ast< (ShowTree) >> + | LIDENT "Show"; LIDENT "Conjectures"; "." -> <:ast< (ShowProofs) >> + +(* Tactic Definition *) + + | LIDENT "Tactic"; "Definition"; id = identarg; "["; + ids = ne_identarg_list; "]"; ":="; tac = Prim.astact; "." -> + <:ast< (TacticDefinition $id (AST $tac) ($LIST $ids)) >> + | LIDENT "Tactic"; "Definition"; id = identarg; ":="; tac = Prim.astact; + "." -> <:ast< (TacticDefinition $id (AST $tac)) >> + +(* Hints for Auto and EAuto *) + + | LIDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":="; + LIDENT "Resolve"; c = comarg; "." -> + <:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>> + + | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":="; + LIDENT "Immediate"; c = comarg; "." -> + <:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>> + + | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":="; + LIDENT "Unfold"; c = identarg; "." -> + <:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>> + + | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":="; + LIDENT "Constructors"; c = identarg; "." -> + <:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>> + + | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":="; + LIDENT "Extern"; n = numarg; c = comarg ; tac = tacarg; "." -> + <:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames)) + $n $c (TACTIC $tac))>> + + | LIDENT "Hints"; LIDENT "Resolve"; l = ne_identarg_list; + dbnames = opt_identarg_list; "." -> + <:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >> + + | LIDENT "Hints"; LIDENT "Immediate"; l = ne_identarg_list; + dbnames = opt_identarg_list; "." -> + <:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >> + + | LIDENT "Hints"; LIDENT "Unfold"; l = ne_identarg_list; + dbnames = opt_identarg_list; "." -> + <:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >> + + | LIDENT "HintDestruct"; + dloc = destruct_location; + na = identarg; + hyptyp = comarg; + 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*) + | LIDENT "PrintConstr"; com = comarg; "." -> + <:ast< (PrintConstr $com)>> + ] ]; + END |