helm/software/components/tactics/paramodulation/utils.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 let debug = true;;
  29
  30 let debug_print s = if debug then prerr_endline (Lazy.force s);;
  31
  32 let print_metasenv metasenv =
  33   String.concat "\n--------------------------\n"
  34     (List.map (fun (i, context, term) ->
  35                  (string_of_int i) ^ " [\n" ^ (CicPp.ppcontext context) ^
  36                    "\n] " ^  (CicPp.ppterm term))
  37        metasenv)
  38 ;;
  39
  40
  41
  42
  43 let print_subst ?(prefix="\n") subst =
  44     String.concat prefix
  45      (List.map
  46        (fun (i, (c, t, ty)) ->
  47           Printf.sprintf "?%d -> %s : %s" i
  48             (CicPp.ppterm t) (CicPp.ppterm ty))
  49        subst)
  50 ;;
  51
  52 type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;;
  53
  54 let string_of_comparison = function
  55   | Lt -> "<"
  56   | Le -> "<="
  57   | Gt -> ">"
  58   | Ge -> ">="
  59   | Eq -> "="
  60   | Incomparable -> "I"
  61
  62 module OrderedTerm =
  63 struct
  64   type t = Cic.term
  65
  66   let compare = Pervasives.compare
  67 end
  68
  69 module TermSet = Set.Make(OrderedTerm);;
  70 module TermMap = Map.Make(OrderedTerm);;
  71
  72 let symbols_of_term term =
  73   let module C = Cic in
  74   let rec aux map = function
  75     | C.Meta _ -> map
  76     | C.Appl l ->
  77         List.fold_left (fun res t -> (aux res t)) map l
  78     | t ->
  79         let map =
  80           try
  81             let c = TermMap.find t map in
  82             TermMap.add t (c+1) map
  83           with Not_found ->
  84             TermMap.add t 1 map
  85         in
  86         map
  87   in
  88   aux TermMap.empty term
  89 ;;
  90
  91
  92 let metas_of_term term =
  93   let module C = Cic in
  94   let rec aux = function
  95     | C.Meta _ as t -> TermSet.singleton t
  96     | C.Appl l ->
  97         List.fold_left (fun res t -> TermSet.union res (aux t)) TermSet.empty l
  98     | t -> TermSet.empty (* TODO: maybe add other cases? *)
  99   in
 100   aux term
 101 ;;
 102
 103
 104 (************************* rpo ********************************)
 105 let number = [
 106   UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)",3;
 107   UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)",6;
 108   UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)",9;
 109   HelmLibraryObjects.Peano.pred_URI, 12;
 110   HelmLibraryObjects.Peano.plus_URI, 15;
 111   HelmLibraryObjects.Peano.minus_URI, 18;
 112   HelmLibraryObjects.Peano.mult_URI, 21;
 113   UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1)",103;
 114   UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)",106;
 115   UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)",109;
 116   UriManager.uri_of_string "cic:/matita/nat/nat/pred.con",112;
 117   UriManager.uri_of_string "cic:/matita/nat/plus/plus.con",115;
 118   UriManager.uri_of_string "cic:/matita/nat/minus/minus.con",118;
 119   UriManager.uri_of_string "cic:/matita/nat/times/times.con",121;
 120   ]
 121 ;;
 122
 123 let atomic t =
 124   match t with
 125       Cic.Const _
 126     | Cic.MutInd _
 127     | Cic.MutConstruct _
 128     | Cic.Rel _ -> true
 129     | _ -> false
 130
 131 let sig_order_const t1 t2 =
 132   try
 133     let u1 = CicUtil.uri_of_term t1 in
 134     let u2 = CicUtil.uri_of_term t2 in
 135     let n1 = List.assoc u1 number in
 136     let n2 = List.assoc u2 number in
 137     if n1 < n2 then Lt
 138     else if n1 > n2 then Gt
 139     else
 140       begin
 141         prerr_endline ("t1 = "^(CicPp.ppterm t1));
 142         prerr_endline ("t2 = "^(CicPp.ppterm t2));
 143         assert false
 144       end
 145   with
 146       Invalid_argument _
 147     | Not_found -> Incomparable
 148
 149 let sig_order t1 t2 =
 150   match t1, t2 with
 151       Cic.Rel n, Cic.Rel m when n < m -> Gt (* inverted order *)
 152     | Cic.Rel n, Cic.Rel m when n = m -> Incomparable
 153     | Cic.Rel n, Cic.Rel m when n > m -> Lt
 154     | Cic.Rel _, _ -> Gt
 155     | _, Cic.Rel _ -> Lt
 156     | _,_ -> sig_order_const t1 t2
 157
 158 let rec rpo_lt t1 t2 =
 159   let module C = Cic in
 160   let first_trie =
 161     match t1,t2 with
 162         C.Meta (_, _), C.Meta (_,_) -> false
 163       | C.Meta (_,_) , t2 -> TermSet.mem t1 (metas_of_term t2)
 164       | t1, C.Meta (_,_) -> false
 165       | C.Appl [h1;a1],C.Appl [h2;a2] when h1=h2 ->
 166           rpo_lt a1 a2
 167       | C.Appl (h1::arg1),C.Appl (h2::arg2) when h1=h2 ->
 168           if lex_lt arg1 arg2 then
 169             check_lt arg1 t2
 170           else false
 171       | C.Appl (h1::arg1),C.Appl (h2::arg2) ->
 172           (match sig_order h1 h2 with
 173              | Lt -> check_lt arg1 t2
 174              | _ -> false)
 175       | C.Appl (h1::arg1), t2 when atomic t2 ->
 176           (match sig_order h1 t2 with
 177              | Lt -> check_lt arg1 t2
 178              | _ -> false)
 179       | t1 , C.Appl (h2::arg2) when atomic t1 ->
 180           (match sig_order t1 h2 with
 181              | Lt -> true
 182              | _ -> false )
 183       | C.Appl [] , _ -> assert false
 184       | _ , C.Appl [] -> assert false
 185       | t1, t2 when (atomic t1 && atomic t2 && t1<>t2) ->
 186           (match sig_order t1 t2 with
 187              | Lt -> true
 188              | _ -> false)
 189       | _,_ -> false
 190   in
 191   if first_trie then true else
 192   match t2 with
 193       C.Appl (_::args) ->
 194         List.exists (fun a -> t1 = a || rpo_lt t1 a) args
 195     | _ -> false
 196
 197 and lex_lt l1 l2 =
 198   match l1,l2 with
 199       [],[] -> false
 200     | [],_ -> assert false
 201     | _, [] -> assert false
 202     | a1::l1, a2::l2 when a1 = a2 -> lex_lt l1 l2
 203     | a1::_, a2::_ -> rpo_lt a1 a2
 204
 205 and check_lt l t =
 206   List.fold_left
 207     (fun b a -> b && (rpo_lt a t))
 208     true l
 209 ;;
 210
 211 let rpo t1 t2 =
 212   if rpo_lt t2 t1 then Gt
 213   else if rpo_lt t1 t2 then Lt
 214   else Incomparable
 215
 216
 217 (*********************** fine rpo *****************************)
 218
 219 (* (weight of constants, [(meta, weight_of_meta)]) *)
 220 type weight = int * (int * int) list;;
 221
 222 let string_of_weight (cw, mw) =
 223   let s =
 224     String.concat ", "
 225       (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
 226   in
 227   Printf.sprintf "[%d; %s]" cw s
 228
 229
 230 let weight_of_term ?(consider_metas=true) term =
 231   let module C = Cic in
 232   let vars_dict = Hashtbl.create 5 in
 233   let rec aux = function
 234     | C.Meta (metano, _) when consider_metas ->
 235         (try
 236            let oldw = Hashtbl.find vars_dict metano in
 237            Hashtbl.replace vars_dict metano (oldw+1)
 238          with Not_found ->
 239            Hashtbl.add vars_dict metano 1);
 240         0
 241     | C.Meta _ -> 0 (* "variables" are lighter than constants and functions...*)
 242
 243     | C.Var (_, ens)
 244     | C.Const (_, ens)
 245     | C.MutInd (_, _, ens)
 246     | C.MutConstruct (_, _, _, ens) ->
 247         List.fold_left (fun w (u, t) -> (aux t) + w) 1 ens
 248
 249     | C.Cast (t1, t2)
 250     | C.Lambda (_, t1, t2)
 251     | C.Prod (_, t1, t2)
 252     | C.LetIn (_, t1, t2) ->
 253         let w1 = aux t1 in
 254         let w2 = aux t2 in
 255         w1 + w2 + 1
 256
 257     | C.Appl l -> List.fold_left (+) 0 (List.map aux l)
 258
 259     | C.MutCase (_, _, outt, t, pl) ->
 260         let w1 = aux outt in
 261         let w2 = aux t in
 262         let w3 = List.fold_left (+) 0 (List.map aux pl) in
 263         w1 + w2 + w3 + 1
 264
 265     | C.Fix (_, fl) ->
 266         List.fold_left (fun w (n, i, t1, t2) -> (aux t1) + (aux t2) + w) 1 fl
 267
 268     | C.CoFix (_, fl) ->
 269         List.fold_left (fun w (n, t1, t2) -> (aux t1) + (aux t2) + w) 1 fl
 270
 271     | _ -> 1
 272   in
 273   let w = aux term in
 274   let l =
 275     Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict [] in
 276   let compare w1 w2 =
 277     match w1, w2 with
 278     | (m1, _), (m2, _) -> m2 - m1
 279   in
 280   (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
 281 ;;
 282
 283
 284 module OrderedInt = struct
 285   type t = int
 286
 287   let compare = Pervasives.compare
 288 end
 289
 290 module IntSet = Set.Make(OrderedInt)
 291
 292 let compute_equality_weight ty left right =
 293   let metasw = ref 0 in
 294   let weight_of t =
 295     let w, m = (weight_of_term ~consider_metas:true t) in
 296     metasw := !metasw + (2 * (List.length m));
 297     w
 298   in
 299   (* Warning: the following let cannot be expanded since it forces the
 300      right evaluation order!!!! *)
 301   let w = (weight_of ty) + (weight_of left) + (weight_of right) in
 302   w + !metasw
 303 ;;
 304
 305
 306 (* returns a "normalized" version of the polynomial weight wl (with type
 307  * weight list), i.e. a list sorted ascending by meta number,
 308  * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
 309  * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
 310  *      (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
 311 let normalize_weight maxmeta (cw, wl) =
 312   let rec aux = function
 313     | 0 -> []
 314     | m -> (m, 0)::(aux (m-1))
 315   in
 316   let tmpl = aux maxmeta in
 317   let wl =
 318     List.sort
 319       (fun (m, _) (n, _) -> Pervasives.compare m n)
 320       (List.fold_left
 321          (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
 322   in
 323   (cw, wl)
 324 ;;
 325
 326
 327 let normalize_weights (cw1, wl1) (cw2, wl2) =
 328   let rec aux wl1 wl2 =
 329     match wl1, wl2 with
 330     | [], [] -> [], []
 331     | (m, w)::tl1, (n, w')::tl2 when m = n ->
 332         let res1, res2 = aux tl1 tl2 in
 333         (m, w)::res1, (n, w')::res2
 334     | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
 335         let res1, res2 = aux tl1 wl2 in
 336         (m, w)::res1, (m, 0)::res2
 337     | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
 338         let res1, res2 = aux wl1 tl2 in
 339         (n, 0)::res1, (n, w')::res2
 340     | [], (n, w)::tl2 ->
 341         let res1, res2 = aux [] tl2 in
 342         (n, 0)::res1, (n, w)::res2
 343     | (m, w)::tl1, [] ->
 344         let res1, res2 = aux tl1 [] in
 345         (m, w)::res1, (m, 0)::res2
 346     | _, _ -> assert false
 347   in
 348   let cmp (m, _) (n, _) = compare m n in
 349   let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
 350   (cw1, wl1), (cw2, wl2)
 351 ;;
 352
 353
 354 let compare_weights ?(normalize=false)
 355     ((h1, w1) as weight1) ((h2, w2) as weight2)=
 356   let (h1, w1), (h2, w2) =
 357     if normalize then
 358       normalize_weights weight1 weight2
 359     else
 360       (h1, w1), (h2, w2)
 361   in
 362   let res, diffs =
 363     try
 364       List.fold_left2
 365         (fun ((lt, eq, gt), diffs) w1 w2 ->
 366            match w1, w2 with
 367            | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
 368                let diffs = (w1 - w2) + diffs in
 369                let r = compare w1 w2 in
 370                if r < 0 then (lt+1, eq, gt), diffs
 371                else if r = 0 then (lt, eq+1, gt), diffs
 372                else (lt, eq, gt+1), diffs
 373            | (meta1, w1), (meta2, w2) ->
 374                debug_print
 375                  (lazy
 376                     (Printf.sprintf "HMMM!!!! %s, %s\n"
 377                        (string_of_weight weight1) (string_of_weight weight2)));
 378                assert false)
 379         ((0, 0, 0), 0) w1 w2
 380     with Invalid_argument _ ->
 381       debug_print
 382         (lazy
 383            (Printf.sprintf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n"
 384               (string_of_weight (h1, w1)) (string_of_weight weight1)
 385               (string_of_weight (h2, w2)) (string_of_weight weight2)
 386               (string_of_bool normalize)));
 387       assert false
 388   in
 389   let hdiff = h1 - h2 in
 390   match res with
 391   | (0, _, 0) ->
 392       if hdiff < 0 then Lt
 393       else if hdiff > 0 then Gt
 394       else Eq (* Incomparable *)
 395   | (m, _, 0) ->
 396       if hdiff <= 0 then Lt
 397       else if (- diffs) >= hdiff then Le else Incomparable
 398   | (0, _, m) ->
 399       if hdiff >= 0 then Gt
 400       else if diffs >= (- hdiff) then Ge else Incomparable
 401   | (m, _, n) when m > 0 && n > 0 ->
 402       Incomparable
 403   | _ -> assert false
 404
 405 ;;
 406
 407
 408 let rec aux_ordering ?(recursion=true) t1 t2 =
 409   let module C = Cic in
 410   let compare_uris u1 u2 =
 411     let res =
 412       compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) in
 413     if res < 0 then Lt
 414     else if res = 0 then Eq
 415     else Gt
 416   in
 417   match t1, t2 with
 418   | C.Meta _, _
 419   | _, C.Meta _ -> Incomparable
 420
 421   | t1, t2 when t1 = t2 -> Eq
 422
 423   | C.Rel n, C.Rel m -> if n > m then Lt else Gt
 424   | C.Rel _, _ -> Lt
 425   | _, C.Rel _ -> Gt
 426
 427   | C.Const (u1, _), C.Const (u2, _) -> compare_uris u1 u2
 428   | C.Const _, _ -> Lt
 429   | _, C.Const _ -> Gt
 430
 431   | C.MutInd (u1, _, _), C.MutInd (u2, _, _) -> compare_uris u1 u2
 432   | C.MutInd _, _ -> Lt
 433   | _, C.MutInd _ -> Gt
 434
 435   | C.MutConstruct (u1, _, _, _), C.MutConstruct (u2, _, _, _) ->
 436       compare_uris u1 u2
 437   | C.MutConstruct _, _ -> Lt
 438   | _, C.MutConstruct _ -> Gt
 439
 440   | C.Appl l1, C.Appl l2 when recursion ->
 441       let rec cmp t1 t2 =
 442         match t1, t2 with
 443         | [], [] -> Eq
 444         | _, [] -> Gt
 445         | [], _ -> Lt
 446         | hd1::tl1, hd2::tl2 ->
 447             let o = aux_ordering hd1 hd2 in
 448             if o = Eq then cmp tl1 tl2
 449             else o
 450       in
 451       cmp l1 l2
 452   | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion ->
 453       aux_ordering h1 h2
 454
 455   | t1, t2 ->
 456       debug_print
 457         (lazy
 458            (Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
 459               (CicPp.ppterm t1) (CicPp.ppterm t2)));
 460       Incomparable
 461 ;;
 462
 463
 464 (* w1, w2 are the weights, they should already be normalized... *)
 465 let nonrec_kbo_w (t1, w1) (t2, w2) =
 466   match compare_weights w1 w2 with
 467   | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
 468   | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
 469   | Eq -> aux_ordering t1 t2
 470   | res -> res
 471 ;;
 472
 473
 474 let nonrec_kbo t1 t2 =
 475   let w1 = weight_of_term t1 in
 476   let w2 = weight_of_term t2 in
 477   (*
 478   prerr_endline ("weight1 :"^(string_of_weight w1));
 479   prerr_endline ("weight2 :"^(string_of_weight w2));
 480   *)
 481   match compare_weights ~normalize:true w1 w2 with
 482   | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
 483   | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
 484   | Eq -> aux_ordering t1 t2
 485   | res -> res
 486 ;;
 487
 488
 489 let rec kbo t1 t2 =
 490   let aux = aux_ordering ~recursion:false in
 491   let w1 = weight_of_term t1
 492   and w2 = weight_of_term t2 in
 493   let rec cmp t1 t2 =
 494     match t1, t2 with
 495     | [], [] -> Eq
 496     | _, [] -> Gt
 497     | [], _ -> Lt
 498     | hd1::tl1, hd2::tl2 ->
 499         let o =
 500           kbo hd1 hd2
 501         in
 502         if o = Eq then cmp tl1 tl2
 503         else o
 504   in
 505   let comparison = compare_weights ~normalize:true w1 w2 in
 506   match comparison with
 507   | Le ->
 508       let r = aux t1 t2 in
 509       if r = Lt then Lt
 510       else if r = Eq then (
 511         match t1, t2 with
 512         | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
 513             if cmp tl1 tl2 = Lt then Lt else Incomparable
 514         | _, _ ->  Incomparable
 515       ) else Incomparable
 516   | Ge ->
 517       let r = aux t1 t2 in
 518       if r = Gt then Gt
 519       else if r = Eq then (
 520         match t1, t2 with
 521         | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
 522             if cmp tl1 tl2 = Gt then Gt else Incomparable
 523         | _, _ ->  Incomparable
 524       ) else Incomparable
 525   | Eq ->
 526       let r = aux t1 t2 in
 527       if r = Eq then (
 528         match t1, t2 with
 529         | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
 530             cmp tl1 tl2
 531         | _, _ ->  Incomparable
 532       ) else r
 533   | res -> res
 534 ;;
 535
 536 let rec ao t1 t2 =
 537   let get_hd t =
 538     match t with
 539         Cic.MutConstruct(uri,tyno,cno,_) -> Some(uri,tyno,cno)
 540       | Cic.Appl(Cic.MutConstruct(uri,tyno,cno,_)::_) ->
 541           Some(uri,tyno,cno)
 542       | _ -> None in
 543   let aux = aux_ordering ~recursion:false in
 544   let w1 = weight_of_term t1
 545   and w2 = weight_of_term t2 in
 546   let rec cmp t1 t2 =
 547     match t1, t2 with
 548     | [], [] -> Eq
 549     | _, [] -> Gt
 550     | [], _ -> Lt
 551     | hd1::tl1, hd2::tl2 ->
 552         let o =
 553           ao hd1 hd2
 554         in
 555         if o = Eq then cmp tl1 tl2
 556         else o
 557   in
 558   match get_hd t1, get_hd t2 with
 559       Some(_),None -> Lt
 560     | None,Some(_) -> Gt
 561     | _ ->
 562         let comparison = compare_weights ~normalize:true w1 w2 in
 563           match comparison with
 564             | Le ->
 565                 let r = aux t1 t2 in
 566                   if r = Lt then Lt
 567                   else if r = Eq then (
 568                     match t1, t2 with
 569                       | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
 570                           if cmp tl1 tl2 = Lt then Lt else Incomparable
 571                       | _, _ ->  Incomparable
 572                   ) else Incomparable
 573             | Ge ->
 574                 let r = aux t1 t2 in
 575                   if r = Gt then Gt
 576                   else if r = Eq then (
 577                     match t1, t2 with
 578                       | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
 579                           if cmp tl1 tl2 = Gt then Gt else Incomparable
 580                       | _, _ ->  Incomparable
 581                   ) else Incomparable
 582             | Eq ->
 583                 let r = aux t1 t2 in
 584                   if r = Eq then (
 585                     match t1, t2 with
 586                       | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
 587                           cmp tl1 tl2
 588                       | _, _ ->  Incomparable
 589                   ) else r
 590             | res -> res
 591 ;;
 592
 593 let names_of_context context =
 594   List.map
 595     (function
 596        | None -> None
 597        | Some (n, e) -> Some n)
 598     context
 599 ;;
 600
 601
 602 let rec lpo t1 t2 =
 603   let module C = Cic in
 604   match t1, t2 with
 605   | t1, t2 when t1 = t2 -> Eq
 606   | t1, (C.Meta _ as m) ->
 607       if TermSet.mem m (metas_of_term t1) then Gt else Incomparable
 608   | (C.Meta _ as m), t2 ->
 609       if TermSet.mem m (metas_of_term t2) then Lt else Incomparable
 610   | C.Appl (hd1::tl1), C.Appl (hd2::tl2) -> (
 611       let res =
 612         let f o r t =
 613           if r then true else
 614             match lpo t o with
 615             | Gt | Eq -> true
 616             | _ -> false
 617         in
 618         let res1 = List.fold_left (f t2) false tl1 in
 619         if res1 then Gt
 620         else let res2 = List.fold_left (f t1) false tl2 in
 621         if res2 then Lt
 622         else Incomparable
 623       in
 624       if res <> Incomparable then
 625         res
 626       else
 627         let f o r t =
 628           if not r then false else
 629             match lpo o t with
 630             | Gt -> true
 631             | _ -> false
 632         in
 633         match aux_ordering hd1 hd2 with
 634         | Gt ->
 635             let res = List.fold_left (f t1) false tl2 in
 636             if res then Gt
 637             else Incomparable
 638         | Lt ->
 639             let res = List.fold_left (f t2) false tl1 in
 640             if res then Lt
 641             else Incomparable
 642         | Eq -> (
 643             let lex_res =
 644               try
 645                 List.fold_left2
 646                   (fun r t1 t2 -> if r <> Eq then r else lpo t1 t2)
 647                   Eq tl1 tl2
 648               with Invalid_argument _ ->
 649                 Incomparable
 650             in
 651             match lex_res with
 652             | Gt ->
 653                 if List.fold_left (f t1) false tl2 then Gt
 654                 else Incomparable
 655             | Lt ->
 656                 if List.fold_left (f t2) false tl1 then Lt
 657                 else Incomparable
 658             | _ -> Incomparable
 659           )
 660         | _ -> Incomparable
 661     )
 662   | t1, t2 -> aux_ordering t1 t2
 663 ;;
 664
 665
 666 (* settable by the user... *)
 667 let compare_terms = ref nonrec_kbo;;
 668 (* let compare_terms = ref ao;; *)
 669 (* let compare_terms = ref rpo;; *)
 670
 671 let guarded_simpl ?(debug=false) context t =
 672   if !compare_terms == nonrec_kbo then t
 673   else
 674     let t' = ProofEngineReduction.simpl context t in
 675     if t = t' then t else
 676       begin
 677         let simpl_order = !compare_terms t t' in
 678         if debug then
 679           prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t'));
 680         if simpl_order = Gt then (if debug then prerr_endline "GT";t')
 681         else (if debug then prerr_endline "NO_GT";t)
 682       end
 683 ;;
 684
 685 type equality_sign = Negative | Positive;;
 686
 687 let string_of_sign = function
 688   | Negative -> "Negative"
 689   | Positive -> "Positive"
 690 ;;
 691
 692
 693 type pos = Left | Right
 694
 695 let string_of_pos = function
 696   | Left -> "Left"
 697   | Right -> "Right"
 698 ;;
 699
 700
 701 let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ())
 702 let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ())
 703 let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ())
 704 let eq_XURI () =
 705   let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
 706   UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
 707 let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())