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       let r =
 909         if subterms_only then
 910           []
 911         else
 912           find_all_matches
 913             metasenv context ugraph lift_amount term termty candidates
 914       in
 915       r @ res, lifted_term
 916 ;;
 917
 918 (**
 919    superposition_right
 920    returns a list of new clauses inferred with a right superposition step
 921    between the positive equation "target" and one in the "table" "newmeta" is
 922    the first free meta index, i.e. the first number above the highest meta
 923    index: its updated value is also returned
 924 *)
 925 let superposition_right bag
 926   ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
 927   let module C = Cic in
 928   let module S = CicSubstitution in
 929   let module M = CicMetaSubst in
 930   let module HL = HelmLibraryObjects in
 931   let module CR = CicReduction in
 932   let module U = Utils in
 933   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 934     Equality.open_equality target
 935   in
 936   if Utils.debug_metas then
 937     ignore (check_target bag context target "superpositionright");
 938   let metasenv' = newmetas in
 939   let maxmeta = ref newmeta in
 940   let res1, res2 =
 941     match ordering with
 942     | U.Gt ->
 943         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
 944     | U.Lt ->
 945         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
 946     | _ ->
 947         let res l r =
 948           List.filter
 949             (fun (_, subst, _, _, _) ->
 950                let subst = apply_subst subst in
 951                let o = !Utils.compare_terms (subst l) (subst r) in
 952                o <> U.Lt && o <> U.Le)
 953             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
 954         in
 955         (res left right), (res right left)
 956   in
 957   let build_new ordering (bo, s, m, ug, eq_found) =
 958     if Utils.debug_metas then
 959       ignore (check_target bag context (snd eq_found) "buildnew1" );
 960
 961     let pos, equality =  eq_found in
 962     let (_, proof', (ty, what, other, _), menv',id') =
 963       Equality.open_equality  equality in
 964     let what, other = if pos = Utils.Left then what, other else other, what in
 965
 966     let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
 967     let newgoal, newproof =
 968       (* qua *)
 969       let bo' =
 970         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
 971       in
 972       let name = C.Name "x" in
 973       let bo'' =
 974         let l, r =
 975           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 976         C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 977       in
 978       bo',
 979         Equality.Step
 980           (s,(Equality.SuperpositionRight,
 981                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
 982     in
 983     let newmeta, newequality =
 984       let left, right =
 985         if ordering = U.Gt then newgoal, apply_subst s right
 986         else apply_subst s left, newgoal in
 987       let neworder = !Utils.compare_terms left right in
 988       let newmenv = (* Founif.filter s *) m in
 989       let stat = (eq_ty, left, right, neworder) in
 990       let eq' =
 991         let w = Utils.compute_equality_weight stat in
 992         Equality.mk_equality bag (w, newproof, stat, newmenv) in
 993       if Utils.debug_metas then
 994         ignore (check_target bag context eq' "buildnew3");
 995       let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
 996       if Utils.debug_metas then
 997         ignore (check_target bag context eq' "buildnew4");
 998       newm, eq'
 999     in
1000     maxmeta := newmeta;
1001     if Utils.debug_metas then
1002       ignore(check_target bag context newequality "buildnew2");
1003     newequality
1004   in
1005   let new1 = List.map (build_new U.Gt) res1
1006   and new2 = List.map (build_new U.Lt) res2 in
1007   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1008   (!maxmeta,
1009    (List.filter ok (new1 @ new2)))
1010 ;;
1011
1012 (** demodulation, when the target is a theorem *)
1013 let rec demodulation_theorem bag env table theorem =
1014   let module C = Cic in
1015   let module S = CicSubstitution in
1016   let module M = CicMetaSubst in
1017   let module HL = HelmLibraryObjects in
1018   let eq_uri =
1019     match LibraryObjects.eq_URI() with
1020     | Some u -> u
1021     | None -> assert false in
1022   let metasenv, context, ugraph = env in
1023   let proof, theo, metas = theorem in
1024   let build_newtheorem (t, subst, menv, ug, eq_found) =
1025     let pos, equality = eq_found in
1026     let (_, proof', (ty, what, other, _), menv',id) =
1027       Equality.open_equality equality in
1028     let peq =
1029       match proof' with
1030       | Equality.Exact p -> p
1031       | _ -> assert false in
1032     let what, other =
1033       if pos = Utils.Left then what, other else other, what in
1034     let newtheo = apply_subst subst (S.subst other t) in
1035     let name = C.Name "x" in
1036     let body = apply_subst subst t in
1037     let pred = C.Lambda(name,ty,body) in
1038     let newproof =
1039       match pos with
1040         | Utils.Left ->
1041           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1042         | Utils.Right ->
1043           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1044     in
1045     newproof,newtheo
1046   in
1047   let res = demodulation_aux bag metas context ugraph table 0 theo in
1048   match res with
1049   | Some t ->
1050       let newproof, newtheo = build_newtheorem t in
1051       if Equality.meta_convertibility theo newtheo then
1052         newproof, newtheo
1053       else
1054         demodulation_theorem bag env table (newproof,newtheo,[])
1055   | None ->
1056       proof,theo
1057 ;;
1058
1059 (*****************************************************************************)
1060 (**                         OPERATIONS ON GOALS                             **)
1061 (**                                                                         **)
1062 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
1063 (*****************************************************************************)
1064
1065 (* new: demodulation of non_equality terms *)
1066 let build_newg bag context goal rule expansion =
1067   let goalproof,_,_ = goal in
1068   let (t,subst,menv,ug,eq_found) = expansion in
1069   let pos, equality = eq_found in
1070   let (_, proof', (ty, what, other, _), menv',id) =
1071     Equality.open_equality equality in
1072   let what, other = if pos = Utils.Left then what, other else other, what in
1073   let newterm, newgoalproof =
1074     let bo =
1075       Utils.guarded_simpl context
1076         (apply_subst subst (CicSubstitution.subst other t))
1077     in
1078     let name = Cic.Name "x" in
1079     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1080     let newgoalproofstep = (rule,pos,id,subst,pred) in
1081     bo, (newgoalproofstep::goalproof)
1082   in
1083   let newmetasenv = (* Founif.filter subst *) menv in
1084   (newgoalproof, newmetasenv, newterm)
1085 ;;
1086
1087 let rec demod bag env table goal =
1088   let goalproof,menv,t = goal in
1089   let _, context, ugraph = env in
1090   let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
1091   match res with
1092     | Some newt ->
1093         let newg =
1094           build_newg bag context goal Equality.Demodulation newt
1095         in
1096         let _,_,newt = newg in
1097         if Equality.meta_convertibility t newt then
1098           false, goal
1099         else
1100           true, snd (demod bag env table newg)
1101     | None ->
1102         false, goal
1103 ;;
1104
1105 let open_goal g =
1106   match g with
1107   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
1108       (* assert (LibraryObjects.is_eq_URI uri); *)
1109       proof,menv,eq,ty,l,r
1110   | _ -> assert false
1111
1112 let ty_of_goal (_,_,ty) = ty ;;
1113
1114 (* checks if two goals are metaconvertible *)
1115 let goal_metaconvertibility_eq g1 g2 =
1116   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1117 ;;
1118
1119 (* when the betaexpand_term function is called on the left/right side of the
1120  * goal, the predicate has to be fixed
1121  * C[x] ---> (eq ty unchanged C[x])
1122  * [posu] is the side of the [unchanged] term in the original goal
1123  *)
1124
1125 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1126   let _,_,eq,ty,l,r = open_goal goal in
1127   let unchanged = if posu = Utils.Left then l else r in
1128   let unchanged = CicSubstitution.lift 1 unchanged in
1129   let ty = CicSubstitution.lift 1 ty in
1130   let pred =
1131     match posu with
1132     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1133     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1134   in
1135   (pred, subst, menv, ug, eq_f)
1136 ;;
1137
1138 (* ginve the old [goal], the side that has not changed [posu] and the
1139  * expansion builds a new goal *)
1140 let build_newgoal bag context goal posu rule expansion =
1141   let goalproof,_,_,_,_,_ = open_goal goal in
1142   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1143   let pos, equality = eq_found in
1144   let (_, proof', (ty, what, other, _), menv',id) =
1145     Equality.open_equality equality in
1146   let what, other = if pos = Utils.Left then what, other else other, what in
1147   let newterm, newgoalproof =
1148     let bo =
1149       Utils.guarded_simpl context
1150         (apply_subst subst (CicSubstitution.subst other t))
1151     in
1152     let name = Cic.Name "x" in
1153     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1154     let newgoalproofstep = (rule,pos,id,subst,pred) in
1155     bo, (newgoalproofstep::goalproof)
1156   in
1157   let newmetasenv = (* Founif.filter subst *) menv in
1158   (newgoalproof, newmetasenv, newterm)
1159 ;;
1160
1161 (**
1162    superposition_left
1163    returns a list of new clauses inferred with a left superposition step
1164    the negative equation "target" and one of the positive equations in "table"
1165 *)
1166 let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
1167   let names = Utils.names_of_context context in
1168   let proof,menv,eq,ty,l,r = open_goal goal in
1169   let c = !Utils.compare_terms l r in
1170   let newgoals =
1171     if c = Utils.Incomparable then
1172       begin
1173       let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1174       let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1175       (* prerr_endline "incomparable";
1176       prerr_endline (string_of_int (List.length expansionsl));
1177       prerr_endline (string_of_int (List.length expansionsr));
1178       *)
1179 (*
1180       if expansionsl <> [] then prerr_endline "expansionl";
1181       if expansionsr <> [] then prerr_endline "expansionr";
1182 *)
1183       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1184       @
1185       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1186       end
1187     else
1188         match c with
1189         | Utils.Gt -> (* prerr_endline "GT"; *)
1190             let big,small,possmall = l,r,Utils.Right in
1191             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1192             List.map
1193               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1194               expansions
1195         | Utils.Lt -> (* prerr_endline "LT"; *)
1196             let big,small,possmall = r,l,Utils.Left in
1197             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1198             List.map
1199               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1200               expansions
1201         | Utils.Eq -> []
1202         | _ ->
1203             prerr_endline
1204               ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1205             assert false
1206   in
1207   (* rinfresco le meta *)
1208   List.fold_right
1209     (fun g (max,acc) ->
1210        let max,g = Equality.fix_metas_goal max g in max,g::acc)
1211     newgoals (maxmeta,[])
1212 ;;
1213
1214 (** demodulation, when the target is a goal *)
1215 let rec demodulation_goal bag env table goal =
1216   let goalproof,menv,_,_,left,right = open_goal goal in
1217   let _, context, ugraph = env in
1218 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
1219   let do_right () =
1220       let resright = demodulation_aux bag menv context ugraph table 0 right in
1221       match resright with
1222       | Some t ->
1223           let newg =
1224             build_newgoal bag context goal Utils.Left Equality.Demodulation t
1225           in
1226           if goal_metaconvertibility_eq goal newg then
1227             false, goal
1228           else
1229             true, snd (demodulation_goal bag env table newg)
1230       | None -> false, goal
1231   in
1232   let resleft = demodulation_aux bag menv context ugraph table 0 left in
1233   match resleft with
1234   | Some t ->
1235       let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1236       if goal_metaconvertibility_eq goal newg then
1237         do_right ()
1238       else
1239         true, snd (demodulation_goal bag env table newg)
1240   | None -> do_right ()
1241 ;;
1242
1243 type next = L | R
1244 type solved = Yes of Equality.goal | No of Equality.goal list
1245
1246 (* returns all the 1 step demodulations *)
1247 module C = Cic;;
1248 module S = CicSubstitution;;
1249 let rec demodulation_all_aux
1250   metasenv context ugraph table lift_amount term
1251 =
1252   let candidates =
1253     get_candidates ~env:(metasenv,context,ugraph) Matching table term
1254   in
1255   match term with
1256   | C.Meta _ -> []
1257   | _ ->
1258       let termty, ugraph = C.Implicit None, ugraph in
1259       let res =
1260         find_all_matches
1261           metasenv context ugraph lift_amount term termty candidates
1262       in
1263       match term with
1264       | C.Appl l ->
1265          let res, _, _ =
1266            List.fold_left
1267             (fun (res,l,r) t ->
1268                res @
1269                List.map
1270                  (fun (rel, s, m, ug, c) ->
1271                    (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1272                  (demodulation_all_aux
1273                    metasenv context ugraph table lift_amount t),
1274                l@[List.hd r], List.tl r)
1275             (res, [], List.map (S.lift 1) l) l
1276          in
1277          res
1278       | C.Prod (nn, s, t)
1279       | C.Lambda (nn, s, t) ->
1280           let context = (Some (nn, C.Decl s))::context in
1281           let mk s t =
1282             match term with
1283             | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
1284           in
1285           res @
1286           List.map
1287             (fun (rel, subst, m, ug, c) ->
1288                mk (S.lift 1 s) rel, subst, m, ug, c)
1289             (demodulation_all_aux
1290               metasenv context ugraph table (lift_amount+1) t)
1291               (* we could demodulate also in s, but then t may be badly
1292                * typed... *)
1293       | t -> res
1294 ;;
1295
1296 let solve_demodulating bag env table initgoal steps =
1297   let _, context, ugraph = env in
1298   let solved goal res side =
1299     let newg = build_newgoal bag context goal side Equality.Demodulation res in
1300     match newg with
1301     | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right])
1302       when LibraryObjects.is_eq_URI uri ->
1303         (try
1304           let _ =
1305             Founif.unification m m context left right CicUniv.empty_ugraph
1306           in
1307           Yes newg
1308         with CicUnification.UnificationFailure _ -> No [newg])
1309     | _ -> No [newg]
1310   in
1311   let solved goal res_list side =
1312     let newg = List.map (fun x -> solved goal x side) res_list in
1313     try
1314       List.find (function Yes _ -> true | _ -> false) newg
1315     with Not_found ->
1316       No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
1317   in
1318   let rec first f l =
1319     match l with
1320     | [] -> None
1321     | x::tl ->
1322        match f x with
1323        | None -> first f tl
1324        | Some x as ok -> ok
1325   in
1326   let rec aux steps next goal =
1327     if steps = 0 then None else
1328     let goalproof,menv,_,_,left,right = open_goal goal in
1329     let do_step t =
1330       demodulation_all_aux menv context ugraph table 0 t
1331     in
1332     match next with
1333     | L ->
1334         (match do_step left with
1335         | _::_ as res ->
1336             (match solved goal res Utils.Right with
1337             | No newgoals ->
1338                  (match first (aux (steps - 1) L) newgoals with
1339                  | Some g as success -> success
1340                  | None -> aux steps R goal)
1341             | Yes newgoal -> Some newgoal)
1342         | [] -> aux steps R goal)
1343     | R ->
1344         (match do_step right with
1345         | _::_ as res ->
1346             (match solved goal res Utils.Left with
1347             | No newgoals ->
1348                  (match first (aux (steps - 1) L) newgoals with
1349                  | Some g as success -> success
1350                  | None -> None)
1351             | Yes newgoal -> Some newgoal)
1352         | [] -> None)
1353   in
1354   aux steps L initgoal
1355 ;;
1356
1357 let get_stats () = "" ;;