How should you perform simple read-only string operations against linear-typed strings?

Question

This code compiles and works as intended:

// patscc -O2 -flto -DATS_MEMALLOC_LIBC rltest_dats.o -o rltest -latslib -lreadline
#include "share/atspre_staload.hats"

fn obey(cmd: string): void =
  case+ cmd of
  | "bye" => exit(0)
  | "hi" => println!("hello yourself")
  | _ => ()

extern fun readline(prompt: string): strptr = "ext#"

implement main0() =
  let
    val input = readline(": ")
  in
    if iseqz(input) then (
      println!("exiting on EOF");
      strptr_free(input);
    ) else (
      println!("you entered: ", input);
      obey(cmd) where {
        extern castfn strptr2string{l:addr}(s: !strptr(l)): string
        val cmd = strptr2string(input)
      };
      strptr_free(input);
      main0();
    )
  end

where the where at least ensures that a read-only copy isn't held and possibly referenced after the strptr_free.

Of course, it would even better if the type system enforced that. My first attempt hoped it would:

#include "share/atspre_staload.hats"

fn obey{l:addr}(cmd: !strptr(l)): void =
  case+ cmd of
  | "bye" => exit(0)
  | "hi" => println!("hello yourself")
  | _ => ()

extern fun readline(prompt: string): strptr = "ext#"

implement main0() =
  let
    val input = readline(": ")
  in
    if iseqz(input) then (
      println!("exiting on EOF");
      strptr_free(input);
    ) else (
      println!("you entered: ", input);
      obey(input);
      strptr_free(input);
      main0();
    )
  end

but fails at the string pattern-matching with error(3): the string pattern is ill-typed.

Is there no way to do this without casting? If there isn't, how can I cast without losing safety?

Answer 1

The code you need can be written as follows:

fn
obey
(cmd: !Strptr1): void =
ifcase
| cmd = "bye" => exit(0)
| cmd = "hi" => println!("hello yourself")
| _(*else*) => ()

extern fun readline(prompt: string): strptr = "ext#"

implement main0() = let
  val input = readline(": ")
  prval () = lemma_strptr_param(input)
in
if
iseqz(input)
then
(
  println!("exiting on EOF");
  strptr_free(input);
) else (
  println!("you entered: ", input);
  obey(input);
  strptr_free(input);
  main0();
)
end

Right now, only string (not strptr) can be used as a pattern.