*** empty log message ***

[helm.git] / helm / ocaml / paramodulation / inference.ml

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 999666bca4652602566c3043c2cf4d967c8b4933..4d56d30e963d9f0dcf5b8a55aac923fe21a4a6c6 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -292,7 +292,31 @@ let rec restore_subst (* context *) subst =
     subst
 ;;
 
-      
+
+exception MatchingFailure;;
+
+let matching metasenv context t1 t2 ugraph =
+  try
+    let subst, metasenv, ugraph =
+      CicUnification.fo_unif metasenv context t1 t2 ugraph
+    in
+    let t' = CicMetaSubst.apply_subst subst t1 in
+    if not (meta_convertibility t1 t') then
+      raise MatchingFailure
+    else
+      let metas = metas_of_term t1 in
+      let fix_subst = function
+        | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
+            (j, (c, Cic.Meta (i, lc), ty))
+        | s -> s
+      in
+      let subst = List.map fix_subst subst in
+      subst, metasenv, ugraph
+  with e ->
+    raise MatchingFailure
+;;
+
+
 let beta_expand ?(metas_ok=true) ?(match_only=false)
     what type_of_what where context metasenv ugraph = 
   let module S = CicSubstitution in
@@ -559,47 +583,33 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
             let subst', metasenv', ugraph' =
 (*               Printf.printf "provo a unificare %s e %s\n" *)
 (*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
-              CicUnification.fo_unif metasenv context
-                (S.lift lift_amount what) term ugraph
+              if match_only then
+                matching metasenv context term (S.lift lift_amount what)ugraph
+              else
+                CicUnification.fo_unif metasenv context
+                  (S.lift lift_amount what) term ugraph
             in
 (*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
 (*             (CicPp.ppterm (S.lift lift_amount what)); *)
 (*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
 (*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
             (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
-            if match_only then
-              let t' = CicMetaSubst.apply_subst subst' term in
-              if not (meta_convertibility term t') then (
-(*                 if print_info then ( *)
-(*                   let names = names_of_context context in *)
-(*                   Printf.printf *)
-(*                     "\nbeta_expand: term e t' sono diversi!:\n%s\n%s\n\n" *)
-(*                     (CicPp.pp term names) (CicPp.pp t' names) *)
-(*                 ); *)
-                res, lifted_term
-              ) else (
-                let metas = metas_of_term term in
-(*                 let ok = ref false in *)
-                let fix_subst = function
-                  | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas ->
-(*                       Printf.printf "fix_subst: scambio ?%d e ?%d\n" i j; *)
-(*                       ok := true; *)
-                      (j, (c, C.Meta (i, lc), ty))
-                  | s -> s
-                in
-                let subst' = List.map fix_subst subst' in
-(*                 if !ok then ( *)
-(*                   Printf.printf "aaa:\nterm: %s\nt'%s\n term subst': %s\n" *)
-(*                     (CicPp.ppterm term) *)
-(*                     (CicPp.ppterm t') *)
-(*                     (CicPp.ppterm (CicMetaSubst.apply_subst subst' term)) *)
-(*                 ); *)
-                ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
-                 lifted_term)
-              )
-(*               ((C.Rel (1 + lift_amount), restore_subst context subst', *)
-(*                 metasenv', ugraph')::res, lifted_term) *)
-            else
+(*             if match_only then *)
+(*               let t' = CicMetaSubst.apply_subst subst' term in *)
+(*               if not (meta_convertibility term t') then ( *)
+(*                 res, lifted_term *)
+(*               ) else ( *)
+(*                 let metas = metas_of_term term in *)
+(*                 let fix_subst = function *)
+(*                   | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
+(*                       (j, (c, C.Meta (i, lc), ty)) *)
+(*                   | s -> s *)
+(*                 in *)
+(*                 let subst' = List.map fix_subst subst' in *)
+(*                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
+(*                  lifted_term) *)
+(*               ) *)
+(*             else *)
               ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
                lifted_term)
           with e ->
@@ -1144,3 +1154,53 @@ let demodulation newmeta env target source =
 *)
 
 
+let subsumption env target source =
+  let _, (ty, tl, tr), tmetas, _ = target
+  and _, (ty', sl, sr), smetas, _ = source in
+  if ty <> ty' then
+    false
+  else
+    let metasenv, context, ugraph = env in
+    let metasenv = metasenv @ tmetas @ smetas in
+    let names = names_of_context context in
+    let samesubst subst subst' =
+(*       Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
+(*         (print_subst subst) (print_subst subst'); *)
+(*       print_newline (); *)
+      let tbl = Hashtbl.create (List.length subst) in
+      List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
+      List.for_all
+        (fun (m, (c, t1, t2)) ->
+           try
+             let c', t1', t2' = Hashtbl.find tbl m in
+             if (c = c') && (t1 = t1') && (t2 = t2') then true
+             else false
+           with Not_found ->
+             true)
+        subst'
+    in
+    let subsaux left right left' right' =
+      try
+        let subst, menv, ug = matching metasenv context left left' ugraph
+        and subst', menv', ug' = matching metasenv context right right' ugraph
+        in
+(*         Printf.printf "left = right: %s = %s\n" *)
+(*           (CicPp.pp left names) (CicPp.pp right names); *)
+(*         Printf.printf "left' = right': %s = %s\n" *)
+(*           (CicPp.pp left' names) (CicPp.pp right' names);         *)
+        samesubst subst subst'
+      with e ->
+(*         print_endline (Printexc.to_string e); *)
+        false
+    in
+    let res = 
+      if subsaux tl tr sl sr then true
+      else subsaux tl tr sr sl
+    in
+    if res then (
+      Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
+        (string_of_equality ~env target) (string_of_equality ~env source);
+      print_newline ();
+    );
+    res
+;;