I only handled the half of the definition which handles the representation of formulas. The representation of rewrite rules will come next. To test this (without properly testing it), I also implemented the Interpreter and AST interfaces which allows us to parse into a AST String, from which point we could possibly change the underlying type of the AST to some AST a and then generically interpret that AST as a formula of a given logic system (e.g. PropositionalLogic). It should be decently modular, although a lot of the code that would take advantage of that modularity (e.g. fmap for ASTs) has not yet been written.
I only handled the half of the definition which handles the representation of formulas. The representation of rewrite rules will come next. To test this (without properly testing it), I also implemented the
InterpreterandASTinterfaces which allows us to parse into aAST String, from which point we could possibly change the underlying type of the AST to someAST aand then genericallyinterpretthat AST as a formula of a given logic system (e.g.PropositionalLogic). It should be decently modular, although a lot of the code that would take advantage of that modularity (e.g.fmapforASTs) has not yet been written.resolves #5 (partially - rewrite rules coming later)