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 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 subst context metasenv t1' t2'
  79                    in
  80                     true,subst,metasenv
  81                  with
  82                   Not_found -> false,subst,metasenv)
  83          ) (true,subst,metasenv) ln lm
  84        with
  85         Invalid_argument _ ->
  86          raise (UnificationFailure (sprintf
  87            "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)))
  88        in
  89         if ok then
  90           subst,metasenv
  91         else
  92           raise (UnificationFailure (sprintf
  93             "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."
  94             (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
  95    | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
  96        fo_unif_subst subst context metasenv t2 t1
  97    | (C.Meta (n,l), t)
  98    | (t, C.Meta (n,l)) ->
  99        let subst'',metasenv' =
 100         try
 101          let oldt = (List.assoc n subst) in
 102          let lifted_oldt = S.lift_meta l oldt in
 103           fo_unif_subst subst context metasenv lifted_oldt t
 104         with Not_found ->
 105          let t',metasenv',subst' =
 106           try
 107            CicMetaSubst.delift n subst context metasenv l t
 108           with
 109              (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
 110            | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 111          in
 112           (n, t')::subst', metasenv'
 113        in
 114         let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv' in
 115         (try
 116           let tyt =
 117             type_of_aux' metasenv' subst'' context t
 118           in
 119            fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt
 120         with AssertFailure _ ->
 121           (* TODO huge hack!!!!
 122            * we keep on unifying/refining in the hope that the problem will be
 123            * eventually solved. In the meantime we're breaking a big invariant:
 124            * the terms that we are unifying are no longer well typed in the
 125            * current context (in the worst case we could even diverge)
 126            *)
 127 (*
 128 prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
 129 prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 130 *)
 131           (subst'', metasenv'))
 132    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 133    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 134       if UriManager.eq uri1 uri2 then
 135        fo_unif_subst_exp_named_subst subst context metasenv
 136         exp_named_subst1 exp_named_subst2
 137       else
 138        raise (UnificationFailure (sprintf
 139         "Can't unify %s with %s due to different constants"
 140         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 141    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 142       if UriManager.eq uri1 uri2 && i1 = i2 then
 143        fo_unif_subst_exp_named_subst subst context metasenv
 144         exp_named_subst1 exp_named_subst2
 145       else
 146        raise (UnificationFailure (sprintf
 147         "Can't unify %s with %s due to different inductive principles"
 148         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 149    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 150      C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 151       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 152        fo_unif_subst_exp_named_subst subst context metasenv
 153         exp_named_subst1 exp_named_subst2
 154       else
 155        raise (UnificationFailure (sprintf
 156         "Can't unify %s with %s due to different inductive constructors"
 157         (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 158    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 159    | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
 160    | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
 161    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
 162        let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in
 163         fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 164    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 165        let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in
 166         fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
 167    | (C.LetIn (_,s1,t1), t2)
 168    | (t2, C.LetIn (_,s1,t1)) ->
 169        fo_unif_subst subst context metasenv t2 (S.subst s1 t1)
 170    | (C.Appl l1, C.Appl l2) ->
 171        let lr1 = List.rev l1 in
 172        let lr2 = List.rev l2 in
 173        let rec fo_unif_l subst metasenv =
 174         function
 175            [],_
 176          | _,[] -> assert false
 177          | ([h1],[h2]) ->
 178              fo_unif_subst subst context metasenv h1 h2
 179          | ([h],l)
 180          | (l,[h]) ->
 181              fo_unif_subst subst context metasenv h (C.Appl (List.rev l))
 182          | ((h1::l1),(h2::l2)) ->
 183             let subst', metasenv' =
 184              fo_unif_subst subst context metasenv h1 h2
 185             in
 186              fo_unif_l subst' metasenv' (l1,l2)
 187        in
 188         fo_unif_l subst metasenv (lr1, lr2)
 189    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 190        let subst', metasenv' =
 191         fo_unif_subst subst context metasenv outt1 outt2 in
 192        let subst'',metasenv'' =
 193         fo_unif_subst subst' context metasenv' t1' t2' in
 194        (try
 195          List.fold_left2
 196           (function (subst,metasenv) ->
 197             fo_unif_subst subst context metasenv
 198           ) (subst'',metasenv'') pl1 pl2
 199         with
 200          Invalid_argument _ ->
 201           raise (UnificationFailure (sprintf
 202             "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
 203    | (C.Rel _, _) | (_,  C.Rel _)
 204    | (C.Sort _ ,_) | (_, C.Sort _)
 205    | (C.Const _, _) | (_, C.Const _)
 206    | (C.MutInd  _, _) | (_, C.MutInd _)
 207    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
 208    | (C.Fix _, _) | (_, C.Fix _)
 209    | (C.CoFix _, _) | (_, C.CoFix _) ->
 210        if R.are_convertible subst context t1 t2 then
 211         subst, metasenv
 212        else
 213         raise (UnificationFailure (sprintf
 214           "Can't unify %s with %s because they are not convertible"
 215           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 216    | (_,_) ->
 217        if R.are_convertible subst context t1 t2 then
 218         subst, metasenv
 219        else
 220         raise (UnificationFailure (sprintf
 221           "Can't unify %s with %s because they are not convertible"
 222           (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
 223
 224 and fo_unif_subst_exp_named_subst subst context metasenv
 225  exp_named_subst1 exp_named_subst2
 226 =
 227  try
 228   List.fold_left2
 229    (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
 230      assert (uri1=uri2) ;
 231      fo_unif_subst subst context metasenv t1 t2
 232    ) (subst,metasenv) exp_named_subst1 exp_named_subst2
 233  with
 234   Invalid_argument _ ->
 235    let print_ens ens =
 236     String.concat " ; "
 237      (List.map
 238        (fun (uri,t) ->
 239          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
 240        ) ens)
 241    in
 242     raise (UnificationFailure (sprintf
 243      "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)))
 244
 245 (* A substitution is a (int * Cic.term) list that associates a               *)
 246 (* metavariable i with its body.                                             *)
 247 (* metasenv is of type Cic.metasenv                                          *)
 248 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
 249 (* a new substitution which is already unwinded and ready to be applied and  *)
 250 (* a new metasenv in which some hypothesis in the contexts of the            *)
 251 (* metavariables may have been restricted.                                   *)
 252 let fo_unif metasenv context t1 t2 = fo_unif_subst [] context metasenv t1 t2 ;;
 253
 254 let fo_unif_subst subst context metasenv t1 t2 =
 255   let enrich_msg msg =
 256     sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
 257       (CicMetaSubst.ppterm subst t1)
 258       (try
 259         CicPp.ppterm (type_of_aux' metasenv subst context t1)
 260       with _ -> "MALFORMED")
 261       (CicMetaSubst.ppterm subst t2)
 262       (try
 263         CicPp.ppterm (type_of_aux' metasenv subst context t2)
 264       with _ -> "MALFORMED")
 265       (CicMetaSubst.ppcontext subst context)
 266       (CicMetaSubst.ppmetasenv metasenv subst) msg
 267   in
 268   try
 269     fo_unif_subst subst context metasenv t1 t2
 270   with
 271   | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
 272   | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))
 273 ;;
 274