X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=07d08345c3a7f0f10dc0469466bf0ff2e198baf4;hb=21ee96d317a4f0e7abfe76f697defe78acc10b94;hp=a2a76d4f51075676f331782b79eaae0344b3d642;hpb=dce1bca274f93a3bddcc0f6b04cbf126ccff42b0;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index a2a76d4f5..07d08345c 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -14,9 +14,9 @@ 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= debug_print 
-(* let print ?(depth=0) s = 
-  prerr_endline (String.make depth '\t'^Lazy.force 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,7 +53,7 @@ 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
@@ -83,7 +83,6 @@ let current_goal status =
     open_goal, ctx, gty
 
 
-
 (* =============================== paramod =========================== *)
 let auto_paramod ~params:(l,_) status goal =
   let gty = get_goalty status goal in
@@ -103,7 +102,7 @@ let auto_paramod ~params:(l,_) status goal =
     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
   with
   | [] -> raise (Error (lazy "no proof found",None))
-  | (pt, metasenv, subst)::_ -> 
+  | (pt, _, metasenv, subst)::_ -> 
       let status = status#set_obj (n,h,metasenv,subst,o) in
       instantiate status goal (mk_cic_term (ctx_of gty) pt)
 ;;
@@ -113,18 +112,26 @@ let auto_paramod_tac ~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)
+  let gname, ctx, gty = List.assoc goal metasenv in
+  let gty = NCicUntrusted.apply_subst subst ctx gty in
+  let build_status (pt, _, metasenv, subst) =
+    (* let stamp = Unix.gettimeofday () in *)
+    let metasenv, subst, pt, pty = 
+      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
+	status#set_obj (n,h,metasenv,subst,o)
   in
     List.map build_status
       (NCicParamod.fast_eq_check status metasenv subst ctx 
-	 eq_cache (NCic.Rel ~-1,t))
+	 eq_cache (NCic.Rel ~-1,gty))
 ;;
 
 let fast_eq_check eq_cache status goal =
@@ -133,19 +140,44 @@ let fast_eq_check eq_cache status goal =
   | 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 fast_eq_check_tac_all  ~params eq_cache status = 
   let g,_,_ = current_goal status in
@@ -1179,6 +1211,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 **************)
 
 
@@ -1322,10 +1395,12 @@ 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 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 status = 
+    smart_apply_auto ("",0,t) eq_cache status in 
+ (* let status = NTactics.apply_tac ("",0,t) status in *)
    let og_no = openg_no status in 
    if og_no > flags.maxwidth || 
       (depth = flags.maxdepth && og_no <> 0) then
@@ -1363,7 +1438,7 @@ let applicative_case depth signature status flags gty (cache:cache) =
   let elems = 
     List.fold_left 
       (fun elems cand ->
-        match try_candidate flags depth status cand with
+        match try_candidate flags depth status cache.unit_eq cand with
         | None -> elems
         | Some x -> x::elems)
       [] candidates
@@ -1416,28 +1491,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
-             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 rec guess_name name ctx = 
   if name = "_" then guess_name "auto" ctx else
   if not (List.mem_assoc name ctx) then name else