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