0
votes

Hi to all the community, for school project i have to implemment an Ocaml interpreter, defined in this way:

Types:

type generic = A | B | C | D | … | Z

type typ = 
    Tint 
  | Tbool
  | Tchar
  | Tlist of typ
  | Tfun of typ list * typ
  | Tgen of generic

Expressions:

type exp = 
    Eint of int 
  | Ebool of bool 
  | Echar of char
  | Empty
  | Cons of exp * exp
  | Den of ide
  | Prod of exp * exp
  | Sum of exp * exp
  | Diff of exp * exp
  | Mod of exp * exp
  | Div of exp * exp
  | Lessint of exp * exp
  | Eqint of exp * exp
  | Iszero of exp
  | Lesschar of exp * exp
  | Eqchar of exp * exp
  | Or of exp * exp
  | And of exp * exp
  | Not of exp
  | Ifthenelse of exp * exp * exp
  | Let of (ide * exp) list * exp      
  | Fun of ide list * exp
  | Apply of exp * exp list

The language has, as basic types, integer, boolean, character, functions and lists of any kind beside functional objects. Functions have a list of parameter that are identifier, and the expression Den of ide gives the expressible value associated to identifier, and the type of the identifier is type ide = string. Local declarations are a list of identifiers and expression (Let of (ide * exp) list * exp).

"Write a type inference system and an interpreter for this dynamically scoped language. The binding policy to be adopted is the deep binding policy. The result of the evaluation of an expression is a suitable value and a type. In case of a function it should return a closed expression, and closed means that each identifier in the expression must be either a local declaration or a parameter."

"The interpreter implemented at the previous point may be eager or lazy, where eager means that the argument passed to a function are evaluated as they are passed, whereas lazy means that the evaluation of the argument is performed as they are really used".

"The type inference function (type_inf) should receive an expression and should return its type which is an element of the following type"

I've already implemented types,environment,typechecker and the sem_eager but have some problems with the lazy one and dont know if my sem_eager is correct the way i did. Can someone give a look? Thanks a lot, i'm posting the code i already did these days:

(**SYNTAX**)
type generic = A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z ;;

type ide = string;;

type exp =  
  | Eint of int  
  | Ebool of bool  
  | Echar of char
  | Empty
  | Cons of exp * exp
  | Den of ide
  | Prod of exp * exp 
  | Sum of exp * exp 
  | Diff of exp * exp 
  | Mod of exp * exp 
  | Div of exp * exp 
  | Lessint of exp * exp 
  | Eqint of exp * exp 
  | Iszero of exp 
  | Lesschar of exp * exp 
  | Eqchar of exp * exp 
  | Or of exp * exp 
  | And of exp * exp 
  | Not of exp 
  | Ifthenelse of exp * exp * exp
  | Let of (ide * exp) list * exp      
  | Fun of ide list * exp
  | Apply of exp * exp list
;;

(**Types**)
type typ =  
  | Tint  
  | Tbool 
  | Tchar 
  | Tlist of typ 
  | Tfun of typ list * typ
  | Tgen of generic;;

(**AUXILIAR FUNCTION**)
let rec type_leg x = match x with
      | Eint (v) -> true
      | Ebool (v) -> true
      | Echar (v) -> true
      | Empty -> true
      | _ -> false;;

let rev list =
    let rec aux acc = function
      | [] -> acc
      | h::t -> aux (h::acc) t in
    aux [] list;;

(** ENVIRONMENT **)

type env = (ide*exp) list;;
let rho:env = [];;

let insert_value ((id:ide), el) (r:env) = if type_leg(el) then (id,el)::r     else r;;

let rec insert letlist (rho:env) = match letlist with
  |[] -> rho
  |hd::tl -> insert tl (insert_value hd rho);; 

let rec getExp (id:ide) (rho:env) = match rho with
  | [] -> (Empty)
  | hd::tl -> if fst(hd) = id then snd(hd) else getExp id tl
;;

exception TypeError of string;;

(**TYPE INFERENCE**)

