ashalkhakov/shuntingyard.dats

## shuntingyard.dats
#include
"share/atspre_staload.hats"

(* ****** ****** *)
(* operator interface *)

datatype assoc = ASSOCnone | ASSOCleft | ASSOCright
extern
fun
eq_assoc_assoc (assoc, assoc):<> bool
overload = with eq_assoc_assoc
extern
fun
ne_assoc_assoc (assoc, assoc):<> bool
overload <> with ne_assoc_assoc

abstype operator = ptr
extern
fun
operator_make (label: string, a: assoc, precedence: Nat): operator
extern
fun
operator_label (operator): string
extern
fun
operator_prec (operator): Nat
extern
fun
operator_assoc (operator): assoc
extern
fun
operator_fprint (FILEref, operator): void

(* ****** ****** *)
// operator implementation

local

// need a hash table (string->operator info)
// need methods for populating it
datatype OPERATOR = OPERATOR of (string, assoc, Nat)
assume operator = OPERATOR

in

implement
eq_assoc_assoc (l, r) =
  case+ (l, r) of
  | (ASSOCnone (), ASSOCnone ()) => true
  | (ASSOCleft (), ASSOCleft ()) => true
  | (ASSOCright (), ASSOCright ()) => true
  | (_, _) => false

implement
ne_assoc_assoc (l, r) = ~(eq_assoc_assoc (l, r))

implement
operator_make (label, a, p) = OPERATOR (label, a, p)

implement
operator_label (o) = let
  val+ OPERATOR (lab, _, _) = o
in
  lab
end

implement
operator_prec (o) = let
  val+ OPERATOR (lab, a, p) = o
in
  p
end

implement
operator_assoc (o) = let
  val+ OPERATOR (lab, a, p) = o
in
  a
end

implement
operator_fprint (out, o) = {
  val+ OPERATOR (lab, a, p) = o
  (*
  val s =
    (case+ a of
    | ASSOCnone () => "no"
    | ASSOCleft () => "lf"
    | ASSOCright () => "rg"): string
  *)
  val () = fprint!(out, lab)
  (*
  val () = fprint!(out, "(")
  val () = fprint!(out, s)
  val p = (g0ofg1)p
  val () = fprint!(out, ",", p, ")")
  *)
}

end

(* FIXME: HACK *)
overload fprint with operator_fprint

(* ****** ****** *)
(* token interface *)

%{^

typedef enum {
    NIL = 0,
    OPER = 1,
    NUMBER = 2,
    COMMA = 3,
    LPAR = 4,
    RPAR = 5,
    FUNCALL = 6
} CTOKEN_ENUM;
typedef struct {
  CTOKEN_ENUM tt;
  union {
      atstype_boxed oper;
      int num;
  } tv;
} CTOKEN_TYPE;

ATSinline()
CTOKEN_TYPE TOKEN_NUMBER(atstype_int x) {
  CTOKEN_TYPE res;
  res.tt = NUMBER;
  res.tv.num = x;
  return res;
}
ATSinline()
CTOKEN_TYPE TOKEN_LPAR() {
    CTOKEN_TYPE res;
    res.tt = LPAR;
    return res;
}
ATSinline()
CTOKEN_TYPE TOKEN_RPAR() {
    CTOKEN_TYPE res;
    res.tt = RPAR;
    return res;
}
ATSinline()
CTOKEN_TYPE TOKEN_OPERATOR(atstype_boxed oper) {
    CTOKEN_TYPE res;
    res.tt = OPER;
    res.tv.oper = oper;
    return res;
}

ATSinline()
atstype_bool TOK_IS_OPER (CTOKEN_TYPE tok) {
    return tok.tt == OPER ? atsbool_true : atsbool_false;
}
ATSinline()
atstype_bool TOK_IS_NUMBER(CTOKEN_TYPE tok) {
    return tok.tt == NUMBER ? atsbool_true : atsbool_false;
}
ATSinline()
atstype_bool TOK_IS_COMMA(CTOKEN_TYPE tok) {
    return tok.tt == COMMA ? atsbool_true : atsbool_false;
}
ATSinline()
atstype_bool TOK_IS_LPAR(CTOKEN_TYPE tok) {
    return tok.tt == LPAR ? atsbool_true : atsbool_false;
}
ATSinline()
atstype_bool TOK_IS_RPAR(CTOKEN_TYPE tok) {
    return tok.tt == RPAR ? atsbool_true : atsbool_false;
}
ATSinline()
atstype_bool TOK_IS_FUNCALL(CTOKEN_TYPE tok) {
    return tok.tt == FUNCALL ? atsbool_true : atsbool_false;
}
ATSinline()
atstype_int TOK_GET_NUMBER (CTOKEN_TYPE tok) {
    return tok.tv.num;
}
ATSinline()
atstype_boxed TOK_GET_OPERATOR (CTOKEN_TYPE tok) {
    return tok.tv.oper;
}

%}

