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