Some stylesheets are now generated with Di Lena's meta_style.

[helm.git] / helm / gTopLevel / fourierR.ml

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index bdba623190cc8ab47fa6b533f232ff5a26aec7a7..17ff3f8fe732a37a923a6a3b2a91346ba7f98ccc 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -80,7 +80,10 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
 
 
 let rewrite_simpl_tac ~term ~status =
- Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:ReductionTactics.simpl_tac ~status
+ Tacticals.then_ ~start:(rewrite_tac ~term)
+  ~continuation:
+   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
+  ~status
 ;;
 
 (******************** THE FOURIER TACTIC ***********************)
@@ -391,7 +394,7 @@ let ineq1_of_term (h,t) =
                 |_->assert false)(* match u *)
           | Cic.MutInd (u,i,o) ->
               (match UriManager.string_of_uri u with 
-                "cic:/Coq/Init/Logic_Type/eqT.con" ->  
+                "cic:/Coq/Init/Logic_Type/eqT.ind" ->  
                           let t0= arg1 in
                            let arg1= arg2 in
                            let arg2= List.hd(List.tl (List.tl next)) in
@@ -528,8 +531,8 @@ 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 _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 
@@ -644,11 +647,11 @@ let tac_zero_infeq_pos gl (n,d) ~status =
  (*let cste = pf_parse_constr gl in*)
  debug("inizio tac_zero_infeq_pos\n");
  let tacn = ref 
-  (if n=0 then
+  (*(if n=0 then
     (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) 
-   else
+   else*)
     (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
-  )
+ (* ) *)
   in
   let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
   for i=1 to n-1 do 
@@ -714,7 +717,7 @@ let r =
      (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
      Tacticals.then_
       ~start:
-        (ReductionTactics.fold_tac
+        (ReductionTactics.fold_tac ~also_in_hypotheses:false
           ~term:
             (Cic.Appl
               [_Rle ; _R0 ;
@@ -745,8 +748,10 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
   let metasenv' = (fresh_meta,context,t)::metasenv in
    let proof' = curi,metasenv',pbo,pty in
     let proof'',goals =
-     PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta 
-      (fresh_meta,irl),t))::al)) ~status:(proof',goal)
+     PrimitiveTactics.apply_tac 
+      (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
+      ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
+       ~status:(proof',goal)
     in
      proof'',fresh_meta::goals
 ;;
@@ -759,6 +764,9 @@ let my_cut ~term:c ~status:(proof,goal)=
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 
+debug("my_cut di "^CicPp.ppterm c^"\n");
+
+
   let fresh_meta = ProofEngineHelpers.new_meta proof in
   let irl =
    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
@@ -920,7 +928,7 @@ let assumption_tac ~status:(proof,goal)=
 (* !!!!! fix !!!!!!!!!! *)
 let contradiction_tac ~status:(proof,goal)=
        Tacticals.then_ 
-               ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
+               ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
                ~continuation:(Tacticals.then_ 
                        ~start:(Ring.elim_type_tac ~term:_False) 
                        ~continuation:(assumption_tac))
@@ -1135,7 +1143,7 @@ theoreme,so let's parse our thesis *)
        in
        tac:=(Tacticals.thens 
          ~start:(my_cut ~term:ineq) 
-         ~continuations:[Tacticals.then_  
+         ~continuations:[(*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 = List.find (function (m,_,_) -> m=goal) 
@@ -1148,6 +1156,7 @@ theoreme,so let's parse our thesis *)
             ~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
@@ -1163,25 +1172,6 @@ theoreme,so let's parse our thesis *)
                   r)
                 ~continuations:
                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1
-(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
-   di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
-   parametri della equality_replace vengono passati al contrario? Oppure la
-   tattica usa i parametri al contrario?
-   CODICE NEL COMMENTO NON PORTATO. ORA ESISTE ANCHE LA TATTICA symmetry_tac
-                ~continuations:[Tacticals.then_ 
-                  ~start:(
-                    fun ~status:(proof,goal as status) ->
-                    debug("ECCOCI\n");
-                     let curi,metasenv,pbo,pty = proof in
-                    let metano,context,ty = List.find (function (m,_,_) -> m=
-                     goal) metasenv in
-                     debug("ty = "^CicPp.ppterm ty^"\n");
-                    let r = PrimitiveTactics.apply_tac ~term:_sym_eqT 
-                     ~status in
-                    debug("fine ECCOCI\n");
-                    r)
-                  ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
-*)
                 ;Tacticals.try_tactics 
                   ~tactics:[ "ring", (fun ~status -> 
                                        debug("begin RING\n");
@@ -1190,7 +1180,8 @@ theoreme,so let's parse our thesis *)
                                        r)
                        ; "id", Tacticals.id_tac] 
                 ])
-              ;Tacticals.then_ 
+              ;(*Tacticals.id_tac*)
+               Tacticals.then_ 
                 ~start:
                  (
                  fun ~status:(proof,goal as status) ->
@@ -1208,21 +1199,27 @@ theoreme,so let's parse our thesis *)
                   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:=*)
-       tac:=(Tacticals.thens 
+       (*tac:=(Tacticals.thens 
          ~start:(PrimitiveTactics.cut_tac ~term:_False)
         ~continuations:[Tacticals.then_ 
           ~start:(PrimitiveTactics.intros_tac ~name:"??")
           ~continuation:contradiction_tac
-        ;!tac])
+        ;!tac]) FIXED - this was useless*)
+       (* tac:=!tac*)
 
 
     |_-> assert false)(*match (!lutil) *)
   |_-> assert false); (*match res*)
   debug ("finalmente applico tac\n");
-  (!tac ~status:(proof,goal)) 
+  (
+  let r = !tac ~status:(proof,goal) in
+  debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
+  
+  ) 
 ;;
 
 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;