helm/software/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 debug_print x = prerr_endline (Lazy.force x) in
 501   let module C = Cic in
 502   let module M = CicMetaSubst in
 503   let module U = CicUnification in
 504   let lookup = lookup_subst in
 505   let rec occurs_check subst what where =
 506     match where with
 507     | t when what = t -> true
 508     | C.Appl l -> List.exists (occurs_check subst what) l
 509     | C.Meta _ ->
 510         let t = lookup where subst in
 511         if t <> where then occurs_check subst what t else false
 512     | _ -> false
 513   in
 514   let rec unif subst menv s t =
 515     let s = match s with C.Meta _ -> lookup s subst | _ -> s
 516     and t = match t with C.Meta _ -> lookup t subst | _ -> t
 517
 518     in
 519     match s, t with
 520     | s, t when s = t -> subst, menv
 521     | C.Meta (i, _), C.Meta (j, _)
 522         when (locked locked_menv i) &&(locked locked_menv j) ->
 523         raise
 524           (U.UnificationFailure (lazy "Inference.unification.unif"))
 525     | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->
 526         unif subst menv t s
 527     | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
 528         unif subst menv t s
 529     | C.Meta _, t when occurs_check subst s t ->
 530         raise
 531           (U.UnificationFailure (lazy "Inference.unification.unif"))
 532     | C.Meta (i, l), t when (locked locked_menv i) ->
 533         raise
 534           (U.UnificationFailure (lazy "Inference.unification.unif"))
 535     | C.Meta (i, l), t -> (
 536         try
 537           let _, _, ty = CicUtil.lookup_meta i menv in
 538           assert (not (List.mem_assoc i subst));
 539           let subst = (buildsubst i context t ty)::subst in
 540           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
 541           subst, menv
 542         with CicUtil.Meta_not_found m ->
 543           let names = names_of_context context in
 544           debug_print
 545             (lazy
 546                (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
 547                   (CicPp.pp t1 names) (CicPp.pp t2 names)
 548                   (print_metasenv menv) (print_metasenv metasenv)));
 549           assert false
 550       )
 551     | _, C.Meta _ -> unif subst menv t s
 552     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
 553         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 554     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
 555         try
 556           List.fold_left2
 557             (fun (subst', menv) s t -> unif subst' menv s t)
 558             (subst, menv) tls tlt
 559         with Invalid_argument _ ->
 560           raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 561       )
 562     | _, _ ->
 563         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 564   in
 565   let subst, menv = unif [] metasenv t1 t2 in
 566   let menv = filter subst menv in
 567   List.rev subst, menv, ugraph
 568 ;;
 569
 570 let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
 571 let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
 572 let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
 573 let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 574
 575 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
 576   let metasenv = metasenv1 @ metasenv2 in
 577   let subst, menv, ug =
 578     if not (is_simple_term t1) || not (is_simple_term t2) then (
 579       debug_print
 580         (lazy
 581            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
 582               (CicPp.ppterm t1) (CicPp.ppterm t2)));
 583       raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif"))
 584     ) else
 585       if b then
 586         (* full unification *)
 587         unification_simple [] metasenv context t1 t2 ugraph
 588       else
 589         (* matching: metasenv1 is locked *)
 590         unification_simple metasenv1 metasenv context t1 t2 ugraph
 591   in
 592   if Utils.debug_res then
 593             ignore(check_disjoint_invariant subst menv "unif");
 594   (* let flatten subst =
 595     List.map
 596       (fun (i, (context, term, ty)) ->
 597          let context = apply_subst_context subst context in
 598          let term = apply_subst subst term in
 599          let ty = apply_subst subst ty in
 600            (i, (context, term, ty))) subst
 601   in
 602   let flatten subst = profiler.HExtlib.profile flatten subst in
 603   let subst = flatten subst in *)
 604     subst, menv, ug
 605 ;;
 606
 607 exception MatchingFailure;;
 608
 609 let matching1 metasenv1 metasenv2 context t1 t2 ugraph =
 610   try
 611     unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
 612   with
 613     CicUnification .UnificationFailure _ ->
 614       raise MatchingFailure
 615 ;;
 616
 617 let unification = unification_aux true
 618 ;;
 619
 620 (** matching takes in input the _disjoint_ metasenv of t1 and  t2;
 621 it perform unification in the union metasenv, then check that
 622 the first metasenv has not changed *)
 623
 624 let matching = matching1;;
 625
 626 let check_eq context msg eq =
 627   let w, proof, (eq_ty, left, right, order), metas = eq in
 628   if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
 629    (fst (CicTypeChecker.type_of_aux' metas context  left CicUniv.empty_ugraph))
 630    CicUniv.empty_ugraph))
 631   then
 632     begin
 633       prerr_endline msg;
 634       assert false;
 635     end
 636   else ()
 637 ;;
 638
 639 let find_equalities context proof =
 640   let module C = Cic in
 641   let module S = CicSubstitution in
 642   let module T = CicTypeChecker in
 643   let eq_uri = LibraryObjects.eq_URI () in
 644   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 645   let ok_types ty menv =
 646     List.for_all (fun (_, _, mt) -> mt = ty) menv
 647   in
 648   let rec aux index newmeta = function
 649     | [] -> [], newmeta
 650     | (Some (_, C.Decl (term)))::tl ->
 651         let do_find context term =
 652           match term with
 653           | C.Prod (name, s, t) ->
 654               let (head, newmetas, args, newmeta) =
 655                 ProofEngineHelpers.saturate_term newmeta []
 656                   context (S.lift index term) 0
 657               in
 658               let p =
 659                 if List.length args = 0 then
 660                   C.Rel index
 661                 else
 662                   C.Appl ((C.Rel index)::args)
 663               in (
 664                 match head with
 665                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 666                     when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
 667                     debug_print
 668                       (lazy
 669                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 670                     let o = !Utils.compare_terms t1 t2 in
 671                     let stat = (ty,t1,t2,o) in
 672                     let w = compute_equality_weight stat in
 673                     let proof = BasicProof ([],p) in
 674                     let e = (w, proof, stat, newmetas) in
 675                     Some e, (newmeta+1)
 676                 | _ -> None, newmeta
 677               )
 678           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 679               when UriManager.eq uri eq_uri ->
 680               let ty = S.lift index ty in
 681               let t1 = S.lift index t1 in
 682               let t2 = S.lift index t2 in
 683               let o = !Utils.compare_terms t1 t2 in
 684               let stat = (ty,t1,t2,o) in
 685               let w = compute_equality_weight stat in
 686               let e = (w, BasicProof ([],(C.Rel index)), stat, []) in
 687               Some e, (newmeta+1)
 688           | _ -> None, newmeta
 689         in (
 690           match do_find context term with
 691           | Some p, newmeta ->
 692               let tl, newmeta' = (aux (index+1) newmeta tl) in
 693               if newmeta' < newmeta then
 694                 prerr_endline "big trouble";
 695               (index, p)::tl, newmeta' (* max???? *)
 696           | None, _ ->
 697               aux (index+1) newmeta tl
 698         )
 699     | _::tl ->
 700         aux (index+1) newmeta tl
 701   in
 702   let il, maxm = aux 1 newmeta context in
 703   let indexes, equalities = List.split il in
 704   ignore (List.iter (check_eq context "find") equalities);
 705   indexes, equalities, maxm
 706 ;;
 707
 708
 709 (*
 710 let equations_blacklist =
 711   List.fold_left
 712     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
 713     UriManager.UriSet.empty [
 714       "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
 715       "cic:/Coq/Init/Logic/trans_eq.con";
 716       "cic:/Coq/Init/Logic/f_equal.con";
 717       "cic:/Coq/Init/Logic/f_equal2.con";
 718       "cic:/Coq/Init/Logic/f_equal3.con";
 719       "cic:/Coq/Init/Logic/f_equal4.con";
 720       "cic:/Coq/Init/Logic/f_equal5.con";
 721       "cic:/Coq/Init/Logic/sym_eq.con";
 722       "cic:/Coq/Init/Logic/eq_ind.con";
 723       "cic:/Coq/Init/Logic/eq_ind_r.con";
 724       "cic:/Coq/Init/Logic/eq_rec.con";
 725       "cic:/Coq/Init/Logic/eq_rec_r.con";
 726       "cic:/Coq/Init/Logic/eq_rect.con";
 727       "cic:/Coq/Init/Logic/eq_rect_r.con";
 728       "cic:/Coq/Logic/Eqdep/UIP.con";
 729       "cic:/Coq/Logic/Eqdep/UIP_refl.con";
 730       "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
 731       "cic:/Coq/ZArith/Zcompare/rename.con";
 732       (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
 733          perche' questo cacchio di teorema rompe le scatole :'( *)
 734       "cic:/Rocq/SUBST/comparith/mult_n_2.con";
 735
 736       "cic:/matita/logic/equality/eq_f.con";
 737       "cic:/matita/logic/equality/eq_f2.con";
 738       "cic:/matita/logic/equality/eq_rec.con";
 739       "cic:/matita/logic/equality/eq_rect.con";
 740     ]
 741 ;;
 742 *)
 743 let equations_blacklist = UriManager.UriSet.empty;;
 744
 745
 746 let find_library_equalities dbd context status maxmeta =
 747   let module C = Cic in
 748   let module S = CicSubstitution in
 749   let module T = CicTypeChecker in
 750   let blacklist =
 751     List.fold_left
 752       (fun s u -> UriManager.UriSet.add u s)
 753       equations_blacklist
 754       [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 755        eq_ind_r_URI ()]
 756   in
 757   let candidates =
 758     List.fold_left
 759       (fun l uri ->
 760          if UriManager.UriSet.mem uri blacklist then
 761            l
 762          else
 763            let t = CicUtil.term_of_uri uri in
 764            let ty, _ =
 765              CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
 766            in
 767            (uri, t, ty)::l)
 768       []
 769       (let t1 = Unix.gettimeofday () in
 770        let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
 771        let t2 = Unix.gettimeofday () in
 772        (debug_print
 773           (lazy
 774              (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
 775                 (t2 -. t1))));
 776        eqs)
 777   in
 778   let eq_uri1 = eq_XURI ()
 779   and eq_uri2 = LibraryObjects.eq_URI () in
 780   let iseq uri =
 781     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
 782   in
 783   let ok_types ty menv =
 784     List.for_all (fun (_, _, mt) -> mt = ty) menv
 785   in
 786   let rec has_vars = function
 787     | C.Meta _ | C.Rel _ | C.Const _ -> false
 788     | C.Var _ -> true
 789     | C.Appl l -> List.exists has_vars l
 790     | C.Prod (_, s, t) | C.Lambda (_, s, t)
 791     | C.LetIn (_, s, t) | C.Cast (s, t) ->
 792         (has_vars s) || (has_vars t)
 793     | _ -> false
 794  in
 795   let rec aux newmeta = function
 796     | [] -> [], newmeta
 797     | (uri, term, termty)::tl ->
 798         debug_print
 799           (lazy
 800              (Printf.sprintf "Examining: %s (%s)"
 801                 (CicPp.ppterm term) (CicPp.ppterm termty)));
 802         let res, newmeta =
 803           match termty with
 804           | C.Prod (name, s, t) when not (has_vars termty) ->
 805               let head, newmetas, args, newmeta =
 806                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
 807               in
 808               let p =
 809                 if List.length args = 0 then
 810                   term
 811                 else
 812                   C.Appl (term::args)
 813               in (
 814                 match head with
 815                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 816                     when (iseq uri) && (ok_types ty newmetas) ->
 817                     debug_print
 818                       (lazy
 819                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 820                     let o = !Utils.compare_terms t1 t2 in
 821                     let stat = (ty,t1,t2,o) in
 822                     let w = compute_equality_weight stat in
 823                     let proof = BasicProof ([],p) in
 824                     let e = (w, proof, stat, newmetas) in
 825                     Some e, (newmeta+1)
 826                 | _ -> None, newmeta
 827               )
 828           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 829               when iseq uri && not (has_vars termty) ->
 830               let o = !Utils.compare_terms t1 t2 in
 831               let stat = (ty,t1,t2,o) in
 832               let w = compute_equality_weight stat in
 833               let e = (w, BasicProof ([],term), stat, []) in
 834               Some e, (newmeta+1)
 835           | _ -> None, newmeta
 836         in
 837         match res with
 838         | Some e ->
 839             let tl, newmeta' = aux newmeta tl in
 840               if newmeta' < newmeta then
 841                 prerr_endline "big trouble";
 842               (uri, e)::tl, newmeta' (* max???? *)
 843         | None ->
 844             aux newmeta tl
 845   in
 846   let found, maxm = aux maxmeta candidates in
 847   let uriset, eqlist =
 848     (List.fold_left
 849        (fun (s, l) (u, e) ->
 850           if List.exists (meta_convertibility_eq e) (List.map snd l) then (
 851             debug_print
 852               (lazy
 853                  (Printf.sprintf "NO!! %s already there!"
 854                     (string_of_equality e)));
 855             (UriManager.UriSet.add u s, l)
 856           ) else (UriManager.UriSet.add u s, (u, e)::l))
 857        (UriManager.UriSet.empty, []) found)
 858   in
 859   uriset, eqlist, maxm
 860 ;;
 861
 862
 863 let find_library_theorems dbd env status equalities_uris =
 864   let module C = Cic in
 865   let module S = CicSubstitution in
 866   let module T = CicTypeChecker in
 867   let blacklist =
 868     let refl_equal =
 869       UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
 870     let s =
 871       UriManager.UriSet.remove refl_equal
 872         (UriManager.UriSet.union equalities_uris equations_blacklist)
 873     in
 874     List.fold_left
 875       (fun s u -> UriManager.UriSet.add u s)
 876       s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 877          eq_ind_r_URI ()]
 878   in
 879   let metasenv, context, ugraph = env in
 880   let candidates =
 881     List.fold_left
 882       (fun l uri ->
 883          if UriManager.UriSet.mem uri blacklist then l
 884          else
 885            let t = CicUtil.term_of_uri uri in
 886            let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
 887            (t, ty, [])::l)
 888       [] (MetadataQuery.signature_of_goal ~dbd status)
 889   in
 890   let refl_equal =
 891     let u = eq_XURI () in
 892     let t = CicUtil.term_of_uri u in
 893     let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
 894     (t, ty, [])
 895   in
 896   refl_equal::candidates
 897 ;;
 898
 899
 900 let find_context_hypotheses env equalities_indexes =
 901   let metasenv, context, ugraph = env in
 902   let _, res =
 903     List.fold_left
 904       (fun (n, l) entry ->
 905          match entry with
 906          | None -> (n+1, l)
 907          | Some _ ->
 908              if List.mem n equalities_indexes then
 909                (n+1, l)
 910              else
 911                let t = Cic.Rel n in
 912                let ty, _ =
 913                  CicTypeChecker.type_of_aux' metasenv context t ugraph in
 914                (n+1, (t, ty, [])::l))
 915       (1, []) context
 916   in
 917   res
 918 ;;
 919
 920 (*
 921 let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
 922   let table = Hashtbl.create (List.length args) in
 923
 924   let newargs, newmeta =
 925     List.fold_right
 926       (fun t (newargs, index) ->
 927          match t with
 928          | Cic.Meta (i, l) ->
 929              if Hashtbl.mem table i then
 930                let idx = Hashtbl.find table i in
 931                ((Cic.Meta (idx, l))::newargs, index+1)
 932              else
 933                let _ = Hashtbl.add table i index in
 934                ((Cic.Meta (index, l))::newargs, index+1)
 935          | _ -> assert false)
 936       args ([], newmeta+1)
 937   in
 938
 939   let repl where =
 940     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
 941       ~where
 942   in
 943   let menv' =
 944     List.fold_right
 945       (fun (i, context, term) menv ->
 946          try
 947            let index = Hashtbl.find table i in
 948            (index, context, term)::menv
 949          with Not_found ->
 950            (i, context, term)::menv)
 951       menv []
 952   in
 953   let ty = repl ty
 954   and left = repl left
 955   and right = repl right in
 956   let metas =
 957     (metas_of_term left) @
 958       (metas_of_term right) @
 959       (metas_of_term ty) @ (metas_of_proof p) in
 960   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
 961   let newargs =
 962     List.filter
 963       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
 964   in
 965   let _ =
 966     if List.length metas > 0 then
 967       let first = List.hd metas in
 968       (* this new equality might have less variables than its parents: here
 969          we fill the gap with a dummy arg. Example:
 970          with (f X Y) = X we can simplify
 971          (g X) = (f X Y) in
 972          (g X) = X.
 973          So the new equation has only one variable, but it still has type like
 974          \lambda X,Y:..., so we need to pass a dummy arg for Y
 975          (I hope this makes some sense...)
 976       *)
 977       Hashtbl.iter
 978         (fun k v ->
 979            if not (List.exists
 980                      (function Cic.Meta (i, _) -> i = v | _ -> assert false)
 981                      newargs) then
 982              Hashtbl.replace table k first)
 983         (Hashtbl.copy table)
 984   in
 985   let rec fix_proof = function
 986    | NoProof -> NoProof
 987     | BasicProof term -> BasicProof (repl term)
 988     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
 989         let subst' =
 990           List.fold_left
 991             (fun s arg ->
 992                match arg with
 993                | Cic.Meta (i, l) -> (
 994                    try
 995                      let j = Hashtbl.find table i in
 996                      if List.mem_assoc i subst then
 997                        s
 998                      else
 999                        let _, context, ty = CicUtil.lookup_meta i menv in
1000                        (i, (context, Cic.Meta (j, l), ty))::s
1001                    with Not_found | CicUtil.Meta_not_found _ ->
1002                      s
1003                  )
1004                | _ -> assert false)
1005             [] args
1006         in
1007         ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
1008     | p -> assert false
1009   in
1010   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
1011   (newmeta +1, neweq)
1012 ;;
1013 *)
1014
1015 let relocate newmeta menv =
1016   let subst, metasenv, newmeta =
1017     List.fold_right
1018       (fun (i, context, ty) (subst, menv, maxmeta) ->
1019         let irl = [] (*
1020          CicMkImplicit.identity_relocation_list_for_metavariable context *)
1021         in
1022         let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty in
1023         let newmeta = maxmeta, context, ty in
1024         newsubst::subst, newmeta::menv, maxmeta+1)
1025       menv ([], [], newmeta+1)
1026   in
1027   let metasenv = apply_subst_metasenv subst metasenv in
1028   let subst = flatten_subst subst in
1029   subst, metasenv, newmeta
1030
1031
1032 let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
1033   (*
1034   let metas = (metas_of_term left)@(metas_of_term right)
1035     @(metas_of_term ty)@(metas_of_proof p) in
1036   let menv = List.filter (fun (i, _, _) -> List.mem i metas) menv in
1037   *)
1038   (* debug
1039   let _ , eq =
1040     fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
1041   prerr_endline (string_of_equality eq); *)
1042   let subst, metasenv, newmeta = relocate newmeta menv in
1043 (*
1044   if newmeta > 2839 then
1045     begin
1046       prerr_endline (CicPp.ppterm left ^ " = " ^ CicPp.ppterm right);
1047       prerr_endline (CicMetaSubst.ppsubst subst);
1048       prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
1049       assert false;
1050     end;
1051 *)
1052   let ty = apply_subst subst ty in
1053   let left = apply_subst subst left in
1054   let right = apply_subst subst right in
1055   let fix_proof = function
1056     | NoProof -> NoProof
1057     | BasicProof (subst',term) -> BasicProof (subst@subst',term)
1058     | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
1059         (*
1060         let newsubst =
1061           List.map
1062             (fun (i, (context, term, ty)) ->
1063                let context = apply_subst_context subst context in
1064                let term = apply_subst subst term in
1065                let ty = apply_subst subst ty in
1066                  (i, (context, term, ty))) subst' in *)
1067           ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
1068     | p -> assert false
1069   in
1070   let p = fix_proof p in
1071   (*
1072   let metas = (metas_of_term left)@(metas_of_term right)
1073     @(metas_of_term ty)@(metas_of_proof p) in
1074   let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
1075   *)
1076   let eq = (w, p, (ty, left, right, o), metasenv) in
1077   (* debug prerr_endline (string_of_equality eq); *)
1078   newmeta+1, eq
1079
1080 let term_is_equality term =
1081   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
1082   match term with
1083   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
1084   | _ -> false
1085 ;;
1086
1087
1088 exception TermIsNotAnEquality;;
1089
1090 let equality_of_term proof term =
1091   let eq_uri = LibraryObjects.eq_URI () in
1092   let iseq uri = UriManager.eq uri eq_uri in
1093   match term with
1094   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1095       let o = !Utils.compare_terms t1 t2 in
1096       let stat = (ty,t1,t2,o) in
1097       let w = compute_equality_weight stat in
1098       let e = (w, BasicProof ([],proof), stat, []) in
1099       e
1100   | _ ->
1101       raise TermIsNotAnEquality
1102 ;;
1103
1104
1105 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1106
1107 let is_weak_identity (metasenv, context, ugraph) = function
1108   | (_, _, (ty, left, right, _), menv) ->
1109        (left = right ||
1110           (meta_convertibility left right))
1111            (* the test below is not a good idea since it stops
1112               demodulation too early *)
1113            (* (fst (CicReduction.are_convertible
1114                   ~metasenv:(metasenv @ menv) context left right ugraph)))*)
1115 ;;
1116
1117 let is_identity (metasenv, context, ugraph) = function
1118   | (_, _, (ty, left, right, _), menv) ->
1119        (left = right ||
1120           (* (meta_convertibility left right)) *)
1121            (fst (CicReduction.are_convertible
1122                   ~metasenv:(metasenv @ menv) context left right ugraph)))
1123 ;;
1124
1125
1126 let term_of_equality equality =
1127   let _, _, (ty, left, right, _), menv = equality in
1128   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
1129   let argsno = List.length menv in
1130   let t =
1131     CicSubstitution.lift argsno
1132       (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
1133   in
1134   snd (
1135     List.fold_right
1136       (fun (i,_,ty) (n, t) ->
1137          let name = Cic.Name ("X" ^ (string_of_int n)) in
1138          let ty = CicSubstitution.lift (n-1) ty in
1139          let t =
1140            ProofEngineReduction.replace
1141              ~equality:eq ~what:[i]
1142              ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
1143          in
1144            (n-1, Cic.Prod (name, ty, t)))
1145       menv (argsno, t))
1146 ;;