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