X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=0ff4ddbe5358b82e7c27782c4e5974b6693d6e2e;hb=711a06aebcd4f8e1127a56d82dd1fc4de22d5ea2;hp=4d6d7f8867bb3ada4821ff47ca46a5a6ab84d6b6;hpb=e97c74e4d17e6fc0ce7c39b092f3214244ae21d1;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 4d6d7f886..0ff4ddbe5 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -14,8 +14,10 @@ open Printf
 let debug = ref false
 let debug_print ?(depth=0) s = 
   if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
-let print ?(depth=0) s = 
+(* let print= debug_print *)
+ let print ?(depth=0) s = 
   prerr_endline (String.make depth '\t'^Lazy.force s) 
+
 let debug_do f = if !debug then f () else ()
 
 open Continuationals.Stack
@@ -51,6 +53,190 @@ let auto_paramod_tac ~params status =
   NTactics.distribute_tac (auto_paramod ~params) status
 ;;
 
+(*************** subsumption ****************)
+module IntSet = Set.Make(struct type t = int let compare = compare end)
+(* exceptions *)
+
+let get_sgoalty status g =
+ let _,_,metasenv,subst,_ = status#obj in
+ try
+   let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
+   let ty = NCicUntrusted.apply_subst subst ctx ty in
+   let ctx = NCicUntrusted.apply_subst_context 
+     ~fix_projections:true subst ctx
+   in
+     NTacStatus.mk_cic_term ctx ty
+ with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
+;;
+
+let deps status g =
+  let gty = get_sgoalty status g in
+  metas_of_term status gty
+;;
+
+let menv_closure status gl = 
+  let rec closure acc = function
+    | [] -> acc
+    | x::l when IntSet.mem x acc -> closure acc l
+    | x::l -> closure (IntSet.add x acc) (deps status x @ l)
+  in closure IntSet.empty gl
+;;
+
+let close_wrt_context =
+  List.fold_left 
+    (fun ty ctx_entry -> 
+	match ctx_entry with 
+       | name, NCic.Decl t -> NCic.Prod(name,t,ty)
+       | name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty)
+;;
+
+let args_for_context ?(k=1) ctx =
+  let _,args =
+    List.fold_left 
+      (fun (n,l) ctx_entry -> 
+	 match ctx_entry with 
+	   | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
+	   | name, NCic.Def(bo, _) -> n+1,l)
+      (k,[]) ctx in
+    args
+
+let constant_for_meta ctx ty i =
+  let name = "cic:/foo"^(string_of_int i)^".con" in
+  let uri = NUri.uri_of_string name in
+  let ty = close_wrt_context ty ctx in
+  (* prerr_endline (NCicPp.ppterm [] [] [] ty); *)
+  let attr = (`Generated,`Definition,`Local) in
+  let obj = NCic.Constant([],name,None,ty,attr) in
+    (* Constant  of relevance * string * term option * term * c_attr *)
+    (uri,0,[],[],obj)
+
+(* not used *)
+let refresh metasenv =
+  List.fold_left 
+    (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
+       let ikind = NCicUntrusted.kind_of_meta iattr in
+       let metasenv,j,instance,ty = 
+	 NCicMetaSubst.mk_meta ~attrs:iattr 
+	   metasenv ctx ~with_type:ty ikind in
+       let s_entry = i,(iattr, ctx, instance, ty) in
+       let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
+	 metasenv,s_entry::subst) 
+      (metasenv,[]) metasenv
+
+(* close metasenv returns a ground instance of all the metas in the
+metasenv, insantiatied with axioms, and the list of these axioms *)
+let close_metasenv metasenv subst = 
+  (*
+  let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
+  *)
+  let metasenv = NCicUntrusted.sort_metasenv subst metasenv in 
+    List.fold_left 
+      (fun (subst,objs) (i,(iattr,ctx,ty)) ->
+	 let ty = NCicUntrusted.apply_subst subst ctx ty in
+         let ctx = 
+	   NCicUntrusted.apply_subst_context ~fix_projections:true 
+	     subst ctx in
+	 let (uri,_,_,_,obj) as okind = 
+	   constant_for_meta ctx ty i in
+	 try
+	   NCicEnvironment.check_and_add_obj okind;
+	   let iref = NReference.reference_of_spec uri NReference.Decl in
+	   let iterm =
+	     let args = args_for_context ctx in
+	       if args = [] then NCic.Const iref 
+	       else NCic.Appl(NCic.Const iref::args)
+	   in
+           (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
+	   let s_entry = i, ([], ctx, iterm, ty)
+	   in s_entry::subst,okind::objs
+	 with _ -> assert false)
+      (subst,[]) metasenv
+;;
+
+let ground_instances status gl =
+  let _,_,metasenv,subst,_ = status#obj in
+  let subset = menv_closure status gl in
+  let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
+(*
+  let submenv = metasenv in
+*)
+  let subst, objs = close_metasenv submenv subst in
+  try
+    List.iter
+      (fun i -> 
+	 let (_, ctx, t, _) = List.assoc i subst in
+	   debug_print (lazy (NCicPp.ppterm ctx [] [] t));
+	   List.iter 
+	     (fun (uri,_,_,_,_) as obj -> 
+		NCicEnvironment.invalidate_item (`Obj (uri, obj))) 
+	     objs;
+	   ())
+      gl
+  with
+      Not_found -> assert false 
+  (* (ctx,t) *)
+;;
+
+let replace_meta i args target = 
+  let rec aux k = function
+    (* TODO: local context *)
+    | NCic.Meta (j,lc) when i = j ->
+	(match args with
+	   | [] -> NCic.Rel 1
+	   | _ -> let args = 
+	       List.map (NCicSubstitution.subst_meta lc) args in
+	       NCic.Appl(NCic.Rel k::args))
+    | NCic.Meta (j,lc) as m ->
+        (match lc with
+           _,NCic.Irl _ -> m
+         | n,NCic.Ctx l ->
+            NCic.Meta
+             (i,(0,NCic.Ctx
+                 (List.map (fun t ->
+                   aux k (NCicSubstitution.lift n t)) l))))
+    | t -> NCicUtils.map (fun _ k -> k+1) k aux t
+ in
+   aux 1 target
+;;
+
+let close_wrt_metasenv subst =
+  List.fold_left 
+    (fun ty (i,(iattr,ctx,mty)) ->
+       let mty = NCicUntrusted.apply_subst subst ctx mty in
+       let ctx = 
+	 NCicUntrusted.apply_subst_context ~fix_projections:true 
+	   subst ctx in
+       let cty = close_wrt_context mty ctx in
+       let name = "foo"^(string_of_int i) in
+       let ty = NCicSubstitution.lift 1 ty in
+       let args = args_for_context ~k:1 ctx in
+         (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
+       let ty = replace_meta i args ty
+       in
+       NCic.Prod(name,cty,ty))
+;;
+
+let close status g =
+  let _,_,metasenv,subst,_ = status#obj in
+  let subset = menv_closure status [g] in
+  let subset = IntSet.remove g subset in
+  let elems = IntSet.elements subset in 
+  let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
+  let ty = NCicUntrusted.apply_subst subst ctx ty in
+  debug_print (lazy ("metas in " ^ (NCicPp.ppterm ctx [] metasenv ty)));
+  debug_print (lazy (String.concat ", " (List.map string_of_int elems)));
+  let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
+  let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in 
+(*  
+    let submenv = metasenv in
+*)
+  let ty = close_wrt_metasenv subst ty submenv in
+    debug_print (lazy (NCicPp.ppterm ctx [] [] ty));
+    ctx,ty
+;;
+
+
+
 (* =================================== auto =========================== *)
 (****************** AUTO ********************
 
@@ -994,7 +1180,6 @@ let pp_th status =
        pp_idx status idx)
 ;;
 
-
 let search_in_th gty th = 
   let c = ctx_of gty in
   let rec aux acc = function
@@ -1024,21 +1209,18 @@ type goal = int * sort (* goal, depth, sort *)
 type fail = goal * cic_term
 type candidate = int * Ast.term (* unique candidate number, candidate *)
 
-module IntSet = Set.Make(struct type t = int let compare = compare end)
-(* exceptions *)
-
 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
                                 atoms of the input goals *)
 exception Proved of #NTacStatus.tac_status
 
