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