Commit a0cbdd5b authored by Simon Prucker's avatar Simon Prucker
Browse files

Skeleton for Lexer and Parser for Formulae

parent 32e32855
Pipeline #15994 waiting for manual action with stages
in 41 seconds
{
exception Error of string
}
let al = ['a'-'z''A'-'Z']
let num = ['0'-'9']
let alnum = (al|num)+
let id = ['a'-'z'](alnum)+
let nat0 = num+
rule lex = parse
| [' ' '\t']+ {lex lexbuf}
| '\n' {Lexing.new_line lexbuf ; lex lexbuf}
| "=>" {FormulaParser.Implies}
| "/\\" {FormulaParser.And}
| "\\/" {FormulaParser.Or}
| "<=>" {FormulaParser.Equiv}
| '<' {FormulaParser.DiaOpen}
| '>' {FormulaParser.DiaClose}
| '[' {FormulaParser.BoxOpen}
| ']' {FormulaParser.BoxClose}
| '(' {FormulaParser.LBrace}
| ')' {FormulaParser.RBrace}
| '{' {FormulaParser.CLBrace}
| '}' {FormulaParser.CRBrace}
| id as s {FormulaParser.Identifyer s}
| nat0 as n {FormulaParser.Nat0 (int_of_string n)}
| eof {FormulaParser.EOF}
\ No newline at end of file
module CF = CoAlgFormula
%{
%}
%token And
%token Or
%token Not
%token Implies
%token Equiv
%token DiaOpen
%token BoxOpen
%token DiaClose
%token BoxClose
%token True
%token False
%token CLBrace (*Curly Left Brace*)
%token CRBrace
%token RBrace
%token LBrace
%token <string> Identifyer
%token <int> Nat0
%token EOF
%start <CoAlgFormula.formula> formula
%%
formula:
| LBrace a = prec0 RBrace EOF {a}
prec0:
| a = prec1 Equiv b = prec0 {CF.formula.EQU (a, b)}
| a = prec1 Implies b = prec0 {CF.formula.IMP (a, b)}
| a = prec1 {a}
| LBrace a = prec0 RBrace {a}
prec1:
| a = prec2 Or b = prec1 {CF.formula.OR (a,b)}
| a = prec2 {a}
| LBrace a = prec0 RBrace {a}
prec2:
| a = prec3 And b = prec2 {CF.formula.AND (a,b)}
| a = prec2 {a}
| LBrace a = prec0 RBrace {a}
prec3:
| Not a = prec3 {CF.formula.NOT a}
| DiaOpen m = modalContent DiaClose a = prec3 {match m with
| (b, c) -> CF.formula.MORETHAN (b, c, a)
| x:int list -> CF.formula.ALLOWS (x, a)
| x -> CF.formula.EX (x, a)}
| BoxOpen m = modalContent BoxClose a = prec3 {match m with
| (b, c) -> CF.formula.MAXEXCEPT (b, c, a)
| x:int list -> CF.formula.ENFORCES (x, a)
| x -> CF.formula.AX (x, a)}
| a = prec4 {a}
| LBrace a = prec0 RBrace {a}
prec4:
| a = Identifyer {CF.formula.AP a}
| True {CF.formula.TRUE}
| False {CF.formula.FALSE}
| LBrace a = prec0 RBrace {a}
modalContent:
| {"unimod"}
| a = Identifyer {a}
| a = Nat0 b = Identifyer {(a, b)}
| CLBrace a = natSeq CRBrace {a}
natSeq:
| {[]}
| a = Nat0 b = natSeq {a :: b}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment