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