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
  29 (******* CIC substitution ***************************************************)
  30
  31 type cic_substitution = Cic.substitution
  32 let cic_apply_subst = CicMetaSubst.apply_subst
  33 let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
  34 let cic_ppsubst = CicMetaSubst.ppsubst
  35 let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail
  36 let cic_flatten_subst subst =
  37     List.map
  38       (fun (i, (context, term, ty)) ->
  39          let context = (* cic_apply_subst_context subst*) context in
  40          let term = cic_apply_subst subst term in
  41          let ty = cic_apply_subst subst ty in
  42          (i, (context, term, ty))) subst
  43 let rec cic_lookup_subst meta subst =
  44   match meta with
  45   | Cic.Meta (i, _) -> (
  46       try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst
  47       in cic_lookup_subst t subst
  48       with Not_found -> meta
  49     )
  50   | _ -> meta
  51 ;;
  52
  53 let cic_merge_subst_if_possible s1 s2 =
  54   let already_in = Hashtbl.create 13 in
  55   let rec aux acc = function
  56     | ((i,_,x) as s)::tl ->
  57         (try
  58           let x' = Hashtbl.find already_in i in
  59           if x = x' then aux acc tl else None
  60         with
  61         | Not_found ->
  62             Hashtbl.add already_in i x;
  63             aux (s::acc) tl)
  64     | [] -> Some acc
  65   in
  66     aux [] (s1@s2)
  67 ;;
  68
  69 (******** NAIF substitution **************************************************)
  70 (*
  71  * naif version of apply subst; the local context of metas is ignored;
  72  * we assume the substituted term must be lifted according to the nesting
  73  * depth of the meta.
  74  * Alternatively, we could used implicit instead of metas
  75  *)
  76
  77 type naif_substitution = (int * Cic.term) list
  78
  79 let naif_apply_subst subst term =
  80  let rec aux k t =
  81    match t with
  82        Cic.Rel _ -> t
  83      | Cic.Var (uri,exp_named_subst) ->
  84          let exp_named_subst' =
  85            List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
  86          in
  87            Cic.Var (uri, exp_named_subst')
  88     | Cic.Meta (i, l) ->
  89         (try
  90           aux k (CicSubstitution.lift k (List.assoc i subst))
  91          with Not_found -> t)
  92     | Cic.Sort _
  93     | Cic.Implicit _ -> t
  94     | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
  95     | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
  96     | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
  97     | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
  98     | Cic.Appl [] -> assert false
  99     | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
 100     | Cic.Const (uri,exp_named_subst) ->
 101         let exp_named_subst' =
 102           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
 103         in
 104           if exp_named_subst' != exp_named_subst then
 105             Cic.Const (uri, exp_named_subst')
 106           else
 107             t (* TODO: provare a mantenere il piu' possibile sharing *)
 108     | Cic.MutInd (uri,typeno,exp_named_subst) ->
 109         let exp_named_subst' =
 110           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
 111         in
 112           Cic.MutInd (uri,typeno,exp_named_subst')
 113     | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 114         let exp_named_subst' =
 115           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
 116         in
 117           Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
 118     | Cic.MutCase (sp,i,outty,t,pl) ->
 119         let pl' = List.map (aux k) pl in
 120           Cic.MutCase (sp, i, aux k outty, aux k t, pl')
 121     | Cic.Fix (i, fl) ->
 122         let len = List.length fl in
 123         let fl' =
 124          List.map
 125            (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
 126         in
 127           Cic.Fix (i, fl')
 128     | Cic.CoFix (i, fl) ->
 129         let len = List.length fl in
 130         let fl' =
 131           List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
 132         in
 133           Cic.CoFix (i, fl')
 134 in
 135   aux 0 term
 136 ;;
 137
 138 (* naif version of apply_subst_metasenv: we do not apply the
 139 substitution to the context *)
 140
 141 let naif_apply_subst_metasenv subst metasenv =
 142   List.map
 143     (fun (n, context, ty) ->
 144       (n, context, naif_apply_subst subst ty))
 145     (List.filter
 146       (fun (i, _, _) -> not (List.mem_assoc i subst))
 147       metasenv)
 148
 149 let naif_ppsubst names subst =
 150   "{" ^ String.concat "; "
 151     (List.map
 152       (fun (idx, t) ->
 153          Printf.sprintf "%d:= %s" idx (CicPp.pp t names))
 154     subst) ^ "}"
 155 ;;
 156
 157 let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
 158
 159 let naif_flatten_subst subst =
 160   List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
 161 ;;
 162
 163 let rec naif_lookup_subst meta subst =
 164   match meta with
 165     | Cic.Meta (i, _) ->
 166         (try
 167           naif_lookup_subst (List.assoc i subst) subst
 168         with
 169             Not_found -> meta)
 170     | _ -> meta
 171 ;;
 172
 173 let naif_merge_subst_if_possible s1 s2 =
 174   let already_in = Hashtbl.create 13 in
 175   let rec aux acc = function
 176     | ((i,x) as s)::tl ->
 177         (try
 178           let x' = Hashtbl.find already_in i in
 179           if x = x' then aux acc tl else None
 180         with
 181         | Not_found ->
 182             Hashtbl.add already_in i x;
 183             aux (s::acc) tl)
 184     | [] -> Some acc
 185   in
 186     aux [] (s1@s2)
 187 ;;
 188
 189 (********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
 190
 191 type substitution = naif_substitution
 192 let apply_subst = naif_apply_subst
 193 let apply_subst_metasenv = naif_apply_subst_metasenv
 194 let ppsubst ~names l = naif_ppsubst (names:(Cic.name option)list) l
 195 let buildsubst = naif_buildsubst
 196 let flatten_subst = naif_flatten_subst
 197 let lookup_subst = naif_lookup_subst
 198
 199 (* filter out from metasenv the variables in substs *)
 200 let filter subst metasenv =
 201   List.filter
 202     (fun (m, _, _) ->
 203          try let _ = List.find (fun (i, _) -> m = i) subst in false
 204          with Not_found -> true)
 205     metasenv
 206 ;;
 207
 208 let is_in_subst i subst = List.mem_assoc i subst;;
 209
 210 let merge_subst_if_possible = naif_merge_subst_if_possible;;
 211
 212 let empty_subst = [];;
 213
 214 (********* EQUALITY **********************************************************)
 215
 216 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
 217 type uncomparable = int -> int
 218 type equality =
 219     uncomparable *       (* trick to break structural equality *)
 220     int  *               (* weight *)
 221     proof *
 222     (Cic.term *          (* type *)
 223      Cic.term *          (* left side *)
 224      Cic.term *          (* right side *)
 225      Utils.comparison) * (* ordering *)
 226     Cic.metasenv  *      (* environment for metas *)
 227     int                  (* id *)
 228 and proof = new_proof * old_proof
 229
 230 and new_proof =
 231   | Exact of Cic.term
 232   | Step of substitution * (rule * int*(Utils.pos*int)* Cic.term) (* eq1, eq2,predicate *)
 233 and old_proof =
 234   | NoProof (* term is the goal missing a proof *)
 235   | BasicProof of substitution * Cic.term
 236   | ProofBlock of
 237       substitution * UriManager.uri *
 238         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * old_proof
 239   | ProofGoalBlock of old_proof * old_proof
 240   | ProofSymBlock of Cic.term list * old_proof
 241   | SubProof of Cic.term * int * old_proof
 242 and goal_proof = (Utils.pos * int * substitution * Cic.term) list
 243 ;;
 244
 245 (* globals *)
 246 let maxid = ref 0;;
 247 let id_to_eq = Hashtbl.create 1024;;
 248
 249 let freshid () =
 250   incr maxid; !maxid
 251 ;;
 252
 253 let reset () =
 254   maxid := 0;
 255   Hashtbl.clear  id_to_eq
 256 ;;
 257
 258 let uncomparable = fun _ -> 0
 259
 260 let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
 261   let id = freshid () in
 262   let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in
 263   Hashtbl.add id_to_eq id eq;
 264   eq
 265 ;;
 266
 267 let mk_tmp_equality (weight,(ty,l,r,o),m) =
 268   let id = -1 in
 269   uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id
 270 ;;
 271
 272
 273 let open_equality (_,weight,proof,(ty,l,r,o),m,id) =
 274   (weight,proof,(ty,l,r,o),m,id)
 275
 276 let string_of_equality ?env eq =
 277   match env with
 278   | None ->
 279       let w, _, (ty, left, right, o), _ , id = open_equality eq in
 280       Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
 281               id w (CicPp.ppterm ty)
 282               (CicPp.ppterm left)
 283               (Utils.string_of_comparison o) (CicPp.ppterm right)
 284   | Some (_, context, _) ->
 285       let names = Utils.names_of_context context in
 286       let w, _, (ty, left, right, o), _ , id = open_equality eq in
 287       Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
 288               id w (CicPp.pp ty names)
 289               (CicPp.pp left names) (Utils.string_of_comparison o)
 290               (CicPp.pp right names)
 291 ;;
 292
 293 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
 294   Pervasives.compare s1 s2
 295 ;;
 296
 297 let rec string_of_proof_old ?(names=[]) = function
 298   | NoProof -> "NoProof "
 299   | BasicProof (s, t) -> "BasicProof(" ^
 300       ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")"
 301   | SubProof (t, i, p) ->
 302       Printf.sprintf "SubProof(%s, %s, %s)"
 303         (CicPp.pp t names) (string_of_int i) (string_of_proof_old p)
 304   | ProofSymBlock (_,p) ->
 305       Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p)
 306   | ProofBlock (subst, _, _, _ ,(_,eq),old) ->
 307       let _,(_,p),_,_,_ = open_equality eq in
 308       "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^
 309       string_of_proof_old p ^ ")"
 310   | ProofGoalBlock (p1, p2) ->
 311       Printf.sprintf "ProofGoalBlock(%s, %s)"
 312         (string_of_proof_old p1) (string_of_proof_old p2)
 313 ;;
 314
 315
 316 let proof_of_id id =
 317   try
 318     let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
 319       p,l,r
 320   with
 321       Not_found -> assert false
 322
 323
 324 let string_of_proof_new ?(names=[]) p gp =
 325   let str_of_rule = function
 326     | SuperpositionRight -> "SupR"
 327     | SuperpositionLeft -> "SupL"
 328     | Demodulation -> "Demod"
 329   in
 330   let str_of_pos = function
 331     | Utils.Left -> "left"
 332     | Utils.Right -> "right"
 333   in
 334   let fst3 (x,_,_) = x in
 335   let rec aux margin name =
 336     let prefix = String.make margin ' ' ^ name ^ ": " in function
 337     | Exact t ->
 338         Printf.sprintf "%sExact (%s)\n"
 339           prefix (CicPp.pp t names)
 340     | Step (subst,(rule,eq1,(pos,eq2),pred)) ->
 341         Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
 342           prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
 343           (CicPp.pp pred names)^
 344         aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^
 345         aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2))
 346   in
 347   aux 0 "" p ^
 348   String.concat "\n"
 349     (List.map
 350       (fun (pos,i,s,t) ->
 351         (Printf.sprintf
 352           "GOAL: %s %d %s %s\n"
 353             (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^
 354         aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
 355       gp)
 356 ;;
 357
 358 let rec depend eq id =
 359   let (_,(p,_),(_,_,_,_),_,ideq) = open_equality eq in
 360   if id = ideq then true else
 361   match p with
 362       Exact _ -> false
 363     | Step (_,(_,id1,(_,id2),_)) ->
 364         let eq1 = Hashtbl.find id_to_eq id1 in
 365         let eq2 = Hashtbl.find id_to_eq id2 in
 366         depend eq1 id || depend eq1 id2
 367 ;;
 368
 369 let ppsubst = ppsubst ~names:[]
 370
 371 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
 372 let build_ens uri termlist =
 373   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 374   match obj with
 375   | Cic.Constant (_, _, _, uris, _) ->
 376       assert (List.length uris <= List.length termlist);
 377       let rec aux = function
 378         | [], tl -> [], tl
 379         | (uri::uris), (term::tl) ->
 380             let ens, args = aux (uris, tl) in
 381             (uri, term)::ens, args
 382         | _, _ -> assert false
 383       in
 384       aux (uris, termlist)
 385   | _ -> assert false
 386 ;;
 387
 388 let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
 389   let rec do_build_proof proof =
 390     match proof with
 391     | NoProof ->
 392         Printf.fprintf stderr "WARNING: no proof!\n";
 393         noproof
 394     | BasicProof (s,term) -> apply_subst s term
 395     | ProofGoalBlock (proofbit, proof) ->
 396         print_endline "found ProofGoalBlock, going up...";
 397         do_build_goal_proof proofbit proof
 398     | ProofSymBlock (termlist, proof) ->
 399         let proof = do_build_proof proof in
 400         let ens, args = build_ens (Utils.sym_eq_URI ()) termlist in
 401         Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
 402     | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
 403         let t' = Cic.Lambda (name, ty, bo) in
 404         let _, (_,proof), (ty, what, other, _), menv',_ = open_equality eq in
 405         let proof' = do_build_proof proof in
 406         let eqproof = do_build_proof eqproof in
 407         let what, other =
 408           if pos = Utils.Left then what, other else other, what
 409         in
 410         apply_subst subst
 411           (Cic.Appl [Cic.Const (eq_URI, []); ty;
 412                      what; t'; eqproof; other; proof'])
 413     | SubProof (term, meta_index, proof) ->
 414         let proof = do_build_proof proof in
 415         let eq i = function
 416           | Cic.Meta (j, _) -> i = j
 417           | _ -> false
 418         in
 419         ProofEngineReduction.replace
 420           ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
 421
 422   and do_build_goal_proof proofbit proof =
 423     match proof with
 424     | ProofGoalBlock (pb, p) ->
 425         do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
 426     | _ -> do_build_proof (replace_proof proofbit proof)
 427
 428   and replace_proof newproof = function
 429     | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
 430         let eqproof' = replace_proof newproof eqproof in
 431         ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
 432     | ProofGoalBlock (pb, p) ->
 433         let pb' = replace_proof newproof pb in
 434         ProofGoalBlock (pb', p)
 435     | BasicProof _ -> newproof
 436     | SubProof (term, meta_index, p) ->
 437         SubProof (term, meta_index, replace_proof newproof p)
 438     | p -> p
 439   in
 440   do_build_proof proof
 441 ;;
 442
 443 let mk_sym uri ty t1 t2 p =
 444   let ens, args =  build_ens uri [ty;t1;t2;p] in
 445     Cic.Appl (Cic.Const(uri, ens) :: args)
 446 ;;
 447
 448 let mk_trans uri ty t1 t2 t3 p12 p23 =
 449   let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
 450     Cic.Appl (Cic.Const (uri, ens) :: args)
 451 ;;
 452
 453 let mk_eq_ind uri ty what pred p1 other p2 =
 454  Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
 455 ;;
 456
 457 let p_of_sym ens tl =
 458   let args = List.map snd ens @ tl in
 459   match args with
 460     | [_;_;_;p] -> p
 461     | _ -> assert false
 462 ;;
 463
 464 let open_trans ens tl =
 465   let args = List.map snd ens @ tl in
 466   match args with
 467     | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
 468     | _ -> assert false
 469 ;;
 470
 471 let canonical t =
 472   let rec remove_refl t =
 473     match t with
 474     | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
 475           when LibraryObjects.is_trans_eq_URI uri_trans ->
 476           let ty,l,m,r,p1,p2 = open_trans ens tl in
 477             (match p1,p2 with
 478               | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 ->
 479                   remove_refl p2
 480               | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] ->
 481                   remove_refl p1
 482               | _ -> Cic.Appl (List.map remove_refl args))
 483     | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
 484     | _ -> t
 485   in
 486   let rec canonical t =
 487     match t with
 488       | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
 489           when LibraryObjects.is_sym_eq_URI uri_sym ->
 490           (match p_of_sym ens tl with
 491              | Cic.Appl ((Cic.Const(uri,ens))::tl)
 492                  when LibraryObjects.is_sym_eq_URI uri ->
 493                    canonical (p_of_sym ens tl)
 494              | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
 495                  when LibraryObjects.is_trans_eq_URI uri_trans ->
 496                  let ty,l,m,r,p1,p2 = open_trans ens tl in
 497                    mk_trans uri_trans ty r m l
 498                      (canonical (mk_sym uri_sym ty m r p2))
 499                      (canonical (mk_sym uri_sym ty l m p1))
 500              | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
 501                  when LibraryObjects.is_eq_ind_URI uri_ind ||
 502                       LibraryObjects.is_eq_ind_r_URI uri_ind ->
 503                  let ty, what, pred, p1, other, p2 =
 504                    match tl with
 505                    | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
 506                    | _ -> assert false
 507                  in
 508                  let pred,l,r =
 509                    match pred with
 510                    | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
 511                        when LibraryObjects.is_eq_URI uri ->
 512                          Cic.Lambda
 513                            (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
 514                    | _ ->
 515                        prerr_endline (CicPp.ppterm pred);
 516                        assert false
 517                  in
 518                  let l = CicSubstitution.subst what l in
 519                  let r = CicSubstitution.subst what r in
 520                  Cic.Appl
 521                    [he;ty;what;pred;
 522                     canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
 523              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
 524                  when LibraryObjects.is_eq_URI uri -> t
 525              | _ -> Cic.Appl (List.map canonical args))
 526       | Cic.Appl l -> Cic.Appl (List.map canonical l)
 527       | _ -> t
 528   in
 529   remove_refl (canonical t)
 530 ;;
 531
 532 let build_proof_step subst p1 p2 pos l r pred =
 533   let p1 = apply_subst subst p1 in
 534   let p2 = apply_subst subst p2 in
 535   let l = apply_subst subst l in
 536   let r = apply_subst subst r in
 537   let pred = apply_subst subst pred in
 538   let ty,body = (* Cic.Implicit None *)
 539     match pred with
 540       | Cic.Lambda (_,ty,body) -> ty,body
 541       | _ -> assert false
 542   in
 543   let what, other = (* Cic.Implicit None, Cic.Implicit None *)
 544     if pos = Utils.Left then l,r else r,l
 545   in
 546   let is_not_fixed t =
 547    CicSubstitution.subst (Cic.Implicit None) t <>
 548    CicSubstitution.subst (Cic.Rel 1) t
 549   in
 550     match body,pos with
 551 (*
 552       |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
 553          let third = CicSubstitution.subst (Cic.Implicit None) third in
 554          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
 555          let uri_sym = LibraryObjects.sym_eq_URI ~eq in
 556            mk_trans uri_trans ty other what third
 557             (mk_sym uri_sym ty what other p2) p1
 558       |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right ->
 559          let third = CicSubstitution.subst (Cic.Implicit None) third in
 560          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
 561            mk_trans uri_trans ty other what third p2 p1
 562       |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left ->
 563          let third = CicSubstitution.subst (Cic.Implicit None) third in
 564          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
 565            mk_trans uri_trans ty third what other p1 p2
 566       |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right ->
 567          let third = CicSubstitution.subst (Cic.Implicit None) third in
 568          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
 569          let uri_sym = LibraryObjects.sym_eq_URI ~eq in
 570            mk_trans uri_trans ty third what other p1
 571             (mk_sym uri_sym ty other what p2)
 572       | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs
 573         ->
 574           let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
 575           let uri_trans = LibraryObjects.trans_eq_URI ~eq in
 576           let pred_of t = CicSubstitution.subst t lhs in
 577           let pred_of_what = pred_of what in
 578           let pred_of_other = pred_of other in
 579           (*           p2 : what = other
 580            * ====================================
 581            *  inject p2:  P(what) = P(other)
 582            *)
 583           let rec inject ty lhs what other p2 =
 584            match p2 with
 585            | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
 586                when LibraryObjects.is_trans_eq_URI uri_trans ->
 587                let ty,l,m,r,plm,pmr = open_trans ens tl in
 588                mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
 589                  (inject ty lhs m r pmr) (inject ty lhs l m plm)
 590            | _ ->
 591            let liftedty = CicSubstitution.lift 1 ty in
 592            let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
 593            let refl_eq_part =
 594             Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
 595            in
 596             (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
 597              (Cic.Lambda (Cic.Name "foo",ty,
 598                (Cic.Appl
 599                [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
 600                 refl_eq_part what p2)
 601           in
 602            mk_trans uri_trans ty pred_of_other pred_of_what rhs
 603              (inject ty lhs what other p2) p1
 604       | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
 605         ->
 606           let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
 607           let uri_trans = LibraryObjects.trans_eq_URI ~eq in
 608           let pred_of t = CicSubstitution.subst t lhs in
 609           let pred_of_what = pred_of what in
 610           let pred_of_other = pred_of other in
 611           (*           p2 : what = other
 612            * ====================================
 613            *  inject p2:  P(what) = P(other)
 614            *)
 615           let rec inject ty lhs what other p2 =
 616            match p2 with
 617            | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
 618                when LibraryObjects.is_trans_eq_URI uri_trans ->
 619                let ty,l,m,r,plm,pmr = open_trans ens tl in
 620                mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
 621                  (inject ty lhs m l plm)
 622                  (inject ty lhs r m pmr)
 623            | _ ->
 624              let liftedty = CicSubstitution.lift 1 ty in
 625              let lifted_pred_of_other =
 626                CicSubstitution.lift 1 (pred_of other) in
 627              let refl_eq_part =
 628               Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
 629              in
 630               mk_eq_ind (Utils.eq_ind_URI ()) ty other
 631                (Cic.Lambda (Cic.Name "foo",ty,
 632                  (Cic.Appl
 633                  [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
 634                   refl_eq_part what p2
 635           in
 636            mk_trans uri_trans ty pred_of_other pred_of_what rhs
 637             (inject ty lhs what other p2) p1
 638       | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
 639         ->
 640           let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
 641           let uri_trans = LibraryObjects.trans_eq_URI ~eq in
 642           let pred_of t = CicSubstitution.subst t rhs in
 643           let pred_of_what = pred_of what in
 644           let pred_of_other = pred_of other in
 645           (*           p2 : what = other
 646            * ====================================
 647            *  inject p2:  P(what) = P(other)
 648            *)
 649           let rec inject ty lhs what other p2 =
 650            match p2 with
 651            | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
 652                when LibraryObjects.is_trans_eq_URI uri_trans ->
 653                let ty,l,m,r,plm,pmr = open_trans ens tl in
 654                  mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
 655                    (inject ty lhs m r pmr)
 656                    (inject ty lhs l m plm)
 657            | _ ->
 658            let liftedty = CicSubstitution.lift 1 ty in
 659            let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
 660            let refl_eq_part =
 661             Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
 662            in
 663             (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
 664              (Cic.Lambda (Cic.Name "foo",ty,
 665                (Cic.Appl
 666                [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
 667                 refl_eq_part what p2)
 668           in
 669            mk_trans uri_trans ty lhs pred_of_what pred_of_other
 670              p1 (inject ty rhs other what p2)
 671       | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
 672         ->
 673           let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
 674           let uri_trans = LibraryObjects.trans_eq_URI ~eq in
 675           let pred_of t = CicSubstitution.subst t rhs in
 676           let pred_of_what = pred_of what in
 677           let pred_of_other = pred_of other in
 678           (*           p2 : what = other
 679            * ====================================
 680            *  inject p2:  P(what) = P(other)
 681            *)
 682           let rec inject ty lhs what other p2 =
 683            match p2 with
 684            | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
 685                when LibraryObjects.is_trans_eq_URI uri_trans ->
 686                let ty,l,m,r,plm,pmr = open_trans ens tl in
 687                  (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
 688                    (inject ty lhs m l plm)
 689                    (inject ty lhs r m pmr))
 690            | _ ->
 691            let liftedty = CicSubstitution.lift 1 ty in
 692            let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
 693            let refl_eq_part =
 694             Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
 695            in
 696             mk_eq_ind (Utils.eq_ind_URI ()) ty other
 697              (Cic.Lambda (Cic.Name "foo",ty,
 698                (Cic.Appl
 699                [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
 700                 refl_eq_part what p2
 701           in
 702            mk_trans uri_trans ty lhs pred_of_what pred_of_other
 703              p1 (inject ty rhs other what p2)
 704 *)
 705       | _, Utils.Left ->
 706         mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
 707       | _, Utils.Right ->
 708         mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
 709 ;;
 710
 711 let build_proof_term_new proof =
 712   let rec aux = function
 713      | Exact term -> term
 714      | Step (subst,(_, id1, (pos,id2), pred)) ->
 715          let p,_,_ = proof_of_id id1 in
 716          let p1 = aux p in
 717          let p,l,r = proof_of_id id2 in
 718          let p2 = aux p in
 719            build_proof_step subst p1 p2 pos l r pred
 720   in
 721    aux proof
 722 ;;
 723
 724 let wfo goalproof proof =
 725   let rec aux acc id =
 726     let p,_,_ = proof_of_id id in
 727     match p with
 728     | Exact _ -> if (List.mem id acc) then acc else id :: acc
 729     | Step (_,(_,id1, (_,id2), _)) ->
 730         let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
 731         let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
 732         id :: acc
 733   in
 734   let acc =
 735     match proof with
 736       | Exact _ -> []
 737       | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2
 738   in
 739   List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof
 740 ;;
 741
 742 let string_of_id names id =
 743   try
 744     let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
 745     match p with
 746     | Exact t ->
 747         Printf.sprintf "%d = %s: %s = %s" id
 748           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
 749     | Step (_,(step,id1, (_,id2), _) ) ->
 750         Printf.sprintf "%6d: %s %6d %6d   %s = %s" id
 751           (if step = SuperpositionRight then "SupR" else "Demo")
 752           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
 753   with
 754       Not_found -> assert false
 755
 756 let pp_proof names goalproof proof =
 757   String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^
 758   "\ngoal is demodulated with " ^
 759     (String.concat " "
 760       ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
 761 ;;
 762
 763 let build_goal_proof l initial =
 764   let proof =
 765    List.fold_left
 766    (fun  current_proof (pos,id,subst,pred) ->
 767       let p,l,r = proof_of_id id in
 768       let p = build_proof_term_new p in
 769       let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
 770         build_proof_step subst current_proof p pos l r pred)
 771    initial l
 772   in
 773   canonical proof
 774 ;;
 775
 776 let refl_proof ty term =
 777   Cic.Appl
 778     [Cic.MutConstruct
 779        (LibraryObjects.eq_URI (), 0, 1, []);
 780        ty; term]
 781 ;;
 782
 783 let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
 784
 785 let relocate newmeta menv =
 786   let subst, metasenv, newmeta =
 787     List.fold_right
 788       (fun (i, context, ty) (subst, menv, maxmeta) ->
 789         let irl = [] (*
 790          CicMkImplicit.identity_relocation_list_for_metavariable context *)
 791         in
 792         let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
 793         let newmeta = maxmeta, context, ty in
 794         newsubst, newmeta::menv, maxmeta+1)
 795       menv ([], [], newmeta+1)
 796   in
 797   let metasenv = apply_subst_metasenv subst metasenv in
 798   let subst = flatten_subst subst in
 799   subst, metasenv, newmeta
 800
 801
 802 let fix_metas newmeta eq =
 803   let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
 804   (* debug
 805   let _ , eq =
 806     fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
 807   prerr_endline (string_of_equality eq); *)
 808   let subst, metasenv, newmeta = relocate newmeta menv in
 809   let ty = apply_subst subst ty in
 810   let left = apply_subst subst left in
 811   let right = apply_subst subst right in
 812   let fix_proof = function
 813     | NoProof -> NoProof
 814     | BasicProof (subst',term) -> BasicProof (subst@subst',term)
 815     | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
 816         (*
 817         let newsubst =
 818           List.map
 819             (fun (i, (context, term, ty)) ->
 820                let context = apply_subst_context subst context in
 821                let term = apply_subst subst term in
 822                let ty = apply_subst subst ty in
 823                  (i, (context, term, ty))) subst' in *)
 824           ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
 825     | p -> assert false
 826   in
 827   let fix_new_proof = function
 828     | Exact p -> Exact (apply_subst subst p)
 829     | Step (s,(r,id1,(pos,id2),pred)) ->
 830         Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
 831   in
 832   let new_p = fix_new_proof p1 in
 833   let old_p = fix_proof p2 in
 834   let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
 835   (* debug prerr_endline (string_of_equality eq); *)
 836   newmeta+1, eq
 837
 838 exception NotMetaConvertible;;
 839
 840 let meta_convertibility_aux table t1 t2 =
 841   let module C = Cic in
 842   let rec aux ((table_l, table_r) as table) t1 t2 =
 843     match t1, t2 with
 844     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
 845         let m1_binding, table_l =
 846           try List.assoc m1 table_l, table_l
 847           with Not_found -> m2, (m1, m2)::table_l
 848         and m2_binding, table_r =
 849           try List.assoc m2 table_r, table_r
 850           with Not_found -> m1, (m2, m1)::table_r
 851         in
 852         if (m1_binding <> m2) || (m2_binding <> m1) then
 853           raise NotMetaConvertible
 854         else (
 855           try
 856             List.fold_left2
 857               (fun res t1 t2 ->
 858                  match t1, t2 with
 859                  | None, Some _ | Some _, None -> raise NotMetaConvertible
 860                  | None, None -> res
 861                  | Some t1, Some t2 -> (aux res t1 t2))
 862               (table_l, table_r) tl1 tl2
 863           with Invalid_argument _ ->
 864             raise NotMetaConvertible
 865         )
 866     | C.Var (u1, ens1), C.Var (u2, ens2)
 867     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
 868         aux_ens table ens1 ens2
 869     | C.Cast (s1, t1), C.Cast (s2, t2)
 870     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
 871     | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
 872     | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
 873         let table = aux table s1 s2 in
 874         aux table t1 t2
 875     | C.Appl l1, C.Appl l2 -> (
 876         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 877         with Invalid_argument _ -> raise NotMetaConvertible
 878       )
 879     | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
 880         when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
 881     | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
 882         when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
 883         aux_ens table ens1 ens2
 884     | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
 885         when (UriManager.eq u1 u2) && i1 = i2 ->
 886         let table = aux table s1 s2 in
 887         let table = aux table t1 t2 in (
 888           try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 889           with Invalid_argument _ -> raise NotMetaConvertible
 890         )
 891     | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
 892         try
 893           List.fold_left2
 894             (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
 895                if i1 <> i2 then raise NotMetaConvertible
 896                else
 897                  let res = (aux res s1 s2) in aux res t1 t2)
 898             table il1 il2
 899         with Invalid_argument _ -> raise NotMetaConvertible
 900       )
 901     | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
 902         try
 903           List.fold_left2
 904             (fun res (n1, s1, t1) (n2, s2, t2) ->
 905                let res = aux res s1 s2 in aux res t1 t2)
 906             table il1 il2
 907         with Invalid_argument _ -> raise NotMetaConvertible
 908       )
 909     | t1, t2 when t1 = t2 -> table
 910     | _, _ -> raise NotMetaConvertible
 911
 912   and aux_ens table ens1 ens2 =
 913     let cmp (u1, t1) (u2, t2) =
 914       Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
 915     in
 916     let ens1 = List.sort cmp ens1
 917     and ens2 = List.sort cmp ens2 in
 918     try
 919       List.fold_left2
 920         (fun res (u1, t1) (u2, t2) ->
 921            if not (UriManager.eq u1 u2) then raise NotMetaConvertible
 922            else aux res t1 t2)
 923         table ens1 ens2
 924     with Invalid_argument _ -> raise NotMetaConvertible
 925   in
 926   aux table t1 t2
 927 ;;
 928
 929
 930 let meta_convertibility_eq eq1 eq2 =
 931   let _, _, (ty, left, right, _), _,_ = open_equality eq1 in
 932   let _, _, (ty', left', right', _), _,_ = open_equality eq2 in
 933   if ty <> ty' then
 934     false
 935   else if (left = left') && (right = right') then
 936     true
 937   else if (left = right') && (right = left') then
 938     true
 939   else
 940     try
 941       let table = meta_convertibility_aux ([], []) left left' in
 942       let _ = meta_convertibility_aux table right right' in
 943       true
 944     with NotMetaConvertible ->
 945       try
 946         let table = meta_convertibility_aux ([], []) left right' in
 947         let _ = meta_convertibility_aux table right left' in
 948         true
 949       with NotMetaConvertible ->
 950         false
 951 ;;
 952
 953
 954 let meta_convertibility t1 t2 =
 955   if t1 = t2 then
 956     true
 957   else
 958     try
 959       ignore(meta_convertibility_aux ([], []) t1 t2);
 960       true
 961     with NotMetaConvertible ->
 962       false
 963 ;;
 964
 965 exception TermIsNotAnEquality;;
 966
 967 let term_is_equality term =
 968   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
 969   match term with
 970   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
 971   | _ -> false
 972 ;;
 973
 974 let equality_of_term proof term =
 975   let eq_uri = LibraryObjects.eq_URI () in
 976   let iseq uri = UriManager.eq uri eq_uri in
 977   match term with
 978   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
 979       let o = !Utils.compare_terms t1 t2 in
 980       let stat = (ty,t1,t2,o) in
 981       let w = Utils.compute_equality_weight stat in
 982       let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
 983       e
 984   | _ ->
 985       raise TermIsNotAnEquality
 986 ;;
 987
 988 let is_weak_identity eq =
 989   let _,_,(_,left, right,_),_,_ = open_equality eq in
 990   left = right || meta_convertibility left right
 991 ;;
 992
 993 let is_identity (_, context, ugraph) eq =
 994   let _,_,(ty,left,right,_),menv,_ = open_equality eq in
 995   left = right ||
 996   (* (meta_convertibility left right)) *)
 997   fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
 998 ;;
 999
1000
1001 let term_of_equality equality =
1002   let _, _, (ty, left, right, _), menv, _= open_equality equality in
1003   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
1004   let argsno = List.length menv in
1005   let t =
1006     CicSubstitution.lift argsno
1007       (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
1008   in
1009   snd (
1010     List.fold_right
1011       (fun (i,_,ty) (n, t) ->
1012          let name = Cic.Name ("X" ^ (string_of_int n)) in
1013          let ty = CicSubstitution.lift (n-1) ty in
1014          let t =
1015            ProofEngineReduction.replace
1016              ~equality:eq ~what:[i]
1017              ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
1018          in
1019            (n-1, Cic.Prod (name, ty, t)))
1020       menv (argsno, t))
1021 ;;
1022