components/tactics/paramodulation/equality.ml

   1 (* cOpyright (C) 2005, 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 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
  27
  28 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
  29 type uncomparable = int -> int
  30 type equality =
  31     uncomparable *       (* trick to break structural equality *)
  32     int  *               (* weight *)
  33     proof *
  34     (Cic.term *          (* type *)
  35      Cic.term *          (* left side *)
  36      Cic.term *          (* right side *)
  37      Utils.comparison) * (* ordering *)
  38     Cic.metasenv  *      (* environment for metas *)
  39     int                  (* id *)
  40 and proof =
  41   | Exact of Cic.term
  42   | Step of Subst.substitution * (rule * int*(Utils.pos*int)* Cic.term)
  43             (* subst, (rule,eq1, eq2,predicate) *)
  44 and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list
  45 ;;
  46
  47 (* globals *)
  48 let maxid = ref 0;;
  49 let id_to_eq = Hashtbl.create 1024;;
  50
  51 let freshid () =
  52   incr maxid; !maxid
  53 ;;
  54
  55 let reset () =
  56   maxid := 0;
  57   Hashtbl.clear  id_to_eq
  58 ;;
  59
  60 let uncomparable = fun _ -> 0
  61
  62 let mk_equality (weight,p,(ty,l,r,o),m) =
  63   let id = freshid () in
  64   let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
  65   Hashtbl.add id_to_eq id eq;
  66   eq
  67 ;;
  68
  69 let mk_tmp_equality (weight,(ty,l,r,o),m) =
  70   let id = -1 in
  71   uncomparable,weight,Exact (Cic.Implicit None),(ty,l,r,o),m,id
  72 ;;
  73
  74
  75 let open_equality (_,weight,proof,(ty,l,r,o),m,id) =
  76   (weight,proof,(ty,l,r,o),m,id)
  77
  78 let string_of_equality ?env eq =
  79   match env with
  80   | None ->
  81       let w, _, (ty, left, right, o), _ , id = open_equality eq in
  82       Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
  83               id w (CicPp.ppterm ty)
  84               (CicPp.ppterm left)
  85               (Utils.string_of_comparison o) (CicPp.ppterm right)
  86   | Some (_, context, _) ->
  87       let names = Utils.names_of_context context in
  88       let w, _, (ty, left, right, o), _ , id = open_equality eq in
  89       Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
  90               id w (CicPp.pp ty names)
  91               (CicPp.pp left names) (Utils.string_of_comparison o)
  92               (CicPp.pp right names)
  93 ;;
  94
  95 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
  96   Pervasives.compare s1 s2
  97 ;;
  98
  99 let proof_of_id id =
 100   try
 101     let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
 102       p,l,r
 103   with
 104       Not_found -> assert false
 105
 106
 107 let string_of_proof ?(names=[]) p gp =
 108   let str_of_rule = function
 109     | SuperpositionRight -> "SupR"
 110     | SuperpositionLeft -> "SupL"
 111     | Demodulation -> "Demod"
 112   in
 113   let str_of_pos = function
 114     | Utils.Left -> "left"
 115     | Utils.Right -> "right"
 116   in
 117   let fst3 (x,_,_) = x in
 118   let rec aux margin name =
 119     let prefix = String.make margin ' ' ^ name ^ ": " in function
 120     | Exact t ->
 121         Printf.sprintf "%sExact (%s)\n"
 122           prefix (CicPp.pp t names)
 123     | Step (subst,(rule,eq1,(pos,eq2),pred)) ->
 124         Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
 125           prefix (str_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
 126           (CicPp.pp pred names)^
 127         aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^
 128         aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2))
 129   in
 130   aux 0 "" p ^
 131   String.concat "\n"
 132     (List.map
 133       (fun (pos,i,s,t) ->
 134         (Printf.sprintf
 135           "GOAL: %s %d %s %s\n"
 136             (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^
 137         aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
 138       gp)
 139 ;;
 140
 141 let rec depend eq id =
 142   let (_,p,(_,_,_,_),_,ideq) = open_equality eq in
 143   if id = ideq then true else
 144   match p with
 145       Exact _ -> false
 146     | Step (_,(_,id1,(_,id2),_)) ->
 147         let eq1 = Hashtbl.find id_to_eq id1 in
 148         let eq2 = Hashtbl.find id_to_eq id2 in
 149         depend eq1 id || depend eq2 id
 150 ;;
 151
 152 let ppsubst = Subst.ppsubst ~names:[];;
 153
 154 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
 155 let build_ens uri termlist =
 156   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 157   match obj with
 158   | Cic.Constant (_, _, _, uris, _) ->
 159       assert (List.length uris <= List.length termlist);
 160       let rec aux = function
 161         | [], tl -> [], tl
 162         | (uri::uris), (term::tl) ->
 163             let ens, args = aux (uris, tl) in
 164             (uri, term)::ens, args
 165         | _, _ -> assert false
 166       in
 167       aux (uris, termlist)
 168   | _ -> assert false
 169 ;;
 170
 171 let mk_sym uri ty t1 t2 p =
 172   let ens, args =  build_ens uri [ty;t1;t2;p] in
 173     Cic.Appl (Cic.Const(uri, ens) :: args)
 174 ;;
 175
 176 let mk_trans uri ty t1 t2 t3 p12 p23 =
 177   let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
 178     Cic.Appl (Cic.Const (uri, ens) :: args)
 179 ;;
 180
 181 let mk_eq_ind uri ty what pred p1 other p2 =
 182  Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
 183 ;;
 184
 185 let p_of_sym ens tl =
 186   let args = List.map snd ens @ tl in
 187   match args with
 188     | [_;_;_;p] -> p
 189     | _ -> assert false
 190 ;;
 191
 192 let open_trans ens tl =
 193   let args = List.map snd ens @ tl in
 194   match args with
 195     | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
 196     | _ -> assert false
 197 ;;
 198
 199 let open_eq_ind args =
 200   match args with
 201   | [ty;l;pred;pl;r;pleqr] -> ty,l,pred,pl,r,pleqr
 202   | _ -> assert false
 203 ;;
 204
 205 let open_pred pred =
 206   match pred with
 207   | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r]))
 208      when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
 209   | _ -> prerr_endline (CicPp.ppterm pred); assert false
 210 ;;
 211
 212 let is_not_fixed t =
 213    CicSubstitution.subst (Cic.Implicit None) t <>
 214    CicSubstitution.subst (Cic.Rel 1) t
 215 ;;
 216
 217
 218 let canonical t =
 219   let rec remove_refl t =
 220     match t with
 221     | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
 222           when LibraryObjects.is_trans_eq_URI uri_trans ->
 223           let ty,l,m,r,p1,p2 = open_trans ens tl in
 224             (match p1,p2 with
 225               | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 ->
 226                   remove_refl p2
 227               | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] ->
 228                   remove_refl p1
 229               | _ -> Cic.Appl (List.map remove_refl args))
 230     | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
 231     | _ -> t
 232   in
 233   let rec canonical t =
 234     match t with
 235       | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
 236           when LibraryObjects.is_sym_eq_URI uri_sym ->
 237           (match p_of_sym ens tl with
 238              | Cic.Appl ((Cic.Const(uri,ens))::tl)
 239                  when LibraryObjects.is_sym_eq_URI uri ->
 240                    canonical (p_of_sym ens tl)
 241              | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
 242                  when LibraryObjects.is_trans_eq_URI uri_trans ->
 243                  let ty,l,m,r,p1,p2 = open_trans ens tl in
 244                    mk_trans uri_trans ty r m l
 245                      (canonical (mk_sym uri_sym ty m r p2))
 246                      (canonical (mk_sym uri_sym ty l m p1))
 247              | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
 248                  when LibraryObjects.is_eq_ind_URI uri_ind ||
 249                       LibraryObjects.is_eq_ind_r_URI uri_ind ->
 250                  let ty, what, pred, p1, other, p2 =
 251                    match tl with
 252                    | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
 253                    | _ -> assert false
 254                  in
 255                  let pred,l,r =
 256                    match pred with
 257                    | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
 258                        when LibraryObjects.is_eq_URI uri ->
 259                          Cic.Lambda
 260                            (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
 261                    | _ ->
 262                        prerr_endline (CicPp.ppterm pred);
 263                        assert false
 264                  in
 265                  let l = CicSubstitution.subst what l in
 266                  let r = CicSubstitution.subst what r in
 267                  Cic.Appl
 268                    [he;ty;what;pred;
 269                     canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
 270              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
 271                  when LibraryObjects.is_eq_URI uri -> t
 272              | _ -> Cic.Appl (List.map canonical args))
 273       | Cic.Appl l -> Cic.Appl (List.map canonical l)
 274       | _ -> t
 275   in
 276   remove_refl (canonical t)
 277 ;;
 278
 279 let ty_of_lambda = function
 280   | Cic.Lambda (_,ty,_) -> ty
 281   | _ -> assert false
 282 ;;
 283
 284 let compose_contexts ctx1 ctx2 =
 285   ProofEngineReduction.replace_lifting
 286     ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[ctx2] ~where:ctx1
 287 ;;
 288
 289 let put_in_ctx ctx t =
 290   ProofEngineReduction.replace_lifting
 291     ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[t] ~where:ctx
 292 ;;
 293
 294 let mk_eq uri ty l r =
 295   Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r]
 296 ;;
 297
 298 let mk_refl uri ty t =
 299   Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t]
 300 ;;
 301
 302 let open_eq = function
 303   | Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] when LibraryObjects.is_eq_URI uri ->
 304       uri, ty, l ,r
 305   | _ -> assert false
 306 ;;
 307
 308 let contextualize uri ty left right t =
 309   (* aux [uri] [ty] [left] [right] [ctx] [t]
 310    *
 311    * the parameters validate this invariant
 312    *   t: eq(uri) ty left right
 313    * that is used only by the base case
 314    *
 315    * ctx is a term with an open (Rel 1). (Rel 1) is the empty context
 316    *)
 317     let rec aux uri ty left right ctx_d = function
 318       | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
 319         when LibraryObjects.is_eq_ind_URI uri_ind ||
 320              LibraryObjects.is_eq_ind_r_URI uri_ind ->
 321           let ty1,what,pred,p1,other,p2 = open_eq_ind tl in
 322           let ty2,eq,lp,rp = open_pred pred in
 323           let uri_trans = LibraryObjects.trans_eq_URI ~eq:uri in
 324           let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
 325           let is_not_fixed_lp = is_not_fixed lp in
 326           let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in
 327           (* extract the context and the fixed term from the predicate *)
 328           let m, ctx_c =
 329             let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
 330             (* they were under a lambda *)
 331             let m =  CicSubstitution.subst (Cic.Implicit None) m in
 332             let ctx_c = CicSubstitution.subst (Cic.Rel 1) ctx_c in
 333             m, ctx_c
 334           in
 335           (* create the compound context and put the terms under it *)
 336           let ctx_dc = compose_contexts ctx_d ctx_c in
 337           let dc_what = put_in_ctx ctx_dc what in
 338           let dc_other = put_in_ctx ctx_dc other in
 339           (* m is already in ctx_c so it is put in ctx_d only *)
 340           let d_m = put_in_ctx ctx_d m in
 341           (* we also need what in ctx_c *)
 342           let c_what = put_in_ctx ctx_c what in
 343           (* now put the proofs in the compound context *)
 344           let p1 = (* p1: dc_what = d_m *)
 345             if is_not_fixed_lp then
 346               aux uri ty1 c_what m ctx_d p1
 347             else
 348               mk_sym uri_sym ty d_m dc_what
 349                 (aux uri ty1 m c_what ctx_d p1)
 350           in
 351           let p2 = (* p2: dc_other = dc_what *)
 352             if avoid_eq_ind then
 353               mk_sym uri_sym ty dc_what dc_other
 354                 (aux uri ty1 what other ctx_dc p2)
 355             else
 356               aux uri ty1 other what ctx_dc p2
 357           in
 358           (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
 359              if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *)
 360           let a,b,c,paeqb,pbeqc =
 361             if is_not_fixed_lp then
 362               dc_other,dc_what,d_m,p2,p1
 363             else
 364               d_m,dc_what,dc_other,
 365                 (mk_sym uri_sym ty dc_what d_m p1),
 366                 (mk_sym uri_sym ty dc_other dc_what p2)
 367           in
 368           mk_trans uri_trans ty a b c paeqb pbeqc
 369     | t ->
 370         let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
 371         let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
 372         let pred =
 373           (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
 374           let ctx_d = CicSubstitution.lift_from 2 1 ctx_d in (* bleah *)
 375           let r = put_in_ctx ctx_d (CicSubstitution.lift 1 left) in
 376           let l = ctx_d in
 377           let lty = CicSubstitution.lift 1 ty in
 378           Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
 379         in
 380         let d_left = put_in_ctx ctx_d left in
 381         let d_right = put_in_ctx ctx_d right in
 382         let refl_eq = mk_refl uri ty d_left in
 383         mk_sym uri_sym ty d_right d_left
 384           (mk_eq_ind uri_ind ty left pred refl_eq right t)
 385   in
 386   let empty_context = Cic.Rel 1 in
 387   aux uri ty left right empty_context t
 388 ;;
 389
 390 let contextualize_rewrites t ty =
 391   let eq,ty,l,r = open_eq ty in
 392   contextualize eq ty l r t
 393 ;;
 394
 395 let build_proof_step subst p1 p2 pos l r pred =
 396   let p1 = Subst.apply_subst subst p1 in
 397   let p2 = Subst.apply_subst subst p2 in
 398   let l  = Subst.apply_subst subst l in
 399   let r  = Subst.apply_subst subst r in
 400   let pred = Subst.apply_subst subst pred in
 401   let ty,body =
 402     match pred with
 403       | Cic.Lambda (_,ty,body) -> ty,body
 404       | _ -> assert false
 405   in
 406   let what, other =
 407     if pos = Utils.Left then l,r else r,l
 408   in
 409     match pos with
 410       | Utils.Left ->
 411         mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
 412       | Utils.Right ->
 413         mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
 414 ;;
 415
 416 let build_proof_term proof =
 417   let rec aux = function
 418      | Exact term -> term
 419      | Step (subst,(_, id1, (pos,id2), pred)) ->
 420          let p,_,_ = proof_of_id id1 in
 421          let p1 = aux p in
 422          let p,l,r = proof_of_id id2 in
 423          let p2 = aux p in
 424            build_proof_step subst p1 p2 pos l r pred
 425   in
 426    aux proof
 427 ;;
 428
 429 let wfo goalproof proof =
 430   let rec aux acc id =
 431     let p,_,_ = proof_of_id id in
 432     match p with
 433     | Exact _ -> if (List.mem id acc) then acc else id :: acc
 434     | Step (_,(_,id1, (_,id2), _)) ->
 435         let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
 436         let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
 437         id :: acc
 438   in
 439   let acc =
 440     match proof with
 441       | Exact _ -> []
 442       | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2
 443   in
 444   List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof
 445 ;;
 446
 447 let string_of_id names id =
 448   try
 449     let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
 450     match p with
 451     | Exact t ->
 452         Printf.sprintf "%d = %s: %s = %s" id
 453           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
 454     | Step (_,(step,id1, (_,id2), _) ) ->
 455         Printf.sprintf "%6d: %s %6d %6d   %s = %s" id
 456           (if step = SuperpositionRight then "SupR" else "Demo")
 457           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
 458   with
 459       Not_found -> assert false
 460
 461 let pp_proof names goalproof proof =
 462   String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^
 463   "\ngoal is demodulated with " ^
 464     (String.concat " "
 465       ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
 466 ;;
 467
 468 let build_goal_proof l initial ty se =
 469   let se = List.map (fun i -> Cic.Meta (i,[])) se in
 470   let proof,se =
 471     let rec aux se current_proof = function
 472       | [] -> current_proof,se
 473       | (pos,id,subst,pred)::tl ->
 474            let p,l,r = proof_of_id id in
 475            let p = build_proof_term p in
 476            let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
 477            let proof = build_proof_step subst current_proof p pos l r pred in
 478            let proof,se = aux se proof tl in
 479            Subst.apply_subst subst proof,
 480            List.map (fun x -> Subst.apply_subst subst x) se
 481     in
 482     aux se initial l
 483   in
 484   canonical (contextualize_rewrites proof ty), se
 485 ;;
 486
 487 let refl_proof ty term =
 488   Cic.Appl
 489     [Cic.MutConstruct
 490        (LibraryObjects.eq_URI (), 0, 1, []);
 491        ty; term]
 492 ;;
 493
 494 let metas_of_proof p =
 495   let p = build_proof_term p in
 496   Utils.metas_of_term p
 497 ;;
 498
 499 let relocate newmeta menv =
 500   let subst, metasenv, newmeta =
 501     List.fold_right
 502       (fun (i, context, ty) (subst, menv, maxmeta) ->
 503         let irl = [] (*
 504          CicMkImplicit.identity_relocation_list_for_metavariable context *)
 505         in
 506         let newsubst = Subst.buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
 507         let newmeta = maxmeta, context, ty in
 508         newsubst, newmeta::menv, maxmeta+1)
 509       menv (Subst.empty_subst, [], newmeta+1)
 510   in
 511   let metasenv = Subst.apply_subst_metasenv subst metasenv in
 512   let subst = Subst.flatten_subst subst in
 513   subst, metasenv, newmeta
 514
 515
 516 let fix_metas newmeta eq =
 517   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
 518   (* debug
 519   let _ , eq =
 520     fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
 521   prerr_endline (string_of_equality eq); *)
 522   let subst, metasenv, newmeta = relocate newmeta menv in
 523   let ty = Subst.apply_subst subst ty in
 524   let left = Subst.apply_subst subst left in
 525   let right = Subst.apply_subst subst right in
 526   let fix_proof = function
 527     | Exact p -> Exact (Subst.apply_subst subst p)
 528     | Step (s,(r,id1,(pos,id2),pred)) ->
 529         Step (Subst.concat s subst,(r,id1,(pos,id2), pred))
 530   in
 531   let p = fix_proof p in
 532   let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in
 533   (* debug prerr_endline (string_of_equality eq); *)
 534   newmeta+1, eq
 535
 536 exception NotMetaConvertible;;
 537
 538 let meta_convertibility_aux table t1 t2 =
 539   let module C = Cic in
 540   let rec aux ((table_l, table_r) as table) t1 t2 =
 541     match t1, t2 with
 542     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
 543         let m1_binding, table_l =
 544           try List.assoc m1 table_l, table_l
 545           with Not_found -> m2, (m1, m2)::table_l
 546         and m2_binding, table_r =
 547           try List.assoc m2 table_r, table_r
 548           with Not_found -> m1, (m2, m1)::table_r
 549         in
 550         if (m1_binding <> m2) || (m2_binding <> m1) then
 551           raise NotMetaConvertible
 552         else (
 553           try
 554             List.fold_left2
 555               (fun res t1 t2 ->
 556                  match t1, t2 with
 557                  | None, Some _ | Some _, None -> raise NotMetaConvertible
 558                  | None, None -> res
 559                  | Some t1, Some t2 -> (aux res t1 t2))
 560               (table_l, table_r) tl1 tl2
 561           with Invalid_argument _ ->
 562             raise NotMetaConvertible
 563         )
 564     | C.Var (u1, ens1), C.Var (u2, ens2)
 565     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
 566         aux_ens table ens1 ens2
 567     | C.Cast (s1, t1), C.Cast (s2, t2)
 568     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
 569     | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
 570     | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
 571         let table = aux table s1 s2 in
 572         aux table t1 t2
 573     | C.Appl l1, C.Appl l2 -> (
 574         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 575         with Invalid_argument _ -> raise NotMetaConvertible
 576       )
 577     | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
 578         when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
 579     | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
 580         when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
 581         aux_ens table ens1 ens2
 582     | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
 583         when (UriManager.eq u1 u2) && i1 = i2 ->
 584         let table = aux table s1 s2 in
 585         let table = aux table t1 t2 in (
 586           try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 587           with Invalid_argument _ -> raise NotMetaConvertible
 588         )
 589     | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
 590         try
 591           List.fold_left2
 592             (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
 593                if i1 <> i2 then raise NotMetaConvertible
 594                else
 595                  let res = (aux res s1 s2) in aux res t1 t2)
 596             table il1 il2
 597         with Invalid_argument _ -> raise NotMetaConvertible
 598       )
 599     | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
 600         try
 601           List.fold_left2
 602             (fun res (n1, s1, t1) (n2, s2, t2) ->
 603                let res = aux res s1 s2 in aux res t1 t2)
 604             table il1 il2
 605         with Invalid_argument _ -> raise NotMetaConvertible
 606       )
 607     | t1, t2 when t1 = t2 -> table
 608     | _, _ -> raise NotMetaConvertible
 609
 610   and aux_ens table ens1 ens2 =
 611     let cmp (u1, t1) (u2, t2) =
 612       Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
 613     in
 614     let ens1 = List.sort cmp ens1
 615     and ens2 = List.sort cmp ens2 in
 616     try
 617       List.fold_left2
 618         (fun res (u1, t1) (u2, t2) ->
 619            if not (UriManager.eq u1 u2) then raise NotMetaConvertible
 620            else aux res t1 t2)
 621         table ens1 ens2
 622     with Invalid_argument _ -> raise NotMetaConvertible
 623   in
 624   aux table t1 t2
 625 ;;
 626
 627
 628 let meta_convertibility_eq eq1 eq2 =
 629   let _, _, (ty, left, right, _), _,_ = open_equality eq1 in
 630   let _, _, (ty', left', right', _), _,_ = open_equality eq2 in
 631   if ty <> ty' then
 632     false
 633   else if (left = left') && (right = right') then
 634     true
 635   else if (left = right') && (right = left') then
 636     true
 637   else
 638     try
 639       let table = meta_convertibility_aux ([], []) left left' in
 640       let _ = meta_convertibility_aux table right right' in
 641       true
 642     with NotMetaConvertible ->
 643       try
 644         let table = meta_convertibility_aux ([], []) left right' in
 645         let _ = meta_convertibility_aux table right left' in
 646         true
 647       with NotMetaConvertible ->
 648         false
 649 ;;
 650
 651
 652 let meta_convertibility t1 t2 =
 653   if t1 = t2 then
 654     true
 655   else
 656     try
 657       ignore(meta_convertibility_aux ([], []) t1 t2);
 658       true
 659     with NotMetaConvertible ->
 660       false
 661 ;;
 662
 663 exception TermIsNotAnEquality;;
 664
 665 let term_is_equality term =
 666   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
 667   match term with
 668   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
 669   | _ -> false
 670 ;;
 671
 672 let equality_of_term proof term =
 673   let eq_uri = LibraryObjects.eq_URI () in
 674   let iseq uri = UriManager.eq uri eq_uri in
 675   match term with
 676   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
 677       let o = !Utils.compare_terms t1 t2 in
 678       let stat = (ty,t1,t2,o) in
 679       let w = Utils.compute_equality_weight stat in
 680       let e = mk_equality (w, Exact proof, stat,[]) in
 681       e
 682   | _ ->
 683       raise TermIsNotAnEquality
 684 ;;
 685
 686 let is_weak_identity eq =
 687   let _,_,(_,left, right,_),_,_ = open_equality eq in
 688   left = right || meta_convertibility left right
 689 ;;
 690
 691 let is_identity (_, context, ugraph) eq =
 692   let _,_,(ty,left,right,_),menv,_ = open_equality eq in
 693   left = right ||
 694   (* (meta_convertibility left right)) *)
 695   fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
 696 ;;
 697
 698
 699 let term_of_equality equality =
 700   let _, _, (ty, left, right, _), menv, _= open_equality equality in
 701   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
 702   let argsno = List.length menv in
 703   let t =
 704     CicSubstitution.lift argsno
 705       (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
 706   in
 707   snd (
 708     List.fold_right
 709       (fun (i,_,ty) (n, t) ->
 710          let name = Cic.Name ("X" ^ (string_of_int n)) in
 711          let ty = CicSubstitution.lift (n-1) ty in
 712          let t =
 713            ProofEngineReduction.replace
 714              ~equality:eq ~what:[i]
 715              ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
 716          in
 717            (n-1, Cic.Prod (name, ty, t)))
 718       menv (argsno, t))
 719 ;;
 720