From cc42541eeaaec0371940e07efdb009a4ee74e468 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 20 Oct 2015 13:04:45 +0200 Subject: Boxing the Goal.enter primitive into a record type. --- plugins/fourier/fourierR.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'plugins/fourier') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 7a56cd6657..e5c9b27075 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -19,6 +19,7 @@ open Globnames open Tacmach open Fourier open Contradiction +open Proofview.Notations (****************************************************************************** Opérations sur les combinaisons linéaires affines. @@ -462,7 +463,7 @@ exception GoalDone (* Résolution d'inéquations linéaires dans R *) let rec fourier () = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; let goal = strip_outer_cast concl in @@ -622,7 +623,7 @@ let rec fourier () = (* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) !tac (* ((tclABSTRACT None !tac) gl) *) - end + end } ;; (* -- cgit v1.2.3 From 19e2576c979c57ad0827f6a4364713930e0c6d4f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 30 Dec 2015 09:12:39 +0100 Subject: Simplifying code of fourier. --- plugins/fourier/fourierR.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) (limited to 'plugins/fourier') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index e5c9b27075..b1f642c1d2 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -413,13 +413,6 @@ let tac_zero_infeq_false gl (n,d) = (tac_zero_inf_pos gl (-n,d))) ;; -let create_meta () = mkMeta(Evarutil.new_meta());; - -let my_cut c gl= - let concl = pf_concl gl in - apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl -;; - let exact = exact_check;; let tac_use h = @@ -587,7 +580,7 @@ let rec fourier () = then tac_zero_inf_false gl (rational_to_fraction cres) else tac_zero_infeq_false gl (rational_to_fraction cres) in - tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq)) + tac:=(Tacticals.New.tclTHENS (cut ineq) [Tacticals.New.tclTHEN (change_concl (mkAppL [| get coq_not; ineq|] )) -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- plugins/fourier/Fourier.v | 2 +- plugins/fourier/Fourier_util.v | 2 +- plugins/fourier/fourier.ml | 2 +- plugins/fourier/fourierR.ml | 2 +- plugins/fourier/g_fourier.ml4 | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/fourier') diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v index 1832de85b3..1d7ee93ea3 100644 --- a/plugins/fourier/Fourier.v +++ b/plugins/fourier/Fourier.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- plugins/fourier/fourierR.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'plugins/fourier') diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 4c0aa6c759..8bc84608e6 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -445,7 +445,11 @@ let is_ineq (h,t) = ;; *) -let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;; +let list_of_sign s = + let open Context.Named.Declaration in + List.map (function LocalAssum (name, typ) -> name, typ + | LocalDef (name, _, typ) -> name, typ) + s;; let mkAppL a = let l = Array.to_list a in -- cgit v1.2.3