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