X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=fdf2d2ea3138130ca23aa7ecabeac40b0fc1fdb0;hb=ced2abc1e3fe84d5bbfa9ccb2ebf46f253279ebe;hp=0251a84c9062fe1c5bc290cac5eae55dfe93d262;hpb=fa0b30be968340ec83c8821169218e7bdcbc8426;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 0251a84c9..fdf2d2ea3 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -11,11 +11,11 @@
 
 open Printf
 
-let debug = ref true
+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= debug_print *)
- 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 ()
@@ -53,10 +53,11 @@ let menv_closure status gl =
   in closure IntSet.empty gl
 ;;
 
-(* we call a "fact" an object whose hypothesis occurs in the goal 
+(* we call a "fact" an object whose hypothesis occur in the goal 
    or in types of goal-variables *)
 let is_a_fact status ty =   
-  let status, ty, _ = saturate ~delta:max_int status ty in
+  let status, ty, _ = saturate ~delta:0 status ty in
+  debug_print (lazy (ppterm status ty));
   let g_metas = metas_of_term status ty in
   let clos = menv_closure status g_metas in
   let _,_,metasenv,_,_ = status#obj in
@@ -83,69 +84,109 @@ let current_goal status =
     open_goal, ctx, gty
 
 
-
 (* =============================== paramod =========================== *)
-let auto_paramod ~params:(l,_) status goal =
-  let gty = get_goalty status goal in
+let solve fast status eq_cache goal =
+  let f = 
+    if fast then NCicParamod.fast_eq_check
+    else NCicParamod.paramod in
   let n,h,metasenv,subst,o = status#obj in
-  let status,t = term_of_cic_term status gty (ctx_of gty) in
-  let status, l = 
-    List.fold_left
-      (fun (status, l) t ->
-        let status, t = disambiguate status (ctx_of gty) t None in
-        let status, ty = typeof status (ctx_of t) t in
-        let status, t =  term_of_cic_term status t (ctx_of gty) in
-        let status, ty = term_of_cic_term status ty (ctx_of ty) in
-        (status, (t,ty) :: l))
-      (status,[]) l
-  in
-  match
-    NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
-  with
-  | [] -> raise (Error (lazy "no proof found",None))
-  | (pt, metasenv, subst)::_ -> 
-      let status = status#set_obj (n,h,metasenv,subst,o) in
-      instantiate status goal (mk_cic_term (ctx_of gty) pt)
-;;
-
-let auto_paramod_tac ~params status = 
-  NTactics.distribute_tac (auto_paramod ~params) status
-;;
-
-let fast_eq_check_all status eq_cache goal =
-  let gty = get_goalty status goal in
-  let ctx = ctx_of gty in 
-  let n,h,metasenv,subst,o = status#obj in
-  let status,t = term_of_cic_term status gty ctx in 
-  let build_status (pt, metasenv, subst) =
-    let status = status#set_obj (n,h,metasenv,subst,o) in
-    let gty = get_goalty status goal in
-    instantiate status goal (mk_cic_term ctx pt)
-  in
-    List.map build_status
-      (NCicParamod.fast_eq_check status metasenv subst ctx 
-	 eq_cache (NCic.Rel ~-1,t))
+  let gname, ctx, gty = List.assoc goal metasenv in
+  let gty = NCicUntrusted.apply_subst subst ctx gty in
+  let build_status (pt, _, metasenv, subst) =
+    try
+      debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
+      let stamp = Unix.gettimeofday () in 
+      let metasenv, subst, pt, pty =
+	NCicRefiner.typeof status
+       	 (* (status#set_coerc_db NCicCoercion.empty_db) *)
+	  metasenv subst ctx pt None in
+	debug_print (lazy ("refined: "^(NCicPp.ppterm ctx subst metasenv pt)));
+	debug_print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty)));
+	let metasenv, subst =
+	  NCicUnification.unify status metasenv subst ctx gty pty 
+	(* the previous code is much less expensive than directly refining
+	   pt with expected type pty 
+	   in 
+	   prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty));
+	   NCicRefiner.typeof 
+       	     (status#set_coerc_db NCicCoercion.empty_db) 
+	     metasenv subst ctx pt (Some gty) *)
+	in 
+	  print (lazy (Printf.sprintf "Refined in %fs"
+		     (Unix.gettimeofday() -. stamp))); 
+	  let status = status#set_obj (n,h,metasenv,subst,o) in
+	  let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
+	  let subst = (goal,(gname,ctx,pt,pty)) :: subst in
+	    Some (status#set_obj (n,h,metasenv,subst,o))
+    with 
+	NCicRefiner.RefineFailure msg 
+      | NCicRefiner.Uncertain msg ->
+	  debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+			snd (Lazy.force msg))); None
+      | NCicRefiner.AssertFailure msg -> 
+	  debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+			Lazy.force msg)); None
+      | _ -> None
+    in
+    HExtlib.filter_map build_status
+      (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
 ;;
 
 let fast_eq_check eq_cache status goal =
-  match fast_eq_check_all status eq_cache goal with
+  match solve true status eq_cache goal with
   | [] -> raise (Error (lazy "no proof found",None))
   | s::_ -> s
 ;;
 
-let fast_eq_check_tac ~params s = 
-  NTactics.distribute_tac (fast_eq_check s#eq_cache) s
+let dist_fast_eq_check eq_cache s = 
+  NTactics.distribute_tac (fast_eq_check eq_cache) s
 ;;
 
 let auto_eq_check eq_cache status =
   try 
-    let s = 
-      NTactics.distribute_tac (fast_eq_check eq_cache) status in
+    let s = dist_fast_eq_check eq_cache status in
       [s]
   with
     | Error _ -> []
 ;;
 
+(* warning: ctx is supposed to be already instantiated w.r.t subst *)
+let index_local_equations eq_cache status =
+  let open_goals = head_goals status#stack in
+  let open_goal = List.hd open_goals in
+  let ngty = get_goalty status open_goal in
+  let ctx = ctx_of ngty in
+  let c = ref 0 in
+  List.fold_left 
+    (fun eq_cache _ ->
+       c:= !c+1;
+       let t = NCic.Rel !c in
+	 try
+	   let ty = NCicTypeChecker.typeof [] [] ctx t in
+             debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
+	     NCicParamod.forward_infer_step eq_cache t ty
+	 with 
+	   | NCicTypeChecker.TypeCheckerFailure _
+	   | NCicTypeChecker.AssertFailure _ -> eq_cache) 
+    eq_cache ctx
+;;
+
+let fast_eq_check_tac ~params s = 
+  let unit_eq = index_local_equations s#eq_cache s in   
+  dist_fast_eq_check unit_eq s
+;;
+
+let paramod eq_cache status goal =
+  match solve false status eq_cache goal with
+  | [] -> raise (Error (lazy "no proof found",None))
+  | s::_ -> s
+;;
+
+let paramod_tac ~params s = 
+  let unit_eq = index_local_equations s#eq_cache s in   
+  NTactics.distribute_tac (paramod unit_eq) s
+;;
+
 (*
 let fast_eq_check_tac_all  ~params eq_cache status = 
   let g,_,_ = current_goal status in
@@ -158,6 +199,17 @@ let fast_eq_check_tac_all  ~params eq_cache status =
 ;;
 *)
 
+(*
+let demod status eq_cache goal =
+  let n,h,metasenv,subst,o = status#obj in
+  let gname, ctx, gty = List.assoc goal metasenv in
+  let gty = NCicUntrusted.apply_subst subst ctx gty in
+
+let demod_tac ~params s = 
+  let unit_eq = index_local_equations s#eq_cache s in   
+  dist_fast_eq_check unit_eq s
+*)
+
 (*************** subsumption ****************)
 
 let close_wrt_context =
@@ -1179,6 +1231,47 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa
 ;;
 *)
 
+(****************** smart application ********************)
+
+
+let smart_apply t unit_eq status g = 
+  let n,h,metasenv,subst,o = status#obj in
+  let gname, ctx, gty = List.assoc g metasenv in
+  (* let ggty = mk_cic_term context gty in *)
+  let status, t = disambiguate status ctx t None in
+  let status,t = term_of_cic_term status t ctx in
+  let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+  let ty,metasenv,args = NCicMetaSubst.saturate metasenv subst ctx ty 0 in
+  let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
+  let status = status#set_obj (n,h,metasenv,subst,o) in
+  let pterm = if args=[] then t else NCic.Appl(t::args) in
+  let eq_coerc =       
+    let uri = 
+      NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
+    let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
+      NCic.Const ref
+  in
+  let smart = 
+    NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
+  let smart = mk_cic_term ctx smart in 
+    try
+      let status = instantiate status g smart in
+      let _,_,metasenv,subst,_ = status#obj in
+      let _,ctx,jty = List.assoc j metasenv in
+      let jty = NCicUntrusted.apply_subst subst ctx jty in
+        debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
+	fast_eq_check unit_eq status j
+    with
+      | Error _ as e -> debug_print (lazy "error"); raise e
+
+let smart_apply_tac t s =
+  let unit_eq = index_local_equations s#eq_cache s in   
+  NTactics.distribute_tac (smart_apply t unit_eq) s
+
+let smart_apply_auto t eq_cache =
+  NTactics.distribute_tac (smart_apply t eq_cache)
+
+
 (****************** types **************)
 
 
@@ -1263,7 +1356,7 @@ let pp_th status =
 let search_in_th gty th = 
   let c = ctx_of gty in
   let rec aux acc = function
-   | [] -> Ncic_termSet.elements acc
+   | [] -> (* Ncic_termSet.elements *) acc
    | (_::tl) as k ->
        try 
          let idx = List.assq k th in
@@ -1297,7 +1390,7 @@ type candidate = int * Ast.term (* unique candidate number, candidate *)
 
 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
                                 atoms of the input goals *)