let rec type_inf (e:exp) (rho:env) = match e with
  |Eint (n)  -> Tint
  |Ebool (n) -> Tbool
  |Echar (n) -> Tchar
  |Empty -> type_inf (Echar ('E')) rho
  |Cons (v, l) -> 
    (match (type_inf v rho, l) with
    |(t,Empty) -> if type_inf (Empty) rho = type_inf (Echar ('E')) rho then Tlist (t) else raise (TypeError "error")
    |(t,l) -> let temp = (type_inf l rho) in if temp = Tlist (t) then type_inf l rho else raise (TypeError "Different type"))
  |Den (id) -> type_inf (getExp id rho) rho
  |Prod (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    |(Tint, Tint) -> Tint
    |_ -> raise (TypeError "Not a Tint"))
  |Sum (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    |(Tint, Tint) -> Tint
    |_ -> raise (TypeError "Not a Tint"))
  |Diff (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    |(Tint, Tint) -> Tint
    |_ -> raise (TypeError "Not a Tint"))
  |Mod (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    |(Tint, Tint) -> Tint
    |_ -> raise (TypeError "Not a Tint"))
  |Div (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    |(Tint, Tint) -> Tint
    |_ -> raise (TypeError "Not a Tint"))
  |Lessint (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    | (Tint, Tint) -> Tbool
    | _ -> raise (TypeError "TODO"))
  |Eqint (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    | (Tint, Tint) -> Tbool
    | _ -> raise (TypeError "TODO"))
  |Iszero e1 -> (match (type_inf e1 rho) with
    | Tint -> Tbool
    | _ -> raise (TypeError " "))
  |Lesschar (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    | (Tchar, Tchar) -> Tbool
    | _ -> raise (TypeError " "))
  |Eqchar (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    | (Tchar, Tchar)-> Tbool
    | _ -> raise (TypeError " "))
  |Or (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    | (Tbool , Tbool) -> Tbool
    | _ -> raise (TypeError " "))
  |And (e1, e2) -> (match (type_inf e1 rho, type_inf e2 rho) with
    | (Tbool , Tbool) -> Tbool
    | _ -> raise (TypeError " "))
  |Not e1 -> (match (type_inf e1 rho) with
    | Tbool -> Tbool
    | _ -> raise (TypeError "cis"))
  |Ifthenelse (g, e1, e2) -> (match (type_inf g rho, type_inf e1 rho, type_inf e2 rho) with
    |(b, exp1, exp2) when exp1 = exp2 && b = Tbool -> exp1
    |_ -> raise (TypeError "error"))
  |Let (l , ex) -> type_inf ex (insert l rho)
  |Fun (l, ex) -> Tfun (getTypeFun l [], type_inf ex rho)
  |Apply (ex, l) -> type_inf ex rho

and getTypeFun l temp = match l with
    [] -> rev temp
   |hd::tl -> if type_leg (Den (hd)) then getTypeFun tl ( (type_inf (Den (hd)) rho)::temp)
    else getTypeFun tl ((Tgen (A))::temp);;


