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
  18 let (===) x y = Pervasives.compare x y = 0 ;;
  19
  20 let fail_exc metasenv subst context t1 t2 =
  21   UnificationFailure (lazy (
  22   "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
  23   " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
  24 ;;
  25
  26 let mk_appl hd tl =
  27   match hd with
  28   | NCic.Appl l -> NCic.Appl (l@tl)
  29   | _ -> NCic.Appl (hd :: tl)
  30 ;;
  31
  32 let flexible l =
  33   List.exists
  34     (function
  35        | NCic.Meta _
  36        | NCic.Appl (NCic.Meta _::_) -> true
  37        | _ -> false) l
  38 ;;
  39
  40 exception WrongShape;;
  41
  42 let eta_reduce after_beta_expansion after_beta_expansion_body
  43      before_beta_expansion
  44  =
  45  try
  46   match before_beta_expansion,after_beta_expansion_body with
  47   | NCic.Appl l1, NCic.Appl l2 ->
  48       let rec all_but_last check_last = function
  49         | [] -> assert false
  50         | [NCic.Rel 1] -> []
  51         | [_] -> if check_last then raise WrongShape else []
  52         | he::tl -> he::(all_but_last check_last tl)
  53       in
  54       let all_but_last check_last l =
  55         match all_but_last check_last l with
  56         | [] -> assert false
  57         | [he] -> he
  58         | l -> NCic.Appl l
  59       in
  60       let t =
  61         NCicSubstitution.subst (NCic.Sort NCic.Prop) (all_but_last true l2) in
  62       let all_but_last = all_but_last false l in
  63       if t = all_but_last then all_but_last else after_beta_expansion
  64   | _ -> after_beta_expansion
  65  with WrongShape -> after_beta_expansion
  66 ;;
  67
  68 let rec beta_expand num test_equality_only metasenv subst context t arg =
  69   let rec aux (n,context as k) (metasenv, subst as acc) t' =
  70    try
  71     let metasenv, subst =
  72      unify (* test_equality_only *) metasenv subst context
  73       (NCicSubstitution.lift n arg) t'
  74     in
  75      (metasenv, subst), C.Rel (1 + n)
  76    with Uncertain _ | UnificationFailure _ ->
  77        match t' with
  78        | NCic.Rel m  ->
  79            (metasenv, subst), if m <= n then NCic.Rel m else NCic.Rel (m+1)
  80        (* andrea: in general, beta_expand can create badly typed
  81         terms. This happens quite seldom in practice, UNLESS we
  82         iterate on the local context. For this reason, we renounce
  83         to iterate and just lift *)
  84        | NCic.Meta (i,(shift,lc)) ->
  85            (metasenv,subst), NCic.Meta (i,(shift+1,lc))
  86        | t ->
  87            NCicUntrusted.map_term_fold_a
  88              (fun e (n,ctx) -> n+i,e::ctx) k aux acc t
  89
  90   in
  91   let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
  92   let fresh_name = "Hbeta" ^ string_of_int num in
  93   let (metasenv,subst), t = aux (0, context) (metasenv, subst) t in
  94   let t = eta_reduce (C.Lambda (fresh_name,argty,t)) t t in
  95   metasenv, subst, t
  96
  97 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
  98   let _, subst, metasenv, hd =
  99     List.fold_right
 100       (fun arg (num,subst,metasenv,t) ->
 101          let subst, metasenv, t =
 102            beta_expand num test_equality_only metasenv subst context t arg
 103          in
 104            num+1,subst,metasenv,t)
 105       args (1,subst,metasenv,t)
 106   in
 107     metasenv, subst, hd
 108
 109 and instantiate test_eq_only metasenv subst context n lc t swap =
 110   let unif m s c t1 t2 =
 111     if swap then unify m s c t2 t1 else unify m s c t1 t2
 112   in
 113   let ty_t =
 114     try NCicTypeChecker.typeof ~subst ~metasenv context t
 115     with NCicTypeChecker.TypeCheckerFailure _ -> assert false
 116   in
 117   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
 118   let ty = NCicSubstitution.subst_meta lc ty in
 119   let metasenv, subst = unify metasenv susbt context ty ty_t in
 120   let (metasenv, subst), t =
 121     NCicMetaSubst.delift metasenv subst context n lc t
 122   in
 123   (* Unifying the types may have already instantiated n. *)
 124   try
 125     let _, _,oldt,_ = CicUtil.lookup_subst n subst in
 126     let oldt = NCicSubstitution.subst_meta lc oldt in
 127     (* conjecture: always fail --> occur check *)
 128     unify test_eq_only metasenv subst context oldt t
 129   with CicUtil.Subst_not_found _ ->
 130     (* by cumulativity when unify(?,Type_i)
 131      * we could ? := Type_j with j <= i... *)
 132     let subst = (n, (name, ctx, t, ty)) :: subst in
 133     let metasenv =
 134       List.filter (fun (m,_) -> not (n = m)) metasenv
 135     in
 136     subst, metasenv
 137
 138 and unify metasenv subst context t1 t2 =
 139  let rec aux test_eq_only metasenv subst context t1 t2 =
 140    let fo_unif test_eq_only metasenv subst t1 t2 =
 141      if t1 === t2 then
 142        metasenv, subst
 143      else
 144        match (t1,t2) with
 145        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
 146            if NCicEnvironment.universe_leq a b then metasenv, subst
 147            else raise (fail_exc metasenv subst context t1 t2)
 148        | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
 149            if NCicEnvironment.universe_eq a b then metasenv, subst
 150            else raise (fail_exc metasenv subst context t1 t2)
 151        | (C.Sort C.Prop,C.Sort (C.Type _)) ->
 152            if (not test_eq_only) then metasenv, subst
 153            else raise (fail_exc metasenv subst context t1 t2)
 154
 155        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
 156        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 157            let metasenv, subst = aux true metasenv subst context s1 s2 in
 158            aux test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
 159        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
 160            let metasenv,subst=aux test_eq_only metasenv subst context ty1 ty2 in
 161            let metasenv,subst=aux test_eq_only metasenv subst context s1 s2 in
 162            let context = (name1, C.Def (s1,ty1))::context in
 163            aux test_eq_only metasenv subst context t1 t2
 164
 165        | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
 166           (try
 167            let l1 = NCicUtils.expand_local_context l1 in
 168            let l2 = NCicUtils.expand_local_context l2 in
 169            let metasenv, subst, to_restrict, _ =
 170             List.fold_right2
 171              (fun t1 t2 (metasenv, subst, to_restrict, i) ->
 172                 try
 173                   aux test_eq_only metasenv subst context
 174                     (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2),
 175                   to_restrict, i-1
 176                 with UnificationFailure _ | Uncertain _ ->
 177                   metasenv, subst, i::to_restrict, i-1)
 178              l1 l2 (metasenv, subst, [], List.length l1)
 179            in
 180            let metasenv, subst, _ =
 181              NCicMetaSubst.restrict metasenv subst n1 to_restrict
 182            in
 183              metasenv, subst
 184           with
 185            | Invalid_argument _ -> assert false
 186            | NCicMetaSubst.MetaSubstFailure msg ->
 187               try
 188                 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
 189                 let term1 = NCicSubstitution.subst_meta lc1 term in
 190                 let term2 = NCicSubstitution.subst_meta lc2 term in
 191                   aux test_eq_only metasenv subst context term1 term2
 192               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
 193
 194        | C.Meta (n,lc), t ->
 195            try
 196              let _,_,term,_ = NCicUtils.lookup_subst n subst in
 197              let term = NCicSubstitution.subst_meta lc term in
 198                aux test_eq_only metasenv subst context term t
 199            with NCicUtils.Subst_not_found _->
 200              instantiate test_eq_only metasenv subst context n lc t false
 201
 202        | t, C.Meta (n,lc) ->
 203            try
 204              let _,_,term,_ = NCicUtils.lookup_subst n subst in
 205              let term = NCicSubstitution.subst_meta lc term in
 206                aux test_eq_only metasenv subst context t term
 207            with NCicUtils.Subst_not_found _->
 208              instantiate test_eq_only metasenv subst context n lc t true
 209
 210        | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
 211             let _,_,term,_ = NCicUtils.lookup_subst i subst in
 212             let term = NCicSubstitution.subst_meta l term in
 213               aux test_eq_only metasenv subst context (mk_appl term args) t2
 214
 215        | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
 216             let _,_,term,_ = NCicUtils.lookup_subst i subst in
 217             let term = NCicSubstitution.subst_meta l term in
 218               aux test_eq_only metasenv subst context t1 (mk_appl term args)
 219
 220        |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
 221           NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
 222             try
 223               List.fold_left2
 224                 (fun (metasenv, subst) t1 t2 ->
 225                   aux test_eq_only metasenv subst context t1 t2)
 226                 (metasenv,subst) l1 l2
 227             with Invalid_argument _ ->
 228               raise (fail_exc metasenv subst context t1 t2)
 229
 230        | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
 231            (* we verify that none of the args is a Meta,
 232               since beta expanding w.r.t a metavariable makes no sense  *)
 233               let subst, metasenv, beta_expanded =
 234                 beta_expand_many
 235                   test_equality_only metasenv subst context t2 args ugraph
 236               in
 237                 aux test_eq_only metasenv subst context
 238                   (C.Meta (i,l)) beta_expanded
 239        | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
 240                  let subst,metasenv,beta_expanded =
 241                    beta_expand_many
 242                      test_equality_only
 243                      metasenv subst context t1 args ugraph
 244                  in
 245                    fo_unif_subst test_equality_only subst context metasenv
 246                      (C.Meta (i,l)) beta_expanded ugraph1
 247           | _,_ ->
 248 .......
 249        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
 250            when (Ref.eq r1 r2 &&
 251              List.length (E.get_relevance r1) >= List.length tl1) ->
 252          let relevance = E.get_relevance r1 in
 253          let relevance = match r1 with
 254              | Ref.Ref (_,Ref.Con (_,_,lno)) ->
 255                  let _,relevance = HExtlib.split_nth lno relevance in
 256                    HExtlib.mk_list false lno @ relevance
 257              | _ -> relevance
 258          in
 259          let fail = ref ~-1 in
 260          let res = (try
 261              HExtlib.list_forall_default3
 262               (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
 263               tl1 tl2 true relevance
 264             with Invalid_argument _ -> false)
 265          in res
 266          (* if res then true
 267          else
 268            let relevance = get_relevance_p ~subst context _hd1 tl1 in
 269            let _,relevance = HExtlib.split_nth !fail relevance in
 270            let b,relevance = (match relevance with
 271              | [] -> assert false
 272              | b::tl -> b,tl) in
 273            let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
 274            let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in
 275            if (not b) then
 276              (dance ();
 277               try
 278                HExtlib.list_forall_default3
 279                 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
 280                 tl1 tl2 true relevance
 281              with Invalid_argument _ -> false)
 282            else false *)
 283        | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
 284            aux test_eq_only context hd1 hd2 &&
 285            let relevance = get_relevance ~subst context hd1 tl1 in
 286            (try
 287              HExtlib.list_forall_default3
 288               (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
 289               tl1 tl2 true relevance
 290             with Invalid_argument _ -> false)
 291
 292        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
 293           C.Match (ref2,outtype2,term2,pl2)) ->
 294            let _,_,itl,_,_ = E.get_checked_indtys ref1 in
 295            let _,_,ty,_ = List.nth itl tyno in
 296            let rec remove_prods ~subst context ty =
 297              let ty = whd ~subst context ty in
 298              match ty with
 299              | C.Sort _ -> ty
 300              | C.Prod (name,so,ta) ->
 301                    remove_prods ~subst ((name,(C.Decl so))::context) ta
 302              | _ -> assert false
 303            in
 304            let is_prop =
 305              match remove_prods ~subst [] ty with
 306              | C.Sort C.Prop -> true
 307              | _ -> false
 308            in
 309            let rec remove_prods ~subst context ty =
 310              let ty = whd ~subst context ty in
 311              match ty with
 312              | C.Sort _ -> ty
 313              | C.Prod (name,so,ta) ->
 314                    remove_prods ~subst ((name,(C.Decl so))::context) ta
 315              | _ -> assert false
 316            in
 317            if not (Ref.eq ref1 ref2) then
 318              raise (uncert_exc metasenv subst context t1 t2)
 319            else
 320              let metasenv, subst =
 321                aux test_eq_only metasenv subst context outtype1 outtype2 in
 322              let metasenv, subst =
 323                try aux test_eq_only metasenv subst context term1 term2
 324                with UnificationFailure _ | Uncertain _ when is_prop ->
 325                  metasenv, subst
 326              in
 327              try
 328               List.fold_left2
 329                (fun (metasenv,subst) -> aux test_eq_only metasenv subst context)
 330                (metasenv, subst) pl1 pl2
 331              with Invalid_argument _ ->
 332                raise (uncert_exc metasenv subst context t1 t2)
 333        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
 334        | _ -> raise (uncert_exc metasenv subst context t1 t2)
 335     in
 336     let rec unif_machines metasenv subst = function
 337       | ((k1,e1,NCic.Meta _ as t1,s1 as m1),(k2,e2,t2,s2 as m2),delta)
 338       | ((k1,e1,t1,s1 as m1),(k2,e2,NCic.Meta _ as t2,s2 as m2),delta) ->
 339           try
 340             fo_unif test_eq_only metasenv subst (R.unwind m1) (R.unwind m2)
 341           with UnificationFailure _ | Uncertain _ when delta > 0 ->
 342             let delta = delta - 1 in
 343             let red = R.reduce ~delta ~subst context in
 344             unif_machines metasenv subst (red m1,red m2,delta)
 345       | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
 346         try
 347           let metasenv, subst =
 348             fo_unif test_eq_only metasenv subst
 349               (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[]))
 350           in
 351           let relevance =
 352             match t1 with
 353             | C.Const r -> NCicEnvironment.get_relevance r
 354             | _ -> [] in
 355           try
 356             let rec check_stack f l1 l2 r a =
 357               match l1,l2,r with
 358               | x1::tl1, x2::tl2, r::tr ->
 359                   check_stack f tl1 tl2 tr (f x1 x2 r a)
 360               | x1::tl1, x2::tl2, [] ->
 361                   check_stack f tl1 tl2 tr (f x1 x2 true a)
 362               | [], [], _ -> a
 363               | _ -> raise (Invalid_argument "check_stack")
 364             in
 365             check_stack
 366               (fun t1 t2 b (metasenv,subst) ->
 367                 try
 368                   let t1 = RS.from_stack t1 in
 369                   let t2 = RS.from_stack t2 in
 370                   unif_machines metasenv subst (small_delta_step t1 t2)
 371                 with UnificationFailure _ | Uncertain _ when not b ->
 372                   metasenv, subst)
 373               s1 s2 relevance (metasenv,subst)
 374           with Invalid_argument _ ->
 375             raise (UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm
 376             ~metasenv ~subst ~context (R.unwind m1) ^ " with " ^ NCicPp.ppterm
 377             ~metasenv ~subst ~context (R.unwind m2))))
 378         with UnificationFailure _ | Uncertain _ when delta > 0 ->
 379           let delta = delta - 1 in
 380           let red = R.reduce ~delta ~subst context in
 381           unif_machines metasenv subst (red m1,red m2,delta)
 382      in
 383      let height_of = function
 384       | NCic.Const (Ref.Ref (_,Ref.Def h))
 385       | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
 386       | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
 387       | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
 388       | NCic.Meta _ -> max_int
 389       | _ -> 0
 390      in
 391      let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
 392        let h1 = height_of t1 in
 393        let h2 = height_of t2 in
 394        let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
 395        R.reduce ~delta ~subst context m1,
 396        R.reduce ~delta ~subst context m2,
 397        delta
 398      in
 399      try fo_unif test_eq_only metasenv subst t1 t2
 400      with UnificationFailure msg |Uncertain msg as exn ->
 401        try
 402          unif_machines metasenv subst
 403           (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
 404        with
 405        | UnificationFailure _ -> raise (UnificationFailure msg)
 406        | Uncertain _ -> raise exn
 407  in
 408   aux false metasenv subst context t1 t2
 409 ;;
 410
 411
 412
 413 (*
 414
 415 open Printf
 416
 417 exception UnificationFailure of string Lazy.t;;
 418 exception Uncertain of string Lazy.t;;
 419 exception AssertFailure of string Lazy.t;;
 420
 421 let verbose = false;;
 422 let debug_print = fun _ -> ()
 423
 424 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
 425 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
 426 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
 427 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
 428
 429 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
 430
 431 let type_of_aux' metasenv subst context term ugraph =
 432 let foo () =
 433   try
 434     profile.HExtlib.profile
 435       (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
 436   with
 437       CicTypeChecker.TypeCheckerFailure msg ->
 438         let msg =
 439          lazy
 440           (sprintf
 441            "Kernel Type checking error:
 442 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
 443              (CicMetaSubst.ppterm ~metasenv subst term)
 444              (CicMetaSubst.ppterm ~metasenv [] term)
 445              (CicMetaSubst.ppcontext ~metasenv subst context)
 446              (CicMetaSubst.ppmetasenv subst metasenv)
 447              (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
 448         raise (AssertFailure msg)
 449     | CicTypeChecker.AssertFailure msg ->
 450         let msg = lazy
 451          (sprintf
 452            "Kernel Type checking assertion failure:
 453 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
 454              (CicMetaSubst.ppterm ~metasenv subst term)
 455              (CicMetaSubst.ppterm ~metasenv [] term)
 456              (CicMetaSubst.ppcontext ~metasenv subst context)
 457              (CicMetaSubst.ppmetasenv subst metasenv)
 458              (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
 459         raise (AssertFailure msg)
 460 in profiler_toa.HExtlib.profile foo ()
 461 ;;
 462
 463 let exists_a_meta l =
 464   List.exists
 465     (function
 466        | Cic.Meta _
 467        | Cic.Appl (Cic.Meta _::_) -> true
 468        | _ -> false) l
 469
 470 let rec deref subst t =
 471   let snd (_,a,_) = a in
 472   match t with
 473       Cic.Meta(n,l) ->
 474         (try
 475            deref subst
 476              (CicSubstitution.subst_meta
 477                 l (snd (CicUtil.lookup_subst n subst)))
 478          with
 479              CicUtil.Subst_not_found _ -> t)
 480     | Cic.Appl(Cic.Meta(n,l)::args) ->
 481         (match deref subst (Cic.Meta(n,l)) with
 482            | Cic.Lambda _ as t ->
 483                deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
 484            | r -> Cic.Appl(r::args))
 485     | Cic.Appl(((Cic.Lambda _) as t)::args) ->
 486            deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
 487     | t -> t
 488 ;;
 489
 490 let deref subst t =
 491  let foo () = deref subst t
 492  in profiler_deref.HExtlib.profile foo ()
 493
 494 exception WrongShape;;
 495 let eta_reduce after_beta_expansion after_beta_expansion_body
 496      before_beta_expansion
 497  =
 498  try
 499   match before_beta_expansion,after_beta_expansion_body with
 500      Cic.Appl l, Cic.Appl l' ->
 501       let rec all_but_last check_last =
 502        function
 503           [] -> assert false
 504         | [Cic.Rel 1] -> []
 505         | [_] -> if check_last then raise WrongShape else []
 506         | he::tl -> he::(all_but_last check_last tl)
 507       in
 508        let all_but_last check_last l =
 509         match all_but_last check_last l with
 510            [] -> assert false
 511          | [he] -> he
 512          | l -> Cic.Appl l
 513        in
 514        let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
 515        let all_but_last = all_but_last false l in
 516         (* here we should test alpha-equivalence; however we know by
 517            construction that here alpha_equivalence is equivalent to = *)
 518         if t = all_but_last then
 519          all_but_last
 520         else
 521          after_beta_expansion
 522    | _,_ -> after_beta_expansion
 523  with
 524   WrongShape -> after_beta_expansion
 525
 526 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
 527  let module S = CicSubstitution in
 528  let module C = Cic in
 529 let foo () =
 530   let rec aux metasenv subst n context t' ugraph =
 531    try
 532
 533     let subst,metasenv,ugraph1 =
 534      fo_unif_subst test_equality_only subst context metasenv
 535       (CicSubstitution.lift n arg) t' ugraph
 536
 537     in
 538      subst,metasenv,C.Rel (1 + n),ugraph1
 539    with
 540       Uncertain _
 541     | UnificationFailure _ ->
 542        match t' with
 543         | C.Rel m  -> subst,metasenv,
 544            (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
 545         | C.Var (uri,exp_named_subst) ->
 546            let subst,metasenv,exp_named_subst',ugraph1 =
 547             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 548            in
 549             subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
 550         | C.Meta (i,l) ->
 551             (* andrea: in general, beta_expand can create badly typed
 552              terms. This happens quite seldom in practice, UNLESS we
 553              iterate on the local context. For this reason, we renounce
 554              to iterate and just lift *)
 555             let l =
 556               List.map
 557                 (function
 558                      Some t -> Some (CicSubstitution.lift 1 t)
 559                    | None -> None) l in
 560             subst, metasenv, C.Meta (i,l), ugraph
 561         | C.Sort _
 562         | C.Implicit _ as t -> subst,metasenv,t,ugraph
 563         | C.Cast (te,ty) ->
 564             let subst,metasenv,te',ugraph1 =
 565               aux metasenv subst n context te ugraph in
 566             let subst,metasenv,ty',ugraph2 =
 567               aux metasenv subst n context ty ugraph1 in
 568             (* TASSI: sure this is in serial? *)
 569             subst,metasenv,(C.Cast (te', ty')),ugraph2
 570         | C.Prod (nn,s,t) ->
 571            let subst,metasenv,s',ugraph1 =
 572              aux metasenv subst n context s ugraph in
 573            let subst,metasenv,t',ugraph2 =
 574              aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
 575                ugraph1
 576            in
 577            (* TASSI: sure this is in serial? *)
 578            subst,metasenv,(C.Prod (nn, s', t')),ugraph2
 579         | C.Lambda (nn,s,t) ->
 580            let subst,metasenv,s',ugraph1 =
 581              aux metasenv subst n context s ugraph in
 582            let subst,metasenv,t',ugraph2 =
 583             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
 584            in
 585            (* TASSI: sure this is in serial? *)
 586             subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
 587         | C.LetIn (nn,s,ty,t) ->
 588            let subst,metasenv,s',ugraph1 =
 589              aux metasenv subst n context s ugraph in
 590            let subst,metasenv,ty',ugraph1 =
 591              aux metasenv subst n context ty ugraph in
 592            let subst,metasenv,t',ugraph2 =
 593             aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
 594               ugraph1
 595            in
 596            (* TASSI: sure this is in serial? *)
 597             subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
 598         | C.Appl l ->
 599            let subst,metasenv,revl',ugraph1 =
 600             List.fold_left
 601              (fun (subst,metasenv,appl,ugraph) t ->
 602                let subst,metasenv,t',ugraph1 =
 603                  aux metasenv subst n context t ugraph in
 604                 subst,metasenv,(t'::appl),ugraph1
 605              ) (subst,metasenv,[],ugraph) l
 606            in
 607             subst,metasenv,(C.Appl (List.rev revl')),ugraph1
 608         | C.Const (uri,exp_named_subst) ->
 609            let subst,metasenv,exp_named_subst',ugraph1 =
 610             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 611            in
 612             subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
 613         | C.MutInd (uri,i,exp_named_subst) ->
 614            let subst,metasenv,exp_named_subst',ugraph1 =
 615             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 616            in
 617             subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
 618         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 619            let subst,metasenv,exp_named_subst',ugraph1 =
 620             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 621            in
 622             subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
 623         | C.MutCase (sp,i,outt,t,pl) ->
 624            let subst,metasenv,outt',ugraph1 =
 625              aux metasenv subst n context outt ugraph in
 626            let subst,metasenv,t',ugraph2 =
 627              aux metasenv subst n context t ugraph1 in
 628            let subst,metasenv,revpl',ugraph3 =
 629             List.fold_left
 630              (fun (subst,metasenv,pl,ugraph) t ->
 631                let subst,metasenv,t',ugraph1 =
 632                  aux metasenv subst n context t ugraph in
 633                subst,metasenv,(t'::pl),ugraph1
 634              ) (subst,metasenv,[],ugraph2) pl
 635            in
 636            subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
 637            (* TASSI: not sure this is serial *)
 638         | C.Fix (i,fl) ->
 639 (*CSC: not implemented
 640            let tylen = List.length fl in
 641             let substitutedfl =
 642              List.map
 643               (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 644                fl
 645             in
 646              C.Fix (i, substitutedfl)
 647 *)
 648             subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
 649         | C.CoFix (i,fl) ->
 650 (*CSC: not implemented
 651            let tylen = List.length fl in
 652             let substitutedfl =
 653              List.map
 654               (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 655                fl
 656             in
 657              C.CoFix (i, substitutedfl)
 658
 659 *)
 660             subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
 661
 662   and aux_exp_named_subst metasenv subst n context ens ugraph =
 663    List.fold_right
 664     (fun (uri,t) (subst,metasenv,l,ugraph) ->
 665       let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
 666        subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
 667   in
 668   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
 669   let fresh_name =
 670    FreshNamesGenerator.mk_fresh_name ~subst
 671     metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
 672   in
 673    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
 674    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
 675    subst, metasenv, t'', ugraph2
 676 in profiler_beta_expand.HExtlib.profile foo ()
 677
 678
 679 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
 680   let _,subst,metasenv,hd,ugraph =
 681     List.fold_right
 682       (fun arg (num,subst,metasenv,t,ugraph) ->
 683          let subst,metasenv,t,ugraph1 =
 684            beta_expand num test_equality_only
 685              metasenv subst context t arg ugraph
 686          in
 687            num+1,subst,metasenv,t,ugraph1
 688       ) args (1,subst,metasenv,t,ugraph)
 689   in
 690     subst,metasenv,hd,ugraph
 691
 692 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
 693   match xxx with
 694   | [] -> ()
 695   | (m2,_,c2,c2')::_ ->
 696      let m1,c1,c1' = carr,to1,to2 in
 697      let unopt =
 698        function Some (_,t) -> CicPp.ppterm t
 699        | None -> "id"
 700      in
 701      HLog.warn
 702        ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
 703        CoercDb.string_of_carr car2^": " ^
 704        CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
 705        unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
 706        unopt c2^" + "^unopt c2')
 707
 708 (* NUOVA UNIFICAZIONE *)
 709 (* A substitution is a (int * Cic.term) list that associates a
 710    metavariable i with its body.
 711    A metaenv is a (int * Cic.term) list that associate a metavariable
 712    i with is type.
 713    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
 714    a new substitution which is _NOT_ unwinded. It must be unwinded before
 715    applying it. *)
 716
 717 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
 718  let module C = Cic in
 719  let module R = CicReduction in
 720  let module S = CicSubstitution in
 721  let t1 = deref subst t1 in
 722  let t2 = deref subst t2 in
 723  let (&&&) a b = (a && b) || ((not a) && (not b)) in
 724 (* let bef = Sys.time () in *)
 725  let b,ugraph =
 726   if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
 727    false,ugraph
 728   else
 729 let foo () =
 730    R.are_convertible ~subst ~metasenv context t1 t2 ugraph
 731 in profiler_are_convertible.HExtlib.profile foo ()
 732  in
 733 (* let aft = Sys.time () in
 734 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
 735 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
 736 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
 737    if b then
 738      subst, metasenv, ugraph
 739    else
 740    match (t1, t2) with
 741      | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
 742          let _,subst,metasenv,ugraph1 =
 743            (try
 744               List.fold_left2
 745                 (fun (j,subst,metasenv,ugraph) t1 t2 ->
 746                    match t1,t2 with
 747                        None,_
 748                      | _,None -> j+1,subst,metasenv,ugraph
 749                      | Some t1', Some t2' ->
 750                          (* First possibility:  restriction    *)
 751                          (* Second possibility: unification    *)
 752                          (* Third possibility:  convertibility *)
 753                          let b, ugraph1 =
 754                          R.are_convertible
 755                            ~subst ~metasenv context t1' t2' ugraph
 756                          in
 757                          if b then
 758                            j+1,subst,metasenv, ugraph1
 759                          else
 760                            (try
 761                               let subst,metasenv,ugraph2 =
 762                                 fo_unif_subst
 763                                   test_equality_only
 764                                   subst context metasenv t1' t2' ugraph
 765                               in
 766                                 j+1,subst,metasenv,ugraph2
 767                             with
 768                                 Uncertain _
 769                               | UnificationFailure _ ->
 770 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
 771                                   let metasenv, subst =
 772                                     CicMetaSubst.restrict
 773                                       subst [(n,j)] metasenv in
 774                                     j+1,subst,metasenv,ugraph1)
 775                 ) (1,subst,metasenv,ugraph) ln lm
 776             with
 777                 Exit ->
 778                   raise
 779                     (UnificationFailure (lazy "1"))
 780                     (*
 781                     (sprintf
 782                       "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
 783                       (CicMetaSubst.ppterm ~metasenv subst t1)
 784                       (CicMetaSubst.ppterm ~metasenv subst t2))) *)
 785               | Invalid_argument _ ->
 786                   raise
 787                     (UnificationFailure (lazy "2")))
 788                     (*
 789                     (sprintf
 790                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
 791                       (CicMetaSubst.ppterm ~metasenv subst t1)
 792                       (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
 793          in subst,metasenv,ugraph1
 794      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
 795          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
 796      | (C.Meta (n,l), t)
 797      | (t, C.Meta (n,l)) ->
 798          let swap =
 799            match t1,t2 with
 800                C.Meta (n,_), C.Meta (m,_) when n < m -> false
 801              | _, C.Meta _ -> false
 802              | _,_ -> true
 803          in
 804          let lower = fun x y -> if swap then y else x in
 805          let upper = fun x y -> if swap then x else y in
 806          let fo_unif_subst_ordered
 807              test_equality_only subst context metasenv m1 m2 ugraph =
 808            fo_unif_subst test_equality_only subst context metasenv
 809              (lower m1 m2) (upper m1 m2) ugraph
 810          in
 811          begin
 812          let subst,metasenv,ugraph1 =
 813            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
 814            (try
 815               let tyt,ugraph1 =
 816                 type_of_aux' metasenv subst context t ugraph
 817               in
 818                 fo_unif_subst
 819                   test_equality_only
 820                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
 821             with
 822                 UnificationFailure _ as e -> raise e
 823               | Uncertain msg -> raise (UnificationFailure msg)
 824               | AssertFailure _ ->
 825                   debug_print (lazy "siamo allo huge hack");
 826                   (* TODO huge hack!!!!
 827                    * we keep on unifying/refining in the hope that
 828                    * the problem will be eventually solved.
 829                    * In the meantime we're breaking a big invariant:
 830                    * the terms that we are unifying are no longer well
 831                    * typed in the current context (in the worst case
 832                    * we could even diverge) *)
 833                   (subst, metasenv,ugraph)) in
 834          let t',metasenv,subst =
 835            try
 836              CicMetaSubst.delift n subst context metasenv l t
 837            with
 838                (CicMetaSubst.MetaSubstFailure msg)->
 839                  raise (UnificationFailure msg)
 840              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 841          in
 842          let t'',ugraph2 =
 843            match t' with
 844                C.Sort (C.Type u) when not test_equality_only ->
 845                  let u' = CicUniv.fresh () in
 846                  let s = C.Sort (C.Type u') in
 847                   (try
 848                     let ugraph2 =
 849                      CicUniv.add_ge (upper u u') (lower u u') ugraph1
 850                     in
 851                      s,ugraph2
 852                    with
 853                     CicUniv.UniverseInconsistency msg ->
 854                      raise (UnificationFailure msg))
 855              | _ -> t',ugraph1
 856          in
 857          (* Unifying the types may have already instantiated n. Let's check *)
 858          try
 859            let (_, oldt,_) = CicUtil.lookup_subst n subst in
 860            let lifted_oldt = S.subst_meta l oldt in
 861              fo_unif_subst_ordered
 862                test_equality_only subst context metasenv t lifted_oldt ugraph2
 863          with
 864              CicUtil.Subst_not_found _ ->
 865                let (_, context, ty) = CicUtil.lookup_meta n metasenv in
 866                let subst = (n, (context, t'',ty)) :: subst in
 867                let metasenv =
 868                  List.filter (fun (m,_,_) -> not (n = m)) metasenv in
 869                subst, metasenv, ugraph2
 870          end
 871    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 872    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 873       if UriManager.eq uri1 uri2 then
 874        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 875         exp_named_subst1 exp_named_subst2 ugraph
 876       else
 877        raise (UnificationFailure (lazy
 878           (sprintf
 879             "Can't unify %s with %s due to different constants"
 880             (CicMetaSubst.ppterm ~metasenv subst t1)
 881             (CicMetaSubst.ppterm ~metasenv subst t2))))
 882    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 883        if UriManager.eq uri1 uri2 && i1 = i2 then
 884          fo_unif_subst_exp_named_subst
 885            test_equality_only
 886            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 887        else
 888          raise (UnificationFailure
 889            (lazy
 890             (sprintf
 891              "Can't unify %s with %s due to different inductive principles"
 892              (CicMetaSubst.ppterm ~metasenv subst t1)
 893              (CicMetaSubst.ppterm ~metasenv subst t2))))
 894    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 895        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 896        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 897          fo_unif_subst_exp_named_subst
 898            test_equality_only
 899            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 900        else
 901          raise (UnificationFailure
 902           (lazy
 903             (sprintf
 904               "Can't unify %s with %s due to different inductive constructors"
 905               (CicMetaSubst.ppterm ~metasenv subst t1)
 906               (CicMetaSubst.ppterm ~metasenv subst t2))))
 907    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 908    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
 909                               subst context metasenv te t2 ugraph
 910    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
 911                               subst context metasenv t1 te ugraph
 912    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 913        let subst',metasenv',ugraph1 =
 914          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
 915        in
 916          fo_unif_subst test_equality_only
 917            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 918    | (C.LetIn (_,s1,ty1,t1), t2)
 919    | (t2, C.LetIn (_,s1,ty1,t1)) ->
 920        fo_unif_subst
 921         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
 922    | (C.Appl l1, C.Appl l2) ->
 923        (* andrea: this case should be probably rewritten in the
 924           spirit of deref *)
 925        (match l1,l2 with
 926           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
 927               (try
 928                  List.fold_left2
 929                    (fun (subst,metasenv,ugraph) t1 t2 ->
 930                       fo_unif_subst
 931                         test_equality_only subst context metasenv t1 t2 ugraph)
 932                    (subst,metasenv,ugraph) l1 l2
 933                with (Invalid_argument msg) ->
 934                  raise (UnificationFailure (lazy msg)))
 935           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
 936               (* we verify that none of the args is a Meta,
 937                 since beta expanding with respoect to a metavariable
 938                 makes no sense  *)
 939  (*
 940               (try
 941                  let (_,t,_) = CicUtil.lookup_subst i subst in
 942                  let lifted = S.subst_meta l t in
 943                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 944                    fo_unif_subst
 945                     test_equality_only
 946                      subst context metasenv reduced t2 ugraph
 947                with CicUtil.Subst_not_found _ -> *)
 948               let subst,metasenv,beta_expanded,ugraph1 =
 949                 beta_expand_many
 950                   test_equality_only metasenv subst context t2 args ugraph
 951               in
 952                 fo_unif_subst test_equality_only subst context metasenv
 953                   (C.Meta (i,l)) beta_expanded ugraph1
 954           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
 955               (* (try
 956                  let (_,t,_) = CicUtil.lookup_subst i subst in
 957                  let lifted = S.subst_meta l t in
 958                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 959                    fo_unif_subst
 960                      test_equality_only
 961                      subst context metasenv t1 reduced ugraph
 962                with CicUtil.Subst_not_found _ -> *)
 963                  let subst,metasenv,beta_expanded,ugraph1 =
 964                    beta_expand_many
 965                      test_equality_only
 966                      metasenv subst context t1 args ugraph
 967                  in
 968                    fo_unif_subst test_equality_only subst context metasenv
 969                      (C.Meta (i,l)) beta_expanded ugraph1
 970           | _,_ ->
 971               let lr1 = List.rev l1 in
 972               let lr2 = List.rev l2 in
 973               let rec
 974                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
 975                 match (l1,l2) with
 976                     [],_
 977                   | _,[] -> assert false
 978                   | ([h1],[h2]) ->
 979                       fo_unif_subst
 980                         test_equality_only subst context metasenv h1 h2 ugraph
 981                   | ([h],l)
 982                   | (l,[h]) ->
 983                       fo_unif_subst test_equality_only subst context metasenv
 984                         h (C.Appl (List.rev l)) ugraph
 985                   | ((h1::l1),(h2::l2)) ->
 986                       let subst', metasenv',ugraph1 =
 987                         fo_unif_subst
 988                           test_equality_only
 989                           subst context metasenv h1 h2 ugraph
 990                       in
 991                         fo_unif_l
 992                           test_equality_only subst' metasenv' (l1,l2) ugraph1
 993               in
 994               (try
 995                 fo_unif_l
 996                   test_equality_only subst metasenv (lr1, lr2)  ugraph
 997               with
 998               | UnificationFailure s
 999               | Uncertain s as exn ->
1000                   (match l1, l2 with
1001                             (* {{{ pullback *)
1002                   | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1003                      (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1004                     CoercDb.is_a_coercion cc1 <> None &&
1005                     CoercDb.is_a_coercion cc2 <> None &&
1006                     not (UriManager.eq uri1 uri2) ->
1007 (*DEBUGGING ONLY:
1008 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1009 *)
1010                      let inner_coerced t =
1011                       let t = CicMetaSubst.apply_subst subst t in
1012                       let rec aux c x t =
1013                         match t with
1014                         | Cic.Appl l ->
1015                             (match CoercGraph.coerced_arg l with
1016                             | None -> c, x
1017                             | Some (t,_) -> aux (List.hd l) t t)
1018                         | _ ->  c, x
1019                       in
1020                       aux (Cic.Implicit None) (Cic.Implicit None) t
1021                      in
1022                       let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1023                       let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1024                       let car1, car2 =
1025                         match
1026                           CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1027                         with
1028                         | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1029                         | _ -> assert false
1030                       in
1031                       let head1_c, head2_c =
1032                         match
1033                           CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1034                         with
1035                         | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1036                         | _ -> assert false
1037                       in
1038                       let unfold uri ens args =
1039                         let o, _ =
1040                           CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1041                         in
1042                         assert (ens = []);
1043                         match o with
1044                         | Cic.Constant (_,Some bo,_,_,_) ->
1045                             CicReduction.head_beta_reduce ~delta:false
1046                               (Cic.Appl (bo::args))
1047                         | _ -> assert false
1048                       in
1049                       let conclude subst metasenv ugraph last_tl1' last_tl2' =
1050                        let subst',metasenv,ugraph =
1051 (*DEBUGGING ONLY:
1052 prerr_endline
1053   ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1054    " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1055 *)
1056                         fo_unif_subst test_equality_only subst context
1057                          metasenv last_tl1' last_tl2' ugraph
1058                        in
1059                        if subst = subst' then raise exn
1060                        else
1061 (*DEBUGGING ONLY:
1062 let subst,metasenv,ugrph as res =
1063 *)
1064                         fo_unif_subst test_equality_only subst' context
1065                          metasenv (C.Appl l1) (C.Appl l2) ugraph
1066 (*DEBUGGING ONLY:
1067 in
1068 (prerr_endline
1069   (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1070    " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1071 res)
1072 *)
1073                       in
1074                       if CoercDb.eq_carr car1 car2 then
1075                          match last_tl1,last_tl2 with
1076                          | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1077                          | _, C.Meta _
1078                          | C.Meta _, _ ->
1079                            let subst,metasenv,ugraph =
1080                             fo_unif_subst test_equality_only subst context
1081                              metasenv last_tl1 last_tl2 ugraph
1082                            in
1083                             fo_unif_subst test_equality_only subst context
1084                              metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1085                          | _ when CoercDb.eq_carr head1_c head2_c ->
1086                              (* composite VS composition + metas avoiding
1087                               * coercions not only in coerced position    *)
1088                              if c1 <> cc1 && c2 <> cc2 then
1089                                conclude subst metasenv ugraph
1090                                 last_tl1 last_tl2
1091                              else
1092                               let l1, l2 =
1093                                if c1 = cc1 then
1094                                  unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1095                                else
1096                                  Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1097                               in
1098                                fo_unif_subst test_equality_only subst context
1099                                 metasenv l1 l2 ugraph
1100                          | _ -> raise exn
1101                       else
1102                        let grow1 =
1103                          match last_tl1 with Cic.Meta _ -> true | _ -> false in
1104                        let grow2 =
1105                          match last_tl2 with Cic.Meta _ -> true | _ -> false in
1106                        if not (grow1 || grow2) then
1107                           (* no flexible terminals -> no pullback, but
1108                            * we still unify them, in some cases it helps *)
1109                           conclude subst metasenv ugraph last_tl1 last_tl2
1110                        else
1111                         let meets =
1112                           CoercGraph.meets
1113                             metasenv subst context (grow1,car1) (grow2,car2)
1114                         in
1115                         (match meets with
1116                         | [] -> raise exn
1117                         | (carr,metasenv,to1,to2)::xxx ->
1118                            warn_if_not_unique xxx to1 to2 carr car1 car2;
1119                            let last_tl1',(subst,metasenv,ugraph) =
1120                             match grow1,to1 with
1121                              | true,Some (last,coerced) ->
1122                                  last,
1123                                   fo_unif_subst test_equality_only subst context
1124                                   metasenv coerced last_tl1 ugraph
1125                              | _ -> last_tl1,(subst,metasenv,ugraph)
1126                            in
1127                            let last_tl2',(subst,metasenv,ugraph) =
1128                             match grow2,to2 with
1129                              | true,Some (last,coerced) ->
1130                                  last,
1131                                   fo_unif_subst test_equality_only subst context
1132                                   metasenv coerced last_tl2 ugraph
1133                              | _ -> last_tl2,(subst,metasenv,ugraph)
1134                            in
1135                            conclude subst metasenv ugraph last_tl1' last_tl2')
1136                         (* }}} pullback *)
1137                   (* {{{ CSC: This is necessary because of the "elim H" tactic
1138                          where the type of H is only reducible to an
1139                          inductive type. This could be extended from inductive
1140                          types to any rigid term. However, the code is
1141                          duplicated in two places: inside applications and
1142                          outside them. Probably it would be better to
1143                          work with lambda-bar terms instead. *)
1144                   | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1145                   | (_, Cic.MutInd _::_) ->
1146                      let t1' = R.whd ~subst context t1 in
1147                      (match t1' with
1148                           C.Appl (C.MutInd _::_) ->
1149                             fo_unif_subst test_equality_only
1150                               subst context metasenv t1' t2 ugraph
1151                         | _ -> raise (UnificationFailure (lazy "88")))
1152                   | (Cic.MutInd _::_,_) ->
1153                      let t2' = R.whd ~subst context t2 in
1154                      (match t2' with
1155                           C.Appl (C.MutInd _::_) ->
1156                             fo_unif_subst test_equality_only
1157                               subst context metasenv t1 t2' ugraph
1158                         | _ -> raise
1159                             (UnificationFailure
1160                                (lazy ("not a mutind :"^
1161                                 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1162                      (* }}} elim H *)
1163                   | _ -> raise exn)))
1164    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1165        let subst', metasenv',ugraph1 =
1166         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1167           ugraph in
1168        let subst'',metasenv'',ugraph2 =
1169         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1170           ugraph1 in
1171        (try
1172          List.fold_left2
1173           (fun (subst,metasenv,ugraph) t1 t2 ->
1174             fo_unif_subst
1175              test_equality_only subst context metasenv t1 t2 ugraph
1176           ) (subst'',metasenv'',ugraph2) pl1 pl2
1177         with
1178          Invalid_argument _ ->
1179           raise (UnificationFailure (lazy "6.1")))
1180            (* (sprintf
1181               "Error trying to unify %s with %s: the number of branches is not the same."
1182               (CicMetaSubst.ppterm ~metasenv subst t1)
1183               (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1184    | (C.Rel _, _) | (_,  C.Rel _) ->
1185        if t1 = t2 then
1186          subst, metasenv,ugraph
1187        else
1188         raise (UnificationFailure (lazy
1189            (sprintf
1190              "Can't unify %s with %s because they are not convertible"
1191              (CicMetaSubst.ppterm ~metasenv subst t1)
1192              (CicMetaSubst.ppterm ~metasenv subst t2))))
1193    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1194        let subst,metasenv,beta_expanded,ugraph1 =
1195          beta_expand_many
1196            test_equality_only metasenv subst context t2 args ugraph
1197        in
1198          fo_unif_subst test_equality_only subst context metasenv
1199            (C.Meta (i,l)) beta_expanded ugraph1
1200    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1201        let subst,metasenv,beta_expanded,ugraph1 =
1202          beta_expand_many
1203            test_equality_only metasenv subst context t1 args ugraph
1204        in
1205          fo_unif_subst test_equality_only subst context metasenv
1206            beta_expanded (C.Meta (i,l)) ugraph1
1207 (* Works iff there are no arguments applied to it; similar to the
1208    case below
1209    | (_, C.MutInd _) ->
1210        let t1' = R.whd ~subst context t1 in
1211        (match t1' with
1212             C.MutInd _ ->
1213               fo_unif_subst test_equality_only
1214                 subst context metasenv t1' t2 ugraph
1215           | _ -> raise (UnificationFailure (lazy "8")))
1216 *)
1217    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1218        let subst',metasenv',ugraph1 =
1219          fo_unif_subst true subst context metasenv s1 s2 ugraph
1220        in
1221          fo_unif_subst test_equality_only
1222            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1223    | (C.Prod _, _) ->
1224        (match CicReduction.whd ~subst context t2 with
1225         | C.Prod _ as t2 ->
1226             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1227         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1228    | (_, C.Prod _) ->
1229        (match CicReduction.whd ~subst context t1 with
1230         | C.Prod _ as t1 ->
1231             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1232         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1233    | (_,_) ->
1234      (* delta-beta reduction should almost never be a problem for
1235         unification since:
1236          1. long computations require iota reduction
1237          2. it is extremely rare that a close term t1 (that could be unified
1238             to t2) beta-delta reduces to t1' while t2 does not beta-delta
1239             reduces in the same way. This happens only if one meta of t2
1240             occurs in head position during beta reduction. In this unluky
1241             case too much reduction will be performed on t1 and unification
1242             will surely fail. *)
1243      let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1244      let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1245       if t1 = t1' && t2 = t2' then
1246        raise (UnificationFailure
1247         (lazy
1248           (sprintf
1249             "Can't unify %s with %s because they are not convertible"
1250             (CicMetaSubst.ppterm ~metasenv subst t1)
1251             (CicMetaSubst.ppterm ~metasenv subst t2))))
1252       else
1253        try
1254         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1255        with
1256           UnificationFailure _
1257         | Uncertain _ ->
1258            raise (UnificationFailure
1259             (lazy
1260               (sprintf
1261                 "Can't unify %s with %s because they are not convertible"
1262                 (CicMetaSubst.ppterm ~metasenv subst t1)
1263                 (CicMetaSubst.ppterm ~metasenv subst t2))))
1264
1265 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1266  exp_named_subst1 exp_named_subst2 ugraph
1267 =
1268  try
1269   List.fold_left2
1270    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1271      assert (uri1=uri2) ;
1272      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1273    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1274  with
1275   Invalid_argument _ ->
1276    let print_ens ens =
1277     String.concat " ; "
1278      (List.map
1279        (fun (uri,t) ->
1280          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1281        ) ens)
1282    in
1283     raise (UnificationFailure (lazy (sprintf
1284      "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2))))
1285
1286 (* A substitution is a (int * Cic.term) list that associates a               *)
1287 (* metavariable i with its body.                                             *)
1288 (* metasenv is of type Cic.metasenv                                          *)
1289 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
1290 (* a new substitution which is already unwinded and ready to be applied and  *)
1291 (* a new metasenv in which some hypothesis in the contexts of the            *)
1292 (* metavariables may have been restricted.                                   *)
1293 let fo_unif metasenv context t1 t2 ugraph =
1294  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1295
1296 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1297  lazy (
1298   if verbose then
1299    sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
1300     (CicMetaSubst.ppterm ~metasenv subst t1)
1301     (try
1302       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1303       CicPp.ppterm ty_t1
1304     with
1305     | UnificationFailure s
1306     | Uncertain s
1307     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1308     (CicMetaSubst.ppterm ~metasenv subst t2)
1309     (try
1310       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1311       CicPp.ppterm ty_t2
1312     with
1313     | UnificationFailure s
1314     | Uncertain s
1315     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1316     (CicMetaSubst.ppcontext ~metasenv subst context)
1317     (CicMetaSubst.ppmetasenv subst metasenv)
1318     (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1319  else
1320    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1321     (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1322     (try
1323       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1324       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1325     with
1326     | UnificationFailure s
1327     | Uncertain s
1328     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1329     (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1330     (try
1331       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1332       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1333     with
1334     | UnificationFailure s
1335     | Uncertain s
1336     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1337     (CicMetaSubst.ppcontext ~metasenv subst context)
1338     (CicMetaSubst.ppmetasenv subst metasenv)
1339     (Lazy.force msg)
1340  )
1341
1342 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1343   try
1344     fo_unif_subst false subst context metasenv t1 t2 ugraph
1345   with
1346   | AssertFailure msg ->
1347      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1348   | UnificationFailure msg ->
1349      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1350 ;;
1351 *)