# this makefile was automatically generated; do not edit 

TIMEOUT ?= 10

WHY=why --no-arrays -explain -locs bsearch.loc  -split-user-conj

GWHY=gwhy-bin --no-arrays -explain -locs bsearch.loc  -split-user-conj

CADULIB=/home/jc/soft/why/lib

CADULIBFILE=caduceus.why

COQTACTIC=intuition

COQDEP=coqdep -I `coqc -where`/user-contrib

.PHONY: all coq pvs simplify ergo cvcl harvey smtlib cvc3 z3 zenon

all: simplify/bsearch_why.sx

coq: coq.depend coq/bsearch_why.vo

coq/bsearch_spec_why.v: why/bsearch_spec.why
	@echo 'why -coq-v8 [...] why/bsearch_spec.why' && $(WHY) -coq-v8 -dir coq -coq-preamble "Require Export Caduceus." $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why

coq/%_why.v: why/bsearch_spec.why why/%.why
	@echo 'why -coq-v8 [...] why/$*.why' &&$(WHY) -coq-v8 -dir coq -coq-preamble "Require Export bsearch_spec_why." -coq-tactic "$(COQTACTIC)" $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

coq/%.vo: coq/%.v
	coqc -I coq $<

pvs: pvs/bsearch_spec_why.pvs pvs/bsearch_why.pvs

pvs/%_spec_why.pvs: why/%_spec.why
	$(WHY) -pvs -dir pvs -pvs-preamble "importing why@why" $(CADULIB)/why/$(CADULIBFILE) why/$*_spec.why

pvs/%_why.pvs: pvs/bsearch_spec_why.pvs why/%.why
	$(WHY) -pvs -dir pvs -pvs-preamble "importing bsearch_spec_why" $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

pvs/caduceus_why.pvs:
	$(WHY) -pvs -dir pvs $(CADULIB)/why/$(CADULIBFILE)

isabelle: isabelle/bsearch_why.thy isabelle/bsearch_spec_why.thy

isabelle/%_spec_why.thy: why/%_spec.why
	$(WHY) -isabelle -dir isabelle -isabelle-base-theory caduceus_why $(CADULIB)/why/$(CADULIBFILE) why/$*_spec.why

isabelle/%_why.thy: isabelle/bsearch_spec_why.thy why/%.why
	$(WHY) -isabelle -dir isabelle -isabelle-base-theory bsearch_spec_why $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why
	cp -f /home/jc/soft/why/lib/isabelle/caduceus_why.thy isabelle/

simplify: simplify/bsearch_why.sx
	@echo 'Running Simplify on proof obligations' && (dp -timeout $(TIMEOUT) $^)

simplify/%_why.sx: why/bsearch_spec.why why/%.why
	@echo 'why -simplify [...] why/$*.why' && $(WHY) -simplify -no-simplify-prelude -dir  simplify $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

ergo: why/bsearch_why.why
	@echo 'Running Ergo on proof obligations' && (dp -timeout $(TIMEOUT) $^)

why/%_why.sx: why/bsearch_spec.why why/%.why
	@echo 'why -why [...] why/$*.why' && $(WHY) -why -dir why $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

project: why/bsearch.wpr

why/%.wpr: why/bsearch_ctx.why
	@echo 'why --project [...] why/$*.why' && $(WHY) --project -dir why $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

goals: why/bsearch_ctx.why

why/%_ctx.why: why/bsearch_spec.why why/%.why
	@echo 'why --multi-why [...] why/$*.why' && $(WHY) --multi-why -dir why $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

why/%_why.why: why/bsearch_spec.why why/%.why
	@echo 'why -why [...] why/$*.why' && $(WHY) -why -dir why $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

cvcl: cvcl/bsearch_why.cvc

	@echo 'Running CVC Lite on proof obligations' && (dp -timeout $(TIMEOUT) $^)

cvcl/%_why.cvc: why/bsearch_spec.why why/%.why
	@echo 'why -cvcl [...] why/$*.why' && $(WHY) -cvcl --encoding sstrat -dir cvcl $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

harvey: harvey/bsearch_why.rv
	@echo 'Running haRVey on proof obligations' && (dp -timeout $(TIMEOUT) $^)

harvey/%_why.rv: why/bsearch_spec.why why/%.why
	@echo 'why -harvey [...] why/$*.why' && $(WHY) -harvey -dir harvey $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

zenon: zenon/bsearch_why.znn
	@echo 'Running Zenon on proof obligations' && (dp -timeout $(TIMEOUT) $^)

zenon/%_why.znn: why/bsearch_spec.why why/%.why
	@echo 'why -zenon [...] why/$*.why' && $(WHY) -zenon -dir zenon $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

smtlib: smtlib/bsearch_why.smt
	@echo 'Running Yices on proof obligations' && (dp -timeout $(TIMEOUT) $^)

smtlib/%_why.smt: why/bsearch_spec.why why/%.why
	@echo 'why -smtlib [...] why/$*.why' && $(WHY) -smtlib --encoding sstrat -exp all   -dir smtlib $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

z3: z3/bsearch_why.smt
	@echo 'Running Z3 on proof obligations' && (dp -smt-solver z3 -timeout $(TIMEOUT) $^)

z3/%_why.smt: why/bsearch_spec.why why/%.why
	@echo 'why -smtlib [...] why/$*.why' && $(WHY) -smtlib --encoding sstrat -exp all   -dir z3 $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

cvc3: cvc3/bsearch_why.smt
	@echo 'Running CVC3 on proof obligations' && (dp -smt-solver cvc3 -timeout $(TIMEOUT) $^)

cvc3/%_why.smt: why/bsearch_spec.why why/%.why
	@echo 'why -smtlib [...] why/$*.why' && $(WHY) -smtlib --encoding sstrat -exp all   -dir cvc3 $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

gui stat: bsearch.stat

%.stat: why/bsearch_spec.why why/%.why
	@echo 'gwhy-bin [...] why/$*.why' && $(GWHY) $(CADULIB)/why/$(CADULIBFILE) why/bsearch_spec.why why/$*.why

-include bsearch.depend

coq.depend: coq/bsearch_spec_why.v coq/bsearch_why.v
	-$(COQDEP) -I coq coq/bsearch*_why.v > bsearch.depend

clean:
	rm -f coq/*.vo