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 (lazy "4"))
 468            (* (sprintf
 469               "Can't unify %s with %s due to different inductive principles"
 470               (CicMetaSubst.ppterm subst t1)
 471               (CicMetaSubst.ppterm subst t2))) *)
 472    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 473        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 474        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 475          fo_unif_subst_exp_named_subst
 476            test_equality_only
 477            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 478        else
 479          raise (UnificationFailure (lazy "5"))
 480            (* (sprintf
 481               "Can't unify %s with %s due to different inductive constructors"
 482               (CicMetaSubst.ppterm subst t1)
 483               (CicMetaSubst.ppterm subst t2))) *)
 484    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 485    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
 486                               subst context metasenv te t2 ugraph
 487    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
 488                               subst context metasenv t1 te ugraph
 489    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 490        let subst',metasenv',ugraph1 =
 491          fo_unif_subst true subst context metasenv s1 s2 ugraph
 492        in
 493          fo_unif_subst test_equality_only
 494            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 495    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 496        let subst',metasenv',ugraph1 =
 497          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
 498        in
 499          fo_unif_subst test_equality_only
 500            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 501    | (C.LetIn (_,s1,t1), t2)
 502    | (t2, C.LetIn (_,s1,t1)) ->
 503        fo_unif_subst
 504         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
 505    | (C.Appl l1, C.Appl l2) ->
 506        (* andrea: this case should be probably rewritten in the
 507           spirit of deref *)
 508        (match l1,l2 with
 509           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
 510               (try
 511                  List.fold_left2
 512                    (fun (subst,metasenv,ugraph) t1 t2 ->
 513                       fo_unif_subst
 514                         test_equality_only subst context metasenv t1 t2 ugraph)
 515                    (subst,metasenv,ugraph) l1 l2
 516                with (Invalid_argument msg) ->
 517                  raise (UnificationFailure (lazy msg)))
 518           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
 519               (* we verify that none of the args is a Meta,
 520                 since beta expanding with respoect to a metavariable
 521                 makes no sense  *)
 522  (*
 523               (try
 524                  let (_,t,_) = CicUtil.lookup_subst i subst in
 525                  let lifted = S.subst_meta l t in
 526                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 527                    fo_unif_subst
 528                     test_equality_only
 529                      subst context metasenv reduced t2 ugraph
 530                with CicUtil.Subst_not_found _ -> *)
 531               let subst,metasenv,beta_expanded,ugraph1 =
 532                 beta_expand_many
 533                   test_equality_only metasenv subst context t2 args ugraph
 534               in
 535                 fo_unif_subst test_equality_only subst context metasenv
 536                   (C.Meta (i,l)) beta_expanded ugraph1
 537           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
 538               (* (try
 539                  let (_,t,_) = CicUtil.lookup_subst i subst in
 540                  let lifted = S.subst_meta l t in
 541                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 542                    fo_unif_subst
 543                      test_equality_only
 544                      subst context metasenv t1 reduced ugraph
 545                with CicUtil.Subst_not_found _ -> *)
 546                  let subst,metasenv,beta_expanded,ugraph1 =
 547                    beta_expand_many
 548                      test_equality_only
 549                      metasenv subst context t1 args ugraph
 550                  in
 551                    fo_unif_subst test_equality_only subst context metasenv
 552                      (C.Meta (i,l)) beta_expanded ugraph1
 553           | _,_ ->
 554               let lr1 = List.rev l1 in
 555               let lr2 = List.rev l2 in
 556               let rec
 557                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
 558                 match (l1,l2) with
 559                     [],_
 560                   | _,[] -> assert false
 561                   | ([h1],[h2]) ->
 562                       fo_unif_subst
 563                         test_equality_only subst context metasenv h1 h2 ugraph
 564                   | ([h],l)
 565                   | (l,[h]) ->
 566                       fo_unif_subst test_equality_only subst context metasenv
 567                         h (C.Appl (List.rev l)) ugraph
 568                   | ((h1::l1),(h2::l2)) ->
 569                       let subst', metasenv',ugraph1 =
 570                         fo_unif_subst
 571                           test_equality_only
 572                           subst context metasenv h1 h2 ugraph
 573                       in
 574                         fo_unif_l
 575                           test_equality_only subst' metasenv' (l1,l2) ugraph1
 576               in
 577               (try
 578                 fo_unif_l
 579                   test_equality_only subst metasenv (lr1, lr2)  ugraph
 580               with
 581               | UnificationFailure s
 582               | Uncertain s as exn ->
 583                   (match l1, l2 with
 584                   | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
 585                      (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
 586                     CoercGraph.is_a_coercion c1 &&
 587                     CoercGraph.is_a_coercion c2 &&
 588                     not (UriManager.eq uri1 uri2) ->
 589                       let body1, attrs1, ugraph =
 590                         match CicEnvironment.get_obj ugraph uri1 with
 591                         | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
 592                         | _ -> assert false
 593                       in
 594                       let body2, attrs2, ugraph =
 595                         match CicEnvironment.get_obj ugraph uri2 with
 596                         | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
 597                         | _ -> assert false
 598                       in
 599                       let is_composite1 =
 600                         List.exists
 601                          (function `Class (`Coercion _) -> true | _-> false)
 602                          attrs1
 603                       in
 604                       let is_composite2 =
 605                         List.exists
 606                          (function `Class (`Coercion _) -> true | _-> false)
 607                          attrs2
 608                       in
 609                       (match is_composite1, is_composite2 with
 610                       | false, false -> raise exn
 611                       | true, false ->
 612                           let body1 = CicSubstitution.subst_vars ens1 body1 in
 613                           let appl = Cic.Appl (body1::tl1) in
 614                           let redappl = CicReduction.head_beta_reduce appl in
 615                           fo_unif_subst
 616                             test_equality_only subst context metasenv
 617                               redappl t2 ugraph
 618                       | false, true ->
 619                           let body2 = CicSubstitution.subst_vars ens2 body2 in
 620                           let appl = Cic.Appl (body2::tl2) in
 621                           let redappl = CicReduction.head_beta_reduce appl in
 622                           fo_unif_subst
 623                             test_equality_only subst context metasenv
 624                              t1 redappl ugraph
 625                       | true, true ->
 626                           let body1 = CicSubstitution.subst_vars ens1 body1 in
 627                           let appl1 = Cic.Appl (body1::tl1) in
 628                           let redappl1 = CicReduction.head_beta_reduce appl1 in
 629                           let body2 = CicSubstitution.subst_vars ens2 body2 in
 630                           let appl2 = Cic.Appl (body2::tl2) in
 631                           let redappl2 = CicReduction.head_beta_reduce appl2 in
 632                           fo_unif_subst
 633                             test_equality_only subst context metasenv
 634                              redappl1 redappl2 ugraph)
 635                   (*CSC: This is necessary because of the "elim H" tactic
 636                          where the type of H is only reducible to an
 637                          inductive type. This could be extended from inductive
 638                          types to any rigid term. However, the code is
 639                          duplicated in two places: inside applications and
 640                          outside them. Probably it would be better to
 641                          work with lambda-bar terms instead. *)
 642                   | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
 643                   | (_, Cic.MutInd _::_) ->
 644                      let t1' = R.whd ~subst context t1 in
 645                      (match t1' with
 646                           C.Appl (C.MutInd _::_) ->
 647                             fo_unif_subst test_equality_only
 648                               subst context metasenv t1' t2 ugraph
 649                         | _ -> raise (UnificationFailure (lazy "88")))
 650                   | (Cic.MutInd _::_,_) ->
 651                      let t2' = R.whd ~subst context t2 in
 652                      (match t2' with
 653                           C.Appl (C.MutInd _::_) ->
 654                             fo_unif_subst test_equality_only
 655                               subst context metasenv t1 t2' ugraph
 656                         | _ -> raise (UnificationFailure (lazy "99")))
 657                   | _ -> raise exn)))
 658    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 659        let subst', metasenv',ugraph1 =
 660         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
 661           ugraph in
 662        let subst'',metasenv'',ugraph2 =
 663         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
 664           ugraph1 in
 665        (try
 666          List.fold_left2
 667           (fun (subst,metasenv,ugraph) t1 t2 ->
 668             fo_unif_subst
 669              test_equality_only subst context metasenv t1 t2 ugraph
 670           ) (subst'',metasenv'',ugraph2) pl1 pl2
 671         with
 672          Invalid_argument _ ->
 673           raise (UnificationFailure (lazy "6.1")))
 674            (* (sprintf
 675               "Error trying to unify %s with %s: the number of branches is not the same."
 676               (CicMetaSubst.ppterm subst t1)
 677               (CicMetaSubst.ppterm subst t2)))) *)
 678    | (C.Rel _, _) | (_,  C.Rel _) ->
 679        if t1 = t2 then
 680          subst, metasenv,ugraph
 681        else
 682         raise (UnificationFailure (lazy
 683            (sprintf
 684              "Can't unify %s with %s because they are not convertible"
 685              (CicMetaSubst.ppterm subst t1)
 686              (CicMetaSubst.ppterm subst t2))))
 687    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
 688        let subst,metasenv,beta_expanded,ugraph1 =
 689          beta_expand_many
 690            test_equality_only metasenv subst context t2 args ugraph
 691        in
 692          fo_unif_subst test_equality_only subst context metasenv
 693            (C.Meta (i,l)) beta_expanded ugraph1
 694    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
 695        let subst,metasenv,beta_expanded,ugraph1 =
 696          beta_expand_many
 697            test_equality_only metasenv subst context t1 args ugraph
 698        in
 699          fo_unif_subst test_equality_only subst context metasenv
 700            beta_expanded (C.Meta (i,l)) ugraph1
 701 (* Works iff there are no arguments applied to it; similar to the
 702    case below
 703    | (_, C.MutInd _) ->
 704        let t1' = R.whd ~subst context t1 in
 705        (match t1' with
 706             C.MutInd _ ->
 707               fo_unif_subst test_equality_only
 708                 subst context metasenv t1' t2 ugraph
 709           | _ -> raise (UnificationFailure (lazy "8")))
 710 *)
 711 (* The following idea could be exploited again; right now we have no
 712    longer any example requiring it
 713    | (C.Prod _, t2) ->
 714        let t2' = R.whd ~subst context t2 in
 715        (match t2' with
 716             C.Prod _ ->
 717               fo_unif_subst test_equality_only
 718                 subst context metasenv t1 t2' ugraph
 719           | _ -> raise (UnificationFailure (lazy "8")))
 720    | (t1, C.Prod _) ->
 721        let t1' = R.whd ~subst context t1 in
 722        (match t1' with
 723             C.Prod _ ->
 724               fo_unif_subst test_equality_only
 725                 subst context metasenv t1' t2 ugraph
 726           | _ -> (* raise (UnificationFailure "9")) *)
 727              raise
 728                 (UnificationFailure (lazy (sprintf
 729                    "Can't unify %s with %s because they are not convertible"
 730                    (CicMetaSubst.ppterm subst t1)
 731                    (CicMetaSubst.ppterm subst t2)))))
 732 *)
 733    | (_,_) ->
 734      (* delta-beta reduction should almost never be a problem for
 735         unification since:
 736          1. long computations require iota reduction
 737          2. it is extremely rare that a close term t1 (that could be unified
 738             to t2) beta-delta reduces to t1' while t2 does not beta-delta
 739             reduces in the same way. This happens only if one meta of t2
 740             occurs in head position during beta reduction. In this unluky
 741             case too much reduction will be performed on t1 and unification
 742             will surely fail. *)
 743      let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
 744      let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
 745       if t1 = t1' && t2 = t2' then
 746        raise (UnificationFailure
 747         (lazy
 748           (sprintf
 749             "Can't unify %s with %s because they are not convertible"
 750             (CicMetaSubst.ppterm subst t1)
 751             (CicMetaSubst.ppterm subst t2))))
 752       else
 753        try
 754         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
 755        with
 756           UnificationFailure _
 757         | Uncertain _ ->
 758            raise (UnificationFailure
 759             (lazy
 760               (sprintf
 761                 "Can't unify %s with %s because they are not convertible"
 762                 (CicMetaSubst.ppterm subst t1)
 763                 (CicMetaSubst.ppterm subst t2))))
 764
 765 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 766  exp_named_subst1 exp_named_subst2 ugraph
 767 =
 768  try
 769   List.fold_left2
 770    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
 771      assert (uri1=uri2) ;
 772      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
 773    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
 774  with
 775   Invalid_argument _ ->
 776    let print_ens ens =
 777     String.concat " ; "
 778      (List.map
 779        (fun (uri,t) ->
 780          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
 781        ) ens)
 782    in
 783     raise (UnificationFailure (lazy (sprintf
 784      "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))))
 785
 786 (* A substitution is a (int * Cic.term) list that associates a               *)
 787 (* metavariable i with its body.                                             *)
 788 (* metasenv is of type Cic.metasenv                                          *)
 789 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 790 (* a new substitution which is already unwinded and ready to be applied and  *)
 791 (* a new metasenv in which some hypothesis in the contexts of the            *)
 792 (* metavariables may have been restricted.                                   *)
 793 let fo_unif metasenv context t1 t2 ugraph =
 794  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 795
 796 let enrich_msg msg subst context metasenv t1 t2 ugraph =
 797  lazy (
 798   if verbose then
 799    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"
 800     (CicMetaSubst.ppterm subst t1)
 801     (try
 802       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 803       CicPp.ppterm ty_t1
 804     with
 805     | UnificationFailure s
 806     | Uncertain s
 807     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 808     (CicMetaSubst.ppterm subst t2)
 809     (try
 810       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 811       CicPp.ppterm ty_t2
 812     with
 813     | UnificationFailure s
 814     | Uncertain s
 815     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 816     (CicMetaSubst.ppcontext subst context)
 817     (CicMetaSubst.ppmetasenv subst metasenv)
 818     (CicMetaSubst.ppsubst subst) (Lazy.force msg)
 819  else
 820    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 821     (CicMetaSubst.ppterm_in_context subst t1 context)
 822     (try
 823       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 824       CicMetaSubst.ppterm_in_context subst ty_t1 context
 825     with
 826     | UnificationFailure s
 827     | Uncertain s
 828     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 829     (CicMetaSubst.ppterm_in_context subst t2 context)
 830     (try
 831       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 832       CicMetaSubst.ppterm_in_context subst ty_t2 context
 833     with
 834     | UnificationFailure s
 835     | Uncertain s
 836     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 837     (CicMetaSubst.ppcontext subst context)
 838     (CicMetaSubst.ppmetasenv subst metasenv)
 839     (Lazy.force msg)
 840  )
 841
 842 let fo_unif_subst subst context metasenv t1 t2 ugraph =
 843   try
 844     fo_unif_subst false subst context metasenv t1 t2 ugraph
 845   with
 846   | AssertFailure msg ->
 847      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 848   | UnificationFailure msg ->
 849      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 850 ;;