syntax.ml

   1: (** Abstract syntax *)
   2: 
   3: (** Type type of variable names *)
   4: type name = string
   5: 
   6: (** The type of field names *)
   7: type label = string
   8: 
   9: (** Types *)
  10: type ty =
  11:   | TInt (** integers [int] *)
  12:   | TBool (** boolean values [bool] *)
  13:   | TArrow of ty * ty (** function types [ty1 -> ty2] *)
  14:   | TRecord of (label * ty) list (** records [{l1:ty1, ..., lN:tyN}] *)
  15: 
  16: (** Expressions *)
  17: type expr =
  18:   | Var of name (** variable *)
  19:   | Int of int (** integer constant *)
  20:   | Plus of expr * expr (** sum [e1 + e2] *)
  21:   | Minus of expr * expr (** difference [e1 - e2] *)
  22:   | Times of expr * expr (** products [e1 * e2] *)
  23:   | Divide of expr * expr (** quotient [e1 / e2] *)
  24:   | Bool of bool (** boolean constant [true] or [false] *)
  25:   | Equal of expr * expr (** integer equality [e1 = e2] *)
  26:   | Less of expr * expr (** integer comparison [e1 < e2] *)
  27:   | And of expr * expr (** conjunction [e1 and e2] *)
  28:   | Or of expr * expr (** disjunction [e1 or e2] *)
  29:   | Not of expr (** negation [not e] *)
  30:   | If of expr * expr * expr (** conditional [if e1 then e2 else e3] *)
  31:   | Fun of name * name * ty * ty * expr (** recursive function [fun f(x : ty1):ty2 is e] *)
  32:   | Closure of environment * name * expr (** closure (internal value) *)
  33:   | Let of name * expr * expr (** local definition [let x = e1 in e2] *)
  34:   | App of expr * expr (** application [e1 e2] *)
  35:   | Record of (label * expr) list (** record [{l1=e1, ..., lN=eN}] *)
  36:   | Project of expr * label (** field projection [e.l] *)
  37: 
  38: (** An environment is an associative list [(x1,v1);...;(xN,vN)]. *)
  39: and environment = (name * expr) list
  40: 
  41: (** Toplevel commands *)
  42: type toplevel_cmd =
  43:   | Expr of expr (** an expression to be evaluated *)
  44:   | Def of name * expr (** Global definition [let x = e] *)
  45:   | Use of string (** load a file [$use "<filename>"] *)
  46:   | Quit (** exit toplevel [$quit] *)
  47: 
  48: (** [string_of_type ty] converts type [ty] to a string. *)
  49: let string_of_type ty =
  50:   let rec to_str n ty =
  51:     let (m, str) =
  52:       match ty with
  53:         | TInt -> (4, "int")
  54:         | TBool -> (4, "bool")
  55:         | TRecord ts ->
  56:             (4, "{" ^
  57:                String.concat ", "
  58:                (List.map (fun (l,t) -> l ^ " : " ^ (to_str (-1) t)) ts) ^
  59:                "}")
  60:         | TArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2))
  61:     in
  62:       if m > n then str else "(" ^ str ^ ")"
  63:   in
  64:     to_str (-1) ty
  65: 
  66: (** [string_of_value v] converts a value [v] to a string. *)
  67: let rec string_of_value = function
  68:   | Int n -> string_of_int n
  69:   | Bool b -> string_of_bool b
  70:   | Record rs ->
  71:       "{" ^ String.concat ", "
  72:         (List.map (fun (l,e) -> l ^ " = " ^ (string_of_value e)) rs) ^
  73:         "}"
  74:   | Closure _ -> "<fun>"
  75:   | _ -> assert false

