# Makefile for GFJ

COQ_ARGS := -impredicative-set
COQ := coqc $(COQ_ARGS)

all : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
        Arith.vo Lambda.vo Exception.vo Ref.vo Bool.vo \
	Ref_Arith.vo Lambda_Arith.vo Exception_Arith.vo \
	Ref_Bool.vo Lambda_Bool.vo Exception_Bool.vo \
	Lambda_Exception.vo Lambda_Ref.vo \
	Ref_Exception.vo Lambda_Exception_State.vo \
	Ref_Arith.vo Ref_Exception.vo

FJ_tactics.vo : FJ_tactics.v
	$(TIME) coqc FJ_tactics.v

Functors.vo : FJ_tactics.vo Functors.v
	$(TIME) $(COQ) Functors.v

MonadLib.vo : Functors.vo MonadLib.v
	$(TIME) $(COQ) MonadLib.v

Names.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.v
	$(TIME) $(COQ) Names.v

PNames.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.v
	$(TIME) $(COQ) PNames.v

Arith.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo Arith.v
	$(TIME) $(COQ) Arith.v

Ref.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo Ref.v
	$(TIME) $(COQ) Ref.v

Bool.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo Bool.v
	$(TIME) $(COQ) Bool.v

Lambda.vo : FJ_tactics.vo Functors.vo MonadLib.vo PNames.vo Names.vo Lambda.v
	$(TIME) $(COQ) Lambda.v

Ref_Arith.vo : FJ_tactics.vo Functors.vo MonadLib.vo Arith.vo Names.vo Ref.vo Ref_Arith.v
	$(TIME) $(COQ) Ref_Arith.v

Ref_Bool.vo : FJ_tactics.vo Functors.vo MonadLib.vo Bool.vo Names.vo Ref.vo Ref_Bool.v
	$(TIME) $(COQ) Ref_Bool.v

Exception.vo : FJ_tactics.vo Functors.vo Names.vo MonadLib.vo Names.vo Exception.v
	$(TIME) $(COQ) Exception.v

Exception_Arith.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo Arith.vo Exception.vo Exception_Arith.v
	$(TIME) $(COQ) Exception_Arith.v

Exception_Bool.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo  Bool.vo Exception.vo Exception_Bool.v
	$(TIME) $(COQ) Exception_Bool.v

Ref_Exception.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo Ref.vo Exception.vo Ref_Exception.v
	$(TIME) $(COQ) Ref_Exception.v

Lambda_Ref.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo Lambda.vo Ref.vo Lambda_Ref.v
	$(TIME) $(COQ) Lambda_Ref.v

Lambda_Exception.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo Lambda.vo Exception.vo Lambda_Exception.v
	$(TIME) $(COQ) Lambda_Exception.v

Lambda_Exception_State.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo Lambda.vo \
	Exception.vo Ref.vo Lambda_Exception_State.v
	$(TIME) $(COQ) Lambda_Exception_State.v

Lambda_Arith.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo Lambda.vo Arith.vo Lambda_Arith.v
	$(TIME) $(COQ) Lambda_Arith.v

Lambda_Bool.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo Lambda.vo Bool.vo Lambda_Bool.v
	$(TIME) $(COQ) Lambda_Bool.v

tests : test_A.vo test_AB.vo test_ABE.vo test_AE.vo test_AL.vo \
	test_AR.vo test_ARE.vo test_ARL.vo test_ARLE.vo test_B.vo \
	test_BAL.vo test_BAR.vo test_BARE.vo test_BARLE.vo test_BE.vo \
	test_L.vo test_BL.vo test_BRE.vo test_BRLE.vo test_BLE.vo \
	test_LRE.vo test_LR.vo test_LE.vo

test_A.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo Arith.vo test_A.v
	$(TIME) $(COQ) test_A.v

test_AB.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo Arith.vo Bool.vo test_AB.v
	$(TIME) $(COQ) test_AB.v

test_ABE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Arith.vo Bool.vo Exception.vo \
	Exception_Arith.vo Exception_Bool.vo \
	test_ABE.v
	$(TIME) $(COQ) test_ABE.v

test_AE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Arith.vo Exception.vo \
	Exception_Arith.vo \
	test_AE.v
	$(TIME) $(COQ) test_AE.v

test_AL.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Arith.vo Lambda.vo \
	Lambda_Arith.vo	\
	test_AL.v
	$(TIME) $(COQ) test_AL.v

test_AR.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Arith.vo Ref.vo \
	Ref_Arith.vo \
	test_AR.v
	$(TIME) $(COQ) test_AR.v

test_ARE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Arith.vo Ref.vo Exception.vo \
	Ref_Arith.vo Ref_Exception.vo \
	test_ARE.v
	$(TIME) $(COQ) test_ARE.v

