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