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 =
  35   try
  36     CicMetaSubst.type_of_aux' metasenv subst context term
  37   with
  38   | CicMetaSubst.MetaSubstFailure msg ->
  39     raise (AssertFailure
  40       ((sprintf
  41         "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"
  42         (CicMetaSubst.ppterm subst term)
  43         (CicMetaSubst.ppcontext subst context)
  44         (CicMetaSubst.ppmetasenv metasenv subst) msg)))
  45
  46 let rec beta_expand test_equality_only metasenv subst context t arg =
  47  let module S = CicSubstitution in
  48  let module C = Cic in
  49   let rec aux metasenv subst n context t' =
  50    try
  51     let subst,metasenv =
  52      fo_unif_subst test_equality_only subst context metasenv
  53       (CicSubstitution.lift n arg) t'
  54     in
  55      subst,metasenv,C.Rel (1 + n)
  56    with
  57       Uncertain _
  58     | UnificationFailure _ ->
  59        match t' with
  60         | C.Rel m  -> subst,metasenv, if m <= n then C.Rel m else C.Rel (m+1)
  61         | C.Var (uri,exp_named_subst) ->
  62            let subst,metasenv,exp_named_subst' =
  63             aux_exp_named_subst metasenv subst n context exp_named_subst
  64            in
  65             subst,metasenv,C.Var (uri,exp_named_subst')
  66         | C.Meta (i,l) as t->
  67            (try
  68              let (_, t') = CicMetaSubst.lookup_subst i subst in
  69               aux metasenv subst n context (CicSubstitution.lift_meta l t')
  70             with
  71              CicMetaSubst.SubstNotFound _ -> subst,metasenv,t)
  72         | C.Sort _
  73         | C.Implicit _ as t -> subst,metasenv,t
  74         | C.Cast (te,ty) ->
  75            let subst,metasenv,te' = aux metasenv subst n context te in
  76            let subst,metasenv,ty' = aux metasenv subst n context ty in
  77            subst,metasenv,C.Cast (te', ty')
  78         | C.Prod (nn,s,t) ->
  79            let subst,metasenv,s' = aux metasenv subst n context s in
  80            let subst,metasenv,t' =
  81             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
  82            in
  83             subst,metasenv,C.Prod (nn, s', t')
  84         | C.Lambda (nn,s,t) ->
  85            let subst,metasenv,s' = aux metasenv subst n context s in
  86            let subst,metasenv,t' =
  87             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
  88            in
  89             subst,metasenv,C.Lambda (nn, s', t')
  90         | C.LetIn (nn,s,t) ->
  91            let subst,metasenv,s' = aux metasenv subst n context s in
  92            let subst,metasenv,t' =
  93             aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
  94            in
  95             subst,metasenv,C.LetIn (nn, s', t')
  96         | C.Appl l ->
  97            let subst,metasenv,revl' =
  98             List.fold_left
  99              (fun (subst,metasenv,appl) t ->
 100                let subst,metasenv,t' = aux metasenv subst n context t in
 101                 subst,metasenv,t'::appl
 102              ) (subst,metasenv,[]) l
 103            in
 104             subst,metasenv,C.Appl (List.rev revl')
 105         | C.Const (uri,exp_named_subst) ->
 106            let subst,metasenv,exp_named_subst' =
 107             aux_exp_named_subst metasenv subst n context exp_named_subst
 108            in
 109             subst,metasenv,C.Const (uri,exp_named_subst')
 110         | C.MutInd (uri,i,exp_named_subst) ->
 111            let subst,metasenv,exp_named_subst' =
 112             aux_exp_named_subst metasenv subst n context exp_named_subst
 113            in
 114             subst,metasenv,C.MutInd (uri,i,exp_named_subst')
 115         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 116            let subst,metasenv,exp_named_subst' =
 117             aux_exp_named_subst metasenv subst n context exp_named_subst
 118            in
 119             subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst')
 120         | C.MutCase (sp,i,outt,t,pl) ->
 121            let subst,metasenv,outt' = aux metasenv subst n context outt in
 122            let subst,metasenv,t' = aux metasenv subst n context t in
 123            let subst,metasenv,revpl' =
 124             List.fold_left
 125              (fun (subst,metasenv,pl) t ->
 126                let subst,metasenv,t' = aux metasenv subst n context t in
 127                 subst,metasenv,t'::pl
 128              ) (subst,metasenv,[]) pl
 129            in
 130            subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl')
 131         | C.Fix (i,fl) ->
 132 (*CSC: not implemented
 133            let tylen = List.length fl in
 134             let substitutedfl =
 135              List.map
 136               (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 137                fl
 138             in
 139              C.Fix (i, substitutedfl)
 140 *) subst,metasenv,CicMetaSubst.lift subst 1 t'
 141         | C.CoFix (i,fl) ->
 142 (*CSC: not implemented
 143            let tylen = List.length fl in
 144             let substitutedfl =
 145              List.map
 146               (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 147                fl
 148             in
 149              C.CoFix (i, substitutedfl)
 150 *) subst,metasenv,CicMetaSubst.lift subst 1 t'
 151
 152   and aux_exp_named_subst metasenv subst n context ens =
 153    List.fold_right
 154     (fun (uri,t) (subst,metasenv,l) ->
 155       let subst,metasenv,t' = aux metasenv subst n context t in
 156        subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
 157   in
 158   let argty = type_of_aux' metasenv subst context arg in
 159   let fresh_name =
 160    FreshNamesGenerator.mk_fresh_name
 161     metasenv context (Cic.Name "Heta") ~typ:argty
 162   in
 163    let subst,metasenv,t' = aux metasenv subst 0 context t in
 164     subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
 165
 166 and beta_expand_many test_equality_only metasenv subst context t =
 167  List.fold_left
 168   (fun (subst,metasenv,t) arg ->
 169     beta_expand test_equality_only metasenv subst context t arg
 170   ) (subst,metasenv,t)
 171
 172 (* NUOVA UNIFICAZIONE *)
 173 (* A substitution is a (int * Cic.term) list that associates a
 174    metavariable i with its body.
 175    A metaenv is a (int * Cic.term) list that associate a metavariable
 176    i with is type.
 177    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
 178    a new substitution which is _NOT_ unwinded. It must be unwinded before
 179    applying it. *)
 180
 181 and fo_unif_subst test_equality_only subst context metasenv t1 t2 =
 182  let module C = Cic in
 183  let module R = CicMetaSubst in
 184  let module S = CicSubstitution in
 185   match (t1, t2) with
 186      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
 187        let ok,subst,metasenv =
 188        try
 189         List.fold_left2
 190          (fun (b,subst,metasenv) t1 t2 ->
 191            if b then true,subst,metasenv else
 192             match t1,t2 with
 193                None,_
 194              | _,None -> true,subst,metasenv
 195              | Some t1', Some t2' ->
 196                 (* First possibility:  restriction    *)
 197                 (* Second possibility: unification    *)
 198                 (* Third possibility:  convertibility *)
 199                 if R.are_convertible subst context t1' t2' then
 200                  true,subst,metasenv
 201                 else
 202                  (try
 203                    let subst,metasenv =
 204                     fo_unif_subst
 205                      test_equality_only subst context metasenv t1' t2'
 206                    in
 207                     true,subst,metasenv
 208                  with
 209                   Not_found -> false,subst,metasenv)
 210          ) (true,subst,metasenv) ln lm
 211        with
 212         Invalid_argument _ ->
 213          raise (UnificationFailure (sprintf
 214            "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)))
 215        in
 216         if ok then
 217           subst,metasenv
 218         else
 219           raise (UnificationFailure (sprintf
 220             "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."
 221             (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 222    | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
 223        fo_unif_subst test_equality_only subst context metasenv t2 t1
 224    | (C.Meta (n,l), t)
 225    | (t, C.Meta (n,l)) ->
 226        let swap =
 227         match t1,t2 with
 228            C.Meta (n,_), C.Meta (m,_) when n < m -> false
 229          | _, C.Meta _ -> false
 230          | _,_ -> true
 231        in
 232        let lower = fun x y -> if swap then y else x in
 233        let upper = fun x y -> if swap then x else y in
 234        let fo_unif_subst_ordered
 235         test_equality_only subst context metasenv m1 m2 =
 236           fo_unif_subst test_equality_only subst context metasenv
 237            (lower m1 m2) (upper m1 m2)
 238        in
 239         begin
 240         try
 241           let (_, oldt) = CicMetaSubst.lookup_subst n subst in
 242           let lifted_oldt = S.lift_meta l oldt in
 243           let ty_lifted_oldt =
 244             type_of_aux' metasenv subst context lifted_oldt
 245           in
 246           let tyt = type_of_aux' metasenv subst context t in
 247           let (subst, metasenv) =
 248             fo_unif_subst_ordered test_equality_only subst context metasenv
 249               tyt ty_lifted_oldt
 250           in
 251           fo_unif_subst_ordered
 252             test_equality_only subst context metasenv t lifted_oldt
 253         with CicMetaSubst.SubstNotFound _ ->
 254          (* First of all we unify the type of the meta with the type of the term *)
 255          let subst,metasenv =
 256           let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
 257           (try
 258             let tyt = type_of_aux' metasenv subst context t in
 259              fo_unif_subst
 260               test_equality_only
 261                subst context metasenv tyt (S.lift_meta l meta_type)
 262           with AssertFailure _ ->
 263             (* TODO huge hack!!!!
 264              * we keep on unifying/refining in the hope that the problem will be
 265              * eventually solved. In the meantime we're breaking a big invariant:
 266              * the terms that we are unifying are no longer well typed in the
 267              * current context (in the worst case we could even diverge)
 268              *)
 269 (*
 270 prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
 271 prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 272 *)
 273             (subst, metasenv))
 274          in
 275           let t',metasenv,subst =
 276            try
 277             CicMetaSubst.delift n subst context metasenv l t
 278            with
 279               (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
 280             | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 281           in
 282            let t'' =
 283             match t' with
 284                C.Sort (C.Type u) when not test_equality_only ->
 285                  let u' = CicUniv.fresh () in
 286                  let s = C.Sort (C.Type u') in
 287                   ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
 288                  s
 289               | _ -> t'
 290            in
 291             (* Unifying the types may have already instantiated n. Let's check *)
 292             try
 293              let (_, oldt) = CicMetaSubst.lookup_subst n subst in
 294              let lifted_oldt = S.lift_meta l oldt in
 295               fo_unif_subst_ordered
 296                test_equality_only subst context metasenv t lifted_oldt
 297             with
 298              CicMetaSubst.SubstNotFound _ ->
 299                let (_, context, _) = CicUtil.lookup_meta n metasenv in
 300                let subst = (n, (context, t'')) :: subst in
 301                let metasenv =
 302 (*                 CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *)
 303                 CicMetaSubst.apply_subst_metasenv subst metasenv
 304                in
 305                subst, metasenv
 306 (*               (n,t'')::subst, metasenv *)
 307         end
 308    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 309    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 310       if UriManager.eq uri1 uri2 then
 311        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 312         exp_named_subst1 exp_named_subst2
 313       else
 314        raise (UnificationFailure (sprintf
 315         "Can't unify %s with %s due to different constants"
 316         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 317    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 318       if UriManager.eq uri1 uri2 && i1 = i2 then
 319        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 320         exp_named_subst1 exp_named_subst2
 321       else
 322        raise (UnificationFailure (sprintf
 323         "Can't unify %s with %s due to different inductive principles"
 324         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 325    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 326      C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 327       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 328        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 329         exp_named_subst1 exp_named_subst2
 330       else
 331        raise (UnificationFailure (sprintf
 332         "Can't unify %s with %s due to different inductive constructors"
 333         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 334    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 335    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
 336                               subst context metasenv te t2
 337    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
 338                               subst context metasenv t1 te
 339    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 340         (* TASSI: this is the only case in which we want == *)
 341        let subst',metasenv' = fo_unif_subst true
 342                                subst context metasenv s1 s2 in
 343         fo_unif_subst test_equality_only
 344          subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 345    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 346         (* TASSI: ask someone a reason for not putting true here *)
 347        let subst',metasenv' = fo_unif_subst test_equality_only
 348                                subst context metasenv s1 s2 in
 349         fo_unif_subst test_equality_only
 350          subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 351    | (C.LetIn (_,s1,t1), t2)
 352    | (t2, C.LetIn (_,s1,t1)) ->
 353        fo_unif_subst
 354         test_equality_only subst context metasenv t2 (S.subst s1 t1)
 355    | (C.Appl l1, C.Appl l2) ->
 356        let subst,metasenv,t1',t2' =
 357         match l1,l2 with
 358            C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j ->
 359              subst,metasenv,t1,t2
 360          (* In the first two cases when we reach the next begin ... end
 361             section useless work is done since, by construction, the list
 362             of arguments will be equal.
 363          *)
 364          | C.Meta (i,l)::args, _ ->
 365             let subst,metasenv,t2' =
 366              beta_expand_many test_equality_only metasenv subst context t2 args
 367             in
 368              subst,metasenv,t1,t2'
 369          | _, C.Meta (i,l)::args ->
 370             let subst,metasenv,t1' =
 371              beta_expand_many test_equality_only metasenv subst context t1 args
 372             in
 373              subst,metasenv,t1',t2
 374          | _,_ ->
 375              subst,metasenv,t1,t2
 376        in
 377         begin
 378          match t1',t2' with
 379             C.Appl l1, C.Appl l2 ->
 380              let lr1 = List.rev l1 in
 381              let lr2 = List.rev l2 in
 382              let rec fo_unif_l test_equality_only subst metasenv =
 383               function
 384                  [],_
 385                | _,[] -> assert false
 386                | ([h1],[h2]) ->
 387                    fo_unif_subst test_equality_only subst context metasenv h1 h2
 388                | ([h],l)
 389                | (l,[h]) ->
 390                   fo_unif_subst
 391                    test_equality_only subst context metasenv h (C.Appl (List.rev l))
 392                | ((h1::l1),(h2::l2)) ->
 393                   let subst', metasenv' =
 394                    fo_unif_subst test_equality_only subst context metasenv h1 h2
 395                   in
 396                    fo_unif_l test_equality_only subst' metasenv' (l1,l2)
 397              in
 398               fo_unif_l test_equality_only subst metasenv (lr1, lr2)
 399           | _ -> assert false
 400         end
 401    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 402        let subst', metasenv' =
 403         fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
 404        let subst'',metasenv'' =
 405         fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in
 406        (try
 407          List.fold_left2
 408           (function (subst,metasenv) ->
 409             fo_unif_subst test_equality_only subst context metasenv
 410           ) (subst'',metasenv'') pl1 pl2
 411         with
 412          Invalid_argument _ ->
 413           raise (UnificationFailure (sprintf
 414             "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
 415    | (C.Rel _, _) | (_,  C.Rel _) ->
 416        if t1 = t2 then
 417          subst, metasenv
 418        else
 419         raise (UnificationFailure (sprintf
 420           "Can't unify %s with %s because they are not convertible"
 421           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 422    | (C.Sort _ ,_) | (_, C.Sort _)
 423    | (C.Const _, _) | (_, C.Const _)
 424    | (C.MutInd  _, _) | (_, C.MutInd _)
 425    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
 426    | (C.Fix _, _) | (_, C.Fix _)
 427    | (C.CoFix _, _) | (_, C.CoFix _) ->
 428        if t1 = t2 || R.are_convertible subst context t1 t2 then
 429         subst, metasenv
 430        else
 431         raise (UnificationFailure (sprintf
 432           "Can't unify %s with %s because they are not convertible"
 433           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 434    | (_,_) ->
 435        if R.are_convertible subst context t1 t2 then
 436         subst, metasenv
 437        else
 438         raise (UnificationFailure (sprintf
 439           "Can't unify %s with %s because they are not convertible"
 440           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 441
 442 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 443  exp_named_subst1 exp_named_subst2
 444 =
 445  try
 446   List.fold_left2
 447    (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
 448      assert (uri1=uri2) ;
 449      fo_unif_subst test_equality_only subst context metasenv t1 t2
 450    ) (subst,metasenv) exp_named_subst1 exp_named_subst2
 451  with
 452   Invalid_argument _ ->
 453    let print_ens ens =
 454     String.concat " ; "
 455      (List.map
 456        (fun (uri,t) ->
 457          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
 458        ) ens)
 459    in
 460     raise (UnificationFailure (sprintf
 461      "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)))
 462
 463 (* A substitution is a (int * Cic.term) list that associates a               *)
 464 (* metavariable i with its body.                                             *)
 465 (* metasenv is of type Cic.metasenv                                          *)
 466 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 467 (* a new substitution which is already unwinded and ready to be applied and  *)
 468 (* a new metasenv in which some hypothesis in the contexts of the            *)
 469 (* metavariables may have been restricted.                                   *)
 470 let fo_unif metasenv context t1 t2 =
 471  fo_unif_subst false [] context metasenv t1 t2 ;;
 472
 473 let fo_unif_subst subst context metasenv t1 t2 =
 474   let enrich_msg msg =
 475     sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 476       (CicMetaSubst.ppterm subst t1)
 477       (try
 478         CicPp.ppterm (type_of_aux' metasenv subst context t1)
 479       with _ -> "MALFORMED")
 480       (CicMetaSubst.ppterm subst t2)
 481       (try
 482         CicPp.ppterm (type_of_aux' metasenv subst context t2)
 483       with _ -> "MALFORMED")
 484       (CicMetaSubst.ppcontext subst context)
 485       (CicMetaSubst.ppmetasenv metasenv subst) msg
 486   in
 487   try
 488     fo_unif_subst false subst context metasenv t1 t2
 489   with
 490   | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
 491   | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))
 492 ;;
 493