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