#define OPER 1
#define NUMBER 2
#define COMMA 3
#define LPAR 4
#define RPAR 5
#define FUNCALL 6

abst@ype token (int) = $extype"CTOKEN_TYPE"
typedef Token = [tag:int] token(tag)

extern
fun
token_number (int): token (NUMBER) = "ext#TOKEN_NUMBER"
extern
fun
token_lpar (): token (LPAR) = "ext#TOKEN_LPAR"
extern
fun
token_rpar (): token (RPAR) = "ext#TOKEN_RPAR"
extern
fun
token_operator (operator): token (OPER) = "ext#TOKEN_OPERATOR"


extern
fun
token_is_operator {i:int} (token(i)): bool(i==OPER) = "ext#TOK_IS_OPER"
extern
fun
token_is_number {i:int} (token(i)): bool(i==NUMBER) = "ext#TOK_IS_NUMBER"
extern
fun
token_is_comma {i:int} (token(i)): bool(i==COMMA) = "ext#TOK_IS_COMMA"
extern
fun
token_is_lpar {i:int} (token(i)): bool(i==LPAR) = "ext#TOK_IS_LPAR"
extern
fun
token_is_rpar {i:int} (token(i)): bool(i==RPAR) = "ext#TOK_IS_RPAR"
extern
fun
token_is_funcall {i:int} (token(i)): bool(i==FUNCALL) = "ext#TOK_IS_FUNCALL"
extern
fun
token_get_number (token(NUMBER)): int = "ext#TOK_GET_NUMBER"
extern
fun
token_get_operator (token(OPER)): operator = "ext#TOK_GET_OPERATOR"

extern
fun
token_fprint (out: FILEref, Token): void
overload fprint with token_fprint
extern
fun
token_print (Token): void
overload print with token_print

(* ****** ****** *)
(* token implementation *)

implement
token_fprint (out, tok) =
  if token_is_operator (tok) then {
    val oper = token_get_operator (tok)
    val () = fprint!(out, oper)
  } else if token_is_number (tok) then {
    val num = token_get_number (tok)
    val () = fprint!(out, num)
  } else if token_is_comma (tok) then {
    val () = fprint!(out, ",")
  } else if token_is_lpar (tok) then {
      val () = fprint!(out, "(")
  } else if token_is_rpar (tok) then {
      val () = fprint!(out, ")")
  }
  else fprint!(out, "NIL()")

implement
token_print (tok) = token_fprint (stdout_ref, tok)

(* ****** ****** *)

(* will not return a token if EOF *)
extern
fun{}
tokenizer_get_token (&Token? >> opt (Token, b)): #[b:bool] bool b
extern
fun{}
tokenizer_emit_token (&Token): void

extern
fun{}
shunting_yard (): void

staload "libats/SATS/stkarray.sats"
staload _(*anon*) = "libats/DATS/stkarray.dats"

extern
fun{a:t@ype}
stkarray_peek_top
  {m,n:int | n > 0}
(
  stk: !stkarray (INV(a), m, n) >> stkarray (a, m, n)
) :<!wrt> (a) // endfun

implement{a}
stkarray_peek_top {m,n} (stk) = let
  prval () = lemma_stkarray_param (stk)
  val res = stkarray_takeout<a> (stk)
  val () = stkarray_insert<a> (stk, res)
in
  res
end

