helm/software/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           let subst = Subst.buildsubst i context t ty subst in
 110           subst, menv
 111         with CicUtil.Meta_not_found m ->
 112           let names = names_of_context context in
 113           (*debug_print
 114             (lazy*) prerr_endline
 115                (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
 116                   (CicPp.pp t1 names) (CicPp.pp t2 names)
 117                   (print_metasenv menv) (print_metasenv metasenv));
 118           assert false
 119       )
 120     | _, C.Meta _ -> unif subst menv t s
 121     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
 122         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 123     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
 124         try
 125           List.fold_left2
 126             (fun (subst', menv) s t -> unif subst' menv s t)
 127             (subst, menv) tls tlt
 128         with Invalid_argument _ ->
 129           raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 130       )
 131     | _, _ ->
 132         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 133   in
 134   let subst, menv = unif Subst.empty_subst metasenv t1 t2 in
 135   let menv = Subst.filter subst menv in
 136   subst, menv, ugraph
 137 ;;
 138
 139 let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
 140 let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
 141 let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
 142 let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 143
 144 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
 145   let metasenv =
 146     HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2))
 147     (* metasenv1 @ metasenv2 *)
 148   in
 149   let subst, menv, ug =
 150     if not (is_simple_term t1) || not (is_simple_term t2) then (
 151       debug_print
 152         (lazy
 153            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
 154               (CicPp.ppterm t1) (CicPp.ppterm t2)));
 155       raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif"))
 156     ) else
 157       if b then
 158         (* full unification *)
 159         unification_simple [] metasenv context t1 t2 ugraph
 160       else
 161         (* matching: metasenv1 is locked *)
 162         unification_simple metasenv1 metasenv context t1 t2 ugraph
 163   in
 164   if Utils.debug_res then
 165             ignore(check_disjoint_invariant subst menv "unif");
 166   (* let flatten subst =
 167     List.map
 168       (fun (i, (context, term, ty)) ->
 169          let context = apply_subst_context subst context in
 170          let term = apply_subst subst term in
 171          let ty = apply_subst subst ty in
 172            (i, (context, term, ty))) subst
 173   in
 174   let flatten subst = profiler.HExtlib.profile flatten subst in
 175   let subst = flatten subst in *)
 176     subst, menv, ug
 177 ;;
 178
 179 exception MatchingFailure;;
 180
 181 (** matching takes in input the _disjoint_ metasenv of t1 and  t2;
 182 it perform unification in the union metasenv, then check that
 183 the first metasenv has not changed *)
 184 let matching metasenv1 metasenv2 context t1 t2 ugraph =
 185   try
 186     unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
 187   with
 188     CicUnification.UnificationFailure _ ->
 189       raise MatchingFailure
 190 ;;
 191
 192 let unification m1 m2 c t1 t2 ug =
 193   try
 194     unification_aux true m1 m2 c t1 t2 ug
 195   with exn ->
 196     raise exn
 197 ;;
 198
 199 let get_stats () = "" (*<:show<Inference.>>*) ;;