Commented an assertion.

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

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index b229cc05fc2102c396ab87af6de2e51a747022bb..1d798f9dc1a7d8b88867a5bc9fa6bb908a636405 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -202,7 +202,7 @@ let build_ens uri termlist =
   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
   match obj with
   | Cic.Constant (_, _, _, uris, _) ->
-      assert (List.length uris <= List.length termlist);
+      (* assert (List.length uris <= List.length termlist); *)
       let rec aux = function
         | [], tl -> [], tl
         | (uri::uris), (term::tl) ->
@@ -372,7 +372,8 @@ let contextualize uri ty left right t =
    * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
    * ctx_ty is the type of ctx
    *)
-    let rec aux uri ty left right ctx_d ctx_ty = function
+    let rec aux uri ty left right ctx_d ctx_ty t =
+      match t with 
       | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) 
         when LibraryObjects.is_sym_eq_URI uri_sym  ->
           let ty,l,r,p = open_sym ens tl in
@@ -407,8 +408,8 @@ let contextualize uri ty left right t =
           let c_what = put_in_ctx ctx_c what in
           (* now put the proofs in the compound context *)
           let p1 = (* p1: dc_what = d_m *)
-            if is_not_fixed_lp then 
-              aux uri ty2 c_what m ctx_d ctx_ty p1 
+            if is_not_fixed_lp then
+              aux uri ty2 c_what m ctx_d ctx_ty p1
             else
               mk_sym uri_sym ctx_ty d_m dc_what
                 (aux uri ty2 m c_what ctx_d ctx_ty p1)
@@ -417,7 +418,7 @@ let contextualize uri ty left right t =
             if avoid_eq_ind then
               mk_sym uri_sym ctx_ty dc_what dc_other
                 (aux uri ty1 what other ctx_dc ctx_ty p2)
-            else
+             else
               aux uri ty1 other what ctx_dc ctx_ty p2
           in
           (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
@@ -496,7 +497,7 @@ let build_proof_step eq lift subst p1 p2 pos l r pred =
     p
 ;;
 
-let parametrize_proof p l r ty = 
+let parametrize_proof menv p l r ty = 
   let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in
   let mot = CicUtil.metas_of_term_set in
   let parameters = uniq (mot p @ mot l @ mot r) in 
@@ -517,9 +518,21 @@ let parametrize_proof 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 args, proof,_ = 
     List.fold_left 
@@ -729,7 +742,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 cic l r (CicSubstitution.lift n mty)
+          parametrize_proof menv cic l r (CicSubstitution.lift n mty)
         in
         let h = (id, instance)::lift_list h in
         acc@[id,real_cic],n+1,h) 
@@ -858,10 +871,11 @@ exception NotMetaConvertible;;
 
 let meta_convertibility_aux table t1 t2 =
   let module C = Cic in
-  let rec aux ((table_l, table_r) as table) t1 t2 =
+  let rec aux ((table_l,table_r) as table) t1 t2 =
     match t1, t2 with
+    | C.Meta (m1, tl1), C.Meta (m2, tl2) when m1 = m2 -> table
+    | C.Meta (m1, tl1), C.Meta (m2, tl2) when m1 < m2 -> aux table t2 t1
     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
-        let tl1, tl2 = [],[] in
         let m1_binding, table_l =
           try List.assoc m1 table_l, table_l
           with Not_found -> m2, (m1, m2)::table_l
@@ -871,18 +885,7 @@ let meta_convertibility_aux table t1 t2 =
         in
         if (m1_binding <> m2) || (m2_binding <> m1) then
           raise NotMetaConvertible
-        else (
-          try
-            List.fold_left2
-              (fun res t1 t2 ->
-                 match t1, t2 with
-                 | None, Some _ | Some _, None -> raise NotMetaConvertible
-                 | None, None -> res
-                 | Some t1, Some t2 -> (aux res t1 t2))
-              (table_l, table_r) tl1 tl2
-          with Invalid_argument _ ->
-            raise NotMetaConvertible
-        )
+        else table_l,table_r
     | C.Var (u1, ens1), C.Var (u2, ens2)
     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
         aux_ens table ens1 ens2
@@ -958,12 +961,12 @@ let meta_convertibility_eq eq1 eq2 =
     true
   else
     try
-      let table = meta_convertibility_aux ([], []) left left' in
+      let table = meta_convertibility_aux ([],[]) left left' in
       let _ = meta_convertibility_aux table right right' in
       true
     with NotMetaConvertible ->
       try
-        let table = meta_convertibility_aux ([], []) left right' in
+        let table = meta_convertibility_aux ([],[]) left right' in
         let _ = meta_convertibility_aux table right left' in
         true
       with NotMetaConvertible ->
@@ -976,7 +979,7 @@ let meta_convertibility t1 t2 =
     true
   else
     try
-      ignore(meta_convertibility_aux ([], []) t1 t2);
+      ignore(meta_convertibility_aux ([],[]) t1 t2);
       true
     with NotMetaConvertible ->
       false
@@ -1006,14 +1009,16 @@ let equality_of_term bag proof term =
 
 let is_weak_identity eq = 
   let _,_,(_,left, right,_),_,_ = open_equality eq in
-  left = right || meta_convertibility left right 
+   left = right 
+   (* doing metaconv here is meaningless *)
 ;;
 
 let is_identity (_, context, ugraph) eq = 
   let _,_,(ty,left,right,_),menv,_ = open_equality eq in
-  left = right ||
-  (* (meta_convertibility left right)) *)
-  fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+  (* doing metaconv here is meaningless *)
+  left = right
+(*   fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+ *   *)
 ;;