implement{}
shunting_yard () = {
  vtypedef opstack = stkarray (Token)

  fun
  pop_until_lpar (opstack: !opstack >> _): bool =
    if stkarray_isnot_nil (opstack) then let
      var tok = stkarray_peek_top<Token> (opstack)
    in
      if :(opstack: opstack) => token_is_lpar (tok) then let
        val notfull = stkarray_isnot_full (opstack)
        val () = assert_errmsg (notfull, "stack overflow")
        val () = stkarray_insert<Token> (opstack, tok)
      in
        true
      end else let
        var tok = stkarray_takeout<Token> (opstack)
        val () = tokenizer_emit_token (tok)
      in
        pop_until_lpar (opstack)
      end
    end else false
  // end of [pop_until_lpar]

  fun
  shift (opstack: !opstack >> _, o1: operator): void =
    if stkarray_isnot_nil (opstack) then let
      //var tok = stkarray_peek_top<Token> (opstack)
      var tok = stkarray_takeout<Token> (opstack)
    in
      if token_is_operator (tok) then let
        val o2 = token_get_operator (tok)
        val r = operator_assoc (o1) = ASSOCleft && operator_prec (o1) <= operator_prec (o2)
        val q = operator_assoc (o2) = ASSOCright && operator_prec (o1) < operator_prec (o2)
        val p = r || q
      in
        if p then let
          val () = tokenizer_emit_token (tok)
        in
          shift (opstack, o1)
        end else let
          val notfull = stkarray_isnot_full (opstack)
          val () = assert_errmsg (notfull, "stack overflow")
          val () = stkarray_insert<Token> (opstack, tok)
        in
          (*empty*)
        end
      end else let
        val notfull = stkarray_isnot_full (opstack)
        val () = assert_errmsg (notfull, "stack overflow")
        val () = stkarray_insert<Token> (opstack, tok) (* token is not an operator *)
      in
      end
    end
  // end of [shift]

  fun
  clear (opstack: opstack): void = let
    prval () = lemma_stkarray_param (opstack)
  in
    if stkarray_isnot_nil (opstack) then let
      var tok = stkarray_takeout<Token> (opstack)
      (*
      val () = println!("clearing token: ")
      val () = token_print (tok)
      *)
      val ispar = token_is_lpar (tok) || token_is_rpar (tok)
      (*
      val () = println!("is parentheses: ", ispar)
      *)
      val () = assert_errmsg (~ispar, "mismatched parens 1")
      val () = tokenizer_emit_token (tok)
    in
      clear (opstack)
    end else stkarray_free_nil (opstack)
  end // end of [clear]

  fun
  loop (opstack: opstack): void = let
    var tok : Token
    val b = tokenizer_get_token (tok)
  in
    if :(tok: Token?) => b then let
      prval () = opt_unsome (tok)
      val () =
          if token_is_number (tok) then tokenizer_emit_token (tok)
          else if token_is_funcall (tok) then tokenizer_emit_token (tok)
          else if token_is_comma (tok) then let
            val lp = pop_until_lpar (opstack)
            val () = assert_errmsg (lp, "misplaced separator or mismatched parentheses")
          in
            (*empty*)
          end else if token_is_operator (tok) then let
            val o1 = token_get_operator (tok)
            val () = shift (opstack, o1)
            (*
            val () = println!("shifted!")
            *)
            val notfull = stkarray_isnot_full (opstack)
            val () = assert_errmsg (notfull, "stack overflow")
            val () = stkarray_insert<Token> (opstack, tok)
          in
            (*empty*)
          end else if token_is_lpar (tok) then let
            val notfull = stkarray_isnot_full (opstack)
            val () = assert_errmsg (notfull, "stack overflow")
            val () = stkarray_insert<Token> (opstack, tok)
            //val () = tokenizer_emit_token (tok)
          in
          end else if token_is_rpar (tok) then let
            (*
            val () = println!("got to rpar")
            *)
            val lp = pop_until_lpar (opstack)
            (*
            val () = println!("popped until lpar")
            *)
            val () = assert_errmsg (lp, "mismatched parentheses")
            val-true = stkarray_isnot_nil (opstack) // implied by lp=true!
            val lpar_tok = stkarray_takeout<Token> (opstack) // pop the lpar
            (*
            val () = println!("popped the token: ", lpar_tok)
            *)
          in
            if stkarray_isnot_nil (opstack) then let
              var tok = stkarray_takeout<Token> (opstack)
            in
              if token_is_funcall (tok) then tokenizer_emit_token (tok)
            end
          end else tokenizer_emit_token (tok)
      // end of [val]
    in
      loop (opstack)
    end else let
      prval () = opt_unnone (tok)
    in
      clear (opstack)
    end
  end

  #define OPSTACK_SIZE 512
  val opstack = stkarray_make_cap<Token> ((i2sz)OPSTACK_SIZE)
  val () = loop (opstack)
}

