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