Hindley-milner type system

.merlin

@@ -1,27 +1,3 @@
-S src
-S src/boa
-S src/calc
-S src/calc_var
-S src/comm
-S src/lambda
-S src/levy
-S src/minihaskell
-S src/miniml
-S src/miniml_error
-S src/miniprolog
-S src/poly
-S src/sub
-B _build/src
-B _build/src/boa
-B _build/src/calc
-B _build/src/calc_var
-B _build/src/comm
-B _build/src/lambda
-B _build/src/levy
-B _build/src/minihaskell
-B _build/src/miniml
-B _build/src/miniml_error
-B _build/src/miniprolog
-B _build/src/poly
-B _build/src/sub
+S src/**
+B _build/**
 PKG menhirLib

Makefile

@@ -19,7 +19,7 @@ default:
 all: $(LANGS)
 
 $(LANGS): % :
-	$(OCAMLBUILD) -use-menhir -menhir "menhir --explain" -libs unix -I $(SRCDIR) src/$@/$@.$(BUILD)
+	$(OCAMLBUILD) -r -use-menhir -menhir "menhir --explain" -libs unix -I $(SRCDIR) src/$@/$@.$(BUILD)
 
 clean:
 	$(OCAMLBUILD) -clean

src/hm/.merlin

@@ -0,0 +1,5 @@
+FLG -w +A-4-6-9-40-42-44
+FLG -w -32-34-37
+FLG -strict_sequence -safe_string
+
+REC

src/hm/README.markdown

@@ -0,0 +1,9 @@
+An eager impure functional language with an hindley-milner type system that supports
+type inference, parametric polymorphism and value restriction. 
+The implementation contains a parser, type inference,
+and an interpreter. The language has integers, references, first class
+functions, and a general fixpoint operator.
+
+The file `example.hm` demonstrates the usage of the value restriction.
+
+The implementation is based on the article [Efficient and Insightful Generalization](http://okmij.org/ftp/ML/generalization.html) by Oleg Kiselyov.

src/hm/_tags

@@ -0,0 +1,7 @@
+true: debug
+
+true: warn(+A-4-6-9-40-42-44)
+true: strict_sequence, safe_string, short_paths
+true: bin_annot, keep_locs
+
+true : use_menhir, explain

src/hm/eval.ml

@@ -0,0 +1,99 @@
+open Syntax
+
+(** Global Environment *)
+
+type env = value NameMap.t
+let initial_env = NameMap.empty
+let add = NameMap.add
+let find x env =
+  if NameMap.mem x env then
+    NameMap.find x env
+  else
+    Zoo.error "Unbound variable %a" Printer.name x
+
+(** Substitutions *)
+
+let rec subst_value x v = function
+  | Constant c -> Constant c
+  | Lambda (y,e) when not @@ Name.equal x y ->
+    (Lambda (y, subst x v e))
+  | Lambda (_, _) 
+  | Y 
+  | Ref _
+    as v -> v
+
+(** e[x -> v] *)
+and subst x v e = match e with
+  | Var y when Name.equal x y -> V v
+  | Var n -> Var n
+  | V v' -> V (subst_value x v v')
+  | App (f,e) -> App (subst x v f, List.map (subst x v) e)
+  | Let (y,e1,e2) when not @@ Name.equal x y ->
+    Let (y, subst x v e1, subst x v e2)
+  | Let (y,e1,e2) ->
+    Let (y, subst x v e1, e2)
+
+let subst_env = NameMap.fold subst
+
+(** Evaluation *)
+
+let const x = V (Constant x)
+let delta c v = match c,v with
+  | Int _, [] -> None
+
+  | Plus, [ Constant (Int i) ; Constant (Int j) ] ->
+    Some (V (Constant (Int (i + j))))
+  | Plus, [ Constant (Int i) ] ->
+    let n = Name.create ~name:"i" () in
+    Some (V (Lambda (n, App (const Plus, [const @@ Int i; Var n]))))
+
+  | NewRef, [ v ] -> Some (V (Ref (ref v)))
+  | Get, [ Ref r ] -> Some (V !r)
+  | Set, [ Ref r ] ->
+    let n = Name.create ~name:"r" () in
+    Some (V (Lambda (n, App (const Set, [V (Ref r); Var n]))))
+  | Set, [ Ref r ; v ] -> r := v ; Some (V v)
+
+  | _ -> None
+
+exception Not_reducible : expr -> exn
+
+let log_eval i = Format.printf "%s< %a@." (String.make i ' ') Printer.expr
+let log_val i = Format.printf "%s> %a@." (String.make i ' ') Printer.value
+
+let reduction_failure e = 
+  Zoo.error ~kind:"Execution error"
+    "The following expression can not be reduced:@.%a" Printer.expr e
+
+let rec eval i e = match e with
+  | V v -> v
+  | Var _ -> reduction_failure e
+  | Let (x,e1,e2) ->
+    (* log_eval i e ; *)
+    let v = eval (i+1) e1 in
+    let v' = eval (i+1) @@ subst x v e2 in
+    (* log_val i v' ; *)
+    v'
+  | App(f,l) ->
+    (* log_eval i e ; *)
+    let vf = eval (i+1) f in
+    let ve = List.map (eval @@ i+1) l in
+    let v = eval_app (i+1) e vf ve in
+    (* log_val i v ; *)
+    v   
+
+and eval_app i eorig f l = match f, l with
+  | _, [] -> f
+  | Ref _, _ -> reduction_failure eorig
+  | Y, ve::t ->
+    let n = Name.create ~name:"Y" () in
+    eval_app i eorig ve (Lambda(n, App(V Y, [V ve; Var n])) :: t)
+  | Lambda(x, body), (v :: t) ->
+    eval_app i eorig (eval (i+1) @@ subst x v body) t
+  | Constant c, l ->
+    begin match delta c l with
+      | Some x -> eval (i+1) x
+      | None -> reduction_failure eorig
+    end
+
+let execute env p = eval 0 @@ subst_env env p

src/hm/example.hm

@@ -0,0 +1,8 @@
+let x =
+  let id = fun x -> x in
+  let id2 = id id in
+  let x = id2 3 in
+  id2
+let x = 2
+let plusx = fun y -> + x y
+let a = plusx 2

src/hm/hm.ml

@@ -0,0 +1,44 @@
+module HM = Zoo.Main (struct
+
+    let name = "HM"
+
+    type command = Syntax.command
+
+    let options = []
+
+    type environment = {
+      ty : Type.Env.env ;
+      name: Syntax.Rename.env ;
+      value: Eval.env ;
+    }
+    let add_def x ty v env = {
+      ty = Type.Env.add x ty env.ty ;
+      name = Syntax.Rename.add x.name x env.name ;
+      value = Eval.add x v env.value ;
+    }
+    let initial_environment = {
+      ty = Type.Env.empty;
+      name = Syntax.Rename.SMap.empty ;
+      value = Eval.initial_env ;
+    }
+
+    let read_more str = 
+      let i = ref (String.length str - 1) in
+      while !i >= 0 && List.mem str.[!i] [' '; '\n'; '\t'; '\r'] do decr i done ;
+      !i < 1 || (str.[!i] <> ';' || str.[!i - 1] <> ';')
+
+    let file_parser = Some (Parser.file Lexer.token)
+    let toplevel_parser = Some (Parser.toplevel Lexer.token)
+
+    let exec env c =
+      let c = Syntax.Rename.command env.name c in
+      match c with
+      | Syntax.Def (x, e) ->
+        let ty = Typing.infer_top env.ty e in
+        let v = Eval.execute env.value e in
+        Zoo.print_info "@[<2>%a@ : @[%a@]@ = @[%a@]@."
+          Printer.name x  Printer.typ ty  Printer.value v ;
+        add_def x ty v env
+  end)
+
+let () = HM.main ()

src/hm/lexer.mll

@@ -0,0 +1,23 @@
+{
+open Parser
+}
+
+rule token = parse
+  | [' ' '\t']     { token lexbuf }     (* skip blanks *)
+  | '\n' { Lexing.new_line lexbuf ; token lexbuf }
+  | '-'?[ '0'-'9' ]+ as x	{INT (int_of_string x)}
+  | "Y" { YTOK }
+  | "let" { LET }
+  | "+" { PLUS }
+  | "in" { IN }
+  | "=" { EQUAL }
+  | "fun" { FUN }
+  | "ref" { REF }
+  | "!" { BANG }
+  | ":=" { COLONEQUAL }
+  | "->" { RIGHTARROW }
+  | '('	{ LPAREN }
+  | ')'	{ RPAREN }
+  | [ 'A'-'Z' 'a'-'z' '0'-'9' '_' '\'' ]+ as s  { IDENT s }
+  | eof	{ EOF }
+  | ";;"	{ SEMISEMI }

src/hm/parser.mly

@@ -0,0 +1,60 @@
+%{
+open Syntax
+%}
+
+%token EOF SEMISEMI
+%token YTOK
+%token <string> IDENT
+%token <int> INT
+%token EQUAL PLUS
+%token LPAREN RPAREN
+%token LET IN
+%token RIGHTARROW FUN
+%token REF BANG COLONEQUAL
+
+%nonassoc FUN
+%left FUNAPP
+%nonassoc INT IDENT LPAREN YTOK PLUS REF BANG COLONEQUAL
+
+%start file
+%type <Syntax.command list> file
+
+%start toplevel
+%type <Syntax.command> toplevel
+
+%%
+file: list(command) EOF { $1 }
+toplevel: command SEMISEMI { $1 }
+
+command:
+  | LET name=name EQUAL e=expr { Def (name, e) }
+
+expr:
+  | e=simple_expr %prec FUN { e }
+  | f=simple_expr l=list_expr %prec FUNAPP
+     { App (f,List.rev l) }
+  | LET name=name EQUAL e1=expr IN e2=expr { Let (name, e1, e2) }
+
+simple_expr:
+  | v=value { V v }
+  | name=name { Var name }
+  | LPAREN e=expr RPAREN { e }
+
+list_expr:
+  | simple_expr  { [$1] }
+  | list_expr simple_expr { $2 :: $1 }
+
+value:
+  | FUN name=name RIGHTARROW e=expr { Lambda (name, e) }
+  | c=constant { Constant c }
+  | YTOK { Y }
+
+constant:
+  | i=INT { Int i }
+  | PLUS { Plus }
+  | REF { NewRef }
+  | BANG { Get }
+  | COLONEQUAL { Set }
+
+name:
+  | name=IDENT { Name.dummy name }