From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 19 Sep 2002 14:57:41 +0000 (+0000)
Subject: Tactic update
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~69
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9519a138c26383f30f018376bc6cf875f8b0c82e;p=helm.git

Tactic update
---

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 5c42e9ecc..7e66efa49 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -31,6 +31,9 @@ des in
 
 open Fourier
 
+
+let debug x = print_string x ; flush stdout;;
+
 (******************************************************************************
 Operations on linear combinations.
 
@@ -385,6 +388,7 @@ let fourier_lineq lineq1 =
                   h.hflin.fhom;
                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
              lineq1 in
+   debug ("chiamo unsolvable sul sistema di "^ string_of_int (List.length sys) ^"\n");
    unsolvable sys
 ;;
 
@@ -576,15 +580,44 @@ let mkAppL a =
 let rec strip_outer_cast c = match c with
   | Cic.Cast (c,_) -> strip_outer_cast c
   | _ -> c
+;;
+
+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),Cic.Decl(t)) when name = id -> n 
+			| _ -> find_in_context_aux next (n+1))
+  in find_in_context_aux context 1 (*?? bisogna invertire il contesto? ??*)
+;;
+
+(* mi sembra quadratico *)
+let rec filter_real_hyp context =
+  match context with
+  [] -> []
+  | Some(Cic.Name(h),Cic.Def(t))::next -> [(Cic.Rel(find_in_context h next),t)] @
+  						filter_real_hyp next
+  | a::next -> filter_real_hyp next
+;;
+
+	
 
 (* se pf_concl estrae la concl*)
-(*let rec fourier ~status:(((p_uri,p_meta,p_incom,p_tes) as proof,goal) as status)=
-    let goal = strip_outer_cast p_tes in
-    let fhyp = String.copy "new_hyp_for_fourier" in *)
+let rec fourier ~status:(proof,goal)=
+	debug ("invoco fourier_tac sul goal"^string_of_int(goal)^"\n");
+	let curi,metasenv,pbo,pty = proof in
+	let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+	
+	(* il goal di prima dovrebbe essere ty
+	let goal = strip_outer_cast (pf_concl gl) in*)
+	
+    	let fhyp = String.copy "new_hyp_for_fourier" in 
     (* si le but est une inéquation, on introduit son contraire,
        et le but à prouver devient False *)
-(*    try (let tac =
-     match goal with
+
+    try (let tac =
+     match ty with
       Cic.Appl ( Cic.Const(u,boh)::args) ->
       (match UriManager.string_of_uri u with
 	     "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> 
@@ -609,31 +642,34 @@ let rec strip_outer_cast c = match c with
 	      		~continuation:fourier)
 	    |_->assert false)
         |_->assert false
-      in tac status)
-     with _ -> *)
+      in tac (proof,goal) )
+     with _ -> 
 
     (* les hypothèses *)
 
-    (***** Come estraggo pf_hyps?????????????? *******)
-(*    let hyps = List.map (fun (h,t) -> (Cic.Var(h),t))
-                        (list_of_sign (pf_hyps gl)) in
+    
+    (* ? fix if None  ?????*)
+    debug ("estraggo hp da context "^ string_of_int(List.length context)^"\n");
+    let hyps = filter_real_hyp context in
+    debug ("trasformo in eq "^ string_of_int (List.length hyps)^"\n");
     let lineq =ref [] in
-    List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
+    List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
 		        with _-> ())
               hyps;
 
-	   *) 
+	    
     (* lineq = les inéquations découlant des hypothèses *)
 
+    debug ("applico fourier a "^ string_of_int (List.length !lineq)^"\n");
 
-(*
     let res=fourier_lineq (!lineq) in
-    let tac=ref tclIDTAC in
+    (*let tac=ref tclIDTAC in*)
     if res=[]
     then (print_string "Tactic Fourier fails.\n";
 		       flush stdout)
-
-*)
+;debug "fine\n";
+;(proof,[goal])	
+;;
     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
 
 (*
@@ -769,5 +805,5 @@ let v_fourier = add_tactic "Fourier" fourier_tac
 (*open CicReduction*)
 (*open PrimitiveTactics*)
 (*open ProofEngineTypes*)
-let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;
+let fourier_tac ~status:(proof,goal) = ignore(fourier (proof,goal)) ; (proof,[goal]) ;;
 
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 2b476a674..ab4474dea 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -47,9 +47,9 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/public/sacerdot/currentproof";;
+let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
 (*CSC: the getter should handle the innertypes, not the FS *)
-let innertypesfile = "/public/sacerdot/innertypes";;
+let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
 
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)