]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/fourierR.ml
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
- new CicTextualParser
[helm.git] / helm / gTopLevel / fourierR.ml
diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 0dd76f89a5a806ade2c9556b3226639014b053f5..247a47248600e87d270f561bb3398d5480c4e20b 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -33,18 +33,18 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
   let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
    let eq_ind_r,ty,t1,t2 = 
     match CicTypeChecker.type_of_aux' metasenv context equality with
-       C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
-        when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") ->
+       C.Appl [C.MutInd (uri,0,_) ; ty ; t1 ; t2]
+        when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
          let eq_ind_r =
           C.Const
-           (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0)
+           (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
          in
           eq_ind_r,ty,t1,t2
-     | C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
+     | C.Appl [C.MutInd (uri,0,_) ; ty ; t1 ; t2]
         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
          let eqT_ind_r =
           C.Const
-           (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",0)
+           (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[])
          in
           eqT_ind_r,ty,t1,t2
      | _ ->
@@ -57,8 +57,7 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
      let t1' = CicSubstitution.lift 1 t1 in
      let gty'' =
       ProofEngineReduction.replace_lifting
-       ~equality:
-        (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true)
+       ~equality:ProofEngineReduction.alpha_equivalence
        ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
      in
       C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
@@ -79,33 +78,9 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
       (proof',[fresh_meta])
 ;;
 
-
-
-let simpl_tac ~status:(proof,goal) =
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-
-prerr_endline("simpl_tac su "^CicPp.ppterm ty);
- 
- let new_ty = ProofEngineReduction.simpl context ty in
-
-prerr_endline("ritorna "^CicPp.ppterm new_ty);
-
- let new_metasenv = 
-   List.map
-   (function
-     (n,_,_) when n = metano -> (metano,context,new_ty)
-     | _ as t -> t
-   ) metasenv
- in
- (curi,new_metasenv,pbo,pty), [metano]
-
-;;
-
-let rewrite_simpl_tac ~term ~status =
-
- Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status
-
+let rewrite_simpl_tac ~term =
+ Tacticals.then_ ~start:(rewrite_tac ~term)
+  ~continuation:ReductionTactics.simpl_tac
 ;;
 
 (******************** THE FOURIER TACTIC ***********************)
@@ -229,9 +204,9 @@ let flin_emult a f =
 *)
 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
+   Cic.Cast  (t,_) -> string_of_term t
+  |Cic.Const (u,_) -> UriManager.string_of_uri u
+  |Cic.Var   (u,_) -> UriManager.string_of_uri u
   | _ -> "not_of_constant"
 ;;
 
@@ -516,88 +491,143 @@ i.e. on obtient une contradiction.
 *)
 
 
-let _eqT = Cic.MutInd(UriManager.uri_of_string 
- "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;;
-let _False = Cic.MutInd (UriManager.uri_of_string 
- "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
-let _not = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Init/Logic/not.con") 0;;
-let _R0 = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
-let _R1 = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
-let _R = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;;
-let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
-let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
-let _Rfourier_ge_to_le  =Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
-let _Rfourier_gt_to_lt         =Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
-let _Rfourier_le=Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
-let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;;
-let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
-let _Rfourier_lt=Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
-let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;;
-let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
-let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
-let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
-let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
-let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
-let _Rinv  = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
-let _Rinv_R1 = Cic.Const(UriManager.uri_of_string 
- "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
-let _Rle = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
-let _Rle_mult_inv_pos =  Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
-let _Rle_not_lt = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
-let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
-let _Rle_zero_pos_plus1 =  Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
-let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
-let _Rlt = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
-let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
-let _Rlt_not_le =  Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
-let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
-let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
-let _Rminus = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
-let _Rmult = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
-let _Rnot_le_le =Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
-let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
-let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
-let _Ropp = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
-let _Rplus = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
-let _sym_eqT = Cic.Const(UriManager.uri_of_string 
- "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
+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 _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
+    "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")[];;
+let _Rfourier_le_le =
+ Cic.Const
+  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con")
+  [];;
+let _Rfourier_le_lt =
+ Cic.Const
+  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con")
+  [] ;;
+let _Rfourier_lt =
+ Cic.Const
+  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") []
+;;
+let _Rfourier_lt_le =
+ Cic.Const
+  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con")
+  []
+;;
+let _Rfourier_lt_lt =
+ Cic.Const
+  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con")
+  []
+;;
+let _Rfourier_not_ge_lt =
+ Cic.Const
+  (UriManager.uri_of_string
+    "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [];;
+let _Rfourier_not_gt_le =
+ Cic.Const
+  (UriManager.uri_of_string
+    "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [];;
+let _Rfourier_not_le_gt =
+ Cic.Const
+  (UriManager.uri_of_string
+    "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 _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_not_lt.con") [];;
+let _Rle_zero_1 =
+ 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_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_not_le.con") [];;
+let _Rlt_zero_1 =
+ 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 _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 _sym_eqT =
+ Cic.Const
+  (UriManager.uri_of_string
+    "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") [];;
 
 (******************************************************************************)
 
@@ -1018,7 +1048,7 @@ theoreme,so let's parse our thesis *)
          " disequazioni\n");
 
   let res=fourier_lineq (!lineq) in
-  let tac=ref Ring.id_tac in
+  let tac=ref Tacticals.id_tac in
   if res=[] then 
        (print_string "Tactic Fourier fails.\n";flush stdout;
         failwith "fourier_tac fails")
@@ -1204,7 +1234,7 @@ theoreme,so let's parse our thesis *)
                                        let r = Ring.ring_tac  ~status in
                                        debug ("end RING\n");
                                        r)
-                       ; "id", Ring.id_tac] 
+                       ; "id", Tacticals.id_tac] 
                 ])
 (* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *)
               ;tac2]))
Unnamed repository; edit this file 'description' to name the repository.