<commit_before>include ../../common.mk

# tests that should pass
PASS = \
  Simple \
  Self \
  Poly \
  Irrefutable \
  LocalTopoSort \
  InstCtx \
  ExhaustGuard \
  PartialAppliedPolyDataCon \
  NonStructuralRec \
  DotName \
  MapAccumR \
  Sub \
  FTP \
  AddAndReplace \
  FTPDefault \
  PolyInstance2 \
  PolyInstance3 \
  MutrecInst \
  Bits \
  BitsRewrite \
  Records \
  RecordConstruction \
  PatternGuard \
  Guard2 \
  Notations \

# tests that *should* pass but currently fail
TODO_PASS  = \
  Renamed \
  RenameModule \
  TopBind \
  InstVar \
  Mutrec \
  Existential \
  TypeAnnotations \
  StrictPair \




MODULES = $(PASS) $(TODO_PASS)

VFILES    = $(addsuffix .v,$(MODULES)) Renamed.v
VOFILES   = $(patsubst %.v,%.vo,$(VFILES))
COQFLAGS  = ""

# typecheck *quietly*
TYPECHECK=coqc 1>/dev/null

main:
	# Call ourselves with -k, so that we see all test outputs,
	# even if some fail
	$(MAKE) -k all

all:  $(VFILES) pass todo_pass

pass: $(addsuffix .pass,$(PASS))
	@echo -------- END PASS ------------

todo_pass: $(foreach f,$(TODO_PASS),$(f).fail)
	@echo
	@echo "Any names printed without errors should be moved from TODO_PASS to PASS"

%.pass : %.v
	@/bin/echo -n "$<: "
	@if ! test -e $<; \
	 then echo -e "\033[1;31mmissing\033[0m (should pass)"; exit 1;\
	 elif ! $(TYPECHECK) $< >&/dev/null; \
	 then echo -e "\033[1;31mfailed\033[0m (should pass)"; exit 1;  \
	 else echo -e "\033[1;32mpassed\033[0m"; \
	 fi

%.fail : %.v
	@/bin/echo -n "$<: "
	@if ! test -e $<; \
	 then echo -e "\033[1;31mmissing\033[0m"; \
	 elif ! $(TYPECHECK) $< >&/dev/null; \
	 then echo -e "\033[1;31mfailed\033[0m"; \
	 else echo -e "\033[1;32mpassed\033[0m (unexpected)"; exit 1; \
	 fi

%.vo : %.v
	@coqc -Q . "" $*.v

.SECONDEXPANSION:
%.v : FORCE $$(wildcard $*/edits) $$(wildcard $*/preamble.v) %.hs 
	@rm -f $*.v
	@if [ -e $*/preamble.v ]; then P_ARG="-p $*/preamble.v"; else P_ARG=; fi;\
	if [ -e $*/edits ]; then E_ARG="-e $*/edits"; else E_ARG=; fi;\
	$(HS_TO_COQ) $${E_ARG} -e renamings -o . $${P_ARG} $*.hs 1>/dev/null

Renamed.v: RenameMe.hs RenameMe.hs-boot RenameMeToo.hs RenameMe/edits
	@rm -f Renamed.v
	ghc -c RenameMe.hs-boot
	ghc -c RenameMeToo.hs
	$(HS_TO_COQ) -e RenameMe/edits -e renamings -o . RenameMe.hs RenameMeToo.hs 1>/dev/null

# We always want to re-build the .v files, to test the current build of hs-to-coq
FORCE:
<commit_msg>tests: Renamed No need to manually call ghc<commit_after>include ../../common.mk

# tests that should pass
PASS = \
  Simple \
  Self \
  Poly \
  Irrefutable \
  LocalTopoSort \
  InstCtx \
  ExhaustGuard \
  PartialAppliedPolyDataCon \
  NonStructuralRec \
  DotName \
  MapAccumR \
  Sub \
  FTP \
  AddAndReplace \
  FTPDefault \
  PolyInstance2 \
  PolyInstance3 \
  MutrecInst \
  Bits \
  BitsRewrite \
  Records \
  RecordConstruction \
  PatternGuard \
  Guard2 \
  Notations \

# tests that *should* pass but currently fail
TODO_PASS  = \
  Renamed \
  RenameModule \
  TopBind \
  InstVar \
  Mutrec \
  Existential \
  TypeAnnotations \
  StrictPair \




MODULES = $(PASS) $(TODO_PASS)

VFILES    = $(addsuffix .v,$(MODULES)) Renamed.v
VOFILES   = $(patsubst %.v,%.vo,$(VFILES))
COQFLAGS  = ""

# typecheck *quietly*
TYPECHECK=coqc 1>/dev/null

main:
	# Call ourselves with -k, so that we see all test outputs,
	# even if some fail
	$(MAKE) -k all

all:  $(VFILES) pass todo_pass

pass: $(addsuffix .pass,$(PASS))
	@echo -------- END PASS ------------

todo_pass: $(foreach f,$(TODO_PASS),$(f).fail)
	@echo
	@echo "Any names printed without errors should be moved from TODO_PASS to PASS"

%.pass : %.v
	@/bin/echo -n "$<: "
	@if ! test -e $<; \
	 then echo -e "\033[1;31mmissing\033[0m (should pass)"; exit 1;\
	 elif ! $(TYPECHECK) $< >&/dev/null; \
	 then echo -e "\033[1;31mfailed\033[0m (should pass)"; exit 1;  \
	 else echo -e "\033[1;32mpassed\033[0m"; \
	 fi

%.fail : %.v
	@/bin/echo -n "$<: "
	@if ! test -e $<; \
	 then echo -e "\033[1;31mmissing\033[0m"; \
	 elif ! $(TYPECHECK) $< >&/dev/null; \
	 then echo -e "\033[1;31mfailed\033[0m"; \
	 else echo -e "\033[1;32mpassed\033[0m (unexpected)"; exit 1; \
	 fi

%.vo : %.v
	@coqc -Q . "" $*.v

.SECONDEXPANSION:
%.v : FORCE $$(wildcard $*/edits) $$(wildcard $*/preamble.v) %.hs 
	@rm -f $*.v
	@if [ -e $*/preamble.v ]; then P_ARG="-p $*/preamble.v"; else P_ARG=; fi;\
	if [ -e $*/edits ]; then E_ARG="-e $*/edits"; else E_ARG=; fi;\
	$(HS_TO_COQ) $${E_ARG} -e renamings -o . $${P_ARG} $*.hs 1>/dev/null

Renamed.v: RenameMe.hs RenameMe.hs-boot RenameMeToo.hs RenameMe/edits
	@rm -f Renamed.v
	$(HS_TO_COQ) -e RenameMe/edits -e renamings -o . RenameMe.hs RenameMeToo.hs 1>/dev/null

# We always want to re-build the .v files, to test the current build of hs-to-coq
FORCE:

{'fraction_non_alphanumeric': 0.17876857749469213, 'fraction_numerical': 0.02929936305732484, 'mean_word_length': 2.718232044198895, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '478685', 'n_tokens_mistral': 2096, 'n_tokens_neox': 1945, 'n_words': 495}