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