T	tipo
x	identificatore
d	dichiarazione

e	espressione
v	variabile
c	comando

DOMINI SINTATTICI

T ::= X |
      e1..e2 |			sottocampo
      array X1 of X2 |		array
      record  {x:X} end |	record
      union x:X of {e:(x:X)} default x:X end |
      ptr X


d ::= {type X=T | enum X=({x}) | var x:T | const x=e | proc x=c}

v ::= x | v[e] | v.x | v^

e ::= x | v | op({e})

c ::= ... |
      begin d; {c} end |
      with v do c


SEMANTICA STATICA (type-checking)

Senv |- Sstate,T => Sstate',TV | error
Senv |- Sstate,d => Sstate',Senv' | error

Senv,Sstate |- e => TV | error
Senv,Sstate |- v => TV | error
Senv,Sstate |- c => ok | error


DOMINI SEMANTICI

name couter per implementare la generativita di tipi e costanti
N

type value
TV = N

ambiente statico
Senv = Id ->_f type TV | var TV | const TV | proc

stato statico
Sstate = N x
       ( N ->_f base | enum | array N N | record {x:N} |
		union x:N of {x:N} default x:N )

0 indica la funzione parziale ovunque indefinita

n:=t indica la funzione parziale definita solo su n e con valore t

g[g'] e' la funzione parziale t.c. g[g'](m) = if m in dom g' then g' m else g m

operazione s+s' di estensione dello stato statico
   (n,g)+(n',g') = (n+n',g[g'])
in genere il dom g' ed n hanno intersezione vuota


Senv |- Sstate,T => Sstate',TV | error ----------------------------------------

(* lo stato statico non subisce modifiche, ma solo estensioni, questo
   permette di dare due interpretazioni alle asserzioni

   f |- s,T => s',m e f |- s,d => s',f'

   1) s' (ed f') sono il nuovo stato (ed ambiente)

   2) s' (ed f') e' l'incremento che va aggiunto al vecchio stato s (e
      ambiente f) per ottenere il nuovo stato (ambiente)

   noi adotteremo la 2) perche' e' piu flessibile, in particolare
   permette di trattare le dichiarazioni mutuamente ricorsive e le
   dichiarazioni locali ad altre dichiarazioni. *)

f(X)=type m
-------------------
f |- s,X => (0,0),m

(* (0,0) indica che lo stato non subisce variazioni *)

f,(n,g) |- ei => m (i=1,2)
g(m) = enum
----------------------------
f |- (n,g),e1..e2 => (0,0),m

(* nel type-checking a compile-time si ignorano i bounds, poiche'
   il bound-checking puo' essere fatto solo a run-time *)

f(Xi)=type mi (i=1,2)
g(m1)=enum
-------------------------------------------------------
f |- (n,g), array X1 of X2 => (1,n:=array m1 m2),n

f(Xi)=type mi
--------------------------------------------------------------
f |- (n,g), record {xi:Xi} end => (1,n:=record {xi:mi}),n

f(X)=type m, f(Xi)=type mi, f(X')=type m'
g(m)=enum
f,(n,g) |- ei => m
-------------------------------------------------------
f |- (n,g), union x:X of {ei:(xi:Xi)} default x':X' end
     => (1,n:=record {xi:mi}),n

(* a compile-time non si puo' verificare se le espressioni ei hanno
   valori distinti, a meno che non si ammettano solo espressioni
   valutabili staticamente *)

f(X)=type m
----------------------------------------
f |- (n,g), ptr X => (n+1,n:=ptr m),n


Senv |- Sstate,d => Sstate',Senv' | error -------------------------------------

------------------
f |- s, => (0,0),0

f |- s,d => s',f'
f[f']|- s+s',T => s'',m
-----------------------------------------
f |- s,d type X=T => s'+s'',f'[X:=type m]

f |- s,d => (n,g),f'
------------------------------------------------------------------------
f |- (n,g),d enum X={xi} => (n+1,g[n:=enum]),f'[X:=type n,{xi:=const n}]

f |- s,d => s',f'
f[f']|- s+s',T => s'',m
---------------------------------------
f |- s,d var x:T => s'+s'',f'[x:=var m]

f |- s,d => s',f'
f[f'],s'+s' |- e => m
---------------------------------------
f |- s,d const x=e => s',f'[x:=const m]

f |- s,d => s',f'
f[f'],s+s' |- c => ok
-----------------------------------
f |- s,d proc x=c => s',f'[x:=proc]


Senv,Sstate |- v => TV | error ------------------------------------------------

f(x)= var m
-----------------
f,(n,g) |- x => m

f,(n,g) |- v => m
f,(n,g) |- e => m1
f(m)=array m1 m2
---------------------
f,(n,g) |- v[e] => m2

f,(n,g) |- v => m
f(m)=record {xi:mi}
---------------------
f,(n,g) |- v.xi => mi

(* analogomente per i tipi union, dove il controllo sul valore del
   tag puo' essere fatto solo a run-time *)


Senv,Sstate |- e => TV | error ------------------------------------------------

f(x)=const m
-----------------
f,(n,g) |- x => m

f,(n,g) |- v => m
-----------------
f,(n,g) |- v => m

f,(n,g) |- ei => mi
op:{mi}->m (* devono essere nomi di tipi base *)
------------------------------------------------
f,(n,g) |- op({ei}) => m

Senv,Sstate |- c => ok | error ------------------------------------------------

f |- s,d => s',f'
f[f'],s+s' |- ci => ok
------------------------------
f,s |- begin d; {ci} end => ok

(* questa regola non permette definizioni ricorsive in d *)

f[f'] |- s+(0,g'),d => s',f' dove (n',g')=s'
f[f'],s+s' |- ci => ok
------------------------------
f,s |- begin d; {ci} end => ok

(* questa regola permette definizioni in d mutuamente ricorsive, in
   pascal la ricorsione e' limitata ai tipi puntatore e alle
   procedure, cioe' nella loro definizione si puo' fare riferimento a
   identificatori non ancora definiti *)