#include "share/atspre_staload.hats"
#include "share/HATS/atspre_staload_libats_ML.hats"

typedef cfun1 (a:t@ype, b:t@ype) = a -<cloref1> b
typedef cfun2 (a:t@ype, b:t@ype, c:t@ype) = (a,b) -<cloref1> c

// ----------------------------------------------------------------------
// ----------------------- INPUT ----------------------------------------
// ----------------------------------------------------------------------

abstype input_type = ptr
stadef input_t = input_type

extern fun create_input(content: string): input_t
extern fun avail_input(input: input_t, pos: size_t, nchars: size_t): bool
extern fun get_input(input: input_t, pos: size_t, nchars: size_t): string

local
  extern castfn string_2_input(content: string):<> input_t
  extern castfn input_2_string(input: input_t):<> string
in
  implement create_input(content) = string_2_input(content)

  implement avail_input(input, pos, nchars) = let
    val len = length(input_2_string(input))
  in nchars <= (len-pos) end

  implement get_input(input, pos, nchars) = let
    val ins = input_2_string(input)
  in string_make_substring(ins, pos, nchars) end
end

// -----------------------------------------------------------------------
// ----------------------- STATUS ----------------------------------------
// -----------------------------------------------------------------------

abstype status_type(a: t@ype) = ptr
stadef status_t = status_type

extern fun{a: t@ype} success_status(index: size_t, value: a): status_t(a)
extern fun{a: t@ype} value_status(status: status_t(a)): Option(a)
extern fun{a: t@ype} expected_status(status: status_t(a)): string
extern fun{a: t@ype} index_status(status: status_t(a)): size_t
extern fun{a: t@ype} flag_status(status: status_t(a)): bool
extern fun{a: t@ype} failure_status(index: size_t, expected: string): status_t(a)
extern fun{a: t@ype} print_status(status: status_t(a)): void
extern fun{a: t@ype} print_error_status(status: status_t(a)): void

local
  datatype status_dt(a: t@ype) =
    | Success of (size_t, a)
    | Failure of (size_t, string)

  assume status_type = status_dt
in
  implement{a} success_status(index, value) = Success{a}(index, value)
  implement{a} failure_status(index, expected) = Failure{a}(index, expected)

  implement{a} index_status(status) = case+ status of
    | Failure(index, _) => index
    | Success(index, _) => index

  implement{a} value_status(status) = case+ status of
    | Success(_, value) => option_some<a>(value)
    | Failure(_, _) => option_none<a>()

  implement{a} expected_status(status) = case+ status of
    | Failure(_, expected) => expected
    | Success(_, _) => ""

  implement{a} flag_status(status) = case+ status of
    | Failure(_, _) => false
    | Success(_, _) => true

  implement{a} print_error_status(status) = let
    val expected = expected_status<a>(status)
    val index = index_status<a>(status)
  in fprintln! (stderr_ref, "KO : ", index, " -> \"", expected, "\" expected") end
end

// -----------------------------------------------------------------------
// ----------------------- PARSER ----------------------------------------
// -----------------------------------------------------------------------

abstype parser_type(a: t@ype) = ptr
stadef parser_t = parser_type

extern fun{a: t@ype} create_parser(f: cfun2(input_t, size_t, status_t(a))): parser_t(a)
extern fun{a: t@ype} exec_parser(input: input_t, pos: size_t, parser: parser_t(a)): status_t(a)
extern fun{a: t@ype} parse(input: input_t, parser: parser_t(a)): status_t(a)
extern fun string_parser(value: string): parser_t(string)
extern fun{a: t@ype} seq_parser(parsers: list0(parser_t(a))): parser_t(list0(a))
extern fun{a, b: t@ype} fmap_parser(parser: parser_t(a), f: cfun1(a, b)): parser_t(b)

local
  datatype parser_dt(a: t@ype) =
    Parser of (cfun2(input_t, size_t, status_t(a)))
  assume parser_type = parser_dt

  datatype pair_dt(a: t@ype, b: t@ype) = 
    Pair of (a, b)

  datatype either_dt (a: t@ype, b: t@ype) =
    | Left(a,b) of (a)
    | Right(a,b) of (b)

  typedef seq_success_t(a: t@ype) = pair_dt(list0(a), size_t)
  typedef seq_fail_t(a: t@ype) = status_t(a)

  extern fun{a: t@ype} seq_ok(list: list0(a), index: size_t):
           either_dt(seq_success_t(a), seq_fail_t(a))
  extern fun{a: t@ype} seq_ko(status: status_t(a)):
           either_dt(seq_success_t(a), seq_fail_t(a))

