Removed the context from the metasenv to avoid trivial typing errors (lists

with different lengths).

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 4745fecc2e5a971bfe53d90510422c4a164d227d..7d981cf316f92611101631e01dceec5e522e7557 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -905,6 +905,7 @@ let rec betaexpand_term
          CicTypeChecker.type_of_aux' metasenv context term ugraph 
       in
       let candidates = get_candidates Unification table term in
+      (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
       let r = 
         if subterms_only then 
           [] 
@@ -1176,17 +1177,13 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
       prerr_endline (string_of_int (List.length expansionsl));
       prerr_endline (string_of_int (List.length expansionsr));
       *)
-(*
-      if expansionsl <> [] then prerr_endline "expansionl";
-      if expansionsr <> [] then prerr_endline "expansionr";
-*)
       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
       @
       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
       end
     else
         match c with 
-        | Utils.Gt -> (* prerr_endline "GT"; *) 
+        | Utils.Gt -> 
             let big,small,possmall = l,r,Utils.Right in
             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
             List.map 

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 5fa1dafeb288c537e1d67a98d2b7ebd6ec6880b1..aed51e35bd2d66bd1b3c44289d75d229f50538ae 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -777,7 +777,7 @@ let simplify_equalities bag eq_uri env equalities =
        (Printf.sprintf "equalities:\n%s\n"
           (String.concat "\n"
              (List.map Equality.string_of_equality equalities))));
-  Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
+Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
   match equalities with
     | [] -> []
     | hd::tl ->
@@ -939,17 +939,16 @@ let infer_goal_set bag env active goals =
     | [] -> active_goals, []
     | hd::tl ->
         let changed,selected = simplify_goal bag env hd active in
-(*
-        if changed then
-          prerr_endline ("--------------- goal semplificato");
-*)
         let (_,_,t1) = selected in
+        (* 
+        if changed && Utils.debug then
+          prerr_endline ("goal semplificato: " ^  CicPp.ppterm t1); *)
         let already_in = 
           List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) 
               active_goals
         in
         if already_in then 
-             aux tl
+             aux tl 
           else
             let passive_goals = tl in
             let new_passive_goals =
@@ -1441,7 +1440,6 @@ let build_proof
       (* replacing fake mets with real ones *)
       (* prerr_endline "replacing metas..."; *)
       let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
-      if proof_menv = [] then prerr_endline "VUOTA";
       CicMetaSubst.ppmetasenv [] proof_menv;
       let what, with_what = 
         List.fold_left 
@@ -1490,7 +1488,6 @@ let build_proof
           ~where:type_of_goal
       in
       let goal_proof,goal_ty,real_menv,_ = 
-        prerr_endline "parte la refine";
         try
           CicRefine.type_of_aux' metasenv context goal_proof
             CicUniv.empty_ugraph
@@ -1664,7 +1661,10 @@ let given_clause
     List.partition (fun (_,c,_) -> c = context)  metasenv in
   (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));  *)
   Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
-  let canonical_menv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv 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) canonical_menv in
   let goal = [], metasenv', cleaned_goal in
   let env = metasenv,context,CicUniv.empty_ugraph in

diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml
index a85ccc674220482c782598f26d1d1d1e8e4b9394..86c9c1430105e0948c4ba3274284b9b9b03caded 100644 (file)
--- a/helm/software/components/tactics/paramodulation/utils.ml
+++ b/helm/software/components/tactics/paramodulation/utils.ml
@@ -114,6 +114,8 @@ let rec remove_local_context =
     | Cic.Meta (i,_) -> Cic.Meta (i,[])
     | Cic.Appl l ->
        Cic.Appl(List.map remove_local_context l)
+    | Cic.Prod (n,s,t) -> 
+       Cic.Prod (n,remove_local_context s, remove_local_context t)
     | t -> t