Как заменить статические утверждения на prfuns? - PullRequest
Новая
       20

Как заменить статические утверждения на prfuns?

0 голосов
/ 02 июня 2018

Рассмотрим эту не определенную (но работающую) программу: 

#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())изменено, чтобы вернуть что-то отличное от 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 и т.п. выше на dataprops и функции проверки.Это возможно?В основном я хочу сделать это, чтобы лучше понять доказательство теорем в 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 не является исчерпывающим.

Ответы [ 2 ]

0 голосов
/ 03 июня 2018

Следующий код должен исправить ошибку стирания: 

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) }
  )
0 голосов
/ 03 июня 2018

Полученная ошибка говорит о том, что test_promotable может возвращать 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() => ()
      )
  )
...