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