type_check.ml

   1: (** Type checking with record subtyping *)
   2: 
   3: open Syntax
   4: 
   5: exception Type_error of string
   6: 
   7: (** [type_error msg] spro¾i izjemo [Type_error msg] *)
   8: let type_error msg = raise (Type_error msg)
   9: 
  10: (** [occurs x lst] returns [true] if [x] appears as a key in the
  11:     associative array [lst] *)
  12: let occurs x lst = List.exists (fun (y,_) -> x = y) lst
  13: 
  14: (** [check_labels lst] check whether all elements of [lst] are distinct. *)
  15: let rec check_labels = function
  16:     [] -> ()
  17:   | l :: ls ->
  18:       if List.mem l ls then type_error ("label " ^ l ^ " occurs more than once") ;
  19:       check_labels ls
  20: 
  21: (** [lookup_type x ctx] looks up the type of [x] in context [ctx]. *)
  22: let lookup_type x ctx =
  23:   try List.assoc x ctx with Not_found -> type_error ("unknown variable " ^ x)
  24: 
  25: (** [type_of ctx e] returns the type of [e] in context [ctx]. *)
  26: let rec type_of ctx = function
  27:     Var x -> lookup_type x ctx
  28:   | Int _ -> TInt
  29:   | Plus (e1, e2) 
  30:   | Minus (e1, e2) 
  31:   | Times (e1, e2) 
  32:   | Divide (e1, e2) -> check ctx e1 TInt; check ctx e2 TInt; TInt
  33:   | Bool _ -> TBool
  34:   | Equal (e1, e2)
  35:   | Less (e1, e2) -> check ctx e1 TInt; check ctx e2 TInt; TBool
  36:   | And (e1, e2)
  37:   | Or (e1, e2) -> check ctx e1 TBool; check ctx e2 TBool; TBool
  38:   | Not e -> check ctx e TBool; TBool
  39:   | If (e1, e2, e3) ->
  40:       check ctx e1 TBool;
  41:       let ty2 = type_of ctx e2 in
  42:       let ty3 = type_of ctx e3 in
  43:         if subtype ty2 ty3 then ty3
  44:         else if subtype ty3 ty2 then ty2
  45:         else type_error "incompatible types in conditional"
  46:   | Fun (f, x, ty1, ty2, e) ->
  47:       check ((f, TArrow(ty1,ty2)) :: (x, ty1) :: ctx) e ty2 ;
  48:       TArrow (ty1, ty2)
  49:   | Closure _ -> assert false
  50:   | Let (x, e1, e2) -> type_of ((x, type_of ctx e1)::ctx) e2
  51:   | App (e1, e2) ->
  52:       (match type_of ctx e1 with
  53:            TArrow (ty1, ty2) -> check ctx e2 ty1; ty2
  54:          | _ -> type_error "function expected")
  55:   | Record rs ->
  56:       check_labels (List.map fst  rs) ;
  57:       TRecord (List.map (fun (l, e) -> (l, type_of ctx e)) rs)
  58:   | Project (e, l) ->
  59:       (match type_of ctx e with
  60:            TRecord ts ->
  61:              (try List.assoc l ts with
  62:                   Not_found -> type_error ("no such field " ^ l))
  63:          | _ -> type_error "record expected" )
  64: 
  65: (** [check ctx e ty] checks whether [e] can be given type [ty] in
  66:     context [ctx]. *)
  67: and check ctx e ty =
  68:   if not (subtype (type_of ctx e) ty) then type_error "incompatible types"
  69: 
  70: (** [sybtype ty1 ty2] returns [true] if [ty1] is a subtype of [ty2]. *)
  71: and subtype ty1 ty2 =
  72:   (ty1 = ty2) ||
  73:     (match ty1, ty2 with
  74:          TArrow (u1, v1), TArrow (u2, v2) ->
  75:            (subtype u2 u1) && (subtype v1 v2)
  76:        | TRecord ts1, TRecord ts2 ->
  77:            List.for_all
  78:              (fun (l,ty) -> List.exists (fun (l',ty') -> l = l' && subtype ty' ty) ts1)
  79:              ts2
  80:        | _, _ -> false
  81:     )

