# Theory Code_Export

```(*
Author:   Benedikt Seidl
*)

section ‹Code export to Standard ML›

theory Code_Export
imports
"LTL_to_DRA/DRA_Instantiation"
LTL.Code_Equations
"HOL-Library.Code_Target_Numeral"
begin

subsection ‹Hashing Sets›

global_interpretation comp_fun_commute "plus o cube o hashcode :: ('a :: hashable) ⇒ hashcode ⇒ hashcode"
by unfold_locales (auto simp: cube_def)

lemma [code]:
"hashcode (set xs) = fold (plus o cube o hashcode) (remdups xs) (uint32_of_nat (length (remdups xs)))"

lemma [code]:
"hashcode (abs_ltln⇩P φ) = hashcode (min_dnf φ)"
by simp

lemma min_dnf_rep_abs[simp]:
"min_dnf (Unf (rep_ltln⇩Q (abs_ltln⇩Q φ))) = min_dnf (Unf φ)"
using Quotient3_ltln⇩Q ltl_prop_equiv_min_dnf ltl_prop_unfold_equiv_def rep_abs_rsp by fastforce

lemma [code]:
"hashcode (abs_ltln⇩Q φ) = hashcode (min_dnf (Unf φ))"
by simp

subsection ‹LTL to DRA›

declare ltl_to_dra⇩P.af_letter⇩F_lifted_semantics [code]
declare ltl_to_dra⇩P.af_letter⇩G_lifted_semantics [code]
declare ltl_to_dra⇩P.af_letter⇩ν_lifted_semantics [code]

declare ltl_to_dra⇩Q.af_letter⇩F_lifted_semantics [code]
declare ltl_to_dra⇩Q.af_letter⇩G_lifted_semantics [code]
declare ltl_to_dra⇩Q.af_letter⇩ν_lifted_semantics [code]

definition atoms_ltlc_list_literals :: "String.literal ltlc ⇒ String.literal list"
where
"atoms_ltlc_list_literals = atoms_ltlc_list"

definition ltlc_to_draei_literals :: "equiv ⇒ String.literal ltlc ⇒ (String.literal set, nat) draei"
where
"ltlc_to_draei_literals = ltlc_to_draei"

definition sort_transitions :: "(nat × String.literal set × nat) list ⇒ (nat × String.literal set × nat) list"
where
"sort_transitions = sort_key fst"

export_code True_ltlc Iff_ltlc ltlc_to_draei_literals Prop PropUnfold
alphabetei initialei transitionei conditionei
integer_of_nat atoms_ltlc_list_literals sort_transitions set
in SML module_name LTL file_prefix LTL_to_DRA

subsection ‹LTL to NBA›

(* TODO *)

subsection ‹LTL to LDBA›

(* TODO *)

end
```