Theory Java2Jinja

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

section ‹Setup for converter Java2Jinja›

theory Java2Jinja 

  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
  purge run = 
  lmap (λobs. case obs of ExternalCall _ _ (Cons (Intg i) _) v  i)
    (λ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

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_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

  wf_J_prog' exec_J_rr exec_J_rnd 
  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"

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