#########################################################################
#									#
# 			Makefile for Elle (EVAL)			#
#									#
#########################################################################

#To make the system, cd to this directory and type  
#	make -f Makefile 

#Environment variable ISABELLECOMP specifies the compiler.
#Environment variable ISABELLEBIN specifies the directory containing 
#                     the images for Isabelle object logics.
#Environment variable ISABELLELOCALBIN specifies the destination directory for 
#                     Elle images.
#For Poly/ML, ISABELLEBIN and ISABELLE must begin with a /


BIN = $(ISABELLEBIN)
LOCALBIN = $(ISABELLELOCALBIN)
COMP = $(ISABELLECOMP)
FILES =  ROOT.ML EvalProver.ML eval_obj.thy eval_obj.ML \
         eval_atexp.thy eval_exprow.thy eval_exp.thy \
         eval_match.thy eval_mrule.thy eval_dec.thy \
         eval_valbind.thy eval_atpat.thy \
         eval_patrow.thy eval_pat.thy eval_program.thy \
          

TESTFILES = Test1.ML Test2.ML Test3.ML Test4.ML Test5.ML

$(LOCALBIN)/EVAL:   $(LOCALBIN)/KERNEL  $(FILES) 
	case "$(COMP)" in \
	poly*)	echo 'make_database"$(LOCALBIN)/EVAL"; quit();'  \
			| $(COMP) $(LOCALBIN)/KERNEL;\
		echo 'use"ROOT";' | $(COMP) $(LOCALBIN)/EVAL;;\
	sml*)	echo 'use"ROOT.ML"; xML"$(LOCALBIN)/EVAL" banner;'\
                   | $(LOCALBIN)/KERNEL;;\
	*)	echo Bad value for ISABELLECOMP;;\
	esac


test:	$(TESTFILES)
	case "$(COMP)" in \
	poly*)  echo 'use "Test"' \
                     | $(COMP) $(LOCALBIN)/EVAL;;\
	sml*)	echo 'use "Test.ML"' \
                     | $(LOCALBIN)/EVAL;;\
	*)	echo Bad value for ISABELLECOMP;;\
	esac

.PRECIOUS:   $(LOCALBIN)/KERNEL  $(LOCALBIN)/EVAL 
