dependences update

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index fb60178391e968425257d08ad297b0620ddeb28b..c5f3132e9aa5e5e1cb56849862f78e09175f0aed 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -298,7 +298,7 @@ let add_to_passive passive new_pos preferred =
       pos 
   in
   pos_head @ pos_list @ pos_tail, add pos_set pos,
-   List.fold_left Indexing.index pos_table new_pos
+   List.fold_left Indexing.index pos_table pos
 ;;
 
 (* TODO *)
@@ -902,8 +902,7 @@ let check_if_goals_set_is_solved bag env active passive goals =
             (fun bag -> check_if_goal_is_subsumed bag env (snd active));
             (fun bag -> check_if_goal_is_subsumed bag env (last passive))
              ])
-(* provare active and passive?*)
-    (bag,None) active_goals
+    (bag,None) (active_goals @ passive_goals)
 ;;
 
 let infer_goal_set bag env active goals = 
@@ -1196,9 +1195,15 @@ let add_to_active bag active passive env ty term newmetas =
    | Some eq_uri -> 
        try 
          let bag, current = Equality.equality_of_term bag term ty newmetas in
-         let bag, current = Equality.fix_metas bag current in
-         match add_to_active_aux bag active passive env eq_uri current with
-         | _,a,p,b -> a,p,b
+         let w,_,_,_,_ = Equality.open_equality current in
+         if w > 100 then 
+           (HLog.debug 
+             ("skipping giant " ^ CicPp.ppterm term ^ " of weight " ^
+                string_of_int w); active, passive, bag)
+         else
+          let bag, current = Equality.fix_metas bag current in
+          match add_to_active_aux bag active passive env eq_uri current with
+          | _,a,p,b -> a,p,b
        with
        | Equality.TermIsNotAnEquality -> active, passive, bag
 ;;
@@ -1654,6 +1659,77 @@ let given_clause
     Some (subst, proof,gl),a,p, b
 ;;
 
+let solve_narrowing bag status active passive goal_steps =
+  let proof, goalno = status in
+  let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
+  let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+  let cleaned_goal = Utils.remove_local_context type_of_goal in
+  let metas_occurring_in_goal = CicUtil.metas_of_term cleaned_goal in
+  let canonical_menv,other_menv = 
+    List.partition (fun (_,c,_) -> c = context)  metasenv in
+  let canonical_menv = 
+    List.map 
+     (fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv 
+  in
+  let metasenv' = 
+    List.filter 
+      (fun (i,_,_)-> i<>goalno && List.mem_assoc i metas_occurring_in_goal) 
+      canonical_menv 
+  in
+  let goal = [], metasenv', cleaned_goal in
+  let env = metasenv,context,CicUniv.empty_ugraph in
+  let goals = 
+    let table = List.fold_left Indexing.index (last passive) (fst active) in
+    goal :: Indexing.demodulation_all_goal bag env table goal 4
+  in
+  let rec aux newactives newpassives bag = function
+    | [] -> bag, (newactives, newpassives)
+    | hd::tl ->
+        let selected = hd in
+        let (_,m1,t1) = selected in
+        let already_in = 
+          List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) 
+              newactives
+        in
+        if already_in then 
+             aux newactives newpassives bag tl 
+          else
+            let bag, newpassives =
+              if Utils.metas_of_term t1 = [] then 
+                bag, newpassives
+              else 
+                let bag, new' = 
+                   Indexing.superposition_left bag env (snd active) selected
+                in
+                let new' = 
+                  List.map 
+                    (fun x -> let b, x = simplify_goal bag env x active in x)
+                    new'
+                in
+                bag, newpassives @ new'
+            in
+            aux (selected::newactives) newpassives bag tl
+  in 
+  let rec do_n bag ag pg = function
+    | 0 -> None, active, passive, bag
+    | n -> 
+        let bag, (ag, pg) = aux [] [] bag (ag @ pg) in
+        match check_if_goals_set_is_solved bag env active passive (ag,pg) with
+        | bag, None -> do_n bag ag pg (n-1)
+        | bag, Some (gproof,newproof,subsumption_id,subsumption_subst,pmenv)->
+            let subst, proof, gl =
+              build_proof bag
+                status gproof newproof subsumption_id subsumption_subst pmenv
+            in
+            let uri,metasenv,subst,meta_proof,term_to_prove,attrs = proof in
+            let proof = 
+              uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs
+            in
+            Some (subst, proof,gl),active,passive, bag
+  in
+   do_n bag [] goals goal_steps
+;;
+
 
 let add_to_passive eql passives = 
   add_to_passive passives eql eql