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