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