components/tactics/paramodulation/founif.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 open Utils;;
  31 open Printf;;
  32
  33 let debug_print s = ();;(*prerr_endline (Lazy.force s);;*)
  34
  35 let check_disjoint_invariant subst metasenv msg =
  36   if (List.exists
  37         (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
  38   then
  39     begin
  40       prerr_endline ("not disjoint: " ^ msg);
  41       assert false
  42     end
  43 ;;
  44
  45 let rec check_irl start = function
  46   | [] -> true
  47   | None::tl -> check_irl (start+1) tl
  48   | (Some (Cic.Rel x))::tl ->
  49       if x = start then check_irl (start+1) tl else false
  50   | _ -> false
  51 ;;
  52
  53 let rec is_simple_term = function
  54   | Cic.Appl ((Cic.Meta _)::_) -> false
  55   | Cic.Appl l -> List.for_all is_simple_term l
  56   | Cic.Meta (i, l) -> let l = [] in check_irl 1 l
  57   | Cic.Rel _ -> true
  58   | Cic.Const _ -> true
  59   | Cic.MutInd (_, _, []) -> true
  60   | Cic.MutConstruct (_, _, _, []) -> true
  61   | _ -> false
  62 ;;
  63
  64 let locked menv i =
  65   List.exists (fun (j,_,_) -> i = j) menv
  66 ;;
  67
  68 let unification_simple locked_menv metasenv context t1 t2 ugraph =
  69   let module C = Cic in
  70   let module M = CicMetaSubst in
  71   let module U = CicUnification in
  72   let lookup = Subst.lookup_subst in
  73   let rec occurs_check subst what where =
  74     match where with
  75     | Cic.Meta(i,_) when i = what -> true
  76     | C.Appl l -> List.exists (occurs_check subst what) l
  77     | C.Meta _ ->
  78         let t = lookup where subst in
  79         if t <> where then occurs_check subst what t else false
  80     | _ -> false
  81   in
  82   let rec unif subst menv s t =
  83     let s = match s with C.Meta _ -> lookup s subst | _ -> s
  84     and t = match t with C.Meta _ -> lookup t subst | _ -> t
  85
  86     in
  87     match s, t with
  88     | s, t when s = t -> subst, menv
  89     (* sometimes the same meta has different local contexts; this
  90        could create "cyclic" substitutions *)
  91     | C.Meta (i, _), C.Meta (j, _) when i=j ->  subst, menv
  92     | C.Meta (i, _), C.Meta (j, _)
  93         when (locked locked_menv i) &&(locked locked_menv j) ->
  94         raise
  95           (U.UnificationFailure (lazy "Inference.unification.unif"))
  96     | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->
  97         unif subst menv t s
  98     | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
  99         unif subst menv t s
 100     | C.Meta (i,_), t when occurs_check subst i t ->
 101         raise
 102           (U.UnificationFailure (lazy "Inference.unification.unif"))
 103     | C.Meta (i, l), t when (locked locked_menv i) ->
 104         raise
 105           (U.UnificationFailure (lazy "Inference.unification.unif"))
 106     | C.Meta (i, l), t -> (
 107         try
 108           let _, _, ty = CicUtil.lookup_meta i menv in
 109           assert (not (Subst.is_in_subst i subst));
 110           let subst = Subst.buildsubst i context t ty subst in
 111           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
 112           subst, menv
 113         with CicUtil.Meta_not_found m ->
 114           let names = names_of_context context in
 115           (*debug_print
 116             (lazy*) prerr_endline
 117                (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
 118                   (CicPp.pp t1 names) (CicPp.pp t2 names)
 119                   (print_metasenv menv) (print_metasenv metasenv));
 120           assert false
 121       )
 122     | _, C.Meta _ -> unif subst menv t s
 123     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
 124         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 125     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
 126         try
 127           List.fold_left2
 128             (fun (subst', menv) s t -> unif subst' menv s t)
 129             (subst, menv) tls tlt
 130         with Invalid_argument _ ->
 131           raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 132       )
 133     | _, _ ->
 134         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 135   in
 136   let subst, menv = unif Subst.empty_subst metasenv t1 t2 in
 137   let menv = Subst.filter subst menv in
 138   subst, menv, ugraph
 139 ;;
 140
 141 let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
 142 let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
 143 let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
 144 let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 145
 146 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
 147   let metasenv =
 148     HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2))
 149     (* metasenv1 @ metasenv2 *)
 150   in
 151   let subst, menv, ug =
 152     if not (is_simple_term t1) || not (is_simple_term t2) then (
 153       debug_print
 154         (lazy
 155            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
 156               (CicPp.ppterm t1) (CicPp.ppterm t2)));
 157       raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif"))
 158     ) else
 159       if b then
 160         (* full unification *)
 161         unification_simple [] metasenv context t1 t2 ugraph
 162       else
 163         (* matching: metasenv1 is locked *)
 164         unification_simple metasenv1 metasenv context t1 t2 ugraph
 165   in
 166   if Utils.debug_res then
 167             ignore(check_disjoint_invariant subst menv "unif");
 168   (* let flatten subst =
 169     List.map
 170       (fun (i, (context, term, ty)) ->
 171          let context = apply_subst_context subst context in
 172          let term = apply_subst subst term in
 173          let ty = apply_subst subst ty in
 174            (i, (context, term, ty))) subst
 175   in
 176   let flatten subst = profiler.HExtlib.profile flatten subst in
 177   let subst = flatten subst in *)
 178     subst, menv, ug
 179 ;;
 180
 181 exception MatchingFailure;;
 182
 183 (** matching takes in input the _disjoint_ metasenv of t1 and  t2;
 184 it perform unification in the union metasenv, then check that
 185 the first metasenv has not changed *)
 186 let matching metasenv1 metasenv2 context t1 t2 ugraph =
 187   try
 188     unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
 189   with
 190     CicUnification.UnificationFailure _ ->
 191       raise MatchingFailure
 192 ;;
 193
 194 let unification m1 m2 c t1 t2 ug =
 195   try
 196     unification_aux true m1 m2 c t1 t2 ug
 197   with exn ->
 198     raise exn
 199 ;;
 200
 201 let get_stats () = "" (*<:show<Inference.>>*) ;;