X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=4193d41da75b58035ca3c5c0565a645f8e9eae51;hb=d40ad33ad3d075c5dd74b6a67131683b0ebe32d6;hp=d8e92cbad4172b6b3064d3ac4f9867851a1283c0;hpb=dfee894b6cc036014bbbf1f508621840f44144d7;p=helm.git

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index d8e92cbad..4193d41da 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -912,19 +912,72 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa
 ;;
 *)
 
-module CacheElem : Set.OrderedType =
- struct
-  type t = 
-   | Failed_in of int * NCic.term     (* depth, goal type *)
-   | Succeded of Cic.term * Cic.term  (* proof, proof type *)
-   | UnderInspection of Cic.term      (* avoid looping *)
 
-  let compare = Pervasives.compare
- end
+type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
 
-module CacheSet = Set.Make(CacheElem)
-module Cache = 
-  Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CacheSet)
+let mk_th_cache status gl = 
+  List.fold_left 
+    (fun (status, acc) g ->
+       let gty = get_goalty status g in
+       let ctx = ctx_of gty in
+       if List.mem_assq ctx acc then status, acc else
+         let idx = InvRelDiscriminationTree.empty in
+         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 idx = InvRelDiscriminationTree.index idx ty t in
+              status, i+1, idx)
+             (status, 1, idx) ctx
+          in
+         status, (ctx, idx) :: acc)
+    (status,[]) gl
+;;
+
+let add_to_th t ty c = 
+  let key_c = ctx_of t in
+  if not (List.mem_assq key_c c) then
+      (key_c ,InvRelDiscriminationTree.index 
+               InvRelDiscriminationTree.empty ty t ) :: c 
+  else
+    let rec replace = function
+      | [] -> []
+      | (x, idx) :: tl when x == key_c -> 
+          (x, InvRelDiscriminationTree.index idx ty t) :: tl
+      | x :: tl -> x :: replace tl
+    in 
+      replace c
+;;
+
+let search_in_th gty th = 
+  let c = ctx_of gty in
+  let rec aux acc = function
+   | [] -> Ncic_termSet.elements acc
+   | (_::tl) as k ->
+       try 
+         let idx = List.assq k th in
+         let acc = Ncic_termSet.union acc 
+           (InvRelDiscriminationTree.retrieve_unifiables idx gty)
+         in
+         aux acc tl
+       with Not_found -> aux acc tl
+  in
+    aux Ncic_termSet.empty c
+;;
+
+let pp_th status = 
+  List.iter 
+    (fun ctx, idx ->
+       prerr_endline "-----------------------------------------------";
+       prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx);
+       prerr_endline "||====>  ";
+       InvRelDiscriminationTree.iter idx
+          (fun k set ->
+             prerr_endline ("K: " ^ NCicInverseRelIndexable.string_of_path k);
+             Ncic_termSet.iter 
+             (fun t -> prerr_endline ("\t"^ppterm status t)) set))
+;;
 
 type cache_examination_result =
   [ `Failed_in of int
@@ -936,7 +989,7 @@ type cache_examination_result =
 type sort = T | P
 type goal = int * int * sort (* goal, depth, sort *)
 type fail = goal * cic_term
-type candidate = int * NCic.term (* unique candidate number, candidate *)
+type candidate = int * Ast.term (* unique candidate number, candidate *)
 
 type op = 
   (* goal has to be proved *)
@@ -952,7 +1005,7 @@ type 'a elem =
 type 'a auto_status = 
   (* list of computations that may lead to the solution: all op list will
    * end with the same (S(g,_)) *)
-  'a elem list * Cache.t
+  'a elem list * th_cache
 
 type 'a auto_result = 
   | Gaveup 
@@ -969,9 +1022,9 @@ let close_failures _ c = c;;
 let prunable _ _ _ = false;;
 let cache_examine cache gty = `Notfound;;
 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 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 equational_case _ _ _ _ _ _ = [];;
 let sort_new_elems l = l;;
 let only _ _ _ = true;;
 
@@ -979,41 +1032,42 @@ let candidate_no = ref 0;;
 
 let try_candidate status t g =
  try
-   debug_print (lazy (" try " ^ 
-     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t
-   ));
-   let ast_for_t = 
-     match t with
-     | NCic.Rel i -> assert false
-     | NCic.Const ref -> Ast.NRef ref
-     | _ -> assert false
-   in
+   debug_print (lazy (" try " ^ CicNotationPp.pp_term t));
    let status = NTactics.focus_tac [g] status in
-   let status = NTactics.apply_tac ("",0,ast_for_t) status in
+   let status = NTactics.apply_tac ("",0,t) status in
    let open_goals = head_goals status#stack in
+   debug_print 
+     (lazy (" success: "^String.concat " "(List.map string_of_int open_goals)));
    incr candidate_no;
    Some ((!candidate_no,t),status,open_goals)
- with Error (msg,exn) -> debug_print msg; None
+ with Error (msg,exn) -> debug_print (lazy " failed"); None
 ;;
 
+let rec mk_irl n = function
+  | [] -> []
+  | _ :: tl -> NCic.Rel n :: mk_irl (n+1) tl
+;;
 
-let get_candidates status context gty =
+let get_candidates status cache_th signature gty =
   let universe = status#auto_cache in
-  let _, gty = term_of_cic_term status gty (ctx_of gty) in
+  let context = ctx_of gty in
+  let _, raw_gty = term_of_cic_term status gty context in
   let cands = 
-    NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty
+    NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty
   in
-  (* XXX we have to trie for the context *)
-  let cands = NDiscriminationTree.TermSet.elements cands in
-  List.iter (fun x -> 
-    debug_print (lazy (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)))
-    cands;
-  cands
+  let cands = 
+    List.filter (only signature context) 
+      (NDiscriminationTree.TermSet.elements cands)
+  in
+  List.map (fun t -> 
+     let _status, t = term_of_cic_term status t context in Ast.NCic t) 
+     (search_in_th gty cache_th)
+  @ 
+  List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
 ;;
 
-let applicative_case signature status flags g gty cache context = 
-  let candidates = get_candidates status context gty in
-  let candidates = List.filter (only signature context) candidates in
+let applicative_case signature status flags g gty cache = 
+  let candidates = get_candidates status cache signature gty in
   debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates)));
   let elems = 
     List.fold_left 
