(* Taken from http://www.pps.jussieu.fr/~cousinea/Nanjing/
   The top-down parser is built with Stream (http://caml.inria.fr/pub/docs/manual-ocaml/libref/Stream.html).
   Stream is turned into a separate camlp4 extension (http://brion.inria.fr/gallium/index.php/Camlp4).
   In the interactive mode, [ocaml camlp4o.cma camlincaml.ml]
      or, [ocaml] -> [#load "camlp4o.cma";;] -> [#use "camlincaml.ml";;] -> [Full_toplevel.toplevel_loop();;]
   In the compiling mode, [ocamlc -pp camlp4o camlincaml.ml]
   Note that camlp4 can do fancier jobs for extending languages.
   Here we only do the plain old top-down parsing.
*)

module type GENERIC_LEXER =
sig
type token =
   | Keyword of string
   | Ident of string
   | Integer of int

val build_lexer :
     string list -> (char Stream.t -> token Stream.t)

val string_of_token : token -> string
end

module Generic_Lexer : GENERIC_LEXER =
struct
type token =
   | Keyword of string
   | Ident of string
   | Integer of int;;

let string_of_token = function
  | Keyword s -> "Keyword " ^ s
  | Ident id -> "Ident " ^ id
  | Integer i -> "Integer " ^ string_of_int i;;

let rec read_integer accumulator = parser
  | [< ' ('0' .. '9' as c); flow >] ->
      read_integer (10 * accumulator + int_of_char c - 48) flow
  | [< >] ->
      accumulator;;

let buffer = String.make 10 '-';;

let rec read_word position = parser
   [< ' ('A' .. 'Z' | 'a' .. 'z' | '0' .. '9' | '_' | '\''
            as c); flow >] ->
      if position < String.length buffer then buffer.[position] <- c;
      read_word (position + 1) flow
  | [< >] ->
      String.sub buffer 0 (min position (String.length buffer));;

let rec read_symbol position = parser
  | [< ' ('!' | '$' | '%' | '&' | '*' | '+' | '-' | '.' | '/' | ':' | 
          ';' | '<' | '=' | '>' | '?' | '@' | '^' | '|' | '~' as c); flow >] ->
      if position < String.length buffer then buffer.[position] <- c;
      read_symbol (position + 1) flow
  | [< >] ->
      String.sub buffer 0 (min position (String.length buffer));;

let rec read_comment = parser
  | [< ''\n' >] -> ()
  | [< 'c; flow >] -> read_comment flow;;

let kw_or_ident keyword_table ident =
    try Hashtbl.find keyword_table ident
    with Not_found -> Ident(ident);;

let kw_or_error keyword_table character =
    let ident = String.make 1 character in
    try Hashtbl.find keyword_table ident
    with Not_found -> raise (Stream.Error ("Illegal character " ^ ident));;

let rec read_token table = parser
  | [< ' (' ' | '\n' | '\r' | '\t'); flow >] ->
      read_token table flow
  | [< ''#'; flow >] ->
      read_comment flow; read_token table flow
  | [< ' ('A' .. 'Z' | 'a' .. 'z'  as c); flow >] ->
      buffer.[0] <- c;
      kw_or_ident table (read_word 1 flow)
  | [< ' ('!' | '$' | '%' | '&' | '*' | '+' | '.' | '/' | ':' | ';' | 
          '<' | '=' | '>' | '?' | '@' | '^' | '|' | '~' as c); flow >] ->
      buffer.[0] <- c;
      kw_or_ident table (read_symbol 1 flow)
  | [< ' ('0' .. '9' as c); flow >] ->
      Integer(read_integer (int_of_char c - 48) flow)
  | [< ''-'; flow >] ->
      begin parser
      | [< ' ('0' .. '9' as c) >] ->
          Integer(- (read_integer (int_of_char c - 48) flow))
      | [< >] ->
          buffer.[0] <- '-';
          kw_or_ident table (read_symbol 1 flow)
      end flow
  | [< 'c >] ->
      kw_or_error table c;;

let rec analyser table flow =
    Stream.from
      (function n ->
        (parser
         | [< token = read_token table >] -> Some token
         | [< >] -> raise Stream.Failure) flow);;

let build_lexer keywords =
    let keyword_table = Hashtbl.create 17 in
    List.iter
      (function mot -> Hashtbl.add keyword_table mot (Keyword mot))
      keywords;
    analyser keyword_table;;
end

module type SYNTAX =
sig
type expression =
   | Variable of string
   | Function of (pattern * expression) list
   | Application of expression * expression
   | Let of definition * expression
   | Boolean of bool
   | Number of int
   | Pair of expression * expression
   | Nil
   | Cons of expression * expression

and pattern =
  | Variable_pattern of string
  | Boolean_pattern of bool
  | Number_pattern of int
  | Pair_pattern of pattern * pattern
  | Nil_pattern
  | Motif_cons of pattern * pattern

and definition =
  { recursive: bool;
    name: string;
    expr: expression };;

type sentence =
  | Expression of expression
  | Definition of definition;;

val read_sentence : char Stream.t -> sentence;;
end





module Syntax: SYNTAX =
struct
type expression =
   | Variable of string
   | Function of (pattern * expression) list
   | Application of expression * expression
   | Let of definition * expression
   | Boolean of bool
   | Number of int
   | Pair of expression * expression
   | Nil
   | Cons of expression * expression

and pattern =
  | Variable_pattern of string
  | Boolean_pattern of bool
  | Number_pattern of int
  | Pair_pattern of pattern * pattern
  | Nil_pattern
  | Motif_cons of pattern * pattern

and definition =
  { recursive: bool;
    name: string;
    expr: expression };;

type sentence =
  | Expression of expression
  | Definition of definition;;

open Generic_Lexer;;

let is_an_operator operators op = List.mem op operators;;
  
let read_operator operators = parser
  | [< 'Keyword op when is_an_operator operators op >] -> op;;

let read_operation read_base operators =
  let rec read_rest e1 = parser
  | [< op = read_operator operators;
       e2 = read_base;
       e = read_rest (Application(Variable op, Pair(e1, e2))) >] -> e
  | [< >] -> e1 in
  parser [< e1 = read_base; e = read_rest e1 >] -> e;;

let read_infix read_base infixe build_syntax flow =
  let rec read_beginning = parser
    [< e1 = read_base; e2 = read_rest e1 >] -> e2
  and read_rest e1 = parser
  | [< 'Keyword op when op = infixe; e2 = read_beginning>] ->
      build_syntax e1 e2
  | [< >] -> e1 in
  read_beginning flow;;

let rec sentence = parser
  | [< d = definition; p = definition_end d; 'Keyword ";;" >] -> p
  | [< e = expression; 'Keyword ";;" >] -> Expression e
and definition_end d = parser
  | [< 'Keyword "in"; e = expression >] -> Expression (Let(d, e))
  | [< >] -> Definition d

and expression = parser
  | [< d = definition; 'Keyword "in"; e = expression >] -> Let(d, e)
  | [< 'Keyword "function"; liste = case_list >] ->
      Function(liste)
  | [< 'Keyword "match"; e = expression; 'Keyword "with";
       liste = case_list >] ->
      Application(Function(liste), e)
  | [< e = expr5 >] -> e

and expr_simple = parser
  | [< 'Integer i >] -> Number i
  | [< 'Keyword "true" >] -> Boolean true
  | [< 'Keyword "false" >] -> Boolean false
  | [< 'Ident id >] -> Variable id
  | [< 'Keyword "["; 'Keyword "]" >] -> Nil
  | [< 'Keyword "("; e = expression; 'Keyword ")" >] -> e

and expr0 = parser
  | [< es = expr_simple; e = application_sequence es >] -> e

and application_sequence f = parser
  | [< arg = expr_simple;
       e = application_sequence (Application(f, arg)) >] -> e
  | [<>] -> f

and expr1 flow =
  read_operation expr0 ["*"; "/"] flow

and expr2 flow =
  read_operation expr1 ["+"; "-"] flow

and expr3 flow =
  read_operation expr2 ["="; "<>"; "<"; ">"; "<="; ">="] flow

and expr4 flow =
  read_infix expr3 "::" (fun e1 e2 -> Cons(e1, e2)) flow

and expr5 flow =
  read_infix expr4 "," (fun e1 e2 -> Pair(e1, e2)) flow

and definition = parser
  | [< 'Keyword "let"; r = recursive; 'Ident name; 'Keyword "="; e = expression >] ->
      {recursive = r; name = name; expr = e}
and recursive = parser
  | [< 'Keyword "rec" >] -> true
  | [< >] -> false

and case_list = parser
  | [< m = pattern; 'Keyword "->"; e = expression; reste = other_cases >] ->
      (m, e) :: reste

and other_cases = parser
  | [< 'Keyword "|"; m = pattern; 'Keyword "->"; e = expression;
       reste = other_cases >] -> (m, e) :: reste
  | [< >] -> []

and pattern_simple = parser
  | [< 'Ident id >] -> Variable_pattern id
  | [< 'Integer n >] -> Number_pattern n
  | [< 'Keyword "true" >] -> Boolean_pattern true
  | [< 'Keyword "false" >] -> Boolean_pattern false
  | [< 'Keyword "["; 'Keyword "]" >] -> Nil_pattern
  | [< 'Keyword "("; m = pattern; 'Keyword ")" >] -> m

and pattern1 flow =
  read_infix pattern_simple "::" (fun m1 m2 -> Motif_cons(m1, m2)) flow

and pattern flow =
  read_infix pattern1 "," (fun m1 m2 -> Pair_pattern(m1, m2)) flow;;

let 
lexical_analyser = build_lexer
   ["function"; "let"; "rec"; "in"; "match"; "with"; "->"; ";;";
    "true"; "false"; "["; "]"; "("; ")"; "::"; "|"; ",";
    "*"; "/"; "-"; "+"; "="; "<>"; "<"; ">"; "<="; ">="; "::"];;

let read_sentence f = sentence (lexical_analyser f);;
end;;


module type EVAL =
sig
open Syntax;;

type value =
   | Number_value of int
   | Boolean_value of bool
   | Pair_value of value * value
   | Nil_value
   | Cons_value of value * value
   | Closure_value of closure
   | Primitive_value of (value -> value)

and closure =
  { definition : (pattern * expression) list;
    mutable environnment : environnment }

and environnment = (string * value) list;;

val eval: environnment -> expression -> value;;
val eval_definition: environnment -> definition -> environnment;;
val print_value: value -> unit;;

exception Error of string;;
end



module Eval : EVAL =
struct
open Syntax;;

type value =
   | Number_value of int
   | Boolean_value of bool
   | Pair_value of value * value
   | Nil_value
   | Cons_value of value * value
   | Closure_value of closure
   | Primitive_value of (value -> value)

and closure =
  { definition : (pattern * expression) list;
    mutable environnment : environnment }

and environnment = (string * value) list;;

exception Error of string;;

exception Patern_matching_failure;;

let rec pattern_matching value pattern =
  match (value, pattern) with
  | (v, Variable_pattern id) -> [id, v]
  | (Boolean_value b1, Boolean_pattern b2) ->
      if b1 = b2 then [] else raise Patern_matching_failure
  | (Number_value i1, Number_pattern i2) ->
      if i1 = i2 then [] else raise Patern_matching_failure
  | (Pair_value(v1, v2), Pair_pattern(m1, m2)) ->
      pattern_matching v1 m1 @ pattern_matching v2 m2
  | (Nil_value, Nil_pattern) -> []
  | (Cons_value(v1, v2), Motif_cons(m1, m2)) ->
      pattern_matching v1 m1 @ pattern_matching v2 m2
  | (_, _) -> raise Patern_matching_failure;;

let rec eval env expr =
  match expr with
  | Variable id ->
      begin try
        List.assoc id env
      with Not_found -> raise(Error(id ^ " est inconnu"))
      end
  | Function(case_list) ->
      Closure_value {definition = case_list; environnment = env}
  | Application(func, argument) ->
      let val_func = eval env func in
      let val_argument = eval env argument in
      begin match val_func with
      | Primitive_value func_primitive ->
          func_primitive val_argument
      | Closure_value closure ->
          eval_application closure.environnment
                             closure.definition val_argument
      | _ ->
          raise(Error "application d'une value non funcnelle")
      end
  | Let(definition, body) ->
      eval (eval_definition env definition) body
  | Boolean b -> Boolean_value b
  | Number n -> Number_value n
  | Pair(e1, e2) -> Pair_value(eval env e1, eval env e2)
  | Nil -> Nil_value
  | Cons(e1, e2) -> Cons_value(eval env e1, eval env e2)

and eval_application env case_list argument =
  match case_list with
  | [] -> raise(Error "échec du pattern_matching")
  | (pattern, expr) :: other_cases ->
      try
        let exstended_end = pattern_matching argument pattern @ env in
        eval exstended_end expr
      with Patern_matching_failure ->
        eval_application env other_cases argument

and eval_definition current_env def =
  match def.recursive with
  | false -> (def.name, eval current_env def.expr) :: current_env
  | true ->
      match def.expr with
      | Function case_list ->
          let closure =
            { definition = case_list; environnment = [] } in
          let exstended_end =
            (def.name, Closure_value closure) :: current_env in
          closure.environnment <- exstended_end;
          exstended_end
      | _ -> raise(Error "non functional let rec");;

let rec print_value = function
  | Number_value n -> print_int n
  | Boolean_value false -> print_string "false"
  | Boolean_value true -> print_string "true"
  | Pair_value (v1, v2) ->
      print_string "("; print_value v1;
      print_string ", "; print_value v2;
      print_string ")"
  | Nil_value ->
      print_string "[]"
  | Cons_value (v1, v2) ->
      print_value v1;
      print_string "::"; print_value v2
  | Closure_value _ | Primitive_value _ ->
      print_string "<fun>";;
end


module type TYPES =
sig
type simple_type and type_scheme;;

val int_type : simple_type;;
val bool_type : simple_type;;
val arrow_type : simple_type -> simple_type -> simple_type;;
val product_type : simple_type -> simple_type -> simple_type;;
val list_type : simple_type -> simple_type;;

val new_unknown : unit -> simple_type;;
val unify : simple_type -> simple_type -> unit;;
val generalization : simple_type -> type_scheme;;
val instanciation : type_scheme -> simple_type;;
val trivial_scheme : simple_type -> type_scheme;;
val definition_beginning : unit -> unit;;
val definition_end : unit -> unit;;

exception Conflict of simple_type * simple_type;;
exception Circularity of simple_type * simple_type;;

val print_type : simple_type -> unit;;
val print_scheme : type_scheme -> unit;;
end

module Types : TYPES =
struct
type simple_type =
   | Variable of type_variable
   | Term of string * simple_type array

and type_variable =
  { mutable level: int;
    mutable value: variable_value }

and variable_value =
  | Unknown
  | Known of simple_type;;

type type_scheme =
  { parameters: type_variable list;
    body: simple_type };;

exception Conflict of simple_type * simple_type;;
exception Circularity of simple_type * simple_type;;

let int_type = Term("int", [||])
and bool_type = Term("bool", [||])
and arrow_type t1 t2 = Term("->", [|t1; t2|])
and product_type t1 t2 = Term("*", [|t1; t2|])
and list_type t = Term("list", [|t|]);;

let rec value_of = function
  | Variable({value = Known ty1} as var) ->
      let value_of_ty1 = value_of ty1 in
      var.value <- Known value_of_ty1;
      value_of_ty1
  | ty -> ty;;

let occurrence_test var ty =
  let rec test t =
    match value_of t with
    | Variable var' ->
        if var == var' then raise(Circularity(Variable var, ty))
    | Term(constructor, arguments) ->
        Array.iter test arguments
  in test ty;;

let rec fix_levelx level_max ty =
  match value_of ty with
  | Variable var ->
      if var.level > level_max then var.level <- level_max
  | Term(constructor, arguments) ->
      Array.iter (fix_levelx level_max) arguments;;

let rec unify ty1 ty2 =
  let value1 = value_of ty1
  and value2 = value_of ty2 in
  if value1 == value2 then () else
    match (value1, value2) with
    | Variable var, ty ->
        occurrence_test var ty;
        fix_levelx var.level ty;        
        var.value <- Known ty
    | ty, Variable var ->
        occurrence_test var ty;
        fix_levelx var.level ty;        
        var.value <- Known ty
    | Term(constr1, arguments1), Term(constr2, arguments2) ->
        if constr1 <> constr2 then
          raise (Conflict(value1, value2))
        else
          for i = 0 to Array.length arguments1 - 1 do
            unify arguments1.(i) arguments2.(i)
          done;;
let binding_level = ref 0;;

let definition_beginning () = incr binding_level
and definition_end () = decr binding_level;;

let new_unknown () =
  Variable {level = !binding_level; value = Unknown};;

let generalization ty =
  let parameters = ref [] in
  let rec find_parameters ty =
    match value_of ty with
    | Variable var ->
        if var.level > !binding_level && not (List.memq var !parameters)
        then parameters := var :: !parameters
    | Term(constr, arguments) ->
        Array.iter find_parameters arguments in
  find_parameters ty;
  {parameters = !parameters; body = ty};;

let trivial_scheme ty = {parameters = []; body = ty};;

let instanciation scheme =
  match scheme.parameters with
  | [] -> scheme.body
  | parameters ->
      let nouvelles_inconnues =
        List.map (fun var -> (var, new_unknown())) parameters in
      let rec copy ty =
        match value_of ty with
        | Variable var as ty ->
            begin try
              List.assq var nouvelles_inconnues
            with Not_found ->
              ty
            end
        | Term(constr, arguments) ->
            Term(constr, Array.map copy arguments) in
      copy scheme.body;;

let variable_names = ref ([] : (type_variable * string) list)
and variable_counter = ref 0;;

let print_var var =
  print_string "'";
  try
    print_string (List.assq var !variable_names)
  with Not_found ->
    let name =
      String.make 1
        (char_of_int (int_of_char 'a' + !variable_counter)) in
    incr variable_counter;
    variable_names := (var, name) :: !variable_names;
    print_string name;;

let rec print ty =
  match value_of ty with
  | Variable var ->
      print_var var
  | Term(constructor, arguments) ->
      match Array.length arguments with
      | 0 -> print_string constructor
      | 1 -> print arguments.(0);
             print_string " "; print_string constructor
      | 2 -> print_string "("; print arguments.(0);
             print_string " "; print_string constructor;
             print_string " "; print arguments.(1);
             print_string ")"
      | _ -> failwith "constructor de type ayant trop d'arguments";;

let print_type ty =
  variable_names := [];
  variable_counter := 0;
  print ty;;
  
let print_scheme scheme =
  variable_names := [];
  variable_counter := 0;
  if scheme.parameters <> [] then begin
    print_string "pour tout ";
    List.iter (fun var -> print_var var; print_string " ")
            scheme.parameters;
    print_string ", "
  end;
  print scheme.body;;
end



module type SYNTHESIS =
sig
open Syntax;;
open Types;;

type environnment = (string * type_scheme) list;;

val type_exp : environnment -> expression -> simple_type;;
val type_def : environnment -> definition -> environnment;;

exception Error of string;;
end


module Synthesis : SYNTHESIS =
struct
open Syntax;;
open Types;;

type environnment = (string * type_scheme) list;;

exception Error of string;;

let rec type_pattern env = function
  | Variable_pattern id ->
      let ty = new_unknown() in
      (ty, (id, trivial_scheme ty) :: env)
  | Boolean_pattern b ->
      (bool_type, env)
  | Number_pattern n ->
      (int_type, env)
  | Pair_pattern(m1, m2) ->
      let (ty1, env1) = type_pattern env m1 in
      let (ty2, env2) = type_pattern env1 m2 in
      (product_type ty1 ty2, env2)
  | Nil_pattern ->
      (list_type (new_unknown()), env)
  | Motif_cons(m1, m2) ->
      let (ty1, env1) = type_pattern env m1 in
      let (ty2, env2) = type_pattern env1 m2 in
      unify (list_type ty1) ty2;
      (ty2, env2);;

let rec type_exp env = function
  | Variable id ->
      begin try instanciation (List.assoc id env)
      with Not_found -> raise (Error (id ^ " is unknown"))
      end
  | Function case_list ->
      let argument_type = new_unknown()
      and result_type = new_unknown() in
      let type_case (pattern, expr) =
        let (type_pattern, exstended_end) = type_pattern env pattern in
        unify type_pattern argument_type;
        let type_expr = type_exp exstended_end expr in
        unify type_expr result_type in
      List.iter type_case case_list;
      arrow_type argument_type result_type
  | Application(func, argument) ->
      let function_type = type_exp env func in
      let argument_type = type_exp env argument in
      let result_type = new_unknown() in
      unify function_type (arrow_type argument_type result_type);
      result_type
  | Let(def, body) -> type_exp (type_def env def) body
  | Boolean b -> bool_type
  | Number n -> int_type
  | Pair(e1, e2) -> product_type (type_exp env e1) (type_exp env e2)
  | Nil -> list_type (new_unknown())
  | Cons(e1, e2) ->
      let type_e1 = type_exp env e1 in
      let type_e2 = type_exp env e2 in
      unify (list_type type_e1) type_e2;
      type_e2

and type_def env def =
  definition_beginning();
  let type_expr =
    match def.recursive with
    | false -> type_exp env def.expr
    | true ->
        let temporary_type = new_unknown() in
        let type_expr =
          type_exp ((def.name, trivial_scheme temporary_type) :: env)
                   def.expr in
        unify type_expr temporary_type;
        type_expr in
  definition_end();
  (def.name, generalization type_expr) :: env;;
end

module type TOPLEVEL =
sig
val toplevel_loop : unit -> unit
end

module Interpretor : TOPLEVEL =
struct
open Syntax;;
open Eval;;

let code_number n =
    Number_value n
and decode_number = function
  | Number_value n -> n
  | _ -> raise(Error "integer expected")
and code_boolean b =
    Boolean_value b
and decode_boolean = function
  | Boolean_value b -> b
  | _ -> raise(Error "boolean expected");;

(* To transform a global function Toplevel into functional value *)

let prim1 coder computation decoder =
  Primitive_value (function v -> coder (computation (decoder v)))
and prim2 coder computation decoder1 decoder2 =
  Primitive_value (function
   | Pair_value (v1, v2) ->
       coder (computation (decoder1 v1) (decoder2 v2))
   | _ -> raise (Error "pair expected"));;

(* The initial environment *)

let initial_env =
  ["+",  prim2 code_number  ( + ) decode_number decode_number;
   "-",  prim2 code_number  ( - ) decode_number decode_number;
   "*",  prim2 code_number  ( * ) decode_number decode_number;
   "/",  prim2 code_number  ( / ) decode_number decode_number;
   "=",  prim2 code_boolean ( = ) decode_number decode_number;
   "<>", prim2 code_boolean ( <> ) decode_number decode_number;
   "<",  prim2 code_boolean ( < ) decode_number decode_number;
   ">",  prim2 code_boolean ( > ) decode_number decode_number;
   "<=", prim2 code_boolean ( <= ) decode_number decode_number;
   ">=", prim2 code_boolean ( >= ) decode_number decode_number;
   "not", prim1 code_boolean ( not ) decode_boolean;
   "read_int", prim1 code_number (fun x -> read_int ()) decode_number;
   "write_int", prim1 code_number
                      (fun x -> print_int x; print_newline (); 0)
                      decode_number];;
let toplevel_loop () =
  let env_global = ref initial_env in
  let input_flow = Stream.of_channel stdin in
  try
    while true do
      print_string "# "; flush stdout;
      try
        match read_sentence input_flow with
        | Expression expr ->
            let res = eval !env_global expr in
            print_string "- = "; print_value res;
            print_newline ()
        | Definition def ->
            let new_env = eval_definition !env_global def in
            begin match new_env with
            | (name, v) :: _ ->
                print_string name; print_string " = ";
                print_value v; print_newline ()
            | _ -> failwith "mauvaise gestion des definitions"
            end;
            env_global := new_env
      with
      | Stream.Error s ->
          print_string ("Syntax error: " ^ s); print_newline ()
      | Error msg ->
          print_string "Evaluation error: "; print_string msg;
          print_newline ()
    done
  with Stream.Failure -> ();;

if not !Sys.interactive then toplevel_loop ();;
end

module Type_checker : TOPLEVEL =
struct
open Syntax;;
open Types;;
open Synthesis;;

let arithmetic_type = trivial_scheme
  (arrow_type (product_type int_type int_type) int_type)
and comparison_type = trivial_scheme
  (arrow_type (product_type int_type int_type) bool_type);;

let initial_env =
  ["+",  arithmetic_type; "-", arithmetic_type;
   "*",  arithmetic_type; "/", arithmetic_type;
   "=",  comparison_type; "<>", comparison_type;
   "<",  comparison_type; ">", comparison_type;
   "<=", comparison_type; ">=", comparison_type;
   "not", trivial_scheme (arrow_type bool_type bool_type);
   "read_int", trivial_scheme (arrow_type int_type int_type);
   "write_int", trivial_scheme (arrow_type int_type int_type)];;

let toplevel_loop () =
  let env_global = ref initial_env in
  let input_flow = Stream.of_channel stdin in
  try
    while true do
      print_string "# "; flush stdout;
      try
        match read_sentence input_flow with
        | Expression expr ->
            let ty = type_exp !env_global expr in
            print_string "- : "; print_type ty;
            print_newline ()
        | Definition def ->
            let new_env = type_def !env_global def in
            begin match new_env with
            | (name, scheme) :: _ ->
                print_string name; print_string " : ";
                print_scheme scheme; print_newline ()
            | _ -> failwith "bad environment"
            end;
            env_global := new_env
      with
      | Stream.Error s ->
          print_string ("Syntax error: " ^ s); print_newline ()
      | Conflict (ty1, ty2) ->
          print_string "Type incompatibility between ";
          print_type ty1; print_string " and ";
          print_type ty2; print_newline()
      | Circularity (var, ty) ->
          print_string "Impossible to identify ";
          print_type var; print_string " and ";
          print_type ty; print_newline()
      | Error msg ->
          print_string "Typing error: "; print_string msg;
          print_newline ()
    done
  with Stream.Failure -> ();;

if not !Sys.interactive then toplevel_loop ();;
end



module Full_toplevel : TOPLEVEL =
struct
open Syntax;;
open Eval;;
open Types;;
open Synthesis;;

(* The evaluation environnment *)

let code_number n =
    Number_value n
and decode_number = function
  | Number_value n -> n
  | _ -> raise(Error "integer expected")
and code_boolean b =
    Boolean_value b
and decode_boolean = function
  | Boolean_value b -> b
  | _ -> raise(Error "boolean expected");;

(*To transform a global function into a functional value *)

let prim1 coder computation decoder =
  Primitive_value(function v -> coder (computation (decoder v)))
and prim2 coder computation decoder1 decoder2 =
  Primitive_value(function
   | Pair_value (v1, v2) ->
       coder (computation (decoder1 v1) (decoder2 v2))
   | _ -> raise (Error "pair expected"));;

(* The initial environnment *)

let initial_eval_env =
  ["+",  prim2 code_number  ( + ) decode_number decode_number;
   "-",  prim2 code_number  ( - ) decode_number decode_number;
   "*",  prim2 code_number  ( * ) decode_number decode_number;
   "/",  prim2 code_number  ( / ) decode_number decode_number;
   "=",  prim2 code_boolean ( = ) decode_number decode_number;
   "<>", prim2 code_boolean ( <> ) decode_number decode_number;
   "<",  prim2 code_boolean ( < ) decode_number decode_number;
   ">",  prim2 code_boolean ( > ) decode_number decode_number;
   "<=", prim2 code_boolean ( <= ) decode_number decode_number;
   ">=", prim2 code_boolean ( >= ) decode_number decode_number;
   "not", prim1 code_boolean ( not ) decode_boolean;
   "read_int", prim1 code_number (fun x -> read_int ()) decode_number;
   "write_int", prim1 code_number
                      (fun x -> print_int x; print_newline (); 0)
                      decode_number];;

(* The typing environnment *)

let arithmetic_type = trivial_scheme
  (arrow_type (product_type int_type int_type) int_type)
and comparison_type = trivial_scheme
  (arrow_type (product_type int_type int_type) bool_type);;

let initial_typing_env =
  ["+",  arithmetic_type; "-",  arithmetic_type;
   "*",  arithmetic_type; "/",  arithmetic_type;
   "=",  comparison_type; "<>", comparison_type;
   "<",  comparison_type; ">",  comparison_type;
   "<=", comparison_type; ">=", comparison_type;
   "not", trivial_scheme(arrow_type bool_type bool_type);
   "read_int", trivial_scheme(arrow_type int_type int_type);
   "write_int", trivial_scheme(arrow_type int_type int_type)];;

(* The toplevel loop  *)

let toplevel_loop () =
  let typing_env = ref initial_typing_env
  and eval_env = ref initial_eval_env in
  let input_flow = Stream.of_channel stdin in
  try
    while true do
      print_string "# "; flush stdout;
      try
        match read_sentence input_flow with
        | Expression expr ->
            let ty = type_exp !typing_env expr in
            let res = eval !eval_env expr in
            print_string "- : "; print_type ty;
            print_string " = "; print_value res;
            print_newline ()
        | Definition def ->
            let new_typing_env = type_def !typing_env def in
            let new_eval_env = eval_definition !eval_env def in
            begin match (new_typing_env, new_eval_env) with
            | (name, scheme) :: _, (_, v) :: _ ->
                print_string name; print_string " : ";
                print_scheme scheme; print_string " = ";
                print_value v; print_newline ()
            | _ -> failwith "incorrect treatment of definitions"
            end;
            typing_env := new_typing_env;
            eval_env := new_eval_env
      with
      | Stream.Error s ->
          print_string ("Syntaxe error: " ^ s); print_newline ()
      | Stream.Failure -> raise Sys.Break
      | Conflict(ty1, ty2) ->
          print_string "Type incompatibility between ";
          print_type ty1; print_string " and ";
          print_type ty2; print_newline ()
      | Circularity(var, ty) ->
          print_string "Impossible to identify ";
          print_type var; print_string " and ";
          print_type ty; print_newline ()
      | Eval.Error msg ->
          print_string "Evaluation error: "; print_string msg;
          print_newline ()
      | Synthesis.Error msg ->
          print_string "Typing error: "; print_string msg;
          print_newline ()
    done
  with Sys.Break -> ();;

if !Sys.interactive then () else toplevel_loop ();;
end