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