; NOTE: We explcitly write 'bash ./mk_int_file.sh' instead of just
; calling the script so this works in native Windows. This is needed to
; even build a source package in Windows, since we ship exactly this
; dune file and script. We should consider just shipping the generated
; ML files, if there's a convenient way to do so.

; This one is special and hand-written... sigh
; (rule
;   (target FStar_UInt8.ml)
;   (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
;   (action (with-stdout-to %{target} (run bash ./mk_int_file.sh U 8))))

(rule
  (target FStar_UInt16.ml)
  (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh U 16))))

(rule
  (target FStar_UInt32.ml)
  (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh U 32))))

(rule
  (target FStar_UInt64.ml)
  (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh U 64))))

(rule
  (target FStar_Int8.ml)
  (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh S 8))))

(rule
  (target FStar_Int16.ml)
  (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh S 16))))

(rule
  (target FStar_Int32.ml)
  (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh S 32))))

(rule
  (target FStar_Int64.ml)
  (deps (:script mk_int_file.sh) (:body FStar_Ints.ml.body))
  (action (with-stdout-to %{target} (run bash ./mk_int_file.sh S 64))))
