(**
   Langages : sémantique et modèles d'exécution.
   Thibaut Balabonski @ Université Paris-Sud, M2 FIIL.

   Cours 2, 18 septembre 2017.
   Continuations
*)

(**
   Point de départ : on définit une tâche, qu'on instancie trois fois,
   exécutées l'une après l'autre.
   Cet exemple est repris du cours de Xavier Leroy.
*)

let sequential_task message increment =
  let rec loop n =
    (* Tant que [n] < 10 ... *)
    if n >= 10 then () else begin
      (* Afficher le message et la valeur de [n] *)
      print_string message; print_int n;
      (* Puis incrémenter [n] et recommencer *)
      loop(n + increment)
    end
  in
  loop 0

(*
  let _ =
    sequential_task " A" 1;
    sequential_task " B" 2;
    sequential_task " C" 3
*)

(**
   On veut créer une variante dans laquelle les différentes tâches peuvent
   se passer la main en cours de route.
   Pour cela, chaque tâche peut volontairement s'interrompre avec une
   primitive [yield], qui met en suspens le reste du calcul et permet à
   une autre tâche de reprendre au point où elle s'était arrêtée précédemment.

   On n'a pas de moyen primitif de capturer "le reste du calcul" pour en
   créer une suspension (certains langages ont une fonction [callcc] pour
   faire exactement cela).
   On va coder ça indirectement en représentant dès l'origine les morceaux
   de code susceptibles d'être suspendus par des fonctions.

   On va se donner une file d'attente des différentes tâches ou suspensions
   à exécuter, et les primitives suivantes :
   - [fork: (unit -> unit) -> unit] telle que [fork f] place la suspension [f]
     dans la file d'attente.
   - [yield: (unit -> unit) -> unit] telle que [yield k] place la suspension [f]
     dans la file d'attente et relance la première tâche en attente.
   - [terminate: unit -> unit] qui termine la tâche courante et relance la
     première tâche en attente.

   Le code serait alors :
   
   let task message increment =
     let rec loop n =
       (* Elle s'arrête explicitement à la fin de la boucle. *)
       if n >= 10 then terminate() else begin
         print_string message; print_int n;
         (* Après chaque tour de boucle, elle s'interrompt et passe la main
            à une autre tâche, après avoir placé dans la file d'attente la
            suspension correspondant au tour de boucle suivant. *)
 	 yield(fun () ->
	   loop(n + increment));
       end
     in
     loop 0

   let _ =
     fork(fun () -> task " A" 1);
     fork(fun () -> task " B" 2);
     fork(fun () -> task " C" 3);
     terminate()
*)
  

(**
   File d'attente et primitives

   Version brutale : la file d'attente est une référence sur une liste.
*)
let queue = ref []
  
let enqueue t =
  queue := !queue @ [t]
    
let dequeue () =
  match !queue with
    | [] -> raise Not_found
    | t::q' -> queue := q'; t
      
let is_empty () =
  !queue = []

(**
   Implémentations des primitives.
*)
let fork (t: unit -> unit) =
  enqueue t
    
let yield k =
  (* D'abord, s'interrompre et se placer dans la file *)
  enqueue k;
   (* Ensuite, lancer la première tâche de la file.
      Remarque sur le type : l'appel de fonction [dequeue ()] renvoie la
      première tâche en attente dans la file, c'est-à-dire une suspension.
      Pour relancer cette tâche on l'applique donc à [()].
   *)
  let next = dequeue () in
  next ()
    
let terminate () =
  (* S'il n'y a plus de tâche en attente, point final. *)
  if is_empty ()
  then exit 0
  else (dequeue ()) ()  (* Équivalent à let next = dequeue () in next () *)
    
let task message increment =
  let rec loop n =
    if n >= 10 then terminate() else begin
      print_string message; print_int n;
      yield(fun () ->
	loop(n + increment));
    end;
  in
  loop 0

(*
  let _ =
    fork(fun () -> task " A" 1);
    fork(fun () -> task " B" 2);
    fork(fun () -> task " C" 3);
    terminate()
*)

(**
   Bilan : on a pu encoder des mécanismes de concurrence (interruption et
   relance de tâche) en n'utilisant que des mécanismes fonctionnels.
   La notion cruciale ici était celle de "continuation" : une représentation
   de "ce qui doit être fait après".
*)

(**
   Continuation-Passing Style

   Transformation à appliquer à un programme fonctionnel.
   Rend le flot de contrôle explicite.

   Transforme un terme en une fonction qui prend en paramètre une continuation,
   cette continuation représentant ce qui doit être fait une fois la valeur
   du terme obtenue.

   Pour les constantes, les variables ou les valeurs, on ne fait rien de
   spécial.

         ⟦N⟧ = λk.k N
         ⟦x⟧ = λk.k x
      ⟦λx.a⟧ = λk.k (λx.⟦a⟧)

   Pour l'application, il faut décomposer le calcul :
   - on calcule d'abord la valeur de a₁, qui sera appelée v₁ dans la
     continuation,
   - la continuation calcule ensuite la valeur de a₂, qui sera appelée v₂
     dans sa propre continuation,
   - puis la première valeur v₁ est appliquée à la deuxième v₂, et le tout est
     passé à la continuation englobante [k].

     ⟦a₁ a₂⟧ = λk.⟦a₁⟧ (λv₁.⟦a₂⟧ (λv₂. k (v₁ v₂)))

   Exemple de transformation

     ⟦(λx.a)b⟧
       = λk. ⟦λx.a⟧ (λv₁.⟦b⟧ (λv₂. k (v₁ v₂)))
       = λk. (λk₀.k₀(λx.⟦a⟧)) (λv₁.(λk₁.k₁b) (λv₂. k (v₁ v₂)))
       = λk. (λk₀.k₀(λx.(λk₂.k₂a))) (λv₁.(λk₁.k₁b) (λv₂. k (v₁ v₂)))
   
   Le terme transformé contient de nombreuses applications artificielles qui
   peuvent être réduites. On parle de "réductions administratives", qui sont
   des artefacts de la transformations et ne sont pas vraiment pertinentes
   pour le terme d'origine.
   On peut obtenir un terme simplifié en les réduisant :
     ⟶β λk. (λk₀.k₀(λx.(λk₂.k₂a))) (λv₁.(λv₂. k (v₁ v₂)) b)
     ⟶β λk. (λk₀.k₀(λx.(λk₂.k₂a))) (λv₁. k (v₁ b))
     ⟶β ...
   Mais il n'est pas évident de distinguer les réductions administratives de
   celles qui concernent vraiment le terme d'origine.

   Alternative : transformations en une passe, qui regardent un peu plus
   finement le terme pour un résultat garanti sans réductions administratives.
   (Voir Danvy & Nielsen, One-Pass CPS)

   Ces transformations peuvent être appliquées à différents programmes
   fonctionnels. Nous allons explorer certains des effets que cela peut avoir.
*)

(**
   Considérons d'abord la fonction [List.map] habituelle.
     [map : ('a -> 'b) -> 'a list -> 'b list]
   Son code ressemble à ceci.
*)

let rec map f l =
  match l with
    | []    -> []
    | a::l' -> (f a) :: (map f l')

