X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=118261af027c2efa101facb0d21a39d611b03a0e;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=9f653abd51e63f2eb9b545fbf70112f261bc6e37;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index 9f653abd5..118261af0 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))
 
@@ -26,59 +29,92 @@ let wrap fname f x =
   with 
   | MultiPassDisambiguator.DisambiguationError _ 
   | NCicRefiner.RefineFailure _ 
+  | NCicRefiner.Uncertain _ 
   | NCicUnification.UnificationFailure _ 
+  | NCicUnification.Uncertain _ 
   | NCicTypeChecker.TypeCheckerFailure _ 
-  | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname)
+  | NCicMetaSubst.MetaSubstFailure _
+  | NCicMetaSubst.Uncertain _ 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 =
+class virtual 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 = NotationPt.term Disambiguate.disambiguator_input
 type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
 
-let pp_tac_status status = 
-  prerr_endline (NCicPp.ppobj status#obj);
-  prerr_endline ("STACK:\n" ^ Continuationals.Stack.pp status#stack)
-;;
-
 type cic_term = NCic.context * NCic.term
 let ctx_of (c,_) = c ;;
 let mk_cic_term c t = c,t ;;
 
-let ppterm status t =
- let uri,height,metasenv,subst,obj = status#obj in
+let ppterm (status:#pstatus) t =
+ let _uri,_height,metasenv,subst,_obj = status#obj in
  let context,t = t in
-  NCicPp.ppterm ~metasenv ~subst ~context t
+  status#ppterm ~metasenv ~subst ~context t
 ;;
 
-let ppcontext status c =
- let uri,height,metasenv,subst,obj = status#obj in
-  NCicPp.ppcontext ~metasenv ~subst c
+let ppcontext (status: #pstatus) c =
+ let _uri,_height,metasenv,subst,_obj = status#obj in
+  status#ppcontext ~metasenv ~subst c
 ;;
 
-let ppterm_and_context status t =
- let uri,height,metasenv,subst,obj = status#obj in
+let ppterm_and_context (status: #pstatus) t =
+ let _uri,_height,metasenv,subst,_obj = status#obj in
  let context,t = t in
-  NCicPp.ppcontext ~metasenv ~subst context ^ "\n ⊢ "^ 
-  NCicPp.ppterm ~metasenv ~subst ~context t
+  status#ppcontext ~metasenv ~subst context ^ "\n ⊢ "^ 
+  status#ppterm ~metasenv ~subst ~context t
 ;;
 
-let relocate status destination (source,t as orig) =
+let relocate status destination (source,_t as orig) =
  pp(lazy("relocate:\n" ^ ppterm_and_context status orig));
  pp(lazy("relocate in:\n" ^ ppcontext status destination));
  let rc = 
@@ -87,24 +123,24 @@ let relocate status destination (source,t as orig) =
     let rec compute_ops ctx = function (* destination, source *)
       | (n1, NCic.Decl t1 as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
           if n1 = n2 && 
-             NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
+             NCicReduction.are_convertible status ctx ~subst ~metasenv t1 t2 then
             compute_ops (e::ctx) (cl1,cl2)
           else
             [ `Delift ctx; `Lift (List.rev ex) ]
       | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Def (b2,t2))::cl2 ->
           if n1 = n2 && 
-             NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 &&
-             NCicReduction.are_convertible ctx ~subst ~metasenv b1 b2 then
+             NCicReduction.are_convertible status ctx ~subst ~metasenv t1 t2 &&
+             NCicReduction.are_convertible status ctx ~subst ~metasenv b1 b2 then
             compute_ops (e::ctx) (cl1,cl2)
           else
             [ `Delift ctx; `Lift (List.rev ex) ]
-      | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
+      | (n1, NCic.Def (_b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
           if n1 = n2 && 
-             NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
+             NCicReduction.are_convertible status ctx ~subst ~metasenv t1 t2 then
             compute_ops (e::ctx) (cl1,cl2)
           else
             [ `Delift ctx; `Lift (List.rev ex) ]
-      | (n1, NCic.Decl _)::cl1 as ex, (n2, NCic.Def _)::cl2 -> 
+      | (_n1, NCic.Decl _)::_cl1 as ex, (_n2, NCic.Def _)::_cl2 -> 
             [ `Delift ctx; `Lift (List.rev ex) ]
       | _::_ as ex, [] -> [ `Lift (List.rev ex) ]
       | [], _::_ -> [ `Delift ctx ]
@@ -116,23 +152,23 @@ let relocate status destination (source,t as orig) =
      (fun (status, (source,t)) -> function 
       | `Lift extra_ctx -> 
            let len = List.length extra_ctx in
-           status, (extra_ctx@source, NCicSubstitution.lift len t)
+           status, (extra_ctx@source, NCicSubstitution.lift status len t)
       | `Delift ctx -> 
             let len_ctx = List.length ctx in
             let irl = mk_irl 1 (List.length ctx) in
             let lc = List.length source - len_ctx, NCic.Ctx irl in
             let u, d, metasenv, subst, o = status#obj in
             pp(lazy("delifting as " ^ 
-              NCicPp.ppterm ~metasenv ~subst ~context:source 
-               (NCic.Meta (0,lc))));
+              status#ppterm ~metasenv ~subst ~context:source 
+               (NCic.Meta (-1,lc))));
             let (metasenv, subst), t =
-              NCicMetaSubst.delift 
+              NCicMetaSubst.delift status
                  ~unify:(fun m s c t1 t2 -> 
                    try Some (NCicUnification.unify status m s c t1 t2)
                    with 
                     | NCicUnification.UnificationFailure _ 
                     | NCicUnification.Uncertain _ -> None) 
-               metasenv subst source 0 lc t
+               metasenv subst source (-1) lc t
             in
             let status = status#set_obj (u, d, metasenv, subst, o) in
             status, (ctx,t))
@@ -151,13 +187,15 @@ let term_of_cic_term s t c =
 let disambiguate status context t ty =
  let status, expty = 
    match ty with 
-   | None -> status, None 
-   | Some ty -> 
-       let status, (_,x) = relocate status context ty in status, Some x 
+   | `XTSome ty -> 
+       let status, (_,x) = relocate status context ty in status, `XTSome x 
+   | `XTNone -> status, `XTNone 
+   | `XTSort -> status, `XTSort
+   | `XTInd  -> status, `XTInd
  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) 
@@ -167,14 +205,14 @@ let disambiguate a b c d = wrap "disambiguate" (disambiguate a b c) d;;
 let typeof status ctx t =
   let status, (_,t) = relocate status ctx t in
   let _,_,metasenv,subst,_ = status#obj in
-  let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
+  let ty = NCicTypeChecker.typeof status ~subst ~metasenv ctx t in
   status, (ctx, ty)
 ;;
 let typeof a b c = wrap "typeof" (typeof a b) c;;
 
 let saturate status ?delta (ctx,t) =
   let n,h,metasenv,subst,k = status#obj in
-  let t,metasenv,args = NCicMetaSubst.saturate ?delta metasenv subst ctx t 0 in
+  let t,metasenv,args = NCicMetaSubst.saturate status ?delta metasenv subst ctx t 0 in
   let status = status#set_obj (n,h,metasenv,subst,k) in
   status, (ctx,t), List.map (fun x -> ctx,x) args
 ;;
@@ -183,17 +221,26 @@ let saturate a ?delta b = wrap "saturate" (saturate a ?delta) b;;
 let whd status ?delta ctx t =
   let status, (_,t) = relocate status ctx t in
   let _,_,_,subst,_ = status#obj in
-  let t = NCicReduction.whd ~subst ?delta ctx t in
+  let t = NCicReduction.whd status ~subst ?delta ctx t in
   status, (ctx, t)
 ;;
   
 let normalize status ?delta ctx t =
   let status, (_,t) = relocate status ctx t in
   let _,_,_,subst,_ = status#obj in
-  let t = NCicTacReduction.normalize ~subst ?delta ctx t in
+  let t = NCicTacReduction.normalize status ~subst ?delta ctx t in
   status, (ctx, t)
 ;;
   
+let are_convertible status ctx a b =
+  let status, (_,a) = relocate status ctx a in
+  let status, (_,b) = relocate status ctx b in
+  let _n,_h,metasenv,subst,_o = status#obj in
+  let res = NCicReduction.are_convertible status metasenv subst ctx a b in
+   status, res
+;;
+let are_convertible a b c d = wrap "are_convertible" (are_convertible a b c) d;;
+
 let unify status ctx a b =
   let status, (_,a) = relocate status ctx a in
   let status, (_,b) = relocate status ctx b in
@@ -207,7 +254,7 @@ let fix_sorts status (ctx,t) =
  let f () =
   let name,height,metasenv,subst,obj = status#obj in
   let metasenv, t = 
-    NCicUnification.fix_sorts metasenv subst t in
+    NCicUnification.fix_sorts status metasenv subst t in
   let status = status#set_obj (name,height,metasenv,subst,obj) in
    status, (ctx,t)
  in
@@ -218,9 +265,11 @@ let refine status ctx term expty =
   let status, (_,term) = relocate status ctx term in
   let status, expty = 
     match expty with
-      None -> status, None 
-    | Some e -> 
-        let status, (_, e) = relocate status ctx e in status, Some e
+    | `XTSome e -> 
+        let status, (_, e) = relocate status ctx e in status, `XTSome e
+    | `XTNone -> status, `XTNone 
+    | `XTSort -> status, `XTSort
+    | `XTInd  -> status, `XTInd
   in
   let name,height,metasenv,subst,obj = status#obj in
   let metasenv,subst,t,ty = 
@@ -249,18 +298,22 @@ let to_subst status i entry =
   status#set_obj (name,height,metasenv,subst,obj)
 ;;
 
-let instantiate status i t =
+let instantiate status ?refine:(dorefine=true) i t =
  let _,_,metasenv,_,_ = status#obj in
  let gname, context, gty = List.assoc i metasenv in
- let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in
-  to_subst status i (gname,context,t,ty)
+  if dorefine then
+   let status, (_,t), (_,ty) = refine status context t (`XTSome (context,gty)) in
+    to_subst status i (gname,context,t,ty)
+  else
+   let status,(_,ty) = typeof status context t in
+    to_subst status i (gname,context,snd t,ty)
 ;;
 
 let instantiate_with_ast status i t =
  let _,_,metasenv,_,_ = status#obj in
  let gname, context, gty = List.assoc i metasenv in
  let ggty = mk_cic_term context gty in
- let status, (_,t) = disambiguate status context t (Some ggty) in
+ let status, (_,t) = disambiguate status context t (`XTSome ggty) in
   to_subst status i (gname,context,t,gty)
 ;;
 
@@ -325,12 +378,12 @@ let select_term
       else
         let _,_,_,subst,_ = status#obj in
         match t with
-        | NCic.Meta (i,lc) when List.mem_assoc i subst ->
+        | NCic.Meta (i,_lc) when List.mem_assoc i subst ->
             let _,_,t,_ = NCicUtils.lookup_subst i subst in
             aux ctx (status,already_found) t
         | NCic.Meta _ -> (status,already_found),t
         | _ ->
-          NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux
+          NCicUntrusted.map_term_fold_a status (fun e c -> e::c) ctx aux
            (status,already_found) t
      in 
        aux ctx (status,false) t
@@ -341,7 +394,7 @@ let select_term
     | _, NCic.Meta (i,lc) when List.mem_assoc i subst ->
         let cic = 
           let _,_,t,_ = NCicUtils.lookup_subst i subst in
-          NCicSubstitution.subst_meta lc t
+          NCicSubstitution.subst_meta status lc t
         in
         select status ctx pat cic
     | NCic.LetIn (_,t1,s1,b1), NCic.LetIn (n,t2,s2,b2) ->
@@ -360,7 +413,7 @@ let select_term
         let ctx = (n, NCic.Decl s2) :: ctx in
         let status, t = select status ctx t1 t2 in
         status, NCic.Prod (n,s,t)
-    | NCic.Appl l1, NCic.Appl l2 ->
+    | NCic.Appl l1, NCic.Appl l2 when List.length l1 = List.length l2 ->
         let status, l = 
            List.fold_left2
              (fun (status,l) x y -> 
@@ -369,7 +422,8 @@ let select_term
              (status,[]) l1 l2
         in
         status, NCic.Appl (List.rev l)
-    | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2) ->
+    | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2)
+      when List.length pl1 = List.length pl2 ->
         let status, t = select status ctx t1 t2 in
         let status, ot = select status ctx ot1 ot2 in
         let status, pl = 
@@ -383,7 +437,7 @@ let select_term
     | NCic.Implicit `Hole, t -> 
         (match wanted with
         | Some wanted -> 
-             let status', wanted = disambiguate status ctx wanted None in
+             let status', wanted = disambiguate status ctx wanted `XTNone in
              pp(lazy("wanted: "^ppterm status' wanted));
              let (status',found), t' = match_term status' ctx wanted t in
               if found then status',t' else status,t
@@ -392,9 +446,9 @@ let select_term
             status,t)
     | NCic.Implicit _, t -> status, t
     | _,t -> 
-        fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[]
+        fail (lazy ("malformed pattern: " ^ status#ppterm ~metasenv:[]
           ~context:[] ~subst:[] pat ^ " against " ^ 
-          NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))
+          status#ppterm ~metasenv:[] ~subst:[] ~context:[] t))
   in
   pp(lazy ("select in: "^ppterm low_status (context,term)));
   let status, term = select low_status context path term in
@@ -411,27 +465,27 @@ let analyse_indty status ty =
    | _,NCic.Appl (NCic.Const (NRef.Ref (_,(NRef.Ind _)) as ref) :: args) -> 
          ref, args
    | _,_ -> fail (lazy ("not an inductive type: " ^ ppterm status ty)) in
- let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in
+ let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys status ref in
  let _,_,_,cl = List.nth tl i in
  let consno = List.length cl in
  let left, right = HExtlib.split_nth lno args in
- status, (ref, consno, left, right)
+ status, (ref, consno, left, right, cl)
 ;;
 
 let apply_subst status ctx t =
  let status, (_,t) = relocate status ctx t in
  let _,_,_,subst,_ = status#obj in
-  status, (ctx, NCicUntrusted.apply_subst subst ctx t)
+  status, (ctx, NCicUntrusted.apply_subst status subst ctx t)
 ;;
 
 let apply_subst_context status ~fix_projections ctx =
  let _,_,_,subst,_ = status#obj in
-  NCicUntrusted.apply_subst_context ~fix_projections subst ctx
+  NCicUntrusted.apply_subst_context status ~fix_projections subst ctx
 ;;
 
 let metas_of_term status (context,t) =
  let _,_,_,subst,_ = status#obj in
- NCicUntrusted.metas_of_term subst context t
+ NCicUntrusted.metas_of_term status subst context t
 ;;
 
 (* ============= move this elsewhere ====================*)
@@ -442,7 +496,7 @@ class type ['stack] g_status =
   method stack: 'stack
  end
 
-class ['stack] status =
+class virtual ['stack] status =
  fun (o: NCic.obj) (s: 'stack) ->
  object (self)
    inherit (pstatus o)
@@ -453,14 +507,19 @@ class ['stack] status =
    = fun o -> (self#set_pstatus o)#set_stack o#stack
   end
 
-class type lowtac_status = [unit] status
+class type virtual lowtac_status = [unit] status
 
 type 'status lowtactic = #lowtac_status as 'status -> int -> 'status
 
-class type tac_status = [Continuationals.Stack.t] status
+class type virtual tac_status = [Continuationals.Stack.t] status
 
 type 'status tactic = #tac_status as 'status -> 'status
 
+let pp_tac_status (status: #tac_status) = 
+  prerr_endline (status#ppobj status#obj);
+  prerr_endline ("STACK:\n" ^ Continuationals.Stack.pp status#stack)
+;;
+
 module NCicInverseRelIndexable : Discrimination_tree.Indexable
 with type input = cic_term and type constant_name = NUri.uri = struct