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