eval.ml

   1: (** Large step evaluation semantics. *)
   2: 
   3: open Syntax
   4: 
   5: exception Runtime_error of string
   6: 
   7: (** [runtime_error msg] reports a runtime error by raising [Runtime_error msg] *)
   8: let runtime_error msg = raise (Runtime_error msg)
   9: 
  10: (** [lookup_value x env] looks up the value of [x] in environment [env]. *)
  11: let lookup_value x env =
  12:   try List.assoc x env with Not_found -> runtime_error ("unknown variable " ^ x)
  13: 
  14: (** [eval env e] evaluates expression [e] in environment [env]. *)
  15: let rec eval env = function
  16:   | Var x -> lookup_value x env
  17:   | Int _ as e -> e
  18:   | Plus (e1, e2) ->
  19:       (match eval env e1, eval env e2 with
  20:            Int k1, Int k2 -> Int (k1 + k2)
  21:          | _, _ -> runtime_error "integers expected in addition")
  22:   | Minus (e1, e2) ->
  23:       (match eval env e1, eval env e2 with
  24:            Int k1, Int k2 -> Int (k1 - k2)
  25:          | _, _ -> runtime_error "integers expected in subtraction")
  26:   | Times (e1, e2) ->
  27:       (match eval env e1, eval env e2 with
  28:            Int k1, Int k2 -> Int (k1 * k2)
  29:          | _, _ -> runtime_error "integers expected in multiplication")
  30:   | Divide (e1, e2) ->
  31:       (match eval env e1, eval env e2 with
  32:            Int k1, Int 0 -> runtime_error "division by zero"
  33:          | Int k1, Int k2 -> Int (k1 / k2)
  34:          | _, _ -> runtime_error "integers expeced in quotient")
  35:   | Bool _ as e -> e
  36:   | Equal (e1, e2) ->
  37:       (match eval env e1, eval env e2 with
  38:            Int k1, Int k2 -> Bool (k1 = k2)
  39:          | _, _ -> runtime_error "integers expected in equality")
  40:   | Less (e1, e2) ->
  41:       (match eval env e1, eval env e2 with
  42:            Int k1, Int k2 -> Bool (k1 < k2)
  43:          | _, _ -> runtime_error "integers expected in comparison")
  44:   | And (e1, e2) ->
  45:       (match eval env e1, eval env e2 with
  46:            Bool b1, Bool b2 -> Bool (b1 && b2)
  47:          | _, _ -> runtime_error "boolean values expected in conjunction")
  48:   | Or (e1, e2) ->
  49:       (match eval env e1, eval env e2 with
  50:            Bool b1, Bool b2 -> Bool (b1 || b2)
  51:          | _, _ -> runtime_error "boolean values expected in disjunction")
  52:   | Not b ->
  53:       (match eval env b with
  54:            Bool b -> Bool (not b)
  55:          | _ -> runtime_error "boolean values expected in negation")
  56:   | If (e1, e2, e3) ->
  57:       (match eval env e1 with
  58:            Bool true -> eval env e2
  59:          | Bool false -> eval env e3
  60:          | _ -> runtime_error "boolean value expected in conditional")
  61:   | Fun (f, x, _, _, e) ->
  62:       let rec c = Closure ((f,c)::env, x, e) in c
  63:   | Closure _ as e -> e
  64:   | Let (x, e1, e2) -> eval ((x, eval env e1)::env) e2
  65:   | App (e1, e2) ->
  66:       (match eval env e1 with
  67:            Closure (env', x, e) -> eval ((x,eval env e2)::env') e
  68:          | _ -> runtime_error "invalid application")
  69:   | Record rs ->
  70:       Record (List.map (fun (l,e) -> (l, eval env e)) rs)
  71:   | Project (e, l) ->
  72:       (match eval env e with
  73:            Record vs -> eval env (snd (List.find (fun (l',_) -> l = l') vs))
  74:          | _ -> runtime_error "record expected")
  75: 

lexer.mll

   1: {
   2:   open Parser
   3:   open Lexing
   4: 
   5:   let incr_linenum lexbuf =
   6:     let pos = lexbuf.lex_curr_p in
   7:     lexbuf.lex_curr_p <- { pos with
   8:       pos_lnum = pos.pos_lnum + 1;
   9:       pos_bol = pos.pos_cnum;
  10:     }
  11: }
  12: 
  13: let var = ['_' 'a'-'z' 'A'-'Z'] ['_' 'a'-'z' 'A'-'Z' '0'-'9']*
  14: 
  15: rule token = parse
  16:     '#' [^'\n']* '\n' { incr_linenum lexbuf; token lexbuf }
  17:   | '\n'            { incr_linenum lexbuf; token lexbuf }
  18:   | [' ' '\t']      { token lexbuf }
  19:   | ['0'-'9']+      { INT (int_of_string(lexeme lexbuf)) }
  20:   | "and"           { AND }
  21:   | "bool"          { TBOOL }
  22:   | "else"          { ELSE }
  23:   | "false"         { FALSE }
  24:   | "fun"           { FUN }
  25:   | "if"            { IF }
  26:   | "in"            { IN }
  27:   | "is"            { IS }
  28:   | "int"           { TINT }
  29:   | "let"           { LET }  
  30:   | "not"           { NOT }
  31:   | "or"            { OR }
  32:   | "then"          { THEN }
  33:   | "true"          { TRUE }
  34:   | "$use"          { USE }
  35:   | "$quit"         { QUIT }
  36:   | ";;"            { SEMICOLON2 }
  37:   | '\"' [^'\"']* '\"' { let str = lexeme lexbuf in
  38:                         STRING (String.sub str 1 (String.length str - 2)) }
  39:   | '('             { LPAREN }
  40:   | ')'             { RPAREN }
  41:   | '*'             { TIMES }
  42:   | '+'             { PLUS }
  43:   | ','             { COMMA }
  44:   | '.'             { PERIOD }
  45:   | '-'             { MINUS }
  46:   | "->"            { TARROW }
  47:   | '/'             { DIVIDE }
  48:   | ':'             { COLON }
  49:   | '<'             { LESS }
  50:   | '='             { EQUAL }
  51:   | '{'             { LBRACE }
  52:   | '}'             { RBRACE }
  53:   | var             { VAR (lexeme lexbuf) }
  54:   | eof             { EOF }
  55: 
  56: {
  57: }

parser.mly

   1: %{
   2:   open Syntax
   3: %}
   4: 
   5: %token TINT TBOOL TARROW
   6: %token LBRACE RBRACE
   7: %token COLON COMMA PERIOD
   8: %token <Syntax.name> VAR
   9: %token <int> INT
  10: %token PLUS MINUS TIMES DIVIDE
  11: %token TRUE FALSE
  12: %token EQUAL LESS
  13: %token AND OR NOT
  14: %token IF THEN ELSE
  15: %token FUN IS
  16: %token LPAREN RPAREN
  17: %token LET IN
  18: %token QUIT
  19: %token SEMICOLON2
  20: %token USE
  21: %token <string>STRING
  22: %token EOF
  23: 
  24: %start toplevel
  25: %type <Syntax.toplevel_cmd list> toplevel
  26: 
  27: %right SEMICOLON2
  28: %right COMMA
  29: %nonassoc LET IN
  30: %right FUN IS
  31: %nonassoc IF THEN ELSE
  32: %left OR
  33: %left AND
  34: $nonassoc NOT
  35: %nonassoc EQUAL LESS
  36: %left PLUS MINUS
  37: %left TIMES DIVIDE
  38: %left PERIOD
  39: %right TARROW
  40: 
  41: %%
  42: 
  43: toplevel:
  44:   | EOF                      { [] }
  45:   | exprtop                  { $1 }
  46:   | deftop                   { $1 }
  47:   | cmdtop                   { $1 }
  48: 
  49: deftop:
  50:   | def EOF                  { [$1] }
  51:   | def SEMICOLON2 toplevel  { $1 :: $3 }
  52:   | def deftop               { $1 :: $2 }
  53:   | def cmdtop               { $1 :: $2 }
  54: 
  55: exprtop:
  56:   | expr EOF                 { [Expr $1] }
  57:   | expr SEMICOLON2 toplevel { Expr $1 :: $3 }
  58: 
  59: cmdtop:
  60:   | cmd EOF                  { [$1] }
  61:   | cmd SEMICOLON2 toplevel  { $1 :: $3 }
  62: 
  63: cmd:
  64:   | USE STRING { Use $2 }
  65:   | QUIT       { Quit }
  66: 
  67: def:
  68:   | LET VAR EQUAL expr { Def ($2, $4) }
  69: 
  70: expr:
  71:   | non_app             { $1 }
  72:   | app                 { $1 }
  73:   | arith               { $1 }
  74:   | boolean             { $1 }
  75:   | IF expr THEN expr ELSE expr               { If ($2, $4, $6) }
  76:   | FUN VAR LPAREN VAR COLON ty RPAREN COLON ty IS expr { Fun ($2, $4, $6, $9, $11) }
  77: 
  78: app:
  79:     app non_app         { App ($1, $2) }
  80:   | non_app non_app     { App ($1, $2) }
  81: 
  82: non_app:
  83:     VAR                                  { Var $1 }
  84:   | TRUE                          { Bool true }
  85:   | FALSE                         { Bool false }
  86:   | INT                                  { Int $1 }
  87:   | LPAREN expr RPAREN                  { $2 }    
  88:   | LBRACE RBRACE               { Record [] }
  89:   | LBRACE record_list RBRACE   { Record $2 }
  90:   | non_app PERIOD VAR          { Project ($1, $3) }
  91: 
  92: arith:
  93:   | MINUS INT           { Int (-$2) }
  94:   | expr PLUS expr        { Plus ($1, $3) }
  95:   | expr MINUS expr        { Minus ($1, $3) }
  96:   | expr TIMES expr        { Times ($1, $3) }
  97:   | expr DIVIDE expr        { Divide ($1, $3) }
  98: 
  99: boolean:
 100:   | expr EQUAL expr     { Equal ($1, $3) }
 101:   | expr LESS expr      { Less ($1, $3) }
 102:   | expr AND expr       { And ($1, $3) }
 103:   | expr OR expr        { Or ($1, $3) }
 104:   | NOT expr         { Not $2 }
 105: 
 106: record_list:
 107:   | field                   { [$1] }
 108:   | field COMMA record_list { $1 :: $3 }
 109: 
 110: field:
 111:   | VAR EQUAL expr          { ($1, $3) }
 112: 
 113: ty:
 114:     TBOOL                      { TBool }
 115:   | TINT                      { TInt }
 116:   | ty TARROW ty             { TArrow ($1, $3) }
 117:   | LBRACE RBRACE            { TRecord [] }
 118:   | LBRACE trecord_list RBRACE { TRecord $2 }
 119:   | LPAREN ty RPAREN         { $2 }
 120: 
 121: trecord_list:
 122:   | tfield                    { [$1] }
 123:   | tfield COMMA trecord_list { $1 :: $3 }
 124: 
 125: tfield:
 126:   | VAR COLON ty              { ($1, $3) }
 127: 
 128: %%

sub.ml

   1: (** Sub tolevel. *)
   2: 
   3: open Message
   4: open Syntax
   5: 
   6: (**
   7:    The toplevel accepts global value definitions [let x = e] and expressions,
   8:    separated by double semicolons [;;] when contained in a file.
   9:  
  10:    Usage:
  11:  
  12:      [sub] runs the interactive loop
  13:  
  14:      [sub dat1 ... datN] evaluates the contents of files
  15:      [dat1], ..., [datN] then runs the interactive loop.
  16:  
  17:      [sub -n dat1 ..., datN] evaluates the contents of files
  18:      [dat1],...,[datN] and exits.
  19: *)
  20: 
  21: exception Fatal_error of string
  22: 
  23: let fatal_error msg = raise (Fatal_error msg)
  24: 
  25: (** [exec_cmd (ctx, env) n cmd] executes the toplevel command [cmd] in
  26:     the given context [ctx] and environment [env]. It forces
  27:     evaluation of up to [n] nodes of pairs and lists. It returns the
  28:     new context and environment. *)
  29: let rec exec_cmd n (ctx, env) = function
  30:     Expr e ->
  31:       (* type check [e], evaluate, and print result *)
  32:       let ty = Type_check.type_of ctx e in
  33:       let v = Eval.eval env e in
  34:         print_endline ("- : " ^ string_of_type ty ^ " = " ^ string_of_value v) ;
  35:         (ctx, env)
  36:   | Def (x, e) ->
  37:       (* type check [e], and store it unevaluated! *)
  38:       let ty = Type_check.type_of ctx e in
  39:       let v = Eval.eval env e in
  40:         print_endline ("val " ^ x ^ " : " ^ string_of_type ty ^ " = " ^ string_of_value v) ;
  41:         ((x,ty) :: ctx, (x,v) :: env)
  42:   | Quit -> raise End_of_file
  43:   | Use fn -> exec_file n (ctx, env) fn
  44: 
  45: (** [exec_file (ctx, env) n fn] executes the contents of file [fn] in
  46:     the given context [ctx] and environment [env]. It forces
  47:     evaluation of up to [n] levels of nesting of pairs and lists. It
  48:     returns the new context and environment. *)
  49: and exec_file n ce fn =
  50:   let fh = open_in fn in
  51:   let lex = Message.lexer_from_channel fn fh in
  52:     try
  53:       let cmds = Parser.toplevel Lexer.token lex in
  54:         close_in fh ;
  55:         exec_cmds n ce cmds
  56:     with
  57:         Type_check.Type_error msg -> fatal_error (fn ^ ":\n" ^ msg)
  58:       | Eval.Runtime_error msg -> fatal_error msg
  59:       | Sys.Break -> fatal_error "Interrupted."
  60:       | Parsing.Parse_error | Failure("lexing: empty token") ->
  61:           fatal_error (Message.syntax_error lex)
  62: 
  63: (** [exec_cmds (ctx, env) n cmds] executes the list of toplevel
  64:     commands [cmd] in the given context [ctx] and environment
  65:     [env]. It forces evaluation of up to [n] levels of nesting of
  66:     pairs and lists. It returns the new context and environment. *)
  67: and exec_cmds n ce cmds =
  68:   List.fold_left (exec_cmd n) ce cmds
  69: ;;
  70: 
  71: (** [shell ctx env] is the interactive shell. Here [ctx] and [env] are
  72:     the context and environment of global definitions. *)
  73: let shell n ctx env =
  74:   print_string ("Sub. Press ") ;
  75:   print_string (match Sys.os_type with
  76:                     "Unix" | "Cygwin" -> "Ctrl-D"
  77:                   | "Win32" -> "Ctrl-Z"
  78:                   | _ -> "EOF") ;
  79:   print_endline " to exit." ;
  80:   let global_ctx = ref ctx in
  81:   let global_env = ref env in
  82:     try
  83:       while true do
  84:         try
  85:           (* read a line, parse it and exectute it *)
  86:           print_string "Sub> ";
  87:           let str = read_line () in
  88:           let lex = Message.lexer_from_string str in
  89:           let cmds =
  90:             try
  91:               Parser.toplevel Lexer.token lex
  92:             with
  93:               | Failure("lexing: empty token")
  94:               | Parsing.Parse_error -> fatal_error (Message.syntax_error lex)
  95:           in
  96:           let (ctx, env) = exec_cmds n (!global_ctx, !global_env) cmds in
  97:             (* set the new values of the global context and environment *)
  98:             global_ctx := ctx ;
  99:             global_env := env
 100:         with
 101:             Fatal_error msg -> Message.report msg
 102:           | Eval.Runtime_error msg -> Message.report msg
 103:           | Type_check.Type_error msg -> Message.report msg
 104:           | Sys.Break -> Message.report ("Interrupted.")
 105:       done 
 106:     with
 107:         End_of_file -> print_endline "\nGood bye."
 108: 
 109: (** The main program. *)
 110: let main =
 111:   Sys.catch_break true ;
 112:   let print_depth = ref 100 in
 113:   let noninteractive = ref false in
 114:   let files = ref [] in
 115:     Arg.parse
 116:       [("-n", Arg.Set noninteractive, "do not run the interactive shell")]
 117:       (fun f -> files := f :: !files)
 118:       "Usage: sub [-n] [file] ..." ;
 119:     files := List.rev !files ;
 120:     let ctx, env =
 121:       try
 122:         List.fold_left (exec_file !print_depth) ([],[]) !files
 123:       with
 124:           Fatal_error msg -> Message.report msg ; exit 1
 125:     in    
 126:       if not !noninteractive then shell !print_depth ctx env