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