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 type_of_aux' metasenv subst context term ugraph =
  43 let foo () =
  44   try
  45     CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
  46   with
  47       CicTypeChecker.TypeCheckerFailure msg ->
  48         let msg =
  49          lazy
  50           (sprintf
  51            "Kernel Type checking error:
  52 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
  53              (CicMetaSubst.ppterm subst term)
  54              (CicMetaSubst.ppterm [] term)
  55              (CicMetaSubst.ppcontext subst context)
  56              (CicMetaSubst.ppmetasenv subst metasenv)
  57              (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
  58         raise (AssertFailure msg)
  59     | CicTypeChecker.AssertFailure msg ->
  60         let msg = lazy
  61          (sprintf
  62            "Kernel Type checking assertion failure:
  63 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
  64              (CicMetaSubst.ppterm subst term)
  65              (CicMetaSubst.ppterm [] term)
  66              (CicMetaSubst.ppcontext subst context)
  67              (CicMetaSubst.ppmetasenv subst metasenv)
  68              (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
  69         raise (AssertFailure msg)
  70 in profiler_toa.HExtlib.profile foo ()
  71 ;;
  72
  73 let exists_a_meta l =
  74   List.exists (function Cic.Meta _ -> true | _ -> false) l
  75
  76 let rec deref subst t =
  77   let snd (_,a,_) = a in
  78   match t with
  79       Cic.Meta(n,l) ->
  80         (try
  81            deref subst
  82              (CicSubstitution.subst_meta
  83                 l (snd (CicUtil.lookup_subst n subst)))
  84          with
  85              CicUtil.Subst_not_found _ -> t)
  86     | Cic.Appl(Cic.Meta(n,l)::args) ->
  87         (match deref subst (Cic.Meta(n,l)) with
  88            | Cic.Lambda _ as t ->
  89                deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
  90            | r -> Cic.Appl(r::args))
  91     | Cic.Appl(((Cic.Lambda _) as t)::args) ->
  92            deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
  93     | t -> t
  94 ;;
  95
  96 let deref subst t =
  97  let foo () = deref subst t
  98  in profiler_deref.HExtlib.profile foo ()
  99
 100 exception WrongShape;;
 101 let eta_reduce after_beta_expansion after_beta_expansion_body
 102      before_beta_expansion
 103  =
 104  try
 105   match before_beta_expansion,after_beta_expansion_body with
 106      Cic.Appl l, Cic.Appl l' ->
 107       let rec all_but_last check_last =
 108        function
 109           [] -> assert false
 110         | [Cic.Rel 1] -> []
 111         | [_] -> if check_last then raise WrongShape else []
 112         | he::tl -> he::(all_but_last check_last tl)
 113       in
 114        let all_but_last check_last l =
 115         match all_but_last check_last l with
 116            [] -> assert false
 117          | [he] -> he
 118          | l -> Cic.Appl l
 119        in
 120        let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
 121        let all_but_last = all_but_last false l in
 122         (* here we should test alpha-equivalence; however we know by
 123            construction that here alpha_equivalence is equivalent to = *)
 124         if t = all_but_last then
 125          all_but_last
 126         else
 127          after_beta_expansion
 128    | _,_ -> after_beta_expansion
 129  with
 130   WrongShape -> after_beta_expansion
 131
 132 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
 133  let module S = CicSubstitution in
 134  let module C = Cic in
 135 let foo () =
 136   let rec aux metasenv subst n context t' ugraph =
 137    try
 138
 139     let subst,metasenv,ugraph1 =
 140      fo_unif_subst test_equality_only subst context metasenv
 141       (CicSubstitution.lift n arg) t' ugraph
 142
 143     in
 144      subst,metasenv,C.Rel (1 + n),ugraph1
 145    with
 146       Uncertain _
 147     | UnificationFailure _ ->
 148        match t' with
 149         | C.Rel m  -> subst,metasenv,
 150            (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
 151         | C.Var (uri,exp_named_subst) ->
 152            let subst,metasenv,exp_named_subst',ugraph1 =
 153             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 154            in
 155             subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
 156         | C.Meta (i,l) ->
 157             (* andrea: in general, beta_expand can create badly typed
 158              terms. This happens quite seldom in practice, UNLESS we
 159              iterate on the local context. For this reason, we renounce
 160              to iterate and just lift *)
 161             let l =
 162               List.map
 163                 (function
 164                      Some t -> Some (CicSubstitution.lift 1 t)
 165                    | None -> None) l in
 166             subst, metasenv, C.Meta (i,l), ugraph
 167         | C.Sort _
 168         | C.Implicit _ as t -> subst,metasenv,t,ugraph
 169         | C.Cast (te,ty) ->
 170             let subst,metasenv,te',ugraph1 =
 171               aux metasenv subst n context te ugraph in
 172             let subst,metasenv,ty',ugraph2 =
 173               aux metasenv subst n context ty ugraph1 in
 174             (* TASSI: sure this is in serial? *)
 175             subst,metasenv,(C.Cast (te', ty')),ugraph2
 176         | C.Prod (nn,s,t) ->
 177            let subst,metasenv,s',ugraph1 =
 178              aux metasenv subst n context s ugraph in
 179            let subst,metasenv,t',ugraph2 =
 180              aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
 181                ugraph1
 182            in
 183            (* TASSI: sure this is in serial? *)
 184            subst,metasenv,(C.Prod (nn, s', t')),ugraph2
 185         | C.Lambda (nn,s,t) ->
 186            let subst,metasenv,s',ugraph1 =
 187              aux metasenv subst n context s ugraph in
 188            let subst,metasenv,t',ugraph2 =
 189             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
 190            in
 191            (* TASSI: sure this is in serial? *)
 192             subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
 193         | C.LetIn (nn,s,t) ->
 194            let subst,metasenv,s',ugraph1 =
 195              aux metasenv subst n context s ugraph in
 196            let subst,metasenv,t',ugraph2 =
 197             aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
 198               ugraph1
 199            in
 200            (* TASSI: sure this is in serial? *)
 201             subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
 202         | C.Appl l ->
 203            let subst,metasenv,revl',ugraph1 =
 204             List.fold_left
 205              (fun (subst,metasenv,appl,ugraph) t ->
 206                let subst,metasenv,t',ugraph1 =
 207                  aux metasenv subst n context t ugraph in
 208                 subst,metasenv,(t'::appl),ugraph1
 209              ) (subst,metasenv,[],ugraph) l
 210            in
 211             subst,metasenv,(C.Appl (List.rev revl')),ugraph1
 212         | C.Const (uri,exp_named_subst) ->
 213            let subst,metasenv,exp_named_subst',ugraph1 =
 214             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 215            in
 216             subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
 217         | C.MutInd (uri,i,exp_named_subst) ->
 218            let subst,metasenv,exp_named_subst',ugraph1 =
 219             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 220            in
 221             subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
 222         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 223            let subst,metasenv,exp_named_subst',ugraph1 =
 224             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 225            in
 226             subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
 227         | C.MutCase (sp,i,outt,t,pl) ->
 228            let subst,metasenv,outt',ugraph1 =
 229              aux metasenv subst n context outt ugraph in
 230            let subst,metasenv,t',ugraph2 =
 231              aux metasenv subst n context t ugraph1 in
 232            let subst,metasenv,revpl',ugraph3 =
 233             List.fold_left
 234              (fun (subst,metasenv,pl,ugraph) t ->
 235                let subst,metasenv,t',ugraph1 =
 236                  aux metasenv subst n context t ugraph in
 237                subst,metasenv,(t'::pl),ugraph1
 238              ) (subst,metasenv,[],ugraph2) pl
 239            in
 240            subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
 241            (* TASSI: not sure this is serial *)
 242         | C.Fix (i,fl) ->
 243 (*CSC: not implemented
 244            let tylen = List.length fl in
 245             let substitutedfl =
 246              List.map
 247               (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 248                fl
 249             in
 250              C.Fix (i, substitutedfl)
 251 *)
 252             subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
 253         | C.CoFix (i,fl) ->
 254 (*CSC: not implemented
 255            let tylen = List.length fl in
 256             let substitutedfl =
 257              List.map
 258               (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 259                fl
 260             in
 261              C.CoFix (i, substitutedfl)
 262
 263 *)
 264             subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
 265
 266   and aux_exp_named_subst metasenv subst n context ens ugraph =
 267    List.fold_right
 268     (fun (uri,t) (subst,metasenv,l,ugraph) ->
 269       let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
 270        subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
 271   in
 272   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
 273   let fresh_name =
 274    FreshNamesGenerator.mk_fresh_name ~subst
 275     metasenv context (Cic.Name "Hbeta") ~typ:argty
 276   in
 277    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
 278    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
 279    subst, metasenv, t'', ugraph2
 280 in profiler_beta_expand.HExtlib.profile foo ()
 281
 282
 283 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
 284   let subst,metasenv,hd,ugraph =
 285     List.fold_right
 286       (fun arg (subst,metasenv,t,ugraph) ->
 287          let subst,metasenv,t,ugraph1 =
 288            beta_expand test_equality_only
 289              metasenv subst context t arg ugraph
 290          in
 291            subst,metasenv,t,ugraph1
 292       ) args (subst,metasenv,t,ugraph)
 293   in
 294     subst,metasenv,hd,ugraph
 295
 296
 297 (* NUOVA UNIFICAZIONE *)
 298 (* A substitution is a (int * Cic.term) list that associates a
 299    metavariable i with its body.
 300    A metaenv is a (int * Cic.term) list that associate a metavariable
 301    i with is type.
 302    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
 303    a new substitution which is _NOT_ unwinded. It must be unwinded before
 304    applying it. *)
 305
 306 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
 307  let module C = Cic in
 308  let module R = CicReduction in
 309  let module S = CicSubstitution in
 310  let t1 = deref subst t1 in
 311  let t2 = deref subst t2 in
 312  let b,ugraph  =
 313 let foo () =
 314    R.are_convertible ~subst ~metasenv context t1 t2 ugraph
 315 in profiler_are_convertible.HExtlib.profile foo ()
 316  in
 317    if b then
 318      subst, metasenv, ugraph
 319    else
 320    match (t1, t2) with
 321      | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
 322          let _,subst,metasenv,ugraph1 =
 323            (try
 324               List.fold_left2
 325                 (fun (j,subst,metasenv,ugraph) t1 t2 ->
 326                    match t1,t2 with
 327                        None,_
 328                      | _,None -> j+1,subst,metasenv,ugraph
 329                      | Some t1', Some t2' ->
 330                          (* First possibility:  restriction    *)
 331                          (* Second possibility: unification    *)
 332                          (* Third possibility:  convertibility *)
 333                          let b, ugraph1 =
 334                          R.are_convertible
 335                            ~subst ~metasenv context t1' t2' ugraph
 336                          in
 337                          if b then
 338                            j+1,subst,metasenv, ugraph1
 339                          else
 340                            (try
 341                               let subst,metasenv,ugraph2 =
 342                                 fo_unif_subst
 343                                   test_equality_only
 344                                   subst context metasenv t1' t2' ugraph
 345                               in
 346                                 j+1,subst,metasenv,ugraph2
 347                             with
 348                                 Uncertain _
 349                               | UnificationFailure _ ->
 350 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
 351                                   let metasenv, subst =
 352                                     CicMetaSubst.restrict
 353                                       subst [(n,j)] metasenv in
 354                                     j+1,subst,metasenv,ugraph1)
 355                 ) (1,subst,metasenv,ugraph) ln lm
 356             with
 357                 Exit ->
 358                   raise
 359                     (UnificationFailure (lazy "1"))
 360                     (*
 361                     (sprintf
 362                       "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."
 363                       (CicMetaSubst.ppterm subst t1)
 364                       (CicMetaSubst.ppterm subst t2))) *)
 365               | Invalid_argument _ ->
 366                   raise
 367                     (UnificationFailure (lazy "2")))
 368                     (*
 369                     (sprintf
 370                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
 371                       (CicMetaSubst.ppterm subst t1)
 372                       (CicMetaSubst.ppterm subst t2)))) *)
 373          in subst,metasenv,ugraph1
 374      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
 375          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
 376      | (C.Meta (n,l), t)
 377      | (t, C.Meta (n,l)) ->
 378          let swap =
 379            match t1,t2 with
 380                C.Meta (n,_), C.Meta (m,_) when n < m -> false
 381              | _, C.Meta _ -> false
 382              | _,_ -> true
 383          in
 384          let lower = fun x y -> if swap then y else x in
 385          let upper = fun x y -> if swap then x else y in
 386          let fo_unif_subst_ordered
 387              test_equality_only subst context metasenv m1 m2 ugraph =
 388            fo_unif_subst test_equality_only subst context metasenv
 389              (lower m1 m2) (upper m1 m2) ugraph
 390          in
 391          begin
 392          let subst,metasenv,ugraph1 =
 393            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
 394            (try
 395               let tyt,ugraph1 =
 396                 type_of_aux' metasenv subst context t ugraph
 397               in
 398                 fo_unif_subst
 399                   test_equality_only
 400                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
 401             with
 402                 UnificationFailure _ as e -> raise e
 403               | Uncertain msg -> raise (UnificationFailure msg)
 404               | AssertFailure _ ->
 405                   debug_print (lazy "siamo allo huge hack");
 406                   (* TODO huge hack!!!!
 407                    * we keep on unifying/refining in the hope that
 408                    * the problem will be eventually solved.
 409                    * In the meantime we're breaking a big invariant:
 410                    * the terms that we are unifying are no longer well
 411                    * typed in the current context (in the worst case
 412                    * we could even diverge) *)
 413                   (subst, metasenv,ugraph)) in
 414          let t',metasenv,subst =
 415            try
 416              CicMetaSubst.delift n subst context metasenv l t
 417            with
 418                (CicMetaSubst.MetaSubstFailure msg)->
 419                  raise (UnificationFailure msg)
 420              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 421          in
 422          let t'',ugraph2 =
 423            match t' with
 424                C.Sort (C.Type u) when not test_equality_only ->
 425                  let u' = CicUniv.fresh () in
 426                  let s = C.Sort (C.Type u') in
 427                  let ugraph2 =
 428                    CicUniv.add_ge (upper u u') (lower u u') ugraph1
 429                  in
 430                    s,ugraph2
 431              | _ -> t',ugraph1
 432          in
 433          (* Unifying the types may have already instantiated n. Let's check *)
 434          try
 435            let (_, oldt,_) = CicUtil.lookup_subst n subst in
 436            let lifted_oldt = S.subst_meta l oldt in
 437              fo_unif_subst_ordered
 438                test_equality_only subst context metasenv t lifted_oldt ugraph2
 439          with
 440              CicUtil.Subst_not_found _ ->
 441                let (_, context, ty) = CicUtil.lookup_meta n metasenv in
 442                let subst = (n, (context, t'',ty)) :: subst in
 443                let metasenv =
 444                  List.filter (fun (m,_,_) -> not (n = m)) metasenv in
 445                subst, metasenv, ugraph2
 446          end
 447    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 448    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 449       if UriManager.eq uri1 uri2 then
 450        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 451         exp_named_subst1 exp_named_subst2 ugraph
 452       else
 453        raise (UnificationFailure (lazy
 454           (sprintf
 455             "Can't unify %s with %s due to different constants"
 456             (CicMetaSubst.ppterm subst t1)
 457             (CicMetaSubst.ppterm subst t2))))
 458    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 459        if UriManager.eq uri1 uri2 && i1 = i2 then
 460          fo_unif_subst_exp_named_subst
 461            test_equality_only
 462            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 463        else
 464          raise (UnificationFailure (lazy "4"))
 465            (* (sprintf
 466               "Can't unify %s with %s due to different inductive principles"
 467               (CicMetaSubst.ppterm subst t1)
 468               (CicMetaSubst.ppterm subst t2))) *)
 469    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 470        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 471        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 472          fo_unif_subst_exp_named_subst
 473            test_equality_only
 474            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 475        else
 476          raise (UnificationFailure (lazy "5"))
 477            (* (sprintf
 478               "Can't unify %s with %s due to different inductive constructors"
 479               (CicMetaSubst.ppterm subst t1)
 480               (CicMetaSubst.ppterm subst t2))) *)
 481    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 482    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
 483                               subst context metasenv te t2 ugraph
 484    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
 485                               subst context metasenv t1 te ugraph
 486    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 487        let subst',metasenv',ugraph1 =
 488          fo_unif_subst true subst context metasenv s1 s2 ugraph
 489        in
 490          fo_unif_subst test_equality_only
 491            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 492    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 493        let subst',metasenv',ugraph1 =
 494          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
 495        in
 496          fo_unif_subst test_equality_only
 497            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 498    | (C.LetIn (_,s1,t1), t2)
 499    | (t2, C.LetIn (_,s1,t1)) ->
 500        fo_unif_subst
 501         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
 502    | (C.Appl l1, C.Appl l2) ->
 503        (* andrea: this case should be probably rewritten in the
 504           spirit of deref *)
 505        (match l1,l2 with
 506           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
 507               (try
 508                  List.fold_left2
 509                    (fun (subst,metasenv,ugraph) t1 t2 ->
 510                       fo_unif_subst
 511                         test_equality_only subst context metasenv t1 t2 ugraph)
 512                    (subst,metasenv,ugraph) l1 l2
 513                with (Invalid_argument msg) ->
 514                  raise (UnificationFailure (lazy msg)))
 515           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
 516               (* we verify that none of the args is a Meta,
 517                 since beta expanding with respoect to a metavariable
 518                 makes no sense  *)
 519  (*
 520               (try
 521                  let (_,t,_) = CicUtil.lookup_subst i subst in
 522                  let lifted = S.subst_meta l t in
 523                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 524                    fo_unif_subst
 525                     test_equality_only
 526                      subst context metasenv reduced t2 ugraph
 527                with CicUtil.Subst_not_found _ -> *)
 528               let subst,metasenv,beta_expanded,ugraph1 =
 529                 beta_expand_many
 530                   test_equality_only metasenv subst context t2 args ugraph
 531               in
 532                 fo_unif_subst test_equality_only subst context metasenv
 533                   (C.Meta (i,l)) beta_expanded ugraph1
 534           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
 535               (* (try
 536                  let (_,t,_) = CicUtil.lookup_subst i subst in
 537                  let lifted = S.subst_meta l t in
 538                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 539                    fo_unif_subst
 540                      test_equality_only
 541                      subst context metasenv t1 reduced ugraph
 542                with CicUtil.Subst_not_found _ -> *)
 543                  let subst,metasenv,beta_expanded,ugraph1 =
 544                    beta_expand_many
 545                      test_equality_only
 546                      metasenv subst context t1 args ugraph
 547                  in
 548                    fo_unif_subst test_equality_only subst context metasenv
 549                      (C.Meta (i,l)) beta_expanded ugraph1
 550           | _,_ ->
 551               let lr1 = List.rev l1 in
 552               let lr2 = List.rev l2 in
 553               let rec
 554                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
 555                 match (l1,l2) with
 556                     [],_
 557                   | _,[] -> assert false
 558                   | ([h1],[h2]) ->
 559                       fo_unif_subst
 560                         test_equality_only subst context metasenv h1 h2 ugraph
 561                   | ([h],l)
 562                   | (l,[h]) ->
 563                       fo_unif_subst test_equality_only subst context metasenv
 564                         h (C.Appl (List.rev l)) ugraph
 565                   | ((h1::l1),(h2::l2)) ->
 566                       let subst', metasenv',ugraph1 =
 567                         fo_unif_subst
 568                           test_equality_only
 569                           subst context metasenv h1 h2 ugraph
 570                       in
 571                         fo_unif_l
 572                           test_equality_only subst' metasenv' (l1,l2) ugraph1
 573               in
 574               (try
 575                 fo_unif_l
 576                   test_equality_only subst metasenv (lr1, lr2)  ugraph
 577               with
 578               | UnificationFailure _
 579               | Uncertain _ as exn ->
 580                   (match l1, l2 with
 581                   | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
 582                      (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
 583                     CoercGraph.is_a_coercion c1 &&
 584                     CoercGraph.is_a_coercion c2 ->
 585                       let body1, attrs1, ugraph =
 586                         match CicEnvironment.get_obj ugraph uri1 with
 587                         | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
 588                         | _ -> assert false
 589                       in
 590                       let body2, attrs2, ugraph =
 591                         match CicEnvironment.get_obj ugraph uri2 with
 592                         | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
 593                         | _ -> assert false
 594                       in
 595                       let is_composite1 =
 596                         List.exists ((=) (`Class `Coercion)) attrs1 in
 597                       let is_composite2 =
 598                         List.exists ((=) (`Class `Coercion)) attrs2 in
 599                       (match is_composite1, is_composite2 with
 600                       | false, false -> raise exn
 601                       | true, false ->
 602                           let body1 = CicSubstitution.subst_vars ens1 body1 in
 603                           let appl = Cic.Appl (body1::tl1) in
 604                           let redappl = CicReduction.head_beta_reduce appl in
 605                           fo_unif_subst
 606                             test_equality_only subst context metasenv
 607                               redappl t2 ugraph
 608                       | false, true ->
 609                           let body2 = CicSubstitution.subst_vars ens2 body2 in
 610                           let appl = Cic.Appl (body2::tl2) in
 611                           let redappl = CicReduction.head_beta_reduce appl in
 612                           fo_unif_subst
 613                             test_equality_only subst context metasenv
 614                              t1 redappl ugraph
 615                       | true, true ->
 616                           let body1 = CicSubstitution.subst_vars ens1 body1 in
 617                           let appl1 = Cic.Appl (body1::tl1) in
 618                           let redappl1 = CicReduction.head_beta_reduce appl1 in
 619                           let body2 = CicSubstitution.subst_vars ens2 body2 in
 620                           let appl2 = Cic.Appl (body2::tl2) in
 621                           let redappl2 = CicReduction.head_beta_reduce appl2 in
 622                           fo_unif_subst
 623                             test_equality_only subst context metasenv
 624                              redappl1 redappl2 ugraph)
 625                   | _ -> raise exn)))
 626    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 627        let subst', metasenv',ugraph1 =
 628         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
 629           ugraph in
 630        let subst'',metasenv'',ugraph2 =
 631         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
 632           ugraph1 in
 633        (try
 634          List.fold_left2
 635           (fun (subst,metasenv,ugraph) t1 t2 ->
 636             fo_unif_subst
 637              test_equality_only subst context metasenv t1 t2 ugraph
 638           ) (subst'',metasenv'',ugraph2) pl1 pl2
 639         with
 640          Invalid_argument _ ->
 641           raise (UnificationFailure (lazy "6.1")))
 642            (* (sprintf
 643               "Error trying to unify %s with %s: the number of branches is not the same."
 644               (CicMetaSubst.ppterm subst t1)
 645               (CicMetaSubst.ppterm subst t2)))) *)
 646    | (C.Rel _, _) | (_,  C.Rel _) ->
 647        if t1 = t2 then
 648          subst, metasenv,ugraph
 649        else
 650         raise (UnificationFailure (lazy
 651            (sprintf
 652              "Can't unify %s with %s because they are not convertible"
 653              (CicMetaSubst.ppterm subst t1)
 654              (CicMetaSubst.ppterm subst t2))))
 655    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
 656        let subst,metasenv,beta_expanded,ugraph1 =
 657          beta_expand_many
 658            test_equality_only metasenv subst context t2 args ugraph
 659        in
 660          fo_unif_subst test_equality_only subst context metasenv
 661            (C.Meta (i,l)) beta_expanded ugraph1
 662    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
 663        let subst,metasenv,beta_expanded,ugraph1 =
 664          beta_expand_many
 665            test_equality_only metasenv subst context t1 args ugraph
 666        in
 667          fo_unif_subst test_equality_only subst context metasenv
 668            beta_expanded (C.Meta (i,l)) ugraph1
 669    | (C.Sort _ ,_) | (_, C.Sort _)
 670    | (C.Const _, _) | (_, C.Const _)
 671    | (C.MutInd  _, _) | (_, C.MutInd _)
 672    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
 673    | (C.Fix _, _) | (_, C.Fix _)
 674    | (C.CoFix _, _) | (_, C.CoFix _) ->
 675        if t1 = t2 then
 676          subst, metasenv, ugraph
 677        else
 678          let b,ugraph1 =
 679            R.are_convertible ~subst ~metasenv context t1 t2 ugraph
 680          in
 681            if b then
 682              subst, metasenv, ugraph1
 683            else
 684              raise
 685                 (UnificationFailure (lazy (sprintf
 686                   "Can't unify %s with %s because they are not convertible"
 687                   (CicMetaSubst.ppterm subst t1)
 688                   (CicMetaSubst.ppterm subst t2))))
 689    | (C.Prod _, t2) ->
 690        let t2' = R.whd ~subst context t2 in
 691        (match t2' with
 692             C.Prod _ ->
 693               fo_unif_subst test_equality_only
 694                 subst context metasenv t1 t2' ugraph
 695           | _ -> raise (UnificationFailure (lazy "8")))
 696    | (t1, C.Prod _) ->
 697        let t1' = R.whd ~subst context t1 in
 698        (match t1' with
 699             C.Prod _ ->
 700               fo_unif_subst test_equality_only
 701                 subst context metasenv t1' t2 ugraph
 702           | _ -> (* raise (UnificationFailure "9")) *)
 703              raise
 704                 (UnificationFailure (lazy (sprintf
 705                    "Can't unify %s with %s because they are not convertible"
 706                    (CicMetaSubst.ppterm subst t1)
 707                    (CicMetaSubst.ppterm subst t2)))))
 708    | (_,_) ->
 709        raise (UnificationFailure (lazy "10"))
 710          (* (sprintf
 711             "Can't unify %s with %s because they are not convertible"
 712             (CicMetaSubst.ppterm subst t1)
 713             (CicMetaSubst.ppterm subst t2))) *)
 714
 715 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 716  exp_named_subst1 exp_named_subst2 ugraph
 717 =
 718  try
 719   List.fold_left2
 720    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
 721      assert (uri1=uri2) ;
 722      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
 723    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
 724  with
 725   Invalid_argument _ ->
 726    let print_ens ens =
 727     String.concat " ; "
 728      (List.map
 729        (fun (uri,t) ->
 730          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
 731        ) ens)
 732    in
 733     raise (UnificationFailure (lazy (sprintf
 734      "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))))
 735
 736 (* A substitution is a (int * Cic.term) list that associates a               *)
 737 (* metavariable i with its body.                                             *)
 738 (* metasenv is of type Cic.metasenv                                          *)
 739 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 740 (* a new substitution which is already unwinded and ready to be applied and  *)
 741 (* a new metasenv in which some hypothesis in the contexts of the            *)
 742 (* metavariables may have been restricted.                                   *)
 743 let fo_unif metasenv context t1 t2 ugraph =
 744  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 745
 746 let enrich_msg msg subst context metasenv t1 t2 ugraph =
 747  lazy (
 748   if verbose then
 749    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"
 750     (CicMetaSubst.ppterm subst t1)
 751     (try
 752       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 753       CicPp.ppterm ty_t1
 754     with
 755     | UnificationFailure s
 756     | Uncertain s
 757     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 758     (CicMetaSubst.ppterm subst t2)
 759     (try
 760       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 761       CicPp.ppterm ty_t2
 762     with
 763     | UnificationFailure s
 764     | Uncertain s
 765     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 766     (CicMetaSubst.ppcontext subst context)
 767     (CicMetaSubst.ppmetasenv subst metasenv)
 768     (CicMetaSubst.ppsubst subst) (Lazy.force msg)
 769  else
 770    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 771     (CicMetaSubst.ppterm_in_context subst t1 context)
 772     (try
 773       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 774       CicMetaSubst.ppterm_in_context subst ty_t1 context
 775     with
 776     | UnificationFailure s
 777     | Uncertain s
 778     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 779     (CicMetaSubst.ppterm_in_context subst t2 context)
 780     (try
 781       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 782       CicMetaSubst.ppterm_in_context subst ty_t2 context
 783     with
 784     | UnificationFailure s
 785     | Uncertain s
 786     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 787     (CicMetaSubst.ppcontext subst context)
 788     (CicMetaSubst.ppmetasenv subst metasenv)
 789     (Lazy.force msg)
 790  )
 791
 792 let fo_unif_subst subst context metasenv t1 t2 ugraph =
 793   try
 794     fo_unif_subst false subst context metasenv t1 t2 ugraph
 795   with
 796   | AssertFailure msg ->
 797      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 798   | UnificationFailure msg ->
 799      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 800 ;;