Есть ли разница в выразительности между внешней практикой и внешней кастой? - PullRequest
Новая
       11

Есть ли разница в выразительности между внешней практикой и внешней кастой?

0 голосов
/ 25 августа 2018

Рассмотрим: 

#include "share/atspre_staload.hats"

fun only_zero(n: int(0)): void =
        println!("This is definitely zero: ", n)

fun less_than{n,m:int | n < m}(n: int(n), m: int(m)): void =
        println!(n, " is less than ", m)

implement main0() = (
        only_zero(zeroify(n));
        only_zero(m);
        less_than(b, a);
        less_than(f, e) where { val (f, e) = make_less_than((d, c)) };
) where {
        val n = 5
        val m = ~5
        val (a, b, c, d) = (1, 2, 3, 4)
        extern castfn zeroify{n:int}(n: int(n)): int(0)
        extern praxi lemma_this_is_zero{n:int}(n: int(n)): [n == 0] void
        extern castfn make_less_than{n,m:int}(t: (int(n), int(m))): [o,p:int | o < p] (int(o), int(p))
        extern praxi lemma_less_than{n,m:int}(n: int(n), m: int(m)): [n < m] void
        prval _ = lemma_this_is_zero(m)
}

, который имеет такой вывод: 

This is definitely zero: 5
This is definitely zero: -5
2 is less than 1
4 is less than 3

Существуют ли случаи, когда один из них требует другого?

1 Ответ

0 голосов
/ 26 августа 2018

Если вы используете 'castfn', вам нужно убедиться, что на целевом языке есть соответствующая неявная функция приведения.Например, int2double - это castfn, если C является целевым языком.

С другой стороны, praxi / prfun полностью удален, и в сгенерированном коде нет никаких следов.

Я бы сказал, чтоpraxi / prfun является более общим, но int2double определенно не является praxi / prfun.

...