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