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.empty_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               prerr_endline ("extended context " ^ msg);
 168               prerr_endline (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             check_metasenv "founif :" metasenv';
 317             Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
 318           in
 319           let c, other =
 320             if pos = Utils.Left then left, right
 321             else right, left
 322           in
 323           if o <> U.Incomparable then
 324             let res =
 325               try
 326                 do_match c
 327               with Founif.MatchingFailure ->
 328                 find_matches bag metasenv context ugraph lift_amount term termty tl
 329             in
 330               if Utils.debug_res then ignore (check_res res "find1");
 331               res
 332           else
 333             let res =
 334               try do_match c
 335               with Founif.MatchingFailure -> None
 336             in
 337               if Utils.debug_res then ignore (check_res res "find2");
 338             match res with
 339             | Some (_, s, _, _, _) ->
 340                 let c' = apply_subst s c in
 341                 (*
 342              let other' = U.guarded_simpl context (apply_subst s other) in *)
 343                 let other' = apply_subst s other in
 344                 let order = cmp c' other' in
 345                 if order = U.Gt then
 346                   res
 347                 else
 348                   find_matches bag
 349                     metasenv context ugraph lift_amount term termty tl
 350             | None ->
 351                 find_matches bag metasenv context ugraph lift_amount term termty tl
 352 ;;
 353
 354 let find_matches metasenv context ugraph lift_amount term termty =
 355   find_matches metasenv context ugraph lift_amount term termty
 356 ;;
 357
 358 (*
 359   as above, but finds all the matching equalities, and the matching condition
 360   can be either Founif.matching or Inference.unification
 361 *)
 362 (* XXX termty unused *)
 363 let rec find_all_matches ?(unif_fun=Founif.unification)
 364     metasenv context ugraph lift_amount term termty =
 365   let module C = Cic in
 366   let module U = Utils in
 367   let module S = CicSubstitution in
 368   let module M = CicMetaSubst in
 369   let module HL = HelmLibraryObjects in
 370   let cmp = !Utils.compare_terms in
 371   let check = match termty with C.Implicit None -> false | _ -> true in
 372   function
 373     | [] -> []
 374     | candidate::tl ->
 375         let pos, equality = candidate in
 376         let (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in
 377         if check && not (fst (CicReduction.are_convertible
 378                                 ~metasenv context termty ty ugraph)) then (
 379           find_all_matches metasenv context ugraph lift_amount term termty tl
 380         ) else
 381         let do_match c =
 382           let subst', metasenv', ugraph' =
 383             unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
 384           in
 385           (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
 386         in
 387
 388         let c, other =
 389           if pos = Utils.Left then left, right
 390           else right, left
 391         in
 392         if o <> U.Incomparable then
 393           try
 394             let res = do_match c in
 395             res::(find_all_matches ~unif_fun metasenv context ugraph
 396                     lift_amount term termty tl)
 397           with
 398           | Founif.MatchingFailure
 399           | CicUnification.UnificationFailure _
 400           | CicUnification.Uncertain _ ->
 401               find_all_matches ~unif_fun metasenv context ugraph
 402                 lift_amount term termty tl
 403         else
 404           try
 405             let res = do_match c in
 406             match res with
 407             | _, s, _, _, _ ->
 408                 let c' = apply_subst s c
 409                 and other' = apply_subst s other in
 410                 let order = cmp c' other' in
 411                 if order <> U.Lt && order <> U.Le then
 412                   res::(find_all_matches ~unif_fun metasenv context ugraph
 413                           lift_amount term termty tl)
 414                 else
 415                   find_all_matches ~unif_fun metasenv context ugraph
 416                     lift_amount term termty tl
 417           with
 418           | Founif.MatchingFailure
 419           | CicUnification.UnificationFailure _
 420           | CicUnification.Uncertain _ ->
 421               find_all_matches ~unif_fun metasenv context ugraph
 422                 lift_amount term termty tl
 423 ;;
 424
 425 let find_all_matches
 426   ?unif_fun metasenv context ugraph lift_amount term termty l
 427 =
 428     find_all_matches
 429       ?unif_fun metasenv context ugraph lift_amount term termty l
 430   (*prerr_endline "CANDIDATES:";
 431   List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
 432   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
 433   (List.length rc));*)
 434 ;;
 435 (*
 436   returns true if target is subsumed by some equality in table
 437 *)
 438 (*
 439 let print_res l =
 440   prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
 441     ((pos,equation),_)) -> Equality.string_of_equality equation)l))
 442 ;;
 443 *)
 444
 445 let subsumption_aux use_unification env table target =
 446   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
 447   let _, context, ugraph = env in
 448   let metasenv = tmetas in
 449   let predicate, unif_fun =
 450     if use_unification then
 451       Unification, Founif.unification
 452     else
 453       Matching, Founif.matching
 454   in
 455   let leftr =
 456     match left with
 457     | Cic.Meta _ when not use_unification -> []
 458     | _ ->
 459         let leftc = get_candidates predicate table left in
 460         find_all_matches ~unif_fun
 461           metasenv context ugraph 0 left ty leftc
 462   in
 463   let rec ok what leftorright = function
 464     | [] -> None
 465     | (_, subst, menv, ug, (pos,equation))::tl ->
 466         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
 467         try
 468           let other = if pos = Utils.Left then r else l in
 469           let what' = Subst.apply_subst subst what in
 470           let other' = Subst.apply_subst subst other in
 471           let subst', menv', ug' =
 472             unif_fun metasenv m context what' other' ugraph
 473           in
 474           (match Subst.merge_subst_if_possible subst subst' with
 475           | None -> ok what leftorright tl
 476           | Some s -> Some (s, equation, leftorright <> pos ))
 477         with
 478         | Founif.MatchingFailure
 479         | CicUnification.UnificationFailure _ -> ok what leftorright tl
 480   in
 481   match ok right Utils.Left leftr with
 482   | Some _ as res -> res
 483   | None ->
 484       let rightr =
 485         match right with
 486           | Cic.Meta _ when not use_unification -> []
 487           | _ ->
 488               let rightc = get_candidates predicate table right in
 489                 find_all_matches ~unif_fun
 490                   metasenv context ugraph 0 right ty rightc
 491       in
 492         ok left Utils.Right rightr
 493 ;;
 494
 495 let subsumption x y z =
 496   subsumption_aux false x y z
 497 ;;
 498
 499 let unification x y z =
 500   subsumption_aux true x y z
 501 ;;
 502
 503 (* the target must be disjoint from the equations in the table *)
 504 let subsumption_aux_all use_unification env table target =
 505   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
 506   let _, context, ugraph = env in
 507   let metasenv = tmetas in
 508   check_for_duplicates metasenv "subsumption_aux_all";
 509   let predicate, unif_fun =
 510     if use_unification then
 511       Unification, Founif.unification
 512     else
 513       Matching, Founif.matching
 514   in
 515   let leftr =
 516     match left with
 517     | Cic.Meta _ (*when not use_unification*) -> []
 518     | _ ->
 519         let leftc = get_candidates predicate table left in
 520         find_all_matches ~unif_fun
 521           metasenv context ugraph 0 left ty leftc
 522   in
 523   let rightr =
 524         match right with
 525           | Cic.Meta _ (*when not use_unification*) -> []
 526           | _ ->
 527               let rightc = get_candidates predicate table right in
 528                 find_all_matches ~unif_fun
 529                   metasenv context ugraph 0 right ty rightc
 530   in
 531   let rec ok_all what leftorright = function
 532     | [] -> []
 533     | (_, subst, menv, ug, (pos,equation))::tl ->
 534         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
 535         try
 536           let other = if pos = Utils.Left then r else l in
 537           let what' = Subst.apply_subst subst what in
 538           let other' = Subst.apply_subst subst other in
 539           let subst', menv', ug' =
 540             unif_fun metasenv m context what' other' ugraph
 541           in
 542           (match Subst.merge_subst_if_possible subst subst' with
 543           | None -> ok_all what leftorright tl
 544           | Some s ->
 545               (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
 546         with
 547         | Founif.MatchingFailure
 548         | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
 549   in
 550   (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
 551 ;;
 552
 553 let subsumption_all x y z =
 554   subsumption_aux_all false x y z
 555 ;;
 556
 557 let unification_all x y z =
 558   subsumption_aux_all true x y z
 559 ;;
 560
 561 let rec demodulation_aux bag ?from ?(typecheck=false)
 562   metasenv context ugraph table lift_amount term =
 563   let module C = Cic in
 564   let module S = CicSubstitution in
 565   let module M = CicMetaSubst in
 566   let module HL = HelmLibraryObjects in
 567   (* prerr_endline ("demodulating " ^ CicPp.ppterm term); *)
 568   check_for_duplicates metasenv "in input a demodulation aux";
 569   let candidates =
 570     get_candidates
 571       ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
 572   in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates
 573   in
 574   let res =
 575     match term with
 576       | C.Meta _ -> None
 577       | term ->
 578           let res =
 579             try
 580               let termty, ugraph =
 581                 if typecheck then
 582                   CicTypeChecker.type_of_aux' metasenv context term ugraph
 583                 else
 584                   C.Implicit None, ugraph
 585               in
 586                 find_matches bag metasenv context ugraph
 587                   lift_amount term termty candidates
 588             with _ ->
 589               prerr_endline "type checking error";
 590               prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
 591               prerr_endline ("term: " ^ (CicPp.ppterm term));
 592               assert false;
 593               (* None *)
 594           in
 595           let res =
 596             (if Utils.debug_res then
 597             ignore(check_res res "demod1");
 598             if check_demod_res res metasenv "demod" then res else None) in
 599           if res <> None then
 600               res
 601             else
 602               match term with
 603                 | C.Appl l ->
 604                     let res, ll =
 605                       List.fold_left
 606                         (fun (res, tl) t ->
 607                            if res <> None then
 608                              (res, tl @ [S.lift 1 t])
 609                            else
 610                              let r =
 611                                demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck
 612                                  lift_amount t
 613                              in
 614                                match r with
 615                                  | None -> (None, tl @ [S.lift 1 t])
 616                                  | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 617                         (None, []) l
 618                     in (
 619                         match res with
 620                           | None -> None
 621                           | Some (_, subst, menv, ug, eq_found) ->
 622                               Some (C.Appl ll, subst, menv, ug, eq_found)
 623                       )
 624 (*
 625                 | C.Prod (nn, s, t) ->
 626                     let r1 =
 627                       demodulation_aux bag ~from:"2"
 628                         metasenv context ugraph table lift_amount s in (
 629                         match r1 with
 630                           | None ->
 631                               let r2 =
 632                                 demodulation_aux bag metasenv
 633                                   ((Some (nn, C.Decl s))::context) ugraph
 634                                   table (lift_amount+1) t
 635                               in (
 636                                   match r2 with
 637                                     | None -> None
 638                                     | Some (t', subst, menv, ug, eq_found) ->
 639                                         Some (C.Prod (nn, (S.lift 1 s), t'),
 640                                               subst, menv, ug, eq_found)
 641                                 )
 642                           | Some (s', subst, menv, ug, eq_found) ->
 643                               Some (C.Prod (nn, s', (S.lift 1 t)),
 644                                     subst, menv, ug, eq_found)
 645                       )
 646                 | C.Lambda (nn, s, t) ->
 647                     prerr_endline "siam qui";
 648                     let r1 =
 649                       demodulation_aux bag
 650                         metasenv context ugraph table lift_amount s in (
 651                         match r1 with
 652                           | None ->
 653                               let r2 =
 654                                 demodulation_aux bag metasenv
 655                                   ((Some (nn, C.Decl s))::context) ugraph
 656                                   table (lift_amount+1) t
 657                               in (
 658                                   match r2 with
 659                                     | None -> None
 660                                     | Some (t', subst, menv, ug, eq_found) ->
 661                                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 662                                               subst, menv, ug, eq_found)
 663                                 )
 664                           | Some (s', subst, menv, ug, eq_found) ->
 665                               Some (C.Lambda (nn, s', (S.lift 1 t)),
 666                                     subst, menv, ug, eq_found)
 667                       )
 668 *)
 669                 | t ->
 670                     None
 671   in
 672   if Utils.debug_res then ignore(check_res res "demod_aux output");
 673   res
 674 ;;
 675
 676 exception Foo
 677
 678 (** demodulation, when target is an equality *)
 679 let rec demodulation_equality bag ?from eq_uri newmeta env table target =
 680         (*
 681           prerr_endline ("demodulation_eq:\n");
 682         Index.iter table (fun l ->
 683           let l = Index.PosEqSet.elements l in
 684           let l =
 685             List.map (fun (p,e) ->
 686               Utils.string_of_pos p ^ Equality.string_of_equality e) l in
 687           prerr_endline (String.concat "\n" l)
 688           );
 689           *)
 690   let module C = Cic in
 691   let module S = CicSubstitution in
 692   let module M = CicMetaSubst in
 693   let module HL = HelmLibraryObjects in
 694   let module U = Utils in
 695   let metasenv, context, ugraph = env in
 696   let w, proof, (eq_ty, left, right, order), metas, id =
 697     Equality.open_equality target
 698   in
 699   (* first, we simplify *)
 700 (*   let right = U.guarded_simpl context right in *)
 701 (*   let left = U.guarded_simpl context left in *)
 702 (*   let order = !Utils.compare_terms left right in *)
 703 (*   let stat = (eq_ty, left, right, order) in  *)
 704 (*  let w = Utils.compute_equality_weight stat in*)
 705   (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
 706   if Utils.debug_metas then
 707     ignore(check_target bag context target "demod equalities input");
 708   let metasenv' = (* metasenv @ *) metas in
 709   let maxmeta = ref newmeta in
 710
 711   let build_newtarget is_left (t, subst, menv, ug, eq_found) =
 712
 713     if Utils.debug_metas then
 714       begin
 715         ignore(check_for_duplicates menv "input1");
 716         ignore(check_disjoint_invariant subst menv "input2");
 717         let substs = Subst.ppsubst subst in
 718         ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
 719       end;
 720     let pos, equality = eq_found in
 721     let (_, proof',
 722         (ty, what, other, _), menv',id') = Equality.open_equality equality in
 723     let ty =
 724       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 725       with CicUtil.Meta_not_found _ -> ty
 726     in
 727     let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
 728     let what, other = if pos = Utils.Left then what, other else other, what in
 729     let newterm, newproof =
 730       let bo =
 731         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 732 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
 733       let name = C.Name "x" in
 734       let bo' =
 735         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 736           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 737       in
 738           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
 739           (Cic.Lambda (name, ty, bo'))))))
 740     in
 741     let newmenv = menv in
 742     let left, right = if is_left then newterm, right else left, newterm in
 743     let ordering = !Utils.compare_terms left right in
 744     let stat = (eq_ty, left, right, ordering) in
 745     let res =
 746       let w = Utils.compute_equality_weight stat in
 747           (Equality.mk_equality bag (w, newproof, stat,newmenv))
 748     in
 749     if Utils.debug_metas then
 750       ignore(check_target bag context res "buildnew_target output");
 751     !maxmeta, res
 752   in
 753
 754   let res =
 755     demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
 756   in
 757   if Utils.debug_res then check_res res "demod result";
 758   let newmeta, newtarget =
 759     match res with
 760     | Some t ->
 761         let newmeta, newtarget = build_newtarget true t in
 762           (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
 763           if (Equality.is_weak_identity newtarget) (* || *)
 764             (*Equality.meta_convertibility_eq target newtarget*) then
 765               newmeta, newtarget
 766           else
 767             demodulation_equality bag ?from eq_uri newmeta env table newtarget
 768     | None ->
 769         let res = demodulation_aux bag metasenv' context ugraph table 0 right in
 770         if Utils.debug_res then check_res res "demod result 1";
 771           match res with
 772           | Some t ->
 773               let newmeta, newtarget = build_newtarget false t in
 774                 if (Equality.is_weak_identity newtarget) ||
 775                   (Equality.meta_convertibility_eq target newtarget) then
 776                     newmeta, newtarget
 777                 else
 778                    demodulation_equality bag ?from eq_uri newmeta env table newtarget
 779           | None ->
 780               newmeta, target
 781   in
 782   (* newmeta, newtarget *)
 783   newmeta,newtarget
 784 ;;
 785
 786 (**
 787    Performs the beta expansion of the term "term" w.r.t. "table",
 788    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 789    in table.
 790 *)
 791 let rec betaexpand_term
 792   ?(subterms_only=false) metasenv context ugraph table lift_amount term
 793 =
 794   let module C = Cic in
 795   let module S = CicSubstitution in
 796   let module M = CicMetaSubst in
 797   let module HL = HelmLibraryObjects in
 798
 799   let res, lifted_term =
 800     match term with
 801     | C.Meta (i, l) ->
 802         let l = [] in
 803         let l', lifted_l =
 804           List.fold_right
 805             (fun arg (res, lifted_tl) ->
 806                match arg with
 807                | Some arg ->
 808                    let arg_res, lifted_arg =
 809                      betaexpand_term metasenv context ugraph table
 810                        lift_amount arg in
 811                    let l1 =
 812                      List.map
 813                        (fun (t, s, m, ug, eq_found) ->
 814                           (Some t)::lifted_tl, s, m, ug, eq_found)
 815                        arg_res
 816                    in
 817                    (l1 @
 818                       (List.map
 819                          (fun (l, s, m, ug, eq_found) ->
 820                             (Some lifted_arg)::l, s, m, ug, eq_found)
 821                          res),
 822                     (Some lifted_arg)::lifted_tl)
 823                | None ->
 824                    (List.map
 825                       (fun (r, s, m, ug, eq_found) ->
 826                          None::r, s, m, ug, eq_found) res,
 827                     None::lifted_tl)
 828             ) l ([], [])
 829         in
 830         let e =
 831           List.map
 832             (fun (l, s, m, ug, eq_found) ->
 833                (C.Meta (i, l), s, m, ug, eq_found)) l'
 834         in
 835         e, C.Meta (i, lifted_l)
 836
 837     | C.Rel m ->
 838         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 839
 840     | C.Prod (nn, s, t) ->
 841         let l1, lifted_s =
 842           betaexpand_term metasenv context ugraph table lift_amount s in
 843         let l2, lifted_t =
 844           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 845             table (lift_amount+1) t in
 846         let l1' =
 847           List.map
 848             (fun (t, s, m, ug, eq_found) ->
 849                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 850         and l2' =
 851           List.map
 852             (fun (t, s, m, ug, eq_found) ->
 853                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 854         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 855
 856     | C.Lambda (nn, s, t) ->
 857         let l1, lifted_s =
 858           betaexpand_term metasenv context ugraph table lift_amount s in
 859         let l2, lifted_t =
 860           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 861             table (lift_amount+1) t in
 862         let l1' =
 863           List.map
 864             (fun (t, s, m, ug, eq_found) ->
 865                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 866         and l2' =
 867           List.map
 868             (fun (t, s, m, ug, eq_found) ->
 869                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 870         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 871
 872     | C.Appl l ->
 873         let l', lifted_l =
 874           List.fold_left
 875             (fun (res, lifted_tl) arg ->
 876                let arg_res, lifted_arg =
 877                  betaexpand_term metasenv context ugraph table lift_amount arg
 878                in
 879                let l1 =
 880                  List.map
 881                    (fun (a, s, m, ug, eq_found) ->
 882                       a::lifted_tl, s, m, ug, eq_found)
 883                    arg_res
 884                in
 885                (l1 @
 886                   (List.map
 887                      (fun (r, s, m, ug, eq_found) ->
 888                         lifted_arg::r, s, m, ug, eq_found)
 889                      res),
 890                 lifted_arg::lifted_tl)
 891             ) ([], []) (List.rev l)
 892         in
 893         (List.map
 894            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 895          C.Appl lifted_l)
 896
 897     | t -> [], (S.lift lift_amount t)
 898   in
 899   match term with
 900   | C.Meta (i, l) -> res, lifted_term
 901   | term ->
 902       let termty, ugraph =
 903 (*        C.Implicit None, ugraph *)
 904          CicTypeChecker.type_of_aux' metasenv context term ugraph
 905       in
 906       let candidates = get_candidates Unification table term in
 907       let r =
 908         if subterms_only then
 909           []
 910         else
 911           find_all_matches
 912             metasenv context ugraph lift_amount term termty candidates
 913       in
 914       r @ res, lifted_term
 915 ;;
 916
 917 (**
 918    superposition_right
 919    returns a list of new clauses inferred with a right superposition step
 920    between the positive equation "target" and one in the "table" "newmeta" is
 921    the first free meta index, i.e. the first number above the highest meta
 922    index: its updated value is also returned
 923 *)
 924 let superposition_right bag
 925   ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
 926   let module C = Cic in
 927   let module S = CicSubstitution in
 928   let module M = CicMetaSubst in
 929   let module HL = HelmLibraryObjects in
 930   let module CR = CicReduction in
 931   let module U = Utils in
 932   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 933     Equality.open_equality target
 934   in
 935   if Utils.debug_metas then
 936     ignore (check_target bag context target "superpositionright");
 937   let metasenv' = newmetas in
 938   let maxmeta = ref newmeta in
 939   let res1, res2 =
 940     match ordering with
 941     | U.Gt ->
 942         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
 943     | U.Lt ->
 944         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
 945     | _ ->
 946         let res l r =
 947           List.filter
 948             (fun (_, subst, _, _, _) ->
 949                let subst = apply_subst subst in
 950                let o = !Utils.compare_terms (subst l) (subst r) in
 951                o <> U.Lt && o <> U.Le)
 952             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
 953         in
 954         (res left right), (res right left)
 955   in
 956   let build_new ordering (bo, s, m, ug, eq_found) =
 957     if Utils.debug_metas then
 958       ignore (check_target bag context (snd eq_found) "buildnew1" );
 959
 960     let pos, equality =  eq_found in
 961     let (_, proof', (ty, what, other, _), menv',id') =
 962       Equality.open_equality  equality in
 963     let what, other = if pos = Utils.Left then what, other else other, what in
 964
 965     let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
 966     let newgoal, newproof =
 967       (* qua *)
 968       let bo' =
 969         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
 970       in
 971       let name = C.Name "x" in
 972       let bo'' =
 973         let l, r =
 974           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 975         C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 976       in
 977       bo',
 978         Equality.Step
 979           (s,(Equality.SuperpositionRight,
 980                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
 981     in
 982     let newmeta, newequality =
 983       let left, right =
 984         if ordering = U.Gt then newgoal, apply_subst s right
 985         else apply_subst s left, newgoal in
 986       let neworder = !Utils.compare_terms left right in
 987       let newmenv = (* Founif.filter s *) m in
 988       let stat = (eq_ty, left, right, neworder) in
 989       let eq' =
 990         let w = Utils.compute_equality_weight stat in
 991         Equality.mk_equality bag (w, newproof, stat, newmenv) in
 992       if Utils.debug_metas then
 993         ignore (check_target bag context eq' "buildnew3");
 994       let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
 995       if Utils.debug_metas then
 996         ignore (check_target bag context eq' "buildnew4");
 997       newm, eq'
 998     in
 999     maxmeta := newmeta;
1000     if Utils.debug_metas then
1001       ignore(check_target bag context newequality "buildnew2");
1002     newequality
1003   in
1004   let new1 = List.map (build_new U.Gt) res1
1005   and new2 = List.map (build_new U.Lt) res2 in
1006   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1007   (!maxmeta,
1008    (List.filter ok (new1 @ new2)))
1009 ;;
1010
1011 (** demodulation, when the target is a theorem *)
1012 let rec demodulation_theorem bag env table theorem =
1013   let module C = Cic in
1014   let module S = CicSubstitution in
1015   let module M = CicMetaSubst in
1016   let module HL = HelmLibraryObjects in
1017   let eq_uri =
1018     match LibraryObjects.eq_URI() with
1019     | Some u -> u
1020     | None -> assert false in
1021   let metasenv, context, ugraph = env in
1022   let proof, theo, metas = theorem in
1023   let build_newtheorem (t, subst, menv, ug, eq_found) =
1024     let pos, equality = eq_found in
1025     let (_, proof', (ty, what, other, _), menv',id) =
1026       Equality.open_equality equality in
1027     let peq =
1028       match proof' with
1029       | Equality.Exact p -> p
1030       | _ -> assert false in
1031     let what, other =
1032       if pos = Utils.Left then what, other else other, what in
1033     let newtheo = apply_subst subst (S.subst other t) in
1034     let name = C.Name "x" in
1035     let body = apply_subst subst t in
1036     let pred = C.Lambda(name,ty,body) in
1037     let newproof =
1038       match pos with
1039         | Utils.Left ->
1040           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1041         | Utils.Right ->
1042           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1043     in
1044     newproof,newtheo
1045   in
1046   let res = demodulation_aux bag metas context ugraph table 0 theo in
1047   match res with
1048   | Some t ->
1049       let newproof, newtheo = build_newtheorem t in
1050       if Equality.meta_convertibility theo newtheo then
1051         newproof, newtheo
1052       else
1053         demodulation_theorem bag env table (newproof,newtheo,[])
1054   | None ->
1055       proof,theo
1056 ;;
1057
1058 (*****************************************************************************)
1059 (**                         OPERATIONS ON GOALS                             **)
1060 (**                                                                         **)
1061 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
1062 (*****************************************************************************)
1063
1064 (* new: demodulation of non_equality terms *)
1065 let build_newg bag context goal rule expansion =
1066   let goalproof,_,_ = goal in
1067   let (t,subst,menv,ug,eq_found) = expansion in
1068   let pos, equality = eq_found in
1069   let (_, proof', (ty, what, other, _), menv',id) =
1070     Equality.open_equality equality in
1071   let what, other = if pos = Utils.Left then what, other else other, what in
1072   let newterm, newgoalproof =
1073     let bo =
1074       Utils.guarded_simpl context
1075         (apply_subst subst (CicSubstitution.subst other t))
1076     in
1077     let bo' = apply_subst subst t in
1078     let ty = apply_subst subst ty in
1079     let name = Cic.Name "x" in
1080     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1081     bo, (newgoalproofstep::goalproof)
1082   in
1083   let newmetasenv = (* Founif.filter subst *) menv in
1084   (newgoalproof, newmetasenv, newterm)
1085 ;;
1086
1087 let rec demod bag env table goal =
1088   let goalproof,menv,t = goal in
1089   let _, context, ugraph = env in
1090   let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
1091   match res with
1092     | Some newt ->
1093         let newg =
1094           build_newg bag context goal Equality.Demodulation newt
1095         in
1096         let _,_,newt = newg in
1097         if Equality.meta_convertibility t newt then
1098           false, goal
1099         else
1100           true, snd (demod bag env table newg)
1101     | None ->
1102         false, goal
1103 ;;
1104
1105 let open_goal g =
1106   match g with
1107   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
1108       (* assert (LibraryObjects.is_eq_URI uri); *)
1109       proof,menv,eq,ty,l,r
1110   | _ -> assert false
1111
1112 let ty_of_goal (_,_,ty) = ty ;;
1113
1114 (* checks if two goals are metaconvertible *)
1115 let goal_metaconvertibility_eq g1 g2 =
1116   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1117 ;;
1118
1119 (* when the betaexpand_term function is called on the left/right side of the
1120  * goal, the predicate has to be fixed
1121  * C[x] ---> (eq ty unchanged C[x])
1122  * [posu] is the side of the [unchanged] term in the original goal
1123  *)
1124
1125 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1126   let _,_,eq,ty,l,r = open_goal goal in
1127   let unchanged = if posu = Utils.Left then l else r in
1128   let unchanged = CicSubstitution.lift 1 unchanged in
1129   let ty = CicSubstitution.lift 1 ty in
1130   let pred =
1131     match posu with
1132     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1133     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1134   in
1135   (pred, subst, menv, ug, eq_f)
1136 ;;
1137
1138 (* ginve the old [goal], the side that has not changed [posu] and the
1139  * expansion builds a new goal *)
1140 let build_newgoal bag context goal posu rule expansion =
1141   let goalproof,_,_,_,_,_ = open_goal goal in
1142   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1143   let pos, equality = eq_found in
1144   let (_, proof', (ty, what, other, _), menv',id) =
1145     Equality.open_equality equality in
1146   let what, other = if pos = Utils.Left then what, other else other, what in
1147   let newterm, newgoalproof =
1148     let bo =
1149       Utils.guarded_simpl context
1150         (apply_subst subst (CicSubstitution.subst other t))
1151     in
1152     let bo' = apply_subst subst t in
1153     let ty = apply_subst subst ty in
1154     let name = Cic.Name "x" in
1155     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1156     bo, (newgoalproofstep::goalproof)
1157   in
1158   let newmetasenv = (* Founif.filter subst *) menv in
1159   (newgoalproof, newmetasenv, newterm)
1160 ;;
1161
1162 (**
1163    superposition_left
1164    returns a list of new clauses inferred with a left superposition step
1165    the negative equation "target" and one of the positive equations in "table"
1166 *)
1167 let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
1168   let names = Utils.names_of_context context in
1169   let proof,menv,eq,ty,l,r = open_goal goal in
1170   let c = !Utils.compare_terms l r in
1171   let newgoals =
1172     if c = Utils.Incomparable then
1173       begin
1174       let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1175       let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1176       (* prerr_endline "incomparable";
1177       prerr_endline (string_of_int (List.length expansionsl));
1178       prerr_endline (string_of_int (List.length expansionsr));
1179       *)
1180       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1181       @
1182       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1183       end
1184     else
1185         match c with
1186         | Utils.Gt -> (* prerr_endline "GT"; *)
1187             let big,small,possmall = l,r,Utils.Right in
1188             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1189             List.map
1190               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1191               expansions
1192         | Utils.Lt -> (* prerr_endline "LT"; *)
1193             let big,small,possmall = r,l,Utils.Left in
1194             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1195             List.map
1196               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1197               expansions
1198         | Utils.Eq -> []
1199         | _ ->
1200             prerr_endline
1201               ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1202             assert false
1203   in
1204   (* rinfresco le meta *)
1205   List.fold_right
1206     (fun g (max,acc) ->
1207        let max,g = Equality.fix_metas_goal max g in max,g::acc)
1208     newgoals (maxmeta,[])
1209 ;;
1210
1211 (** demodulation, when the target is a goal *)
1212 let rec demodulation_goal bag env table goal =
1213   let goalproof,menv,_,_,left,right = open_goal goal in
1214   let _, context, ugraph = env in
1215 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
1216   let do_right () =
1217       let resright = demodulation_aux bag menv context ugraph table 0 right in
1218       match resright with
1219       | Some t ->
1220           let newg =
1221             build_newgoal bag context goal Utils.Left Equality.Demodulation t
1222           in
1223           if goal_metaconvertibility_eq goal newg then
1224             false, goal
1225           else
1226             true, snd (demodulation_goal bag env table newg)
1227       | None -> false, goal
1228   in
1229   let resleft = demodulation_aux bag menv context ugraph table 0 left in
1230   match resleft with
1231   | Some t ->
1232       let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1233       if goal_metaconvertibility_eq goal newg then
1234         do_right ()
1235       else
1236         true, snd (demodulation_goal bag env table newg)
1237   | None -> do_right ()
1238 ;;
1239
1240 type next = L | R
1241 type solved = Yes of Equality.goal | No of Equality.goal list
1242
1243 (* returns all the 1 step demodulations *)
1244 module C = Cic;;
1245 module S = CicSubstitution;;
1246 let rec demodulation_all_aux
1247   metasenv context ugraph table lift_amount term
1248 =
1249   let candidates =
1250     get_candidates ~env:(metasenv,context,ugraph) Matching table term
1251   in
1252   match term with
1253   | C.Meta _ -> []
1254   | _ ->
1255       let termty, ugraph = C.Implicit None, ugraph in
1256       let res =
1257         find_all_matches
1258           metasenv context ugraph lift_amount term termty candidates
1259       in
1260       match term with
1261       | C.Appl l ->
1262          let res, _, _ =
1263            List.fold_left
1264             (fun (res,l,r) t ->
1265                res @
1266                List.map
1267                  (fun (rel, s, m, ug, c) ->
1268                    (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1269                  (demodulation_all_aux
1270                    metasenv context ugraph table lift_amount t),
1271                l@[List.hd r], List.tl r)
1272             (res, [], List.map (S.lift 1) l) l
1273          in
1274          res
1275       | C.Prod (nn, s, t)
1276       | C.Lambda (nn, s, t) ->
1277           let context = (Some (nn, C.Decl s))::context in
1278           let mk s t =
1279             match term with
1280             | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
1281           in
1282           res @
1283           List.map
1284             (fun (rel, subst, m, ug, c) ->
1285                mk (S.lift 1 s) rel, subst, m, ug, c)
1286             (demodulation_all_aux
1287               metasenv context ugraph table (lift_amount+1) t)
1288               (* we could demodulate also in s, but then t may be badly
1289                * typed... *)
1290       | t -> res
1291 ;;
1292
1293 let solve_demodulating bag env table initgoal steps =
1294   let _, context, ugraph = env in
1295   let solved goal res side =
1296     let newg = build_newgoal bag context goal side Equality.Demodulation res in
1297     match newg with
1298     | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right])
1299       when LibraryObjects.is_eq_URI uri ->
1300         (try
1301           let _ =
1302             Founif.unification m m context left right CicUniv.empty_ugraph
1303           in
1304           Yes newg
1305         with CicUnification.UnificationFailure _ -> No [newg])
1306     | _ -> No [newg]
1307   in
1308   let solved goal res_list side =
1309     let newg = List.map (fun x -> solved goal x side) res_list in
1310     try
1311       List.find (function Yes _ -> true | _ -> false) newg
1312     with Not_found ->
1313       No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
1314   in
1315   let rec first f l =
1316     match l with
1317     | [] -> None
1318     | x::tl ->
1319        match f x with
1320        | None -> first f tl
1321        | Some x as ok -> ok
1322   in
1323   let rec aux steps next goal =
1324     if steps = 0 then None else
1325     let goalproof,menv,_,_,left,right = open_goal goal in
1326     let do_step t =
1327       demodulation_all_aux menv context ugraph table 0 t
1328     in
1329     match next with
1330     | L ->
1331         (match do_step left with
1332         | _::_ as res ->
1333             (match solved goal res Utils.Right with
1334             | No newgoals ->
1335                  (match first (aux (steps - 1) L) newgoals with
1336                  | Some g as success -> success
1337                  | None -> aux steps R goal)
1338             | Yes newgoal -> Some newgoal)
1339         | [] -> aux steps R goal)
1340     | R ->
1341         (match do_step right with
1342         | _::_ as res ->
1343             (match solved goal res Utils.Left with
1344             | No newgoals ->
1345                  (match first (aux (steps - 1) L) newgoals with
1346                  | Some g as success -> success
1347                  | None -> None)
1348             | Yes newgoal -> Some newgoal)
1349         | [] -> None)
1350   in
1351   aux steps L initgoal
1352 ;;
1353
1354 let get_stats () = "" ;;