@@ -1027,17 +1081,17 @@ let applicative_case signature status flags g gty cache context =
 ;;
 
 let equational_and_applicative_case
-  signature flags status g depth gty cache context
+  signature flags status g depth gty cache 
 =
  let elems = 
   if false (*is_equational_case gty flags*) then
     let elems =
       equational_case
-        signature status flags g gty cache context
+        signature status flags g gty cache 
     in
     let more_elems =
         applicative_case 
-          signature status flags g gty cache context
+          signature status flags g gty cache 
     in
       elems@more_elems
   else
@@ -1048,7 +1102,7 @@ let equational_and_applicative_case
            gty m context signature universe cache flags
       | None -> *)
          applicative_case 
-          signature status flags g gty cache context
+          signature status flags g gty cache 
     in
       elems
  in
@@ -1057,7 +1111,7 @@ let equational_and_applicative_case
    List.map (fun c,s,gl -> c,s,List.map (fun i -> i,depth-1,P) gl) elems 
  in
  let elems = sort_new_elems elems in
- elems
+ elems, cache
 ;;
 
 let calculate_goal_ty (goalno,_,_) status = 
@@ -1084,7 +1138,43 @@ let remove_s_from_fl (id,_,_) (fl : fail list) =
     aux fl
 ;;
 