-exception Proved of #NTacStatus.tac_status
+exception Proved of NTacStatus.tac_status
 
 (* let close_failures _ c = c;; *)
 (* let prunable _ _ _ = false;; *)
@@ -1322,53 +1415,107 @@ let openg_no status = List.length (head_goals status#stack)
 let sort_new_elems l =
   List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
 
-let try_candidate flags depth status t =
+let try_candidate ?(smart=0) flags depth status eq_cache t =
  try
-   debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
-   let status = NTactics.apply_tac ("",0,t) status in
-   let og_no = openg_no status in 
-   if og_no > flags.maxwidth || 
+   print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t));
+  let status = 
+    if smart= 0 then NTactics.apply_tac ("",0,t) status 
+    else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status 
+    else (* smart = 2: both *)
+      try NTactics.apply_tac ("",0,t) status 
+      with Error _ -> 
+	smart_apply_auto ("",0,t) eq_cache status in 
+  let og_no = openg_no status in 
+    if (* og_no > flags.maxwidth || *)
       (depth = flags.maxdepth && og_no <> 0) then
-      (debug_print ~depth (lazy "pruned immediately"); None)
+	(print ~depth (lazy "pruned immediately"); None)
    else
      (incr candidate_no;
       Some ((!candidate_no,t),status))
  with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
 ;;
 