(* ****** ****** *)

fun
test_drive (inp: string): void = let
  val () = println!("input: ", inp)

  var str = inp: string
  prval pf_str = view@ (str)

  // TODO: move into a proper lookup table
  val op_pow = operator_make ("^", ASSOCright, 4)
  val op_mul = operator_make ("*", ASSOCleft, 3)
  val op_div = operator_make ("/", ASSOCleft, 3)
  val op_sum = operator_make ("+", ASSOCleft, 2)
  val op_sub = operator_make ("-", ASSOCright, 2)

  implement
  tokenizer_get_token<> (tok) = let
    prval (pf_res, fpf) = decode($vcopyenv_v(pf_str))
    val s = (g1ofg0)str
    prval () = lemma_string_param (s)
    prval () = fpf (pf_res)
  in
    if string_isnot_empty (s) then let
      val c = string_head (s)
      (*
      val () = println!("input char:", c)
      *)
      prval (pf_res, fpf) = decode($vcopyenv_v(pf_str))
      val () = str := (g0ofg1)(string_tail s)
      prval () = fpf (pf_res)
    in
      if c = '\n' then tokenizer_get_token<> (tok) // skip!
      else let
        val () = tok := (
          if isdigit c then let
            val n = char2int0 c
            val n0 = char2int0 '0'
            val n = n - n0
          in
            token_number (n)
          end else if c = '\(' then token_lpar ()
          else if c = ')' then token_rpar ()
          else if c = '^' then token_operator (op_pow)
          else if c = '*' then token_operator (op_mul)
          else if c = '/' then token_operator (op_div)
          else if c = '+' then token_operator (op_sum)
          else if c = '-' then token_operator (op_sub)
          else let
            val () = println! ("unknown character: ", c)
            val () = assert_errmsg (false, "unrecognized input character")
          in
            token_lpar () // arbitrary
          end
        ) (* end of [val] *)
        prval () = opt_some (tok)
      in
        true
      end
    end else let
      prval () = opt_none (tok)
    in
      false
    end
  end // end of [let]

  var ntokens = 0 : int
  prval pf_ntokens = view@ (ntokens)
  implement
  tokenizer_emit_token<> (tok) = {
    prval (pf, fpf) = decode($vcopyenv_v(pf_ntokens))
    val () = if isgtz(ntokens) then print!(" ")
    val () = ntokens := succ(ntokens)
    prval () = fpf (pf)
    val () = print! (tok)
  }

  val () = shunting_yard<> ()
  val () = println!()

  prval () = view@ (str) := pf_str
  prval () = view@ (ntokens) := pf_ntokens
in
end

(* ****** ****** *)

staload "libc/SATS/stdio.sats"
staload
UN="prelude/SATS/unsafe.sats"

fun loop
  {sz:pos} (
  inp: FILEref
, buf: &bytes(sz)? >> _
, sz: int sz
) : void = let
  val p = fgets0 (buf, sz, inp)
in
  if p > 0 then let // p=addr@(buf) or NULL
    val () = test_drive ($UN.cast{string}(p))
  in
    loop (inp, buf, sz)
  end else () // end of [if]
end // end of [loop]

fun
read_from_stdin (): void = {
  #define BUFSZ 128
  var buf = @[byte][BUFSZ]()
  val () = loop (stdin_ref, buf, BUFSZ)
}

implement
main0 () = let
  val () = println!("test 1")
  val () = test_drive("3+4")

  val () = println!("test 2")
  val () = test_drive("2+2*2")

  val () = println!("test 3")
  val () = test_drive("(2+2)*2")

  val () = println!("test 4")
  val () = test_drive("3+4*2/(1-5)^2^3")

  val () = println!("Try your own expression below! Press Ctrl-C to exit.")
  val () = read_from_stdin ()
in

