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