X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=5fa1dafeb288c537e1d67a98d2b7ebd6ec6880b1;hb=3e51297756e2c2422db7e35ca03af7123ff2498d;hp=9739f1ccf44ac84767adc0ea018210d601e3d75f;hpb=2f4cf6f683207d7e755f8ba067f86c2f98f778fb;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 9739f1ccf..5fa1dafeb 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -125,8 +125,11 @@ let make_passive eq_list =
   let set =
     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
   in
-  (*EqualitySet.elements set*) eq_list, set (* see applys.ma *)
+  (* we have the invariant that the list and the set have the same
+   * cardinality *)
+  EqualitySet.elements set, set
 ;;
+
 let make_empty_active () = [], Indexing.empty ;;
 let make_active eq_list = 
   eq_list, List.fold_left Indexing.index Indexing.empty eq_list
@@ -134,6 +137,7 @@ let make_active eq_list =
 
 let size_of_passive (passive_list, _) = List.length passive_list;;
 let size_of_active (active_list, _) = List.length active_list;;
+
 let passive_is_empty = function
   | [], s when EqualitySet.is_empty s -> true
   | [], s -> assert false (* the set and the list should be in sync *)
@@ -711,7 +715,7 @@ let activate_theorem (active, passive) =
 ;;
 
 
-
+(*
 let simplify_theorems bag env theorems ?passive (active_list, active_table) =
   let pl, passive_table =
     match passive with
@@ -741,7 +745,7 @@ let simplify_theorems bag env theorems ?passive (active_list, active_table) =
       let p_theorems = List.map (mapfun passive_table) p_theorems in
       List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
 ;;
-
+*)
 
 let rec simpl bag eq_uri env e others others_simpl =
   let active = others @ others_simpl in
@@ -820,8 +824,8 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
          Equality.mk_equality bag
            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) 
       in
-(*      match Indexing.subsumption env table goal_equation with*)
-       match Indexing.unification env table goal_equation with 
+       match Indexing.subsumption env table goal_equation with 
+       (* match Indexing.unification env table goal_equation with *)
         | Some (subst, equality, swapped ) ->
 (*
             prerr_endline 
@@ -843,25 +847,27 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
   | _ -> None
 ;;
 
-let find_all_subsumed bag env table (goalproof,menv,ty) =
+let find_all_subsumed bag maxm env table (goalproof,menv,ty) =
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when LibraryObjects.is_eq_URI uri ->
       let goal_equation = 
-        Equality.mk_equality bag
-          (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) 
+        (Equality.mk_equality bag
+          (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv)) 
       in
-	List.map
+      List.map
 	  (fun (subst, equality, swapped ) ->
 	     let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
              let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
+             Indexing.check_for_duplicates cicmenv "from subsumption";
              let p =
 	       if swapped then
                  Equality.symmetric bag eq_ty l id uri m
 	       else
                  p
              in (goalproof, p, id, subst, cicmenv))
-	  (Indexing.unification_all env table goal_equation)
+          (Indexing.subsumption_all env table goal_equation)
+	  (* (Indexing.unification_all env table goal_equation) *)
   | _ -> assert false
 ;;
 
@@ -876,12 +882,12 @@ let check_if_goal_is_identity env = function
     (let _,context,_ = env in
     try 
      let s,m,_ = 
-       Founif.unification m m context left right CicUniv.empty_ugraph 
+       Founif.unification [] m context left right CicUniv.empty_ugraph 
      in
       let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
       let m = Subst.apply_subst_metasenv s m in
       Some (goalproof, reflproof, 0, s,m)
-    with _ -> None)
+    with CicUnification.UnificationFailure _ -> None)
   | _ -> None
 ;;                              
     
@@ -1277,10 +1283,11 @@ let fix_proof metasenv context all_implicits p =
 	  let metasenv,s = aux metasenv n s in
 	  let metasenv,t = aux metasenv (n+1) t in
 	    metasenv,Cic.Prod(name,s,t)
-      | Cic.LetIn(name,s,t) ->
+      | Cic.LetIn(name,s,ty,t) ->
 	  let metasenv,s = aux metasenv n s in
+	  let metasenv,ty = aux metasenv n ty in
 	  let metasenv,t = aux metasenv (n+1) t in
-	    metasenv,Cic.LetIn(name,s,t)	      
+	    metasenv,Cic.LetIn(name,s,ty,t)
       | Cic.Const(uri,ens) -> 
 	  let metasenv,ens =
 	    List.fold_right 
