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