]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_unification/cicUnification.ml
transcript: now we can generate procedural output
[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
306 (* NUOVA UNIFICAZIONE *)
307 (* A substitution is a (int * Cic.term) list that associates a
308    metavariable i with its body.
309    A metaenv is a (int * Cic.term) list that associate a metavariable
310    i with is type. 
311    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
312    a new substitution which is _NOT_ unwinded. It must be unwinded before
313    applying it. *)
314
315 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =  
316  let module C = Cic in
317  let module R = CicReduction in
318  let module S = CicSubstitution in
319  let t1 = deref subst t1 in
320  let t2 = deref subst t2 in
321  let (&&&) a b = (a && b) || ((not a) && (not b)) in
322 (* let bef = Sys.time () in *)
323  let b,ugraph =
324   if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
325    false,ugraph
326   else
327 let foo () =
328    R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
329 in profiler_are_convertible.HExtlib.profile foo ()
330  in
331 (* let aft = Sys.time () in
332 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
333    if b then
334      subst, metasenv, ugraph 
335    else
336    match (t1, t2) with
337      | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
338          let _,subst,metasenv,ugraph1 =
339            (try
340               List.fold_left2
341                 (fun (j,subst,metasenv,ugraph) t1 t2 ->
342                    match t1,t2 with
343                        None,_
344                      | _,None -> j+1,subst,metasenv,ugraph
345                      | Some t1', Some t2' ->
346                          (* First possibility:  restriction    *)
347                          (* Second possibility: unification    *)
348                          (* Third possibility:  convertibility *)
349                          let b, ugraph1 = 
350                          R.are_convertible 
351                            ~subst ~metasenv context t1' t2' ugraph
352                          in
353                          if b then
354                            j+1,subst,metasenv, ugraph1 
355                          else
356                            (try
357                               let subst,metasenv,ugraph2 =
358                                 fo_unif_subst 
359                                   test_equality_only 
360                                   subst context metasenv t1' t2' ugraph
361                               in
362                                 j+1,subst,metasenv,ugraph2
363                             with
364                                 Uncertain _
365                               | UnificationFailure _ ->
366 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); 
367                                   let metasenv, subst = 
368                                     CicMetaSubst.restrict 
369                                       subst [(n,j)] metasenv in
370                                     j+1,subst,metasenv,ugraph1)
371                 ) (1,subst,metasenv,ugraph) ln lm
372             with
373                 Exit ->
374                   raise 
375                     (UnificationFailure (lazy "1"))
376                     (*
377                     (sprintf
378                       "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."
379                       (CicMetaSubst.ppterm ~metasenv subst t1) 
380                       (CicMetaSubst.ppterm ~metasenv subst t2))) *)
381               | Invalid_argument _ ->
382                   raise 
383                     (UnificationFailure (lazy "2")))
384                     (*
385                     (sprintf
386                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match." 
387                       (CicMetaSubst.ppterm ~metasenv subst t1) 
388                       (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
389          in subst,metasenv,ugraph1
390      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
391          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
392      | (C.Meta (n,l), t)   
393      | (t, C.Meta (n,l)) ->
394          let swap =
395            match t1,t2 with
396                C.Meta (n,_), C.Meta (m,_) when n < m -> false
397              | _, C.Meta _ -> false
398              | _,_ -> true
399          in
400          let lower = fun x y -> if swap then y else x in
401          let upper = fun x y -> if swap then x else y in
402          let fo_unif_subst_ordered 
403              test_equality_only subst context metasenv m1 m2 ugraph =
404            fo_unif_subst test_equality_only subst context metasenv 
405              (lower m1 m2) (upper m1 m2) ugraph
406          in
407          begin
408          let subst,metasenv,ugraph1 = 
409            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
410            (try
411               let tyt,ugraph1 = 
412                 type_of_aux' metasenv subst context t ugraph 
413               in
414                 fo_unif_subst 
415                   test_equality_only 
416                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
417             with 
418                 UnificationFailure _ as e -> raise e
419               | Uncertain msg -> raise (UnificationFailure msg)
420               | AssertFailure _ ->
421                   debug_print (lazy "siamo allo huge hack");
422                   (* TODO huge hack!!!!
423                    * we keep on unifying/refining in the hope that 
424                    * the problem will be eventually solved. 
425                    * In the meantime we're breaking a big invariant:
426                    * the terms that we are unifying are no longer well 
427                    * typed in the current context (in the worst case 
428                    * we could even diverge) *)
429                   (subst, metasenv,ugraph)) in
430          let t',metasenv,subst =
431            try 
432              CicMetaSubst.delift n subst context metasenv l t
433            with
434                (CicMetaSubst.MetaSubstFailure msg)-> 
435                  raise (UnificationFailure msg)
436              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
437          in
438          let t'',ugraph2 =
439            match t' with
440                C.Sort (C.Type u) when not test_equality_only ->
441                  let u' = CicUniv.fresh () in
442                  let s = C.Sort (C.Type u') in
443                   (try
444                     let ugraph2 =   
445                      CicUniv.add_ge (upper u u') (lower u u') ugraph1
446                     in
447                      s,ugraph2
448                    with
449                     CicUniv.UniverseInconsistency msg ->
450                      raise (UnificationFailure msg))
451              | _ -> t',ugraph1
452          in
453          (* Unifying the types may have already instantiated n. Let's check *)
454          try
455            let (_, oldt,_) = CicUtil.lookup_subst n subst in
456            let lifted_oldt = S.subst_meta l oldt in
457              fo_unif_subst_ordered 
458                test_equality_only subst context metasenv t lifted_oldt ugraph2
459          with
460              CicUtil.Subst_not_found _ -> 
461                let (_, context, ty) = CicUtil.lookup_meta n metasenv in
462                let subst = (n, (context, t'',ty)) :: subst in
463                let metasenv =
464                  List.filter (fun (m,_,_) -> not (n = m)) metasenv in
465                subst, metasenv, ugraph2
466          end
467    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
468    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
469       if UriManager.eq uri1 uri2 then
470        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
471         exp_named_subst1 exp_named_subst2 ugraph
472       else
473        raise (UnificationFailure (lazy 
474           (sprintf
475             "Can't unify %s with %s due to different constants"
476             (CicMetaSubst.ppterm ~metasenv subst t1) 
477             (CicMetaSubst.ppterm ~metasenv subst t2))))
478    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
479        if UriManager.eq uri1 uri2 && i1 = i2 then
480          fo_unif_subst_exp_named_subst 
481            test_equality_only 
482            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
483        else
484          raise (UnificationFailure
485            (lazy
486             (sprintf
487              "Can't unify %s with %s due to different inductive principles"
488              (CicMetaSubst.ppterm ~metasenv subst t1) 
489              (CicMetaSubst.ppterm ~metasenv subst t2))))
490    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
491        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
492        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
493          fo_unif_subst_exp_named_subst
494            test_equality_only 
495            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
496        else
497          raise (UnificationFailure
498           (lazy
499             (sprintf
500               "Can't unify %s with %s due to different inductive constructors"
501               (CicMetaSubst.ppterm ~metasenv subst t1) 
502               (CicMetaSubst.ppterm ~metasenv subst t2))))
503    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
504    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
505                               subst context metasenv te t2 ugraph
506    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only 
507                               subst context metasenv t1 te ugraph
508    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 
509        let subst',metasenv',ugraph1 = 
510          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph 
511        in
512          fo_unif_subst test_equality_only 
513            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
514    | (C.LetIn (_,s1,ty1,t1), t2)  
515    | (t2, C.LetIn (_,s1,ty1,t1)) -> 
516        fo_unif_subst 
517         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
518    | (C.Appl l1, C.Appl l2) -> 
519        (* andrea: this case should be probably rewritten in the 
520           spirit of deref *)
521        (match l1,l2 with
522           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
523               (try 
524                  List.fold_left2 
525                    (fun (subst,metasenv,ugraph) t1 t2 ->
526                       fo_unif_subst 
527                         test_equality_only subst context metasenv t1 t2 ugraph)
528                    (subst,metasenv,ugraph) l1 l2 
529                with (Invalid_argument msg) -> 
530                  raise (UnificationFailure (lazy msg)))
531           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
532               (* we verify that none of the args is a Meta, 
533                 since beta expanding with respoect to a metavariable 
534                 makes no sense  *)
535  (*
536               (try 
537                  let (_,t,_) = CicUtil.lookup_subst i subst in
538                  let lifted = S.subst_meta l t in
539                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
540                    fo_unif_subst 
541                     test_equality_only 
542                      subst context metasenv reduced t2 ugraph
543                with CicUtil.Subst_not_found _ -> *)
544               let subst,metasenv,beta_expanded,ugraph1 =
545                 beta_expand_many 
546                   test_equality_only metasenv subst context t2 args ugraph 
547               in
548                 fo_unif_subst test_equality_only subst context metasenv 
549                   (C.Meta (i,l)) beta_expanded ugraph1
550           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
551               (* (try 
552                  let (_,t,_) = CicUtil.lookup_subst i subst in
553                  let lifted = S.subst_meta l t in
554                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
555                    fo_unif_subst 
556                      test_equality_only 
557                      subst context metasenv t1 reduced ugraph
558                with CicUtil.Subst_not_found _ -> *)
559                  let subst,metasenv,beta_expanded,ugraph1 =
560                    beta_expand_many 
561                      test_equality_only 
562                      metasenv subst context t1 args ugraph 
563                  in
564                    fo_unif_subst test_equality_only subst context metasenv 
565                      (C.Meta (i,l)) beta_expanded ugraph1
566           | _,_ ->
567               let lr1 = List.rev l1 in
568               let lr2 = List.rev l2 in
569               let rec 
570                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
571                 match (l1,l2) with
572                     [],_
573                   | _,[] -> assert false
574                   | ([h1],[h2]) ->
575                       fo_unif_subst 
576                         test_equality_only subst context metasenv h1 h2 ugraph
577                   | ([h],l) 
578                   | (l,[h]) ->
579                       fo_unif_subst test_equality_only subst context metasenv
580                         h (C.Appl (List.rev l)) ugraph
581                   | ((h1::l1),(h2::l2)) -> 
582                       let subst', metasenv',ugraph1 = 
583                         fo_unif_subst 
584                           test_equality_only 
585                           subst context metasenv h1 h2 ugraph
586                       in 
587                         fo_unif_l 
588                           test_equality_only subst' metasenv' (l1,l2) ugraph1
589               in
590               (try 
591                 fo_unif_l 
592                   test_equality_only subst metasenv (lr1, lr2)  ugraph
593               with 
594               | UnificationFailure s
595               | Uncertain s as exn -> 
596                   (match l1, l2 with
597                   | (((Cic.Const (uri1, ens1)) as cc1) :: tl1), 
598                      (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
599                     CoercDb.is_a_coercion cc1 <> None && 
600                     CoercDb.is_a_coercion cc2 <> None &&
601                     not (UriManager.eq uri1 uri2) ->
602 (*DEBUGGING ONLY: 
603 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
604 let res =
605         *)
606                      let inner_coerced t =
607                       let t = CicMetaSubst.apply_subst subst t in
608                       let rec aux c x t =
609                         match t with
610                         | Cic.Appl l -> 
611                             (match CoercGraph.coerced_arg l with
612                             | None -> c, x
613                             | Some (t,_) -> aux (List.hd l) t t)
614                         | _ ->  c, x
615                       in
616                       aux (Cic.Implicit None) (Cic.Implicit None) t
617                      in
618                       let c1,last_tl1 = inner_coerced (Cic.Appl l1) in 
619                       let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
620                       let car1, car2 =
621                         match 
622                           CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
623                         with
624                         | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
625                         | _ -> assert false
626                       in
627                       let head1_c, head2_c =
628                         match 
629                           CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
630                         with
631                         | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
632                         | _ -> assert false
633                       in
634                       let unfold uri ens args =
635                         let o, _ = 
636                           CicEnvironment.get_obj CicUniv.oblivion_ugraph uri 
637                         in
638                         assert (ens = []);
639                         match o with
640                         | Cic.Constant (_,Some bo,_,_,_) -> 
641                             CicReduction.head_beta_reduce ~delta:false
642                               (Cic.Appl (bo::args))
643                         | _ -> assert false
644                       in
645                       if CoercDb.eq_carr car1 car2 then
646                          match last_tl1,last_tl2 with
647                          | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
648                          | _, C.Meta _
649                          | C.Meta _, _ ->
650                            let subst,metasenv,ugraph =
651                             fo_unif_subst test_equality_only subst context
652                              metasenv last_tl1 last_tl2 ugraph
653                            in
654                             fo_unif_subst test_equality_only subst context
655                              metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
656                          | _ when CoercDb.eq_carr head1_c head2_c ->
657                            let l1, l2 = 
658                                (* composite VS composition + metas avoiding
659                                 * coercions not only in coerced position *)
660                                if c1 = cc1 then 
661                                  unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
662                                else Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
663                            in
664                             fo_unif_subst test_equality_only subst context
665                              metasenv l1 l2 ugraph
666                          | _ -> raise exn
667                       else
668                        let meets = 
669                          CoercGraph.meets metasenv subst context car1 car2 
670                        in
671                        (match meets with
672                         | [] -> raise exn
673                         | (carr,metasenv,to1,to2)::xxx -> 
674                           (match xxx with
675                           | [] -> ()
676                           | (m2,_,c2,c2')::_ ->
677                           let m1,_,c1,c1' = carr,metasenv,to1,to2 in
678                           let unopt = 
679                             function Some (_,t) -> CicPp.ppterm t 
680                             | None -> "id"
681                           in
682                           HLog.warn 
683                             ("There are two minimal joins of "^
684                             CoercDb.string_of_carr car1^" and "^
685                             CoercDb.string_of_carr car2^": " ^ 
686                             CoercDb.string_of_carr m1 ^ " via "^unopt c1^" + "^
687                             unopt c1'^" and "^CoercDb.string_of_carr m2^" via "^
688                             unopt c2^" + "^unopt c2'));
689                           let last_tl1',(subst,metasenv,ugraph) =
690                            match last_tl1,to1 with
691                             | Cic.Meta (i1,l1),Some (last,coerced) -> 
692                                 last,
693                                   fo_unif_subst test_equality_only subst context
694                                      metasenv coerced last_tl1 ugraph
695                             | _ -> last_tl1,(subst,metasenv,ugraph) 
696                           in
697                           let last_tl2',(subst,metasenv,ugraph) =
698                            match last_tl2,to2 with
699                             | Cic.Meta (i2,l2),Some (last,coerced) -> 
700                                 last,
701                                   fo_unif_subst test_equality_only subst context
702                                      metasenv coerced last_tl2 ugraph
703                             | _ -> last_tl2,(subst,metasenv,ugraph) 
704                           in
705                         (*DEBUGGING ONLY:
706 prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
707 *)
708                            let subst,metasenv,ugraph =
709                             fo_unif_subst test_equality_only subst context
710                              metasenv last_tl1' last_tl2' ugraph
711                            in
712                             fo_unif_subst test_equality_only subst context
713                              metasenv (C.Appl l1) (C.Appl l2) ugraph)
714 (*DEBUGGING ONLY:
715 in
716 let subst,metasenv,ugraph = res in
717 prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
718 res
719 *)
720
721                   (*CSC: This is necessary because of the "elim H" tactic
722                          where the type of H is only reducible to an
723                          inductive type. This could be extended from inductive
724                          types to any rigid term. However, the code is
725                          duplicated in two places: inside applications and
726                          outside them. Probably it would be better to
727                          work with lambda-bar terms instead. *)
728                   | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
729                   | (_, Cic.MutInd _::_) ->
730                      let t1' = R.whd ~subst context t1 in
731                      (match t1' with
732                           C.Appl (C.MutInd _::_) -> 
733                             fo_unif_subst test_equality_only 
734                               subst context metasenv t1' t2 ugraph         
735                         | _ -> raise (UnificationFailure (lazy "88")))
736                   | (Cic.MutInd _::_,_) ->
737                      let t2' = R.whd ~subst context t2 in
738                      (match t2' with
739                           C.Appl (C.MutInd _::_) -> 
740                             fo_unif_subst test_equality_only 
741                               subst context metasenv t1 t2' ugraph         
742                         | _ -> raise 
743                             (UnificationFailure 
744                                (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 ))))
745                   | _ -> raise exn)))
746    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
747        let subst', metasenv',ugraph1 = 
748         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
749           ugraph in
750        let subst'',metasenv'',ugraph2 = 
751         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
752           ugraph1 in
753        (try
754          List.fold_left2 
755           (fun (subst,metasenv,ugraph) t1 t2 ->
756             fo_unif_subst 
757              test_equality_only subst context metasenv t1 t2 ugraph
758           ) (subst'',metasenv'',ugraph2) pl1 pl2 
759         with
760          Invalid_argument _ ->
761           raise (UnificationFailure (lazy "6.1")))
762            (* (sprintf
763               "Error trying to unify %s with %s: the number of branches is not the same." 
764               (CicMetaSubst.ppterm ~metasenv subst t1) 
765               (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
766    | (C.Rel _, _) | (_,  C.Rel _) ->
767        if t1 = t2 then
768          subst, metasenv,ugraph
769        else
770         raise (UnificationFailure (lazy 
771            (sprintf
772              "Can't unify %s with %s because they are not convertible"
773              (CicMetaSubst.ppterm ~metasenv subst t1) 
774              (CicMetaSubst.ppterm ~metasenv subst t2))))
775    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
776        let subst,metasenv,beta_expanded,ugraph1 =
777          beta_expand_many 
778            test_equality_only metasenv subst context t2 args ugraph 
779        in
780          fo_unif_subst test_equality_only subst context metasenv 
781            (C.Meta (i,l)) beta_expanded ugraph1
782    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
783        let subst,metasenv,beta_expanded,ugraph1 =
784          beta_expand_many 
785            test_equality_only metasenv subst context t1 args ugraph 
786        in
787          fo_unif_subst test_equality_only subst context metasenv 
788            beta_expanded (C.Meta (i,l)) ugraph1
789 (* Works iff there are no arguments applied to it; similar to the
790    case below
791    | (_, C.MutInd _) ->
792        let t1' = R.whd ~subst context t1 in
793        (match t1' with
794             C.MutInd _ -> 
795               fo_unif_subst test_equality_only 
796                 subst context metasenv t1' t2 ugraph         
797           | _ -> raise (UnificationFailure (lazy "8")))
798 *)
799    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
800        let subst',metasenv',ugraph1 = 
801          fo_unif_subst true subst context metasenv s1 s2 ugraph 
802        in
803          fo_unif_subst test_equality_only 
804            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
805    | (C.Prod _, _) ->
806        (match CicReduction.whd ~subst context t2 with
807         | C.Prod _ as t2 -> 
808             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
809         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
810    | (_, C.Prod _) ->
811        (match CicReduction.whd ~subst context t1 with
812         | C.Prod _ as t1 -> 
813             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
814         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
815    | (_,_) ->
816      (* delta-beta reduction should almost never be a problem for
817         unification since:
818          1. long computations require iota reduction
819          2. it is extremely rare that a close term t1 (that could be unified
820             to t2) beta-delta reduces to t1' while t2 does not beta-delta
821             reduces in the same way. This happens only if one meta of t2
822             occurs in head position during beta reduction. In this unluky
823             case too much reduction will be performed on t1 and unification
824             will surely fail. *)
825      let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
826      let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
827       if t1 = t1' && t2 = t2' then
828        raise (UnificationFailure
829         (lazy 
830           (sprintf
831             "Can't unify %s with %s because they are not convertible"
832             (CicMetaSubst.ppterm ~metasenv subst t1) 
833             (CicMetaSubst.ppterm ~metasenv subst t2))))
834       else
835        try
836         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
837        with
838           UnificationFailure _
839         | Uncertain _ ->
840            raise (UnificationFailure
841             (lazy 
842               (sprintf
843                 "Can't unify %s with %s because they are not convertible"
844                 (CicMetaSubst.ppterm ~metasenv subst t1) 
845                 (CicMetaSubst.ppterm ~metasenv subst t2))))
846
847 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
848  exp_named_subst1 exp_named_subst2 ugraph
849 =
850  try
851   List.fold_left2
852    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
853      assert (uri1=uri2) ;
854      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
855    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
856  with
857   Invalid_argument _ ->
858    let print_ens ens =
859     String.concat " ; "
860      (List.map
861        (fun (uri,t) ->
862          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
863        ) ens) 
864    in
865     raise (UnificationFailure (lazy (sprintf
866      "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))))
867
868 (* A substitution is a (int * Cic.term) list that associates a               *)
869 (* metavariable i with its body.                                             *)
870 (* metasenv is of type Cic.metasenv                                          *)
871 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
872 (* a new substitution which is already unwinded and ready to be applied and  *)
873 (* a new metasenv in which some hypothesis in the contexts of the            *)
874 (* metavariables may have been restricted.                                   *)
875 let fo_unif metasenv context t1 t2 ugraph = 
876  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
877
878 let enrich_msg msg subst context metasenv t1 t2 ugraph =
879  lazy (
880   if verbose then
881    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"
882     (CicMetaSubst.ppterm ~metasenv subst t1)
883     (try
884       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
885       CicPp.ppterm ty_t1
886     with 
887     | UnificationFailure s
888     | Uncertain s
889     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
890     (CicMetaSubst.ppterm ~metasenv subst t2)
891     (try
892       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
893       CicPp.ppterm ty_t2
894     with
895     | UnificationFailure s
896     | Uncertain s
897     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
898     (CicMetaSubst.ppcontext ~metasenv subst context)
899     (CicMetaSubst.ppmetasenv subst metasenv)
900     (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
901  else
902    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
903     (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
904     (try
905       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
906       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
907     with 
908     | UnificationFailure s
909     | Uncertain s
910     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
911     (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
912     (try
913       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
914       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
915     with
916     | UnificationFailure s
917     | Uncertain s
918     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
919     (CicMetaSubst.ppcontext ~metasenv subst context)
920     (CicMetaSubst.ppmetasenv subst metasenv)
921     (Lazy.force msg)
922  )
923
924 let fo_unif_subst subst context metasenv t1 t2 ugraph =
925   try
926     fo_unif_subst false subst context metasenv t1 t2 ugraph
927   with
928   | AssertFailure msg ->
929      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
930   | UnificationFailure msg ->
931      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
932 ;;