cambiato il tipo equality, aggiunto l'ordinamento tra left e right

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 4d56d30e963d9f0dcf5b8a55aac923fe21a4a6c6..00e543c2e6d182e3f0cf05b4baa12b783aef99d6 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -5,16 +5,17 @@ let string_of_equality ?env =
   match env with
   | None -> (
       function
-        | _, (ty, left, right), _, _ ->
-            Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty)
-              (CicPp.ppterm left) (CicPp.ppterm right)
+        | _, (ty, left, right, o), _, _ ->
+            Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
+              (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
     )
   | Some (_, context, _) -> (
       let names = names_of_context context in
       function
-        | _, (ty, left, right), _, _ ->
-            Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names)
-              (CicPp.pp left names) (CicPp.pp right names)
+        | _, (ty, left, right, o), _, _ ->
+            Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
+              (CicPp.pp left names) (string_of_comparison o)
+              (CicPp.pp right names)
     )
 ;;
 
@@ -160,8 +161,8 @@ let meta_convertibility_aux table t1 t2 =
 
 
 let meta_convertibility_eq eq1 eq2 =
-  let _, (ty, left, right), _, _ = eq1
-  and _, (ty', left', right'), _, _ = eq2 in
+  let _, (ty, left, right, _), _, _ = eq1
+  and _, (ty', left', right', _), _, _ = eq2 in
   if ty <> ty' then
     false
   else if (left = left') && (right = right') then
@@ -584,7 +585,7 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
 (*               Printf.printf "provo a unificare %s e %s\n" *)
 (*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
               if match_only then
-                matching metasenv context term (S.lift lift_amount what)ugraph
+                matching metasenv context term (S.lift lift_amount what) ugraph
               else
                 CicUnification.fo_unif metasenv context
                   (S.lift lift_amount what) term ugraph
@@ -677,12 +678,13 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
 
 
 type equality =
-    Cic.term  *    (* proof *)
-    (Cic.term *    (* type *)
-     Cic.term *    (* left side *)
-     Cic.term) *   (* right side *)
-    Cic.metasenv * (* environment for metas *)
-    Cic.term list  (* arguments *)
+    Cic.term  *          (* proof *)
+    (Cic.term *          (* type *)
+     Cic.term *          (* left side *)
+     Cic.term *          (* right side *)
+     Utils.comparison) * (* ordering *)  
+    Cic.metasenv *       (* environment for metas *)
+    Cic.term list        (* arguments *)
 ;;
 
 
@@ -719,12 +721,15 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
                 match head with
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
                     Printf.printf "OK: %s\n" (CicPp.ppterm term);
-                    Some (p, (ty, t1, t2), newmetas, args), (newmeta+1)
+                    let o = !Utils.compare_terms t1 t2 in
+                    Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1)
                 | _ -> None, newmeta
               )
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
-              Some (C.Rel index,
-                    (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1)
+              let t1 = S.lift index t1
+              and t2 = S.lift index t2 in
+              let o = !Utils.compare_terms t1 t2 in
+              Some (C.Rel index, (ty, t1, t2, o), [], []), (newmeta+1)
           | _ -> None, newmeta
         in (
           match do_find context term with
@@ -741,7 +746,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 ;;
 
 
-let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
+let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
   let table = Hashtbl.create (List.length args) in
   let newargs, _ =
     List.fold_right
@@ -777,7 +782,7 @@ let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
   in
   (newmeta + (List.length newargs) + 1,
-   (repl proof, (ty, left, right), menv', newargs))
+   (repl proof, (ty, left, right, o), menv', newargs))
 ;;
 
 
@@ -785,7 +790,8 @@ exception TermIsNotAnEquality;;
 
 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
-      (proof, (ty, t1, t2), [], [])
+      let o = !Utils.compare_terms t1 t2 in
+      (proof, (ty, t1, t2, o), [], [])
   | _ ->
       raise TermIsNotAnEquality
 ;;
@@ -802,8 +808,8 @@ let superposition_left (metasenv, context, ugraph) target source =
   let module CR = CicReduction in
   (* we assume that target is ground (does not contain metavariables): this
    * should always be the case (I hope, at least) *)
-  let proof, (eq_ty, left, right), _, _ = target in
-  let eqproof, (ty, t1, t2), newmetas, args = source in
+  let proof, (eq_ty, left, right, t_order), _, _ = target in
+  let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
 
   let compare_terms = !Utils.compare_terms in
 
@@ -811,7 +817,7 @@ let superposition_left (metasenv, context, ugraph) target source =
     []
   else    
     let where, is_left =
-      match compare_terms left right with
+      match t_order (* compare_terms left right *) with
       | Lt -> right, false
       | Gt -> left, true
       | _ -> (
@@ -822,7 +828,7 @@ let superposition_left (metasenv, context, ugraph) target source =
         )
     in
     let metasenv' = newmetas @ metasenv in
-    let result = compare_terms t1 t2 in
+    let result = s_order (* compare_terms t1 t2 *) in
     let res1, res2 = 
       match result with
       | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
@@ -865,10 +871,10 @@ let superposition_left (metasenv, context, ugraph) target source =
         | _ -> assert false
       in
       let equation =
-        if is_left then (eq_ty, newgoal, right)
-        else (eq_ty, left, newgoal)
+        if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
+        else (eq_ty, left, newgoal, compare_terms left newgoal)
       in
-      (eqproof, equation, [], [])
+      (newgoalproof (* eqproof *), equation, [], [])
     in
     let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
     and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
@@ -882,8 +888,8 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
-  let eqproof, (eq_ty, left, right), newmetas, args = target in
-  let eqp', (ty', t1, t2), newm', args' = source in
+  let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
+  let eqp', (ty', t1, t2, s_order), newm', args' = source in
   let maxmeta = ref newmeta in
 
   let compare_terms = !Utils.compare_terms in
@@ -909,8 +915,8 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
     in
     let metasenv' = metasenv @ newmetas @ newm' in
     let beta_expand = beta_expand ~metas_ok:false in
-    let cmp1 = compare_terms left right
-    and cmp2 = compare_terms t1 t2 in
+    let cmp1 = t_order (* compare_terms left right *)
+    and cmp2 = s_order (* compare_terms t1 t2 *) in
     let res1, res2, res3, res4 =
       let res l r s t =
         List.filter
@@ -977,8 +983,9 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
         let left, right =
           if is_left then (newterm, M.apply_subst s right)
           else (M.apply_subst s left, newterm) in
+        let neworder = compare_terms left right in
         fix_metas !maxmeta
-          (neweqproof, (eq_ty, left, right), newmetas, newargs)
+          (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
       in
       maxmeta := newmeta;
       newequality
@@ -988,15 +995,16 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
     and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
     and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
     let ok = function
-      | _, (_, left, right), _, _ ->
+      | _, (_, left, right, _), _, _ ->
           not (fst (CR.are_convertible context left right ugraph))
     in
-    !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
+    (!maxmeta,
+     (List.filter ok (new1 @ new2 @ new3 @ new4)))
 ;;
 
 
 let is_identity ((_, context, ugraph) as env) = function
-  | ((_, (ty, left, right), _, _) as equality) ->
+  | ((_, (ty, left, right, _), _, _) as equality) ->
       let res =
         (left = right ||
             (fst (CicReduction.are_convertible context left right ugraph)))
@@ -1016,8 +1024,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
 
-  let proof, (eq_ty, left, right), metas, args = target
-  and proof', (ty, t1, t2), metas', args' = source in
+  let proof, (eq_ty, left, right, t_order), metas, args = target
+  and proof', (ty, t1, t2, s_order), metas', args' = source in
 
   let compare_terms = !Utils.compare_terms in
   
@@ -1025,7 +1033,7 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
     newmeta, target
   else
     let first_step, get_params = 
-      match compare_terms t1 t2 with
+      match s_order (* compare_terms t1 t2 *) with
       | Gt -> 1, (function
                     | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
                     | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
@@ -1047,7 +1055,7 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
           first_step, get_params
     in
     let rec demodulate newmeta step metasenv target =
-      let proof, (eq_ty, left, right), metas, args = target in
+      let proof, (eq_ty, left, right, t_order), metas, args = target in
       let is_left, what, other, eq_URI = get_params step in
 
       let env = metasenv, context, ugraph in
@@ -1116,6 +1124,7 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
               if is_left then newterm, right
               else left, newterm
             in
+            let neworder = compare_terms left right in
 (*             let newmetasenv = metasenv @ metas in *)
 (*             let newargs = args @ args' in *)
 (*             fix_metas newmeta *)
@@ -1127,7 +1136,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
                 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
                 args
             in
-            newmeta, (newproof, (eq_ty, left, right), newmetasenv, newargs)
+            newmeta,
+            (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
           in
 (*           Printf.printf *)
 (*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
@@ -1155,8 +1165,8 @@ let demodulation newmeta env target source =
 
 
 let subsumption env target source =
-  let _, (ty, tl, tr), tmetas, _ = target
-  and _, (ty', sl, sr), smetas, _ = source in
+  let _, (ty, tl, tr, _), tmetas, _ = target
+  and _, (ty', sl, sr, _), smetas, _ = source in
   if ty <> ty' then
     false
   else