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