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