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