Как вам следует выполнять простые строковые операции только для чтения со строками линейного типа?

Question

Этот код компилируется и работает как задумано:

// 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 по крайней мере, гарантирует, что копия только для чтения не хранится и, возможно, ссылка на нее после strptr_free,

Конечно, было бы еще лучше, если бы система типов обеспечивала это. Моя первая попытка надеялась, что это будет:

#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

но терпит неудачу при сопоставлении с шаблоном строки error(3): the string pattern is ill-typed.

Нет ли способа сделать это без кастинга? Если нет, как я могу сыграть без потери безопасности?

Answer 1

Код, который вам нужен, может быть написан следующим образом:

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

Прямо сейчас, только строка (не strptr) может быть использована в качестве шаблона.