matitaB/components/ng_refiner/nCicUnification.ml

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