-let get_candidates status cache signature gty =
+let get_candidates ?(smart=true) status cache signature gty =
   let universe = status#auto_cache in
   let context = ctx_of gty in
+  let t_ast t = 
+     let _status, t = term_of_cic_term status t context 
+     in Ast.NCic t in
+  let c_ast = function 
+    | NCic.Const r -> Ast.NRef r | _ -> assert false in
   let _, raw_gty = term_of_cic_term status gty context in
   let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables 
-	universe raw_gty
-  in
-  let cands = 
-    List.filter (only signature context) 
-      (NDiscriminationTree.TermSet.elements cands)
+	universe raw_gty in
+  let local_cands = search_in_th gty cache in
+  let together global local =
+    List.map c_ast 
+      (List.filter (only signature context) 
+	(NDiscriminationTree.TermSet.elements global)) @
+      List.map t_ast (Ncic_termSet.elements local) in
+  let candidates = together cands local_cands in
+  let smart_candidates = 
+    if smart then
+      match raw_gty with
+	| NCic.Appl (hd::tl) -> 
+            let weak_gty = 
+	      NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0))) 
+			   (List.length tl)) in
+	    let more_cands = 
+	      NDiscriminationTree.DiscriminationTree.retrieve_unifiables 
+		universe weak_gty in
+	    let smart_cands = 
+	      NDiscriminationTree.TermSet.diff more_cands cands in
+ 	    let cic_weak_gty = mk_cic_term context weak_gty in
+	    let more_local_cands = search_in_th cic_weak_gty cache in
+	    let smart_local_cands = 
+	      Ncic_termSet.diff more_local_cands local_cands in
+	      together smart_cands smart_local_cands  
+	| _ -> []
+    else [] 
   in
