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