Exercice 1:
-----------

[
  FUN f int [x:bool,y:int](if x y 0);
  ECHO ([b:bool](f b 42) true)
]

G0 |- (FUN f int [x:bool,y:int](if x y 0)) : G0[f:bool->int->int]
- G0[x:bool,y:int] |- (if x y 0) : int
  - G0[x:bool,y:int] |- x : bool
  - G0[x:bool,y:int] |- y : int
  - G0[x:bool,y:int] |- 0 : int

soit G = G0[f: bool -> int -> int] 
G |- ([b:bool](f b 42) true) : int
- G |- [b:bool](f b 42) : bool -> int
  - G[b:bool] |- (f b 42) : int
    - G[b:bool] |- f : bool -> int -> int
    - G[b:bool] |- b : bool
    - G[b:bool] |- 42 : int
- G |-  true : bool

Exercice 2:
-----------
[] désigne l'environnement vide et $ le flux de sortie vide.

[
  CONST x int 42;
  FUN f [x:bool](if x 0 1);
  ECHO (add x (f true))
]

|- p ~> (42.$)

On ne détaille pas les applications des règles sémantiques pour (CMDS)

|- CONST x int 42 ~> [x=inZ(42)] (règle (CONST))
[x=inZ(42)]|- FUN f [x:bool](if x 0 1) ~> [x=inZ(42);f=InF((if x 0 1),[x],[x=inZ(42)])] (règle (FUN))
soit r1 =[x=inZ(42);f=InF((if x 0 1),[x],[x=inZ(42)])]
r1,$ |- ECHO (add x (f bool)) ~> (42.$) (règle (ECHO))
r1 |- (add x (f bool)) ~> inZ(42) (règle (PRIM2))
- r1 |- x ~> inZ(42) (règle (ID))
  car r1(x) = [x=inZ(42);f=inF(..)](x) = [x=inZ(42)](x) = inZ(42)
- r1 |- (f true) ~> inZ(0) (règle (APP))
  - r1 |- f ~> inF((if x 0 1),[x],[x=inZ(42)]) (règle (ID))
  - r1 |- true ~> inZ(1) (règle (TRUE))
  - r2 = [x=inZ(42);x=inZ(1)]
    r2 |- (if x 0 1) ~> inZ(0) (règle (IF1))
    - r2 |- x ~> inZ(1) car r2(x) = [x=inZ(42),x=inZ(1)](x) = inZ(1) (règle (ID))
    - r2 |- 0 ~> inZ(0) (règle (NUM))
- pi2(add)(42,0) = 42+0 = 42

Exercice 3:
-----------

Soit r = [f=inFR((if x 42 (f (not x))), f, [x], [])]

r |- (f false) ~> inZ(42) (règle (APPR))
- r |- f ~> inFR((if x 42 (f (not x))), f, [x], []) (règle (ID))
- r |- false ~> inZ(0) (règle (FALSE))
- r1 = [x=inZ(0); f=inFR((if x 42 (f (not x))), f, [x], [])]
  r1 |- (if x 42 (f (not x))) ~> inZ(42) (règle (IF0))
  - r1 |- x ~> inZ(0) (règle (ID))
  - r1 |- (f (not x)) ~> inZ(42) (règle (APPR))
    - r1 |- f ~> inFR(inFR((if x 42 (f (not x))), f, [x], []))
    - r1 |- (not x) ~> inZ(1) (règle (PRIM1))
      - r1 |- x ~> inZ(0)
    - r3 = [x=inZ(0)][f=inFR((if x 42 (f (not x))), f, [x], [])]
      r3 |- (if x 42 (f (not x))) ~> inZ(42) (règle (IF1))
      - r3 |- x ~> inZ(1) (règle (ID))
      - r3 |- 42 ~> inZ(42) (règle (NUM))