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 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 metasenv subst context t1 t2 =
  25  (lazy (
  26   "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
  27   " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
  28
  29 let mk_appl ~upto hd tl =
  30   NCicReduction.head_beta_reduce ~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 subst t =
  39   let delift_if_not_occur body =
  40     try
  41         Some (NCicSubstitution.psubst ~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 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 ~metasenv ~subst c =
 112       "\nctx:\n"^ NCicPp.ppcontext ~metasenv ~subst c
 113 ;;
 114 let ppmetasenv ~subst m = "\nmenv:\n" ^ NCicPp.ppmetasenv ~subst m;;
 115
 116 let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "";;
 117 let ppmetasenv ~subst:_subst _metasenv = "";;
 118 let ppterm ~metasenv ~subst ~context = NCicPp.ppterm ~metasenv ~subst ~context;;
 119 (* let ppterm ~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 rdb metasenv subst context argsno ty =
 147  pp (lazy ("LAMBDA INTROS: " ^ ppterm ~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 ~subst context ty with
 156          C.Prod (n,so,ta) ->
 157           let metasenv,bo =
 158            lambda_intros rdb 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 metasenv subst is_sup test_eq_only exc t =
 168   (*D*)  inside 'f'; try let rc =
 169   pp (lazy (NCicPp.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 (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 exc metasenv subst context t =
 209  let t = NCicReduction.whd ~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 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 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 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 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 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 exc metasenv subst context ty in
 273      metasenv,subst,t
 274 ;;
 275
 276 let rec instantiate rdb 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 ~metasenv ~subst ~context t));
 279   let exc =
 280     UnificationFailure (mk_msg 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 ~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 ~metasenv ~subst ~context t));
 289     let (metasenv, subst), t =
 290       try
 291         NCicMetaSubst.delift
 292          ~unify:(fun m s c t1 t2 ->
 293            let ind = !indent in
 294            let res =
 295              try Some (unify rdb 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 ~metasenv ~subst ~context:cc t^ppmetasenv ~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 lc oldt in
 313       let t = NCicSubstitution.subst_meta lc t in
 314       (* conjecture: always fail --> occur check *)
 315       unify rdb 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 metasenv subst swap test_eq_only exc t in
 322   let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in
 323   let metasenv,subst,t =
 324    match kind with
 325       `IsSort -> sortfy exc metasenv subst context t
 326     | `IsType -> tipify 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 ~metasenv ~subst ~context ty ^ "=<=" ^
 353             ppterm ~metasenv ~subst ~context ty_t));
 354           let metasenv, subst =
 355             unify rdb 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
 366                ~unify:(fun m s c t1 t2 ->
 367                  let ind = !indent in
 368                  let res = try Some (unify rdb 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 lc ty in
 384         pp (lazy ("On the types: " ^
 385           ppterm ~metasenv ~subst ~context ty_t ^ "=<=" ^
 386           ppterm ~metasenv ~subst ~context lty));
 387         let metasenv, subst =
 388           unify rdb 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 rdb 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 ~metasenv ~subst ~context t1 ^
 399           (if swap then " ==>?== "
 400            else " ==<?==" ) ^
 401          ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
 402          ~subst metasenv));
 403      pp (lazy("  " ^ ppterm ~metasenv ~subst:[] ~context t1 ^
 404           (if swap then " ==>??== "
 405            else " ==<??==" ) ^
 406          ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv
 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 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 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 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 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 rdb true metasenv subst context s1 s2 swap in
 443            unify rdb 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 rdb test_eq_only metasenv subst context ty1 ty2 swap in
 446            let metasenv,subst=unify rdb test_eq_only metasenv subst context s1 s2 swap in
 447            let context = (name1, C.Def (s1,ty1))::context in
 448            unify rdb 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 rdb (*test_eq_only*) true metasenv subst context
 460                     (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift 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 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 lc1 term in
 480                 let term2 = NCicSubstitution.subst_meta lc2 term in
 481                   unify rdb 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 rdb (*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 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 ~subst context t1 with
 498               | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
 499                  let metasenv, lambda_Mj =
 500                    lambda_intros rdb metasenv subst context (List.length args)
 501                     (NCicTypeChecker.typeof ~metasenv ~subst context meta)
 502                  in
 503                    unify rdb 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 ~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 rdb 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 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 rdb 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 lc term in
 541             unify rdb test_eq_only metasenv subst context t term swap
 542        | C.Meta (n,_), _ when List.mem_assoc n subst ->
 543             unify rdb 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 l term in
 548               unify rdb test_eq_only metasenv subst context t1
 549                 (mk_appl ~upto:(List.length args) term args) swap
 550        | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
 551             unify rdb 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 rdb test_eq_only metasenv subst context m lc'
 561             (NCicReduction.head_beta_reduce ~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 lc tyn in
 566           let tym = NCicSubstitution.subst_meta 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 rdb test_eq_only metasenv subst context m lc'
 572             (NCicReduction.head_beta_reduce ~subst t1) (not swap)
 573        | C.Meta (n,lc), t ->
 574           instantiate rdb test_eq_only metasenv subst context n lc
 575             (NCicReduction.head_beta_reduce ~subst t) swap
 576        | t, C.Meta (n,lc) ->
 577           instantiate rdb test_eq_only metasenv subst context n lc
 578            (NCicReduction.head_beta_reduce ~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 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 rdb 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 rdb metasenv subst context (List.length args)
 620                   (NCicTypeChecker.typeof ~metasenv ~subst context meta)
 621                in
 622                let metasenv, subst =
 623                  unify rdb test_eq_only metasenv subst context
 624                    (C.Meta (i,l)) lambda_Mj swap
 625                in
 626                let metasenv, subst =
 627                  unify rdb 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 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 rdb 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 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 rdb 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 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 ref1 in
 667            let _,_,ty,_ = List.nth itl tyno in
 668            let rec remove_prods ~subst context ty =
 669              let ty = NCicReduction.whd ~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 metasenv subst context t1 t2))
 683            else*)
 684              let metasenv, subst =
 685               unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
 686              let metasenv, subst =
 687                try unify rdb 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 rdb 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 metasenv subst context t1 t2))
 701            else
 702             raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
 703        | _ -> raise (KeepReducing (mk_msg 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 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 subst context t1 = [] &&
 714          NCicUntrusted.metas_of_term subst context t2 = []
 715       then None
 716       else begin
 717     (*D*) inside 'H'; try let rc =
 718      pp(lazy ("\nProblema:\n" ^
 719         ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
 720         ppterm ~metasenv ~subst ~context t2));
 721       let candidates =
 722         NCicUnifHint.look_for_hint rdb 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 ~metasenv ~subst ~context a ^  " =?= " ^
 732                    ppterm ~metasenv ~subst ~context b) premises) ^
 733               "\n-------------------------------------------\n"^
 734               ppterm ~metasenv ~subst ~context c1 ^  " = " ^
 735               ppterm ~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 rdb 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 ~delta:max_int ~subst context m1,
 761       NCicReduction.reduce_machine ~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 t1) (norm2,NCicReduction.unwind 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 t1) (norm2,NCicReduction.unwind 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 ~delta:0 ~subst context m2
 821      else if norm2 then
 822       NCicReduction.reduce_machine ~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 ~delta ~subst context m1,
 828       NCicReduction.reduce_machine ~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 ~metasenv ~subst ~context
 836              (NCicReduction.unwind (k1,e1,t1,s1)) ^
 837            " === " ^
 838            ppterm ~metasenv ~subst ~context
 839              (NCicReduction.unwind (k2,e2,t2,s2))));
 840          pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
 841           let relevance = [] (* TO BE UNDERSTOOD
 842             match t1 with
 843             | C.Const r -> NCicEnvironment.get_relevance 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 (k1,e1,t1,List.rev l1),
 859                 NCicReduction.unwind (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 (k1,e1,t1,s1)),
 866                 (NCicReduction.unwind (k2,e2,t2,s2)),[]
 867             | _ -> check_stack l1 l2 r []
 868           in
 869         let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in
 870         try
 871           fo_unif_heads_and_cont_or_unwind_and_hints
 872             test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
 873             (fun ms -> List.fold_left unif_from_stack ms todo)
 874             m1 m2
 875         with
 876          | KeepReducing _ -> assert false
 877          | KeepReducingThis _ ->
 878             assert (not (norm1 && norm2));
 879             unif_machines metasenv subst (small_delta_step ~subst m1 m2)
 880          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
 881            -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
 882          | UnificationFailure msg
 883            when could_reduce (NCicReduction.unwind (fst m1))
 884              || could_reduce (NCicReduction.unwind (fst m2))
 885            -> raise (Uncertain msg)
 886       (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn
 887      in
 888      try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
 889      with
 890       | KeepReducingThis (msg,tm1,tm2) ->
 891          (try
 892            unif_machines metasenv subst (tm1,tm2)
 893           with
 894           | UnificationFailure _ -> raise (UnificationFailure msg)
 895           | Uncertain _ -> raise (Uncertain msg)
 896           | KeepReducing _ -> assert false)
 897       | KeepReducing _ -> assert false
 898
 899  (*D*)  in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn
 900
 901 and delift_type_wrt_terms rdb metasenv subst context t args =
 902   let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
 903   let (metasenv, subst), t =
 904    try
 905     NCicMetaSubst.delift
 906       ~unify:(fun m s c t1 t2 ->
 907          let ind = !indent in
 908          let res =
 909            try Some (unify rdb false m s c t1 t2 false)
 910            with UnificationFailure _ | Uncertain _ -> None
 911          in
 912          indent := ind; res)
 913       metasenv subst context 0 (0,NCic.Ctx lc) t
 914    with
 915       NCicMetaSubst.MetaSubstFailure _
 916     | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
 917   in
 918    metasenv, subst, t
 919 ;;
 920
 921
 922 let unify rdb ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2=
 923   indent := "";
 924   unify rdb test_eq_only metasenv subst context t1 t2 swap;;
 925
 926 let fix_sorts m s =
 927   fix m s true false (UnificationFailure (lazy "no sup"))
 928 ;;