ATS (langage de programmation)

dataprop exprime les prédicats sous forme de types algébriques.

Exemple de prédicats en pseudo-code assez similaire à la source ATS (voir ci-dessous pour une source ATS valide) pour la fonction factorielle, dont le nom est abrégé en « FACT » :

 FACT(n, r) ssi fact(n) = r
 MUL(n, m, prod) ssi n * m = prod
 
 FACT(n, r) = 
     FACT(0, 1) 
   | FACT(n, r) ssi FACT(n-1, r1) et MUL(n, r1, r) // pour n> 0
 
 // exprime le fact(n) = r ssi r = n * r1 et r1 = fact(n-1)

En code ATS :

 dataprop FACT (int, int) =
  | FACTbas (0, 1)       // basic case: FACT(0, 1)
  | {n:int | n > 0} {r,r1:int} // inductive case
    FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r))

où FACT (int, int) est un type de preuve

Factoriel non récursif avec proposition ou " Théorème " prouvant à travers la construction dataprop.

L'évaluation de fact1 (n-1) renvoie une paire (proof_n_minus_1 | result_of_n_minus_1) qui est utilisée dans le calcul de fact1 (n). Les preuves expriment les prédicats de la proposition.

[FACT (n, r)] implique [fact (n) = r]
 [MUL (n, m, prod)] implique [n * m = prod]

FAIT (0, 1)
 FACT (n, r) ssi FACT (n-1, r1) et MUL (n, r1, r) pour tout n> 0

Se souvenir:

{...} quantification universelle
[...] quantification existentielle
(... | ...) (preuve | valeur)
@ (...) tuple plat ou tuple de paramètres de fonction variadique
. <...>. métrique de terminaison [6]

#include "share/atspre_staload.hats"

dataprop FACT (int, int) =
 | FACTbas (0, 1) of () // basic case
 | {n:nat}{r:int}    // inductive case
  FACTind (n+1, (n+1)*r) of (FACT (n, r))

(* note that int(x), also int x, is the monovalued type of the int x value.

 The function signature below says:
 forall n:nat, exists r:int where fact( num: int(n)) returns (FACT (n, r) | int(r)) *)

fun fact{n:nat} .<n>. (n: int (n)) : [r:int] (FACT (n, r) | int(r)) =
(
 ifcase
 | n > 0 => ((FACTind(pf1) | n * r1)) where 
 { 
  val (pf1 | r1) = fact (n-1)
 }
 | _(*else*) => (FACTbas() | 1)
)

implement main0 (argc, argv) =
{
 val () = if (argc != 2) then prerrln! ("Usage: ", argv[0], " <integer>")

 val () = assert (argc >= 2)
 val n0 = g0string2int (argv[1])
 val n0 = g1ofg0 (n0)
 val () = assert (n0 >= 0)
 val (_(*pf*) | res) = fact (n0)

 val ((*void*)) = println! ("fact(", n0, ") = ", res)
}

Tout cela peut être ajouté à un seul fichier et compilé comme suit. La compilation devrait fonctionner avec divers compilateurs C back-end, par exemple gcc . Le nettoyage de la mémoire n'est pas utilisé sauf indication explicite avec -D_ATS_GCATS)

$ patscc fact1.dats -o fact1
$ ./fact1 4

compile et donne le résultat attendu

• booléen (vrai, faux)
• int (littéraux: 255, 0377, 0xFF), unaire moins comme ~ (comme dans ML)
• double
• char 'a'
• chaîne "abc"

préfixe @ ou aucun signifie allocation directe, plate ou sans boîte

 val x : @(int, char) = @(15, 'c') // x.0 = 15 ; x.1 = 'c'
 val @(a, b) = x          // pattern matching binding, a= 15, b='c'
 val x = @{first=15, second='c'}  // x.first = 15
 val @{first=a, second=b} = x    // a= 15, b='c'
 val @{second=b, ...} = x      // with omission, b='c'

