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