Theory Solver_Code

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
License: LGPL
*)

section ‹Generating Code for the Solver›

theory Solver_Code
  imports Algorithm
begin

external_file ‹src/Main.hs›

export_code solve checking Haskell ― ‹test whether Haskell code generation works›

export_code solve integer_of_nat nat_of_integer in Haskell module_name HLDE file_prefix generated

compile_generated_files ✐‹contributor Makarius›
  ‹code/generated/HLDE.hs›
  external_files ‹Main.hs› (in src)
  export_files ‹hlde› (exe)
  export_prefix ‹code/generated›
  where ‹fn dir =>
    let
      val exec = Generated_Files.execute dir;
      val _ =
        exec ‹Compilation› ("mv code/generated/HLDE.hs . && " ^
          File.bash_path \<^path>‹$ISABELLE_GHC› ^ " -o hlde Main.hs");

      val print_coeffs = enclose "[" "]" o commas o map string_of_int;
      fun print_hlde (xs, ys) =
        writeln (exec ‹Test› ("./hlde <<< '(" ^ print_coeffs xs ^ ", " ^ print_coeffs ys ^ ")'"));
    in print_hlde ([3, 5, 1], [2, 7]) end
›

end