components/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 (* $Id$ *)
  27
  28 open Printf
  29
  30 exception UnificationFailure of string Lazy.t;;
  31 exception Uncertain of string Lazy.t;;
  32 exception AssertFailure of string Lazy.t;;
  33
  34 let verbose = false;;
  35 let debug_print = fun _ -> ()
  36
  37 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
  38 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
  39 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
  40 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
  41
  42 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
  43
  44 let type_of_aux' metasenv subst context term ugraph =
  45 let foo () =
  46   try
  47     profile.HExtlib.profile
  48       (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
  49   with
  50       CicTypeChecker.TypeCheckerFailure msg ->
  51         let msg =
  52          lazy
  53           (sprintf
  54            "Kernel Type checking error:
  55 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
  56              (CicMetaSubst.ppterm ~metasenv subst term)
  57              (CicMetaSubst.ppterm ~metasenv [] term)
  58              (CicMetaSubst.ppcontext ~metasenv subst context)
  59              (CicMetaSubst.ppmetasenv subst metasenv)
  60              (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
  61         raise (AssertFailure msg)
  62     | CicTypeChecker.AssertFailure msg ->
  63         let msg = lazy
  64          (sprintf
  65            "Kernel Type checking assertion failure:
  66 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
  67              (CicMetaSubst.ppterm ~metasenv subst term)
  68              (CicMetaSubst.ppterm ~metasenv [] term)
  69              (CicMetaSubst.ppcontext ~metasenv subst context)
  70              (CicMetaSubst.ppmetasenv subst metasenv)
  71              (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
  72         raise (AssertFailure msg)
  73 in profiler_toa.HExtlib.profile foo ()
  74 ;;
  75
  76 let exists_a_meta l =
  77   List.exists
  78     (function
  79        | Cic.Meta _
  80        | Cic.Appl (Cic.Meta _::_) -> true
  81        | _ -> false) l
  82
  83 let rec deref subst t =
  84   let snd (_,a,_) = a in
  85   match t with
  86       Cic.Meta(n,l) ->
  87         (try
  88            deref subst
  89              (CicSubstitution.subst_meta
  90                 l (snd (CicUtil.lookup_subst n subst)))
  91          with
  92              CicUtil.Subst_not_found _ -> t)
  93     | Cic.Appl(Cic.Meta(n,l)::args) ->
  94         (match deref subst (Cic.Meta(n,l)) with
  95            | Cic.Lambda _ as t ->
  96                deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
  97            | r -> Cic.Appl(r::args))
  98     | Cic.Appl(((Cic.Lambda _) as t)::args) ->
  99            deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
 100     | t -> t
 101 ;;
 102
 103 let deref subst t =
 104  let foo () = deref subst t
 105  in profiler_deref.HExtlib.profile foo ()
 106
 107 exception WrongShape;;
 108 let eta_reduce after_beta_expansion after_beta_expansion_body
 109      before_beta_expansion
 110  =
 111  try
 112   match before_beta_expansion,after_beta_expansion_body with
 113      Cic.Appl l, Cic.Appl l' ->
 114       let rec all_but_last check_last =
 115        function
 116           [] -> assert false
 117         | [Cic.Rel 1] -> []
 118         | [_] -> if check_last then raise WrongShape else []
 119         | he::tl -> he::(all_but_last check_last tl)
 120       in
 121        let all_but_last check_last l =
 122         match all_but_last check_last l with
 123            [] -> assert false
 124          | [he] -> he
 125          | l -> Cic.Appl l
 126        in
 127        let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
 128        let all_but_last = all_but_last false l in
 129         (* here we should test alpha-equivalence; however we know by
 130            construction that here alpha_equivalence is equivalent to = *)
 131         if t = all_but_last then
 132          all_but_last
 133         else
 134          after_beta_expansion
 135    | _,_ -> after_beta_expansion
 136  with
 137   WrongShape -> after_beta_expansion
 138
 139 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
 140  let module S = CicSubstitution in
 141  let module C = Cic in
 142 let foo () =
 143   let rec aux metasenv subst n context t' ugraph =
 144    try
 145
 146     let subst,metasenv,ugraph1 =
 147      fo_unif_subst test_equality_only subst context metasenv
 148       (CicSubstitution.lift n arg) t' ugraph
 149
 150     in
 151      subst,metasenv,C.Rel (1 + n),ugraph1
 152    with
 153       Uncertain _
 154     | UnificationFailure _ ->
 155        match t' with
 156         | C.Rel m  -> subst,metasenv,
 157            (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
 158         | C.Var (uri,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.Var (uri,exp_named_subst'),ugraph1
 163         | C.Meta (i,l) ->
 164             (* andrea: in general, beta_expand can create badly typed
 165              terms. This happens quite seldom in practice, UNLESS we
 166              iterate on the local context. For this reason, we renounce
 167              to iterate and just lift *)
 168             let l =
 169               List.map
 170                 (function
 171                      Some t -> Some (CicSubstitution.lift 1 t)
 172                    | None -> None) l in
 173             subst, metasenv, C.Meta (i,l), ugraph
 174         | C.Sort _
 175         | C.Implicit _ as t -> subst,metasenv,t,ugraph
 176         | C.Cast (te,ty) ->
 177             let subst,metasenv,te',ugraph1 =
 178               aux metasenv subst n context te ugraph in
 179             let subst,metasenv,ty',ugraph2 =
 180               aux metasenv subst n context ty ugraph1 in
 181             (* TASSI: sure this is in serial? *)
 182             subst,metasenv,(C.Cast (te', ty')),ugraph2
 183         | C.Prod (nn,s,t) ->
 184            let subst,metasenv,s',ugraph1 =
 185              aux metasenv subst n context s ugraph in
 186            let subst,metasenv,t',ugraph2 =
 187              aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
 188                ugraph1
 189            in
 190            (* TASSI: sure this is in serial? *)
 191            subst,metasenv,(C.Prod (nn, s', t')),ugraph2
 192         | C.Lambda (nn,s,t) ->
 193            let subst,metasenv,s',ugraph1 =
 194              aux metasenv subst n context s ugraph in
 195            let subst,metasenv,t',ugraph2 =
 196             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
 197            in
 198            (* TASSI: sure this is in serial? *)
 199             subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
 200         | C.LetIn (nn,s,t) ->
 201            let subst,metasenv,s',ugraph1 =
 202              aux metasenv subst n context s ugraph in
 203            let subst,metasenv,t',ugraph2 =
 204             aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
 205               ugraph1
 206            in
 207            (* TASSI: sure this is in serial? *)
 208             subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
 209         | C.Appl l ->
 210            let subst,metasenv,revl',ugraph1 =
 211             List.fold_left
 212              (fun (subst,metasenv,appl,ugraph) t ->
 213                let subst,metasenv,t',ugraph1 =
 214                  aux metasenv subst n context t ugraph in
 215                 subst,metasenv,(t'::appl),ugraph1
 216              ) (subst,metasenv,[],ugraph) l
 217            in
 218             subst,metasenv,(C.Appl (List.rev revl')),ugraph1
 219         | C.Const (uri,exp_named_subst) ->
 220            let subst,metasenv,exp_named_subst',ugraph1 =
 221             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 222            in
 223             subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
 224         | C.MutInd (uri,i,exp_named_subst) ->
 225            let subst,metasenv,exp_named_subst',ugraph1 =
 226             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 227            in
 228             subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
 229         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 230            let subst,metasenv,exp_named_subst',ugraph1 =
 231             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 232            in
 233             subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
 234         | C.MutCase (sp,i,outt,t,pl) ->
 235            let subst,metasenv,outt',ugraph1 =
 236              aux metasenv subst n context outt ugraph in
 237            let subst,metasenv,t',ugraph2 =
 238              aux metasenv subst n context t ugraph1 in
 239            let subst,metasenv,revpl',ugraph3 =
 240             List.fold_left
 241              (fun (subst,metasenv,pl,ugraph) t ->
 242                let subst,metasenv,t',ugraph1 =
 243                  aux metasenv subst n context t ugraph in
 244                subst,metasenv,(t'::pl),ugraph1
 245              ) (subst,metasenv,[],ugraph2) pl
 246            in
 247            subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
 248            (* TASSI: not sure this is serial *)
 249         | C.Fix (i,fl) ->
 250 (*CSC: not implemented
 251            let tylen = List.length fl in
 252             let substitutedfl =
 253              List.map
 254               (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 255                fl
 256             in
 257              C.Fix (i, substitutedfl)
 258 *)
 259             subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
 260         | C.CoFix (i,fl) ->
 261 (*CSC: not implemented
 262            let tylen = List.length fl in
 263             let substitutedfl =
 264              List.map
 265               (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 266                fl
 267             in
 268              C.CoFix (i, substitutedfl)
 269
 270 *)
 271             subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
 272
 273   and aux_exp_named_subst metasenv subst n context ens ugraph =
 274    List.fold_right
 275     (fun (uri,t) (subst,metasenv,l,ugraph) ->
 276       let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
 277        subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
 278   in
 279   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
 280   let fresh_name =
 281    FreshNamesGenerator.mk_fresh_name ~subst
 282     metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
 283   in
 284    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
 285    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
 286    subst, metasenv, t'', ugraph2
 287 in profiler_beta_expand.HExtlib.profile foo ()
 288
 289
 290 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
 291   let _,subst,metasenv,hd,ugraph =
 292     List.fold_right
 293       (fun arg (num,subst,metasenv,t,ugraph) ->
 294          let subst,metasenv,t,ugraph1 =
 295            beta_expand num test_equality_only
 296              metasenv subst context t arg ugraph
 297          in
 298            num+1,subst,metasenv,t,ugraph1
 299       ) args (1,subst,metasenv,t,ugraph)
 300   in
 301     subst,metasenv,hd,ugraph
 302
 303
 304 (* NUOVA UNIFICAZIONE *)
 305 (* A substitution is a (int * Cic.term) list that associates a
 306    metavariable i with its body.
 307    A metaenv is a (int * Cic.term) list that associate a metavariable
 308    i with is type.
 309    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
 310    a new substitution which is _NOT_ unwinded. It must be unwinded before
 311    applying it. *)
 312
 313 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
 314  let module C = Cic in
 315  let module R = CicReduction in
 316  let module S = CicSubstitution in
 317  let t1 = deref subst t1 in
 318  let t2 = deref subst t2 in
 319  let b,ugraph  =
 320 let foo () =
 321    R.are_convertible ~subst ~metasenv context t1 t2 ugraph
 322 in profiler_are_convertible.HExtlib.profile foo ()
 323  in
 324    if b then
 325      subst, metasenv, ugraph
 326    else
 327    match (t1, t2) with
 328      | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
 329          let _,subst,metasenv,ugraph1 =
 330            (try
 331               List.fold_left2
 332                 (fun (j,subst,metasenv,ugraph) t1 t2 ->
 333                    match t1,t2 with
 334                        None,_
 335                      | _,None -> j+1,subst,metasenv,ugraph
 336                      | Some t1', Some t2' ->
 337                          (* First possibility:  restriction    *)
 338                          (* Second possibility: unification    *)
 339                          (* Third possibility:  convertibility *)
 340                          let b, ugraph1 =
 341                          R.are_convertible
 342                            ~subst ~metasenv context t1' t2' ugraph
 343                          in
 344                          if b then
 345                            j+1,subst,metasenv, ugraph1
 346                          else
 347                            (try
 348                               let subst,metasenv,ugraph2 =
 349                                 fo_unif_subst
 350                                   test_equality_only
 351                                   subst context metasenv t1' t2' ugraph
 352                               in
 353                                 j+1,subst,metasenv,ugraph2
 354                             with
 355                                 Uncertain _
 356                               | UnificationFailure _ ->
 357 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
 358                                   let metasenv, subst =
 359                                     CicMetaSubst.restrict
 360                                       subst [(n,j)] metasenv in
 361                                     j+1,subst,metasenv,ugraph1)
 362                 ) (1,subst,metasenv,ugraph) ln lm
 363             with
 364                 Exit ->
 365                   raise
 366                     (UnificationFailure (lazy "1"))
 367                     (*
 368                     (sprintf
 369                       "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."
 370                       (CicMetaSubst.ppterm ~metasenv subst t1)
 371                       (CicMetaSubst.ppterm ~metasenv subst t2))) *)
 372               | Invalid_argument _ ->
 373                   raise
 374                     (UnificationFailure (lazy "2")))
 375                     (*
 376                     (sprintf
 377                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
 378                       (CicMetaSubst.ppterm ~metasenv subst t1)
 379                       (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
 380          in subst,metasenv,ugraph1
 381      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
 382          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
 383      | (C.Meta (n,l), t)
 384      | (t, C.Meta (n,l)) ->
 385          let swap =
 386            match t1,t2 with
 387                C.Meta (n,_), C.Meta (m,_) when n < m -> false
 388              | _, C.Meta _ -> false
 389              | _,_ -> true
 390          in
 391          let lower = fun x y -> if swap then y else x in
 392          let upper = fun x y -> if swap then x else y in
 393          let fo_unif_subst_ordered
 394              test_equality_only subst context metasenv m1 m2 ugraph =
 395            fo_unif_subst test_equality_only subst context metasenv
 396              (lower m1 m2) (upper m1 m2) ugraph
 397          in
 398          begin
 399          let subst,metasenv,ugraph1 =
 400            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
 401            (try
 402               let tyt,ugraph1 =
 403                 type_of_aux' metasenv subst context t ugraph
 404               in
 405                 fo_unif_subst
 406                   test_equality_only
 407                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
 408             with
 409                 UnificationFailure _ as e -> raise e
 410               | Uncertain msg -> raise (UnificationFailure msg)
 411               | AssertFailure _ ->
 412                   debug_print (lazy "siamo allo huge hack");
 413                   (* TODO huge hack!!!!
 414                    * we keep on unifying/refining in the hope that
 415                    * the problem will be eventually solved.
 416                    * In the meantime we're breaking a big invariant:
 417                    * the terms that we are unifying are no longer well
 418                    * typed in the current context (in the worst case
 419                    * we could even diverge) *)
 420                   (subst, metasenv,ugraph)) in
 421          let t',metasenv,subst =
 422            try
 423              CicMetaSubst.delift n subst context metasenv l t
 424            with
 425                (CicMetaSubst.MetaSubstFailure msg)->
 426                  raise (UnificationFailure msg)
 427              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 428          in
 429          let t'',ugraph2 =
 430            match t' with
 431                C.Sort (C.Type u) when not test_equality_only ->
 432                  let u' = CicUniv.fresh () in
 433                  let s = C.Sort (C.Type u') in
 434                   (try
 435                     let ugraph2 =
 436                      CicUniv.add_ge (upper u u') (lower u u') ugraph1
 437                     in
 438                      s,ugraph2
 439                    with
 440                     CicUniv.UniverseInconsistency msg ->
 441                      raise (UnificationFailure msg))
 442              | _ -> t',ugraph1
 443          in
 444          (* Unifying the types may have already instantiated n. Let's check *)
 445          try
 446            let (_, oldt,_) = CicUtil.lookup_subst n subst in
 447            let lifted_oldt = S.subst_meta l oldt in
 448              fo_unif_subst_ordered
 449                test_equality_only subst context metasenv t lifted_oldt ugraph2
 450          with
 451              CicUtil.Subst_not_found _ ->
 452                let (_, context, ty) = CicUtil.lookup_meta n metasenv in
 453                let subst = (n, (context, t'',ty)) :: subst in
 454                let metasenv =
 455                  List.filter (fun (m,_,_) -> not (n = m)) metasenv in
 456                subst, metasenv, ugraph2
 457          end
 458    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 459    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 460       if UriManager.eq uri1 uri2 then
 461        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 462         exp_named_subst1 exp_named_subst2 ugraph
 463       else
 464        raise (UnificationFailure (lazy
 465           (sprintf
 466             "Can't unify %s with %s due to different constants"
 467             (CicMetaSubst.ppterm ~metasenv subst t1)
 468             (CicMetaSubst.ppterm ~metasenv subst t2))))
 469    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 470        if UriManager.eq uri1 uri2 && i1 = i2 then
 471          fo_unif_subst_exp_named_subst
 472            test_equality_only
 473            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 474        else
 475          raise (UnificationFailure
 476            (lazy
 477             (sprintf
 478              "Can't unify %s with %s due to different inductive principles"
 479              (CicMetaSubst.ppterm ~metasenv subst t1)
 480              (CicMetaSubst.ppterm ~metasenv subst t2))))
 481    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 482        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 483        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 484          fo_unif_subst_exp_named_subst
 485            test_equality_only
 486            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 487        else
 488          raise (UnificationFailure
 489           (lazy
 490             (sprintf
 491               "Can't unify %s with %s due to different inductive constructors"
 492               (CicMetaSubst.ppterm ~metasenv subst t1)
 493               (CicMetaSubst.ppterm ~metasenv subst t2))))
 494    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 495    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
 496                               subst context metasenv te t2 ugraph
 497    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
 498                               subst context metasenv t1 te ugraph
 499    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 500        let subst',metasenv',ugraph1 =
 501          fo_unif_subst true subst context metasenv s1 s2 ugraph
 502        in
 503          fo_unif_subst test_equality_only
 504            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 505    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 506        let subst',metasenv',ugraph1 =
 507          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
 508        in
 509          fo_unif_subst test_equality_only
 510            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 511    | (C.LetIn (_,s1,t1), t2)
 512    | (t2, C.LetIn (_,s1,t1)) ->
 513        fo_unif_subst
 514         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
 515    | (C.Appl l1, C.Appl l2) ->
 516        (* andrea: this case should be probably rewritten in the
 517           spirit of deref *)
 518        (match l1,l2 with
 519           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
 520               (try
 521                  List.fold_left2
 522                    (fun (subst,metasenv,ugraph) t1 t2 ->
 523                       fo_unif_subst
 524                         test_equality_only subst context metasenv t1 t2 ugraph)
 525                    (subst,metasenv,ugraph) l1 l2
 526                with (Invalid_argument msg) ->
 527                  raise (UnificationFailure (lazy msg)))
 528           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
 529               (* we verify that none of the args is a Meta,
 530                 since beta expanding with respoect to a metavariable
 531                 makes no sense  *)
 532  (*
 533               (try
 534                  let (_,t,_) = CicUtil.lookup_subst i subst in
 535                  let lifted = S.subst_meta l t in
 536                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 537                    fo_unif_subst
 538                     test_equality_only
 539                      subst context metasenv reduced t2 ugraph
 540                with CicUtil.Subst_not_found _ -> *)
 541               let subst,metasenv,beta_expanded,ugraph1 =
 542                 beta_expand_many
 543                   test_equality_only metasenv subst context t2 args ugraph
 544               in
 545                 fo_unif_subst test_equality_only subst context metasenv
 546                   (C.Meta (i,l)) beta_expanded ugraph1
 547           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
 548               (* (try
 549                  let (_,t,_) = CicUtil.lookup_subst i subst in
 550                  let lifted = S.subst_meta l t in
 551                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 552                    fo_unif_subst
 553                      test_equality_only
 554                      subst context metasenv t1 reduced ugraph
 555                with CicUtil.Subst_not_found _ -> *)
 556                  let subst,metasenv,beta_expanded,ugraph1 =
 557                    beta_expand_many
 558                      test_equality_only
 559                      metasenv subst context t1 args ugraph
 560                  in
 561                    fo_unif_subst test_equality_only subst context metasenv
 562                      (C.Meta (i,l)) beta_expanded ugraph1
 563           | _,_ ->
 564               let lr1 = List.rev l1 in
 565               let lr2 = List.rev l2 in
 566               let rec
 567                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
 568                 match (l1,l2) with
 569                     [],_
 570                   | _,[] -> assert false
 571                   | ([h1],[h2]) ->
 572                       fo_unif_subst
 573                         test_equality_only subst context metasenv h1 h2 ugraph
 574                   | ([h],l)
 575                   | (l,[h]) ->
 576                       fo_unif_subst test_equality_only subst context metasenv
 577                         h (C.Appl (List.rev l)) ugraph
 578                   | ((h1::l1),(h2::l2)) ->
 579                       let subst', metasenv',ugraph1 =
 580                         fo_unif_subst
 581                           test_equality_only
 582                           subst context metasenv h1 h2 ugraph
 583                       in
 584                         fo_unif_l
 585                           test_equality_only subst' metasenv' (l1,l2) ugraph1
 586               in
 587               (try
 588                 fo_unif_l
 589                   test_equality_only subst metasenv (lr1, lr2)  ugraph
 590               with
 591               | UnificationFailure s
 592               | Uncertain s as exn ->
 593                   (match l1, l2 with
 594                   | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
 595                      (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
 596                     CoercDb.is_a_coercion' c1 &&
 597                     CoercDb.is_a_coercion' c2 &&
 598                     not (UriManager.eq uri1 uri2) ->
 599 (*DEBUGGING ONLY:
 600 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 601 let res =
 602 *)
 603                      let rec look_for_first_coercion c tl =
 604                       match
 605                        CicMetaSubst.apply_subst subst (HExtlib.list_last tl)
 606                       with
 607                          Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl')
 608                           when CoercDb.is_a_coercion' c' ->
 609                            look_for_first_coercion c' tl'
 610                        | last_tl -> c,last_tl
 611                      in
 612                       let c1,last_tl1 = look_for_first_coercion c1 tl1 in
 613                       let c2,last_tl2 = look_for_first_coercion c2 tl2 in
 614                       let car1 =
 615                         CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in
 616                       let car2 =
 617                         CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in
 618                       if CoercDb.eq_carr car1 car2 then
 619                        (match last_tl1,last_tl2 with
 620                            C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn
 621                          | C.Meta _, _
 622                          | _, C.Meta _ ->
 623                            let subst,metasenv,ugraph =
 624                             fo_unif_subst test_equality_only subst context
 625                              metasenv last_tl1 last_tl2 ugraph
 626                            in
 627                             fo_unif_subst test_equality_only subst context
 628                              metasenv (C.Appl l1) (C.Appl l2) ugraph
 629                          | _ -> raise exn)
 630                       else
 631                        let meets =
 632                          CoercGraph.meets metasenv subst context car1 car2
 633                        in
 634                         (match meets with
 635                         | [] -> raise exn
 636                         | (carr,metasenv,to1,to2)::xxx ->
 637                           (match xxx with
 638                           [] -> ()
 639                           | (m2,_,c2,c2')::_ ->
 640                           let m1,_,c1,c1' = carr,metasenv,to1,to2 in
 641                           let unopt =
 642                             function Some (_,t) -> CicPp.ppterm t
 643                             | None -> "id"
 644                           in
 645                           HLog.warn
 646                             ("There are two minimal joins of "^
 647                             CoercDb.name_of_carr car1^" and "^
 648                             CoercDb.name_of_carr car2^": " ^
 649                             CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
 650                             unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
 651                             unopt c2^" + "^unopt c2'));
 652                           let last_tl1',(subst,metasenv,ugraph) =
 653                            match last_tl1,to1 with
 654                             | Cic.Meta (i1,l1),Some (last,coerced) ->
 655                                 last,
 656                                   fo_unif_subst test_equality_only subst context
 657                                      metasenv coerced last_tl1 ugraph
 658                             | _ -> last_tl1,(subst,metasenv,ugraph)
 659                           in
 660                           let last_tl2',(subst,metasenv,ugraph) =
 661                            match last_tl2,to2 with
 662                             | Cic.Meta (i2,l2),Some (last,coerced) ->
 663                                 last,
 664                                   fo_unif_subst test_equality_only subst context
 665                                      metasenv coerced last_tl2 ugraph
 666                             | _ -> last_tl2,(subst,metasenv,ugraph)
 667                           in
 668                         (*DEBUGGING ONLY:
 669 prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
 670 *)
 671                            let subst,metasenv,ugraph =
 672                             fo_unif_subst test_equality_only subst context
 673                              metasenv last_tl1' last_tl2' ugraph
 674                            in
 675                             fo_unif_subst test_equality_only subst context
 676                              metasenv (C.Appl l1) (C.Appl l2) ugraph)
 677 (*DEBUGGING ONLY:
 678 in
 679 let subst,metasenv,ugraph = res in
 680 prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 681 res
 682 *)
 683                   (*CSC: This is necessary because of the "elim H" tactic
 684                          where the type of H is only reducible to an
 685                          inductive type. This could be extended from inductive
 686                          types to any rigid term. However, the code is
 687                          duplicated in two places: inside applications and
 688                          outside them. Probably it would be better to
 689                          work with lambda-bar terms instead. *)
 690                   | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
 691                   | (_, Cic.MutInd _::_) ->
 692                      let t1' = R.whd ~subst context t1 in
 693                      (match t1' with
 694                           C.Appl (C.MutInd _::_) ->
 695                             fo_unif_subst test_equality_only
 696                               subst context metasenv t1' t2 ugraph
 697                         | _ -> raise (UnificationFailure (lazy "88")))
 698                   | (Cic.MutInd _::_,_) ->
 699                      let t2' = R.whd ~subst context t2 in
 700                      (match t2' with
 701                           C.Appl (C.MutInd _::_) ->
 702                             fo_unif_subst test_equality_only
 703                               subst context metasenv t1 t2' ugraph
 704                         | _ -> raise
 705                             (UnificationFailure
 706                                (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 ))))
 707                   | _ -> raise exn)))
 708    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 709        let subst', metasenv',ugraph1 =
 710         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
 711           ugraph in
 712        let subst'',metasenv'',ugraph2 =
 713         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
 714           ugraph1 in
 715        (try
 716          List.fold_left2
 717           (fun (subst,metasenv,ugraph) t1 t2 ->
 718             fo_unif_subst
 719              test_equality_only subst context metasenv t1 t2 ugraph
 720           ) (subst'',metasenv'',ugraph2) pl1 pl2
 721         with
 722          Invalid_argument _ ->
 723           raise (UnificationFailure (lazy "6.1")))
 724            (* (sprintf
 725               "Error trying to unify %s with %s: the number of branches is not the same."
 726               (CicMetaSubst.ppterm ~metasenv subst t1)
 727               (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
 728    | (C.Rel _, _) | (_,  C.Rel _) ->
 729        if t1 = t2 then
 730          subst, metasenv,ugraph
 731        else
 732         raise (UnificationFailure (lazy
 733            (sprintf
 734              "Can't unify %s with %s because they are not convertible"
 735              (CicMetaSubst.ppterm ~metasenv subst t1)
 736              (CicMetaSubst.ppterm ~metasenv subst t2))))
 737    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
 738        let subst,metasenv,beta_expanded,ugraph1 =
 739          beta_expand_many
 740            test_equality_only metasenv subst context t2 args ugraph
 741        in
 742          fo_unif_subst test_equality_only subst context metasenv
 743            (C.Meta (i,l)) beta_expanded ugraph1
 744    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
 745        let subst,metasenv,beta_expanded,ugraph1 =
 746          beta_expand_many
 747            test_equality_only metasenv subst context t1 args ugraph
 748        in
 749          fo_unif_subst test_equality_only subst context metasenv
 750            beta_expanded (C.Meta (i,l)) ugraph1
 751 (* Works iff there are no arguments applied to it; similar to the
 752    case below
 753    | (_, C.MutInd _) ->
 754        let t1' = R.whd ~subst context t1 in
 755        (match t1' with
 756             C.MutInd _ ->
 757               fo_unif_subst test_equality_only
 758                 subst context metasenv t1' t2 ugraph
 759           | _ -> raise (UnificationFailure (lazy "8")))
 760 *)
 761 (* The following idea could be exploited again; right now we have no
 762    longer any example requiring it
 763    | (C.Prod _, t2) ->
 764        let t2' = R.whd ~subst context t2 in
 765        (match t2' with
 766             C.Prod _ ->
 767               fo_unif_subst test_equality_only
 768                 subst context metasenv t1 t2' ugraph
 769           | _ -> raise (UnificationFailure (lazy "8")))
 770    | (t1, C.Prod _) ->
 771        let t1' = R.whd ~subst context t1 in
 772        (match t1' with
 773             C.Prod _ ->
 774               fo_unif_subst test_equality_only
 775                 subst context metasenv t1' t2 ugraph
 776           | _ -> (* raise (UnificationFailure "9")) *)
 777              raise
 778                 (UnificationFailure (lazy (sprintf
 779                    "Can't unify %s with %s because they are not convertible"
 780                    (CicMetaSubst.ppterm ~metasenv subst t1)
 781                    (CicMetaSubst.ppterm ~metasenv subst t2)))))
 782 *)
 783    | (_,_) ->
 784      (* delta-beta reduction should almost never be a problem for
 785         unification since:
 786          1. long computations require iota reduction
 787          2. it is extremely rare that a close term t1 (that could be unified
 788             to t2) beta-delta reduces to t1' while t2 does not beta-delta
 789             reduces in the same way. This happens only if one meta of t2
 790             occurs in head position during beta reduction. In this unluky
 791             case too much reduction will be performed on t1 and unification
 792             will surely fail. *)
 793      let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
 794      let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
 795       if t1 = t1' && t2 = t2' then
 796        raise (UnificationFailure
 797         (lazy
 798           (sprintf
 799             "Can't unify %s with %s because they are not convertible"
 800             (CicMetaSubst.ppterm ~metasenv subst t1)
 801             (CicMetaSubst.ppterm ~metasenv subst t2))))
 802       else
 803        try
 804         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
 805        with
 806           UnificationFailure _
 807         | Uncertain _ ->
 808            raise (UnificationFailure
 809             (lazy
 810               (sprintf
 811                 "Can't unify %s with %s because they are not convertible"
 812                 (CicMetaSubst.ppterm ~metasenv subst t1)
 813                 (CicMetaSubst.ppterm ~metasenv subst t2))))
 814
 815 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 816  exp_named_subst1 exp_named_subst2 ugraph
 817 =
 818  try
 819   List.fold_left2
 820    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
 821      assert (uri1=uri2) ;
 822      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
 823    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
 824  with
 825   Invalid_argument _ ->
 826    let print_ens ens =
 827     String.concat " ; "
 828      (List.map
 829        (fun (uri,t) ->
 830          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
 831        ) ens)
 832    in
 833     raise (UnificationFailure (lazy (sprintf
 834      "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))))
 835
 836 (* A substitution is a (int * Cic.term) list that associates a               *)
 837 (* metavariable i with its body.                                             *)
 838 (* metasenv is of type Cic.metasenv                                          *)
 839 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 840 (* a new substitution which is already unwinded and ready to be applied and  *)
 841 (* a new metasenv in which some hypothesis in the contexts of the            *)
 842 (* metavariables may have been restricted.                                   *)
 843 let fo_unif metasenv context t1 t2 ugraph =
 844  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 845
 846 let enrich_msg msg subst context metasenv t1 t2 ugraph =
 847  lazy (
 848   if verbose then
 849    sprintf "[Verbose] 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"
 850     (CicMetaSubst.ppterm ~metasenv subst t1)
 851     (try
 852       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 853       CicPp.ppterm ty_t1
 854     with
 855     | UnificationFailure s
 856     | Uncertain s
 857     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 858     (CicMetaSubst.ppterm ~metasenv subst t2)
 859     (try
 860       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 861       CicPp.ppterm ty_t2
 862     with
 863     | UnificationFailure s
 864     | Uncertain s
 865     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 866     (CicMetaSubst.ppcontext ~metasenv subst context)
 867     (CicMetaSubst.ppmetasenv subst metasenv)
 868     (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
 869  else
 870    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 871     (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
 872     (try
 873       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 874       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
 875     with
 876     | UnificationFailure s
 877     | Uncertain s
 878     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 879     (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
 880     (try
 881       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 882       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
 883     with
 884     | UnificationFailure s
 885     | Uncertain s
 886     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 887     (CicMetaSubst.ppcontext ~metasenv subst context)
 888     (CicMetaSubst.ppmetasenv subst metasenv)
 889     (Lazy.force msg)
 890  )
 891
 892 let fo_unif_subst subst context metasenv t1 t2 ugraph =
 893   try
 894     fo_unif_subst false subst context metasenv t1 t2 ugraph
 895   with
 896   | AssertFailure msg ->
 897      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 898   | UnificationFailure msg ->
 899      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 900 ;;