-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 cache_add_underinspection c _ _ = c;;
+(* 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 cache_add_underinspection c _ _ = c;; *)
 let equational_case _ _ _ _ _ _ = [];;
-let only _ _ _ = true;;
+let only _ _ _ = true;; 
 
 let candidate_no = ref 0;;
 
@@ -1046,10 +1228,9 @@ let sort_new_elems l =
   List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l
 ;;
 
-let try_candidate flags depth status t g =
+let try_candidate flags depth status t =
  try
    debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
-   (* let status = NTactics.focus_tac [g] status in *)
    let status = NTactics.apply_tac ("",0,t) status in
    let open_goals = head_goals status#stack in
    debug_print ~depth
@@ -1063,12 +1244,12 @@ let try_candidate flags depth status t g =
  with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
 ;;
 
-let get_candidates status cache_th signature gty =
+let get_candidates status cache signature gty =
   let universe = status#auto_cache 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 raw_gty
+  let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables 
+	universe raw_gty
   in
   let cands = 
     List.filter (only signature context) 
@@ -1076,20 +1257,21 @@ let get_candidates status cache_th signature gty =
   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)
+     (search_in_th gty cache)
   @ 
   List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
 ;;
 
-let applicative_case depth signature status flags g gty cache =
+let applicative_case depth signature status flags gty cache =
+  let tcache,_ = cache in
   app_counter:= !app_counter+1; 