préfixe 'signifie allocation indirecte ou encadrée

 val x : '(int, char) = '(15, 'c') // x.0 = 15 ; x.1 = 'c'
 val '(a, b) = x          // a= 15, b='c'
 val x = '{first=15, second='c'}  // x.first = 15
 val '{first=a, second=b} = x    // a= 15, b='c'
 val '{second=b, ...} = x      // b='c'

spécial

Avec '|' comme séparateur, certaines fonctions renvoient la valeur du résultat encapsulée avec une évaluation des prédicats

val (predicate_proofs | values) = mes paramètres

{...} quantification universelle
[...] quantification existentielle
(...) expression entre parenthèses ou tuple

(... | ...) (preuves | valeurs)

. <...>. métrique de terminaison

@ (...) tuple plat ou tuple de paramètres de fonction variadique (voir l'exemple printf)

@ [byte] [BUFLEN] type d'un tableau de valeurs BUFLEN de type octet 
@ [byte] [BUFLEN] () instance de tableau
@ [byte] [BUFLEN] (0) tableau initialisé à 0

sorte

domaine

 sortdef nat = {a: int | a >= 0 }   // from prelude: ∀ ''a'' ∈ int ...

 typedef String = [a:nat] string(a)  // [..]: ∃ ''a'' ∈ nat ...

type (comme tri)

tri générique pour les éléments de la longueur d'un mot pointeur, à utiliser dans les fonctions polymorphes paramétrées par type. Également "types en boîte" [7].

taper

version linéaire du type précédent avec longueur abstraite. Également des types non emballés. [7]

viewtype

une classe de domaine comme type avec une vue (association de mémoire)

viewt @ ype

version linéaire du type de vue avec une longueur abstraite. Il remplace le type de vue

vue

relation d'un Type et d'un emplacement mémoire. L'infixe @ est son constructeur le plus courant

T @ L affirme qu'il existe une vue de type T à l'emplacement L

 fun {a:t@ype} ptr_get0 {l:addr} (pf: a @ l | p: ptr l): @(a @ l | a)
 
 fun {a:t@ype} ptr_set0 {l:addr} (pf: a? @ l | p: ptr l, x: a): @(a @ l | void)

le type de ptr_get0 (T) est ∀ l : adr. (T @ l | ptr (l)) → (T @ l | T) // voir manuel, section 7.1. Accès sécurisé à la mémoire via des pointeurs [8]

viewdef array_v (a: viewt @ ype, n: int, l: addr) = @ [a] [n] @ l

T?

type éventuellement non initialisé

comme dans le cas +, val +, type +, viewtype +,. . .

• avec le suffixe '+' le compilateur émet une erreur en cas d'alternatives non exhaustives
• sans suffixe, le compilateur émet un avertissement
• avec '-' comme suffixe, évite le contrôle d'exhaustivité

 staload "foo.sats" // foo.sats is loaded and then opened into the current namespace

 staload F = "foo.sats" // to use identifiers qualified as $F.bar

 dynload "foo.dats" // loaded dynamically at run-time

Les vues de données sont souvent déclarées pour encoder des relations définies de manière récursive sur des ressources linéaires.

dataview array_v (a: viewt @ ype +, int, addr) = | {l: addr} array_v_none (a, 0, l) | {n: nat} {l: addr} array_v_some (a, n + 1, l) of (a @ l, array_v (a, n, l + sizeof a))

Types de données

type de données jour ouvrable = Mon | Tue | Mer | Thu | ven

listes

type de données list0 (a: t @ ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)

Un type de vue de données est similaire à un type de données, mais il est linéaire. Avec un dataviewtype, le programmeur est autorisé à libérer explicitement (ou désallouer) de manière sûre la mémoire utilisée pour stocker les constructeurs associés au dataviewtype[9].

variables locales

var res: int avec pf_res = 1 // introduit pf_res comme alias de view @ (res)

sur l' allocation de tableau de pile:

#define BUFLEN 10
var! p_buf avec pf_buf = @ [octet] [BUFLEN] (0) // pf_buf = @ [octet] [BUFLEN] (0) @ p_buf 

Voir les déclarations val et var