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