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