components/cic_unification/cicUnification.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Printf
  29
  30 exception UnificationFailure of string Lazy.t;;
  31 exception Uncertain of string Lazy.t;;
  32 exception AssertFailure of string Lazy.t;;
  33
  34 let verbose = false;;
  35 let debug_print = fun _ -> ()
  36
  37 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
  38 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
  39 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
  40 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
  41
  42 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
  43
  44 let type_of_aux' metasenv subst context term ugraph =
  45 let foo () =
  46   try
  47     profile.HExtlib.profile
  48       (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
  49   with
  50       CicTypeChecker.TypeCheckerFailure msg ->
  51         let msg =
  52          lazy
  53           (sprintf
  54            "Kernel Type checking error:
  55 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
  56              (CicMetaSubst.ppterm subst term)
  57              (CicMetaSubst.ppterm [] term)
  58              (CicMetaSubst.ppcontext subst context)
  59              (CicMetaSubst.ppmetasenv subst metasenv)
  60              (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
  61         raise (AssertFailure msg)
  62     | CicTypeChecker.AssertFailure msg ->
  63         let msg = lazy
  64          (sprintf
  65            "Kernel Type checking assertion failure:
  66 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
  67              (CicMetaSubst.ppterm subst term)
  68              (CicMetaSubst.ppterm [] term)
  69              (CicMetaSubst.ppcontext subst context)
  70              (CicMetaSubst.ppmetasenv subst metasenv)
  71              (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
  72         raise (AssertFailure msg)
  73 in profiler_toa.HExtlib.profile foo ()
  74 ;;
  75
  76 let exists_a_meta l =
  77   List.exists (function Cic.Meta _ -> true | _ -> false) l
  78
  79 let rec deref subst t =
  80   let snd (_,a,_) = a in
  81   match t with
  82       Cic.Meta(n,l) ->
  83         (try
  84            deref subst
  85              (CicSubstitution.subst_meta
  86                 l (snd (CicUtil.lookup_subst n subst)))
  87          with
  88              CicUtil.Subst_not_found _ -> t)
  89     | Cic.Appl(Cic.Meta(n,l)::args) ->
  90         (match deref subst (Cic.Meta(n,l)) with
  91            | Cic.Lambda _ as t ->
  92                deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
  93            | r -> Cic.Appl(r::args))
  94     | Cic.Appl(((Cic.Lambda _) as t)::args) ->
  95            deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
  96     | t -> t
  97 ;;
  98
  99 let deref subst t =
 100  let foo () = deref subst t
 101  in profiler_deref.HExtlib.profile foo ()
 102
 103 exception WrongShape;;
 104 let eta_reduce after_beta_expansion after_beta_expansion_body
 105      before_beta_expansion
 106  =
 107  try
 108   match before_beta_expansion,after_beta_expansion_body with
 109      Cic.Appl l, Cic.Appl l' ->
 110       let rec all_but_last check_last =
 111        function
 112           [] -> assert false
 113         | [Cic.Rel 1] -> []
 114         | [_] -> if check_last then raise WrongShape else []
 115         | he::tl -> he::(all_but_last check_last tl)
 116       in
 117        let all_but_last check_last l =
 118         match all_but_last check_last l with
 119            [] -> assert false
 120          | [he] -> he
 121          | l -> Cic.Appl l
 122        in
 123        let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
 124        let all_but_last = all_but_last false l in
 125         (* here we should test alpha-equivalence; however we know by
 126            construction that here alpha_equivalence is equivalent to = *)
 127         if t = all_but_last then
 128          all_but_last
 129         else
 130          after_beta_expansion
 131    | _,_ -> after_beta_expansion
 132  with
 133   WrongShape -> after_beta_expansion
 134
 135 let unif_ty = ref true
 136
 137 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
 138  let module S = CicSubstitution in
 139  let module C = Cic in
 140 let foo () =
 141   let rec aux metasenv subst n context t' ugraph =
 142    try
 143
 144     let subst,metasenv,ugraph1 =
 145      fo_unif_subst test_equality_only subst context metasenv
 146       (CicSubstitution.lift n arg) t' ugraph
 147
 148     in
 149      subst,metasenv,C.Rel (1 + n),ugraph1
 150    with
 151       Uncertain _
 152     | UnificationFailure _ ->
 153        match t' with
 154         | C.Rel m  -> subst,metasenv,
 155            (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
 156         | C.Var (uri,exp_named_subst) ->
 157            let subst,metasenv,exp_named_subst',ugraph1 =
 158             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 159            in
 160             subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
 161         | C.Meta (i,l) ->
 162             (* andrea: in general, beta_expand can create badly typed
 163              terms. This happens quite seldom in practice, UNLESS we
 164              iterate on the local context. For this reason, we renounce
 165              to iterate and just lift *)
 166             let l =
 167               List.map
 168                 (function
 169                      Some t -> Some (CicSubstitution.lift 1 t)
 170                    | None -> None) l in
 171             subst, metasenv, C.Meta (i,l), ugraph
 172         | C.Sort _
 173         | C.Implicit _ as t -> subst,metasenv,t,ugraph
 174         | C.Cast (te,ty) ->
 175             let subst,metasenv,te',ugraph1 =
 176               aux metasenv subst n context te ugraph in
 177             let subst,metasenv,ty',ugraph2 =
 178               aux metasenv subst n context ty ugraph1 in
 179             (* TASSI: sure this is in serial? *)
 180             subst,metasenv,(C.Cast (te', ty')),ugraph2
 181         | C.Prod (nn,s,t) ->
 182            let subst,metasenv,s',ugraph1 =
 183              aux metasenv subst n context s ugraph in
 184            let subst,metasenv,t',ugraph2 =
 185              aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
 186                ugraph1
 187            in
 188            (* TASSI: sure this is in serial? *)
 189            subst,metasenv,(C.Prod (nn, s', t')),ugraph2
 190         | C.Lambda (nn,s,t) ->
 191            let subst,metasenv,s',ugraph1 =
 192              aux metasenv subst n context s ugraph in
 193            let subst,metasenv,t',ugraph2 =
 194             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
 195            in
 196            (* TASSI: sure this is in serial? *)
 197             subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
 198         | C.LetIn (nn,s,t) ->
 199            let subst,metasenv,s',ugraph1 =
 200              aux metasenv subst n context s ugraph in
 201            let subst,metasenv,t',ugraph2 =
 202             aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
 203               ugraph1
 204            in
 205            (* TASSI: sure this is in serial? *)
 206             subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
 207         | C.Appl l ->
 208            let subst,metasenv,revl',ugraph1 =
 209             List.fold_left
 210              (fun (subst,metasenv,appl,ugraph) t ->
 211                let subst,metasenv,t',ugraph1 =
 212                  aux metasenv subst n context t ugraph in
 213                 subst,metasenv,(t'::appl),ugraph1
 214              ) (subst,metasenv,[],ugraph) l
 215            in
 216             subst,metasenv,(C.Appl (List.rev revl')),ugraph1
 217         | C.Const (uri,exp_named_subst) ->
 218            let subst,metasenv,exp_named_subst',ugraph1 =
 219             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 220            in
 221             subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
 222         | C.MutInd (uri,i,exp_named_subst) ->
 223            let subst,metasenv,exp_named_subst',ugraph1 =
 224             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 225            in
 226             subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
 227         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 228            let subst,metasenv,exp_named_subst',ugraph1 =
 229             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 230            in
 231             subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
 232         | C.MutCase (sp,i,outt,t,pl) ->
 233            let subst,metasenv,outt',ugraph1 =
 234              aux metasenv subst n context outt ugraph in
 235            let subst,metasenv,t',ugraph2 =
 236              aux metasenv subst n context t ugraph1 in
 237            let subst,metasenv,revpl',ugraph3 =
 238             List.fold_left
 239              (fun (subst,metasenv,pl,ugraph) t ->
 240                let subst,metasenv,t',ugraph1 =
 241                  aux metasenv subst n context t ugraph in
 242                subst,metasenv,(t'::pl),ugraph1
 243              ) (subst,metasenv,[],ugraph2) pl
 244            in
 245            subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
 246            (* TASSI: not sure this is serial *)
 247         | C.Fix (i,fl) ->
 248 (*CSC: not implemented
 249            let tylen = List.length fl in
 250             let substitutedfl =
 251              List.map
 252               (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 253                fl
 254             in
 255              C.Fix (i, substitutedfl)
 256 *)
 257             subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
 258         | C.CoFix (i,fl) ->
 259 (*CSC: not implemented
 260            let tylen = List.length fl in
 261             let substitutedfl =
 262              List.map
 263               (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 264                fl
 265             in
 266              C.CoFix (i, substitutedfl)
 267
 268 *)
 269             subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
 270
 271   and aux_exp_named_subst metasenv subst n context ens ugraph =
 272    List.fold_right
 273     (fun (uri,t) (subst,metasenv,l,ugraph) ->
 274       let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
 275        subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
 276   in
 277   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
 278   let fresh_name =
 279    FreshNamesGenerator.mk_fresh_name ~subst
 280     metasenv context (Cic.Name "Hbeta") ~typ:argty
 281   in
 282    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
 283    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
 284    subst, metasenv, t'', ugraph2
 285 in profiler_beta_expand.HExtlib.profile foo ()
 286
 287
 288 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
 289   let subst,metasenv,hd,ugraph =
 290     List.fold_right
 291       (fun arg (subst,metasenv,t,ugraph) ->
 292          let subst,metasenv,t,ugraph1 =
 293            beta_expand test_equality_only
 294              metasenv subst context t arg ugraph
 295          in
 296            subst,metasenv,t,ugraph1
 297       ) args (subst,metasenv,t,ugraph)
 298   in
 299     subst,metasenv,hd,ugraph
 300
 301
 302 (* NUOVA UNIFICAZIONE *)
 303 (* A substitution is a (int * Cic.term) list that associates a
 304    metavariable i with its body.
 305    A metaenv is a (int * Cic.term) list that associate a metavariable
 306    i with is type.
 307    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
 308    a new substitution which is _NOT_ unwinded. It must be unwinded before
 309    applying it. *)
 310
 311 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
 312  let module C = Cic in
 313  let module R = CicReduction in
 314  let module S = CicSubstitution in
 315  let t1 = deref subst t1 in
 316  let t2 = deref subst t2 in
 317  let b,ugraph  =
 318 let foo () =
 319    R.are_convertible ~subst ~metasenv context t1 t2 ugraph
 320 in profiler_are_convertible.HExtlib.profile foo ()
 321  in
 322    if b then
 323      subst, metasenv, ugraph
 324    else
 325    match (t1, t2) with
 326      | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
 327          let _,subst,metasenv,ugraph1 =
 328            (try
 329               List.fold_left2
 330                 (fun (j,subst,metasenv,ugraph) t1 t2 ->
 331                    match t1,t2 with
 332                        None,_
 333                      | _,None -> j+1,subst,metasenv,ugraph
 334                      | Some t1', Some t2' ->
 335                          (* First possibility:  restriction    *)
 336                          (* Second possibility: unification    *)
 337                          (* Third possibility:  convertibility *)
 338                          let b, ugraph1 =
 339                          R.are_convertible
 340                            ~subst ~metasenv context t1' t2' ugraph
 341                          in
 342                          if b then
 343                            j+1,subst,metasenv, ugraph1
 344                          else
 345                            (try
 346                               let subst,metasenv,ugraph2 =
 347                                 fo_unif_subst
 348                                   test_equality_only
 349                                   subst context metasenv t1' t2' ugraph
 350                               in
 351                                 j+1,subst,metasenv,ugraph2
 352                             with
 353                                 Uncertain _
 354                               | UnificationFailure _ ->
 355 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
 356                                   let metasenv, subst =
 357                                     CicMetaSubst.restrict
 358                                       subst [(n,j)] metasenv in
 359                                     j+1,subst,metasenv,ugraph1)
 360                 ) (1,subst,metasenv,ugraph) ln lm
 361             with
 362                 Exit ->
 363                   raise
 364                     (UnificationFailure (lazy "1"))
 365                     (*
 366                     (sprintf
 367                       "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."
 368                       (CicMetaSubst.ppterm subst t1)
 369                       (CicMetaSubst.ppterm subst t2))) *)
 370               | Invalid_argument _ ->
 371                   raise
 372                     (UnificationFailure (lazy "2")))
 373                     (*
 374                     (sprintf
 375                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
 376                       (CicMetaSubst.ppterm subst t1)
 377                       (CicMetaSubst.ppterm subst t2)))) *)
 378          in subst,metasenv,ugraph1
 379      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
 380          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
 381      | (C.Meta (n,l), t)
 382      | (t, C.Meta (n,l)) ->
 383          let swap =
 384            match t1,t2 with
 385                C.Meta (n,_), C.Meta (m,_) when n < m -> false
 386              | _, C.Meta _ -> false
 387              | _,_ -> true
 388          in
 389          let lower = fun x y -> if swap then y else x in
 390          let upper = fun x y -> if swap then x else y in
 391          let fo_unif_subst_ordered
 392              test_equality_only subst context metasenv m1 m2 ugraph =
 393            fo_unif_subst test_equality_only subst context metasenv
 394              (lower m1 m2) (upper m1 m2) ugraph
 395          in
 396          begin
 397          let subst,metasenv,ugraph1 =
 398            if not (!unif_ty) then subst,metasenv,ugraph else
 399            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
 400            (try
 401               let tyt,ugraph1 =
 402                 type_of_aux' metasenv subst context t ugraph
 403               in
 404                 fo_unif_subst
 405                   test_equality_only
 406                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
 407             with
 408                 UnificationFailure _ as e -> raise e
 409               | Uncertain msg -> raise (UnificationFailure msg)
 410               | AssertFailure _ ->
 411                   debug_print (lazy "siamo allo huge hack");
 412                   (* TODO huge hack!!!!
 413                    * we keep on unifying/refining in the hope that
 414                    * the problem will be eventually solved.
 415                    * In the meantime we're breaking a big invariant:
 416                    * the terms that we are unifying are no longer well
 417                    * typed in the current context (in the worst case
 418                    * we could even diverge) *)
 419                   (subst, metasenv,ugraph)) in
 420          let t',metasenv,subst =
 421            try
 422              CicMetaSubst.delift n subst context metasenv l t
 423            with
 424                (CicMetaSubst.MetaSubstFailure msg)->
 425                  raise (UnificationFailure msg)
 426              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 427          in
 428          let t'',ugraph2 =
 429            match t' with
 430                C.Sort (C.Type u) when not test_equality_only ->
 431                  let u' = CicUniv.fresh () in
 432                  let s = C.Sort (C.Type u') in
 433                  let ugraph2 =
 434                    CicUniv.add_ge (upper u u') (lower u u') ugraph1
 435                  in
 436                    s,ugraph2
 437              | _ -> t',ugraph1
 438          in
 439          (* Unifying the types may have already instantiated n. Let's check *)
 440          try
 441            let (_, oldt,_) = CicUtil.lookup_subst n subst in
 442            let lifted_oldt = S.subst_meta l oldt in
 443              fo_unif_subst_ordered
 444                test_equality_only subst context metasenv t lifted_oldt ugraph2
 445          with
 446              CicUtil.Subst_not_found _ ->
 447                let (_, context, ty) = CicUtil.lookup_meta n metasenv in
 448                let subst = (n, (context, t'',ty)) :: subst in
 449                let metasenv =
 450                  List.filter (fun (m,_,_) -> not (n = m)) metasenv in
 451                subst, metasenv, ugraph2
 452          end
 453    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 454    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 455       if UriManager.eq uri1 uri2 then
 456        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 457         exp_named_subst1 exp_named_subst2 ugraph
 458       else
 459        raise (UnificationFailure (lazy
 460           (sprintf
 461             "Can't unify %s with %s due to different constants"
 462             (CicMetaSubst.ppterm subst t1)
 463             (CicMetaSubst.ppterm subst t2))))
 464    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 465        if UriManager.eq uri1 uri2 && i1 = i2 then
 466          fo_unif_subst_exp_named_subst
 467            test_equality_only
 468            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 469        else
 470          raise (UnificationFailure (lazy "4"))
 471            (* (sprintf
 472               "Can't unify %s with %s due to different inductive principles"
 473               (CicMetaSubst.ppterm subst t1)
 474               (CicMetaSubst.ppterm subst t2))) *)
 475    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 476        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 477        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 478          fo_unif_subst_exp_named_subst
 479            test_equality_only
 480            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 481        else
 482          raise (UnificationFailure (lazy "5"))
 483            (* (sprintf
 484               "Can't unify %s with %s due to different inductive constructors"
 485               (CicMetaSubst.ppterm subst t1)
 486               (CicMetaSubst.ppterm subst t2))) *)
 487    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 488    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
 489                               subst context metasenv te t2 ugraph
 490    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
 491                               subst context metasenv t1 te ugraph
 492    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 493        let subst',metasenv',ugraph1 =
 494          fo_unif_subst true subst context metasenv s1 s2 ugraph
 495        in
 496          fo_unif_subst test_equality_only
 497            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 498    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 499        let subst',metasenv',ugraph1 =
 500          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
 501        in
 502          fo_unif_subst test_equality_only
 503            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 504    | (C.LetIn (_,s1,t1), t2)
 505    | (t2, C.LetIn (_,s1,t1)) ->
 506        fo_unif_subst
 507         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
 508    | (C.Appl l1, C.Appl l2) ->
 509        (* andrea: this case should be probably rewritten in the
 510           spirit of deref *)
 511        (match l1,l2 with
 512           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
 513               (try
 514                  List.fold_left2
 515                    (fun (subst,metasenv,ugraph) t1 t2 ->
 516                       fo_unif_subst
 517                         test_equality_only subst context metasenv t1 t2 ugraph)
 518                    (subst,metasenv,ugraph) l1 l2
 519                with (Invalid_argument msg) ->
 520                  raise (UnificationFailure (lazy msg)))
 521           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
 522               (* we verify that none of the args is a Meta,
 523                 since beta expanding with respoect to a metavariable
 524                 makes no sense  *)
 525  (*
 526               (try
 527                  let (_,t,_) = CicUtil.lookup_subst i subst in
 528                  let lifted = S.subst_meta l t in
 529                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 530                    fo_unif_subst
 531                     test_equality_only
 532                      subst context metasenv reduced t2 ugraph
 533                with CicUtil.Subst_not_found _ -> *)
 534               let subst,metasenv,beta_expanded,ugraph1 =
 535                 beta_expand_many
 536                   test_equality_only metasenv subst context t2 args ugraph
 537               in
 538                 fo_unif_subst test_equality_only subst context metasenv
 539                   (C.Meta (i,l)) beta_expanded ugraph1
 540           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
 541               (* (try
 542                  let (_,t,_) = CicUtil.lookup_subst i subst in
 543                  let lifted = S.subst_meta l t in
 544                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 545                    fo_unif_subst
 546                      test_equality_only
 547                      subst context metasenv t1 reduced ugraph
 548                with CicUtil.Subst_not_found _ -> *)
 549                  let subst,metasenv,beta_expanded,ugraph1 =
 550                    beta_expand_many
 551                      test_equality_only
 552                      metasenv subst context t1 args ugraph
 553                  in
 554                    fo_unif_subst test_equality_only subst context metasenv
 555                      (C.Meta (i,l)) beta_expanded ugraph1
 556           | _,_ ->
 557               let lr1 = List.rev l1 in
 558               let lr2 = List.rev l2 in
 559               let rec
 560                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
 561                 match (l1,l2) with
 562                     [],_
 563                   | _,[] -> assert false
 564                   | ([h1],[h2]) ->
 565                       fo_unif_subst
 566                         test_equality_only subst context metasenv h1 h2 ugraph
 567                   | ([h],l)
 568                   | (l,[h]) ->
 569                       fo_unif_subst test_equality_only subst context metasenv
 570                         h (C.Appl (List.rev l)) ugraph
 571                   | ((h1::l1),(h2::l2)) ->
 572                       let subst', metasenv',ugraph1 =
 573                         fo_unif_subst
 574                           test_equality_only
 575                           subst context metasenv h1 h2 ugraph
 576                       in
 577                         fo_unif_l
 578                           test_equality_only subst' metasenv' (l1,l2) ugraph1
 579               in
 580               (try
 581                 fo_unif_l
 582                   test_equality_only subst metasenv (lr1, lr2)  ugraph
 583               with
 584               | UnificationFailure _
 585               | Uncertain _ as exn ->
 586                   (match l1, l2 with
 587                   | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
 588                      (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
 589                     CoercGraph.is_a_coercion c1 &&
 590                     CoercGraph.is_a_coercion c2 ->
 591                       let body1, attrs1, ugraph =
 592                         match CicEnvironment.get_obj ugraph uri1 with
 593                         | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
 594                         | _ -> assert false
 595                       in
 596                       let body2, attrs2, ugraph =
 597                         match CicEnvironment.get_obj ugraph uri2 with
 598                         | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
 599                         | _ -> assert false
 600                       in
 601                       let is_composite1 =
 602                         List.exists ((=) (`Class `Coercion)) attrs1 in
 603                       let is_composite2 =
 604                         List.exists ((=) (`Class `Coercion)) attrs2 in
 605                       (match is_composite1, is_composite2 with
 606                       | false, false -> raise exn
 607                       | true, false ->
 608                           let body1 = CicSubstitution.subst_vars ens1 body1 in
 609                           let appl = Cic.Appl (body1::tl1) in
 610                           let redappl = CicReduction.head_beta_reduce appl in
 611                           fo_unif_subst
 612                             test_equality_only subst context metasenv
 613                               redappl t2 ugraph
 614                       | false, true ->
 615                           let body2 = CicSubstitution.subst_vars ens2 body2 in
 616                           let appl = Cic.Appl (body2::tl2) in
 617                           let redappl = CicReduction.head_beta_reduce appl in
 618                           fo_unif_subst
 619                             test_equality_only subst context metasenv
 620                              t1 redappl ugraph
 621                       | true, true ->
 622                           let body1 = CicSubstitution.subst_vars ens1 body1 in
 623                           let appl1 = Cic.Appl (body1::tl1) in
 624                           let redappl1 = CicReduction.head_beta_reduce appl1 in
 625                           let body2 = CicSubstitution.subst_vars ens2 body2 in
 626                           let appl2 = Cic.Appl (body2::tl2) in
 627                           let redappl2 = CicReduction.head_beta_reduce appl2 in
 628                           fo_unif_subst
 629                             test_equality_only subst context metasenv
 630                              redappl1 redappl2 ugraph)
 631                   | _ -> raise exn)))
 632    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 633        let subst', metasenv',ugraph1 =
 634         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
 635           ugraph in
 636        let subst'',metasenv'',ugraph2 =
 637         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
 638           ugraph1 in
 639        (try
 640          List.fold_left2
 641           (fun (subst,metasenv,ugraph) t1 t2 ->
 642             fo_unif_subst
 643              test_equality_only subst context metasenv t1 t2 ugraph
 644           ) (subst'',metasenv'',ugraph2) pl1 pl2
 645         with
 646          Invalid_argument _ ->
 647           raise (UnificationFailure (lazy "6.1")))
 648            (* (sprintf
 649               "Error trying to unify %s with %s: the number of branches is not the same."
 650               (CicMetaSubst.ppterm subst t1)
 651               (CicMetaSubst.ppterm subst t2)))) *)
 652    | (C.Rel _, _) | (_,  C.Rel _) ->
 653        if t1 = t2 then
 654          subst, metasenv,ugraph
 655        else
 656         raise (UnificationFailure (lazy
 657            (sprintf
 658              "Can't unify %s with %s because they are not convertible"
 659              (CicMetaSubst.ppterm subst t1)
 660              (CicMetaSubst.ppterm subst t2))))
 661    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
 662        let subst,metasenv,beta_expanded,ugraph1 =
 663          beta_expand_many
 664            test_equality_only metasenv subst context t2 args ugraph
 665        in
 666          fo_unif_subst test_equality_only subst context metasenv
 667            (C.Meta (i,l)) beta_expanded ugraph1
 668    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
 669        let subst,metasenv,beta_expanded,ugraph1 =
 670          beta_expand_many
 671            test_equality_only metasenv subst context t1 args ugraph
 672        in
 673          fo_unif_subst test_equality_only subst context metasenv
 674            beta_expanded (C.Meta (i,l)) ugraph1
 675    | (C.Sort _ ,_) | (_, C.Sort _)
 676    | (C.Const _, _) | (_, C.Const _)
 677    | (C.MutInd  _, _) | (_, C.MutInd _)
 678    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
 679    | (C.Fix _, _) | (_, C.Fix _)
 680    | (C.CoFix _, _) | (_, C.CoFix _) ->
 681        if t1 = t2 then
 682          subst, metasenv, ugraph
 683        else
 684          let b,ugraph1 =
 685            R.are_convertible ~subst ~metasenv context t1 t2 ugraph
 686          in
 687            if b then
 688              subst, metasenv, ugraph1
 689            else
 690              raise
 691                 (UnificationFailure (lazy (sprintf
 692                   "Can't unify %s with %s because they are not convertible"
 693                   (CicMetaSubst.ppterm subst t1)
 694                   (CicMetaSubst.ppterm subst t2))))
 695    | (C.Prod _, t2) ->
 696        let t2' = R.whd ~subst context t2 in
 697        (match t2' with
 698             C.Prod _ ->
 699               fo_unif_subst test_equality_only
 700                 subst context metasenv t1 t2' ugraph
 701           | _ -> raise (UnificationFailure (lazy "8")))
 702    | (t1, C.Prod _) ->
 703        let t1' = R.whd ~subst context t1 in
 704        (match t1' with
 705             C.Prod _ ->
 706               fo_unif_subst test_equality_only
 707                 subst context metasenv t1' t2 ugraph
 708           | _ -> (* raise (UnificationFailure "9")) *)
 709              raise
 710                 (UnificationFailure (lazy (sprintf
 711                    "Can't unify %s with %s because they are not convertible"
 712                    (CicMetaSubst.ppterm subst t1)
 713                    (CicMetaSubst.ppterm subst t2)))))
 714    | (_,_) ->
 715        raise (UnificationFailure (lazy "10"))
 716          (* (sprintf
 717             "Can't unify %s with %s because they are not convertible"
 718             (CicMetaSubst.ppterm subst t1)
 719             (CicMetaSubst.ppterm subst t2))) *)
 720
 721 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 722  exp_named_subst1 exp_named_subst2 ugraph
 723 =
 724  try
 725   List.fold_left2
 726    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
 727      assert (uri1=uri2) ;
 728      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
 729    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
 730  with
 731   Invalid_argument _ ->
 732    let print_ens ens =
 733     String.concat " ; "
 734      (List.map
 735        (fun (uri,t) ->
 736          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
 737        ) ens)
 738    in
 739     raise (UnificationFailure (lazy (sprintf
 740      "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))))
 741
 742 (* A substitution is a (int * Cic.term) list that associates a               *)
 743 (* metavariable i with its body.                                             *)
 744 (* metasenv is of type Cic.metasenv                                          *)
 745 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 746 (* a new substitution which is already unwinded and ready to be applied and  *)
 747 (* a new metasenv in which some hypothesis in the contexts of the            *)
 748 (* metavariables may have been restricted.                                   *)
 749 let fo_unif metasenv context t1 t2 ugraph =
 750  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 751
 752 let enrich_msg msg subst context metasenv t1 t2 ugraph =
 753  lazy (
 754   if verbose then
 755    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"
 756     (CicMetaSubst.ppterm subst t1)
 757     (try
 758       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 759       CicPp.ppterm ty_t1
 760     with
 761     | UnificationFailure s
 762     | Uncertain s
 763     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 764     (CicMetaSubst.ppterm subst t2)
 765     (try
 766       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 767       CicPp.ppterm ty_t2
 768     with
 769     | UnificationFailure s
 770     | Uncertain s
 771     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 772     (CicMetaSubst.ppcontext subst context)
 773     (CicMetaSubst.ppmetasenv subst metasenv)
 774     (CicMetaSubst.ppsubst subst) (Lazy.force msg)
 775  else
 776    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 777     (CicMetaSubst.ppterm_in_context subst t1 context)
 778     (try
 779       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 780       CicMetaSubst.ppterm_in_context subst ty_t1 context
 781     with
 782     | UnificationFailure s
 783     | Uncertain s
 784     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 785     (CicMetaSubst.ppterm_in_context subst t2 context)
 786     (try
 787       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 788       CicMetaSubst.ppterm_in_context subst ty_t2 context
 789     with
 790     | UnificationFailure s
 791     | Uncertain s
 792     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 793     (CicMetaSubst.ppcontext subst context)
 794     (CicMetaSubst.ppmetasenv subst metasenv)
 795     (Lazy.force msg)
 796  )
 797
 798 let fo_unif_subst subst context metasenv t1 t2 ugraph =
 799   try
 800     fo_unif_subst false subst context metasenv t1 t2 ugraph
 801   with
 802   | AssertFailure msg ->
 803      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 804   | UnificationFailure msg ->
 805      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 806 ;;