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