matitaB/components/ng_refiner/nCicUnification.ml

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