diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 12:48:32 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 14:27:21 +0100 |
commit | af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch) | |
tree | b8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /plugins/fourier | |
parent | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff) |
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'plugins/fourier')
-rw-r--r-- | plugins/fourier/fourier.ml | 52 | ||||
-rw-r--r-- | plugins/fourier/fourierR.ml | 40 |
2 files changed, 46 insertions, 46 deletions
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml index 626629063..9e257c82a 100644 --- a/plugins/fourier/fourier.ml +++ b/plugins/fourier/fourier.ml @@ -6,13 +6,13 @@ (* * 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,13 +85,13 @@ 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 @@ -105,24 +105,24 @@ let add_hist le = {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,7 +146,7 @@ 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 @@ -157,12 +157,12 @@ let deduce lie = !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 diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 4b70201b2..7274324d3 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -8,8 +8,8 @@ -(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients -des inéquations et équations sont entiers. En attendant la tactique Field. +(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients +des inéquations et équations sont entiers. En attendant la tactique Field. *) open Term @@ -22,10 +22,10 @@ open Fourier open Contradiction (****************************************************************************** -Opérations sur les combinaisons linéaires affines. -La partie homogène d'une combinaison linéaire est en fait une table de hash +Opérations sur les combinaisons linéaires affines. +La partie homogène d'une combinaison linéaire est en fait une table de hash qui donne le coefficient d'un terme du calcul des constructions, -qui est zéro si le terme n'y est pas. +qui est zéro si le terme n'y est pas. *) module Constrhash = Hashtbl.Make @@ -175,9 +175,9 @@ let flin_to_alist f = !res ;; -(* Représentation des hypothèses qui sont des inéquations ou des équations. +(* Représentation des hypothèses qui sont des inéquations ou des équations. *) -type hineq={hname:constr; (* le nom de l'hypothèse *) +type hineq={hname:constr; (* le nom de l'hypothèse *) htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) hleft:constr; hright:constr; @@ -185,7 +185,7 @@ type hineq={hname:constr; (* le nom de l'hypothèse *) hstrict:bool} ;; -(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 +(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 *) exception NoIneq @@ -256,12 +256,12 @@ let ineq1_of_constr (h,t) = |_-> raise NoIneq ;; -(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) +(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) *) let fourier_lineq lineq1 = let nvar=ref (-1) in - let hvar=Constrhash.create 50 in (* la table des variables des inéquations *) + let hvar=Constrhash.create 50 in (* la table des variables des inéquations *) List.iter (fun f -> Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin nvar:=(!nvar)+1; @@ -342,7 +342,7 @@ let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le") let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp") (****************************************************************************** -Construction de la preuve en cas de succès de la méthode de Fourier, +Construction de la preuve en cas de succès de la méthode de Fourier, i.e. on obtient une contradiction. *) let is_int x = (x.den)=1 @@ -461,15 +461,15 @@ let mkAppL a = exception GoalDone -(* Résolution d'inéquations linéaires dans R *) +(* Résolution d'inéquations linéaires dans R *) let rec fourier () = Proofview.Goal.nf_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 let fhyp=Id.of_string "new_hyp_for_fourier" in - (* si le but est une inéquation, on introduit son contraire, - et le but à prouver devient False *) + (* si le but est une inéquation, on introduit son contraire, + et le but à prouver devient False *) try match (kind_of_term goal) with App (f,args) -> @@ -497,23 +497,23 @@ let rec fourier () = |_-> raise GoalDone) |_-> raise GoalDone with GoalDone -> - (* les hypothèses *) + (* les hypothèses *) let hyps = List.map (fun (h,t)-> (mkVar h,t)) (list_of_sign (Proofview.Goal.hyps gl)) in let lineq =ref [] in List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) with NoIneq -> ()) hyps; - (* lineq = les inéquations découlant des hypothèses *) + (* lineq = les inéquations découlant des hypothèses *) if !lineq=[] then Errors.error "No inequalities"; let res=fourier_lineq (!lineq) in let tac=ref (Proofview.tclUNIT ()) in if res=[] then Errors.error "fourier failed" - (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) + (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> - (* lc=coefficients multiplicateurs des inéquations + (* lc=coefficients multiplicateurs des inéquations qui donnent 0<cres ou 0<=cres selon sres *) (*print_string "Fourier's method can prove the goal...";flush stdout;*) let lutil=ref [] in @@ -523,7 +523,7 @@ let rec fourier () = then (lutil:=(h,c)::(!lutil)(*; print_rational(c);print_string " "*))) (List.combine (!lineq) lc); - (* on construit la combinaison linéaire des inéquation *) + (* on construit la combinaison linéaire des inéquation *) (match (!lutil) with (h1,c1)::lutil -> let s=ref (h1.hstrict) in @@ -603,7 +603,7 @@ let rec fourier () = (mkApp (get coq_Rinv, [|get coq_R1|])) (get coq_R1)) -(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) +(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) [Tacticals.New.tclORELSE (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) |