From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- plugins/romega/refl_omega.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/romega') diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 8156e84114..95407c5ff1 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -44,7 +44,7 @@ let occ_step_eq s1 s2 = match s1, s2 with (* chemin identifiant une proposition sous forme du nom de l'hypothèse et d'une liste de pas à partir de la racine de l'hypothèse *) -type occurence = {o_hyp : Names.Id.t; o_path : occ_path} +type occurrence = {o_hyp : Names.Id.t; o_path : occ_path} (* \subsection{refiable formulas} *) type oformula = @@ -81,7 +81,7 @@ and oequation = { e_left: oformula; (* formule brute gauche *) e_right: oformula; (* formule brute droite *) e_trace: Term.constr; (* tactique de normalisation *) - e_origin: occurence; (* l'hypothèse dont vient le terme *) + e_origin: occurrence; (* l'hypothèse dont vient le terme *) e_negated: bool; (* vrai si apparait en position nié après normalisation *) e_depends: direction list; (* liste des points de disjonction dont @@ -111,7 +111,7 @@ type environment = { real_indices : (int,int) Hashtbl.t; mutable cnt_connectors : int; equations : (int,oequation) Hashtbl.t; - constructors : (int, occurence) Hashtbl.t + constructors : (int, occurrence) Hashtbl.t } (* \subsection{Solution tree} @@ -136,7 +136,7 @@ type solution_tree = chemins pour extraire des equations ou d'hypothèses *) type context_content = - CCHyp of occurence + CCHyp of occurrence | CCEqua of int (* \section{Specific utility functions to handle base types} *) -- cgit v1.2.3 From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 7 Dec 2015 10:52:14 +0100 Subject: Fix some typos. --- plugins/romega/refl_omega.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/romega') diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 95407c5ff1..560e6a899e 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -46,7 +46,7 @@ let occ_step_eq s1 s2 = match s1, s2 with d'une liste de pas à partir de la racine de l'hypothèse *) type occurrence = {o_hyp : Names.Id.t; o_path : occ_path} -(* \subsection{refiable formulas} *) +(* \subsection{reifiable formulas} *) type oformula = (* integer *) | Oint of Bigint.bigint @@ -55,7 +55,7 @@ type oformula = | Omult of oformula * oformula | Ominus of oformula * oformula | Oopp of oformula - (* an atome in the environment *) + (* an atom in the environment *) | Oatom of int (* weird expression that cannot be translated *) | Oufo of oformula @@ -75,7 +75,7 @@ type oproposition = | Pimp of int * oproposition * oproposition | Pprop of Term.constr -(* Les équations ou proposiitions atomiques utiles du calcul *) +(* Les équations ou propositions atomiques utiles du calcul *) and oequation = { e_comp: comparaison; (* comparaison *) e_left: oformula; (* formule brute gauche *) @@ -1266,7 +1266,7 @@ let resolution env full_reified_goal systems_list = | (O_right :: l) -> app coq_p_right [| loop l |] in let correct_index = let i = List.index0 Names.Id.equal e.e_origin.o_hyp l_hyps in - (* PL: it seems that additionnally introduced hyps are in the way during + (* PL: it seems that additionally introduced hyps are in the way during normalization, hence this index shifting... *) if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce) in -- cgit v1.2.3 From 15b28f0ae1e31506f3fb153fc6e50bc861717eb9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 14:26:43 +0100 Subject: Moving conversion functions to the new tactic API. --- plugins/romega/refl_omega.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/romega') diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 560e6a899e..177c870b3c 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1285,7 +1285,7 @@ let resolution env full_reified_goal systems_list = Proofview.V82.of_tactic (Tactics.change_concl reified) >> Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> - Tactics.normalise_vm_in_concl >> + Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >> (*i Alternatives to the previous line: - Normalisation without VM: Tactics.normalise_in_concl -- cgit v1.2.3 From 60f6d46c6e623a39fc66a21cbac5aaecdf4c67c6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 23 Feb 2016 18:50:31 +0100 Subject: Getting rid of the "<:tactic< ... >>" quotations. It used to allow to represent parts of tactic AST directly in ML code. Most of the uses were trivial, only calling a constant, except for tauto that had an important code base written in this style. Removing this reduces the dependency to CAMLPX and the preeminence of Ltac in ML code. --- plugins/romega/g_romega.ml4 | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'plugins/romega') diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 0a99a26b36..6b2b2bbfaf 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -10,15 +10,22 @@ DECLARE PLUGIN "romega_plugin" +open Names open Refl_omega +let eval_tactic name = + let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in + let kn = KerName.make2 (MPfile dp) (Label.make name) in + let tac = Tacenv.interp_ltac kn in + Tacinterp.eval_tactic tac + let romega_tactic l = let tacs = List.map (function - | "nat" -> Tacinterp.interp <:tactic> - | "positive" -> Tacinterp.interp <:tactic> - | "N" -> Tacinterp.interp <:tactic> - | "Z" -> Tacinterp.interp <:tactic> + | "nat" -> eval_tactic "zify_nat" + | "positive" -> eval_tactic "zify_positive" + | "N" -> eval_tactic "zify_N" + | "Z" -> eval_tactic "zify_op" | s -> Errors.error ("No ROmega knowledge base for type "^s)) (Util.List.sort_uniquize String.compare l) in -- cgit v1.2.3 From d5656a6c28f79d59590d4fde60c5158a649d1b65 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Mar 2016 11:16:03 +0100 Subject: Making parentheses mandatory in tactic scopes. --- plugins/romega/ReflOmegaCore.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/romega') diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index b84cf25405..36511386ac 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1492,7 +1492,7 @@ with Simplify := match goal with end. Ltac prove_stable x th := - match constr:x with + match constr:(x) with | ?X1 => unfold term_stable, X1; intros; Simplify; simpl; apply th -- cgit v1.2.3 From 4b2cdf733df6dc23247b078679e71da98e54f5cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:57:05 +0100 Subject: Removing the special status of generic entries defined by Coq itself. The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there. --- plugins/romega/g_romega.ml4 | 2 ++ 1 file changed, 2 insertions(+) (limited to 'plugins/romega') diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 6b2b2bbfaf..61efa9f545 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -12,6 +12,8 @@ DECLARE PLUGIN "romega_plugin" open Names open Refl_omega +open Constrarg +open Pcoq.Prim let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in -- cgit v1.2.3