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