summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKai Stevenson <kai@kaistevenson.com>2023-06-12 03:19:31 -0700
committerKai Stevenson <kai@kaistevenson.com>2023-06-12 03:19:31 -0700
commit88a8012eeb81be74a6bcaccfc514fd134a85c71a (patch)
tree5f0cfdc75f058588f69ae9af1d87f8f9e8f15748
parent43bfe5935b3f1d38775c3bc65262aca5683c0fb5 (diff)
added some comments, added a license and a readme
-rw-r--r--LICENSE2
-rw-r--r--README7
-rw-r--r--parse.c3
-rw-r--r--proposition.c2
4 files changed, 14 insertions, 0 deletions
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..d2aaaae
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,2 @@
+Copyright 2023 Kai Stevenson
+All rights reserved
diff --git a/README b/README
new file mode 100644
index 0000000..566a01c
--- /dev/null
+++ b/README
@@ -0,0 +1,7 @@
+Kai Stevenson
+Canonical project is at git.aberrantflux.xyz/operetta.git
+
+Operetta is a formal logic interpreter and solver.
+Formal logic is not so different from a programming language. This project was an opportunity for me
+to refine the techniques developed in Precedent. This time, I implemented a lexer loosely inspired by
+the one used in NoExcess.
diff --git a/parse.c b/parse.c
index d7ec467..d26cfe8 100644
--- a/parse.c
+++ b/parse.c
@@ -50,6 +50,7 @@ line_t parse_line(char* content) {
}
prop_t parse_proposition(tokenSet_t tokenSet, int* seek) {
prop_t prop;
+ /* recurse to parse the parenthetical as its own proposition */
if (tokenSet.tokens[*seek].type == OPEN_PAREN) {
(*seek)++;
prop = parse_proposition(tokenSet, seek);
@@ -63,6 +64,7 @@ prop_t parse_proposition(tokenSet_t tokenSet, int* seek) {
return prop;
}
else {
+ /* the proposition we just read had a relation, so find the related proposition */
tokenType_t rel = tokenSet.tokens[*seek].type;
(*seek)++;
prop_t* prop1p = malloc(sizeof(prop_t));
@@ -80,6 +82,7 @@ just_t parse_justification(tokenSet_t tokenSet) {
}
justRule_t just;
int* references = malloc(sizeof(int) * (tokenSet.count - 2));
+ /* check the relation, then use a ternary operator for elim/intro */
switch (tokenSet.tokens[0].type) {
case CONJUNCTION:
just = tokenSet.tokens[1].type == ELIMINATION ? CONJUNCT_ELIM : CONJUNCT_INTRO;
diff --git a/proposition.c b/proposition.c
index 76ae4cd..2c1410c 100644
--- a/proposition.c
+++ b/proposition.c
@@ -1,4 +1,5 @@
#include "proposition.h"
+/* a proposition defines a relation between two propositions */
prop_t init_prop(prop_t* propA, prop_t* propB, tokenType_t relation) {
prop_t prop;
prop.propA = propA;
@@ -6,6 +7,7 @@ prop_t init_prop(prop_t* propA, prop_t* propB, tokenType_t relation) {
prop.relation = relation;
return prop;
}
+/* a simple proposition is one with only a name */
prop_t init_simple_prop(char* name) {
prop_t prop;
prop.name = name;