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

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* let _profiler = <:profiler<_profiler>>;; *)
  27
  28 (* $Id$ *)
  29
  30 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
  31 (*
  32 module Index = Equality_indexing.DT (* path tree based indexing *)
  33 *)
  34
  35 let debug_print = Utils.debug_print;;
  36
  37 (*
  38 for debugging
  39 let check_equation env equation msg =
  40   let w, proof, (eq_ty, left, right, order), metas, args = equation in
  41   let metasenv, context, ugraph = env
  42   let metasenv' = metasenv @ metas in
  43     try
  44       CicTypeChecker.type_of_aux' metasenv' context left ugraph;
  45       CicTypeChecker.type_of_aux' metasenv' context right ugraph;
  46       ()
  47     with
  48         CicUtil.Meta_not_found _ as exn ->
  49           begin
  50             prerr_endline msg;
  51             prerr_endline (CicPp.ppterm left);
  52             prerr_endline (CicPp.ppterm right);
  53             raise exn
  54           end
  55 *)
  56
  57 type retrieval_mode = Matching | Unification;;
  58
  59 let string_of_res ?env =
  60   function
  61       None -> "None"
  62     | Some (t, s, m, u, (p,e)) ->
  63         Printf.sprintf "Some: (%s, %s, %s)"
  64           (Utils.string_of_pos p)
  65           (Equality.string_of_equality ?env e)
  66           (CicPp.ppterm t)
  67 ;;
  68
  69 let print_res ?env res =
  70   prerr_endline
  71     (String.concat "\n"
  72        (List.map (string_of_res ?env) res))
  73 ;;
  74
  75 let print_candidates ?env mode term res =
  76   let _ =
  77     match mode with
  78     | Matching ->
  79         prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
  80     | Unification ->
  81         prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
  82   in
  83   prerr_endline
  84     (String.concat "\n"
  85        (List.map
  86           (fun (p, e) ->
  87              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
  88                (Equality.string_of_equality ?env e))
  89           res));
  90 ;;
  91
  92
  93 let apply_subst = Subst.apply_subst
  94
  95 let index = Index.index
  96 let remove_index = Index.remove_index
  97 let in_index = Index.in_index
  98 let empty = Index.empty
  99 let init_index = Index.init_index
 100
 101 let check_disjoint_invariant subst metasenv msg =
 102   if (List.exists
 103         (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
 104   then
 105     begin
 106       prerr_endline ("not disjoint: " ^ msg);
 107       assert false
 108     end
 109 ;;
 110
 111 let check_for_duplicates metas msg =
 112   let rec aux = function
 113     | [] -> true
 114     | (m,_,_)::tl -> not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in
 115   let b = aux metas in
 116     if not b then
 117       begin
 118       prerr_endline ("DUPLICATI " ^ msg);
 119       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 120       assert false
 121       end
 122     else ()
 123 ;;
 124
 125 let check_metasenv msg menv =
 126   List.iter
 127     (fun (i,ctx,ty) ->
 128        try ignore(CicTypeChecker.type_of_aux' menv ctx ty
 129                   CicUniv.empty_ugraph)
 130        with
 131          | CicUtil.Meta_not_found _ ->
 132              prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv);
 133              assert false
 134          | _ -> ()
 135     ) menv
 136 ;;
 137
 138 (* the metasenv returned by res must included in the original one,
 139 due to matching. If it fails, it is probably because we are not
 140 demodulating with a unit equality *)
 141
 142 let not_unit_eq ctx eq =
 143   let (_,_,(ty,left,right,o),metas,_) = Equality.open_equality eq in
 144   let b =
 145   List.exists
 146     (fun (_,_,ty) ->
 147        try
 148          let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.oblivion_ugraph
 149          in s = Cic.Sort(Cic.Prop)
 150        with _ ->
 151          prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas
 152   in b
 153 (*
 154 if b then prerr_endline ("not a unit equality: " ^ Equality.string_of_equality eq); b *)
 155 ;;
 156
 157 let check_demod_res res metasenv msg =
 158   match res with
 159     | Some (_, _, menv, _, _) ->
 160         let b =
 161           List.for_all
 162             (fun (i,_,_) ->
 163                (List.exists (fun (j,_,_) -> i=j) metasenv)) menv
 164         in
 165           if (not b) then
 166             begin
 167               debug_print (lazy ("extended context " ^ msg));
 168               debug_print (lazy (CicMetaSubst.ppmetasenv [] menv));
 169             end;
 170         b
 171     | None -> false
 172 ;;
 173
 174 let check_res res msg =
 175   match res with
 176     | Some (t, subst, menv, ug, eq_found) ->
 177         let eqs = Equality.string_of_equality (snd eq_found) in
 178         check_metasenv msg menv;
 179         check_disjoint_invariant subst menv msg;
 180         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
 181     | None -> ()
 182 ;;
 183
 184 let check_target bag context target msg =
 185   let w, proof, (eq_ty, left, right, order), metas,_ =
 186     Equality.open_equality target in
 187   (* check that metas does not contains duplicates *)
 188   let eqs = Equality.string_of_equality target in
 189   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
 190   let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
 191     @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof)  in
 192   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
 193   let _ = if menv <> metas then
 194     begin
 195       prerr_endline ("extra metas " ^ msg);
 196       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 197       prerr_endline "**********************";
 198       prerr_endline (CicMetaSubst.ppmetasenv [] menv);
 199       prerr_endline ("left: " ^ (CicPp.ppterm left));
 200       prerr_endline ("right: " ^ (CicPp.ppterm right));
 201       prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
 202       assert false
 203     end
 204   else () in ()
 205 (*
 206   try
 207       ignore(CicTypeChecker.type_of_aux'
 208         metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph)
 209   with e ->
 210       prerr_endline msg;
 211       prerr_endline (Founif.string_of_proof proof);
 212       prerr_endline (CicPp.ppterm (Founif.build_proof_term proof));
 213       prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
 214       prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
 215       raise e
 216 *)
 217
 218
 219 (* returns a list of all the equalities in the tree that are in relation
 220    "mode" with the given term, where mode can be either Matching or
 221    Unification.
 222
 223    Format of the return value: list of tuples in the form:
 224    (position - Left or Right - of the term that matched the given one in this
 225      equality,
 226     equality found)
 227
 228    Note that if equality is "left = right", if the ordering is left > right,
 229    the position will always be Left, and if the ordering is left < right,
 230    position will be Right.
 231 *)
 232
 233 let get_candidates ?env mode tree term =
 234   let s =
 235     match mode with
 236     | Matching ->
 237         Index.retrieve_generalizations tree term
 238     | Unification ->
 239         Index.retrieve_unifiables tree term
 240
 241   in
 242   Index.PosEqSet.elements s
 243 ;;
 244
 245 (*
 246   finds the first equality in the index that matches "term", of type "termty"
 247   termty can be Implicit if it is not needed. The result (one of the sides of
 248   the equality, actually) should be not greater (wrt the term ordering) than
 249   term
 250
 251   Format of the return value:
 252
 253   (term to substitute, [Cic.Rel 1 properly lifted - see the various
 254                         build_newtarget functions inside the various
 255                         demodulation_* functions]
 256    substitution used for the matching,
 257    metasenv,
 258    ugraph, [substitution, metasenv and ugraph have the same meaning as those
 259    returned by CicUnification.fo_unif]
 260    (equality where the matching term was found, [i.e. the equality to use as
 261                                                 rewrite rule]
 262     uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
 263          the equality: this is used to build the proof term, again see one of
 264          the build_newtarget functions]
 265    ))
 266 *)
 267 let rec find_matches bag metasenv context ugraph lift_amount term termty =
 268   let module C = Cic in
 269   let module U = Utils in
 270   let module S = CicSubstitution in
 271   let module M = CicMetaSubst in
 272   let module HL = HelmLibraryObjects in
 273   let cmp = !Utils.compare_terms in
 274   let check = match termty with C.Implicit None -> false | _ -> true in
 275   function
 276     | [] -> None
 277     | candidate::tl ->
 278         let pos, equality = candidate in
 279         (* if not_unit_eq context equality then
 280           begin
 281             prerr_endline "not a unit";
 282             prerr_endline (Equality.string_of_equality equality)
 283           end; *)
 284         let (_, proof, (ty, left, right, o), metas,_) =
 285           Equality.open_equality equality
 286         in
 287         if Utils.debug_metas then
 288           ignore(check_target bag context (snd candidate) "find_matches");
 289         if Utils.debug_res then
 290           begin
 291             let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
 292             let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
 293             let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
 294             let ms="metasenv =" ^ (CicMetaSubst.ppmetasenv [] metasenv) ^ "\n" in
 295             let eq_uri =
 296               match LibraryObjects.eq_URI () with
 297                 | Some (uri) -> uri
 298                 | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
 299             let p="proof = "^
 300               (CicPp.ppterm(Equality.build_proof_term bag eq_uri [] 0 proof))^"\n"
 301             in
 302
 303               check_for_duplicates metas "gia nella metas";
 304               check_for_duplicates metasenv "gia nel metasenv";
 305               check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^ms^p)
 306           end;
 307         if check && not (fst (CicReduction.are_convertible
 308                                 ~metasenv context termty ty ugraph)) then (
 309           find_matches bag metasenv context ugraph lift_amount term termty tl
 310         ) else
 311           let do_match c =
 312             let subst', metasenv', ugraph' =
 313               Founif.matching
 314                 metasenv metas context term (S.lift lift_amount c) ugraph
 315             in
 316             if Utils.debug_metas then
 317               check_metasenv "founif :" metasenv';
 318             Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
 319           in
 320           let c, other =
 321             if pos = Utils.Left then left, right
 322             else right, left
 323           in
 324           if o <> U.Incomparable then
 325             let res =
 326               try
 327                 do_match c
 328               with Founif.MatchingFailure ->
 329                 find_matches bag metasenv context ugraph lift_amount term termty tl
 330             in
 331               if Utils.debug_res then ignore (check_res res "find1");
 332               res
 333           else
 334             let res =
 335               try do_match c
 336               with Founif.MatchingFailure -> None
 337             in
 338               if Utils.debug_res then ignore (check_res res "find2");
 339             match res with
 340             | Some (_, s, _, _, _) ->
 341                 let c' = apply_subst s c in
 342                 (*
 343              let other' = U.guarded_simpl context (apply_subst s other) in *)
 344                 let other' = apply_subst s other in
 345                 let order = cmp c' other' in
 346                 if order = U.Gt then
 347                   res
 348                 else
 349                   find_matches bag
 350                     metasenv context ugraph lift_amount term termty tl
 351             | None ->
 352                 find_matches bag metasenv context ugraph lift_amount term termty tl
 353 ;;
 354
 355 let find_matches metasenv context ugraph lift_amount term termty =
 356   find_matches metasenv context ugraph lift_amount term termty
 357 ;;
 358
 359 (*
 360   as above, but finds all the matching equalities, and the matching condition
 361   can be either Founif.matching or Inference.unification
 362 *)
 363 (* XXX termty unused *)
 364 let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false)
 365     metasenv context ugraph lift_amount term termty =
 366   let module C = Cic in
 367   let module U = Utils in
 368   let module S = CicSubstitution in
 369   let module M = CicMetaSubst in
 370   let module HL = HelmLibraryObjects in
 371   (* prerr_endline ("matching " ^  CicPp.ppterm term); *)
 372   let cmp x y =
 373           let r = !Utils.compare_terms x y in
 374 (*
 375           prerr_endline (
 376                   CicPp.ppterm x ^ "   " ^
 377                   Utils.string_of_comparison r ^ "   " ^
 378                        CicPp.ppterm y );
 379 *)
 380           r
 381   in
 382   let check = match termty with C.Implicit None -> false | _ -> true in
 383   function
 384     | [] -> []
 385     | candidate::tl ->
 386         let pos, equality = candidate in
 387         let (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in
 388         if check && not (fst (CicReduction.are_convertible
 389                                 ~metasenv context termty ty ugraph)) then (
 390           find_all_matches metasenv context ugraph lift_amount term termty tl
 391         ) else
 392         let do_match c =
 393           let subst', metasenv', ugraph' =
 394             unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
 395           in
 396           (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
 397         in
 398
 399         let c, other =
 400           if pos = Utils.Left then left, right
 401           else right, left
 402         in
 403         if o <> U.Incomparable then
 404           try
 405             let res = do_match c in
 406             res::(find_all_matches ~unif_fun metasenv context ugraph
 407                     lift_amount term termty tl)
 408           with
 409           | Founif.MatchingFailure
 410           | CicUnification.UnificationFailure _
 411           | CicUnification.Uncertain _ ->
 412               find_all_matches ~unif_fun metasenv context ugraph
 413                 lift_amount term termty tl
 414         else
 415           try
 416             let res = do_match c in
 417             match res with
 418             | _, s, _, _, _ ->
 419                 let c' = apply_subst s c
 420                 and other' = apply_subst s other in
 421                 let order = cmp c' other' in
 422                 if (demod && order = U.Gt) ||
 423                    (not demod && (order <> U.Lt && order <> U.Le))
 424                 then
 425                   res::(find_all_matches ~unif_fun metasenv context ugraph
 426                           lift_amount term termty tl)
 427                 else
 428                   find_all_matches ~unif_fun metasenv context ugraph
 429                      lift_amount term termty tl
 430           with
 431           | Founif.MatchingFailure
 432           | CicUnification.UnificationFailure _
 433           | CicUnification.Uncertain _ ->
 434               find_all_matches ~unif_fun metasenv context ugraph
 435                 lift_amount term termty tl
 436 ;;
 437
 438 let find_all_matches
 439   ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
 440 =
 441     find_all_matches
 442       ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
 443   (*prerr_endline "CANDIDATES:";
 444   List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
 445   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
 446   (List.length rc));*)
 447 ;;
 448 (*
 449   returns true if target is subsumed by some equality in table
 450 *)
 451 (*
 452 let print_res l =
 453   prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
 454     ((pos,equation),_)) -> Equality.string_of_equality equation)l))
 455 ;;
 456 *)
 457
 458 let subsumption_aux use_unification env table target =
 459   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
 460   let _, context, ugraph = env in
 461   let metasenv = tmetas in
 462   let predicate, unif_fun =
 463     if use_unification then
 464       Unification, Founif.unification
 465     else
 466       Matching, Founif.matching
 467   in
 468   let leftr =
 469     match left with
 470     | Cic.Meta _ when not use_unification -> []
 471     | _ ->
 472         let leftc = get_candidates predicate table left in
 473         find_all_matches ~unif_fun
 474           metasenv context ugraph 0 left ty leftc
 475   in
 476   let rec ok what leftorright = function
 477     | [] -> None
 478     | (_, subst, menv, ug, (pos,equation))::tl ->
 479         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
 480         try
 481           let other = if pos = Utils.Left then r else l in
 482           let what' = Subst.apply_subst subst what in
 483           let other' = Subst.apply_subst subst other in
 484           let subst', menv', ug' =
 485             unif_fun metasenv m context what' other' ugraph
 486           in
 487           (match Subst.merge_subst_if_possible subst subst' with
 488           | None -> ok what leftorright tl
 489           | Some s -> Some (s, equation, leftorright <> pos ))
 490         with
 491         | Founif.MatchingFailure
 492         | CicUnification.UnificationFailure _ -> ok what leftorright tl
 493   in
 494   match ok right Utils.Left leftr with
 495   | Some _ as res -> res
 496   | None ->
 497       let rightr =
 498         match right with
 499           | Cic.Meta _ when not use_unification -> []
 500           | _ ->
 501               let rightc = get_candidates predicate table right in
 502                 find_all_matches ~unif_fun
 503                   metasenv context ugraph 0 right ty rightc
 504       in
 505         ok left Utils.Right rightr
 506 ;;
 507
 508 let subsumption x y z =
 509   subsumption_aux false x y z
 510 ;;
 511
 512 let unification x y z =
 513   subsumption_aux true x y z
 514 ;;
 515
 516 (* the target must be disjoint from the equations in the table *)
 517 let subsumption_aux_all use_unification env table target =
 518   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
 519   let _, context, ugraph = env in
 520   let metasenv = tmetas in
 521   if Utils.debug_metas then
 522     check_for_duplicates metasenv "subsumption_aux_all";
 523   let predicate, unif_fun =
 524     if use_unification then
 525       Unification, Founif.unification
 526     else
 527       Matching, Founif.matching
 528   in
 529   let leftr =
 530     match left with
 531     | Cic.Meta _ (*when not use_unification*) -> []
 532     | _ ->
 533         let leftc = get_candidates predicate table left in
 534         find_all_matches ~unif_fun
 535           metasenv context ugraph 0 left ty leftc
 536   in
 537   let rightr =
 538         match right with
 539           | Cic.Meta _ (*when not use_unification*) -> []
 540           | _ ->
 541               let rightc = get_candidates predicate table right in
 542                 find_all_matches ~unif_fun
 543                   metasenv context ugraph 0 right ty rightc
 544   in
 545   let rec ok_all what leftorright = function
 546     | [] -> []
 547     | (_, subst, menv, ug, (pos,equation))::tl ->
 548         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
 549         try
 550           let other = if pos = Utils.Left then r else l in
 551           let what' = Subst.apply_subst subst what in
 552           let other' = Subst.apply_subst subst other in
 553           let subst', menv', ug' =
 554             unif_fun [] menv context what' other' ugraph
 555           in
 556           (match Subst.merge_subst_if_possible subst subst' with
 557           | None -> ok_all what leftorright tl
 558           | Some s ->
 559               (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
 560         with
 561         | Founif.MatchingFailure
 562         | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
 563   in
 564   (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
 565 ;;
 566
 567 let subsumption_all x y z =
 568   subsumption_aux_all false x y z
 569 ;;
 570
 571 let unification_all x y z =
 572   subsumption_aux_all true x y z
 573 ;;
 574
 575 let rec demodulation_aux bag ?from ?(typecheck=false)
 576   metasenv context ugraph table lift_amount term =
 577   let module C = Cic in
 578   let module S = CicSubstitution in
 579   let module M = CicMetaSubst in
 580   let module HL = HelmLibraryObjects in
 581   if Utils.debug_metas then
 582     check_for_duplicates metasenv "in input a demodulation aux";
 583   let candidates =
 584     get_candidates
 585       ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
 586   in
 587 (*   let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in *)
 588   let res =
 589     match term with
 590       | C.Meta _ -> None
 591       | term ->
 592           let res =
 593             try
 594               let termty, ugraph =
 595                 if typecheck then
 596                   CicTypeChecker.type_of_aux' metasenv context term ugraph
 597                 else
 598                   C.Implicit None, ugraph
 599               in
 600                 find_matches bag metasenv context ugraph
 601                   lift_amount term termty candidates
 602             with _ ->
 603               prerr_endline "type checking error";
 604               prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
 605               prerr_endline ("term: " ^ (CicPp.ppterm term));
 606               assert false;
 607               (* None *)
 608           in
 609           let res =
 610             (if Utils.debug_res then
 611             ignore(check_res res "demod1");
 612             if check_demod_res res metasenv "demod" then res else None) in
 613           if res <> None then
 614               res
 615             else
 616               match term with
 617                 | C.Appl l ->
 618                     let res, ll =
 619                       List.fold_left
 620                         (fun (res, tl) t ->
 621                            if res <> None then
 622                              (res, tl @ [S.lift 1 t])
 623                            else
 624                              let r =
 625                                demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck
 626                                  lift_amount t
 627                              in
 628                                match r with
 629                                  | None -> (None, tl @ [S.lift 1 t])
 630                                  | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 631                         (None, []) l
 632                     in (
 633                         match res with
 634                           | None -> None
 635                           | Some (_, subst, menv, ug, eq_found) ->
 636                               Some (C.Appl ll, subst, menv, ug, eq_found)
 637                       )
 638 (*
 639                 | C.Prod (nn, s, t) ->
 640                     let r1 =
 641                       demodulation_aux bag ~from:"2"
 642                         metasenv context ugraph table lift_amount s in (
 643                         match r1 with
 644                           | None ->
 645                               let r2 =
 646                                 demodulation_aux bag metasenv
 647                                   ((Some (nn, C.Decl s))::context) ugraph
 648                                   table (lift_amount+1) t
 649                               in (
 650                                   match r2 with
 651                                     | None -> None
 652                                     | Some (t', subst, menv, ug, eq_found) ->
 653                                         Some (C.Prod (nn, (S.lift 1 s), t'),
 654                                               subst, menv, ug, eq_found)
 655                                 )
 656                           | Some (s', subst, menv, ug, eq_found) ->
 657                               Some (C.Prod (nn, s', (S.lift 1 t)),
 658                                     subst, menv, ug, eq_found)
 659                       )
 660                 | C.Lambda (nn, s, t) ->
 661                     prerr_endline "siam qui";
 662                     let r1 =
 663                       demodulation_aux bag
 664                         metasenv context ugraph table lift_amount s in (
 665                         match r1 with
 666                           | None ->
 667                               let r2 =
 668                                 demodulation_aux bag metasenv
 669                                   ((Some (nn, C.Decl s))::context) ugraph
 670                                   table (lift_amount+1) t
 671                               in (
 672                                   match r2 with
 673                                     | None -> None
 674                                     | Some (t', subst, menv, ug, eq_found) ->
 675                                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 676                                               subst, menv, ug, eq_found)
 677                                 )
 678                           | Some (s', subst, menv, ug, eq_found) ->
 679                               Some (C.Lambda (nn, s', (S.lift 1 t)),
 680                                     subst, menv, ug, eq_found)
 681                       )
 682 *)
 683                 | t ->
 684                     None
 685   in
 686   if Utils.debug_res then ignore(check_res res "demod_aux output");
 687   res
 688 ;;
 689
 690 exception Foo
 691
 692 (** demodulation, when target is an equality *)
 693 let rec demodulation_equality bag ?from eq_uri env table target =
 694   let module C = Cic in
 695   let module S = CicSubstitution in
 696   let module M = CicMetaSubst in
 697   let module HL = HelmLibraryObjects in
 698   let module U = Utils in
 699   let metasenv, context, ugraph = env in
 700   let w, proof, (eq_ty, left, right, order), metas, id =
 701     Equality.open_equality target
 702   in
 703   (* first, we simplify *)
 704 (*   let right = U.guarded_simpl context right in *)
 705 (*   let left = U.guarded_simpl context left in *)
 706 (*   let order = !Utils.compare_terms left right in *)
 707 (*   let stat = (eq_ty, left, right, order) in  *)
 708 (*  let w = Utils.compute_equality_weight stat in*)
 709   (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
 710   if Utils.debug_metas then
 711     ignore(check_target bag context target "demod equalities input");
 712   let metasenv' = (* metasenv @ *) metas in
 713
 714   let build_newtarget bag is_left (t, subst, menv, ug, eq_found) =
 715
 716     if Utils.debug_metas then
 717       begin
 718         ignore(check_for_duplicates menv "input1");
 719         ignore(check_disjoint_invariant subst menv "input2");
 720         let substs = Subst.ppsubst subst in
 721         ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
 722       end;
 723     let pos, equality = eq_found in
 724     let (_, proof',
 725         (ty, what, other, _), menv',id') = Equality.open_equality equality in
 726     (*
 727     let ty =
 728       try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
 729       with CicUtil.Meta_not_found _ -> ty
 730     in *)
 731     let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
 732     let what, other = if pos = Utils.Left then what, other else other, what in
 733     let newterm, newproof =
 734       let bo =
 735         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 736 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
 737       let name = C.Name "x" in
 738       let bo' =
 739         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 740           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 741       in
 742           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
 743           (Cic.Lambda (name, ty, bo'))))))
 744     in
 745     let newmenv = menv in
 746     let left, right = if is_left then newterm, right else left, newterm in
 747     let ordering = !Utils.compare_terms left right in
 748     let stat = (eq_ty, left, right, ordering) in
 749     let bag, res =
 750       let w = Utils.compute_equality_weight stat in
 751       Equality.mk_equality bag (w, newproof, stat,newmenv)
 752     in
 753     if Utils.debug_metas then
 754       ignore(check_target bag context res "buildnew_target output");
 755     bag, res
 756   in
 757   let res =
 758     demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
 759   in
 760   if Utils.debug_res then check_res res "demod result";
 761   let bag, newtarget =
 762     match res with
 763     | Some t ->
 764         let bag, newtarget = build_newtarget bag true t in
 765           (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
 766           if (Equality.is_weak_identity newtarget) (* || *)
 767             (*Equality.meta_convertibility_eq target newtarget*) then
 768               bag, newtarget
 769           else
 770             demodulation_equality bag ?from eq_uri env table newtarget
 771     | None ->
 772         let res = demodulation_aux bag metasenv' context ugraph table 0 right in
 773         if Utils.debug_res then check_res res "demod result 1";
 774           match res with
 775           | Some t ->
 776               let bag, newtarget = build_newtarget bag false t in
 777                 if (Equality.is_weak_identity newtarget) ||
 778                   (Equality.meta_convertibility_eq target newtarget) then
 779                     bag, newtarget
 780                 else
 781                    demodulation_equality bag ?from eq_uri env table newtarget
 782           | None ->
 783               bag, target
 784   in
 785   (* newmeta, newtarget *)
 786   bag, newtarget
 787 ;;
 788
 789 (**
 790    Performs the beta expansion of the term "term" w.r.t. "table",
 791    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 792    in table.
 793 *)
 794 let rec betaexpand_term
 795   ?(subterms_only=false) metasenv context ugraph table lift_amount term
 796 =
 797   let module C = Cic in
 798   let module S = CicSubstitution in
 799   let module M = CicMetaSubst in
 800   let module HL = HelmLibraryObjects in
 801
 802   let res, lifted_term =
 803     match term with
 804     | C.Meta (i, l) ->
 805         let l = [] in
 806         let l', lifted_l =
 807           List.fold_right
 808             (fun arg (res, lifted_tl) ->
 809                match arg with
 810                | Some arg ->
 811                    let arg_res, lifted_arg =
 812                      betaexpand_term metasenv context ugraph table
 813                        lift_amount arg in
 814                    let l1 =
 815                      List.map
 816                        (fun (t, s, m, ug, eq_found) ->
 817                           (Some t)::lifted_tl, s, m, ug, eq_found)
 818                        arg_res
 819                    in
 820                    (l1 @
 821                       (List.map
 822                          (fun (l, s, m, ug, eq_found) ->
 823                             (Some lifted_arg)::l, s, m, ug, eq_found)
 824                          res),
 825                     (Some lifted_arg)::lifted_tl)
 826                | None ->
 827                    (List.map
 828                       (fun (r, s, m, ug, eq_found) ->
 829                          None::r, s, m, ug, eq_found) res,
 830                     None::lifted_tl)
 831             ) l ([], [])
 832         in
 833         let e =
 834           List.map
 835             (fun (l, s, m, ug, eq_found) ->
 836                (C.Meta (i, l), s, m, ug, eq_found)) l'
 837         in
 838         e, C.Meta (i, lifted_l)
 839
 840     | C.Rel m ->
 841         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 842
 843     | C.Prod (nn, s, t) ->
 844         let l1, lifted_s =
 845           betaexpand_term metasenv context ugraph table lift_amount s in
 846         let l2, lifted_t =
 847           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 848             table (lift_amount+1) t in
 849         let l1' =
 850           List.map
 851             (fun (t, s, m, ug, eq_found) ->
 852                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 853         and l2' =
 854           List.map
 855             (fun (t, s, m, ug, eq_found) ->
 856                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 857         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 858
 859     | C.Lambda (nn, s, t) ->
 860         let l1, lifted_s =
 861           betaexpand_term metasenv context ugraph table lift_amount s in
 862         let l2, lifted_t =
 863           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 864             table (lift_amount+1) t in
 865         let l1' =
 866           List.map
 867             (fun (t, s, m, ug, eq_found) ->
 868                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 869         and l2' =
 870           List.map
 871             (fun (t, s, m, ug, eq_found) ->
 872                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 873         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 874
 875     | C.Appl l ->
 876         let l', lifted_l =
 877           List.fold_left
 878             (fun (res, lifted_tl) arg ->
 879                let arg_res, lifted_arg =
 880                  betaexpand_term metasenv context ugraph table lift_amount arg
 881                in
 882                let l1 =
 883                  List.map
 884                    (fun (a, s, m, ug, eq_found) ->
 885                       a::lifted_tl, s, m, ug, eq_found)
 886                    arg_res
 887                in
 888                (l1 @
 889                   (List.map
 890                      (fun (r, s, m, ug, eq_found) ->
 891                         lifted_arg::r, s, m, ug, eq_found)
 892                      res),
 893                 lifted_arg::lifted_tl)
 894             ) ([], []) (List.rev l)
 895         in
 896         (List.map
 897            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 898          C.Appl lifted_l)
 899
 900     | t -> [], (S.lift lift_amount t)
 901   in
 902   match term with
 903   | C.Meta (i, l) -> res, lifted_term
 904   | term ->
 905       let termty, ugraph =
 906        C.Implicit None, ugraph
 907 (*          CicTypeChecker.type_of_aux' metasenv context term ugraph  *)
 908       in
 909       let candidates = get_candidates Unification table term in
 910       (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
 911       let r =
 912         if subterms_only then
 913           []
 914         else
 915           find_all_matches
 916             metasenv context ugraph lift_amount term termty candidates
 917       in
 918       r @ res, lifted_term
 919 ;;
 920
 921 (**
 922    superposition_right
 923    returns a list of new clauses inferred with a right superposition step
 924    between the positive equation "target" and one in the "table" "newmeta" is
 925    the first free meta index, i.e. the first number above the highest meta
 926    index: its updated value is also returned
 927 *)
 928 let superposition_right bag
 929   ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target=
 930   let module C = Cic in
 931   let module S = CicSubstitution in
 932   let module M = CicMetaSubst in
 933   let module HL = HelmLibraryObjects in
 934   let module CR = CicReduction in
 935   let module U = Utils in
 936   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 937     Equality.open_equality target
 938   in
 939   if Utils.debug_metas then
 940     ignore (check_target bag context target "superpositionright");
 941   let metasenv' = newmetas in
 942   let res1, res2 =
 943     match ordering with
 944     | U.Gt ->
 945         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
 946     | U.Lt ->
 947         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
 948     | _ ->
 949         let res l r =
 950           List.filter
 951             (fun (_, subst, _, _, _) ->
 952                let subst = apply_subst subst in
 953                let o = !Utils.compare_terms (subst l) (subst r) in
 954                o <> U.Lt && o <> U.Le)
 955             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
 956         in
 957         (res left right), (res right left)
 958   in
 959   let build_new bag ordering (bo, s, m, ug, eq_found) =
 960     if Utils.debug_metas then
 961       ignore (check_target bag context (snd eq_found) "buildnew1" );
 962
 963     let pos, equality =  eq_found in
 964     let (_, proof', (ty, what, other, _), menv',id') =
 965       Equality.open_equality  equality in
 966     let what, other = if pos = Utils.Left then what, other else other, what in
 967
 968     let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
 969     let newgoal, newproof =
 970       (* qua *)
 971       let bo' =
 972         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
 973       in
 974       let name = C.Name "x" in
 975       let bo'' =
 976         let l, r =
 977           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 978         C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 979       in
 980       bo',
 981         Equality.Step
 982           (s,(Equality.SuperpositionRight,
 983                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
 984     in
 985     let bag, newequality =
 986       let left, right =
 987         if ordering = U.Gt then newgoal, apply_subst s right
 988         else apply_subst s left, newgoal in
 989       let neworder = !Utils.compare_terms left right in
 990       let newmenv = (* Founif.filter s *) m in
 991       let stat = (eq_ty, left, right, neworder) in
 992       let bag, eq' =
 993         let w = Utils.compute_equality_weight stat in
 994         Equality.mk_equality bag (w, newproof, stat, newmenv) in
 995       if Utils.debug_metas then
 996         ignore (check_target bag context eq' "buildnew3");
 997       let bag, eq' = Equality.fix_metas bag eq' in
 998       if Utils.debug_metas then
 999         ignore (check_target bag context eq' "buildnew4");
1000       bag, eq'
1001     in
1002     if Utils.debug_metas then
1003       ignore(check_target bag context newequality "buildnew2");
1004     bag, newequality
1005   in
1006   let bag, new1 =
1007     List.fold_right
1008       (fun x (bag,acc) ->
1009         let bag, e = build_new bag U.Gt x in
1010         bag, e::acc) res1 (bag,[])
1011   in
1012   let bag, new2 =
1013     List.fold_right
1014       (fun x (bag,acc) ->
1015         let bag, e = build_new bag U.Lt x in
1016         bag, e::acc) res2 (bag,[])
1017   in
1018   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1019   bag, List.filter ok (new1 @ new2)
1020 ;;
1021
1022 (** demodulation, when the target is a theorem *)
1023 let rec demodulation_theorem bag env table theorem =
1024   let module C = Cic in
1025   let module S = CicSubstitution in
1026   let module M = CicMetaSubst in
1027   let module HL = HelmLibraryObjects in
1028   let eq_uri =
1029     match LibraryObjects.eq_URI() with
1030     | Some u -> u
1031     | None -> assert false in
1032   let metasenv, context, ugraph = env in
1033   let proof, theo, metas = theorem in
1034   let build_newtheorem (t, subst, menv, ug, eq_found) =
1035     let pos, equality = eq_found in
1036     let (_, proof', (ty, what, other, _), menv',id) =
1037       Equality.open_equality equality in
1038     let peq =
1039       match proof' with
1040       | Equality.Exact p -> p
1041       | _ -> assert false in
1042     let what, other =
1043       if pos = Utils.Left then what, other else other, what in
1044     let newtheo = apply_subst subst (S.subst other t) in
1045     let name = C.Name "x" in
1046     let body = apply_subst subst t in
1047     let pred = C.Lambda(name,ty,body) in
1048     let newproof =
1049       match pos with
1050         | Utils.Left ->
1051           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1052         | Utils.Right ->
1053           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1054     in
1055     newproof,newtheo
1056   in
1057   let res = demodulation_aux bag metas context ugraph table 0 theo in
1058   match res with
1059   | Some t ->
1060       let newproof, newtheo = build_newtheorem t in
1061       if Equality.meta_convertibility theo newtheo then
1062         newproof, newtheo
1063       else
1064         demodulation_theorem bag env table (newproof,newtheo,[])
1065   | None ->
1066       proof,theo
1067 ;;
1068
1069 (*****************************************************************************)
1070 (**                         OPERATIONS ON GOALS                             **)
1071 (**                                                                         **)
1072 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
1073 (*****************************************************************************)
1074
1075 (* new: demodulation of non_equality terms *)
1076 let build_newg bag context goal rule expansion =
1077   let goalproof,_,_ = goal in
1078   let (t,subst,menv,ug,eq_found) = expansion in
1079   let pos, equality = eq_found in
1080   let (_, proof', (ty, what, other, _), menv',id) =
1081     Equality.open_equality equality in
1082   let what, other = if pos = Utils.Left then what, other else other, what in
1083   let newterm, newgoalproof =
1084     let bo =
1085       Utils.guarded_simpl context
1086         (apply_subst subst (CicSubstitution.subst other t))
1087     in
1088     let name = Cic.Name "x" in
1089     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1090     let newgoalproofstep = (rule,pos,id,subst,pred) in
1091     bo, (newgoalproofstep::goalproof)
1092   in
1093   let newmetasenv = (* Founif.filter subst *) menv in
1094   (newgoalproof, newmetasenv, newterm)
1095 ;;
1096
1097 let rec demod bag env table goal =
1098   let _,menv,t = goal in
1099   let _, context, ugraph = env in
1100   let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:false)in
1101   match res with
1102     | Some newt ->
1103         let newg =
1104           build_newg bag context goal Equality.Demodulation newt
1105         in
1106         let _,_,newt = newg in
1107         if Equality.meta_convertibility t newt then
1108           false, goal
1109         else
1110           true, snd (demod bag env table newg)
1111     | None ->
1112         false, goal
1113 ;;
1114
1115 let open_goal g =
1116   match g with
1117   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
1118       (* assert (LibraryObjects.is_eq_URI uri); *)
1119       proof,menv,eq,ty,l,r
1120   | _ -> assert false
1121
1122 let ty_of_goal (_,_,ty) = ty ;;
1123
1124 (* checks if two goals are metaconvertible *)
1125 let goal_metaconvertibility_eq g1 g2 =
1126   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1127 ;;
1128
1129 (* when the betaexpand_term function is called on the left/right side of the
1130  * goal, the predicate has to be fixed
1131  * C[x] ---> (eq ty unchanged C[x])
1132  * [posu] is the side of the [unchanged] term in the original goal
1133  *)
1134
1135 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1136   let _,_,eq,ty,l,r = open_goal goal in
1137   let unchanged = if posu = Utils.Left then l else r in
1138   let unchanged = CicSubstitution.lift 1 unchanged in
1139   let ty = CicSubstitution.lift 1 ty in
1140   let pred =
1141     match posu with
1142     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1143     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1144   in
1145   (pred, subst, menv, ug, eq_f)
1146 ;;
1147
1148 (* ginve the old [goal], the side that has not changed [posu] and the
1149  * expansion builds a new goal *)
1150 let build_newgoal bag context goal posu rule expansion =
1151   let goalproof,_,_,_,_,_ = open_goal goal in
1152   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1153   let pos, equality = eq_found in
1154   let (_, proof', (ty, what, other, _), menv',id) =
1155     Equality.open_equality equality in
1156   let what, other = if pos = Utils.Left then what, other else other, what in
1157   let newterm, newgoalproof =
1158     let bo =
1159       Utils.guarded_simpl context
1160         (apply_subst subst (CicSubstitution.subst other t))
1161     in
1162     let name = Cic.Name "x" in
1163     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1164     let newgoalproofstep = (rule,pos,id,subst,pred) in
1165     bo, (newgoalproofstep::goalproof)
1166   in
1167   let newmetasenv = (* Founif.filter subst *) menv in
1168   (newgoalproof, newmetasenv, newterm)
1169 ;;
1170
1171 (**
1172    superposition_left
1173    returns a list of new clauses inferred with a left superposition step
1174    the negative equation "target" and one of the positive equations in "table"
1175 *)
1176 let superposition_left bag (metasenv, context, ugraph) table goal =
1177   let names = Utils.names_of_context context in
1178   let proof,menv,eq,ty,l,r = open_goal goal in
1179   let c = !Utils.compare_terms l r in
1180   let newgoals =
1181     if c = Utils.Incomparable then
1182       begin
1183       let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1184       let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1185       (* prerr_endline "incomparable";
1186       prerr_endline (string_of_int (List.length expansionsl));
1187       prerr_endline (string_of_int (List.length expansionsr));
1188       *)
1189       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1190       @
1191       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1192       end
1193     else
1194         match c with
1195         | Utils.Gt ->
1196             let big,small,possmall = l,r,Utils.Right in
1197             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1198             List.map
1199               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1200               expansions
1201         | Utils.Lt -> (* prerr_endline "LT"; *)
1202             let big,small,possmall = r,l,Utils.Left in
1203             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1204             List.map
1205               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1206               expansions
1207         | Utils.Eq -> []
1208         | _ ->
1209             prerr_endline
1210               ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1211             assert false
1212   in
1213   (* rinfresco le meta *)
1214   List.fold_right
1215     (fun g (b,acc) ->
1216        let b,g = Equality.fix_metas_goal b g in
1217        b,g::acc)
1218     newgoals (bag,[])
1219 ;;
1220
1221 (** demodulation, when the target is a goal *)
1222 let rec demodulation_goal bag env table goal =
1223   let goalproof,menv,_,_,left,right = open_goal goal in
1224   let _, context, ugraph = env in
1225 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
1226   let do_right () =
1227       let resright = demodulation_aux bag menv context ugraph table 0 right in
1228       match resright with
1229       | Some t ->
1230           let newg =
1231             build_newgoal bag context goal Utils.Left Equality.Demodulation t
1232           in
1233           if goal_metaconvertibility_eq goal newg then
1234             false, goal
1235           else
1236             true, snd (demodulation_goal bag env table newg)
1237       | None -> false, goal
1238   in
1239   let resleft = demodulation_aux bag menv context ugraph table 0 left in
1240   match resleft with
1241   | Some t ->
1242       let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1243       if goal_metaconvertibility_eq goal newg then
1244         do_right ()
1245       else
1246         true, snd (demodulation_goal bag env table newg)
1247   | None -> do_right ()
1248 ;;
1249
1250 (* returns all the 1 step demodulations *)
1251 module C = Cic;;
1252 module S = CicSubstitution;;
1253
1254 let rec demodulation_all_aux
1255   metasenv context ugraph table lift_amount term
1256 =
1257   let candidates =
1258     get_candidates ~env:(metasenv,context,ugraph) Matching table term
1259   in
1260   match term with
1261   | C.Meta _ -> []
1262   | _ ->
1263       let termty, ugraph = C.Implicit None, ugraph in
1264       let res =
1265         find_all_matches
1266           ~unif_fun:Founif.matching ~demod:true
1267             metasenv context ugraph lift_amount term termty candidates
1268       in
1269       match term with
1270       | C.Appl l ->
1271          let res, _, _, _ =
1272            List.fold_left
1273             (fun (res,b,l,r) t ->
1274                if not b then res,b,l,r
1275                else
1276                  let demods_for_t =
1277                    demodulation_all_aux
1278                      metasenv context ugraph table lift_amount t
1279                  in
1280                  let b = demods_for_t = [] in
1281                  res @
1282                    List.map
1283                     (fun (rel, s, m, ug, c) ->
1284                       (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1285                    demods_for_t, b, l@[List.hd r], List.tl r)
1286             (res, true, [], List.map (S.lift 1) l) l
1287          in
1288          res
1289       | t -> res
1290 ;;
1291
1292 let demod_all steps bag env table goal =
1293   let _, context, ugraph = env in
1294   let is_visited l (_,_,t) =
1295     List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
1296   in
1297   let rec aux steps visited nf bag = function
1298     | _ when steps = 0 -> visited, bag, nf
1299     | [] -> visited, bag, nf
1300     | goal :: rest when is_visited visited goal-> aux steps visited nf bag rest
1301     | goal :: rest ->
1302         let visited = goal :: visited in
1303         let _,menv,t = goal in
1304         let res = demodulation_all_aux menv context ugraph table 0 t in
1305         let steps = if res = [] then steps-1 else steps in
1306         let new_goals =
1307           List.map (build_newg bag context goal Equality.Demodulation) res
1308         in
1309         let nf = if new_goals = [] then goal :: nf else nf in
1310         aux steps visited nf bag (new_goals @ rest)
1311   in
1312   aux steps [] [] bag [goal]
1313 ;;
1314
1315 let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) =
1316   let proof,m,eq,ty,left,right = open_goal goal in
1317   let pl =
1318     List.map
1319       (fun (rule,pos,id,subst,pred) ->
1320         let pred =
1321           match pred with
1322           | Cic.Lambda (name,src,tgt) ->
1323               Cic.Lambda (name,src,
1324                 Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
1325           | _ -> assert false
1326         in
1327         rule,pos,id,subst,pred)
1328       pl
1329   in
1330   let pr =
1331     List.map
1332       (fun (rule,pos,id,subst,pred) ->
1333         let pred =
1334           match pred with
1335           | Cic.Lambda (name,src,tgt) ->
1336               Cic.Lambda (name,src,
1337                 Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
1338           | _ -> assert false
1339         in
1340         rule,pos,id,subst,pred)
1341       pr
1342   in
1343   (pr@pl@proof, m, Cic.Appl [eq;ty;l;r])
1344 ;;
1345
1346 let demodulation_all_goal bag env table goal maxnf =
1347   let proof,menv,eq,ty,left,right = open_goal goal in
1348   let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in
1349   let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in
1350   let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in
1351   let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in
1352   List.fold_left
1353     (fun acc (_,_,l as ld) ->
1354        List.fold_left
1355            (fun acc (_,_,r as rd) ->
1356                 combine_demodulation_proofs bag env goal ld rd :: acc)
1357          acc r_demod)
1358     [] l_demod
1359 ;;
1360
1361 let solve_demodulating bag env table initgoal steps =
1362   let proof,menv,eq,ty,left,right = open_goal initgoal in
1363   let uri =
1364     match eq with
1365     | Cic.MutInd (u,_,_) -> u
1366     | _ -> assert false
1367   in
1368   let _, context, ugraph = env in
1369   let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
1370   let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
1371   let is_solved left right ml mr =
1372     let m = ml @ (List.filter
1373       (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr)
1374     in
1375     try
1376       let s,_,_ =
1377         Founif.unification [] m context left right CicUniv.empty_ugraph in
1378       Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left))
1379     with CicUnification.UnificationFailure _ ->
1380       let solutions =
1381        unification_all env table (Equality.mk_tmp_equality
1382           (0,(Cic.Implicit None,left,right,Utils.Incomparable),m))
1383       in
1384       if solutions = [] then None
1385       else
1386         let s, e, swapped = List.hd solutions in
1387         let _,p,(ty,l,r,_),me,id = Equality.open_equality e in
1388         let bag, p =
1389           if swapped then Equality.symmetric bag ty l id uri me else bag, p
1390         in
1391         Some (bag, m,s, p)
1392   in
1393   let newgoal =
1394    HExtlib.list_findopt
1395      (fun (pr,mr,r) _ ->
1396          try
1397            let pl,ml,l,bag,m,s,p =
1398              match
1399              HExtlib.list_findopt (fun (pl,ml,l) _ ->
1400                match is_solved l r ml mr with
1401                | None -> None
1402                | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p)
1403              ) l_demod
1404              with Some x -> x | _ -> raise Not_found
1405            in
1406            let pl =
1407              List.map
1408                (fun (rule,pos,id,subst,pred) ->
1409                  let pred =
1410                    match pred with
1411                    | Cic.Lambda (name,src,tgt) ->
1412                        Cic.Lambda (name,src,
1413                          Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
1414                    | _ -> assert false
1415                  in
1416                  rule,pos,id,subst,pred)
1417                pl
1418            in
1419            let pr =
1420              List.map
1421                (fun (rule,pos,id,subst,pred) ->
1422                  let pred =
1423                    match pred with
1424                    | Cic.Lambda (name,src,tgt) ->
1425                        Cic.Lambda (name,src,
1426                          Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
1427                    | _ -> assert false
1428                  in
1429                  rule,pos,id,subst,pred)
1430                pr
1431            in
1432            Some (bag,pr@pl@proof,m,s,p)
1433          with Not_found -> None)
1434      r_demod
1435   in
1436   newgoal
1437 ;;
1438
1439
1440