helm/software/components/tactics/paramodulation/indexing.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* let _profiler = <:profiler<_profiler>>;; *)
  27
  28 (* $Id$ *)
  29
  30 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
  31 (*
  32 module Index = Equality_indexing.DT (* path tree based indexing *)
  33 *)
  34
  35 let debug_print = Utils.debug_print;;
  36
  37 (*
  38 for debugging
  39 let check_equation env equation msg =
  40   let w, proof, (eq_ty, left, right, order), metas, args = equation in
  41   let metasenv, context, ugraph = env
  42   let metasenv' = metasenv @ metas in
  43     try
  44       CicTypeChecker.type_of_aux' metasenv' context left ugraph;
  45       CicTypeChecker.type_of_aux' metasenv' context right ugraph;
  46       ()
  47     with
  48         CicUtil.Meta_not_found _ as exn ->
  49           begin
  50             prerr_endline msg;
  51             prerr_endline (CicPp.ppterm left);
  52             prerr_endline (CicPp.ppterm right);
  53             raise exn
  54           end
  55 *)
  56
  57 type retrieval_mode = Matching | Unification;;
  58
  59 let string_of_res ?env =
  60   function
  61       None -> "None"
  62     | Some (t, s, m, u, (p,e)) ->
  63         Printf.sprintf "Some: (%s, %s, %s)"
  64           (Utils.string_of_pos p)
  65           (Equality.string_of_equality ?env e)
  66           (CicPp.ppterm t)
  67 ;;
  68
  69 let print_res ?env res =
  70   prerr_endline
  71     (String.concat "\n"
  72        (List.map (string_of_res ?env) res))
  73 ;;
  74
  75 let print_candidates ?env mode term res =
  76   let _ =
  77     match mode with
  78     | Matching ->
  79         prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
  80     | Unification ->
  81         prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
  82   in
  83   prerr_endline
  84     (String.concat "\n"
  85        (List.map
  86           (fun (p, e) ->
  87              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
  88                (Equality.string_of_equality ?env e))
  89           res));
  90 ;;
  91
  92
  93 let apply_subst = Subst.apply_subst
  94
  95 let index = Index.index
  96 let remove_index = Index.remove_index
  97 let in_index = Index.in_index
  98 let empty = Index.empty
  99 let init_index = Index.init_index
 100
 101 let check_disjoint_invariant subst metasenv msg =
 102   if (List.exists
 103         (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
 104   then
 105     begin
 106       prerr_endline ("not disjoint: " ^ msg);
 107       assert false
 108     end
 109 ;;
 110
 111 let check_for_duplicates metas msg =
 112   let rec aux = function
 113     | [] -> true
 114     | (m,_,_)::tl -> not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in
 115   let b = aux metas in
 116     if not b then
 117       begin
 118       prerr_endline ("DUPLICATI " ^ msg);
 119       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 120       assert false
 121       end
 122     else ()
 123 ;;
 124
 125 let check_metasenv msg menv =
 126   List.iter
 127     (fun (i,ctx,ty) ->
 128        try ignore(CicTypeChecker.type_of_aux' menv ctx ty
 129                   CicUniv.empty_ugraph)
 130        with
 131          | CicUtil.Meta_not_found _ ->
 132              prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv);
 133              assert false
 134          | _ -> ()
 135     ) menv
 136 ;;
 137
 138 (* the metasenv returned by res must included in the original one,
 139 due to matching. If it fails, it is probably because we are not
 140 demodulating with a unit equality *)
 141
 142 let not_unit_eq ctx eq =
 143   let (_,_,(ty,left,right,o),metas,_) = Equality.open_equality eq in
 144   let b =
 145   List.exists
 146     (fun (_,_,ty) ->
 147        try
 148          let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph
 149          in s = Cic.Sort(Cic.Prop)
 150        with _ ->
 151          prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas
 152   in b
 153 (*
 154 if b then prerr_endline ("not a unit equality: " ^ Equality.string_of_equality eq); b *)
 155 ;;
 156
 157 let check_demod_res res metasenv msg =
 158   match res with
 159     | Some (_, _, menv, _, _) ->
 160         let b =
 161           List.for_all
 162             (fun (i,_,_) ->
 163                (List.exists (fun (j,_,_) -> i=j) metasenv)) menv
 164         in
 165           if (not b) then
 166             begin
 167               debug_print (lazy ("extended context " ^ msg));
 168               debug_print (lazy (CicMetaSubst.ppmetasenv [] menv));
 169             end;
 170         b
 171     | None -> false
 172 ;;
 173
 174 let check_res res msg =
 175   match res with
 176     | Some (t, subst, menv, ug, eq_found) ->
 177         let eqs = Equality.string_of_equality (snd eq_found) in
 178         check_metasenv msg menv;
 179         check_disjoint_invariant subst menv msg;
 180         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
 181     | None -> ()
 182 ;;
 183
 184 let check_target bag context target msg =
 185   let w, proof, (eq_ty, left, right, order), metas,_ =
 186     Equality.open_equality target in
 187   (* check that metas does not contains duplicates *)
 188   let eqs = Equality.string_of_equality target in
 189   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
 190   let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
 191     @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof)  in
 192   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
 193   let _ = if menv <> metas then
 194     begin
 195       prerr_endline ("extra metas " ^ msg);
 196       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 197       prerr_endline "**********************";
 198       prerr_endline (CicMetaSubst.ppmetasenv [] menv);
 199       prerr_endline ("left: " ^ (CicPp.ppterm left));
 200       prerr_endline ("right: " ^ (CicPp.ppterm right));
 201       prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
 202       assert false
 203     end
 204   else () in ()
 205 (*
 206   try
 207       ignore(CicTypeChecker.type_of_aux'
 208         metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph)
 209   with e ->
 210       prerr_endline msg;
 211       prerr_endline (Founif.string_of_proof proof);
 212       prerr_endline (CicPp.ppterm (Founif.build_proof_term proof));
 213       prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
 214       prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
 215       raise e
 216 *)
 217
 218
 219 (* returns a list of all the equalities in the tree that are in relation
 220    "mode" with the given term, where mode can be either Matching or
 221    Unification.
 222
 223    Format of the return value: list of tuples in the form:
 224    (position - Left or Right - of the term that matched the given one in this
 225      equality,
 226     equality found)
 227
 228    Note that if equality is "left = right", if the ordering is left > right,
 229    the position will always be Left, and if the ordering is left < right,
 230    position will be Right.
 231 *)
 232
 233 let get_candidates ?env mode tree term =
 234   let s =
 235     match mode with
 236     | Matching ->
 237         Index.retrieve_generalizations tree term
 238     | Unification ->
 239         Index.retrieve_unifiables tree term
 240
 241   in
 242   Index.PosEqSet.elements s
 243 ;;
 244
 245 (*
 246   finds the first equality in the index that matches "term", of type "termty"
 247   termty can be Implicit if it is not needed. The result (one of the sides of
 248   the equality, actually) should be not greater (wrt the term ordering) than
 249   term
 250
 251   Format of the return value:
 252
 253   (term to substitute, [Cic.Rel 1 properly lifted - see the various
 254                         build_newtarget functions inside the various
 255                         demodulation_* functions]
 256    substitution used for the matching,
 257    metasenv,
 258    ugraph, [substitution, metasenv and ugraph have the same meaning as those
 259    returned by CicUnification.fo_unif]
 260    (equality where the matching term was found, [i.e. the equality to use as
 261                                                 rewrite rule]
 262     uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
 263          the equality: this is used to build the proof term, again see one of
 264          the build_newtarget functions]
 265    ))
 266 *)
 267 let rec find_matches bag metasenv context ugraph lift_amount term termty =
 268   let module C = Cic in
 269   let module U = Utils in
 270   let module S = CicSubstitution in
 271   let module M = CicMetaSubst in
 272   let module HL = HelmLibraryObjects in
 273   let cmp = !Utils.compare_terms in
 274   let check = match termty with C.Implicit None -> false | _ -> true in
 275   function
 276     | [] -> None
 277     | candidate::tl ->
 278         let pos, equality = candidate in
 279         (* if not_unit_eq context equality then
 280           begin
 281             prerr_endline "not a unit";
 282             prerr_endline (Equality.string_of_equality equality)
 283           end; *)
 284         let (_, proof, (ty, left, right, o), metas,_) =
 285           Equality.open_equality equality
 286         in
 287         if Utils.debug_metas then
 288           ignore(check_target bag context (snd candidate) "find_matches");
 289         if Utils.debug_res then
 290           begin
 291             let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
 292             let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
 293             let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
 294             let ms="metasenv =" ^ (CicMetaSubst.ppmetasenv [] metasenv) ^ "\n" in
 295             let eq_uri =
 296               match LibraryObjects.eq_URI () with
 297                 | Some (uri) -> uri
 298                 | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
 299             let p="proof = "^
 300               (CicPp.ppterm(Equality.build_proof_term bag eq_uri [] 0 proof))^"\n"
 301             in
 302
 303               check_for_duplicates metas "gia nella metas";
 304               check_for_duplicates metasenv "gia nel metasenv";
 305               check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^ms^p)
 306           end;
 307         if check && not (fst (CicReduction.are_convertible
 308                                 ~metasenv context termty ty ugraph)) then (
 309           find_matches bag metasenv context ugraph lift_amount term termty tl
 310         ) else
 311           let do_match c =
 312             let subst', metasenv', ugraph' =
 313               Founif.matching
 314                 metasenv metas context term (S.lift lift_amount c) ugraph
 315             in
 316             check_metasenv "founif :" metasenv';
 317             Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
 318           in
 319           let c, other =
 320             if pos = Utils.Left then left, right
 321             else right, left
 322           in
 323           if o <> U.Incomparable then
 324             let res =
 325               try
 326                 do_match c
 327               with Founif.MatchingFailure ->
 328                 find_matches bag metasenv context ugraph lift_amount term termty tl
 329             in
 330               if Utils.debug_res then ignore (check_res res "find1");
 331               res
 332           else
 333             let res =
 334               try do_match c
 335               with Founif.MatchingFailure -> None
 336             in
 337               if Utils.debug_res then ignore (check_res res "find2");
 338             match res with
 339             | Some (_, s, _, _, _) ->
 340                 let c' = apply_subst s c in
 341                 (*
 342              let other' = U.guarded_simpl context (apply_subst s other) in *)
 343                 let other' = apply_subst s other in
 344                 let order = cmp c' other' in
 345                 if order = U.Gt then
 346                   res
 347                 else
 348                   find_matches bag
 349                     metasenv context ugraph lift_amount term termty tl
 350             | None ->
 351                 find_matches bag metasenv context ugraph lift_amount term termty tl
 352 ;;
 353
 354 let find_matches metasenv context ugraph lift_amount term termty =
 355   find_matches metasenv context ugraph lift_amount term termty
 356 ;;
 357
 358 (*
 359   as above, but finds all the matching equalities, and the matching condition
 360   can be either Founif.matching or Inference.unification
 361 *)
 362 (* XXX termty unused *)
 363 let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false)
 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 x y =
 372           let r = !Utils.compare_terms x y in
 373 (*
 374           prerr_endline (
 375                   CicPp.ppterm x ^ "   " ^
 376                   Utils.string_of_comparison r ^ "   " ^
 377                        CicPp.ppterm y );
 378 *)
 379           r
 380   in
 381   let check = match termty with C.Implicit None -> false | _ -> true in
 382   function
 383     | [] -> []
 384     | candidate::tl ->
 385         let pos, equality = candidate in
 386         let (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in
 387         if check && not (fst (CicReduction.are_convertible
 388                                 ~metasenv context termty ty ugraph)) then (
 389           find_all_matches metasenv context ugraph lift_amount term termty tl
 390         ) else
 391         let do_match c =
 392           let subst', metasenv', ugraph' =
 393             unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
 394           in
 395           (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
 396         in
 397
 398         let c, other =
 399           if pos = Utils.Left then left, right
 400           else right, left
 401         in
 402         if o <> U.Incomparable then
 403           try
 404             let res = do_match c in
 405             res::(find_all_matches ~unif_fun metasenv context ugraph
 406                     lift_amount term termty tl)
 407           with
 408           | Founif.MatchingFailure
 409           | CicUnification.UnificationFailure _
 410           | CicUnification.Uncertain _ ->
 411               find_all_matches ~unif_fun metasenv context ugraph
 412                 lift_amount term termty tl
 413         else
 414           try
 415             let res = do_match c in
 416             match res with
 417             | _, s, _, _, _ ->
 418                 let c' = apply_subst s c
 419                 and other' = apply_subst s other in
 420                 let order = cmp c' other' in
 421                 if (demod && order = U.Gt) ||
 422                    (not demod && (order <> U.Lt && order <> U.Le))
 423                 then
 424                   res::(find_all_matches ~unif_fun metasenv context ugraph
 425                           lift_amount term termty tl)
 426                 else
 427                   find_all_matches ~unif_fun metasenv context ugraph
 428                      lift_amount term termty tl
 429           with
 430           | Founif.MatchingFailure
 431           | CicUnification.UnificationFailure _
 432           | CicUnification.Uncertain _ ->
 433               find_all_matches ~unif_fun metasenv context ugraph
 434                 lift_amount term termty tl
 435 ;;
 436
 437 let find_all_matches
 438   ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
 439 =
 440     find_all_matches
 441       ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
 442   (*prerr_endline "CANDIDATES:";
 443   List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
 444   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
 445   (List.length rc));*)
 446 ;;
 447 (*
 448   returns true if target is subsumed by some equality in table
 449 *)
 450 (*
 451 let print_res l =
 452   prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
 453     ((pos,equation),_)) -> Equality.string_of_equality equation)l))
 454 ;;
 455 *)
 456
 457 let subsumption_aux use_unification env table target =
 458   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
 459   let _, context, ugraph = env in
 460   let metasenv = tmetas in
 461   let predicate, unif_fun =
 462     if use_unification then
 463       Unification, Founif.unification
 464     else
 465       Matching, Founif.matching
 466   in
 467   let leftr =
 468     match left with
 469     | Cic.Meta _ when not use_unification -> []
 470     | _ ->
 471         let leftc = get_candidates predicate table left in
 472         find_all_matches ~unif_fun
 473           metasenv context ugraph 0 left ty leftc
 474   in
 475   let rec ok what leftorright = function
 476     | [] -> None
 477     | (_, subst, menv, ug, (pos,equation))::tl ->
 478         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
 479         try
 480           let other = if pos = Utils.Left then r else l in
 481           let what' = Subst.apply_subst subst what in
 482           let other' = Subst.apply_subst subst other in
 483           let subst', menv', ug' =
 484             unif_fun metasenv m context what' other' ugraph
 485           in
 486           (match Subst.merge_subst_if_possible subst subst' with
 487           | None -> ok what leftorright tl
 488           | Some s -> Some (s, equation, leftorright <> pos ))
 489         with
 490         | Founif.MatchingFailure
 491         | CicUnification.UnificationFailure _ -> ok what leftorright tl
 492   in
 493   match ok right Utils.Left leftr with
 494   | Some _ as res -> res
 495   | None ->
 496       let rightr =
 497         match right with
 498           | Cic.Meta _ when not use_unification -> []
 499           | _ ->
 500               let rightc = get_candidates predicate table right in
 501                 find_all_matches ~unif_fun
 502                   metasenv context ugraph 0 right ty rightc
 503       in
 504         ok left Utils.Right rightr
 505 ;;
 506
 507 let subsumption x y z =
 508   subsumption_aux false x y z
 509 ;;
 510
 511 let unification x y z =
 512   subsumption_aux true x y z
 513 ;;
 514
 515 (* the target must be disjoint from the equations in the table *)
 516 let subsumption_aux_all use_unification env table target =
 517   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
 518   let _, context, ugraph = env in
 519   let metasenv = tmetas in
 520   check_for_duplicates metasenv "subsumption_aux_all";
 521   let predicate, unif_fun =
 522     if use_unification then
 523       Unification, Founif.unification
 524     else
 525       Matching, Founif.matching
 526   in
 527   let leftr =
 528     match left with
 529     | Cic.Meta _ (*when not use_unification*) -> []
 530     | _ ->
 531         let leftc = get_candidates predicate table left in
 532         find_all_matches ~unif_fun
 533           metasenv context ugraph 0 left ty leftc
 534   in
 535   let rightr =
 536         match right with
 537           | Cic.Meta _ (*when not use_unification*) -> []
 538           | _ ->
 539               let rightc = get_candidates predicate table right in
 540                 find_all_matches ~unif_fun
 541                   metasenv context ugraph 0 right ty rightc
 542   in
 543   let rec ok_all what leftorright = function
 544     | [] -> []
 545     | (_, subst, menv, ug, (pos,equation))::tl ->
 546         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
 547         try
 548           let other = if pos = Utils.Left then r else l in
 549           let what' = Subst.apply_subst subst what in
 550           let other' = Subst.apply_subst subst other in
 551           let subst', menv', ug' =
 552             unif_fun [] menv context what' other' ugraph
 553           in
 554           (match Subst.merge_subst_if_possible subst subst' with
 555           | None -> ok_all what leftorright tl
 556           | Some s ->
 557               (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
 558         with
 559         | Founif.MatchingFailure
 560         | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
 561   in
 562   (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
 563 ;;
 564
 565 let subsumption_all x y z =
 566   subsumption_aux_all false x y z
 567 ;;
 568
 569 let unification_all x y z =
 570   subsumption_aux_all true x y z
 571 ;;
 572
 573 let rec demodulation_aux bag ?from ?(typecheck=false)
 574   metasenv context ugraph table lift_amount term =
 575   let module C = Cic in
 576   let module S = CicSubstitution in
 577   let module M = CicMetaSubst in
 578   let module HL = HelmLibraryObjects in
 579   check_for_duplicates metasenv "in input a demodulation aux";
 580   let candidates =
 581     get_candidates
 582       ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
 583   in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates
 584   in
 585   let res =
 586     match term with
 587       | C.Meta _ -> None
 588       | term ->
 589           let res =
 590             try
 591               let termty, ugraph =
 592                 if typecheck then
 593                   CicTypeChecker.type_of_aux' metasenv context term ugraph
 594                 else
 595                   C.Implicit None, ugraph
 596               in
 597                 find_matches bag metasenv context ugraph
 598                   lift_amount term termty candidates
 599             with _ ->
 600               prerr_endline "type checking error";
 601               prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
 602               prerr_endline ("term: " ^ (CicPp.ppterm term));
 603               assert false;
 604               (* None *)
 605           in
 606           let res =
 607             (if Utils.debug_res then
 608             ignore(check_res res "demod1");
 609             if check_demod_res res metasenv "demod" then res else None) in
 610           if res <> None then
 611               res
 612             else
 613               match term with
 614                 | C.Appl l ->
 615                     let res, ll =
 616                       List.fold_left
 617                         (fun (res, tl) t ->
 618                            if res <> None then
 619                              (res, tl @ [S.lift 1 t])
 620                            else
 621                              let r =
 622                                demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck
 623                                  lift_amount t
 624                              in
 625                                match r with
 626                                  | None -> (None, tl @ [S.lift 1 t])
 627                                  | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 628                         (None, []) l
 629                     in (
 630                         match res with
 631                           | None -> None
 632                           | Some (_, subst, menv, ug, eq_found) ->
 633                               Some (C.Appl ll, subst, menv, ug, eq_found)
 634                       )
 635 (*
 636                 | C.Prod (nn, s, t) ->
 637                     let r1 =
 638                       demodulation_aux bag ~from:"2"
 639                         metasenv context ugraph table lift_amount s in (
 640                         match r1 with
 641                           | None ->
 642                               let r2 =
 643                                 demodulation_aux bag metasenv
 644                                   ((Some (nn, C.Decl s))::context) ugraph
 645                                   table (lift_amount+1) t
 646                               in (
 647                                   match r2 with
 648                                     | None -> None
 649                                     | Some (t', subst, menv, ug, eq_found) ->
 650                                         Some (C.Prod (nn, (S.lift 1 s), t'),
 651                                               subst, menv, ug, eq_found)
 652                                 )
 653                           | Some (s', subst, menv, ug, eq_found) ->
 654                               Some (C.Prod (nn, s', (S.lift 1 t)),
 655                                     subst, menv, ug, eq_found)
 656                       )
 657                 | C.Lambda (nn, s, t) ->
 658                     prerr_endline "siam qui";
 659                     let r1 =
 660                       demodulation_aux bag
 661                         metasenv context ugraph table lift_amount s in (
 662                         match r1 with
 663                           | None ->
 664                               let r2 =
 665                                 demodulation_aux bag metasenv
 666                                   ((Some (nn, C.Decl s))::context) ugraph
 667                                   table (lift_amount+1) t
 668                               in (
 669                                   match r2 with
 670                                     | None -> None
 671                                     | Some (t', subst, menv, ug, eq_found) ->
 672                                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 673                                               subst, menv, ug, eq_found)
 674                                 )
 675                           | Some (s', subst, menv, ug, eq_found) ->
 676                               Some (C.Lambda (nn, s', (S.lift 1 t)),
 677                                     subst, menv, ug, eq_found)
 678                       )
 679 *)
 680                 | t ->
 681                     None
 682   in
 683   if Utils.debug_res then ignore(check_res res "demod_aux output");
 684   res
 685 ;;
 686
 687 exception Foo
 688
 689 (** demodulation, when target is an equality *)
 690 let rec demodulation_equality bag ?from eq_uri env table target =
 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
 711   let build_newtarget bag is_left (t, subst, menv, ug, eq_found) =
 712
 713     if Utils.debug_metas then
 714       begin
 715         ignore(check_for_duplicates menv "input1");
 716         ignore(check_disjoint_invariant subst menv "input2");
 717         let substs = Subst.ppsubst subst in
 718         ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
 719       end;
 720     let pos, equality = eq_found in
 721     let (_, proof',
 722         (ty, what, other, _), menv',id') = Equality.open_equality equality in
 723     let ty =
 724       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 725       with CicUtil.Meta_not_found _ -> ty
 726     in
 727     let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
 728     let what, other = if pos = Utils.Left then what, other else other, what in
 729     let newterm, newproof =
 730       let bo =
 731         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 732 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
 733       let name = C.Name "x" in
 734       let bo' =
 735         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 736           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 737       in
 738           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
 739           (Cic.Lambda (name, ty, bo'))))))
 740     in
 741     let newmenv = menv in
 742     let left, right = if is_left then newterm, right else left, newterm in
 743     let ordering = !Utils.compare_terms left right in
 744     let stat = (eq_ty, left, right, ordering) in
 745     let bag, res =
 746       let w = Utils.compute_equality_weight stat in
 747       Equality.mk_equality bag (w, newproof, stat,newmenv)
 748     in
 749     if Utils.debug_metas then
 750       ignore(check_target bag context res "buildnew_target output");
 751     bag, res
 752   in
 753   let res =
 754     demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
 755   in
 756   if Utils.debug_res then check_res res "demod result";
 757   let bag, newtarget =
 758     match res with
 759     | Some t ->
 760         let bag, newtarget = build_newtarget bag true t in
 761           (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
 762           if (Equality.is_weak_identity newtarget) (* || *)
 763             (*Equality.meta_convertibility_eq target newtarget*) then
 764               bag, newtarget
 765           else
 766             demodulation_equality bag ?from eq_uri env table newtarget
 767     | None ->
 768         let res = demodulation_aux bag metasenv' context ugraph table 0 right in
 769         if Utils.debug_res then check_res res "demod result 1";
 770           match res with
 771           | Some t ->
 772               let bag, newtarget = build_newtarget bag false t in
 773                 if (Equality.is_weak_identity newtarget) ||
 774                   (Equality.meta_convertibility_eq target newtarget) then
 775                     bag, newtarget
 776                 else
 777                    demodulation_equality bag ?from eq_uri env table newtarget
 778           | None ->
 779               bag, target
 780   in
 781   (* newmeta, newtarget *)
 782   bag, newtarget
 783 ;;
 784
 785 (**
 786    Performs the beta expansion of the term "term" w.r.t. "table",
 787    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 788    in table.
 789 *)
 790 let rec betaexpand_term
 791   ?(subterms_only=false) metasenv context ugraph table lift_amount term
 792 =
 793   let module C = Cic in
 794   let module S = CicSubstitution in
 795   let module M = CicMetaSubst in
 796   let module HL = HelmLibraryObjects in
 797
 798   let res, lifted_term =
 799     match term with
 800     | C.Meta (i, l) ->
 801         let l = [] in
 802         let l', lifted_l =
 803           List.fold_right
 804             (fun arg (res, lifted_tl) ->
 805                match arg with
 806                | Some arg ->
 807                    let arg_res, lifted_arg =
 808                      betaexpand_term metasenv context ugraph table
 809                        lift_amount arg in
 810                    let l1 =
 811                      List.map
 812                        (fun (t, s, m, ug, eq_found) ->
 813                           (Some t)::lifted_tl, s, m, ug, eq_found)
 814                        arg_res
 815                    in
 816                    (l1 @
 817                       (List.map
 818                          (fun (l, s, m, ug, eq_found) ->
 819                             (Some lifted_arg)::l, s, m, ug, eq_found)
 820                          res),
 821                     (Some lifted_arg)::lifted_tl)
 822                | None ->
 823                    (List.map
 824                       (fun (r, s, m, ug, eq_found) ->
 825                          None::r, s, m, ug, eq_found) res,
 826                     None::lifted_tl)
 827             ) l ([], [])
 828         in
 829         let e =
 830           List.map
 831             (fun (l, s, m, ug, eq_found) ->
 832                (C.Meta (i, l), s, m, ug, eq_found)) l'
 833         in
 834         e, C.Meta (i, lifted_l)
 835
 836     | C.Rel m ->
 837         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 838
 839     | C.Prod (nn, s, t) ->
 840         let l1, lifted_s =
 841           betaexpand_term metasenv context ugraph table lift_amount s in
 842         let l2, lifted_t =
 843           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 844             table (lift_amount+1) t in
 845         let l1' =
 846           List.map
 847             (fun (t, s, m, ug, eq_found) ->
 848                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 849         and l2' =
 850           List.map
 851             (fun (t, s, m, ug, eq_found) ->
 852                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 853         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 854
 855     | C.Lambda (nn, s, t) ->
 856         let l1, lifted_s =
 857           betaexpand_term metasenv context ugraph table lift_amount s in
 858         let l2, lifted_t =
 859           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 860             table (lift_amount+1) t in
 861         let l1' =
 862           List.map
 863             (fun (t, s, m, ug, eq_found) ->
 864                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 865         and l2' =
 866           List.map
 867             (fun (t, s, m, ug, eq_found) ->
 868                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 869         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 870
 871     | C.Appl l ->
 872         let l', lifted_l =
 873           List.fold_left
 874             (fun (res, lifted_tl) arg ->
 875                let arg_res, lifted_arg =
 876                  betaexpand_term metasenv context ugraph table lift_amount arg
 877                in
 878                let l1 =
 879                  List.map
 880                    (fun (a, s, m, ug, eq_found) ->
 881                       a::lifted_tl, s, m, ug, eq_found)
 882                    arg_res
 883                in
 884                (l1 @
 885                   (List.map
 886                      (fun (r, s, m, ug, eq_found) ->
 887                         lifted_arg::r, s, m, ug, eq_found)
 888                      res),
 889                 lifted_arg::lifted_tl)
 890             ) ([], []) (List.rev l)
 891         in
 892         (List.map
 893            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 894          C.Appl lifted_l)
 895
 896     | t -> [], (S.lift lift_amount t)
 897   in
 898   match term with
 899   | C.Meta (i, l) -> res, lifted_term
 900   | term ->
 901       let termty, ugraph =
 902 (*        C.Implicit None, ugraph *)
 903          CicTypeChecker.type_of_aux' metasenv context term ugraph
 904       in
 905       let candidates = get_candidates Unification table term in
 906       (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
 907       let r =
 908         if subterms_only then
 909           []
 910         else
 911           find_all_matches
 912             metasenv context ugraph lift_amount term termty candidates
 913       in
 914       r @ res, lifted_term
 915 ;;
 916
 917 (**
 918    superposition_right
 919    returns a list of new clauses inferred with a right superposition step
 920    between the positive equation "target" and one in the "table" "newmeta" is
 921    the first free meta index, i.e. the first number above the highest meta
 922    index: its updated value is also returned
 923 *)
 924 let superposition_right bag
 925   ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target=
 926   let module C = Cic in
 927   let module S = CicSubstitution in
 928   let module M = CicMetaSubst in
 929   let module HL = HelmLibraryObjects in
 930   let module CR = CicReduction in
 931   let module U = Utils in
 932   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 933     Equality.open_equality target
 934   in
 935   if Utils.debug_metas then
 936     ignore (check_target bag context target "superpositionright");
 937   let metasenv' = newmetas in
 938   let res1, res2 =
 939     match ordering with
 940     | U.Gt ->
 941         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
 942     | U.Lt ->
 943         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
 944     | _ ->
 945         let res l r =
 946           List.filter
 947             (fun (_, subst, _, _, _) ->
 948                let subst = apply_subst subst in
 949                let o = !Utils.compare_terms (subst l) (subst r) in
 950                o <> U.Lt && o <> U.Le)
 951             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
 952         in
 953         (res left right), (res right left)
 954   in
 955   let build_new bag ordering (bo, s, m, ug, eq_found) =
 956     if Utils.debug_metas then
 957       ignore (check_target bag context (snd eq_found) "buildnew1" );
 958
 959     let pos, equality =  eq_found in
 960     let (_, proof', (ty, what, other, _), menv',id') =
 961       Equality.open_equality  equality in
 962     let what, other = if pos = Utils.Left then what, other else other, what in
 963
 964     let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
 965     let newgoal, newproof =
 966       (* qua *)
 967       let bo' =
 968         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
 969       in
 970       let name = C.Name "x" in
 971       let bo'' =
 972         let l, r =
 973           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 974         C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 975       in
 976       bo',
 977         Equality.Step
 978           (s,(Equality.SuperpositionRight,
 979                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
 980     in
 981     let bag, newequality =
 982       let left, right =
 983         if ordering = U.Gt then newgoal, apply_subst s right
 984         else apply_subst s left, newgoal in
 985       let neworder = !Utils.compare_terms left right in
 986       let newmenv = (* Founif.filter s *) m in
 987       let stat = (eq_ty, left, right, neworder) in
 988       let bag, eq' =
 989         let w = Utils.compute_equality_weight stat in
 990         Equality.mk_equality bag (w, newproof, stat, newmenv) in
 991       if Utils.debug_metas then
 992         ignore (check_target bag context eq' "buildnew3");
 993       let bag, eq' = Equality.fix_metas bag eq' in
 994       if Utils.debug_metas then
 995         ignore (check_target bag context eq' "buildnew4");
 996       bag, eq'
 997     in
 998     if Utils.debug_metas then
 999       ignore(check_target bag context newequality "buildnew2");
1000     bag, newequality
1001   in
1002   let bag, new1 =
1003     List.fold_right
1004       (fun x (bag,acc) ->
1005         let bag, e = build_new bag U.Gt x in
1006         bag, e::acc) res1 (bag,[])
1007   in
1008   let bag, new2 =
1009     List.fold_right
1010       (fun x (bag,acc) ->
1011         let bag, e = build_new bag U.Lt x in
1012         bag, e::acc) res2 (bag,[])
1013   in
1014   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1015   bag, List.filter ok (new1 @ new2)
1016 ;;
1017
1018 (** demodulation, when the target is a theorem *)
1019 let rec demodulation_theorem bag env table theorem =
1020   let module C = Cic in
1021   let module S = CicSubstitution in
1022   let module M = CicMetaSubst in
1023   let module HL = HelmLibraryObjects in
1024   let eq_uri =
1025     match LibraryObjects.eq_URI() with
1026     | Some u -> u
1027     | None -> assert false in
1028   let metasenv, context, ugraph = env in
1029   let proof, theo, metas = theorem in
1030   let build_newtheorem (t, subst, menv, ug, eq_found) =
1031     let pos, equality = eq_found in
1032     let (_, proof', (ty, what, other, _), menv',id) =
1033       Equality.open_equality equality in
1034     let peq =
1035       match proof' with
1036       | Equality.Exact p -> p
1037       | _ -> assert false in
1038     let what, other =
1039       if pos = Utils.Left then what, other else other, what in
1040     let newtheo = apply_subst subst (S.subst other t) in
1041     let name = C.Name "x" in
1042     let body = apply_subst subst t in
1043     let pred = C.Lambda(name,ty,body) in
1044     let newproof =
1045       match pos with
1046         | Utils.Left ->
1047           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1048         | Utils.Right ->
1049           Equality.mk_eq_ind eq_uri ty what pred proof other peq
1050     in
1051     newproof,newtheo
1052   in
1053   let res = demodulation_aux bag metas context ugraph table 0 theo in
1054   match res with
1055   | Some t ->
1056       let newproof, newtheo = build_newtheorem t in
1057       if Equality.meta_convertibility theo newtheo then
1058         newproof, newtheo
1059       else
1060         demodulation_theorem bag env table (newproof,newtheo,[])
1061   | None ->
1062       proof,theo
1063 ;;
1064
1065 (*****************************************************************************)
1066 (**                         OPERATIONS ON GOALS                             **)
1067 (**                                                                         **)
1068 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
1069 (*****************************************************************************)
1070
1071 (* new: demodulation of non_equality terms *)
1072 let build_newg bag context goal rule expansion =
1073   let goalproof,_,_ = goal in
1074   let (t,subst,menv,ug,eq_found) = expansion in
1075   let pos, equality = eq_found in
1076   let (_, proof', (ty, what, other, _), menv',id) =
1077     Equality.open_equality equality in
1078   let what, other = if pos = Utils.Left then what, other else other, what in
1079   let newterm, newgoalproof =
1080     let bo =
1081       Utils.guarded_simpl context
1082         (apply_subst subst (CicSubstitution.subst other t))
1083     in
1084     let name = Cic.Name "x" in
1085     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1086     let newgoalproofstep = (rule,pos,id,subst,pred) in
1087     bo, (newgoalproofstep::goalproof)
1088   in
1089   let newmetasenv = (* Founif.filter subst *) menv in
1090   (newgoalproof, newmetasenv, newterm)
1091 ;;
1092
1093 let rec demod bag env table goal =
1094   let _,menv,t = goal in
1095   let _, context, ugraph = env in
1096   let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
1097   match res with
1098     | Some newt ->
1099         let newg =
1100           build_newg bag context goal Equality.Demodulation newt
1101         in
1102         let _,_,newt = newg in
1103         if Equality.meta_convertibility t newt then
1104           false, goal
1105         else
1106           true, snd (demod bag env table newg)
1107     | None ->
1108         false, goal
1109 ;;
1110
1111 let open_goal g =
1112   match g with
1113   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
1114       (* assert (LibraryObjects.is_eq_URI uri); *)
1115       proof,menv,eq,ty,l,r
1116   | _ -> assert false
1117
1118 let ty_of_goal (_,_,ty) = ty ;;
1119
1120 (* checks if two goals are metaconvertible *)
1121 let goal_metaconvertibility_eq g1 g2 =
1122   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1123 ;;
1124
1125 (* when the betaexpand_term function is called on the left/right side of the
1126  * goal, the predicate has to be fixed
1127  * C[x] ---> (eq ty unchanged C[x])
1128  * [posu] is the side of the [unchanged] term in the original goal
1129  *)
1130
1131 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1132   let _,_,eq,ty,l,r = open_goal goal in
1133   let unchanged = if posu = Utils.Left then l else r in
1134   let unchanged = CicSubstitution.lift 1 unchanged in
1135   let ty = CicSubstitution.lift 1 ty in
1136   let pred =
1137     match posu with
1138     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1139     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1140   in
1141   (pred, subst, menv, ug, eq_f)
1142 ;;
1143
1144 (* ginve the old [goal], the side that has not changed [posu] and the
1145  * expansion builds a new goal *)
1146 let build_newgoal bag context goal posu rule expansion =
1147   let goalproof,_,_,_,_,_ = open_goal goal in
1148   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1149   let pos, equality = eq_found in
1150   let (_, proof', (ty, what, other, _), menv',id) =
1151     Equality.open_equality equality in
1152   let what, other = if pos = Utils.Left then what, other else other, what in
1153   let newterm, newgoalproof =
1154     let bo =
1155       Utils.guarded_simpl context
1156         (apply_subst subst (CicSubstitution.subst other t))
1157     in
1158     let name = Cic.Name "x" in
1159     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
1160     let newgoalproofstep = (rule,pos,id,subst,pred) in
1161     bo, (newgoalproofstep::goalproof)
1162   in
1163   let newmetasenv = (* Founif.filter subst *) menv in
1164   (newgoalproof, newmetasenv, newterm)
1165 ;;
1166
1167 (**
1168    superposition_left
1169    returns a list of new clauses inferred with a left superposition step
1170    the negative equation "target" and one of the positive equations in "table"
1171 *)
1172 let superposition_left bag (metasenv, context, ugraph) table goal =
1173   let names = Utils.names_of_context context in
1174   let proof,menv,eq,ty,l,r = open_goal goal in
1175   let c = !Utils.compare_terms l r in
1176   let newgoals =
1177     if c = Utils.Incomparable then
1178       begin
1179       let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1180       let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1181       (* prerr_endline "incomparable";
1182       prerr_endline (string_of_int (List.length expansionsl));
1183       prerr_endline (string_of_int (List.length expansionsr));
1184       *)
1185       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1186       @
1187       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1188       end
1189     else
1190         match c with
1191         | Utils.Gt ->
1192             let big,small,possmall = l,r,Utils.Right in
1193             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1194             List.map
1195               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1196               expansions
1197         | Utils.Lt -> (* prerr_endline "LT"; *)
1198             let big,small,possmall = r,l,Utils.Left in
1199             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1200             List.map
1201               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1202               expansions
1203         | Utils.Eq -> []
1204         | _ ->
1205             prerr_endline
1206               ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1207             assert false
1208   in
1209   (* rinfresco le meta *)
1210   List.fold_right
1211     (fun g (b,acc) ->
1212        let b,g = Equality.fix_metas_goal b g in
1213        b,g::acc)
1214     newgoals (bag,[])
1215 ;;
1216
1217 (** demodulation, when the target is a goal *)
1218 let rec demodulation_goal bag env table goal =
1219   let goalproof,menv,_,_,left,right = open_goal goal in
1220   let _, context, ugraph = env in
1221 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
1222   let do_right () =
1223       let resright = demodulation_aux bag menv context ugraph table 0 right in
1224       match resright with
1225       | Some t ->
1226           let newg =
1227             build_newgoal bag context goal Utils.Left Equality.Demodulation t
1228           in
1229           if goal_metaconvertibility_eq goal newg then
1230             false, goal
1231           else
1232             true, snd (demodulation_goal bag env table newg)
1233       | None -> false, goal
1234   in
1235   let resleft = demodulation_aux bag menv context ugraph table 0 left in
1236   match resleft with
1237   | Some t ->
1238       let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1239       if goal_metaconvertibility_eq goal newg then
1240         do_right ()
1241       else
1242         true, snd (demodulation_goal bag env table newg)
1243   | None -> do_right ()
1244 ;;
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           ~unif_fun:Founif.matching ~demod:true
1262             metasenv context ugraph lift_amount term termty candidates
1263       in
1264       match term with
1265       | C.Appl l ->
1266          let res, _, _ =
1267            List.fold_left
1268             (fun (res,l,r) t ->
1269                res @
1270                List.map
1271                  (fun (rel, s, m, ug, c) ->
1272                    (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1273                  (demodulation_all_aux
1274                    metasenv context ugraph table lift_amount t),
1275                l@[List.hd r], List.tl r)
1276             (res, [], List.map (S.lift 1) l) l
1277          in
1278          res
1279       | t -> res
1280 ;;
1281
1282 let demod_all steps bag env table goal =
1283   let _, context, ugraph = env in
1284   let is_visited l (_,_,t) =
1285     List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
1286   in
1287   let rec aux steps visited bag = function
1288     | _ when steps = 0 -> visited, bag, []
1289     | [] -> visited, bag, []
1290     | goal :: rest when is_visited visited goal -> aux steps visited bag rest
1291     | goal :: rest ->
1292         let visited = goal :: visited in
1293         let _,menv,t = goal in
1294         let res = demodulation_all_aux menv context ugraph table 0 t in
1295         let steps = if res = [] then steps-1 else steps in
1296         let new_goals =
1297           List.map (build_newg bag context goal Equality.Demodulation) res
1298         in
1299         let visited, bag, res = aux steps visited bag (new_goals @ rest) in
1300         visited, bag, goal :: res
1301   in
1302    aux steps [] bag [goal]
1303 ;;
1304
1305
1306 let solve_demodulating bag env table initgoal steps =
1307   let proof,menv,eq,ty,left,right = open_goal initgoal in
1308   let uri =
1309     match eq with
1310     | Cic.MutInd (u,_,_) -> u
1311     | _ -> assert false
1312   in
1313   let _, context, ugraph = env in
1314   let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
1315   let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
1316   let is_solved left right ml mr =
1317     let m = ml @ (List.filter
1318       (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr)
1319     in
1320     try
1321       let s,_,_ =
1322         Founif.unification [] m context left right CicUniv.empty_ugraph in
1323       Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left))
1324     with CicUnification.UnificationFailure _ ->
1325       let solutions =
1326        unification_all env table (Equality.mk_tmp_equality
1327           (0,(Cic.Implicit None,left,right,Utils.Incomparable),m))
1328       in
1329       if solutions = [] then None
1330       else
1331         let s, e, swapped = List.hd solutions in
1332         let _,p,(ty,l,r,_),me,id = Equality.open_equality e in
1333         let bag, p =
1334           if swapped then Equality.symmetric bag ty l id uri me else bag, p
1335         in
1336         Some (bag, m,s, p)
1337   in
1338   let newgoal =
1339    HExtlib.list_findopt
1340      (fun (pr,mr,r) _ ->
1341          try
1342            let pl,ml,l,bag,m,s,p =
1343              match
1344              HExtlib.list_findopt (fun (pl,ml,l) _ ->
1345                match is_solved l r ml mr with
1346                | None -> None
1347                | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p)
1348              ) l_demod
1349              with Some x -> x | _ -> raise Not_found
1350            in
1351            let pl =
1352              List.map
1353                (fun (rule,pos,id,subst,pred) ->
1354                  let pred =
1355                    match pred with
1356                    | Cic.Lambda (name,src,tgt) ->
1357                        Cic.Lambda (name,src,
1358                          Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
1359                    | _ -> assert false
1360                  in
1361                  rule,pos,id,subst,pred)
1362                pl
1363            in
1364            let pr =
1365              List.map
1366                (fun (rule,pos,id,subst,pred) ->
1367                  let pred =
1368                    match pred with
1369                    | Cic.Lambda (name,src,tgt) ->
1370                        Cic.Lambda (name,src,
1371                          Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
1372                    | _ -> assert false
1373                  in
1374                  rule,pos,id,subst,pred)
1375                pr
1376            in
1377            Some (bag,pr@pl@proof,m,s,p)
1378          with Not_found -> None)
1379      r_demod
1380   in
1381   newgoal
1382 ;;
1383
1384
1385