(**
   Ce code est récursif, mais pas récursif terminal : l'appel à [map f l']
   n'est pas la dernière action effectuée (il reste la concaténation).
   Un nouveau tableau d'activation est donc créé sur la pile pour chaque
   appel récursif, ce qui peut amener à dépasser la capacité de la pile.

   Pour observer ceci, il suffit de construire une grande liste.
*)

let rec make_list a n =
  if n = 0
  then []
  else a :: (make_list a (n-1))

(**
   Ce code n'est pas non plus récursif terminal, la simple construction de
   la liste va donc déjà saturer la pile.

   Une stratégie usuelle consiste à utiliser une fonction auxiliaire
   récursive terminale prenant en paramètre supplémentaire un accumulateur
   produisant petit à petit le résultat.
*)
    
let make_list a n =
  (* Définition de la fonction auxiliaire. On ne répète pas le
     paramètre [a], qui ne varie pas d'un appel récursif à l'autre. *)
  let rec make_list_aux n acc =
    if n=0
    (* À la fin, renvoyer l'accumulateur. *)
    then acc
    (* Sinon, ajouter un élément à l'accumulateur,
       puis appel récursif terminal. *)
    else make_list_aux (n-1) (a::acc)
  in
  (* Initialisation : on commence avec l'accumulateur vide. *)
  make_list_aux n []

(* Cette création de liste fonctionne, mais l'appel à [map] provoquerait
   un dépassement de pile. *)
let biglist = make_list 1 1000000
(* let _ = map (fun x -> x+1) biglist *)

(**
   On pourrait appliquer la même stratégie de l'accumulateur à la
   fonction [map].
   Remarquez cependant que, chaque nouvel élément considéré étant ajouté
   en tête de l'accumulateur, la liste produit est inversée.
   On ajoute donc un appel à une fonction [rev] pour renverser la liste.
*)

let rec rev l acc =
  match l with
    | []    -> acc
    | a::l' -> rev l' (a::acc)
  
let map f l =
  let rec map_aux l acc =
    match l with
      | []    -> rev acc []
      | a::l' -> map_aux l' ((f a)::acc)
  in
  map_aux l []

(* let _ = map (fun x -> x+1) (make_list 1 10000000) *)

    
(**
   Le style de programmation par passage de continuations donne un moyen
   alternatif et systématique d'obtenir un code récursif terminal : chaque
   appel récursif est terminal, et prend en paramètre une continuation
   qui va reconstruire le résultat à la fin.
*)

let rec cps_map f l k =
  match l with
    (* Si la liste est vide, le résultat est [], et on lui applique
       la continuation. *)
    | []    -> k []
    (* Si la liste n'est pas vide, on note [res] le résultat de [map] appelée
       récursivement sur la queue de la liste, et on définit une nouvelle
       continutation qui va ajouter le nouvel élément [f a] en tête de [res]
       avant de passer ce résultat à la continuation englobante.
    *)
    | a::l' -> let a' = f a in
	       cps_map f l' (fun res -> k (a' :: res) )

