]> matita.cs.unibo.it Git - helm.git/blob - components/cic_unification/cicUnification.ml
Patch to the unification to make the case (i l) vs (t l) work when i is
[helm.git] / components / 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 (* $Id$ *)
27
28 open Printf
29
30 exception UnificationFailure of string Lazy.t;;
31 exception Uncertain of string Lazy.t;;
32 exception AssertFailure of string Lazy.t;;
33
34 let verbose = false;;
35 let debug_print = fun _ -> () 
36
37 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
38 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
39 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
40 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
41
42 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
43
44 let type_of_aux' metasenv subst context term ugraph =
45 let foo () =
46   try 
47     profile.HExtlib.profile
48       (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph 
49   with
50       CicTypeChecker.TypeCheckerFailure msg ->
51         let msg =
52          lazy
53           (sprintf
54            "Kernel Type checking error: 
55 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
56              (CicMetaSubst.ppterm subst term)
57              (CicMetaSubst.ppterm [] term)
58              (CicMetaSubst.ppcontext subst context)
59              (CicMetaSubst.ppmetasenv subst metasenv) 
60              (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
61         raise (AssertFailure msg)
62     | CicTypeChecker.AssertFailure msg ->
63         let msg = lazy
64          (sprintf
65            "Kernel Type checking assertion failure: 
66 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
67              (CicMetaSubst.ppterm subst term)
68              (CicMetaSubst.ppterm [] term)
69              (CicMetaSubst.ppcontext subst context)
70              (CicMetaSubst.ppmetasenv subst metasenv) 
71              (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
72         raise (AssertFailure msg)
73 in profiler_toa.HExtlib.profile foo ()
74 ;;
75
76 let exists_a_meta l = 
77   List.exists (function Cic.Meta _ -> true | _ -> false) l
78
79 let rec deref subst t =
80   let snd (_,a,_) = a in
81   match t with
82       Cic.Meta(n,l) -> 
83         (try 
84            deref subst
85              (CicSubstitution.subst_meta 
86                 l (snd (CicUtil.lookup_subst n subst))) 
87          with 
88              CicUtil.Subst_not_found _ -> t)
89     | Cic.Appl(Cic.Meta(n,l)::args) ->
90         (match deref subst (Cic.Meta(n,l)) with
91            | Cic.Lambda _ as t -> 
92                deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
93            | r -> Cic.Appl(r::args))
94     | Cic.Appl(((Cic.Lambda _) as t)::args) ->
95            deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
96     | t -> t
97 ;; 
98
99 let deref subst t =
100  let foo () = deref subst t
101  in profiler_deref.HExtlib.profile foo ()
102
103 exception WrongShape;;
104 let eta_reduce after_beta_expansion after_beta_expansion_body
105      before_beta_expansion
106  =
107  try
108   match before_beta_expansion,after_beta_expansion_body with
109      Cic.Appl l, Cic.Appl l' ->
110       let rec all_but_last check_last =
111        function
112           [] -> assert false
113         | [Cic.Rel 1] -> []
114         | [_] -> if check_last then raise WrongShape else []
115         | he::tl -> he::(all_but_last check_last tl)
116       in
117        let all_but_last check_last l =
118         match all_but_last check_last l with
119            [] -> assert false
120          | [he] -> he
121          | l -> Cic.Appl l
122        in
123        let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
124        let all_but_last = all_but_last false l in
125         (* here we should test alpha-equivalence; however we know by
126            construction that here alpha_equivalence is equivalent to = *)
127         if t = all_but_last then
128          all_but_last
129         else
130          after_beta_expansion
131    | _,_ -> after_beta_expansion
132  with
133   WrongShape -> after_beta_expansion
134
135 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
136  let module S = CicSubstitution in
137  let module C = Cic in
138 let foo () =
139   let rec aux metasenv subst n context t' ugraph =
140    try
141
142     let subst,metasenv,ugraph1 =
143      fo_unif_subst test_equality_only subst context metasenv 
144       (CicSubstitution.lift n arg) t' ugraph
145
146     in
147      subst,metasenv,C.Rel (1 + n),ugraph1
148    with
149       Uncertain _
150     | UnificationFailure _ ->
151        match t' with
152         | C.Rel m  -> subst,metasenv, 
153            (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
154         | C.Var (uri,exp_named_subst) ->
155            let subst,metasenv,exp_named_subst',ugraph1 =
156             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
157            in
158             subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
159         | C.Meta (i,l) ->
160             (* andrea: in general, beta_expand can create badly typed
161              terms. This happens quite seldom in practice, UNLESS we
162              iterate on the local context. For this reason, we renounce
163              to iterate and just lift *)
164             let l = 
165               List.map 
166                 (function
167                      Some t -> Some (CicSubstitution.lift 1 t)
168                    | None -> None) l in
169             subst, metasenv, C.Meta (i,l), ugraph
170         | C.Sort _
171         | C.Implicit _ as t -> subst,metasenv,t,ugraph
172         | C.Cast (te,ty) ->
173             let subst,metasenv,te',ugraph1 = 
174               aux metasenv subst n context te ugraph in
175             let subst,metasenv,ty',ugraph2 = 
176               aux metasenv subst n context ty ugraph1 in 
177             (* TASSI: sure this is in serial? *)
178             subst,metasenv,(C.Cast (te', ty')),ugraph2
179         | C.Prod (nn,s,t) ->
180            let subst,metasenv,s',ugraph1 = 
181              aux metasenv subst n context s ugraph in
182            let subst,metasenv,t',ugraph2 =
183              aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t 
184                ugraph1
185            in
186            (* TASSI: sure this is in serial? *)
187            subst,metasenv,(C.Prod (nn, s', t')),ugraph2
188         | C.Lambda (nn,s,t) ->
189            let subst,metasenv,s',ugraph1 = 
190              aux metasenv subst n context s ugraph in
191            let subst,metasenv,t',ugraph2 =
192             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
193            in
194            (* TASSI: sure this is in serial? *)
195             subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
196         | C.LetIn (nn,s,t) ->
197            let subst,metasenv,s',ugraph1 = 
198              aux metasenv subst n context s ugraph in
199            let subst,metasenv,t',ugraph2 =
200             aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
201               ugraph1
202            in
203            (* TASSI: sure this is in serial? *)
204             subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
205         | C.Appl l ->
206            let subst,metasenv,revl',ugraph1 =
207             List.fold_left
208              (fun (subst,metasenv,appl,ugraph) t ->
209                let subst,metasenv,t',ugraph1 = 
210                  aux metasenv subst n context t ugraph in
211                 subst,metasenv,(t'::appl),ugraph1
212              ) (subst,metasenv,[],ugraph) l
213            in
214             subst,metasenv,(C.Appl (List.rev revl')),ugraph1
215         | C.Const (uri,exp_named_subst) ->
216            let subst,metasenv,exp_named_subst',ugraph1 =
217             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
218            in
219             subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
220         | C.MutInd (uri,i,exp_named_subst) ->
221            let subst,metasenv,exp_named_subst',ugraph1 =
222             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
223            in
224             subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
225         | C.MutConstruct (uri,i,j,exp_named_subst) ->
226            let subst,metasenv,exp_named_subst',ugraph1 =
227             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
228            in
229             subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
230         | C.MutCase (sp,i,outt,t,pl) ->
231            let subst,metasenv,outt',ugraph1 = 
232              aux metasenv subst n context outt ugraph in
233            let subst,metasenv,t',ugraph2 = 
234              aux metasenv subst n context t ugraph1 in
235            let subst,metasenv,revpl',ugraph3 =
236             List.fold_left
237              (fun (subst,metasenv,pl,ugraph) t ->
238                let subst,metasenv,t',ugraph1 = 
239                  aux metasenv subst n context t ugraph in
240                subst,metasenv,(t'::pl),ugraph1
241              ) (subst,metasenv,[],ugraph2) pl
242            in
243            subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
244            (* TASSI: not sure this is serial *)
245         | C.Fix (i,fl) ->
246 (*CSC: not implemented
247            let tylen = List.length fl in
248             let substitutedfl =
249              List.map
250               (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
251                fl
252             in
253              C.Fix (i, substitutedfl)
254 *)
255             subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
256         | C.CoFix (i,fl) ->
257 (*CSC: not implemented
258            let tylen = List.length fl in
259             let substitutedfl =
260              List.map
261               (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
262                fl
263             in
264              C.CoFix (i, substitutedfl)
265
266 *) 
267             subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
268
269   and aux_exp_named_subst metasenv subst n context ens ugraph =
270    List.fold_right
271     (fun (uri,t) (subst,metasenv,l,ugraph) ->
272       let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
273        subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
274   in
275   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
276   let fresh_name =
277    FreshNamesGenerator.mk_fresh_name ~subst
278     metasenv context (Cic.Name "Hbeta") ~typ:argty
279   in
280    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
281    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
282    subst, metasenv, t'', ugraph2
283 in profiler_beta_expand.HExtlib.profile foo ()
284
285
286 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
287   let subst,metasenv,hd,ugraph =
288     List.fold_right
289       (fun arg (subst,metasenv,t,ugraph) ->
290          let subst,metasenv,t,ugraph1 =
291            beta_expand test_equality_only 
292              metasenv subst context t arg ugraph 
293          in
294            subst,metasenv,t,ugraph1 
295       ) args (subst,metasenv,t,ugraph) 
296   in
297     subst,metasenv,hd,ugraph
298
299
300 (* NUOVA UNIFICAZIONE *)
301 (* A substitution is a (int * Cic.term) list that associates a
302    metavariable i with its body.
303    A metaenv is a (int * Cic.term) list that associate a metavariable
304    i with is type. 
305    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
306    a new substitution which is _NOT_ unwinded. It must be unwinded before
307    applying it. *)
308
309 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =  
310  let module C = Cic in
311  let module R = CicReduction in
312  let module S = CicSubstitution in
313  let t1 = deref subst t1 in
314  let t2 = deref subst t2 in
315  let b,ugraph  = 
316 let foo () =
317    R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
318 in profiler_are_convertible.HExtlib.profile foo ()
319  in
320    if b then
321      subst, metasenv, ugraph 
322    else
323    match (t1, t2) with
324      | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
325          let _,subst,metasenv,ugraph1 =
326            (try
327               List.fold_left2
328                 (fun (j,subst,metasenv,ugraph) t1 t2 ->
329                    match t1,t2 with
330                        None,_
331                      | _,None -> j+1,subst,metasenv,ugraph
332                      | Some t1', Some t2' ->
333                          (* First possibility:  restriction    *)
334                          (* Second possibility: unification    *)
335                          (* Third possibility:  convertibility *)
336                          let b, ugraph1 = 
337                          R.are_convertible 
338                            ~subst ~metasenv context t1' t2' ugraph
339                          in
340                          if b then
341                            j+1,subst,metasenv, ugraph1 
342                          else
343                            (try
344                               let subst,metasenv,ugraph2 =
345                                 fo_unif_subst 
346                                   test_equality_only 
347                                   subst context metasenv t1' t2' ugraph
348                               in
349                                 j+1,subst,metasenv,ugraph2
350                             with
351                                 Uncertain _
352                               | UnificationFailure _ ->
353 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); 
354                                   let metasenv, subst = 
355                                     CicMetaSubst.restrict 
356                                       subst [(n,j)] metasenv in
357                                     j+1,subst,metasenv,ugraph1)
358                 ) (1,subst,metasenv,ugraph) ln lm
359             with
360                 Exit ->
361                   raise 
362                     (UnificationFailure (lazy "1"))
363                     (*
364                     (sprintf
365                       "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."
366                       (CicMetaSubst.ppterm subst t1) 
367                       (CicMetaSubst.ppterm subst t2))) *)
368               | Invalid_argument _ ->
369                   raise 
370                     (UnificationFailure (lazy "2")))
371                     (*
372                     (sprintf
373                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match." 
374                       (CicMetaSubst.ppterm subst t1) 
375                       (CicMetaSubst.ppterm subst t2)))) *)
376          in subst,metasenv,ugraph1
377      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
378          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
379      | (C.Meta (n,l), t)   
380      | (t, C.Meta (n,l)) ->
381          let swap =
382            match t1,t2 with
383                C.Meta (n,_), C.Meta (m,_) when n < m -> false
384              | _, C.Meta _ -> false
385              | _,_ -> true
386          in
387          let lower = fun x y -> if swap then y else x in
388          let upper = fun x y -> if swap then x else y in
389          let fo_unif_subst_ordered 
390              test_equality_only subst context metasenv m1 m2 ugraph =
391            fo_unif_subst test_equality_only subst context metasenv 
392              (lower m1 m2) (upper m1 m2) ugraph
393          in
394          begin
395          let subst,metasenv,ugraph1 = 
396            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
397            (try
398               let tyt,ugraph1 = 
399                 type_of_aux' metasenv subst context t ugraph 
400               in
401                 fo_unif_subst 
402                   test_equality_only 
403                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
404             with 
405                 UnificationFailure _ as e -> raise e
406               | Uncertain msg -> raise (UnificationFailure msg)
407               | AssertFailure _ ->
408                   debug_print (lazy "siamo allo huge hack");
409                   (* TODO huge hack!!!!
410                    * we keep on unifying/refining in the hope that 
411                    * the problem will be eventually solved. 
412                    * In the meantime we're breaking a big invariant:
413                    * the terms that we are unifying are no longer well 
414                    * typed in the current context (in the worst case 
415                    * we could even diverge) *)
416                   (subst, metasenv,ugraph)) in
417          let t',metasenv,subst =
418            try 
419              CicMetaSubst.delift n subst context metasenv l t
420            with
421                (CicMetaSubst.MetaSubstFailure msg)-> 
422                  raise (UnificationFailure msg)
423              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
424          in
425          let t'',ugraph2 =
426            match t' with
427                C.Sort (C.Type u) when not test_equality_only ->
428                  let u' = CicUniv.fresh () in
429                  let s = C.Sort (C.Type u') in
430                  let ugraph2 =   
431                    CicUniv.add_ge (upper u u') (lower u u') ugraph1
432                  in
433                    s,ugraph2
434              | _ -> t',ugraph1
435          in
436          (* Unifying the types may have already instantiated n. Let's check *)
437          try
438            let (_, oldt,_) = CicUtil.lookup_subst n subst in
439            let lifted_oldt = S.subst_meta l oldt in
440              fo_unif_subst_ordered 
441                test_equality_only subst context metasenv t lifted_oldt ugraph2
442          with
443              CicUtil.Subst_not_found _ -> 
444                let (_, context, ty) = CicUtil.lookup_meta n metasenv in
445                let subst = (n, (context, t'',ty)) :: subst in
446                let metasenv =
447                  List.filter (fun (m,_,_) -> not (n = m)) metasenv in
448                subst, metasenv, ugraph2
449          end
450    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
451    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
452       if UriManager.eq uri1 uri2 then
453        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
454         exp_named_subst1 exp_named_subst2 ugraph
455       else
456        raise (UnificationFailure (lazy 
457           (sprintf
458             "Can't unify %s with %s due to different constants"
459             (CicMetaSubst.ppterm subst t1) 
460             (CicMetaSubst.ppterm subst t2)))) 
461    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
462        if UriManager.eq uri1 uri2 && i1 = i2 then
463          fo_unif_subst_exp_named_subst 
464            test_equality_only 
465            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
466        else
467          raise (UnificationFailure (lazy "4"))
468            (* (sprintf
469               "Can't unify %s with %s due to different inductive principles"
470               (CicMetaSubst.ppterm subst t1) 
471               (CicMetaSubst.ppterm subst t2))) *)
472    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
473        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
474        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
475          fo_unif_subst_exp_named_subst
476            test_equality_only 
477            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
478        else
479          raise (UnificationFailure (lazy "5"))
480            (* (sprintf
481               "Can't unify %s with %s due to different inductive constructors"
482               (CicMetaSubst.ppterm subst t1) 
483               (CicMetaSubst.ppterm subst t2))) *)
484    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
485    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
486                               subst context metasenv te t2 ugraph
487    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only 
488                               subst context metasenv t1 te ugraph
489    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
490        let subst',metasenv',ugraph1 = 
491          fo_unif_subst true subst context metasenv s1 s2 ugraph 
492        in
493          fo_unif_subst test_equality_only 
494            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
495    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 
496        let subst',metasenv',ugraph1 = 
497          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph 
498        in
499          fo_unif_subst test_equality_only 
500            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
501    | (C.LetIn (_,s1,t1), t2)  
502    | (t2, C.LetIn (_,s1,t1)) -> 
503        fo_unif_subst 
504         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
505    | (C.Appl l1, C.Appl l2) -> 
506        (* andrea: this case should be probably rewritten in the 
507           spirit of deref *)
508        (match l1,l2 with
509           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
510               (try 
511                  List.fold_left2 
512                    (fun (subst,metasenv,ugraph) t1 t2 ->
513                       fo_unif_subst 
514                         test_equality_only subst context metasenv t1 t2 ugraph)
515                    (subst,metasenv,ugraph) l1 l2 
516                with (Invalid_argument msg) -> 
517                  raise (UnificationFailure (lazy msg)))
518           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
519               (* we verify that none of the args is a Meta, 
520                 since beta expanding with respoect to a metavariable 
521                 makes no sense  *)
522  (*
523               (try 
524                  let (_,t,_) = CicUtil.lookup_subst i subst in
525                  let lifted = S.subst_meta l t in
526                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
527                    fo_unif_subst 
528                     test_equality_only 
529                      subst context metasenv reduced t2 ugraph
530                with CicUtil.Subst_not_found _ -> *)
531               let subst,metasenv,beta_expanded,ugraph1 =
532                 beta_expand_many 
533                   test_equality_only metasenv subst context t2 args ugraph 
534               in
535                 fo_unif_subst test_equality_only subst context metasenv 
536                   (C.Meta (i,l)) beta_expanded ugraph1
537           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
538               (* (try 
539                  let (_,t,_) = CicUtil.lookup_subst i subst in
540                  let lifted = S.subst_meta l t in
541                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
542                    fo_unif_subst 
543                      test_equality_only 
544                      subst context metasenv t1 reduced ugraph
545                with CicUtil.Subst_not_found _ -> *)
546                  let subst,metasenv,beta_expanded,ugraph1 =
547                    beta_expand_many 
548                      test_equality_only 
549                      metasenv subst context t1 args ugraph 
550                  in
551                    fo_unif_subst test_equality_only subst context metasenv 
552                      (C.Meta (i,l)) beta_expanded ugraph1
553           | _,_ ->
554               let lr1 = List.rev l1 in
555               let lr2 = List.rev l2 in
556               let rec 
557                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
558                 match (l1,l2) with
559                     [],_
560                   | _,[] -> assert false
561                   | ([h1],[h2]) ->
562                       fo_unif_subst 
563                         test_equality_only subst context metasenv h1 h2 ugraph
564                   | ([h],l) 
565                   | (l,[h]) ->
566                       fo_unif_subst test_equality_only subst context metasenv
567                         h (C.Appl (List.rev l)) ugraph
568                   | ((h1::l1),(h2::l2)) -> 
569                       let subst', metasenv',ugraph1 = 
570                         fo_unif_subst 
571                           test_equality_only 
572                           subst context metasenv h1 h2 ugraph
573                       in 
574                         fo_unif_l 
575                           test_equality_only subst' metasenv' (l1,l2) ugraph1
576               in
577               (try 
578                 fo_unif_l 
579                   test_equality_only subst metasenv (lr1, lr2)  ugraph
580               with 
581               | UnificationFailure _
582               | Uncertain _ as exn -> 
583                   (match l1, l2 with
584                   | (((Cic.Const (uri1, ens1)) as c1) :: tl1), 
585                      (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
586                     CoercGraph.is_a_coercion c1 && 
587                     CoercGraph.is_a_coercion c2 ->
588                       let body1, attrs1, ugraph = 
589                         match CicEnvironment.get_obj ugraph uri1 with
590                         | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
591                         | _ -> assert false
592                       in
593                       let body2, attrs2, ugraph = 
594                         match CicEnvironment.get_obj ugraph uri2 with
595                         | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
596                         | _ -> assert false
597                       in
598                       let is_composite1 = 
599                         List.exists ((=) (`Class `Coercion)) attrs1 in
600                       let is_composite2 = 
601                         List.exists ((=) (`Class `Coercion)) attrs2 in
602                       (match is_composite1, is_composite2 with
603                       | false, false -> raise exn
604                       | true, false ->
605                           let body1 = CicSubstitution.subst_vars ens1 body1 in
606                           let appl = Cic.Appl (body1::tl1) in
607                           let redappl = CicReduction.head_beta_reduce appl in
608                           fo_unif_subst 
609                             test_equality_only subst context metasenv 
610                               redappl t2 ugraph
611                       | false, true -> 
612                           let body2 = CicSubstitution.subst_vars ens2 body2 in
613                           let appl = Cic.Appl (body2::tl2) in
614                           let redappl = CicReduction.head_beta_reduce appl in
615                           fo_unif_subst 
616                             test_equality_only subst context metasenv 
617                              t1 redappl ugraph
618                       | true, true ->
619                           let body1 = CicSubstitution.subst_vars ens1 body1 in
620                           let appl1 = Cic.Appl (body1::tl1) in
621                           let redappl1 = CicReduction.head_beta_reduce appl1 in
622                           let body2 = CicSubstitution.subst_vars ens2 body2 in
623                           let appl2 = Cic.Appl (body2::tl2) in
624                           let redappl2 = CicReduction.head_beta_reduce appl2 in
625                           fo_unif_subst 
626                             test_equality_only subst context metasenv 
627                              redappl1 redappl2 ugraph)
628                   (*CSC: This is necessary because of the "elim H" tactic
629                          where the type of H is only reducible to an
630                          inductive type. This could be extended from inductive
631                          types to any rigid term. However, the code is
632                          duplicated in two places: inside applications and
633                          outside them. Probably it would be better to
634                          work with lambda-bar terms instead. *)
635                   | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
636                   | (_, Cic.MutInd _::_) ->
637                      let t1' = R.whd ~subst context t1 in
638                      (match t1' with
639                           C.Appl (C.MutInd _::_) -> 
640                             fo_unif_subst test_equality_only 
641                               subst context metasenv t1' t2 ugraph         
642                         | _ -> raise (UnificationFailure (lazy "88")))
643                   | (Cic.MutInd _::_,_) ->
644                      let t2' = R.whd ~subst context t2 in
645                      (match t2' with
646                           C.Appl (C.MutInd _::_) -> 
647                             fo_unif_subst test_equality_only 
648                               subst context metasenv t1 t2' ugraph         
649                         | _ -> raise (UnificationFailure (lazy "99")))
650                   | _ -> raise exn)))
651    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
652        let subst', metasenv',ugraph1 = 
653         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
654           ugraph in
655        let subst'',metasenv'',ugraph2 = 
656         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
657           ugraph1 in
658        (try
659          List.fold_left2 
660           (fun (subst,metasenv,ugraph) t1 t2 ->
661             fo_unif_subst 
662              test_equality_only subst context metasenv t1 t2 ugraph
663           ) (subst'',metasenv'',ugraph2) pl1 pl2 
664         with
665          Invalid_argument _ ->
666           raise (UnificationFailure (lazy "6.1")))
667            (* (sprintf
668               "Error trying to unify %s with %s: the number of branches is not the same." 
669               (CicMetaSubst.ppterm subst t1) 
670               (CicMetaSubst.ppterm subst t2)))) *)
671    | (C.Rel _, _) | (_,  C.Rel _) ->
672        if t1 = t2 then
673          subst, metasenv,ugraph
674        else
675         raise (UnificationFailure (lazy 
676            (sprintf
677              "Can't unify %s with %s because they are not convertible"
678              (CicMetaSubst.ppterm subst t1) 
679              (CicMetaSubst.ppterm subst t2))))
680    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
681        let subst,metasenv,beta_expanded,ugraph1 =
682          beta_expand_many 
683            test_equality_only metasenv subst context t2 args ugraph 
684        in
685          fo_unif_subst test_equality_only subst context metasenv 
686            (C.Meta (i,l)) beta_expanded ugraph1
687    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
688        let subst,metasenv,beta_expanded,ugraph1 =
689          beta_expand_many 
690            test_equality_only metasenv subst context t1 args ugraph 
691        in
692          fo_unif_subst test_equality_only subst context metasenv 
693            beta_expanded (C.Meta (i,l)) ugraph1
694 (* Works iff there are no arguments applied to it; similar to the
695    case below
696    | (_, C.MutInd _) ->
697        let t1' = R.whd ~subst context t1 in
698        (match t1' with
699             C.MutInd _ -> 
700               fo_unif_subst test_equality_only 
701                 subst context metasenv t1' t2 ugraph         
702           | _ -> raise (UnificationFailure (lazy "8")))
703 *)
704 (* The following idea could be exploited again; right now we have no
705    longer any example requiring it
706    | (C.Prod _, t2) ->
707        let t2' = R.whd ~subst context t2 in
708        (match t2' with
709             C.Prod _ -> 
710               fo_unif_subst test_equality_only 
711                 subst context metasenv t1 t2' ugraph         
712           | _ -> raise (UnificationFailure (lazy "8")))
713    | (t1, C.Prod _) ->
714        let t1' = R.whd ~subst context t1 in
715        (match t1' with
716             C.Prod _ -> 
717               fo_unif_subst test_equality_only 
718                 subst context metasenv t1' t2 ugraph         
719           | _ -> (* raise (UnificationFailure "9")) *)
720              raise 
721                 (UnificationFailure (lazy (sprintf
722                    "Can't unify %s with %s because they are not convertible"
723                    (CicMetaSubst.ppterm subst t1) 
724                    (CicMetaSubst.ppterm subst t2)))))
725 *)
726    | (_,_) ->
727      (* delta-beta reduction should almost never be a problem for
728         unification since:
729          1. long computations require iota reduction
730          2. it is extremely rare that a close term t1 (that could be unified
731             to t2) beta-delta reduces to t1' while t2 does not beta-delta
732             reduces in the same way. This happens only if one meta of t2
733             occurs in head position during beta reduction. In this unluky
734             case too much reduction will be performed on t1 and unification
735             will surely fail. *)
736      let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
737      let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
738       if t1 = t1' && t2 = t2' then
739        raise (UnificationFailure
740         (lazy 
741           (sprintf
742             "Can't unify %s with %s because they are not convertible"
743             (CicMetaSubst.ppterm subst t1) 
744             (CicMetaSubst.ppterm subst t2))))
745       else
746        try
747         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
748        with
749           UnificationFailure _
750         | Uncertain _ ->
751            raise (UnificationFailure
752             (lazy 
753               (sprintf
754                 "Can't unify %s with %s because they are not convertible"
755                 (CicMetaSubst.ppterm subst t1) 
756                 (CicMetaSubst.ppterm subst t2))))
757
758 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
759  exp_named_subst1 exp_named_subst2 ugraph
760 =
761  try
762   List.fold_left2
763    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
764      assert (uri1=uri2) ;
765      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
766    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
767  with
768   Invalid_argument _ ->
769    let print_ens ens =
770     String.concat " ; "
771      (List.map
772        (fun (uri,t) ->
773          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
774        ) ens) 
775    in
776     raise (UnificationFailure (lazy (sprintf
777      "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))))
778
779 (* A substitution is a (int * Cic.term) list that associates a               *)
780 (* metavariable i with its body.                                             *)
781 (* metasenv is of type Cic.metasenv                                          *)
782 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
783 (* a new substitution which is already unwinded and ready to be applied and  *)
784 (* a new metasenv in which some hypothesis in the contexts of the            *)
785 (* metavariables may have been restricted.                                   *)
786 let fo_unif metasenv context t1 t2 ugraph = 
787  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
788
789 let enrich_msg msg subst context metasenv t1 t2 ugraph =
790  lazy (
791   if verbose then
792    sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
793     (CicMetaSubst.ppterm subst t1)
794     (try
795       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
796       CicPp.ppterm ty_t1
797     with 
798     | UnificationFailure s
799     | Uncertain s
800     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
801     (CicMetaSubst.ppterm subst t2)
802     (try
803       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
804       CicPp.ppterm ty_t2
805     with
806     | UnificationFailure s
807     | Uncertain s
808     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
809     (CicMetaSubst.ppcontext subst context)
810     (CicMetaSubst.ppmetasenv subst metasenv)
811     (CicMetaSubst.ppsubst subst) (Lazy.force msg)
812  else
813    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
814     (CicMetaSubst.ppterm_in_context subst t1 context)
815     (try
816       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
817       CicMetaSubst.ppterm_in_context subst ty_t1 context
818     with 
819     | UnificationFailure s
820     | Uncertain s
821     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
822     (CicMetaSubst.ppterm_in_context subst t2 context)
823     (try
824       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
825       CicMetaSubst.ppterm_in_context subst ty_t2 context
826     with
827     | UnificationFailure s
828     | Uncertain s
829     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
830     (CicMetaSubst.ppcontext subst context)
831     (CicMetaSubst.ppmetasenv subst metasenv)
832     (Lazy.force msg)
833  )
834
835 let fo_unif_subst subst context metasenv t1 t2 ugraph =
836   try
837     fo_unif_subst false subst context metasenv t1 t2 ugraph
838   with
839   | AssertFailure msg ->
840      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
841   | UnificationFailure msg ->
842      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
843 ;;