test_RE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Ref.vo Exception.vo Ref_Exception.vo test_RE.v
	$(TIME) $(COQ) test_RE.v

test_ARL.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Arith.vo Ref.vo Lambda.vo \
	Ref_Arith.vo Lambda_Arith.vo Lambda_Ref.vo \
	test_ARL.v
	$(TIME) $(COQ) test_ARL.v

test_LR.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Ref.vo Lambda.vo Lambda_Ref.vo \
	test_LR.v
	$(TIME) $(COQ) test_LR.v

test_ARLE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Arith.vo Ref.vo Exception.vo Lambda.vo \
	Ref_Arith.vo Lambda_Arith.vo Exception_Arith.vo \
	Lambda_Exception.vo Lambda_Ref.vo Ref_Exception.vo Lambda_Exception_State.vo \
	test_ARLE.v
	$(TIME) $(COQ) test_ARLE.v

test_LRE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Ref.vo Exception.vo Lambda.vo \
	Lambda_Exception.vo Lambda_Ref.vo Ref_Exception.vo Lambda_Exception_State.vo \
	test_LRE.v
	$(TIME) $(COQ) test_LRE.v

test_LE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Exception.vo Lambda.vo Lambda_Exception.vo test_LRE.v
	$(TIME) $(COQ) test_LE.v

test_B.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Bool.vo \
	test_B.v
	$(TIME) $(COQ) test_B.v

test_BAL.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Arith.vo Bool.vo Lambda.vo \
	Lambda_Arith.vo Lambda_Bool.vo \
	test_BAL.v
	$(TIME) $(COQ) test_BAL.v

test_BALE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Arith.vo Bool.vo Exception.vo Lambda.vo \
	Lambda_Arith.vo Exception_Arith.vo \
	Lambda_Bool.vo Exception_Bool.vo \
	Lambda_Exception.vo \
	test_BALE.v
	$(TIME) $(COQ) test_BALE.v

test_BAR.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Arith.vo Bool.vo Ref.vo \
	Ref_Arith.vo Ref_Bool.vo \
	test_BAR.v
	$(TIME) $(COQ) test_BAR.v

test_BR.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Arith.vo Bool.vo Ref.vo \
	Ref_Bool.vo test_BR.v 
	$(TIME) $(COQ) test_BAR.v

test_BARE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Arith.vo Bool.vo Ref.vo Exception.vo \
	Ref_Arith.vo Ref_Bool.vo Exception_Arith.vo Exception_Bool.vo \
	test_BARE.v
	$(TIME) $(COQ) test_BARE.v

test_BRE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Bool.vo Ref.vo Exception.vo \
	Ref_Bool.vo Exception_Bool.vo test_BRE.v
	$(TIME) $(COQ) test_BRE.v

test_BLE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Bool.vo Exception.vo Lambda.vo \
	Lambda_Bool.vo Exception_Bool.vo \
	Lambda_Exception.vo test_BLE.v
	$(TIME) $(COQ) test_BLE.v

test_BARL.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Arith.vo Bool.vo Ref.vo Lambda.vo \
	Ref_Arith.vo Ref_Bool.vo \
	Lambda_Arith.vo Lambda_Bool.vo Lambda_Ref.vo \
	test_BARL.v
	$(TIME) $(COQ) test_BARL.v

test_BARLE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Arith.vo Bool.vo Ref.vo Exception.vo Lambda.vo \
	Ref_Arith.vo Lambda_Arith.vo Exception_Arith.vo \
	Ref_Bool.vo Lambda_Bool.vo Exception_Bool.vo \
	Lambda_Exception.vo Lambda_Ref.vo Ref_Exception.vo Lambda_Exception_State.vo \
	test_BARLE.v
	$(TIME) $(COQ) test_BARLE.v

test_BRLE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Bool.vo Ref.vo Exception.vo Lambda.vo \
	Ref_Bool.vo Lambda_Bool.vo Exception_Bool.vo \
	Lambda_Exception.vo Lambda_Ref.vo Ref_Exception.vo Lambda_Exception_State.vo \
	test_BRLE.v
	$(TIME) $(COQ) test_BRLE.v

test_BE.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo \
	Bool.vo Exception.vo \
	Exception_Bool.vo \
	test_BE.v
	$(TIME) $(COQ) test_BE.v

test_BL.vo : FJ_tactics.vo Functors.vo MonadLib.vo Names.vo PNames.vo \
	Bool.vo Lambda.vo \
	Lambda_Bool.vo \
	test_BL.v
	$(TIME) $(COQ) test_BL.v

test_L.vo : FJ_tactics.vo Functors.vo MonadLib.vo PNames.vo Names.vo \
	Lambda.vo \
	test_L.v
	$(TIME) $(COQ) test_L.v

clean :
	rm *.vo *.glob
