(* --- Lexer : transforme le char stream en token stream ----------------- *)
   
type token = LAMBDA | FIX | COLON | DOT | AMPERSEND | EPSILON
           | LPAR | RPAR | IN | OUT | COERCE | SUPER | LET
           | SMALLER | HIDE | EQUAL | IDENT of string | ARROW
           | LBRACK | RBRACK | COMMA | INT | VAL of int | SUCC
           | PRED | EQZ | BOOL | TRUE | FALSE | ITE | SEMIC
           | STAR | QUEST | LBR | RBR;;

(* Elimine les espaces et les retours chariot *)
let rec spaces = function                                             
  [< '` ` | `\t` | `\n`; spaces _ >] -> ()
| [< >] -> ();;

  
let int_of_digit =
  function  `0`..`9` as c   -> (int_of_char c)-(int_of_char `0`)
      |      _  ->  failwith "Not a Digit";;
      

let rec integer n = function
  [< ' `0`..`9` as c; (integer (10*n+int_of_digit  c)) r>]  ->  r
| [<>]  -> VAL n;;

(* Reconnait les identificateurs et les mots reserves *)
let ident_buf = make_string 20 ` `;;                            
let rec ident len = function
  [< '(`a`..`z` | `A`..`Z`) as c;
     (if len >= 20 then ident len
                   else (set_nth_char ident_buf len c; ident (succ len))) s >] -> s
| [< >] -> (match sub_string ident_buf 0 len with 
      "in" -> IN
    | "out" -> OUT
    | "coerce" -> COERCE
    | "super" -> SUPER
    | "fix" -> FIX
    | "let" -> LET
    | "hide" -> HIDE
    | "bool" -> BOOL
    | "int" -> INT
    | "ite" -> ITE
    | "true" -> TRUE
    | "false" -> FALSE
    | "succ" -> SUCC
    | "pred" -> PRED
    | "eqz" -> EQZ
    | s -> IDENT s);;

(* Analyseur lexical *)
let rec lexer str = spaces str;                                                               
match str with
  [< '` `|`\t`|`\n`; spaces _>]  -> [< lexer str>]
| [< '`(`; spaces _ >] -> [< 'LPAR; lexer str >]        (* Reconnaissance des divers tokens *)
| [< '`)`; spaces _ >] -> [< 'RPAR; lexer str >]
| [< '`[`; spaces _ >] -> [< 'LBR; lexer str >]                     
| [< '`]`; spaces _ >] -> [< 'RBR; lexer str >]
| [< '`\\`; spaces _ >] -> [< 'LAMBDA; lexer str >]
| [< '`.`; spaces _ >] -> [< 'DOT; lexer str >]
| [<'`-`; '`>`; spaces _ >]  ->   [< 'ARROW; lexer str >]
| [< '`?`; spaces _ >] -> [< 'QUEST; lexer str >]
| [< '`*`; spaces _ >] -> [< 'STAR; lexer str >]
| [< '`=`; spaces _ >] -> [< 'EQUAL; lexer str >]
| [< '`&`; spaces _ >] -> [< 'AMPERSEND; lexer str >]
| [< '`@`; spaces _ >] -> [< 'EPSILON; lexer str >]
| [< '`<`; spaces _ >] -> [< 'SMALLER; lexer str >]
| [< '`{`; spaces _ >] -> [< 'LBRACK; lexer str >]
| [< '`}`; spaces _ >] -> [< 'RBRACK; lexer str >]
| [< '`,`; spaces _ >] -> [< 'COMMA; lexer str >]
| [< '`:`; spaces _ >] -> [< 'COLON; lexer str >]
| [<' `0`..`9` as c; (integer (int_of_digit c)) tok; spaces _>]
                       -> [<'tok; lexer str >]
| [< '(`a`..`z` | `A`..`Z`) as c; (set_nth_char ident_buf 0 c; ident 1) tok; spaces _ >]   
                       -> [< 'tok; lexer str >]
| [< '`;` >] -> [< 'SEMIC >]
| [< 't >] -> failwith ("Erreur lexicale : le caractere "^(make_string 1 t)^" est illegal.")
| [< >] -> failwith "Point-virgule attendu.";;

(* --- Parser -------*)

type
  pretype = Bool | Star | Int | Atom of atomictype
          | Arrow of pretype*pretype
          | Method of (atomictype*pretype) list
and
  atomictype == string;;

type
  expression = Var of string
             | Quest
             | Const of bool
             | Val of int
             | Succ
             | Pred
             | Eqz
             | Lambda of string*pretype*expression
             | Fix of string*pretype*expression
             | Ite of expression*expression*expression
             | App of expression*expression
             | Epsilon
             | Ampersend of expression*((atomictype*pretype) list)*expression
             | Coerce of atomictype*expression
             | Super of atomictype*expression
             | In of atomictype*expression
             | Out of atomictype*expression
and
  terme = Expression of expression
             | Subtyping of atomictype*(atomictype list)*terme
             | Declaration of atomictype*pretype*terme;;

(* Quelques sous-fonctions destinees a attraper les exceptions *)

let rec printToken n s = if n = 0 then "" else let char = (match s with                         
  [< 'LAMBDA >] -> "\\"
| [< 'COLON >] -> ":"
| [< 'DOT >] -> "."
| [< 'AMPERSEND >] -> "&"
| [< 'EPSILON >] -> "@"
| [< 'LPAR >] -> "("                        (* Imprime n tokens du stream s *)
| [< 'RPAR >] -> ") "
| [< 'IN >] -> "in "
| [< 'OUT >] -> "out "
| [< 'COERCE >] -> "coerce "
| [< 'SUPER >] -> "super "
| [< 'LET >] -> "let "
| [< 'EQUAL >] -> "= "
| [< 'FIX >] -> "fix "
| [< 'SMALLER >] -> "< "
| [< 'HIDE >] -> "hide "
| [< 'IDENT a >] -> a^" "
| [< 'ARROW >] -> "-> "
| [< 'LBRACK >] -> "{"
| [< 'RBRACK >] -> "} "
| [< 'COMMA >] -> ", "
| [< 'BOOL >] -> "bool "
| [< 'INT >] -> "int "
| [< 'SEMIC>] -> ";"
| [< 'STAR >] -> "* "
| [< 'QUEST >] -> "? "
| [< 'PRED >] -> "pred "
| [< 'SUCC >] -> "succ "
| [< 'EQZ >] -> "eqz "
| [< 'TRUE >] -> "true "
| [< 'FALSE >] -> "false "
| [< 'ITE >] -> "ite"
| [< >] -> "") in if char = "" then "" else char^(printToken (n-1) s);;

let aulieu s = " au lieu de '" ^ (printToken 8 s) ^ "...'.";;

(* Verifie la presence d'un IDENT dans s *)
let ifIDENT s = match s with                               
  [< 'IDENT A >] -> A
| [< >] -> failwith ("Identificateur attendu"^(aulieu s));;

(* Verifie la presence du token t *)
let ifToken t s =                                                                                                
  let error debut t =
       failwith ((match t with 
                   IN -> "in"
                 | LBRACK -> "{"
                 | LBR -> "["
                 | COLON -> ":"
                 | SEMIC -> ";"
                 | EQUAL -> "="
                 | DOT -> "."
                 | COMMA -> ","
                 | RPAR -> ")"
                 | ARROW -> "->"
                 | RBRACK -> "}"
                 | RBR -> "]"
                 | _ -> failwith "Impossible!")^" attendu"^(aulieu [< debut; s >]))
  in match s with
        [< 'u >] -> if u = t then () else error [< 'u >] t
      | [< >] -> error [< >] t;;


(* La fonction parsePretype reconnait un pretype. Plusieurs cas sont a traiter :
     - si on trouve une liste de la forme {t1, ..., tn} on la passe a parseListeTypes qui se charge
       d'appeler parsePretype pour chacun des types t1... tn et forme une liste des les pretypes retournes.
     - si on trouve un bool ou un identificateur, on enregistre un bool ou un atomictype
     - en cas de parentheses, on realise un appel recursif
     - une fois reconnu un pretype, la sous-fonction rest regarde s'il est suivi d'une fleche et d'un autre
       pretype. Si oui, on cree on cree un "Arrow". On realise ainsi un parenthesage implicite a droite :
       a -> b -> c devient a -> (b -> c)                              *)

        
exception InvalidPretype;;
             
let rec parseListeTypes s = match s with
  [< 'IDENT nom; (ifToken ARROW) _; parsePretype t; parseListeTypes l  >]
        -> (nom, t)::l
| [< 'COMMA; ifIDENT nom; (ifToken ARROW) _; parsePretype t; parseListeTypes l >]
        -> (nom, t)::l
| [< '(STAR | BOOL | INT) ;(ifToken ARROW) _; parsePretype t; parseListeTypes l >]
        -> failwith "Le dispatching n'est pas permis sur les types predefinis"
| [< >] -> []
and
rest t1 = function
  [< 'ARROW; parsePretype t2 >] -> Arrow (t1, t2)
| [< >] -> t1
and
parsePretype s = match s with
  [< 'LBRACK; parseListeTypes l; (ifToken RBRACK) _; (rest (Method l)) t >] -> t
| [< 'STAR; (rest Star) t >] -> t
| [< 'BOOL; (rest Bool) t >] -> t
| [< 'INT; (rest Int) t >] -> t
| [< 'IDENT atomtyp; (rest (Atom atomtyp)) t >] -> t
| [< 'LPAR; parsePretype t; (ifToken RPAR) _; (rest t) u >] -> u
| [< >] -> raise InvalidPretype;;

(* Les fonctions find* rattrapent les exceptions generees par les fonctions ci-dessus *)

let findListeTypes s = try parseListeTypes s
                       with InvalidPretype -> failwith ("Pretype attendu"^(aulieu s));;

let findpretype s = try parsePretype s
                    with InvalidPretype -> failwith ("Pretype attendu"^(aulieu s));;

(* Suit le parser pour les expressions. Il comprend plusieurs sous-fonctions :
   - calcProgram est charge d'evaluer un terme. Si il trouve "let A ...", il distingue (grace a la
     sous-fonction suite) les constructions "let A hide ..." et "let A < A1, ... An in ...". Si le
     terme ne commence pas par "let", il s'agit d'une expression.
   - calcSmallExpression evalue une expression simple (i.e. qui soit d'un seul morceau, donc n'etant
     pas formee d'une application ou d'un ampersend. La fonction rest relie les expressions calculees
     par calcSmallExpression pour former les applications et les ampersends. Elle realise un parenthesage
     implicite a gauche : "f x y" est interprete comme "(f x) y".      
       E   ->   F R'                      Expression
       R'  ->   &{ } F R' | emptyword     rest
       F   ->   S R''                     Factor
       R''  ->   S R'' | emptyword        restTwo
       S   ->   (E) | \x:T.F | ....       SmallExpression 
*)
      
let isempty s = try (end_of_stream s); true with Parse_failure -> false;;

(* Analyse une clause "let a < b, c, ... " *)
let renvoieListeAtomes s =                                 
  let rec itere = function
    [< 'IDENT nom; itere l >] -> (nom::l)
  | [< 'COMMA; ifIDENT nom; itere l >] -> (nom::l)
  | [< >] -> []
in let l = itere s
in if l = [] then failwith ("Type atomique attendu"^(aulieu s)) else l;;

let rec parseProgram s = 
  let suite A = function
    [< 'SMALLER; renvoieListeAtomes l; (ifToken IN) _; parseProgram p >] -> Subtyping (A, l, p)
  | [< 'HIDE; findpretype T; (ifToken IN) _; parseProgram p >] -> Declaration (A, T, p)
  | [< >] -> failwith ("'<' ou 'HIDE' attendu"^(aulieu s))
in match s with
  [< 'LET; ifIDENT A; (suite A) s >] -> s
| [< parseExpression M; (ifToken SEMIC) _ >] -> Expression M

and parseExpression s =
  let rec rest e1 s = match s with
    [< 'AMPERSEND; (ifToken LBRACK) _; findListeTypes l;
        (ifToken RBRACK) _; parseFactor e2; (rest (Ampersend (e1, l, e2))) u >] -> u
  | [< >] ->  e1
  in match s with
    [< 'LBR; ifIDENT x; (ifToken COLON) _; findpretype T; (ifToken EQUAL) _; parseExpression M
          ; (ifToken RBR) _; parseExpression N >] -> App(Lambda(x, T, N), M)
  | [< parseFactor e0; (rest e0) u >] -> u
  | [< >] -> failwith ("Expression attendue"^(aulieu s))

and parseFactor s =
  let rec restTwo  e1 s = match s with
    [< parseSmallExpression e2; (restTwo (App(e1, e2))) u >] -> u
  | [< >] ->  e1
  in match s with [< parseSmallExpression e0; (restTwo e0) u >] -> u
                        | [< >] -> failwith ("Expression attendue"^(aulieu s))

and parseSmallExpression s = match s with
  [< 'QUEST >] -> Quest
| [< 'TRUE >] -> Const true
| [< 'FALSE >] -> Const false
| [< 'SUCC >] -> Succ
| [< 'PRED >] -> Pred
| [< 'EQZ >] -> Eqz
| [< 'VAL n >] -> Val n
| [< 'IDENT x >] -> Var x
| [< 'LAMBDA; ifIDENT x; (ifToken COLON) _; findpretype T; (ifToken DOT) _; parseFactor M >]
              -> Lambda (x, T, M)
| [< 'FIX; ifIDENT x; (ifToken COLON) _; findpretype T; (ifToken DOT) _; parseExpression M >]
              -> Fix (x, T, M)
| [< 'ITE; (ifToken LPAR) _; parseExpression e1; (ifToken COMMA) _; parseExpression e2
                ; (ifToken COMMA) _; parseExpression e3; (ifToken RPAR) _ >] -> Ite(e1,e2,e3)
| [< 'EPSILON >] -> Epsilon
| [< 'COERCE; (ifToken LBR) _; ifIDENT A; (ifToken RBR) _;
                (ifToken LPAR) _; parseExpression M  ; (ifToken RPAR) _ >] -> Coerce (A, M)
| [< 'SUPER; (ifToken LBR) _; ifIDENT A;  (ifToken RBR) _;
                (ifToken LPAR) _; parseExpression M ; (ifToken RPAR) _ >] -> Super (A, M)
| [< 'IN; (ifToken LBR) _; ifIDENT A; (ifToken RBR) _;
                (ifToken LPAR) _; parseExpression M  ; (ifToken RPAR) _ >] -> In (A, M)
| [< 'OUT; (ifToken LBR) _; ifIDENT A; (ifToken RBR) _;
                (ifToken LPAR) _; parseExpression M  ; (ifToken RPAR) _ >] -> Out (A, M)
| [< 'LPAR; parseExpression M; (ifToken RPAR) _ >] -> M
| [< '(COLON | DOT | LET | SMALLER | HIDE | ARROW |
       LBRACK | RBRACK | BOOL | EQUAL | STAR) as bidule >]
         -> failwith ("'" ^ (printToken 8 [< 'bidule; s >]) ^ "...' n'est pas une expression!");;




(* --- Pretty-printer ------------------------------- *)

(* La fonction imprime renvoie une chaine representant un pretype *)

let rec imprime = function
  Bool -> "bool"
| Star -> "*"
| Int -> "int"
| Atom a -> a
| Arrow (t, u) -> "("^(imprime t)^" -> "^(imprime u)^")"
| Method l -> "{"^(imprimeListe l)^"}"
and imprimeListe = function
  (a, t)::l -> (imprime (Arrow(Atom a, t)))^(if l = [] then "" else ", "^(imprimeListe l))
| [] -> "";;
 
let rec exprToString = function 
    Var x -> x 
  | Val n -> (string_of_int n) 
  | Const t -> if t then "true" else "false"
  | Eqz -> "eqz"
  | Pred -> "pred"
  | Succ -> "succ"
  | Quest -> "?"
  | Fix (s, t, e) -> "fix "^s^":"^(imprime t)^"."^(exprToString e)
  | Lambda (s, t, e) -> "\\"^s^":"^(imprime t)^"."^(exprToString e)
  | App (e, f) -> "("^(exprToString e)^") "^(exprToString f)
  | Epsilon -> "@"
  | Ampersend (e, l, f) -> "("^(exprToString e)^" &{"^(imprimeListe l)^"} "^(exprToString f)^")"
  | Coerce (A, e) -> "coerce["^A^"]("^(exprToString e)^")"
  | Super (A, e) -> "super["^A^"]("^(exprToString e)^")"
  | In (A, e) -> "in["^A^"]("^(exprToString e)^")"
  | Out (A, e) -> "out["^A^"]("^(exprToString e)^")"
  | Ite (e1,e2,e3) -> "ite("^(exprToString e1)^","^(exprToString e2)^","^(exprToString e3)^")";;

let prettyprint s = print_string ((exprToString s)^"\n");;


(* --- Evaluateur ---------------- *)


(* Renvoie la classe d'un objet afin de pouvoir appliquer une fonction surchargee *)

let getTag = function   
  In (a, _) -> a
| Coerce (a, _) -> a
| Super (a, _) -> a
| _ -> failwith "Ceci n'est pas un objet.";;

(* La fonction smaller compare deux types atomiques. Elle tire ses renseignements de la structure hier
  (hierarchie), qui est de type (atomictype*(atomictype list)) list : a chaque type atomique elle associe
  la liste de ceux qui sont plus grands que lui.*)

let smaller hier A B = (A = B) or (mem B (try assoc A hier with Not_found -> []));;

(* La fonction findMin extrait d'une liste de types atomiques le type le moins general qui soit plus
   general que D. En fait ici liste est une (atomictype*pretype) list, mais on oublie le pretype qui ne
   nous sert a rien. La fonction findGreater ne conserve dans la liste que les types plus generaux que D.
   La fonction search en extrait le minimum. Une exception est produite si celui-ci n'existe pas.  *)

let rec findMin hier liste D =
  let rec findGreater = function
    A::l -> (if (smaller hier D A) then [A] else [])@(findGreater l)
  | [] -> []
  and search curMin = function
    A::l -> if (smaller hier A curMin) then search A l
                else search curMin l
  | [] -> curMin
in
  match findGreater (map (fun (a, t) -> a) liste) with
    A::l -> search A l
  | [] -> failwith ("Cette methode ne peut s'appliquer au type "^D^".");;
  
(* Suivent quelques fonctions auxiliaires ... *)


(* Renvoie le dernier element d'une liste *)
let dernier l = match (rev l) with a::l -> a | [] -> failwith "Liste vide!";;         


(* Equivalent de la fonction mem de caml : prend une liste de couples et indique si
  A apparait en tant que premier element de l'un de ces couples *)
let rec customMem A = function               
  B::l -> if (fst B = A) then true else (customMem A l)           
| [] -> false;;

(* Prend une liste de types et verifie que chacun de ces types apparait dans decl *)
let rec megaMem decl = function             
  A::l -> (customMem A decl) & (megaMem decl l)
| [] -> true;;

(* La fonction moinsGeneral compare deux pretypes *)
let rec existe hier decl fleche = function
  (a, t)::l -> (moinsGeneral hier decl (Arrow(Atom a, t), fleche)) or (existe hier decl fleche l)
| [] -> false
and moinsGeneral hier decl = function
  (Bool, Bool) -> true
| (Star, Star) -> true
| (Int, Int) -> true
| (Atom a, Atom b) -> smaller hier a b
| (Arrow(t1, t2), Arrow(u1, u2))
    -> (moinsGeneral hier decl (t2, u2)) & (moinsGeneral hier decl (u1, t1))
| (Method l, Method m)
    -> it_list (fun x y -> x & y) true (map (fun (a, t) -> existe hier decl (Arrow(Atom a, t)) l) m)
| _ -> false;;


(* typexpression renvoie le type d'une expression. Genere une erreur en cas d'incompatibilites *)


let rec wellformed hier decl = 
    let  atomictypes = (map (fun(a, t) -> a) decl)     (*ensemble des types atomiques*)
in function
  Bool -> true
| Star -> true
| Int -> true
| Atom a -> true
| Arrow(t1,t2) -> (wellformed hier decl t1) & (wellformed hier decl t2)
| Method l -> let domain_de_l = (map (fun(a,t) -> a) l)
               in (covariance l) & (multinheritance domain_de_l domain_de_l)

(* il controle la condition de covariance *)
where rec covariance = function                            
 (a,t):: l1 -> (check a t l1) & (covariance l1)
| []  -> true

and check a t = function
  (b,s)::l2 -> (if (smaller hier a b) then moinsGeneral hier decl (t,s)
                else if (smaller hier b a) then moinsGeneral hier decl (s,t)
                else true) & (check a t l2)
| [] -> true


(* il controle tout couple du domain *)                  

and multinheritance domain = function                    
  a::l -> (apply domain a l) & (multinheritance domain l)
| [] -> true


(* il controle tout couple (a, reste_du_domain) *)  

and apply domain a = function                             
  b::l -> let LBab = lowerbounds a b atomictypes
           in ((list_length LBab)=0 or (contains domain (maximalElements LBab)))
               & (apply domain a l)
| [] -> true

and lowerbounds a b = function
  c::l -> (if (smaller hier c a) & (smaller hier c b) then [c] else [])@(lowerbounds a b l)
| [] -> []


(* il donne la liste des elements maximaux *)

and maximalElements liste =                               
    let rec isMaximal a = function
         b::l -> ((b=a) or not(smaller hier a b)) & (isMaximal a l)
       | [] -> true
    and explore l1 = function
         a::l2 -> (if (isMaximal a l1) then [a] else [])@(explore l1 l2)
       | [] -> []
    in explore liste liste


(* il dit si la liste l1 contient la liste l2 *)

and contains l1 = function               
 a::l2 -> (if (mem a l1) then true else false) & (contains l1 l2)
| [] -> true ;;
          

let rec typexpression hier decl env = function
  Val n -> Int
| Const x -> Bool
| Quest -> Star
| Epsilon -> Method []
| Eqz -> Arrow(Int, Bool)
| Pred -> Arrow(Int, Int)
| Succ -> Arrow(Int, Int)
| Var x -> (try assoc x env with Not_found 
              -> failwith ("[type-checker] Pretype absent de l'environnement: variable \""
                           ^(x)^"\" non liee"))
| Fix (s, t, f )
       -> if wellformed hier decl t then
             (if moinsGeneral hier decl ((typexpression hier decl ((s, t)::env) f), t) then t
              else failwith ("[type-checker] Le type "^(imprime t)^
                             " de la variable de recursion n'est pas "^
                             " compatible avec la definition"))
          else (failwith ("[type-checker] Le pretype "^(imprime t)^
                          " n'est pas bien forme")) 
| Lambda (s, t, f ) -> if wellformed hier decl t then Arrow(t, typexpression hier decl ((s, t)::env) f) 
                       else (failwith ("[type-checker] Le pretype "^(imprime t)^
                                       " n'est pas bien forme")) 
| App (f, g) -> let v = typexpression hier decl env g
  in (match (typexpression hier decl env f) with
       Arrow(t, u) -> if moinsGeneral hier decl (v, t) then u
                      else failwith ("[type-checker] Impossible d'appliquer "^
                                     (imprime t)^" -> "^(imprime u)^" a "^
                                     (imprime v)^" dans "^
                                     (exprToString(App (f, g))))
     | Method l -> (match v with    
                      Atom A -> assoc (findMin hier l A) l
                    | _ -> failwith ("[type-checker] Methode appliquee au pretype "
                                     ^(imprime v)^"!"))
     | _ as t -> failwith ("[type-checker] Le type "^(imprime t)^
                           " est utilise comme type fonctionnel!"))
| Ampersend (f, l, g)
     -> if wellformed hier decl (Method l)  then
           (match (rev l) with
               (a,t)::l' ->
                     if 
                       (moinsGeneral hier decl (typexpression hier decl env f , Method l')) &
                       (moinsGeneral hier decl (typexpression hier decl env g , Arrow(Atom a, t)))
                     then Method l
                     else failwith("[type-checker] Index incompatible: ...&"
                                          ^(imprime(Method l)))
              | []      -> failwith "[type-checker] Index vide?!?!")
        else failwith ("[type-checker] Le pretype "^(imprime (Method l))^
                       " n'est pas bien forme")
| Coerce (a, f) -> let b = typexpression hier decl env f in 
                      if moinsGeneral hier decl (b , Atom a) then (Atom a) 
                      else failwith ("[type-checker] Coercion impossible:"^(imprime (Atom a))^
                                     " n'est pas plus grand que "^(imprime b))
| Super (a, f) -> let b = typexpression hier decl env f in 
                      if moinsGeneral hier decl (b , Atom a) then (Atom a) 
                      else failwith ("[type-checker] Super impossible:"^(imprime (Atom a))^
                                     " n'est pas plus grand que "^(imprime b))
| In (a, f) -> let t = typexpression hier decl env f in 
               let b = (try assoc a decl with Not_found
                               -> failwith ("[type-checker] Le type objet "
                                            ^a^" n'est pas defini!"))
                in if moinsGeneral hier decl (t, b) 
                   then Atom a
                   else failwith ("[type-checker] `in` impossible: le type representaton de "^
                                  (imprime (Atom a))^" n'est pas plus grand que "^(imprime t))
 | Out (a, f) -> let b = typexpression hier decl env f in 
                       if moinsGeneral hier decl (b , Atom a) 
                       then (try assoc a decl with Not_found
                                 -> failwith ("[type-checker] Le type objet "
                                              ^a^" n'est pas defini!"))
                       else failwith ("[type-checker] Out impossible:"^(imprime (Atom a))^
                                      " n'est pas plus grand que "^(imprime b))
| Ite (e1,e2,e3) -> if  (typexpression hier decl env e1) = Bool then
                      let t2 =  (typexpression hier decl env e2)
                      and t3 =  (typexpression hier decl env e3) in
                          if moinsGeneral hier decl (t2, t3) then t3 else
                          if moinsGeneral hier decl (t3, t2) then t2 else
                          failwith("[type-checker] Types incompatibles "^
                                   "dans ite dans l'expression "
                                   ^(exprToString(Ite (e1,e2,e3))))
                      else failwith("[type-checker] le premier argument "^
                                     "de ite n'est pas bool dans l'expression "
                                     ^(exprToString (Ite(e1,e2,e3))));;

(* Mise a jour de la hierarchie des types lors d'une declaration "let A < A1, ... An". Il faut non seulement
   noter que A < A1 ... An  mais aussi en deduire les nouvelles relations qui en decoulent par transitivite.
   Deux types de cas se presentent :
   - si on declare a < b alors qu'on avait deja b < c, on doit noter a < c. C'est ce dont se charge updateDown
   - si on declare b < c alors qu'on avait deja a < b, on doit noter a < c. C'est ce dont se charge updateUp.
   La fonction updateHier, apres avoir verifie l'existence des types specifies, met a jour la hierarchie des
   types en appelant ces  deux sous-fonctions.*)

let updateDown hier A B =
  let greaterthanB = try assoc B hier with Not_found -> []
  in if customMem A hier
      then map (fun ((x, m) as elem) -> if x = A then (x, B::greaterthanB@m) else elem) hier
      else (A, B::greaterthanB)::hier;;

let rec updateUp A l = function
  (x, listex)::suite -> (x, listex@(if mem A listex then l else []))::(updateUp A l suite)
| [] -> [];;

let updateHier decl hier A l =
 if not (customMem A hier) then                  (* ici on controle si A a deja ete' declare' comme soustype *)
  if (customMem A decl) & (megaMem decl l) then   (* ici on controle si tous les types ont ete declares *)
    if it_list (fun x y -> x & y) true
           (* controle des types representation *)
           (map (fun B -> moinsGeneral hier decl (assoc A decl, assoc B decl)) l)  
    then  
        let rec parcoursl h = function 
          B::l -> parcoursl (updateDown h A B) l
          | [] -> h
        in updateUp A l (parcoursl hier l)
    else failwith "Sous-typage incompatible avec l'ordre sur les pretypes."     
  else failwith ("Type objet non declare:  let "^A^"  < ...")
else failwith("Sous-typage pour "^A^" deja declare");;

(*pour faire marcher seulment le type-checker*)

let rec typeterme hier decl = function
  Expression e -> typexpression hier decl [] e
| Declaration (atomtyp, pretyp, term)
        -> if customMem atomtyp decl
              then failwith ("Le type "^atomtyp^" est deja declare")
              else typeterme hier ((atomtyp, pretyp)::decl) term
| Subtyping (atomtyp, l, term) -> typeterme (updateHier decl hier atomtyp l) decl term;;

(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
(*                                     EVALUATEUR                                           *)
(*__________________________________________________________________________________________*)

(* L'evaluateur proprement dit. Il se compose de deux sous-fonction recursives : evalterme et evalexpr,
   chargees d'evaluer respectivement termes et expressions. Elles prennent deux parametres : la hierarchie
   des types atomiques (de type (atomictype*(atomictype list)) list), et la liste des declarations de types
   atomiques (atomictype*pretype list).      *)



let eval = evalterme [] []

where rec evalterme hier decl = function
  Expression e -> (evalexpr hier decl e)
| Declaration (atomtyp, pretyp, term)
        -> if customMem atomtyp decl then failwith ("Le type "^atomtyp^" est deja declare")
           else evalterme hier ((atomtyp, pretyp)::decl) term
| Subtyping (atomtyp, l, term) -> evalterme (updateHier decl hier atomtyp l) decl term



(* pour effecter le type-checking nous on fait preceder l'interpretation de une expression par
                (typexpression hier decl [] M) 
   de facon que si le terme n'est pas bien type' la fonction typexpression souleve une failure  *)
   
and evalexpr hier decl M = 
(match M with
  Epsilon -> Epsilon
| Var x -> failwith ("La variable "^x^" n'est pas definie.")
| Val n -> Val n
| Succ -> Succ
| Pred -> Pred
| Eqz -> Eqz
| Quest -> Quest
| Const x -> Const x
| Ite (e1, e2, e3) -> let b = (evalexpr hier decl e1) in (match b with
                    Const true   -> (evalexpr hier decl e2)
                  | Const false  -> (evalexpr hier decl e3)
                  | _ -> failwith "Type checker bug??")
| Lambda x -> Lambda x
| Fix(x, t, f) ->  evalexpr hier decl (remplace x (Fix(x, t, f)) f)
| Ampersend x -> Ampersend x
| Coerce (a, x) -> let x1 = (evalexpr hier decl x) in  Coerce (a, x1)
| Super (a, x) -> let x1 = (evalexpr hier decl x) in  Super (a, x1)
| In (a, x) -> In (a , x)
| Out (A, e) -> let e1 = evalexpr hier decl e
                 in (match e1 with
                    In (_, expr) -> (evalexpr hier decl expr)
                  | Coerce (_, expr) -> (evalexpr hier decl (Out (A, expr)))
                  | _ -> failwith ("J'attandais un tagged value et j'ai trouve' "
                                    ^(exprToString e1)))
| App (e, f) -> let e1 = evalexpr hier decl e
                      and f1 = evalexpr hier decl f
                      in (match e1 with
          Eqz -> (match f1 with
                   Val 0 -> Const true
                 | Val n -> Const false
                 | _  -> failwith "eqz: Type checker bug??")
        | Pred -> (match f1 with
                   Val 0 -> Val 0
                 | Val n -> Val (n-1)
                 | _  -> failwith " pred: Type checker bug??")
        | Succ -> (match f1 with
                   Val n -> Val (n+1)
                 | _ as y -> failwith "succ: Type checker bug??")
        | Lambda (x, t, M) -> evalexpr hier decl (remplace x f1 M)
        | Ampersend (M1, l, M2)
              -> let D' = findMin hier l (getTag f1)
                 and Dn = fst (dernier l)
                  in (match f1 with
                        Super (a, N) -> evalexpr hier decl
                                           (if D' = Dn then App(M2, N) else App(M1, f1))
                      | _ -> evalexpr hier decl (App ((if D' = Dn then M2 else M1), f1)))
        | _ -> failwith "Valeur non fonctionnelle utilisee comme fonction!"))

(* La fonction remplace prend en argument une expression et y remplace toutes les occurences de
   la variable x par l'expression e *)
  
and remplace x e = function
  Var y -> if y = x then e else Var y
| Lambda (s, t, f) -> Lambda (s, t, if s = x then f else (remplace x e f))
| Fix (s, t, f) -> Fix (s, t, if s = x then f else (remplace x e f))
| App (f, g) -> App (remplace x e f, remplace x e g)
| Ampersend (f, l, g) -> Ampersend (remplace x e f, l, remplace x e g)
| Coerce (a, f) -> Coerce (a, remplace x e f)
| Super (a, f) -> Super (a, remplace x e f)
| In (a, f) -> In (a, remplace x e f)
| Out (a, f) -> Out (a, remplace x e f)
| Ite (e1,e2,e3) -> Ite (remplace x e e1, remplace x e e2, remplace x e e3)
| _ as y -> y;;

(*--------pour evaluer a l'interieur des lambda et des In------------*)
let internaleval = evalterme [] []

where rec evalterme hier decl = function
  Expression e -> ((typexpression hier decl [] e);  internalevalexpr hier decl e)
| Declaration (atomtyp, pretyp, term)
        -> if customMem atomtyp decl then failwith ("Le type "^atomtyp^" est deja declare")
           else evalterme hier ((atomtyp, pretyp)::decl) term
| Subtyping (atomtyp, l, term) -> evalterme (updateHier decl hier atomtyp l) decl term


and  internalevalexpr hier decl = function
  Epsilon -> Epsilon
| Var x -> Var x
| Val n -> Val n
| Succ -> Succ
| Pred -> Pred
| Eqz -> Eqz
| Quest -> Quest
| Const x -> Const x
| Fix(x, t, f) -> remplace x (Fix(x, t, f)) f
| Lambda (x, t, M) -> Lambda (x , t, (internalevalexpr hier decl M))
| Ampersend x -> Ampersend x
| Coerce (a, x) -> let x1 = (internalevalexpr hier decl x) in  Coerce (a, x1)
| Super (a, x) -> let x1 = (internalevalexpr hier decl x) in  Super (a, x1)
| In (a, x) -> In (a , internalevalexpr hier decl x)
| Ite (e1, e2, e3)
      -> let b = (internalevalexpr hier decl e1)
          in (match b with
                Const true   -> (internalevalexpr hier decl e2)
              | Const false  -> (internalevalexpr hier decl e3)
              | _ -> Ite (b,(internalevalexpr hier decl e2),(internalevalexpr hier decl e2)))
| Out (A, e) -> let e1 = internalevalexpr hier decl e
                      in (match e1 with
                        In (_, expr) -> (internalevalexpr hier decl expr)
                      | Coerce (_, expr) -> (internalevalexpr hier decl (Out (A, expr)))
                      | _ -> Out (A,e1))
| App (e, f) -> let e1 = internalevalexpr hier decl e
                      and f1 = internalevalexpr hier decl f
                      in  (match e1 with
          Eqz -> (match f1 with
                   Val 0 -> Const true
                 | Val n -> Const false
                 | _  -> App (e1,f1))
        | Pred -> (match f1 with
                   Val 0 -> Val 0
                 | Val n -> Val (n-1)
                 | _  -> App (e1,f1))
        | Succ -> (match f1 with
                   Val n -> Val (n+1)
                 | _  -> App (e1,f1))
        | Lambda (x, t, M) -> internalevalexpr hier decl (remplace x f1 M)
        | Ampersend (M1, l, M2) ->
              let D' = findMin hier l (getTag f1)
              and Dn = fst (dernier l)
               in (match f1 with
                      Super (a, N) -> internalevalexpr hier decl
                                         (if D' = Dn then App(M2, N) else App(M1, f1))
                    | _ -> internalevalexpr hier decl (App ((if D' = Dn then M2 else M1), f1)))
        | _ -> App (e1,f1))
  
and union = function
  (l, []) -> l
| ([], l) -> l
| (x::l1, l) -> if (mem x l ) then union(l1,l) else union(l1,x::l)

and diff = function
  ([], x) -> []
| (y::l, x) -> if (x=y) then l else (y::(diff(l,x)))

and FV = function 
  Var x -> [x]
| Ite (e1, e2, e3) -> union(FV(e1), union(FV(e2),FV(e3)))
| Fix (x, t, e) -> diff(FV(e), x)
| Lambda (x, t, e) -> diff(FV(e), x)
| Ampersend (e1, l, e2)  ->  union(FV(e1),FV(e2))
| Coerce (a, e) -> FV(e)
| Super (a, e) -> FV(e)
| In (a, e) ->  FV(e)
| Out (A, e) -> FV(e)
| App (e1, e2) ->  union(FV(e1),FV(e2))
| _ -> []

and remplace x e = function
  Var y -> if y = x then e else Var y
| Fix (y, t, f) -> if  y = x then  Fix (y, t, f)
                      else if not(mem x (FV(f))) then Fix (y, t, remplace x e f)
                      else remplace x e (Fix(y^"a", t, remplace y (Var(y^"a")) f))
| Lambda (y, t, f) -> if  y = x then  Lambda (y, t, f)
                      else if not(mem x (FV(f))) then Lambda (y, t, remplace x e f)
                      else remplace x e (Lambda(y^"a", t, remplace y (Var(y^"a")) f))
| App (f, g) -> App (remplace x e f, remplace x e g)
| Ampersend (f, l, g) -> Ampersend (remplace x e f, l, remplace x e g)
| Coerce (a, f) -> Coerce (a, remplace x e f)
| Super (a, f) -> Super (a, remplace x e f)
| In (a, f) -> In (a, remplace x e f)
| Out (a, f) -> Out (a, remplace x e f)
| Ite (e1,e2,e3) -> Ite (remplace x e e1, remplace x e e2, remplace x e e3)
| _ as y -> y;;

(* Les fonctions exportees*)

let ParseString x = parseProgram (lexer(stream_of_string x));;

let ParseFile x =  (parseProgram(lexer (stream_of_string x)));;
                 
let CalcString x = try   let syntaxtree = (parseProgram(lexer (stream_of_string x))) 
                    in  print_string ("- : "^imprime(typeterme [] [] syntaxtree)^"\n");
                        prettyprint(eval (syntaxtree))
             with Failure s -> print_string ("Erreur : "^s^"\n");;

let TypeString x = try print_string (imprime(typeterme [] [] (parseProgram(lexer (stream_of_string x)))))
             with Failure s -> print_string ("Erreur : "^s^"\n");;


let TypeFile x = 
     try print_string (imprime(typeterme [] [] (parseProgram(lexer (stream_of_channel (open_in x))))))
     with Failure s -> print_string ("Erreur : "^s^"\n");;


let CalcFile x = try let syntaxtree = (parseProgram(lexer (stream_of_channel (open_in x)))) 
                      in  print_string ("- : "^imprime(typeterme [] [] syntaxtree)^"\n");
                          prettyprint(eval (syntaxtree))
                 with Failure s -> print_string ("Erreur : "^s^"\n");;

let InternalCalcString x = try let syntaxtree = (parseProgram(lexer (stream_of_string x))) 
                         in  print_string ("- : "^imprime(typeterme [] [] syntaxtree)^"\n");
                             prettyprint(internaleval (syntaxtree))
                     with Failure s -> print_string ("Erreur : "^s^"\n");;

let InternalCalcFile x = try  let syntaxtree = (parseProgram(lexer (stream_of_channel (open_in x)))) 
                               in  print_string ("- : "^imprime(typeterme [] [] syntaxtree)^"\n");
                                   prettyprint(internaleval (syntaxtree))
                         with Failure s -> print_string ("Erreur : "^s^"\n");;