matita/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 lty ^ "=<=" ^
 386           ppterm ~metasenv ~subst ~context ty_t));
 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), t ->
 563           instantiate rdb test_eq_only metasenv subst context n lc
 564             (NCicReduction.head_beta_reduce ~subst t) swap
 565        | t, C.Meta (n,lc) ->
 566           instantiate rdb test_eq_only metasenv subst context n lc
 567            (NCicReduction.head_beta_reduce ~subst t) (not swap)
 568
 569        (* higher order unification case *)
 570        | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
 571            (* this easy_case handles "(? ?) =?= (f a)", same number of
 572             * args, preferring the instantiation "f" over "\_.f a" for the
 573             * metavariable in head position. Since the arguments of the meta
 574             * are flexible, delift would ignore them generating a constant
 575             * function even in the easy case above *)
 576            let easy_case =
 577              match t2 with
 578              | NCic.Appl (f :: f_args)
 579                when
 580                List.exists (NCicMetaSubst.is_flexible context ~subst) args ->
 581                 let mlen = List.length args in
 582                 let flen = List.length f_args in
 583                 let min_len = min mlen flen in
 584                 let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
 585                 let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
 586                  (try
 587                     Some (List.fold_left2
 588                       (fun (m, s) t1 t2 ->
 589                         unify rdb test_eq_only m s context t1 t2 swap
 590                       ) (metasenv,subst)
 591                         ((NCicUntrusted.mk_appl meta mhe)::margs)
 592                         ((NCicUntrusted.mk_appl f fhe)::fargs))
 593                   with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
 594                     None)
 595              | _ -> None
 596            in
 597            (match easy_case with
 598            | Some ms -> ms
 599            | None ->
 600                (* This case handles "(?_f ..ti..) =?= t2", abstracting every
 601                 * non flexible ti (delift skips local context items that are
 602                 * flexible) from t2 in two steps:
 603                 *  1) ?_f := \..xi.. .?
 604                 *  2) ?_f ..ti..  =?= t2 --unif_machines-->
 605                       ?_f[..ti..] =?= t2 --instantiate-->
 606                       delift [..ti..] t2 *)
 607                let metasenv, lambda_Mj =
 608                  lambda_intros rdb metasenv subst context (List.length args)
 609                   (NCicTypeChecker.typeof ~metasenv ~subst context meta)
 610                in
 611                let metasenv, subst =
 612                  unify rdb test_eq_only metasenv subst context
 613                    (C.Meta (i,l)) lambda_Mj swap
 614                in
 615                let metasenv, subst =
 616                  unify rdb test_eq_only metasenv subst context t1 t2 swap
 617                in
 618                (try
 619                  let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
 620                  let term = eta_reduce subst term in
 621                  let subst = List.filter (fun (j,_) -> j <> i) subst in
 622                  metasenv, ((i, (name, ctx, term, ty)) :: subst)
 623                with Not_found -> assert false))
 624
 625        | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
 626            unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
 627
 628        (* processing this case here we avoid a useless small delta step *)
 629        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
 630          when Ref.eq r1 r2 ->
 631            let relevance = NCicEnvironment.get_relevance r1 in
 632            let metasenv, subst, _ =
 633              try
 634                List.fold_left2
 635                  (fun (metasenv, subst, relevance) t1 t2 ->
 636                     let b, relevance =
 637                       match relevance with b::tl -> b,tl | _ -> true, [] in
 638                     let metasenv, subst =
 639                       try unify rdb test_eq_only metasenv subst context t1 t2
 640                             swap
 641                       with UnificationFailure _ | Uncertain _ when not b ->
 642                         metasenv, subst
 643                     in
 644                       metasenv, subst, relevance)
 645                  (metasenv, subst, relevance) tl1 tl2
 646              with
 647                 Invalid_argument _ ->
 648                  raise (Uncertain (mk_msg metasenv subst context t1 t2))
 649               | KeepReducing _ | KeepReducingThis _ -> assert false
 650            in
 651              metasenv, subst
 652
 653        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
 654           C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
 655            let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
 656            let _,_,ty,_ = List.nth itl tyno in
 657            let rec remove_prods ~subst context ty =
 658              let ty = NCicReduction.whd ~subst context ty in
 659              match ty with
 660              | C.Sort _ -> ty
 661              | C.Prod (name,so,ta) ->
 662                    remove_prods ~subst ((name,(C.Decl so))::context) ta
 663              | _ -> assert false
 664            in
 665            let is_prop =
 666              match remove_prods ~subst [] ty with
 667              | C.Sort C.Prop -> true
 668              | _ -> false
 669            in
 670            (* if not (Ref.eq ref1 ref2) then
 671              raise (Uncertain (mk_msg metasenv subst context t1 t2))
 672            else*)
 673              let metasenv, subst =
 674               unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
 675              let metasenv, subst =
 676                try unify rdb test_eq_only metasenv subst context term1 term2 swap
 677                with UnificationFailure _ | Uncertain _ when is_prop ->
 678                  metasenv, subst
 679              in
 680              (try
 681               List.fold_left2
 682                (fun (metasenv,subst) t1 t2 ->
 683                   unify rdb test_eq_only metasenv subst context t1 t2 swap)
 684                (metasenv, subst) pl1 pl2
 685              with Invalid_argument _ -> assert false)
 686        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
 687        | _ when norm1 && norm2 ->
 688            if (could_reduce t1 || could_reduce t2) then
 689             raise (Uncertain (mk_msg metasenv subst context t1 t2))
 690            else
 691             raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
 692        | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
 693      (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn
 694     in
 695     let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
 696      try fo_unif test_eq_only metasenv subst nt1 nt2
 697      with
 698       UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
 699        raise (KeepReducing (mk_msg metasenv subst context t1 t2))
 700     in
 701     let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
 702       if NCicUntrusted.metas_of_term subst context t1 = [] &&
 703          NCicUntrusted.metas_of_term subst context t2 = []
 704       then None
 705       else begin
 706     (*D*) inside 'H'; try let rc =
 707      pp(lazy ("\nProblema:\n" ^
 708         ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
 709         ppterm ~metasenv ~subst ~context t2));
 710       let candidates =
 711         NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
 712       in
 713       let rec cand_iter = function
 714         | [] -> None (* raise exc *)
 715         | (metasenv,(c1,c2),premises)::tl ->
 716             pp (lazy ("\nProvo il candidato:\n" ^
 717               String.concat "\n"
 718                 (List.map
 719                   (fun (a,b) ->
 720                    ppterm ~metasenv ~subst ~context a ^  " =?= " ^
 721                    ppterm ~metasenv ~subst ~context b) premises) ^
 722               "\n-------------------------------------------\n"^
 723               ppterm ~metasenv ~subst ~context c1 ^  " = " ^
 724               ppterm ~metasenv ~subst ~context c2));
 725             try
 726     (*D*) inside 'K'; try let rc =
 727               let metasenv,subst =
 728                 fo_unif test_eq_only metasenv subst mt1 (false,c1) in
 729               let metasenv,subst =
 730                 fo_unif test_eq_only metasenv subst (false,c2) mt2 in
 731               let metasenv,subst =
 732                 List.fold_left
 733                   (fun (metasenv, subst) (x,y) ->
 734                      unify rdb test_eq_only metasenv subst context x y false)
 735                   (metasenv, subst) (List.rev premises)
 736               in
 737               pp(lazy("FUNZIONA!"));
 738               Some (metasenv, subst)
 739      (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn
 740             with
 741              KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
 742            | KeepReducingThis _ -> assert false
 743       in
 744         cand_iter candidates
 745      (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn
 746       end
 747     in
 748     let put_in_whd m1 m2 =
 749       NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
 750       NCicReduction.reduce_machine ~delta:max_int ~subst context m2
 751     in
 752     let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
 753       try fo_unif test_eq_only metasenv subst m1 m2
 754       with
 755       | UnificationFailure _ as exn -> raise exn
 756       | KeepReducing _ | Uncertain _ as exn ->
 757         let (t1,norm1 as tm1),(t2,norm2 as tm2) =
 758          put_in_whd (0,[],t1,[]) (0,[],t2,[])
 759         in
 760          match
 761            try_hints metasenv subst
 762             (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
 763          with
 764           | Some x -> x
 765           | None ->
 766               match exn with
 767               | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
 768               | Uncertain _ as exn -> raise exn
 769               | _ -> assert false
 770     in
 771     let fo_unif_heads_and_cont_or_unwind_and_hints
 772       test_eq_only metasenv subst m1 m2 cont hm1 hm2
 773      =
 774       let ms, continuation =
 775         (* calling the continuation inside the outermost try is an option
 776            and makes unification stronger, but looks not frequent to me
 777            that heads unify but not the arguments and that an hints can fix
 778            that *)
 779         try fo_unif test_eq_only metasenv subst m1 m2, cont
 780         with
 781         | UnificationFailure _
 782         | KeepReducing _ | Uncertain _ as exn ->
 783            let (t1,norm1),(t2,norm2) = hm1, hm2 in
 784            match
 785              try_hints metasenv subst
 786               (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
 787            with
 788             | Some x -> x, fun x -> x
 789             | None ->
 790                 match exn with
 791                 | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
 792                 | UnificationFailure _ | Uncertain _ as exn -> raise exn
 793                 | _ -> assert false
 794       in
 795         continuation ms
 796     in
 797     let height_of = function
 798      | NCic.Const (Ref.Ref (_,Ref.Def h))
 799      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
 800      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
 801      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
 802      | _ -> 0
 803     in
 804     let small_delta_step ~subst
 805       ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
 806     =
 807      assert (not (norm1 && norm2));
 808      if norm1 then
 809       x1,NCicReduction.reduce_machine ~delta:0 ~subst context m2
 810      else if norm2 then
 811       NCicReduction.reduce_machine ~delta:0 ~subst context m1,x2
 812      else
 813       let h1 = height_of t1 in
 814       let h2 = height_of t2 in
 815       let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
 816       NCicReduction.reduce_machine ~delta ~subst context m1,
 817       NCicReduction.reduce_machine ~delta ~subst context m2
 818     in
 819     let rec unif_machines metasenv subst =
 820       function
 821       | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
 822      (*D*) inside 'M'; try let rc =
 823          pp (lazy("UM: " ^
 824            ppterm ~metasenv ~subst ~context
 825              (NCicReduction.unwind (k1,e1,t1,s1)) ^
 826            " === " ^
 827            ppterm ~metasenv ~subst ~context
 828              (NCicReduction.unwind (k2,e2,t2,s2))));
 829          pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
 830           let relevance =
 831             match t1 with
 832             | C.Const r -> NCicEnvironment.get_relevance r
 833             | _ -> [] in
 834           let unif_from_stack (metasenv, subst) (t1, t2, b) =
 835               try
 836                 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
 837                 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
 838                 unif_machines metasenv subst (put_in_whd t1 t2)
 839               with UnificationFailure _ | Uncertain _ when not b ->
 840                 metasenv, subst
 841           in
 842           let rec check_stack l1 l2 r todo =
 843             match l1,l2,r with
 844             | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
 845             | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
 846             | l1, l2, _ ->
 847                NCicReduction.unwind (k1,e1,t1,List.rev l1),
 848                 NCicReduction.unwind (k2,e2,t2,List.rev l2),
 849                 todo
 850           in
 851           let check_stack l1 l2 r =
 852             match t1, t2 with
 853             | NCic.Meta _, _ | _, NCic.Meta _ ->
 854                 (NCicReduction.unwind (k1,e1,t1,s1)),
 855                 (NCicReduction.unwind (k2,e2,t2,s2)),[]
 856             | _ -> check_stack l1 l2 r []
 857           in
 858         let hh1,hh2,todo =
 859           check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
 860         try
 861           fo_unif_heads_and_cont_or_unwind_and_hints
 862             test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
 863             (fun ms -> List.fold_left unif_from_stack ms todo)
 864             m1 m2
 865         with
 866          | KeepReducing _ -> assert false
 867          | KeepReducingThis _ ->
 868             assert (not (norm1 && norm2));
 869             unif_machines metasenv subst (small_delta_step ~subst m1 m2)
 870          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
 871            -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
 872          | UnificationFailure msg
 873            when could_reduce (NCicReduction.unwind (fst m1))
 874              || could_reduce (NCicReduction.unwind (fst m2))
 875            -> raise (Uncertain msg)
 876       (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn
 877      in
 878      try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
 879      with
 880       | KeepReducingThis (msg,tm1,tm2) ->
 881          (try
 882            unif_machines metasenv subst (tm1,tm2)
 883           with
 884           | UnificationFailure _ -> raise (UnificationFailure msg)
 885           | Uncertain _ -> raise (Uncertain msg)
 886           | KeepReducing _ -> assert false)
 887       | KeepReducing _ -> assert false
 888
 889  (*D*)  in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn
 890
 891 and delift_type_wrt_terms rdb metasenv subst context t args =
 892   let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
 893   let (metasenv, subst), t =
 894    try
 895     NCicMetaSubst.delift
 896       ~unify:(fun m s c t1 t2 ->
 897          let ind = !indent in
 898          let res =
 899            try Some (unify rdb false m s c t1 t2 false)
 900            with UnificationFailure _ | Uncertain _ -> None
 901          in
 902          indent := ind; res)
 903       metasenv subst context 0 (0,NCic.Ctx lc) t
 904    with
 905       NCicMetaSubst.MetaSubstFailure _
 906     | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
 907   in
 908    metasenv, subst, t
 909 ;;
 910
 911
 912 let unify rdb ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2=
 913   indent := "";
 914   unify rdb test_eq_only metasenv subst context t1 t2 swap;;
 915
 916 let fix_sorts m s =
 917   fix m s true false (UnificationFailure (lazy "no sup"))
 918 ;;