diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /plugins/fourier/fourier.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'plugins/fourier/fourier.ml')
-rw-r--r-- | plugins/fourier/fourier.ml | 87 |
1 files changed, 43 insertions, 44 deletions
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml index c39c2387..50a5150d 100644 --- a/plugins/fourier/fourier.ml +++ b/plugins/fourier/fourier.ml @@ -1,18 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Méthode d'élimination de Fourier *) -(* Référence: +(* Méthode d'élimination de Fourier *) +(* Référence: Auteur(s) : Fourier, Jean-Baptiste-Joseph -Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,... +Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,... -Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890 +Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890 Pages: 326-327 @@ -20,8 +20,8 @@ http://gallica.bnf.fr/ *) (* Un peu de calcul sur les rationnels... -Les opérations rendent des rationnels normalisés, -i.e. le numérateur et le dénominateur sont premiers entre eux. +Les opérations rendent des rationnels normalisés, +i.e. le numérateur et le dénominateur sont premiers entre eux. *) type rational = {num:int; den:int} @@ -59,9 +59,9 @@ let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};; let rinf x y = x.num*y.den < y.num*x.den;; let rinfeq x y = x.num*y.den <= y.num*x.den;; -(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation +(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation c1x1+...+cnxn < d si strict=true, <= sinon, -hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ. +hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ. *) type ineq = {coef:rational list; @@ -70,8 +70,8 @@ type ineq = {coef:rational list; let pop x l = l:=x::(!l);; -(* sépare la liste d'inéquations s selon que leur premier coefficient est -négatif, nul ou positif. *) +(* sépare la liste d'inéquations s selon que leur premier coefficient est +négatif, nul ou positif. *) let partitionne s = let lpos=ref [] in let lneg=ref [] in @@ -85,44 +85,44 @@ let partitionne s = s; [!lneg;!lnul;!lpos] ;; -(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!): -(add_hist [(equation 1, s1);...;(équation n, sn)]) +(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!): +(add_hist [(equation 1, s1);...;(équation n, sn)]) = -[{équation 1, [1;0;...;0], s1}; - {équation 2, [0;1;...;0], s2}; +[{équation 1, [1;0;...;0], s1}; + {équation 2, [0;1;...;0], s2}; ... - {équation n, [0;0;...;1], sn}] + {équation n, [0;0;...;1], sn}] *) let add_hist le = let n = List.length le in - let i=ref 0 in + let i = ref 0 in List.map (fun (ie,s) -> - let h =ref [] in - for k=1 to (n-(!i)-1) do pop r0 h; done; + let h = ref [] in + for _k = 1 to (n - (!i) - 1) do pop r0 h; done; pop r1 h; - for k=1 to !i do pop r0 h; done; + for _k = 1 to !i do pop r0 h; done; i:=!i+1; {coef=ie;hist=(!h);strict=s}) le ;; -(* additionne deux inéquations *) +(* additionne deux inéquations *) let ie_add ie1 ie2 = {coef=List.map2 rplus ie1.coef ie2.coef; hist=List.map2 rplus ie1.hist ie2.hist; strict=ie1.strict || ie2.strict} ;; -(* multiplication d'une inéquation par un rationnel (positif) *) +(* multiplication d'une inéquation par un rationnel (positif) *) let ie_emult a ie = {coef=List.map (fun x -> rmult a x) ie.coef; hist=List.map (fun x -> rmult a x) ie.hist; strict= ie.strict} ;; -(* on enlève le premier coefficient *) +(* on enlève le premier coefficient *) let ie_tl ie = {coef=List.tl ie.coef;hist=ie.hist;strict=ie.strict} ;; -(* le premier coefficient: "tête" de l'inéquation *) +(* le premier coefficient: "tête" de l'inéquation *) let hd_coef ie = List.hd ie.coef ;; -(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient. +(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient. *) let deduce_add lneg lpos = let res=ref [] in @@ -136,8 +136,8 @@ let deduce_add lneg lpos = lneg; !res ;; -(* élimination de la première variable à partir d'une liste d'inéquations: -opération qu'on itère dans l'algorithme de Fourier. +(* élimination de la première variable à partir d'une liste d'inéquations: +opération qu'on itère dans l'algorithme de Fourier. *) let deduce1 s = match (partitionne s) with @@ -146,38 +146,37 @@ let deduce1 s = (List.map ie_tl lnul)@lnew |_->assert false ;; -(* algorithme de Fourier: on élimine successivement toutes les variables. +(* algorithme de Fourier: on élimine successivement toutes les variables. *) let deduce lie = let n = List.length (fst (List.hd lie)) in let lie=ref (add_hist lie) in - for i=1 to n-1 do + for _i = 1 to n - 1 do lie:= deduce1 !lie; done; !lie ;; -(* donne [] si le système a des solutions, +(* donne [] si le système a des solutions, sinon donne [c,s,lc] -où lc est la combinaison linéaire des inéquations de départ +où lc est la combinaison linéaire des inéquations de départ qui donne 0 < c si s=true ou 0 <= c sinon -cette inéquation étant absurde. +cette inéquation étant absurde. *) + +exception Contradiction of (rational * bool * rational list) list + let unsolvable lie = let lr = deduce lie in - let res = ref [] in - (try (List.iter (fun e -> - match e with - {coef=[c];hist=lc;strict=s} -> - if (rinf c r0 && (not s)) || (rinfeq c r0 && s) - then (res := [c,s,lc]; - raise (Failure "contradiction found")) - |_->assert false) - lr) - with e when Errors.noncritical e -> ()); - !res -;; + let check = function + | {coef=[c];hist=lc;strict=s} -> + if (rinf c r0 && (not s)) || (rinfeq c r0 && s) + then raise (Contradiction [c,s,lc]) + |_->assert false + in + try List.iter check lr; [] + with Contradiction l -> l (* Exemples: |