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