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 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") ~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 (subst,metasenv,t,ugraph) ->
 294          let subst,metasenv,t,ugraph1 =
 295            beta_expand test_equality_only
 296              metasenv subst context t arg ugraph
 297          in
 298            subst,metasenv,t,ugraph1
 299       ) args (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                     CoercGraph.is_a_coercion c1 &&
 597                     CoercGraph.is_a_coercion c2 &&
 598                     not (UriManager.eq uri1 uri2) ->
 599                       let body1, attrs1, ugraph =
 600                         match CicEnvironment.get_obj ugraph uri1 with
 601                         | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
 602                         | _ -> assert false
 603                       in
 604                       let body2, attrs2, ugraph =
 605                         match CicEnvironment.get_obj ugraph uri2 with
 606                         | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
 607                         | _ -> assert false
 608                       in
 609                       let is_composite1 =
 610                         List.exists
 611                          (function `Class (`Coercion _) -> true | _-> false)
 612                          attrs1
 613                       in
 614                       let is_composite2 =
 615                         List.exists
 616                          (function `Class (`Coercion _) -> true | _-> false)
 617                          attrs2
 618                       in
 619                       (match is_composite1, is_composite2 with
 620                       | false, false -> raise exn
 621                       | true, false ->
 622                           let body1 = CicSubstitution.subst_vars ens1 body1 in
 623                           let appl = Cic.Appl (body1::tl1) in
 624                           let redappl = CicReduction.head_beta_reduce appl in
 625                           fo_unif_subst
 626                             test_equality_only subst context metasenv
 627                               redappl t2 ugraph
 628                       | false, true ->
 629                           let body2 = CicSubstitution.subst_vars ens2 body2 in
 630                           let appl = Cic.Appl (body2::tl2) in
 631                           let redappl = CicReduction.head_beta_reduce appl in
 632                           fo_unif_subst
 633                             test_equality_only subst context metasenv
 634                              t1 redappl ugraph
 635                       | true, true ->
 636                           let body1 = CicSubstitution.subst_vars ens1 body1 in
 637                           let appl1 = Cic.Appl (body1::tl1) in
 638                           let redappl1 = CicReduction.head_beta_reduce appl1 in
 639                           let body2 = CicSubstitution.subst_vars ens2 body2 in
 640                           let appl2 = Cic.Appl (body2::tl2) in
 641                           let redappl2 = CicReduction.head_beta_reduce appl2 in
 642                           fo_unif_subst
 643                             test_equality_only subst context metasenv
 644                              redappl1 redappl2 ugraph)
 645                   (*CSC: This is necessary because of the "elim H" tactic
 646                          where the type of H is only reducible to an
 647                          inductive type. This could be extended from inductive
 648                          types to any rigid term. However, the code is
 649                          duplicated in two places: inside applications and
 650                          outside them. Probably it would be better to
 651                          work with lambda-bar terms instead. *)
 652                   | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
 653                   | (_, Cic.MutInd _::_) ->
 654                      let t1' = R.whd ~subst context t1 in
 655                      (match t1' with
 656                           C.Appl (C.MutInd _::_) ->
 657                             fo_unif_subst test_equality_only
 658                               subst context metasenv t1' t2 ugraph
 659                         | _ -> raise (UnificationFailure (lazy "88")))
 660                   | (Cic.MutInd _::_,_) ->
 661                      let t2' = R.whd ~subst context t2 in
 662                      (match t2' with
 663                           C.Appl (C.MutInd _::_) ->
 664                             fo_unif_subst test_equality_only
 665                               subst context metasenv t1 t2' ugraph
 666                         | _ -> raise
 667                             (UnificationFailure
 668                                (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 ))))
 669                   | _ -> raise exn)))
 670    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 671        let subst', metasenv',ugraph1 =
 672         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
 673           ugraph in
 674        let subst'',metasenv'',ugraph2 =
 675         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
 676           ugraph1 in
 677        (try
 678          List.fold_left2
 679           (fun (subst,metasenv,ugraph) t1 t2 ->
 680             fo_unif_subst
 681              test_equality_only subst context metasenv t1 t2 ugraph
 682           ) (subst'',metasenv'',ugraph2) pl1 pl2
 683         with
 684          Invalid_argument _ ->
 685           raise (UnificationFailure (lazy "6.1")))
 686            (* (sprintf
 687               "Error trying to unify %s with %s: the number of branches is not the same."
 688               (CicMetaSubst.ppterm ~metasenv subst t1)
 689               (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
 690    | (C.Rel _, _) | (_,  C.Rel _) ->
 691        if t1 = t2 then
 692          subst, metasenv,ugraph
 693        else
 694         raise (UnificationFailure (lazy
 695            (sprintf
 696              "Can't unify %s with %s because they are not convertible"
 697              (CicMetaSubst.ppterm ~metasenv subst t1)
 698              (CicMetaSubst.ppterm ~metasenv subst t2))))
 699    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
 700        let subst,metasenv,beta_expanded,ugraph1 =
 701          beta_expand_many
 702            test_equality_only metasenv subst context t2 args ugraph
 703        in
 704          fo_unif_subst test_equality_only subst context metasenv
 705            (C.Meta (i,l)) beta_expanded ugraph1
 706    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
 707        let subst,metasenv,beta_expanded,ugraph1 =
 708          beta_expand_many
 709            test_equality_only metasenv subst context t1 args ugraph
 710        in
 711          fo_unif_subst test_equality_only subst context metasenv
 712            beta_expanded (C.Meta (i,l)) ugraph1
 713 (* Works iff there are no arguments applied to it; similar to the
 714    case below
 715    | (_, C.MutInd _) ->
 716        let t1' = R.whd ~subst context t1 in
 717        (match t1' with
 718             C.MutInd _ ->
 719               fo_unif_subst test_equality_only
 720                 subst context metasenv t1' t2 ugraph
 721           | _ -> raise (UnificationFailure (lazy "8")))
 722 *)
 723 (* The following idea could be exploited again; right now we have no
 724    longer any example requiring it
 725    | (C.Prod _, t2) ->
 726        let t2' = R.whd ~subst context t2 in
 727        (match t2' with
 728             C.Prod _ ->
 729               fo_unif_subst test_equality_only
 730                 subst context metasenv t1 t2' ugraph
 731           | _ -> raise (UnificationFailure (lazy "8")))
 732    | (t1, C.Prod _) ->
 733        let t1' = R.whd ~subst context t1 in
 734        (match t1' with
 735             C.Prod _ ->
 736               fo_unif_subst test_equality_only
 737                 subst context metasenv t1' t2 ugraph
 738           | _ -> (* raise (UnificationFailure "9")) *)
 739              raise
 740                 (UnificationFailure (lazy (sprintf
 741                    "Can't unify %s with %s because they are not convertible"
 742                    (CicMetaSubst.ppterm ~metasenv subst t1)
 743                    (CicMetaSubst.ppterm ~metasenv subst t2)))))
 744 *)
 745    | (_,_) ->
 746      (* delta-beta reduction should almost never be a problem for
 747         unification since:
 748          1. long computations require iota reduction
 749          2. it is extremely rare that a close term t1 (that could be unified
 750             to t2) beta-delta reduces to t1' while t2 does not beta-delta
 751             reduces in the same way. This happens only if one meta of t2
 752             occurs in head position during beta reduction. In this unluky
 753             case too much reduction will be performed on t1 and unification
 754             will surely fail. *)
 755      let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
 756      let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
 757       if t1 = t1' && t2 = t2' then
 758        raise (UnificationFailure
 759         (lazy
 760           (sprintf
 761             "Can't unify %s with %s because they are not convertible"
 762             (CicMetaSubst.ppterm ~metasenv subst t1)
 763             (CicMetaSubst.ppterm ~metasenv subst t2))))
 764       else
 765        try
 766         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
 767        with
 768           UnificationFailure _
 769         | Uncertain _ ->
 770            raise (UnificationFailure
 771             (lazy
 772               (sprintf
 773                 "Can't unify %s with %s because they are not convertible"
 774                 (CicMetaSubst.ppterm ~metasenv subst t1)
 775                 (CicMetaSubst.ppterm ~metasenv subst t2))))
 776
 777 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 778  exp_named_subst1 exp_named_subst2 ugraph
 779 =
 780  try
 781   List.fold_left2
 782    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
 783      assert (uri1=uri2) ;
 784      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
 785    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
 786  with
 787   Invalid_argument _ ->
 788    let print_ens ens =
 789     String.concat " ; "
 790      (List.map
 791        (fun (uri,t) ->
 792          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
 793        ) ens)
 794    in
 795     raise (UnificationFailure (lazy (sprintf
 796      "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))))
 797
 798 (* A substitution is a (int * Cic.term) list that associates a               *)
 799 (* metavariable i with its body.                                             *)
 800 (* metasenv is of type Cic.metasenv                                          *)
 801 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 802 (* a new substitution which is already unwinded and ready to be applied and  *)
 803 (* a new metasenv in which some hypothesis in the contexts of the            *)
 804 (* metavariables may have been restricted.                                   *)
 805 let fo_unif metasenv context t1 t2 ugraph =
 806  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 807
 808 let enrich_msg msg subst context metasenv t1 t2 ugraph =
 809  lazy (
 810   if verbose then
 811    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"
 812     (CicMetaSubst.ppterm ~metasenv subst t1)
 813     (try
 814       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 815       CicPp.ppterm ty_t1
 816     with
 817     | UnificationFailure s
 818     | Uncertain s
 819     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 820     (CicMetaSubst.ppterm ~metasenv subst t2)
 821     (try
 822       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 823       CicPp.ppterm ty_t2
 824     with
 825     | UnificationFailure s
 826     | Uncertain s
 827     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 828     (CicMetaSubst.ppcontext ~metasenv subst context)
 829     (CicMetaSubst.ppmetasenv subst metasenv)
 830     (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
 831  else
 832    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 833     (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
 834     (try
 835       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 836       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
 837     with
 838     | UnificationFailure s
 839     | Uncertain s
 840     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 841     (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
 842     (try
 843       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 844       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
 845     with
 846     | UnificationFailure s
 847     | Uncertain s
 848     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 849     (CicMetaSubst.ppcontext ~metasenv subst context)
 850     (CicMetaSubst.ppmetasenv subst metasenv)
 851     (Lazy.force msg)
 852  )
 853
 854 let fo_unif_subst subst context metasenv t1 t2 ugraph =
 855   try
 856     fo_unif_subst false subst context metasenv t1 t2 ugraph
 857   with
 858   | AssertFailure msg ->
 859      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 860   | UnificationFailure msg ->
 861      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 862 ;;