-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathFormulaParser.ts
More file actions
199 lines (181 loc) · 5.54 KB
/
FormulaParser.ts
File metadata and controls
199 lines (181 loc) · 5.54 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
/*
Formula parser
Copyright (C) 2025 Andreas Kovalski
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
enum NonVariableToken {
LeftParen = "(",
RightParen = ")",
Ampersand = "&",
Line = "|",
Minus = "-",
Arrow = "->",
Truth = "T",
Falsity = "F",
}
type Token = VariableText | NonVariableToken
function parseFormula(formulaText : string) : Formula{
/**
* Lexer for propositional formulas
*
* @param formulaText A string of a propositional formula
* @returns A list of tokens contained in {@link formulaText}
*
*/
function scan(formulaText : string) : Token[]{
let tokens : Token[] = []
let formula = ""
let currentCharIndex = 0
function atEnd() {
return currentCharIndex >= formula.length
}
function advance(){
return formula[currentCharIndex++]
}
function peek(){
return atEnd() ? '\0': formula[currentCharIndex]
}
function variable(){
let varName = ""
while(!atEnd() && isVariableText(peek()))
varName += advance()
return varName
}
tokens = []
formula = formulaText
currentCharIndex = 0
while(!atEnd()){
let char : string
switch(char = advance()){
case " ":
case "\t":
break;
case "(":
tokens.push(NonVariableToken.LeftParen)
break;
case ")":
tokens.push(NonVariableToken.RightParen)
break;
case "-":
if(peek() == ">"){
tokens.push(NonVariableToken.Arrow)
advance()
}
else
tokens.push(NonVariableToken.Minus)
break;
case "&":
tokens.push(NonVariableToken.Ampersand)
break;
case "|":
tokens.push(NonVariableToken.Line)
break;
case "T":
if(!isVariableText(peek()))tokens.push(NonVariableToken.Truth)
else tokens.push("" + char + variable())
break;
case "F":
if(!isVariableText(peek()))tokens.push(NonVariableToken.Falsity)
else tokens.push("" + char + variable())
break;
default:
if(isVariableText(char))
tokens.push("" + char + variable())
else throw new Error("Found unexpected character '" + char + "' in formula " + formulaText)
}
}
return tokens
}
/*
Grammar for parsing formulas using recursive descent
Formula -> Impl
Impl -> Or (Arrow Or)*
Or -> And (Line And)*
And -> Neg Ampersand Neg
Neg -> (Minus)? Primary
Primary -> Truth | Falsity | "(" Formula ")" | Variable
*/
/**
* A parser for propositional logic
* parses a list of tokens created by {@link scan}
*
* @param tokens list of tokens in order
* @returns An {@link https://en.wikipedia.org/wiki/Abstract_syntax_tree | AST} of the formula
*/
const parse = function(tokens : Token[]){
let currentTokenIndex = 0
const formula = () => implication()
function implication() : Formula{
let left = disjunction()
while(match(NonVariableToken.Arrow)){
const right = disjunction()
left = new Implication(left, right)
}
return left
}
function disjunction() : Formula{
let left = conjunction()
while(match(NonVariableToken.Line)){
const right = conjunction()
left = new Disjunction(left, right)
}
return left
}
function conjunction() : Formula{
let left = negation()
while(match(NonVariableToken.Ampersand)){
const right = negation()
left = new Conjunction(left, right)
}
return left
}
function negation() : Formula{
if(match(NonVariableToken.Minus))
return new Negation(negation())
return primary()
}
function primary() : Formula{
let primary : Formula
if(match(NonVariableToken.Truth))
return Truth.create()
if(match(NonVariableToken.Falsity))
return Falsity.create()
if(match(NonVariableToken.LeftParen)){
primary = formula()
if(!match(NonVariableToken.RightParen))
throw new Error("An expression in brackets was not closed")
}
else if(isVariableText(peek())){
let name = advance() as string
return Variable.create(name)
}
else throw new Error("Expexted Expression, instead got '" + peek() + "'");
return primary
}
const atEnd = () => currentTokenIndex >= tokens.length
function advance() {
if(!atEnd())return tokens[currentTokenIndex++]
throw new Error("Can't advance: Already at end")
}
function match(token : Token){
if(atEnd() || peek() !== token)return false
advance()
return true
}
const peek = () => tokens[currentTokenIndex]
currentTokenIndex = 0
const formulaAST : Formula = formula()
if(!atEnd())console.error("Couldn't parse the entire expression, only '" + formulaAST.acceptVisitor(new FormulaPrinter()) + "'")
return formulaAST
}
return parse(scan(formulaText))
}