helm/software/components/ng_refiner/nCicUnification.ml

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