CONCEPTION DE LANGAGE
			---------------------
			   Examen fev 2008
			       Corrigé

Affectation multiple
--------------------

 Syntaxe: x1, .., xn := e1, .., en

 On fait naturellement l'hypothèse que la suite de variable et la suite
d'expressions sont de même longueur.

 Il y a plusieurs possibilités:
  1) macro pour la séquence x1 := e1; ..; xn := en
  2) macro pour la séquence xn := en; ..; x1 := e1 
     (je l'ai vu dans certaines copies)
  3) affectation parallèle

 La possibilité la plus rigolote est 3) affectation parallèle: elle
permet de faire l'échange entre deux variable en une seule instruction
       	  	x, y := y, x

 Pour définir la fonction sémantique, on peut
  a) soit utiliser la facilité de la notation avec les "trois petits points"
  b) soit donner une définition par (double) récurrence sur les listes
     de variables et d'expressions
  c) soit se compliquer la vie avec le point fixe d'une fonction.

 On ne considère que la solution rigolote.

 Pour aller vite, on confond le nom de la variable 'xi' avec son adresse en
mémoire.

 a) S[[x1, .., xn ':=' e1, .., en]](r, m)
    = setMem x1 (E[[e1]](r,m)) ..(setMem xn (E[[en]](r,m)) m)

   Notez que toutes les expressions sont évaluées dans le même contexte

 b) On peut écrire
    S[[xn := en]](r,m) = setMem xn (E[[en]](r,m)
    S[[x1, x2, .. := e1, e2, ..]](r,m) 
    = setMem x1 (E[[e1]](r,m)) (S[[x2, .. := e2, ..]](r,m))

   Ici aussi, toutes les expressions sont évaluées dans le même contexte

 c) avec point fixe, on prend le point fixe d'une fonction à trois arguements:
     - xs: suite de noms/adresse de variables
     - es: suit d'expressions
     - m': mémoire
    On définit une fonction récursive sur les suites en utilisant une syntaxe
   de filtrage "à la ML":

   S[[x1, .., xn := e1, .., en]](r,m) 
   = ((!w \xs \es \m'.
     	case xs, es:
          [], [] -> m'
        | x:xs, e:es -> w xs es (setMem x (E[[e]](r, m)) m'))
      (x1, .., xn) (e1, .., en) m)

   Notez que la mémoire caluclée est m' et la mémoire qui sert à l'évaluation
  des expressions de es est la mémoire m de départ.

Un boucle
----------

 No comment, personne n'est bêtement tombé dans le (léger) piège.

Un langage de gardes
--------------------

Lexique: 
  symboles réservés: ':=' ':' ';' et '.'
  mots clef: 'Variables' 'Control' 'Loop'

  plus ce qu'il faut pour les expressions arithmétiques et logiques.

  ident: identificateurs
  num: constantes numériques
  bool: constantes booléennes

Syntaxe

Prog ::= 'Variables' ':' Initvar 'Control' ':' InitCtrl 'Loop' ':' Actions

InitVar ::= ident ':=' num '.'
       | ident ':=' num ';' InitVar
 
InitCtrl ::= ident ':=' bool
       | ident ':=' bool ';' InitCtrl

Actions ::= Action 
	| Action Actions

Action ::= ident ':' Effets 

Effets ::= ident ':=' Exp '.'
       | ident ':=' Exp ';' Effets

Pour les expressions, on distingue syntaxiquement les entiers de booléens

Exp ::= BoolExp | IntExp

Sémantique

 On a deux types de valeurs: Val = Int + Bool
 
 On ne distingue pas environnement et mémoire,	
 on ne considère qu'un environnement: Env = Ident -> Val#
 avec 
  setEnv: ident -> Val -> Env -> Env
  getEnv: ident -> Env -> Val

 On pose r0, l'environnement vide.
 
 Programmes;
  P: Prog -> Env
  P[['Variables:' vs 'Control:' cs 'Loop:' as]]
   = A[[as]] ( C[[cs]] ( V[[vs]] r0))

 Déclarations/initialisations:
  V: InitVar -> Env -> Env
  V[[ x ':=' n '.' ]] r = setEnv x inInt(n) r
  V[[ x ':=' n ';' vs]] r = V[[vs]](setEnv x inInt(n) r)

  C: InitCtrl -> Env -> Env
  C[[ x ':=' b '.']] r = setEnv x inBool(b) r
  C[[ x ':=' b ';' cs]] r = C[[cs]](setEnv x inBool(b) r)

 Bloc d'actions (équations récursives):
  ici, il faut réfléchir une peu. Il est demandé que "le contexte [..] 
  d'exécution d'une action soit celui présent au débiut de la boucle".
  Pour évaluer un bloc d'action, on a donc deux contextes: celui qui sert
  au calcul des expressions et celui qui est calculé. 

  La fonction sémantique du bloc d'action (B) est une boucle sans fin
  d'itération de la suite d'actions gardées. La fonction sémantique de
  la suite d'action gardées (A) doit tenir compte du requisit sur les
  environnements. On pose donc
   B: Actions -> Env -> Env
   A: Actions -> (Env * Env) -> Env

  B[[ as ]] r = ((!w. \r'. A[[ as ]](r, r')) r)

  A[[ c':' es '.' ]](r, r') =
    case getEnv c r:
      inBool(true) -> F[[es]](r, r')
    | _ -> r'
  A[[ c':' es ';' as]](r, r') =
    case getEnv c r:
      inBool(true) -> A[[as]](r, F[[es]](r, r'))
    | _ -> A[[as]](r, r')
    
  Suite d'affectations (effets):
  on retrouve l'utilisation des deux environnements.
  F: Effets -> (Env * Env) -> Env

  F[[ x ':=' e '.' ]](r, r') = setEnv x (E[[e]]r) r'
  F[[ x ':=' e ';' es ]](r, r')
   = F[[es]](r, setEnv x (E[[e]]r) r')

  Nota: pour être plus rigoureux, il eût fallu distinguer entre expressions
  booléennes et expressions entières...