(* Corrige examen Systemes Synchrones, MPRI 2.23-1. 2018/2019 *) Notation Haskell: \x -> e pour fun x -> e (OCaml) let x = e1 in e2 pour let rec x = e1 in e2. data f = C t1 t2 pour type f = C of t1 * t2. J'utilise les notations OCaml a chaque fois que possible; le programmeur Haskell corrigera aisement. Q1: spair x y = lift2 (\x, y -> (x, y)) x y sfst x = lift1 (\(x, y) -> x) x snd x = lift1 (\(x, y) -> y Q2: (* mini-langage *) type p = d list and d = Node of string * string * e and e = | Epre of v * e | Eimmediate of v | Evar of string | Epair of e * e | Efst of e | Esnd of e | Eop1 of string * e | Eop2 of string * e * e | Emux of e * e * e | Eapp of string * e | Elet of string * e * e | Erec of string * e and v = Int of int | Bool of bool (* mini-haskell *) type hp = hd list and hd = Fun of string * string * he and he = | Hident of string | Himmediate of v | Hvar of string | Happ of he * he list | Hlet of string * he * he let rec trad_vers_haskell d_list = List.map trad_def d_list (* pour simplifier, on fait l'hypothese que let definitions locales *) (* [let x = e1 in e2] sont telles que x n'apparait pas dans e1. *) and trad_def (Node(f, x, e)) = match e with | Epre(v, e) -> Happ (Hident "pre") [trad_immediate v; trad_exp e] | Eimmediate(v) -> trad_immediate v | Evar(x) -> Hvar x | Epair(e1, e2) -> Happ (Hident (",")) [trad_exp e1; trad_exp e2] | Efst(e) -> Happ (Hident ("fst")) [trad_exp e] | Eop1(f, e) -> Happ (Hident f) [trad_exp e] | Eop2(f, e1, e2) -> Happ (Hident f) [trad_exp e1; trad_exp e2] | Emux(e1, e2, e3) -> Happ (Hident "mux") [trad_exp e1; trad_exp e2; trad_exp e3] | Eapp(f, e) -> Happ (Hident f) [trad_exp e] | Elet(x, e1, e2) -> Hlet(x, trad_exp e1, trad_exp e2) | Erec(x, e) -> Hlet(x, trad_exp e, Hident(x)) Q3: co_lift1 op (Co f s) = Co (\s -> let v, s' = f s in op v, s') s co_lift2 op (Co f1 s1) (Co f2 s2) = Co (\(s1, s2) -> let v1, s1' = f1 s1 in let v2, s2' = f2 s2 in op v1 v2, (s1', s2')) (s1, s2) co_mux (Co f1 s1) (Co f2 s2) (Co f3 s3) = Co (\(s1, s2, s3) -> let v1, s1' = f1 s1 in let v2, s2' = f2 s2 in let v3, s3' = f3 s3 in if v1 then v2 else v3, (s1', s2', s3')) (s1, s2, s3) Q4: Il y en a une infinite. L'equivalence entre (Co f1 s1) et (Co f2 s2) dont il est question ici est la bisimulation. Nous sommes dans un cas plus simple cependant puisque f1 et f2 sont des fonctions, et non des relations. 1. La plus simple, sans calcul du resultat: Co (\() -> (1 * 2) + 3, ()) () 2. L'application des operations donne: co_lift0 1 = Co (\() -> 1, ()) () co_lift0 2 = Co (\() -> 2, ()) () co_lift0 3 = Co (\() -> 3, ()) () Co F S = lift1 (*) (co_lift0 1) (co_lift0 2) = Co (\(s1, s2) -> let v1, s1' = (fun () -> 1, ()) s1 in let v2, s2' = (fun () -> 2, ()) s2 in v1 * v2, (s1', s2')) ((), ()) co_lift1 (+) F (lift0 3) = Co (\((s1, s2), s3) -> let v, (s1', s2') = F (s1, s2) in let v3, s' = (fun () -> 3, ()) () in v + v3, ((s1', s2'), s')) (((), ()), ()) Le programme donne se simplifie, par exemple, en: Co (\(s_pre1, s_pre2) -> (s_pre1 + s_pre2, (1, 3))) (0, 2) Q5: Co (\(s_pre0, s_pre1) -> s_pre0, (s_pre1, 2)) (0, 1) Q6: Co (\(s_pre1, s_pre0) -> let fib = s_pre1 in let v = fib + s_pre0 in fib, (v, fib) (1, 0) Q7: co_pre v (Co f s) = Co (\(s_pre, s) -> let v, s' = f s in s_pre, (v, s')) (v, s) Q8: Une application synchrone est telle que pour produire la valeur courante de la sortie, il suffit de donner a p la valeur courante de l'entree. co_apply (CoP p ps) (Co f s) = Co (\(s, ps) -> let v, s' = f s in let v', ps' = p ps v in v', (s', ps')) (s, ps) Q9: co_pipe proc1 proc2 x = co_apply proc1 (co_apply proc2 x) Q10: Une recusion sur les suites se traduit en une recursion dans l'instant. On profite ici de l'expressivite de la paresse qui permet de ne pas avoir a realiser d'ordonnancement statique. co_fix (CoP p ps) (Co f s) = Co (\(ps, s) -> let v, s' = f s in (* attention: il faut bien une recusion ici *) let rec v', ps' = p ps (v, v') in v', (ps', s')) (ps, s) Q11: La traduction procede de la meme maniere. Vous remplacer chaque operation par leur version co-iterative. Q12: La propriete d'execution en memoire bornee se deduit directement de la signature des operateurs. Une valeur Co f s est de type CoStream S A. La taille maximale utilisee est celle de S. Notez que l'inference de type de Haskell calcule automatiquement la taille de la memoire necessaire. Q13. Dans le cas ou toutes les variables de recursion apparaissent a droite d'un retard, la recursion let rec v', ps' = p ps (v, v') in ... peut etre traduite en une sequence de definitions (let) sans recursion. Pour vous en convaincre, reprenons l'exemple du calcul de la suite de fibonacci: rec fib = pre 1 (plus fib (pre 0 fib)) dummy = Co (fun () -> ()) () Par definition de co_fix: co_fix (CoP (\(s_pre1, s_pre0), (_, fib) -> let fib = s_pre1 in let v = fib + s_pre0 in fib, (v, fib)) (1, 0)) dummy = Co (\((s_pre1, s_pre0), ()) -> let fib, (s_pre1', s_pre0') = (\(s_pre1, s_pre0), (_, fib) -> let fib = s_pre1 in let v = fib + s_pre0 in fib, (v, fib)) (s_pre1, s_pre0), ((), fib) in fib, ((s_pre1', s_pre0'), ())) ((1, 0), ()) = Par beta-reduction du membre interne: Co (\((s_pre1, s_pre0), ()) -> let fib, (s_pre1', s_pre0') = let fib = s_pre1 in let v = fib + s_pre0 in fib, (v, fib) in fib, ((s_pre1', s_pre0'), ())) ((1, 0), ()) = Par deplacement des let et let/rec: Co (\((s_pre1, s_pre0), ()) -> let fib1 = s_pre1 and v = fib1 + s_pre0 and fib = fib1 and (s_pre1', s_pre0') = (v, fib1) in fib, ((s_pre1', s_pre0'), ())) ((1, 0), ()) = Par ordonnacement statique des equations: Co (\((s_pre1, s_pre0), ()) -> let fib1 = s_pre1 in let v = fib1 + s_pre0 in let fib = fib1 in let (s_pre1', s_pre0') = (v, fib1) in fib, ((s_pre1', s_pre0'), ())) ((1, 0), ()). Et on peut continuer encore un peu ! Les techniques presentees ici se generalisent au cas de fonctions d'ordre superieur (cf. Caspi et Pouzet, 98).