--- a/Makefile Tue Feb 28 02:02:34 1995 +0100
+++ b/Makefile Tue Feb 28 10:48:46 1995 +0100
@@ -18,50 +18,16 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML HOL.thy HOL.ML simpdata.ML Ord.thy Ord.ML \
- Set.thy Set.ML Fun.thy Fun.ML subset.thy subset.ML \
- equalities.thy equalities.ML thy_syntax.ML \
- Prod.thy Prod.ML Trancl.ML Trancl.thy Sum.thy Sum.ML WF.thy WF.ML \
- mono.thy mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML \
- add_ind_def.ML ind_syntax.ML indrule.ML Inductive.ML Inductive.thy \
- intr_elim.ML datatype.ML ../Pure/section_utils.ML\
- Finite.ML Finite.thy\
- Arith.thy Arith.ML Sexp.thy Sexp.ML Univ.thy Univ.ML \
- List.thy List.ML \
- ../Provers/classical.ML ../Provers/simplifier.ML \
- ../Provers/splitter.ML ../Provers/ind.ML
-
-IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
- IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy\
- IMP/Properties.thy IMP/Properties.ML
+THYS = HOL.thy Ord.thy Set.thy Fun.thy subset.thy \
+ equalities.thy Prod.thy Trancl.thy Sum.thy WF.thy \
+ mono.thy Lfp.thy Gfp.thy Nat.thy Inductive.thy \
+ Finite.thy Arith.thy Sexp.thy Univ.thy List.thy
-IOA_FILES = IOA/ROOT.ML IOA/example/Action.ML IOA/example/Action.thy\
- IOA/example/Channels.ML IOA/example/Channels.thy\
- IOA/example/Correctness.ML IOA/example/Correctness.thy\
- IOA/example/Impl.ML IOA/example/Impl.thy IOA/example/Lemmas.ML\
- IOA/example/Lemmas.thy IOA/example/Multiset.ML\
- IOA/example/Multiset.thy IOA/example/Packet.thy\
- IOA/example/Receiver.ML IOA/example/Receiver.thy\
- IOA/example/Sender.ML IOA/example/Sender.thy IOA/example/Spec.thy\
- IOA/meta_theory/Asig.thy IOA/meta_theory/IOA.ML\
- IOA/meta_theory/IOA.thy IOA/meta_theory/Option.ML\
- IOA/meta_theory/Option.thy IOA/meta_theory/Solve.ML\
- IOA/meta_theory/Solve.thy
-
-EX_FILES = ex/ROOT.ML ex/cla.ML \
- ex/LexProd.ML ex/LexProd.thy ex/meson.ML ex/mesontest.ML\
- ex/MT.ML ex/MT.thy ex/Acc.ML ex/Acc.thy \
- ex/PropLog.ML ex/PropLog.thy ex/Puzzle.ML ex/Puzzle.thy\
- ex/Qsort.thy ex/Qsort.ML ex/LList.thy ex/LList.ML \
- ex/Rec.ML ex/Rec.thy ex/rel.ML ex/set.ML ex/Simult.ML ex/Simult.thy\
- ex/Term.ML ex/Term.thy ex/String.thy ex/String.ML
-
-SUBST_FILES = Subst/ROOT.ML Subst/AList.ML Subst/AList.thy\
- Subst/Setplus.ML Subst/Setplus.thy\
- Subst/Subst.ML Subst/Subst.thy\
- Subst/Unifier.ML Subst/Unifier.thy\
- Subst/UTerm.ML Subst/UTerm.thy\
- Subst/UTLemmas.ML Subst/UTLemmas.thy
+FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
+ ind_syntax.ML indrule.ML intr_elim.ML simpdata.ML\
+ subtype.ML thy_syntax.ML ../Pure/section_utils.ML\
+ ../Provers/classical.ML ../Provers/simplifier.ML \
+ ../Provers/splitter.ML ../Provers/ind.ML $(THYS) $(THYS:.thy=.ML)
$(BIN)/HOL: $(BIN)/Pure $(FILES)
if [ -d $${ISABELLEBIN:?}/Pure ];\
@@ -75,21 +41,74 @@
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/HOL ;;\
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ $(COMP) is not poly or sml; exit 1;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-#Directories IMP and Subst also test the system
-#Load ex/ROOT.ML last since it creates the file "test"
-test: $(BIN)/HOL $(IMP_FILES) $(IOA_FILES) $(SUBST_FILES) $(EX_FILES)
- case "$(COMP)" in \
- poly*) echo '(use"IMP/ROOT.ML"; use"IOA/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML"); quit();' \
- | $(COMP) $(BIN)/HOL ;;\
- sml*) echo '(use"IMP/ROOT.ML"; use"IOA/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML");' | $(BIN)/HOL;;\
- *) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+#### Testing of HOL
+
+#A macro referring to the object-logic (depends on ML compiler)
+LOGIC:sh=case $ISABELLECOMP in \
+ poly*) echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
+ sml*) echo "$ISABELLEBIN/HOL" ;;\
+ *) echo "echo Bad value for ISABELLECOMP: \
+ $ISABELLEBIN is not poly or sml; exit 1" ;;\
esac
-.PRECIOUS: $(BIN)/Pure $(BIN)/HOL
+##IMP-semantics example
+IMP_THYS = IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy IMP/Properties.thy
+IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
+
+IMP: $(BIN)/HOL $(IMP_FILES)
+ echo 'use"IMP/ROOT.ML";quit();' | $(LOGIC)
+
+##The integers in HOL
+INTEG_THYS = Integ/Relation.thy Integ/Equiv.thy Integ/Integ.thy
+
+INTEG_FILES = Integ/ROOT.ML $(INTEG_THYS) $(INTEG_THYS:.thy=.ML)
+
+Integ: $(BIN)/HOL $(INTEG_FILES)
+ echo 'use"Integ/ROOT.ML";quit();' | $(LOGIC)
+
+##I/O Automata
+IOA_THYS = IOA/example/Action.thy IOA/example/Channels.thy\
+ IOA/example/Correctness.thy IOA/example/Impl.thy \
+ IOA/example/Lemmas.thy IOA/example/Multiset.thy \
+ IOA/example/Receiver.thy IOA/example/Sender.thy \
+ IOA/meta_theory/Asig.thy IOA/meta_theory/IOA.thy \
+ IOA/meta_theory/Option.thy IOA/meta_theory/Solve.thy
+
+IOA_FILES = IOA/ROOT.ML IOA/example/Packet.thy IOA/example/Spec.thy\
+ $(IOA_THYS) $(IOA_THYS:.thy=.ML)
+
+IOA: $(BIN)/HOL $(IOA_FILES)
+ echo 'use"IOA/ROOT.ML";quit();' | $(LOGIC)
+
+##Properties of substitutions
+SUBST_THYS = Subst/AList.thy Subst/Setplus.thy\
+ Subst/Subst.thy Subst/Unifier.thy\
+ Subst/UTerm.thy Subst/UTLemmas.thy
+
+SUBST_FILES = Subst/ROOT.ML $(SUBST_THYS) $(SUBST_THYS:.thy=.ML)
+
+Subst: $(BIN)/HOL $(SUBST_FILES)
+ echo 'use"Subst/ROOT.ML";quit();' | $(LOGIC)
+
+##Miscellaneous examples
+EX_THYS = ex/LexProd.thy ex/MT.thy ex/Acc.thy \
+ ex/PropLog.thy ex/Puzzle.thy ex/Qsort.thy ex/LList.thy \
+ ex/Rec.thy ex/Simult.thy ex/Term.thy ex/String.thy
+
+EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
+ ex/set.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
+
+ex: $(BIN)/HOL $(EX_FILES)
+ echo 'use"ex/ROOT.ML";quit();' | $(LOGIC)
+
+#Full test.
+test: $(BIN)/HOL IMP Integ IOA Subst ex
+ echo 'Test examples ran successfully' > test
+
+.PRECIOUS: $(BIN)/Pure $(BIN)/HOL