16 #Makes FOL if this file is ABSENT -- but not |
16 #Makes FOL if this file is ABSENT -- but not |
17 #if it is out of date, since this Makefile does not know its dependencies! |
17 #if it is out of date, since this Makefile does not know its dependencies! |
18 |
18 |
19 BIN = $(ISABELLEBIN) |
19 BIN = $(ISABELLEBIN) |
20 COMP = $(ISABELLECOMP) |
20 COMP = $(ISABELLECOMP) |
21 FILES = ROOT.ML ZF.thy ZF.ML upair.thy upair.ML subset.thy subset.ML \ |
21 THYS = ZF.thy upair.thy subset.thy pair.thy domrange.thy \ |
22 thy_syntax.ML pair.thy pair.ML domrange.thy domrange.ML \ |
22 func.thy AC.thy simpdata.thy equalities.thy Bool.thy \ |
23 func.thy func.ML AC.thy AC.ML simpdata.thy simpdata.ML\ |
23 Sum.thy QPair.thy mono.thy Fixedpt.thy ind_syntax.thy add_ind_def.thy \ |
24 equalities.thy equalities.ML Bool.thy Bool.ML \ |
24 constructor.thy intr_elim.thy indrule.thy Inductive.thy \ |
25 Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \ |
25 Perm.thy Rel.thy EquivClass.thy Trancl.thy \ |
26 ../Pure/section_utils.ML ind_syntax.thy ind_syntax.ML \ |
26 WF.thy Order.thy Ordinal.thy Epsilon.thy Arith.thy Univ.thy \ |
27 add_ind_def.thy add_ind_def.ML \ |
27 QUniv.thy Datatype.thy OrderArith.thy OrderType.thy \ |
28 intr_elim.thy intr_elim.ML indrule.thy indrule.ML \ |
28 Cardinal.thy CardinalArith.thy Cardinal_AC.thy InfDatatype.thy \ |
29 Inductive.thy Inductive.ML \ |
29 Zorn.thy Nat.thy Finite.thy List.thy |
30 Perm.thy Perm.ML Rel.thy Rel.ML EquivClass.ML EquivClass.thy \ |
|
31 Trancl.thy Trancl.ML \ |
|
32 WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \ |
|
33 Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ |
|
34 QUniv.thy QUniv.ML constructor.ML Datatype.thy Datatype.ML \ |
|
35 OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \ |
|
36 Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \ |
|
37 Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \ |
|
38 Zorn.thy Zorn.ML Nat.thy Nat.ML Finite.thy Finite.ML \ |
|
39 List.thy List.ML |
|
40 |
30 |
41 IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\ |
31 FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML $(THYS) $(THYS:.thy=.ML) |
42 IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy |
32 |
43 |
|
44 EX_FILES = ex/ROOT.ML ex/misc.ML ex/Ramsey.ML ex/Ramsey.thy\ |
|
45 ex/Integ.ML ex/Integ.thy\ |
|
46 ex/twos_compl.thy ex/twos_compl.ML ex/Bin.thy ex/Bin.ML\ |
|
47 ex/BT.thy ex/BT.ML ex/Term.thy ex/Term.ML \ |
|
48 ex/TF.thy ex/TF.ML ex/Ntree.thy ex/Ntree.ML \ |
|
49 ex/Brouwer.thy ex/Brouwer.ML \ |
|
50 ex/Data.thy ex/Data.ML ex/Enum.thy ex/Enum.ML \ |
|
51 ex/Rmap.thy ex/Rmap.ML ex/PropLog.ML ex/PropLog.thy \ |
|
52 ex/ListN.thy ex/ListN.ML ex/Acc.thy ex/Acc.ML\ |
|
53 ex/Comb.thy ex/Comb.ML ex/Primrec.thy ex/Primrec.ML\ |
|
54 ex/LList.thy ex/LList.ML ex/CoUnit.thy ex/CoUnit.ML |
|
55 |
33 |
56 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
34 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
57 $(BIN)/ZF: $(BIN)/FOL $(FILES) |
35 $(BIN)/ZF: $(BIN)/FOL $(FILES) |
58 case "$(COMP)" in \ |
36 case "$(COMP)" in \ |
59 poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
37 poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
60 echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\ |
38 echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\ |
61 sml*) echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\ |
39 sml*) echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\ |
62 *) echo Bad value for ISABELLECOMP: \ |
40 *) echo Bad value for ISABELLECOMP: \ |
63 $(COMP) is not poly or sml;;\ |
41 $(COMP) is not poly or sml; exit 1;;\ |
64 esac |
42 esac |
65 |
43 |
66 $(BIN)/FOL: |
44 $(BIN)/FOL: |
67 cd ../FOL; $(MAKE) |
45 cd ../FOL; $(MAKE) |
68 |
46 |
69 #Directory IMP also tests the system |
47 #### Testing of ZF |
70 #Load ex/ROOT.ML last since it creates the file "test" |
48 |
71 test: $(BIN)/ZF $(IMP_FILES) $(EX_FILES) |
49 #A macro referring to the object-logic (depends on ML compiler) |
72 case "$(COMP)" in \ |
50 LOGIC:sh=case $ISABELLECOMP in \ |
73 poly*) echo '(use"IMP/ROOT.ML"; use"ex/ROOT.ML"); quit();' | \ |
51 poly*) echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\ |
74 $(COMP) $(BIN)/ZF ;;\ |
52 sml*) echo "$ISABELLEBIN/ZF" ;;\ |
75 sml*) echo '(use"IMP/ROOT.ML"; use"ex/ROOT.ML");' | $(BIN)/ZF;;\ |
53 *) echo "echo Bad value for ISABELLECOMP: \ |
76 *) echo Bad value for ISABELLECOMP: \ |
54 $ISABELLEBIN is not poly or sml; exit 1" ;;\ |
77 $(COMP) is not poly or sml;;\ |
|
78 esac |
55 esac |
79 |
56 |
|
57 ##IMP-semantics example |
|
58 IMP_THYS = IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy |
|
59 IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML) |
|
60 |
|
61 IMP: $(BIN)/ZF $(IMP_FILES) |
|
62 echo 'use"IMP/ROOT.ML";quit();' | $(LOGIC) |
|
63 |
|
64 ##Coinduction example |
|
65 COIND_THYS = Coind/ECR.thy Coind/Language.thy\ |
|
66 Coind/MT.thy Coind/Map.thy Coind/Static.thy \ |
|
67 Coind/Types.thy Coind/Values.thy |
|
68 |
|
69 COIND_FILES = Coind/ROOT.ML Coind/BCR.thy Coind/Dynamic.thy \ |
|
70 $(COIND_THYS) $(COIND_THYS:.thy=.ML) |
|
71 |
|
72 Coind: $(BIN)/ZF $(COIND_FILES) |
|
73 echo 'use"Coind/ROOT.ML";quit();' | $(LOGIC) |
|
74 |
|
75 ##Miscellaneous examples |
|
76 EX_THYS = ex/Ramsey.thy ex/Integ.thy ex/twos_compl.thy ex/Bin.thy \ |
|
77 ex/BT.thy ex/Term.thy ex/TF.thy ex/Ntree.thy \ |
|
78 ex/Brouwer.thy ex/Data.thy ex/Enum.thy \ |
|
79 ex/Rmap.thy ex/PropLog.thy ex/ListN.thy ex/Acc.thy \ |
|
80 ex/Comb.thy ex/Primrec.thy ex/LList.thy ex/CoUnit.thy |
|
81 EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
|
82 |
|
83 #Test ZF by loading the examples in directory ex |
|
84 ex: $(BIN)/ZF $(EX_FILES) |
|
85 echo 'use"ex/ROOT.ML";quit();' | $(LOGIC) |
|
86 |
|
87 #Full test. |
|
88 test: $(BIN)/ZF IMP Coind ex |
|
89 echo 'Test examples ran successfully' > test |
|
90 |
80 .PRECIOUS: $(BIN)/FOL $(BIN)/ZF |
91 .PRECIOUS: $(BIN)/FOL $(BIN)/ZF |