Theory MLTL_Language_Partition_Codegen

theory MLTL_Language_Partition_Codegen

imports MLTL_Language_Partition_Algorithm Show.Shows_Literal

begin

section ‹Pretty Parsing›

fun nat_to_string:: "nat ⇒ string" where 
"nat_to_string n = String.explode (Shows_Literal.showl n)"

fun mltl_to_literal_aux:: "nat mltl ⇒ string" where 
  "mltl_to_literal_aux True⇩m = ''true''"
| "mltl_to_literal_aux False⇩m = ''false''"
| "mltl_to_literal_aux (Prop⇩m (p)) = ''p''@(nat_to_string p)"
| "mltl_to_literal_aux (Not⇩m φ) = ''(!''@(mltl_to_literal_aux φ)@'')''"
| "mltl_to_literal_aux (φ And⇩m ψ) = ''('' @ (mltl_to_literal_aux φ) @ '' & '' @ (mltl_to_literal_aux ψ) @ '')''"
| "mltl_to_literal_aux (φ Or⇩m ψ) = ''('' @ (mltl_to_literal_aux φ) @ '' | '' @ (mltl_to_literal_aux ψ) @ '')''"
| "mltl_to_literal_aux (G⇩m [a,b] φ) = ''(G['' @ (nat_to_string a) @ '','' @ (nat_to_string b) @ ''] '' @ (mltl_to_literal_aux φ) @ '')''"
| "mltl_to_literal_aux (F⇩m [a,b] φ) = ''(F['' @ (nat_to_string a) @ '','' @ (nat_to_string b) @ ''] '' @ (mltl_to_literal_aux φ) @ '')''"
| "mltl_to_literal_aux (φ R⇩m [a,b] ψ) = ''('' @ (mltl_to_literal_aux φ) @ '' R['' @ (nat_to_string a) @ '','' @ (nat_to_string b) @ ''] '' @ (mltl_to_literal_aux ψ) @ '')''"
| "mltl_to_literal_aux (φ U⇩m [a,b] ψ) = ''('' @ (mltl_to_literal_aux φ) @ '' U['' @ (nat_to_string a) @ '','' @ (nat_to_string b) @ ''] '' @ (mltl_to_literal_aux ψ) @ '')''"

fun mltl_to_literal:: "nat mltl ⇒ String.literal"
  where "mltl_to_literal φ = String.implode (mltl_to_literal_aux φ)"

value "mltl_to_literal ((Prop⇩m (3) And⇩m True⇩m) U⇩m[3,4] False⇩m) = 
       STR ''((p3 & true) U[3,4] false)''"

section "Code Export"

export_code LP_mltl mltl_to_literal in Haskell module_name LP_mltl

end