// required_predicates = set(normalize_token(t) for t in doc.xpath("//token/@base"))
coq_lib_index = {coq_lib_entry.split()[1] : coq_lib_entry \
for coq_lib_entry in coq_lib}
nltk_lib_index = {nltk_lib_entry.split()[1] : nltk_lib_entry \
for nltk_lib_entry in nltk_lib}
result_lib = []
for predicate in required_predicates:
if predicate in reserved_predicates:
continue
After Change
sig_merged = sig_auto
sig_merged.update(sig_arbi) // overwrites automatically inferred types.
// Remove predicates that are reserved or not required (e.g. variables).
preds_to_remove = set()
preds_to_remove.update(reserved_predicates)
for pred in sig_merged:
if pred not in required_predicates and not re.match(r"\S+_[0-9]", pred):
preds_to_remove.add(pred)
for pred in preds_to_remove:
if pred in sig_merged:
del sig_merged[pred]
// Convert into coq style library entries.
dynamic_library = []
for predicate, pred_type in sig_merged.items():
library_entry = build_library_entry(predicate, pred_type)
dynamic_library.append(library_entry)