-  List.map (fun t -> 
-     let _status, t = term_of_cic_term status t context in Ast.NCic t) 
-     (search_in_th gty cache)
-  @ 
-  List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
+    candidates, smart_candidates
 ;;
 
 let applicative_case depth signature status flags gty (cache:cache) =
-  let tcache = cache.facts in
   app_counter:= !app_counter+1; 
-  let candidates = get_candidates status tcache signature gty in
+  let _,_,metasenv,subst,_ = status#obj in
+  let context = ctx_of gty in
+  let tcache = cache.facts in
+  let is_eq =   
+    let status, t = term_of_cic_term status gty context  in 
+    NCicParamod.is_equation metasenv subst context t 
+  in
+  debug_print(lazy (string_of_bool is_eq)); 
+  let candidates, smart_candidates = 
+    get_candidates ~smart:(not is_eq) status tcache signature gty in
   debug_print ~depth
     (lazy ("candidates: " ^ string_of_int (List.length candidates)));
+  debug_print ~depth
+    (lazy ("smart candidates: " ^ 
+	     string_of_int (List.length smart_candidates)));
+(*
+  let sm = 0 in 
+  let smart_candidates = [] in *)
+  let sm = if is_eq then 0 else 2 in 
   let elems = 
     List.fold_left 
       (fun elems cand ->
-        match try_candidate flags depth status cand with
+        match try_candidate (~smart:sm) 
+	  flags depth status cache.unit_eq cand with
         | None -> elems
         | Some x -> x::elems)
       [] candidates
   in
-  elems
+  let more_elems = 
+    List.fold_left 
+      (fun elems cand ->
+        match try_candidate (~smart:1) 
+	  flags depth status cache.unit_eq cand with
+        | None -> elems
+        | Some x -> x::elems)
+      [] smart_candidates
+  in
+  elems@more_elems
 ;;
 
 exception Found
@@ -1416,28 +1563,6 @@ let is_subsumed depth status gty cache =
     with Found -> debug_print ~depth (lazy "success");true)
 ;;
 
-(* warning: ctx is supposed to be already instantiated w.r.t subst *)
-let index_local_equations eq_cache status =
-  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 c = ref 0 in
-  List.fold_left 
-    (fun eq_cache _ ->
-       c:= !c+1;
-       let t = NCic.Rel !c in
-	 try
-	   let ty = NCicTypeChecker.typeof [] [] ctx t in
-             prerr_endline ("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty));
-	     NCicParamod.forward_infer_step eq_cache t ty
-	 with 
-	   | NCicTypeChecker.TypeCheckerFailure _
-	   | NCicTypeChecker.AssertFailure _ -> eq_cache) 
-    eq_cache ctx
-;;
-
 let rec guess_name name ctx = 
   if name = "_" then guess_name "auto" ctx else
   if not (List.mem_assoc name ctx) then name else
@@ -1474,7 +1599,6 @@ let rec intros_facts ~depth status facts =
 let rec intros ~depth status (cache:cache) =
     match is_prod status with
       | Some _ ->
-          prerr_endline "is prod";
 	  let status,facts =
 	    intros_facts ~depth status cache.facts 
 	  in 
@@ -1507,17 +1631,19 @@ let do_something signature flags status g depth gty cache =
   (* whd *)
   let l = reduce ~depth status g in
   (* backward aplications *)
-  let l1 = applicative_case depth signature status flags gty cache in
-  (* fast paramodulation *) 
-  let l2 = 
+  let l1 = 
     List.map 
       (fun s ->
 	 incr candidate_no;
 	 ((!candidate_no,Ast.Ident("__paramod",None)),s))
-      (auto_eq_check cache.unit_eq status)
-  (* states in l2 have have an set of subgoals: no point to sort them *)
+      (auto_eq_check cache.unit_eq status) in
+  let l2 = 
+    if (l1 <> []) then []
+    else applicative_case depth signature status flags gty cache 
+  (* fast paramodulation *) 
   in
-    l2 @ (sort_new_elems (l@l1)), cache
+  (* states in l1 have have an empty set of subgoals: no point to sort them *)
+    l1 @ (sort_new_elems (l@l2)), cache
 ;;
 
 let pp_goal = function
@@ -1600,7 +1726,7 @@ let focus_tac focus status =
    status#set_stack gstatus
 ;;
 
-let rec auto_clusters 
+let rec auto_clusters ?(top=false)  
     flags signature cache depth status : unit =
   debug_print ~depth (lazy "entering auto clusters");
   (* ignore(Unix.select [] [] [] 0.01); *)
@@ -1614,6 +1740,7 @@ let rec auto_clusters
     debug_print ~depth (lazy ("goals = " ^ 
       String.concat "," (List.map string_of_int goals)));
     let classes = HExtlib.clusters (deps status) goals in
+    let classes = if top then List.rev classes else classes in
       debug_print ~depth
 	(lazy 
 	   (String.concat "\n" 
@@ -1621,21 +1748,25 @@ let rec auto_clusters
 	      (fun l -> 
 		 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
 	   classes)));
-      let status = 
+      let status,b = 
 	List.fold_left
-	  (fun status gl -> 
+	  (fun (status,b) gl -> 
 	     let status = focus_tac gl status in
 	     try 
                debug_print ~depth (lazy ("focusing on" ^ 
 			      String.concat "," (List.map string_of_int gl)));
-               auto_main flags signature cache depth status; status
-	     with Proved(status) -> NTactics.merge_tac status)
-	  status classes
-      in raise (Proved status)
+               auto_main flags signature cache depth status; assert false
+	     with 
+	       | Proved(status) -> (NTactics.merge_tac status,true)
+	       | Gaveup _ when top -> (NTactics.merge_tac status,b)
+	  )
+	  (status,false) classes
+      in if b then raise (Proved status) else raise (Gaveup IntSet.empty)
 
 and
 
-(* let rec auto_main flags signature cache status k depth = *)
+(* the goals returned upon failure are an unsatisfiable subset 
+   of the initial head goals in the stack *)
 
 auto_main flags signature (cache:cache) depth status: unit =
   debug_print ~depth (lazy "entering auto main");
@@ -1644,8 +1775,11 @@ auto_main flags signature (cache:cache) depth status: unit =
   let goals = head_goals status#stack in
   match goals with
     | [] -> raise (Proved status)
-    | _ ->
-        let branch = List.length(goals)>1 in
+    | orig::_ ->
+	let ng = List.length goals in 
+        if ng > flags.maxwidth then 
+	  (print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty))
+        else let branch = ng>1 in
 	if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
         else
 	let status = 
