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