matita/components/ng_refiner/nCicUnification.ml

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