]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_unification/cicUnification.ml
added margin option to the pp
[helm.git] / helm / software / 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 ~metasenv subst term)
57              (CicMetaSubst.ppterm ~metasenv [] term)
58              (CicMetaSubst.ppcontext ~metasenv subst context)
59              (CicMetaSubst.ppmetasenv subst metasenv) 
60              (CicMetaSubst.ppsubst ~metasenv 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 ~metasenv subst term)
68              (CicMetaSubst.ppterm ~metasenv [] term)
69              (CicMetaSubst.ppcontext ~metasenv subst context)
70              (CicMetaSubst.ppmetasenv subst metasenv) 
71              (CicMetaSubst.ppsubst ~metasenv 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 
78     (function 
79        | Cic.Meta _  
80        | Cic.Appl (Cic.Meta _::_) -> true
81        | _ -> false) l
82
83 let rec deref subst t =
84   let snd (_,a,_) = a in
85   match t with
86       Cic.Meta(n,l) -> 
87         (try 
88            deref subst
89              (CicSubstitution.subst_meta 
90                 l (snd (CicUtil.lookup_subst n subst))) 
91          with 
92              CicUtil.Subst_not_found _ -> t)
93     | Cic.Appl(Cic.Meta(n,l)::args) ->
94         (match deref subst (Cic.Meta(n,l)) with
95            | Cic.Lambda _ as t -> 
96                deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
97            | r -> Cic.Appl(r::args))
98     | Cic.Appl(((Cic.Lambda _) as t)::args) ->
99            deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
100     | t -> t
101 ;; 
102
103 let deref subst t =
104  let foo () = deref subst t
105  in profiler_deref.HExtlib.profile foo ()
106
107 exception WrongShape;;
108 let eta_reduce after_beta_expansion after_beta_expansion_body
109      before_beta_expansion
110  =
111  try
112   match before_beta_expansion,after_beta_expansion_body with
113      Cic.Appl l, Cic.Appl l' ->
114       let rec all_but_last check_last =
115        function
116           [] -> assert false
117         | [Cic.Rel 1] -> []
118         | [_] -> if check_last then raise WrongShape else []
119         | he::tl -> he::(all_but_last check_last tl)
120       in
121        let all_but_last check_last l =
122         match all_but_last check_last l with
123            [] -> assert false
124          | [he] -> he
125          | l -> Cic.Appl l
126        in
127        let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
128        let all_but_last = all_but_last false l in
129         (* here we should test alpha-equivalence; however we know by
130            construction that here alpha_equivalence is equivalent to = *)
131         if t = all_but_last then
132          all_but_last
133         else
134          after_beta_expansion
135    | _,_ -> after_beta_expansion
136  with
137   WrongShape -> after_beta_expansion
138
139 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
140  let module S = CicSubstitution in
141  let module C = Cic in
142 let foo () =
143   let rec aux metasenv subst n context t' ugraph =
144    try
145
146     let subst,metasenv,ugraph1 =
147      fo_unif_subst test_equality_only subst context metasenv 
148       (CicSubstitution.lift n arg) t' ugraph
149
150     in
151      subst,metasenv,C.Rel (1 + n),ugraph1
152    with
153       Uncertain _
154     | UnificationFailure _ ->
155        match t' with
156         | C.Rel m  -> subst,metasenv, 
157            (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
158         | C.Var (uri,exp_named_subst) ->
159            let subst,metasenv,exp_named_subst',ugraph1 =
160             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
161            in
162             subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
163         | C.Meta (i,l) ->
164             (* andrea: in general, beta_expand can create badly typed
165              terms. This happens quite seldom in practice, UNLESS we
166              iterate on the local context. For this reason, we renounce
167              to iterate and just lift *)
168             let l = 
169               List.map 
170                 (function
171                      Some t -> Some (CicSubstitution.lift 1 t)
172                    | None -> None) l in
173             subst, metasenv, C.Meta (i,l), ugraph
174         | C.Sort _
175         | C.Implicit _ as t -> subst,metasenv,t,ugraph
176         | C.Cast (te,ty) ->
177             let subst,metasenv,te',ugraph1 = 
178               aux metasenv subst n context te ugraph in
179             let subst,metasenv,ty',ugraph2 = 
180               aux metasenv subst n context ty ugraph1 in 
181             (* TASSI: sure this is in serial? *)
182             subst,metasenv,(C.Cast (te', ty')),ugraph2
183         | C.Prod (nn,s,t) ->
184            let subst,metasenv,s',ugraph1 = 
185              aux metasenv subst n context s ugraph in
186            let subst,metasenv,t',ugraph2 =
187              aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t 
188                ugraph1
189            in
190            (* TASSI: sure this is in serial? *)
191            subst,metasenv,(C.Prod (nn, s', t')),ugraph2
192         | C.Lambda (nn,s,t) ->
193            let subst,metasenv,s',ugraph1 = 
194              aux metasenv subst n context s ugraph in
195            let subst,metasenv,t',ugraph2 =
196             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
197            in
198            (* TASSI: sure this is in serial? *)
199             subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
200         | C.LetIn (nn,s,ty,t) ->
201            let subst,metasenv,s',ugraph1 = 
202              aux metasenv subst n context s ugraph in
203            let subst,metasenv,ty',ugraph1 = 
204              aux metasenv subst n context ty ugraph in
205            let subst,metasenv,t',ugraph2 =
206             aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
207               ugraph1
208            in
209            (* TASSI: sure this is in serial? *)
210             subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
211         | C.Appl l ->
212            let subst,metasenv,revl',ugraph1 =
213             List.fold_left
214              (fun (subst,metasenv,appl,ugraph) t ->
215                let subst,metasenv,t',ugraph1 = 
216                  aux metasenv subst n context t ugraph in
217                 subst,metasenv,(t'::appl),ugraph1
218              ) (subst,metasenv,[],ugraph) l
219            in
220             subst,metasenv,(C.Appl (List.rev revl')),ugraph1
221         | C.Const (uri,exp_named_subst) ->
222            let subst,metasenv,exp_named_subst',ugraph1 =
223             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
224            in
225             subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
226         | C.MutInd (uri,i,exp_named_subst) ->
227            let subst,metasenv,exp_named_subst',ugraph1 =
228             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
229            in
230             subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
231         | C.MutConstruct (uri,i,j,exp_named_subst) ->
232            let subst,metasenv,exp_named_subst',ugraph1 =
233             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
234            in
235             subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
236         | C.MutCase (sp,i,outt,t,pl) ->
237            let subst,metasenv,outt',ugraph1 = 
238              aux metasenv subst n context outt ugraph in
239            let subst,metasenv,t',ugraph2 = 
240              aux metasenv subst n context t ugraph1 in
241            let subst,metasenv,revpl',ugraph3 =
242             List.fold_left
243              (fun (subst,metasenv,pl,ugraph) t ->
244                let subst,metasenv,t',ugraph1 = 
245                  aux metasenv subst n context t ugraph in
246                subst,metasenv,(t'::pl),ugraph1
247              ) (subst,metasenv,[],ugraph2) pl
248            in
249            subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
250            (* TASSI: not sure this is serial *)
251         | C.Fix (i,fl) ->
252 (*CSC: not implemented
253            let tylen = List.length fl in
254             let substitutedfl =
255              List.map
256               (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
257                fl
258             in
259              C.Fix (i, substitutedfl)
260 *)
261             subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
262         | C.CoFix (i,fl) ->
263 (*CSC: not implemented
264            let tylen = List.length fl in
265             let substitutedfl =
266              List.map
267               (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
268                fl
269             in
270              C.CoFix (i, substitutedfl)
271
272 *) 
273             subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
274
275   and aux_exp_named_subst metasenv subst n context ens ugraph =
276    List.fold_right
277     (fun (uri,t) (subst,metasenv,l,ugraph) ->
278       let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
279        subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
280   in
281   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
282   let fresh_name =
283    FreshNamesGenerator.mk_fresh_name ~subst
284     metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
285   in
286    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
287    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
288    subst, metasenv, t'', ugraph2
289 in profiler_beta_expand.HExtlib.profile foo ()
290
291
292 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
293   let _,subst,metasenv,hd,ugraph =
294     List.fold_right
295       (fun arg (num,subst,metasenv,t,ugraph) ->
296          let subst,metasenv,t,ugraph1 =
297            beta_expand num test_equality_only 
298              metasenv subst context t arg ugraph 
299          in
300            num+1,subst,metasenv,t,ugraph1 
301       ) args (1,subst,metasenv,t,ugraph) 
302   in
303     subst,metasenv,hd,ugraph
304
305 and warn_if_not_unique xxx car1 car2 =
306   let unopt = 
307     function 
308     | Some (_,Cic.Appl(Cic.Const(u,_)::_)) -> UriManager.string_of_uri u 
309     | Some (_,t) -> CicPp.ppterm t 
310     | None -> "id"
311   in
312   match xxx with
313   | [] -> ()
314   | _ -> 
315      HLog.warn 
316        ("There are "^string_of_int (List.length xxx + 1)^
317         " minimal joins of "^ CoercDb.string_of_carr car1^" and "^
318        CoercDb.string_of_carr car2^": " ^
319      String.concat " and "
320        (List.map 
321           (fun (m2,_,c2,c2') ->
322           " via "^CoercDb.string_of_carr m2^" via "^unopt c2^" + "^unopt c2')
323           xxx))
324
325 (* NUOVA UNIFICAZIONE *)
326 (* A substitution is a (int * Cic.term) list that associates a
327    metavariable i with its body.
328    A metaenv is a (int * Cic.term) list that associate a metavariable
329    i with is type. 
330    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
331    a new substitution which is _NOT_ unwinded. It must be unwinded before
332    applying it. *)
333
334 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =  
335  let module C = Cic in
336  let module R = CicReduction in
337  let module S = CicSubstitution in
338  let t1 = deref subst t1 in
339  let t2 = deref subst t2 in
340  let (&&&) a b = (a && b) || ((not a) && (not b)) in
341 (* let bef = Sys.time () in *)
342  let b,ugraph =
343   if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
344    false,ugraph
345   else
346 let foo () =
347    R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
348 in profiler_are_convertible.HExtlib.profile foo ()
349  in
350 (* let aft = Sys.time () in
351 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
352 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
353 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
354    if b then
355      subst, metasenv, ugraph 
356    else
357    match (t1, t2) with
358      | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
359          let _,subst,metasenv,ugraph1 =
360            (try
361               List.fold_left2
362                 (fun (j,subst,metasenv,ugraph) t1 t2 ->
363                    match t1,t2 with
364                        None,_
365                      | _,None -> j+1,subst,metasenv,ugraph
366                      | Some t1', Some t2' ->
367                          (* First possibility:  restriction    *)
368                          (* Second possibility: unification    *)
369                          (* Third possibility:  convertibility *)
370                          let b, ugraph1 = 
371                          R.are_convertible 
372                            ~subst ~metasenv context t1' t2' ugraph
373                          in
374                          if b then
375                            j+1,subst,metasenv, ugraph1 
376                          else
377                            (try
378                               let subst,metasenv,ugraph2 =
379                                 fo_unif_subst 
380                                   test_equality_only 
381                                   subst context metasenv t1' t2' ugraph
382                               in
383                                 j+1,subst,metasenv,ugraph2
384                             with
385                                 Uncertain _
386                               | UnificationFailure _ ->
387 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); 
388                                   let metasenv, subst = 
389                                     CicMetaSubst.restrict 
390                                       subst [(n,j)] metasenv in
391                                     j+1,subst,metasenv,ugraph1)
392                 ) (1,subst,metasenv,ugraph) ln lm
393             with
394                 Exit ->
395                   raise 
396                     (UnificationFailure (lazy "1"))
397                     (*
398                     (sprintf
399                       "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."
400                       (CicMetaSubst.ppterm ~metasenv subst t1) 
401                       (CicMetaSubst.ppterm ~metasenv subst t2))) *)
402               | Invalid_argument _ ->
403                   raise 
404                     (UnificationFailure (lazy "2")))
405                     (*
406                     (sprintf
407                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match." 
408                       (CicMetaSubst.ppterm ~metasenv subst t1) 
409                       (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
410          in subst,metasenv,ugraph1
411      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
412          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
413      | (C.Meta (n,l), t)   
414      | (t, C.Meta (n,l)) ->
415          let swap =
416            match t1,t2 with
417                C.Meta (n,_), C.Meta (m,_) when n < m -> false
418              | _, C.Meta _ -> false
419              | _,_ -> true
420          in
421          let lower = fun x y -> if swap then y else x in
422          let upper = fun x y -> if swap then x else y in
423          let fo_unif_subst_ordered 
424              test_equality_only subst context metasenv m1 m2 ugraph =
425            fo_unif_subst test_equality_only subst context metasenv 
426              (lower m1 m2) (upper m1 m2) ugraph
427          in
428          begin
429          let subst,metasenv,ugraph1 = 
430            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
431            (try
432               let tyt,ugraph1 = 
433                 type_of_aux' metasenv subst context t ugraph 
434               in
435                 fo_unif_subst 
436                   test_equality_only 
437                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
438             with 
439                 UnificationFailure _ as e -> raise e
440               | Uncertain msg -> raise (UnificationFailure msg)
441               | AssertFailure _ ->
442                   debug_print (lazy "siamo allo huge hack");
443                   (* TODO huge hack!!!!
444                    * we keep on unifying/refining in the hope that 
445                    * the problem will be eventually solved. 
446                    * In the meantime we're breaking a big invariant:
447                    * the terms that we are unifying are no longer well 
448                    * typed in the current context (in the worst case 
449                    * we could even diverge) *)
450                   (subst, metasenv,ugraph)) in
451          let t',metasenv,subst =
452            try 
453              CicMetaSubst.delift n subst context metasenv l t
454            with
455                (CicMetaSubst.MetaSubstFailure msg)-> 
456                  raise (UnificationFailure msg)
457              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
458          in
459          let t'',ugraph2 =
460            match t' with
461                C.Sort (C.Type u) when not test_equality_only ->
462                  let u' = CicUniv.fresh () in
463                  let s = C.Sort (C.Type u') in
464                   (try
465                     let ugraph2 =   
466                      CicUniv.add_ge (upper u u') (lower u u') ugraph1
467                     in
468                      s,ugraph2
469                    with
470                     CicUniv.UniverseInconsistency msg ->
471                      raise (UnificationFailure msg))
472              | _ -> t',ugraph1
473          in
474          (* Unifying the types may have already instantiated n. Let's check *)
475          try
476            let (_, oldt,_) = CicUtil.lookup_subst n subst in
477            let lifted_oldt = S.subst_meta l oldt in
478              fo_unif_subst_ordered 
479                test_equality_only subst context metasenv t lifted_oldt ugraph2
480          with
481              CicUtil.Subst_not_found _ -> 
482                let (_, context, ty) = CicUtil.lookup_meta n metasenv in
483                let subst = (n, (context, t'',ty)) :: subst in
484                let metasenv =
485                  List.filter (fun (m,_,_) -> not (n = m)) metasenv in
486                subst, metasenv, ugraph2
487          end
488    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
489    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
490       if UriManager.eq uri1 uri2 then
491        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
492         exp_named_subst1 exp_named_subst2 ugraph
493       else
494        raise (UnificationFailure (lazy 
495           (sprintf
496             "Can't unify %s with %s due to different constants"
497             (CicMetaSubst.ppterm ~metasenv subst t1) 
498             (CicMetaSubst.ppterm ~metasenv subst t2))))
499    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
500        if UriManager.eq uri1 uri2 && i1 = i2 then
501          fo_unif_subst_exp_named_subst 
502            test_equality_only 
503            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
504        else
505          raise (UnificationFailure
506            (lazy
507             (sprintf
508              "Can't unify %s with %s due to different inductive principles"
509              (CicMetaSubst.ppterm ~metasenv subst t1) 
510              (CicMetaSubst.ppterm ~metasenv subst t2))))
511    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
512        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
513        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
514          fo_unif_subst_exp_named_subst
515            test_equality_only 
516            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
517        else
518          raise (UnificationFailure
519           (lazy
520             (sprintf
521               "Can't unify %s with %s due to different inductive constructors"
522               (CicMetaSubst.ppterm ~metasenv subst t1) 
523               (CicMetaSubst.ppterm ~metasenv subst t2))))
524    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
525    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
526                               subst context metasenv te t2 ugraph
527    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only 
528                               subst context metasenv t1 te ugraph
529    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 
530        let subst',metasenv',ugraph1 = 
531          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph 
532        in
533          fo_unif_subst test_equality_only 
534            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
535    | (C.LetIn (_,s1,ty1,t1), t2)  
536    | (t2, C.LetIn (_,s1,ty1,t1)) -> 
537        fo_unif_subst 
538         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
539    | (C.Appl l1, C.Appl l2) -> 
540        (* andrea: this case should be probably rewritten in the 
541           spirit of deref *)
542        (match l1,l2 with
543           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
544               (try 
545                  List.fold_left2 
546                    (fun (subst,metasenv,ugraph) t1 t2 ->
547                       fo_unif_subst 
548                         test_equality_only subst context metasenv t1 t2 ugraph)
549                    (subst,metasenv,ugraph) l1 l2 
550                with (Invalid_argument msg) -> 
551                  raise (UnificationFailure (lazy msg)))
552           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
553               (* we verify that none of the args is a Meta, 
554                 since beta expanding with respoect to a metavariable 
555                 makes no sense  *)
556  (*
557               (try 
558                  let (_,t,_) = CicUtil.lookup_subst i subst in
559                  let lifted = S.subst_meta l t in
560                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
561                    fo_unif_subst 
562                     test_equality_only 
563                      subst context metasenv reduced t2 ugraph
564                with CicUtil.Subst_not_found _ -> *)
565               let subst,metasenv,beta_expanded,ugraph1 =
566                 beta_expand_many 
567                   test_equality_only metasenv subst context t2 args ugraph 
568               in
569                 fo_unif_subst test_equality_only subst context metasenv 
570                   (C.Meta (i,l)) beta_expanded ugraph1
571           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
572               (* (try 
573                  let (_,t,_) = CicUtil.lookup_subst i subst in
574                  let lifted = S.subst_meta l t in
575                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
576                    fo_unif_subst 
577                      test_equality_only 
578                      subst context metasenv t1 reduced ugraph
579                with CicUtil.Subst_not_found _ -> *)
580                  let subst,metasenv,beta_expanded,ugraph1 =
581                    beta_expand_many 
582                      test_equality_only 
583                      metasenv subst context t1 args ugraph 
584                  in
585                    fo_unif_subst test_equality_only subst context metasenv 
586                      (C.Meta (i,l)) beta_expanded ugraph1
587           | _,_ ->
588               let lr1 = List.rev l1 in
589               let lr2 = List.rev l2 in
590               let rec 
591                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
592                 match (l1,l2) with
593                     [],_
594                   | _,[] -> assert false
595                   | ([h1],[h2]) ->
596                       fo_unif_subst 
597                         test_equality_only subst context metasenv h1 h2 ugraph
598                   | ([h],l) 
599                   | (l,[h]) ->
600                       fo_unif_subst test_equality_only subst context metasenv
601                         h (C.Appl (List.rev l)) ugraph
602                   | ((h1::l1),(h2::l2)) -> 
603                       let subst', metasenv',ugraph1 = 
604                         fo_unif_subst 
605                           test_equality_only 
606                           subst context metasenv h1 h2 ugraph
607                       in 
608                         fo_unif_l 
609                           test_equality_only subst' metasenv' (l1,l2) ugraph1
610               in
611               (try 
612                 fo_unif_l 
613                   test_equality_only subst metasenv (lr1, lr2)  ugraph
614               with 
615               | UnificationFailure s
616               | Uncertain s as exn -> 
617                   (match l1, l2 with
618                             (* {{{ pullback *)
619                   | (((Cic.Const (uri1, ens1)) as cc1) :: tl1), 
620                      (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
621                     CoercDb.is_a_coercion cc1 <> None && 
622                     CoercDb.is_a_coercion cc2 <> None &&
623                     not (UriManager.eq uri1 uri2) ->
624 (*DEBUGGING ONLY:
625 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
626 *)
627                      let inner_coerced ?(skip_non_c=false) t =
628                       let t = CicMetaSubst.apply_subst subst t in
629                       let rec aux c x t =
630                         match t with
631                         | Cic.Appl l -> 
632                             (match CoercGraph.coerced_arg l with
633                             | None when skip_non_c -> 
634                                 aux c (HExtlib.list_last l)            
635                                  (HExtlib.list_last l)            
636                             | None -> c, x
637                             | Some (t,_) -> aux (List.hd l) t t)
638                         | _ ->  c, x
639                       in
640                       aux (Cic.Implicit None) (Cic.Implicit None) t
641                      in
642                       let c1,last_tl1 = inner_coerced (Cic.Appl l1) in 
643                       let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
644                       let car1, car2 =
645                         match 
646                           CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
647                         with
648                         | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
649                         | _ -> assert false
650                       in
651                       let head1_c, head2_c =
652                         match 
653                           CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
654                         with
655                         | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
656                         | _ -> assert false
657                       in
658                       let unfold uri ens args =
659                         let o, _ = 
660                           CicEnvironment.get_obj CicUniv.oblivion_ugraph uri 
661                         in
662                         assert (ens = []);
663                         match o with
664                         | Cic.Constant (_,Some bo,_,_,_) -> 
665                             CicReduction.head_beta_reduce ~delta:false
666                               (Cic.Appl (bo::args))
667                         | _ -> assert false
668                       in
669                       let conclude subst metasenv ugraph last_tl1' last_tl2' =
670                        let subst',metasenv,ugraph =
671 (*DEBUGGING ONLY:
672 prerr_endline 
673   ("conclude: " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ 
674    " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
675 *)
676                         fo_unif_subst test_equality_only subst context
677                          metasenv last_tl1' last_tl2' ugraph
678                        in
679                        if subst = subst' then raise exn 
680                        else
681 (*DEBUGGING ONLY: 
682 let subst,metasenv,ugrph as res = 
683 *)
684                         fo_unif_subst test_equality_only subst' context
685                          metasenv (C.Appl l1) (C.Appl l2) ugraph
686 (*DEBUGGING ONLY: 
687 in
688 (prerr_endline 
689   ("OK: "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
690    " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
691 res)
692 *)
693                       in
694 (*DEBUGGING ONLY: 
695 prerr_endline (Printf.sprintf 
696 "Pullback problem\nterm1: %s\nterm2: %s\ncar1: %s\ncar2: %s\nlast_tl1: %s
697 last_tl2: %s\nhead1_c: %s\nhead2_c: %s\n"
698 (CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context)
699 (CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context)
700 (CoercDb.string_of_carr car1)
701 (CoercDb.string_of_carr car2)
702 (CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1 context)
703 (CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2 context)
704 (CoercDb.string_of_carr head1_c)
705 (CoercDb.string_of_carr head2_c)
706 );
707 *)
708                       if CoercDb.eq_carr car1 car2 then
709                          match last_tl1,last_tl2 with
710                          | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
711                          | _, C.Meta _
712                          | C.Meta _, _ ->
713                            let subst,metasenv,ugraph =
714                             fo_unif_subst test_equality_only subst context
715                              metasenv last_tl1 last_tl2 ugraph
716                            in
717                             fo_unif_subst test_equality_only subst context
718                              metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
719                          | _ when CoercDb.eq_carr head1_c head2_c ->
720                              (* composite VS composition + metas avoiding
721                               * coercions not only in coerced position    *)
722                              if c1 <> cc1 && c2 <> cc2 then
723                                conclude subst metasenv ugraph
724                                 last_tl1 last_tl2
725                              else
726                               let l1, l2 = 
727                                if c1 = cc1 then 
728                                  unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
729                                else
730                                  Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
731                               in
732                                fo_unif_subst test_equality_only subst context
733                                 metasenv l1 l2 ugraph
734                          | _ -> raise exn
735                       else
736                       let grow1 =
737                         match last_tl1 with Cic.Meta _ -> true | _ -> false in
738                       let grow2 =
739                         match last_tl2 with Cic.Meta _ -> true | _ -> false in
740                       if not (grow1 || grow2) then
741                         let _,last_tl1 = 
742                           inner_coerced ~skip_non_c:true (Cic.Appl l1) in 
743                         let _,last_tl2 = 
744                           inner_coerced ~skip_non_c:true  (Cic.Appl l2) in
745                         conclude subst metasenv ugraph last_tl1 last_tl2
746                       else
747                         let meets = 
748                            CoercGraph.meets 
749                             metasenv subst context (grow1,car1) (grow2,car2)
750                         in
751                         (match
752                         HExtlib.list_findopt
753                           (fun (carr,metasenv,to1,to2) meet_no ->
754                              try
755                            let last_tl1',(subst,metasenv,ugraph) =
756                             match grow1,to1 with
757                              | true,Some (last,coerced) -> 
758                                  last,
759                                   fo_unif_subst test_equality_only subst context
760                                   metasenv coerced last_tl1 ugraph
761                              | _ -> last_tl1,(subst,metasenv,ugraph)
762                            in
763                            let last_tl2',(subst,metasenv,ugraph) =
764                             match grow2,to2 with
765                              | true,Some (last,coerced) -> 
766                                  last,
767                                   fo_unif_subst test_equality_only subst context
768                                   metasenv coerced last_tl2 ugraph
769                              | _ -> last_tl2,(subst,metasenv,ugraph)
770                            in
771                            if meet_no > 0 then
772                              HLog.warn ("Using pullback number " ^ string_of_int
773                                meet_no);
774                            Some 
775                             (conclude subst metasenv ugraph last_tl1' last_tl2')
776                              with
777                              | UnificationFailure _ 
778                              | Uncertain _ -> None)
779                           meets
780                         with
781                         | Some x -> x
782                         | None -> raise exn)
783                         (* }}} pullback *)
784                   (* {{{ CSC: This is necessary because of the "elim H" tactic
785                          where the type of H is only reducible to an
786                          inductive type. This could be extended from inductive
787                          types to any rigid term. However, the code is
788                          duplicated in two places: inside applications and
789                          outside them. Probably it would be better to
790                          work with lambda-bar terms instead. *)
791                   | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
792                   | (_, Cic.MutInd _::_) ->
793                      let t1' = R.whd ~subst context t1 in
794                      (match t1' with
795                           C.Appl (C.MutInd _::_) -> 
796                             fo_unif_subst test_equality_only 
797                               subst context metasenv t1' t2 ugraph         
798                         | _ -> raise (UnificationFailure (lazy "88")))
799                   | (Cic.MutInd _::_,_) ->
800                      let t2' = R.whd ~subst context t2 in
801                      (match t2' with
802                           C.Appl (C.MutInd _::_) -> 
803                             fo_unif_subst test_equality_only 
804                               subst context metasenv t1 t2' ugraph         
805                         | _ -> raise 
806                             (UnificationFailure 
807                                (lazy ("not a mutind :"^
808                                 CicMetaSubst.ppterm ~metasenv subst t2 ))))
809                      (* }}} elim H *)
810                   | _ -> raise exn)))
811    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
812        let subst', metasenv',ugraph1 = 
813         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
814           ugraph in
815        let subst'',metasenv'',ugraph2 = 
816         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
817           ugraph1 in
818        (try
819          List.fold_left2 
820           (fun (subst,metasenv,ugraph) t1 t2 ->
821             fo_unif_subst 
822              test_equality_only subst context metasenv t1 t2 ugraph
823           ) (subst'',metasenv'',ugraph2) pl1 pl2 
824         with
825          Invalid_argument _ ->
826           raise (UnificationFailure (lazy "6.1")))
827            (* (sprintf
828               "Error trying to unify %s with %s: the number of branches is not the same." 
829               (CicMetaSubst.ppterm ~metasenv subst t1) 
830               (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
831    | (C.Rel _, _) | (_,  C.Rel _) ->
832        if t1 = t2 then
833          subst, metasenv,ugraph
834        else
835         raise (UnificationFailure (lazy 
836            (sprintf
837              "Can't unify %s with %s because they are not convertible"
838              (CicMetaSubst.ppterm ~metasenv subst t1) 
839              (CicMetaSubst.ppterm ~metasenv subst t2))))
840    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
841        let subst,metasenv,beta_expanded,ugraph1 =
842          beta_expand_many 
843            test_equality_only metasenv subst context t2 args ugraph 
844        in
845          fo_unif_subst test_equality_only subst context metasenv 
846            (C.Meta (i,l)) beta_expanded ugraph1
847    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
848        let subst,metasenv,beta_expanded,ugraph1 =
849          beta_expand_many 
850            test_equality_only metasenv subst context t1 args ugraph 
851        in
852          fo_unif_subst test_equality_only subst context metasenv 
853            beta_expanded (C.Meta (i,l)) ugraph1
854 (* Works iff there are no arguments applied to it; similar to the
855    case below
856    | (_, C.MutInd _) ->
857        let t1' = R.whd ~subst context t1 in
858        (match t1' with
859             C.MutInd _ -> 
860               fo_unif_subst test_equality_only 
861                 subst context metasenv t1' t2 ugraph         
862           | _ -> raise (UnificationFailure (lazy "8")))
863 *)
864    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
865        let subst',metasenv',ugraph1 = 
866          fo_unif_subst true subst context metasenv s1 s2 ugraph 
867        in
868          fo_unif_subst test_equality_only 
869            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
870    | (C.Prod _, _) ->
871        (match CicReduction.whd ~subst context t2 with
872         | C.Prod _ as t2 -> 
873             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
874         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
875    | (_, C.Prod _) ->
876        (match CicReduction.whd ~subst context t1 with
877         | C.Prod _ as t1 -> 
878             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
879         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
880    | (_,_) ->
881      (* delta-beta reduction should almost never be a problem for
882         unification since:
883          1. long computations require iota reduction
884          2. it is extremely rare that a close term t1 (that could be unified
885             to t2) beta-delta reduces to t1' while t2 does not beta-delta
886             reduces in the same way. This happens only if one meta of t2
887             occurs in head position during beta reduction. In this unluky
888             case too much reduction will be performed on t1 and unification
889             will surely fail. *)
890      let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
891      let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
892       if t1 = t1' && t2 = t2' then
893        raise (UnificationFailure
894         (lazy 
895           (sprintf
896             "Can't unify %s with %s because they are not convertible"
897             (CicMetaSubst.ppterm ~metasenv subst t1) 
898             (CicMetaSubst.ppterm ~metasenv subst t2))))
899       else
900        try
901         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
902        with
903           UnificationFailure _
904         | Uncertain _ ->
905            raise (UnificationFailure
906             (lazy 
907               (sprintf
908                 "Can't unify %s with %s because they are not convertible"
909                 (CicMetaSubst.ppterm ~metasenv subst t1) 
910                 (CicMetaSubst.ppterm ~metasenv subst t2))))
911
912 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
913  exp_named_subst1 exp_named_subst2 ugraph
914 =
915  try
916   List.fold_left2
917    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
918      assert (uri1=uri2) ;
919      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
920    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
921  with
922   Invalid_argument _ ->
923    let print_ens ens =
924     String.concat " ; "
925      (List.map
926        (fun (uri,t) ->
927          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
928        ) ens) 
929    in
930     raise (UnificationFailure (lazy (sprintf
931      "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))))
932
933 (* A substitution is a (int * Cic.term) list that associates a               *)
934 (* metavariable i with its body.                                             *)
935 (* metasenv is of type Cic.metasenv                                          *)
936 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
937 (* a new substitution which is already unwinded and ready to be applied and  *)
938 (* a new metasenv in which some hypothesis in the contexts of the            *)
939 (* metavariables may have been restricted.                                   *)
940 let fo_unif metasenv context t1 t2 ugraph = 
941  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
942
943 let enrich_msg msg subst context metasenv t1 t2 ugraph =
944  lazy (
945   if verbose then
946    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"
947     (CicMetaSubst.ppterm ~metasenv subst t1)
948     (try
949       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
950       CicPp.ppterm ty_t1
951     with 
952     | UnificationFailure s
953     | Uncertain s
954     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
955     (CicMetaSubst.ppterm ~metasenv subst t2)
956     (try
957       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
958       CicPp.ppterm ty_t2
959     with
960     | UnificationFailure s
961     | Uncertain s
962     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
963     (CicMetaSubst.ppcontext ~metasenv subst context)
964     (CicMetaSubst.ppmetasenv subst metasenv)
965     (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
966  else
967    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
968     (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
969     (try
970       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
971       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
972     with 
973     | UnificationFailure s
974     | Uncertain s
975     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
976     (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
977     (try
978       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
979       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
980     with
981     | UnificationFailure s
982     | Uncertain s
983     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
984     (CicMetaSubst.ppcontext ~metasenv subst context)
985     ("OMITTED" (*CicMetaSubst.ppmetasenv subst metasenv*))
986     (Lazy.force msg)
987  )
988
989 let fo_unif_subst subst context metasenv t1 t2 ugraph =
990   try
991     fo_unif_subst false subst context metasenv t1 t2 ugraph
992   with
993   | AssertFailure msg ->
994      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
995   | UnificationFailure msg ->
996      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
997 ;;