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