# =====================================================================
#
# 		 MAKEFILE FOR THE HOL LIBRARY: CSP
#
# =====================================================================

# =====================================================================
#
# MAIN ENTRIES:
#
# make all	    : create theories and compile code
#
# make clean	    : remove theories and compiled code
#	
# =====================================================================

# =====================================================================
# MACROS:
#
# Hol	    : the pathname of the version of hol used
# =====================================================================

Hol=/usr/groups/hol/HOL2/bin/hol

clean:
	rm -f *_ml.o *_ml.l *.th 
	@echo "===> library csp: all object code and theory files deleted"  

.SUFFIXES: .th .ml

.ml.th:;	/bin/rm -f $*.th $*.log
		echo 'set_flag(`abort_when_fail`,true);;'\
	             'loadt `$*`;;'\
                     'print_theory `-`;;'\
                     'quit();;' | ${Hol} > $*.log 2>&1

all:	boolarith1.th boolarith2.th list_lib1.th\
	traces.th restrict.th star.th order.th\
	process_ty.th\
	stop.th run.th prefix.th after.th choice.th parallel.th\
	process_fix.th mu.th process.th\
	after_laws.th par_laws.th\
	csp_syntax.th
	@echo "===> library csp rebuilt"

boolarith1.th: boolarith1.ml

boolarith2.th: boolarith2.ml boolarith1.th

list_lib1.th: list_lib1.ml

traces.th: traces.ml list_lib1.th

restrict.th: restrict.ml traces.th boolarith2.th

star.th: star.ml restrict.th

order.th: order.ml restrict.th

process_ty.th: process_ty.ml star.th
 
stop.th: stop.ml process_ty.th
 
run.th: run.ml process_ty.th
 
prefix.th: prefix.ml process_ty.th
 
after.th: after.ml process_ty.th
 
choice.th: choice.ml process_ty.th

parallel.th: parallel.ml process_ty.th

process_fix.th: process_fix.ml stop.th

mu.th: mu.ml process_fix.th

process.th: process.ml run.th prefix.th choice.th after.th parallel.th mu.th

after_laws.th: after_laws.ml process.th

par_laws.th: par_laws.ml process.th

csp_syntax.th: csp_syntax.ml process.th