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 check_for_duplicates metas msg =
 145   let rec aux = function
 146     | [] -> true
 147     | (m,_,_)::tl ->
 148         not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in
 149   let b = aux metas in
 150   if not b then
 151     begin
 152       prerr_endline ("DUPLICATI ---- " ^ msg);
 153       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 154       assert false
 155     end
 156   else b
 157 ;;
 158
 159 let check_metasenv msg menv =
 160   List.iter
 161     (fun (i,ctx,ty) ->
 162        try ignore(CicTypeChecker.type_of_aux' menv ctx ty
 163                   CicUniv.empty_ugraph)
 164        with
 165          | CicUtil.Meta_not_found _ ->
 166              prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv);
 167              assert false
 168          | _ -> ()
 169     ) menv
 170 ;;
 171
 172 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
 173   let metasenv = metasenv1@metasenv2 in
 174   if Utils.debug_metas then
 175     begin
 176       ignore(check_for_duplicates metasenv "unification_aux");
 177       check_metasenv "unification_aux" metasenv;
 178     end;
 179   let subst, menv, ug =
 180     if not (is_simple_term t1) || not (is_simple_term t2) then (
 181       debug_print
 182         (lazy
 183            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
 184               (CicPp.ppterm t1) (CicPp.ppterm t2)));
 185       raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif"))
 186     ) else
 187       if b then
 188         (* full unification *)
 189         unification_simple [] metasenv context t1 t2 ugraph
 190       else
 191         (* matching: metasenv1 is locked *)
 192         unification_simple metasenv1 metasenv context t1 t2 ugraph
 193   in
 194   if Utils.debug_res then
 195             ignore(check_disjoint_invariant subst menv "unif");
 196   (* let flatten subst =
 197     List.map
 198       (fun (i, (context, term, ty)) ->
 199          let context = apply_subst_context subst context in
 200          let term = apply_subst subst term in
 201          let ty = apply_subst subst ty in
 202            (i, (context, term, ty))) subst
 203   in
 204   let flatten subst = profiler.HExtlib.profile flatten subst in
 205   let subst = flatten subst in *)
 206   if Utils.debug_metas then
 207     ignore(check_for_duplicates menv "unification_aux prima di apply_subst");
 208   let menv = Subst.apply_subst_metasenv subst menv in
 209   if Utils.debug_metas then
 210     (let _ = check_for_duplicates menv "unif_aux after" in
 211     check_metasenv "unification_aux after 1" menv);
 212   subst, menv, ug
 213 ;;
 214
 215 exception MatchingFailure;;
 216
 217 (** matching takes in input the _disjoint_ metasenv of t1 and  t2;
 218 it perform unification in the union metasenv, then check that
 219 the first metasenv has not changed *)
 220 let matching metasenv1 metasenv2 context t1 t2 ugraph =
 221   try
 222     unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
 223   with
 224     CicUnification.UnificationFailure _ ->
 225       raise MatchingFailure
 226 ;;
 227
 228 let unification m1 m2 c t1 t2 ug =
 229   let m1 =
 230     if (m1 = m2 && m1 <> []) then assert false
 231       (* (prerr_endline "eccoci 2"; []) *) else m1 in
 232   (*
 233   prerr_endline (CicPp.ppterm t1);
 234   prerr_endline (CicPp.ppterm t2);
 235   prerr_endline "++++++++++"; *)
 236   try
 237     unification_aux true m1 m2 c t1 t2 ug
 238   with exn ->
 239     raise exn
 240 ;;
 241
 242 let get_stats () = "" (*<:show<Inference.>>*) ;;