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 (* NUOVA UNIFICAZIONE *)
  47 (* A substitution is a (int * Cic.term) list that associates a
  48    metavariable i with its body.
  49    A metaenv is a (int * Cic.term) list that associate a metavariable
  50    i with is type.
  51    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
  52    a new substitution which is _NOT_ unwinded. It must be unwinded before
  53    applying it. *)
  54
  55 let rec fo_unif_subst test_equality_only subst context metasenv t1 t2 =
  56  let module C = Cic in
  57  let module R = CicMetaSubst in
  58  let module S = CicSubstitution in
  59   match (t1, t2) with
  60      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
  61        let ok,subst,metasenv =
  62        try
  63         List.fold_left2
  64          (fun (b,subst,metasenv) t1 t2 ->
  65            if b then true,subst,metasenv else
  66             match t1,t2 with
  67                None,_
  68              | _,None -> true,subst,metasenv
  69              | Some t1', Some t2' ->
  70                 (* First possibility:  restriction    *)
  71                 (* Second possibility: unification    *)
  72                 (* Third possibility:  convertibility *)
  73                 if R.are_convertible subst context t1' t2' then
  74                  true,subst,metasenv
  75                 else
  76                  (try
  77                    let subst,metasenv =
  78                     fo_unif_subst
  79                      test_equality_only subst context metasenv t1' t2'
  80                    in
  81                     true,subst,metasenv
  82                  with
  83                   Not_found -> false,subst,metasenv)
  84          ) (true,subst,metasenv) ln lm
  85        with
  86         Invalid_argument _ ->
  87          raise (UnificationFailure (sprintf
  88            "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)))
  89        in
  90         if ok then
  91           subst,metasenv
  92         else
  93           raise (UnificationFailure (sprintf
  94             "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."
  95             (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
  96    | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
  97        fo_unif_subst test_equality_only subst context metasenv t2 t1
  98    | (C.Meta (n,l), t)
  99    | (t, C.Meta (n,l)) ->
 100        let swap =
 101         match t1,t2 with
 102            C.Meta (n,_), C.Meta (m,_) when n < m -> false
 103          | _, C.Meta _ -> false
 104          | _,_ -> true
 105        in
 106        let lower = fun x y -> if swap then y else x in
 107        let upper = fun x y -> if swap then x else y in
 108        let fo_unif_subst_ordered
 109         test_equality_only subst context metasenv m1 m2 =
 110           fo_unif_subst test_equality_only subst context metasenv
 111            (lower m1 m2) (upper m1 m2)
 112        in
 113        let subst'',metasenv' =
 114         try
 115          let oldt = (List.assoc n subst) in
 116          let lifted_oldt = S.lift_meta l oldt in
 117           fo_unif_subst_ordered
 118            test_equality_only subst context metasenv t lifted_oldt
 119         with Not_found ->
 120          let t',metasenv',subst' =
 121           try
 122            CicMetaSubst.delift n subst context metasenv l t
 123           with
 124              (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
 125            | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 126          in
 127           let t'' =
 128            match t' with
 129               C.Sort (C.Type u) when not test_equality_only ->
 130                 let u' = CicUniv.fresh () in
 131                 let s = C.Sort (C.Type u') in
 132                  ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
 133                 s
 134              | _ -> t'
 135           in
 136            (n, t'')::subst', metasenv'
 137        in
 138         let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
 139         (try
 140           let tyt =
 141             type_of_aux' metasenv' subst'' context t
 142           in
 143            fo_unif_subst
 144             test_equality_only
 145              subst'' context metasenv' tyt (S.lift_meta l meta_type)
 146         with AssertFailure _ ->
 147           (* TODO huge hack!!!!
 148            * we keep on unifying/refining in the hope that the problem will be
 149            * eventually solved. In the meantime we're breaking a big invariant:
 150            * the terms that we are unifying are no longer well typed in the
 151            * current context (in the worst case we could even diverge)
 152            *)
 153 (*
 154 prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
 155 prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 156 *)
 157           (subst'', metasenv'))
 158    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 159    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 160       if UriManager.eq uri1 uri2 then
 161        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 162         exp_named_subst1 exp_named_subst2
 163       else
 164        raise (UnificationFailure (sprintf
 165         "Can't unify %s with %s due to different constants"
 166         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 167    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 168       if UriManager.eq uri1 uri2 && i1 = i2 then
 169        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 170         exp_named_subst1 exp_named_subst2
 171       else
 172        raise (UnificationFailure (sprintf
 173         "Can't unify %s with %s due to different inductive principles"
 174         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 175    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 176      C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 177       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 178        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 179         exp_named_subst1 exp_named_subst2
 180       else
 181        raise (UnificationFailure (sprintf
 182         "Can't unify %s with %s due to different inductive constructors"
 183         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 184    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 185    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
 186                               subst context metasenv te t2
 187    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
 188                               subst context metasenv t1 te
 189    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 190         (* TASSI: this is the only case in which we want == *)
 191        let subst',metasenv' = fo_unif_subst true
 192                                subst context metasenv s1 s2 in
 193         fo_unif_subst test_equality_only
 194          subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 195    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 196         (* TASSI: ask someone a reason for not putting true here *)
 197        let subst',metasenv' = fo_unif_subst test_equality_only
 198                                subst context metasenv s1 s2 in
 199         fo_unif_subst test_equality_only
 200          subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 201    | (C.LetIn (_,s1,t1), t2)
 202    | (t2, C.LetIn (_,s1,t1)) ->
 203        fo_unif_subst
 204         test_equality_only subst context metasenv t2 (S.subst s1 t1)
 205    | (C.Appl l1, C.Appl l2) ->
 206        let lr1 = List.rev l1 in
 207        let lr2 = List.rev l2 in
 208        let rec fo_unif_l test_equality_only subst metasenv =
 209         function
 210            [],_
 211          | _,[] -> assert false
 212          | ([h1],[h2]) ->
 213              fo_unif_subst test_equality_only subst context metasenv h1 h2
 214          | ([h],l)
 215          | (l,[h]) ->
 216              fo_unif_subst
 217               test_equality_only subst context metasenv h (C.Appl (List.rev l))
 218          | ((h1::l1),(h2::l2)) ->
 219             let subst', metasenv' =
 220              fo_unif_subst test_equality_only subst context metasenv h1 h2
 221             in
 222              fo_unif_l test_equality_only subst' metasenv' (l1,l2)
 223        in
 224         fo_unif_l test_equality_only subst metasenv (lr1, lr2)
 225    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 226        let subst', metasenv' =
 227         fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
 228        let subst'',metasenv'' =
 229         fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in
 230        (try
 231          List.fold_left2
 232           (function (subst,metasenv) ->
 233             fo_unif_subst test_equality_only subst context metasenv
 234           ) (subst'',metasenv'') pl1 pl2
 235         with
 236          Invalid_argument _ ->
 237           raise (UnificationFailure (sprintf
 238             "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
 239    | (C.Rel _, _) | (_,  C.Rel _)
 240    | (C.Sort _ ,_) | (_, C.Sort _)
 241    | (C.Const _, _) | (_, C.Const _)
 242    | (C.MutInd  _, _) | (_, C.MutInd _)
 243    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
 244    | (C.Fix _, _) | (_, C.Fix _)
 245    | (C.CoFix _, _) | (_, C.CoFix _) ->
 246        if R.are_convertible subst context t1 t2 then
 247         subst, metasenv
 248        else
 249         raise (UnificationFailure (sprintf
 250           "Can't unify %s with %s because they are not convertible"
 251           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 252    | (_,_) ->
 253        if R.are_convertible subst context t1 t2 then
 254         subst, metasenv
 255        else
 256         raise (UnificationFailure (sprintf
 257           "Can't unify %s with %s because they are not convertible"
 258           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 259
 260 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 261  exp_named_subst1 exp_named_subst2
 262 =
 263  try
 264   List.fold_left2
 265    (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
 266      assert (uri1=uri2) ;
 267      fo_unif_subst test_equality_only subst context metasenv t1 t2
 268    ) (subst,metasenv) exp_named_subst1 exp_named_subst2
 269  with
 270   Invalid_argument _ ->
 271    let print_ens ens =
 272     String.concat " ; "
 273      (List.map
 274        (fun (uri,t) ->
 275          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
 276        ) ens)
 277    in
 278     raise (UnificationFailure (sprintf
 279      "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)))
 280
 281 (* A substitution is a (int * Cic.term) list that associates a               *)
 282 (* metavariable i with its body.                                             *)
 283 (* metasenv is of type Cic.metasenv                                          *)
 284 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 285 (* a new substitution which is already unwinded and ready to be applied and  *)
 286 (* a new metasenv in which some hypothesis in the contexts of the            *)
 287 (* metavariables may have been restricted.                                   *)
 288 let fo_unif metasenv context t1 t2 =
 289  fo_unif_subst false [] context metasenv t1 t2 ;;
 290
 291 let fo_unif_subst subst context metasenv t1 t2 =
 292   let enrich_msg msg =
 293     sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 294       (CicMetaSubst.ppterm subst t1)
 295       (try
 296         CicPp.ppterm (type_of_aux' metasenv subst context t1)
 297       with _ -> "MALFORMED")
 298       (CicMetaSubst.ppterm subst t2)
 299       (try
 300         CicPp.ppterm (type_of_aux' metasenv subst context t2)
 301       with _ -> "MALFORMED")
 302       (CicMetaSubst.ppcontext subst context)
 303       (CicMetaSubst.ppmetasenv metasenv subst) msg
 304   in
 305   try
 306     fo_unif_subst false subst context metasenv t1 t2
 307   with
 308   | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
 309   | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))
 310 ;;
 311