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

diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile
index 85668aaf9dfa2410e7183e222aecbf78f83516ea..c50c1b41f3f715f32dd3985b96fe0145074136e2 100644 (file)
--- a/helm/ocaml/paramodulation/Makefile
+++ b/helm/ocaml/paramodulation/Makefile
@@ -5,9 +5,9 @@ TEST_REQUIRES = \
        helm-tactics \
        helm-cic_transformations \
        helm-cic_textual_parser2 \
-       helm-mathql_interpreter \
-       helm-mathql_generator \
-       helm-xmldiff 
+#      helm-mathql_interpreter \
+#      helm-mathql_generator \
+#      helm-xmldiff 
 #      lablgtk2 \
 #      mathml-editor \
 #      lablgtkmathview \
@@ -16,12 +16,12 @@ TEST_REQUIRES = \
 REQUIRES = $(TEST_REQUIRES) #gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade
 
 OCAMLOPTIONS = \
-       -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -thread
+       -package "$(REQUIRES)" -predicates "$(PREDICATES)" #-pp camlp4o -thread
 OCAMLFIND = ocamlfind
 OCAMLDEBUGOPTIONS = -g
 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS)
 OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS)
-OCAMLDEP = $(OCAMLFIND) ocamldep -pp camlp4o
+OCAMLDEP = $(OCAMLFIND) ocamldep #-pp camlp4o
 OCAMLDEBUG = wowcamldebug
 
 LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))

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

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index fab2026adf255443cacb4e58306a7c65fea51cd3..0cc0fcb708d9f51be2a844a04fece6b5656e433a 100644 (file)
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -1,15 +1,24 @@
 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 *)
 ;;
 
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
 
+exception MatchingFailure
+
+val matching:
+  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+  CicUniv.universe_graph ->
+  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+
+
 (**
    Performs the beta expansion of the term "where" w.r.t. "what",
    i.e. returns the list of all the terms t s.t. "(t what) = where".
@@ -66,3 +75,7 @@ val is_identity: environment -> equality -> bool
 val string_of_equality: ?env:environment -> equality -> string
 
 val subsumption: environment -> equality -> equality -> bool
+
+val metas_of_term: Cic.term -> int list
+
+val fix_metas: int -> equality -> int * equality

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 4c1480d100c86a72a88ee652de5d4dcd5d697a69..5f9ffe33506e7ac4c266c41f5361af6368f20cd6 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -7,21 +7,13 @@ type result =
 ;;
 
 
-type equality_sign = Negative | Positive;;
-
-let string_of_sign = function
-  | Negative -> "Negative"
-  | Positive -> "Positive"
-;;
-
-
 (*
 let symbols_of_equality (_, (_, left, right), _, _) =
   TermSet.union (symbols_of_term left) (symbols_of_term right)
 ;;
 *)
 
-let symbols_of_equality ((_, (_, left, right), _, _) as equality) =
+let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
   let m1 = symbols_of_term left in
   let m = 
     TermMap.fold
@@ -49,8 +41,8 @@ struct
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let _, (ty, left, right), _, _ = eq1
-        and _, (ty', left', right'), _, _ = eq2 in
+        let _, (ty, left, right, _), _, _ = eq1
+        and _, (ty', left', right', _), _, _ = eq2 in
         let weight_of t = fst (weight_of_term ~consider_metas:false t) in
         let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
@@ -234,7 +226,7 @@ let contains_empty env (negative, positive) =
   try
     let (proof, _, _, _) =
       List.find
-        (fun (proof, (ty, left, right), m, a) ->
+        (fun (proof, (ty, left, right, ordering), m, a) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
@@ -663,24 +655,18 @@ let main () =
   let env = (metasenv, context, ugraph) in
   try
     let term_equality = equality_of_term meta_proof goal in
-    let meta_proof, (eq_ty, left, right), _, _ = term_equality in
+    let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
     let active = [] in
     let passive = make_passive [term_equality] equalities in
-    Printf.printf "\ncurrent goal: %s ={%s} %s\n"
-      (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
+    Printf.printf "\ncurrent goal: %s\n"
+      (string_of_equality ~env term_equality);
     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
-    Printf.printf "\nequalities:\n";
-    List.iter
-      (function (_, (ty, t1, t2), _, _) ->
-         let w1 = weight_of_term t1 in
-         let w2 = weight_of_term t2 in
-         let res = !compare_terms t1 t2 in
-         Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
-           (PP.ppterm t1) (string_of_weight w1)
-           (string_of_comparison res)
-           (PP.ppterm t2) (string_of_weight w2))
-      equalities;
+    Printf.printf "\nequalities:\n%s\n"
+      (String.concat "\n"
+         (List.map
+            (string_of_equality ~env)
+            equalities));
     print_endline "--------------------------------------------------";
     let start = Unix.gettimeofday () in
     print_endline "GO!";

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index b0aa00e890021aa93d00a4e38340efe283697cab..4a20f5c3d80eb1547d88801d88d4741c96965f9e 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -397,3 +397,12 @@ let rec lpo t1 t2 =
 
 (* settable by the user... *)
 let compare_terms = ref nonrec_kbo;;
+
+
+type equality_sign = Negative | Positive;;
+
+let string_of_sign = function
+  | Negative -> "Negative"
+  | Positive -> "Positive"
+;;
+

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 1adf90e5045094c048c30fe624f3d4ade8b2e068..295d1aa4d47d4c73ed428fd6ea26f0577ff2625f 100644 (file)
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -31,3 +31,8 @@ val lpo: Cic.term -> Cic.term -> comparison
 
 (** term-ordering function settable by the user *)
 val compare_terms: (Cic.term -> Cic.term -> comparison) ref
+
+type equality_sign = Negative | Positive
+
+val string_of_sign: equality_sign -> string
+