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