X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=26e92add4fd5cb656c98dff5a5557b197a954c81;hb=f167565ea9faf28f4e3d76b8f160fd269cd1aa84;hp=1aaeb50f6367ea58863034b8d12af18981203101;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index 1aaeb50f6..26e92add4 100644 --- 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)