des inéquations et équations sont entiers. En attendant la tactique Field.
*)
-(*open Term
-open Tactics
-open Clenv
-open Names
+(*open Term // in coq/kernel
+open Tactics
+open Clenv
+open Names
open Tacmach*)
open Fourier
(******************************************************************************
+Operations on linear combinations.
+
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.
*)
-(*type flin = {fhom:(constr , rational)Hashtbl.t;
- fcste:rational};;
-let flin_zero () = {fhom=Hashtbl.create 50;fcste=r0};;
-let flin_coef f x = try (Hashtbl.find f.fhom x) with _-> r0;;
+(**
+ The type for linear combinations
+*)
+type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
+;;
+
+(**
+ @return an empty flin
+*)
+let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
+;;
-let flin_add f x c =
+(**
+ @param f a flin
+ @param x a Cic.term
+ @return the rational associated with x (coefficient)
+*)
+let flin_coef f x =
+ try
+ (Hashtbl.find f.fhom x)
+ with
+ _ -> r0
+;;
+
+(**
+ Adds c to the coefficient of x
+ @param f a flin
+ @param x a Cic.term
+ @param c a rational
+ @return the new flin
+*)
+let flin_add f x c =
let cx = flin_coef f x in
Hashtbl.remove f.fhom x;
Hashtbl.add f.fhom x (rplus cx c);
f
;;
-let flin_add_cste f c =
+(**
+ Adds c to f.fcste
+ @param f a flin
+ @param c a rational
+ @return the new flin
+*)
+let flin_add_cste f c =
{fhom=f.fhom;
fcste=rplus f.fcste c}
;;
+(**
+ @return a empty flin with r1 in fcste
+*)
let flin_one () = flin_add_cste (flin_zero()) r1;;
+(**
+ Adds two flin
+*)
let flin_plus f1 f2 =
let f3 = flin_zero() in
Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
;;
+(**
+ Substracts two flin
+*)
let flin_minus f1 f2 =
let f3 = flin_zero() in
Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
;;
+
+(**
+ @return f times a
+*)
let flin_emult a f =
let f2 = flin_zero() in
Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
flin_add_cste f2 (rmult a f.fcste);
-;;*)
-
+;;
+
+
(*****************************************************************************)
-(*let parse_ast = Pcoq.parse_string Pcoq.Constr.constr;;
+
+(*
+
+ no idea about helm parser ??????????????????????????????
+
+let parse_ast = Pcoq.parse_string Pcoq.Constr.constr;;
let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
let pf_parse_constr gl s =
Astterm.interp_constr Evd.empty (pf_env gl) (parse_ast s);;
+*)
+
-let rec string_of_constr c =
- match kind_of_term c with
- Cast (c,t) -> string_of_constr c
- |Const c -> string_of_path c
- |Var(c) -> string_of_id c
+(**
+ @param t a term
+ @return proiection on string of t
+*)
+let rec string_of_term t =
+ match t with
+ Cic.Cast (t1,t2) -> string_of_term t1
+ |Cic.Const (u,boh) -> UriManager.string_of_uri u
+ |Cic.Var (u) -> UriManager.string_of_uri u
| _ -> "not_of_constant"
;;
-let rec rational_of_constr c =
- match kind_of_term c with
- | Cast (c,t) -> (rational_of_constr c)
- | App (c,args) ->
- (match kind_of_term c with
- Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.Ropp" ->
- rop (rational_of_constr args.(0))
- |"Coq.Reals.Rdefinitions.Rinv" ->
- rinv (rational_of_constr args.(0))
- |"Coq.Reals.Rdefinitions.Rmult" ->
- rmult (rational_of_constr args.(0))
- (rational_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rdiv" ->
- rdiv (rational_of_constr args.(0))
- (rational_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rplus" ->
- rplus (rational_of_constr args.(0))
- (rational_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rminus" ->
- rminus (rational_of_constr args.(0))
- (rational_of_constr args.(1))
+(* coq wrapper
+let string_of_constr = string_of_term
+;;
+*)
+
+(**
+ @param t a term
+ @raise Failure if conversion is impossible
+ @return rational proiection of t
+*)
+let rec rational_of_term t =
+ (* fun to apply f to the first and second rational-term of l *)
+ let rat_of_binop f l =
+ let a = List.hd l and
+ b = List.hd(List.tl l) in
+ f (rational_of_term a) (rational_of_term b)
+ in
+ (* as before, but f is unary *)
+ let rat_of_unop f l =
+ f (rational_of_term (List.hd l))
+ in
+ match t with
+ | Cic.Cast (t1,t2) -> (rational_of_term t1)
+ | Cic.Appl (t1::next) ->
+ (match t1 with
+ Cic.Const (u,boh) ->
+ (match (UriManager.string_of_uri u) with
+ "cic:/Coq/Reals/Rdefinitions/Ropp" ->
+ rat_of_unop rop next
+ |"cic:/Coq/Reals/Rdefinitions/Rinv" ->
+ rat_of_unop rinv next
+ |"cic:/Coq/Reals/Rdefinitions/Rmult" ->
+ rat_of_binop rmult next
+ |"cic:/Coq/Reals/Rdefinitions/Rdiv" ->
+ rat_of_binop rdiv next
+ |"cic:/Coq/Reals/Rdefinitions/Rplus" ->
+ rat_of_binop rplus next
+ |"cic:/Coq/Reals/Rdefinitions/Rminus" ->
+ rat_of_binop rminus next
| _ -> failwith "not a rational")
| _ -> failwith "not a rational")
- | Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.R1" -> r1
- |"Coq.Reals.Rdefinitions.R0" -> r0
+ | Cic.Const (u,boh) ->
+ (match (UriManager.string_of_uri u) with
+ "cic:/Coq/Reals/Rdefinitions/R1" -> r1
+ |"cic:/Coq/Reals/Rdefinitions/R0" -> r0
| _ -> failwith "not a rational")
| _ -> failwith "not a rational"
;;
-let rec flin_of_constr c =
+(* coq wrapper
+let rational_of_const = rational_of_term;;
+*)
+
+
+let rec flin_of_term t =
+ let fl_of_binop f l =
+ let a = List.hd l and
+ b = List.hd(List.tl l) in
+ f (flin_of_term a) (flin_of_term b)
+ in
try(
- match kind_of_term c with
- | Cast (c,t) -> (flin_of_constr c)
- | App (c,args) ->
- (match kind_of_term c with
- Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.Ropp" ->
- flin_emult (rop r1) (flin_of_constr args.(0))
- |"Coq.Reals.Rdefinitions.Rplus"->
- flin_plus (flin_of_constr args.(0))
- (flin_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rminus"->
- flin_minus (flin_of_constr args.(0))
- (flin_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rmult"->
- (try (let a=(rational_of_constr args.(0)) in
- try (let b = (rational_of_constr args.(1)) in
- (flin_add_cste (flin_zero()) (rmult a b)))
- with _-> (flin_add (flin_zero())
- args.(1)
- a))
- with _-> (flin_add (flin_zero())
- args.(0)
- (rational_of_constr args.(1))))
- |"Coq.Reals.Rdefinitions.Rinv"->
- let a=(rational_of_constr args.(0)) in
+ match t with
+ | Cic.Cast (t1,t2) -> (flin_of_term t1)
+ | Cic.Appl (t1::next) ->
+ begin
+ match t1 with
+ Cic.Const (u,boh) ->
+ begin
+ match (UriManager.string_of_uri u) with
+ "cic:/Coq/Reals/Rdefinitions/Ropp" ->
+ flin_emult (rop r1) (flin_of_term (List.hd next))
+ |"cic:/Coq/Reals/Rdefinitions/Rplus"->
+ fl_of_binop flin_plus next
+ |"cic:/Coq/Reals/Rdefinitions/Rminus"->
+ fl_of_binop flin_minus next
+ |"cic:/Coq/Reals/Rdefinitions/Rmult"->
+ begin
+ let arg1 = (List.hd next) and
+ arg2 = (List.hd(List.tl next))
+ in
+ try
+ begin
+ let a = rational_of_term arg1 in
+ try
+ begin
+ let b = (rational_of_term arg2) in
+ (flin_add_cste (flin_zero()) (rmult a b))
+ end
+ with
+ _ -> (flin_add (flin_zero()) arg2 a)
+ end
+ with
+ _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
+ end
+ |"cic:/Coq/Reals/Rdefinitions/Rinv"->
+ let a=(rational_of_term (List.hd next)) in
flin_add_cste (flin_zero()) (rinv a)
- |"Coq.Reals.Rdefinitions.Rdiv"->
- (let b=(rational_of_constr args.(1)) in
- try (let a = (rational_of_constr args.(0)) in
- (flin_add_cste (flin_zero()) (rdiv a b)))
- with _-> (flin_add (flin_zero())
- args.(0)
- (rinv b)))
- |_->assert false)
- |_ -> assert false)
- | Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.R1" -> flin_one ()
- |"Coq.Reals.Rdefinitions.R0" -> flin_zero ()
- |_-> assert false)
+ |"cic:/Coq/Reals/Rdefinitions/Rdiv"->
+ begin
+ let b=(rational_of_term (List.hd(List.tl next))) in
+ try
+ begin
+ let a = (rational_of_term (List.hd next)) in
+ (flin_add_cste (flin_zero()) (rdiv a b))
+ end
+ with
+ _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
+ end
+ |_->assert false
+ end
+ |_ -> assert false
+ end
+ | Cic.Const (u,boh) ->
+ begin
+ match (UriManager.string_of_uri u) with
+ "cic:/Coq/Reals/Rdefinitions/R1" -> flin_one ()
+ |"cic:/Coq/Reals/Rdefinitions/R0" -> flin_zero ()
+ |_-> assert false
+ end
|_-> assert false)
- with _ -> flin_add (flin_zero())
- c
- r1
+ with _ -> flin_add (flin_zero()) t r1
;;
+(* coq wrapper
+let flin_of_constr = flin_of_term;;
+*)
+
+(*
let flin_to_alist f =
let res=ref [] in
Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
(* 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;
projects / helm.git / commitdiff