Theory Java2Jinja

(*  Title:      JinjaThreads/Execute/Java2Jinja.thy
    Author:     Andreas Lochbihler
*)

section ‹Setup for converter Java2Jinja›

theory Java2Jinja 
imports
  Code_Generation
  ToString
begin

code_identifier
  code_module Java2Jinja ⇀ (SML) Code_Generation

definition j_Program :: "addr J_mb cdecl list ⇒ addr J_prog"
where "j_Program = Program"

export_code wf_J_prog' j_Program in SML file ‹JWellForm.ML› 

text ‹Functions for extracting calls to the native print method›

definition purge where
  "⋀run.
  purge run = 
  lmap (λobs. case obs of ExternalCall _ _ (Cons (Intg i) _) v ⇒ i)
  (lfilter
    (λobs. case obs of ExternalCall _ M (Cons (Intg i) Nil) _ ⇒ M = print | _ ⇒ False) 
    (lconcat (lmap (llist_of ∘ snd) (llist_of_tllist run))))"

text ‹Various other functions›

instantiation heapobj :: toString begin
primrec toString_heapobj :: "heapobj ⇒ String.literal" where
  "toString (Obj C fs) = sum_list [STR ''(Obj '', toString C, STR '', '', toString fs, STR '')'']"
| "toString (Arr T si fs el) = 
   sum_list [STR ''(['', toString si, STR '']'', toString T, STR '', '', toString fs, STR '', '', toString (map snd (rm_to_list el)), STR '')'']"
instance proof qed
end

definition case_llist' where "case_llist' = case_llist"
definition case_tllist' where "case_tllist' = case_tllist"
definition terminal' where "terminal' = terminal"
definition llist_of_tllist' where "llist_of_tllist' = llist_of_tllist"
definition thr' where "thr' = thr"
definition shr' where "shr' = shr"

definition heap_toString :: "heap ⇒ String.literal"
where "heap_toString = toString"

definition thread_toString :: "(thread_id, (addr expr × addr locals) × (addr ⇒f nat)) rbt ⇒ String.literal"
where "thread_toString = toString"

definition thread_toString' :: "(thread_id, addr jvm_thread_state' × (addr ⇒f nat)) rbt ⇒ String.literal"
where "thread_toString' = toString"

definition trace_toString :: "thread_id × (addr, thread_id) obs_event list ⇒ String.literal"
where "trace_toString = toString"

code_identifier
  code_module Cardinality ⇀ (SML) Set
| code_module Code_Cardinality ⇀ (SML) Set
| code_module Conditionally_Complete_Lattices ⇀ (SML) Set
| code_module List ⇀ (SML) Set
| code_module Predicate ⇀ (SML) Set
| code_module Parity ⇀ (SML) Bit_Operations
| type_class semiring_parity ⇀ (SML) Bit_Operations.semiring_parity
| class_instance int :: semiring_parity ⇀ (SML) Bit_Operations.semiring_parity_int
| class_instance int :: ring_parity ⇀ (SML) Bit_Operations.semiring_parity_int
| constant member_i_i ⇀ (SML) Set.member_i_i

export_code
  wf_J_prog' exec_J_rr exec_J_rnd 
  j_Program
  purge case_llist' case_tllist' terminal' llist_of_tllist'
  thr' shr' heap_toString thread_toString trace_toString
  in SML
  file ‹J_Execute.ML›

definition j2jvm :: "addr J_prog ⇒ addr jvm_prog" where "j2jvm = J2JVM"

export_code
  wf_jvm_prog' exec_JVM_rr exec_JVM_rnd j2jvm
  j_Program 
  purge case_llist' case_tllist' terminal' llist_of_tllist'
  thr' shr' heap_toString thread_toString' trace_toString
  in SML
  file ‹JVM_Execute2.ML›

end