doc-src/Tutorial/IsaMakefile
author nipkow
Thu, 12 Nov 1998 16:45:17 +0100
changeset 5850 9712294e60b9
parent 5621 1fe18aca1062
child 6099 d4866f6ff2f9
permissions -rw-r--r--
*** empty log message ***

#
# IsaMakefile for Tutorial
#

## targets

default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Misc


## global settings

SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log


## HOL

HOL:
	@cd $(SRC)/HOL; $(ISATOOL) make HOL


## HOL-Ifexpr

HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz

Ifexpr/Ifexpr.thy: Ifexpr/prolog Ifexpr/boolex Ifexpr/value Ifexpr/ifex \
  Ifexpr/valif Ifexpr/bool2if Ifexpr/normif Ifexpr/norm Ifexpr/normal \
  Ifexpr/end
	@cd Ifexpr; \
	cat prolog boolex value ifex valif bool2if normif norm normal \
	  end > Ifexpr.thy

$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
	@$(ISATOOL) usedir $(OUT)/HOL Ifexpr


## HOL-ToyList

HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz

ToyList/ToyList.ML: ToyList/autotac ToyList/addsimps2 ToyList/inductxs \
  ToyList/lemma1 ToyList/lemma2 ToyList/lemma3 \
  ToyList/qed1 ToyList/qed2 ToyList/qed3 ToyList/thm ToyList/qed
	cd ToyList; \
	cat lemma2 inductxs autotac qed2 addsimps2 lemma3 qed3 \
	    lemma1 inductxs autotac qed1 thm inductxs autotac qed > ToyList.ML

$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ToyList.ML \
  ToyList/ROOT.ML
	@$(ISATOOL) usedir $(OUT)/HOL ToyList

## HOL-CodeGen

HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz

CodeGen/CodeGen.thy: CodeGen/prolog CodeGen/expr CodeGen/value \
  CodeGen/instr CodeGen/exec CodeGen/comp CodeGen/end
	cd CodeGen; cat prolog expr value instr exec comp end > CodeGen.thy

$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy CodeGen/goal1.ML \
  CodeGen/goal2.ML CodeGen/simpsplit.ML CodeGen/ROOT.ML
	@$(ISATOOL) usedir $(OUT)/HOL CodeGen

## HOL-Datatype

HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz

Datatype/appmap.ML: Datatype/appmap
	cat Datatype/goal Datatype/appmap Datatype/semi > Datatype/appmap.ML

Datatype/ABexp.thy: Datatype/abprolog Datatype/abdata Datatype/abconstseval \
  Datatype/abevala Datatype/abevalb Datatype/abconstssubst Datatype/absubsta\
  Datatype/absubstb
	cd Datatype; cat abprolog abdata abconstseval abevala abevalb abconstssubst absubsta absubstb end > ABexp.thy

Datatype/Term.thy: Datatype/tprolog Datatype/mutnested Datatype/tdata \
  Datatype/tconstssubst Datatype/tsubst Datatype/tsubsts
	cd Datatype; cat tprolog mutnested tdata tconstssubst tsubst tsubsts end > Term.thy

Datatype/Trie.thy: Datatype/trieprolog Datatype/assoc Datatype/trie \
  Datatype/triesels Datatype/lookup Datatype/update
	cd Datatype; cat trieprolog assoc trie triesels lookup update end > Trie.thy

$(LOG)/HOL-Datatype.gz: $(OUT)/HOL \
  Datatype/ABexp.thy Datatype/Term.thy Datatype/Trie.thy \
  Datatype/ROOT.ML Datatype/abgoalind.ML Datatype/autotac.ML \
  Datatype/tidproof.ML Datatype/appmap.ML Datatype/lookupempty.ML \
  Datatype/trieAdds.ML Datatype/triemain.ML Datatype/trieinduct.ML Datatype/trieexhaust.ML
	@$(ISATOOL) usedir $(OUT)/HOL Datatype

## HOL-Misc

HOL-Misc: HOL $(LOG)/HOL-Misc.gz

Misc/Tree.thy: Misc/treeprolog Misc/tree Misc/end
	cd Misc; cat treeprolog tree end > Tree.thy

Misc/NatSum.thy: Misc/natsumprolog Misc/natsum Misc/end
	cd Misc; cat natsumprolog natsum end > NatSum.thy

Misc/Types.thy: Misc/typesprolog Misc/types Misc/end
	cd Misc; cat typesprolog types end > Types.thy

Misc/Defs.thy: Misc/defsprolog Misc/consts Misc/defs Misc/end
	cd Misc; cat defsprolog consts defs end > Defs.thy

Misc/ConstDefs.thy: Misc/constdefsprolog Misc/constdefs Misc/end
	cd Misc; cat constdefsprolog constdefs end > ConstDefs.thy

$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/exhaust.ML Misc/autotac.ML \
  Misc/Tree.thy Misc/NatSum.thy Misc/NatSum.ML Misc/Types.thy \
  Misc/Defs.thy Misc/ConstDefs.thy \
  Misc/Exor.thy Misc/exorgoal.ML Misc/exorproof.ML \
  Misc/splitif.ML Misc/splitlist.ML Misc/induct_auto.ML \
  Misc/Itrev.thy Misc/itrev1.ML Misc/itrev2.ML Misc/itrev3.ML
	@$(ISATOOL) usedir $(OUT)/HOL Misc


## clean

clean:
	@rm -f $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-Misc.gz