27 subtype.ML thy_syntax.ML ../Pure/section_utils.ML\ |
27 subtype.ML thy_syntax.ML ../Pure/section_utils.ML\ |
28 ../Provers/hypsubst.ML ../Provers/classical.ML\ |
28 ../Provers/hypsubst.ML ../Provers/classical.ML\ |
29 ../Provers/simplifier.ML ../Provers/splitter.ML\ |
29 ../Provers/simplifier.ML ../Provers/splitter.ML\ |
30 $(NAMES:%=%.thy) $(NAMES:%=%.ML) |
30 $(NAMES:%=%.thy) $(NAMES:%=%.ML) |
31 |
31 |
32 $(BIN)/HOL: $(BIN)/Pure $(FILES) |
32 $(BIN)/Old_HOL: $(BIN)/Pure $(FILES) |
33 if [ -d $${ISABELLEBIN:?}/Pure ];\ |
33 if [ -d $${ISABELLEBIN:?}/Pure ];\ |
34 then echo Bad value for ISABELLEBIN: \ |
34 then echo Bad value for ISABELLEBIN: \ |
35 $(BIN) is the Isabelle source directory; \ |
35 $(BIN) is the Isabelle source directory; \ |
36 exit 1; \ |
36 exit 1; \ |
37 fi;\ |
37 fi;\ |
38 case "$(COMP)" in \ |
38 case "$(COMP)" in \ |
39 poly*) echo 'make_database"$(BIN)/HOL"; quit();' \ |
39 poly*) echo 'make_database"$(BIN)/Old_HOL"; quit();' \ |
40 | $(COMP) $(BIN)/Pure;\ |
40 | $(COMP) $(BIN)/Pure;\ |
41 echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL ;;\ |
41 echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/Old_HOL;;\ |
42 sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\ |
42 sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/Old_HOL" banner;' | \ |
|
43 $(BIN)/Pure ;;\ |
43 *) echo Bad value for ISABELLECOMP: \ |
44 *) echo Bad value for ISABELLECOMP: \ |
44 $(COMP) is not poly or sml; exit 1;;\ |
45 $(COMP) is not poly or sml; exit 1;;\ |
45 esac |
46 esac |
46 |
47 |
47 $(BIN)/Pure: |
48 $(BIN)/Pure: |
49 |
50 |
50 #### Testing of HOL |
51 #### Testing of HOL |
51 |
52 |
52 #A macro referring to the object-logic (depends on ML compiler) |
53 #A macro referring to the object-logic (depends on ML compiler) |
53 LOGIC:sh=case $ISABELLECOMP in \ |
54 LOGIC:sh=case $ISABELLECOMP in \ |
54 poly*) echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\ |
55 poly*) echo "$ISABELLECOMP $ISABELLEBIN/Old_HOL" ;;\ |
55 sml*) echo "$ISABELLEBIN/HOL" ;;\ |
56 sml*) echo "$ISABELLEBIN/Old_HOL" ;;\ |
56 *) echo "echo Bad value for ISABELLECOMP: \ |
57 *) echo "echo Bad value for ISABELLECOMP: \ |
57 $ISABELLEBIN is not poly or sml; exit 1" ;;\ |
58 $ISABELLEBIN is not poly or sml; exit 1" ;;\ |
58 esac |
59 esac |
59 |
60 |
60 ##IMP-semantics example |
61 ##IMP-semantics example |
61 IMP_NAMES = Com Denotation Equiv Properties |
62 IMP_NAMES = Com Denotation Equiv Properties |
62 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) |
63 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) |
63 |
64 |
64 IMP: $(BIN)/HOL $(IMP_FILES) |
65 IMP: $(BIN)/Old_HOL $(IMP_FILES) |
65 echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC) |
66 echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC) |
66 |
67 |
67 ##The integers in HOL |
68 ##The integers in HOL |
68 INTEG_NAMES = Relation Equiv Integ |
69 INTEG_NAMES = Relation Equiv Integ |
69 |
70 |
70 INTEG_FILES = Integ/ROOT.ML \ |
71 INTEG_FILES = Integ/ROOT.ML \ |
71 $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML) |
72 $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML) |
72 |
73 |
73 Integ: $(BIN)/HOL $(INTEG_FILES) |
74 Integ: $(BIN)/Old_HOL $(INTEG_FILES) |
74 echo 'exit_use"Integ/ROOT.ML";quit();' | $(LOGIC) |
75 echo 'exit_use"Integ/ROOT.ML";quit();' | $(LOGIC) |
75 |
76 |
76 ##I/O Automata |
77 ##I/O Automata |
77 IOA_EX_NAMES = Action Channels Correctness Impl Lemmas Multiset Receiver Sender |
78 IOA_EX_NAMES = Action Channels Correctness Impl Lemmas Multiset Receiver Sender |
78 IOA_MT_NAMES = Asig IOA Option Solve |
79 IOA_MT_NAMES = Asig IOA Option Solve |
79 |
80 |
80 IOA_FILES = IOA/ROOT.ML IOA/example/Packet.thy IOA/example/Spec.thy\ |
81 IOA_FILES = IOA/ROOT.ML IOA/example/Packet.thy IOA/example/Spec.thy\ |
81 $(IOA_EX_NAMES:%=IOA/example/%.thy) $(IOA_EX_NAMES:%=IOA/example/%.ML)\ |
82 $(IOA_EX_NAMES:%=IOA/example/%.thy) $(IOA_EX_NAMES:%=IOA/example/%.ML)\ |
82 $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML) |
83 $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML) |
83 |
84 |
84 IOA: $(BIN)/HOL $(IOA_FILES) |
85 IOA: $(BIN)/Old_HOL $(IOA_FILES) |
85 echo 'exit_use"IOA/ROOT.ML";quit();' | $(LOGIC) |
86 echo 'exit_use"IOA/ROOT.ML";quit();' | $(LOGIC) |
86 |
87 |
87 ##Properties of substitutions |
88 ##Properties of substitutions |
88 SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas |
89 SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas |
89 |
90 |
90 SUBST_FILES = Subst/ROOT.ML \ |
91 SUBST_FILES = Subst/ROOT.ML \ |
91 $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) |
92 $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) |
92 |
93 |
93 Subst: $(BIN)/HOL $(SUBST_FILES) |
94 Subst: $(BIN)/Old_HOL $(SUBST_FILES) |
94 echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC) |
95 echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC) |
95 |
96 |
96 ##Miscellaneous examples |
97 ##Miscellaneous examples |
97 EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String |
98 EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String |
98 |
99 |
99 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
100 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
100 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
101 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
101 |
102 |
102 ex: $(BIN)/HOL $(EX_FILES) |
103 ex: $(BIN)/Old_HOL $(EX_FILES) |
103 echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC) |
104 echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC) |
104 |
105 |
105 #Full test. |
106 #Full test. |
106 test: $(BIN)/HOL IMP Integ IOA Subst ex |
107 test: $(BIN)/Old_HOL IMP Integ IOA Subst ex |
107 echo 'Test examples ran successfully' > test |
108 echo 'Test examples ran successfully' > test |
108 |
109 |
109 .PRECIOUS: $(BIN)/Pure $(BIN)/HOL |
110 .PRECIOUS: $(BIN)/Pure $(BIN)/Old_HOL |