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