The goal is to produce a tool that allows performing arbitrary operations on code, including:
- browsing
- refactoring
- correctness proofs
- literate programming
- version control
- automatic inlining and minimization
- peer review
Everything is stored in a graph database, allowing fine grained version control, hypertext navigation, and literate programming.
Text entry is syntax directed, meaning that code is stored internally as a graph structure, rather than just lines of text.
New code can be entered as text, but it is immediately parsed and converted to a graph structure.
Alternatively, text entry can be restricted to applications of syntactic production rules based on a formally defined grammar, also stored in the graph database.
Existing code can be modified in place according to predefined rules of inference, allowing code to be transformed or refined automatically while preserving or generalizing the semantics.
Each transformation step is also stored in the database, and sequences of transformations can serve as version control history or be presented as a proof of equivalence or implication between two expressions.
Once these tools are working, the system can be used to bootstrap its own replacement, where the entire system is formally proven and automatically verified from the first line of code.
- syndir.ijs
- (eventually) the main application
Various alternate implementations/attempts to be merged with above:
- graphdb.ijs
- simple graph database / triple store
- mvars.ijs
- helper for memory mapped variables (uses jmf)
- stringdb.ijs
- persistent key-value store (uses jfiles)
- boxed.ijs
- boxed token editor widget
- list.ijs
- list data type
- cursor.ijs
- cursor object
- proofed.ijs
- tree-centric syntax directed editor
- stype.ijs
- type inspection (redundant?)
- unify.ijs
- unification algorithm
- sx.ijs
- s-expressions
- parseco.ijs
- parser combinators
- dict.ijs
- in-memory key-value dictionaries
- rel.ijs
- relational programming (with syntax directed example)
PL/0 is a toy language designed by Niklaus Wirth for teaching compilers.
- pl0.sx
- pl/0 grammar as an s-expression.
- load-pl0.ijs
- load pl0.sx into jfdag database.
- pl0syntax.ijs
- unparse and pretty-print the pl0 grammar.
The old directory contains older prototype components,
and will likely be removed:
- unparse.ijs
- unparser/pretty-printer
- sx-by-hand.ijs
- handwritten s-expression parser
- boxer
- tree/stack builder based on boxes