helm/ocaml/paramodulation/indexing.ml

   1
   2 type retrieval_mode = Matching | Unification;;
   3
   4
   5 let print_candidates mode term res =
   6   let _ =
   7     match mode with
   8     | Matching ->
   9         Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
  10     | Unification ->
  11         Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
  12   in
  13   print_endline
  14     (String.concat "\n"
  15        (List.map
  16           (fun (p, e) ->
  17              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
  18                (Inference.string_of_equality e))
  19           res));
  20   print_endline "|";
  21 ;;
  22
  23
  24 let indexing_retrieval_time = ref 0.;;
  25
  26
  27 (* let my_apply_subst subst term = *)
  28 (*   let module C = Cic in *)
  29 (*   let lookup lift_amount meta = *)
  30 (*     match meta with *)
  31 (*     | C.Meta (i, _) -> ( *)
  32 (*         try *)
  33 (*           let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in *)
  34 (*           (\* CicSubstitution.lift lift_amount  *\)t *)
  35 (*         with Not_found -> meta *)
  36 (*       ) *)
  37 (*     | _ -> assert false *)
  38 (*   in *)
  39 (*   let rec apply_aux lift_amount =  function *)
  40 (*     | C.Meta (i, l) as t -> lookup lift_amount t *)
  41 (*     | C.Appl l -> C.Appl (List.map (apply_aux lift_amount) l) *)
  42 (*     | C.Prod (nn, s, t) -> *)
  43 (*         C.Prod (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
  44 (*     | C.Lambda (nn, s, t) -> *)
  45 (*         C.Lambda (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
  46 (*     | t -> t *)
  47 (*   in *)
  48 (*   apply_aux 0 term *)
  49 (* ;; *)
  50
  51
  52 (* let apply_subst subst term = *)
  53 (*   Printf.printf "| apply_subst:\n| subst: %s\n| term: %s\n" *)
  54 (*     (Utils.print_subst ~prefix:" ; " subst) (CicPp.ppterm term); *)
  55 (*   let res = my_apply_subst subst term in *)
  56 (* (\*   let res = CicMetaSubst.apply_subst subst term in *\) *)
  57 (*   Printf.printf "| res: %s\n" (CicPp.ppterm res); *)
  58 (*   print_endline "|"; *)
  59 (*   res *)
  60 (* ;; *)
  61
  62 (* let apply_subst = my_apply_subst *)
  63 let apply_subst = CicMetaSubst.apply_subst
  64
  65
  66 let apply_subst =
  67   let profile = CicUtil.profile "apply_subst" in
  68   (fun s a -> profile (apply_subst s) a)
  69 ;;
  70
  71
  72 (*
  73 let empty_table () =
  74   Path_indexing.PSTrie.empty
  75 ;;
  76
  77 let index = Path_indexing.index
  78 and remove_index = Path_indexing.remove_index
  79 and in_index = Path_indexing.in_index;;
  80
  81 let get_candidates mode trie term =
  82   let t1 = Unix.gettimeofday () in
  83   let res =
  84     let s =
  85       match mode with
  86       | Matching -> Path_indexing.retrieve_generalizations trie term
  87       | Unification -> Path_indexing.retrieve_unifiables trie term
  88 (*       Path_indexing.retrieve_all trie term *)
  89     in
  90     Path_indexing.PosEqSet.elements s
  91   in
  92 (*   print_candidates mode term res; *)
  93   let t2 = Unix.gettimeofday () in
  94   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
  95   res
  96 ;;
  97 *)
  98
  99
 100 let empty_table () =
 101   Discrimination_tree.DiscriminationTree.empty
 102 ;;
 103
 104 let index = Discrimination_tree.index
 105 and remove_index = Discrimination_tree.remove_index
 106 and in_index = Discrimination_tree.in_index;;
 107
 108 let get_candidates mode tree term =
 109   let t1 = Unix.gettimeofday () in
 110   let res =
 111     let s =
 112       match mode with
 113       | Matching -> Discrimination_tree.retrieve_generalizations tree term
 114       | Unification -> Discrimination_tree.retrieve_unifiables tree term
 115     in
 116     Discrimination_tree.PosEqSet.elements s
 117   in
 118 (*   print_candidates mode term res; *)
 119 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
 120 (*   print_newline (); *)
 121   let t2 = Unix.gettimeofday () in
 122   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
 123   res
 124 ;;
 125
 126
 127 (* let get_candidates = *)
 128 (*   let profile = CicUtil.profile "Indexing.get_candidates" in *)
 129 (*   (fun mode tree term -> profile (get_candidates mode tree) term) *)
 130 (* ;; *)
 131
 132
 133 let match_unif_time_ok = ref 0.;;
 134 let match_unif_time_no = ref 0.;;
 135
 136
 137 let rec find_matches metasenv context ugraph lift_amount term =
 138   let module C = Cic in
 139   let module U = Utils in
 140   let module S = CicSubstitution in
 141   let module M = CicMetaSubst in
 142   let module HL = HelmLibraryObjects in
 143   let cmp = !Utils.compare_terms in
 144   let names = Utils.names_of_context context in
 145   function
 146     | [] -> None
 147     | candidate::tl ->
 148         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
 149         let do_match c other eq_URI =
 150           let subst', metasenv', ugraph' =
 151             let t1 = Unix.gettimeofday () in
 152             try
 153               let r =
 154                 Inference.matching (metasenv @ metas) context
 155                   term (S.lift lift_amount c) ugraph in
 156               let t2 = Unix.gettimeofday () in
 157               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 158               r
 159             with e ->
 160               let t2 = Unix.gettimeofday () in
 161               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 162               raise e
 163           in
 164             Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 165                   (candidate, eq_URI))
 166         in
 167         let c, other, eq_URI =
 168           if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
 169           else right, left, HL.Logic.eq_ind_r_URI
 170         in
 171         if o <> U.Incomparable then
 172           try
 173             do_match c other eq_URI
 174           with e ->
 175             find_matches metasenv context ugraph lift_amount term tl
 176         else
 177           let res = try do_match c other eq_URI with e -> None in
 178           match res with
 179           | Some (_, s, _, _, _) ->
 180               let c' = (* M. *)apply_subst s c
 181               and other' = (* M. *)apply_subst s other in
 182               let order = cmp c' other' in
 183               let names = U.names_of_context context in
 184               if order = U.Gt then
 185                 res
 186               else
 187                 find_matches metasenv context ugraph lift_amount term tl
 188           | None ->
 189               find_matches metasenv context ugraph lift_amount term tl
 190 ;;
 191
 192
 193 let rec find_all_matches ?(unif_fun=Inference.unification)
 194     metasenv context ugraph lift_amount term =
 195   let module C = Cic in
 196   let module U = Utils in
 197   let module S = CicSubstitution in
 198   let module M = CicMetaSubst in
 199   let module HL = HelmLibraryObjects in
 200   let cmp = !Utils.compare_terms in
 201   let names = Utils.names_of_context context in
 202   function
 203     | [] -> []
 204     | candidate::tl ->
 205         let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
 206         let do_match c other eq_URI =
 207           let subst', metasenv', ugraph' =
 208             let t1 = Unix.gettimeofday () in
 209             try
 210               let r =
 211                 unif_fun (metasenv @ metas) context
 212                   term (S.lift lift_amount c) ugraph in
 213               let t2 = Unix.gettimeofday () in
 214               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 215               r
 216             with e ->
 217               let t2 = Unix.gettimeofday () in
 218               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 219               raise e
 220           in
 221           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 222            (candidate, eq_URI))
 223         in
 224         let c, other, eq_URI =
 225           if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
 226           else right, left, HL.Logic.eq_ind_r_URI
 227         in
 228         if o <> U.Incomparable then
 229           try
 230             let res = do_match c other eq_URI in
 231             res::(find_all_matches ~unif_fun metasenv context ugraph
 232                     lift_amount term tl)
 233           with e ->
 234             find_all_matches ~unif_fun metasenv context ugraph
 235               lift_amount term tl
 236         else
 237           try
 238             let res = do_match c other eq_URI in
 239             match res with
 240             | _, s, _, _, _ ->
 241                 let c' = (* M. *)apply_subst s c
 242                 and other' = (* M. *)apply_subst s other in
 243                 let order = cmp c' other' in
 244                 let names = U.names_of_context context in
 245                 if order <> U.Lt && order <> U.Le then
 246                   res::(find_all_matches ~unif_fun metasenv context ugraph
 247                           lift_amount term tl)
 248                 else
 249                   find_all_matches ~unif_fun metasenv context ugraph
 250                     lift_amount term tl
 251           with e ->
 252             find_all_matches ~unif_fun metasenv context ugraph
 253               lift_amount term tl
 254 ;;
 255
 256
 257 let subsumption env table target =
 258   let _, (ty, left, right, _), tmetas, _ = target in
 259   let metasenv, context, ugraph = env in
 260   let metasenv = metasenv @ tmetas in
 261   let samesubst subst subst' =
 262     let tbl = Hashtbl.create (List.length subst) in
 263     List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
 264     List.for_all
 265       (fun (m, (c, t1, t2)) ->
 266          try
 267            let c', t1', t2' = Hashtbl.find tbl m in
 268            if (c = c') && (t1 = t1') && (t2 = t2') then true
 269            else false
 270          with Not_found ->
 271            true)
 272       subst'
 273   in
 274   let leftr =
 275     match left with
 276     | Cic.Meta _ -> []
 277     | _ ->
 278         let leftc = get_candidates Matching table left in
 279         find_all_matches ~unif_fun:Inference.matching
 280           metasenv context ugraph 0 left leftc
 281   in
 282   let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) =
 283     try
 284       let other = if pos = Utils.Left then r else l in
 285       let subst', menv', ug' =
 286         let t1 = Unix.gettimeofday () in
 287         try
 288           let r =
 289             Inference.matching metasenv context what other ugraph in
 290           let t2 = Unix.gettimeofday () in
 291           match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 292           r
 293         with e ->
 294           let t2 = Unix.gettimeofday () in
 295           match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 296           raise e
 297       in
 298       samesubst subst subst'
 299     with e ->
 300       false
 301   in
 302   let r = List.exists (ok right) leftr in
 303   if r then
 304     true
 305   else
 306     let rightr =
 307       match right with
 308       | Cic.Meta _ -> []
 309       | _ ->
 310           let rightc = get_candidates Matching table right in
 311           find_all_matches ~unif_fun:Inference.matching
 312             metasenv context ugraph 0 right rightc
 313     in
 314     List.exists (ok left) rightr
 315 ;;
 316
 317
 318 let rec demodulate_term metasenv context ugraph table lift_amount term =
 319   let module C = Cic in
 320   let module S = CicSubstitution in
 321   let module M = CicMetaSubst in
 322   let module HL = HelmLibraryObjects in
 323   let candidates = get_candidates Matching table term in
 324   match term with
 325   | C.Meta _ -> None
 326   | term ->
 327       let res =
 328         find_matches metasenv context ugraph lift_amount term candidates
 329       in
 330       if res <> None then
 331         res
 332       else
 333         match term with
 334         | C.Appl l ->
 335             let res, ll =
 336               List.fold_left
 337                 (fun (res, tl) t ->
 338                    if res <> None then
 339                      (res, tl @ [S.lift 1 t])
 340                    else
 341                      let r =
 342                        demodulate_term metasenv context ugraph table
 343                          lift_amount t
 344                      in
 345                      match r with
 346                      | None -> (None, tl @ [S.lift 1 t])
 347                      | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 348                 (None, []) l
 349             in (
 350               match res with
 351               | None -> None
 352               | Some (_, subst, menv, ug, eq_found) ->
 353                   Some (C.Appl ll, subst, menv, ug, eq_found)
 354             )
 355         | C.Prod (nn, s, t) ->
 356             let r1 =
 357               demodulate_term metasenv context ugraph table lift_amount s in (
 358               match r1 with
 359               | None ->
 360                   let r2 =
 361                     demodulate_term metasenv
 362                       ((Some (nn, C.Decl s))::context) ugraph
 363                       table (lift_amount+1) t
 364                   in (
 365                     match r2 with
 366                     | None -> None
 367                     | Some (t', subst, menv, ug, eq_found) ->
 368                         Some (C.Prod (nn, (S.lift 1 s), t'),
 369                               subst, menv, ug, eq_found)
 370                   )
 371               | Some (s', subst, menv, ug, eq_found) ->
 372                   Some (C.Prod (nn, s', (S.lift 1 t)),
 373                         subst, menv, ug, eq_found)
 374             )
 375         | t ->
 376             None
 377 ;;
 378
 379
 380 let build_ens_for_sym_eq ty x y =
 381   [(UriManager.uri_of_string
 382       "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty);
 383    (UriManager.uri_of_string
 384       "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x);
 385    (UriManager.uri_of_string
 386       "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)]
 387 ;;
 388
 389
 390 let build_newtarget_time = ref 0.;;
 391
 392
 393 let demod_counter = ref 1;;
 394
 395 let rec demodulation newmeta env table sign target =
 396   let module C = Cic in
 397   let module S = CicSubstitution in
 398   let module M = CicMetaSubst in
 399   let module HL = HelmLibraryObjects in
 400   let metasenv, context, ugraph = env in
 401   let _, proof, (eq_ty, left, right, order), metas, args = target in
 402   let metasenv' = metasenv @ metas in
 403
 404   let maxmeta = ref newmeta in
 405
 406   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 407     let time1 = Unix.gettimeofday () in
 408
 409     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 410     let what, other = if pos = Utils.Left then what, other else other, what in
 411     let newterm, newproof =
 412       let bo = (* M. *)apply_subst subst (S.subst other t) in
 413       let t' =
 414         let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
 415         incr demod_counter;
 416         let l, r =
 417           if is_left then t, S.lift 1 right else S.lift 1 left, t in
 418         (name, ty, S.lift 1 eq_ty, l, r)
 419       in
 420       if sign = Utils.Positive then
 421         (bo,
 422          Inference.ProofBlock (subst, eq_URI, t', eq_found, proof))
 423       else
 424         let metaproof =
 425           incr maxmeta;
 426           let irl =
 427             CicMkImplicit.identity_relocation_list_for_metavariable context in
 428           Printf.printf "\nADDING META: %d\n" !maxmeta;
 429           print_newline ();
 430           C.Meta (!maxmeta, irl)
 431         in
 432         let target' =
 433           let eq_found =
 434             let proof' =
 435               let ens =
 436                 if pos = Utils.Left then
 437                   build_ens_for_sym_eq ty what other
 438                 else
 439                   build_ens_for_sym_eq ty other what
 440               in
 441               Inference.ProofSymBlock (ens, proof')
 442             in
 443             let what, other =
 444               if pos = Utils.Left then what, other else other, what
 445             in
 446             pos, (0, proof', (ty, other, what, Utils.Incomparable),
 447                   menv', args')
 448           in
 449           let target_proof =
 450             let pb =
 451               Inference.ProofBlock (subst, eq_URI, t', eq_found,
 452                                     Inference.BasicProof metaproof)
 453             in
 454             match proof with
 455             | Inference.BasicProof _ ->
 456                 print_endline "replacing a BasicProof";
 457                 pb
 458             | Inference.ProofGoalBlock (_, parent_eq) ->
 459                 print_endline "replacing another ProofGoalBlock";
 460                 Inference.ProofGoalBlock (pb, parent_eq)
 461             | _ -> assert false
 462           in
 463           (0, target_proof, (eq_ty, left, right, order), metas, args)
 464         in
 465         let refl =
 466           C.Appl [C.MutConstruct (* reflexivity *)
 467                     (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
 468                   eq_ty; if is_left then right else left]
 469         in
 470         (bo,
 471          Inference.ProofGoalBlock (Inference.BasicProof refl, target'))
 472     in
 473     let left, right = if is_left then newterm, right else left, newterm in
 474     let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
 475     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
 476     and newargs =
 477       List.filter
 478         (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
 479         args
 480     in
 481     let ordering = !Utils.compare_terms left right in
 482
 483     let time2 = Unix.gettimeofday () in
 484     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 485
 486     let res =
 487       let w = Utils.compute_equality_weight eq_ty left right in
 488       (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
 489     in
 490 (*     if sign = Utils.Positive then ( *)
 491 (*       let newm, res = Inference.fix_metas !maxmeta res in *)
 492 (*       maxmeta := newm; *)
 493 (*       !maxmeta, res *)
 494 (*     ) else *)
 495     !maxmeta(* newmeta *), res
 496   in
 497   let res = demodulate_term metasenv' context ugraph table 0 left in
 498 (*   let build_identity (w, p, (t, l, r, o), m, a) = *)
 499 (*     match o with *)
 500 (*     | Utils.Gt -> (w, p, (t, r, r, Utils.Eq), m, a) *)
 501 (*     | _ -> (w, p, (t, l, l, Utils.Eq), m, a) *)
 502 (*   in *)
 503   match res with
 504   | Some t ->
 505       let newmeta, newtarget = build_newtarget true t in
 506       if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
 507         (Inference.meta_convertibility_eq target newtarget) then
 508           newmeta, newtarget
 509       else
 510 (*         if subsumption env table newtarget then *)
 511 (*           newmeta, build_identity newtarget *)
 512 (*         else *)
 513         demodulation newmeta env table sign newtarget
 514   | None ->
 515       let res = demodulate_term metasenv' context ugraph table 0 right in
 516       match res with
 517       | Some t ->
 518           let newmeta, newtarget = build_newtarget false t in
 519           if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
 520             (Inference.meta_convertibility_eq target newtarget) then
 521               newmeta, newtarget
 522           else
 523 (*             if subsumption env table newtarget then *)
 524 (*               newmeta, build_identity newtarget *)
 525 (*             else *)
 526               demodulation newmeta env table sign newtarget
 527       | None ->
 528           newmeta, target
 529 ;;
 530
 531
 532 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 533   let module C = Cic in
 534   let module S = CicSubstitution in
 535   let module M = CicMetaSubst in
 536   let module HL = HelmLibraryObjects in
 537   let candidates = get_candidates Unification table term in
 538   let res, lifted_term =
 539     match term with
 540     | C.Meta (i, l) ->
 541         let l', lifted_l =
 542           List.fold_right
 543             (fun arg (res, lifted_tl) ->
 544                match arg with
 545                | Some arg ->
 546                    let arg_res, lifted_arg =
 547                      betaexpand_term metasenv context ugraph table
 548                        lift_amount arg in
 549                    let l1 =
 550                      List.map
 551                        (fun (t, s, m, ug, eq_found) ->
 552                           (Some t)::lifted_tl, s, m, ug, eq_found)
 553                        arg_res
 554                    in
 555                    (l1 @
 556                       (List.map
 557                          (fun (l, s, m, ug, eq_found) ->
 558                             (Some lifted_arg)::l, s, m, ug, eq_found)
 559                          res),
 560                     (Some lifted_arg)::lifted_tl)
 561                | None ->
 562                    (List.map
 563                       (fun (r, s, m, ug, eq_found) ->
 564                          None::r, s, m, ug, eq_found) res,
 565                     None::lifted_tl)
 566             ) l ([], [])
 567         in
 568         let e =
 569           List.map
 570             (fun (l, s, m, ug, eq_found) ->
 571                (C.Meta (i, l), s, m, ug, eq_found)) l'
 572         in
 573         e, C.Meta (i, lifted_l)
 574
 575     | C.Rel m ->
 576         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 577
 578     | C.Prod (nn, s, t) ->
 579         let l1, lifted_s =
 580           betaexpand_term metasenv context ugraph table lift_amount s in
 581         let l2, lifted_t =
 582           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 583             table (lift_amount+1) t in
 584         let l1' =
 585           List.map
 586             (fun (t, s, m, ug, eq_found) ->
 587                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 588         and l2' =
 589           List.map
 590             (fun (t, s, m, ug, eq_found) ->
 591                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 592         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 593
 594     | C.Appl l ->
 595         let l', lifted_l =
 596           List.fold_right
 597             (fun arg (res, lifted_tl) ->
 598                let arg_res, lifted_arg =
 599                  betaexpand_term metasenv context ugraph table lift_amount arg
 600                in
 601                let l1 =
 602                  List.map
 603                    (fun (a, s, m, ug, eq_found) ->
 604                       a::lifted_tl, s, m, ug, eq_found)
 605                    arg_res
 606                in
 607                (l1 @
 608                   (List.map
 609                      (fun (r, s, m, ug, eq_found) ->
 610                         lifted_arg::r, s, m, ug, eq_found)
 611                      res),
 612                 lifted_arg::lifted_tl)
 613             ) l ([], [])
 614         in
 615         (List.map
 616            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 617          C.Appl lifted_l)
 618
 619     | t -> [], (S.lift lift_amount t)
 620   in
 621   match term with
 622   | C.Meta _ -> res, lifted_term
 623   | term ->
 624       let r =
 625         find_all_matches metasenv context ugraph lift_amount term candidates
 626       in
 627       r @ res, lifted_term
 628 ;;
 629
 630
 631 let sup_l_counter = ref 1;;
 632
 633 let superposition_left newmeta (metasenv, context, ugraph) table target =
 634   let module C = Cic in
 635   let module S = CicSubstitution in
 636   let module M = CicMetaSubst in
 637   let module HL = HelmLibraryObjects in
 638   let module CR = CicReduction in
 639   let module U = Utils in
 640   let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
 641   let expansions, _ =
 642     let term = if ordering = U.Gt then left else right in
 643     betaexpand_term metasenv context ugraph table 0 term
 644   in
 645   let maxmeta = ref newmeta in
 646   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 647
 648     print_endline "\nSUPERPOSITION LEFT\n";
 649
 650     let time1 = Unix.gettimeofday () in
 651
 652     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 653     let what, other = if pos = Utils.Left then what, other else other, what in
 654     let newgoal, newproof =
 655       let bo' = (* M. *)apply_subst s (S.subst other bo) in
 656       let t' =
 657         let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
 658         incr sup_l_counter;
 659         let l, r =
 660           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 661         (name, ty, S.lift 1 eq_ty, l, r)
 662       in
 663 (*       let bo'' = *)
 664 (*         C.Appl ( *)
 665 (*           [C.MutInd (HL.Logic.eq_URI, 0, []); *)
 666 (*            S.lift 1 eq_ty] @ *)
 667 (*             if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *)
 668 (*             else [S.lift 1 left; S.lift 1 bo']) *)
 669 (*       in *)
 670 (*       let t' = *)
 671 (*         let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in *)
 672 (*         incr sup_l_counter; *)
 673 (*         C.Lambda (name, ty, bo'') *)
 674 (*       in *)
 675       incr maxmeta;
 676       let metaproof =
 677         let irl =
 678           CicMkImplicit.identity_relocation_list_for_metavariable context in
 679         C.Meta (!maxmeta, irl)
 680       in
 681       let target' =
 682         let eq_found =
 683           let proof' =
 684             let ens =
 685               if pos = Utils.Left then
 686                 build_ens_for_sym_eq ty what other
 687               else
 688                 build_ens_for_sym_eq ty other what
 689             in
 690             Inference.ProofSymBlock (ens, proof')
 691           in
 692           let what, other =
 693             if pos = Utils.Left then what, other else other, what
 694           in
 695           pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 696         in
 697         let target_proof =
 698           let pb =
 699             Inference.ProofBlock (s, eq_URI, t', eq_found,
 700                                   Inference.BasicProof metaproof)
 701           in
 702           match proof with
 703           | Inference.BasicProof _ ->
 704               print_endline "replacing a BasicProof";
 705               pb
 706           | Inference.ProofGoalBlock (_, parent_eq) ->
 707               print_endline "replacing another ProofGoalBlock";
 708               Inference.ProofGoalBlock (pb, parent_eq)
 709           | _ -> assert false
 710         in
 711         (weight, target_proof, (eq_ty, left, right, ordering), [], [])
 712       in
 713       let refl =
 714         C.Appl [C.MutConstruct (* reflexivity *)
 715                   (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
 716                 eq_ty; if ordering = U.Gt then right else left]
 717       in
 718       (bo',
 719        Inference.ProofGoalBlock (Inference.BasicProof refl, target'))
 720     in
 721     let left, right =
 722       if ordering = U.Gt then newgoal, right else left, newgoal in
 723     let neworder = !Utils.compare_terms left right in
 724
 725     let time2 = Unix.gettimeofday () in
 726     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 727
 728     let res =
 729       let w = Utils.compute_equality_weight eq_ty left right in
 730       (w, newproof, (eq_ty, left, right, neworder), [], [])
 731     in
 732     res
 733   in
 734   !maxmeta, List.map build_new expansions
 735 ;;
 736
 737
 738 let sup_r_counter = ref 1;;
 739
 740 let superposition_right newmeta (metasenv, context, ugraph) table target =
 741   let module C = Cic in
 742   let module S = CicSubstitution in
 743   let module M = CicMetaSubst in
 744   let module HL = HelmLibraryObjects in
 745   let module CR = CicReduction in
 746   let module U = Utils in
 747   let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 748   let metasenv' = metasenv @ newmetas in
 749   let maxmeta = ref newmeta in
 750   let res1, res2 =
 751     match ordering with
 752     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
 753     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
 754     | _ ->
 755         let res l r =
 756           List.filter
 757             (fun (_, subst, _, _, _) ->
 758                let subst = (* M. *)apply_subst subst in
 759                let o = !Utils.compare_terms (subst l) (subst r) in
 760                o <> U.Lt && o <> U.Le)
 761             (fst (betaexpand_term metasenv' context ugraph table 0 l))
 762         in
 763         (res left right), (res right left)
 764   in
 765   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
 766
 767     let time1 = Unix.gettimeofday () in
 768
 769     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 770     let what, other = if pos = Utils.Left then what, other else other, what in
 771     let newgoal, newproof =
 772       let bo' = (* M. *)apply_subst s (S.subst other bo) in
 773       let t' =
 774         let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
 775         incr sup_r_counter;
 776         let l, r =
 777           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 778         (name, ty, S.lift 1 eq_ty, l, r)
 779       in
 780 (*       let bo'' = *)
 781 (*         C.Appl ( *)
 782 (*           [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ *)
 783 (*             if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *)
 784 (*             else [S.lift 1 left; S.lift 1 bo']) *)
 785 (*       in *)
 786 (*       let t' = *)
 787 (*         let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in *)
 788 (*         incr sup_r_counter; *)
 789 (*         C.Lambda (name, ty, bo'') *)
 790 (*       in *)
 791       bo',
 792       Inference.ProofBlock (s, eq_URI, t', eq_found, eqproof(* target *))
 793 (*       (\* M. *\)apply_subst s *)
 794 (*         (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
 795 (*                  eqproof; other; proof']) *)
 796     in
 797     let newmeta, newequality =
 798       let left, right =
 799         if ordering = U.Gt then newgoal, (* M. *)apply_subst s right
 800         else (* M. *)apply_subst s left, newgoal in
 801       let neworder = !Utils.compare_terms left right
 802       and newmenv = newmetas @ menv'
 803       and newargs = args @ args' in
 804       let eq' =
 805         let w = Utils.compute_equality_weight eq_ty left right in
 806         (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
 807       and env = (metasenv, context, ugraph) in
 808       let newm, eq' = Inference.fix_metas !maxmeta eq' in
 809       newm, eq'
 810     in
 811     maxmeta := newmeta;
 812
 813     let time2 = Unix.gettimeofday () in
 814     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 815
 816     newequality
 817   in
 818
 819 (*   let build_new = *)
 820 (*     let profile = CicUtil.profile "Indexing.superposition_right.build_new" in *)
 821 (*     (fun o e -> profile (build_new o) e) *)
 822 (*   in *)
 823
 824   let new1 = List.map (build_new U.Gt) res1
 825   and new2 = List.map (build_new U.Lt) res2 in
 826   let ok = function
 827     | _, _, (_, left, right, _), _, _ ->
 828         not (fst (CR.are_convertible context left right ugraph))
 829   in
 830   (!maxmeta,
 831    (List.filter ok (new1 @ new2)))
 832 ;;