Code restructuring.

[helm.git] / helm / ocaml / tactics / paramodulation / utils.ml

diff --git a/helm/ocaml/tactics/paramodulation/utils.ml b/helm/ocaml/tactics/paramodulation/utils.ml
index b2555cdb4b1f9323262a5e164615d942818d300b..defd72b16e3746a3bdf9d4bcf0061efae31c64ae 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/utils.ml
+++ b/helm/ocaml/tactics/paramodulation/utils.ml
@@ -25,7 +25,7 @@
 
 (* $Id$ *)
 
-let debug = true;;
+let debug = false;;
 
 let debug_print s = if debug then prerr_endline (Lazy.force s);;
 
@@ -109,7 +109,14 @@ let number = [
   HelmLibraryObjects.Peano.pred_URI, 12;
   HelmLibraryObjects.Peano.plus_URI, 15;
   HelmLibraryObjects.Peano.minus_URI, 18;
-  HelmLibraryObjects.Peano.mult_URI, 21
+  HelmLibraryObjects.Peano.mult_URI, 21;
+  UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1)",103;
+  UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)",106;
+  UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)",109;
+  UriManager.uri_of_string "cic:/matita/nat/nat/pred.con",112;
+  UriManager.uri_of_string "cic:/matita/nat/plus/plus.con",115;
+  UriManager.uri_of_string "cic:/matita/nat/minus/minus.con",118;
+  UriManager.uri_of_string "cic:/matita/nat/times/times.con",121;
   ]
 ;;
 
@@ -117,10 +124,11 @@ let atomic t =
   match t with
       Cic.Const _ 
     | Cic.MutInd _ 
-    | Cic.MutConstruct _ -> true
+    | Cic.MutConstruct _ 
+    | Cic.Rel _ -> true
     | _ -> false
 
-let sig_order t1 t2 =
+let sig_order_const t1 t2 =
   try
     let u1 = CicUtil.uri_of_term t1 in
     let u2 = CicUtil.uri_of_term t2 in  
@@ -138,52 +146,73 @@ let sig_order t1 t2 =
       Invalid_argument _ 
     | Not_found -> Incomparable
 
-let rec rpo t1 t2 =
+let sig_order t1 t2 =
+  match t1, t2 with
+      Cic.Rel n, Cic.Rel m when n < m -> Gt (* inverted order *)
+    | Cic.Rel n, Cic.Rel m when n = m -> Incomparable
+    | Cic.Rel n, Cic.Rel m when n > m -> Lt
+    | Cic.Rel _, _ -> Gt
+    | _, Cic.Rel _ -> Lt
+    | _,_ -> sig_order_const t1 t2
+
+let rec rpo_lt t1 t2 =
   let module C = Cic in 
