您应该如何对线性类型的字符串执行简单的只读字符串操作？答案

【问题标题】：How should you perform simple read-only string operations against linear-typed strings?您应该如何对线性类型的字符串执行简单的只读字符串操作？
【发布时间】：2018-02-08 21:20:02
【问题描述】：

此代码按预期编译和工作：

// 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. 进行字符串模式匹配时失败

没有强制转换就没有办法做到这一点吗？如果没有，我怎样才能在不失去安全性的情况下施放？

【问题讨论】：

标签： ats linear-types

【解决方案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）可以用作模式。

【讨论】：