TOOLDIR=/Users/mark/bitbucket/lem
HERDDIR=/Users/mark/git/herdtools/herd
HOLDIR=/Users/mark/warez/HOL

all: MetaTheory.sig

LEMFLAGS= -wl_unused_vars ign -wl_pat_exh ign

# Herd to Lem
c11_base.lem: c11_base.cat
	$(HERDDIR)/herd -model ./c11_base.cat -dumplem > ./c11_base.lem

cpp11.lem : c11_partialSC.cat c11_base.lem
	$(HERDDIR)/herd -model ./c11_partialSC.cat -dumplem > ./cpp11.lem

# Lem to HOL
Cmm_auxScript.sml: cmm_aux.lem $(TOOLDIR)/lem
	$(TOOLDIR)/lem $(LEMFLAGS) -tex -tex_suppress_target_names -suppress_renaming -hol cmm_aux.lem

CmmScript.sml: Cmm_auxScript.sml cmm.lem $(TOOLDIR)/lem
	$(TOOLDIR)/lem $(LEMFLAGS) -tex -tex_suppress_target_names -suppress_renaming -hol cmm.lem

herdScript.sml C11_baseScript.sml Cpp11Script.sml Cpp11soundnessScript.sml: CmmScript.sml c11_base.lem cpp11.lem herd.lem $(TOOLDIR)/lem
	$(TOOLDIR)/lem $(LEMFLAGS) -tex -tex_suppress_target_names -suppress_renaming	 -hol herd.lem c11_base.lem cpp11.lem cpp11soundness.lem

# Build HOL
Cmm_auxTheory.sig Cmm_auxTheory.sml Cmm_auxTheory.ui Cmm_auxTheory.uo: Cmm_auxScript.sml
	$(HOLDIR)/bin/Holmake Cmm_auxTheory.sig Cmm_auxTheory.sml Cmm_auxTheory.ui Cmm_auxTheory.uo

CmmTheory.sig CmmTheory.sml CmmTheory.ui CmmTheory.uo: CmmScript.sml
	$(HOLDIR)/bin/Holmake CmmTheory.sig CmmTheory.sml CmmTheory.ui CmmTheory.uo

HerdTheory.sig HerdTheory.sml HerdTheory.ui HerdTheory.uo: CmmTheory.sig CmmTheory.sml CmmTheory.ui CmmTheory.uo herdScript.sml
	$(HOLDIR)/bin/Holmake HerdTheory.sig HerdTheory.sml HerdTheory.ui HerdTheory.uo

C11_baseTheory.sig C11_baseTheory.sml C11_baseTheory.ui C11_baseTheory.uo: HerdTheory.sig HerdTheory.sml HerdTheory.ui HerdTheory.uo CmmTheory.sig CmmTheory.sml CmmTheory.ui CmmTheory.uo C11_baseScript.sml
	$(HOLDIR)/bin/Holmake C11_baseTheory.sig C11_baseTheory.sml C11_baseTheory.ui C11_baseTheory.uo


Cpp11Theory.sig Cpp11Theory.sml Cpp11Theory.ui Cpp11Theory.uo: HerdTheory.sig HerdTheory.sml HerdTheory.ui HerdTheory.uo CmmTheory.sig CmmTheory.sml CmmTheory.ui CmmTheory.uo C11_baseTheory.sig C11_baseTheory.sml C11_baseTheory.ui C11_baseTheory.uo Cpp11Script.sml
	$(HOLDIR)/bin/Holmake Cpp11Theory.sig Cpp11Theory.sml Cpp11Theory.ui Cpp11Theory.uo

Cpp11soundnessTheory.sig Cpp11soundnessTheory.sml Cpp11soundnessTheory.ui Cpp11soundnessTheory.uo: Cpp11Theory.sig Cpp11Theory.sml Cpp11Theory.ui Cpp11Theory.uo CmmTheory.sig CmmTheory.sml CmmTheory.ui CmmTheory.uo Cpp11soundnessScript.sml
	$(HOLDIR)/bin/Holmake Cpp11soundnessTheory.sig Cpp11soundnessTheory.sml Cpp11soundnessTheory.ui Cpp11soundnessTheory.uo

MetaTheory.sig MetaTheory.sml MetaTheory.ui MetaTheory.uo: Cpp11soundnessTheory.sig Cpp11soundnessTheory.sml Cpp11soundnessTheory.ui Cpp11soundnessTheory.uo MetaScript.sml
	$(HOLDIR)/bin/Holmake MetaTheory.sig MetaTheory.sml MetaTheory.ui MetaTheory.uo

clean:
	rm -rf *.tex *.uo *.ui *.sig *Theory.sml Cmm_auxScript.sml Cpp11Script.sml Cpp11soundnessAuxiliaryScript.sml Cpp11soundnessScript.sml OpenclScript.sml OpenclsoundnessAuxiliaryScript.sml OpenclsoundnessScript.sml CmmAuxiliaryScript.sml CmmScript.sml oOpenclmmAuxiliaryScript.sml OpenclmmScript.sml herdScript.sml OpenclherdScript.sml cpp11.lem c11_base.lem c11_baseScript.sml
