helm/software/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
  18 let (===) x y = Pervasives.compare x y = 0 ;;
  19
  20 let uncert_exc metasenv subst context t1 t2 =
  21   Uncertain (lazy (
  22   "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
  23   " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
  24 ;;
  25
  26 let fail_exc metasenv subst context t1 t2 =
  27   UnificationFailure (lazy (
  28   "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
  29   " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2));
  30 ;;
  31
  32 let mk_appl ~upto hd tl =
  33   NCicReduction.head_beta_reduce ~upto
  34     (match hd with
  35     | NCic.Appl l -> NCic.Appl (l@tl)
  36     | _ -> NCic.Appl (hd :: tl))
  37 ;;
  38
  39 let flexible l =
  40   List.exists
  41     (function
  42        | NCic.Meta _
  43        | NCic.Appl (NCic.Meta _::_) -> true
  44        | _ -> false) l
  45 ;;
  46
  47 exception WrongShape;;
  48
  49 let eta_reduce =
  50   let delift_if_not_occur body orig =
  51     try
  52         NCicSubstitution.psubst ~avoid_beta_redexes:true
  53           (fun () -> raise WrongShape) [()] body
  54     with WrongShape -> orig
  55   in
  56   function
  57   | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
  58       delift_if_not_occur hd orig
  59   | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig
  60     when HExtlib.list_last l = NCic.Rel 1 ->
  61        let body =
  62          let args, _ = HExtlib.split_nth (List.length l - 1) l in
  63          NCic.Appl (hd::args)
  64        in
  65        delift_if_not_occur body orig
  66   | t -> t
  67 ;;
  68
  69 module C = NCic;;
  70 module Ref = NReference;;
  71
  72 let indent = ref "";;
  73 let inside c = indent := !indent ^ String.make 1 c;;
  74 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
  75
  76 let pp s =
  77   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
  78 ;;
  79
  80 let pp _ = ();;
  81
  82 let fix_sorts swap metasenv subst context meta t =
  83   let rec aux () = function
  84     | NCic.Sort (NCic.Type u) as orig ->
  85         if swap then
  86          match NCicEnvironment.sup u with
  87          | None -> prerr_endline "no sup for" ;
  88             raise (fail_exc metasenv subst context meta t)
  89          | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
  90         else
  91          NCic.Sort (NCic.Type (
  92            match NCicEnvironment.sup NCicEnvironment.type0 with
  93            | Some x -> x
  94            | _ -> assert false))
  95     | NCic.Meta _ as orig -> orig
  96     | t -> NCicUtils.map (fun _ _ -> ()) () aux t
  97   in
  98     aux () t
  99 ;;
 100
 101 let rec beta_expand hdb num test_eq_only swap metasenv subst context t arg =
 102   let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
 103    try
 104     let metasenv, subst =
 105      if swap then
 106       unify hdb test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
 107      else
 108       unify hdb test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
 109     in
 110      (metasenv, subst), NCic.Rel (1 + n)
 111    with Uncertain _ | UnificationFailure _ ->
 112        match t' with
 113        | NCic.Rel m as orig ->
 114            (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
 115        (* andrea: in general, beta_expand can create badly typed
 116         terms. This happens quite seldom in practice, UNLESS we
 117         iterate on the local context. For this reason, we renounce
 118         to iterate and just lift *)
 119        | NCic.Meta (i,(shift,lc)) ->
 120            (metasenv,subst), NCic.Meta (i,(shift+1,lc))
 121        | NCic.Prod (name, src, tgt) as orig ->
 122            let (metasenv, subst), src1 = aux (n,context,true) acc src in
 123            let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
 124            let ms, tgt1 = aux k (metasenv, subst) tgt in
 125            if src == src1 && tgt == tgt1 then ms, orig else
 126            ms, NCic.Prod (name, src1, tgt1)
 127        | t ->
 128            NCicUntrusted.map_term_fold_a
 129              (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
 130
 131   in
 132   let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
 133   let fresh_name = "Hbeta" ^ string_of_int num in
 134   let (metasenv,subst), t1 =
 135     aux (0, context, test_eq_only) (metasenv, subst) t in
 136   let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
 137   try
 138     ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
 139     metasenv, subst, t2
 140   with NCicTypeChecker.TypeCheckerFailure _ ->
 141     metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
 142
 143 and beta_expand_many hdb test_equality_only swap metasenv subst context t args =
 144 (* (*D*)  inside 'B'; try let rc = *)
 145   pp (lazy (String.concat ", "
 146      (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
 147      args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
 148   let _, subst, metasenv, hd =
 149     List.fold_right
 150       (fun arg (num,subst,metasenv,t) ->
 151          let metasenv, subst, t =
 152            beta_expand hdb num test_equality_only swap metasenv subst context t arg
 153          in
 154            num+1,subst,metasenv,t)
 155       args (1,subst,metasenv,t)
 156   in
 157   pp (lazy ("Head syntesized by b-exp: " ^
 158     NCicPp.ppterm ~metasenv ~subst ~context hd));
 159     metasenv, subst, hd
 160 (* (*D*)  in outside (); rc with exn -> outside (); raise exn *)
 161
 162 and instantiate hdb test_eq_only metasenv subst context n lc t swap =
 163  (*D*)  inside 'I'; try let rc =
 164          pp (lazy(string_of_int n ^ " :=?= "^
 165            NCicPp.ppterm ~metasenv ~subst ~context t));
 166   let unify test_eq_only m s c t1 t2 =
 167     if swap then unify hdb test_eq_only m s c t2 t1
 168     else unify hdb test_eq_only m s c t1 t2
 169   in
 170   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
 171   let metasenv, subst, t =
 172     match ty with
 173     | NCic.Implicit (`Typeof _) ->
 174        metasenv,subst, t
 175          (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
 176     | _ ->
 177        pp (lazy (
 178          "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
 179           NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
 180           NCicPp.ppmetasenv ~subst metasenv));
 181        let t, ty_t =
 182          try t, NCicTypeChecker.typeof ~subst ~metasenv context t
 183          with
 184          | NCicTypeChecker.AssertFailure msg ->
 185            (pp (lazy "fine typeof (fallimento)");
 186            let ft=fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t in
 187            if ft == t then
 188              (prerr_endline ( ("ILLTYPED: " ^
 189                 NCicPp.ppterm ~metasenv ~subst ~context t
 190             ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
 191             NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
 192             NCicPp.ppmetasenv ~subst metasenv
 193             ));
 194                      assert false)
 195            else
 196             try
 197               pp (lazy ("typeof: " ^
 198                 NCicPp.ppterm ~metasenv ~subst ~context ft));
 199               ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
 200             with NCicTypeChecker.AssertFailure _ ->
 201               assert false)
 202          | NCicTypeChecker.TypeCheckerFailure msg ->
 203               prerr_endline (Lazy.force msg);
 204               pp msg; assert false
 205        in
 206        let lty = NCicSubstitution.subst_meta lc ty in
 207        pp (lazy ("On the types: " ^
 208         NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
 209         NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
 210          ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
 211        let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
 212        metasenv, subst, t
 213   in
 214          pp (lazy(string_of_int n ^ " := 111 = "^
 215            NCicPp.ppterm ~metasenv ~subst ~context t));
 216   let (metasenv, subst), t =
 217     try NCicMetaSubst.delift metasenv subst context n lc t
 218     with NCicMetaSubst.Uncertain msg ->
 219          pp (lazy ("delift fails: " ^ Lazy.force msg));
 220          raise (Uncertain msg)
 221     | NCicMetaSubst.MetaSubstFailure msg ->
 222          pp (lazy ("delift fails: " ^ Lazy.force msg));
 223          raise (UnificationFailure msg)
 224   in
 225          pp (lazy(string_of_int n ^ " := 222 = "^
 226            NCicPp.ppterm ~metasenv ~subst ~context:ctx t
 227          ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv));
 228   (* Unifying the types may have already instantiated n. *)
 229   try
 230     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
 231     let oldt = NCicSubstitution.subst_meta lc oldt in
 232     let t = NCicSubstitution.subst_meta lc t in
 233     (* conjecture: always fail --> occur check *)
 234     unify test_eq_only metasenv subst context oldt t
 235   with NCicUtils.Subst_not_found _ ->
 236     (* by cumulativity when unify(?,Type_i)
 237      * we could ? := Type_j with j <= i... *)
 238     let subst = (n, (name, ctx, t, ty)) :: subst in
 239     pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
 240       ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
 241     let metasenv =
 242       List.filter (fun (m,_) -> not (n = m)) metasenv
 243     in
 244     metasenv, subst
 245  (*D*)  in outside(); rc with exn -> outside (); raise exn
 246
 247 and unify hdb test_eq_only metasenv subst context t1 t2 =
 248  (*D*) inside 'U'; try let rc =
 249    let fo_unif test_eq_only metasenv subst t1 t2 =
 250     (*D*) inside 'F'; try let rc =
 251      pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
 252          NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ NCicPp.ppmetasenv
 253          ~subst metasenv));
 254      if t1 === t2 then
 255        metasenv, subst
 256      else
 257        match (t1,t2) with
 258        | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
 259        | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
 260            prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
 261            assert false
 262        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
 263            if NCicEnvironment.universe_leq a b then metasenv, subst
 264            else raise (fail_exc metasenv subst context t1 t2)
 265        | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
 266            if NCicEnvironment.universe_eq a b then metasenv, subst
 267            else raise (fail_exc metasenv subst context t1 t2)
 268        | (C.Sort C.Prop,C.Sort (C.Type _)) ->
 269            if (not test_eq_only) then metasenv, subst
 270            else raise (fail_exc metasenv subst context t1 t2)
 271
 272        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
 273        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 274            let metasenv, subst = unify hdb true metasenv subst context s1 s2 in
 275            unify hdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
 276        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
 277            let metasenv,subst=unify hdb test_eq_only metasenv subst context ty1 ty2 in
 278            let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in
 279            let context = (name1, C.Def (s1,ty1))::context in
 280            unify hdb test_eq_only metasenv subst context t1 t2
 281
 282        | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
 283           (try
 284            let l1 = NCicUtils.expand_local_context l1 in
 285            let l2 = NCicUtils.expand_local_context l2 in
 286            let metasenv, subst, to_restrict, _ =
 287             List.fold_right2
 288              (fun t1 t2 (metasenv, subst, to_restrict, i) ->
 289                 try
 290                   let metasenv, subst =
 291                    unify hdb test_eq_only metasenv subst context
 292                     (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
 293                   in
 294                   metasenv, subst, to_restrict, i-1
 295                 with UnificationFailure _ | Uncertain _ ->
 296                   metasenv, subst, i::to_restrict, i-1)
 297              l1 l2 (metasenv, subst, [], List.length l1)
 298            in
 299            if to_restrict <> [] then
 300              let metasenv, subst, _ =
 301                NCicMetaSubst.restrict metasenv subst n1 to_restrict
 302              in
 303                metasenv, subst
 304            else metasenv, subst
 305           with
 306            | Invalid_argument _ -> assert false
 307            | NCicMetaSubst.MetaSubstFailure msg ->
 308               try
 309                 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
 310                 let term1 = NCicSubstitution.subst_meta lc1 term in
 311                 let term2 = NCicSubstitution.subst_meta lc2 term in
 312                   unify hdb test_eq_only metasenv subst context term1 term2
 313               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
 314
 315        | C.Meta (n,lc), t ->
 316            (try
 317              let _,_,term,_ = NCicUtils.lookup_subst n subst in
 318              let term = NCicSubstitution.subst_meta lc term in
 319                unify hdb test_eq_only metasenv subst context term t
 320            with NCicUtils.Subst_not_found _->
 321              instantiate hdb test_eq_only metasenv subst context n lc
 322                (NCicReduction.head_beta_reduce ~subst t) false)
 323
 324        | t, C.Meta (n,lc) ->
 325            (try
 326              let _,_,term,_ = NCicUtils.lookup_subst n subst in
 327              let term = NCicSubstitution.subst_meta lc term in
 328                unify hdb test_eq_only metasenv subst context t term
 329            with NCicUtils.Subst_not_found _->
 330              instantiate hdb test_eq_only metasenv subst context n lc
 331               (NCicReduction.head_beta_reduce ~subst t) true)
 332
 333        | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
 334             let _,_,term,_ = NCicUtils.lookup_subst i subst in
 335             let term = NCicSubstitution.subst_meta l term in
 336               unify hdb test_eq_only metasenv subst context
 337                 (mk_appl ~upto:(List.length args) term args) t2
 338
 339        | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
 340             let _,_,term,_ = NCicUtils.lookup_subst i subst in
 341             let term = NCicSubstitution.subst_meta l term in
 342               unify hdb test_eq_only metasenv subst context t1
 343                 (mk_appl ~upto:(List.length args) term args)
 344
 345        |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
 346           NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
 347             (try
 348               List.fold_left2
 349                 (fun (metasenv, subst) t1 t2 ->
 350                   unify hdb test_eq_only metasenv subst context t1 t2)
 351                 (metasenv,subst) l1 l2
 352             with Invalid_argument _ ->
 353               raise (fail_exc metasenv subst context t1 t2))
 354
 355        | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
 356            (* we verify that none of the args is a Meta,
 357               since beta expanding w.r.t a metavariable makes no sense  *)
 358               let metasenv, subst, beta_expanded =
 359                 beta_expand_many hdb
 360                   test_eq_only false
 361                   metasenv subst context t2 args
 362               in
 363                 unify hdb test_eq_only metasenv subst context
 364                   (C.Meta (i,l)) beta_expanded
 365
 366        | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
 367               let metasenv, subst, beta_expanded =
 368                 beta_expand_many hdb
 369                   test_eq_only true
 370                   metasenv subst context t1 args
 371               in
 372                 unify hdb test_eq_only metasenv subst context
 373                   beta_expanded (C.Meta (i,l))
 374
 375        (* processing this case here we avoid a useless small delta step *)
 376        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
 377          when Ref.eq r1 r2 ->
 378            let relevance = NCicEnvironment.get_relevance r1 in
 379            let relevance = match r1 with
 380              | Ref.Ref (_,Ref.Con (_,_,lno)) ->
 381                  let _,relevance = HExtlib.split_nth lno relevance in
 382                    HExtlib.mk_list false lno @ relevance
 383              | _ -> relevance
 384            in
 385            let metasenv, subst, _ =
 386              try
 387                List.fold_left2
 388                  (fun (metasenv, subst, relevance) t1 t2 ->
 389                     let b, relevance =
 390                       match relevance with b::tl -> b,tl | _ -> true, [] in
 391                     let metasenv, subst =
 392                       try unify hdb test_eq_only metasenv subst context t1 t2
 393                       with UnificationFailure _ | Uncertain _ when not b ->
 394                         metasenv, subst
 395                     in
 396                       metasenv, subst, relevance)
 397                  (metasenv, subst, relevance) tl1 tl2
 398              with Invalid_argument _ ->
 399                raise (uncert_exc metasenv subst context t1 t2)
 400            in
 401              metasenv, subst
 402
 403        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
 404           C.Match (ref2,outtype2,term2,pl2)) ->
 405            let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
 406            let _,_,ty,_ = List.nth itl tyno in
 407            let rec remove_prods ~subst context ty =
 408              let ty = NCicReduction.whd ~subst context ty in
 409              match ty with
 410              | C.Sort _ -> ty
 411              | C.Prod (name,so,ta) ->
 412                    remove_prods ~subst ((name,(C.Decl so))::context) ta
 413              | _ -> assert false
 414            in
 415            let is_prop =
 416              match remove_prods ~subst [] ty with
 417              | C.Sort C.Prop -> true
 418              | _ -> false
 419            in
 420            if not (Ref.eq ref1 ref2) then
 421              raise (uncert_exc metasenv subst context t1 t2)
 422            else
 423              let metasenv, subst =
 424               unify hdb test_eq_only metasenv subst context outtype1 outtype2 in
 425              let metasenv, subst =
 426                try unify hdb test_eq_only metasenv subst context term1 term2
 427                with UnificationFailure _ | Uncertain _ when is_prop ->
 428                  metasenv, subst
 429              in
 430              (try
 431               List.fold_left2
 432                (fun (metasenv,subst) ->
 433                   unify hdb test_eq_only metasenv subst context)
 434                (metasenv, subst) pl1 pl2
 435              with Invalid_argument _ ->
 436                raise (uncert_exc metasenv subst context t1 t2))
 437        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
 438        | _ when NCicUntrusted.metas_of_term subst context t1 = [] &&
 439                 NCicUntrusted.metas_of_term subst context t2 = [] ->
 440                   raise (fail_exc metasenv subst context t1 t2)
 441        | _ -> raise (uncert_exc metasenv subst context t1 t2)
 442      (*D*)  in outside(); rc with exn -> outside (); raise exn
 443     in
 444     let try_hints metasenv subst t1 t2 (* exc*) =
 445 (*
 446             prerr_endline ("\n\n\n looking for hints for : " ^
 447               NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
 448               NCicPp.ppterm ~metasenv ~subst ~context t2);
 449 *)
 450       let candidates =
 451         NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
 452       in
 453       let rec cand_iter = function
 454         | [] -> None (* raise exc *)
 455         | (metasenv,(c1,c2),premises)::tl ->
 456 (*
 457             prerr_endline ("\n attempt: " ^
 458               NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
 459               NCicPp.ppterm ~metasenv ~subst ~context c1 ^  " AND " ^
 460               NCicPp.ppterm ~metasenv ~subst ~context c2 ^  " ==?== " ^
 461               NCicPp.ppterm ~metasenv ~subst ~context t2);
 462 *)
 463             try
 464               let metasenv,subst =
 465                 fo_unif test_eq_only metasenv subst t1 c1 in
 466               let metasenv,subst =
 467                 fo_unif test_eq_only metasenv subst c2 t2 in
 468               let metasenv,subst =
 469                 List.fold_left
 470                   (fun (metasenv, subst) (x,y) ->
 471                      unify hdb test_eq_only metasenv subst context x y)
 472                   (metasenv, subst) premises
 473               in
 474               Some (metasenv, subst)
 475             with
 476               UnificationFailure _ | Uncertain _ ->
 477                 prerr_endline (" <candidate fails");
 478                 cand_iter tl
 479       in
 480         cand_iter candidates
 481     in
 482     let height_of = function
 483      | NCic.Const (Ref.Ref (_,Ref.Def h))
 484      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
 485      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
 486      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
 487      | _ -> 0
 488     in
 489     let put_in_whd m1 m2 =
 490       NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
 491       NCicReduction.reduce_machine ~delta:max_int ~subst context m2
 492     in
 493     let small_delta_step ~subst
 494       ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
 495     =
 496      assert (not (norm1 && norm2));
 497      if norm1 then
 498       x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
 499      else if norm2 then
 500       NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
 501      else
 502       let h1 = height_of t1 in
 503       let h2 = height_of t2 in
 504       let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
 505       NCicReduction.reduce_machine ~delta ~subst context m1,
 506       NCicReduction.reduce_machine ~delta ~subst context m2
 507     in
 508     let rec unif_machines metasenv subst =
 509       function
 510       | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
 511      (*D*) inside 'M'; try let rc =
 512          pp (lazy("UM: " ^
 513            NCicPp.ppterm ~metasenv ~subst ~context
 514              (NCicReduction.unwind (k1,e1,t1,s1)) ^
 515            " === " ^
 516            NCicPp.ppterm ~metasenv ~subst ~context
 517              (NCicReduction.unwind (k2,e2,t2,s2))));
 518 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
 519           let relevance = [] (* TO BE UNDERSTOOD
 520             match t1 with
 521             | C.Const r -> NCicEnvironment.get_relevance r
 522             | _ -> [] *) in
 523           let unif_from_stack t1 t2 b metasenv subst =
 524               try
 525                 let t1 = NCicReduction.from_stack t1 in
 526                 let t2 = NCicReduction.from_stack t2 in
 527                 unif_machines metasenv subst (put_in_whd t1 t2)
 528               with UnificationFailure _ | Uncertain _ when not b ->
 529                 metasenv, subst
 530           in
 531           let rec check_stack l1 l2 r todo =
 532             match l1,l2,r with
 533             | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
 534             | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
 535             | l1, l2, _ ->
 536                NCicReduction.unwind (k1,e1,t1,List.rev l1),
 537                 NCicReduction.unwind (k2,e2,t2,List.rev l2),
 538                 todo
 539           in
 540         let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
 541         try
 542          let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in
 543          List.fold_left
 544           (fun (metasenv,subst) (x1,x2,r) ->
 545             unif_from_stack x1 x2 r metasenv subst
 546           ) (metasenv,subst) todo
 547         with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
 548             unif_machines metasenv subst (small_delta_step ~subst m1 m2)
 549       (*D*)  in outside(); rc with exn -> outside (); raise exn
 550      in
 551      try fo_unif test_eq_only metasenv subst t1 t2
 552      with
 553      | UnificationFailure msg as exn ->
 554           (try
 555             unif_machines metasenv subst
 556              (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
 557           with
 558           | UnificationFailure _ -> raise (UnificationFailure msg)
 559           | Uncertain _ -> raise exn)
 560      | Uncertain msg as exn ->
 561        match try_hints metasenv subst t1 t2 with
 562        | Some x -> x
 563        | None ->
 564           try
 565             unif_machines metasenv subst
 566              (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
 567           with
 568           | UnificationFailure _ -> raise (UnificationFailure msg)
 569           | Uncertain _ -> raise exn
 570  (*D*)  in outside(); rc with exn -> outside (); raise exn
 571 ;;
 572
 573 let unify hdb =
 574   indent := "";
 575   unify hdb false;;
 576
 577