aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES8
-rw-r--r--contrib/omega/OmegaSyntax.v4
-rw-r--r--contrib/ring/Quote.v2
-rw-r--r--contrib/ring/Ring.v4
-rw-r--r--contrib/ring/Ring_abstract.v206
-rw-r--r--contrib/ring/Ring_theory.v37
-rw-r--r--contrib/xml/Xml.v2
-rw-r--r--parsing/g_prim.ml412
-rw-r--r--tactics/EAuto.v2
-rw-r--r--tactics/Equality.v26
-rw-r--r--tactics/Inv.v6
-rw-r--r--tactics/Refine.v2
-rw-r--r--tactics/Tauto.v2
13 files changed, 59 insertions, 254 deletions
diff --git a/CHANGES b/CHANGES
index f8086a826..7a90f791f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,9 +35,11 @@ commandes)
motifs des règles d'affichage est maintenant celui associé au nom de
la grammaire (vernac, tactic ou constr). Donc plus de piquants
<:vernac:<...>> etc. Pour retourner de l'ast, il faut typer
-explicitement la grammaire avec Ast ou List (renommé d'ailleurs
-AstList), ou, si c'est dans une règle Syntax, utiliser la quotation
-<< ... >> qui replace dans ast.
+explicitement la grammaire avec "ast" ou "List" (renommé d'ailleurs
+"ast list"), ou, si c'est dans une règle Syntax, utiliser la quotation
+<< ... >> qui replace dans ast. Pour les nouvelles grammaires (autre
+que les 3 primitives), on peut typer avec "constr", "tactic", ou
+"vernac" pour utiliser le parseur correspondant.
- AddPath -> Add Path;
Print LoadPath -> Print Path;
diff --git a/contrib/omega/OmegaSyntax.v b/contrib/omega/OmegaSyntax.v
index 327f23a64..af673b097 100644
--- a/contrib/omega/OmegaSyntax.v
+++ b/contrib/omega/OmegaSyntax.v
@@ -8,7 +8,7 @@
(* $Id$ *)
-Grammar vernac vernac : Ast :=
+Grammar vernac vernac : ast :=
omega_sett [ "Set" "Omega" "Time" "." ] -> [(OmegaFlag "+time")]
| omega_sets [ "Set" "Omega" "System" "." ] -> [(OmegaFlag "+system")]
| omega_seta [ "Set" "Omega" "Action" "." ] -> [(OmegaFlag "+action")]
@@ -21,7 +21,7 @@ Grammar vernac vernac : Ast :=
| omega_set [ "Set" "Omega" stringarg($id) "." ] -> [(OmegaFlag $id)].
-Grammar tactic simple_tactic : Ast :=
+Grammar tactic simple_tactic : ast :=
omega [ "Omega" ] -> [(Omega)].
Syntax tactic level 0:
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index abde178e1..e7c995cf3 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/ring/Quote.v
@@ -79,7 +79,7 @@ Implicit Arguments Off.
Declare ML Module "quote".
-Grammar tactic simple_tactic : Ast :=
+Grammar tactic simple_tactic : ast :=
quote [ "Quote" identarg($f) ] -> [(Quote $f)]
| quote_lc [ "Quote" identarg($f) "[" ne_identarg_list($lc) "]"] ->
[ (Quote $f ($LIST $lc)) ].
diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v
index 9045eab5f..81b2077a4 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/Ring.v
@@ -9,14 +9,14 @@ Require Export Ring_abstract.
Declare ML Module "ring".
-Grammar tactic simple_tactic : Ast :=
+Grammar tactic simple_tactic : ast :=
ring [ "Ring" constrarg_list($arg) ] -> [(Ring ($LIST $arg))].
Syntax tactic level 0:
ring [ << (Ring ($LIST $lc)) >> ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ]
| ring_e [ << (Ring) >> ] -> ["Ring"].
-Grammar vernac vernac : Ast :=
+Grammar vernac vernac : ast :=
addring [ "Add" "Ring"
constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($t)
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 6bb1f5aa9..60fa01ff1 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -448,210 +448,4 @@ Tactic Definition Solve1 :=
[Rewrite H; Simpl; Auto
|Simpl in H0; Rewrite H0; Auto ].
-Lemma signed_sum_merge_ok : (x,y:signed_sum)
- (interp_sacs (signed_sum_merge x y))
- ==(Aplus (interp_sacs x) (interp_sacs y)).
-
- Induction x.
- Intro; Simpl; Auto.
-
- Induction y; Intros.
-
- Auto.
-
- Solve1.
-
- Simpl; Generalize (varlist_eq_prop v v0).
- Elim (varlist_eq v v0); Simpl.
-
- Intro Heq; Rewrite (Heq I).
- Rewrite H.
- Repeat Rewrite isacs_aux_ok.
- Rewrite (Th_plus_permute T).
- Repeat Rewrite (Th_plus_assoc T).
- Rewrite (Th_plus_sym T (Aopp (interp_vl Amult Aone Azero vm v0))
- (interp_vl Amult Aone Azero vm v0)).
- Rewrite (Th_opp_def T).
- Rewrite (Th_plus_zero_left T).
- Reflexivity.
-
- Solve1.
-
- Induction y; Intros.
-
- Auto.
-
- Simpl; Generalize (varlist_eq_prop v v0).
- Elim (varlist_eq v v0); Simpl.
-
- Intro Heq; Rewrite (Heq I).
- Rewrite H.
- Repeat Rewrite isacs_aux_ok.
- Rewrite (Th_plus_permute T).
- Repeat Rewrite (Th_plus_assoc T).
- Rewrite (Th_opp_def T).
- Rewrite (Th_plus_zero_left T).
- Reflexivity.
-
- Solve1.
-
- Solve1.
-
-Save.
-
-Tactic Definition Solve2 :=
- Elim (varlist_lt l v); Simpl; Rewrite isacs_aux_ok;
- [ Auto
- | Rewrite H; Auto ].
-
-Lemma plus_varlist_insert_ok : (l:varlist)(s:signed_sum)
- (interp_sacs (plus_varlist_insert l s))
- == (Aplus (interp_vl Amult Aone Azero vm l) (interp_sacs s)).
-Proof.
-
- Induction s.
- Trivial.
-
- Simpl; Intros.
- Solve2.
-
- Simpl; Intros.
- Generalize (varlist_eq_prop l v).
- Elim (varlist_eq l v); Simpl.
-
- Intro Heq; Rewrite (Heq I).
- Repeat Rewrite isacs_aux_ok.
- Repeat Rewrite (Th_plus_assoc T).
- Rewrite (Th_opp_def T).
- Rewrite (Th_plus_zero_left T).
- Reflexivity.
-
- Solve2.
-
-Save.
-
-Lemma minus_varlist_insert_ok : (l:varlist)(s:signed_sum)
- (interp_sacs (minus_varlist_insert l s))
- == (Aplus (Aopp (interp_vl Amult Aone Azero vm l)) (interp_sacs s)).
-Proof.
-
- Induction s.
- Trivial.
-
- Simpl; Intros.
- Generalize (varlist_eq_prop l v).
- Elim (varlist_eq l v); Simpl.
-
- Intro Heq; Rewrite (Heq I).
- Repeat Rewrite isacs_aux_ok.
- Repeat Rewrite (Th_plus_assoc T).
- Rewrite (Th_plus_sym T (Aopp (interp_vl Amult Aone Azero vm v))
- (interp_vl Amult Aone Azero vm v)).
- Rewrite (Th_opp_def T).
- Auto.
-
- Simpl; Intros.
- Solve2.
-
- Simpl; Intros; Solve2.
-
-Save.
-
-Lemma plus_sum_scalar_ok : (l:varlist)(s:signed_sum)
- (interp_sacs (plus_sum_scalar l s))
- == (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s)).
-Proof.
-
- Induction s.
- Trivial.
-
- Simpl; Intros.
- Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
- Repeat Rewrite isacs_aux_ok.
- Rewrite H.
- Auto.
-
- Simpl; Intros.
- Repeat Rewrite isacs_aux_ok.
- Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
- Rewrite H.
- Rewrite (Th_distr_right T).
- Rewrite <- (Th_opp_mult_right T).
- Reflexivity.
-
-Save.
-
-Lemma minus_sum_scalar_ok : (l:varlist)(s:signed_sum)
- (interp_sacs (minus_sum_scalar l s))
- == (Aopp (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s))).
-Proof.
-
- Induction s; Simpl; Intros.
-
- Rewrite (Th_mult_zero_right T); Symmetry; Apply (Th_opp_zero T).
-
- Simpl; Intros.
- Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
- Repeat Rewrite isacs_aux_ok.
- Rewrite H.
- Rewrite (Th_distr_right T).
- Rewrite (Th_plus_opp_opp T).
- Reflexivity.
-
- Simpl; Intros.
- Repeat Rewrite isacs_aux_ok.
- Rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
- Rewrite H.
- Rewrite (Th_distr_right T).
- Rewrite <- (Th_opp_mult_right T).
- Rewrite <- (Th_plus_opp_opp T).
- Rewrite (Th_opp_opp T).
- Reflexivity.
-
-Save.
-
-Lemma signed_sum_prod_ok : (x,y:signed_sum)
- (interp_sacs (signed_sum_prod x y)) ==
- (Amult (interp_sacs x) (interp_sacs y)).
-Proof.
-
- Induction x.
-
- Simpl; EAuto 1.
-
- Intros; Simpl.
- Rewrite signed_sum_merge_ok.
- Rewrite plus_sum_scalar_ok.
- Repeat Rewrite isacs_aux_ok.
- Rewrite H.
- Auto.
-
- Intros; Simpl.
- Repeat Rewrite isacs_aux_ok.
- Rewrite signed_sum_merge_ok.
- Rewrite minus_sum_scalar_ok.
- Rewrite H.
- Rewrite (Th_distr_left T).
- Rewrite (Th_opp_mult_left T).
- Reflexivity.
-
-Save.
-
-Theorem apolynomial_normalize_ok : (p:apolynomial)
- (interp_sacs (apolynomial_normalize p))==(interp_ap p).
-Proof.
- Induction p; Simpl; Auto 1.
- Intros.
- Rewrite signed_sum_merge_ok.
- Rewrite H; Rewrite H0; Reflexivity.
- Intros.
- Rewrite signed_sum_prod_ok.
- Rewrite H; Rewrite H0; Reflexivity.
- Intros.
- Rewrite minus_sum_scalar_ok.
- Simpl.
- Rewrite (Th_mult_one_left T).
- Rewrite H; Reflexivity.
-Save.
-
End abstract_rings.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index adf55b500..2901942ef 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -5,34 +5,35 @@ Require Export Bool.
Implicit Arguments On.
-Grammar ring formula :=
+Grammar ring formula : constr :=
formula_expr [ expr($p) ] -> [$p]
-| formula_eq [ expr($p) "==" expr($c) ] -> [<<(eqT A $p $c)>>]
-with expr :=
+| formula_eq [ expr($p) "==" expr($c) ] -> [ (eqT A $p $c) ]
+
+with expr : constr :=
RIGHTA
- expr_plus [ expr($p) "+" expr($c) ] -> [<<(Aplus $p $c)>>]
+ expr_plus [ expr($p) "+" expr($c) ] -> [ (Aplus $p $c) ]
| expr_expr1 [ expr1($p) ] -> [$p]
-with expr1 :=
+with expr1 : constr :=
RIGHTA
- expr1_plus [ expr1($p) "*" expr1($c) ] -> [<<(Amult $p $c)>>]
+ expr1_plus [ expr1($p) "*" expr1($c) ] -> [ (Amult $p $c) ]
| expr1_final [ final($p) ] -> [$p]
-with final :=
- final_var [ prim:var($id) ] -> [$id]
-| final_command [ "[" command:command($c) "]" ] -> [$c]
-| final_app [ "(" application($r) ")" ] -> [$r]
-| final_0 [ "0" ] -> [<<Azero>>]
-| final_1 [ "1" ] -> [<<Aone>>]
-| final_uminus [ "-" expr($c) ] -> [<<(Aopp $c)>>]
+with final : constr :=
+ final_var [ prim:var($id) ] -> [ $id ]
+| final_constr [ "[" constr:constr($c) "]" ] -> [ $c ]
+| final_app [ "(" application($r) ")" ] -> [ $r ]
+| final_0 [ "0" ] -> [ Azero ]
+| final_1 [ "1" ] -> [ Aone ]
+| final_uminus [ "-" expr($c) ] -> [ (Aopp $c) ]
-with application :=
+with application : constr :=
LEFTA
- app_cons [ application($p) application($c1) ] -> [<<($p $c1)>>]
- | app_tail [ expr($c1) ] -> [$c1].
+ app_cons [ application($p) application($c1) ] -> [ ($p $c1) ]
+ | app_tail [ expr($c1) ] -> [ $c1 ].
-Grammar command command0 :=
- formula_in_command [ "[" "|" ring:formula($c) "|" "]" ] -> [$c].
+Grammar constr constr0 :=
+ formula_in_constr [ "[" "|" ring:formula($c) "|" "]" ] -> [ $c ].
Section Theory_of_semi_rings.
diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v
index 0c82ae669..edd50e79d 100644
--- a/contrib/xml/Xml.v
+++ b/contrib/xml/Xml.v
@@ -10,7 +10,7 @@
Declare ML Module "xml" "xmlcommand" "xmlentries".
-Grammar vernac vernac : Ast :=
+Grammar vernac vernac : ast :=
xml_print [ "Print" "XML" identarg($id) "." ] ->
[(Print $id)]
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 30897a359..8951e94a8 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -67,12 +67,20 @@ GEXTEND Gram
[[ p = astlist; "->"; a = action -> Node(loc,"CASE",[p;a]) ]]
;
entry_type:
- [[ ":"; IDENT "AstList" ->
+ [[ ":"; IDENT "ast"; IDENT "list" ->
let _ = set_default_action_parser astlist in Id(loc,"LIST")
| ":"; IDENT "List" -> (* For compatibility *)
let _ = set_default_action_parser astlist in Id(loc,"LIST")
- | ":"; IDENT "Ast" ->
+ | ":"; IDENT "list" -> (* For compatibility *)
+ let _ = set_default_action_parser astlist in Id(loc,"LIST")
+ | ":"; IDENT "ast" ->
let _ = set_default_action_parser ast in Id(loc,"AST")
+ | ":"; IDENT "constr" ->
+ let _ = set_default_action_parser Constr.constr in Id(loc,"AST")
+ | ":"; IDENT "tactic" ->
+ let _ = set_default_action_parser Tactic.tactic in Id(loc,"AST")
+ | ":"; IDENT "vernac" ->
+ let _ = set_default_action_parser Vernac.vernac in Id(loc,"AST")
| -> Id(loc,"AST") ]]
;
END
diff --git a/tactics/EAuto.v b/tactics/EAuto.v
index 5c1994c5b..ba5403de4 100644
--- a/tactics/EAuto.v
+++ b/tactics/EAuto.v
@@ -13,7 +13,7 @@
(* Prolog.v *)
(****************************************************************************)
-Grammar tactic simple_tactic: Ast :=
+Grammar tactic simple_tactic: ast :=
eapply [ "EApply" constrarg_binding_list($cl) ]
-> [(EApplyWithBindings ($LIST $cl))]
| eexact [ "EExact" constrarg($c) ] -> [(EExact $c)]
diff --git a/tactics/Equality.v b/tactics/Equality.v
index 66193ca21..971d1e72c 100644
--- a/tactics/Equality.v
+++ b/tactics/Equality.v
@@ -3,41 +3,41 @@
Declare ML Module "equality".
-Grammar vernac orient_rule: Ast :=
+Grammar vernac orient_rule: ast :=
lr ["LR"] -> [ "LR" ]
|rl ["RL"] -> [ "RL" ]
-with rule_list: AstList :=
+with rule_list: ast list :=
single_rlt [ constrarg($com) orient_rule($ort) ] ->
[ (VERNACARGLIST $com $ort) ]
|recursive_rlt [ constrarg($com) orient_rule($ort) rule_list($tail)] ->
[ (VERNACARGLIST $com $ort) ($LIST $tail) ]
-with base_list: AstList :=
+with base_list: ast list :=
single_blt [identarg($rbase) "[" rule_list($rlt) "]"] ->
[ (VERNACARGLIST $rbase ($LIST $rlt)) ]
|recursive_blt [identarg($rbase) "[" rule_list($rlt) "]"
base_list($blt)] ->
[ (VERNACARGLIST $rbase ($LIST $rlt)) ($LIST $blt) ]
-with vernac: Ast :=
+with vernac: ast :=
addrule ["HintRewrite" base_list($blt) "."] ->
[ (HintRewrite ($LIST $blt)) ].
-Grammar tactic list_tactics: AstList :=
+Grammar tactic list_tactics: ast list :=
single_lt [tactic($tac)] -> [$tac]
|recursive_lt [tactic($tac) "|" list_tactics($tail)] ->
[ $tac ($LIST $tail) ]
-with step_largs: AstList :=
+with step_largs: ast list :=
nil_step [] -> []
|solve_step ["with" "Solve"] -> [(REDEXP (SolveStep))]
|use_step ["with" "Use"] -> [(REDEXP (Use))]
|all_step ["with" "All"] -> [(REDEXP (All))]
-with rest_largs: AstList :=
+with rest_largs: ast list :=
nil_rest [] -> []
|solve_rest ["with" "Solve"] -> [(REDEXP (SolveRest))]
|cond_rest ["with" "Cond"] -> [(REDEXP (Cond))]
-with autorew_largs: AstList :=
+with autorew_largs: ast list :=
step_arg ["Step" "=" "[" list_tactics($ltac) "]" step_largs($slargs)] ->
[(REDEXP (Step ($LIST $ltac))) ($LIST $slargs)]
|rest_arg ["Rest" "=" "[" list_tactics($ltac) "]" rest_largs($llargs)] ->
@@ -45,30 +45,30 @@ with autorew_largs: AstList :=
|depth_arg ["Depth" "=" numarg($dth)] ->
[(REDEXP (Depth $dth))]
-with list_args_autorew: AstList :=
+with list_args_autorew: ast list :=
nil_laa [] -> []
|recursive_laa [autorew_largs($largs) list_args_autorew($laa)] ->
[($LIST $largs) ($LIST $laa)]
-with hintbase_list: AstList :=
+with hintbase_list: ast list :=
nil_hintbase [] -> []
| base_by_name [identarg($id) hintbase_list($tail)] ->
[ (REDEXP (ByName $id)) ($LIST $tail)]
| explicit_base ["[" hintbase($b) "]" hintbase_list($tail)] ->
[(REDEXP (Explicit ($LIST $b))) ($LIST $tail) ]
-with hintbase: AstList :=
+with hintbase: ast list :=
onehint_lr [ constrarg($c) "LR" ] -> [(REDEXP (LR $c))]
| onehint_rl [ constrarg($c) "RL" ] -> [(REDEXP (RL $c))]
| conshint_lr [ constrarg($c) "LR" hintbase($tail)] -> [(REDEXP (LR $c)) ($LIST $tail)]
| conshint_rl [ constrarg($c) "RL" hintbase($tail)] -> [(REDEXP (RL $c)) ($LIST $tail)]
-with simple_tactic: Ast :=
+with simple_tactic: ast :=
AutoRewrite [ "AutoRewrite" "[" hintbase_list($lbase) "]"
list_args_autorew($laa)] ->
[(AutoRewrite (REDEXP (BaseList ($LIST $lbase))) ($LIST $laa))].
-Grammar tactic simple_tactic: Ast :=
+Grammar tactic simple_tactic: ast :=
replace [ "Replace" constrarg($c1) "with" constrarg($c2) ] -> [(Replace $c1 $c2)]
| deqhyp [ "Simplify_eq" identarg($id) ] -> [(DEqHyp $id)]
diff --git a/tactics/Inv.v b/tactics/Inv.v
index 2bde23bf7..1abcdd824 100644
--- a/tactics/Inv.v
+++ b/tactics/Inv.v
@@ -26,7 +26,7 @@ Syntax tactic level 0:
| inversion_clear [<<(INVCOM InversionClear)>>] -> [ "Inversion_clear" ].
-Grammar tactic simple_tactic: Ast :=
+Grammar tactic simple_tactic: ast :=
inversion [ inversion_com($ic) identarg($id) ] -> [(Inv $ic $id)]
| inversion_in [ inversion_com($ic) identarg($id) "in" ne_identarg_list($l) ]
-> [(InvIn $ic $id ($LIST $l))]
@@ -48,13 +48,13 @@ Grammar tactic simple_tactic: Ast :=
Inversion -> [(UseInversionLemmaIn $id $c ($LIST $l))]
esac
-with inversion_com: Ast :=
+with inversion_com: ast :=
simple_inv [ "Simple" "Inversion" ] -> [ HalfInversion ]
| inversion_com [ "Inversion" ] -> [ Inversion ]
| inv_clear [ "Inversion_clear" ] -> [ InversionClear ].
-Grammar vernac vernac: Ast :=
+Grammar vernac vernac: ast :=
der_inv_clr [ "Derive" "Inversion_clear" identarg($na) identarg($id) "." ]
-> [(MakeInversionLemmaFromHyp 1 $na $id)]
diff --git a/tactics/Refine.v b/tactics/Refine.v
index b4e023cde..33d6d9cab 100644
--- a/tactics/Refine.v
+++ b/tactics/Refine.v
@@ -3,7 +3,7 @@
Declare ML Module "refine".
-Grammar tactic simple_tactic: Ast :=
+Grammar tactic simple_tactic: ast :=
tcc [ "Refine" castedopenconstrarg($c) ] -> [(Tcc $c)].
Syntax tactic level 0:
diff --git a/tactics/Tauto.v b/tactics/Tauto.v
index 2f4475057..c6283109c 100644
--- a/tactics/Tauto.v
+++ b/tactics/Tauto.v
@@ -3,7 +3,7 @@
Declare ML Module "tauto".
-Grammar tactic simple_tactic: Ast :=
+Grammar tactic simple_tactic: ast :=
tauto [ "Tauto" ] -> [(Tauto)]
| intuition [ "Intuition" ] -> [(Intuition)].
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 19:14:03 +0000