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