如何用 prfun 替换静态断言？

Question

考虑这个未精炼（但有效）程序：

#include "share/atspre_staload.hats"

datatype class =
        | mage   | fighter | thief | cleric
        | wizard | warrior | ninja | priest

fn promoteclass(job: class): class =
        case- job of
        | mage() => wizard()
        | fighter() => warrior()
        | thief() => ninja()
        | cleric() => priest()

fn getsomeclass(): class = mage()

val- wizard() = promoteclass(getsomeclass())

implement main0() = ()

将 wizard() 传递给 promoteclass() 是运行时错误，如果将 promoteclass(getsomeclass()) 更改为 return 而不是 wizard()，则会出现运行时错误].

哪个不行！我宁愿将这两个 - 符号翻转为 + 并在前两个错误情况下得到 编译时间 错误。如果意外转置提升案例可能是编译时错误，比如 priest() => cleric()

，那也很好

这种愿望导致了对上述内容的改进，这也很好用：

#include "share/atspre_staload.hats"

datatype class(int) =
        | mage(0)   | fighter(1) | thief(2) | cleric(3)
        | wizard(4) | warrior(5) | ninja(6) | priest(7)

fn promoteclass{n:int | n < 4}(job: class(n)): [m:int | m == n + 4] class(m) =
        case+ job of
        | mage() => wizard()
        | fighter() => warrior()
        | thief() => ninja()
        | cleric() => priest()

fn getsomeclass(): class(0) = mage()

val+ wizard() = promoteclass(getsomeclass())

implement main0() = ()

但我喜欢做的是用数据道具和证明函数替换 n < 4 等。那可能吗？主要是我想这样做是为了更好地理解 ATS 中的定理证明，但它似乎也是获得与第二个示例相同的保证的途径，而没有它的所有冗长（特别是添加了额外的功能，对这些进行操作类).

这是我尝试做的：

#include "share/atspre_staload.hats"

datatype class(int) =
        | mage(0)   | fighter(1) | thief(2) | cleric(3)
        | wizard(4) | warrior(5) | ninja(6) | priest(7)

dataprop promotable(int) =
        | {n:int}promotable_yes(n)
        | {n:int}promotable_no(n)

prfun test_promotable.<>.{n:int}():<> promotable(n) =
        sif n < 4 then promotable_yes{n}() else promotable_no{n}()

fn promoteclass{n:int}(job: class(n)): [m:int] class(m) =
        let
                prval promotable_yes() = test_promotable{n}()
        in
                case+ job of
                | mage() => wizard()
                | fighter() => warrior()
                | thief() => ninja()
                | cleric() => priest()
        end

fn getsomeclass(): class(0) = mage()

val+ wizard() = promoteclass(getsomeclass())

implement main0() = ()

但我马上就被告知 prval 分配是非详尽的。

Answer 1

你得到的错误说 test_promotable 可能 return promotable_no，这是真的（因为测试可能会失败）。

不确定以下样式是否是您想要的：

dataprop
promotable(int) =
  | pf_mage(0)
  | pf_fighter(1)
  | pf_thief(2)
  | pf_cleric(3)

fn promoteclass{n:int}
  (pf: promotable(n) | job: class(n)): [m:int] class(m) =
  (
    case+ job of
    | mage() => wizard()
    | fighter() => warrior()
    | thief() => ninja()
    | cleric() => priest()
    | _ =/=>>
      (
        case+ pf of
        | pf_mage() => ()
        | pf_fighter() => ()
        | pf_thief() => ()
        | pf_cleric() => ()
      )
  )

Answer 2

以下代码应修复擦除错误：

fn promoteclass{n:int}
  (pf: promotable(n) | job: class(n)): [m:int] class(m) =
  (
    case+ job of
    | mage() => wizard()
    | fighter() => warrior()
    | thief() => ninja()
    | cleric() => priest()
    | _ =/=>> () where
      {
        prval () =
        (
        case+ pf of
        | pf_mage() => ()
        | pf_fighter() => ()
        | pf_thief() => ()
        | pf_cleric() => ()
        ) : [false] void
      }
  )

您可以将证明代码移动到证明函数中；证明函数的类型有点复杂。这是我拥有的：

prfn
not_promotable
  {n:int | n != 0&&n != 1&&n != 2&&n != 3 }
  (pf: promotable(n)):<> [false] void =
(
case+ pf of
| pf_mage() => ()
| pf_fighter() => ()
| pf_thief() => ()
| pf_cleric() => ()
)

fn promoteclass{n:int}
  (pf: promotable(n) | job: class(n)): [m:int] class(m) =
  (
    case+ job of
    | mage() => wizard()
    | fighter() => warrior()
    | thief() => ninja()
    | cleric() => priest()
    | _ =/=>> () where { prval () = not_promotable(pf) }
  )

如何用 prfun 替换静态断言？

How do you replace static assertions with prfuns?

ats