@@ -1295,15 +1302,16 @@ let fix_proof metasenv context all_implicits p =
   aux metasenv 0 p 
 ;;
 
-let fix_metasenv metasenv =
+let fix_metasenv context metasenv =
   List.fold_left 
     (fun m (i,c,t) ->
-       let m,t = fix_proof m c false t in
+       let m,t = fix_proof m context false t in
        let m = List.filter (fun (j,_,_) -> j<>i) m in
-	 (i,c,t)::m)
+	 (i,context,t)::m)
     metasenv metasenv
 ;;
 
+
 (* status: input proof status
  * goalproof: forward steps on goal
  * newproof: backward steps
@@ -1346,7 +1354,8 @@ let build_proof
   in
 (*   Equality.draw_proof bag names goalproof newproof subsumption_id; *)
   let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
-  let real_menv =  fix_metasenv (proof_menv@metasenv) in
+  (* assert (metasenv=[]); *)
+  let real_menv =  fix_metasenv context (proof_menv@metasenv) in
   let real_menv,goal_proof = 
     fix_proof real_menv context false goal_proof in
 (*
@@ -1586,6 +1595,10 @@ let all_subsumed bag maxm status active passive =
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let env = metasenv,context,CicUniv.empty_ugraph in
   let cleaned_goal = Utils.remove_local_context type_of_goal in
+  let canonical_menv,other_menv = 
+    List.partition (fun (_,c,_) -> c = context)  metasenv in
+  (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));   *)
+  let metasenv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
   debug_print (lazy (string_of_int (List.length (fst active))));
    (* we simplify using both actives passives *)
@@ -1593,21 +1606,35 @@ let all_subsumed bag maxm status active passive =
     List.fold_left 
       (fun (l,tbl) eq -> eq::l,(Indexing.index tbl eq))
       active (list_of_passive passive) in
+  let (_,_,ty) = goal in
+  debug_print (lazy ("prima " ^ CicPp.ppterm ty));
   let _,goal = simplify_goal bag env goal table in
   let (_,_,ty) = goal in
-  debug_print (lazy (CicPp.ppterm ty));
-  let subsumed = find_all_subsumed bag env (snd table) goal in
+  debug_print (lazy ("in mezzo " ^ CicPp.ppterm ty));
+  let subsumed = find_all_subsumed bag !maxmeta env (snd table) goal in
+  debug_print (lazy ("dopo " ^ CicPp.ppterm ty));
   let subsumed_or_id =
     match (check_if_goal_is_identity env goal) with
 	None -> subsumed
       | Some id -> id::subsumed in
+  debug_print (lazy "dopo subsumed");
   let res =
     List.map 
       (fun 
 	 (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
+	   let subst, proof, gl =
 	     build_proof bag
-               status goalproof newproof subsumption_id subsumption_subst proof_menv)
-      subsumed_or_id in
+               status goalproof newproof subsumption_id subsumption_subst proof_menv
+	   in
+	   let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
+           let newmetasenv = 
+             other_menv @ 
+             List.filter
+               (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
+           in
+	   let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
+	     (subst, proof,gl)) subsumed_or_id 
+  in 
   res, !maxmeta
 
 
@@ -1633,8 +1660,12 @@ let given_clause
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
   let cleaned_goal = Utils.remove_local_context type_of_goal in
+  let canonical_menv,other_menv = 
+    List.partition (fun (_,c,_) -> c = context)  metasenv in
+  (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));  *)
   Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
-  let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in
+  let canonical_menv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
+  let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in
   let goal = [], metasenv', cleaned_goal in
   let env = metasenv,context,CicUniv.empty_ugraph in
   debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
@@ -1643,7 +1674,6 @@ let given_clause
   debug_print (lazy ">>>>>>>>>>>>>>"); 
   let goals = make_goal_set goal in
   match 
-(* given_caluse non prende in input maxm ????? *)
     given_clause bag eq_uri env goals passive active 
       goal_steps saturation_steps max_time
   with
@@ -1655,9 +1685,12 @@ let given_clause
       build_proof bag
         status goalproof newproof subsumption_id subsumption_subst proof_menv
     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),a,p, !maxmeta
 ;;
 
+
 let add_to_passive eql passives = 
   add_to_passive passives eql eql
 ;;