let symbol_table = Hashtbl.create 503;;
(* eq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "eq",
- None, Some "cic:/Coq/Init/Logic/eq.ind"))
+ None, Some HelmLibraryObjects.Logic.eq_SURI))
:: List.map acic2cexpr (List.tl args)));;
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)"
- (fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "eq",
- None, Some "cic:/Coq/Init/Logic_Type/eqT.ind"))
- :: List.map acic2cexpr (List.tl args)));;
-
(* and *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.and_XURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "and",
- None, Some "cic:/Coq/Init/Logic/and.ind"))
+ None, Some HelmLibraryObjects.Logic.and_SURI))
:: List.map acic2cexpr args));;
(* or *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.or_XURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "or",
- None, Some "cic:/Coq/Init/Logic/or.ind"))
+ None, Some HelmLibraryObjects.Logic.or_SURI))
:: List.map acic2cexpr args));;
(* iff *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/iff.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.iff_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "iff",
- None, Some "cic:/Coq/Init/Logic/iff.con"))
+ None, Some HelmLibraryObjects.Logic.iff_SURI))
:: List.map acic2cexpr args));;
(* not *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.not_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "not",
- None, Some "cic:/Coq/Init/Logic/not.con"))
+ None, Some HelmLibraryObjects.Logic.not_SURI))
:: List.map acic2cexpr args));;
(* Rinv *)
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rinv.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rinv_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "inv",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+ None, Some HelmLibraryObjects.Reals.rinv_SURI))
:: List.map acic2cexpr args));;
(* Ropp *)
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Ropp.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.ropp_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "opp",
- None, Some "cic:/Coq/Reals/Rdefinitions/Ropp.con"))
+ None, Some HelmLibraryObjects.Reals.ropp_SURI))
:: List.map acic2cexpr args));;
(* exists *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)"
- (fun aid sid args acic2cexpr ->
- match (List.tl args) with
- [Cic.ALambda (_,Cic.Name n,s,t)] ->
- Binder
- (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
- | _ -> raise Not_found);;
-
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
(fun aid sid args acic2cexpr ->
match (List.tl args) with
[Cic.ALambda (_,Cic.Name n,s,t)] ->
| _ -> raise Not_found);;
(* leq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.le_XURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "leq",
- None, Some "cic:/Coq/Init/Peano/le.ind"))
+ None, Some HelmLibraryObjects.Peano.le_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rle_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "leq",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rle.con"))
+ None, Some HelmLibraryObjects.Reals.rle_SURI))
:: List.map acic2cexpr args));;
(* lt *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/lt.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.lt_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "lt",
- None, Some "cic:/Coq/Init/Peano/lt.con"))
+ None, Some HelmLibraryObjects.Peano.lt_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rlt.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rlt_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "lt",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rlt.con"))
+ None, Some HelmLibraryObjects.Reals.rlt_SURI))
:: List.map acic2cexpr args));;
(* geq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/ge.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.ge_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "geq",
- None, Some "cic:/Coq/Init/Peano/ge.con"))
+ None, Some HelmLibraryObjects.Peano.ge_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rge.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rge_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "geq",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rge.con"))
+ None, Some HelmLibraryObjects.Reals.rge_SURI))
:: List.map acic2cexpr args));;
(* gt *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/gt.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.gt_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "gt",
- None, Some "cic:/Coq/Init/Peano/gt.con"))
+ None, Some HelmLibraryObjects.Peano.gt_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rgt.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rgt_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "gt",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rgt.con"))
+ None, Some HelmLibraryObjects.Reals.rgt_SURI))
:: List.map acic2cexpr args));;
(* plus *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/plus.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.plus_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "plus",
- None, Some "cic:/Coq/Init/Peano/plus.con"))
+ None, Some HelmLibraryObjects.Peano.plus_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con"
+Hashtbl.add symbol_table HelmLibraryObjects.BinInt.zplus_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "plus",
- None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con"))
+ None, Some HelmLibraryObjects.BinInt.zplus_SURI))
:: List.map acic2cexpr args));;
-let rplus_uri =
- UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;;
-let r0_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" ;;
-let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;;
-
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
(fun aid sid args acic2cexpr ->
let appl () =
Appl
(Some aid, (Symbol (Some sid, "plus",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
+ None, Some HelmLibraryObjects.Reals.rplus_SURI))
:: List.map acic2cexpr args)
in
let rec aux acc = function
| [ Cic.AConst (nid, uri, []); n] when
- UriManager.eq uri r1_uri ->
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
(match n with
- | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
+ | Cic.AConst (_, uri, []) when
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
Num (Some aid, string_of_int (acc + 2))
| Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
- UriManager.eq uri rplus_uri ->
+ UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
aux (acc + 1) args
| _ -> appl ())
| _ -> appl ()
(**
- The type for linear combinations
+ The type for linear combinations
*)
-type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
+type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
;;
(**
- @return an empty flin
+ @return an empty flin
*)
let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
;;
(**
- @param f a flin
- @param x a Cic.term
- @return the rational associated with x (coefficient)
+ @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
+ 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
+ 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 =
match x with
f
;;
(**
- Adds c to f.fcste
- @param f a flin
- @param c a rational
- @return the new flin
+ 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;
;;
(**
- @return a empty flin with r1 in fcste
+ @return a empty flin with r1 in fcste
*)
let flin_one () = flin_add_cste (flin_zero()) r1;;
(**
- Adds two flin
+ Adds two flin
*)
let flin_plus f1 f2 =
let f3 = flin_zero() in
;;
(**
- Substracts two flin
+ Substracts two flin
*)
let flin_minus f1 f2 =
let f3 = flin_zero() in
;;
(**
- @return a times f
+ @return a times f
*)
let flin_emult a f =
let f2 = flin_zero() in
(**
- @param t a term
- @raise Failure if conversion is impossible
- @return rational proiection of t
+ @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)
+ 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))
+ 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.con" ->
- rat_of_unop rop next
- |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
+ if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then
+ rat_of_unop rop next
+ else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then
rat_of_unop rinv next
- |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
+ else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then
rat_of_binop rmult next
- |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
+ else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then
rat_of_binop rdiv next
- |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
+ else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then
rat_of_binop rplus next
- |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
+ else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then
rat_of_binop rminus next
- | _ -> failwith "not a rational")
+ else failwith "not a rational"
| _ -> failwith "not a rational")
| Cic.Const (u,boh) ->
- (match (UriManager.string_of_uri u) with
- "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
- |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
- | _ -> failwith "not a rational")
+ if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then r1
+ else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then r0
+ else failwith "not a rational"
| _ -> failwith "not a rational"
;;
;;
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
+ 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 t with
| Cic.Cast (t1,t2) -> (flin_of_term t1)
| Cic.Appl (t1::next) ->
- begin
- match t1 with
+ begin
+ match t1 with
Cic.Const (u,boh) ->
begin
- match (UriManager.string_of_uri u) with
- "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
+ if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then
flin_emult (rop r1) (flin_of_term (List.hd next))
- |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
+ else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then
fl_of_binop flin_plus next
- |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
+ else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then
fl_of_binop flin_minus next
- |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
- begin
- let arg1 = (List.hd next) and
- arg2 = (List.hd(List.tl next))
- in
- if fails rational_of_term arg1
- then
- if fails rational_of_term arg2
- then
- ( (* prodotto tra 2 incognite ????? impossibile*)
- failwith "Sistemi lineari!!!!\n"
- )
- else
- (
- match arg1 with
- Cic.Rel(n) -> (*trasformo al volo*)
- (flin_add (flin_zero()) arg1 (rational_of_term arg2))
- |_-> (* test this *)
- let tmp = flin_of_term arg1 in
- flin_emult (rational_of_term arg2) (tmp)
- )
- else
- if fails rational_of_term arg2
- then
- (
- match arg2 with
- Cic.Rel(n) -> (*trasformo al volo*)
- (flin_add (flin_zero()) arg2 (rational_of_term arg1))
- |_-> (* test this *)
- let tmp = flin_of_term arg2 in
- flin_emult (rational_of_term arg1) (tmp)
-
- )
- else
- ( (*prodotto tra razionali*)
- (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))
- )
- (*try
- begin
- (*let a = rational_of_term arg1 in
- debug("ho fatto rational of term di "^CicPp.ppterm arg1^
- " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
- let a = flin_of_term arg1
- try
- begin
- let b = (rational_of_term arg2) in
- debug("ho fatto rational of term di "^CicPp.ppterm arg2^
- " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
- (flin_add_cste (flin_zero()) (rmult a b))
- end
- with
- _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
- (flin_add (flin_zero()) arg2 a)
- end
- with
- _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
- (flin_add(flin_zero()) arg1 (rational_of_term arg2))
- *)
- end
- |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
- let a=(rational_of_term (List.hd next)) in
- flin_add_cste (flin_zero()) (rinv a)
- |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
- 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
+ else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then
+ begin
+ let arg1 = (List.hd next) and
+ arg2 = (List.hd(List.tl next))
+ in
+ if fails rational_of_term arg1
+ then
+ if fails rational_of_term arg2
+ then
+ ( (* prodotto tra 2 incognite ????? impossibile*)
+ failwith "Sistemi lineari!!!!\n"
+ )
+ else
+ (
+ match arg1 with
+ Cic.Rel(n) -> (*trasformo al volo*)
+ (flin_add (flin_zero()) arg1 (rational_of_term arg2))
+ |_-> (* test this *)
+ let tmp = flin_of_term arg1 in
+ flin_emult (rational_of_term arg2) (tmp)
+ )
+ else
+ if fails rational_of_term arg2
+ then
+ (
+ match arg2 with
+ Cic.Rel(n) -> (*trasformo al volo*)
+ (flin_add (flin_zero()) arg2 (rational_of_term arg1))
+ |_-> (* test this *)
+ let tmp = flin_of_term arg2 in
+ flin_emult (rational_of_term arg1) (tmp)
+
+ )
+ else
+ ( (*prodotto tra razionali*)
+ (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))
+ )
+ (*try
+ begin
+ (*let a = rational_of_term arg1 in
+ debug("ho fatto rational of term di "^CicPp.ppterm arg1^
+ " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
+ let a = flin_of_term arg1
+ try
+ begin
+ let b = (rational_of_term arg2) in
+ debug("ho fatto rational of term di "^CicPp.ppterm arg2^
+ " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
+ (flin_add_cste (flin_zero()) (rmult a b))
+ end
+ with
+ _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
+ (flin_add (flin_zero()) arg2 a)
+ end
+ with
+ _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
+ (flin_add(flin_zero()) arg1 (rational_of_term arg2))
+ *)
+ end
+ else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then
+ let a=(rational_of_term (List.hd next)) in
+ flin_add_cste (flin_zero()) (rinv a)
+ else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then
+ 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
+ else assert false
+ end
+ |_ -> assert false
+ end
| Cic.Const (u,boh) ->
begin
- match (UriManager.string_of_uri u) with
- "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
- |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
- |_-> assert false
- end
+ if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then flin_one ()
+ else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then flin_zero ()
+ else assert false
+ end
|_-> assert false)
with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1
;;
*)
(**
- Translates a flin to (c,x) list
- @param f a flin
- @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
+ Translates a flin to (c,x) list
+ @param f a flin
+ @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
*)
let flin_to_alist f =
let res=ref [] in
*)
(**
- The structure for ineq
+ The structure for ineq
*)
type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
let arg2= List.hd(List.tl next) in
(match t1 with (* match t1 *)
Cic.Const (u,boh) ->
- (match UriManager.string_of_uri u with (* match u *)
- "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
- [{hname=h;
+ if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then
+ [{hname=h;
htype="Rlt";
- hleft=arg1;
- hright=arg2;
- hflin= flin_minus (flin_of_term arg1)
+ hleft=arg1;
+ hright=arg2;
+ hflin= flin_minus (flin_of_term arg1)
(flin_of_term arg2);
- hstrict=true}]
- |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
- [{hname=h;
+ hstrict=true}]
+ else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then
+ [{hname=h;
htype="Rgt";
- hleft=arg2;
- hright=arg1;
- hflin= flin_minus (flin_of_term arg2)
+ hleft=arg2;
+ hright=arg1;
+ hflin= flin_minus (flin_of_term arg2)
(flin_of_term arg1);
- hstrict=true}]
- |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
+ hstrict=true}]
+ else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then
[{hname=h;
htype="Rle";
- hleft=arg1;
- hright=arg2;
- hflin= flin_minus (flin_of_term arg1)
+ hleft=arg1;
+ hright=arg2;
+ hflin= flin_minus (flin_of_term arg1)
(flin_of_term arg2);
- hstrict=false}]
- |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
+ hstrict=false}]
+ else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then
[{hname=h;
htype="Rge";
- hleft=arg2;
- hright=arg1;
- hflin= flin_minus (flin_of_term arg2)
+ hleft=arg2;
+ hright=arg1;
+ hflin= flin_minus (flin_of_term arg2)
(flin_of_term arg1);
- hstrict=false}]
- |_->assert false)(* match u *)
+ hstrict=false}]
+ else assert false
| Cic.MutInd (u,i,o) ->
- (match UriManager.string_of_uri u with
- "cic:/Coq/Init/Logic_Type/eqT.ind" ->
- let t0= arg1 in
+ if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then
+ let t0= arg1 in
let arg1= arg2 in
let arg2= List.hd(List.tl (List.tl next)) in
- (match t0 with
+ (match t0 with
Cic.Const (u,boh) ->
- (match UriManager.string_of_uri u with
- "cic:/Coq/Reals/Rdefinitions/R.con"->
+ if UriManager.eq u HelmLibraryObjects.Reals.r_URI then
[{hname=h;
htype="eqTLR";
- hleft=arg1;
- hright=arg2;
- hflin= flin_minus (flin_of_term arg1)
+ hleft=arg1;
+ hright=arg2;
+ hflin= flin_minus (flin_of_term arg1)
(flin_of_term arg2);
- hstrict=false};
+ hstrict=false};
{hname=h;
htype="eqTRL";
- hleft=arg2;
- hright=arg1;
- hflin= flin_minus (flin_of_term arg2)
+ hleft=arg2;
+ hright=arg1;
+ hflin= flin_minus (flin_of_term arg2)
(flin_of_term arg1);
- hstrict=false}]
- |_-> assert false)
- |_-> assert false)
- |_-> assert false)
+ hstrict=false}]
+ else assert false
+ |_-> assert false)
+ else assert false
|_-> assert false)(* match t1 *)
|_-> assert false (* match t *)
;;
match l with
[] -> ()
| (a,b)::next -> (print_rl a;
- print_string (if b=true then "strict\n"else"\n");
- print_sys next)
+ print_string (if b=true then "strict\n"else"\n");
+ print_sys next)
;;
(*let print_hash h =
- Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
+ Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
;;*)
let fourier_lineq lineq1 =
let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
List.iter (fun f ->
Hashtbl.iter (fun x c ->
- try (Hashtbl.find hvar x;())
- with _-> nvar:=(!nvar)+1;
- Hashtbl.add hvar x (!nvar);
- debug("aggiungo una var "^
- string_of_int !nvar^" per "^
- CicPp.ppterm x^"\n"))
+ try (Hashtbl.find hvar x;())
+ with _-> nvar:=(!nvar)+1;
+ Hashtbl.add hvar x (!nvar);
+ debug("aggiungo una var "^
+ string_of_int !nvar^" per "^
+ CicPp.ppterm x^"\n"))
f.hflin.fhom)
lineq1;
(*print_hash hvar;*)
*)
-let _eqT = Cic.MutInd((UriManager.uri_of_string
- "cic:/Coq/Init/Logic_Type/eqT.ind"), 0, []) ;;
-let _False = Cic.MutInd ((UriManager.uri_of_string
- "cic:/Coq/Init/Logic/False.ind"), 0, []) ;;
-let _not = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Init/Logic/not.con"), []);;
-let _R0 = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/R0.con"), []) ;;
-let _R1 = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/R1.con"), []) ;;
-let _R = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/R.con"), []) ;;
+let _eqT = Cic.MutInd(HelmLibraryObjects.Logic.eq_URI, 0, []) ;;
+let _False = Cic.MutInd (HelmLibraryObjects.Logic.false_URI, 0, []) ;;
+let _not = Cic.Const (HelmLibraryObjects.Logic.not_URI,[]);;
+let _R0 = Cic.Const (HelmLibraryObjects.Reals.r0_URI,[]);;
+let _R1 = Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]);;
+let _R = Cic.Const (HelmLibraryObjects.Reals.r_URI,[]);;
let _Rfourier_eqLR_to_le=Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"), []) ;;
let _Rfourier_eqRL_to_le=Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"), []) ;;
let _Rfourier_ge_to_le =Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con"), []) ;;
-let _Rfourier_gt_to_lt =Cic.Const ((UriManager.uri_of_string
+let _Rfourier_gt_to_lt =Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con"), []) ;;
let _Rfourier_le=Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rfourier_le.con"), []) ;;
"cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con"), []) ;;
let _Rfourier_not_lt_ge = Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con"), []) ;;
-let _Rinv = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rinv.con"), []) ;;
-let _Rinv_R1 = Cic.Const((UriManager.uri_of_string
- "cic:/Coq/Reals/Rbase/Rinv_R1.con" ), []) ;;
-let _Rle = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rle.con"), []) ;;
+let _Rinv = Cic.Const (HelmLibraryObjects.Reals.rinv_URI, []);;
+let _Rinv_R1 = Cic.Const(HelmLibraryObjects.Reals.rinv_r1_URI, []);;
+let _Rle = Cic.Const (HelmLibraryObjects.Reals.rle_URI, []);;
let _Rle_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con"), []) ;;
let _Rle_not_lt = Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"), []) ;;
let _Rle_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con"), []) ;;
-(*let _Rle_zero_zero = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con"), []) ;;*)
-let _Rlt = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rlt.con"), []) ;;
+let _Rlt = Cic.Const (HelmLibraryObjects.Reals.rlt_URI, []);;
let _Rlt_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con"), []) ;;
let _Rlt_not_le = Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"), []) ;;
let _Rlt_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con"), []) ;;
-let _Rminus = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rminus.con"), []) ;;
-let _Rmult = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rmult.con"), []) ;;
+let _Rminus = Cic.Const (HelmLibraryObjects.Reals.rminus_URI, []);;
+let _Rmult = Cic.Const (HelmLibraryObjects.Reals.rmult_URI, []);;
let _Rnot_le_le =Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rnot_le_le.con"), []) ;;
let _Rnot_lt0 = Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rnot_lt0.con"), []) ;;
let _Rnot_lt_lt =Cic.Const ((UriManager.uri_of_string
"cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con"), []) ;;
-let _Ropp = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Ropp.con"), []) ;;
-let _Rplus = Cic.Const ((UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rplus.con"), []) ;;
+let _Ropp = Cic.Const (HelmLibraryObjects.Reals.ropp_URI, []);;
+let _Rplus = Cic.Const (HelmLibraryObjects.Reals.rplus_URI, []);;
(******************************************************************************)
0 -> _R0 (* o forse R0 + R0 ????? *)
| 1 -> _R1
| _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
-;;
-
+;;
+
let int_to_real n =
let x = int_to_real_aux (abs n) in
if n < 0 then
- Cic.Appl [ _Ropp ; x ]
+ Cic.Appl [ _Ropp ; x ]
else
- x
+ x
;;
for i=1 to n-1 do
tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
~status _Rlt_zero_pos_plus1;
- PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
- ~continuation:!tacn);
+ PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
+ ~continuation:!tacn);
done;
for i=1 to d-1 do
tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
- ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
+ ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
done;
)
~continuation:
(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
- ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
+ ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
debug("end tac_zero_infeq_false\n");
r
(*PORTING
|"Rle" -> exact ~term:h.hname ~status
|"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
~term:_Rfourier_gt_to_lt)
- ~continuation:(exact ~term:h.hname)) ~status
+ ~continuation:(exact ~term:h.hname)) ~status
|"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
~term:_Rfourier_ge_to_le)
~continuation:(exact ~term:h.hname)) ~status
let is_ineq (h,t) =
match t with
Cic.Appl ( Cic.Const(u,boh)::next) ->
- (match (UriManager.string_of_uri u) with
- "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
- |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
- |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
- |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
- |"cic:/Coq/Init/Logic_Type/eqT.con" ->
+ (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI or
+ UriManager.eq u HelmLibraryObjects.Reals.rgt_URI or
+ UriManager.eq u HelmLibraryObjects.Reals.rle_URI or
+ UriManager.eq u HelmLibraryObjects.Reals.rge_URI then true
+ else if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then
(match (List.hd next) with
Cic.Const (uri,_) when
- UriManager.string_of_uri uri =
- "cic:/Coq/Reals/Rdefinitions/R.con" -> true
+ UriManager.eq uri HelmLibraryObjects.Reals.r_URI
+ -> true
| _ -> false)
- |_->false)
+ else false)
|_->false
;;
(*let find_in_context id context =
let rec find_in_context_aux c n =
- match c with
- [] -> failwith (id^" not found in context")
- | a::next -> (match a with
- Some (Cic.Name(name),_) when name = id -> n
- (*? magari al posto di _ qualcosaltro?*)
- | _ -> find_in_context_aux next (n+1))
+ match c with
+ [] -> failwith (id^" not found in context")
+ | a::next -> (match a with
+ Some (Cic.Name(name),_) when name = id -> n
+ (*? magari al posto di _ qualcosaltro?*)
+ | _ -> find_in_context_aux next (n+1))
in
find_in_context_aux context 1
;;
match context with
[] -> []
| 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)
+ 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 _ =
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)
- )
+ (
+ (*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 *)
+(* lifts everithing at the conclusion level *)
let rec superlift c n=
match c with
[] -> []
;;
let tcl_fail a ~status:(proof,goal) =
- match a with
- 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
- |_-> (proof,[goal])
+ match a with
+ 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
+ |_-> (proof,[goal])
;;
(* Galla: moved in variousTactics.ml
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let num = ref 0 in
let tac_list = List.map
- ( fun x -> num := !num + 1;
- match x with
- Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
- | _ -> ("fake",tcl_fail 1)
- )
- context
+ ( fun x -> num := !num + 1;
+ match x with
+ Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
+ | _ -> ("fake",tcl_fail 1)
+ )
+ context
in
Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
;;
(* Galla: moved in negationTactics.ml
(* !!!!! fix !!!!!!!!!! *)
let contradiction_tac ~status:(proof,goal)=
- Tacticals.then_
+ Tacticals.then_
(*inutile sia questo che quello prima della chiamata*)
- ~start:PrimitiveTactics.intros_tac
- ~continuation:(Tacticals.then_
- ~start:(VariousTactics.elim_type_tac ~term:_False)
- ~continuation:(assumption_tac))
- ~status:(proof,goal)
+ ~start:PrimitiveTactics.intros_tac
+ ~continuation:(Tacticals.then_
+ ~start:(VariousTactics.elim_type_tac ~term:_False)
+ ~continuation:(assumption_tac))
+ ~status:(proof,goal)
;;
*)
let th_to_appl = ref _Rfourier_not_le_gt in
(match s_ty with
Cic.Appl ( Cic.Const(u,boh)::args) ->
- (match UriManager.string_of_uri u with
- "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
- _Rfourier_not_ge_lt
- |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
+ th_to_appl :=
+ (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then
+ _Rfourier_not_ge_lt
+ else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then
_Rfourier_not_gt_le
- |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
+ else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then
_Rfourier_not_le_gt
- |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
+ else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then
_Rfourier_not_lt_ge
- |_-> failwith "fourier can't be applyed")
+ else failwith "fourier can't be applyed")
|_-> failwith "fourier can't be applyed");
(* fix maybe strip_outer_cast goes here?? *)
(* transform hyps into inequations *)
List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
- with _-> ())
+ with _-> ())
hyps;
-
+
debug ("applico fourier a "^ string_of_int (List.length !lineq)^
" disequazioni\n");
let res=fourier_lineq (!lineq) in
let tac=ref Tacticals.id_tac in
if res=[] then
- (print_string "Tactic Fourier fails.\n";flush stdout;
- failwith "fourier_tac fails")
+ (print_string "Tactic Fourier fails.\n";flush stdout;
+ failwith "fourier_tac fails")
else
(
match res with (*match res*)
let lutil=ref [] in
List.iter
(fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
- (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
- )
+ (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
+ )
(List.combine (!lineq) lc);
-
+
print_string (" quindi lutil e' lunga "^
- string_of_int (List.length (!lutil))^"\n");
+ string_of_int (List.length (!lutil))^"\n");
(* on construit la combinaison linéaire des inéquation *)
(match (!lutil) with (*match (!lutil) *)
(h1,c1)::lutil ->
debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
-
+
let s=ref (h1.hstrict) in
-
+
let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
List.iter (fun (h,c) ->
- s:=(!s)||(h.hstrict);
- t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
- [_Rmult;rational_to_real c;h.hleft ] ]);
- t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
- [_Rmult;rational_to_real c;h.hright] ]))
+ s:=(!s)||(h.hstrict);
+ t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
+ [_Rmult;rational_to_real c;h.hleft ] ]);
+ t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
+ [_Rmult;rational_to_real c;h.hright] ]))
lutil;
-
+
let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
let tc=rational_to_real cres in
debug "inizio a costruire tac1\n";
Fourier.print_rational(c1);
-
+
let tac1=ref ( fun ~status ->
- if h1.hstrict then
- (Tacticals.thens
- ~start:(
- fun ~status ->
- debug ("inizio t1 strict\n");
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
- debug ("ty = "^ CicPp.ppterm ty^"\n");
+ if h1.hstrict then
+ (Tacticals.thens
+ ~start:(
+ fun ~status ->
+ debug ("inizio t1 strict\n");
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
+ debug ("ty = "^ CicPp.ppterm ty^"\n");
PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
~continuations:[tac_use h1;tac_zero_inf_pos
(rational_to_fraction c1)]
- ~status
- )
+ ~status
+ )
else
- (Tacticals.thens
- ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
+ (Tacticals.thens
+ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
~continuations:[tac_use h1;tac_zero_inf_pos
- (rational_to_fraction c1)] ~status
- )
- )
-
+ (rational_to_fraction c1)] ~status
+ )
+ )
+
in
s:=h1.hstrict;
List.iter (fun (h,c) ->
(if (!s) then
- (if h.hstrict then
- (debug("tac1 1\n");
- tac1:=(Tacticals.thens
- ~start:(PrimitiveTactics.apply_tac
- ~term:_Rfourier_lt_lt)
- ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
- (rational_to_fraction c)])
- )
- else
- (debug("tac1 2\n");
- Fourier.print_rational(c1);
- tac1:=(Tacticals.thens
- ~start:(
- fun ~status ->
- debug("INIZIO TAC 1 2\n");
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
- debug ("ty = "^ CicPp.ppterm ty^"\n");
+ (if h.hstrict then
+ (debug("tac1 1\n");
+ tac1:=(Tacticals.thens
+ ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rfourier_lt_lt)
+ ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
+ (rational_to_fraction c)])
+ )
+ else
+ (debug("tac1 2\n");
+ Fourier.print_rational(c1);
+ tac1:=(Tacticals.thens
+ ~start:(
+ fun ~status ->
+ debug("INIZIO TAC 1 2\n");
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
+ debug ("ty = "^ CicPp.ppterm ty^"\n");
PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
- ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
- (rational_to_fraction c)])
+ ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
+ (rational_to_fraction c)])
)
)
- else
+ else
(if h.hstrict then
- (debug("tac1 3\n");
- tac1:=(Tacticals.thens
- ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
- ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
+ (debug("tac1 3\n");
+ tac1:=(Tacticals.thens
+ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
+ ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
(rational_to_fraction c)])
- )
- else
- (debug("tac1 4\n");
- tac1:=(Tacticals.thens
- ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
- ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
+ )
+ else
+ (debug("tac1 4\n");
+ tac1:=(Tacticals.thens
+ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
+ ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
(rational_to_fraction c)])
- )
+ )
)
- );
- s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
-
+ );
+ s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
+
let tac2 =
if sres then
- tac_zero_inf_false goal (rational_to_fraction cres)
+ tac_zero_inf_false goal (rational_to_fraction cres)
else
- tac_zero_infeq_false goal (rational_to_fraction cres)
+ tac_zero_infeq_false goal (rational_to_fraction cres)
in
tac:=(Tacticals.thens
~start:(my_cut ~term:ineq)
~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
- ~start:(fun ~status:(proof,goal as status) ->
+ ~start:(fun ~status:(proof,goal as status) ->
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
PrimitiveTactics.change_tac ~what:ty
- ~with_what:(Cic.Appl [ _not; ineq]) ~status)
- ~continuation:(Tacticals.then_
+ ~with_what:(Cic.Appl [ _not; ineq]) ~status)
+ ~continuation:(Tacticals.then_
~start:(PrimitiveTactics.apply_tac ~term:
- (if sres then _Rnot_lt_lt else _Rnot_le_le))
- ~continuation:(Tacticals.thens
- ~start:(
- fun ~status ->
- debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
- let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
- ~status
- in
- (match r with (p,gl) ->
- debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
+ (if sres then _Rnot_lt_lt else _Rnot_le_le))
+ ~continuation:(Tacticals.thens
+ ~start:(
+ fun ~status ->
+ debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
+ let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
+ ~status
+ in
+ (match r with (p,gl) ->
+ debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
r)
- ~continuations:[(Tacticals.thens
- ~start:(
- fun ~status ->
- let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
- (match r with (p,gl) ->
- debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
- r)
- ~continuations:
+ ~continuations:[(Tacticals.thens
+ ~start:(
+ fun ~status ->
+ let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
+ (match r with (p,gl) ->
+ debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
+ r)
+ ~continuations:
[PrimitiveTactics.apply_tac ~term:_Rinv_R1
- ;Tacticals.try_tactics
- ~tactics:[ "ring", (fun ~status ->
- debug("begin RING\n");
- let r = Ring.ring_tac ~status in
- debug ("end RING\n");
- r)
- ; "id", Tacticals.id_tac]
- ])
- ;(*Tacticals.id_tac*)
- Tacticals.then_
- ~start:
- (
- fun ~status:(proof,goal as status) ->
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- (* check if ty is of type *)
- let w1 =
- debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
- (match ty with
- Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
- |_ -> assert false)
- in
- let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
- debug("fine MY_CHNGE\n");
- r
-
- )
- ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
- ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
+ ;Tacticals.try_tactics
+ ~tactics:[ "ring", (fun ~status ->
+ debug("begin RING\n");
+ let r = Ring.ring_tac ~status in
+ debug ("end RING\n");
+ r)
+ ; "id", Tacticals.id_tac]
+ ])
+ ;(*Tacticals.id_tac*)
+ Tacticals.then_
+ ~start:
+ (
+ fun ~status:(proof,goal as status) ->
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ (* check if ty is of type *)
+ let w1 =
+ debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
+ (match ty with
+ Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
+ |_ -> assert false)
+ in
+ let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
+ debug("fine MY_CHNGE\n");
+ r
+
+ )
+ ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
+ ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
|_-> assert false)(*match (!lutil) *)
|_-> assert false); (*match res*)
projects / helm.git / commitdiff