aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_proofs.ml44
-rw-r--r--parsing/g_tactic.ml427
-rw-r--r--parsing/g_vernac.ml410
-rw-r--r--parsing/pcoq.ml42
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/pretty.ml3
6 files changed, 41 insertions, 7 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 0f0d70f8b..1cd140ed6 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -33,15 +33,17 @@ GEXTEND Gram
[ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >>
| IDENT "Goal"; "." -> <:ast< (GOAL) >>
| "Proof"; "." -> <:ast< (GOAL) >>
+ | IDENT "Begin"; "." -> <:ast< (GOAL) >>
| IDENT "Abort"; "." -> <:ast< (ABORT) >>
| "Qed"; "." -> <:ast< (SaveNamed) >>
| IDENT "Save"; "." -> <:ast< (SaveNamed) >>
| IDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
+ | IDENT "Defined"; id = identarg; "." -> <:ast< (DefinedAnonymous $id) >>
| 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 "Save"; id = identarg; "." -> <:ast< (SaveAnonymous $id) >>
| IDENT "Suspend"; "." -> <:ast< (SUSPEND) >>
| IDENT "Resume"; "." -> <:ast< (RESUME) >>
| IDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >>
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 99e7e136e..18a9da82b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -212,7 +212,19 @@ GEXTEND Gram
| "()" -> <:ast< (VOID) >> ] ]
;
let_clause:
- [ [ id = identarg; "="; te=tactic_expr -> <:ast< (LETCLAUSE $id $te) >> ] ]
+ [ [ id = identarg; "="; te=tactic_expr -> <:ast< (LETCLAUSE $id $te) >>
+ | id = identarg; ":"; c = constrarg; ":="; "Proof" ->
+ (match c with
+ | Coqast.Node(_,"COMMAND",[csr]) ->
+ <:ast< (LETTOPCLAUSE $id (CONSTR $csr)) >>
+ | _ -> errorlabstrm "Gram.let_clause" [<'sTR "Not a COMMAND">])
+ | id = identarg; ":"; c = constrarg; ":="; te = tactic_expr ->
+ <:ast< (LETCUTCLAUSE $id $c $te) >>
+ | id = identarg; ":"; c = constrarg ->
+ (match c with
+ | Coqast.Node(_,"COMMAND",[csr]) ->
+ <:ast< (LETTOPCLAUSE $id (CONSTR $csr)) >>
+ | _ -> errorlabstrm "Gram.let_clause" [<'sTR "Not a COMMAND">]) ] ]
;
rec_clause:
[ [ name = identarg; it = LIST1 input_fun; "->"; body = tactic_expr ->
@@ -273,6 +285,17 @@ GEXTEND Gram
<:ast< (REC (RECDECL $rc ($LIST $rcl)) $body) >>
| IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And"; IDENT "In";
u = tactic_expr -> <:ast< (LET (LETDECL ($LIST $llc)) $u) >>
+ | IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And" ->
+ (match llc with
+ | [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
+ <:ast< (StartProof "LETTOP" $id $c) >>
+ | _ -> <:ast< (LETCUT (LETDECL ($LIST $llc))) >>)
+ | IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And";
+ tb = Vernac.theorem_body; "Qed" ->
+ (match llc with
+ | [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
+ <:ast< (TheoremProof "LETTOP" $id $c $tb) >>
+ | _ -> errorlabstrm "Gram.tactic_atom" [<'sTR "Not a LETTOPCLAUSE">])
| IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list
-> <:ast< (MATCHCONTEXT ($LIST $mrl)) >>
| IDENT "Match"; com = constrarg; IDENT "With"; mrl = match_list ->
@@ -308,7 +331,7 @@ GEXTEND Gram
| "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >>
| IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = Constr.constr ->
<:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >>
- | "'"; c = ident_or_constrarg -> c ] ]
+ | "'"; c = constrarg -> c ] ]
;
simple_tactic:
[ [ IDENT "Fix"; n = pure_numarg -> <:ast< (Fix $n) >>
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2eab11665..7f22ba49a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -22,7 +22,11 @@ GEXTEND Gram
| "["; l = vernac_list_tail -> <:ast< (VernacList ($LIST $l)) >> ] ]
;
vernac: LAST
- [ [ tac = tacarg; "." -> <:ast< (SOLVE 1 (TACTIC $tac)) >> ] ]
+ [ [ tac = tacarg; "." ->
+ (match tac with
+ | Coqast.Node(_,kind,_)
+ when kind = "StartProof" || kind = "TheoremProof" -> tac
+ | _ -> <:ast< (SOLVE 1 (TACTIC $tac)) >>) ] ]
;
vernac_list_tail:
[ [ v = vernac; l = vernac_list_tail -> v :: l
@@ -52,7 +56,8 @@ GEXTEND Gram
[ [ "Theorem" -> <:ast< "THEOREM" >>
| IDENT "Lemma" -> <:ast< "LEMMA" >>
| IDENT "Fact" -> <:ast< "FACT" >>
- | IDENT "Remark" -> <:ast< "REMARK" >> ] ]
+ | IDENT "Remark" -> <:ast< "REMARK" >>
+ | IDENT "Decl" -> <:ast< "DECL" >> ] ]
;
def_tok:
[ [ "Definition" -> <:ast< "DEFINITION" >>
@@ -103,7 +108,6 @@ GEXTEND Gram
| thm = thm_tok; id = identarg; ":"; c = constrarg; ":="; "Proof";
tb = theorem_body; "Qed"; "." ->
<:ast< (TheoremProof $thm $id $c $tb) >>
-
| def = def_tok; s = identarg; bl = binders_list;
":"; t = Constr.constr; "." ->
<:ast< (StartProof $def $s (CONSTR ($ABSTRACT "PRODLIST" $bl $t))) >>
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b10921817..5df722f1b 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -289,6 +289,7 @@ module Tactic =
let input_fun = gec "input_fun"
let lconstrarg = gec "lconstrarg"
let let_clause = gec "let_clause"
+ let letcut_clause = gec "letcut_clause"
let clausearg = gec "clausearg"
let match_context_rule = gec "match_context_rule"
let match_hyps = gec "match_hyps"
@@ -360,6 +361,7 @@ module Vernac =
let ne_constrarg_list = gec_list "ne_constrarg_list"
let tacarg = gec "tacarg"
let sortarg = gec "sortarg"
+ let theorem_body = gec "theorem_body"
let gallina = gec "gallina"
let gallina_ext = gec "gallina_ext"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c4f61aa75..1999733f0 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -120,6 +120,7 @@ module Tactic :
val lconstrarg : Coqast.t Gram.Entry.e
val lconstrarg_binding_list : Coqast.t list Gram.Entry.e
val let_clause : Coqast.t Gram.Entry.e
+ val letcut_clause : Coqast.t Gram.Entry.e
val match_context_rule : Coqast.t Gram.Entry.e
val match_hyps : Coqast.t Gram.Entry.e
val match_pattern : Coqast.t Gram.Entry.e
@@ -172,6 +173,7 @@ module Vernac :
val ne_constrarg_list : Coqast.t list Gram.Entry.e
val tacarg : Coqast.t Gram.Entry.e
val sortarg : Coqast.t Gram.Entry.e
+ val theorem_body : Coqast.t Gram.Entry.e
val gallina : Coqast.t Gram.Entry.e
val gallina_ext : Coqast.t Gram.Entry.e
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 33c5f862e..007a2e4ab 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -434,7 +434,8 @@ let inspect depth =
open Classops
-let string_of_strength = function
+let string_of_strength = function
+ | NotDeclare -> "(temp)"
| NeverDischarge -> "(global)"
| DischargeAt sp -> "(disch@"^(string_of_dirpath sp)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 06:24:15 +0000