From c6b222d016300d3b123a4d1863c048b950292844 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Nov 2002 19:45:48 +0000 Subject: [PATCH] comments in fourier.ml now are in ocamldoc style bug in fourierR.ml (wrong Rel) solved --- helm/gTopLevel/fourier.ml | 53 +++++++++++++++++++++++++++++-------- helm/gTopLevel/fourierR.ml | 29 ++++++++++++-------- helm/gTopLevel/gTopLevel.ml | 9 ++++--- 3 files changed, 65 insertions(+), 26 deletions(-) diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml index c1a40e6e1..3704bf67b 100644 --- a/helm/gTopLevel/fourier.ml +++ b/helm/gTopLevel/fourier.ml @@ -21,7 +21,7 @@ Pages: 326-327 http://gallica.bnf.fr/ *) - +(** @author The Coq Development Team *) (* Un peu de calcul sur les rationnels... @@ -30,10 +30,14 @@ i.e. le num *) +(** Type for coefficents *) +type rational = { +num:int; (** Numerator *) +den:int; (** Denumerator *) +};; -type rational = {num:int; - den:int} -;; +(** Debug function. + @param x the rational to print*) let print_rational x = print_int x.num; print_string "/"; @@ -42,8 +46,9 @@ let print_rational x = let rec pgcd x y = if y = 0 then x else pgcd y (x mod y);; - +(** The constant 0*) let r0 = {num=0;den=1};; +(** The constant 1*) let r1 = {num=1;den=1};; let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in @@ -51,22 +56,41 @@ let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in else (let d=pgcd x.num x.den in let d= (if d<0 then -d else d) in {num=(x.num)/d;den=(x.den)/d});; - + +(** Calculates the opposite of a rational. + @param x The rational + @return -x*) let rop x = rnorm {num=(-x.num);den=x.den};; +(** Sums two rationals. + @param x A rational + @param y Another rational + @return x+y*) let rplus x y = rnorm {num=x.num*y.den + y.num*x.den;den=x.den*y.den};; - +(** Substracts two rationals. + @param x A rational + @param y Another rational + @return x-y*) let rminus x y = rnorm {num=x.num*y.den - y.num*x.den;den=x.den*y.den};; - +(** Multiplyes two rationals. + @param x A rational + @param y Another rational + @return x*y*) let rmult x y = rnorm {num=x.num*y.num;den=x.den*y.den};; - +(** Inverts arational. + @param x A rational + @return x{^ -1} *) let rinv x = rnorm {num=x.den;den=x.num};; - +(** Divides two rationals. + @param x A rational + @param y Another rational + @return x/y*) 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 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. @@ -165,13 +189,20 @@ let deduce lie = !lie ;; -(* donne [] si le système a des solutions, +(* donne [] si le système a des find solutions, sinon donne [c,s,lc] 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. *) +(** Tryes to find if the system admits solutions. + @param lie the list of inequations + @return a list that can be empty if the system has solutions. Otherwise it returns a + one elements list [\[(c,s,lc)\]]. {b c} is the rational that can be obtained solving the system, + {b s} is true if the inequation that proves that the system is absurd is of type [c < 0], false if + [c <= 0], {b lc} is a list of rational that represents the liear combination to obtain the + absurd inequation *) let unsolvable lie = let lr = deduce lie in let res = ref [] in diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 17ff3f8fe..d6d5fd34a 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -461,7 +461,7 @@ let fourier_lineq lineq1 = debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n"); let sys= List.map (fun h-> let v=Array.create ((!nvar)+1) r0 in - Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c) + Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c) h.hflin.fhom; ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) lineq1 in @@ -847,7 +847,7 @@ let rec strip_outer_cast c = match c with | _ -> c ;; -let find_in_context id context = +(*let find_in_context id context = let rec find_in_context_aux c n = match c with [] -> failwith (id^" not found in context") @@ -865,10 +865,26 @@ let rec filter_real_hyp context cont = [] -> [] | Some(Cic.Name(h),Cic.Decl(t))::next -> ( let n = find_in_context h cont in + debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n"); [(Cic.Rel(n),t)] @ filter_real_hyp next cont) | a::next -> debug(" no\n"); filter_real_hyp next cont +;;*) +let filter_real_hyp context _ = + let rec filter_aux context num = + match context with + [] -> [] + | Some(Cic.Name(h),Cic.Decl(t))::next -> + ( + (*let n = find_in_context h cont in*) + debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n"); + [(Cic.Rel(num),t)] @ filter_aux next (num+1) + ) + | a::next -> filter_aux next (num+1) + in + filter_aux context 1 ;; + (* lifts everithing at the conclusion level *) let rec superlift c n= match c with @@ -1192,7 +1208,6 @@ theoreme,so let's parse our thesis *) let w1 = debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n"); (match ty with - (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*) Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a]) |_ -> assert false) in @@ -1203,14 +1218,6 @@ theoreme,so let's parse our thesis *) ) ~continuation:(*PORTINGTacticals.id_tac*)tac2])) ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) - (*tac:=(Tacticals.thens - ~start:(PrimitiveTactics.cut_tac ~term:_False) - ~continuations:[Tacticals.then_ - ~start:(PrimitiveTactics.intros_tac ~name:"??") - ~continuation:contradiction_tac - ;!tac]) FIXED - this was useless*) - (* tac:=!tac*) - |_-> assert false)(*match (!lutil) *) |_-> assert false); (*match res*) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 8aa9e8288..aca0fe12d 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -60,18 +60,19 @@ let htmlfooter = "" ;; -(* +(* TASSI let prooffile = "/home/tassi/miohelm/tmp/currentproof";; -let prooffile = "/public/sacerdot/currentproof";; +let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";; *) let prooffile = "/public/sacerdot/currentproof";; let prooffiletype = "/public/sacerdot/currentprooftype";; (*CSC: the getter should handle the innertypes, not the FS *) -(* + +(* TASSI let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; -let innertypesfile = "/public/sacerdot/innertypes";; +let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";; *) let innertypesfile = "/public/sacerdot/innertypes";; -- 2.39.2