Behaviour of CicRefine.type_of_aux' on MutCases changed: branches are now

[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 7123c134a93a98056655f6cee83e55600b559945..7f093e3f88085e9c3505ed66a25f3d3278fab1f4 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) ->
@@ -269,6 +269,48 @@ let is_not_fixed t =
 ;;
 
 let canonical t context menv = 
+  let remove_cycles t =
+   let is_transitive =
+    function
+       Cic.Appl (Cic.Const (uri_trans,_)::_)
+        when LibraryObjects.is_trans_eq_URI uri_trans ->
+         true
+     | _ -> false in
+   let rec collect =
+    function
+       Cic.Appl (Cic.Const (uri_trans,ens)::tl)
+        when LibraryObjects.is_trans_eq_URI uri_trans ->
+         let ty,l,m,r,p1,p2 = open_trans ens tl in
+          (if is_transitive p1 then fst (collect p1) else [l,p1]) @
+           (if is_transitive p2 then fst (collect p2) else [m,p2]),
+          (r, uri_trans, ty)
+     | t -> assert false in
+   let rec cut_to_last_duplicate l acc =
+    function
+       [] -> List.rev acc
+     | (l',p)::tl when l=l' -> 
+if acc <> [] then
+prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
+         cut_to_last_duplicate l [l',p] tl
+     | (l',p)::tl ->
+         cut_to_last_duplicate l ((l',p)::acc) tl
+   in
+   let rec rebuild =
+    function
+       (l,_)::_::_ as steps, ((r,uri_trans,ty) as last) ->
+         (match cut_to_last_duplicate l [] steps with
+             (l,p1)::((m,_)::_::_ as tl) ->
+               mk_trans uri_trans ty l m r p1 (rebuild (tl,last))
+           | [l,p1 ; m,p2] -> mk_trans uri_trans ty l m r p1 p2
+           | [l,p1] -> p1
+           | [] -> assert false)
+     | _ -> assert false
+   in
+    if is_transitive t then
+     rebuild (collect t)
+    else
+     t
+  in
   let rec remove_refl t =
     match t with
     | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
@@ -314,7 +356,7 @@ let canonical t context menv =
       | Cic.Appl l -> Cic.Appl (List.map (canonical context) l)
       | _ -> t
   in
-  remove_refl (canonical context t)
+   remove_cycles (remove_refl (canonical context t))
 ;;
   
 let compose_contexts ctx1 ctx2 = 
@@ -372,7 +414,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 +450,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 +460,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 +539,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 +560,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 +784,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)