-  match t1,t2 with 
-      C.Meta (_, _), C.Meta (_,_) -> Incomparable
-    | C.Meta (_,_) as t1,t2 when TermSet.mem t1 (metas_of_term t2)
-       -> Lt
-    | t1, (C.Meta (_,_) as t2) when TermSet.mem t2 (metas_of_term t1)
-       -> Gt
-    | C.Appl (h1::arg1),C.Appl (h2::arg2) when h1=h2 ->
-       (match lex arg1 arg2 with
-          | Lt when (check Gt t2 arg1) -> Lt 
-          | Gt when (check Gt t1 arg2) -> Gt
-          | _ -> Incomparable )
-    | C.Appl (h1::arg1),C.Appl (h2::arg2) -> 
-       (match sig_order h1 h2 with
-         | Lt when (check Gt t2 arg1) -> Lt 
-         | Gt when (check Gt t1 arg2) -> Gt
-         | _ -> Incomparable )
-    | C.Appl (h1::arg1), t2 when atomic t2 ->
-       (match sig_order h1 t2 with
-          | Lt when (check Gt t2 arg1) -> Lt 
-          | Gt -> Gt
-           | _ -> Incomparable )
-    | t1 , C.Appl (h2::arg2) when atomic t1 ->
-       (match sig_order t1 h2 with
-          | Lt -> Lt 
-          | Gt when (check Gt t1 arg2) -> Gt
-           | _ -> Incomparable )
-    | C.Appl [] , _ -> assert false 
-    | _ , C.Appl [] -> assert false
-    | _,_ -> Incomparable
-
-and lex l1 l2 = 
+  let first_trie =
+    match t1,t2 with 
+       C.Meta (_, _), C.Meta (_,_) -> false
+      | C.Meta (_,_) , t2 -> TermSet.mem t1 (metas_of_term t2)
+      | t1, C.Meta (_,_) -> false
+      | C.Appl [h1;a1],C.Appl [h2;a2] when h1=h2 -> 
+         rpo_lt a1 a2
+      | C.Appl (h1::arg1),C.Appl (h2::arg2) when h1=h2 ->
+         if lex_lt arg1 arg2 then
+           check_lt arg1 t2 
+         else false
+      | C.Appl (h1::arg1),C.Appl (h2::arg2) -> 
+         (match sig_order h1 h2 with
+            | Lt -> check_lt arg1 t2
+            | _ -> false)
+      | C.Appl (h1::arg1), t2 when atomic t2 ->
+         (match sig_order h1 t2 with
+            | Lt -> check_lt arg1 t2
+            | _ -> false)
+      | t1 , C.Appl (h2::arg2) when atomic t1 ->
+         (match sig_order t1 h2 with
+            | Lt -> true
+             | _ -> false )
+      | C.Appl [] , _ -> assert false 
+      | _ , C.Appl [] -> assert false
+      | t1, t2 when (atomic t1 && atomic t2 && t1<>t2) ->
+         (match sig_order t1 t2 with
+            | Lt -> true
+            | _ -> false)
+      | _,_ -> false
+  in
+  if first_trie then true else
+  match t2 with
+      C.Appl (_::args) ->
+       List.exists (fun a -> t1 = a || rpo_lt t1 a) args
+    | _ -> false
+ 
+and lex_lt l1 l2 = 
   match l1,l2 with
-      [],[] -> Incomparable
+      [],[] -> false
     | [],_ -> assert false
     | _, [] -> assert false
-    | a1::l1, a2::l2 when a1 = a2 -> lex l1 l2
-    | a1::_, a2::_ -> rpo a1 a2
-
-and check o t l =
+    | a1::l1, a2::l2 when a1 = a2 -> lex_lt l1 l2
+    | a1::_, a2::_ -> rpo_lt a1 a2
+ 
+and check_lt l t =
   List.fold_left 
-    (fun b a -> b && (rpo t a = o)) 
+    (fun b a -> b && (rpo_lt a t))
     true l
 ;;
 
+let rpo t1 t2 =
+  if rpo_lt t2 t1 then Gt
+  else if rpo_lt t1 t2 then Lt
+  else Incomparable
+
 
 (*********************** fine rpo *****************************)
 
@@ -635,18 +664,20 @@ let rec lpo t1 t2 =
 
 
 (* settable by the user... *)
-let compare_terms = ref nonrec_kbo;; 
+(* let compare_terms = ref nonrec_kbo;; *)
 (* let compare_terms = ref ao;; *)
-(* let compare_terms = ref rpo;; *)
+let compare_terms = ref rpo;; 
 
-let guarded_simpl context t = t
-(*
+let guarded_simpl ?(debug=false) context t =
   let t' = ProofEngineReduction.simpl context t in
-  let simpl_order = !compare_terms t t' in
-  if simpl_order = Gt then 
-    (* prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t')); *)
-  t'
-  else t *)
+  if t = t' then t else
+    begin
+      let simpl_order = !compare_terms t t' in
+      if debug then
+       prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t'));
+      if simpl_order = Gt then (if debug then prerr_endline "GT";t')
+      else (if debug then prerr_endline "NO_GT";t)
+    end
 ;;
 
 type equality_sign = Negative | Positive;;