cicDischarge: new module for discharging the explicit variables occurring in a

[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 30138b378f9eac358305f3ffbcc4170e05de44c7..bfbab9c3ec43c878a9f4f08be05dbeab1f26acd0 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -323,8 +323,8 @@ Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ "
                   remove_refl p1
               | _ -> Cic.Appl (List.map remove_refl args))
     | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
-    | Cic.LetIn (name,bo,rest) ->
-        Cic.LetIn (name,remove_refl bo,remove_refl rest)
+    | Cic.LetIn (name,bo,ty,rest) ->
+        Cic.LetIn (name,remove_refl bo,remove_refl ty,remove_refl rest)
     | _ -> t
   in
   let rec canonical_trough_lambda context = function
@@ -335,10 +335,11 @@ Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ "
 
   and canonical context t =
     match t with
-      | Cic.LetIn(name,bo,rest) -> 
+      | Cic.LetIn(name,bo,ty,rest) -> 
           let bo = canonical_trough_lambda context bo in
-          let context' = (Some (name,Cic.Def (bo,None)))::context in
-          Cic.LetIn(name,bo,canonical context' rest)
+          let ty = canonical_trough_lambda context ty in
+          let context' = (Some (name,Cic.Def (bo,ty)))::context in
+          Cic.LetIn(name,bo,ty,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
@@ -430,8 +431,10 @@ let contextualize uri ty left right t =
         when LibraryObjects.is_sym_eq_URI uri_sym  ->
           let ty,l,r,p = open_sym ens tl in
           mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p)
-      | Cic.LetIn (name,body,rest) ->
-          Cic.LetIn (name,look_ahead (aux uri) body, aux uri ty left right ctx_d ctx_ty rest)
+      | Cic.LetIn (name,body,bodyty,rest) ->
+         Cic.LetIn
+          (name,look_ahead (aux uri) body, bodyty,
+           aux uri ty left right ctx_d ctx_ty rest)
       | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
         when LibraryObjects.is_eq_ind_URI uri_ind || 
              LibraryObjects.is_eq_ind_r_URI uri_ind ->
@@ -800,6 +803,9 @@ let build_goal_proof bag eq l initial ty se context menv =
         acc@[id,real_cic],n+1,h) 
       ([],0,[]) lets
   in
+  let lets =
+   List.map (fun (id,cic) -> id,cic,Cic.Implicit (Some `Type)) lets
+  in
   let proof,se = 
     let rec aux se current_proof = function
       | [] -> current_proof,se
@@ -830,11 +836,13 @@ let build_goal_proof bag eq l initial ty se context menv =
   let n,proof = 
     let initial = proof in
     List.fold_right
-      (fun (id,cic) (n,p) -> 
+      (fun (id,cic,ty) (n,p) -> 
         n-1,
         Cic.LetIn (
           Cic.Name ("H"^string_of_int id),
-          cic, p))
+          cic,
+          ty,
+          p))
     lets (letsno-1,initial)
   in
    canonical 
@@ -944,9 +952,12 @@ let meta_convertibility_aux table t1 t2 =
         aux_ens table ens1 ens2
     | C.Cast (s1, t1), C.Cast (s2, t2)
     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
-    | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
-    | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
+    | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) ->
+        let table = aux table s1 s2 in
+        aux table t1 t2
+    | C.LetIn (_, s1, ty1, t1), C.LetIn (_, s2, ty2, t2) ->
         let table = aux table s1 s2 in
+        let table = aux table ty1 ty2 in
         aux table t1 t2
     | C.Appl l1, C.Appl l2 -> (
         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
@@ -1026,7 +1037,6 @@ let meta_convertibility_eq eq1 eq2 =
         false
 ;;
 
-
 let meta_convertibility t1 t2 =
   if t1 = t2 then
     true
@@ -1038,6 +1048,32 @@ let meta_convertibility t1 t2 =
       false
 ;;
 
+let meta_convertibility_subst t1 t2 menv =
+  if t1 = t2 then
+    Some([])
+  else
+    try
+      let (l,_) = meta_convertibility_aux ([],[]) t1 t2 in
+      let subst =
+       List.map
+         (fun (x,y) ->
+            try 
+              let (_,c,t) = CicUtil.lookup_meta x menv in
+              let irl = 
+                CicMkImplicit.identity_relocation_list_for_metavariable c in
+              (y,(c,Cic.Meta(x,irl),t))
+            with CicUtil.Meta_not_found _ ->
+              try 
+                let (_,c,t) = CicUtil.lookup_meta y menv in
+                let irl =  
+                  CicMkImplicit.identity_relocation_list_for_metavariable c in
+                  (x,(c,Cic.Meta(y,irl),t))
+              with CicUtil.Meta_not_found _ -> assert false) l in   
+       Some subst
+    with NotMetaConvertible ->
+      None
+;;
+
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
@@ -1176,7 +1212,7 @@ let rec pp_proofterm name t context =
     | _ -> assert false
   in
   let rec skip_letin ctx = function
-    | Cic.LetIn (n,b,t) -> 
+    | Cic.LetIn (n,b,_,t) -> 
         pp_proofterm (Some (rename "Lemma " n)) b ctx:: 
           skip_letin ((Some n)::ctx) t
     | t -> 
@@ -1198,7 +1234,7 @@ let rec pp_proofterm name t context =
               when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)->
                 pp true p
           | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] 
-              when Pcre.pmatch ~pat:"eq_f1" (UriManager.string_of_uri uri)->
+              when Pcre.pmatch ~pat:"eq_OF_eq" (UriManager.string_of_uri uri)->
                 pp true p
           | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] 
               when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)->