Module Closed.Eval

Le module Eval fournit un interprète pour Closed.

La sémantique du langage sans fermetures est défini par un interprète de référence, la fonction eval de ce module.

Celle-ci associe aux programmes du langage (de type t) leur valeur (de type value) dans un environnement (de type env). L'environnement détermine la valeur des variables libres de l'expression.

Les programmes Closed ont accès à une mémoire dans laquelle qu'ils peuvent modifier en place. La possibilité de réaliser de tels effets de bords rend la sémantique de Closed un peu plus complexe que celle de Skimmel.

type location

Le type (abstrait) des emplacements mémoire.

type value =
  1. | VLit of int
    (*

    Les constantes littérales sont des valeurs.

    *)
  2. | VPair of value * value
    (*

    Les paires de valeurs sont des valeurs.

    *)
  3. | VThunk of thunk
    (*

    Les suspensions (thunks) sont des valeurs.

    *)
  4. | VLoc of location
    (*

    Les emplacements mémoire (locations) sont des valeurs.

    *)

Les valeurs sont les résultats possibles de l'évaluation d'une expression du langage cible Closed.

and thunk = {
  1. code : exp Id.MultiScoped.t;
    (*

    Le paramètre code fournit la fonction avec ses paramètres formels en attente de leurs arguments.

    *)
  2. mutable args : env;
    (*

    L'environnement args stocke les arguments effectifs déjà fournis.

    Ce champ est déclaré modifiable pour faciliter l'implémentation des suspensions récursives.

    *)
  3. globals : env;
    (*

    L'environnement globals stocke les valeurs des définitions de fonctions réalisées à la surface du fichier.

    *)
}

Une suspension (thunk) est une fonction multi-arguments en attente d'évaluation.

and env = value Id.Env.t

Les environnements spécifient la valeur des variables libres d'une expression du langage en associant à chacune sa valeur.

Les valeurs et environnements sont affichables, pas les suspensions ni les emplacements mémoires.

val pp_value : Format.formatter -> value -> unit
val pp_env : Format.formatter -> env -> unit
val initial_env : 'a Id.Env.t

L'environnement initial, vide.

type memory

Un type représentant la mémoire manipulée par les programmes Closed.

val empty_memory : memory

La mémoire vide.

Les fonctions d'allocation, lecture et écriture dans la mémoire.

La mémoire associe à des adresses des blocs, auxquels on peut penser comme à des tableaux de valeurs (value).

val allocate : int -> memory -> location * memory

allocate size m alloue un nouveau bloc de taille sz dans la mémoire m et renvoie l, m' où m' est la mémoire modifiée et l est l'emplacement mémoire du nouveau bloc dans m'.

val read : location -> int -> memory -> value option

read l i m essaie de lire la ième valeur du bloc situé à l'emplacement l dans la mémoire m. Si ce i est compris entre 0 inclus et la taille du bloc d'emplacement l exclue, alors la fonction renvoie Some v où v est la valeur située à l'indice en question. Sinon, l'indice est invalide, et la fonction renvoie None.

val write : location -> int -> value -> memory -> memory option

write l i v m essaie d'écrire la valeur v à la ième valeur du bloc situé à l'emplacement l dans la mémoire m. Si ce i est compris entre 0 inclus et la taille du bloc d'emplacement l exclue, alors la fonction renvoie Some m où m est la mémoire modifiée. Sinon, l'indice est invalide, et la fonction renvoie None.

type 'a computation = memory -> 'a * memory
val eval_exp : env -> exp -> value computation

Un appel eval_exp env e renvoie le calcul de la valeur de l'expression e en supposant que la valeur des variables libres de e soit définie par l'environnement env.

Ce calcul interrompra l'exécution du programme avec une erreur si l'expression e est mal typée ou contient une erreur. Par exemple, e pourrait :

  • chercher à appliquer un entier à un argument, comme s'il s'agissait d'une fonction,
  • calculer le ET logique de deux fonctions,
  • faire référence à une variable qui n'est pas définie dans env,
  • accéder à un indice dans un bloc mémoire qui n'existe pas (voir par exemple la documentation de read ci-dessus).

La liste ci-dessus n'est pas exhaustive.

val eval : env -> t -> value computation

Un appel eval env p renvoie le calcul de la valeur du programme p dans l'environnement env. Celle-ci est par définition celle de l'expression principale de p.