(* DISCRIMINATION TREES *)
+let init_index () =
+ Hashtbl.clear Discrimination_tree.arities;
+;;
+
let empty_table () =
Discrimination_tree.DiscriminationTree.empty
;;
(candidate, eq_URI))
in
let c, other, eq_URI =
- if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
- else right, left, HL.Logic.eq_ind_r_URI
+ if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+ else right, left, Utils.eq_ind_r_URI ()
in
if o <> U.Incomparable then
try
(candidate, eq_URI))
in
let c, other, eq_URI =
- if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
- else right, left, HL.Logic.eq_ind_r_URI
+ if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+ else right, left, Utils.eq_ind_r_URI ()
in
if o <> U.Incomparable then
try
;;
-let build_ens_for_sym_eq ty x y =
- [(UriManager.uri_of_string
- "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty);
- (UriManager.uri_of_string
- "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x);
- (UriManager.uri_of_string
- "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)]
-;;
-
-
let build_newtarget_time = ref 0.;;
incr demod_counter;
let bo' =
let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
- C.Appl [C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+ C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
S.lift 1 eq_ty; l; r]
in
if sign = Utils.Positive then
(* let target' = *)
let eq_found =
let proof' =
- let ens =
- if pos = Utils.Left then
- build_ens_for_sym_eq ty what other
- else
- build_ens_for_sym_eq ty other what
+(* let ens = *)
+(* if pos = Utils.Left then *)
+(* build_ens_for_sym_eq ty what other *)
+(* else *)
+(* build_ens_for_sym_eq ty other what *)
+ let termlist =
+ if pos = Utils.Left then [ty; what; other]
+ else [ty; other; what]
in
- Inference.ProofSymBlock (ens, proof')
+ Inference.ProofSymBlock (termlist, proof')
in
let what, other =
if pos = Utils.Left then what, other else other, what
(* in *)
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
- (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+ (LibraryObjects.eq_URI (), 0, 1, []);
eq_ty; if is_left then right else left]
in
(bo,
let bo'' =
let l, r =
if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
- C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty; l; r]
+ C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+ S.lift 1 eq_ty; l; r]
in
incr maxmeta;
let metaproof =
(* let target' = *)
let eq_found =
let proof' =
- let ens =
- if pos = Utils.Left then
- build_ens_for_sym_eq ty what other
- else
- build_ens_for_sym_eq ty other what
+(* let ens = *)
+(* if pos = Utils.Left then *)
+(* build_ens_for_sym_eq ty what other *)
+(* else *)
+(* build_ens_for_sym_eq ty other what *)
+(* in *)
+ let termlist =
+ if pos = Utils.Left then [ty; what; other]
+ else [ty; other; what]
in
- Inference.ProofSymBlock (ens, proof')
+ Inference.ProofSymBlock (termlist, proof')
in
let what, other =
if pos = Utils.Left then what, other else other, what
(* in *)
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
- (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+ (LibraryObjects.eq_URI (), 0, 1, []);
eq_ty; if ordering = U.Gt then right else left]
in
(bo',
let bo'' =
let l, r =
if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
- C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty; l; r]
+ C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+ S.lift 1 eq_ty; l; r]
in
bo',
Inference.ProofBlock (
(* | _, _, (_, left, right, _), _, _ -> *)
(* not (fst (CR.are_convertible context left right ugraph)) *)
(* in *)
+ let _ =
+ let env = metasenv, context, ugraph in
+ debug_print
+ (lazy
+ (Printf.sprintf "end of superposition_right:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun e -> "Positive " ^
+ (Inference.string_of_equality ~env e)) (new1 @ new2))))))
+ in
let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
in
let eq_found =
let proof' =
- let ens =
- if pos = Utils.Left then build_ens_for_sym_eq ty what other
- else build_ens_for_sym_eq ty other what
+(* let ens = *)
+(* if pos = Utils.Left then build_ens_for_sym_eq ty what other *)
+(* else build_ens_for_sym_eq ty other what *)
+(* in *)
+ let termlist =
+ if pos = Utils.Left then [ty; what; other]
+ else [ty; other; what]
in
- Inference.ProofSymBlock (ens, proof')
+ Inference.ProofSymBlock (termlist, proof')
in
let what, other =
if pos = Utils.Left then what, other else other, what