TOOLDIR=../../../../git/lem
HERDDIR=../../../../git/herdtools/herd
HOLDIR=../../../../warez/HOL

all: MetaTheory.sig

LEMFLAGS= -wl_unused_vars ign -wl_pat_exh ign

# Herd to Lem
cpp11.lem : c11_partialSC.cat
	$(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 Cpp11Script.sml Cpp11soundnessScript.sml: CmmScript.sml cpp11.lem herd.lem $(TOOLDIR)/lem
	$(TOOLDIR)/lem $(LEMFLAGS) -tex -tex_suppress_target_names -suppress_renaming	 -hol herd.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

Cpp11Theory.sig Cpp11Theory.sml Cpp11Theory.ui Cpp11Theory.uo: HerdTheory.sig HerdTheory.sml HerdTheory.ui HerdTheory.uo CmmTheory.sig CmmTheory.sml CmmTheory.ui CmmTheory.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 *.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
