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         (* name, ty, eq_ty, left, right *)
  20         (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) *
  21         (Utils.pos * equality) * proof
  22   | ProofGoalBlock of proof * equality
  23   | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof
  24 ;;
  25
  26
  27 let string_of_equality ?env =
  28   match env with
  29   | None -> (
  30       function
  31         | w, _, (ty, left, right, o), _, _ ->
  32             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
  33               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
  34     )
  35   | Some (_, context, _) -> (
  36       let names = names_of_context context in
  37       function
  38         | w, _, (ty, left, right, o), _, _ ->
  39             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
  40               (CicPp.pp left names) (string_of_comparison o)
  41               (CicPp.pp right names)
  42     )
  43 ;;
  44
  45
  46 let build_proof_term equality =
  47 (*   Printf.printf "build_term_proof %s" (string_of_equality equality); *)
  48 (*   print_newline (); *)
  49
  50   let indent = ref 0 in
  51
  52   let rec do_build_proof proof =
  53     match proof with
  54     | NoProof ->
  55         Printf.fprintf stderr "WARNING: no proof!\n";
  56 (*           (string_of_equality equality); *)
  57         Cic.Implicit None
  58     | BasicProof term -> term
  59     | ProofGoalBlock (proofbit, equality) ->
  60         print_endline "found ProofGoalBlock, going up...";
  61         let _, proof, _, _, _ = equality in
  62         do_build_goal_proof proofbit proof
  63     | ProofSymBlock (ens, proof) ->
  64         let proof = do_build_proof proof in
  65         Cic.Appl [
  66           Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
  67           proof
  68         ]
  69     | ProofBlock (subst, eq_URI, t', (pos, eq), eqproof) ->
  70 (*         Printf.printf "\nsubst:\n%s\n" (print_subst subst); *)
  71 (*         print_newline (); *)
  72
  73         let name, ty, eq_ty, left, right = t' in
  74         let bo =
  75           Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
  76                     eq_ty; left; right]
  77         in
  78         let t' = Cic.Lambda (name, ty, (* CicSubstitution.lift 1 *) bo) in
  79         (*       Printf.printf "   ProofBlock: eq = %s, eq' = %s" *)
  80         (*         (string_of_equality eq) (string_of_equality eq'); *)
  81         (*       print_newline (); *)
  82
  83 (*         let s = String.make !indent ' ' in *)
  84 (*         incr indent; *)
  85
  86 (*         print_endline (s ^ "build proof'------------"); *)
  87
  88         let proof' =
  89           let _, proof', _, _, _ = eq in
  90           do_build_proof proof'
  91         in
  92 (*         print_endline (s ^ "END proof'"); *)
  93
  94 (*         print_endline (s ^ "build eqproof-----------"); *)
  95
  96         let eqproof = do_build_proof eqproof in
  97
  98 (*         print_endline (s ^ "END eqproof"); *)
  99 (*         decr indent; *)
 100
 101
 102         let _, _, (ty, what, other, _), menv', args' = eq in
 103         let what, other =
 104           if pos = Utils.Left then what, other else other, what
 105         in
 106         CicMetaSubst.apply_subst subst
 107           (Cic.Appl [Cic.Const (eq_URI, []); ty;
 108                      what; t'; eqproof; other; proof'])
 109
 110   and do_build_goal_proof proofbit proof =
 111 (*     match proofbit with *)
 112 (*     | BasicProof _ -> do_build_proof proof *)
 113 (*     | proofbit -> *)
 114         match proof with
 115         | ProofGoalBlock (pb, eq) ->
 116             do_build_proof (ProofGoalBlock (replace_proof proofbit pb, eq))
 117 (*             let _, proof, _, _, _  = eq in *)
 118 (*             let newproof = replace_proof proofbit proof in *)
 119 (*             do_build_proof newproof *)
 120
 121 (*         | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *)
 122 (*             let eqproof' = replace_proof proofbit eqproof in *)
 123 (*             do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *)
 124         | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
 125
 126   and replace_proof newproof = function
 127     | ProofBlock (subst, eq_URI, t', poseq, eqproof) ->
 128         let uri = eq_URI in
 129 (*           if eq_URI = HelmLibraryObjects.Logic.eq_ind_URI then *)
 130 (*             HelmLibraryObjects.Logic.eq_ind_r_URI *)
 131 (*           else *)
 132 (*             HelmLibraryObjects.Logic.eq_ind_URI *)
 133 (*         in *)
 134         let eqproof' = replace_proof newproof eqproof in
 135         ProofBlock (subst, uri(* eq_URI *), t', poseq, eqproof')
 136 (*         ProofBlock (subst, eq_URI, t', poseq, newproof) *)
 137     | ProofGoalBlock (pb, equality) ->
 138         let pb' = replace_proof newproof pb in
 139         ProofGoalBlock (pb', equality)
 140 (*         let w, proof, t, menv, args = equality in *)
 141 (*         let proof' = replace_proof newproof proof in *)
 142 (*         ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
 143     | BasicProof _ -> newproof
 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 (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
 484     | C.Meta (i, l), t -> (
 485         try
 486           let _, _, ty = CicUtil.lookup_meta i menv in
 487           let subst =
 488             if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
 489             else subst
 490           in
 491           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
 492           subst, menv
 493         with CicUtil.Meta_not_found m ->
 494           let names = names_of_context context in
 495           debug_print (lazy (
 496             Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
 497               (CicPp.pp t1 names) (CicPp.pp t2 names)
 498               (print_metasenv menv) (print_metasenv metasenv)));
 499           assert false
 500       )
 501     | _, C.Meta _ -> unif subst menv t s
 502     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
 503         raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
 504     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
 505         try
 506           List.fold_left2
 507             (fun (subst', menv) s t -> unif subst' menv s t)
 508             (subst, menv) tls tlt
 509         with Invalid_argument _ ->
 510           raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
 511       )
 512     | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
 513   in
 514   let subst, menv = unif [] metasenv t1 t2 in
 515   let menv =
 516     List.filter
 517       (fun (m, _, _) ->
 518          try let _ = List.find (fun (i, _) -> m = i) subst in false
 519          with Not_found -> true)
 520       menv
 521   in
 522   List.rev subst, menv, ugraph
 523 ;;
 524
 525
 526 let unification metasenv context t1 t2 ugraph =
 527 (*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
 528   let subst, menv, ug =
 529     if not (is_simple_term t1) || not (is_simple_term t2) then (
 530       debug_print (lazy (
 531         Printf.sprintf "NOT SIMPLE TERMS: %s %s"
 532           (CicPp.ppterm t1) (CicPp.ppterm t2)));
 533       CicUnification.fo_unif metasenv context t1 t2 ugraph
 534     ) else
 535       unification_simple metasenv context t1 t2 ugraph
 536   in
 537   let rec fix_term = function
 538     | (Cic.Meta (i, l) as t) ->
 539         let t' = lookup_subst t subst in
 540         if t <> t' then fix_term t' else t
 541     | Cic.Appl l -> Cic.Appl (List.map fix_term l)
 542     | t -> t
 543   in
 544   let rec fix_subst = function
 545     | [] -> []
 546     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
 547   in
 548 (*   Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
 549 (*   print_endline "|"; *)
 550   fix_subst subst, menv, ug
 551 ;;
 552
 553
 554 (* let unification = CicUnification.fo_unif;; *)
 555
 556 exception MatchingFailure;;
 557
 558
 559 let matching_simple metasenv context t1 t2 ugraph =
 560   let module C = Cic in
 561   let module M = CicMetaSubst in
 562   let module U = CicUnification in
 563   let lookup meta subst =
 564     match meta with
 565     | C.Meta (i, _) -> (
 566         try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 567         with Not_found -> meta
 568       )
 569     | _ -> assert false
 570   in
 571   let rec do_match subst menv s t =
 572 (*     Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
 573 (*       (print_subst subst); *)
 574 (*     print_newline (); *)
 575 (*     let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
 576 (*     let t = match t with C.Meta _ -> lookup t subst | _ -> t in  *)
 577     (*       Printf.printf "after apply_subst: %s %s\n%s" *)
 578     (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
 579     (*       print_newline (); *)
 580     match s, t with
 581     | s, t when s = t -> subst, menv
 582 (*     | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
 583 (*         do_match subst menv t s *)
 584 (*     | C.Meta _, t when occurs_check subst s t -> *)
 585 (*         raise MatchingFailure *)
 586 (*     | s, C.Meta _ when occurs_check subst t s -> *)
 587 (*         raise MatchingFailure *)
 588     | s, C.Meta (i, l) ->
 589         let filter_menv i menv =
 590           List.filter (fun (m, _, _) -> i <> m) menv
 591         in
 592         let subst, menv =
 593           let value = lookup t subst in
 594           match value with
 595 (*           | C.Meta (i', l') when Hashtbl.mem table i' -> *)
 596 (*               (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
 597           | value when value = t ->
 598               let _, _, ty = CicUtil.lookup_meta i menv in
 599               (i, (context, s, ty))::subst, filter_menv i menv
 600           | value when value <> s ->
 601               raise MatchingFailure
 602           | value -> do_match subst menv s value
 603         in
 604         subst, menv
 605 (*           else if value <> s then *)
 606 (*             raise MatchingFailure *)
 607 (*           else subst *)
 608 (*           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
 609 (*           else subst *)
 610 (*         in *)
 611 (*         let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
 612 (*         subst, menv *)
 613 (*     | _, C.Meta _ -> do_match subst menv t s *)
 614 (*     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
 615 (*         raise MatchingFailure *)
 616     | C.Appl ls, C.Appl lt -> (
 617         try
 618           List.fold_left2
 619             (fun (subst, menv) s t -> do_match subst menv s t)
 620             (subst, menv) ls lt
 621         with Invalid_argument _ ->
 622 (*           print_endline (Printexc.to_string e); *)
 623 (*           Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
 624 (*           print_newline ();           *)
 625           raise MatchingFailure
 626       )
 627     | _, _ ->
 628 (*         Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
 629 (*         print_newline (); *)
 630         raise MatchingFailure
 631   in
 632   let subst, menv = do_match [] metasenv t1 t2 in
 633   (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
 634   (*     print_newline (); *)
 635   subst, menv, ugraph
 636 ;;
 637
 638
 639 let matching metasenv context t1 t2 ugraph =
 640 (*   if (is_simple_term t1) && (is_simple_term t2) then *)
 641 (*     let subst, menv, ug = *)
 642 (*       matching_simple metasenv context t1 t2 ugraph in *)
 643 (* (\*     Printf.printf "matching %s %s:\n%s\n" *\) *)
 644 (* (\*       (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
 645 (* (\*     print_newline (); *\) *)
 646 (*     subst, menv, ug *)
 647 (*   else *)
 648 (*   Printf.printf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
 649 (*   print_newline (); *)
 650     try
 651       let subst, metasenv, ugraph =
 652         (*       CicUnification.fo_unif metasenv context t1 t2 ugraph *)
 653         unification metasenv context t1 t2 ugraph
 654       in
 655       let t' = CicMetaSubst.apply_subst subst t1 in
 656       if not (meta_convertibility t1 t') then
 657         raise MatchingFailure
 658       else
 659         let metas = metas_of_term t1 in
 660         let fix_subst = function
 661           | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
 662               (j, (c, Cic.Meta (i, lc), ty))
 663           | s -> s
 664         in
 665         let subst = List.map fix_subst subst in
 666
 667 (*         Printf.printf "matching %s %s:\n%s\n" *)
 668 (*           (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
 669 (*         print_newline (); *)
 670
 671         subst, metasenv, ugraph
 672     with
 673     | CicUnification.UnificationFailure _
 674     | CicUnification.Uncertain _ ->
 675 (*       Printf.printf "failed to match %s %s\n" *)
 676 (*         (CicPp.ppterm t1) (CicPp.ppterm t2); *)
 677 (*       print_endline (Printexc.to_string e); *)
 678       raise MatchingFailure
 679 ;;
 680
 681 (* let matching = *)
 682 (*   let profile = CicUtil.profile "Inference.matching" in *)
 683 (*   (fun metasenv context t1 t2 ugraph -> *)
 684 (*      profile (matching metasenv context t1 t2) ugraph) *)
 685 (* ;; *)
 686
 687
 688 let beta_expand ?(metas_ok=true) ?(match_only=false)
 689     what type_of_what where context metasenv ugraph =
 690   let module S = CicSubstitution in
 691   let module C = Cic in
 692
 693 (*   let _ = *)
 694 (*     let names = names_of_context context in *)
 695 (*     Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
 696 (*       (CicPp.pp what names) (CicPp.ppterm what) *)
 697 (*       (CicPp.pp where names) (CicPp.ppterm where); *)
 698 (*     print_newline (); *)
 699 (*   in *)
 700   (*
 701     return value:
 702     ((list of all possible beta expansions, subst, metasenv, ugraph),
 703      lifted term)
 704   *)
 705   let rec aux lift_amount term context metasenv subst ugraph =
 706 (*     Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
 707     let res, lifted_term =
 708       match term with
 709       | C.Rel m  ->
 710           [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 711
 712       | C.Var (uri, exp_named_subst) ->
 713           let ens', lifted_ens =
 714             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 715           in
 716           let expansions =
 717             List.map
 718               (fun (e, s, m, ug) ->
 719                  (C.Var (uri, e), s, m, ug)) ens'
 720           in
 721           expansions, C.Var (uri, lifted_ens)
 722
 723       | C.Meta (i, l) ->
 724           let l', lifted_l =
 725             List.fold_right
 726               (fun arg (res, lifted_tl) ->
 727                  match arg with
 728                  | Some arg ->
 729                      let arg_res, lifted_arg =
 730                        aux lift_amount arg context metasenv subst ugraph in
 731                      let l1 =
 732                        List.map
 733                          (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
 734                          arg_res
 735                      in
 736                      (l1 @
 737                         (List.map
 738                            (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
 739                            res),
 740                       (Some lifted_arg)::lifted_tl)
 741                  | None ->
 742                      (List.map
 743                         (fun (r, s, m, ug) -> None::r, s, m, ug)
 744                         res,
 745                       None::lifted_tl)
 746               ) l ([], [])
 747           in
 748           let e =
 749             List.map
 750               (fun (l, s, m, ug) ->
 751                  (C.Meta (i, l), s, m, ug)) l'
 752           in
 753           e, C.Meta (i, lifted_l)
 754
 755       | C.Sort _
 756       | C.Implicit _ as t -> [], t
 757
 758       | C.Cast (s, t) ->
 759           let l1, lifted_s =
 760             aux lift_amount s context metasenv subst ugraph in
 761           let l2, lifted_t =
 762             aux lift_amount t context metasenv subst ugraph
 763           in
 764           let l1' =
 765             List.map
 766               (fun (t, s, m, ug) ->
 767                  C.Cast (t, lifted_t), s, m, ug) l1 in
 768           let l2' =
 769             List.map
 770               (fun (t, s, m, ug) ->
 771                  C.Cast (lifted_s, t), s, m, ug) l2 in
 772           l1'@l2', C.Cast (lifted_s, lifted_t)
 773
 774       | C.Prod (nn, s, t) ->
 775           let l1, lifted_s =
 776             aux lift_amount s context metasenv subst ugraph in
 777           let l2, lifted_t =
 778             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
 779               metasenv subst ugraph
 780           in
 781           let l1' =
 782             List.map
 783               (fun (t, s, m, ug) ->
 784                  C.Prod (nn, t, lifted_t), s, m, ug) l1 in
 785           let l2' =
 786             List.map
 787               (fun (t, s, m, ug) ->
 788                  C.Prod (nn, lifted_s, t), s, m, ug) l2 in
 789           l1'@l2', C.Prod (nn, lifted_s, lifted_t)
 790
 791       | C.Lambda (nn, s, t) ->
 792           let l1, lifted_s =
 793             aux lift_amount s context metasenv subst ugraph in
 794           let l2, lifted_t =
 795             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
 796               metasenv subst ugraph
 797           in
 798           let l1' =
 799             List.map
 800               (fun (t, s, m, ug) ->
 801                  C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
 802           let l2' =
 803             List.map
 804               (fun (t, s, m, ug) ->
 805                  C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
 806           l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
 807
 808       | C.LetIn (nn, s, t) ->
 809           let l1, lifted_s =
 810             aux lift_amount s context metasenv subst ugraph in
 811           let l2, lifted_t =
 812             aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
 813               metasenv subst ugraph
 814           in
 815           let l1' =
 816             List.map
 817               (fun (t, s, m, ug) ->
 818                  C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
 819           let l2' =
 820             List.map
 821               (fun (t, s, m, ug) ->
 822                  C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
 823           l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
 824
 825       | C.Appl l ->
 826           let l', lifted_l =
 827             aux_list lift_amount l context metasenv subst ugraph
 828           in
 829           (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
 830            C.Appl lifted_l)
 831
 832       | C.Const (uri, exp_named_subst) ->
 833           let ens', lifted_ens =
 834             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 835           in
 836           let expansions =
 837             List.map
 838               (fun (e, s, m, ug) ->
 839                  (C.Const (uri, e), s, m, ug)) ens'
 840           in
 841           (expansions, C.Const (uri, lifted_ens))
 842
 843       | C.MutInd (uri, i ,exp_named_subst) ->
 844           let ens', lifted_ens =
 845             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 846           in
 847           let expansions =
 848             List.map
 849               (fun (e, s, m, ug) ->
 850                  (C.MutInd (uri, i, e), s, m, ug)) ens'
 851           in
 852           (expansions, C.MutInd (uri, i, lifted_ens))
 853
 854       | C.MutConstruct (uri, i, j, exp_named_subst) ->
 855           let ens', lifted_ens =
 856             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 857           in
 858           let expansions =
 859             List.map
 860               (fun (e, s, m, ug) ->
 861                  (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
 862           in
 863           (expansions, C.MutConstruct (uri, i, j, lifted_ens))
 864
 865       | C.MutCase (sp, i, outt, t, pl) ->
 866           let pl_res, lifted_pl =
 867             aux_list lift_amount pl context metasenv subst ugraph
 868           in
 869           let l1, lifted_outt =
 870             aux lift_amount outt context metasenv subst ugraph in
 871           let l2, lifted_t =
 872             aux lift_amount t context metasenv subst ugraph in
 873
 874           let l1' =
 875             List.map
 876               (fun (outt, s, m, ug) ->
 877                  C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
 878           let l2' =
 879             List.map
 880               (fun (t, s, m, ug) ->
 881                  C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
 882           let l3' =
 883             List.map
 884               (fun (pl, s, m, ug) ->
 885                  C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
 886           in
 887           (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
 888
 889       | C.Fix (i, fl) ->
 890           let len = List.length fl in
 891           let fl', lifted_fl =
 892             List.fold_right
 893               (fun (nm, idx, ty, bo) (res, lifted_tl) ->
 894                  let lifted_ty = S.lift lift_amount ty in
 895                  let bo_res, lifted_bo =
 896                    aux (lift_amount+len) bo context metasenv subst ugraph in
 897                  let l1 =
 898                    List.map
 899                      (fun (a, s, m, ug) ->
 900                         (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
 901                      bo_res
 902                  in
 903                  (l1 @
 904                     (List.map
 905                        (fun (r, s, m, ug) ->
 906                           (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
 907                   (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
 908               ) fl ([], [])
 909           in
 910           (List.map
 911              (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
 912            C.Fix (i, lifted_fl))
 913
 914       | C.CoFix (i, fl) ->
 915           let len = List.length fl in
 916           let fl', lifted_fl =
 917             List.fold_right
 918               (fun (nm, ty, bo) (res, lifted_tl) ->
 919                  let lifted_ty = S.lift lift_amount ty in
 920                  let bo_res, lifted_bo =
 921                    aux (lift_amount+len) bo context metasenv subst ugraph in
 922                  let l1 =
 923                    List.map
 924                      (fun (a, s, m, ug) ->
 925                         (nm, lifted_ty, a)::lifted_tl, s, m, ug)
 926                      bo_res
 927                  in
 928                  (l1 @
 929                     (List.map
 930                        (fun (r, s, m, ug) ->
 931                           (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
 932                   (nm, lifted_ty, lifted_bo)::lifted_tl)
 933               ) fl ([], [])
 934           in
 935           (List.map
 936              (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
 937            C.CoFix (i, lifted_fl))
 938     in
 939     let retval =
 940       match term with
 941       | C.Meta _ when (not metas_ok) ->
 942           res, lifted_term
 943       | _ ->
 944 (*           let term' = *)
 945 (*             if match_only then replace_metas context term *)
 946 (*             else term *)
 947 (*           in *)
 948           try
 949             let subst', metasenv', ugraph' =
 950 (*               Printf.printf "provo a unificare %s e %s\n" *)
 951 (*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
 952               if match_only then
 953                 matching metasenv context term (S.lift lift_amount what) ugraph
 954               else
 955                 CicUnification.fo_unif metasenv context
 956                   (S.lift lift_amount what) term ugraph
 957             in
 958 (*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
 959 (*             (CicPp.ppterm (S.lift lift_amount what)); *)
 960 (*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
 961 (*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
 962             (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
 963 (*             if match_only then *)
 964 (*               let t' = CicMetaSubst.apply_subst subst' term in *)
 965 (*               if not (meta_convertibility term t') then ( *)
 966 (*                 res, lifted_term *)
 967 (*               ) else ( *)
 968 (*                 let metas = metas_of_term term in *)
 969 (*                 let fix_subst = function *)
 970 (*                   | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
 971 (*                       (j, (c, C.Meta (i, lc), ty)) *)
 972 (*                   | s -> s *)
 973 (*                 in *)
 974 (*                 let subst' = List.map fix_subst subst' in *)
 975 (*                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
 976 (*                  lifted_term) *)
 977 (*               ) *)
 978 (*             else *)
 979               ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
 980                lifted_term)
 981           with
 982           | MatchingFailure
 983           | CicUnification.UnificationFailure _
 984           | CicUnification.Uncertain _ ->
 985               res, lifted_term
 986     in
 987 (*     Printf.printf "exit aux\n"; *)
 988     retval
 989
 990   and aux_list lift_amount l context metasenv subst ugraph =
 991     List.fold_right
 992       (fun arg (res, lifted_tl) ->
 993          let arg_res, lifted_arg =
 994            aux lift_amount arg context metasenv subst ugraph in
 995          let l1 = List.map
 996            (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
 997          in
 998          (l1 @ (List.map
 999                   (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
1000           lifted_arg::lifted_tl)
1001       ) l ([], [])
1002
1003   and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
1004     List.fold_right
1005       (fun (u, arg) (res, lifted_tl) ->
1006          let arg_res, lifted_arg =
1007            aux lift_amount arg context metasenv subst ugraph in
1008          let l1 =
1009            List.map
1010              (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
1011          in
1012          (l1 @ (List.map (fun (r, s, m, ug) ->
1013                             (u, lifted_arg)::r, s, m, ug) res),
1014           (u, lifted_arg)::lifted_tl)
1015       ) exp_named_subst ([], [])
1016
1017   in
1018   let expansions, _ =
1019 (*     let where = *)
1020 (*       if match_only then replace_metas (\* context *\) where *)
1021 (*       else where *)
1022 (*     in *)
1023     aux 0 where context metasenv [] ugraph
1024   in
1025   let mapfun =
1026 (*     if match_only then *)
1027 (*       (fun (term, subst, metasenv, ugraph) -> *)
1028 (*          let term' = *)
1029 (*            C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
1030 (*          and subst = restore_subst subst in *)
1031 (*          (term', subst, metasenv, ugraph)) *)
1032 (*     else *)
1033       (fun (term, subst, metasenv, ugraph) ->
1034          let term' = C.Lambda (C.Anonymous, type_of_what, term) in
1035          (term', subst, metasenv, ugraph))
1036   in
1037   List.map mapfun expansions
1038 ;;
1039
1040
1041 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
1042   let module C = Cic in
1043   let module S = CicSubstitution in
1044   let module T = CicTypeChecker in
1045   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
1046   let ok_types ty menv =
1047     List.for_all (fun (_, _, mt) -> mt = ty) menv
1048   in
1049   let rec aux index newmeta = function
1050     | [] -> [], newmeta
1051     | (Some (_, C.Decl (term)))::tl ->
1052         let do_find context term =
1053           match term with
1054           | C.Prod (name, s, t) ->
1055 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
1056               let (head, newmetas, args, newmeta) =
1057                 ProofEngineHelpers.saturate_term newmeta []
1058                   context (S.lift index term) 0
1059               in
1060               let p =
1061                 if List.length args = 0 then
1062                   C.Rel index
1063                 else
1064                   C.Appl ((C.Rel index)::args)
1065               in (
1066                 match head with
1067                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
1068                     when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
1069                     debug_print (lazy (
1070                       Printf.sprintf "OK: %s" (CicPp.ppterm term)));
1071 (*                     debug_print (lazy ( *)
1072 (*                       Printf.sprintf "args: %s\n" *)
1073 (*                         (String.concat ", " (List.map CicPp.ppterm args)))); *)
1074 (*                     debug_print (lazy ( *)
1075 (*                       Printf.sprintf "newmetas:\n%s\n" *)
1076 (*                         (print_metasenv newmetas))); *)
1077                     let o = !Utils.compare_terms t1 t2 in
1078                     let w = compute_equality_weight ty t1 t2 in
1079                     let proof = BasicProof p in
1080                     let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
1081                     Some e, (newmeta+1)
1082                 | _ -> None, newmeta
1083               )
1084           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
1085               when UriManager.eq uri eq_uri ->
1086               let t1 = S.lift index t1
1087               and t2 = S.lift index t2 in
1088               let o = !Utils.compare_terms t1 t2 in
1089               let w = compute_equality_weight ty t1 t2 in
1090               let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
1091               Some e, (newmeta+1)
1092           | _ -> None, newmeta
1093         in (
1094           match do_find context term with
1095           | Some p, newmeta ->
1096               let tl, newmeta' = (aux (index+1) newmeta tl) in
1097               p::tl, max newmeta newmeta'
1098           | None, _ ->
1099               aux (index+1) newmeta tl
1100         )
1101     | _::tl ->
1102         aux (index+1) newmeta tl
1103   in
1104   aux 1 newmeta context
1105 ;;
1106
1107
1108 let equations_blacklist =
1109   List.fold_left
1110     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
1111     UriManager.UriSet.empty [
1112       "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
1113       "cic:/Coq/Init/Logic/trans_eq.con";
1114       "cic:/Coq/Init/Logic/f_equal.con";
1115       "cic:/Coq/Init/Logic/f_equal2.con";
1116       "cic:/Coq/Init/Logic/f_equal3.con";
1117       "cic:/Coq/Init/Logic/sym_eq.con";
1118 (*       "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
1119 (*       "cic:/Coq/Init/Peano/mult_n_Sm.con"; *)
1120
1121       (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
1122          perche' questo cacchio di teorema rompe le scatole :'( *)
1123       "cic:/Rocq/SUBST/comparith/mult_n_2.con";
1124     ]
1125 ;;
1126
1127 let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
1128   let module C = Cic in
1129   let module S = CicSubstitution in
1130   let module T = CicTypeChecker in
1131   let candidates =
1132     List.fold_left
1133       (fun l uri ->
1134         let suri = UriManager.string_of_uri uri in
1135          if UriManager.UriSet.mem uri equations_blacklist then
1136            l
1137          else
1138            let t = CicUtil.term_of_uri uri in
1139            let ty, _ =
1140              CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
1141            in
1142            (t, ty)::l)
1143       []
1144       (MetadataQuery.equations_for_goal ~dbd status)
1145   in
1146   let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI
1147   and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in
1148   let iseq uri =
1149     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
1150   in
1151   let ok_types ty menv =
1152     List.for_all (fun (_, _, mt) -> mt = ty) menv
1153   in
1154   let rec aux newmeta = function
1155     | [] -> [], newmeta
1156     | (term, termty)::tl ->
1157         debug_print (lazy (
1158           Printf.sprintf "Examining: %s (%s)"
1159             (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty)));
1160         let res, newmeta =
1161           match termty with
1162           | C.Prod (name, s, t) ->
1163               let head, newmetas, args, newmeta =
1164                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
1165               in
1166               let p =
1167                 if List.length args = 0 then
1168                   term
1169                 else
1170                   C.Appl (term::args)
1171               in (
1172                 match head with
1173                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
1174                     when (iseq uri) && (ok_types ty newmetas) ->
1175                     debug_print (lazy (
1176                       Printf.sprintf "OK: %s" (CicPp.ppterm term)));
1177                     let o = !Utils.compare_terms t1 t2 in
1178                     let w = compute_equality_weight ty t1 t2 in
1179                     let proof = BasicProof p in
1180                     let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
1181                     Some e, (newmeta+1)
1182                 | _ -> None, newmeta
1183               )
1184           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1185               let o = !Utils.compare_terms t1 t2 in
1186               let w = compute_equality_weight ty t1 t2 in
1187               let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
1188               Some e, (newmeta+1)
1189           | _ -> None, newmeta
1190         in
1191         match res with
1192         | Some e ->
1193             let tl, newmeta' = aux newmeta tl in
1194             e::tl, max newmeta newmeta'
1195         | None ->
1196             aux newmeta tl
1197   in
1198   let found, maxm = aux maxmeta candidates in
1199   (List.fold_left
1200      (fun l e ->
1201         if List.exists (meta_convertibility_eq e) l then (
1202           debug_print (lazy (
1203             Printf.sprintf "NO!! %s already there!" (string_of_equality e)));
1204           l
1205         )
1206         else e::l)
1207      [] found), maxm
1208 ;;
1209
1210
1211 let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
1212 (*   print_endline ("fix_metas " ^ (string_of_int newmeta)); *)
1213   let table = Hashtbl.create (List.length args) in
1214   let is_this_case = ref false in
1215   let newargs, newmeta =
1216     List.fold_right
1217       (fun t (newargs, index) ->
1218          match t with
1219          | Cic.Meta (i, l) ->
1220              Hashtbl.add table i index;
1221 (*              if index = 5469 then ( *)
1222 (*                Printf.printf "?5469 COMES FROM (%d): %s\n" *)
1223 (*                  i (string_of_equality equality); *)
1224 (*                print_newline (); *)
1225 (*                is_this_case := true *)
1226 (*              ); *)
1227              ((Cic.Meta (index, l))::newargs, index+1)
1228          | _ -> assert false)
1229       args ([], newmeta+1)
1230   in
1231   let repl where =
1232     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1233       ~where
1234   in
1235   let menv' =
1236     List.fold_right
1237       (fun (i, context, term) menv ->
1238          try
1239            let index = Hashtbl.find table i in
1240            (index, context, term)::menv
1241          with Not_found ->
1242            (i, context, term)::menv)
1243       menv []
1244   in
1245   let ty = repl ty
1246   and left = repl left
1247   and right = repl right in
1248   let metas = (metas_of_term left) @ (metas_of_term right) in
1249   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
1250   and newargs =
1251     List.filter
1252       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1253   in
1254   let rec fix_proof = function
1255     | NoProof -> NoProof
1256     | BasicProof term -> BasicProof (repl term)
1257     | ProofBlock (subst, eq_URI, t', (pos, eq), p) ->
1258
1259 (*         Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
1260 (*           (string_of_equality equality) (print_subst subst); *)
1261
1262         let subst' =
1263           List.fold_left
1264             (fun s arg ->
1265                match arg with
1266                | Cic.Meta (i, l) -> (
1267                    try
1268                      let j = Hashtbl.find table i in
1269                      if List.mem_assoc i subst then
1270                        s
1271                      else
1272 (*                        let _, context, ty = CicUtil.lookup_meta j menv' in *)
1273 (*                        (i, (context, Cic.Meta (j, l), ty))::s *)
1274                        let _, context, ty = CicUtil.lookup_meta i menv in
1275                        (i, (context, Cic.Meta (j, l), ty))::s
1276                    with Not_found -> s
1277                  )
1278                | _ -> assert false)
1279             [] args
1280         in
1281 (*         let subst'' = *)
1282 (*           List.map *)
1283 (*             (fun (i, e) -> *)
1284 (*                try let j = Hashtbl.find table i in (j, e) *)
1285 (*                with _ -> (i, e)) subst *)
1286 (*         in *)
1287
1288 (*         Printf.printf "subst' is:\n%s\n" (print_subst subst'); *)
1289 (*         print_newline (); *)
1290
1291         ProofBlock (subst' @ subst, eq_URI, t', (pos, eq), p)
1292 (*     | ProofSymBlock (ens, p) -> *)
1293 (*         let ens' = List.map (fun (u, t) -> (u, repl t)) ens in *)
1294 (*         ProofSymBlock (ens', fix_proof p) *)
1295     | p -> assert false
1296   in
1297 (*   (newmeta + (List.length newargs) + 2, *)
1298   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
1299 (*   if !is_this_case then ( *)
1300 (*     print_endline "\nTHIS IS THE TROUBLE!!!"; *)
1301 (*     let pt = build_proof_term neweq in *)
1302 (*     Printf.printf "equality: %s\nproof: %s\n" *)
1303 (*       (string_of_equality neweq) (CicPp.ppterm pt); *)
1304 (*     print_endline (String.make 79 '-'); *)
1305 (*   ); *)
1306   (newmeta + 1, neweq)
1307 (*    (w, fix_proof p, (ty, left, right, o), menv', newargs)) *)
1308 ;;
1309
1310
1311 let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term =
1312   let iseq uri = UriManager.eq uri eq_uri in
1313   match term with
1314   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
1315   | _ -> false
1316 ;;
1317
1318
1319 exception TermIsNotAnEquality;;
1320
1321 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term =
1322   let iseq uri = UriManager.eq uri eq_uri in
1323   match term with
1324   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1325       let o = !Utils.compare_terms t1 t2 in
1326       let w = compute_equality_weight ty t1 t2 in
1327       let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
1328       e
1329 (*       (proof, (ty, t1, t2, o), [], []) *)
1330   | _ ->
1331       raise TermIsNotAnEquality
1332 ;;
1333
1334
1335 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1336
1337
1338 (*
1339 let superposition_left (metasenv, context, ugraph) target source =
1340   let module C = Cic in
1341   let module S = CicSubstitution in
1342   let module M = CicMetaSubst in
1343   let module HL = HelmLibraryObjects in
1344   let module CR = CicReduction in
1345   (* we assume that target is ground (does not contain metavariables): this
1346    * should always be the case (I hope, at least) *)
1347   let proof, (eq_ty, left, right, t_order), _, _ = target in
1348   let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
1349
1350   let compare_terms = !Utils.compare_terms in
1351
1352   if eq_ty <> ty then
1353     []
1354   else
1355     let where, is_left =
1356       match t_order (* compare_terms left right *) with
1357       | Lt -> right, false
1358       | Gt -> left, true
1359       | _ -> (
1360           Printf.printf "????????? %s = %s" (CicPp.ppterm left)
1361             (CicPp.ppterm right);
1362           print_newline ();
1363           assert false (* again, for ground terms this shouldn't happen... *)
1364         )
1365     in
1366     let metasenv' = newmetas @ metasenv in
1367     let result = s_order (* compare_terms t1 t2 *) in
1368     let res1, res2 =
1369       match result with
1370       | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
1371       | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
1372       | _ ->
1373           let res1 =
1374             List.filter
1375               (fun (t, s, m, ug) ->
1376                  compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
1377               (beta_expand t1 ty where context metasenv' ugraph)
1378           and res2 =
1379             List.filter
1380               (fun (t, s, m, ug) ->
1381                  compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
1382               (beta_expand t2 ty where context metasenv' ugraph)
1383           in
1384           res1, res2
1385     in
1386     (*   let what, other = *)
1387     (*     if is_left then left, right *)
1388     (*     else right, left *)
1389     (*   in *)
1390     let build_new what other eq_URI (t, s, m, ug) =
1391       let newgoal, newgoalproof =
1392         match t with
1393         | C.Lambda (nn, ty, bo) ->
1394             let bo' = S.subst (M.apply_subst s other) bo in
1395             let bo'' =
1396               C.Appl (
1397                 [C.MutInd (HL.Logic.eq_URI, 0, []);
1398                  S.lift 1 eq_ty] @
1399                   if is_left then [bo'; S.lift 1 right]
1400                   else [S.lift 1 left; bo'])
1401             in
1402             let t' = C.Lambda (nn, ty, bo'') in
1403             S.subst (M.apply_subst s other) bo,
1404             M.apply_subst s
1405               (C.Appl [C.Const (eq_URI, []); ty; what; t';
1406                        proof; other; eqproof])
1407         | _ -> assert false
1408       in
1409       let equation =
1410         if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
1411         else (eq_ty, left, newgoal, compare_terms left newgoal)
1412       in
1413       (newgoalproof (* eqproof *), equation, [], [])
1414     in
1415     let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
1416     and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
1417     new1 @ new2
1418 ;;
1419
1420
1421 let superposition_right newmeta (metasenv, context, ugraph) target source =
1422   let module C = Cic in
1423   let module S = CicSubstitution in
1424   let module M = CicMetaSubst in
1425   let module HL = HelmLibraryObjects in
1426   let module CR = CicReduction in
1427   let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
1428   let eqp', (ty', t1, t2, s_order), newm', args' = source in
1429   let maxmeta = ref newmeta in
1430
1431   let compare_terms = !Utils.compare_terms in
1432
1433   if eq_ty <> ty' then
1434     newmeta, []
1435   else
1436     (*   let ok term subst other other_eq_side ugraph = *)
1437     (*     match term with *)
1438     (*     | C.Lambda (nn, ty, bo) -> *)
1439     (*         let bo' = S.subst (M.apply_subst subst other) bo in *)
1440     (*         let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
1441     (*         not res *)
1442     (*     |  _ -> assert false *)
1443     (*   in *)
1444     let condition left right what other (t, s, m, ug) =
1445       let subst = M.apply_subst s in
1446       let cmp1 = compare_terms (subst what) (subst other) in
1447       let cmp2 = compare_terms (subst left) (subst right) in
1448       (*     cmp1 = Gt && cmp2 = Gt *)
1449       cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
1450         (*     && (ok t s other right ug) *)
1451     in
1452     let metasenv' = metasenv @ newmetas @ newm' in
1453     let beta_expand = beta_expand ~metas_ok:false in
1454     let cmp1 = t_order (* compare_terms left right *)
1455     and cmp2 = s_order (* compare_terms t1 t2 *) in
1456     let res1, res2, res3, res4 =
1457       let res l r s t =
1458         List.filter
1459           (condition l r s t)
1460           (beta_expand s eq_ty l context metasenv' ugraph)
1461       in
1462       match cmp1, cmp2 with
1463       | Gt, Gt ->
1464           (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
1465       | Gt, Lt ->
1466           [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
1467       | Lt, Gt ->
1468           [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
1469       | Lt, Lt ->
1470           [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
1471       | Gt, _ ->
1472           let res1 = res left right t1 t2
1473           and res2 = res left right t2 t1 in
1474           res1, res2, [], []
1475       | Lt, _ ->
1476           let res3 = res right left t1 t2
1477           and res4 = res right left t2 t1 in
1478           [], [], res3, res4
1479       | _, Gt ->
1480           let res1 = res left right t1 t2
1481           and res3 = res right left t1 t2 in
1482           res1, [], res3, []
1483       | _, Lt ->
1484           let res2 = res left right t2 t1
1485           and res4 = res right left t2 t1 in
1486           [], res2, [], res4
1487       | _, _ ->
1488           let res1 = res left right t1 t2
1489           and res2 = res left right t2 t1
1490           and res3 = res right left t1 t2
1491           and res4 = res right left t2 t1 in
1492           res1, res2, res3, res4
1493     in
1494     let newmetas = newmetas @ newm' in
1495     let newargs = args @ args' in
1496     let build_new what other is_left eq_URI (t, s, m, ug) =
1497       (*     let what, other = *)
1498       (*       if is_left then left, right *)
1499       (*       else right, left *)
1500       (*     in *)
1501       let newterm, neweqproof =
1502         match t with
1503         | C.Lambda (nn, ty, bo) ->
1504             let bo' = M.apply_subst s (S.subst other bo) in
1505             let bo'' =
1506               C.Appl (
1507                 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
1508                   if is_left then [bo'; S.lift 1 right]
1509                   else [S.lift 1 left; bo'])
1510             in
1511             let t' = C.Lambda (nn, ty, bo'') in
1512             bo',
1513             M.apply_subst s
1514               (C.Appl [C.Const (eq_URI, []); ty; what; t';
1515                        eqproof; other; eqp'])
1516         | _ -> assert false
1517       in
1518       let newmeta, newequality =
1519         let left, right =
1520           if is_left then (newterm, M.apply_subst s right)
1521           else (M.apply_subst s left, newterm) in
1522         let neworder = compare_terms left right in
1523         fix_metas !maxmeta
1524           (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
1525       in
1526       maxmeta := newmeta;
1527       newequality
1528     in
1529     let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
1530     and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
1531     and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
1532     and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
1533     let ok = function
1534       | _, (_, left, right, _), _, _ ->
1535           not (fst (CR.are_convertible context left right ugraph))
1536     in
1537     (!maxmeta,
1538      (List.filter ok (new1 @ new2 @ new3 @ new4)))
1539 ;;
1540 *)
1541
1542
1543 let is_identity ((_, context, ugraph) as env) = function
1544   | ((_, _, (ty, left, right, _), _, _) as equality) ->
1545       (left = right ||
1546           (fst (CicReduction.are_convertible context left right ugraph)))
1547 ;;
1548
1549
1550 (*
1551 let demodulation newmeta (metasenv, context, ugraph) target source =
1552   let module C = Cic in
1553   let module S = CicSubstitution in
1554   let module M = CicMetaSubst in
1555   let module HL = HelmLibraryObjects in
1556   let module CR = CicReduction in
1557
1558   let proof, (eq_ty, left, right, t_order), metas, args = target
1559   and proof', (ty, t1, t2, s_order), metas', args' = source in
1560
1561   let compare_terms = !Utils.compare_terms in
1562
1563   if eq_ty <> ty then
1564     newmeta, target
1565   else
1566     let first_step, get_params =
1567       match s_order (* compare_terms t1 t2 *) with
1568       | Gt -> 1, (function
1569                     | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
1570                     | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
1571                     | _ -> assert false)
1572       | Lt -> 1, (function
1573                     | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1574                     | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1575                     | _ -> assert false)
1576       | _ ->
1577           let first_step = 3 in
1578           let get_params step =
1579             match step with
1580             | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
1581             | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
1582             | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1583             | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1584             | _ -> assert false
1585           in
1586           first_step, get_params
1587     in
1588     let rec demodulate newmeta step metasenv target =
1589       let proof, (eq_ty, left, right, t_order), metas, args = target in
1590       let is_left, what, other, eq_URI = get_params step in
1591
1592       let env = metasenv, context, ugraph in
1593       let names = names_of_context context in
1594 (*       Printf.printf *)
1595 (*         "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1596 (*         (string_of_equality ~env target) (CicPp.pp what names) *)
1597 (*         (CicPp.pp other names) (string_of_bool is_left); *)
1598 (*       Printf.printf "step: %d" step; *)
1599 (*       print_newline (); *)
1600
1601       let ok (t, s, m, ug) =
1602         compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
1603       in
1604       let res =
1605         let r = (beta_expand ~metas_ok:false ~match_only:true
1606                    what ty (if is_left then left else right)
1607                    context (metasenv @ metas) ugraph)
1608         in
1609 (*         let m' = metas_of_term what *)
1610 (*         and m'' = metas_of_term (if is_left then left else right) in *)
1611 (*         if (List.mem 527 m'') && (List.mem 6 m') then ( *)
1612 (*           Printf.printf *)
1613 (*             "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1614 (*             (string_of_equality ~env target) (CicPp.pp what names) *)
1615 (*             (CicPp.pp other names) (string_of_bool is_left); *)
1616 (*           Printf.printf "step: %d" step; *)
1617 (*           print_newline (); *)
1618 (*           print_endline "res:"; *)
1619 (*           List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
1620 (*           print_newline (); *)
1621 (*           Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
1622 (*           print_newline (); *)
1623 (*         ); *)
1624         List.filter ok r
1625       in
1626       match res with
1627       | [] ->
1628           if step = 0 then newmeta, target
1629           else demodulate newmeta (step-1) metasenv target
1630       | (t, s, m, ug)::_ ->
1631           let newterm, newproof =
1632             match t with
1633             | C.Lambda (nn, ty, bo) ->
1634 (*                 let bo' = M.apply_subst s (S.subst other bo) in *)
1635                 let bo' = S.subst (M.apply_subst s other) bo in
1636                 let bo'' =
1637                   C.Appl (
1638                     [C.MutInd (HL.Logic.eq_URI, 0, []);
1639                      S.lift 1 eq_ty] @
1640                       if is_left then [bo'; S.lift 1 right]
1641                       else [S.lift 1 left; bo'])
1642                 in
1643                 let t' = C.Lambda (nn, ty, bo'') in
1644 (*                 M.apply_subst s (S.subst other bo), *)
1645                 bo',
1646                 M.apply_subst s
1647                   (C.Appl [C.Const (eq_URI, []); ty; what; t';
1648                            proof; other; proof'])
1649             | _ -> assert false
1650           in
1651           let newmeta, newtarget =
1652             let left, right =
1653 (*               if is_left then (newterm, M.apply_subst s right) *)
1654 (*               else (M.apply_subst s left, newterm) in *)
1655               if is_left then newterm, right
1656               else left, newterm
1657             in
1658             let neworder = compare_terms left right in
1659 (*             let newmetasenv = metasenv @ metas in *)
1660 (*             let newargs = args @ args' in *)
1661 (*             fix_metas newmeta *)
1662 (*               (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
1663             let m = (metas_of_term left) @ (metas_of_term right) in
1664             let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
1665             and newargs =
1666               List.filter
1667                 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
1668                 args
1669             in
1670             newmeta,
1671             (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
1672           in
1673 (*           Printf.printf *)
1674 (*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
1675 (*             (string_of_equality ~env newtarget) *)
1676 (*             (string_of_equality ~env target); *)
1677 (* (\*           let _, _, newm, newa = newtarget in *\) *)
1678 (* (\*           Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
1679 (* (\*             (print_metasenv newm) *\) *)
1680 (* (\*             (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
1681 (*           print_newline (); *)
1682           if is_identity env newtarget then
1683             newmeta, newtarget
1684           else
1685             demodulate newmeta first_step metasenv newtarget
1686     in
1687     demodulate newmeta first_step (metasenv @ metas') target
1688 ;;
1689
1690
1691 (*
1692 let demodulation newmeta env target source =
1693   newmeta, target
1694 ;;
1695 *)
1696
1697
1698 let subsumption env target source =
1699   let _, (ty, tl, tr, _), tmetas, _ = target
1700   and _, (ty', sl, sr, _), smetas, _ = source in
1701   if ty <> ty' then
1702     false
1703   else
1704     let metasenv, context, ugraph = env in
1705     let metasenv = metasenv @ tmetas @ smetas in
1706     let names = names_of_context context in
1707     let samesubst subst subst' =
1708 (*       Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
1709 (*         (print_subst subst) (print_subst subst'); *)
1710 (*       print_newline (); *)
1711       let tbl = Hashtbl.create (List.length subst) in
1712       List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
1713       List.for_all
1714         (fun (m, (c, t1, t2)) ->
1715            try
1716              let c', t1', t2' = Hashtbl.find tbl m in
1717              if (c = c') && (t1 = t1') && (t2 = t2') then true
1718              else false
1719            with Not_found ->
1720              true)
1721         subst'
1722     in
1723     let subsaux left right left' right' =
1724       try
1725         let subst, menv, ug = matching metasenv context left left' ugraph
1726         and subst', menv', ug' = matching metasenv context right right' ugraph
1727         in
1728 (*         Printf.printf "left = right: %s = %s\n" *)
1729 (*           (CicPp.pp left names) (CicPp.pp right names); *)
1730 (*         Printf.printf "left' = right': %s = %s\n" *)
1731 (*           (CicPp.pp left' names) (CicPp.pp right' names);         *)
1732         samesubst subst subst'
1733       with e ->
1734 (*         print_endline (Printexc.to_string e); *)
1735         false
1736     in
1737     let res =
1738       if subsaux tl tr sl sr then true
1739       else subsaux tl tr sr sl
1740     in
1741     if res then (
1742       Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
1743         (string_of_equality ~env target) (string_of_equality ~env source);
1744       print_newline ();
1745     );
1746     res
1747 ;;
1748 *)
1749
1750
1751 let extract_differing_subterms t1 t2 =
1752   let module C = Cic in
1753   let rec aux t1 t2 =
1754     match t1, t2 with
1755     | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
1756         [(t1, t2)]
1757     | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
1758         let res = List.concat (List.map2 aux tl1 tl2) in
1759         if h1 <> h2 then
1760           if res = [] then [(h1, h2)] else [(t1, t2)]
1761         else
1762           if List.length res > 1 then [(t1, t2)] else res
1763     | t1, t2 ->
1764         if t1 <> t2 then [(t1, t2)] else []
1765   in
1766   let res = aux t1 t2 in
1767   match res with
1768   | hd::[] -> Some hd
1769   | _ -> None
1770 ;;
1771
1772