diff options
Diffstat (limited to 'lib/parsing/headers.ml')
| -rw-r--r-- | lib/parsing/headers.ml | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/lib/parsing/headers.ml b/lib/parsing/headers.ml new file mode 100644 index 0000000..8d63381 --- /dev/null +++ b/lib/parsing/headers.ml @@ -0,0 +1,74 @@ +(* Useful types for parsing *) + +open Types + +exception Parse_Error of string + +type terminal = tok + +type nonterminal = S | E | E' | F | F' | G | G' | H | H' | I + +type symbol = Nt of nonterminal | Tm of terminal + +type production = nonterminal * (symbol list) + +(* possible actions to take when LL parsing *) +type action = + | PREDICT of production + | MATCH of tok + | ACCEPT + | REJECT + +(* takes in top stack symbol and the next input token and selects action to take *) +type table = symbol -> tok -> action + +(* mutable abstract syntax tree *) +type ast = + | Br of symbol * (ast ref) list + | Lf of symbol + +(* parsing state *) +type state = { + stack : symbol list; + ast_stack : ast ref list; (* list of ast refs corresponding to symbols on the stack *) + input : tok list; + finished : bool; + accepted : bool +} + +(* convert ast to proposition *) +let rec prop_of_ast (tree : ast) : proposition = + match tree with + | Lf (Tm TRUE) -> True + | Lf (Tm FALSE) -> False + | Lf (Tm (LIT s)) -> Lit s + | Br (Nt S, e_ref :: _) -> prop_of_ast !e_ref + | Br (Nt I, _ :: e_ref :: _ :: _) -> prop_of_ast !e_ref (* I ::= LEFT_PAREN E RIGHT_PAREN *) + | Br (Nt I, _ :: i_ref :: _) -> let inner_prop = prop_of_ast !i_ref in Not(inner_prop) (* I ::= NOT I *) + | Br (Nt I, [some_ref]) -> (* I ::= TRUE | FALSE | LIT s *) + begin + match !some_ref with + | Lf (Tm TRUE) -> True + | Lf (Tm FALSE) -> False + | Lf (Tm (LIT s)) -> Lit s + | _ -> failwith "some bug" + end + | Br (Nt a, b_ref :: a'_ref :: _) -> (* A ::= B A' *) + begin + match !a'_ref with + | Lf _ -> prop_of_ast !b_ref (* A' ::= eps *) + | Br (_, _ :: tl) -> (* A' ::= CONNECTOR B A' *) + let left = prop_of_ast !b_ref in + let right = prop_of_ast (Br(Nt a, tl)) in + begin + match a with + | E -> Iff(left, right) + | F -> Implies(left, right) + | G -> Or(left, right) + | H -> And(left, right) + | _ -> failwith "a bug!" + end + | _ -> failwith "another bug" + end + | _ -> failwith "found a bug!" +
\ No newline at end of file |