From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 16 Oct 2009 12:40:16 +0000 (+0000)
Subject: some work for auto
X-Git-Tag: make_still_working~3288
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f00757144b2cd7e6457fed55dbc1309d11a542dc;p=helm.git

some work for auto
---

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 4193d41da..a80334d01 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -13,8 +13,8 @@
 
 open Printf
 
-let debug = true
-let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+let debug = ref false
+let debug_print s = if !debug then prerr_endline (Lazy.force s) else ()
 
 open Continuationals.Stack
 open NTacStatus
@@ -925,9 +925,19 @@ let mk_th_cache status gl =
          let status,_,idx = 
            List.fold_left (fun (status, i, idx) _ -> 
               let t = mk_cic_term ctx (NCic.Rel i) in
-              let status, ty = typeof status ctx t in
-              let _, ty, _ = saturate status ty in
+              let status, orig_ty = typeof status ctx t in
+              let _, ty, _ = saturate ~delta:max_int status orig_ty in
               let idx = InvRelDiscriminationTree.index idx ty t in
+              let idx = 
+                let _, ty = term_of_cic_term status ty (ctx_of ty) in
+                match ty with
+                | NCic.Const (NReference.Ref (_,NReference.Def h)) 
+                | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_) 
+                   when h > 0 ->
+                     let _,ty,_= saturate status ~delta:(h-1) orig_ty in
+                     InvRelDiscriminationTree.index idx ty t
+                | _ -> idx
+              in
               status, i+1, idx)
              (status, 1, idx) ctx
           in
@@ -1025,11 +1035,14 @@ let put_in_subst s _ _ _  = s;;
 let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; 
 let cache_add_underinspection c _ _ = c;;
 let equational_case _ _ _ _ _ _ = [];;
-let sort_new_elems l = l;;
 let only _ _ _ = true;;
 
 let candidate_no = ref 0;;
 
+let sort_new_elems l = 
+  List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2) l
+;;
+
 let try_candidate status t g =
  try
    debug_print (lazy (" try " ^ CicNotationPp.pp_term t));
diff --git a/helm/software/components/ng_tactics/nAuto.mli b/helm/software/components/ng_tactics/nAuto.mli
index 7121bb946..99d6aa7e8 100644
--- a/helm/software/components/ng_tactics/nAuto.mli
+++ b/helm/software/components/ng_tactics/nAuto.mli
@@ -15,3 +15,4 @@ val auto_tac:
   params:(NTacStatus.tactic_term list * (string * string) list) -> 
    's NTacStatus.tactic
 
+val debug : bool ref
diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 8d47439c0..f51f4d2d7 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -162,13 +162,13 @@ let typeof status ctx t =
 ;;
 let typeof a b c = wrap "typeof" (typeof a b) c;;
 
-let saturate status (ctx,t) =
+let saturate status ?delta (ctx,t) =
   let n,h,metasenv,subst,k = status#obj in
-  let t, metasenv, args = NCicMetaSubst.saturate metasenv subst ctx t 0 in
+  let t,metasenv,args = NCicMetaSubst.saturate ?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
 ;;
-let saturate a b = wrap "saturate" (saturate a) b;;
+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
diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 2c1ad3b1e..c7e3ea75e 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -57,7 +57,7 @@ val apply_subst:
  #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
 val fix_sorts: cic_term -> cic_term
 val saturate :
- #pstatus as 'status -> cic_term -> 'status * cic_term * cic_term list
+ #pstatus as 'status -> ?delta:int -> cic_term -> 'status * cic_term * cic_term list
 
 val get_goalty: #pstatus -> int -> cic_term
 val mk_meta: