From af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 9 Dec 2014 12:48:32 +0100 Subject: Switch the few remaining iso-latin-1 files to utf8 --- plugins/cc/README | 2 +- plugins/extraction/README | 6 +- plugins/fourier/fourier.ml | 52 ++++++------- plugins/fourier/fourierR.ml | 40 +++++----- plugins/micromega/sos.ml | 4 +- plugins/micromega/sos_lib.ml | 4 +- plugins/nsatz/polynom.ml | 2 +- plugins/omega/coq_omega.ml | 2 +- plugins/omega/g_omega.ml4 | 2 +- plugins/omega/omega.ml | 11 +-- plugins/romega/const_omega.ml | 2 +- plugins/romega/const_omega.mli | 2 +- plugins/romega/g_romega.ml4 | 2 +- plugins/romega/refl_omega.ml | 168 ++++++++++++++++++++--------------------- 14 files changed, 145 insertions(+), 154 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/README b/plugins/cc/README index 073b140ea..c616b5daa 100644 --- a/plugins/cc/README +++ b/plugins/cc/README @@ -3,7 +3,7 @@ cctac: congruence-closure for coq author: Pierre Corbineau, Stage de DEA au LSV, ENS Cachan - Thèse au LRI, Université Paris Sud XI + Thèse au LRI, Université Paris Sud XI Files : diff --git a/plugins/extraction/README b/plugins/extraction/README index a9a7b04d5..458ba0deb 100644 --- a/plugins/extraction/README +++ b/plugins/extraction/README @@ -14,7 +14,7 @@ Who did it ? ------------ The current implementation (from version 7.0 up to now) has been done -by P. Letouzey during his PhD, helped by J.C. Filliâtre and supervised +by P. Letouzey during his PhD, helped by J.C. Filliâtre and supervised by C. Paulin. An earlier implementation (versions 6.x) was due to B. Werner and @@ -118,7 +118,7 @@ Axioms, and then "Extract Constant ..." [1]: -Exécution de termes de preuves: une nouvelle méthode d'extraction +Exécution de termes de preuves: une nouvelle méthode d'extraction pour le Calcul des Constructions Inductives, Pierre Letouzey, DEA thesis, 2000, http://www.pps.jussieu.fr/~letouzey/download/rapport_dea.ps.gz @@ -129,7 +129,7 @@ Types 2002 Post-Workshop Proceedings. http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz [3]: -Programmation fonctionnelle certifiée: l'extraction de programmes +Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. Pierre Letouzey, PhD thesis, 2004. http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.ps.gz http://www.pps.jussieu.fr/~letouzey/download/these_letouzey_English.ps.gz 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 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 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 ()) diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index 35699f219..cc89e2b9d 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -1,9 +1,9 @@ (* ========================================================================= *) (* - This code originates from John Harrison's HOL LIGHT 2.30 *) (* (see file LICENSE.sos for license, copyright and disclaimer) *) -(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) +(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) (* independent bits *) -(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) +(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) (* ========================================================================= *) (* ========================================================================= *) diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index 235f9ce9b..f54914f25 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -2,9 +2,9 @@ (* - This code originates from John Harrison's HOL LIGHT 2.30 *) (* (see file LICENSE.sos for license, copyright and disclaimer) *) (* This code is the HOL LIGHT library code used by sos.ml *) -(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) +(* - Laurent Théry (thery@sophia.inria.fr) has isolated the HOL *) (* independent bits *) -(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) +(* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) (* ========================================================================= *) open Num diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 8566cf0d6..464bc7740 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -602,7 +602,7 @@ and pgcd_pol_rec p q x = res ) -(* Sub-résultants: +(* Sub-résultants: ai*Ai = Qi*Ai+1 + bi*Ai+2 diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index b35ef1772..6d575a541 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -9,7 +9,7 @@ (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) (* *) -(* Pierre Crégut (CNET, Lannion, France) *) +(* Pierre Crégut (CNET, Lannion, France) *) (* *) (**************************************************************************) diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 83092ccc4..e425cff52 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -9,7 +9,7 @@ (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) (* *) -(* Pierre Crégut (CNET, Lannion, France) *) +(* Pierre Crégut (CNET, Lannion, France) *) (* *) (**************************************************************************) diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 4e9ca6ffc..efecc8add 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -9,7 +9,7 @@ (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) (* *) -(* Pierre Crégut (CNET, Lannion, France) *) +(* Pierre Crégut (CNET, Lannion, France) *) (* *) (* 13/10/2002 : modified to cope with an external numbering of equations *) (* and hypothesis. Its use for Omega is not more complex and it makes *) @@ -585,15 +585,6 @@ let rec depend relie_on accu = function end | [] -> relie_on, accu -(* -let depend relie_on accu trace = - Printf.printf "Longueur de la trace initiale : %d\n" - (trace_length trace + trace_length accu); - let rel',trace' = depend relie_on accu trace in - Printf.printf "Longueur de la trace simplifiée : %d\n" (trace_length trace'); - rel',trace' -*) - let solve (new_eq_id,new_eq_var,print_var) system = try let _ = simplify new_eq_id false system in failwith "no contradiction" with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ()))) diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 3fa9e02cf..21b0f78b5 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -1,7 +1,7 @@ (************************************************************************* PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D + Author: Pierre Crégut - France Télécom R&D Licence : LGPL version 2.1 *************************************************************************) diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index 4ae1cb94c..af50ea0ff 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -1,7 +1,7 @@ (************************************************************************* PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D + Author: Pierre Crégut - France Télécom R&D Licence : LGPL version 2.1 *************************************************************************) diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 4b6c9b790..0a99a26b3 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -1,7 +1,7 @@ (************************************************************************* PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D + Author: Pierre Crégut - France Télécom R&D Licence : LGPL version 2.1 *************************************************************************) diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index f9219407e..8156e8411 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1,7 +1,7 @@ (************************************************************************* PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D + Author: Pierre Crégut - France Télécom R&D Licence : LGPL version 2.1 *************************************************************************) @@ -42,8 +42,8 @@ let occ_step_eq s1 s2 = match s1, s2 with | O_left, O_left | O_right, O_right | O_mono, O_mono -> true | _ -> false -(* 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 *) +(* 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} (* \subsection{refiable formulas} *) @@ -63,7 +63,7 @@ type oformula = (* Operators for comparison recognized by Omega *) type comparaison = Eq | Leq | Geq | Gt | Lt | Neq -(* Type des prédicats réifiés (fragment de calcul propositionnel. Les +(* Type des prédicats réifiés (fragment de calcul propositionnel. Les * quantifications sont externes au langage) *) type oproposition = Pequa of Term.constr * oequation @@ -75,19 +75,19 @@ type oproposition = | Pimp of int * oproposition * oproposition | Pprop of Term.constr -(* Les équations ou proposiitions atomiques utiles du calcul *) +(* Les équations ou proposiitions atomiques utiles du calcul *) and oequation = { e_comp: comparaison; (* comparaison *) 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_negated: bool; (* vrai si apparait en position nié - après normalisation *) + e_origin: occurence; (* 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 - dépend l'accès à l'équation avec la - direction (branche) pour y accéder *) - e_omega: afine (* la fonction normalisée *) + dépend l'accès à l'équation avec la + direction (branche) pour y accéder *) + e_omega: afine (* la fonction normalisée *) } (* \subsection{Proof context} @@ -106,8 +106,8 @@ type environment = { mutable props : Term.constr list; (* Les variables introduites par omega *) mutable om_vars : (oformula * int) list; - (* Traduction des indices utilisés ici en les indices finaux utilisés par - * la tactique Omega après dénombrement des variables utiles *) + (* Traduction des indices utilisés ici en les indices finaux utilisés par + * la tactique Omega après dénombrement des variables utiles *) real_indices : (int,int) Hashtbl.t; mutable cnt_connectors : int; equations : (int,oequation) Hashtbl.t; @@ -115,35 +115,35 @@ type environment = { } (* \subsection{Solution tree} - Définition d'une solution trouvée par Omega sous la forme d'un identifiant, - d'un ensemble d'équation dont dépend la solution et d'une trace *) -(* La liste des dépendances est triée et sans redondance *) + Définition d'une solution trouvée par Omega sous la forme d'un identifiant, + d'un ensemble d'équation dont dépend la solution et d'une trace *) +(* La liste des dépendances est triée et sans redondance *) type solution = { s_index : int; s_equa_deps : int list; s_trace : action list } -(* Arbre de solution résolvant complètement un ensemble de systèmes *) +(* Arbre de solution résolvant complètement un ensemble de systèmes *) type solution_tree = Leaf of solution - (* un noeud interne représente un point de branchement correspondant à - l'élimination d'un connecteur générant plusieurs buts + (* un noeud interne représente un point de branchement correspondant à + l'élimination d'un connecteur générant plusieurs buts (typ. disjonction). Le premier argument est l'identifiant du connecteur *) | Tree of int * solution_tree * solution_tree -(* Représentation de l'environnement extrait du but initial sous forme de - chemins pour extraire des equations ou d'hypothèses *) +(* Représentation de l'environnement extrait du but initial sous forme de + chemins pour extraire des equations ou d'hypothèses *) type context_content = CCHyp of occurence | CCEqua of int (* \section{Specific utility functions to handle base types} *) -(* Nom arbitraire de l'hypothèse codant la négation du but final *) +(* Nom arbitraire de l'hypothèse codant la négation du but final *) let id_concl = Names.Id.of_string "__goal__" -(* Initialisation de l'environnement de réification de la tactique *) +(* Initialisation de l'environnement de réification de la tactique *) let new_environment () = { terms = []; props = []; om_vars = []; cnt_connectors = 0; real_indices = Hashtbl.create 7; @@ -151,17 +151,17 @@ let new_environment () = { constructors = Hashtbl.create 7; } -(* Génération d'un nom d'équation *) +(* Génération d'un nom d'équation *) let new_connector_id env = env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors -(* Calcul de la branche complémentaire *) +(* Calcul de la branche complémentaire *) let barre = function Left x -> Right x | Right x -> Left x -(* Identifiant associé à une branche *) +(* Identifiant associé à une branche *) let indice = function Left x | Right x -> x -(* Affichage de l'environnement de réification (termes et propositions) *) +(* Affichage de l'environnement de réification (termes et propositions) *) let print_env_reification env = let rec loop c i = function [] -> str " ===============================\n\n" @@ -189,12 +189,12 @@ let new_omega_var, rst_omega_var = (function () -> incr cpt; !cpt), (function () -> cpt:=0) -(* Affichage des variables d'un système *) +(* Affichage des variables d'un système *) let display_omega_var i = Printf.sprintf "OV%d" i -(* Recherche la variable codant un terme pour Omega et crée la variable dans - l'environnement si il n'existe pas. Cas ou la variable dans Omega représente +(* Recherche la variable codant un terme pour Omega et crée la variable dans + l'environnement si il n'existe pas. Cas ou la variable dans Omega représente le terme d'un monome (le plus souvent un atome) *) let intern_omega env t = @@ -204,22 +204,22 @@ let intern_omega env t = env.om_vars <- (t,v) :: env.om_vars; v end -(* Ajout forcé d'un lien entre un terme et une variable Cas où la - variable est créée par Omega et où il faut la lier après coup à un atome - réifié introduit de force *) +(* Ajout forcé d'un lien entre un terme et une variable Cas où la + variable est créée par Omega et où il faut la lier après coup à un atome + réifié introduit de force *) let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars -(* Récupère le terme associé à une variable *) +(* Récupère le terme associé à une variable *) let unintern_omega env id = let rec loop = function [] -> failwith "unintern" | ((t,j)::l) -> if Int.equal id j then t else loop l in loop env.om_vars -(* \subsection{Gestion des environnements de variable pour la réflexion} +(* \subsection{Gestion des environnements de variable pour la réflexion} Gestion des environnements de traduction entre termes des constructions - non réifiés et variables des termes reifies. Attention il s'agit de - l'environnement initial contenant tout. Il faudra le réduire après + non réifiés et variables des termes reifies. Attention il s'agit de + l'environnement initial contenant tout. Il faudra le réduire après calcul des variables utiles. *) let add_reified_atom t env = @@ -238,24 +238,24 @@ let add_prop env t = with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i -(* accès a une proposition *) +(* accès a une proposition *) let get_prop v env = try List.nth v env with Invalid_argument _ -> failwith "get_prop" -(* \subsection{Gestion du nommage des équations} *) +(* \subsection{Gestion du nommage des équations} *) (* Ajout d'une equation dans l'environnement de reification *) let add_equation env e = let id = e.e_omega.id in try let _ = Hashtbl.find env.equations id in () with Not_found -> Hashtbl.add env.equations id e -(* accès a une equation *) +(* accès a une equation *) let get_equation env id = try Hashtbl.find env.equations id with Not_found as e -> - Printf.printf "Omega Equation %d non trouvée\n" id; raise e + Printf.printf "Omega Equation %d non trouvée\n" id; raise e -(* Affichage des termes réifiés *) +(* Affichage des termes réifiés *) let rec oprint ch = function | Oint n -> Printf.fprintf ch "%s" (Bigint.to_string n) | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2 @@ -289,7 +289,7 @@ let rec weight env = function | Oufo _ -> -1 | Oatom _ as c -> (intern_omega env c) -(* \section{Passage entre oformules et représentation interne de Omega} *) +(* \section{Passage entre oformules et représentation interne de Omega} *) (* \subsection{Oformula vers Omega} *) @@ -332,12 +332,12 @@ let coq_of_formula env t = | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in loop t -(* \subsection{Oformula vers COQ reifié} *) +(* \subsection{Oformula vers COQ reifié} *) let reified_of_atom env i = try Hashtbl.find env.real_indices i with Not_found -> - Printf.printf "Atome %d non trouvé\n" i; + Printf.printf "Atome %d non trouvé\n" i; Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices; raise Not_found @@ -390,7 +390,7 @@ let reified_of_proposition env f = try reified_of_proposition env f with reraise -> pprint stderr f; raise reraise -(* \subsection{Omega vers COQ réifié} *) +(* \subsection{Omega vers COQ réifié} *) let reified_of_omega env body constant = let coeff_constant = @@ -407,13 +407,13 @@ let reified_of_omega env body c = try reified_of_omega env body c with reraise -> display_eq display_omega_var (body,c); raise reraise -(* \section{Opérations sur les équations} -Ces fonctions préparent les traces utilisées par la tactique réfléchie -pour faire des opérations de normalisation sur les équations. *) +(* \section{Opérations sur les équations} +Ces fonctions préparent les traces utilisées par la tactique réfléchie +pour faire des opérations de normalisation sur les équations. *) -(* \subsection{Extractions des variables d'une équation} *) -(* Extraction des variables d'une équation. *) -(* Chaque fonction retourne une liste triée sans redondance *) +(* \subsection{Extractions des variables d'une équation} *) +(* Extraction des variables d'une équation. *) +(* Chaque fonction retourne une liste triée sans redondance *) let (@@) = List.merge_uniq compare @@ -482,7 +482,7 @@ let rec negate = function let norm l = (List.length l) -(* \subsection{Mélange (fusion) de deux équations} *) +(* \subsection{Mélange (fusion) de deux équations} *) (* \subsubsection{Version avec coefficients} *) let shuffle_path k1 e1 k2 e2 = let rec loop = function @@ -531,7 +531,7 @@ let rec shuffle env (t1,t2) = do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1) else do_list [],Oplus(t1,t2) -(* \subsection{Fusion avec réduction} *) +(* \subsection{Fusion avec réduction} *) let shrink_pair f1 f2 = begin match f1,f2 with @@ -563,7 +563,7 @@ let reduce_factor = function [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c)) | t -> Errors.error "reduce_factor.1" -(* \subsection{Réordonnancement} *) +(* \subsection{Réordonnancement} *) let rec condense env = function Oplus(f1,(Oplus(f2,r) as t)) -> @@ -596,7 +596,7 @@ let rec condense env = function let final = Oplus(t',Oint zero) in tac @ [Lazy.force coq_c_red6], final -(* \subsection{Elimination des zéros} *) +(* \subsection{Elimination des zéros} *) let rec clear_zero = function Oplus(Omult(Oatom v,Oint n),r) when Bigint.equal n zero -> @@ -607,7 +607,7 @@ let rec clear_zero = function (if List.is_empty tac then [] else [do_right (do_list tac)]),Oplus(f,t) | t -> [],t;; -(* \subsection{Transformation des hypothèses} *) +(* \subsection{Transformation des hypothèses} *) let rec reduce env = function Oplus(t1,t2) -> @@ -642,7 +642,7 @@ let normalize_linear_term env t = let trace3,t3 = clear_zero t2 in do_list [trace1; do_list trace2; do_list trace3], t3 -(* Cette fonction reproduit très exactement le comportement de [p_invert] *) +(* Cette fonction reproduit très exactement le comportement de [p_invert] *) let negate_oper = function Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq @@ -668,7 +668,7 @@ let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) = INEQ with e when Logic.catchable_exception e -> raise e -(* \section{Compilation des hypothèses} *) +(* \section{Compilation des hypothèses} *) let rec oformula_of_constr env t = match Z.parse_term t with @@ -697,7 +697,7 @@ and binprop env (neg2,depends,origin,path) oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in let t2' = oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in - (* On numérote le connecteur dans l'environnement. *) + (* On numérote le connecteur dans l'environnement. *) c i t1' t2' and mk_equation env ctxt c connector t1 t2 = @@ -736,7 +736,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1) | _ -> Pprop c -(* Destructuration des hypothèses et de la conclusion *) +(* Destructuration des hypothèses et de la conclusion *) let reify_gl env gl = let concl = Tacmach.pf_concl gl in @@ -819,9 +819,9 @@ let destructurate_hyps syst = | [] -> [[]] in loop syst -(* \subsection{Affichage d'un système d'équation} *) +(* \subsection{Affichage d'un système d'équation} *) -(* Affichage des dépendances de système *) +(* Affichage des dépendances de système *) let display_depend = function Left i -> Printf.printf " L%d" i | Right i -> Printf.printf " R%d" i @@ -852,8 +852,8 @@ let display_systems syst_list = List.iter display_equation syst in List.iter display_system syst_list -(* Extraction des prédicats utilisées dans une trace. Permet ensuite le - calcul des hypothèses *) +(* Extraction des prédicats utilisées dans une trace. Permet ensuite le + calcul des hypothèses *) let rec hyps_used_in_trace = function | act :: l -> @@ -865,9 +865,9 @@ let rec hyps_used_in_trace = function end | [] -> [] -(* Extraction des variables déclarées dans une équation. Permet ensuite - de les déclarer dans l'environnement de la procédure réflexive et - éviter les créations de variable au vol *) +(* Extraction des variables déclarées dans une équation. Permet ensuite + de les déclarer dans l'environnement de la procédure réflexive et + éviter les créations de variable au vol *) let rec variable_stated_in_trace = function | act :: l -> @@ -885,7 +885,7 @@ let rec variable_stated_in_trace = function let add_stated_equations env tree = (* Il faut trier les variables par ordre d'introduction pour ne pas risquer - de définir dans le mauvais ordre *) + de définir dans le mauvais ordre *) let stated_equations = let cmpvar x y = Pervasives.(-) x.st_var y.st_var in let rec loop = function @@ -894,15 +894,15 @@ let add_stated_equations env tree = in loop tree in let add_env st = - (* On retransforme la définition de v en formule reifiée *) + (* On retransforme la définition de v en formule reifiée *) let v_def = oformula_of_omega env st.st_def in - (* Notez que si l'ordre de création des variables n'est pas respecté, + (* Notez que si l'ordre de création des variables n'est pas respecté, * ca va planter *) let coq_v = coq_of_formula env v_def in let v = add_reified_atom coq_v env in (* Le terme qu'il va falloir introduire *) let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; coq_v|] in - (* sa représentation sous forme d'équation mais non réifié car on n'a pas + (* sa représentation sous forme d'équation mais non réifié car on n'a pas * l'environnement pour le faire correctement *) let term_to_reify = (v_def,Oatom v) in (* enregistre le lien entre la variable omega et la variable Coq *) @@ -910,8 +910,8 @@ let add_stated_equations env tree = (v, term_to_generalize,term_to_reify,st.st_def.id) in List.map add_env stated_equations -(* Calcule la liste des éclatements à réaliser sur les hypothèses - nécessaires pour extraire une liste d'équations donnée *) +(* Calcule la liste des éclatements à réaliser sur les hypothèses + nécessaires pour extraire une liste d'équations donnée *) (* PL: experimentally, the result order of the following function seems _very_ crucial for efficiency. No idea why. Do not remove the List.rev @@ -958,7 +958,7 @@ let really_useful_prop l_equa c = | Pnot t1 -> app coq_not [|real_of t1|] | Por(_,t1,t2) -> app coq_or [|real_of t1; real_of t2|] | Pand(_,t1,t2) -> app coq_and [|real_of t1; real_of t2|] - (* Attention : implications sur le lifting des variables à comprendre ! *) + (* Attention : implications sur le lifting des variables à comprendre ! *) | Pimp(_,t1,t2) -> Term.mkArrow (real_of t1) (real_of t2) | Pprop t -> t in let rec loop c = @@ -1166,11 +1166,11 @@ and decompose_tree_hyps trace env ctxt = function (* \section{La fonction principale} *) (* Cette fonction construit la -trace pour la procédure de décision réflexive. A partir des résultats -de l'extraction des systèmes, elle lance la résolution par Omega, puis +trace pour la procédure de décision réflexive. A partir des résultats +de l'extraction des systèmes, elle lance la résolution par Omega, puis l'extraction d'un ensemble minimal de solutions permettant la -résolution globale du système et enfin construit la trace qui permet -de faire rejouer cette solution par la tactique réflexive. *) +résolution globale du système et enfin construit la trace qui permet +de faire rejouer cette solution par la tactique réflexive. *) let resolution env full_reified_goal systems_list = let num = ref 0 in @@ -1181,7 +1181,7 @@ let resolution env full_reified_goal systems_list = simplify_strong (new_omega_eq,new_omega_var,display_omega_var) system in - (* calcule les hypotheses utilisées pour la solution *) + (* calcule les hypotheses utilisées pour la solution *) let vars = hyps_used_in_trace trace in let splits = get_eclatement env vars in if !debug then begin @@ -1202,7 +1202,7 @@ let resolution env full_reified_goal systems_list = display_solution_tree stdout solution_tree; print_newline() end; - (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *) + (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *) let useful_equa_id = equas_of_solution_tree solution_tree in (* recupere explicitement ces equations *) let equations = List.map (get_equation env) useful_equa_id in @@ -1225,8 +1225,8 @@ let resolution env full_reified_goal systems_list = let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in (* L'environnement de base se construit en deux morceaux : - - les variables des équations utiles (et de la conclusion) - - les nouvelles variables declarées durant les preuves *) + - les variables des équations utiles (et de la conclusion) + - les nouvelles variables declarées durant les preuves *) let all_vars_env = useful_vars @ stated_vars in let basic_env = let rec loop i = function @@ -1236,7 +1236,7 @@ let resolution env full_reified_goal systems_list = | [] -> [] in loop 0 all_vars_env in let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in - (* On peut maintenant généraliser le but : env est a jour *) + (* On peut maintenant généraliser le but : env est a jour *) let l_reified_stated = List.map (fun (_,_,(l,r),_) -> app coq_p_eq [| reified_of_formula env l; -- cgit v1.2.3