ats - 如何证明 c -'a' 在 [0,26) 内？

Question

假设我有这段代码:

#include "share/atspre_staload.hats"

val letters = arrayref_make_elt<bool>(i2sz(26), false)

implement main0() =
  begin
    println!("found('a'): ", letters[0]);
    println!("found('f'): ", letters[5]);
  end

产生输出:

found('a'): false
found('f'): false

我想改为按字符索引 letters。实际上，给定任何字符，我想索引到 letters 中，只有当它是有效索引时。

所以这几乎可以工作了:

#include "share/atspre_staload.hats"

val letters = arrayref_make_elt<bool>(i2sz(26), false)

typedef letter = [c:int | c >= 'a' && c <= 'z'] char(c)
typedef letteri = [i:int | i >= 0 && i < 26] int(i)

(* fn letter2index(c: letter): letteri = c - 'a' *)  (* #1 *)

fn letter2index(c: letter): letteri =
  case- c of
  | 'a' => 0
  | 'f' => 5

fn trychar(c: char): void =  (* #2 *)
  if c >= 'a' && c <= 'z' then
    println!("found('", c, "'): ", letters[letter2index(c)])

implement main0() =
  begin
    trychar('a');
    trychar('f');
    trychar('+');  (* #3 *)
  end

如果我在 #2 处将 char 更改为 letter 并在 #3 处删除 trychar('+')，则此编译。但当然我宁愿在 #1 处执行减法而不是大写字母，而且我想将 trychar 应用于任何类型的 char，而不仅仅是一封信。

Answer 1

你想要的代码可以这样写:

#include
"share/atspre_staload.hats"

stadef
isletter(c:int): bool = ('a' <= c && c <= 'z')

val
letters = arrayref_make_elt<bool>(i2sz(26), false)

fn
letter2index
{ c:int
| isletter(c)}
(c: char(c)): int(c-'a') = char2int1(c) - char2int1('a')

fn
trychar
{c:int}
(c: char(c)): void =
if
(c >= 'a') * (c <= 'z')
then
println!("found('", c, "'): ", letters[letter2index(c)])

implement main0() =
begin
  trychar('a');
  trychar('f');
  trychar('+');
end

在您的原始代码中，没有正确使用量词(forall 和 exists)。