wip

Makefile

@@ -2,7 +2,7 @@
 
 BASE := $(shell if test -f BASE; then cat BASE; fi)
 ROOT_PATH := $(shell if test -f ROOT_PATH; then cat ROOT_PATH; else echo HOLLight; fi)
-ERASING := $(shell if test -f ERASING; then cat ERASING; fi)
+MAPPING := $(shell if test -f MAPPING; then cat MAPPING; fi)
 REQUIRING := $(shell if test -f REQUIRING; then cat REQUIRING; fi)
 VOFILES := $(shell if test -f VOFILES; then cat VOFILES; fi)
 
@@ -242,7 +242,7 @@ endif
 
 %.v: %.lp
 	@echo lambdapi export -o stt_coq $<
-	@lambdapi export -o stt_coq --encoding $(HOL2DK_DIR)/encoding.lp --renaming $(HOL2DK_DIR)/renaming.lp --erasing $(ERASING) --use-notations --requiring "$(REQUIRING)" $< > $@
+	@lambdapi export -o stt_coq --encoding $(HOL2DK_DIR)/encoding.lp --renaming $(HOL2DK_DIR)/renaming.lp --erasing $(MAPPING) --use-notations --requiring "$(REQUIRING)" $< > $@
 
 .PHONY: clean-v
 clean-v: rm-v clean-vo

config

@@ -14,22 +14,22 @@ fi
 
 usage() {
     cat <<__EOF__
-usage: `basename $0` $hollight_file.ml $root_path [coq_file_or_module] ... [$file.mk] [$erasing.lp]
+usage: `basename $0` $hollight_file.ml $root_path [coq_file_or_module] ... [$mapping.mk] [$mapping.lp]
 
 arguments:
   $hollight_file.ml: path to an ml file relative to $HOLLIGHT_DIR
   $root_path: name of the generated library
   coq_file_or_module: coq modules that needs to be imported in generated files
-  $file.mk: dependencies of vo files given in arguments
-  $erasing.lp: mappings between lambdapi and coq
+  $mapping.mk: dependencies of vo files given in arguments
+  $mapping.lp: mappings between lambdapi and coq
 
 effect in the current directory:
 - create a file CONFIG containing the command used to create links
 - create a file BASE containing the base name of $hollight_file.ml
 - create a file ROOT_PATH containing $root_path
 - create a file lambdapi.pkg
 - create a file _CoqProject
-- create a file ERASING containing $erasing.lp
+- create a file MAPPING containing $mapping.lp
 - create a file REQUIRING containing the list of Coq module names that need to be imported (in the same order as they are given in the command)
 - create a file VOFILES containing the list of Coq module names corresponding to the Coq files given in arguments with file extension ".vo"
 - add links to $file.mk, the Coq files given in argument and other files in $HOL2DK_DIR and $HOLLIGHT_DIR for translating and checking the proofs of $hollight_file.ml
@@ -47,9 +47,9 @@ parse_args() {
     if test $# -ne 0; then
         case $1 in
             *.lp)
-                if test -z "$erasing"
+                if test -z "$mapping"
                 then
-                    erasing=$1
+                    mapping=$1
                     shift
                     parse_args $*
                 else
@@ -121,8 +121,8 @@ echo "root_path = $root_path" >> lambdapi.pkg
 echo create _CoqProject ...
 echo "-R . $root_path ." > _CoqProject
 
-echo create ERASING ...
-echo ${erasing:-$HOL2DK_DIR/erasing.lp} > ERASING
+echo create MAPPING ...
+echo ${mapping:-$HOL2DK_DIR/With_N.lp} > MAPPING
 
 echo create REQUIRING ...
 echo $requiring > REQUIRING

main.ml

@@ -81,11 +81,11 @@ hol2dk $base.(dk|lp) $thm_id
 Multi-threaded lp file generation by having a file for each named theorem
 -------------------------------------------------------------------------
 
-hol2dk link hollight_file.ml root_path [coq_module_or_file ...] [mappings.lp] [deps.mk]
+hol2dk config hollight_file.ml root_path [coq_module_or_file ...] [mappings.lp] [mappings.mk]
   create files and links to the files generated by hol2dk dump
   in $HOLLIGHT_DIR and to the $HOL2DK_DIR files needed to translate
   hollight_file.prf to Dedukti, Lambdapi and Coq, and check the obtained files
-  (do hol2dk link without arguments to get more details)
+  (do hol2dk config without arguments to get more details)
  
 hol2dk split $base
   generate $base.thp and the files $thm.sti, $thm.pos and $thm.use