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 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
 306   match xxx with
 307   | [] -> ()
 308   | (m2,_,c2,c2')::_ ->
 309      let m1,c1,c1' = carr,to1,to2 in
 310      let unopt =
 311        function Some (_,t) -> CicPp.ppterm t
 312        | None -> "id"
 313      in
 314      HLog.warn
 315        ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
 316        CoercDb.string_of_carr car2^": " ^
 317        CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
 318        unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
 319        unopt c2^" + "^unopt c2')
 320
 321 (* NUOVA UNIFICAZIONE *)
 322 (* A substitution is a (int * Cic.term) list that associates a
 323    metavariable i with its body.
 324    A metaenv is a (int * Cic.term) list that associate a metavariable
 325    i with is type.
 326    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
 327    a new substitution which is _NOT_ unwinded. It must be unwinded before
 328    applying it. *)
 329
 330 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
 331  let module C = Cic in
 332  let module R = CicReduction in
 333  let module S = CicSubstitution in
 334  let t1 = deref subst t1 in
 335  let t2 = deref subst t2 in
 336  let (&&&) a b = (a && b) || ((not a) && (not b)) in
 337 (* let bef = Sys.time () in *)
 338  let b,ugraph =
 339   if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
 340    false,ugraph
 341   else
 342 let foo () =
 343    R.are_convertible ~subst ~metasenv context t1 t2 ugraph
 344 in profiler_are_convertible.HExtlib.profile foo ()
 345  in
 346 (* let aft = Sys.time () in
 347 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
 348 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
 349 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
 350    if b then
 351      subst, metasenv, ugraph
 352    else
 353    match (t1, t2) with
 354      | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
 355          let _,subst,metasenv,ugraph1 =
 356            (try
 357               List.fold_left2
 358                 (fun (j,subst,metasenv,ugraph) t1 t2 ->
 359                    match t1,t2 with
 360                        None,_
 361                      | _,None -> j+1,subst,metasenv,ugraph
 362                      | Some t1', Some t2' ->
 363                          (* First possibility:  restriction    *)
 364                          (* Second possibility: unification    *)
 365                          (* Third possibility:  convertibility *)
 366                          let b, ugraph1 =
 367                          R.are_convertible
 368                            ~subst ~metasenv context t1' t2' ugraph
 369                          in
 370                          if b then
 371                            j+1,subst,metasenv, ugraph1
 372                          else
 373                            (try
 374                               let subst,metasenv,ugraph2 =
 375                                 fo_unif_subst
 376                                   test_equality_only
 377                                   subst context metasenv t1' t2' ugraph
 378                               in
 379                                 j+1,subst,metasenv,ugraph2
 380                             with
 381                                 Uncertain _
 382                               | UnificationFailure _ ->
 383 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
 384                                   let metasenv, subst =
 385                                     CicMetaSubst.restrict
 386                                       subst [(n,j)] metasenv in
 387                                     j+1,subst,metasenv,ugraph1)
 388                 ) (1,subst,metasenv,ugraph) ln lm
 389             with
 390                 Exit ->
 391                   raise
 392                     (UnificationFailure (lazy "1"))
 393                     (*
 394                     (sprintf
 395                       "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."
 396                       (CicMetaSubst.ppterm ~metasenv subst t1)
 397                       (CicMetaSubst.ppterm ~metasenv subst t2))) *)
 398               | Invalid_argument _ ->
 399                   raise
 400                     (UnificationFailure (lazy "2")))
 401                     (*
 402                     (sprintf
 403                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
 404                       (CicMetaSubst.ppterm ~metasenv subst t1)
 405                       (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
 406          in subst,metasenv,ugraph1
 407      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
 408          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
 409      | (C.Meta (n,l), t)
 410      | (t, C.Meta (n,l)) ->
 411          let swap =
 412            match t1,t2 with
 413                C.Meta (n,_), C.Meta (m,_) when n < m -> false
 414              | _, C.Meta _ -> false
 415              | _,_ -> true
 416          in
 417          let lower = fun x y -> if swap then y else x in
 418          let upper = fun x y -> if swap then x else y in
 419          let fo_unif_subst_ordered
 420              test_equality_only subst context metasenv m1 m2 ugraph =
 421            fo_unif_subst test_equality_only subst context metasenv
 422              (lower m1 m2) (upper m1 m2) ugraph
 423          in
 424          begin
 425          let subst,metasenv,ugraph1 =
 426            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
 427            (try
 428               let tyt,ugraph1 =
 429                 type_of_aux' metasenv subst context t ugraph
 430               in
 431                 fo_unif_subst
 432                   test_equality_only
 433                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
 434             with
 435                 UnificationFailure _ as e -> raise e
 436               | Uncertain msg -> raise (UnificationFailure msg)
 437               | AssertFailure _ ->
 438                   debug_print (lazy "siamo allo huge hack");
 439                   (* TODO huge hack!!!!
 440                    * we keep on unifying/refining in the hope that
 441                    * the problem will be eventually solved.
 442                    * In the meantime we're breaking a big invariant:
 443                    * the terms that we are unifying are no longer well
 444                    * typed in the current context (in the worst case
 445                    * we could even diverge) *)
 446                   (subst, metasenv,ugraph)) in
 447          let t',metasenv,subst =
 448            try
 449              CicMetaSubst.delift n subst context metasenv l t
 450            with
 451                (CicMetaSubst.MetaSubstFailure msg)->
 452                  raise (UnificationFailure msg)
 453              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 454          in
 455          let t'',ugraph2 =
 456            match t' with
 457                C.Sort (C.Type u) when not test_equality_only ->
 458                  let u' = CicUniv.fresh () in
 459                  let s = C.Sort (C.Type u') in
 460                   (try
 461                     let ugraph2 =
 462                      CicUniv.add_ge (upper u u') (lower u u') ugraph1
 463                     in
 464                      s,ugraph2
 465                    with
 466                     CicUniv.UniverseInconsistency msg ->
 467                      raise (UnificationFailure msg))
 468              | _ -> t',ugraph1
 469          in
 470          (* Unifying the types may have already instantiated n. Let's check *)
 471          try
 472            let (_, oldt,_) = CicUtil.lookup_subst n subst in
 473            let lifted_oldt = S.subst_meta l oldt in
 474              fo_unif_subst_ordered
 475                test_equality_only subst context metasenv t lifted_oldt ugraph2
 476          with
 477              CicUtil.Subst_not_found _ ->
 478                let (_, context, ty) = CicUtil.lookup_meta n metasenv in
 479                let subst = (n, (context, t'',ty)) :: subst in
 480                let metasenv =
 481                  List.filter (fun (m,_,_) -> not (n = m)) metasenv in
 482                subst, metasenv, ugraph2
 483          end
 484    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 485    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 486       if UriManager.eq uri1 uri2 then
 487        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 488         exp_named_subst1 exp_named_subst2 ugraph
 489       else
 490        raise (UnificationFailure (lazy
 491           (sprintf
 492             "Can't unify %s with %s due to different constants"
 493             (CicMetaSubst.ppterm ~metasenv subst t1)
 494             (CicMetaSubst.ppterm ~metasenv subst t2))))
 495    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 496        if UriManager.eq uri1 uri2 && i1 = i2 then
 497          fo_unif_subst_exp_named_subst
 498            test_equality_only
 499            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 500        else
 501          raise (UnificationFailure
 502            (lazy
 503             (sprintf
 504              "Can't unify %s with %s due to different inductive principles"
 505              (CicMetaSubst.ppterm ~metasenv subst t1)
 506              (CicMetaSubst.ppterm ~metasenv subst t2))))
 507    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 508        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 509        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 510          fo_unif_subst_exp_named_subst
 511            test_equality_only
 512            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 513        else
 514          raise (UnificationFailure
 515           (lazy
 516             (sprintf
 517               "Can't unify %s with %s due to different inductive constructors"
 518               (CicMetaSubst.ppterm ~metasenv subst t1)
 519               (CicMetaSubst.ppterm ~metasenv subst t2))))
 520    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 521    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
 522                               subst context metasenv te t2 ugraph
 523    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
 524                               subst context metasenv t1 te ugraph
 525    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 526        let subst',metasenv',ugraph1 =
 527          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
 528        in
 529          fo_unif_subst test_equality_only
 530            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 531    | (C.LetIn (_,s1,ty1,t1), t2)
 532    | (t2, C.LetIn (_,s1,ty1,t1)) ->
 533        fo_unif_subst
 534         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
 535    | (C.Appl l1, C.Appl l2) ->
 536        (* andrea: this case should be probably rewritten in the
 537           spirit of deref *)
 538        (match l1,l2 with
 539           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
 540               (try
 541                  List.fold_left2
 542                    (fun (subst,metasenv,ugraph) t1 t2 ->
 543                       fo_unif_subst
 544                         test_equality_only subst context metasenv t1 t2 ugraph)
 545                    (subst,metasenv,ugraph) l1 l2
 546                with (Invalid_argument msg) ->
 547                  raise (UnificationFailure (lazy msg)))
 548           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
 549               (* we verify that none of the args is a Meta,
 550                 since beta expanding with respoect to a metavariable
 551                 makes no sense  *)
 552  (*
 553               (try
 554                  let (_,t,_) = CicUtil.lookup_subst i subst in
 555                  let lifted = S.subst_meta l t in
 556                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 557                    fo_unif_subst
 558                     test_equality_only
 559                      subst context metasenv reduced t2 ugraph
 560                with CicUtil.Subst_not_found _ -> *)
 561               let subst,metasenv,beta_expanded,ugraph1 =
 562                 beta_expand_many
 563                   test_equality_only metasenv subst context t2 args ugraph
 564               in
 565                 fo_unif_subst test_equality_only subst context metasenv
 566                   (C.Meta (i,l)) beta_expanded ugraph1
 567           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
 568               (* (try
 569                  let (_,t,_) = CicUtil.lookup_subst i subst in
 570                  let lifted = S.subst_meta l t in
 571                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 572                    fo_unif_subst
 573                      test_equality_only
 574                      subst context metasenv t1 reduced ugraph
 575                with CicUtil.Subst_not_found _ -> *)
 576                  let subst,metasenv,beta_expanded,ugraph1 =
 577                    beta_expand_many
 578                      test_equality_only
 579                      metasenv subst context t1 args ugraph
 580                  in
 581                    fo_unif_subst test_equality_only subst context metasenv
 582                      (C.Meta (i,l)) beta_expanded ugraph1
 583           | _,_ ->
 584               let lr1 = List.rev l1 in
 585               let lr2 = List.rev l2 in
 586               let rec
 587                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
 588                 match (l1,l2) with
 589                     [],_
 590                   | _,[] -> assert false
 591                   | ([h1],[h2]) ->
 592                       fo_unif_subst
 593                         test_equality_only subst context metasenv h1 h2 ugraph
 594                   | ([h],l)
 595                   | (l,[h]) ->
 596                       fo_unif_subst test_equality_only subst context metasenv
 597                         h (C.Appl (List.rev l)) ugraph
 598                   | ((h1::l1),(h2::l2)) ->
 599                       let subst', metasenv',ugraph1 =
 600                         fo_unif_subst
 601                           test_equality_only
 602                           subst context metasenv h1 h2 ugraph
 603                       in
 604                         fo_unif_l
 605                           test_equality_only subst' metasenv' (l1,l2) ugraph1
 606               in
 607               (try
 608                 fo_unif_l
 609                   test_equality_only subst metasenv (lr1, lr2)  ugraph
 610               with
 611               | UnificationFailure s
 612               | Uncertain s as exn ->
 613                   (match l1, l2 with
 614                             (* {{{ pullback *)
 615                   | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
 616                      (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
 617                     CoercDb.is_a_coercion cc1 <> None &&
 618                     CoercDb.is_a_coercion cc2 <> None &&
 619                     not (UriManager.eq uri1 uri2) ->
 620 (*DEBUGGING ONLY:
 621 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 622 *)
 623                      let inner_coerced ?(skip_non_c=false) t =
 624                       let t = CicMetaSubst.apply_subst subst t in
 625                       let rec aux c x t =
 626                         match t with
 627                         | Cic.Appl l ->
 628                             (match CoercGraph.coerced_arg l with
 629                             | None when skip_non_c ->
 630                                 aux c (HExtlib.list_last l)
 631                                  (HExtlib.list_last l)
 632                             | None -> c, x
 633                             | Some (t,_) -> aux (List.hd l) t t)
 634                         | _ ->  c, x
 635                       in
 636                       aux (Cic.Implicit None) (Cic.Implicit None) t
 637                      in
 638                       let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
 639                       let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
 640                       let car1, car2 =
 641                         match
 642                           CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
 643                         with
 644                         | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
 645                         | _ -> assert false
 646                       in
 647                       let head1_c, head2_c =
 648                         match
 649                           CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
 650                         with
 651                         | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
 652                         | _ -> assert false
 653                       in
 654                       let unfold uri ens args =
 655                         let o, _ =
 656                           CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
 657                         in
 658                         assert (ens = []);
 659                         match o with
 660                         | Cic.Constant (_,Some bo,_,_,_) ->
 661                             CicReduction.head_beta_reduce ~delta:false
 662                               (Cic.Appl (bo::args))
 663                         | _ -> assert false
 664                       in
 665                       let conclude subst metasenv ugraph last_tl1' last_tl2' =
 666                        let subst',metasenv,ugraph =
 667 (*DEBUGGING ONLY:
 668 prerr_endline
 669   ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
 670    " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
 671 *)
 672                         fo_unif_subst test_equality_only subst context
 673                          metasenv last_tl1' last_tl2' ugraph
 674                        in
 675                        if subst = subst' then raise exn
 676                        else
 677 (*DEBUGGING ONLY:
 678 let subst,metasenv,ugrph as res =
 679 *)
 680                         fo_unif_subst test_equality_only subst' context
 681                          metasenv (C.Appl l1) (C.Appl l2) ugraph
 682 (*DEBUGGING ONLY:
 683 in
 684 (prerr_endline
 685   (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
 686    " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 687 res)
 688 *)
 689                       in
 690                       if CoercDb.eq_carr car1 car2 then
 691                          match last_tl1,last_tl2 with
 692                          | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
 693                          | _, C.Meta _
 694                          | C.Meta _, _ ->
 695                            let subst,metasenv,ugraph =
 696                             fo_unif_subst test_equality_only subst context
 697                              metasenv last_tl1 last_tl2 ugraph
 698                            in
 699                             fo_unif_subst test_equality_only subst context
 700                              metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
 701                          | _ when CoercDb.eq_carr head1_c head2_c ->
 702                              (* composite VS composition + metas avoiding
 703                               * coercions not only in coerced position    *)
 704                              if c1 <> cc1 && c2 <> cc2 then
 705                                conclude subst metasenv ugraph
 706                                 last_tl1 last_tl2
 707                              else
 708                               let l1, l2 =
 709                                if c1 = cc1 then
 710                                  unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
 711                                else
 712                                  Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
 713                               in
 714                                fo_unif_subst test_equality_only subst context
 715                                 metasenv l1 l2 ugraph
 716                          | _ -> raise exn
 717                       else
 718                       let grow1 =
 719                         match last_tl1 with Cic.Meta _ -> true | _ -> false in
 720                       let grow2 =
 721                         match last_tl2 with Cic.Meta _ -> true | _ -> false in
 722                       if not (grow1 || grow2) then
 723                         let _,last_tl1 =
 724                           inner_coerced ~skip_non_c:true (Cic.Appl l1) in
 725                         let _,last_tl2 =
 726                           inner_coerced ~skip_non_c:true  (Cic.Appl l2) in
 727                         conclude subst metasenv ugraph last_tl1 last_tl2
 728                       else
 729                         let meets =
 730                            CoercGraph.meets
 731                             metasenv subst context (grow1,car1) (grow2,car2)
 732                         in
 733                         (match meets with
 734                         | [] -> raise exn
 735                         | (carr,metasenv,to1,to2)::xxx ->
 736                            warn_if_not_unique xxx to1 to2 carr car1 car2;
 737                            let last_tl1',(subst,metasenv,ugraph) =
 738                             match grow1,to1 with
 739                              | true,Some (last,coerced) ->
 740                                  last,
 741                                   fo_unif_subst test_equality_only subst context
 742                                   metasenv coerced last_tl1 ugraph
 743                              | _ -> last_tl1,(subst,metasenv,ugraph)
 744                            in
 745                            let last_tl2',(subst,metasenv,ugraph) =
 746                             match grow2,to2 with
 747                              | true,Some (last,coerced) ->
 748                                  last,
 749                                   fo_unif_subst test_equality_only subst context
 750                                   metasenv coerced last_tl2 ugraph
 751                              | _ -> last_tl2,(subst,metasenv,ugraph)
 752                            in
 753                            conclude subst metasenv ugraph last_tl1' last_tl2')
 754                         (* }}} pullback *)
 755                   (* {{{ CSC: This is necessary because of the "elim H" tactic
 756                          where the type of H is only reducible to an
 757                          inductive type. This could be extended from inductive
 758                          types to any rigid term. However, the code is
 759                          duplicated in two places: inside applications and
 760                          outside them. Probably it would be better to
 761                          work with lambda-bar terms instead. *)
 762                   | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
 763                   | (_, Cic.MutInd _::_) ->
 764                      let t1' = R.whd ~subst context t1 in
 765                      (match t1' with
 766                           C.Appl (C.MutInd _::_) ->
 767                             fo_unif_subst test_equality_only
 768                               subst context metasenv t1' t2 ugraph
 769                         | _ -> raise (UnificationFailure (lazy "88")))
 770                   | (Cic.MutInd _::_,_) ->
 771                      let t2' = R.whd ~subst context t2 in
 772                      (match t2' with
 773                           C.Appl (C.MutInd _::_) ->
 774                             fo_unif_subst test_equality_only
 775                               subst context metasenv t1 t2' ugraph
 776                         | _ -> raise
 777                             (UnificationFailure
 778                                (lazy ("not a mutind :"^
 779                                 CicMetaSubst.ppterm ~metasenv subst t2 ))))
 780                      (* }}} elim H *)
 781                   | _ -> raise exn)))
 782    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 783        let subst', metasenv',ugraph1 =
 784         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
 785           ugraph in
 786        let subst'',metasenv'',ugraph2 =
 787         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
 788           ugraph1 in
 789        (try
 790          List.fold_left2
 791           (fun (subst,metasenv,ugraph) t1 t2 ->
 792             fo_unif_subst
 793              test_equality_only subst context metasenv t1 t2 ugraph
 794           ) (subst'',metasenv'',ugraph2) pl1 pl2
 795         with
 796          Invalid_argument _ ->
 797           raise (UnificationFailure (lazy "6.1")))
 798            (* (sprintf
 799               "Error trying to unify %s with %s: the number of branches is not the same."
 800               (CicMetaSubst.ppterm ~metasenv subst t1)
 801               (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
 802    | (C.Rel _, _) | (_,  C.Rel _) ->
 803        if t1 = t2 then
 804          subst, metasenv,ugraph
 805        else
 806         raise (UnificationFailure (lazy
 807            (sprintf
 808              "Can't unify %s with %s because they are not convertible"
 809              (CicMetaSubst.ppterm ~metasenv subst t1)
 810              (CicMetaSubst.ppterm ~metasenv subst t2))))
 811    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
 812        let subst,metasenv,beta_expanded,ugraph1 =
 813          beta_expand_many
 814            test_equality_only metasenv subst context t2 args ugraph
 815        in
 816          fo_unif_subst test_equality_only subst context metasenv
 817            (C.Meta (i,l)) beta_expanded ugraph1
 818    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
 819        let subst,metasenv,beta_expanded,ugraph1 =
 820          beta_expand_many
 821            test_equality_only metasenv subst context t1 args ugraph
 822        in
 823          fo_unif_subst test_equality_only subst context metasenv
 824            beta_expanded (C.Meta (i,l)) ugraph1
 825 (* Works iff there are no arguments applied to it; similar to the
 826    case below
 827    | (_, C.MutInd _) ->
 828        let t1' = R.whd ~subst context t1 in
 829        (match t1' with
 830             C.MutInd _ ->
 831               fo_unif_subst test_equality_only
 832                 subst context metasenv t1' t2 ugraph
 833           | _ -> raise (UnificationFailure (lazy "8")))
 834 *)
 835    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 836        let subst',metasenv',ugraph1 =
 837          fo_unif_subst true subst context metasenv s1 s2 ugraph
 838        in
 839          fo_unif_subst test_equality_only
 840            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 841    | (C.Prod _, _) ->
 842        (match CicReduction.whd ~subst context t2 with
 843         | C.Prod _ as t2 ->
 844             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
 845         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
 846    | (_, C.Prod _) ->
 847        (match CicReduction.whd ~subst context t1 with
 848         | C.Prod _ as t1 ->
 849             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
 850         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
 851    | (_,_) ->
 852      (* delta-beta reduction should almost never be a problem for
 853         unification since:
 854          1. long computations require iota reduction
 855          2. it is extremely rare that a close term t1 (that could be unified
 856             to t2) beta-delta reduces to t1' while t2 does not beta-delta
 857             reduces in the same way. This happens only if one meta of t2
 858             occurs in head position during beta reduction. In this unluky
 859             case too much reduction will be performed on t1 and unification
 860             will surely fail. *)
 861      let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
 862      let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
 863       if t1 = t1' && t2 = t2' then
 864        raise (UnificationFailure
 865         (lazy
 866           (sprintf
 867             "Can't unify %s with %s because they are not convertible"
 868             (CicMetaSubst.ppterm ~metasenv subst t1)
 869             (CicMetaSubst.ppterm ~metasenv subst t2))))
 870       else
 871        try
 872         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
 873        with
 874           UnificationFailure _
 875         | Uncertain _ ->
 876            raise (UnificationFailure
 877             (lazy
 878               (sprintf
 879                 "Can't unify %s with %s because they are not convertible"
 880                 (CicMetaSubst.ppterm ~metasenv subst t1)
 881                 (CicMetaSubst.ppterm ~metasenv subst t2))))
 882
 883 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 884  exp_named_subst1 exp_named_subst2 ugraph
 885 =
 886  try
 887   List.fold_left2
 888    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
 889      assert (uri1=uri2) ;
 890      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
 891    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
 892  with
 893   Invalid_argument _ ->
 894    let print_ens ens =
 895     String.concat " ; "
 896      (List.map
 897        (fun (uri,t) ->
 898          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
 899        ) ens)
 900    in
 901     raise (UnificationFailure (lazy (sprintf
 902      "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))))
 903
 904 (* A substitution is a (int * Cic.term) list that associates a               *)
 905 (* metavariable i with its body.                                             *)
 906 (* metasenv is of type Cic.metasenv                                          *)
 907 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 908 (* a new substitution which is already unwinded and ready to be applied and  *)
 909 (* a new metasenv in which some hypothesis in the contexts of the            *)
 910 (* metavariables may have been restricted.                                   *)
 911 let fo_unif metasenv context t1 t2 ugraph =
 912  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 913
 914 let enrich_msg msg subst context metasenv t1 t2 ugraph =
 915  lazy (
 916   if verbose then
 917    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"
 918     (CicMetaSubst.ppterm ~metasenv subst t1)
 919     (try
 920       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 921       CicPp.ppterm ty_t1
 922     with
 923     | UnificationFailure s
 924     | Uncertain s
 925     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 926     (CicMetaSubst.ppterm ~metasenv subst t2)
 927     (try
 928       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 929       CicPp.ppterm ty_t2
 930     with
 931     | UnificationFailure s
 932     | Uncertain s
 933     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 934     (CicMetaSubst.ppcontext ~metasenv subst context)
 935     (CicMetaSubst.ppmetasenv subst metasenv)
 936     (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
 937  else
 938    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 939     (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
 940     (try
 941       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 942       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
 943     with
 944     | UnificationFailure s
 945     | Uncertain s
 946     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 947     (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
 948     (try
 949       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 950       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
 951     with
 952     | UnificationFailure s
 953     | Uncertain s
 954     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 955     (CicMetaSubst.ppcontext ~metasenv subst context)
 956     (CicMetaSubst.ppmetasenv subst metasenv)
 957     (Lazy.force msg)
 958  )
 959
 960 let fo_unif_subst subst context metasenv t1 t2 ugraph =
 961   try
 962     fo_unif_subst false subst context metasenv t1 t2 ugraph
 963   with
 964   | AssertFailure msg ->
 965      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 966   | UnificationFailure msg ->
 967      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 968 ;;