]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/paramodulation/founif.ml
2a9de5ffa8c2d74440dbd2551debdf09ba499ce1
[helm.git] / 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.>>*) ;;