(**
   Pour exécuter une fonction écrite en style CPS, on peut par exemple lui
   donner comme continuation la fonction identité, qui renvoie directement
   le résultat produit.
*)
		 
let map f l = cps_map f l (fun x -> x)


(**
   Exemple de l'action de [cps_map].
   On se donne la fonction [f] == [fun x -> x+1],
   et on note [id] == [fun x -> x].
   Les différentes étapes du calcul sont :

   cps_map f [0; 2; 4] id

   cps_map f [2; 4] (fun res -> id (1 :: res))

   cps_map f [4] (fun res' ->
                   (fun res -> id (1 :: res))
                   (3 :: res')
                 )

   cps_map f [] (fun res'' ->
                  (fun res' ->
                    (fun res -> id (1 :: res))
                    (3 :: res')
                  ) (5 :: res'')
                )

   (fun res'' ->
     (fun res' ->
       (fun res -> id (1 :: res))
       (3 :: res')
     ) (5 :: res'')
   ) []

   (fun res' ->
     (fun res -> id (1 :: res))
     (3 :: res')
   ) (5 :: [])

   (fun res -> id (1 :: res))
   (3 :: 5 :: [])

   id (1 :: 3 :: 5 :: [])

   [1; 3; 5]

   
   L'utilisation totale de mémoire reste importante : la continuation créée
   à la fin des itérations de [cps_map] contient en réalité une fonction,
   c'est-à-dire une clôture, par élément de la liste, comme c'était le cas
   pour les tableaux d'activation dans la première version.
   
   La différence est que cette mémoire n'est plus prise dans la pile, mais
   dans le tas, qui est généralement moins restreint.
   Nous allons voir maintenant une autre transformation de programmes,
   qui permet d'éviter cette création de multiples fonctions.
*)
      
(* let _ = map (fun x -> x+1) (make_list 1 10000000) *)


(**
   Défonctionalisation.

   Objectif : transformer les fonctions en 'autre chose'.
   Langage source : langage avec fonctions générales (peuvent avoir des
   variables libres, et considérées comme "éléments de première classe")
   Langage cible : n'importe quel langage de "premier ordre" (sans notion
   avancée de fonctions)

   Idée : remplacer les fonctions par des structures de données.
   - On prend toutes les fonctions du programme
   - À chacune on associe un constructeur
   - On ajoute une fonction "apply" qui effectue le calcul voulu quand
     une "fonction" est appliquée à ses arguments.

   Exemple sur un λ-terme :
     λx.λy.x 

   À chaque fonction on associe un constructeur :
     C₁ pour λx.λy.x
     C₂ pour λy.x
   
   On donne en argument aux constructeurs les variables libres des
   fonctions correspondantes.
   Fonctions :
     | C₁ 
     | C₂(x)

   La fonction [apply] code ensuite le comportement de la fonction associée
   à chaque constructeur :

   Apply(f, arg) = match f with
     | C₁    -> let x = arg in C₂(x)
     | C₂(x) -> x
*)

(**
   Sur notre exemple, on veut transformer :

   let rec cps_map f l k =
     match l with
       | []    -> k []
       | a::l' -> let a' = f a in
                  cps_map f l' (fun res -> k (a' :: res) )

   let map f l = cps_map f l (fun res -> res)

   On a deux fonctions anonymes pour définir nos continuations :
     [fun res -> res], sans variables libres
     [fun res -> k (a' :: res)], avec variables libres [k] et [a']

   On se donne donc deux constructeurs [End] et [Elt], le deuxième
   possédant deux paramètres.
   La fonction [apply] calcule le résultat de l'application d'une
   continuation. On utilisera le nom [cont] au lieu de [k] pour rappeler
   qu'on manipule une continuation défonctionnalisée, et plus une fonction
   en tant que telle.
*)
  
type 'a cont =
  | End
  | Elt of 'a * 'a cont
      
let rec apply cont res =
  match cont with
    | End           -> res                     (* fun res -> res          *)
    | Elt(a, cont') -> apply cont' (a :: res)  (* fun res -> k (a :: res) *)

(**
   Maintenant, au lieu de construire une clôture pour définir la nouvelle
   continuation, chaque appel à [cps_map] construit une nouvelle structure
   de type ['a cont].
   À la fin, cette continuation défonctionnalisée est appliquée avec [apply].
*)
      
let rec cps_map f l cont =
  match l with
    | []    -> apply cont []
    | a::l' -> cps_map f l' (Elt(f a, cont))
      
let map f l = cps_map f l End

(**
   Reprenons notre exemple.
   On a toujours [f] == [fun x -> x+1] et [id] == [fun x -> x].
   
   cps_map f [0; 2; 4] End
   cps_map f [2; 4]    Elt(1, End)
   cps_map f [4]       Elt(3, Elt(1, End))
   cps_map f []        Elt(5, Elt(3, Elt(1, End))) 
   apply (Elt(5, Elt(3, Elt(1, End)))) []
   apply (Elt(3, Elt(1, End)))        (5 :: [])
   apply (Elt(1, End))                (3 :: 5 :: [])
   apply  End                         (1 :: 3 :: 5 :: [])
   [1; 3; 5]
*)

(**
   Pour finir sur cet exemple, remarquez que le type ['a cont] est
   tout à fait semblable au type ['a list] de Caml :

     type 'a list =
       | Nil
       | Cons of 'a * 'a list

   On peut donc finalement dans ce cas se rabattre sur le type déjà
   existant des listes plutôt que d'en recréer un soi-même.
*)

let rec apply cont res =
  match cont with
    | []       -> res
    | a::cont' -> apply cont' (a :: res)
      
let rec cps_map f l cont =
  match l with
    | []    -> apply cont []
    | a::l' -> cps_map f l' (f a :: cont)
      
let map f l = cps_map f l []

(**
   Pour mémoire, voici le code que nous avions écrit pour obtenir "à la main"
   une fonction récursive terminale, avec utilisation d'un accumulateur et
   d'une fonction auxiliaire de retournement.

   let rec rev l acc =
     match l with
       | []    -> acc
       | a::l' -> rev l' (a::acc)
  
   let map f l =
     let rec map_aux l acc =
       match l with
         | []    -> rev acc []
         | a::l' -> map_aux l' ((f a)::acc)
     in
     map_aux l []

   C'est exactement la même chose.
   Il y a cependant une différence de méthode : produire ce code en
   enchaînant transformation CPS et défonctionnalisation est une procédure
   automatisable.
*)
  


(**
   Autre aspect des continuations : expliciter et manipuler le flot de
   contrôle.

   On se donne la tâche suivante : chercher dans une liste [l] un élément
   vérifiant une certaine propriété [p].

   Dans ce premier code naturel, on écrit à la fois le code correspondant au
   parcours de la liste et celui correspondant à la recherche de l'élément.
*)
let rec find p l =
  match l with
    | []    -> None
    | a::l' -> if p a then Some a else find p l'

(**
   Que faire si on veut plutôt réutiliser une fonction d'itération déjà
   existante, comme [List.iter] ?
     [iter (f: 'a -> unit) (l: 'a list) : unit]
   On peut par exemple lever une exception quand l'élément est trouvé, pour
   modifier le flot de contrôle normal.
*)
let rec iter f l = match l with
  | []    -> ()
  | a::l' -> f a; iter f l'
	
exception Found of int
let find p l =
  try
    iter (fun a -> if p a then raise (Found a)) l;
    None
  with
    | Found a -> Some a

let print_result = function
  | Some a -> print_int a
  | None   -> print_string "none"
    
(* let _ = print_result (find (fun x -> x mod 2 = 0) [1; 3; 4; 6; 7]) *)

(**
   Les continuations donnent une manière alternative de représenter et
   manipuler le flot de contrôle.
   On donne d'abord une version avec continuations de [iter], qui prend
   en paramètre supplémentaire une continuation spécifiant ce qui doit
   être fait à la fin de l'itération.
   On demande aussi à ce que le premier paramètre (la fonction), soit
   en style par passage de continuations : elle attend en deuxième paramètre
   une continuation qui lui indiquera où reprendre l'exploration de la liste
   une fois qu'elle aura traité l'élément courant.
*)

let rec iter f l k = match l with
  | []    -> k ()
  | a::l' -> f a (fun () -> iter f l' k)

(**
   À partir de là, la fonction itérée peut choisir entre effectivement suivre
   la continuation qui lui a été fournie (et qui poursuit l'itération), ou
   faire autre chose.
   Cette fonction par exemple renvoie directement [Some a] si le test est
   positif, et suit la continuation sinon.
*)

let test p a k =
  if p a
  then Some a
  else k()
    
(**
   On obtient alors pour [find] une simple combinaison de ces deux fonctions,
   en passant à [iter] une continuation qui demande de renvoyer [None] si
   le calcul arrive jusqu'au bout de la liste.
*)
    
let find p l = iter (test p) l (fun () -> None)

(**
   On peut encore le réécrire sous une forme plus proche du précédent en
   faisant de la fonction [test] une fonction anonyme.
*)

let find p l =
  iter (fun a k -> if p a then Some a else k()) l (fun () ->
    None)
  
let _  = print_result (find (fun x -> x mod 2 = 0) [1; 3; 4; 6; 7])
let _  = print_result (find (fun x -> x mod 2 = 0) [1; 3; 5])

(**
   De manière générale, on peut représenter ces deux manières de s'exécuter
   en donnant deux continuations à [test], une pour chaque issue.

   let test p a k k' =
     if p a
     then k' a
     else k ()

   Le TP propose d'explorer cette CPS "à deux canons".
*)