in
  implement{a} create_parser(f) = Parser{a}(f)
  implement{a} exec_parser(input, pos, parser) = let
    val+Parser(f) = parser
  in f(input, pos) end
  implement{a} parse(input, parser) = exec_parser(input, i2sz(0), parser)

  implement string_parser(value) =
    create_parser<string>(lam(input, pos) =<cloref1> let
      val l = length(value)
    in if ~avail_input(input, pos, l) then
      failure_status<string>(pos, value)
    else let
        val s = get_input(input, pos, l)
      in
        if s = value then
          success_status<string>(pos+l, s)
        else
          failure_status<string>(pos, value)
      end
    end)

  implement{a} seq_ok(list, index) = Left{seq_success_t(a),seq_fail_t(a)}(Pair{list0(a), size_t}(list, index))
  implement{a} seq_ko(status) = Right{seq_success_t(a),seq_fail_t(a)}(status)

  implement{a} seq_parser(parsers) =
    create_parser<list0(a)>(lam(input, pos) =<cloref1> let
      fun{a: t@ype} loop(list: list0(parser_t(a)), index: size_t):
           either_dt(seq_success_t(a), seq_fail_t(a)) = case+ list of
        | list0_nil() => seq_ok<a>(list0_nil{a}(), index)
        | list0_cons(parser, tail) => let
          val status = exec_parser<a>(input, index, parser)
          val value = value_status<a>(status)
          val new_index = index_status<a>(status)
        in if option_is_some(value) then let
            val loop_rest = loop(tail, new_index)
          in case+ loop_rest of
            | Left(Pair(list, _)) => seq_ok<a>(list0_cons{a}(option_unsome<a>(value), list), new_index)
            | Right(status) => seq_ko<a>(status)
          end
          else seq_ko<a>(status)
        end 
      val result = loop<a>(parsers, pos)
    in case+ result of
         | Left(Pair(list, index)) => success_status<list0(a)>(index, list)
         | Right(status) => let
           val index = index_status(status)
           val expected = expected_status(status)
         in failure_status<list0(a)>(index, expected) end
    end)

  implement{a,b} fmap_parser(parser, f) =
    create_parser<b>(lam(input, pos) =<cloref1> let
      val status = exec_parser<a>(input, pos, parser)
      val index = index_status<a>(status)
      val value = value_status<a>(status)
    in if option_is_some(value) then
      success_status<b>(index, f(option_unsome(value)))
    else failure_status<b>(index, expected_status<a>(status)) end)
end

// -----------------------------------------------------------------------
// ----------------------- TEST ------------------------------------------
// -----------------------------------------------------------------------

extern fun test_ok(): void
extern fun test_ko(): void

local
in
  implement print_status<list0(string)>(status) = let
    implement fprint_val<string>(out, str) = let
      val () = fprint(out, "\"")
      val () = fprint(out, str)
    in fprint(out, "\"") end

    val value = value_status(status)
  in if option_is_some(value) then let
      val () = fprint_list0_sep(stdout_ref, option_unsome<list0(string)>(value), ", ")
    in fprint_newline(stdout_ref) end
  else print_error_status<list0(string)>(status) end

  implement test_ok() = let
    val s = create_input("hello hello !")
    val hello = string_parser("hello")
    val space = string_parser(" ")
    val l = list0_of_list($list{parser_t(string)}(hello, space, hello))
    val a = seq_parser<string>(l)

    val status = parse(s, a)
  in print_status(status) end

  implement test_ko() = let
    val s = create_input("hello world !")
    val hello = string_parser("hello")
    val space = string_parser(" ")
    val l = list0_of_list($list{parser_t(string)}(hello, space, hello))
    val a = seq_parser<string>(l)
    val status = parse(s, a)
  in print_status(status) end
end

extern fun test_ast(): void

local
  datatype ast_t =
    | String of (string)
    | Seq of (list0(ast_t))
  extern fun fprint_ast(out: FILEref, ast: ast_t): void
  extern fun fprint_list_ast(out: FILEref, ast_list: list0(ast_t)): void
in
  implement fprint_ast(out, ast) = case+ ast of
    | String(a_string) => fprint! (out, "String{\"", a_string, "\"}")
    | Seq(list) => let
      val () = fprint! (out, "Seq{")
      val () = fprint_list_ast(out, list)
    in fprint! (out, "}") end

  implement fprint_list_ast(out, ast_list) = let
    implement fprint_val<ast_t>(out, list) = fprint_ast(out, list)
  in fprint_list0_sep(out, ast_list, ", ") end

  implement print_status<ast_t>(status) = let
    val value = value_status(status)
  in if option_is_some(value) then let
      val () = fprint_ast(stdout_ref, option_unsome<ast_t>(value))
    in fprint_newline(stdout_ref) end
  else
    print_error_status<ast_t>(status)
  end

  implement test_ast() = let
    val input = create_input("hello hello !")
    val hello = fmap_parser<string, ast_t>(string_parser("hello"),
                    lam(str) =<cloref1> String(str))
    val space = fmap_parser<string, ast_t>(string_parser(" "),
                    lam(str) =<cloref1> String(str))
    val seq = fmap_parser<list0(ast_t), ast_t>(
                seq_parser<ast_t>(list0_of_list($list{parser_t(ast_t)}(hello, space, hello))),
                    lam(seq) =<cloref1> Seq(seq))
    val status = parse(input, seq)
  in print_status(status) end
end

implement main0() = let
  val () = test_ok()
  val () = test_ko()
  val () = test_ast()
in () end