# $Header: /users/lal/black/hol/Disser/RCS/Makefile,v 1.8 1997/06/05 23:51:33 black Exp $
# *created  "Wed Nov 13 08:51:10 1996" *by "Paul E. Black"
# *modified "Thu Jun  5 11:38:40 1997" *by "Paul E. Black"

.SUFFIXES: .thms .sml .ps .dvi .tex .view

.PRECIOUS: .dvi .ps

.sml.thms:
	hol90 < $<
	chmod go-w $@

LATEX=latex2e
#LATEX=latex

.tex.dvi:
	${LATEX} $<
	bibtex $*
	${LATEX} $<

.dvi.ps:
	dvips $<

.ps.view:
	ghostview $<

all: partialInf.thms
	@echo other possible targets are clean, shar, hol97.view,
	@echo wellformed.thms, semeq.thms, typeRules.thms, and c_ast.thms.

#-----------------------------------------------------------------------------

# other "source" files needed to rebuild or remake this
OTHER_SRC = Makefile mutrec.hol_lib

# C to HOL parser
C2HOL_SRC = c2holReadMe.sml c2holBuild.sml c2holLex.sml c2holParse.sml

#-----------------------------------------------------------------------------

# C Abstract Syntax Trees definitions in HOL

#		THESE ARE NOT USED, YET
# Type casting and conformance rules
typeRules.thms::	c_ast.thms

# Semantic equivalence of two C statements
semeq.thms::		c_ast.thms

# definitions of Well Formedness conditions
wellformed.thms::	c_ast.thms

# inference rules for Partial Correctness
partialInf.thms::	semeq.thms wellformed.thms

SOURCE_FILES = partialInf.sml wellformed.sml semeq.sml \
	typeRules.sml c_ast.sml

HELPER_FILES = cast2hol.sml partialTactics.sml utilities.sml wellfrmTactics.sml

# files more specific to proof of thttpd
THTTPD_FILES = proofs.sml state.sml syscalls.sml \
	th_*.sml

#-----------------------------------------------------------------------------

clean:
	rm -f *.thms *.holsig
	@echo all done

ALL_SRC_FILES = $(SOURCE_FILES) $(HELPER_FILES) $(THTTPD_FILES) \
	$(OTHER_SRC) $(C2HOL_SRC)

shar: $(ALL_SRC_FILES)
	shar -V $(ALL_SRC_FILES)

# end of $Source: /users/lal/black/hol/Disser/RCS/Makefile,v $