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