1

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

// 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.

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

4

1 回答 1

2

你需要的代码可以这样写：

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）可以用作模式。

于 2018-02-09T14:48:24.013 回答