(** AST non typé *)

type expr =
  | Int of int
  | String of string
  | Concat of expr*expr
  | Add of expr*expr
  | Substring of expr*expr*expr
  | Pair of expr*expr
  | Fst of expr
  | Snd of expr

(** Valeurs *)

type value =
  | VInt of int
  | VString of string
  | VPair of value*value

(** Evaluateur non typé *)

let rec eval = function
  | Int i -> VInt i
  | String s -> VString s
  | Concat (a,b) ->
      begin match eval a, eval b with
        | VString sa, VString sb -> VString (sa^sb)
        | _ -> failwith "eval error"
      end
  | Add (a,b) ->
      begin match eval a, eval b with
        | VInt sa, VInt sb -> VInt (sa+sb)
        | _ -> failwith "eval error"
      end
  | Substring (a,b,c) ->
      begin match eval a, eval b, eval c with
        | VString a, VInt b, VInt c ->
            VString (String.sub a b c)
        | _ -> failwith "eval error"
      end
  | Pair (a,b) -> VPair (eval a, eval b)
  | Fst e ->
      begin match eval e with
        | VPair (a,b) -> a
        | _ -> failwith "eval error"
      end
  | Snd e ->
      begin match eval e with
        | VPair (a,b) -> b
        | _ -> failwith "eval error"
      end

(** Expressions bien typées
  *
  * On représente les types de notre minilangage directement
  * par les types OCaml int, string, et les produits formés
  * à partir de ceux-ci.
  *
  * Un AST de type T wtexpr peut être vu comme un AST de type
  * expr, sauf que les contraintes de typage des GADTs d'OCaml
  * imposent que l'AST est bien typé. *)

type _ wtexpr =
  | WInt : int -> int wtexpr
  | WString : string -> string wtexpr
  | WConcat : string wtexpr * string wtexpr -> string wtexpr
  | WAdd : int wtexpr * int wtexpr -> int wtexpr
  | WSubstring : string wtexpr * int wtexpr * int wtexpr -> string wtexpr
  | WPair : 'a wtexpr * 'b wtexpr -> ('a*'b) wtexpr
  | WFst : ('a*'b) wtexpr -> 'a wtexpr
  | WSnd : ('a*'b) wtexpr -> 'b wtexpr

(** Evaluateur d'expressions bien typées
  *
  * Cette fois ci on renvoie directement une valeur OCaml
  * de type t, sans avoir à définir un type value. En effet,
  * il n'y a pas d'ambiguité quand on sait quel type avait
  * la wtexpr au départ. *)

let rec wteval : type t. t wtexpr -> t = function
  | WInt i -> i
  | WString s -> s
  | WAdd (a,b) -> wteval a + wteval b
  | WConcat (a,b) -> wteval a ^ wteval b
  | WSubstring (s,a,b) -> String.sub (wteval s) (wteval a) (wteval b)
  | WPair (a,b) -> (wteval a, wteval b)
  | WFst a -> fst (wteval a)
  | WSnd a -> snd (wteval a)

(** Type "singleton" pour les types de notre langage
  *
  * Il s'agit de se donner des valeurs pour représenter les
  * types (int, string, int*string, etc.) qui ne sont actuellement
  * que des types OCaml. On utilise un GADT en faisant en sorte
  * qu'il y ait bijection entre valeurs et types. *)

type _ typ =
  | TInt : int typ
  | TString : string typ
  | TPair : 'a typ * 'b typ -> ('a*'b) typ

(** Typeur
  *
  * Etant donné une expr, vérifie si elle est bien typée.
  * Si ce n'est pas le cas, lève une exception. Sinon, renvoyée
  * un type "existentiel" qui contient l'AST typé et son type.
  *
  * NB: l'AST sous-jacent n'est pas modifié (en particulier, il
  * n'est pas évalué) mais seulement annoté. *)

type iswtexpr =
  | IsWT : 'a typ * 'a wtexpr -> iswtexpr

let rec typecheck : expr -> iswtexpr = function
  | Int i -> IsWT (TInt, WInt i)
  | String s -> IsWT (TString, WString s)
  | Add (a,b) ->
      begin match typecheck a, typecheck b with
        | IsWT (TInt, a), IsWT (TInt, b) ->
            IsWT (TInt, WAdd (a,b))
        | _ -> failwith "typecheck error"
      end
  | Concat (a,b) ->
      begin match typecheck a, typecheck b with
        | IsWT (TString, a), IsWT (TString, b) ->
            IsWT (TString, WConcat (a,b))
        | _ -> failwith "typecheck error"
      end
  | Substring (a,b,c) ->
      begin match typecheck a, typecheck b, typecheck c with
        | IsWT (TString, a), IsWT (TInt, b), IsWT (TInt, c) ->
            IsWT (TString, WSubstring (a,b,c))
        | _ -> failwith "typecheck error"
      end
  | Pair (a,b) ->
      let IsWT (ta,a) = typecheck a in
      let IsWT (tb,b) = typecheck b in
        IsWT (TPair (ta,tb), WPair (a,b))
  | Fst a ->
      begin match typecheck a with
        | IsWT (TPair (t,t'), a) -> IsWT (t, WFst a)
        | _ -> failwith "typecheck error"
      end
  | Snd a ->
      begin match typecheck a with
        | IsWT (TPair (t,t'), a) -> IsWT (t', WSnd a)
        | _ -> failwith "typecheck error"
      end

(** Un petit test: prend en entrée une expr, la type, l'évalue,
  * et affiche le résultat, de façon explicite si c'est un objet
  * de type int ou string. *)

let test expr =
  let IsWT (t,e) = typecheck expr in
  let v = wteval e in
    match t with
      | TInt -> Printf.printf "-> %d\n" v
      | TString -> Printf.printf "-> %S\n" v
      | _ -> Printf.printf "<_,_>\n"

let () =
  (* Devrait afficher 15. *)
  test (Add (Int 3, Fst (Snd (Pair (String "", Pair (Int 12, Int 0))))))