-  let candidates = get_candidates status cache signature gty in
+  let candidates = get_candidates status tcache signature gty in
   debug_print ~depth
     (lazy ("candidates: " ^ string_of_int (List.length candidates)));
   let elems = 
     List.fold_left 
       (fun elems cand ->
-        match try_candidate flags depth status cand g with
+        match try_candidate flags depth status cand with
         | None -> elems
         | Some x -> x::elems)
       [] candidates
@@ -1097,6 +1279,52 @@ let applicative_case depth signature status flags g gty cache =
   elems
 ;;
 
+exception Found
+;;
+
+(* gty is supposed to be meta-closed *)
+let is_subsumed depth status gty (_,cache) =
+  if cache=[] then false else (
+  debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty))); 
+  let n,h,metasenv,subst,obj = status#obj in
+  let ctx = ctx_of gty in
+  let _ , target = term_of_cic_term status gty ctx in
+  let target = NCicSubstitution.lift 1 target in 
+  (* candidates must only be searched w.r.t the given context *)
+  let candidates = 
+    try
+    let idx = List.assq ctx cache in
+      Ncic_termSet.elements 
+	(InvRelDiscriminationTree.retrieve_generalizations idx gty)
+    with Not_found -> []
+  in
+  debug_print ~depth
+    (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
+    try
+      List.iter
+	(fun t ->
+	   let _ , source = term_of_cic_term status t ctx in
+	   let implication = 
+	     NCic.Prod("foo",source,target) in
+	   let metasenv,j,_,_ = 
+	     NCicMetaSubst.mk_meta  
+	       metasenv ctx ~with_type:implication `IsType in
+	   let status = status#set_obj (n,h,metasenv,subst,obj) in
+	   let status = status#set_stack [([1,Open j],[],[],`NoTag)] in 
+	   try
+	     let status = NTactics.intro_tac "foo" status in
+	     let status =
+	       NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
+	     in 
+	       if (head_goals status#stack = []) then raise Found
+	       else ()
+           with
+	     | Error _ -> ())
+	candidates;false
+    with Found -> debug_print ~depth (lazy "success");true)
+;;
+
+
 let equational_and_applicative_case
   signature flags status g depth gty cache 
 =
