From 7a46dd920a60b18fca08c55ae1af2f320d300f50 Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Tue, 4 Apr 2017 09:43:27 +0200
Subject: [PATCH] Begin to implement LaTeX syntax parsing
---
src/lib/CoAlgFormula.ml | 11 ++++
src/lib/CoAlgFormula.mli | 2 +
src/lib/Latex.ml | 123 +++++++++++++++++++++++++++++++++++++++
3 files changed, 136 insertions(+)
create mode 100644 src/lib/Latex.ml
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 6472add..7d0c3b5 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -1925,6 +1925,17 @@ let const_choice f1 f2 = CHC (f1, f2)
*)
let const_fusion first f1 = FUS (first, f1)
+(** Constructs a MU formula.
+ @param var The bound variable
+ @param f The formula
+ @returns [mu var. f]*)
+let const_mu var f = MU (var, f)
+
+(** Constructs a NU formula.
+ @param var The bound variable
+ @param f The formula
+ @returns [nu var. f]*)
+let const_nu var f = NU (var, f)
(** Hash-consed formulae, which are in negation normal form,
such that structural and physical equality coincide.
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 3fb17ed..0a687b4 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -136,6 +136,8 @@ val const_enforces : int list -> formula -> formula
val const_allows : int list -> formula -> formula
val const_choice : formula -> formula -> formula
val const_fusion : bool -> formula -> formula
+val const_mu : string -> formula -> formula
+val const_nu : string -> formula -> formula
type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed
and hcFormula_node =
diff --git a/src/lib/Latex.ml b/src/lib/Latex.ml
new file mode 100644
index 0000000..7749df1
--- /dev/null
+++ b/src/lib/Latex.ml
@@ -0,0 +1,123 @@
+open MParser
+open CoAlgFormula
+
+let (<*) = (<<<)
+let ( *> ) = (>>>)
+
+let lexeme p = p <* spaces
+
+let varchar = alphanum <|> char '_'
+
+let skip_symbol str =
+ lexeme (string str >> not_followed_by varchar "superfluous character")
+
+let parens p = between (lexeme (char '(')) (lexeme (char ')')) p
+
+let infix sym f assoc = Infix (skip_symbol sym >> return f, assoc)
+let prefix sym f = Prefix (skip_symbol sym >> return f)
+
+let ptrue = skip_symbol "\\true" >> return TRUE
+let pfalse = skip_symbol "\\false" >> return FALSE
+
+let pname =
+ letter >>= fun start ->
+ many_chars varchar >>= fun rest ->
+ spaces >>
+ return (Char.escaped start ^ rest)
+
+let psym = pname |>> const_ap
+
+let maybe_brace_str =
+ (char '{' *> many1_chars varchar <* char '}')
+ <|> (varchar |>> Char.escaped)
+
+let pnominal =
+ let add_tick s = ("'" ^ s) in
+ lexeme (char '\'' >> many_chars varchar |>> add_tick |>> const_nom)
+
+let pat = string "@_" *> maybe_brace_str |>> const_at
+
+let pmu =
+ skip_symbol "\\mu" >>
+ pname >>= fun var ->
+ lexeme (char '.') >>$ const_mu var
+
+let k_modality constructor name =
+ string name >> (
+ (char '_' *> lexeme (maybe_brace_str |>> constructor))
+ <|> return (constructor ""))
+
+let diamond = lexeme (k_modality const_ex "\\Diamond")
+let box = lexeme (k_modality const_ax "\\Box")
+
+let operators =
+ [
+ [ prefix "\\neg" const_not ];
+ [ Prefix pat ];
+ [ Prefix diamond ];
+ [ Prefix box ];
+ [ infix "\\wedge" const_and Assoc_left ];
+ [ infix "\\vee" const_or Assoc_left ];
+ [ infix "\\implies" const_imp Assoc_right ];
+ [ infix "\\equiv" const_imp Assoc_right ];
+ [ Prefix pmu ];
+ ]
+
+let rec term s = (parens expr <|> ptrue <|> pfalse <|> pnominal <|> psym) s
+and expr s = expression operators term s
+
+let recurse_formula func formula =
+ match formula with
+ (* 0-ary constructors *)
+ | TRUE | FALSE | AP _ | VAR _ -> formula
+ | CONST _
+ | CONSTN _ -> formula
+ (* unary *)
+ | NOT a -> NOT (func a)
+ | AT (s,a) -> AT (s,func a)
+ (* binary *)
+ | OR (a,b) -> OR (func a, func b)
+ | AND (a,b) -> AND (func a, func b)
+ | EQU (a,b) -> EQU (func a, func b)
+ | IMP (a,b) -> IMP (func a, func b)
+ | EX (s,a) -> EX (s,func a)
+ | AX (s,a) -> AX (s,func a)
+ | ENFORCES (s,a) -> ENFORCES (s,func a)
+ | ALLOWS (s,a) -> ALLOWS (s,func a)
+ | MIN (n,s,a) -> MIN (n,s,func a)
+ | MAX (n,s,a) -> MAX (n,s,func a)
+ | ATLEASTPROB (p,a) -> ATLEASTPROB (p, func a)
+ | LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, func a)
+ | MORETHAN (n,s,a) -> MORETHAN (n,s,func a)
+ | MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,func a)
+ | ID(a) -> ID (func a)
+ | NORM(a, b) -> NORM(func a, func b)
+ | NORMN(a, b) -> NORMN(func a, func b)
+ | CHC (a,b) -> CHC (func a, func b)
+ | FUS (s,a) -> FUS (s, func a)
+ | MU (n, f1) -> MU (n, func f1)
+ | NU (n, f1) -> NU (n, func f1)
+ | AF f1 -> AF (func f1)
+ | EF f1 -> EF (func f1)
+ | AG f1 -> AG (func f1)
+ | EG f1 -> EG (func f1)
+ | AU (f1, f2) -> AU (func f1, func f2)
+ | EU (f1, f2) -> EU (func f1, func f2)
+ | AR (f1, f2) -> AR (func f1, func f2)
+ | ER (f1, f2) -> ER (func f1, func f2)
+ | AB (f1, f2) -> AB (func f1, func f2)
+ | EB (f1, f2) -> EB (func f1, func f2)
+
+let bound_check formula =
+ let rec replace_bound symtab formula =
+ match formula with
+ | AP name -> if List.mem name symtab then VAR name else AP name
+ | MU (var, _) | NU (var, _) -> recurse_formula (replace_bound (var::symtab)) formula
+ | _ -> recurse_formula (replace_bound symtab) formula
+ in
+ replace_bound [] formula
+
+let eval s =
+ match parse_string (expr <* eof) s () with
+ | Success x -> Some (bound_check x)
+ | Failed (msg,_) -> None
--
GitLab