(**
   Langages, sémantiques et modèles d'exécution.
   Thibaut Balabonski @ Université Paris-Sud, 2018

   TP types, sous-types, polymorphisme et inférence.
   L'objectif de ce TP est de réaliser un système de typage pour un langage
   mélangeant des traits fonctionnels et impératifs.
*)

(**
   Exercice 1 : vérification des types simples.

   Langage de départ :
     lambda-calcul + constantes + paires + références + structures de contrôle
   avec annotations de types.

   Objectif : vérification des types.
*)

(** Types simples *)
module SimpleTypes = struct
    
  type typ =
    | TVar of string  (** Variables de type ['a] *)
    | TInt            (** Entiers [int]          *)
    | TBool           (** Booléens [bool]        *)
    | TUnit           (** Unité [unit]           *)
    | TFun  of typ * typ  (** Fonctions [T₁ ⟶ T₂]  *)
    | TPair of typ * typ  (** Paires [T₁ * T₂]       *)
    | TRef  of typ        (** Références [ref T]     *)

end
        
(** Expressions avec annotations de types *)
module BaseAST = struct
    
  type expression =
    | Int    of int    (** Entier [n]    *)
    | Bool   of bool   (** Booléen [b]   *)
    | Unit             (** Unité [()]    *)
    | Var    of string (** Variable  [x] *)
    | App    of expression * expression
                       (** Application [e₁ e₂] *)
    | Fun    of string * SimpleTypes.typ * expression
                       (** Fonction [fun x:T -> e] *)
    | Let    of string * expression * expression
                       (** Liaison [let x=e₁ in e₂] *)
    | Op     of string (** Opérateur *)
    | Pair   of expression * expression
                       (** Paire [(e₁, e₂)] *)
    | NewRef of expression
                       (** Création d'une référence initialisée [ref e] *)
    | Sequence of expression * expression
                       (** Séquence d'expressions [e₁; e₂] *)
    | If     of expression * expression * expression
                       (** Conditionnelle [if c then e₁ else e₂] *)
    | While  of expression * expression
                       (** Boucle [while c do e done] *)

  (** 
      Ensemble minimal d'opérateurs à prévoir pour le constructeur [Op]
      - arithmétique et logique :  "+", "<", "&&"
      - paires "fst", "snd"
      - références "deref", "setref"
  *)   
end
      
(**
   Vérificateur de types.
*)
module BaseTypeChecker = struct
  open SimpleTypes
  open BaseAST

  module Env = Map.Make(String)
  type type_env = SimpleTypes.typ Env.t

  (** 
      Objectif : compléter la fonction suivante de typage d'une expression.
      Un appel [type_expression env e] doit :
      - renvoyer le type de [e] dans l'environnement [env] si [e] est bien typée
      - déclencher une exception sinon      
  *)
  let rec type_expression (env: type_env) (e: expression) : typ =
    failwith "Not implemented"

end

  
(** 
    Exercice 2 : inférence des types simples.

    Ci-dessous, une syntaxe quasi-identique à [BaseAST].
    A disparu : l'annotation du paramètre formel d'une fonction par son type.

    Objectif : inférence de types.
*)
module RawAST = struct
  open SimpleTypes
    
  (** Expressions *)
  type expression =
    | Int    of int    (** Entier [n]    *)
    | Bool   of bool   (** Booléen [b]   *)
    | Unit             (** Unité [()]    *)
    | Var    of string (** Variable  [x] *)
    | App    of expression * expression
                       (** Application [e₁ e₂] *)
    | Fun    of string * expression
                       (** Fonction [fun x -> e] *)
    | Let    of string * expression * expression
                       (** Liaison [let x=e₁ in e₂] *)
    | Op     of string (** Opérateur *)
    | Pair   of expression * expression
                       (** Paire [(e₁, e₂)] *)
    | Newref of expression
                       (** Création d'une référence initialisée [ref e] *)
    | Sequence of expression * expression
                       (** Séquence d'expressions [e₁; e₂] *)
    | If     of expression * expression * expression
                       (** Conditionnelle [if c then e₁ else e₂] *)
    | While  of expression * expression
                       (** Boucle [while c do e done] *)

end
  
(**
   Moteur d'inférence de types
*)
module BaseTypeReconstruction = struct
  open SimpleTypes
  open RawAST

  (** 
      Objectif : compléter la fonction suivante de typage d'une expression.
      Un appel [type_expression e] doit :
      - renvoyer le type de [e] dans l'environnement [env] si [e] est bien typée
      - déclencher une exception sinon
      
      Procéder en deux étapes : génération de contraintes sur les types,
      puis résolution par unification.
  *)
  let rec type_expression (e: expression) : typ =
    failwith "Not implemented"

end

(** Bonus : version polymorphe *)

  
(**
   Exercice 3 : sous-typage.

   On ajoute un type optionnel [T?] désignant des valeurs de type [T]
   éventuellement non définies (contrairement au type [T] lui-même pour
   lequel la valeur est à coup sûr définie.

   On a donc la relation de sous-typage [T <: T?], de laquelle on déduit
   une relation plus générale avec les règles habituelles.
*)
module OptionTypes = struct

  (** Les types simples + un type optionnel *)
  type typ =
    | TVar of string      (** Variables de type ['a] *)
    | TInt                (** Entiers [int]          *)
    | TBool               (** Booléens [bool]        *)
    | TUnit               (** Unité [unit]           *)
    | TFun  of typ * typ  (** Fonctions [T₁ ⟶ T₂]  *)
    | TPair of typ * typ  (** Paires [T₁ * T₂]       *)
    | TRef  of typ        (** Références [ref T]     *)

    | TMaybe of typ       (** Type option [T?]       *)
    
end

(**
   Parallèlement à l'introduction du type optionnel, on modifie l'opérateur
   de création de référence, qui crée une référence non initialisée sur un
   type [T] donné en paramètre.
   L'expression [newref T] aura donc le type [ref T?].

   On crée également un opérateur ["isNull"] testant si une valeur donnée
   est indéfinie.
*)
module SubAST = struct

  type expression =
    | Int    of int    (** Entier [n]    *)
    | Bool   of bool   (** Booléen [b]   *)
    | Unit             (** Unité [()]    *)
    | Var    of string (** Variable  [x] *)
    | App    of expression * expression
                       (** Application [e₁ e₂] *)
    | Fun    of string * OptionTypes.typ * expression
                       (** Fonction [fun x:T -> e] *)
    | Let    of string * expression * expression
                       (** Liaison [let x=e₁ in e₂] *)
    | Op     of string (** Opérateur *)
    | Pair   of expression * expression
                       (** Paire [(e₁, e₂)] *)
    | NewRef of OptionTypes.typ
                       (** Création d'une référence non initialisée [newref T] *)
    | Sequence of expression * expression
                       (** Séquence d'expressions [e₁; e₂] *)
    | If     of expression * expression * expression
                       (** Conditionnelle [if c then e₁ else e₂] *)
    | While  of expression * expression
                       (** Boucle [while c do e done] *)

end

(**
   Vérification de types avec sous-typage.

   Ajouter du sous-typage au vérificateur de types simples, avec la règle
   algorithmique standard : le paramètre effectif d'un appel de fonction peut
   être un sous-type du type du paramètre formel.

   On ajoutera les particularités suivantes :
   - Tout opérateur travaillant sur des valeurs concrètes nécessitera des
     opérandes dont le type *n'est pas* un type optionnel.
   - Dans une expression de la forme [if isNull a then e₁ else e₂] avec [a] de
     type [T?], on pourra donner à [a] le type [T] dans la branche [e₂].
*)
module SubTypeChecker = struct
    

end


(**
   Exercice 4 : combiner l'inférence (exercice 2) et le sous-typage (exercice 3)
*)