From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 10 Dec 2009 11:51:22 +0000 (+0000)
Subject: A compiling version?
X-Git-Tag: make_still_working~3167
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e5771907d96b66df32beb557bf775add3fb8dd7;hp=0431f79f14bbf2cdc38c099cacba3a2f71363d7b;p=helm.git

A compiling version?
---

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index b58eb5558..6d5df3196 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -31,13 +31,21 @@ let wrap fname f x =
   | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname)
 ;;
 
+class type g_pstatus =
+ object
+  inherit NEstatus.g_status
+  method obj: NCic.obj
+ end
+
 class pstatus =
  fun (o: NCic.obj) ->
-  object
+ object (self)
    inherit NEstatus.status
    val obj = o
    method obj = obj
    method set_obj o = {< obj = o >}
+   method set_pstatus : 'status. #g_pstatus as 'status -> 'self
+   = fun o -> (self#set_estatus o)#set_obj o#obj
   end
 
 type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
@@ -422,13 +430,21 @@ let metas_of_term status (context,t) =
 
 (* ============= move this elsewhere ====================*)
 
+class type ['stack] g_status =
+ object
+  inherit g_pstatus
+  method stack: 'stack
+ end
+
 class ['stack] status =
  fun (o: NCic.obj) (s: 'stack) ->
-  object
+ object (self)
    inherit (pstatus o)
    val stack = s
    method stack = stack
    method set_stack s = {< stack = s >}
+   method set_status : 'status. 'stack #g_status as 'status -> 'self
+   = fun o -> (self#set_pstatus o)#set_stack o#stack
   end
 
 class type lowtac_status = [unit] status
diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index bf2370ec9..6e4cc79dd 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -14,12 +14,19 @@
 exception Error of string lazy_t * exn option
 val fail: ?exn:exn -> string lazy_t -> 'a
 
+class type g_pstatus =
+ object
+  inherit NEstatus.g_status
+  method obj: NCic.obj
+ end
+
 class pstatus :
  NCic.obj ->
   object ('self)
    inherit NEstatus.status
    method obj: NCic.obj
    method set_obj: NCic.obj -> 'self
+   method set_pstatus: #g_pstatus -> 'self
   end
 
 type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
@@ -83,12 +90,19 @@ val mk_out_scope:
 
 val pp_status: #pstatus -> unit
 
+class type ['stack] g_status =
+ object
+  inherit g_pstatus
+  method stack: 'stack
+ end
+
 class ['stack] status :
  NCic.obj -> 'stack ->
   object ('self)
    inherit pstatus
    method stack: 'stack
    method set_stack: 'stack -> 'self
+   method set_status: 'stack #g_status -> 'self
   end
 
 class type lowtac_status = [unit] status
diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 0251a84c9..515622d4e 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -1297,7 +1297,7 @@ type candidate = int * Ast.term (* unique candidate number, candidate *)
 
 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
                                 atoms of the input goals *)
-exception Proved of #NTacStatus.tac_status
+exception Proved of NTacStatus.tac_status
 
 (* let close_failures _ c = c;; *)
 (* let prunable _ _ _ = false;; *)
@@ -1419,7 +1419,7 @@ let is_subsumed depth status gty cache =
 (* warning: ctx is supposed to be already instantiated w.r.t subst *)
 let index_local_equations eq_cache status =
   let open_goals = head_goals status#stack in
-  assert (List.length open_goals  = 1);
+(*  assert (List.length open_goals  = 1); *)
   let open_goal = List.hd open_goals in
   let ngty = get_goalty status open_goal in
   let ctx = ctx_of ngty in
@@ -1509,14 +1509,16 @@ let do_something signature flags status g depth gty cache =
   (* backward aplications *)
   let l1 = applicative_case depth signature status flags gty cache in
   (* fast paramodulation *) 
-  let l2 = 
+  let l2 = [] in
+(*
     List.map 
       (fun s ->
 	 incr candidate_no;
 	 ((!candidate_no,Ast.Ident("__paramod",None)),s))
       (auto_eq_check cache.unit_eq status)
-  (* states in l2 have have an set of subgoals: no point to sort them *)
   in
+*)
+  (* states in l2 have have an set of subgoals: no point to sort them *)
     l2 @ (sort_new_elems (l@l1)), cache
 ;;
 
@@ -1714,6 +1716,8 @@ let int name l def =
 ;;
 
 let auto_tac ~params:(_univ,flags) status =
+  let oldstatus = status in
+  let status = (status:> NTacStatus.tac_status) in
   let goals = head_goals status#stack in
   let status, facts = mk_th_cache status goals in
   let unit_eq = index_local_equations status#eq_cache status in 
@@ -1764,7 +1768,8 @@ let auto_tac ~params:(_univ,flags) status =
 		  | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
 		  | _ -> assert false
               in
-		s#set_stack stack
+	      let s = s#set_stack stack in
+		oldstatus#set_status s 
   in
   let s = up_to depth depth in
     print(lazy