reverted a commented substitution in build_newgoal, added an euristic to

order the lambdas of a proof abstracted in a letin such that dependency betwwen the types of the lambdas is inferrable by the refiner

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 7f093e3f88085e9c3505ed66a25f3d3278fab1f4..1bc87f8c54fd6e235b903a405e6422b7486ba62e 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -96,8 +96,8 @@ let string_of_equality ?env eq =
               id w (CicPp.ppterm ty)
               (CicPp.ppterm left) 
               (Utils.string_of_comparison o) (CicPp.ppterm right)
-(*         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *)
-         "..." 
+         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) 
+(*          "..."  *)
   | Some (_, context, _) -> 
       let names = Utils.names_of_context context in
       let w, _, (ty, left, right, o), m , id = open_equality eq in
@@ -105,8 +105,8 @@ let string_of_equality ?env eq =
               id w (CicPp.pp ty names)
               (CicPp.pp left names) (Utils.string_of_comparison o)
               (CicPp.pp right names)
-(*         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *)
-           "..."
+         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) 
+(*            "..." *)
 ;;
 
 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
@@ -327,11 +327,18 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
         Cic.LetIn (name,remove_refl bo,remove_refl rest)
     | _ -> t
   in
-  let rec canonical context t =
+  let rec canonical_trough_lambda context = function
+    | Cic.Lambda(name,ty,bo) -> 
+        let context' = (Some (name,Cic.Decl ty))::context in
+        Cic.Lambda(name,ty,canonical_trough_lambda context' bo)
+    | t -> canonical context t
+
+  and canonical context t =
     match t with
       | Cic.LetIn(name,bo,rest) -> 
+          let bo = canonical_trough_lambda context bo in
           let context' = (Some (name,Cic.Def (bo,None)))::context in
-          Cic.LetIn(name,canonical context bo,canonical context' rest)
+          Cic.LetIn(name,bo,canonical context' rest)
       | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
           when LibraryObjects.is_sym_eq_URI uri_sym ->
           (match p_of_sym ens tl with
@@ -344,12 +351,15 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
                    mk_trans uri_trans ty r m l 
                      (canonical context (mk_sym uri_sym ty m r p2)) 
                      (canonical context (mk_sym uri_sym ty l m p1))
-             | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p])) ->
+             | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p]))
+                 when LibraryObjects.is_eq_f_URI uri_feq ->
                  let eq = LibraryObjects.eq_URI_of_eq_f_URI uri_feq in
                  let eq_f_sym =
                    Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, [])
                  in
-                 Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p]))  
+                 let rc = Cic.Appl [eq_f_sym;ty1;ty2;f;x;y;p] in
+                 prerr_endline ("CANONICAL " ^ CicPp.ppterm rc);
+                 rc
              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
                  when LibraryObjects.is_eq_URI uri -> t
              | _ -> Cic.Appl (List.map (canonical context) args))
@@ -539,8 +549,8 @@ let build_proof_step eq lift subst p1 p2 pos l r pred =
     p
 ;;
 
-let parametrize_proof menv p l r ty = 
-  let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in
+let parametrize_proof p l r = 
+  let uniq l = HExtlib.list_uniq (List.sort (fun (i,_) (j,_) -> Pervasives.compare i j) l) in
   let mot = CicUtil.metas_of_term_set in
   let parameters = uniq (mot p @ mot l @ mot r) in 
   (* ?if they are under a lambda? *)
@@ -549,6 +559,21 @@ let parametrize_proof menv p l r ty =
     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
   in
 *)
+  (* resorts l such that *hopefully* dependencies can be inferred *)
+  let guess_dependency p l =
+    match p with
+    | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) 
+        when LibraryObjects.is_eq_ind_URI uri_ind || 
+             LibraryObjects.is_eq_ind_r_URI uri_ind ->
+        let ty,_,_,_,_,_ = open_eq_ind tl in
+        let metas = CicUtil.metas_of_term ty in
+        let nondep, dep = 
+          List.partition (fun (i,_) -> List.exists (fun (j,_) -> j=i) metas) l
+        in
+        nondep@dep
+    | _ -> l
+  in
+  let parameters = guess_dependency p parameters in
   let what = List.map (fun (i,l) -> Cic.Meta (i,l)) parameters in 
   let with_what, lift_no = 
     List.fold_right (fun _ (acc,n) -> ((Cic.Rel n)::acc),n+1) what ([],1) 
@@ -560,22 +585,7 @@ let parametrize_proof menv p l r ty =
       match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) 
     ~what ~with_what ~where:p
   in