end
	#include
	"share/atspre_staload.hats"

	(* **** **** *)
	(* operator interface *)

	datatype assoc = ASSOCnone \| ASSOCleft \| ASSOCright
	extern
	fun
	eq_assoc_assoc (assoc, assoc):<> bool
	overload = with eq_assoc_assoc
	extern
	fun
	ne_assoc_assoc (assoc, assoc):<> bool
	overload <> with ne_assoc_assoc

	abstype operator = ptr
	extern
	fun
	operator_make (label: string, a: assoc, precedence: Nat): operator
	extern
	fun
	operator_label (operator): string
	extern
	fun
	operator_prec (operator): Nat
	extern
	fun
	operator_assoc (operator): assoc
	extern
	fun
	operator_fprint (FILEref, operator): void

	(* **** **** *)
	// operator implementation

	local

	// need a hash table (string->operator info)
	// need methods for populating it
	datatype OPERATOR = OPERATOR of (string, assoc, Nat)
	assume operator = OPERATOR

	in

	implement
	eq_assoc_assoc (l, r) =
	case+ (l, r) of
	\| (ASSOCnone (), ASSOCnone ()) => true
	\| (ASSOCleft (), ASSOCleft ()) => true
	\| (ASSOCright (), ASSOCright ()) => true
	\| (_, _) => false

	implement
	ne_assoc_assoc (l, r) = ~(eq_assoc_assoc (l, r))

	implement
	operator_make (label, a, p) = OPERATOR (label, a, p)

	implement
	operator_label (o) = let
	val+ OPERATOR (lab, _, _) = o
	in
	lab
	end

	implement
	operator_prec (o) = let
	val+ OPERATOR (lab, a, p) = o
	in
	p
	end

	implement
	operator_assoc (o) = let
	val+ OPERATOR (lab, a, p) = o
	in
	a
	end

	implement
	operator_fprint (out, o) = {
	val+ OPERATOR (lab, a, p) = o
	(*
	val s =
	(case+ a of
	\| ASSOCnone () => "no"
	\| ASSOCleft () => "lf"
	\| ASSOCright () => "rg"): string
	*)
	val () = fprint!(out, lab)
	(*
	val () = fprint!(out, "(")
	val () = fprint!(out, s)
	val p = (g0ofg1)p
	val () = fprint!(out, ",", p, ")")
	*)
	}

	end

	(* FIXME: HACK *)
	overload fprint with operator_fprint

	(* **** **** *)
	(* token interface *)

	%{^

	typedef enum {
	NIL = 0,
	OPER = 1,
	NUMBER = 2,
	COMMA = 3,
	LPAR = 4,
	RPAR = 5,
	FUNCALL = 6
	} CTOKEN_ENUM;
	typedef struct {
	CTOKEN_ENUM tt;
	union {
	atstype_boxed oper;
	int num;
	} tv;
	} CTOKEN_TYPE;

	ATSinline()
	CTOKEN_TYPE TOKEN_NUMBER(atstype_int x) {
	CTOKEN_TYPE res;
	res.tt = NUMBER;
	res.tv.num = x;
	return res;
	}
	ATSinline()
	CTOKEN_TYPE TOKEN_LPAR() {
	CTOKEN_TYPE res;
	res.tt = LPAR;
	return res;
	}
	ATSinline()
	CTOKEN_TYPE TOKEN_RPAR() {
	CTOKEN_TYPE res;
	res.tt = RPAR;
	return res;
	}
	ATSinline()
	CTOKEN_TYPE TOKEN_OPERATOR(atstype_boxed oper) {
	CTOKEN_TYPE res;
	res.tt = OPER;
	res.tv.oper = oper;
	return res;
	}

	ATSinline()
	atstype_bool TOK_IS_OPER (CTOKEN_TYPE tok) {
	return tok.tt == OPER ? atsbool_true : atsbool_false;
	}
	ATSinline()
	atstype_bool TOK_IS_NUMBER(CTOKEN_TYPE tok) {
	return tok.tt == NUMBER ? atsbool_true : atsbool_false;
	}
	ATSinline()
	atstype_bool TOK_IS_COMMA(CTOKEN_TYPE tok) {
	return tok.tt == COMMA ? atsbool_true : atsbool_false;
	}
	ATSinline()
	atstype_bool TOK_IS_LPAR(CTOKEN_TYPE tok) {
	return tok.tt == LPAR ? atsbool_true : atsbool_false;
	}
	ATSinline()
	atstype_bool TOK_IS_RPAR(CTOKEN_TYPE tok) {
	return tok.tt == RPAR ? atsbool_true : atsbool_false;
	}
	ATSinline()
	atstype_bool TOK_IS_FUNCALL(CTOKEN_TYPE tok) {
	return tok.tt == FUNCALL ? atsbool_true : atsbool_false;
	}
	ATSinline()
	atstype_int TOK_GET_NUMBER (CTOKEN_TYPE tok) {
	return tok.tv.num;
	}
	ATSinline()
	atstype_boxed TOK_GET_OPERATOR (CTOKEN_TYPE tok) {
	return tok.tv.oper;
	}

	%}

	#define OPER 1
	#define NUMBER 2
	#define COMMA 3
	#define LPAR 4
	#define RPAR 5
	#define FUNCALL 6

	abst@ype token (int) = $extype"CTOKEN_TYPE"
	typedef Token = [tag:int] token(tag)

	extern
	fun
	token_number (int): token (NUMBER) = "ext#TOKEN_NUMBER"
	extern
	fun
	token_lpar (): token (LPAR) = "ext#TOKEN_LPAR"
	extern
	fun
	token_rpar (): token (RPAR) = "ext#TOKEN_RPAR"
	extern
	fun
	token_operator (operator): token (OPER) = "ext#TOKEN_OPERATOR"


	extern
	fun
	token_is_operator {i:int} (token(i)): bool(i==OPER) = "ext#TOK_IS_OPER"
	extern
	fun
	token_is_number {i:int} (token(i)): bool(i==NUMBER) = "ext#TOK_IS_NUMBER"
	extern
	fun
	token_is_comma {i:int} (token(i)): bool(i==COMMA) = "ext#TOK_IS_COMMA"
	extern
	fun
	token_is_lpar {i:int} (token(i)): bool(i==LPAR) = "ext#TOK_IS_LPAR"
	extern
	fun
	token_is_rpar {i:int} (token(i)): bool(i==RPAR) = "ext#TOK_IS_RPAR"
	extern
	fun
	token_is_funcall {i:int} (token(i)): bool(i==FUNCALL) = "ext#TOK_IS_FUNCALL"
	extern
	fun
	token_get_number (token(NUMBER)): int = "ext#TOK_GET_NUMBER"
	extern
	fun
	token_get_operator (token(OPER)): operator = "ext#TOK_GET_OPERATOR"

	extern
	fun
	token_fprint (out: FILEref, Token): void
	overload fprint with token_fprint
	extern
	fun
	token_print (Token): void
	overload print with token_print

	(* **** **** *)
	(* token implementation *)

	implement
	token_fprint (out, tok) =
	if token_is_operator (tok) then {
	val oper = token_get_operator (tok)
	val () = fprint!(out, oper)
	} else if token_is_number (tok) then {
	val num = token_get_number (tok)
	val () = fprint!(out, num)
	} else if token_is_comma (tok) then {
	val () = fprint!(out, ",")
	} else if token_is_lpar (tok) then {
	val () = fprint!(out, "(")
	} else if token_is_rpar (tok) then {
	val () = fprint!(out, ")")
	}
	else fprint!(out, "NIL()")

	implement
	token_print (tok) = token_fprint (stdout_ref, tok)

	(* **** **** *)

	(* will not return a token if EOF *)
	extern
	fun{}
	tokenizer_get_token (&Token? >> opt (Token, b)): #[b:bool] bool b
	extern
	fun{}
	tokenizer_emit_token (&Token): void

	extern
	fun{}
	shunting_yard (): void

	staload "libats/SATS/stkarray.sats"
	staload _(anon) = "libats/DATS/stkarray.dats"

	extern
	fun{a:t@ype}
	stkarray_peek_top
	{m,n:int \| n > 0}
	(
	stk: !stkarray (INV(a), m, n) >> stkarray (a, m, n)
	) :<!wrt> (a) // endfun

	implement{a}
	stkarray_peek_top {m,n} (stk) = let
	prval () = lemma_stkarray_param (stk)
	val res = stkarray_takeout<a> (stk)
	val () = stkarray_insert<a> (stk, res)
	in
	res
	end

	implement{}
	shunting_yard () = {
	vtypedef opstack = stkarray (Token)

	fun
	pop_until_lpar (opstack: !opstack >> _): bool =
	if stkarray_isnot_nil (opstack) then let
	var tok = stkarray_peek_top<Token> (opstack)
	in
	if :(opstack: opstack) => token_is_lpar (tok) then let
	val notfull = stkarray_isnot_full (opstack)
	val () = assert_errmsg (notfull, "stack overflow")
	val () = stkarray_insert<Token> (opstack, tok)
	in
	true
	end else let
	var tok = stkarray_takeout<Token> (opstack)
	val () = tokenizer_emit_token (tok)
	in
	pop_until_lpar (opstack)
	end
	end else false
	// end of [pop_until_lpar]

	fun
	shift (opstack: !opstack >> _, o1: operator): void =
	if stkarray_isnot_nil (opstack) then let
	//var tok = stkarray_peek_top<Token> (opstack)
	var tok = stkarray_takeout<Token> (opstack)
	in
	if token_is_operator (tok) then let
	val o2 = token_get_operator (tok)
	val r = operator_assoc (o1) = ASSOCleft && operator_prec (o1) <= operator_prec (o2)
	val q = operator_assoc (o2) = ASSOCright && operator_prec (o1) < operator_prec (o2)
	val p = r \|\| q
	in
	if p then let
	val () = tokenizer_emit_token (tok)
	in
	shift (opstack, o1)
	end else let
	val notfull = stkarray_isnot_full (opstack)
	val () = assert_errmsg (notfull, "stack overflow")
	val () = stkarray_insert<Token> (opstack, tok)
	in
	(empty)
	end
	end else let
	val notfull = stkarray_isnot_full (opstack)
	val () = assert_errmsg (notfull, "stack overflow")
	val () = stkarray_insert<Token> (opstack, tok) (* token is not an operator *)
	in
	end
	end
	// end of [shift]

	fun
	clear (opstack: opstack): void = let
	prval () = lemma_stkarray_param (opstack)
	in
	if stkarray_isnot_nil (opstack) then let
	var tok = stkarray_takeout<Token> (opstack)
	(*
	val () = println!("clearing token: ")
	val () = token_print (tok)
	*)
	val ispar = token_is_lpar (tok) \|\| token_is_rpar (tok)
	(*
	val () = println!("is parentheses: ", ispar)
	*)
	val () = assert_errmsg (~ispar, "mismatched parens 1")
	val () = tokenizer_emit_token (tok)
	in
	clear (opstack)
	end else stkarray_free_nil (opstack)
	end // end of [clear]

	fun
	loop (opstack: opstack): void = let
	var tok : Token
	val b = tokenizer_get_token (tok)
	in
	if :(tok: Token?) => b then let
	prval () = opt_unsome (tok)
	val () =
	if token_is_number (tok) then tokenizer_emit_token (tok)
	else if token_is_funcall (tok) then tokenizer_emit_token (tok)
	else if token_is_comma (tok) then let
	val lp = pop_until_lpar (opstack)
	val () = assert_errmsg (lp, "misplaced separator or mismatched parentheses")
	in
	(empty)
	end else if token_is_operator (tok) then let
	val o1 = token_get_operator (tok)
	val () = shift (opstack, o1)
	(*
	val () = println!("shifted!")
	*)
	val notfull = stkarray_isnot_full (opstack)
	val () = assert_errmsg (notfull, "stack overflow")
	val () = stkarray_insert<Token> (opstack, tok)
	in
	(empty)
	end else if token_is_lpar (tok) then let
	val notfull = stkarray_isnot_full (opstack)
	val () = assert_errmsg (notfull, "stack overflow")
	val () = stkarray_insert<Token> (opstack, tok)
	//val () = tokenizer_emit_token (tok)
	in
	end else if token_is_rpar (tok) then let
	(*
	val () = println!("got to rpar")
	*)
	val lp = pop_until_lpar (opstack)
	(*
	val () = println!("popped until lpar")
	*)
	val () = assert_errmsg (lp, "mismatched parentheses")
	val-true = stkarray_isnot_nil (opstack) // implied by lp=true!
	val lpar_tok = stkarray_takeout<Token> (opstack) // pop the lpar
	(*
	val () = println!("popped the token: ", lpar_tok)
	*)
	in
	if stkarray_isnot_nil (opstack) then let
	var tok = stkarray_takeout<Token> (opstack)
	in
	if token_is_funcall (tok) then tokenizer_emit_token (tok)
	end
	end else tokenizer_emit_token (tok)
	// end of [val]
	in
	loop (opstack)
	end else let
	prval () = opt_unnone (tok)
	in
	clear (opstack)
	end
	end

	#define OPSTACK_SIZE 512
	val opstack = stkarray_make_cap<Token> ((i2sz)OPSTACK_SIZE)
	val () = loop (opstack)
	}

	(* **** **** *)

	fun
	test_drive (inp: string): void = let
	val () = println!("input: ", inp)

	var str = inp: string
	prval pf_str = view@ (str)

	// TODO: move into a proper lookup table
	val op_pow = operator_make ("^", ASSOCright, 4)
	val op_mul = operator_make ("*", ASSOCleft, 3)
	val op_div = operator_make ("/", ASSOCleft, 3)
	val op_sum = operator_make ("+", ASSOCleft, 2)
	val op_sub = operator_make ("-", ASSOCright, 2)

	implement
	tokenizer_get_token<> (tok) = let
	prval (pf_res, fpf) = decode($vcopyenv_v(pf_str))
	val s = (g1ofg0)str
	prval () = lemma_string_param (s)
	prval () = fpf (pf_res)
	in
	if string_isnot_empty (s) then let
	val c = string_head (s)
	(*
	val () = println!("input char:", c)
	*)
	prval (pf_res, fpf) = decode($vcopyenv_v(pf_str))
	val () = str := (g0ofg1)(string_tail s)
	prval () = fpf (pf_res)
	in
	if c = '\n' then tokenizer_get_token<> (tok) // skip!
	else let
	val () = tok := (
	if isdigit c then let
	val n = char2int0 c
	val n0 = char2int0 '0'
	val n = n - n0
	in
	token_number (n)
	end else if c = '\(' then token_lpar ()
	else if c = ')' then token_rpar ()
	else if c = '^' then token_operator (op_pow)
	else if c = '*' then token_operator (op_mul)
	else if c = '/' then token_operator (op_div)
	else if c = '+' then token_operator (op_sum)
	else if c = '-' then token_operator (op_sub)
	else let
	val () = println! ("unknown character: ", c)
	val () = assert_errmsg (false, "unrecognized input character")
	in
	token_lpar () // arbitrary
	end
	) (* end of [val] *)
	prval () = opt_some (tok)
	in
	true
	end
	end else let
	prval () = opt_none (tok)
	in
	false
	end
	end // end of [let]

	var ntokens = 0 : int
	prval pf_ntokens = view@ (ntokens)
	implement
	tokenizer_emit_token<> (tok) = {
	prval (pf, fpf) = decode($vcopyenv_v(pf_ntokens))
	val () = if isgtz(ntokens) then print!(" ")
	val () = ntokens := succ(ntokens)
	prval () = fpf (pf)
	val () = print! (tok)
	}

	val () = shunting_yard<> ()
	val () = println!()

	prval () = view@ (str) := pf_str
	prval () = view@ (ntokens) := pf_ntokens
	in
	end

	(* **** **** *)

	staload "libc/SATS/stdio.sats"
	staload
	UN="prelude/SATS/unsafe.sats"

	fun loop
	{sz:pos} (
	inp: FILEref
	, buf: &bytes(sz)? >> _
	, sz: int sz
	) : void = let
	val p = fgets0 (buf, sz, inp)
	in
	if p > 0 then let // p=addr@(buf) or NULL
	val () = test_drive ($UN.cast{string}(p))
	in
	loop (inp, buf, sz)
	end else () // end of [if]
	end // end of [loop]

	fun
	read_from_stdin (): void = {
	#define BUFSZ 128
	var buf = @[byte][BUFSZ]()
	val () = loop (stdin_ref, buf, BUFSZ)
	}

	implement
	main0 () = let
	val () = println!("test 1")
	val () = test_drive("3+4")

	val () = println!("test 2")
	val () = test_drive("2+2*2")

	val () = println!("test 3")
	val () = test_drive("(2+2)*2")

	val () = println!("test 4")
	val () = test_drive("3+4*2/(1-5)^2^3")

	val () = println!("Try your own expression below! Press Ctrl-C to exit.")
	val () = read_from_stdin ()
	in

	end