helm/software/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 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 pp s =
  81  if !debug then
  82   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
  83  else
  84   ()
  85 ;;
  86 let inside c =
  87  indent := !indent ^ String.make 1 c;
  88  if !debug then prerr_endline ("{{{" ^ !indent ^ " ")
  89 ;;
  90 let outside ok =
  91  if !debug then prerr_endline "}}}";
  92  if not ok then pp (lazy "exception raised!");
  93  try
  94   indent := String.sub !indent 0 (String.length !indent -1)
  95  with
  96   Invalid_argument _ -> indent := "??"; ()
  97 ;;
  98
  99 let ppcontext ~metasenv ~subst c =
 100       "\nctx:\n"^ NCicPp.ppcontext ~metasenv ~subst c
 101 ;;
 102 let ppmetasenv ~subst m = "\nmenv:\n" ^ NCicPp.ppmetasenv ~subst m;;
 103
 104 let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "";;
 105 let ppmetasenv ~subst:_subst _metasenv = "";;
 106
 107 let fix_sorts swap exc t =
 108   let rec aux () = function
 109     | NCic.Sort (NCic.Type u) as orig ->
 110         if swap then
 111          match NCicEnvironment.sup u with
 112          | None ->
 113             prerr_endline ("no sup for " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] orig) ;
 114             raise exc
 115          | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
 116         else
 117          NCic.Sort (NCic.Type (
 118            match NCicEnvironment.sup NCicEnvironment.type0 with
 119            | Some x -> x
 120            | _ -> assert false))
 121     | NCic.Meta _ as orig -> orig
 122     | t -> NCicUtils.map (fun _ _ -> ()) () aux t
 123   in
 124     aux () t
 125 ;;
 126
 127 let is_locked n subst =
 128    try
 129      match NCicUtils.lookup_subst n subst with
 130      | tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true
 131      | _ -> false
 132    with NCicUtils.Subst_not_found _ -> false
 133 ;;
 134
 135 let rec mk_irl stop base =
 136   if base > stop then []
 137   else (NCic.Rel base) :: mk_irl stop (base+1)
 138 ;;
 139
 140 (* the argument must be a term in whd *)
 141 let rec could_reduce =
 142  function
 143   | C.Meta _ -> true
 144   | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args)
 145      when List.length args > recno -> could_reduce (List.nth args recno)
 146   | C.Match (_,_,arg,_) -> could_reduce arg
 147   | C.Appl (he::_) -> could_reduce he
 148   | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
 149   | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
 150 ;;
 151
 152 let rec lambda_intros rdb metasenv subst context t args =
 153  let tty = NCicTypeChecker.typeof ~metasenv ~subst context t in
 154  let argsty =
 155   List.map
 156   (fun arg -> arg, NCicTypeChecker.typeof ~metasenv ~subst context arg) args in
 157  let context_of_args = context in
 158  let rec mk_lambda metasenv subst context n processed_args = function
 159    | [] ->
 160        let metasenv, _, bo, _ =
 161          NCicMetaSubst.mk_meta metasenv context
 162            (`WithType (NCicSubstitution.lift n tty))
 163        in
 164        metasenv, subst, bo
 165    | (arg,ty)::tail ->
 166        pp(lazy("arg{ " ^
 167          NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^  " : " ^
 168          NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty));
 169        let metasenv, subst, telescopic_ty =
 170          if processed_args = [] then metasenv, subst, ty else
 171          let _ = pp(lazy("delift")) in
 172          delift_type_wrt_terms rdb metasenv subst context
 173            (NCicSubstitution.lift n ty)
 174            (List.map (NCicSubstitution.lift n) (List.rev processed_args))
 175        in
 176        pp(lazy("arg} "^NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty));
 177        let name = "HBeta"^string_of_int n in
 178        let metasenv, subst, bo =
 179         mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
 180          (arg::processed_args) tail
 181        in
 182         metasenv, subst, NCic.Lambda (name, telescopic_ty, bo)
 183  in
 184  pp(lazy("LAMBDA_INTROS{ " ^
 185    NCicPp.ppterm ~metasenv ~subst ~context t ^  ":" ^
 186    NCicPp.ppterm ~metasenv ~subst ~context tty ^ " over " ^
 187    String.concat "," (List.map (NCicPp.ppterm ~metasenv ~subst ~context)args)));
 188  let rc = mk_lambda metasenv subst context 0 [] argsty in
 189  pp(lazy("LAMBDA_INTROS}"));
 190  rc
 191
 192 and instantiate rdb test_eq_only metasenv subst context n lc t swap =
 193  (*D*)  inside 'I'; try let rc =
 194          pp (lazy(string_of_int n ^ " :=?= "^
 195            NCicPp.ppterm ~metasenv ~subst ~context t));
 196   let unify test_eq_only m s c t1 t2 =
 197     if swap then unify rdb test_eq_only m s c t2 t1
 198     else unify rdb test_eq_only m s c t1 t2
 199   in
 200   let has_tag = List.exists in
 201   let tags, _, ty = NCicUtils.lookup_meta n metasenv in
 202   (* on the types *)
 203   let metasenv, subst, t =
 204     match ty with
 205     | NCic.Implicit (`Typeof _) ->
 206          pp(lazy("meta with no type"));
 207          assert(has_tag ((=)`IsSort) tags);
 208          metasenv, subst, t
 209     | _ ->
 210        let exc_to_be =
 211         UnificationFailure (mk_msg metasenv subst context (NCic.Meta (n,lc)) t)
 212        in
 213        let t, ty_t =
 214          try t, NCicTypeChecker.typeof ~subst ~metasenv context t
 215          with
 216          | NCicTypeChecker.AssertFailure msg as exn ->
 217               pp(lazy("we try to fix the sort\n"^
 218                 Lazy.force msg^"\n"^NCicPp.ppmetasenv ~subst metasenv));
 219               let ft = fix_sorts swap exc_to_be t in
 220               pp(lazy("unable to fix the sort"));
 221               if ft == t then raise exn;
 222               (try ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
 223                with NCicTypeChecker.AssertFailure _ -> raise exn)
 224          | NCicTypeChecker.TypeCheckerFailure msg ->
 225               prerr_endline (Lazy.force msg);
 226               prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
 227               prerr_endline (ppcontext ~metasenv ~subst context);
 228               prerr_endline (ppmetasenv ~subst metasenv);
 229               assert false
 230        in
 231        match ty_t with
 232        | NCic.Implicit (`Typeof _) ->
 233            raise (UnificationFailure(lazy "trying to unify a term with a type"))
 234        | _ ->
 235           let lty = NCicSubstitution.subst_meta lc ty in
 236           pp (lazy ("On the types: " ^
 237               NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " ^
 238               NCicPp.ppterm ~metasenv ~subst ~context ty_t));
 239           let metasenv,subst =
 240            try unify test_eq_only metasenv subst context lty ty_t
 241            with NCicEnvironment.BadConstraint _ as exc ->
 242             let ty_t = fix_sorts swap exc_to_be ty_t in
 243              try unify test_eq_only metasenv subst context lty ty_t
 244              with
 245              | NCicEnvironment.BadConstraint _
 246              | UnificationFailure _ -> raise exc
 247           in
 248            metasenv, subst, t
 249   in
 250   (* viral sortification *)
 251   let is_sort metasenv subst context t =
 252     match NCicReduction.whd ~subst context t with
 253     | NCic.Meta (i,_) ->
 254          let tags, _, _ = NCicUtils.lookup_meta i metasenv in
 255          has_tag ((=) `IsSort) tags
 256     | NCic.Sort _ -> true
 257     | _ -> false
 258   in
 259   let rec sortify metasenv subst = function
 260     | NCic.Implicit (`Typeof _) -> assert false
 261     | NCic.Sort _ as t -> metasenv, subst, t, 0
 262     | NCic.Meta (i,_) as t ->
 263          let tags, context, ty = NCicUtils.lookup_meta i metasenv in
 264          if has_tag ((=) `IsSort) tags then metasenv, subst, t, i
 265          else
 266            let ty = NCicReduction.whd ~subst context ty in
 267            let metasenv, subst, ty, _ = sortify metasenv subst ty in
 268            let metasenv, j, m, _ =
 269              NCicMetaSubst.mk_meta metasenv ~attrs:[`IsSort] [] (`WithType ty)
 270            in
 271            pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j));
 272            let subst_entry = i, (tags, context, m, ty) in
 273            let subst = subst_entry :: subst in
 274            let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
 275            metasenv, subst, m, j
 276     | NCic.Appl (NCic.Meta _ as hd :: args) as t ->
 277            let metasenv, subst, lambda_Mj =
 278              lambda_intros rdb metasenv subst context t args
 279            in
 280            let metasenv,subst= unify true metasenv subst context hd lambda_Mj in
 281            let t = NCicReduction.whd ~subst context t in
 282            let _result = sortify metasenv subst t in
 283            (* untested, maybe dead, code *) assert false;
 284     | t ->
 285          if could_reduce t then raise (Uncertain(lazy "not a sort"))
 286          else raise (UnificationFailure(lazy "not a sort"))
 287   in
 288   let metasenv, subst, _, n =
 289     if has_tag ((=) `IsSort) tags then
 290       let m,s,x,_ = sortify metasenv subst (NCicReduction.whd ~subst context t)
 291       in m,s,x,n
 292     else if is_sort metasenv subst context t then
 293       sortify metasenv subst (NCic.Meta (n,lc))
 294     else
 295       metasenv, subst, NCic.Rel ~-1,n
 296   in
 297   let tags, ctx, ty = NCicUtils.lookup_meta n metasenv in
 298   (* instantiation *)
 299   pp (lazy(string_of_int n ^ " := 111 = "^
 300     NCicPp.ppterm ~metasenv ~subst ~context t));
 301   let (metasenv, subst), t =
 302     try
 303       NCicMetaSubst.delift
 304        ~unify:(fun m s c t1 t2 ->
 305          let ind = !indent in
 306          let res =
 307            try Some (unify test_eq_only m s c t1 t2 )
 308            with UnificationFailure _ | Uncertain _ -> None
 309          in
 310          indent := ind; res)
 311        metasenv subst context n lc t
 312     with NCicMetaSubst.Uncertain msg ->
 313          pp (lazy ("delift fails: " ^ Lazy.force msg));
 314          raise (Uncertain msg)
 315     | NCicMetaSubst.MetaSubstFailure msg ->
 316          pp (lazy ("delift fails: " ^ Lazy.force msg));
 317          raise (UnificationFailure msg)
 318   in
 319          pp (lazy(string_of_int n ^ " := 222 = "^
 320            NCicPp.ppterm ~metasenv ~subst ~context:ctx t
 321          ^ ppmetasenv ~subst metasenv));
 322   (* Unifying the types may have already instantiated n. *)
 323   try
 324     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
 325     let oldt = NCicSubstitution.subst_meta lc oldt in
 326     let t = NCicSubstitution.subst_meta lc t in
 327     (* conjecture: always fail --> occur check *)
 328     unify test_eq_only metasenv subst context oldt t
 329   with NCicUtils.Subst_not_found _ ->
 330     let metasenv, tags =
 331       let rec aux = function
 332         | NCic.Meta (j,lc) ->
 333             (try
 334               let _, _, t, _ = NCicUtils.lookup_subst j subst in
 335               aux (NCicSubstitution.subst_meta lc t)
 336             with NCicUtils.Subst_not_found _ ->
 337               let tags', ctx, ty = NCicUtils.lookup_meta j metasenv in
 338               let metasenv = List.remove_assoc j metasenv in
 339               let tags = tags @ tags' in
 340               (j, (tags, ctx, ty)) :: metasenv, tags)
 341         | _ -> metasenv, tags
 342       in
 343         aux t
 344     in
 345     (* by cumulativity when unify(?,Type_i)
 346      * we could ? := Type_j with j <= i... *)
 347     let subst = (n, (tags, ctx, t, ty)) :: subst in
 348     pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
 349       ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
 350     let metasenv =
 351       List.filter (fun (m,_) -> not (n = m)) metasenv
 352     in
 353     metasenv, subst
 354  (*D*)  in outside true; rc with exn -> outside false; raise exn
 355
 356 and unify rdb test_eq_only metasenv subst context t1 t2 =
 357  (*D*) inside 'U'; try let rc =
 358    let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) =
 359     (*D*) inside 'F'; try let rc =
 360      pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
 361          NCicPp.ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
 362          ~subst metasenv));
 363      pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^
 364          NCicPp.ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv
 365          ~subst metasenv));
 366      if t1 === t2 then
 367        metasenv, subst
 368      else
 369        match (t1,t2) with
 370        | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
 371        | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
 372            prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
 373            assert false
 374        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
 375            if NCicEnvironment.universe_leq a b then metasenv, subst
 376            else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
 377        | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
 378            if NCicEnvironment.universe_eq a b then metasenv, subst
 379            else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
 380        | (C.Sort C.Prop,C.Sort (C.Type _)) ->
 381            if (not test_eq_only) then metasenv, subst
 382            else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
 383
 384        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
 385        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 386            let metasenv, subst = unify rdb true metasenv subst context s1 s2 in
 387            unify rdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
 388        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
 389            let metasenv,subst=unify rdb test_eq_only metasenv subst context ty1 ty2 in
 390            let metasenv,subst=unify rdb test_eq_only metasenv subst context s1 s2 in
 391            let context = (name1, C.Def (s1,ty1))::context in
 392            unify rdb test_eq_only metasenv subst context t1 t2
 393
 394        | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
 395           (try
 396            let l1 = NCicUtils.expand_local_context l1 in
 397            let l2 = NCicUtils.expand_local_context l2 in
 398            let metasenv, subst, to_restrict, _ =
 399             List.fold_right2
 400              (fun t1 t2 (metasenv, subst, to_restrict, i) ->
 401                 try
 402                   let metasenv, subst =
 403                    unify rdb test_eq_only metasenv subst context
 404                     (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
 405                   in
 406                   metasenv, subst, to_restrict, i-1
 407                 with UnificationFailure _ | Uncertain _ ->
 408                   metasenv, subst, i::to_restrict, i-1)
 409              l1 l2 (metasenv, subst, [], List.length l1)
 410            in
 411            if to_restrict <> [] then
 412              let metasenv, subst, _ =
 413                NCicMetaSubst.restrict metasenv subst n1 to_restrict
 414              in
 415                metasenv, subst
 416            else metasenv, subst
 417           with
 418            | Invalid_argument _ -> assert false
 419            | NCicMetaSubst.MetaSubstFailure msg ->
 420               try
 421                 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
 422                 let term1 = NCicSubstitution.subst_meta lc1 term in
 423                 let term2 = NCicSubstitution.subst_meta lc2 term in
 424                   unify rdb test_eq_only metasenv subst context term1 term2
 425               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
 426
 427        |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
 428           NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
 429             (try
 430               List.fold_left2
 431                 (fun (metasenv, subst) t1 t2 ->
 432                   unify rdb test_eq_only metasenv subst context t1 t2)
 433                 (metasenv,subst) l1 l2
 434             with Invalid_argument _ ->
 435               raise (UnificationFailure (mk_msg metasenv subst context t1 t2)))
 436
 437        | _, NCic.Meta (n, _) when is_locked n subst ->
 438            (let (metasenv, subst), i =
 439               match NCicReduction.whd ~subst context t1 with
 440               | NCic.Appl (NCic.Meta (i,l)::args) ->
 441                  let metasenv, subst, lambda_Mj =
 442                    lambda_intros rdb metasenv subst context t1 args
 443                  in
 444                    unify rdb test_eq_only metasenv subst context
 445                     (C.Meta (i,l)) lambda_Mj,
 446                    i
 447               | NCic.Meta (i,_) -> (metasenv, subst), i
 448               | _ ->
 449                  raise (UnificationFailure (lazy "Locked term vs non
 450                   flexible term; probably not saturated enough yet!"))
 451              in
 452               let t1 = NCicReduction.whd ~subst context t1 in
 453               let j, lj =
 454                 match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
 455               in
 456               let metasenv, subst =
 457                 instantiate rdb test_eq_only metasenv subst context j lj t2 true
 458               in
 459               (* We need to remove the out_scope_tags to avoid propagation of
 460                  them that triggers again the ad-hoc case *)
 461               let subst =
 462                List.map (fun (i,(tag,ctx,bo,ty)) ->
 463                 let tag =
 464                  List.filter
 465                   (function `InScope | `OutScope _ -> false | _ -> true) tag
 466                 in
 467                   i,(tag,ctx,bo,ty)
 468                 ) subst
 469               in
 470               (try
 471                 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
 472                 let term = eta_reduce subst term in
 473                 let subst = List.filter (fun (j,_) -> j <> i) subst in
 474                 metasenv, ((i, (name, ctx, term, ty)) :: subst)
 475               with Not_found -> assert false))
 476
 477        | C.Meta (n,lc), t when List.mem_assoc n subst ->
 478           let _,_,term,_ = NCicUtils.lookup_subst n subst in
 479           let term = NCicSubstitution.subst_meta lc term in
 480             unify rdb test_eq_only metasenv subst context term t
 481
 482        | t, C.Meta (n,lc) when List.mem_assoc n subst ->
 483           let _,_,term,_ = NCicUtils.lookup_subst n subst in
 484           let term = NCicSubstitution.subst_meta lc term in
 485             unify rdb test_eq_only metasenv subst context t term
 486
 487        | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
 488             let _,_,term,_ = NCicUtils.lookup_subst i subst in
 489             let term = NCicSubstitution.subst_meta l term in
 490               unify rdb test_eq_only metasenv subst context
 491                 (mk_appl ~upto:(List.length args) term args) t2
 492
 493        | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
 494             let _,_,term,_ = NCicUtils.lookup_subst i subst in
 495             let term = NCicSubstitution.subst_meta l term in
 496               unify rdb test_eq_only metasenv subst context t1
 497                 (mk_appl ~upto:(List.length args) term args)
 498
 499        | C.Meta (n,lc), t ->
 500           instantiate rdb test_eq_only metasenv subst context n lc
 501             (NCicReduction.head_beta_reduce ~subst t) false
 502
 503        | t, C.Meta (n,lc) ->
 504           instantiate rdb test_eq_only metasenv subst context n lc
 505            (NCicReduction.head_beta_reduce ~subst t) true
 506
 507        | NCic.Appl (NCic.Meta (i,l)::args), _ ->
 508           let metasenv, subst, lambda_Mj =
 509             lambda_intros rdb metasenv subst context t1 args
 510           in
 511           let metasenv, subst =
 512            try
 513             unify rdb test_eq_only metasenv subst context
 514               (C.Meta (i,l)) lambda_Mj
 515            with UnificationFailure msg | Uncertain msg ->
 516             (* failure: let's try again argument vs argument *)
 517             raise (KeepReducing msg)
 518           in
 519           let metasenv, subst =
 520             unify rdb test_eq_only metasenv subst context t1 t2
 521           in
 522           (try
 523             let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
 524             let term = eta_reduce subst term in
 525             let subst = List.filter (fun (j,_) -> j <> i) subst in
 526             metasenv, ((i, (name, ctx, term, ty)) :: subst)
 527           with Not_found -> assert false)
 528
 529        | _, NCic.Appl (NCic.Meta (i,l)::args) ->
 530          let metasenv, subst, lambda_Mj =
 531            lambda_intros rdb metasenv subst context t2 args
 532          in
 533          let metasenv, subst =
 534           try
 535            unify rdb test_eq_only metasenv subst context
 536             lambda_Mj (C.Meta (i,l))
 537           with UnificationFailure msg | Uncertain msg ->
 538            (* failure: let's try again argument vs argument *)
 539            raise (KeepReducing msg)
 540          in
 541          let metasenv, subst =
 542            unify rdb test_eq_only metasenv subst context t1 t2
 543          in
 544          (try
 545            let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
 546            let term = eta_reduce subst term in
 547            let subst = List.filter (fun (j,_) -> j <> i) subst in
 548            metasenv, ((i, (name, ctx, term, ty)) :: subst)
 549          with Not_found -> assert false)
 550
 551        (* processing this case here we avoid a useless small delta step *)
 552        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
 553          when Ref.eq r1 r2 ->
 554            let relevance = NCicEnvironment.get_relevance r1 in
 555            let relevance = match r1 with
 556              | Ref.Ref (_,Ref.Con (_,_,lno)) ->
 557                  let relevance =
 558                   try snd (HExtlib.split_nth lno relevance)
 559                   with Failure _ -> []
 560                  in
 561                    HExtlib.mk_list false lno @ relevance
 562              | _ -> relevance
 563            in
 564            let metasenv, subst, _ =
 565              try
 566                List.fold_left2
 567                  (fun (metasenv, subst, relevance) t1 t2 ->
 568                     let b, relevance =
 569                       match relevance with b::tl -> b,tl | _ -> true, [] in
 570                     let metasenv, subst =
 571                       try unify rdb test_eq_only metasenv subst context t1 t2
 572                       with UnificationFailure _ | Uncertain _ when not b ->
 573                         metasenv, subst
 574                     in
 575                       metasenv, subst, relevance)
 576                  (metasenv, subst, relevance) tl1 tl2
 577              with
 578                 Invalid_argument _ ->
 579                  raise (Uncertain (mk_msg metasenv subst context t1 t2))
 580               | UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
 581                  raise (KeepReducing (mk_msg metasenv subst context t1 t2))
 582            in
 583              metasenv, subst
 584
 585        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
 586           C.Match (ref2,outtype2,term2,pl2)) ->
 587            let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
 588            let _,_,ty,_ = List.nth itl tyno in
 589            let rec remove_prods ~subst context ty =
 590              let ty = NCicReduction.whd ~subst context ty in
 591              match ty with
 592              | C.Sort _ -> ty
 593              | C.Prod (name,so,ta) ->
 594                    remove_prods ~subst ((name,(C.Decl so))::context) ta
 595              | _ -> assert false
 596            in
 597            let is_prop =
 598              match remove_prods ~subst [] ty with
 599              | C.Sort C.Prop -> true
 600              | _ -> false
 601            in
 602            if not (Ref.eq ref1 ref2) then
 603              raise (Uncertain (mk_msg metasenv subst context t1 t2))
 604            else
 605              let metasenv, subst =
 606               unify rdb test_eq_only metasenv subst context outtype1 outtype2 in
 607              let metasenv, subst =
 608                try unify rdb test_eq_only metasenv subst context term1 term2
 609                with UnificationFailure _ | Uncertain _ when is_prop ->
 610                  metasenv, subst
 611              in
 612              (try
 613               List.fold_left2
 614                (fun (metasenv,subst) ->
 615                   unify rdb test_eq_only metasenv subst context)
 616                (metasenv, subst) pl1 pl2
 617              with Invalid_argument _ -> assert false)
 618        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
 619        | _ when norm1 && norm2 ->
 620            if (could_reduce t1 || could_reduce t2) then
 621             raise (Uncertain (mk_msg metasenv subst context t1 t2))
 622            else
 623             raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
 624        | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
 625      (*D*)  in outside true; rc with exn -> outside false; raise exn
 626     in
 627     let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
 628     (*D*) inside 'H'; try let rc =
 629      pp(lazy ("\nProblema:\n" ^
 630         NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
 631         NCicPp.ppterm ~metasenv ~subst ~context t2));
 632       let candidates =
 633         NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
 634       in
 635       let rec cand_iter = function
 636         | [] -> None (* raise exc *)
 637         | (metasenv,(c1,c2),premises)::tl ->
 638             pp (lazy ("\nProvo il candidato:\n" ^
 639               String.concat "\n"
 640                 (List.map
 641                   (fun (a,b) ->
 642                    NCicPp.ppterm ~metasenv ~subst ~context a ^  " =?= " ^
 643                    NCicPp.ppterm ~metasenv ~subst ~context b) premises) ^
 644               "\n-------------------------------------------\n"^
 645               NCicPp.ppterm ~metasenv ~subst ~context c1 ^  " = " ^
 646               NCicPp.ppterm ~metasenv ~subst ~context c2));
 647             try
 648     (*D*) inside 'K'; try let rc =
 649               let metasenv,subst =
 650                 fo_unif test_eq_only metasenv subst mt1 (false,c1) in
 651               let metasenv,subst =
 652                 fo_unif test_eq_only metasenv subst (false,c2) mt2 in
 653               let metasenv,subst =
 654                 List.fold_left
 655                   (fun (metasenv, subst) (x,y) ->
 656                      unify rdb test_eq_only metasenv subst context x y)
 657                   (metasenv, subst) premises
 658               in
 659               pp(lazy("FUNZIONA!"));
 660               Some (metasenv, subst)
 661      (*D*)  in outside true; rc with exn -> outside false; raise exn
 662             with
 663              KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
 664       in
 665         cand_iter candidates
 666      (*D*)  in outside true; rc with exn -> outside false; raise exn
 667     in
 668     let put_in_whd m1 m2 =
 669       NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
 670       NCicReduction.reduce_machine ~delta:max_int ~subst context m2
 671     in
 672     let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
 673       try fo_unif test_eq_only metasenv subst m1 m2
 674       with
 675       | UnificationFailure _ as exn -> raise exn
 676       | KeepReducing _ | Uncertain _ as exn ->
 677         let (t1,norm1 as tm1),(t2,norm2 as tm2) =
 678          put_in_whd (0,[],t1,[]) (0,[],t2,[])
 679         in
 680          match
 681            try_hints metasenv subst
 682             (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
 683          with
 684           | Some x -> x
 685           | None ->
 686               match exn with
 687               | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
 688               | Uncertain _ as exn -> raise exn
 689               | _ -> assert false
 690     in
 691     let height_of = function
 692      | NCic.Const (Ref.Ref (_,Ref.Def h))
 693      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
 694      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
 695      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
 696      | _ -> 0
 697     in
 698     let small_delta_step ~subst
 699       ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
 700     =
 701      assert (not (norm1 && norm2));
 702      if norm1 then
 703       x1,NCicReduction.reduce_machine ~delta:0 ~subst context m2
 704      else if norm2 then
 705       NCicReduction.reduce_machine ~delta:0 ~subst context m1,x2
 706      else
 707       let h1 = height_of t1 in
 708       let h2 = height_of t2 in
 709       let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
 710       NCicReduction.reduce_machine ~delta ~subst context m1,
 711       NCicReduction.reduce_machine ~delta ~subst context m2
 712     in
 713     let rec unif_machines metasenv subst =
 714       function
 715       | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
 716      (*D*) inside 'M'; try let rc =
 717          pp (lazy("UM: " ^
 718            NCicPp.ppterm ~metasenv ~subst ~context
 719              (NCicReduction.unwind (k1,e1,t1,s1)) ^
 720            " === " ^
 721            NCicPp.ppterm ~metasenv ~subst ~context
 722              (NCicReduction.unwind (k2,e2,t2,s2))));
 723 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
 724           let relevance = [] (* TO BE UNDERSTOOD
 725             match t1 with
 726             | C.Const r -> NCicEnvironment.get_relevance r
 727             | _ -> [] *) in
 728           let unif_from_stack t1 t2 b metasenv subst =
 729               try
 730                 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
 731                 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
 732                 unif_machines metasenv subst (put_in_whd t1 t2)
 733               with UnificationFailure _ | Uncertain _ when not b ->
 734                 metasenv, subst
 735           in
 736           let rec check_stack l1 l2 r todo =
 737             match l1,l2,r with
 738             | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
 739             | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
 740             | l1, l2, _ ->
 741                NCicReduction.unwind (k1,e1,t1,List.rev l1),
 742                 NCicReduction.unwind (k2,e2,t2,List.rev l2),
 743                 todo
 744           in
 745         let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
 746         try
 747          let metasenv,subst =
 748           fo_unif_w_hints test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) in
 749          List.fold_left
 750           (fun (metasenv,subst) (x1,x2,r) ->
 751             unif_from_stack x1 x2 r metasenv subst
 752           ) (metasenv,subst) todo
 753         with
 754          | KeepReducing _ -> assert false
 755          | KeepReducingThis _ ->
 756             assert (not (norm1 && norm2));
 757             unif_machines metasenv subst (small_delta_step ~subst m1 m2)
 758          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
 759            -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
 760          | UnificationFailure msg
 761            when could_reduce (NCicReduction.unwind (fst m1))
 762              || could_reduce (NCicReduction.unwind (fst m2))
 763            -> raise (Uncertain msg)
 764       (*D*)  in outside true; rc with exn -> outside false; raise exn
 765      in
 766      try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
 767      with
 768       | KeepReducingThis (msg,tm1,tm2) ->
 769          (try
 770            unif_machines metasenv subst (tm1,tm2)
 771           with
 772           | UnificationFailure _ -> raise (UnificationFailure msg)
 773           | Uncertain _ -> raise (Uncertain msg)
 774           | KeepReducing _ -> assert false)
 775       | KeepReducing _ -> assert false
 776
 777  (*D*)  in outside true; rc with KeepReducing _ -> assert false | exn -> outside false; raise exn
 778
 779 and delift_type_wrt_terms rdb metasenv subst context t args =
 780   let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
 781   let (metasenv, subst), t =
 782    try
 783     NCicMetaSubst.delift
 784       ~unify:(fun m s c t1 t2 ->
 785          let ind = !indent in
 786          let res =
 787            try Some (unify rdb false m s c t1 t2 )
 788            with UnificationFailure _ | Uncertain _ -> None
 789          in
 790          indent := ind; res)
 791       metasenv subst context 0 (0,NCic.Ctx lc) t
 792    with
 793       NCicMetaSubst.MetaSubstFailure _
 794     | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
 795   in
 796    metasenv, subst, t
 797 ;;
 798
 799
 800 let unify rdb ?(test_eq_only=false) =
 801   indent := "";
 802   unify rdb test_eq_only;;
 803
 804 let fix_sorts = fix_sorts true (UnificationFailure (lazy "no sup"));;