-  let ty_of_m _ = Cic.Implicit (Some `Type)
-(*
-  let ty_of_m = function
-    | Cic.Meta (i,_) ->
-       (try
-         let _,_,ty = CicUtil.lookup_meta i menv in ty
-       with CicUtil.Meta_not_found _ -> 
-         prerr_endline "eccoci";assert false)
-    | _ -> assert false
-*)
-  (*
-  let ty_of_m _ = ty (*function 
-    | Cic.Meta (i,_) -> List.assoc i menv 
-    | _ -> assert false *)
-  *)
-  in
+  let ty_of_m _ = Cic.Implicit (Some `Type) in
   let args, proof,_ = 
     List.fold_left 
       (fun (instance,p,n) m -> 
@@ -613,19 +623,19 @@ let wfo bag goalproof proof id =
 let string_of_id (id_to_eq,_) names id = 
   if id = 0 then "" else 
   try
-    let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
+    let (_,p,(t,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
     match p with
     | Exact t -> 
         Printf.sprintf "%d = %s: %s = %s [%s]" id
           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
-          "..."
-(*         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *)
-    | Step (_,(step,id1, (_,id2), _) ) ->
-        Printf.sprintf "%6d: %s %6d %6d   %s = %s [%s]" id
+(*           "..." *)
+         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) 
+    | Step (_,(step,id1, (dir,id2), p) ) ->
+        Printf.sprintf "%6d: %s %6d %6d   %s =(%s) %s [%s]" id
           (string_of_rule step)
-          id1 id2 (CicPp.pp l names) (CicPp.pp r names)
-(*         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *)
-          "..."
+          id1 id2 (CicPp.pp l names) (CicPp.pp t names) (CicPp.pp r names)
+         (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) 
+          (*"..."*)
   with
       Not_found -> assert false
 
@@ -776,7 +786,6 @@ let build_goal_proof bag eq l initial ty se context menv =
   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
   let lets = get_duplicate_step_in_wfo bag l initial in
   let letsno = List.length lets in
-  let _,mty,_,_ = open_eq ty in
   let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in
   let lets,_,h = 
     List.fold_left
@@ -784,7 +793,7 @@ let build_goal_proof bag eq l initial ty se context menv =
         let p,l,r = proof_of_id bag id in
         let cic = build_proof_term bag eq h n p in
         let real_cic,instance = 
-          parametrize_proof menv cic l r (CicSubstitution.lift n mty)
+          parametrize_proof cic l r 
         in
         let h = (id, instance)::lift_list h in
         acc@[id,real_cic],n+1,h) 
@@ -894,7 +903,8 @@ let fix_metas bag newmeta eq =
 (* List.map (fun i ,_,_ -> i) menv *)
     HExtlib.list_uniq 
       (List.sort Pervasives.compare 
-         (Utils.metas_of_term left @ Utils.metas_of_term right)) 
+         (Utils.metas_of_term left @ Utils.metas_of_term right @
+         Utils.metas_of_term ty)) 
   in
   let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in
   let ty = Subst.apply_subst subst ty in

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index b535119ed2df5702e9c8a3f2f0a99ce4d0bd7b80..e453d95c12c968a3cd696b157db950a6f87408e7 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -621,6 +621,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
     in
+    let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
       let bo = 
@@ -858,6 +859,7 @@ let superposition_right bag
       Equality.open_equality  equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
 
+    let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
     let newgoal, newproof =
       (* qua *)
       let bo' =
@@ -1003,10 +1005,8 @@ let build_newgoal bag context goal posu rule expansion =
       Utils.guarded_simpl context 
         (apply_subst subst (CicSubstitution.subst other t)) 
     in
-    let bo' = (*apply_subst subst*) t in
-    (* patch?? 
-    let bo' = t in
-    let ty = apply_subst subst ty in *)
+    let bo' = apply_subst subst t in
+    let ty = apply_subst subst ty in 
     let name = Cic.Name "x" in 
     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
     bo, (newgoalproofstep::goalproof)

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 514cd049e686e5b882af3368c6f4bbdd386daea3..30561bf07b5df933fecb0da1e3efef1be1539207 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1351,20 +1351,28 @@ let build_proof
   let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in
     (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
 *)
+  let pp_error goal_proof names error exn =
+    prerr_endline "THE PROOF DOES NOT TYPECHECK! <begin>";
+    prerr_endline (CicPp.pp goal_proof names); 
+    prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+    prerr_endline error;
+    prerr_endline "THE PROOF DOES NOT TYPECHECK! <end>";
+    raise exn
+  in
   let goal_proof,goal_ty,real_menv,_ = 
     (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
     try
+            prerr_endline (CicPp.ppterm goal_proof);
       CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
     with 
-      | CicUtil.Meta_not_found _ 
-      | CicRefine.RefineFailure _ 
-      | CicRefine.Uncertain _ 
-      | CicRefine.AssertFailure _
+      | CicRefine.RefineFailure s 
+      | CicRefine.Uncertain s 
+      | CicRefine.AssertFailure s as exn -> 
+          pp_error goal_proof names (Lazy.force s) exn
+      | CicUtil.Meta_not_found i as exn ->
+          pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn
       | Invalid_argument "list_fold_left2" as exn ->
-          prerr_endline "THE PROOF DOES NOT TYPECHECK!";
-          prerr_endline (CicPp.pp goal_proof names); 
-          prerr_endline "THE PROOF DOES NOT TYPECHECK!";
-          raise exn
+          pp_error goal_proof names "Invalid_argument: list_fold_left2" exn 
   in     
   let subst_side_effects,real_menv,_ = 
     try
@@ -1531,15 +1539,17 @@ let build_proof
 let pump_actives context bag maxm active passive saturation_steps max_time =
   reset_refs();
   maxmeta := maxm;
+(*
   let max_l l = 
     List.fold_left 
      (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
       List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
      0 l in
-  let active_l = fst active in
-  let passive_l = fst passive in
-  let ma = max_l active_l in
-  let mp = max_l passive_l in
+*)
+(*   let active_l = fst active in *)
+(*   let passive_l = fst passive in *)
+(*   let ma = max_l active_l in *)
+(*   let mp = max_l passive_l in *)
   match LibraryObjects.eq_URI () with
     | None -> active, passive, !maxmeta
     | Some eq_uri -> 
@@ -1591,16 +1601,18 @@ let given_clause
 =
   reset_refs();
   maxmeta := maxm;
+  let active_l = fst active in
+(*
   let max_l l = 
     List.fold_left 
      (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
       List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
      0 l
   in
-  let active_l = fst active in
   let passive_l = fst passive in
   let ma = max_l active_l in
   let mp = max_l passive_l in
+*)
   let proof, goalno = status in
   let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in