(**SEM_EAGER**)
let rec sem_eager (e:exp) (rho:env)  = match e with
  |Eint (n) ->  (Eint  (n), type_inf (Eint  (n)) rho)
  |Echar (c) -> (Echar (c), type_inf (Echar (c)) rho)
  |Ebool (b) -> (Ebool (b), type_inf (Ebool (b)) rho)
  |Empty -> (Echar ('E'), type_inf (Echar ('E')) rho)
  |Cons (v, l) -> (Cons (v,l), type_inf (Cons(v,l)) rho)
  |Den (id) -> (getExp id rho, type_inf (getExp id rho) rho)
  |Prod (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Eint e1, Tint), (Eint e2, Tint)) -> (Eint (e1 * e2), type_inf (Eint (e1 * e2)) rho)
    |_ -> failwith "errore prodotto")
  |Sum (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Eint e1, Tint), (Eint e2, Tint)) -> (Eint (e1 + e2), type_inf (Eint (e1 + e2)) rho)
    |_ -> failwith "errore somma")
  |Diff (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Eint e1, Tint), (Eint e2, Tint)) -> (Eint (e1 - e2), type_inf (Eint (e1 -  e2)) rho)
    |_ -> failwith "errore differenza") 
  |Mod (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Eint e1, Tint), (Eint e2, Tint)) -> if (not (e2 = 0)) then (Eint (e1 mod e2), type_inf (Eint (e1 mod e2)) rho) else failwith "Division for 0"
    |_ -> failwith "errore modulo") 
  |Div (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Eint e1, Tint), (Eint e2, Tint)) -> (Eint (e1 / e2), type_inf (Eint (e1 / e2)) rho)
    |_ -> failwith "errore divisione")
  |Lessint (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Eint e1, Tint), (Eint e2, Tint)) -> (Ebool (e1 < e2), type_inf (Ebool (e1 < e2)) rho)
    |_ -> failwith "errore lessInt")
  |Eqint (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Eint e1, Tint), (Eint e2, Tint)) -> (Ebool (e1 = e2), type_inf (Ebool (e1 = e2)) rho)
    |_ -> failwith "errore eqInt")
  |Iszero (e1) ->  (match (sem_eager e1 rho) with
    |(Eint e1, Tint) -> (Ebool (e1 = 0), type_inf (Ebool (e1 = 0)) rho)
    |_ -> failwith "errore iszero")
  |Lesschar (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Echar e1, Tchar), (Echar e2, Tchar)) -> (Ebool (e1 < e2), type_inf (Ebool (e1 < e2)) rho)
    |_ -> failwith "errore lesschar")
  |Eqchar (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Echar e1, Tchar), (Echar e2, Tchar)) -> (Ebool (e1 = e2), type_inf (Ebool (e1 = e2)) rho)
    |_ -> failwith "errore eqchar") 
  |Or (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Ebool e1, Tbool), (Ebool e2, Tbool)) -> (Ebool (e1 || e2), type_inf (Ebool (e1 || e2)) rho)
    |_ -> failwith "errore divisione")
  |And (e1, e2) -> (match (sem_eager e1 rho, sem_eager e2 rho) with
    |((Ebool e1, Tbool), (Ebool e2, Tbool)) -> (Ebool (e1 && e2), type_inf (Ebool (e1 && e2)) rho)
    |_ -> failwith "errore divisione") 
  |Not (e1) -> (match (sem_eager e1 rho) with
    |(Ebool e1, Tbool) -> (Ebool (not e1), type_inf (Ebool (not e1)) rho)
    |_ -> failwith "errore divisione")
  |Ifthenelse (g, e1, e2) -> 
  if ((type_inf (e1) rho) = (type_inf (e2) rho)) then
(match (sem_eager g rho) with
    |(Ebool g1, Tbool) -> if g1 then sem_eager e1 rho else sem_eager e2 rho
    |_-> failwith "not a bool")
  else failwith "different type"
  |Let (l, ex) -> sem_eager ex (insert l rho)
  |Fun (l, ex) -> (Fun (l, ex), type_inf (Fun (l, ex)) rho)
  |Apply (foo, l2) ->let rho':env = [] in match foo with
    |Fun (l1, ex) -> sem_eager ex (concatenv (insert (combine l1 l2 []) rho') rho [])
    |_-> failwith "non è una fun"

and combine (l1:ide list) (l2:exp list) (temp:env) = match (l1,l2) with
    ([],[]) -> temp
      |((hd1::tl1),(hd2::tl2)) -> combine tl1 tl2 ((hd1, hd2)::temp)
      |(_,_) -> failwith "lenght fun list doesent match"

    and concatenv (envfun:env) (envgen:env) (envres:env) = match (envfun, envgen) with
        ([],[]) -> envres
      |(hd::tl, []) -> concatenv tl [] (hd::envres)
      |(_,hd::tl) -> concatenv envfun tl (hd::envres)

;;

Thanks to all to have watched my code.

1
This question should be moved on codereview.stackexchange.com. (That's not to say, that you shouldn't post such questions, just the wrong place).ivg

1 Answers

4
votes

Your type inference is completely wrong. Test it on Fun(["x"], Den "x").

The problem is you don't do any inference at all, you just compute the types you already know.

You should use algorithm W.