helm/ocaml/paramodulation/indexing.ml

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