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 fo_unif test_eq_only metasenv subst t1 t2 =
 251     (*D*) inside 'F'; try let rc =
 252      pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
 253          NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ NCicPp.ppmetasenv
 254          ~subst metasenv));
 255      if t1 === t2 then
 256        metasenv, subst
 257      else
 258        match (t1,t2) with
 259        | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
 260        | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
 261            prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
 262            assert false
 263        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
 264            if NCicEnvironment.universe_leq a b then metasenv, subst
 265            else raise (fail_exc metasenv subst context t1 t2)
 266        | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
 267            if NCicEnvironment.universe_eq a b then metasenv, subst
 268            else raise (fail_exc metasenv subst context t1 t2)
 269        | (C.Sort C.Prop,C.Sort (C.Type _)) ->
 270            if (not test_eq_only) then metasenv, subst
 271            else raise (fail_exc metasenv subst context t1 t2)
 272
 273        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
 274        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 275            let metasenv, subst = unify hdb true metasenv subst context s1 s2 in
 276            unify hdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
 277        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
 278            let metasenv,subst=unify hdb test_eq_only metasenv subst context ty1 ty2 in
 279            let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in
 280            let context = (name1, C.Def (s1,ty1))::context in
 281            unify hdb test_eq_only metasenv subst context t1 t2
 282
 283        | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
 284           (try
 285            let l1 = NCicUtils.expand_local_context l1 in
 286            let l2 = NCicUtils.expand_local_context l2 in
 287            let metasenv, subst, to_restrict, _ =
 288             List.fold_right2
 289              (fun t1 t2 (metasenv, subst, to_restrict, i) ->
 290                 try
 291                   let metasenv, subst =
 292                    unify hdb test_eq_only metasenv subst context
 293                     (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
 294                   in
 295                   metasenv, subst, to_restrict, i-1
 296                 with UnificationFailure _ | Uncertain _ ->
 297                   metasenv, subst, i::to_restrict, i-1)
 298              l1 l2 (metasenv, subst, [], List.length l1)
 299            in
 300            if to_restrict <> [] then
 301              let metasenv, subst, _ =
 302                NCicMetaSubst.restrict metasenv subst n1 to_restrict
 303              in
 304                metasenv, subst
 305            else metasenv, subst
 306           with
 307            | Invalid_argument _ -> assert false
 308            | NCicMetaSubst.MetaSubstFailure msg ->
 309               try
 310                 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
 311                 let term1 = NCicSubstitution.subst_meta lc1 term in
 312                 let term2 = NCicSubstitution.subst_meta lc2 term in
 313                   unify hdb test_eq_only metasenv subst context term1 term2
 314               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
 315
 316        | C.Meta (n,lc), t ->
 317            (try
 318              let _,_,term,_ = NCicUtils.lookup_subst n subst in
 319              let term = NCicSubstitution.subst_meta lc term in
 320                unify hdb test_eq_only metasenv subst context term t
 321            with NCicUtils.Subst_not_found _->
 322              instantiate hdb test_eq_only metasenv subst context n lc 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 t true)
 331
 332        | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
 333             let _,_,term,_ = NCicUtils.lookup_subst i subst in
 334             let term = NCicSubstitution.subst_meta l term in
 335               unify hdb test_eq_only metasenv subst context (mk_appl term args) t2
 336
 337        | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
 338             let _,_,term,_ = NCicUtils.lookup_subst i subst in
 339             let term = NCicSubstitution.subst_meta l term in
 340               unify hdb test_eq_only metasenv subst context t1 (mk_appl term args)
 341
 342        |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
 343           NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
 344             (try
 345               List.fold_left2
 346                 (fun (metasenv, subst) t1 t2 ->
 347                   unify hdb test_eq_only metasenv subst context t1 t2)
 348                 (metasenv,subst) l1 l2
 349             with Invalid_argument _ ->
 350               raise (fail_exc metasenv subst context t1 t2))
 351
 352        | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
 353            (* we verify that none of the args is a Meta,
 354               since beta expanding w.r.t a metavariable makes no sense  *)
 355               let metasenv, subst, beta_expanded =
 356                 beta_expand_many hdb
 357                   test_eq_only false
 358                   metasenv subst context t2 args
 359               in
 360                 unify hdb test_eq_only metasenv subst context
 361                   (C.Meta (i,l)) beta_expanded
 362
 363        | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
 364               let metasenv, subst, beta_expanded =
 365                 beta_expand_many hdb
 366                   test_eq_only true
 367                   metasenv subst context t1 args
 368               in
 369                 unify hdb test_eq_only metasenv subst context
 370                   beta_expanded (C.Meta (i,l))
 371
 372        (* processing this case here we avoid a useless small delta step *)
 373        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
 374          when Ref.eq r1 r2 ->
 375            let relevance = NCicEnvironment.get_relevance r1 in
 376            let relevance = match r1 with
 377              | Ref.Ref (_,Ref.Con (_,_,lno)) ->
 378                  let _,relevance = HExtlib.split_nth lno relevance in
 379                    HExtlib.mk_list false lno @ relevance
 380              | _ -> relevance
 381            in
 382            let metasenv, subst, _ =
 383              try
 384                List.fold_left2
 385                  (fun (metasenv, subst, relevance) t1 t2 ->
 386                     let b, relevance =
 387                       match relevance with b::tl -> b,tl | _ -> true, [] in
 388                     let metasenv, subst =
 389                       try unify hdb test_eq_only metasenv subst context t1 t2
 390                       with UnificationFailure _ | Uncertain _ when not b ->
 391                         metasenv, subst
 392                     in
 393                       metasenv, subst, relevance)
 394                  (metasenv, subst, relevance) tl1 tl2
 395              with Invalid_argument _ ->
 396                raise (uncert_exc metasenv subst context t1 t2)
 397            in
 398              metasenv, subst
 399
 400        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
 401           C.Match (ref2,outtype2,term2,pl2)) ->
 402            let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
 403            let _,_,ty,_ = List.nth itl tyno in
 404            let rec remove_prods ~subst context ty =
 405              let ty = NCicReduction.whd ~subst context ty in
 406              match ty with
 407              | C.Sort _ -> ty
 408              | C.Prod (name,so,ta) ->
 409                    remove_prods ~subst ((name,(C.Decl so))::context) ta
 410              | _ -> assert false
 411            in
 412            let is_prop =
 413              match remove_prods ~subst [] ty with
 414              | C.Sort C.Prop -> true
 415              | _ -> false
 416            in
 417            if not (Ref.eq ref1 ref2) then
 418              raise (uncert_exc metasenv subst context t1 t2)
 419            else
 420              let metasenv, subst =
 421               unify hdb test_eq_only metasenv subst context outtype1 outtype2 in
 422              let metasenv, subst =
 423                try unify hdb test_eq_only metasenv subst context term1 term2
 424                with UnificationFailure _ | Uncertain _ when is_prop ->
 425                  metasenv, subst
 426              in
 427              (try
 428               List.fold_left2
 429                (fun (metasenv,subst) ->
 430                   unify hdb test_eq_only metasenv subst context)
 431                (metasenv, subst) pl1 pl2
 432              with Invalid_argument _ ->
 433                raise (uncert_exc metasenv subst context t1 t2))
 434        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
 435        | _ when NCicUntrusted.metas_of_term subst context t1 = [] &&
 436                 NCicUntrusted.metas_of_term subst context t2 = [] ->
 437                   raise (fail_exc metasenv subst context t1 t2)
 438        | _ -> raise (uncert_exc metasenv subst context t1 t2)
 439      (*D*)  in outside(); rc with exn -> outside (); raise exn
 440     in
 441     let try_hints metasenv subst t1 t2 (* exc*) =
 442       let candidates =
 443         NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
 444       in
 445       let rec cand_iter = function
 446         | [] -> None (* raise exc *)
 447         | (metasenv,c1,c2)::tl ->
 448             try
 449               let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in
 450               let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in
 451               Some (metasenv, subst)
 452             with
 453               UnificationFailure _ | Uncertain _ -> cand_iter tl
 454       in
 455         cand_iter candidates
 456     in
 457     let height_of = function
 458      | NCic.Const (Ref.Ref (_,Ref.Def h))
 459      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
 460      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
 461      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
 462      | _ -> 0
 463     in
 464     let put_in_whd m1 m2 =
 465       NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
 466       NCicReduction.reduce_machine ~delta:max_int ~subst context m2
 467     in
 468     let small_delta_step ~subst
 469       ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
 470     =
 471      assert (not (norm1 && norm2));
 472      if norm1 then
 473       x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
 474      else if norm2 then
 475       NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
 476      else
 477       let h1 = height_of t1 in
 478       let h2 = height_of t2 in
 479       let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
 480       NCicReduction.reduce_machine ~delta ~subst context m1,
 481       NCicReduction.reduce_machine ~delta ~subst context m2
 482     in
 483     let rec unif_machines metasenv subst =
 484       function
 485       | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
 486      (*D*) inside 'M'; try let rc =
 487          pp (lazy("UM: " ^
 488            NCicPp.ppterm ~metasenv ~subst ~context
 489              (NCicReduction.unwind (k1,e1,t1,s1)) ^
 490            " === " ^
 491            NCicPp.ppterm ~metasenv ~subst ~context
 492              (NCicReduction.unwind (k2,e2,t2,s2))));
 493 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
 494           let relevance = [] (* TO BE UNDERSTOOD
 495             match t1 with
 496             | C.Const r -> NCicEnvironment.get_relevance r
 497             | _ -> [] *) in
 498           let unif_from_stack t1 t2 b metasenv subst =
 499               try
 500                 let t1 = NCicReduction.from_stack t1 in
 501                 let t2 = NCicReduction.from_stack t2 in
 502                 unif_machines metasenv subst (put_in_whd t1 t2)
 503               with UnificationFailure _ | Uncertain _ when not b ->
 504                 metasenv, subst
 505           in
 506           let rec check_stack l1 l2 r todo =
 507             match l1,l2,r with
 508             | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
 509             | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
 510             | l1, l2, _ ->
 511                NCicReduction.unwind (k1,e1,t1,List.rev l1),
 512                 NCicReduction.unwind (k2,e2,t2,List.rev l2),
 513                 todo
 514           in
 515         let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
 516         try
 517          let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in
 518          List.fold_left
 519           (fun (metasenv,subst) (x1,x2,r) ->
 520             unif_from_stack x1 x2 r metasenv subst
 521           ) (metasenv,subst) todo
 522         with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
 523             unif_machines metasenv subst (small_delta_step ~subst m1 m2)
 524       (*D*)  in outside(); rc with exn -> outside (); raise exn
 525      in
 526      try fo_unif test_eq_only metasenv subst t1 t2
 527      with UnificationFailure msg | Uncertain msg as exn ->
 528        match try_hints metasenv subst t1 t2 with
 529        | Some x -> x
 530        | None ->
 531           try
 532             unif_machines metasenv subst
 533              (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
 534           with
 535           | UnificationFailure _ -> raise (UnificationFailure msg)
 536           | Uncertain _ -> raise exn
 537  (*D*)  in outside(); rc with exn -> outside (); raise exn
 538 ;;
 539
 540 let unify hdb =
 541   indent := "";
 542   unify hdb false;;
 543
 544