matita/components/ng_refiner/nCicUnification.ml

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