]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/ng_refiner/nCicUnification.ml
Debugging code commented out.
[helm.git] / matitaB / components / ng_refiner / nCicUnification.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id$ *)
13
14 exception UnificationFailure of string Lazy.t;;
15 exception Uncertain of string Lazy.t;;
16 exception AssertFailure of string Lazy.t;;
17 exception KeepReducing of string Lazy.t;;
18 exception KeepReducingThis of 
19   string Lazy.t * (NCicReduction.machine * bool) * 
20                   (NCicReduction.machine * bool) ;;
21
22 let (===) x y = Pervasives.compare x y = 0 ;;
23
24 let mk_msg (status:#NCic.status) metasenv subst context t1 t2 =
25  (lazy (
26   "Can't unify " ^ status#ppterm ~metasenv ~subst ~context t1 ^
27   " with " ^ status#ppterm ~metasenv ~subst ~context t2))
28
29 let mk_appl status ~upto hd tl =
30   NCicReduction.head_beta_reduce status ~upto
31     (match hd with
32     | NCic.Appl l -> NCic.Appl (l@tl)
33     | _ -> NCic.Appl (hd :: tl))
34 ;;
35
36 exception WrongShape;;
37
38 let eta_reduce status subst t = 
39   let delift_if_not_occur body =
40     try 
41         Some (NCicSubstitution.psubst status ~avoid_beta_redexes:true
42           (fun () -> raise WrongShape) [()] body)
43     with WrongShape -> None
44   in 
45   let rec eat_lambdas ctx = function
46     | NCic.Lambda (name, src, tgt) -> 
47         eat_lambdas ((name, src) :: ctx) tgt
48     | NCic.Meta (i,lc) as t->
49         (try 
50           let _,_,t,_ = NCicUtils.lookup_subst i subst in
51           let t = NCicSubstitution.subst_meta status lc t in
52           eat_lambdas ctx t
53         with NCicUtils.Subst_not_found _ -> ctx, t)
54     | t -> ctx, t
55   in
56   let context_body = eat_lambdas [] t in
57   let rec aux = function
58     | [],body -> body
59     | (name, src)::ctx, (NCic.Appl (hd::[NCic.Rel 1]) as bo) -> 
60         (match delift_if_not_occur hd with
61         | None -> aux (ctx,NCic.Lambda(name,src, bo)) 
62         | Some bo -> aux (ctx,bo))
63     | (name, src)::ctx, (NCic.Appl args as bo) 
64       when HExtlib.list_last args = NCic.Rel 1 -> 
65         let args, _ = HExtlib.split_nth (List.length args - 1) args in
66         (match delift_if_not_occur (NCic.Appl args) with
67         | None -> aux (ctx,NCic.Lambda(name,src, bo)) 
68         | Some bo -> aux (ctx,bo))
69     | (name, src) :: ctx, t ->
70         aux (ctx,NCic.Lambda(name,src, t)) 
71   in
72     aux context_body
73 ;;
74
75 module C = NCic;;
76 module Ref = NReference;;
77
78 let debug = ref false;;
79 let indent = ref "";;
80 let times = ref [];;
81 let pp s =
82  if !debug then
83   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
84 ;;
85 let inside c =
86  if !debug then
87   begin
88    let time1 = Unix.gettimeofday () in
89    indent := !indent ^ String.make 1 c;
90    times := time1 :: !times;
91    prerr_endline ("{{{" ^ !indent ^ " ")
92   end
93 ;;
94 let outside exc_opt =
95  if !debug then
96   begin
97    let time2 = Unix.gettimeofday () in
98    let time1 =
99     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
100    prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
101    (match exc_opt with
102    | Some e ->  prerr_endline ("exception raised: " ^ Printexc.to_string e)
103    | None -> ());
104    try
105     indent := String.sub !indent 0 (String.length !indent -1)
106    with
107     Invalid_argument _ -> indent := "??"; ()
108   end
109 ;;
110
111 let ppcontext status ~metasenv ~subst c = 
112       "\nctx:\n"^ status#ppcontext ~metasenv ~subst c
113 ;;
114 let ppmetasenv status ~subst m = "\nmenv:\n" ^ status#ppmetasenv ~subst m;;
115
116 let ppcontext _status ~metasenv:_metasenv ~subst:_subst _context = "";;
117 let ppmetasenv _status ~subst:_subst _metasenv = "";;
118 let ppterm (status:#NCic.status) ~metasenv ~subst ~context = status#ppterm ~metasenv ~subst ~context;;
119 (* let ppterm status ~metasenv:_ ~subst:_ ~context:_ _ = "";; *)
120
121 let is_locked n subst =
122    try
123      match NCicUtils.lookup_subst n subst with
124      | tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true
125      | _ -> false
126    with NCicUtils.Subst_not_found _ -> false
127 ;;
128
129 let rec mk_irl stop base =
130   if base > stop then []
131   else (NCic.Rel base) :: mk_irl stop (base+1) 
132 ;;
133
134 (* the argument must be a term in whd *)
135 let rec could_reduce =
136  function
137   | C.Meta _ -> true
138   | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args)
139      when List.length args > recno -> could_reduce (List.nth args recno)
140   | C.Match (_,_,arg,_) -> could_reduce arg
141   | C.Appl (he::_) -> could_reduce he
142   | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
143   | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
144 ;;
145
146 let rec lambda_intros status metasenv subst context argsno ty =
147  pp (lazy ("LAMBDA INTROS: " ^ ppterm status ~metasenv ~subst ~context ty));
148  match argsno with
149     0 -> 
150        let metasenv, _, bo, _ = 
151          NCicMetaSubst.mk_meta metasenv context ~with_type:ty `IsTerm
152        in
153        metasenv, bo
154   | _ ->
155      (match NCicReduction.whd status ~subst context ty with
156          C.Prod (n,so,ta) ->
157           let metasenv,bo =
158            lambda_intros status metasenv subst
159             ((n,C.Decl so)::context) (argsno - 1) ta
160           in
161            metasenv,C.Lambda (n,so,bo)
162        | _ -> assert false)
163 ;;
164   
165 let unopt exc = function None -> raise exc | Some x -> x ;;
166
167 let fix (status:#NCic.status) metasenv subst is_sup test_eq_only exc t =
168   (*D*)  inside 'f'; try let rc =  
169   pp (lazy (status#ppterm ~metasenv ~subst ~context:[] t));
170   let rec aux test_eq_only metasenv = function
171     | NCic.Prod (n,so,ta) ->
172        let metasenv,so = aux true metasenv so in
173        let metasenv,ta = aux test_eq_only metasenv ta in
174         metasenv,NCic.Prod (n,so,ta)
175     | NCic.Sort (NCic.Type [(`CProp|`Type),_]) as orig when test_eq_only ->
176        metasenv,orig
177     | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
178     | NCic.Sort (NCic.Type u) when is_sup ->
179        metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
180     | NCic.Sort (NCic.Type u) ->
181        metasenv, NCic.Sort (NCic.Type 
182          (unopt exc (NCicEnvironment.inf ~strict:false u)))
183     | NCic.Meta (n,_) as orig ->
184         (try 
185           let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
186          with NCicUtils.Subst_not_found _ -> 
187           let metasenv, _ = NCicMetaSubst.extend_meta metasenv n in
188            metasenv, orig)
189     | t ->
190       NCicUntrusted.map_term_fold_a status (fun _ x -> x) test_eq_only aux metasenv t
191   in
192    aux test_eq_only metasenv t
193  (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
194 ;;
195
196 let metasenv_to_subst n (kind,context,ty) metasenv subst =
197  let infos,metasenv = List.partition (fun (n',_) -> n = n') metasenv in
198  let attrs,octx,oty = match infos with [_,infos] -> infos | _ -> assert false in
199  if octx=context && oty=ty then
200   (n,(NCicUntrusted.set_kind kind attrs, octx, oty))::metasenv,subst
201  else 
202   let metasenv, _, bo, _ = 
203    NCicMetaSubst.mk_meta metasenv context ~attrs ~with_type:ty kind in
204   let subst = (n,(NCicUntrusted.set_kind kind attrs,octx,bo,oty))::subst in
205    metasenv,subst
206 ;;
207
208 let rec sortfy status exc metasenv subst context t =
209  let t = NCicReduction.whd status ~subst context t in
210  let metasenv,subst =
211   match t with
212    | NCic.Sort _ -> metasenv, subst
213    | NCic.Meta (n,_) -> 
214       let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
215       let kind = NCicUntrusted.kind_of_meta attrs in
216        if kind = `IsSort then
217         metasenv,subst
218        else
219         (match ty with
220           | NCic.Implicit (`Typeof _) ->
221               metasenv_to_subst n (`IsSort,[],ty) metasenv subst
222           | ty ->
223              let metasenv,subst,ty = sortfy status exc metasenv subst context ty in
224               metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
225    | NCic.Implicit _ -> assert false
226    | _ -> raise exc
227  in
228   metasenv,subst,t
229
230 let tipify status exc metasenv subst context t ty =
231  let is_type attrs =
232   match NCicUntrusted.kind_of_meta attrs with
233      `IsType | `IsSort -> true
234    | `IsTerm -> false
235  in
236  let rec optimize_meta metasenv subst =
237   function 
238      NCic.Meta (n,lc) ->
239       (try
240         let attrs,_,_ = NCicUtils.lookup_meta n metasenv in
241         if is_type attrs then
242          metasenv,subst,true
243         else
244          let _,cc,ty = NCicUtils.lookup_meta n metasenv in
245          let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
246          let metasenv = 
247            NCicUntrusted.replace_in_metasenv n
248             (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
249             metasenv 
250          in
251           metasenv,subst,false
252        with
253         NCicUtils.Meta_not_found _ ->
254          let attrs, _,bo,_ = NCicUtils.lookup_subst n subst in
255          if is_type attrs then
256           metasenv,subst,true
257          else
258           let _,cc,_,ty = NCicUtils.lookup_subst n subst in
259           let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
260           let subst = 
261             NCicUntrusted.replace_in_subst n
262               (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
263              subst 
264           in
265            optimize_meta metasenv subst (NCicSubstitution.subst_meta status lc bo))
266    | _ -> metasenv,subst,false
267  in
268   let metasenv,subst,b = optimize_meta metasenv subst t in
269    if b then
270     metasenv,subst,t
271    else
272     let metasenv,subst,_ = sortfy status exc metasenv subst context ty in
273      metasenv,subst,t
274 ;;
275
276 let rec instantiate status test_eq_only metasenv subst context n lc t swap =
277  (*D*)  inside 'I'; try let rc =  
278   pp (lazy(string_of_int n^" :=?= "^ppterm status ~metasenv ~subst ~context t));
279   let exc = 
280     UnificationFailure (mk_msg status metasenv subst context (NCic.Meta (n,lc)) t) in
281   let move_to_subst i ((_,cc,t,_) as infos) metasenv subst =
282     let metasenv = List.remove_assoc i metasenv in
283     pp(lazy(string_of_int n ^ " :==> "^ ppterm status ~metasenv ~subst ~context:cc t));
284     metasenv, (i,infos) :: subst
285   in
286   let delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv subst =
287     pp (lazy(string_of_int n ^ " := 111 = "^ 
288       ppterm status ~metasenv ~subst ~context t));
289     let (metasenv, subst), t = 
290       try 
291         NCicMetaSubst.delift status
292          ~unify:(fun m s c t1 t2 -> 
293            let ind = !indent in
294            let res = 
295              try Some (unify status test_eq_only m s c t1 t2 false)
296              with UnificationFailure _ | Uncertain _ -> None
297            in
298            indent := ind; res) 
299          metasenv subst context n lc t
300       with NCicMetaSubst.Uncertain msg -> 
301            pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
302            raise (Uncertain msg)
303       | NCicMetaSubst.MetaSubstFailure msg -> 
304            pp (lazy ("delift fails: " ^ Lazy.force msg));
305            raise (UnificationFailure msg)
306     in
307     pp (lazy(string_of_int n ^ " := 222 = "^
308       ppterm status ~metasenv ~subst ~context:cc t^ppmetasenv status ~subst metasenv));
309     (* Unifying the types may have already instantiated n. *)
310     try
311       let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
312       let oldt = NCicSubstitution.subst_meta status lc oldt in
313       let t = NCicSubstitution.subst_meta status lc t in
314       (* conjecture: always fail --> occur check *)
315       unify status test_eq_only metasenv subst context t oldt false
316     with NCicUtils.Subst_not_found _ -> 
317       move_to_subst n (attrs,cc,t,ty) metasenv subst
318   in
319   let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in
320   let kind = NCicUntrusted.kind_of_meta attrs in
321   let metasenv,t = fix status metasenv subst swap test_eq_only exc t in
322   let ty_t = NCicTypeChecker.typeof status ~metasenv ~subst context t in
323   let metasenv,subst,t =
324    match kind with
325       `IsSort -> sortfy status exc metasenv subst context t
326     | `IsType -> tipify status exc metasenv subst context t ty_t
327     | `IsTerm -> metasenv,subst,t in
328   match kind with
329   | `IsSort ->
330      (match ty,t with
331          NCic.Implicit (`Typeof _), NCic.Sort _ ->
332            move_to_subst n (attrs,cc,t,ty_t) metasenv subst  
333        | NCic.Sort (NCic.Type u1), NCic.Sort s ->
334           let s =
335            match s,swap with
336               NCic.Type u2, false ->
337                NCic.Sort (NCic.Type
338                 (unopt exc (NCicEnvironment.inf ~strict:false
339                  (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2))))
340             | NCic.Type u2, true ->
341                if NCicEnvironment.universe_lt u2 u1 then
342                 NCic.Sort (NCic.Type u2)
343                else (raise exc)
344             | NCic.Prop,_ -> NCic.Sort NCic.Prop
345           in
346            move_to_subst n (attrs,cc,s,ty) metasenv subst  
347        | NCic.Implicit (`Typeof _), NCic.Meta _ ->
348           move_to_subst n (attrs,cc,t,ty_t) metasenv subst  
349        | _, NCic.Meta _
350        | NCic.Meta _, NCic.Sort _ ->
351           pp (lazy ("On the types: " ^
352             ppterm status ~metasenv ~subst ~context ty ^ "=<=" ^
353             ppterm status ~metasenv ~subst ~context ty_t)); 
354           let metasenv, subst = 
355             unify status false metasenv subst context ty_t ty false in
356           delift_to_subst test_eq_only n lc (attrs,cc,ty) t
357            context metasenv subst
358        | _ -> assert false)
359   | `IsType
360   | `IsTerm ->
361      (match ty with
362          NCic.Implicit (`Typeof _) ->
363           let (metasenv, subst), ty_t = 
364             try 
365               NCicMetaSubst.delift status
366                ~unify:(fun m s c t1 t2 -> 
367                  let ind = !indent in
368                  let res = try Some (unify status test_eq_only m s c t1 t2 false )
369                    with UnificationFailure _ | Uncertain _ -> None
370                  in
371                  indent := ind; res)
372                metasenv subst context n lc ty_t
373             with NCicMetaSubst.Uncertain msg -> 
374                  pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
375                  raise (Uncertain msg)
376             | NCicMetaSubst.MetaSubstFailure msg -> 
377                  pp (lazy ("delift fails: " ^ Lazy.force msg));
378                  raise (UnificationFailure msg)
379           in
380            delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
381             subst 
382        | _ ->
383         let lty = NCicSubstitution.subst_meta status lc ty in
384         pp (lazy ("On the types: " ^
385           ppterm status ~metasenv ~subst ~context ty_t ^ "=<=" ^
386           ppterm status ~metasenv ~subst ~context lty)); 
387         let metasenv, subst = 
388           unify status false metasenv subst context ty_t lty false
389         in
390         delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv
391          subst)
392  (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
393
394 and unify status test_eq_only metasenv subst context t1 t2 swap =
395  (*D*) inside 'U'; try let rc =
396    let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) =
397     (*D*) inside 'F'; try let rc =  
398      pp (lazy("  " ^ ppterm status ~metasenv ~subst ~context t1 ^ 
399           (if swap then " ==>?== " 
400            else " ==<?==" ) ^ 
401          ppterm status ~metasenv ~subst ~context t2 ^ ppmetasenv status
402          ~subst metasenv));
403      pp (lazy("  " ^ ppterm status ~metasenv ~subst:[] ~context t1 ^
404           (if swap then " ==>??== " 
405            else " ==<??==" ) ^ 
406          ppterm status ~metasenv ~subst:[] ~context t2 ^ ppmetasenv status
407          ~subst metasenv));
408      if t1 === t2 then
409        metasenv, subst
410 (* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
411      else if
412       NCicUntrusted.metas_of_term subst context t1 = [] &&
413       NCicUntrusted.metas_of_term subst context t2 = []
414      then
415       if NCicReduction.are_convertible ~metasenv ~subst context t1 t2 then
416        metasenv,subst
417       else
418        raise (UnificationFailure (lazy "Closed terms not convertible"))
419 *)
420      else
421        match (t1,t2) with
422        | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl [] 
423        | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) -> 
424            prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
425            assert false 
426        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
427            let a, b = if swap then b,a else a,b in
428            if NCicEnvironment.universe_leq a b then metasenv, subst
429            else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
430        | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
431            if NCicEnvironment.universe_eq a b then metasenv, subst
432            else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
433        | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap -> 
434            if (not test_eq_only) then metasenv, subst
435            else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
436        | (C.Sort (C.Type _), C.Sort C.Prop) when swap -> 
437            if (not test_eq_only) then metasenv, subst
438            else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
439
440        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) 
441        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
442            let metasenv, subst = unify status true metasenv subst context s1 s2 swap in
443            unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
444        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
445            let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in
446            let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in
447            let context = (name1, C.Def (s1,ty1))::context in
448            unify status test_eq_only metasenv subst context t1 t2 swap
449
450        | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
451           (try 
452            let l1 = NCicUtils.expand_local_context l1 in
453            let l2 = NCicUtils.expand_local_context l2 in
454            let metasenv, subst, to_restrict, _ =
455             List.fold_right2 
456              (fun t1 t2 (metasenv, subst, to_restrict, i) -> 
457                 try 
458                   let metasenv, subst = 
459                    unify status (*test_eq_only*) true metasenv subst context
460                     (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2)
461                      swap
462                   in
463                   metasenv, subst, to_restrict, i-1  
464                 with UnificationFailure _ | Uncertain _ ->
465                   metasenv, subst, i::to_restrict, i-1)
466              l1 l2 (metasenv, subst, [], List.length l1)
467            in
468            if to_restrict <> [] then
469              let metasenv, subst, _, _ = 
470                NCicMetaSubst.restrict status metasenv subst n1 to_restrict
471              in
472                metasenv, subst
473            else metasenv, subst
474           with 
475            | Invalid_argument _ -> assert false
476            | NCicMetaSubst.MetaSubstFailure msg ->
477               try 
478                 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
479                 let term1 = NCicSubstitution.subst_meta status lc1 term in
480                 let term2 = NCicSubstitution.subst_meta status lc2 term in
481                   unify status test_eq_only metasenv subst context term1 term2 swap
482               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
483
484        |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
485           NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
486             (try
487               List.fold_left2 
488                 (fun (metasenv, subst) t1 t2 ->
489                   unify status (*test_eq_only*) true metasenv subst context t1 
490                     t2 swap)
491                 (metasenv,subst) l1 l2
492             with Invalid_argument _ -> 
493               raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)))
494        
495        | _, NCic.Meta (n, _) when is_locked n subst && not swap->
496            (let (metasenv, subst), i = 
497               match NCicReduction.whd status ~subst context t1 with
498               | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
499                  let metasenv, lambda_Mj =
500                    lambda_intros status metasenv subst context (List.length args)
501                     (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
502                  in
503                    unify status test_eq_only metasenv subst context 
504                     (C.Meta (i,l)) lambda_Mj false,
505                    i
506               | NCic.Meta (i,_) -> (metasenv, subst), i
507               | _ ->
508                  raise (UnificationFailure (lazy "Locked term vs non
509                   flexible term; probably not saturated enough yet!"))
510              in
511               let t1 = NCicReduction.whd status ~subst context t1 in
512               let j, lj = 
513                 match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
514               in
515               let metasenv, subst = 
516                 instantiate status test_eq_only metasenv subst context j lj t2 true
517               in
518               (* We need to remove the out_scope_tags to avoid propagation of
519                  them that triggers again the ad-hoc case *)
520               let subst =
521                List.map (fun (i,(tag,ctx,bo,ty)) ->
522                 let tag =
523                  List.filter
524                   (function `InScope | `OutScope _ -> false | _ -> true) tag
525                 in
526                   i,(tag,ctx,bo,ty)
527                 ) subst
528               in
529               (try
530                 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
531                 let term = eta_reduce status subst term in
532                 let subst = List.filter (fun (j,_) -> j <> i) subst in
533                 metasenv, ((i, (name, ctx, term, ty)) :: subst)
534               with Not_found -> assert false))
535        | NCic.Meta (n, _), _ when is_locked n subst && swap ->
536            unify status test_eq_only metasenv subst context t2 t1 false
537
538        | t, C.Meta (n,lc) when List.mem_assoc n subst -> 
539           let _,_,term,_ = NCicUtils.lookup_subst n subst in
540           let term = NCicSubstitution.subst_meta status lc term in
541             unify status test_eq_only metasenv subst context t term swap
542        | C.Meta (n,_), _ when List.mem_assoc n subst -> 
543             unify status test_eq_only metasenv subst context t2 t1 (not swap)
544
545        | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
546             let _,_,term,_ = NCicUtils.lookup_subst i subst in
547             let term = NCicSubstitution.subst_meta status l term in
548               unify status test_eq_only metasenv subst context t1 
549                 (mk_appl status ~upto:(List.length args) term args) swap
550        | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
551             unify status test_eq_only metasenv subst context t2 t1 (not swap)
552
553        | C.Meta (n,_), C.Meta (m,lc') when 
554            let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
555            let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
556             (n < m && cc1 = cc2) ||
557              let len1 = List.length cc1 in
558              let len2 = List.length cc2 in
559               len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
560           instantiate status test_eq_only metasenv subst context m lc'
561             (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
562        | C.Meta (n,lc), C.Meta (m,lc') when
563           let _,_,tyn = NCicUtils.lookup_meta n metasenv in
564           let _,_,tym = NCicUtils.lookup_meta m metasenv in
565           let tyn = NCicSubstitution.subst_meta status lc tyn in
566           let tym = NCicSubstitution.subst_meta status lc tym in
567            match tyn,tym with
568               NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
569                NCicEnvironment.universe_lt u1 u2
570             | _,_ -> false ->
571           instantiate status test_eq_only metasenv subst context m lc'
572             (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
573        | C.Meta (n,lc), t -> 
574           instantiate status test_eq_only metasenv subst context n lc 
575             (NCicReduction.head_beta_reduce status ~subst t) swap
576        | t, C.Meta (n,lc) -> 
577           instantiate status test_eq_only metasenv subst context n lc 
578            (NCicReduction.head_beta_reduce status ~subst t) (not swap)
579
580        (* higher order unification case *)
581        | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
582            (* this easy_case handles "(? ?) =?= (f a)", same number of 
583             * args, preferring the instantiation "f" over "\_.f a" for the
584             * metavariable in head position. Since the arguments of the meta
585             * are flexible, delift would ignore them generating a constant
586             * function even in the easy case above *)
587            let easy_case = 
588              match t2 with
589              | NCic.Appl (f :: f_args)
590                when 
591                List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
592                 let mlen = List.length args in
593                 let flen = List.length f_args in
594                 let min_len = min mlen flen in
595                 let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
596                 let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
597                  (try 
598                     Some (List.fold_left2 
599                       (fun (m, s) t1 t2 -> 
600                         unify status test_eq_only m s context t1 t2 swap
601                       ) (metasenv,subst)
602                         ((NCicUntrusted.mk_appl meta mhe)::margs)
603                         ((NCicUntrusted.mk_appl f fhe)::fargs))
604                   with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
605                     None) 
606              | _ -> None
607            in
608            (match easy_case with
609            | Some ms -> ms
610            | None ->
611                (* This case handles "(?_f ..ti..) =?= t2", abstracting every
612                 * non flexible ti (delift skips local context items that are
613                 * flexible) from t2 in two steps:
614                 *  1) ?_f := \..xi.. .?
615                 *  2) ?_f ..ti..  =?= t2 --unif_machines-->
616                       ?_f[..ti..] =?= t2 --instantiate-->
617                       delift [..ti..] t2 *)
618                let metasenv, lambda_Mj =
619                  lambda_intros status metasenv subst context (List.length args)
620                   (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
621                in
622                let metasenv, subst = 
623                  unify status test_eq_only metasenv subst context 
624                    (C.Meta (i,l)) lambda_Mj swap
625                in
626                let metasenv, subst = 
627                  unify status test_eq_only metasenv subst context t1 t2 swap
628                in
629                (try
630                  let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
631                  let term = eta_reduce status subst term in
632                  let subst = List.filter (fun (j,_) -> j <> i) subst in
633                  metasenv, ((i, (name, ctx, term, ty)) :: subst)
634                with Not_found -> assert false))
635
636        | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
637            unify status test_eq_only metasenv subst context t2 t1 (not swap)
638
639        (* processing this case here we avoid a useless small delta step *)
640        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) 
641          when Ref.eq r1 r2 ->
642            let relevance = NCicEnvironment.get_relevance status r1 in
643            let metasenv, subst, _ = 
644              try
645                List.fold_left2 
646                  (fun (metasenv, subst, relevance) t1 t2 ->
647                     let b, relevance = 
648                       match relevance with b::tl -> b,tl | _ -> true, [] in
649                     let metasenv, subst = 
650                       try unify status test_eq_only metasenv subst context t1 t2
651                             swap
652                       with UnificationFailure _ | Uncertain _ when not b ->
653                         metasenv, subst
654                     in
655                       metasenv, subst, relevance)
656                  (metasenv, subst, relevance) tl1 tl2
657              with
658                 Invalid_argument _ -> 
659                  raise (Uncertain (mk_msg status metasenv subst context t1 t2))
660               | KeepReducing _ | KeepReducingThis _ -> assert false
661            in 
662              metasenv, subst
663
664        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
665           C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
666            let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
667            let _,_,ty,_ = List.nth itl tyno in
668            let rec remove_prods ~subst context ty = 
669              let ty = NCicReduction.whd status ~subst context ty in
670              match ty with
671              | C.Sort _ -> ty
672              | C.Prod (name,so,ta) -> 
673                    remove_prods ~subst ((name,(C.Decl so))::context) ta
674              | _ -> assert false
675            in
676            let is_prop = 
677              match remove_prods ~subst [] ty with
678              | C.Sort C.Prop -> true
679              | _ -> false 
680            in
681            (* if not (Ref.eq ref1 ref2) then 
682              raise (Uncertain (mk_msg status metasenv subst context t1 t2))
683            else*)
684              let metasenv, subst = 
685               unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
686              let metasenv, subst = 
687                try unify status test_eq_only metasenv subst context term1 term2 swap
688                with UnificationFailure _ | Uncertain _ when is_prop -> 
689                  metasenv, subst
690              in
691              (try
692               List.fold_left2 
693                (fun (metasenv,subst) t1 t2 -> 
694                   unify status test_eq_only metasenv subst context t1 t2 swap)
695                (metasenv, subst) pl1 pl2
696              with Invalid_argument _ -> assert false)
697        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
698        | _ when norm1 && norm2 ->
699            if (could_reduce t1 || could_reduce t2) then
700             raise (Uncertain (mk_msg status metasenv subst context t1 t2))
701            else
702             raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
703        | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
704      (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
705     in
706     let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
707      try fo_unif test_eq_only metasenv subst nt1 nt2
708      with
709       UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
710        raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
711     in
712     let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
713       if NCicUntrusted.metas_of_term status subst context t1 = [] &&
714          NCicUntrusted.metas_of_term status subst context t2 = [] 
715       then None 
716       else begin
717     (*D*) inside 'H'; try let rc =  
718      pp(lazy ("\nProblema:\n" ^
719         ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
720         ppterm status ~metasenv ~subst ~context t2));
721       let candidates = 
722         NCicUnifHint.look_for_hint status metasenv subst context t1 t2
723       in
724       let rec cand_iter = function
725         | [] -> None (* raise exc *)
726         | (metasenv,(c1,c2),premises)::tl -> 
727             pp (lazy ("\nProvo il candidato:\n" ^ 
728               String.concat "\n"
729                 (List.map 
730                   (fun (a,b) ->
731                    ppterm status ~metasenv ~subst ~context a ^  " =?= " ^
732                    ppterm status ~metasenv ~subst ~context b) premises) ^
733               "\n-------------------------------------------\n"^
734               ppterm status ~metasenv ~subst ~context c1 ^  " = " ^
735               ppterm status ~metasenv ~subst ~context c2));
736             try 
737     (*D*) inside 'K'; try let rc =  
738               let metasenv,subst = 
739                 fo_unif test_eq_only metasenv subst mt1 (false,c1) in
740               let metasenv,subst = 
741                 fo_unif test_eq_only metasenv subst (false,c2) mt2 in
742               let metasenv,subst = 
743                 List.fold_left 
744                   (fun (metasenv, subst) (x,y) ->
745                      unify status test_eq_only metasenv subst context x y false)
746                   (metasenv, subst) (List.rev premises)
747               in
748               pp(lazy("FUNZIONA!"));
749               Some (metasenv, subst)
750      (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
751             with
752              KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
753            | KeepReducingThis _ -> assert false
754       in
755         cand_iter candidates
756      (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
757       end
758     in
759     let put_in_whd m1 m2 =
760       NCicReduction.reduce_machine status ~delta:max_int ~subst context m1,
761       NCicReduction.reduce_machine status ~delta:max_int ~subst context m2
762     in
763     let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
764       try fo_unif test_eq_only metasenv subst m1 m2
765       with 
766       | UnificationFailure _ as exn -> raise exn
767       | KeepReducing _ | Uncertain _ as exn ->
768         let (t1,norm1 as tm1),(t2,norm2 as tm2) =
769          put_in_whd (0,[],t1,[]) (0,[],t2,[])
770         in
771          match 
772            try_hints metasenv subst 
773             (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
774          with
775           | Some x -> x
776           | None -> 
777               match exn with 
778               | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
779               | Uncertain _ as exn -> raise exn
780               | _ -> assert false
781     in
782     let fo_unif_heads_and_cont_or_unwind_and_hints 
783       test_eq_only metasenv subst m1 m2 cont hm1 hm2
784      =
785       let ms, continuation = 
786         (* calling the continuation inside the outermost try is an option
787            and makes unification stronger, but looks not frequent to me
788            that heads unify but not the arguments and that an hints can fix 
789            that *)
790         try fo_unif test_eq_only metasenv subst m1 m2, cont
791         with 
792         | UnificationFailure _ 
793         | KeepReducing _ | Uncertain _ as exn ->
794            let (t1,norm1),(t2,norm2) = hm1, hm2 in
795            match 
796              try_hints metasenv subst 
797               (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
798            with
799             | Some x -> x, fun x -> x
800             | None -> 
801                 match exn with 
802                 | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
803                 | UnificationFailure _ | Uncertain _ as exn -> raise exn
804                 | _ -> assert false
805       in
806         continuation ms
807     in
808     let height_of = function
809      | NCic.Const (Ref.Ref (_,Ref.Def h)) 
810      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) 
811      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) 
812      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
813      | _ -> 0
814     in
815     let small_delta_step ~subst  
816       ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
817     =
818      assert (not (norm1 && norm2));
819      if norm1 then
820       x1,NCicReduction.reduce_machine status ~delta:0 ~subst context m2
821      else if norm2 then
822       NCicReduction.reduce_machine status ~delta:0 ~subst context m1,x2
823      else 
824       let h1 = height_of t1 in 
825       let h2 = height_of t2 in
826       let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
827       NCicReduction.reduce_machine status ~delta ~subst context m1,
828       NCicReduction.reduce_machine status ~delta ~subst context m2
829     in
830     let rec unif_machines metasenv subst = 
831       function
832       | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
833      (*D*) inside 'M'; try let rc = 
834          pp (lazy("UM: " ^
835            ppterm status ~metasenv ~subst ~context 
836              (NCicReduction.unwind status (k1,e1,t1,s1)) ^
837            " === " ^ 
838            ppterm status ~metasenv ~subst ~context 
839              (NCicReduction.unwind status (k2,e2,t2,s2))));
840          pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
841           let relevance =
842             match t1 with
843             | C.Const r -> NCicEnvironment.get_relevance status r
844             | _ -> [] in
845           let unif_from_stack (metasenv, subst) (t1, t2, b) =
846               try
847                 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
848                 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
849                 unif_machines metasenv subst (put_in_whd t1 t2)
850               with UnificationFailure _ | Uncertain _ when not b ->
851                 metasenv, subst
852           in
853           let rec check_stack l1 l2 r todo =
854             match l1,l2,r with
855             | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
856             | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
857             | l1, l2, _ ->
858                NCicReduction.unwind status (k1,e1,t1,List.rev l1),
859                 NCicReduction.unwind status (k2,e2,t2,List.rev l2),
860                 todo
861           in
862           let check_stack l1 l2 r =
863             match t1, t2 with
864             | NCic.Meta _, _ | _, NCic.Meta _ ->
865                 (NCicReduction.unwind status (k1,e1,t1,s1)),
866                 (NCicReduction.unwind status (k2,e2,t2,s2)),[]
867             | _ -> check_stack l1 l2 r []
868           in
869         let hh1,hh2,todo =
870           check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
871         try
872           fo_unif_heads_and_cont_or_unwind_and_hints
873             test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) 
874             (fun ms -> List.fold_left unif_from_stack ms todo)
875             m1 m2
876         with
877          | KeepReducing _ -> assert false
878          | KeepReducingThis _ ->
879             assert (not (norm1 && norm2));
880             unif_machines metasenv subst (small_delta_step ~subst m1 m2)
881          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
882            -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
883          | UnificationFailure msg
884            when could_reduce (NCicReduction.unwind status (fst m1))
885              || could_reduce (NCicReduction.unwind status (fst m2))
886            -> raise (Uncertain msg)
887       (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
888      in
889      try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
890      with
891       | KeepReducingThis (msg,tm1,tm2) ->
892          (try 
893            unif_machines metasenv subst (tm1,tm2)
894           with 
895           | UnificationFailure _ -> raise (UnificationFailure msg)
896           | Uncertain _ -> raise (Uncertain msg)
897           | KeepReducing _ -> assert false)
898       | KeepReducing _ -> assert false
899
900  (*D*)  in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn 
901
902 and delift_type_wrt_terms status metasenv subst context t args =
903   let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
904   let (metasenv, subst), t =
905    try
906     NCicMetaSubst.delift status
907       ~unify:(fun m s c t1 t2 -> 
908          let ind = !indent in
909          let res = 
910            try Some (unify status false m s c t1 t2 false)
911            with UnificationFailure _ | Uncertain _ -> None
912          in
913          indent := ind; res)
914       metasenv subst context 0 (0,NCic.Ctx lc) t
915    with
916       NCicMetaSubst.MetaSubstFailure _
917     | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
918   in
919    metasenv, subst, t
920 ;;
921
922
923 let unify status ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2= 
924   indent := "";      
925   unify status test_eq_only metasenv subst context t1 t2 swap;;
926
927 let fix_sorts status m s =
928   fix status m s true false (UnificationFailure (lazy "no sup"))
929 ;;