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