-
Notifications
You must be signed in to change notification settings - Fork 0
Source Code Commentary
The purpose of this document is to describe the structure of the code and help new developers understand how it all hangs together.
Except that their are certain external libraries that we distribute with K in the lib/java folder.
Everything is in the org.kframework package.
Initial start up code is in: o.k.main
However that just dispatches to the individual programs which are in the following packages: kagreg/ kast/ kcheck/ kompile/ krun/ ktest/ ktest2/
This leaves the following general utility packages: backend/ compile/ kil/ parser/ utils/
The K framework contains several programs such as kompile, krun and ktest (there are others, but these are the main ones). However, all of these programs are just scripts that call into the k3.jar with different flags to indicate which mode we are running in. All of these programs call org.kframework.main.Main.main(String[]). That function in turn checks dispatches to the real main function for each of these programs depending on the value of the command line argument.
org.kframework.kompile.KompileFrontEnd.kompile(args2); org.kframework.kagreg.KagregFrontEnd.kagreg(args2); org.kframework.kcheck.KCheckFrontEnd.kcheck(args2); org.kframework.ktest.KTest.test(args2); org.kframework.kast.KastFrontEnd.kast(args2); org.kframework.krun.Main.execute_Krun(args2); org.kframework.krun.ioserver.main.MainServer.main(args2); org.kframework.ktest2.KTest.main(args2);
org.kframework.main.Kpp.codeClean(args2); org.kframework.main.KPretty.main(args2);
FirstStep and LastStep (move to o.k.compile.utils?) OptionsParser (dead?) Kpp (program) KPretty (program)