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     let ty =
 727       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 728       with CicUtil.Meta_not_found _ -> ty
 729     in
 730     let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
 731     let what, other = if pos = Utils.Left then what, other else other, what in
 732     let newterm, newproof =
 733       let bo =
 734         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 735 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
 736       let name = C.Name "x" in
 737       let bo' =
 738         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 739           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 740       in
 741           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
 742           (Cic.Lambda (name, ty, bo'))))))
 743     in
 744     let newmenv = menv in
 745     let left, right = if is_left then newterm, right else left, newterm in
 746     let ordering = !Utils.compare_terms left right in
 747     let stat = (eq_ty, left, right, ordering) in
 748     let bag, res =
 749       let w = Utils.compute_equality_weight stat in
 750       Equality.mk_equality bag (w, newproof, stat,newmenv)
 751     in
 752     if Utils.debug_metas then
 753       ignore(check_target bag context res "buildnew_target output");
 754     bag, res
 755   in
 756   let res =
 757     demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
 758   in
 759   if Utils.debug_res then check_res res "demod result";
 760   let bag, newtarget =
 761     match res with
 762     | Some t ->
 763         let bag, newtarget = build_newtarget bag true t in
 764           (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
 765           if (Equality.is_weak_identity newtarget) (* || *)
 766             (*Equality.meta_convertibility_eq target newtarget*) then
 767               bag, newtarget
 768           else
 769             demodulation_equality bag ?from eq_uri env table newtarget
 770     | None ->
 771         let res = demodulation_aux bag metasenv' context ugraph table 0 right in
 772         if Utils.debug_res then check_res res "demod result 1";
 773           match res with
 774           | Some t ->
 775               let bag, newtarget = build_newtarget bag false t in
 776                 if (Equality.is_weak_identity newtarget) ||
 777                   (Equality.meta_convertibility_eq target newtarget) then
 778                     bag, newtarget
 779                 else
 780                    demodulation_equality bag ?from eq_uri env table newtarget
 781           | None ->
 782               bag, target
 783   in
 784   (* newmeta, newtarget *)
 785   bag, newtarget
 786 ;;
 787
 788 (**
 789    Performs the beta expansion of the term "term" w.r.t. "table",
 790    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 791    in table.
 792 *)
 793 let rec betaexpand_term
 794   ?(subterms_only=false) metasenv context ugraph table lift_amount term
 795 =
 796   let module C = Cic in
 797   let module S = CicSubstitution in
 798   let module M = CicMetaSubst in
 799   let module HL = HelmLibraryObjects in
 800
 801   let res, lifted_term =
 802     match term with
 803     | C.Meta (i, l) ->
 804         let l = [] in
 805         let l', lifted_l =
 806           List.fold_right
 807             (fun arg (res, lifted_tl) ->
 808                match arg with
 809                | Some arg ->
 810                    let arg_res, lifted_arg =
 811                      betaexpand_term metasenv context ugraph table
 812                        lift_amount arg in
 813                    let l1 =
 814                      List.map
 815                        (fun (t, s, m, ug, eq_found) ->
 816                           (Some t)::lifted_tl, s, m, ug, eq_found)
 817                        arg_res
 818                    in
 819                    (l1 @
 820                       (List.map
 821                          (fun (l, s, m, ug, eq_found) ->
 822                             (Some lifted_arg)::l, s, m, ug, eq_found)
 823                          res),
 824                     (Some lifted_arg)::lifted_tl)
 825                | None ->
 826                    (List.map
 827                       (fun (r, s, m, ug, eq_found) ->
 828                          None::r, s, m, ug, eq_found) res,
 829                     None::lifted_tl)
 830             ) l ([], [])
 831         in
 832         let e =
 833           List.map
 834             (fun (l, s, m, ug, eq_found) ->
 835                (C.Meta (i, l), s, m, ug, eq_found)) l'
 836         in
 837         e, C.Meta (i, lifted_l)
 838
 839     | C.Rel m ->
 840         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 841
 842     | C.Prod (nn, s, t) ->
 843         let l1, lifted_s =
 844           betaexpand_term metasenv context ugraph table lift_amount s in
 845         let l2, lifted_t =
 846           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 847             table (lift_amount+1) t in
 848         let l1' =
 849           List.map
 850             (fun (t, s, m, ug, eq_found) ->
 851                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 852         and l2' =
 853           List.map
 854             (fun (t, s, m, ug, eq_found) ->
 855                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 856         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 857
 858     | C.Lambda (nn, s, t) ->
 859         let l1, lifted_s =
 860           betaexpand_term metasenv context ugraph table lift_amount s in
 861         let l2, lifted_t =
 862           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 863             table (lift_amount+1) t in
 864         let l1' =
 865           List.map
 866             (fun (t, s, m, ug, eq_found) ->
 867                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 868         and l2' =
 869           List.map
 870             (fun (t, s, m, ug, eq_found) ->
 871                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 872         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 873
 874     | C.Appl l ->
 875         let l', lifted_l =
 876           List.fold_left
 877             (fun (res, lifted_tl) arg ->
 878                let arg_res, lifted_arg =
 879                  betaexpand_term metasenv context ugraph table lift_amount arg
 880                in
 881                let l1 =
 882                  List.map
 883                    (fun (a, s, m, ug, eq_found) ->
 884                       a::lifted_tl, s, m, ug, eq_found)
 885                    arg_res
 886                in
 887                (l1 @
 888                   (List.map
 889                      (fun (r, s, m, ug, eq_found) ->
 890                         lifted_arg::r, s, m, ug, eq_found)
 891                      res),
 892                 lifted_arg::lifted_tl)
 893             ) ([], []) (List.rev l)
 894         in
 895         (List.map
 896            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 897          C.Appl lifted_l)
 898
 899     | t -> [], (S.lift lift_amount t)
 900   in
 901   match term with
 902   | C.Meta (i, l) -> res, lifted_term
 903   | term ->
 904       let termty, ugraph =
 905        C.Implicit None, ugraph
 906 (*          CicTypeChecker.type_of_aux' metasenv context term ugraph  *)
 907       in
 908       let candidates = get_candidates Unification table term in
 909       (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
 910       let r =
 911         if subterms_only then
 912           []
 913         else
 914           find_all_matches
 915             metasenv context ugraph lift_amount term termty candidates
 916       in
 917       r @ res, lifted_term
 918 ;;
 919
 920 (**
 921    superposition_right
 922    returns a list of new clauses inferred with a right superposition step
 923    between the positive equation "target" and one in the "table" "newmeta" is
 924    the first free meta index, i.e. the first number above the highest meta
 925    index: its updated value is also returned
 926 *)
 927 let superposition_right bag
 928   ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target=
 929   let module C = Cic in
 930   let module S = CicSubstitution in
 931   let module M = CicMetaSubst in
 932   let module HL = HelmLibraryObjects in
 933   let module CR = CicReduction in
 934   let module U = Utils in
 935   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 936     Equality.open_equality target
 937   in
 938   if Utils.debug_metas then
 939     ignore (check_target bag context target "superpositionright");
 940   let metasenv' = newmetas in
 941   let res1, res2 =
 942     match ordering with
 943     | U.Gt ->
 944         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
 945     | U.Lt ->
 946         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
 947     | _ ->
 948         let res l r =
 949           List.filter
 950             (fun (_, subst, _, _, _) ->
 951                let subst = apply_subst subst in
 952                let o = !Utils.compare_terms (subst l) (subst r) in
 953                o <> U.Lt && o <> U.Le)
 954             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
 955         in
 956         (res left right), (res right left)
 957   in
 958   let build_new bag ordering (bo, s, m, ug, eq_found) =
 959     if Utils.debug_metas then
 960       ignore (check_target bag context (snd eq_found) "buildnew1" );
 961
 962     let pos, equality =  eq_found in
 963     let (_, proof', (ty, what, other, _), menv',id') =
 964       Equality.open_equality  equality in
 965     let what, other = if pos = Utils.Left then what, other else other, what in
 966
 967     let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
 968     let newgoal, newproof =
 969       (* qua *)
 970       let bo' =
 971         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
 972       in
 973       let name = C.Name "x" in
 974       let bo'' =
 975         let l, r =
 976           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 977         C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 978       in
 979       bo',
 980         Equality.Step
 981           (s,(Equality.SuperpositionRight,
 982                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
 983     in
 984     let bag, newequality =
 985       let left, right =
 986         if ordering = U.Gt then newgoal, apply_subst s right
 987         else apply_subst s left, newgoal in
 988       let neworder = !Utils.compare_terms left right in
 989       let newmenv = (* Founif.filter s *) m in
 990       let stat = (eq_ty, left, right, neworder) in
 991       let bag, eq' =
 992         let w = Utils.compute_equality_weight stat in
 993         Equality.mk_equality bag (w, newproof, stat, newmenv) in
 994       if Utils.debug_metas then
 995         ignore (check_target bag context eq' "buildnew3");
 996       let bag, eq' = Equality.fix_metas bag eq' in
 997       if Utils.debug_metas then
 998         ignore (check_target bag context eq' "buildnew4");
 999       bag, eq'
1000     in
1001     if Utils.debug_metas then
1002       ignore(check_target bag context newequality "buildnew2");
1003     bag, newequality
1004   in
1005   let bag, new1 =
1006     List.fold_right
1007       (fun x (bag,acc) ->
1008         let bag, e = build_new bag U.Gt x in
1009         bag, e::acc) res1 (bag,[])
1010   in
1011   let bag, new2 =
1012     List.fold_right
1013       (fun x (bag,acc) ->
1014         let bag, e = build_new bag U.Lt x in
1015         bag, e::acc) res2 (bag,[])
1016   in
1017   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1018   bag, List.filter ok (new1 @ new2)
1019 ;;
1020
1021 (** demodulation, when the target is a theorem *)
1022 let rec demodulation_theorem bag env table theorem =
1023   let module C = Cic in
1024   let module S = CicSubstitution in
1025   let module M = CicMetaSubst in
1026   let module HL = HelmLibraryObjects in
1027   let eq_uri =
1028     match LibraryObjects.eq_URI() with
1029     | Some u -> u
1030     | None -> assert false in
1031   let metasenv, context, ugraph = env in
1032   let proof, theo, metas = theorem in
1033   let build_newtheorem (t, subst, menv, ug, eq_found) =
1034     let pos, equality = eq_found in
1035     let (_, proof', (ty, what, other, _), menv',id) =
1036       Equality.open_equality equality in
1037     let peq =
1038       match proof' with
1039       | Equality.Exact p -> p
1040       | _ -> assert false in
1041     let what, other =
1042       if pos = Utils.Left then what, other else other, what in
1043     let newtheo = apply_subst subst (S.subst other t) in
1044     let name = C.Name "x" in
1045     let body = apply_subst subst t in
1046     let pred = C.Lambda(name,ty,body) in
1047     let newproof =
1048       match pos with
1049         | Utils.Left ->
1050           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1051         | Utils.Right ->
1052           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1053     in
1054     newproof,newtheo
1055   in
1056   let res = demodulation_aux bag metas context ugraph table 0 theo in
1057   match res with
1058   | Some t ->
1059       let newproof, newtheo = build_newtheorem t in
1060       if Equality.meta_convertibility theo newtheo then
1061         newproof, newtheo
1062       else
1063         demodulation_theorem bag env table (newproof,newtheo,[])
1064   | None ->
1065       proof,theo
1066 ;;
1067
1068 (*****************************************************************************)
1069 (**                         OPERATIONS ON GOALS                             **)
1070 (**                                                                         **)
1071 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
1072 (*****************************************************************************)
1073
1074 (* new: demodulation of non_equality terms *)
1075 let build_newg bag context goal rule expansion =
1076   let goalproof,_,_ = goal in
1077   let (t,subst,menv,ug,eq_found) = expansion in
1078   let pos, equality = eq_found in
1079   let (_, proof', (ty, what, other, _), menv',id) =
1080     Equality.open_equality equality in
1081   let what, other = if pos = Utils.Left then what, other else other, what in
1082   let newterm, newgoalproof =
1083     let bo =
1084       Utils.guarded_simpl context
1085         (apply_subst subst (CicSubstitution.subst other t))
1086     in
1087     let name = Cic.Name "x" in
1088     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1089     let newgoalproofstep = (rule,pos,id,subst,pred) in
1090     bo, (newgoalproofstep::goalproof)
1091   in
1092   let newmetasenv = (* Founif.filter subst *) menv in
1093   (newgoalproof, newmetasenv, newterm)
1094 ;;
1095
1096 let rec demod bag env table goal =
1097   let _,menv,t = goal in
1098   let _, context, ugraph = env in
1099   let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
1100   match res with
1101     | Some newt ->
1102         let newg =
1103           build_newg bag context goal Equality.Demodulation newt
1104         in
1105         let _,_,newt = newg in
1106         if Equality.meta_convertibility t newt then
1107           false, goal
1108         else
1109           true, snd (demod bag env table newg)
1110     | None ->
1111         false, goal
1112 ;;
1113
1114 let open_goal g =
1115   match g with
1116   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
1117       (* assert (LibraryObjects.is_eq_URI uri); *)
1118       proof,menv,eq,ty,l,r
1119   | _ -> assert false
1120
1121 let ty_of_goal (_,_,ty) = ty ;;
1122
1123 (* checks if two goals are metaconvertible *)
1124 let goal_metaconvertibility_eq g1 g2 =
1125   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1126 ;;
1127
1128 (* when the betaexpand_term function is called on the left/right side of the
1129  * goal, the predicate has to be fixed
1130  * C[x] ---> (eq ty unchanged C[x])
1131  * [posu] is the side of the [unchanged] term in the original goal
1132  *)
1133
1134 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1135   let _,_,eq,ty,l,r = open_goal goal in
1136   let unchanged = if posu = Utils.Left then l else r in
1137   let unchanged = CicSubstitution.lift 1 unchanged in
1138   let ty = CicSubstitution.lift 1 ty in
1139   let pred =
1140     match posu with
1141     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1142     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1143   in
1144   (pred, subst, menv, ug, eq_f)
1145 ;;
1146
1147 (* ginve the old [goal], the side that has not changed [posu] and the
1148  * expansion builds a new goal *)
1149 let build_newgoal bag context goal posu rule expansion =
1150   let goalproof,_,_,_,_,_ = open_goal goal in
1151   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1152   let pos, equality = eq_found in
1153   let (_, proof', (ty, what, other, _), menv',id) =
1154     Equality.open_equality equality in
1155   let what, other = if pos = Utils.Left then what, other else other, what in
1156   let newterm, newgoalproof =
1157     let bo =
1158       Utils.guarded_simpl context
1159         (apply_subst subst (CicSubstitution.subst other t))
1160     in
1161     let name = Cic.Name "x" in
1162     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1163     let newgoalproofstep = (rule,pos,id,subst,pred) in
1164     bo, (newgoalproofstep::goalproof)
1165   in
1166   let newmetasenv = (* Founif.filter subst *) menv in
1167   (newgoalproof, newmetasenv, newterm)
1168 ;;
1169
1170 (**
1171    superposition_left
1172    returns a list of new clauses inferred with a left superposition step
1173    the negative equation "target" and one of the positive equations in "table"
1174 *)
1175 let superposition_left bag (metasenv, context, ugraph) table goal =
1176   let names = Utils.names_of_context context in
1177   let proof,menv,eq,ty,l,r = open_goal goal in
1178   let c = !Utils.compare_terms l r in
1179   let newgoals =
1180     if c = Utils.Incomparable then
1181       begin
1182       let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1183       let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1184       (* prerr_endline "incomparable";
1185       prerr_endline (string_of_int (List.length expansionsl));
1186       prerr_endline (string_of_int (List.length expansionsr));
1187       *)
1188       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1189       @
1190       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1191       end
1192     else
1193         match c with
1194         | Utils.Gt ->
1195             let big,small,possmall = l,r,Utils.Right in
1196             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1197             List.map
1198               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1199               expansions
1200         | Utils.Lt -> (* prerr_endline "LT"; *)
1201             let big,small,possmall = r,l,Utils.Left in
1202             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1203             List.map
1204               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1205               expansions
1206         | Utils.Eq -> []
1207         | _ ->
1208             prerr_endline
1209               ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1210             assert false
1211   in
1212   (* rinfresco le meta *)
1213   List.fold_right
1214     (fun g (b,acc) ->
1215        let b,g = Equality.fix_metas_goal b g in
1216        b,g::acc)
1217     newgoals (bag,[])
1218 ;;
1219
1220 (** demodulation, when the target is a goal *)
1221 let rec demodulation_goal bag env table goal =
1222   let goalproof,menv,_,_,left,right = open_goal goal in
1223   let _, context, ugraph = env in
1224 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
1225   let do_right () =
1226       let resright = demodulation_aux bag menv context ugraph table 0 right in
1227       match resright with
1228       | Some t ->
1229           let newg =
1230             build_newgoal bag context goal Utils.Left Equality.Demodulation t
1231           in
1232           if goal_metaconvertibility_eq goal newg then
1233             false, goal
1234           else
1235             true, snd (demodulation_goal bag env table newg)
1236       | None -> false, goal
1237   in
1238   let resleft = demodulation_aux bag menv context ugraph table 0 left in
1239   match resleft with
1240   | Some t ->
1241       let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1242       if goal_metaconvertibility_eq goal newg then
1243         do_right ()
1244       else
1245         true, snd (demodulation_goal bag env table newg)
1246   | None -> do_right ()
1247 ;;
1248
1249 (* returns all the 1 step demodulations *)
1250 module C = Cic;;
1251 module S = CicSubstitution;;
1252 let rec demodulation_all_aux
1253   metasenv context ugraph table lift_amount term
1254 =
1255   let candidates =
1256     get_candidates ~env:(metasenv,context,ugraph) Matching table term
1257   in
1258   match term with
1259   | C.Meta _ -> []
1260   | _ ->
1261       let termty, ugraph = C.Implicit None, ugraph in
1262       let res =
1263         find_all_matches
1264           ~unif_fun:Founif.matching ~demod:true
1265             metasenv context ugraph lift_amount term termty candidates
1266       in
1267       match term with
1268       | C.Appl l ->
1269          let res, _, _ =
1270            List.fold_left
1271             (fun (res,l,r) t ->
1272                res @
1273                List.map
1274                  (fun (rel, s, m, ug, c) ->
1275                    (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1276                  (demodulation_all_aux
1277                    metasenv context ugraph table lift_amount t),
1278                l@[List.hd r], List.tl r)
1279             (res, [], List.map (S.lift 1) l) l
1280          in
1281          res
1282       | t -> res
1283 ;;
1284
1285 let demod_all steps bag env table goal =
1286   let _, context, ugraph = env in
1287   let is_visited l (_,_,t) =
1288     List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
1289   in
1290   let rec aux steps visited bag = function
1291     | _ when steps = 0 -> visited, bag, []
1292     | [] -> visited, bag, []
1293     | goal :: rest when is_visited visited goal -> aux steps visited bag rest
1294     | goal :: rest ->
1295         let visited = goal :: visited in
1296         let _,menv,t = goal in
1297         let res = demodulation_all_aux menv context ugraph table 0 t in
1298         let steps = if res = [] then steps-1 else steps in
1299         let new_goals =
1300           List.map (build_newg bag context goal Equality.Demodulation) res
1301         in
1302         let visited, bag, res = aux steps visited bag (new_goals @ rest) in
1303         visited, bag, goal :: res
1304   in
1305    aux steps [] bag [goal]
1306 ;;
1307
1308
1309 let solve_demodulating bag env table initgoal steps =
1310   let proof,menv,eq,ty,left,right = open_goal initgoal in
1311   let uri =
1312     match eq with
1313     | Cic.MutInd (u,_,_) -> u
1314     | _ -> assert false
1315   in
1316   let _, context, ugraph = env in
1317   let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
1318   let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
1319   let is_solved left right ml mr =
1320     let m = ml @ (List.filter
1321       (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr)
1322     in
1323     try
1324       let s,_,_ =
1325         Founif.unification [] m context left right CicUniv.empty_ugraph in
1326       Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left))
1327     with CicUnification.UnificationFailure _ ->
1328       let solutions =
1329        unification_all env table (Equality.mk_tmp_equality
1330           (0,(Cic.Implicit None,left,right,Utils.Incomparable),m))
1331       in
1332       if solutions = [] then None
1333       else
1334         let s, e, swapped = List.hd solutions in
1335         let _,p,(ty,l,r,_),me,id = Equality.open_equality e in
1336         let bag, p =
1337           if swapped then Equality.symmetric bag ty l id uri me else bag, p
1338         in
1339         Some (bag, m,s, p)
1340   in
1341   let newgoal =
1342    HExtlib.list_findopt
1343      (fun (pr,mr,r) _ ->
1344          try
1345            let pl,ml,l,bag,m,s,p =
1346              match
1347              HExtlib.list_findopt (fun (pl,ml,l) _ ->
1348                match is_solved l r ml mr with
1349                | None -> None
1350                | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p)
1351              ) l_demod
1352              with Some x -> x | _ -> raise Not_found
1353            in
1354            let pl =
1355              List.map
1356                (fun (rule,pos,id,subst,pred) ->
1357                  let pred =
1358                    match pred with
1359                    | Cic.Lambda (name,src,tgt) ->
1360                        Cic.Lambda (name,src,
1361                          Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
1362                    | _ -> assert false
1363                  in
1364                  rule,pos,id,subst,pred)
1365                pl
1366            in
1367            let pr =
1368              List.map
1369                (fun (rule,pos,id,subst,pred) ->
1370                  let pred =
1371                    match pred with
1372                    | Cic.Lambda (name,src,tgt) ->
1373                        Cic.Lambda (name,src,
1374                          Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
1375                    | _ -> assert false
1376                  in
1377                  rule,pos,id,subst,pred)
1378                pr
1379            in
1380            Some (bag,pr@pl@proof,m,s,p)
1381          with Not_found -> None)
1382      r_demod
1383   in
1384   newgoal
1385 ;;
1386
1387
1388