]> matita.cs.unibo.it Git - helm.git/commitdiff
Subst was missing in perforate small (apparently, gty is not
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 12 Mar 2010 07:40:38 +0000 (07:40 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 12 Mar 2010 07:40:38 +0000 (07:40 +0000)
meta-closed).

helm/software/components/ng_tactics/nnAuto.ml

index bee8b69cc2589680464bbcc87ebb2d61bf4a0b41..ede2e856afb845b2f7205f6c70550c09f4404047 100644 (file)
 
 open Printf
 
-let debug = ref false
 let print ?(depth=0) s = 
   prerr_endline (String.make depth '\t'^Lazy.force s) 
-let debug_print ?(depth=0) s = 
-  if !debug then print ~depth s else ()
-
-let debug_do f = if !debug then f () else ()
+let noprint ?(depth=0) _ = () 
+let debug_print = noprint
 
 open Continuationals.Stack
 open NTacStatus
@@ -54,9 +51,9 @@ let menv_closure status gl =
 
 (* 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 branch status ty =  
   let status, ty, metas = saturate ~delta:0 status ty in
-  debug_print (lazy ("saturated ty :" ^ (ppterm status ty)));
+  noprint (lazy ("saturated ty :" ^ (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 *)
@@ -68,7 +65,11 @@ let is_a_fact status ty =
          | NCic.Meta(i,_) -> IntSet.add i acc
          | _ -> assert false)
       IntSet.empty metas
-  in IntSet.subset menv clos;;
+  in 
+  (* IntSet.subset menv clos *)
+  IntSet.cardinal(IntSet.diff menv clos)
+
+let is_a_fact status ty = branch status ty = 0
 
 let is_a_fact_obj s uri = 
   let obj = NCicEnvironment.get_checked_obj uri in
@@ -655,7 +656,8 @@ let init_cache ?(facts=[]) ?(under_inspection=[],[])
      unit_eq = unit_eq
     }
 
-let only signature _context candidate = 
+let only signature _context candidate = true
+(*
         (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
   let candidate_ty = 
    NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
@@ -669,17 +671,36 @@ let only signature _context candidate =
     debug_print (lazy ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[]
           ~metasenv:[] candidate ^ ": " ^ string_of_int height));
 
-  rc
+  rc *)
 ;; 
 
 let candidate_no = ref 0;;
 
 let openg_no status = List.length (head_goals status#stack)
 
+let sort_candidates status ctx candidates =
+ let _,_,metasenv,subst,_ = status#obj in
+  let branch cand =
+    let status,ct = disambiguate status ctx ("",0,cand) None in
+    let status,t = term_of_cic_term status ct ctx in
+    let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+    let res = branch status (mk_cic_term ctx ty) in
+    debug_print (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = " 
+                     ^ (string_of_int res)));
+      res
+  in 
+  let candidates = List.map (fun t -> branch t,t) candidates in
+  let candidates = 
+     List.sort (fun (a,_) (b,_) -> a - b) candidates in 
+  let candidates = List.map snd candidates in
+    debug_print (lazy ("candidates =\n" ^ (String.concat "\n" 
+       (List.map CicNotationPp.pp_term candidates))));
+    candidates
+
 let sort_new_elems l =
   List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
 
-let try_candidate ?(smart=0) flags depth status eq_cache t =
+let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
  try
   debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
   let status = 
@@ -687,31 +708,44 @@ let try_candidate ?(smart=0) flags depth status eq_cache t =
     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 
+      with Error _ as exc -> 
+        smart_apply_auto ("",0,t) eq_cache status 
+  in
+(*
   let og_no = openg_no status in 
     if (* og_no > flags.maxwidth || *)
       ((depth + 1) = flags.maxdepth && og_no <> 0) then
         (debug_print ~depth (lazy "pruned immediately"); None)
-   else
-     (incr candidate_no;
-      Some ((!candidate_no,t),status))
+    else *)
+      (* useless 
+      let status, cict = disambiguate status ctx ("",0,t) None in
+      let status,ct = term_of_cic_term status cict ctx in
+      let _,_,metasenv,subst,_ = status#obj in
+      let ty = NCicTypeChecker.typeof subst metasenv ctx ct in
+      let res = branch status (mk_cic_term ctx ty) in
+      if smart=1 && og_no > res then 
+       (print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " 
+                   ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
+        print ~depth (lazy "strange application"); None)
+      else *)
+       (incr candidate_no;
+        Some ((!candidate_no,t),status))
  with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
 ;;
 
-let sort_of metasenv ctx t =
-  let ty = NCicTypeChecker.typeof [] metasenv ctx t in
-    NCicTypeChecker.typeof [] metasenv ctx ty
+let sort_of subst metasenv ctx t =
+  let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+    NCicTypeChecker.typeof subst metasenv ctx ty
 ;;
   
 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
 ;;
 
-let perforate_small metasenv context t =
+let perforate_small subst metasenv context t =
   let rec aux = function
     | NCic.Appl (hd::tl) ->
        let map t =
-         let s = sort_of metasenv context t in
+         let s = sort_of subst metasenv context t in
            match s with
              | NCic.Sort(NCic.Type [`Type,u])
                  when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
@@ -733,23 +767,25 @@ let get_candidates ?(smart=true) status cache signature gty =
   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 raw_gty = NCicUntrusted.apply_subst subst context raw_gty in *)
   let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables 
-        universe raw_gty in
+        universe raw_gty in 
   let local_cands = search_in_th gty cache in
   debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty));
   debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands)))));
-  let together global local =
+  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 candidates = together cands local_cands in 
+  let candidates = sort_candidates status context candidates in
   let smart_candidates = 
     if smart then
       match raw_gty with
-        | NCic.Appl _ -> 
-            let weak_gty = perforate_small metasenv context raw_gty in
+        | NCic.Appl _ 
+        | NCic.Const _ 
+        | NCic.Rel _ -> 
+            let weak_gty = perforate_small subst metasenv context raw_gty in
              (*
               NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0))) 
                            (List.length tl)) in *)
@@ -762,11 +798,15 @@ let get_candidates ?(smart=true) status cache signature gty =
             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  
+              together smart_cands smart_local_cands 
+              (* together more_cands more_local_cands *) 
         | _ -> []
     else [] 
   in
-    candidates, smart_candidates
+  let smart_candidates = sort_candidates status context smart_candidates in
+  (* if smart then smart_candidates, []
+     else candidates, [] *)
+  candidates, smart_candidates
 ;;
 
 let applicative_case depth signature status flags gty (cache:cache) =
@@ -807,7 +847,7 @@ let applicative_case depth signature status flags gty (cache:cache) =
            then (debug_print (lazy "pruned: not a fact"); elems)
          else
            match try_candidate (~smart:sm) 
-             flags depth status cache.unit_eq cand with
+             flags depth status cache.unit_eq context cand with
                | None -> elems
                | Some x -> x::elems)
       [] candidates
@@ -824,7 +864,7 @@ let applicative_case depth signature status flags gty (cache:cache) =
            then (debug_print (lazy "pruned: not a fact"); elems)
          else
            match try_candidate (~smart:1) 
-             flags depth status cache.unit_eq cand with
+             flags depth status cache.unit_eq context cand with
                | None -> elems
                | Some x -> x::elems)
         [] smart_candidates
@@ -963,7 +1003,8 @@ let do_something signature flags status g depth gty cache =
   (* states in l1 have have an empty set of subgoals: no point to sort them *)
   debug_print ~depth 
     (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
-    l1 @ (sort_new_elems (l @ l2)), cache
+    (* l1 @ (sort_new_elems (l @ l2)), cache *)
+    l1 @ (List.rev l2) @ l, cache 
 ;;
 
 let pp_goal = function
@@ -1067,21 +1108,33 @@ let deep_focus_tac level focus status =
    status#set_stack gstatus
 ;;
 
-let open_goals level status =
-  let rec aux level gs = 
-    if level = 0 then []
-    else match gs with 
-      | [] -> assert false
-      | (g, _, _, _) :: s -> 
-          let is_open = function
-           | (_,Continuationals.Stack.Open i) -> Some i
-           | (_,Continuationals.Stack.Closed _) -> None
-          in
-           HExtlib.filter_map is_open g @ aux (level-1) s
-  in
-  aux level status#stack
+let rec stack_goals level gs = 
+  if level = 0 then []
+  else match gs with 
+    | [] -> assert false
+    | (g,_,_,_)::s -> 
+        let is_open = function
+          | (_,Continuationals.Stack.Open i) -> Some i
+          | (_,Continuationals.Stack.Closed _) -> None
+        in
+         HExtlib.filter_map is_open g @ stack_goals (level-1) s
+;;
+
+let open_goals level status = stack_goals level status#stack
 ;;
 
+let move_to_side level status =
+match status#stack with
+  | [] -> assert false
+  | (g,_,_,_)::tl ->
+      let is_open = function
+          | (_,Continuationals.Stack.Open i) -> Some i
+          | (_,Continuationals.Stack.Closed _) -> None
+        in 
+      let others = menv_closure status (stack_goals (level-1) tl) in
+      List.for_all (fun i -> IntSet.mem i others) 
+       (HExtlib.filter_map is_open g)
+
 let rec auto_clusters ?(top=false)  
     flags signature cache depth status : unit =
   debug_print ~depth (lazy ("entering auto clusters at depth " ^
@@ -1104,7 +1157,7 @@ let rec auto_clusters ?(top=false)
     List.iter 
        (fun gl ->
           if List.length gl > flags.maxwidth then 
-            (debug_print (lazy "FAIL GLOBAL WIDTH"); 
+            (debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); 
              raise (Gaveup IntSet.empty))
           else ()) classes;
     if List.length classes = 1 then
@@ -1170,13 +1223,20 @@ auto_main flags signature (cache:cache) depth status: unit =
              | a::tl -> let tree = rm_from_th a tree a in
                  {cache with under_inspection = tl,tree} 
        in 
-         auto_clusters flags signature (cache:cache) (depth-1) status
+         auto_clusters flags signature cache (depth-1) status
     | orig::_ ->
+       if depth > 0 && move_to_side depth status
+       then 
+         let _ = print (lazy "merged") in
+         let status = NTactics.merge_tac status in
+           auto_clusters flags signature cache (depth-1) status 
+       else
         let ng = List.length goals in
         (* moved inside auto_clusters *)
         if ng > flags.maxwidth then 
-          (debug_print (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty))
-        else if depth = flags.maxdepth then raise (Gaveup IntSet.empty) 
+          (print ~depth (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty))
+        else if depth = flags.maxdepth then 
+         raise (Gaveup IntSet.empty)
         else 
         let status = NTactics.branch_tac ~force:true status in
         let status, cache = intros ~depth status cache in
@@ -1214,7 +1274,7 @@ auto_main flags signature (cache:cache) depth status: unit =
             with Gaveup _ ->
               debug_print ~depth (lazy "Failed");())
          alternatives;
-       raise (Gaveup IntSet.empty)
+       raise (debug_print(lazy "no more candidates"); Gaveup IntSet.empty)
 ;;
 
 let int name l def =