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 eta_expand test_equality_only metasenv subst context t arg =
  47  let module T = CicTypeChecker in
  48  let module S = CicSubstitution in
  49  let module C = Cic in
  50   let rec aux metasenv subst n context 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     T.type_of_aux' metasenv 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 eta_expand_many test_equality_only metasenv subst context t =
 169  List.fold_left
 170   (fun (subst,metasenv,t) arg ->
 171     eta_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        let subst'',metasenv' =
 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          let t',metasenv',subst' =
 249           try
 250            CicMetaSubst.delift n subst context metasenv l t
 251           with
 252              (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
 253            | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 254          in
 255           let t'' =
 256            match t' with
 257               C.Sort (C.Type u) when not test_equality_only ->
 258                 let u' = CicUniv.fresh () in
 259                 let s = C.Sort (C.Type u') in
 260                  ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
 261                 s
 262              | _ -> t'
 263           in
 264            (n, t'')::subst', metasenv'
 265        in
 266         let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
 267         (try
 268           let tyt =
 269             type_of_aux' metasenv' subst'' context t
 270           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    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 287    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 288       if UriManager.eq uri1 uri2 then
 289        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 290         exp_named_subst1 exp_named_subst2
 291       else
 292        raise (UnificationFailure (sprintf
 293         "Can't unify %s with %s due to different constants"
 294         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 295    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 296       if UriManager.eq uri1 uri2 && i1 = i2 then
 297        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 298         exp_named_subst1 exp_named_subst2
 299       else
 300        raise (UnificationFailure (sprintf
 301         "Can't unify %s with %s due to different inductive principles"
 302         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 303    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 304      C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 305       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 306        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 307         exp_named_subst1 exp_named_subst2
 308       else
 309        raise (UnificationFailure (sprintf
 310         "Can't unify %s with %s due to different inductive constructors"
 311         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 312    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 313    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
 314                               subst context metasenv te t2
 315    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
 316                               subst context metasenv t1 te
 317    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 318         (* TASSI: this is the only case in which we want == *)
 319        let subst',metasenv' = fo_unif_subst true
 320                                subst context metasenv s1 s2 in
 321         fo_unif_subst test_equality_only
 322          subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 323    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 324         (* TASSI: ask someone a reason for not putting true here *)
 325        let subst',metasenv' = fo_unif_subst test_equality_only
 326                                subst context metasenv s1 s2 in
 327         fo_unif_subst test_equality_only
 328          subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 329    | (C.LetIn (_,s1,t1), t2)
 330    | (t2, C.LetIn (_,s1,t1)) ->
 331        fo_unif_subst
 332         test_equality_only subst context metasenv t2 (S.subst s1 t1)
 333    | (C.Appl l1, C.Appl l2) ->
 334        let subst,metasenv,t1',t2' =
 335         match l1,l2 with
 336          (* In the first two cases when we reach the next begin ... end
 337             section useless work is done since, by construction, the list
 338             of arguments will be equal.
 339          *)
 340            C.Meta (i,l)::args, _ ->
 341             let subst,metasenv,t2' =
 342              eta_expand_many test_equality_only metasenv subst context t2 args
 343             in
 344              subst,metasenv,t1,t2'
 345          | _, C.Meta (i,l)::args ->
 346             let subst,metasenv,t1' =
 347              eta_expand_many test_equality_only metasenv subst context t1 args
 348             in
 349              subst,metasenv,t1',t2
 350          | _,_ -> subst,metasenv,t1,t2
 351        in
 352         begin
 353          match t1',t2' with
 354             C.Appl l1, C.Appl l2 ->
 355              let lr1 = List.rev l1 in
 356              let lr2 = List.rev l2 in
 357              let rec fo_unif_l test_equality_only subst metasenv =
 358               function
 359                  [],_
 360                | _,[] -> assert false
 361                | ([h1],[h2]) ->
 362                    fo_unif_subst test_equality_only subst context metasenv h1 h2
 363                | ([h],l)
 364                | (l,[h]) ->
 365                   fo_unif_subst
 366                    test_equality_only subst context metasenv h (C.Appl (List.rev l))
 367                | ((h1::l1),(h2::l2)) ->
 368                   let subst', metasenv' =
 369                    fo_unif_subst test_equality_only subst context metasenv h1 h2
 370                   in
 371                    fo_unif_l test_equality_only subst' metasenv' (l1,l2)
 372              in
 373               fo_unif_l test_equality_only subst metasenv (lr1, lr2)
 374           | _ -> assert false
 375         end
 376    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 377        let subst', metasenv' =
 378         fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
 379        let subst'',metasenv'' =
 380         fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in
 381        (try
 382          List.fold_left2
 383           (function (subst,metasenv) ->
 384             fo_unif_subst test_equality_only subst context metasenv
 385           ) (subst'',metasenv'') pl1 pl2
 386         with
 387          Invalid_argument _ ->
 388           raise (UnificationFailure (sprintf
 389             "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
 390    | (C.Rel _, _) | (_,  C.Rel _)
 391    | (C.Sort _ ,_) | (_, C.Sort _)
 392    | (C.Const _, _) | (_, C.Const _)
 393    | (C.MutInd  _, _) | (_, C.MutInd _)
 394    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
 395    | (C.Fix _, _) | (_, C.Fix _)
 396    | (C.CoFix _, _) | (_, C.CoFix _) ->
 397        if R.are_convertible subst context t1 t2 then
 398         subst, metasenv
 399        else
 400         raise (UnificationFailure (sprintf
 401           "Can't unify %s with %s because they are not convertible"
 402           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 403    | (_,_) ->
 404        if R.are_convertible subst context t1 t2 then
 405         subst, metasenv
 406        else
 407         raise (UnificationFailure (sprintf
 408           "Can't unify %s with %s because they are not convertible"
 409           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 410
 411 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 412  exp_named_subst1 exp_named_subst2
 413 =
 414  try
 415   List.fold_left2
 416    (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
 417      assert (uri1=uri2) ;
 418      fo_unif_subst test_equality_only subst context metasenv t1 t2
 419    ) (subst,metasenv) exp_named_subst1 exp_named_subst2
 420  with
 421   Invalid_argument _ ->
 422    let print_ens ens =
 423     String.concat " ; "
 424      (List.map
 425        (fun (uri,t) ->
 426          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
 427        ) ens)
 428    in
 429     raise (UnificationFailure (sprintf
 430      "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)))
 431
 432 (* A substitution is a (int * Cic.term) list that associates a               *)
 433 (* metavariable i with its body.                                             *)
 434 (* metasenv is of type Cic.metasenv                                          *)
 435 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 436 (* a new substitution which is already unwinded and ready to be applied and  *)
 437 (* a new metasenv in which some hypothesis in the contexts of the            *)
 438 (* metavariables may have been restricted.                                   *)
 439 let fo_unif metasenv context t1 t2 =
 440  fo_unif_subst false [] context metasenv t1 t2 ;;
 441
 442 let fo_unif_subst subst context metasenv t1 t2 =
 443   let enrich_msg msg =
 444     sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 445       (CicMetaSubst.ppterm subst t1)
 446       (try
 447         CicPp.ppterm (type_of_aux' metasenv subst context t1)
 448       with _ -> "MALFORMED")
 449       (CicMetaSubst.ppterm subst t2)
 450       (try
 451         CicPp.ppterm (type_of_aux' metasenv subst context t2)
 452       with _ -> "MALFORMED")
 453       (CicMetaSubst.ppcontext subst context)
 454       (CicMetaSubst.ppmetasenv metasenv subst) msg
 455   in
 456   try
 457     fo_unif_subst false subst context metasenv t1 t2
 458   with
 459   | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
 460   | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))
 461 ;;
 462