]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_unification/cicUnification.ml
New syntax.
[helm.git] / helm / ocaml / cic_unification / cicUnification.ml
1 (* Copyright (C) 2000, 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 open Printf
27
28 exception UnificationFailure of string;;
29 exception Uncertain of string;;
30 exception AssertFailure of string;;
31
32 let debug_print = prerr_endline
33
34 let type_of_aux' metasenv subst context term =
35   try
36     CicMetaSubst.type_of_aux' metasenv subst context term
37   with
38   | CicMetaSubst.MetaSubstFailure msg ->
39     raise (AssertFailure
40       ((sprintf
41         "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
42         (CicMetaSubst.ppterm subst term)
43         (CicMetaSubst.ppcontext subst context)
44         (CicMetaSubst.ppmetasenv metasenv subst) msg)))
45
46 (* NUOVA UNIFICAZIONE *)
47 (* A substitution is a (int * Cic.term) list that associates a
48    metavariable i with its body.
49    A metaenv is a (int * Cic.term) list that associate a metavariable
50    i with is type. 
51    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
52    a new substitution which is _NOT_ unwinded. It must be unwinded before
53    applying it. *)
54
55 let rec fo_unif_subst test_equality_only subst context metasenv t1 t2 =  
56  let module C = Cic in
57  let module R = CicMetaSubst in
58  let module S = CicSubstitution in
59   match (t1, t2) with
60      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
61        let ok,subst,metasenv =
62        try
63         List.fold_left2
64          (fun (b,subst,metasenv) t1 t2 ->
65            if b then true,subst,metasenv else
66             match t1,t2 with
67                None,_
68              | _,None -> true,subst,metasenv
69              | Some t1', Some t2' ->
70                 (* First possibility:  restriction    *)
71                 (* Second possibility: unification    *)
72                 (* Third possibility:  convertibility *)
73                 if R.are_convertible subst context t1' t2' then
74                  true,subst,metasenv
75                 else
76                  (try
77                    let subst,metasenv =
78                     fo_unif_subst 
79                      test_equality_only subst context metasenv t1' t2'
80                    in
81                     true,subst,metasenv
82                  with
83                   Not_found -> false,subst,metasenv)
84          ) (true,subst,metasenv) ln lm
85        with
86         Invalid_argument _ ->
87          raise (UnificationFailure (sprintf
88            "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
89        in
90         if ok then
91           subst,metasenv
92         else
93           raise (UnificationFailure (sprintf
94             "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
95             (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
96    | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
97        fo_unif_subst test_equality_only subst context metasenv t2 t1
98    | (C.Meta (n,l), t)   
99    | (t, C.Meta (n,l)) ->
100        let swap =
101         match t1,t2 with
102            C.Meta (n,_), C.Meta (m,_) when n < m -> false
103          | _, C.Meta _ -> false
104          | _,_ -> true
105        in
106        let lower = fun x y -> if swap then y else x in
107        let upper = fun x y -> if swap then x else y in
108        let fo_unif_subst_ordered 
109         test_equality_only subst context metasenv m1 m2 =
110           fo_unif_subst test_equality_only subst context metasenv 
111            (lower m1 m2) (upper m1 m2)
112        in
113        let subst'',metasenv' =
114         try
115          let oldt = (List.assoc n subst) in
116          let lifted_oldt = S.lift_meta l oldt in
117           fo_unif_subst_ordered 
118            test_equality_only subst context metasenv t lifted_oldt
119         with Not_found ->
120          let t',metasenv',subst' =
121           try
122            CicMetaSubst.delift n subst context metasenv l t
123           with
124              (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
125            | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
126          in
127           let t'' =
128            match t' with
129               C.Sort (C.Type u) when not test_equality_only ->
130                 let u' = CicUniv.fresh () in
131                 let s = C.Sort (C.Type u') in
132                  ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
133                 s
134              | _ -> t'
135           in
136            (n, t'')::subst', metasenv'
137        in
138         let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
139         (try
140           let tyt =
141             type_of_aux' metasenv' subst'' context t
142           in
143            fo_unif_subst 
144             test_equality_only 
145              subst'' context metasenv' tyt (S.lift_meta l meta_type)
146         with AssertFailure _ ->
147           (* TODO huge hack!!!!
148            * we keep on unifying/refining in the hope that the problem will be
149            * eventually solved. In the meantime we're breaking a big invariant:
150            * the terms that we are unifying are no longer well typed in the
151            * current context (in the worst case we could even diverge)
152            *)
153 (*
154 prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
155 prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
156 *)
157           (subst'', metasenv'))
158    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
159    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
160       if UriManager.eq uri1 uri2 then
161        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
162         exp_named_subst1 exp_named_subst2
163       else
164        raise (UnificationFailure (sprintf
165         "Can't unify %s with %s due to different constants"
166         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
167    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
168       if UriManager.eq uri1 uri2 && i1 = i2 then
169        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
170         exp_named_subst1 exp_named_subst2
171       else
172        raise (UnificationFailure (sprintf
173         "Can't unify %s with %s due to different inductive principles"
174         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
175    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
176      C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
177       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
178        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
179         exp_named_subst1 exp_named_subst2
180       else
181        raise (UnificationFailure (sprintf
182         "Can't unify %s with %s due to different inductive constructors"
183         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
184    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
185    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
186                               subst context metasenv te t2
187    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only 
188                               subst context metasenv t1 te
189    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
190         (* TASSI: this is the only case in which we want == *)
191        let subst',metasenv' = fo_unif_subst true 
192                                subst context metasenv s1 s2 in
193         fo_unif_subst test_equality_only 
194          subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
195    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 
196         (* TASSI: ask someone a reason for not putting true here *)
197        let subst',metasenv' = fo_unif_subst test_equality_only 
198                                subst context metasenv s1 s2 in
199         fo_unif_subst test_equality_only 
200          subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
201    | (C.LetIn (_,s1,t1), t2)  
202    | (t2, C.LetIn (_,s1,t1)) -> 
203        fo_unif_subst 
204         test_equality_only subst context metasenv t2 (S.subst s1 t1)
205    | (C.Appl l1, C.Appl l2) -> 
206        let lr1 = List.rev l1 in
207        let lr2 = List.rev l2 in
208        let rec fo_unif_l test_equality_only subst metasenv =
209         function
210            [],_
211          | _,[] -> assert false
212          | ([h1],[h2]) ->
213              fo_unif_subst test_equality_only subst context metasenv h1 h2
214          | ([h],l) 
215          | (l,[h]) ->
216              fo_unif_subst 
217               test_equality_only subst context metasenv h (C.Appl (List.rev l))
218          | ((h1::l1),(h2::l2)) -> 
219             let subst', metasenv' = 
220              fo_unif_subst test_equality_only subst context metasenv h1 h2
221             in 
222              fo_unif_l test_equality_only subst' metasenv' (l1,l2)
223        in
224         fo_unif_l test_equality_only subst metasenv (lr1, lr2) 
225    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
226        let subst', metasenv' = 
227         fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
228        let subst'',metasenv'' = 
229         fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in
230        (try
231          List.fold_left2 
232           (function (subst,metasenv) ->
233             fo_unif_subst test_equality_only subst context metasenv
234           ) (subst'',metasenv'') pl1 pl2 
235         with
236          Invalid_argument _ ->
237           raise (UnificationFailure (sprintf
238             "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
239    | (C.Rel _, _) | (_,  C.Rel _)
240    | (C.Sort _ ,_) | (_, C.Sort _)
241    | (C.Const _, _) | (_, C.Const _)
242    | (C.MutInd  _, _) | (_, C.MutInd _)
243    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
244    | (C.Fix _, _) | (_, C.Fix _) 
245    | (C.CoFix _, _) | (_, C.CoFix _) -> 
246        if R.are_convertible subst context t1 t2 then
247         subst, metasenv
248        else
249         raise (UnificationFailure (sprintf
250           "Can't unify %s with %s because they are not convertible"
251           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
252    | (_,_) ->
253        if R.are_convertible subst context t1 t2 then
254         subst, metasenv
255        else
256         raise (UnificationFailure (sprintf
257           "Can't unify %s with %s because they are not convertible"
258           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
259
260 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
261  exp_named_subst1 exp_named_subst2
262 =
263  try
264   List.fold_left2
265    (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
266      assert (uri1=uri2) ;
267      fo_unif_subst test_equality_only subst context metasenv t1 t2
268    ) (subst,metasenv) exp_named_subst1 exp_named_subst2
269  with
270   Invalid_argument _ ->
271    let print_ens ens =
272     String.concat " ; "
273      (List.map
274        (fun (uri,t) ->
275          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
276        ) ens) 
277    in
278     raise (UnificationFailure (sprintf
279      "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))
280
281 (* A substitution is a (int * Cic.term) list that associates a               *)
282 (* metavariable i with its body.                                             *)
283 (* metasenv is of type Cic.metasenv                                          *)
284 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
285 (* a new substitution which is already unwinded and ready to be applied and  *)
286 (* a new metasenv in which some hypothesis in the contexts of the            *)
287 (* metavariables may have been restricted.                                   *)
288 let fo_unif metasenv context t1 t2 = 
289  fo_unif_subst false [] context metasenv t1 t2 ;;
290
291 let fo_unif_subst subst context metasenv t1 t2 =
292   let enrich_msg msg =
293     sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
294       (CicMetaSubst.ppterm subst t1)
295       (try
296         CicPp.ppterm (type_of_aux' metasenv subst context t1)
297       with _ -> "MALFORMED")
298       (CicMetaSubst.ppterm subst t2)
299       (try
300         CicPp.ppterm (type_of_aux' metasenv subst context t2)
301       with _ -> "MALFORMED")
302       (CicMetaSubst.ppcontext subst context)
303       (CicMetaSubst.ppmetasenv metasenv subst) msg
304   in
305   try
306     fo_unif_subst false subst context metasenv t1 t2
307   with
308   | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
309   | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))
310 ;;
311