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