helm/ocaml/paramodulation/inference.ml

   1 open Utils;;
   2
   3
   4 type equality =
   5     int  *               (* weight *)
   6     proof *
   7     (Cic.term *          (* type *)
   8      Cic.term *          (* left side *)
   9      Cic.term *          (* right side *)
  10      Utils.comparison) * (* ordering *)
  11     Cic.metasenv *       (* environment for metas *)
  12     Cic.term list        (* arguments *)
  13
  14 and proof =
  15   | NoProof
  16   | BasicProof of Cic.term
  17   | ProofBlock of
  18       Cic.substitution * UriManager.uri *
  19         (Cic.name * Cic.term) * Cic.term *
  20         (* name, ty, eq_ty, left, right *)
  21 (*         (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) *  *)
  22         (Utils.pos * equality) * proof
  23   | ProofGoalBlock of proof * proof (* equality *)
  24 (*   | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof *)
  25   | ProofSymBlock of Cic.term list * proof
  26   | SubProof of Cic.term * int * proof
  27 ;;
  28
  29
  30 let string_of_equality ?env =
  31   match env with
  32   | None -> (
  33       function
  34         | w, _, (ty, left, right, o), _, _ ->
  35             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
  36               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
  37     )
  38   | Some (_, context, _) -> (
  39       let names = names_of_context context in
  40       function
  41         | w, _, (ty, left, right, o), _, _ ->
  42             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
  43               (CicPp.pp left names) (string_of_comparison o)
  44               (CicPp.pp right names)
  45     )
  46 ;;
  47
  48
  49 let build_ens_for_sym_eq sym_eq_URI termlist =
  50   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
  51   match obj with
  52   | Cic.Constant (_, _, _, uris, _) ->
  53       assert (List.length uris <= List.length termlist);
  54       let rec aux = function
  55         | [], tl -> [], tl
  56         | (uri::uris), (term::tl) ->
  57             let ens, args = aux (uris, tl) in
  58             (uri, term)::ens, args
  59         | _, _ -> assert false
  60       in
  61       aux (uris, termlist)
  62   | _ -> assert false
  63 (*   [(UriManager.uri_of_string *)
  64 (*       "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty); *)
  65 (*    (UriManager.uri_of_string *)
  66 (*       "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x); *)
  67 (*    (UriManager.uri_of_string *)
  68 (*       "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)] *)
  69 ;;
  70
  71
  72 let build_proof_term proof =
  73   let rec do_build_proof proof =
  74     match proof with
  75     | NoProof ->
  76         Printf.fprintf stderr "WARNING: no proof!\n";
  77         Cic.Implicit None
  78     | BasicProof term -> term
  79     | ProofGoalBlock (proofbit, proof) ->
  80         print_endline "found ProofGoalBlock, going up...";
  81         do_build_goal_proof proofbit proof
  82 (*     | ProofSymBlock (ens, proof) -> *)
  83 (*         let proof = do_build_proof proof in *)
  84 (*         Cic.Appl [ *)
  85 (*           Cic.Const (Utils.sym_eq_URI (), ens); (\* symmetry *\) *)
  86 (*           proof *)
  87 (*         ] *)
  88     | ProofSymBlock (termlist, proof) ->
  89         let proof = do_build_proof proof in
  90         let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
  91         Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
  92     | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) ->
  93         let t' = Cic.Lambda (name, ty, bo) in
  94         let proof' =
  95           let _, proof', _, _, _ = eq in
  96           do_build_proof proof'
  97         in
  98         let eqproof = do_build_proof eqproof in
  99         let _, _, (ty, what, other, _), menv', args' = eq in
 100         let what, other =
 101           if pos = Utils.Left then what, other else other, what
 102         in
 103         CicMetaSubst.apply_subst subst
 104           (Cic.Appl [Cic.Const (eq_URI, []); ty;
 105                      what; t'; eqproof; other; proof'])
 106     | SubProof (term, meta_index, proof) ->
 107         let proof = do_build_proof proof in
 108         let eq i = function
 109           | Cic.Meta (j, _) -> i = j
 110           | _ -> false
 111         in
 112         ProofEngineReduction.replace
 113           ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
 114
 115   and do_build_goal_proof proofbit proof =
 116 (*     match proofbit with *)
 117 (*     | BasicProof _ -> do_build_proof proof *)
 118 (*     | proofbit -> *)
 119         match proof with
 120         | ProofGoalBlock (pb, p(* eq *)) ->
 121             do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p(* eq *)))
 122 (*             let _, proof, _, _, _  = eq in *)
 123 (*             let newproof = replace_proof proofbit proof in *)
 124 (*             do_build_proof newproof *)
 125
 126 (*         | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *)
 127 (*             let eqproof' = replace_proof proofbit eqproof in *)
 128 (*             do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *)
 129         | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
 130
 131   and replace_proof newproof = function
 132     | ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof) ->
 133         let eqproof' = replace_proof newproof eqproof in
 134         ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof')
 135     | ProofGoalBlock (pb, p(* equality *)) ->
 136         let pb' = replace_proof newproof pb in
 137         ProofGoalBlock (pb', p(* equality *))
 138 (*         let w, proof, t, menv, args = equality in *)
 139 (*         let proof' = replace_proof newproof proof in *)
 140 (*         ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
 141     | BasicProof _ -> newproof
 142     | SubProof (term, meta_index, p) ->
 143         SubProof (term, meta_index, replace_proof newproof p)
 144     | p -> p
 145   in
 146 (*   let _, proof, _, _, _ = equality in *)
 147   do_build_proof proof
 148 ;;
 149
 150
 151 let rec metas_of_term = function
 152   | Cic.Meta (i, c) -> [i]
 153   | Cic.Var (_, ens)
 154   | Cic.Const (_, ens)
 155   | Cic.MutInd (_, _, ens)
 156   | Cic.MutConstruct (_, _, _, ens) ->
 157       List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
 158   | Cic.Cast (s, t)
 159   | Cic.Prod (_, s, t)
 160   | Cic.Lambda (_, s, t)
 161   | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
 162   | Cic.Appl l -> List.flatten (List.map metas_of_term l)
 163   | Cic.MutCase (uri, i, s, t, l) ->
 164       (metas_of_term s) @ (metas_of_term t) @
 165         (List.flatten (List.map metas_of_term l))
 166   | Cic.Fix (i, il) ->
 167       List.flatten
 168         (List.map (fun (s, i, t1, t2) ->
 169                      (metas_of_term t1) @ (metas_of_term t2)) il)
 170   | Cic.CoFix (i, il) ->
 171       List.flatten
 172         (List.map (fun (s, t1, t2) ->
 173                      (metas_of_term t1) @ (metas_of_term t2)) il)
 174   | _ -> []
 175 ;;
 176
 177
 178 exception NotMetaConvertible;;
 179
 180 let meta_convertibility_aux table t1 t2 =
 181   let module C = Cic in
 182   let print_table t =
 183     String.concat ", "
 184       (List.map
 185          (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
 186   in
 187   let rec aux ((table_l, table_r) as table) t1 t2 =
 188 (*     Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
 189 (*       (CicPp.ppterm t1) (CicPp.ppterm t2) *)
 190 (*       (print_table table_l) (print_table table_r); *)
 191     match t1, t2 with
 192     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
 193         let m1_binding, table_l =
 194           try List.assoc m1 table_l, table_l
 195           with Not_found -> m2, (m1, m2)::table_l
 196         and m2_binding, table_r =
 197           try List.assoc m2 table_r, table_r
 198           with Not_found -> m1, (m2, m1)::table_r
 199         in
 200 (*         let m1_binding, m2_binding, table = *)
 201 (*           let m1b, table =  *)
 202 (*             try List.assoc m1 table, table *)
 203 (*             with Not_found -> m2, (m1, m2)::table *)
 204 (*           in *)
 205 (*           let m2b, table =  *)
 206 (*             try List.assoc m2 table, table *)
 207 (*             with Not_found -> m1, (m2, m1)::table *)
 208 (*           in *)
 209 (*           m1b, m2b, table *)
 210 (*         in *)
 211 (*         Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
 212 (*           (print_table table_l) (print_table table_r); *)
 213         if (m1_binding <> m2) || (m2_binding <> m1) then
 214           raise NotMetaConvertible
 215         else (
 216           try
 217             List.fold_left2
 218               (fun res t1 t2 ->
 219                  match t1, t2 with
 220                  | None, Some _ | Some _, None -> raise NotMetaConvertible
 221                  | None, None -> res
 222                  | Some t1, Some t2 -> (aux res t1 t2))
 223               (table_l, table_r) tl1 tl2
 224           with Invalid_argument _ ->
 225             raise NotMetaConvertible
 226         )
 227     | C.Var (u1, ens1), C.Var (u2, ens2)
 228     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
 229         aux_ens table ens1 ens2
 230     | C.Cast (s1, t1), C.Cast (s2, t2)
 231     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
 232     | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
 233     | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
 234         let table = aux table s1 s2 in
 235         aux table t1 t2
 236     | C.Appl l1, C.Appl l2 -> (
 237         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 238         with Invalid_argument _ -> raise NotMetaConvertible
 239       )
 240     | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
 241         when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
 242     | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
 243         when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
 244         aux_ens table ens1 ens2
 245     | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
 246         when (UriManager.eq u1 u2) && i1 = i2 ->
 247         let table = aux table s1 s2 in
 248         let table = aux table t1 t2 in (
 249           try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 250           with Invalid_argument _ -> raise NotMetaConvertible
 251         )
 252     | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
 253         try
 254           List.fold_left2
 255             (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
 256                if i1 <> i2 then raise NotMetaConvertible
 257                else
 258                  let res = (aux res s1 s2) in aux res t1 t2)
 259             table il1 il2
 260         with Invalid_argument _ -> raise NotMetaConvertible
 261       )
 262     | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
 263         try
 264           List.fold_left2
 265             (fun res (n1, s1, t1) (n2, s2, t2) ->
 266                let res = aux res s1 s2 in aux res t1 t2)
 267             table il1 il2
 268         with Invalid_argument _ -> raise NotMetaConvertible
 269       )
 270     | t1, t2 when t1 = t2 -> table
 271     | _, _ -> raise NotMetaConvertible
 272
 273   and aux_ens table ens1 ens2 =
 274     let cmp (u1, t1) (u2, t2) =
 275       compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
 276     in
 277     let ens1 = List.sort cmp ens1
 278     and ens2 = List.sort cmp ens2 in
 279     try
 280       List.fold_left2
 281         (fun res (u1, t1) (u2, t2) ->
 282            if not (UriManager.eq u1 u2) then raise NotMetaConvertible
 283            else aux res t1 t2)
 284         table ens1 ens2
 285     with Invalid_argument _ -> raise NotMetaConvertible
 286   in
 287   aux table t1 t2
 288 ;;
 289
 290
 291 let meta_convertibility_eq eq1 eq2 =
 292   let _, _, (ty, left, right, _), _, _ = eq1
 293   and _, _, (ty', left', right', _), _, _ = eq2 in
 294   if ty <> ty' then
 295     false
 296   else if (left = left') && (right = right') then
 297     true
 298   else if (left = right') && (right = left') then
 299     true
 300   else
 301     try
 302       let table = meta_convertibility_aux ([], []) left left' in
 303       let _ = meta_convertibility_aux table right right' in
 304       true
 305     with NotMetaConvertible ->
 306       try
 307         let table = meta_convertibility_aux ([], []) left right' in
 308         let _ = meta_convertibility_aux table right left' in
 309         true
 310       with NotMetaConvertible ->
 311         false
 312 ;;
 313
 314
 315 let meta_convertibility t1 t2 =
 316   let f t =
 317     String.concat ", "
 318       (List.map
 319          (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
 320   in
 321   if t1 = t2 then
 322     true
 323   else
 324     try
 325       let l, r = meta_convertibility_aux ([], []) t1 t2 in
 326       (*     Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
 327       true
 328     with NotMetaConvertible ->
 329       false
 330 ;;
 331
 332
 333 (*
 334 let replace_metas (* context *) term =
 335   let module C = Cic in
 336   let rec aux = function
 337     | C.Meta (i, c) ->
 338 (*         let irl = *)
 339 (*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
 340 (*         in *)
 341 (*         if c = irl then *)
 342 (*           C.Implicit (Some (`MetaIndex i)) *)
 343 (*         else ( *)
 344 (*           Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
 345 (*             (String.concat "\n" *)
 346 (*                (List.map *)
 347 (*                   (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
 348 (*           C.Meta (i, c) *)
 349 (*         ) *)
 350         C.Implicit (Some (`MetaInfo (i, c)))
 351     | C.Var (u, ens) -> C.Var (u, aux_ens ens)
 352     | C.Const (u, ens) -> C.Const (u, aux_ens ens)
 353     | C.Cast (s, t) -> C.Cast (aux s, aux t)
 354     | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
 355     | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
 356     | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
 357     | C.Appl l -> C.Appl (List.map aux l)
 358     | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
 359     | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
 360     | C.MutCase (uri, i, s, t, l) ->
 361         C.MutCase (uri, i, aux s, aux t, List.map aux l)
 362     | C.Fix (i, il) ->
 363         let il' =
 364           List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
 365         C.Fix (i, il')
 366     | C.CoFix (i, il) ->
 367         let il' =
 368           List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
 369         C.CoFix (i, il')
 370     | t -> t
 371   and aux_ens ens =
 372     List.map (fun (u, t) -> (u, aux t)) ens
 373   in
 374   aux term
 375 ;;
 376 *)
 377
 378
 379 (*
 380 let restore_metas (* context *) term =
 381   let module C = Cic in
 382   let rec aux = function
 383     | C.Implicit (Some (`MetaInfo (i, c))) ->
 384 (*         let c = *)
 385 (*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
 386 (*         in *)
 387 (*         C.Meta (i, c) *)
 388 (*         let local_context:(C.term option) list = *)
 389 (*           Marshal.from_string mc 0 *)
 390 (*         in *)
 391 (*         C.Meta (i, local_context) *)
 392         C.Meta (i, c)
 393     | C.Var (u, ens) -> C.Var (u, aux_ens ens)
 394     | C.Const (u, ens) -> C.Const (u, aux_ens ens)
 395     | C.Cast (s, t) -> C.Cast (aux s, aux t)
 396     | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
 397     | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
 398     | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
 399     | C.Appl l -> C.Appl (List.map aux l)
 400     | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
 401     | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
 402     | C.MutCase (uri, i, s, t, l) ->
 403         C.MutCase (uri, i, aux s, aux t, List.map aux l)
 404     | C.Fix (i, il) ->
 405         let il' =
 406           List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
 407         C.Fix (i, il')
 408     | C.CoFix (i, il) ->
 409         let il' =
 410           List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
 411         C.CoFix (i, il')
 412     | t -> t
 413   and aux_ens ens =
 414     List.map (fun (u, t) -> (u, aux t)) ens
 415   in
 416   aux term
 417 ;;
 418 *)
 419
 420 (*
 421 let rec restore_subst (* context *) subst =
 422   List.map
 423     (fun (i, (c, t, ty)) ->
 424        i, (c, restore_metas (* context *) t, ty))
 425     subst
 426 ;;
 427 *)
 428
 429
 430 let rec check_irl start = function
 431   | [] -> true
 432   | None::tl -> check_irl (start+1) tl
 433   | (Some (Cic.Rel x))::tl ->
 434       if x = start then check_irl (start+1) tl else false
 435   | _ -> false
 436 ;;
 437
 438 let rec is_simple_term = function
 439   | Cic.Appl ((Cic.Meta _)::_) -> false
 440   | Cic.Appl l -> List.for_all is_simple_term l
 441   | Cic.Meta (i, l) -> check_irl 1 l
 442   | Cic.Rel _ -> true
 443   | Cic.Const _ -> true
 444   | Cic.MutInd (_, _, []) -> true
 445   | Cic.MutConstruct (_, _, _, []) -> true
 446   | _ -> false
 447 ;;
 448
 449
 450 let lookup_subst meta subst =
 451   match meta with
 452   | Cic.Meta (i, _) -> (
 453       try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 454       with Not_found -> meta
 455     )
 456   | _ -> assert false
 457 ;;
 458
 459
 460 let unification_simple metasenv context t1 t2 ugraph =
 461   let module C = Cic in
 462   let module M = CicMetaSubst in
 463   let module U = CicUnification in
 464   let lookup = lookup_subst in
 465   let rec occurs_check subst what where =
 466     match where with
 467     | t when what = t -> true
 468     | C.Appl l -> List.exists (occurs_check subst what) l
 469     | C.Meta _ ->
 470         let t = lookup where subst in
 471         if t <> where then occurs_check subst what t else false
 472     | _ -> false
 473   in
 474   let rec unif subst menv s t =
 475     let s = match s with C.Meta _ -> lookup s subst | _ -> s
 476     and t = match t with C.Meta _ -> lookup t subst | _ -> t
 477     in
 478     match s, t with
 479     | s, t when s = t -> subst, menv
 480     | C.Meta (i, _), C.Meta (j, _) when i > j ->
 481         unif subst menv t s
 482     | C.Meta _, t when occurs_check subst s t ->
 483         raise
 484           (U.UnificationFailure
 485              (U.failure_msg_of_string "Inference.unification.unif"))
 486     | C.Meta (i, l), t -> (
 487         try
 488           let _, _, ty = CicUtil.lookup_meta i menv in
 489           let subst =
 490             if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
 491             else subst
 492           in
 493           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
 494           subst, menv
 495         with CicUtil.Meta_not_found m ->
 496           let names = names_of_context context in
 497           debug_print
 498             (lazy
 499                (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
 500                   (CicPp.pp t1 names) (CicPp.pp t2 names)
 501                   (print_metasenv menv) (print_metasenv metasenv)));
 502           assert false
 503       )
 504     | _, C.Meta _ -> unif subst menv t s
 505     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
 506         raise (U.UnificationFailure
 507                  (U.failure_msg_of_string "Inference.unification.unif"))
 508     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
 509         try
 510           List.fold_left2
 511             (fun (subst', menv) s t -> unif subst' menv s t)
 512             (subst, menv) tls tlt
 513         with Invalid_argument _ ->
 514           raise (U.UnificationFailure
 515                    (U.failure_msg_of_string "Inference.unification.unif"))
 516       )
 517     | _, _ ->
 518         raise (U.UnificationFailure
 519                  (U.failure_msg_of_string "Inference.unification.unif"))
 520   in
 521   let subst, menv = unif [] metasenv t1 t2 in
 522   let menv =
 523     List.filter
 524       (fun (m, _, _) ->
 525          try let _ = List.find (fun (i, _) -> m = i) subst in false
 526          with Not_found -> true)
 527       menv
 528   in
 529   List.rev subst, menv, ugraph
 530 ;;
 531
 532
 533 let unification metasenv context t1 t2 ugraph =
 534 (*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
 535   let subst, menv, ug =
 536     if not (is_simple_term t1) || not (is_simple_term t2) then (
 537       debug_print
 538         (lazy
 539            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
 540               (CicPp.ppterm t1) (CicPp.ppterm t2)));
 541       CicUnification.fo_unif metasenv context t1 t2 ugraph
 542     ) else
 543       unification_simple metasenv context t1 t2 ugraph
 544   in
 545   let rec fix_term = function
 546     | (Cic.Meta (i, l) as t) ->
 547         let t' = lookup_subst t subst in
 548         if t <> t' then fix_term t' else t
 549     | Cic.Appl l -> Cic.Appl (List.map fix_term l)
 550     | t -> t
 551   in
 552   let rec fix_subst = function
 553     | [] -> []
 554     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
 555   in
 556 (*   Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
 557 (*   print_endline "|"; *)
 558   fix_subst subst, menv, ug
 559 ;;
 560
 561
 562 (* let unification = CicUnification.fo_unif;; *)
 563
 564 exception MatchingFailure;;
 565
 566
 567 let matching_simple metasenv context t1 t2 ugraph =
 568   let module C = Cic in
 569   let module M = CicMetaSubst in
 570   let module U = CicUnification in
 571   let lookup meta subst =
 572     match meta with
 573     | C.Meta (i, _) -> (
 574         try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 575         with Not_found -> meta
 576       )
 577     | _ -> assert false
 578   in
 579   let rec do_match subst menv s t =
 580 (*     Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
 581 (*       (print_subst subst); *)
 582 (*     print_newline (); *)
 583 (*     let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
 584 (*     let t = match t with C.Meta _ -> lookup t subst | _ -> t in  *)
 585     (*       Printf.printf "after apply_subst: %s %s\n%s" *)
 586     (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
 587     (*       print_newline (); *)
 588     match s, t with
 589     | s, t when s = t -> subst, menv
 590 (*     | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
 591 (*         do_match subst menv t s *)
 592 (*     | C.Meta _, t when occurs_check subst s t -> *)
 593 (*         raise MatchingFailure *)
 594 (*     | s, C.Meta _ when occurs_check subst t s -> *)
 595 (*         raise MatchingFailure *)
 596     | s, C.Meta (i, l) ->
 597         let filter_menv i menv =
 598           List.filter (fun (m, _, _) -> i <> m) menv
 599         in
 600         let subst, menv =
 601           let value = lookup t subst in
 602           match value with
 603 (*           | C.Meta (i', l') when Hashtbl.mem table i' -> *)
 604 (*               (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
 605           | value when value = t ->
 606               let _, _, ty = CicUtil.lookup_meta i menv in
 607               (i, (context, s, ty))::subst, filter_menv i menv
 608           | value when value <> s ->
 609               raise MatchingFailure
 610           | value -> do_match subst menv s value
 611         in
 612         subst, menv
 613 (*           else if value <> s then *)
 614 (*             raise MatchingFailure *)
 615 (*           else subst *)
 616 (*           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
 617 (*           else subst *)
 618 (*         in *)
 619 (*         let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
 620 (*         subst, menv *)
 621 (*     | _, C.Meta _ -> do_match subst menv t s *)
 622 (*     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
 623 (*         raise MatchingFailure *)
 624     | C.Appl ls, C.Appl lt -> (
 625         try
 626           List.fold_left2
 627             (fun (subst, menv) s t -> do_match subst menv s t)
 628             (subst, menv) ls lt
 629         with Invalid_argument _ ->
 630 (*           print_endline (Printexc.to_string e); *)
 631 (*           Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
 632 (*           print_newline ();           *)
 633           raise MatchingFailure
 634       )
 635     | _, _ ->
 636 (*         Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
 637 (*         print_newline (); *)
 638         raise MatchingFailure
 639   in
 640   let subst, menv = do_match [] metasenv t1 t2 in
 641   (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
 642   (*     print_newline (); *)
 643   subst, menv, ugraph
 644 ;;
 645
 646
 647 let matching metasenv context t1 t2 ugraph =
 648 (*   if (is_simple_term t1) && (is_simple_term t2) then *)
 649 (*     let subst, menv, ug = *)
 650 (*       matching_simple metasenv context t1 t2 ugraph in *)
 651 (* (\*     Printf.printf "matching %s %s:\n%s\n" *\) *)
 652 (* (\*       (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
 653 (* (\*     print_newline (); *\) *)
 654 (*     subst, menv, ug *)
 655 (*   else *)
 656 (*   debug_print *)
 657 (*     (Printf.sprintf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *)
 658 (*   print_newline (); *)
 659     try
 660       let subst, metasenv, ugraph =
 661         (*       CicUnification.fo_unif metasenv context t1 t2 ugraph *)
 662         unification metasenv context t1 t2 ugraph
 663       in
 664       let t' = CicMetaSubst.apply_subst subst t1 in
 665       if not (meta_convertibility t1 t') then
 666         raise MatchingFailure
 667       else
 668         let metas = metas_of_term t1 in
 669         let fix_subst = function
 670           | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
 671               (j, (c, Cic.Meta (i, lc), ty))
 672           | s -> s
 673         in
 674         let subst = List.map fix_subst subst in
 675
 676 (*         Printf.printf "matching %s %s:\n%s\n" *)
 677 (*           (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
 678 (*         print_newline (); *)
 679
 680         subst, metasenv, ugraph
 681     with
 682     | CicUnification.UnificationFailure _
 683     | CicUnification.Uncertain _ ->
 684 (*       Printf.printf "failed to match %s %s\n" *)
 685 (*         (CicPp.ppterm t1) (CicPp.ppterm t2); *)
 686 (*       print_endline (Printexc.to_string e); *)
 687       raise MatchingFailure
 688 ;;
 689
 690 (* let matching = *)
 691 (*   let profile = CicUtil.profile "Inference.matching" in *)
 692 (*   (fun metasenv context t1 t2 ugraph -> *)
 693 (*      profile (matching metasenv context t1 t2) ugraph) *)
 694 (* ;; *)
 695
 696
 697 let beta_expand ?(metas_ok=true) ?(match_only=false)
 698     what type_of_what where context metasenv ugraph =
 699   let module S = CicSubstitution in
 700   let module C = Cic in
 701
 702 (*   let _ = *)
 703 (*     let names = names_of_context context in *)
 704 (*     Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
 705 (*       (CicPp.pp what names) (CicPp.ppterm what) *)
 706 (*       (CicPp.pp where names) (CicPp.ppterm where); *)
 707 (*     print_newline (); *)
 708 (*   in *)
 709   (*
 710     return value:
 711     ((list of all possible beta expansions, subst, metasenv, ugraph),
 712      lifted term)
 713   *)
 714   let rec aux lift_amount term context metasenv subst ugraph =
 715 (*     Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
 716     let res, lifted_term =
 717       match term with
 718       | C.Rel m  ->
 719           [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 720
 721       | C.Var (uri, exp_named_subst) ->
 722           let ens', lifted_ens =
 723             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 724           in
 725           let expansions =
 726             List.map
 727               (fun (e, s, m, ug) ->
 728                  (C.Var (uri, e), s, m, ug)) ens'
 729           in
 730           expansions, C.Var (uri, lifted_ens)
 731
 732       | C.Meta (i, l) ->
 733           let l', lifted_l =
 734             List.fold_right
 735               (fun arg (res, lifted_tl) ->
 736                  match arg with
 737                  | Some arg ->
 738                      let arg_res, lifted_arg =
 739                        aux lift_amount arg context metasenv subst ugraph in
 740                      let l1 =
 741                        List.map
 742                          (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
 743                          arg_res
 744                      in
 745                      (l1 @
 746                         (List.map
 747                            (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
 748                            res),
 749                       (Some lifted_arg)::lifted_tl)
 750                  | None ->
 751                      (List.map
 752                         (fun (r, s, m, ug) -> None::r, s, m, ug)
 753                         res,
 754                       None::lifted_tl)
 755               ) l ([], [])
 756           in
 757           let e =
 758             List.map
 759               (fun (l, s, m, ug) ->
 760                  (C.Meta (i, l), s, m, ug)) l'
 761           in
 762           e, C.Meta (i, lifted_l)
 763
 764       | C.Sort _
 765       | C.Implicit _ as t -> [], t
 766
 767       | C.Cast (s, t) ->
 768           let l1, lifted_s =
 769             aux lift_amount s context metasenv subst ugraph in
 770           let l2, lifted_t =
 771             aux lift_amount t context metasenv subst ugraph
 772           in
 773           let l1' =
 774             List.map
 775               (fun (t, s, m, ug) ->
 776                  C.Cast (t, lifted_t), s, m, ug) l1 in
 777           let l2' =
 778             List.map
 779               (fun (t, s, m, ug) ->
 780                  C.Cast (lifted_s, t), s, m, ug) l2 in
 781           l1'@l2', C.Cast (lifted_s, lifted_t)
 782
 783       | C.Prod (nn, s, t) ->
 784           let l1, lifted_s =
 785             aux lift_amount s context metasenv subst ugraph in
 786           let l2, lifted_t =
 787             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
 788               metasenv subst ugraph
 789           in
 790           let l1' =
 791             List.map
 792               (fun (t, s, m, ug) ->
 793                  C.Prod (nn, t, lifted_t), s, m, ug) l1 in
 794           let l2' =
 795             List.map
 796               (fun (t, s, m, ug) ->
 797                  C.Prod (nn, lifted_s, t), s, m, ug) l2 in
 798           l1'@l2', C.Prod (nn, lifted_s, lifted_t)
 799
 800       | C.Lambda (nn, s, t) ->
 801           let l1, lifted_s =
 802             aux lift_amount s context metasenv subst ugraph in
 803           let l2, lifted_t =
 804             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
 805               metasenv subst ugraph
 806           in
 807           let l1' =
 808             List.map
 809               (fun (t, s, m, ug) ->
 810                  C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
 811           let l2' =
 812             List.map
 813               (fun (t, s, m, ug) ->
 814                  C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
 815           l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
 816
 817       | C.LetIn (nn, s, t) ->
 818           let l1, lifted_s =
 819             aux lift_amount s context metasenv subst ugraph in
 820           let l2, lifted_t =
 821             aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
 822               metasenv subst ugraph
 823           in
 824           let l1' =
 825             List.map
 826               (fun (t, s, m, ug) ->
 827                  C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
 828           let l2' =
 829             List.map
 830               (fun (t, s, m, ug) ->
 831                  C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
 832           l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
 833
 834       | C.Appl l ->
 835           let l', lifted_l =
 836             aux_list lift_amount l context metasenv subst ugraph
 837           in
 838           (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
 839            C.Appl lifted_l)
 840
 841       | C.Const (uri, exp_named_subst) ->
 842           let ens', lifted_ens =
 843             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 844           in
 845           let expansions =
 846             List.map
 847               (fun (e, s, m, ug) ->
 848                  (C.Const (uri, e), s, m, ug)) ens'
 849           in
 850           (expansions, C.Const (uri, lifted_ens))
 851
 852       | C.MutInd (uri, i ,exp_named_subst) ->
 853           let ens', lifted_ens =
 854             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 855           in
 856           let expansions =
 857             List.map
 858               (fun (e, s, m, ug) ->
 859                  (C.MutInd (uri, i, e), s, m, ug)) ens'
 860           in
 861           (expansions, C.MutInd (uri, i, lifted_ens))
 862
 863       | C.MutConstruct (uri, i, j, exp_named_subst) ->
 864           let ens', lifted_ens =
 865             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 866           in
 867           let expansions =
 868             List.map
 869               (fun (e, s, m, ug) ->
 870                  (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
 871           in
 872           (expansions, C.MutConstruct (uri, i, j, lifted_ens))
 873
 874       | C.MutCase (sp, i, outt, t, pl) ->
 875           let pl_res, lifted_pl =
 876             aux_list lift_amount pl context metasenv subst ugraph
 877           in
 878           let l1, lifted_outt =
 879             aux lift_amount outt context metasenv subst ugraph in
 880           let l2, lifted_t =
 881             aux lift_amount t context metasenv subst ugraph in
 882
 883           let l1' =
 884             List.map
 885               (fun (outt, s, m, ug) ->
 886                  C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
 887           let l2' =
 888             List.map
 889               (fun (t, s, m, ug) ->
 890                  C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
 891           let l3' =
 892             List.map
 893               (fun (pl, s, m, ug) ->
 894                  C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
 895           in
 896           (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
 897
 898       | C.Fix (i, fl) ->
 899           let len = List.length fl in
 900           let fl', lifted_fl =
 901             List.fold_right
 902               (fun (nm, idx, ty, bo) (res, lifted_tl) ->
 903                  let lifted_ty = S.lift lift_amount ty in
 904                  let bo_res, lifted_bo =
 905                    aux (lift_amount+len) bo context metasenv subst ugraph in
 906                  let l1 =
 907                    List.map
 908                      (fun (a, s, m, ug) ->
 909                         (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
 910                      bo_res
 911                  in
 912                  (l1 @
 913                     (List.map
 914                        (fun (r, s, m, ug) ->
 915                           (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
 916                   (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
 917               ) fl ([], [])
 918           in
 919           (List.map
 920              (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
 921            C.Fix (i, lifted_fl))
 922
 923       | C.CoFix (i, fl) ->
 924           let len = List.length fl in
 925           let fl', lifted_fl =
 926             List.fold_right
 927               (fun (nm, ty, bo) (res, lifted_tl) ->
 928                  let lifted_ty = S.lift lift_amount ty in
 929                  let bo_res, lifted_bo =
 930                    aux (lift_amount+len) bo context metasenv subst ugraph in
 931                  let l1 =
 932                    List.map
 933                      (fun (a, s, m, ug) ->
 934                         (nm, lifted_ty, a)::lifted_tl, s, m, ug)
 935                      bo_res
 936                  in
 937                  (l1 @
 938                     (List.map
 939                        (fun (r, s, m, ug) ->
 940                           (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
 941                   (nm, lifted_ty, lifted_bo)::lifted_tl)
 942               ) fl ([], [])
 943           in
 944           (List.map
 945              (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
 946            C.CoFix (i, lifted_fl))
 947     in
 948     let retval =
 949       match term with
 950       | C.Meta _ when (not metas_ok) ->
 951           res, lifted_term
 952       | _ ->
 953 (*           let term' = *)
 954 (*             if match_only then replace_metas context term *)
 955 (*             else term *)
 956 (*           in *)
 957           try
 958             let subst', metasenv', ugraph' =
 959 (*               Printf.printf "provo a unificare %s e %s\n" *)
 960 (*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
 961               if match_only then
 962                 matching metasenv context term (S.lift lift_amount what) ugraph
 963               else
 964                 CicUnification.fo_unif metasenv context
 965                   (S.lift lift_amount what) term ugraph
 966             in
 967 (*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
 968 (*             (CicPp.ppterm (S.lift lift_amount what)); *)
 969 (*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
 970 (*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
 971             (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
 972 (*             if match_only then *)
 973 (*               let t' = CicMetaSubst.apply_subst subst' term in *)
 974 (*               if not (meta_convertibility term t') then ( *)
 975 (*                 res, lifted_term *)
 976 (*               ) else ( *)
 977 (*                 let metas = metas_of_term term in *)
 978 (*                 let fix_subst = function *)
 979 (*                   | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
 980 (*                       (j, (c, C.Meta (i, lc), ty)) *)
 981 (*                   | s -> s *)
 982 (*                 in *)
 983 (*                 let subst' = List.map fix_subst subst' in *)
 984 (*                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
 985 (*                  lifted_term) *)
 986 (*               ) *)
 987 (*             else *)
 988               ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
 989                lifted_term)
 990           with
 991           | MatchingFailure
 992           | CicUnification.UnificationFailure _
 993           | CicUnification.Uncertain _ ->
 994               res, lifted_term
 995     in
 996 (*     Printf.printf "exit aux\n"; *)
 997     retval
 998
 999   and aux_list lift_amount l context metasenv subst ugraph =
1000     List.fold_right
1001       (fun arg (res, lifted_tl) ->
1002          let arg_res, lifted_arg =
1003            aux lift_amount arg context metasenv subst ugraph in
1004          let l1 = List.map
1005            (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
1006          in
1007          (l1 @ (List.map
1008                   (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
1009           lifted_arg::lifted_tl)
1010       ) l ([], [])
1011
1012   and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
1013     List.fold_right
1014       (fun (u, arg) (res, lifted_tl) ->
1015          let arg_res, lifted_arg =
1016            aux lift_amount arg context metasenv subst ugraph in
1017          let l1 =
1018            List.map
1019              (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
1020          in
1021          (l1 @ (List.map (fun (r, s, m, ug) ->
1022                             (u, lifted_arg)::r, s, m, ug) res),
1023           (u, lifted_arg)::lifted_tl)
1024       ) exp_named_subst ([], [])
1025
1026   in
1027   let expansions, _ =
1028 (*     let where = *)
1029 (*       if match_only then replace_metas (\* context *\) where *)
1030 (*       else where *)
1031 (*     in *)
1032     aux 0 where context metasenv [] ugraph
1033   in
1034   let mapfun =
1035 (*     if match_only then *)
1036 (*       (fun (term, subst, metasenv, ugraph) -> *)
1037 (*          let term' = *)
1038 (*            C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
1039 (*          and subst = restore_subst subst in *)
1040 (*          (term', subst, metasenv, ugraph)) *)
1041 (*     else *)
1042       (fun (term, subst, metasenv, ugraph) ->
1043          let term' = C.Lambda (C.Anonymous, type_of_what, term) in
1044          (term', subst, metasenv, ugraph))
1045   in
1046   List.map mapfun expansions
1047 ;;
1048
1049
1050 let find_equalities context proof =
1051   let module C = Cic in
1052   let module S = CicSubstitution in
1053   let module T = CicTypeChecker in
1054   let eq_uri = LibraryObjects.eq_URI () in
1055   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
1056   let ok_types ty menv =
1057     List.for_all (fun (_, _, mt) -> mt = ty) menv
1058   in
1059   let rec aux index newmeta = function
1060     | [] -> [], newmeta
1061     | (Some (_, C.Decl (term)))::tl ->
1062         let do_find context term =
1063           match term with
1064           | C.Prod (name, s, t) ->
1065 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
1066               let (head, newmetas, args, newmeta) =
1067                 ProofEngineHelpers.saturate_term newmeta []
1068                   context (S.lift index term) 0
1069               in
1070               let p =
1071                 if List.length args = 0 then
1072                   C.Rel index
1073                 else
1074                   C.Appl ((C.Rel index)::args)
1075               in (
1076                 match head with
1077                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
1078                     when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
1079                     debug_print
1080                       (lazy
1081                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
1082 (*                     debug_print ( *)
1083 (*                       Printf.sprintf "args: %s\n" *)
1084 (*                         (String.concat ", " (List.map CicPp.ppterm args)))); *)
1085 (*                     debug_print (lazy ( *)
1086 (*                       Printf.sprintf "newmetas:\n%s\n" *)
1087 (*                         (print_metasenv newmetas))); *)
1088                     let o = !Utils.compare_terms t1 t2 in
1089                     let w = compute_equality_weight ty t1 t2 in
1090                     let proof = BasicProof p in
1091                     let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
1092                     Some e, (newmeta+1)
1093                 | _ -> None, newmeta
1094               )
1095           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
1096               when UriManager.eq uri eq_uri ->
1097               let t1 = S.lift index t1
1098               and t2 = S.lift index t2 in
1099               let o = !Utils.compare_terms t1 t2 in
1100               let w = compute_equality_weight ty t1 t2 in
1101               let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
1102               Some e, (newmeta+1)
1103           | _ -> None, newmeta
1104         in (
1105           match do_find context term with
1106           | Some p, newmeta ->
1107               let tl, newmeta' = (aux (index+1) newmeta tl) in
1108               (index, p)::tl, max newmeta newmeta'
1109           | None, _ ->
1110               aux (index+1) newmeta tl
1111         )
1112     | _::tl ->
1113         aux (index+1) newmeta tl
1114   in
1115   let il, maxm = aux 1 newmeta context in
1116   let indexes, equalities = List.split il in
1117   indexes, equalities, maxm
1118 ;;
1119
1120
1121 let equations_blacklist =
1122   List.fold_left
1123     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
1124     UriManager.UriSet.empty [
1125       "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
1126       "cic:/Coq/Init/Logic/trans_eq.con";
1127       "cic:/Coq/Init/Logic/f_equal.con";
1128       "cic:/Coq/Init/Logic/f_equal2.con";
1129       "cic:/Coq/Init/Logic/f_equal3.con";
1130       "cic:/Coq/Init/Logic/f_equal4.con";
1131       "cic:/Coq/Init/Logic/f_equal5.con";
1132       "cic:/Coq/Init/Logic/sym_eq.con";
1133       "cic:/Coq/Init/Logic/eq_ind.con";
1134       "cic:/Coq/Init/Logic/eq_ind_r.con";
1135       "cic:/Coq/Init/Logic/eq_rec.con";
1136       "cic:/Coq/Init/Logic/eq_rec_r.con";
1137       "cic:/Coq/Init/Logic/eq_rect.con";
1138       "cic:/Coq/Init/Logic/eq_rect_r.con";
1139       "cic:/Coq/Logic/Eqdep/UIP.con";
1140       "cic:/Coq/Logic/Eqdep/UIP_refl.con";
1141       "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
1142       "cic:/Coq/ZArith/Zcompare/rename.con";
1143       (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
1144          perche' questo cacchio di teorema rompe le scatole :'( *)
1145       "cic:/Rocq/SUBST/comparith/mult_n_2.con";
1146     ]
1147       ;;
1148
1149 let find_library_equalities dbd context status maxmeta =
1150   let module C = Cic in
1151   let module S = CicSubstitution in
1152   let module T = CicTypeChecker in
1153   let blacklist =
1154     List.fold_left
1155       (fun s u -> UriManager.UriSet.add u s)
1156       equations_blacklist
1157       [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
1158        eq_ind_r_URI ()]
1159   in
1160   let candidates =
1161     List.fold_left
1162       (fun l uri ->
1163         let suri = UriManager.string_of_uri uri in
1164          if UriManager.UriSet.mem uri blacklist then
1165            l
1166          else
1167            let t = CicUtil.term_of_uri uri in
1168            let ty, _ =
1169              CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
1170            in
1171            (uri, t, ty)::l)
1172       []
1173       (MetadataQuery.equations_for_goal ~dbd status)
1174   in
1175   let eq_uri1 = eq_XURI () (* UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI *)
1176   and eq_uri2 = LibraryObjects.eq_URI () in (* HelmLibraryObjects.Logic.eq_URI in *)
1177   let iseq uri =
1178     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
1179   in
1180   let ok_types ty menv =
1181     List.for_all (fun (_, _, mt) -> mt = ty) menv
1182   in
1183   let rec aux newmeta = function
1184     | [] -> [], newmeta
1185     | (uri, term, termty)::tl ->
1186         debug_print
1187           (lazy
1188              (Printf.sprintf "Examining: %s (%s)"
1189                 (CicPp.ppterm term) (CicPp.ppterm termty)));
1190         let res, newmeta =
1191           match termty with
1192           | C.Prod (name, s, t) ->
1193               let head, newmetas, args, newmeta =
1194                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
1195               in
1196               let p =
1197                 if List.length args = 0 then
1198                   term
1199                 else
1200                   C.Appl (term::args)
1201               in (
1202                 match head with
1203                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
1204                     when (iseq uri) && (ok_types ty newmetas) ->
1205                     debug_print
1206                       (lazy
1207                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
1208                     let o = !Utils.compare_terms t1 t2 in
1209                     let w = compute_equality_weight ty t1 t2 in
1210                     let proof = BasicProof p in
1211                     let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
1212                     Some e, (newmeta+1)
1213                 | _ -> None, newmeta
1214               )
1215           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1216               let o = !Utils.compare_terms t1 t2 in
1217               let w = compute_equality_weight ty t1 t2 in
1218               let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
1219               Some e, (newmeta+1)
1220           | _ -> None, newmeta
1221         in
1222         match res with
1223         | Some e ->
1224             let tl, newmeta' = aux newmeta tl in
1225             (uri, e)::tl, max newmeta newmeta'
1226         | None ->
1227             aux newmeta tl
1228   in
1229   let found, maxm = aux maxmeta candidates in
1230   let uriset, eqlist =
1231     (List.fold_left
1232        (fun (s, l) (u, e) ->
1233           if List.exists (meta_convertibility_eq e) l then (
1234             debug_print
1235               (lazy
1236                  (Printf.sprintf "NO!! %s already there!"
1237                     (string_of_equality e)));
1238             (UriManager.UriSet.add u s, l)
1239           ) else (UriManager.UriSet.add u s, e::l))
1240        (UriManager.UriSet.empty, []) found)
1241   in
1242   uriset, eqlist, maxm
1243 ;;
1244
1245
1246 let find_library_theorems dbd env status equalities_uris =
1247   let module C = Cic in
1248   let module S = CicSubstitution in
1249   let module T = CicTypeChecker in
1250   let blacklist =
1251     let refl_equal =
1252       UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
1253     let s =
1254       UriManager.UriSet.remove refl_equal
1255         (UriManager.UriSet.union equalities_uris equations_blacklist)
1256     in
1257     List.fold_left
1258       (fun s u -> UriManager.UriSet.add u s)
1259       s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
1260          eq_ind_r_URI ()]
1261   in
1262   let metasenv, context, ugraph = env in
1263   let candidates =
1264     List.fold_left
1265       (fun l uri ->
1266          if UriManager.UriSet.mem uri blacklist then l
1267          else
1268            let t = CicUtil.term_of_uri uri in
1269            let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
1270            (uri, t, ty, [])::l)
1271       [] (MetadataQuery.signature_of_goal ~dbd status)
1272   in
1273   let refl_equal =
1274     let u = eq_XURI () in
1275     let t = CicUtil.term_of_uri u in
1276     let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
1277     (u, t, ty, [])
1278   in
1279   refl_equal::candidates
1280 ;;
1281
1282
1283 let find_context_hypotheses env equalities_indexes =
1284   let metasenv, context, ugraph = env in
1285   let _, res =
1286     List.fold_left
1287       (fun (n, l) entry ->
1288          match entry with
1289          | None -> (n+1, l)
1290          | Some _ ->
1291              if List.mem n equalities_indexes then
1292                (n+1, l)
1293              else
1294                let t = Cic.Rel n in
1295                let ty, _ =
1296                  CicTypeChecker.type_of_aux' metasenv context t ugraph in
1297                (n+1, (t, ty, [])::l))
1298       (1, []) context
1299   in
1300   res
1301 ;;
1302
1303
1304 let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
1305 (*   print_endline ("fix_metas " ^ (string_of_int newmeta)); *)
1306   let table = Hashtbl.create (List.length args) in
1307   let is_this_case = ref false in
1308   let newargs, newmeta =
1309     List.fold_right
1310       (fun t (newargs, index) ->
1311          match t with
1312          | Cic.Meta (i, l) ->
1313              if Hashtbl.mem table i then
1314                let idx = Hashtbl.find table i in
1315                ((Cic.Meta (idx, l))::newargs, index+1)
1316              else
1317                let _ = Hashtbl.add table i index in
1318                ((Cic.Meta (index, l))::newargs, index+1)
1319          | _ -> assert false)
1320       args ([], newmeta+1)
1321   in
1322   let repl where =
1323     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1324       ~where
1325   in
1326   let menv' =
1327     List.fold_right
1328       (fun (i, context, term) menv ->
1329          try
1330            let index = Hashtbl.find table i in
1331            (index, context, term)::menv
1332          with Not_found ->
1333            (i, context, term)::menv)
1334       menv []
1335   in
1336   let ty = repl ty
1337   and left = repl left
1338   and right = repl right in
1339   let metas = (metas_of_term left) @ (metas_of_term right) in
1340   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
1341   let newargs =
1342     List.filter
1343       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1344   in
1345   let _ =
1346     if List.length metas > 0 then
1347       let first = List.hd metas in
1348       Hashtbl.iter
1349         (fun k v ->
1350            if not (List.exists
1351                      (function Cic.Meta (i, _) -> i = v | _ -> assert false)
1352                      newargs) then
1353              Hashtbl.replace table k first)
1354         (Hashtbl.copy table)
1355   in
1356   let rec fix_proof = function
1357     | NoProof -> NoProof
1358     | BasicProof term -> BasicProof (repl term)
1359     | ProofBlock (subst, eq_URI, namety, bo(* t' *), (pos, eq), p) ->
1360
1361 (*         Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
1362 (*           (string_of_equality equality) (print_subst subst); *)
1363
1364 (*         debug_print "table is:"; *)
1365 (*         Hashtbl.iter *)
1366 (*           (fun k v -> debug_print (Printf.sprintf "%d: %d" k v)) *)
1367 (*           table; *)
1368         let subst' =
1369           List.fold_left
1370             (fun s arg ->
1371                match arg with
1372                | Cic.Meta (i, l) -> (
1373                    try
1374                      let j = Hashtbl.find table i in
1375                      if List.mem_assoc i subst then
1376                        s
1377                      else
1378                        let _, context, ty = CicUtil.lookup_meta i menv in
1379                        (i, (context, Cic.Meta (j, l), ty))::s
1380                    with Not_found | CicUtil.Meta_not_found _ ->
1381 (*                      debug_print ("Not_found meta ?" ^ (string_of_int i)); *)
1382                      s
1383                  )
1384                | _ -> assert false)
1385             [] args
1386         in
1387
1388 (*         Printf.printf "subst' is:\n%s\n" (print_subst subst'); *)
1389 (*         print_newline (); *)
1390
1391         ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
1392     | p -> assert false
1393   in
1394   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
1395   (newmeta + 1, neweq)
1396 ;;
1397
1398
1399 let term_is_equality term =
1400   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
1401   match term with
1402   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
1403   | _ -> false
1404 ;;
1405
1406
1407 exception TermIsNotAnEquality;;
1408
1409 let equality_of_term proof term =
1410   let eq_uri = LibraryObjects.eq_URI () in
1411   let iseq uri = UriManager.eq uri eq_uri in
1412   match term with
1413   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1414       let o = !Utils.compare_terms t1 t2 in
1415       let w = compute_equality_weight ty t1 t2 in
1416       let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
1417       e
1418 (*       (proof, (ty, t1, t2, o), [], []) *)
1419   | _ ->
1420       raise TermIsNotAnEquality
1421 ;;
1422
1423
1424 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1425
1426
1427 (*
1428 let superposition_left (metasenv, context, ugraph) target source =
1429   let module C = Cic in
1430   let module S = CicSubstitution in
1431   let module M = CicMetaSubst in
1432   let module HL = HelmLibraryObjects in
1433   let module CR = CicReduction in
1434   (* we assume that target is ground (does not contain metavariables): this
1435    * should always be the case (I hope, at least) *)
1436   let proof, (eq_ty, left, right, t_order), _, _ = target in
1437   let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
1438
1439   let compare_terms = !Utils.compare_terms in
1440
1441   if eq_ty <> ty then
1442     []
1443   else
1444     let where, is_left =
1445       match t_order (* compare_terms left right *) with
1446       | Lt -> right, false
1447       | Gt -> left, true
1448       | _ -> (
1449           Printf.printf "????????? %s = %s" (CicPp.ppterm left)
1450             (CicPp.ppterm right);
1451           print_newline ();
1452           assert false (* again, for ground terms this shouldn't happen... *)
1453         )
1454     in
1455     let metasenv' = newmetas @ metasenv in
1456     let result = s_order (* compare_terms t1 t2 *) in
1457     let res1, res2 =
1458       match result with
1459       | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
1460       | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
1461       | _ ->
1462           let res1 =
1463             List.filter
1464               (fun (t, s, m, ug) ->
1465                  compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
1466               (beta_expand t1 ty where context metasenv' ugraph)
1467           and res2 =
1468             List.filter
1469               (fun (t, s, m, ug) ->
1470                  compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
1471               (beta_expand t2 ty where context metasenv' ugraph)
1472           in
1473           res1, res2
1474     in
1475     (*   let what, other = *)
1476     (*     if is_left then left, right *)
1477     (*     else right, left *)
1478     (*   in *)
1479     let build_new what other eq_URI (t, s, m, ug) =
1480       let newgoal, newgoalproof =
1481         match t with
1482         | C.Lambda (nn, ty, bo) ->
1483             let bo' = S.subst (M.apply_subst s other) bo in
1484             let bo'' =
1485               C.Appl (
1486                 [C.MutInd (HL.Logic.eq_URI, 0, []);
1487                  S.lift 1 eq_ty] @
1488                   if is_left then [bo'; S.lift 1 right]
1489                   else [S.lift 1 left; bo'])
1490             in
1491             let t' = C.Lambda (nn, ty, bo'') in
1492             S.subst (M.apply_subst s other) bo,
1493             M.apply_subst s
1494               (C.Appl [C.Const (eq_URI, []); ty; what; t';
1495                        proof; other; eqproof])
1496         | _ -> assert false
1497       in
1498       let equation =
1499         if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
1500         else (eq_ty, left, newgoal, compare_terms left newgoal)
1501       in
1502       (newgoalproof (* eqproof *), equation, [], [])
1503     in
1504     let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
1505     and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
1506     new1 @ new2
1507 ;;
1508
1509
1510 let superposition_right newmeta (metasenv, context, ugraph) target source =
1511   let module C = Cic in
1512   let module S = CicSubstitution in
1513   let module M = CicMetaSubst in
1514   let module HL = HelmLibraryObjects in
1515   let module CR = CicReduction in
1516   let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
1517   let eqp', (ty', t1, t2, s_order), newm', args' = source in
1518   let maxmeta = ref newmeta in
1519
1520   let compare_terms = !Utils.compare_terms in
1521
1522   if eq_ty <> ty' then
1523     newmeta, []
1524   else
1525     (*   let ok term subst other other_eq_side ugraph = *)
1526     (*     match term with *)
1527     (*     | C.Lambda (nn, ty, bo) -> *)
1528     (*         let bo' = S.subst (M.apply_subst subst other) bo in *)
1529     (*         let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
1530     (*         not res *)
1531     (*     |  _ -> assert false *)
1532     (*   in *)
1533     let condition left right what other (t, s, m, ug) =
1534       let subst = M.apply_subst s in
1535       let cmp1 = compare_terms (subst what) (subst other) in
1536       let cmp2 = compare_terms (subst left) (subst right) in
1537       (*     cmp1 = Gt && cmp2 = Gt *)
1538       cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
1539         (*     && (ok t s other right ug) *)
1540     in
1541     let metasenv' = metasenv @ newmetas @ newm' in
1542     let beta_expand = beta_expand ~metas_ok:false in
1543     let cmp1 = t_order (* compare_terms left right *)
1544     and cmp2 = s_order (* compare_terms t1 t2 *) in
1545     let res1, res2, res3, res4 =
1546       let res l r s t =
1547         List.filter
1548           (condition l r s t)
1549           (beta_expand s eq_ty l context metasenv' ugraph)
1550       in
1551       match cmp1, cmp2 with
1552       | Gt, Gt ->
1553           (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
1554       | Gt, Lt ->
1555           [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
1556       | Lt, Gt ->
1557           [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
1558       | Lt, Lt ->
1559           [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
1560       | Gt, _ ->
1561           let res1 = res left right t1 t2
1562           and res2 = res left right t2 t1 in
1563           res1, res2, [], []
1564       | Lt, _ ->
1565           let res3 = res right left t1 t2
1566           and res4 = res right left t2 t1 in
1567           [], [], res3, res4
1568       | _, Gt ->
1569           let res1 = res left right t1 t2
1570           and res3 = res right left t1 t2 in
1571           res1, [], res3, []
1572       | _, Lt ->
1573           let res2 = res left right t2 t1
1574           and res4 = res right left t2 t1 in
1575           [], res2, [], res4
1576       | _, _ ->
1577           let res1 = res left right t1 t2
1578           and res2 = res left right t2 t1
1579           and res3 = res right left t1 t2
1580           and res4 = res right left t2 t1 in
1581           res1, res2, res3, res4
1582     in
1583     let newmetas = newmetas @ newm' in
1584     let newargs = args @ args' in
1585     let build_new what other is_left eq_URI (t, s, m, ug) =
1586       (*     let what, other = *)
1587       (*       if is_left then left, right *)
1588       (*       else right, left *)
1589       (*     in *)
1590       let newterm, neweqproof =
1591         match t with
1592         | C.Lambda (nn, ty, bo) ->
1593             let bo' = M.apply_subst s (S.subst other bo) in
1594             let bo'' =
1595               C.Appl (
1596                 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
1597                   if is_left then [bo'; S.lift 1 right]
1598                   else [S.lift 1 left; bo'])
1599             in
1600             let t' = C.Lambda (nn, ty, bo'') in
1601             bo',
1602             M.apply_subst s
1603               (C.Appl [C.Const (eq_URI, []); ty; what; t';
1604                        eqproof; other; eqp'])
1605         | _ -> assert false
1606       in
1607       let newmeta, newequality =
1608         let left, right =
1609           if is_left then (newterm, M.apply_subst s right)
1610           else (M.apply_subst s left, newterm) in
1611         let neworder = compare_terms left right in
1612         fix_metas !maxmeta
1613           (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
1614       in
1615       maxmeta := newmeta;
1616       newequality
1617     in
1618     let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
1619     and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
1620     and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
1621     and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
1622     let ok = function
1623       | _, (_, left, right, _), _, _ ->
1624           not (fst (CR.are_convertible context left right ugraph))
1625     in
1626     (!maxmeta,
1627      (List.filter ok (new1 @ new2 @ new3 @ new4)))
1628 ;;
1629 *)
1630
1631
1632 let is_identity ((_, context, ugraph) as env) = function
1633   | ((_, _, (ty, left, right, _), _, _) as equality) ->
1634       (left = right ||
1635           (meta_convertibility left right) ||
1636           (fst (CicReduction.are_convertible context left right ugraph)))
1637 ;;
1638
1639
1640 (*
1641 let demodulation newmeta (metasenv, context, ugraph) target source =
1642   let module C = Cic in
1643   let module S = CicSubstitution in
1644   let module M = CicMetaSubst in
1645   let module HL = HelmLibraryObjects in
1646   let module CR = CicReduction in
1647
1648   let proof, (eq_ty, left, right, t_order), metas, args = target
1649   and proof', (ty, t1, t2, s_order), metas', args' = source in
1650
1651   let compare_terms = !Utils.compare_terms in
1652
1653   if eq_ty <> ty then
1654     newmeta, target
1655   else
1656     let first_step, get_params =
1657       match s_order (* compare_terms t1 t2 *) with
1658       | Gt -> 1, (function
1659                     | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
1660                     | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
1661                     | _ -> assert false)
1662       | Lt -> 1, (function
1663                     | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1664                     | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1665                     | _ -> assert false)
1666       | _ ->
1667           let first_step = 3 in
1668           let get_params step =
1669             match step with
1670             | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
1671             | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
1672             | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1673             | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1674             | _ -> assert false
1675           in
1676           first_step, get_params
1677     in
1678     let rec demodulate newmeta step metasenv target =
1679       let proof, (eq_ty, left, right, t_order), metas, args = target in
1680       let is_left, what, other, eq_URI = get_params step in
1681
1682       let env = metasenv, context, ugraph in
1683       let names = names_of_context context in
1684 (*       Printf.printf *)
1685 (*         "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1686 (*         (string_of_equality ~env target) (CicPp.pp what names) *)
1687 (*         (CicPp.pp other names) (string_of_bool is_left); *)
1688 (*       Printf.printf "step: %d" step; *)
1689 (*       print_newline (); *)
1690
1691       let ok (t, s, m, ug) =
1692         compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
1693       in
1694       let res =
1695         let r = (beta_expand ~metas_ok:false ~match_only:true
1696                    what ty (if is_left then left else right)
1697                    context (metasenv @ metas) ugraph)
1698         in
1699 (*         let m' = metas_of_term what *)
1700 (*         and m'' = metas_of_term (if is_left then left else right) in *)
1701 (*         if (List.mem 527 m'') && (List.mem 6 m') then ( *)
1702 (*           Printf.printf *)
1703 (*             "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1704 (*             (string_of_equality ~env target) (CicPp.pp what names) *)
1705 (*             (CicPp.pp other names) (string_of_bool is_left); *)
1706 (*           Printf.printf "step: %d" step; *)
1707 (*           print_newline (); *)
1708 (*           print_endline "res:"; *)
1709 (*           List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
1710 (*           print_newline (); *)
1711 (*           Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
1712 (*           print_newline (); *)
1713 (*         ); *)
1714         List.filter ok r
1715       in
1716       match res with
1717       | [] ->
1718           if step = 0 then newmeta, target
1719           else demodulate newmeta (step-1) metasenv target
1720       | (t, s, m, ug)::_ ->
1721           let newterm, newproof =
1722             match t with
1723             | C.Lambda (nn, ty, bo) ->
1724 (*                 let bo' = M.apply_subst s (S.subst other bo) in *)
1725                 let bo' = S.subst (M.apply_subst s other) bo in
1726                 let bo'' =
1727                   C.Appl (
1728                     [C.MutInd (HL.Logic.eq_URI, 0, []);
1729                      S.lift 1 eq_ty] @
1730                       if is_left then [bo'; S.lift 1 right]
1731                       else [S.lift 1 left; bo'])
1732                 in
1733                 let t' = C.Lambda (nn, ty, bo'') in
1734 (*                 M.apply_subst s (S.subst other bo), *)
1735                 bo',
1736                 M.apply_subst s
1737                   (C.Appl [C.Const (eq_URI, []); ty; what; t';
1738                            proof; other; proof'])
1739             | _ -> assert false
1740           in
1741           let newmeta, newtarget =
1742             let left, right =
1743 (*               if is_left then (newterm, M.apply_subst s right) *)
1744 (*               else (M.apply_subst s left, newterm) in *)
1745               if is_left then newterm, right
1746               else left, newterm
1747             in
1748             let neworder = compare_terms left right in
1749 (*             let newmetasenv = metasenv @ metas in *)
1750 (*             let newargs = args @ args' in *)
1751 (*             fix_metas newmeta *)
1752 (*               (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
1753             let m = (metas_of_term left) @ (metas_of_term right) in
1754             let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
1755             and newargs =
1756               List.filter
1757                 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
1758                 args
1759             in
1760             newmeta,
1761             (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
1762           in
1763 (*           Printf.printf *)
1764 (*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
1765 (*             (string_of_equality ~env newtarget) *)
1766 (*             (string_of_equality ~env target); *)
1767 (* (\*           let _, _, newm, newa = newtarget in *\) *)
1768 (* (\*           Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
1769 (* (\*             (print_metasenv newm) *\) *)
1770 (* (\*             (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
1771 (*           print_newline (); *)
1772           if is_identity env newtarget then
1773             newmeta, newtarget
1774           else
1775             demodulate newmeta first_step metasenv newtarget
1776     in
1777     demodulate newmeta first_step (metasenv @ metas') target
1778 ;;
1779
1780
1781 (*
1782 let demodulation newmeta env target source =
1783   newmeta, target
1784 ;;
1785 *)
1786
1787
1788 let subsumption env target source =
1789   let _, (ty, tl, tr, _), tmetas, _ = target
1790   and _, (ty', sl, sr, _), smetas, _ = source in
1791   if ty <> ty' then
1792     false
1793   else
1794     let metasenv, context, ugraph = env in
1795     let metasenv = metasenv @ tmetas @ smetas in
1796     let names = names_of_context context in
1797     let samesubst subst subst' =
1798 (*       Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
1799 (*         (print_subst subst) (print_subst subst'); *)
1800 (*       print_newline (); *)
1801       let tbl = Hashtbl.create (List.length subst) in
1802       List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
1803       List.for_all
1804         (fun (m, (c, t1, t2)) ->
1805            try
1806              let c', t1', t2' = Hashtbl.find tbl m in
1807              if (c = c') && (t1 = t1') && (t2 = t2') then true
1808              else false
1809            with Not_found ->
1810              true)
1811         subst'
1812     in
1813     let subsaux left right left' right' =
1814       try
1815         let subst, menv, ug = matching metasenv context left left' ugraph
1816         and subst', menv', ug' = matching metasenv context right right' ugraph
1817         in
1818 (*         Printf.printf "left = right: %s = %s\n" *)
1819 (*           (CicPp.pp left names) (CicPp.pp right names); *)
1820 (*         Printf.printf "left' = right': %s = %s\n" *)
1821 (*           (CicPp.pp left' names) (CicPp.pp right' names);         *)
1822         samesubst subst subst'
1823       with e ->
1824 (*         print_endline (Printexc.to_string e); *)
1825         false
1826     in
1827     let res =
1828       if subsaux tl tr sl sr then true
1829       else subsaux tl tr sr sl
1830     in
1831     if res then (
1832       Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
1833         (string_of_equality ~env target) (string_of_equality ~env source);
1834       print_newline ();
1835     );
1836     res
1837 ;;
1838 *)
1839
1840
1841 let extract_differing_subterms t1 t2 =
1842   let module C = Cic in
1843   let rec aux t1 t2 =
1844     match t1, t2 with
1845     | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
1846         [(t1, t2)]
1847     | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
1848         let res = List.concat (List.map2 aux tl1 tl2) in
1849         if h1 <> h2 then
1850           if res = [] then [(h1, h2)] else [(t1, t2)]
1851         else
1852           if List.length res > 1 then [(t1, t2)] else res
1853     | t1, t2 ->
1854         if t1 <> t2 then [(t1, t2)] else []
1855   in
1856   let res = aux t1 t2 in
1857   match res with
1858   | hd::[] -> Some hd
1859   | _ -> None
1860 ;;
1861
1862
1863 let rec string_of_proof = function
1864   | NoProof -> "NoProof"
1865   | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
1866   | SubProof (t, i, p) ->
1867       Printf.sprintf "SubProof(%s, %s, %s)"
1868         (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
1869   | ProofSymBlock _ -> "ProofSymBlock"
1870   | ProofBlock _ -> "ProofBlock"
1871   | ProofGoalBlock (p1, p2) ->
1872       Printf.sprintf "ProofGoalBlock(%s, %s)"
1873         (string_of_proof p1) (string_of_proof p2)
1874 ;;