@@ -1108,7 +1336,7 @@ let equational_and_applicative_case
     in
     let more_elems =
         applicative_case depth
-          signature status flags g gty cache 
+          signature status flags gty cache 
     in
       elems@more_elems
   else
@@ -1119,7 +1347,7 @@ let equational_and_applicative_case
            gty m context signature universe cache flags
       | None -> *)
          applicative_case depth
-          signature status flags g gty cache 
+          signature status flags gty cache 
     in
       elems
  in
@@ -1135,7 +1363,7 @@ let equational_and_applicative_case
                       in
 			i,sort) gl) elems 
  in
- let elems = sort_new_elems elems in
+ (* let elems = sort_new_elems elems in *)
  elems, cache
 ;;
 
@@ -1145,22 +1373,59 @@ let rec guess_name name ctx =
   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 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, keys = keys_of_term status t in
-   let cache = List.fold_left (add_to_th t) cache keys in
-   debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
-   incr candidate_no;
-    (* XXX compute the sort *)
-   [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[open_goal,P]],
-   cache
+let intro ~depth status (tcache,fcache) name =
+  let status = NTactics.intro_tac name 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 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, keys = keys_of_term status t in
+  let tcache = List.fold_left (add_to_th t) tcache keys in
+    debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
+  (* unprovability is not stable w.r.t introduction *)
+  status, (tcache,[])
+;;
+
+let rec intros ~depth status cache =
+  let open_goals = head_goals status#stack in
+  assert (List.length open_goals  = 1);
+  let open_goal = List.hd open_goals in
+  let gty = get_goalty status open_goal in
+  let _, raw_gty = term_of_cic_term status gty (ctx_of gty) in
+  match raw_gty with
+    | NCic.Prod (name,_,_) ->
+	let status,cache =
+	  intro ~depth status cache (guess_name name (ctx_of gty))
+	in intros ~depth status cache 
+    | _ -> status, cache, open_goal
+;;
+
+let reduce ~depth status g = 
+  let n,h,metasenv,subst,o = status#obj in 
+  let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
+  let ty = NCicUntrusted.apply_subst subst ctx ty in
+  let ty' = NCicReduction.whd ~subst ctx ty in
+  if ty = ty' then []
+  else
+    (debug_print ~depth 
+      (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty'));
+    let metasenv = 
+      (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv) 
+    in
+    let status = status#set_obj (n,h,metasenv,subst,o) in
+    incr candidate_no;
+    [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[g,P]])
+;;
+
+let do_something signature flags status g depth gty cache =
+  let l = reduce ~depth status g in
+  let l1,cache =
+      (equational_and_applicative_case 
+	 signature flags status g depth gty cache)
+  in
+    sort_new_elems (l@l1), cache
 ;;
 
 let pp_goal = function
@@ -1177,25 +1442,13 @@ let pp_goals status l =
        l)
 ;;
 
-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 deps status g =
-  let gty = get_goalty status g in
-  metas_of_term status gty
-;;
-
 module M = 
   struct 
     type t = int
     let compare = Pervasives.compare
   end
 ;;
+
 module MS = HTopoSort.Make(M)
 ;;
 
@@ -1290,9 +1543,6 @@ let rec auto_clusters
 
 and
 
-(* The pair solved,init_status is used for chaching purposes.
-   solved is the list of goals in init_status already proved. 
-   Initially, init_status=status and k is set to [] *)
 (* let rec auto_main flags signature cache status k depth = *)
 
 auto_main flags signature cache depth status: unit =
@@ -1303,28 +1553,37 @@ auto_main flags signature cache depth status: unit =
   match goals with
     | [] -> raise (Proved status)
     | g::tlg ->
-        if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
-	else
-        let status = 
+	if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
+        else
+	let status = 
 	  if tlg=[] then status 
 	  else NTactics.branch_tac status in
