components/tactics/paramodulation/inference.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$ *)
  27
  28 open Utils;;
  29 open Printf;;
  30
  31 let metas_of_proof_time = ref 0.;;
  32 let metas_of_term_time = ref 0.;;
  33 (*
  34 type substitution = Cic.substitution
  35 let apply_subst = CicMetaSubst.apply_subst
  36 let apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
  37 let ppsubst = CicMetaSubst.ppsubst
  38 let buildsubst n context t ty = (n,(context,t,ty))
  39 let flatten_subst subst =
  40     List.map
  41       (fun (i, (context, term, ty)) ->
  42          let context = (*` apply_subst_context subst*) context in
  43          let term = apply_subst subst term in
  44          let ty = apply_subst subst ty in
  45          (i, (context, term, ty))) subst
  46 let rec lookup_subst meta subst =
  47   match meta with
  48   | Cic.Meta (i, _) -> (
  49       try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst
  50       in lookup_subst t subst
  51       with Not_found -> meta
  52     )
  53   | _ -> meta
  54 ;;
  55 *)
  56
  57 (* naif version of apply subst; the local context of metas is ignored;
  58 we assume the substituted term must be lifted according to the nesting
  59 depth of the meta. Alternatively, ee could used implicit instead of
  60 metas *)
  61
  62
  63 type substitution = (int * Cic.term) list
  64
  65 let apply_subst subst term =
  66  let rec aux k t =
  67    match t with
  68        Cic.Rel _ -> t
  69      | Cic.Var (uri,exp_named_subst) ->
  70          let exp_named_subst' =
  71            List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
  72          in
  73            Cic.Var (uri, exp_named_subst')
  74     | Cic.Meta (i, l) ->
  75         (try
  76           aux k (CicSubstitution.lift k (List.assoc i subst))
  77          with Not_found -> t)
  78     | Cic.Sort _
  79     | Cic.Implicit _ -> t
  80     | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
  81     | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
  82     | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
  83     | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
  84     | Cic.Appl [] -> assert false
  85     | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
  86     | Cic.Const (uri,exp_named_subst) ->
  87         let exp_named_subst' =
  88           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
  89         in
  90           if exp_named_subst' != exp_named_subst then
  91             Cic.Const (uri, exp_named_subst')
  92           else
  93             t (* TODO: provare a mantenere il piu' possibile sharing *)
  94     | Cic.MutInd (uri,typeno,exp_named_subst) ->
  95         let exp_named_subst' =
  96           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
  97         in
  98           Cic.MutInd (uri,typeno,exp_named_subst')
  99     | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 100         let exp_named_subst' =
 101           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
 102         in
 103           Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
 104     | Cic.MutCase (sp,i,outty,t,pl) ->
 105         let pl' = List.map (aux k) pl in
 106           Cic.MutCase (sp, i, aux k outty, aux k t, pl')
 107     | Cic.Fix (i, fl) ->
 108         let len = List.length fl in
 109         let fl' =
 110          List.map
 111            (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
 112         in
 113           Cic.Fix (i, fl')
 114     | Cic.CoFix (i, fl) ->
 115         let len = List.length fl in
 116         let fl' =
 117           List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
 118         in
 119           Cic.CoFix (i, fl')
 120 in
 121   aux 0 term
 122 ;;
 123
 124 (* naif version of apply_subst_metasenv: we do not apply the
 125 substitution to the context *)
 126
 127 let apply_subst_metasenv subst metasenv =
 128   List.map
 129     (fun (n, context, ty) ->
 130       (n, context, apply_subst subst ty))
 131     (List.filter
 132       (fun (i, _, _) -> not (List.mem_assoc i subst))
 133       metasenv)
 134
 135 let ppsubst subst =
 136   String.concat "\n"
 137     (List.map
 138       (fun (idx, t) ->
 139          sprintf "%d:= %s" idx (CicPp.ppterm t))
 140        subst)
 141 ;;
 142
 143 let buildsubst n context t ty = (n,t) ;;
 144
 145 let flatten_subst subst =
 146   List.map (fun (i,t) -> i, apply_subst subst t ) subst
 147 ;;
 148
 149 let rec lookup_subst meta subst =
 150   match meta with
 151     | Cic.Meta (i, _) ->
 152         (try
 153           lookup_subst (List.assoc i subst) subst
 154         with
 155             Not_found -> meta)
 156     | _ -> meta
 157 ;;
 158
 159 type equality =
 160     int  *               (* weight *)
 161     proof *
 162     (Cic.term *          (* type *)
 163      Cic.term *          (* left side *)
 164      Cic.term *          (* right side *)
 165      Utils.comparison) * (* ordering *)
 166     Cic.metasenv        (* environment for metas *)
 167
 168 and proof =
 169   | NoProof (* term is the goal missing a proof *)
 170   | BasicProof of substitution * Cic.term
 171   | ProofBlock of
 172       substitution * UriManager.uri *
 173         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
 174   | ProofGoalBlock of proof * proof
 175   | ProofSymBlock of Cic.term list * proof
 176   | SubProof of Cic.term * int * proof
 177 ;;
 178
 179 let string_of_equality ?env =
 180   match env with
 181   | None -> (
 182       function
 183         | w, _, (ty, left, right, o), _ ->
 184             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
 185               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
 186     )
 187   | Some (_, context, _) -> (
 188       let names = names_of_context context in
 189       function
 190         | w, _, (ty, left, right, o), _ ->
 191             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
 192               (CicPp.pp left names) (string_of_comparison o)
 193               (CicPp.pp right names)
 194     )
 195 ;;
 196
 197
 198 let rec string_of_proof = function
 199   | NoProof -> "NoProof "
 200   | BasicProof (s, t) -> "BasicProof " ^
 201       (CicPp.ppterm (apply_subst s t))
 202   | SubProof (t, i, p) ->
 203       Printf.sprintf "SubProof(%s, %s, %s)"
 204         (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
 205   | ProofSymBlock _ -> "ProofSymBlock"
 206   | ProofBlock (subst, _, _, _ ,_,_) ->
 207       "ProofBlock" ^ (ppsubst subst)
 208   | ProofGoalBlock (p1, p2) ->
 209       Printf.sprintf "ProofGoalBlock(%s, %s)"
 210         (string_of_proof p1) (string_of_proof p2)
 211 ;;
 212
 213
 214 let check_disjoint_invariant subst metasenv msg =
 215   if (List.exists
 216         (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
 217   then
 218     begin
 219       prerr_endline ("not disjoint: " ^ msg);
 220       assert false
 221     end
 222 ;;
 223
 224 (* filter out from metasenv the variables in substs *)
 225 let filter subst metasenv =
 226   List.filter
 227     (fun (m, _, _) ->
 228          try let _ = List.find (fun (i, _) -> m = i) subst in false
 229          with Not_found -> true)
 230     metasenv
 231 ;;
 232
 233 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
 234 let build_ens_for_sym_eq sym_eq_URI termlist =
 235   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
 236   match obj with
 237   | Cic.Constant (_, _, _, uris, _) ->
 238       assert (List.length uris <= List.length termlist);
 239       let rec aux = function
 240         | [], tl -> [], tl
 241         | (uri::uris), (term::tl) ->
 242             let ens, args = aux (uris, tl) in
 243             (uri, term)::ens, args
 244         | _, _ -> assert false
 245       in
 246       aux (uris, termlist)
 247   | _ -> assert false
 248 ;;
 249
 250
 251 let build_proof_term ?(noproof=Cic.Implicit None) proof =
 252   let rec do_build_proof proof =
 253     match proof with
 254     | NoProof ->
 255         Printf.fprintf stderr "WARNING: no proof!\n";
 256         noproof
 257     | BasicProof (s,term) -> apply_subst s term
 258     | ProofGoalBlock (proofbit, proof) ->
 259         print_endline "found ProofGoalBlock, going up...";
 260         do_build_goal_proof proofbit proof
 261     | ProofSymBlock (termlist, proof) ->
 262         let proof = do_build_proof proof in
 263         let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
 264         Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
 265     | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
 266         let t' = Cic.Lambda (name, ty, bo) in
 267         let proof' =
 268           let _, proof', _, _ = eq in
 269           do_build_proof proof'
 270         in
 271         let eqproof = do_build_proof eqproof in
 272         let _, _, (ty, what, other, _), menv' = eq in
 273         let what, other =
 274           if pos = Utils.Left then what, other else other, what
 275         in
 276         apply_subst subst
 277           (Cic.Appl [Cic.Const (eq_URI, []); ty;
 278                      what; t'; eqproof; other; proof'])
 279     | SubProof (term, meta_index, proof) ->
 280         let proof = do_build_proof proof in
 281         let eq i = function
 282           | Cic.Meta (j, _) -> i = j
 283           | _ -> false
 284         in
 285         ProofEngineReduction.replace
 286           ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
 287
 288   and do_build_goal_proof proofbit proof =
 289     match proof with
 290     | ProofGoalBlock (pb, p) ->
 291         do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
 292     | _ -> do_build_proof (replace_proof proofbit proof)
 293
 294   and replace_proof newproof = function
 295     | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
 296         let eqproof' = replace_proof newproof eqproof in
 297         ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
 298     | ProofGoalBlock (pb, p) ->
 299         let pb' = replace_proof newproof pb in
 300         ProofGoalBlock (pb', p)
 301     | BasicProof _ -> newproof
 302     | SubProof (term, meta_index, p) ->
 303         SubProof (term, meta_index, replace_proof newproof p)
 304     | p -> p
 305   in
 306   do_build_proof proof
 307 ;;
 308
 309 let rec metas_of_term = function
 310   | Cic.Meta (i, c) -> [i]
 311   | Cic.Var (_, ens)
 312   | Cic.Const (_, ens)
 313   | Cic.MutInd (_, _, ens)
 314   | Cic.MutConstruct (_, _, _, ens) ->
 315       List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
 316   | Cic.Cast (s, t)
 317   | Cic.Prod (_, s, t)
 318   | Cic.Lambda (_, s, t)
 319   | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
 320   | Cic.Appl l -> List.flatten (List.map metas_of_term l)
 321   | Cic.MutCase (uri, i, s, t, l) ->
 322       (metas_of_term s) @ (metas_of_term t) @
 323         (List.flatten (List.map metas_of_term l))
 324   | Cic.Fix (i, il) ->
 325       List.flatten
 326         (List.map (fun (s, i, t1, t2) ->
 327                      (metas_of_term t1) @ (metas_of_term t2)) il)
 328   | Cic.CoFix (i, il) ->
 329       List.flatten
 330         (List.map (fun (s, t1, t2) ->
 331                      (metas_of_term t1) @ (metas_of_term t2)) il)
 332   | _ -> []
 333 ;;
 334
 335 let rec metas_of_proof p =
 336   if Utils.debug then
 337     let t1 = Unix.gettimeofday () in
 338     let res = metas_of_term (build_proof_term p) in
 339     let t2 = Unix.gettimeofday () in
 340     metas_of_proof_time := !metas_of_proof_time  +. (t2 -. t1);
 341     res
 342   else
 343     metas_of_term (build_proof_term p)
 344 ;;
 345
 346
 347 exception NotMetaConvertible;;
 348
 349 let meta_convertibility_aux table t1 t2 =
 350   let module C = Cic in
 351   let rec aux ((table_l, table_r) as table) t1 t2 =
 352     match t1, t2 with
 353     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
 354         let m1_binding, table_l =
 355           try List.assoc m1 table_l, table_l
 356           with Not_found -> m2, (m1, m2)::table_l
 357         and m2_binding, table_r =
 358           try List.assoc m2 table_r, table_r
 359           with Not_found -> m1, (m2, m1)::table_r
 360         in
 361         if (m1_binding <> m2) || (m2_binding <> m1) then
 362           raise NotMetaConvertible
 363         else (
 364           try
 365             List.fold_left2
 366               (fun res t1 t2 ->
 367                  match t1, t2 with
 368                  | None, Some _ | Some _, None -> raise NotMetaConvertible
 369                  | None, None -> res
 370                  | Some t1, Some t2 -> (aux res t1 t2))
 371               (table_l, table_r) tl1 tl2
 372           with Invalid_argument _ ->
 373             raise NotMetaConvertible
 374         )
 375     | C.Var (u1, ens1), C.Var (u2, ens2)
 376     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
 377         aux_ens table ens1 ens2
 378     | C.Cast (s1, t1), C.Cast (s2, t2)
 379     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
 380     | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
 381     | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
 382         let table = aux table s1 s2 in
 383         aux table t1 t2
 384     | C.Appl l1, C.Appl l2 -> (
 385         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 386         with Invalid_argument _ -> raise NotMetaConvertible
 387       )
 388     | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
 389         when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
 390     | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
 391         when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
 392         aux_ens table ens1 ens2
 393     | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
 394         when (UriManager.eq u1 u2) && i1 = i2 ->
 395         let table = aux table s1 s2 in
 396         let table = aux table t1 t2 in (
 397           try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 398           with Invalid_argument _ -> raise NotMetaConvertible
 399         )
 400     | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
 401         try
 402           List.fold_left2
 403             (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
 404                if i1 <> i2 then raise NotMetaConvertible
 405                else
 406                  let res = (aux res s1 s2) in aux res t1 t2)
 407             table il1 il2
 408         with Invalid_argument _ -> raise NotMetaConvertible
 409       )
 410     | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
 411         try
 412           List.fold_left2
 413             (fun res (n1, s1, t1) (n2, s2, t2) ->
 414                let res = aux res s1 s2 in aux res t1 t2)
 415             table il1 il2
 416         with Invalid_argument _ -> raise NotMetaConvertible
 417       )
 418     | t1, t2 when t1 = t2 -> table
 419     | _, _ -> raise NotMetaConvertible
 420
 421   and aux_ens table ens1 ens2 =
 422     let cmp (u1, t1) (u2, t2) =
 423       compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
 424     in
 425     let ens1 = List.sort cmp ens1
 426     and ens2 = List.sort cmp ens2 in
 427     try
 428       List.fold_left2
 429         (fun res (u1, t1) (u2, t2) ->
 430            if not (UriManager.eq u1 u2) then raise NotMetaConvertible
 431            else aux res t1 t2)
 432         table ens1 ens2
 433     with Invalid_argument _ -> raise NotMetaConvertible
 434   in
 435   aux table t1 t2
 436 ;;
 437
 438
 439 let meta_convertibility_eq eq1 eq2 =
 440   let _, _, (ty, left, right, _), _ = eq1
 441   and _, _, (ty', left', right', _), _ = eq2 in
 442   if ty <> ty' then
 443     false
 444   else if (left = left') && (right = right') then
 445     true
 446   else if (left = right') && (right = left') then
 447     true
 448   else
 449     try
 450       let table = meta_convertibility_aux ([], []) left left' in
 451       let _ = meta_convertibility_aux table right right' in
 452       true
 453     with NotMetaConvertible ->
 454       try
 455         let table = meta_convertibility_aux ([], []) left right' in
 456         let _ = meta_convertibility_aux table right left' in
 457         true
 458       with NotMetaConvertible ->
 459         false
 460 ;;
 461
 462
 463 let meta_convertibility t1 t2 =
 464   if t1 = t2 then
 465     true
 466   else
 467     try
 468       ignore(meta_convertibility_aux ([], []) t1 t2);
 469       true
 470     with NotMetaConvertible ->
 471       false
 472 ;;
 473
 474
 475 let rec check_irl start = function
 476   | [] -> true
 477   | None::tl -> check_irl (start+1) tl
 478   | (Some (Cic.Rel x))::tl ->
 479       if x = start then check_irl (start+1) tl else false
 480   | _ -> false
 481 ;;
 482
 483
 484 let rec is_simple_term = function
 485   | Cic.Appl ((Cic.Meta _)::_) -> false
 486   | Cic.Appl l -> List.for_all is_simple_term l
 487   | Cic.Meta (i, l) -> check_irl 1 l
 488   | Cic.Rel _ -> true
 489   | Cic.Const _ -> true
 490   | Cic.MutInd (_, _, []) -> true
 491   | Cic.MutConstruct (_, _, _, []) -> true
 492   | _ -> false
 493 ;;
 494
 495 let locked menv i =
 496   List.exists (fun (j,_,_) -> i = j) menv
 497 ;;
 498
 499 let unification_simple locked_menv metasenv context t1 t2 ugraph =
 500   let module C = Cic in
 501   let module M = CicMetaSubst in
 502   let module U = CicUnification in
 503   let lookup = lookup_subst in
 504   let rec occurs_check subst what where =
 505     match where with
 506     | t when what = t -> true
 507     | C.Appl l -> List.exists (occurs_check subst what) l
 508     | C.Meta _ ->
 509         let t = lookup where subst in
 510         if t <> where then occurs_check subst what t else false
 511     | _ -> false
 512   in
 513   let rec unif subst menv s t =
 514     let s = match s with C.Meta _ -> lookup s subst | _ -> s
 515     and t = match t with C.Meta _ -> lookup t subst | _ -> t
 516
 517     in
 518     match s, t with
 519     | s, t when s = t -> subst, menv
 520     | C.Meta (i, _), C.Meta (j, _)
 521         when (locked locked_menv i) &&(locked locked_menv j) ->
 522         raise
 523           (U.UnificationFailure (lazy "Inference.unification.unif"))
 524     | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->
 525         unif subst menv t s
 526     | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
 527         unif subst menv t s
 528     | C.Meta _, t when occurs_check subst s t ->
 529         raise
 530           (U.UnificationFailure (lazy "Inference.unification.unif"))
 531     | C.Meta (i, l), t when (locked locked_menv i) ->
 532         raise
 533           (U.UnificationFailure (lazy "Inference.unification.unif"))
 534     | C.Meta (i, l), t -> (
 535         try
 536           let _, _, ty = CicUtil.lookup_meta i menv in
 537           assert (not (List.mem_assoc i subst));
 538           let subst = (buildsubst i context t ty)::subst in
 539           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
 540           subst, menv
 541         with CicUtil.Meta_not_found m ->
 542           let names = names_of_context context in
 543           debug_print
 544             (lazy
 545                (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
 546                   (CicPp.pp t1 names) (CicPp.pp t2 names)
 547                   (print_metasenv menv) (print_metasenv metasenv)));
 548           assert false
 549       )
 550     | _, C.Meta _ -> unif subst menv t s
 551     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
 552         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 553     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
 554         try
 555           List.fold_left2
 556             (fun (subst', menv) s t -> unif subst' menv s t)
 557             (subst, menv) tls tlt
 558         with Invalid_argument _ ->
 559           raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 560       )
 561     | _, _ ->
 562         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 563   in
 564   let subst, menv = unif [] metasenv t1 t2 in
 565   let menv = filter subst menv in
 566   List.rev subst, menv, ugraph
 567 ;;
 568
 569 let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
 570 let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
 571 let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
 572 let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 573
 574 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
 575   let metasenv = metasenv1 @ metasenv2 in
 576   let subst, menv, ug =
 577     if not (is_simple_term t1) || not (is_simple_term t2) then (
 578       debug_print
 579         (lazy
 580            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
 581               (CicPp.ppterm t1) (CicPp.ppterm t2)));
 582       raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif"))
 583     ) else
 584       if b then
 585         (* full unification *)
 586         unification_simple [] metasenv context t1 t2 ugraph
 587       else
 588         (* matching: metasenv1 is locked *)
 589         unification_simple metasenv1 metasenv context t1 t2 ugraph
 590   in
 591   if Utils.debug_res then
 592             ignore(check_disjoint_invariant subst menv "unif");
 593   (* let flatten subst =
 594     List.map
 595       (fun (i, (context, term, ty)) ->
 596          let context = apply_subst_context subst context in
 597          let term = apply_subst subst term in
 598          let ty = apply_subst subst ty in
 599            (i, (context, term, ty))) subst
 600   in
 601   let flatten subst = profiler.HExtlib.profile flatten subst in
 602   let subst = flatten subst in *)
 603     subst, menv, ug
 604 ;;
 605
 606 exception MatchingFailure;;
 607
 608 let matching1 metasenv1 metasenv2 context t1 t2 ugraph =
 609   try
 610     unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
 611   with
 612     CicUnification .UnificationFailure _ ->
 613       raise MatchingFailure
 614 ;;
 615
 616 let unification = unification_aux true
 617 ;;
 618
 619 (** matching takes in input the _disjoint_ metasenv of t1 and  t2;
 620 it perform unification in the union metasenv, then check that
 621 the first metasenv has not changed *)
 622
 623 let matching = matching1;;
 624
 625 let check_eq context msg eq =
 626   let w, proof, (eq_ty, left, right, order), metas = eq in
 627   if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
 628    (fst (CicTypeChecker.type_of_aux' metas context  left CicUniv.empty_ugraph))
 629    CicUniv.empty_ugraph))
 630   then
 631     begin
 632       prerr_endline msg;
 633       assert false;
 634     end
 635   else ()
 636 ;;
 637
 638 let find_equalities context proof =
 639   let module C = Cic in
 640   let module S = CicSubstitution in
 641   let module T = CicTypeChecker in
 642   let eq_uri = LibraryObjects.eq_URI () in
 643   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 644   let ok_types ty menv =
 645     List.for_all (fun (_, _, mt) -> mt = ty) menv
 646   in
 647   let rec aux index newmeta = function
 648     | [] -> [], newmeta
 649     | (Some (_, C.Decl (term)))::tl ->
 650         let do_find context term =
 651           match term with
 652           | C.Prod (name, s, t) ->
 653               let (head, newmetas, args, newmeta) =
 654                 ProofEngineHelpers.saturate_term newmeta []
 655                   context (S.lift index term) 0
 656               in
 657               let p =
 658                 if List.length args = 0 then
 659                   C.Rel index
 660                 else
 661                   C.Appl ((C.Rel index)::args)
 662               in (
 663                 match head with
 664                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 665                     when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
 666                     debug_print
 667                       (lazy
 668                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 669                     let o = !Utils.compare_terms t1 t2 in
 670                     let stat = (ty,t1,t2,o) in
 671                     let w = compute_equality_weight stat in
 672                     let proof = BasicProof ([],p) in
 673                     let e = (w, proof, stat, newmetas) in
 674                     Some e, (newmeta+1)
 675                 | _ -> None, newmeta
 676               )
 677           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 678               when UriManager.eq uri eq_uri ->
 679               let ty = S.lift index ty in
 680               let t1 = S.lift index t1 in
 681               let t2 = S.lift index t2 in
 682               let o = !Utils.compare_terms t1 t2 in
 683               let stat = (ty,t1,t2,o) in
 684               let w = compute_equality_weight stat in
 685               let e = (w, BasicProof ([],(C.Rel index)), stat, []) in
 686               Some e, (newmeta+1)
 687           | _ -> None, newmeta
 688         in (
 689           match do_find context term with
 690           | Some p, newmeta ->
 691               let tl, newmeta' = (aux (index+1) newmeta tl) in
 692               if newmeta' < newmeta then
 693                 prerr_endline "big trouble";
 694               (index, p)::tl, newmeta' (* max???? *)
 695           | None, _ ->
 696               aux (index+1) newmeta tl
 697         )
 698     | _::tl ->
 699         aux (index+1) newmeta tl
 700   in
 701   let il, maxm = aux 1 newmeta context in
 702   let indexes, equalities = List.split il in
 703   ignore (List.iter (check_eq context "find") equalities);
 704   indexes, equalities, maxm
 705 ;;
 706
 707
 708 (*
 709 let equations_blacklist =
 710   List.fold_left
 711     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
 712     UriManager.UriSet.empty [
 713       "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
 714       "cic:/Coq/Init/Logic/trans_eq.con";
 715       "cic:/Coq/Init/Logic/f_equal.con";
 716       "cic:/Coq/Init/Logic/f_equal2.con";
 717       "cic:/Coq/Init/Logic/f_equal3.con";
 718       "cic:/Coq/Init/Logic/f_equal4.con";
 719       "cic:/Coq/Init/Logic/f_equal5.con";
 720       "cic:/Coq/Init/Logic/sym_eq.con";
 721       "cic:/Coq/Init/Logic/eq_ind.con";
 722       "cic:/Coq/Init/Logic/eq_ind_r.con";
 723       "cic:/Coq/Init/Logic/eq_rec.con";
 724       "cic:/Coq/Init/Logic/eq_rec_r.con";
 725       "cic:/Coq/Init/Logic/eq_rect.con";
 726       "cic:/Coq/Init/Logic/eq_rect_r.con";
 727       "cic:/Coq/Logic/Eqdep/UIP.con";
 728       "cic:/Coq/Logic/Eqdep/UIP_refl.con";
 729       "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
 730       "cic:/Coq/ZArith/Zcompare/rename.con";
 731       (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
 732          perche' questo cacchio di teorema rompe le scatole :'( *)
 733       "cic:/Rocq/SUBST/comparith/mult_n_2.con";
 734
 735       "cic:/matita/logic/equality/eq_f.con";
 736       "cic:/matita/logic/equality/eq_f2.con";
 737       "cic:/matita/logic/equality/eq_rec.con";
 738       "cic:/matita/logic/equality/eq_rect.con";
 739     ]
 740 ;;
 741 *)
 742 let equations_blacklist = UriManager.UriSet.empty;;
 743
 744
 745 let find_library_equalities dbd context status maxmeta =
 746   let module C = Cic in
 747   let module S = CicSubstitution in
 748   let module T = CicTypeChecker in
 749   let blacklist =
 750     List.fold_left
 751       (fun s u -> UriManager.UriSet.add u s)
 752       equations_blacklist
 753       [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 754        eq_ind_r_URI ()]
 755   in
 756   let candidates =
 757     List.fold_left
 758       (fun l uri ->
 759          if UriManager.UriSet.mem uri blacklist then
 760            l
 761          else
 762            let t = CicUtil.term_of_uri uri in
 763            let ty, _ =
 764              CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
 765            in
 766            (uri, t, ty)::l)
 767       []
 768       (let t1 = Unix.gettimeofday () in
 769        let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
 770        let t2 = Unix.gettimeofday () in
 771        (debug_print
 772           (lazy
 773              (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
 774                 (t2 -. t1))));
 775        eqs)
 776   in
 777   let eq_uri1 = eq_XURI ()
 778   and eq_uri2 = LibraryObjects.eq_URI () in
 779   let iseq uri =
 780     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
 781   in
 782   let ok_types ty menv =
 783     List.for_all (fun (_, _, mt) -> mt = ty) menv
 784   in
 785   let rec has_vars = function
 786     | C.Meta _ | C.Rel _ | C.Const _ -> false
 787     | C.Var _ -> true
 788     | C.Appl l -> List.exists has_vars l
 789     | C.Prod (_, s, t) | C.Lambda (_, s, t)
 790     | C.LetIn (_, s, t) | C.Cast (s, t) ->
 791         (has_vars s) || (has_vars t)
 792     | _ -> false
 793  in
 794   let rec aux newmeta = function
 795     | [] -> [], newmeta
 796     | (uri, term, termty)::tl ->
 797         debug_print
 798           (lazy
 799              (Printf.sprintf "Examining: %s (%s)"
 800                 (CicPp.ppterm term) (CicPp.ppterm termty)));
 801         let res, newmeta =
 802           match termty with
 803           | C.Prod (name, s, t) when not (has_vars termty) ->
 804               let head, newmetas, args, newmeta =
 805                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
 806               in
 807               let p =
 808                 if List.length args = 0 then
 809                   term
 810                 else
 811                   C.Appl (term::args)
 812               in (
 813                 match head with
 814                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 815                     when (iseq uri) && (ok_types ty newmetas) ->
 816                     debug_print
 817                       (lazy
 818                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 819                     let o = !Utils.compare_terms t1 t2 in
 820                     let stat = (ty,t1,t2,o) in
 821                     let w = compute_equality_weight stat in
 822                     let proof = BasicProof ([],p) in
 823                     let e = (w, proof, stat, newmetas) in
 824                     Some e, (newmeta+1)
 825                 | _ -> None, newmeta
 826               )
 827           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 828               when iseq uri && not (has_vars termty) ->
 829               let o = !Utils.compare_terms t1 t2 in
 830               let stat = (ty,t1,t2,o) in
 831               let w = compute_equality_weight stat in
 832               let e = (w, BasicProof ([],term), stat, []) in
 833               Some e, (newmeta+1)
 834           | _ -> None, newmeta
 835         in
 836         match res with
 837         | Some e ->
 838             let tl, newmeta' = aux newmeta tl in
 839               if newmeta' < newmeta then
 840                 prerr_endline "big trouble";
 841               (uri, e)::tl, newmeta' (* max???? *)
 842         | None ->
 843             aux newmeta tl
 844   in
 845   let found, maxm = aux maxmeta candidates in
 846   let uriset, eqlist =
 847     (List.fold_left
 848        (fun (s, l) (u, e) ->
 849           if List.exists (meta_convertibility_eq e) (List.map snd l) then (
 850             debug_print
 851               (lazy
 852                  (Printf.sprintf "NO!! %s already there!"
 853                     (string_of_equality e)));
 854             (UriManager.UriSet.add u s, l)
 855           ) else (UriManager.UriSet.add u s, (u, e)::l))
 856        (UriManager.UriSet.empty, []) found)
 857   in
 858   uriset, eqlist, maxm
 859 ;;
 860
 861
 862 let find_library_theorems dbd env status equalities_uris =
 863   let module C = Cic in
 864   let module S = CicSubstitution in
 865   let module T = CicTypeChecker in
 866   let blacklist =
 867     let refl_equal =
 868       UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
 869     let s =
 870       UriManager.UriSet.remove refl_equal
 871         (UriManager.UriSet.union equalities_uris equations_blacklist)
 872     in
 873     List.fold_left
 874       (fun s u -> UriManager.UriSet.add u s)
 875       s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 876          eq_ind_r_URI ()]
 877   in
 878   let metasenv, context, ugraph = env in
 879   let candidates =
 880     List.fold_left
 881       (fun l uri ->
 882          if UriManager.UriSet.mem uri blacklist then l
 883          else
 884            let t = CicUtil.term_of_uri uri in
 885            let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
 886            (t, ty, [])::l)
 887       [] (MetadataQuery.signature_of_goal ~dbd status)
 888   in
 889   let refl_equal =
 890     let u = eq_XURI () in
 891     let t = CicUtil.term_of_uri u in
 892     let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
 893     (t, ty, [])
 894   in
 895   refl_equal::candidates
 896 ;;
 897
 898
 899 let find_context_hypotheses env equalities_indexes =
 900   let metasenv, context, ugraph = env in
 901   let _, res =
 902     List.fold_left
 903       (fun (n, l) entry ->
 904          match entry with
 905          | None -> (n+1, l)
 906          | Some _ ->
 907              if List.mem n equalities_indexes then
 908                (n+1, l)
 909              else
 910                let t = Cic.Rel n in
 911                let ty, _ =
 912                  CicTypeChecker.type_of_aux' metasenv context t ugraph in
 913                (n+1, (t, ty, [])::l))
 914       (1, []) context
 915   in
 916   res
 917 ;;
 918
 919 (*
 920 let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
 921   let table = Hashtbl.create (List.length args) in
 922
 923   let newargs, newmeta =
 924     List.fold_right
 925       (fun t (newargs, index) ->
 926          match t with
 927          | Cic.Meta (i, l) ->
 928              if Hashtbl.mem table i then
 929                let idx = Hashtbl.find table i in
 930                ((Cic.Meta (idx, l))::newargs, index+1)
 931              else
 932                let _ = Hashtbl.add table i index in
 933                ((Cic.Meta (index, l))::newargs, index+1)
 934          | _ -> assert false)
 935       args ([], newmeta+1)
 936   in
 937
 938   let repl where =
 939     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
 940       ~where
 941   in
 942   let menv' =
 943     List.fold_right
 944       (fun (i, context, term) menv ->
 945          try
 946            let index = Hashtbl.find table i in
 947            (index, context, term)::menv
 948          with Not_found ->
 949            (i, context, term)::menv)
 950       menv []
 951   in
 952   let ty = repl ty
 953   and left = repl left
 954   and right = repl right in
 955   let metas =
 956     (metas_of_term left) @
 957       (metas_of_term right) @
 958       (metas_of_term ty) @ (metas_of_proof p) in
 959   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
 960   let newargs =
 961     List.filter
 962       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
 963   in
 964   let _ =
 965     if List.length metas > 0 then
 966       let first = List.hd metas in
 967       (* this new equality might have less variables than its parents: here
 968          we fill the gap with a dummy arg. Example:
 969          with (f X Y) = X we can simplify
 970          (g X) = (f X Y) in
 971          (g X) = X.
 972          So the new equation has only one variable, but it still has type like
 973          \lambda X,Y:..., so we need to pass a dummy arg for Y
 974          (I hope this makes some sense...)
 975       *)
 976       Hashtbl.iter
 977         (fun k v ->
 978            if not (List.exists
 979                      (function Cic.Meta (i, _) -> i = v | _ -> assert false)
 980                      newargs) then
 981              Hashtbl.replace table k first)
 982         (Hashtbl.copy table)
 983   in
 984   let rec fix_proof = function
 985    | NoProof -> NoProof
 986     | BasicProof term -> BasicProof (repl term)
 987     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
 988         let subst' =
 989           List.fold_left
 990             (fun s arg ->
 991                match arg with
 992                | Cic.Meta (i, l) -> (
 993                    try
 994                      let j = Hashtbl.find table i in
 995                      if List.mem_assoc i subst then
 996                        s
 997                      else
 998                        let _, context, ty = CicUtil.lookup_meta i menv in
 999                        (i, (context, Cic.Meta (j, l), ty))::s
1000                    with Not_found | CicUtil.Meta_not_found _ ->
1001                      s
1002                  )
1003                | _ -> assert false)
1004             [] args
1005         in
1006         ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
1007     | p -> assert false
1008   in
1009   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
1010   (newmeta +1, neweq)
1011 ;;
1012 *)
1013
1014 let relocate newmeta menv =
1015   let subst, metasenv, newmeta =
1016     List.fold_right
1017       (fun (i, context, ty) (subst, menv, maxmeta) ->
1018         let irl = [] (*
1019          CicMkImplicit.identity_relocation_list_for_metavariable context *)
1020         in
1021         let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty in
1022         let newmeta = maxmeta, context, ty in
1023         newsubst::subst, newmeta::menv, maxmeta+1)
1024       menv ([], [], newmeta+1)
1025   in
1026   let metasenv = apply_subst_metasenv subst metasenv in
1027   let subst = flatten_subst subst in
1028   subst, metasenv, newmeta
1029
1030
1031 let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
1032   (*
1033   let metas = (metas_of_term left)@(metas_of_term right)
1034     @(metas_of_term ty)@(metas_of_proof p) in
1035   let menv = List.filter (fun (i, _, _) -> List.mem i metas) menv in
1036   *)
1037   (* debug
1038   let _ , eq =
1039     fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
1040   prerr_endline (string_of_equality eq); *)
1041   let subst, metasenv, newmeta = relocate newmeta menv in
1042 (*
1043   if newmeta > 2839 then
1044     begin
1045       prerr_endline (CicPp.ppterm left ^ " = " ^ CicPp.ppterm right);
1046       prerr_endline (CicMetaSubst.ppsubst subst);
1047       prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
1048       assert false;
1049     end;
1050 *)
1051   let ty = apply_subst subst ty in
1052   let left = apply_subst subst left in
1053   let right = apply_subst subst right in
1054   let fix_proof = function
1055     | NoProof -> NoProof
1056     | BasicProof (subst',term) -> BasicProof (subst@subst',term)
1057     | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
1058         (*
1059         let newsubst =
1060           List.map
1061             (fun (i, (context, term, ty)) ->
1062                let context = apply_subst_context subst context in
1063                let term = apply_subst subst term in
1064                let ty = apply_subst subst ty in
1065                  (i, (context, term, ty))) subst' in *)
1066           ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
1067     | p -> assert false
1068   in
1069   let p = fix_proof p in
1070   (*
1071   let metas = (metas_of_term left)@(metas_of_term right)
1072     @(metas_of_term ty)@(metas_of_proof p) in
1073   let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
1074   *)
1075   let eq = (w, p, (ty, left, right, o), metasenv) in
1076   (* debug prerr_endline (string_of_equality eq); *)
1077   newmeta+1, eq
1078
1079 let term_is_equality term =
1080   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
1081   match term with
1082   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
1083   | _ -> false
1084 ;;
1085
1086
1087 exception TermIsNotAnEquality;;
1088
1089 let equality_of_term proof term =
1090   let eq_uri = LibraryObjects.eq_URI () in
1091   let iseq uri = UriManager.eq uri eq_uri in
1092   match term with
1093   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1094       let o = !Utils.compare_terms t1 t2 in
1095       let stat = (ty,t1,t2,o) in
1096       let w = compute_equality_weight stat in
1097       let e = (w, BasicProof ([],proof), stat, []) in
1098       e
1099   | _ ->
1100       raise TermIsNotAnEquality
1101 ;;
1102
1103
1104 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1105
1106 let is_weak_identity (metasenv, context, ugraph) = function
1107   | (_, _, (ty, left, right, _), menv) ->
1108        (left = right ||
1109           (meta_convertibility left right))
1110            (* the test below is not a good idea since it stops
1111               demodulation too early *)
1112            (* (fst (CicReduction.are_convertible
1113                   ~metasenv:(metasenv @ menv) context left right ugraph)))*)
1114 ;;
1115
1116 let is_identity (metasenv, context, ugraph) = function
1117   | (_, _, (ty, left, right, _), menv) ->
1118        (left = right ||
1119           (* (meta_convertibility left right)) *)
1120            (fst (CicReduction.are_convertible
1121                   ~metasenv:(metasenv @ menv) context left right ugraph)))
1122 ;;
1123
1124
1125 let term_of_equality equality =
1126   let _, _, (ty, left, right, _), menv = equality in
1127   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
1128   let argsno = List.length menv in
1129   let t =
1130     CicSubstitution.lift argsno
1131       (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
1132   in
1133   snd (
1134     List.fold_right
1135       (fun (i,_,ty) (n, t) ->
1136          let name = Cic.Name ("X" ^ (string_of_int n)) in
1137          let ty = CicSubstitution.lift (n-1) ty in
1138          let t =
1139            ProofEngineReduction.replace
1140              ~equality:eq ~what:[i]
1141              ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
1142          in
1143            (n-1, Cic.Prod (name, ty, t)))
1144       menv (argsno, t))
1145 ;;