- rewrite extended to handle rewritings with eqT

- equality_replace implemented (based on the new rewriting tactic)

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index f0ec4bfceb7b93580dffbc9744ffe381785c1487..403b8b180953895f8505ae6168c054418ce2f6d5 100644 (file)
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -2,7 +2,7 @@ BIN_DIR = /usr/local/bin
 REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \
            helm-xml gdome2-xslt helm-cic_unification helm-mathql \
            helm-mathql_interpreter
-PREDICATES =
+PREDICATES = "gnome,init"
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
 OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
 OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index b9e78233033806975a816af1b2b7a792960f3fe5..d2725ff158fb49ee3445e1a615d7d4e0d0aa27d4 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -31,11 +31,22 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
  let module U = UriManager in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
-   let ty,t1,t2 = 
+   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") ->
-         ty,t1,t2
+         let eq_ind_r =
+          C.Const
+           (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0)
+         in
+          eq_ind_r,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)
+         in
+          eqT_ind_r,ty,t1,t2
      | _ ->
        raise
         (ProofEngineTypes.Fail
@@ -51,16 +62,7 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
      in
       C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
     in
-prerr_endline ("##### Atteso: " ^ CicPp.ppterm
-     (C.Lambda (C.Name "x", ty,
-      C.Appl
-       [C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind",0,0) ;
-        ty ; C.Rel 3 ; C.Rel 1]))
-) ;
 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
-    let eq_ind_r =
-     C.Const
-      (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0) in
     let fresh_meta = ProofEngineHelpers.new_meta proof in
     let irl =
      ProofEngineHelpers.identity_relocation_list_for_metavariable context in
@@ -477,6 +479,7 @@ 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 ;;
@@ -770,23 +773,21 @@ let rec superlift c n=
  
 ;;
 
-(* fix !!!!!!!!!!  this may not work *)
 let equality_replace a b ~status =
+ let module C = Cic in
   let proof,goal = status in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-prerr_endline ("<MY_CUT: " ^ CicPp.ppterm a ^ " <=> " ^ CicPp.ppterm b) ;
-prerr_endline ("### IN MY_CUT: ") ;
-prerr_endline ("@ " ^ CicPp.ppterm ty) ;
-List.iter (function Some (n,Cic.Decl t) -> prerr_endline ("# " ^ CicPp.ppterm t)) context ;
-prerr_endline ("##- IN MY_CUT ") ;
-let res =
-       let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in
-(*CSC: codice ad-hoc per questo caso!!! Non funge in generale *)
-       PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;_R;b;Cic.Lambda(Cic.Name "pippo",_R,Cic.Appl [_not; Cic.Appl [_Rlt;_R0;Cic.Rel 1]])]) ~status
-in
-prerr_endline "EUREKA" ;
-res
+   let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
+   let fresh_meta = ProofEngineHelpers.new_meta proof in
+   let irl =
+    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+   let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
+   let (proof,goals) =
+    rewrite_tac ~term:(C.Meta (fresh_meta,irl))
+     ~status:((curi,metasenv',pbo,pty),goal)
+   in
+    (proof,fresh_meta::goals)
 ;;
 
 let tcl_fail a ~status:(proof,goal) =
@@ -1032,8 +1033,6 @@ let rec fourier ~status:(s_proof,s_goal)=
                        ~continuation:(Tacticals.then_ 
                                ~start:(PrimitiveTactics.apply_tac 
                                                ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
-                                ~continuation:Ring.id_tac
-(*CSC
                                ~continuation:(Tacticals.thens 
                                                ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
                                                ~continuations:[tac2;(Tacticals.thens 
@@ -1051,7 +1050,7 @@ let rec fourier ~status:(s_proof,s_goal)=
                                
                                         )
                                                ] (* end continuations before comment *)
-                                       ) *)
+                                       )
                                );
                        !tac1]
                );(*end tac:=*)