Check mappings

.gitignore

@@ -1,2 +1,3 @@
 _build/
 output*
+.vscode

Makefile

@@ -236,6 +236,22 @@ clean-lpo: rm-lpo
 rm-lpo:
 	-find . -maxdepth 1 -name '*.lpo' -delete
 
+.PHONY: get-check-mappings
+get-check-mappings: opam
+	@echo generate check_mappings file ...
+	@hol2dk check-mappings $(BASE) $(HOL2DK_DIR)/encoding.lp $(HOL2DK_DIR)/renaming.lp $(MAPPING) $(REQUIRING)
+
+BASE_ROCQ_OPTIONS := -q -no-glob -R . $(ROOT_PATH)
+# User specifiable rocq options
+EXTRA_ROCQ_OPTIONS ?=
+ROCQ_OPTIONS := $(BASE_ROCQ_OPTIONS) $(EXTRA_ROCQ_OPTIONS)
+
+.PHONY: check-mappings
+check-mappings: get-check-mappings $(VOFILES)
+	@echo check generated file ...
+	@rocq compile $(ROCQ_OPTIONS) $(BASE)_checkmappings.v
+	rm -f $(BASE)_checkmappings.v $(BASE)_checkmappings.vo $(BASE)_checkmappings.vok $(BASE)_checkmappings.vos
+
 .PHONY: v
 v: $(LP_FILES:%.lp=%.v)
 ifneq ($(SET_LP_FILES),1)
@@ -299,10 +315,6 @@ ifneq ($(INCLUDE_VO_MK),1)
 	touch .finished
 endif
 
-BASE_ROCQ_OPTIONS := -q -no-glob -R . $(ROOT_PATH)
-# User specifiable rocq options
-EXTRA_ROCQ_OPTIONS ?=
-ROCQ_OPTIONS := $(BASE_ROCQ_OPTIONS) $(EXTRA_ROCQ_OPTIONS)
 
 %.vo: %.v
 	@echo rocq $<

dune

@@ -1,7 +1,7 @@
 (executable
  (public_name hol2dk)
  (name main)
- (libraries str unix)
+ (libraries str unix lambdapi.lplib lambdapi.common lambdapi.parsing lambdapi.core lambdapi.export)
 )
 
 (install

dune-project

@@ -22,7 +22,8 @@
   dune
   (ocaml (>= 4.13))
   (hol_light (= 3.0.0))
- )
+  (lambdapi (= 3.0.0))
+)
 )
 
 ; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project

main.ml

@@ -143,6 +143,11 @@ hol2dk files [$path/]$base.(dk|lp)
   for each HOL-Light file required by $HOLLIGHT_DIR/$path/$base.ml, generate
   a (dk|lp) file with the statements of the theorems proved in that file
 
+hol2dk check-mappings $base $encoding.lp $renaming.lp $mappings.lp $requiring
+  generates a file $(base).checkmappings.v that can be used to diagnose
+  badly typed mappings, unused mappings, unmapped axioms and non-fully
+  mapped definitions.
+
 hol2dk env
   print the values of $HOL2DK_DIR and $HOLLIGHT_DIR
 
@@ -1236,6 +1241,22 @@ and command = function
 
   | "abbrev"::_ -> wrong_nb_args()
 
+  (* generate file to check mappings *)
+  | "check-mappings"::b::e::rn::m::rq ->
+    Xmapcheck.base := b ;
+    Export.Coq.stt := true ;
+    Export.Coq.use_implicits := false ;
+    Export.Coq.use_notations := true ;
+    Export.Coq.set_renaming rn ;
+    Xmapcheck.initial_rmap := !Export.Coq.rmap ;
+    Export.Coq.set_mapping m ;
+    Xmapcheck.unused_mappings := !Export.Coq.erase ;
+    Export.Coq.set_encoding e ;
+    Xmapcheck.requiring := String.concat " " rq ;
+    Xmapcheck.generate_check_file()
+
+  | "check-mappings"::_ -> wrong_nb_args()
+
   (* Single file generation (used neither in b.mk nor in Makefile). *)
   | f::args ->
      let r = range args in

renaming.lp

@@ -1,6 +1,36 @@
 // map for renaming dk/lp identifiers (on the right)
 // to Coq expressions (on the left)
 
+builtin "type'" ≔ Set;
+builtin "arrow" ≔ fun;
+builtin "equal" ≔ =;
+builtin "exists_1" ≔ ∃₁;
+builtin "exists_1_def" ≔ ∃₁_def;
+builtin "neg" ≔ ¬;
+builtin "neg_def" ≔ ¬_def;
+builtin "bottom" ≔ ⊥;
+builtin "bottom_def" ≔ ⊥_def;
+builtin "vee" ≔ ∨;
+builtin "vee_def" ≔ ∨_def;
+builtin "existsq" ≔ ∃;
+builtin "exists_def" ≔ ∃_def;
+builtin "forallq" ≔ ∀;
+builtin "forall_def" ≔ ∀_def;
+builtin "doublearrow" ≔ ⇒;
+builtin "doublearrow_def" ≔ ⇒_def;
+builtin "wedge" ≔ ∧;
+builtin "wedge_def" ≔ ∧_def;
+builtin "top" ≔ ⊤;
+builtin "top_def" ≔ ⊤_def;
+builtin "top_i" ≔ ⊤ᵢ;
+builtin "wedge_e1" ≔ ∧ₑ₁;
+builtin "wedge_e2" ≔ ∧ₑ₂;
+builtin "exists_i" ≔ ∃ᵢ;
+builtin "exists_e" ≔ ∃ₑ;
+builtin "vee_i1" ≔ ∨ᵢ₁;
+builtin "vee_i2" ≔ ∨ᵢ₂;
+builtin "vee_e" ≔ ∨ₑ;
+
 builtin "minus" ≔ -;
 builtin "minus_def" ≔ -_def;
 builtin "minus'" ≔ -';

theory_hol.lp

@@ -41,7 +41,7 @@ symbol ⊤ᵢ : Prf ⊤;
 symbol ∧ᵢ [p : El bool] : Prf p → Π [q : El bool], Prf q → Prf (∧ p q);
 symbol ∧ₑ₁ [p q : El bool] : Prf (∧ p q) → Prf p;
 symbol ∧ₑ₂ [p q : El bool] : Prf (∧ p q) → Prf q;
-symbol ∃ᵢ [a] (p : El a → El bool) t : Prf (p t) → Prf (∃ p);
+symbol ∃ᵢ [a] (p : El a → El bool) (t : El a) : Prf (p t) → Prf (∃ p);
 symbol ∃ₑ [a] [p : El a → El bool] : Prf (∃ (λ x, p x)) → Π [r : El bool], (Π x:El a, Prf (p x) → Prf r) → Prf r;
 symbol ∨ᵢ₁ [p : El bool] : Prf p → Π q : El bool, Prf (∨ p q);
 symbol ∨ᵢ₂ (p : El bool) [q : El bool] : Prf q → Prf (∨ p q);