+        let status, cache, g = intros ~depth status cache in
         let gty = get_goalty status g in
+	let ctx,ty = close status g in
+	let closegty = mk_cic_term ctx ty in
         let status, gty = apply_subst status (ctx_of gty) gty in
-        debug_print ~depth (lazy("Depth = " ^ (string_of_int depth)));
-	print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
-        (* let closed = metas_of_term status gty = [] in *)
+	debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); 
+        if is_subsumed depth status closegty cache then 
+	  (debug_print (lazy "SUBSUMED");
+	   raise (Gaveup IntSet.add g IntSet.empty))
+	else 
 	let alternatives, cache = 
           do_something signature flags status g depth gty cache in
+	let loop_cache =         
+	  let tcache,fcache = cache in
+	    tcache,add_to_th closegty fcache closegty in
 	let unsat =
 	  List.fold_left
             (* the underscore information does not need to be returned
                by do_something *)
 	    (fun unsat ((_,t),_,_,status,_) ->
-               let depth' = 
-		 if t=(Ast.Implicit `JustOne) then depth else depth+1 in
-               print (~depth:depth') 
-		 (lazy ("Case: " ^ CicNotationPp.pp_term t)); 
-	       try auto_clusters flags signature cache 
+	       let depth',looping_cache = 
+		 if t=(Ast.Implicit `JustOne) then depth,cache 
+		 else depth+1, loop_cache in
+               debug_print (~depth:depth') 
+		 (lazy ("Case: " ^ CicNotationPp.pp_term t));
+	       try auto_clusters flags signature loop_cache
 		 depth' status; unsat
                with 
 		 | Proved status ->
@@ -1333,10 +1592,10 @@ auto_main flags signature cache depth status: unit =
 		     else 
 		       let status = NTactics.merge_tac status
 		     in
-		     (try auto_clusters flags signature cache 
-			depth status; unsat
+		     ( (* old cache, here *)
+		       try auto_clusters flags signature cache 
+			depth status; assert false
 		      with Gaveup f ->
-                        let debug_print = print in
 			debug_print ~depth 
 			  (lazy ("Unsat1 at depth " ^ (string_of_int depth)
 				   ^ ": " ^ 
@@ -1344,7 +1603,6 @@ auto_main flags signature cache depth status: unit =
                         (* TODO: cache failures *)
 			IntSet.union f unsat)
 		 | Gaveup f -> 
-                     let debug_print = print in
 		     debug_print (~depth:depth')
 		       (lazy ("Unsat2 at depth " ^ (string_of_int depth')
 			      ^ ": " ^ 
@@ -1390,16 +1648,21 @@ let auto_tac ~params:(_univ,flags) status =
   let initial_time = Unix.gettimeofday() in
   app_counter:= 0;
   let rec up_to x y =
-    if x > y then raise (Error (lazy "auto gave up", None))
+    if x > y then
+      (print(lazy
+        ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
+       print(lazy
+        ("Applicative nodes:"^string_of_int !app_counter)); 
+       raise (Error (lazy "auto gave up", None)))
     else
       let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
       let flags = { flags with maxdepth = x } 
       in 
-	try auto_clusters flags signature cache 0 status;status 
+	try auto_clusters flags signature (cache,[]) 0 status;status 
 	with
 	  | Gaveup _ -> up_to (x+1) y
 	  | Proved s -> 
-              HLog.debug ("proved at depth " ^ string_of_int x);
+              print (lazy ("proved at depth " ^ string_of_int x));
               let stack = 
 		match s#stack with
 		  | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
@@ -1408,9 +1671,9 @@ let auto_tac ~params:(_univ,flags) status =
 		s#set_stack stack
   in
   let s = up_to depth depth in
-    debug_print(lazy
+    print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
-    debug_print(lazy
+    print(lazy
         ("Applicative nodes:"^string_of_int !app_counter));
     s
 ;;