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   (* 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   (* prerr_endline ("demodulating " ^ CicPp.ppterm term); *)
 569   check_for_duplicates metasenv "in input a demodulation aux";
 570   let candidates =
 571     get_candidates
 572       ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
 573   in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates
 574   in
 575   let res =
 576     match term with
 577       | C.Meta _ -> None
 578       | term ->
 579           let res =
 580             try
 581               let termty, ugraph =
 582                 if typecheck then
 583                   CicTypeChecker.type_of_aux' metasenv context term ugraph
 584                 else
 585                   C.Implicit None, ugraph
 586               in
 587                 find_matches bag metasenv context ugraph
 588                   lift_amount term termty candidates
 589             with _ ->
 590               prerr_endline "type checking error";
 591               prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
 592               prerr_endline ("term: " ^ (CicPp.ppterm term));
 593               assert false;
 594               (* None *)
 595           in
 596           let res =
 597             (if Utils.debug_res then
 598             ignore(check_res res "demod1");
 599             if check_demod_res res metasenv "demod" then res else None) in
 600           if res <> None then
 601               res
 602             else
 603               match term with
 604                 | C.Appl l ->
 605                     let res, ll =
 606                       List.fold_left
 607                         (fun (res, tl) t ->
 608                            if res <> None then
 609                              (res, tl @ [S.lift 1 t])
 610                            else
 611                              let r =
 612                                demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck
 613                                  lift_amount t
 614                              in
 615                                match r with
 616                                  | None -> (None, tl @ [S.lift 1 t])
 617                                  | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 618                         (None, []) l
 619                     in (
 620                         match res with
 621                           | None -> None
 622                           | Some (_, subst, menv, ug, eq_found) ->
 623                               Some (C.Appl ll, subst, menv, ug, eq_found)
 624                       )
 625 (*
 626                 | C.Prod (nn, s, t) ->
 627                     let r1 =
 628                       demodulation_aux bag ~from:"2"
 629                         metasenv context ugraph table lift_amount s in (
 630                         match r1 with
 631                           | None ->
 632                               let r2 =
 633                                 demodulation_aux bag metasenv
 634                                   ((Some (nn, C.Decl s))::context) ugraph
 635                                   table (lift_amount+1) t
 636                               in (
 637                                   match r2 with
 638                                     | None -> None
 639                                     | Some (t', subst, menv, ug, eq_found) ->
 640                                         Some (C.Prod (nn, (S.lift 1 s), t'),
 641                                               subst, menv, ug, eq_found)
 642                                 )
 643                           | Some (s', subst, menv, ug, eq_found) ->
 644                               Some (C.Prod (nn, s', (S.lift 1 t)),
 645                                     subst, menv, ug, eq_found)
 646                       )
 647                 | C.Lambda (nn, s, t) ->
 648                     prerr_endline "siam qui";
 649                     let r1 =
 650                       demodulation_aux bag
 651                         metasenv context ugraph table lift_amount s in (
 652                         match r1 with
 653                           | None ->
 654                               let r2 =
 655                                 demodulation_aux bag metasenv
 656                                   ((Some (nn, C.Decl s))::context) ugraph
 657                                   table (lift_amount+1) t
 658                               in (
 659                                   match r2 with
 660                                     | None -> None
 661                                     | Some (t', subst, menv, ug, eq_found) ->
 662                                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 663                                               subst, menv, ug, eq_found)
 664                                 )
 665                           | Some (s', subst, menv, ug, eq_found) ->
 666                               Some (C.Lambda (nn, s', (S.lift 1 t)),
 667                                     subst, menv, ug, eq_found)
 668                       )
 669 *)
 670                 | t ->
 671                     None
 672   in
 673   if Utils.debug_res then ignore(check_res res "demod_aux output");
 674   res
 675 ;;
 676
 677 exception Foo
 678
 679 (** demodulation, when target is an equality *)
 680 let rec demodulation_equality bag ?from eq_uri newmeta env table target =
 681         (*
 682           prerr_endline ("demodulation_eq:\n");
 683         Index.iter table (fun l ->
 684           let l = Index.PosEqSet.elements l in
 685           let l =
 686             List.map (fun (p,e) ->
 687               Utils.string_of_pos p ^ Equality.string_of_equality e) l in
 688           prerr_endline (String.concat "\n" l)
 689           );
 690           *)
 691   let module C = Cic in
 692   let module S = CicSubstitution in
 693   let module M = CicMetaSubst in
 694   let module HL = HelmLibraryObjects in
 695   let module U = Utils in
 696   let metasenv, context, ugraph = env in
 697   let w, proof, (eq_ty, left, right, order), metas, id =
 698     Equality.open_equality target
 699   in
 700   (* first, we simplify *)
 701 (*   let right = U.guarded_simpl context right in *)
 702 (*   let left = U.guarded_simpl context left in *)
 703 (*   let order = !Utils.compare_terms left right in *)
 704 (*   let stat = (eq_ty, left, right, order) in  *)
 705 (*  let w = Utils.compute_equality_weight stat in*)
 706   (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
 707   if Utils.debug_metas then
 708     ignore(check_target bag context target "demod equalities input");
 709   let metasenv' = (* metasenv @ *) metas in
 710   let maxmeta = ref newmeta in
 711
 712   let build_newtarget is_left (t, subst, menv, ug, eq_found) =
 713
 714     if Utils.debug_metas then
 715       begin
 716         ignore(check_for_duplicates menv "input1");
 717         ignore(check_disjoint_invariant subst menv "input2");
 718         let substs = Subst.ppsubst subst in
 719         ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
 720       end;
 721     let pos, equality = eq_found in
 722     let (_, proof',
 723         (ty, what, other, _), menv',id') = Equality.open_equality equality in
 724     let ty =
 725       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 726       with CicUtil.Meta_not_found _ -> ty
 727     in
 728     let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
 729     let what, other = if pos = Utils.Left then what, other else other, what in
 730     let newterm, newproof =
 731       let bo =
 732         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 733 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
 734       let name = C.Name "x" in
 735       let bo' =
 736         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 737           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 738       in
 739           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
 740           (Cic.Lambda (name, ty, bo'))))))
 741     in
 742     let newmenv = menv in
 743     let left, right = if is_left then newterm, right else left, newterm in
 744     let ordering = !Utils.compare_terms left right in
 745     let stat = (eq_ty, left, right, ordering) in
 746     let res =
 747       let w = Utils.compute_equality_weight stat in
 748           (Equality.mk_equality bag (w, newproof, stat,newmenv))
 749     in
 750     if Utils.debug_metas then
 751       ignore(check_target bag context res "buildnew_target output");
 752     !maxmeta, res
 753   in
 754
 755   let res =
 756     demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
 757   in
 758   if Utils.debug_res then check_res res "demod result";
 759   let newmeta, newtarget =
 760     match res with
 761     | Some t ->
 762         let newmeta, newtarget = build_newtarget true t in
 763           (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
 764           if (Equality.is_weak_identity newtarget) (* || *)
 765             (*Equality.meta_convertibility_eq target newtarget*) then
 766               newmeta, newtarget
 767           else
 768             demodulation_equality bag ?from eq_uri newmeta env table newtarget
 769     | None ->
 770         let res = demodulation_aux bag metasenv' context ugraph table 0 right in
 771         if Utils.debug_res then check_res res "demod result 1";
 772           match res with
 773           | Some t ->
 774               let newmeta, newtarget = build_newtarget false t in
 775                 if (Equality.is_weak_identity newtarget) ||
 776                   (Equality.meta_convertibility_eq target newtarget) then
 777                     newmeta, newtarget
 778                 else
 779                    demodulation_equality bag ?from eq_uri newmeta env table newtarget
 780           | None ->
 781               newmeta, target
 782   in
 783   (* newmeta, newtarget *)
 784   newmeta,newtarget
 785 ;;
 786
 787 (**
 788    Performs the beta expansion of the term "term" w.r.t. "table",
 789    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 790    in table.
 791 *)
 792 let rec betaexpand_term
 793   ?(subterms_only=false) metasenv context ugraph table lift_amount term
 794 =
 795   let module C = Cic in
 796   let module S = CicSubstitution in
 797   let module M = CicMetaSubst in
 798   let module HL = HelmLibraryObjects in
 799
 800   let res, lifted_term =
 801     match term with
 802     | C.Meta (i, l) ->
 803         let l = [] in
 804         let l', lifted_l =
 805           List.fold_right
 806             (fun arg (res, lifted_tl) ->
 807                match arg with
 808                | Some arg ->
 809                    let arg_res, lifted_arg =
 810                      betaexpand_term metasenv context ugraph table
 811                        lift_amount arg in
 812                    let l1 =
 813                      List.map
 814                        (fun (t, s, m, ug, eq_found) ->
 815                           (Some t)::lifted_tl, s, m, ug, eq_found)
 816                        arg_res
 817                    in
 818                    (l1 @
 819                       (List.map
 820                          (fun (l, s, m, ug, eq_found) ->
 821                             (Some lifted_arg)::l, s, m, ug, eq_found)
 822                          res),
 823                     (Some lifted_arg)::lifted_tl)
 824                | None ->
 825                    (List.map
 826                       (fun (r, s, m, ug, eq_found) ->
 827                          None::r, s, m, ug, eq_found) res,
 828                     None::lifted_tl)
 829             ) l ([], [])
 830         in
 831         let e =
 832           List.map
 833             (fun (l, s, m, ug, eq_found) ->
 834                (C.Meta (i, l), s, m, ug, eq_found)) l'
 835         in
 836         e, C.Meta (i, lifted_l)
 837
 838     | C.Rel m ->
 839         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 840
 841     | C.Prod (nn, s, t) ->
 842         let l1, lifted_s =
 843           betaexpand_term metasenv context ugraph table lift_amount s in
 844         let l2, lifted_t =
 845           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 846             table (lift_amount+1) t in
 847         let l1' =
 848           List.map
 849             (fun (t, s, m, ug, eq_found) ->
 850                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 851         and l2' =
 852           List.map
 853             (fun (t, s, m, ug, eq_found) ->
 854                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 855         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 856
 857     | C.Lambda (nn, s, t) ->
 858         let l1, lifted_s =
 859           betaexpand_term metasenv context ugraph table lift_amount s in
 860         let l2, lifted_t =
 861           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 862             table (lift_amount+1) t in
 863         let l1' =
 864           List.map
 865             (fun (t, s, m, ug, eq_found) ->
 866                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 867         and l2' =
 868           List.map
 869             (fun (t, s, m, ug, eq_found) ->
 870                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 871         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 872
 873     | C.Appl l ->
 874         let l', lifted_l =
 875           List.fold_left
 876             (fun (res, lifted_tl) arg ->
 877                let arg_res, lifted_arg =
 878                  betaexpand_term metasenv context ugraph table lift_amount arg
 879                in
 880                let l1 =
 881                  List.map
 882                    (fun (a, s, m, ug, eq_found) ->
 883                       a::lifted_tl, s, m, ug, eq_found)
 884                    arg_res
 885                in
 886                (l1 @
 887                   (List.map
 888                      (fun (r, s, m, ug, eq_found) ->
 889                         lifted_arg::r, s, m, ug, eq_found)
 890                      res),
 891                 lifted_arg::lifted_tl)
 892             ) ([], []) (List.rev l)
 893         in
 894         (List.map
 895            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 896          C.Appl lifted_l)
 897
 898     | t -> [], (S.lift lift_amount t)
 899   in
 900   match term with
 901   | C.Meta (i, l) -> res, lifted_term
 902   | term ->
 903       let termty, ugraph =
 904 (*        C.Implicit None, ugraph *)
 905          CicTypeChecker.type_of_aux' metasenv context term ugraph
 906       in
 907       let candidates = get_candidates Unification table term in
 908       (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
 909       let r =
 910         if subterms_only then
 911           []
 912         else
 913           find_all_matches
 914             metasenv context ugraph lift_amount term termty candidates
 915       in
 916       r @ res, lifted_term
 917 ;;
 918
 919 (**
 920    superposition_right
 921    returns a list of new clauses inferred with a right superposition step
 922    between the positive equation "target" and one in the "table" "newmeta" is
 923    the first free meta index, i.e. the first number above the highest meta
 924    index: its updated value is also returned
 925 *)
 926 let superposition_right bag
 927   ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
 928   let module C = Cic in
 929   let module S = CicSubstitution in
 930   let module M = CicMetaSubst in
 931   let module HL = HelmLibraryObjects in
 932   let module CR = CicReduction in
 933   let module U = Utils in
 934   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 935     Equality.open_equality target
 936   in
 937   if Utils.debug_metas then
 938     ignore (check_target bag context target "superpositionright");
 939   let metasenv' = newmetas in
 940   let maxmeta = ref newmeta in
 941   let res1, res2 =
 942     match ordering with
 943     | U.Gt ->
 944         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
 945     | U.Lt ->
 946         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
 947     | _ ->
 948         let res l r =
 949           List.filter
 950             (fun (_, subst, _, _, _) ->
 951                let subst = apply_subst subst in
 952                let o = !Utils.compare_terms (subst l) (subst r) in
 953                o <> U.Lt && o <> U.Le)
 954             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
 955         in
 956         (res left right), (res right left)
 957   in
 958   let build_new ordering (bo, s, m, ug, eq_found) =
 959     if Utils.debug_metas then
 960       ignore (check_target bag context (snd eq_found) "buildnew1" );
 961
 962     let pos, equality =  eq_found in
 963     let (_, proof', (ty, what, other, _), menv',id') =
 964       Equality.open_equality  equality in
 965     let what, other = if pos = Utils.Left then what, other else other, what in
 966
 967     let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
 968     let newgoal, newproof =
 969       (* qua *)
 970       let bo' =
 971         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
 972       in
 973       let name = C.Name "x" in
 974       let bo'' =
 975         let l, r =
 976           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 977         C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 978       in
 979       bo',
 980         Equality.Step
 981           (s,(Equality.SuperpositionRight,
 982                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
 983     in
 984     let newmeta, newequality =
 985       let left, right =
 986         if ordering = U.Gt then newgoal, apply_subst s right
 987         else apply_subst s left, newgoal in
 988       let neworder = !Utils.compare_terms left right in
 989       let newmenv = (* Founif.filter s *) m in
 990       let stat = (eq_ty, left, right, neworder) in
 991       let eq' =
 992         let w = Utils.compute_equality_weight stat in
 993         Equality.mk_equality bag (w, newproof, stat, newmenv) in
 994       if Utils.debug_metas then
 995         ignore (check_target bag context eq' "buildnew3");
 996       let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
 997       if Utils.debug_metas then
 998         ignore (check_target bag context eq' "buildnew4");
 999       newm, eq'
1000     in
1001     maxmeta := newmeta;
1002     if Utils.debug_metas then
1003       ignore(check_target bag context newequality "buildnew2");
1004     newequality
1005   in
1006   let new1 = List.map (build_new U.Gt) res1
1007   and new2 = List.map (build_new U.Lt) res2 in
1008   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1009   (!maxmeta,
1010    (List.filter ok (new1 @ new2)))
1011 ;;
1012
1013 (** demodulation, when the target is a theorem *)
1014 let rec demodulation_theorem bag env table theorem =
1015   let module C = Cic in
1016   let module S = CicSubstitution in
1017   let module M = CicMetaSubst in
1018   let module HL = HelmLibraryObjects in
1019   let eq_uri =
1020     match LibraryObjects.eq_URI() with
1021     | Some u -> u
1022     | None -> assert false in
1023   let metasenv, context, ugraph = env in
1024   let proof, theo, metas = theorem in
1025   let build_newtheorem (t, subst, menv, ug, eq_found) =
1026     let pos, equality = eq_found in
1027     let (_, proof', (ty, what, other, _), menv',id) =
1028       Equality.open_equality equality in
1029     let peq =
1030       match proof' with
1031       | Equality.Exact p -> p
1032       | _ -> assert false in
1033     let what, other =
1034       if pos = Utils.Left then what, other else other, what in
1035     let newtheo = apply_subst subst (S.subst other t) in
1036     let name = C.Name "x" in
1037     let body = apply_subst subst t in
1038     let pred = C.Lambda(name,ty,body) in
1039     let newproof =
1040       match pos with
1041         | Utils.Left ->
1042           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1043         | Utils.Right ->
1044           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1045     in
1046     newproof,newtheo
1047   in
1048   let res = demodulation_aux bag metas context ugraph table 0 theo in
1049   match res with
1050   | Some t ->
1051       let newproof, newtheo = build_newtheorem t in
1052       if Equality.meta_convertibility theo newtheo then
1053         newproof, newtheo
1054       else
1055         demodulation_theorem bag env table (newproof,newtheo,[])
1056   | None ->
1057       proof,theo
1058 ;;
1059
1060 (*****************************************************************************)
1061 (**                         OPERATIONS ON GOALS                             **)
1062 (**                                                                         **)
1063 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
1064 (*****************************************************************************)
1065
1066 (* new: demodulation of non_equality terms *)
1067 let build_newg bag context goal rule expansion =
1068   let goalproof,_,_ = goal in
1069   let (t,subst,menv,ug,eq_found) = expansion in
1070   let pos, equality = eq_found in
1071   let (_, proof', (ty, what, other, _), menv',id) =
1072     Equality.open_equality equality in
1073   let what, other = if pos = Utils.Left then what, other else other, what in
1074   let newterm, newgoalproof =
1075     let bo =
1076       Utils.guarded_simpl context
1077         (apply_subst subst (CicSubstitution.subst other t))
1078     in
1079     let name = Cic.Name "x" in
1080     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1081     let newgoalproofstep = (rule,pos,id,subst,pred) in
1082     bo, (newgoalproofstep::goalproof)
1083   in
1084   let newmetasenv = (* Founif.filter subst *) menv in
1085   (newgoalproof, newmetasenv, newterm)
1086 ;;
1087
1088 let rec demod bag env table goal =
1089   let goalproof,menv,t = goal in
1090   let _, context, ugraph = env in
1091   let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
1092   match res with
1093     | Some newt ->
1094         let newg =
1095           build_newg bag context goal Equality.Demodulation newt
1096         in
1097         let _,_,newt = newg in
1098         if Equality.meta_convertibility t newt then
1099           false, goal
1100         else
1101           true, snd (demod bag env table newg)
1102     | None ->
1103         false, goal
1104 ;;
1105
1106 let open_goal g =
1107   match g with
1108   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
1109       (* assert (LibraryObjects.is_eq_URI uri); *)
1110       proof,menv,eq,ty,l,r
1111   | _ -> assert false
1112
1113 let ty_of_goal (_,_,ty) = ty ;;
1114
1115 (* checks if two goals are metaconvertible *)
1116 let goal_metaconvertibility_eq g1 g2 =
1117   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1118 ;;
1119
1120 (* when the betaexpand_term function is called on the left/right side of the
1121  * goal, the predicate has to be fixed
1122  * C[x] ---> (eq ty unchanged C[x])
1123  * [posu] is the side of the [unchanged] term in the original goal
1124  *)
1125
1126 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1127   let _,_,eq,ty,l,r = open_goal goal in
1128   let unchanged = if posu = Utils.Left then l else r in
1129   let unchanged = CicSubstitution.lift 1 unchanged in
1130   let ty = CicSubstitution.lift 1 ty in
1131   let pred =
1132     match posu with
1133     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1134     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1135   in
1136   (pred, subst, menv, ug, eq_f)
1137 ;;
1138
1139 (* ginve the old [goal], the side that has not changed [posu] and the
1140  * expansion builds a new goal *)
1141 let build_newgoal bag context goal posu rule expansion =
1142   let goalproof,_,_,_,_,_ = open_goal goal in
1143   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1144   let pos, equality = eq_found in
1145   let (_, proof', (ty, what, other, _), menv',id) =
1146     Equality.open_equality equality in
1147   let what, other = if pos = Utils.Left then what, other else other, what in
1148   let newterm, newgoalproof =
1149     let bo =
1150       Utils.guarded_simpl context
1151         (apply_subst subst (CicSubstitution.subst other t))
1152     in
1153     let name = Cic.Name "x" in
1154     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1155     let newgoalproofstep = (rule,pos,id,subst,pred) 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 ->
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 () = "" ;;