http://gallica.bnf.fr/
*)
-
+(** @author The Coq Development Team *)
(* Un peu de calcul sur les rationnels...
*)
+(** 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 "/";
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
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.
!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
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
| _ -> 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")
[] -> []
| 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
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
)
~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*)
"</html>"
;;
-(*
+(* 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";;
projects / helm.git / commitdiff