- further simplifications (??) of the status dependencies

[helm.git] / matita / components / ng_tactics / nTacStatus.ml

diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index 1aaeb50f6367ea58863034b8d12af18981203101..26e92add4fd5cb656c98dff5a5557b197a954c81 100644 (file)
--- a/matita/components/ng_tactics/nTacStatus.ml
+++ b/matita/components/ng_tactics/nTacStatus.ml
@@ -16,6 +16,9 @@ let pp x =
  if !debug then prerr_endline (Lazy.force x) else ()
 ;;
 
+type automation_cache = NDiscriminationTree.DiscriminationTree.t
+type unit_eq_cache = NCicParamod.state
+
 exception Error of string lazy_t * exn option
 let fail ?exn msg = raise (Error (msg,exn))
 
@@ -31,24 +34,59 @@ let wrap fname f x =
   | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname)
 ;;
 
+class type g_eq_status =
+ object
+   method eq_cache : unit_eq_cache 
+ end
+
+class eq_status =
+ object(self)
+  val eq_cache = NCicParamod.empty_state
+  method eq_cache = eq_cache
+  method set_eq_cache v = {< eq_cache = v >}
+  method set_eq_status
+   : 'status. #g_eq_status as 'status -> 'self
+   = fun o -> self#set_eq_cache o#eq_cache
+ end
+
+class type g_auto_status =
+ object
+   method auto_cache : automation_cache
+ end
+
+class auto_status =
+ object(self)
+  val auto_cache = NDiscriminationTree.DiscriminationTree.empty
+  method auto_cache = auto_cache
+  method set_auto_cache v = {< auto_cache = v >}
+  method set_auto_status
+   : 'status. #g_auto_status as 'status -> 'self
+   = fun o -> self#set_auto_cache o#auto_cache
+ end
+
 class type g_pstatus =
  object
-  inherit NEstatus.g_status
+  inherit GrafiteDisambiguate.g_status
+  inherit g_auto_status
+  inherit g_eq_status
   method obj: NCic.obj
  end
 
 class pstatus =
  fun (o: NCic.obj) ->
  object (self)
-   inherit NEstatus.status
+   inherit GrafiteDisambiguate.status
+   inherit auto_status
+   inherit eq_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
+   = fun o ->
+    (((self#set_disambiguate_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o
   end
 
-type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
+type tactic_term = NotationPt.term Disambiguate.disambiguator_input
 type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
 
 let pp_tac_status status = 
@@ -157,7 +195,7 @@ let disambiguate status context t ty =
  in
  let uri,height,metasenv,subst,obj = status#obj in
  let metasenv, subst, status, t = 
-   GrafiteDisambiguate.disambiguate_nterm expty status context metasenv subst t 
+   GrafiteDisambiguate.disambiguate_nterm status expty context metasenv subst t 
  in
  let new_pstatus = uri,height,metasenv,subst,obj in
   status#set_obj new_pstatus, (context, t)