-let auto_main context flags signature elems cache =
+let rec guess_name name ctx = 
+  if name = "_" then guess_name "auto" ctx else
+  if not (List.mem_assoc name ctx) then name else
+  guess_name (name^"'") ctx
+;;
+
+let intro_case status gno gty depth cache name =
+   let status = NTactics.focus_tac [gno] status in
+   let status = NTactics.intro_tac (guess_name name (ctx_of gty)) status in
+   let open_goals = head_goals status#stack in
+   assert (List.length open_goals  = 1);
+   let open_goal = List.hd open_goals in
+   let status, cache =
+     let ngty = get_goalty status open_goal in
+     let ctx = ctx_of ngty in
+     let t = mk_cic_term ctx (NCic.Rel 1) in
+     let status, ty = typeof status ctx t in
+     let _status, ty, _args = saturate status ty in
+     status, add_to_th t ty cache 
+   in
+   debug_print (lazy (" intro: "^ string_of_int open_goal));
+(*    pp_th status cache; *)
+   incr candidate_no;
+    (* XXX calculate the sort *)
+   [(!candidate_no,Ast.Implicit `JustOne),status,[open_goal,depth,P]],
+   cache
+;;
+                      
+let do_something signature flags s gno depth gty cache =
+  let _s, raw_gty = term_of_cic_term s gty (ctx_of gty) in
+  match raw_gty with
+  | NCic.Prod (name,_,_) -> intro_case s gno gty depth cache name
+  | _ -> 
+      equational_and_applicative_case signature flags s gno depth gty cache
+;;
+
+let auto_main flags signature elems cache =
   let rec aux (elems, cache : 'a auto_status) =
 (* processa le hint dell'utente *)
 (*     let cache, elems = filter_prune_hint cache elems in *)
@@ -1112,7 +1202,7 @@ let auto_main context flags signature elems cache =
     | (s, size, don, (S(g, key, c) as op)::todo, fl)::orlist ->
         let cache, orlist, fl, sibling_pruned = 
           add_to_cache_and_del_from_orlist_if_green_cut 
-            g s cache key todo orlist fl context size 
+            g s cache key todo orlist fl size 
         in
         let fl = remove_s_from_fl g fl in
         let don = if sibling_pruned then don else op::don in
@@ -1136,6 +1226,7 @@ let auto_main context flags signature elems cache =
             debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
             aux ((s,size,don,todo, fl)::orlist, cache)
         | Some gty ->
+            let s, gty = apply_subst s (ctx_of gty) gty in
             debug_print (lazy ("EXAMINE: "^ ppterm s gty));
             match cache_examine cache gty with
             | `Failed_in d when d >= depth -> 
@@ -1163,9 +1254,8 @@ let auto_main context flags signature elems cache =
                         string_of_int gno ^ "("^ string_of_int size ^ "): "^
                         ppterm s gty));
                     (* elems are possible computations for proving gty *)
-                    let elems =
-                      equational_and_applicative_case 
-                        signature flags s gno depth gty cache context
+                    let elems, cache = 
+                      do_something signature flags s gno depth gty cache
                     in
                     if elems = [] then
                       (* this goal has failed *)
@@ -1204,21 +1294,26 @@ let auto_main context flags signature elems cache =
     (aux (elems, cache) : 'a auto_result)
 ;;
 
-let auto_tac ~params status =
-  let cache = Cache.empty in
+let int name l def = 
+  try int_of_string (List.assoc name l)
+  with Failure _ | Not_found -> def
+;;
+
+let auto_tac ~params:(_univ,flags) status =
   let goals = head_goals status#stack in
-  let depth = 3 in (* XXX fix sort *)
+  let status, cache = mk_th_cache status goals in
+  let depth = int "depth" flags 3 in 
+  (* XXX fix sort *)
   let goals = List.map (fun i -> D(i,depth,P)) goals in
   let elems = [status,0,[],goals,[]] in
-  let context = [] (* XXX big problem *) in
   let signature = () in
   let flags = { 
-          maxwidth = 3; 
+          maxwidth = 3 + List.length goals; 
           maxsize = 10; 
           timeout = Unix.gettimeofday() +. 3000.;
           do_types = false; 
   } in
-  match auto_main context flags signature elems cache with
+  match auto_main flags signature elems cache with
   | Gaveup -> raise (Error (lazy "auto gave up", None))
   | Proved (s, (_orlist, _cache)) -> 
       let stack =