Theory Examples_On_Code_Generation

theory Examples_On_Code_Generation
imports 
 "Gauss_Jordan_IArrays"
 "Code_Real_Approx_By_Float_Addenda"
 "Code_Bit"
begin


definition iarray_of_iarray_to_list_of_list :: "'a iarray iarray => 'a list list"
  where "iarray_of_iarray_to_list_of_list A = map IArray.list_of (map (op !! A) [0..<IArray.length A])"

definition "matrix_z2=IArray[IArray[0,1], IArray[1,1::bit]]"
definition "matrix_rat=IArray[IArray[0,1], IArray[1,-2::rat]]"
definition "matrix_real=IArray[IArray[0,1], IArray[1,-2::real]]"


export_code matrix_z2 
  in SML module_name "matrix_z2" file "matrix_z2.sml"

export_code matrix_rat 
  in SML module_name "matrix_rat" file "matrix_rat.sml"

export_code matrix_real
  in SML module_name "matrix_real" file "matrix_real.sml"

definition "print_result_Gauss A = iarray_of_iarray_to_list_of_list (Gauss_Jordan_iarrays A)"
definition "print_rank A = rank_iarray A"

definition "print_result_z2 = print_result_Gauss (matrix_z2)"
definition "print_result_rat = print_result_Gauss (matrix_rat)"
definition "print_result_real = print_result_Gauss (matrix_real)"

definition "print_rank_z2 = print_rank (matrix_z2)"
definition "print_rank_rat = print_rank (matrix_rat)"
definition "print_rank_real = print_rank (matrix_real)"

export_code 
  print_rank_real
  print_rank_rat
  print_rank_z2
  print_result_real
  print_result_rat
  print_result_z2
  in SML module_name "GJ_GENERATED_CODE" file "GJ_GENERATED_CODE.sml"

end