@@ -1677,7 +1811,9 @@ auto_main flags signature (cache:cache) depth status: unit =
 		 else depth+1, loop_cache in
                debug_print (~depth:depth') 
 		 (lazy ("Case: " ^ CicNotationPp.pp_term t));
-	       try auto_clusters flags signature loop_cache
+	       let flags' = 
+		 {flags with maxwidth = flags.maxwidth - ng +1} in 
+	       try auto_clusters flags' signature loop_cache
 		 depth' status; unsat
                with 
 		 | Proved status ->
@@ -1705,7 +1841,7 @@ auto_main flags signature (cache:cache) depth status: unit =
 		     unsat)
 	    IntSet.empty alternatives
 	in
-	  raise (Gaveup IntSet.add g unsat)
+	  raise (Gaveup IntSet.add orig unsat)
 ;;
 		 
 let int name l def = 
@@ -1714,6 +1850,8 @@ let int name l def =
 ;;
 
 let auto_tac ~params:(_univ,flags) status =
+  let oldstatus = status in
+  let status = (status:> NTacStatus.tac_status) in
   let goals = head_goals status#stack in
   let status, facts = mk_th_cache status goals in
   let unit_eq = index_local_equations status#eq_cache status in 
@@ -1730,7 +1868,7 @@ let auto_tac ~params:(_univ,flags) status =
 *)
   let depth = int "depth" flags 3 in 
   let size  = int "size" flags 10 in 
-  let width = int "width" flags (3+List.length goals) in 
+  let width = int "width" flags 4 (* (3+List.length goals)*) in 
   (* XXX fix sort *)
   let goals = List.map (fun i -> (i,P)) goals in
   let signature = () in
@@ -1754,7 +1892,7 @@ let auto_tac ~params:(_univ,flags) status =
       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;assert false
+	try auto_clusters (~top:true) flags signature cache 0 status;assert false
 	with
 	  | Gaveup _ -> up_to (x+1) y
 	  | Proved s -> 
@@ -1764,7 +1902,8 @@ let auto_tac ~params:(_univ,flags) status =
 		  | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
 		  | _ -> assert false
               in
-		s#set_stack stack
+	      let s = s#set_stack stack in
+		oldstatus#set_status s 
   in
   let s = up_to depth depth in
     print(lazy