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