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 (* $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                 fo_unif_l
 575                   test_equality_only subst metasenv (lr1, lr2)  ugraph)
 576    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 577        let subst', metasenv',ugraph1 =
 578         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
 579           ugraph in
 580        let subst'',metasenv'',ugraph2 =
 581         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
 582           ugraph1 in
 583        (try
 584          List.fold_left2
 585           (fun (subst,metasenv,ugraph) t1 t2 ->
 586             fo_unif_subst
 587              test_equality_only subst context metasenv t1 t2 ugraph
 588           ) (subst'',metasenv'',ugraph2) pl1 pl2
 589         with
 590          Invalid_argument _ ->
 591           raise (UnificationFailure (lazy "6.1")))
 592            (* (sprintf
 593               "Error trying to unify %s with %s: the number of branches is not the same."
 594               (CicMetaSubst.ppterm subst t1)
 595               (CicMetaSubst.ppterm subst t2)))) *)
 596    | (C.Rel _, _) | (_,  C.Rel _) ->
 597        if t1 = t2 then
 598          subst, metasenv,ugraph
 599        else
 600         raise (UnificationFailure (lazy
 601            (sprintf
 602              "Can't unify %s with %s because they are not convertible"
 603              (CicMetaSubst.ppterm subst t1)
 604              (CicMetaSubst.ppterm subst t2))))
 605    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
 606        let subst,metasenv,beta_expanded,ugraph1 =
 607          beta_expand_many
 608            test_equality_only metasenv subst context t2 args ugraph
 609        in
 610          fo_unif_subst test_equality_only subst context metasenv
 611            (C.Meta (i,l)) beta_expanded ugraph1
 612    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
 613        let subst,metasenv,beta_expanded,ugraph1 =
 614          beta_expand_many
 615            test_equality_only metasenv subst context t1 args ugraph
 616        in
 617          fo_unif_subst test_equality_only subst context metasenv
 618            beta_expanded (C.Meta (i,l)) ugraph1
 619    | (C.Sort _ ,_) | (_, C.Sort _)
 620    | (C.Const _, _) | (_, C.Const _)
 621    | (C.MutInd  _, _) | (_, C.MutInd _)
 622    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
 623    | (C.Fix _, _) | (_, C.Fix _)
 624    | (C.CoFix _, _) | (_, C.CoFix _) ->
 625        if t1 = t2 then
 626          subst, metasenv, ugraph
 627        else
 628          let b,ugraph1 =
 629            R.are_convertible ~subst ~metasenv context t1 t2 ugraph
 630          in
 631            if b then
 632              subst, metasenv, ugraph1
 633            else
 634              raise
 635                 (UnificationFailure (lazy (sprintf
 636                   "Can't unify %s with %s because they are not convertible"
 637                   (CicMetaSubst.ppterm subst t1)
 638                   (CicMetaSubst.ppterm subst t2))))
 639    | (C.Prod _, t2) ->
 640        let t2' = R.whd ~subst context t2 in
 641        (match t2' with
 642             C.Prod _ ->
 643               fo_unif_subst test_equality_only
 644                 subst context metasenv t1 t2' ugraph
 645           | _ -> raise (UnificationFailure (lazy "8")))
 646    | (t1, C.Prod _) ->
 647        let t1' = R.whd ~subst context t1 in
 648        (match t1' with
 649             C.Prod _ ->
 650               fo_unif_subst test_equality_only
 651                 subst context metasenv t1' t2 ugraph
 652           | _ -> (* raise (UnificationFailure "9")) *)
 653              raise
 654                 (UnificationFailure (lazy (sprintf
 655                    "Can't unify %s with %s because they are not convertible"
 656                    (CicMetaSubst.ppterm subst t1)
 657                    (CicMetaSubst.ppterm subst t2)))))
 658    | (_,_) ->
 659        raise (UnificationFailure (lazy "10"))
 660          (* (sprintf
 661             "Can't unify %s with %s because they are not convertible"
 662             (CicMetaSubst.ppterm subst t1)
 663             (CicMetaSubst.ppterm subst t2))) *)
 664
 665 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 666  exp_named_subst1 exp_named_subst2 ugraph
 667 =
 668  try
 669   List.fold_left2
 670    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
 671      assert (uri1=uri2) ;
 672      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
 673    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
 674  with
 675   Invalid_argument _ ->
 676    let print_ens ens =
 677     String.concat " ; "
 678      (List.map
 679        (fun (uri,t) ->
 680          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
 681        ) ens)
 682    in
 683     raise (UnificationFailure (lazy (sprintf
 684      "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))))
 685
 686 (* A substitution is a (int * Cic.term) list that associates a               *)
 687 (* metavariable i with its body.                                             *)
 688 (* metasenv is of type Cic.metasenv                                          *)
 689 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 690 (* a new substitution which is already unwinded and ready to be applied and  *)
 691 (* a new metasenv in which some hypothesis in the contexts of the            *)
 692 (* metavariables may have been restricted.                                   *)
 693 let fo_unif metasenv context t1 t2 ugraph =
 694  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
 695
 696 let enrich_msg msg subst context metasenv t1 t2 ugraph =
 697  lazy (
 698   if verbose then
 699    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"
 700     (CicMetaSubst.ppterm subst t1)
 701     (try
 702       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 703       CicPp.ppterm ty_t1
 704     with
 705     | UnificationFailure s
 706     | Uncertain s
 707     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 708     (CicMetaSubst.ppterm subst t2)
 709     (try
 710       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 711       CicPp.ppterm ty_t2
 712     with
 713     | UnificationFailure s
 714     | Uncertain s
 715     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 716     (CicMetaSubst.ppcontext subst context)
 717     (CicMetaSubst.ppmetasenv subst metasenv)
 718     (CicMetaSubst.ppsubst subst) (Lazy.force msg)
 719  else
 720    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 721     (CicMetaSubst.ppterm_in_context subst t1 context)
 722     (try
 723       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
 724       CicMetaSubst.ppterm_in_context subst ty_t1 context
 725     with
 726     | UnificationFailure s
 727     | Uncertain s
 728     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
 729     (CicMetaSubst.ppterm_in_context subst t2 context)
 730     (try
 731       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
 732       CicMetaSubst.ppterm_in_context subst ty_t2 context
 733     with
 734     | UnificationFailure s
 735     | Uncertain s
 736     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
 737     (CicMetaSubst.ppcontext subst context)
 738     (CicMetaSubst.ppmetasenv subst metasenv)
 739     (Lazy.force msg)
 740  )
 741
 742 let fo_unif_subst subst context metasenv t1 t2 ugraph =
 743   try
 744     fo_unif_subst false subst context metasenv t1 t2 ugraph
 745   with
 746   | AssertFailure msg ->
 747      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 748   | UnificationFailure msg ->
 749      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
 750 ;;