From 492871278e193a9a9ed1dfbf9c0adfed02e95e33 Mon Sep 17 00:00:00 2001 From: Drup Date: Sun, 14 Jan 2018 20:05:51 +0100 Subject: [PATCH 1/2] Misc changes to the framework. --- .merlin | 28 ++-------------------------- Makefile | 2 +- src/zoo.ml | 2 +- 3 files changed, 4 insertions(+), 28 deletions(-) diff --git a/.merlin b/.merlin index 6be39dd..065f737 100644 --- a/.merlin +++ b/.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 diff --git a/Makefile b/Makefile index 7a80a94..65e68c7 100644 --- a/Makefile +++ b/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 diff --git a/src/zoo.ml b/src/zoo.ml index 33cacdf..b167243 100644 --- a/src/zoo.ml +++ b/src/zoo.ml @@ -167,7 +167,7 @@ struct (** Parser wrapper that catches syntax-related errors and converts them to errors. *) let wrap_syntax_errors parser lex = - try + try[@warning "-52"] parser lex with | Failure _ -> From 9cbeee391fbfb7ae6132cfe6e5ec2e67792441a6 Mon Sep 17 00:00:00 2001 From: Drup Date: Sun, 14 Jan 2018 22:10:12 +0100 Subject: [PATCH 2/2] Add the HM language Implementation of an hindley-milner type system with value restriction for a strict language, impure language. --- src/hm/.merlin | 5 ++ src/hm/README.markdown | 9 +++ src/hm/_tags | 7 ++ src/hm/eval.ml | 99 ++++++++++++++++++++++++++ src/hm/example.hm | 8 +++ src/hm/hm.ml | 44 ++++++++++++ src/hm/lexer.mll | 23 ++++++ src/hm/parser.mly | 60 ++++++++++++++++ src/hm/printer.ml | 98 ++++++++++++++++++++++++++ src/hm/syntax.ml | 78 +++++++++++++++++++++ src/hm/tagline.markdown | 1 + src/hm/type.ml | 42 +++++++++++ src/hm/typing.ml | 152 ++++++++++++++++++++++++++++++++++++++++ 13 files changed, 626 insertions(+) create mode 100644 src/hm/.merlin create mode 100644 src/hm/README.markdown create mode 100644 src/hm/_tags create mode 100644 src/hm/eval.ml create mode 100644 src/hm/example.hm create mode 100644 src/hm/hm.ml create mode 100644 src/hm/lexer.mll create mode 100644 src/hm/parser.mly create mode 100644 src/hm/printer.ml create mode 100644 src/hm/syntax.ml create mode 100644 src/hm/tagline.markdown create mode 100644 src/hm/type.ml create mode 100644 src/hm/typing.ml diff --git a/src/hm/.merlin b/src/hm/.merlin new file mode 100644 index 0000000..deb88b6 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/hm/README.markdown b/src/hm/README.markdown new file mode 100644 index 0000000..c82c998 --- /dev/null +++ b/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. diff --git a/src/hm/_tags b/src/hm/_tags new file mode 100644 index 0000000..b02754b --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/hm/eval.ml b/src/hm/eval.ml new file mode 100644 index 0000000..0c48cdd --- /dev/null +++ b/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 diff --git a/src/hm/example.hm b/src/hm/example.hm new file mode 100644 index 0000000..5a9ae2c --- /dev/null +++ b/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 diff --git a/src/hm/hm.ml b/src/hm/hm.ml new file mode 100644 index 0000000..3c0d75b --- /dev/null +++ b/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 () diff --git a/src/hm/lexer.mll b/src/hm/lexer.mll new file mode 100644 index 0000000..de66ab8 --- /dev/null +++ b/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 } diff --git a/src/hm/parser.mly b/src/hm/parser.mly new file mode 100644 index 0000000..28523f7 --- /dev/null +++ b/src/hm/parser.mly @@ -0,0 +1,60 @@ +%{ +open Syntax +%} + +%token EOF SEMISEMI +%token YTOK +%token IDENT +%token 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 file + +%start toplevel +%type 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 } diff --git a/src/hm/printer.ml b/src/hm/printer.ml new file mode 100644 index 0000000..216715a --- /dev/null +++ b/src/hm/printer.ml @@ -0,0 +1,98 @@ +open Syntax +module T = Type + +let bold fmt s = Format.fprintf fmt "@<0>%s%s@<0>%s" "\027[1m" s "\027[0m" + +let constant fmt = function + | Int i -> Format.pp_print_int fmt i + | Plus -> bold fmt "+" + | NewRef -> bold fmt "new" + | Get -> bold fmt "!" + | Set -> bold fmt ":=" + +let indice_array = [|"₀";"₁";"₂";"₃";"₄";"₅";"₆";"₇";"₈";"₉"|] +let rec digits fmt i = + if i < 0 then + Format.pp_print_string fmt "₋" + else if i < 10 then + Format.pp_print_string fmt indice_array.(i) + else begin + digits fmt (i/10) ; + Format.pp_print_string fmt indice_array.(i mod 10) + end + +let name fmt {Name. name ; id } = + Format.fprintf fmt "%s%a" name digits id + +let rec value + = fun fmt -> function + | Constant c -> constant fmt c + | Lambda (n,e) -> + Format.fprintf fmt "@[<2>%a %a %a@ %a@]" + bold "fun" + name n + bold "->" + expr e + | Ref { contents } -> Format.fprintf fmt "{%a}" value contents + | Y -> Format.fprintf fmt "Y" + +and expr + = fun fmt -> function + | V v -> value fmt v + | Var v -> name fmt v + | App (f,e) -> + Format.fprintf fmt "@[<2>@[%a@]@ %a@]" + expr_with_paren f + Format.(pp_print_list ~pp_sep:pp_print_space expr_with_paren) e + | Let (n,e1,e2) -> + Format.fprintf fmt "@[@[<2>%a %a %a@ %a@]@ %a@ %a@]" + bold "let" name n + bold "=" expr e1 + bold "in" expr e2 + +and expr_with_paren fmt x = + let must_have_paren = match x with + | App _ -> true + | Let _ -> true + | V (Lambda _) -> true + | _ -> false + in + Format.fprintf fmt + (if must_have_paren then "@[(%a@])" else "%a") expr x + +let rec typ_need_paren = function + | T.Arrow _ -> true + | T.Var { contents = Link t } -> typ_need_paren t + | _ -> false + +let rec tyvar + = fun fmt -> function + | T.Unbound (n,_) -> Format.fprintf fmt "'_%a" name n + | T.Link t -> typ_with_paren fmt t + +and typ + = fun fmt -> function + | T.Const n -> name fmt n + | T.App (f,e) -> Format.fprintf fmt "@[<2>%a@ %a@]" typ_with_paren e typ f + | T.Arrow (a,b) -> Format.fprintf fmt "%a -> %a" typ_with_paren a typ b + | T.Var { contents = x } -> tyvar fmt x + | T.GenericVar n -> Format.fprintf fmt "'%a" name n + +and typ_with_paren fmt x = + let must_have_paren = match x with + | T.Arrow _ -> true + | _ -> false + in + Format.fprintf fmt + (if must_have_paren then "@[(%a@])" else "%a") typ x + +let typ_env fmt env = + let print_env fmt e = + Format.pp_print_list + ~pp_sep:Format.pp_print_cut + (fun fmt (k,ty) -> Format.fprintf fmt "%a: %a" name k typ ty) + fmt + @@ T.Env.M.bindings e + in + Format.fprintf fmt "Server:@;<1 2>@[%a@]@.Client:@;<1 2>@[%a@]@." + print_env env diff --git a/src/hm/syntax.ml b/src/hm/syntax.ml new file mode 100644 index 0000000..026408e --- /dev/null +++ b/src/hm/syntax.ml @@ -0,0 +1,78 @@ +module Name = struct + type t = {name : string ; id : int} + let compare n1 n2 = compare n1.id n2.id + let equal n1 n2 = n1.id = n2.id + let dummy name = { name ; id = -1 } + let create = + let r = ref 0 in + fun ?(name="") () -> + let id = !r in incr r ; + { name ; id } +end +module NameMap = Map.Make(Name) + +type constant = + | Int of int + | Plus + | NewRef + | Get + | Set + +type value = + | Constant of constant + | Lambda of Name.t * expr + | Ref of value ref + | Y + +and expr = + | V of value + | Var of Name.t + | App of expr * expr list + | Let of Name.t * expr * expr +type command = + | Def of Name.t * expr + +let is_value = function + | V _ -> true + | _ -> false + + +module Rename = struct + module SMap = Map.Make(String) + + type env = Name.t SMap.t + + let find x env = + if SMap.mem x env then + SMap.find x env + else + Zoo.error "Unbound variable %s" x + + let add n k env = SMap.add n k env + + let rec value env = function + | Lambda ({name}, e) -> + let new_name = Name.create ~name () in + let env = add name new_name env in + let e = expr env e in + Lambda (new_name, e) + | Constant _ | Y | Ref _ as e-> e + + and expr env = function + | V v -> V (value env v) + | Var { name } -> Var (find name env) + | App (f, l) -> App (expr env f, List.map (expr env) l) + | Let ({name}, e1, e2) -> + let e1 = expr env e1 in + let new_name = Name.create ~name () in + let env = add name new_name env in + let e2 = expr env e2 in + Let (new_name, e1, e2) + + let command env = function + | Def ({name},e) -> + let e = expr env e in + let new_name = Name.create ~name () in + Def (new_name, e) + +end diff --git a/src/hm/tagline.markdown b/src/hm/tagline.markdown new file mode 100644 index 0000000..9e31cae --- /dev/null +++ b/src/hm/tagline.markdown @@ -0,0 +1 @@ +eager, reference, functional, statically typed, parametric polymorphism, type inference, hindley-milner, value restriction. diff --git a/src/hm/type.ml b/src/hm/type.ml new file mode 100644 index 0000000..23818e7 --- /dev/null +++ b/src/hm/type.ml @@ -0,0 +1,42 @@ +open Syntax + +type level = int + +type t = + | Const : Name.t -> t + | App : t * t -> t + | Arrow : t * t -> t + | GenericVar : Name.t -> t + | Var : var ref -> t + +and var = + | Unbound of Name.t * level + | Link of t + +module Env = struct + module M = NameMap + exception Var_not_found of Name.t + type env = t M.t + let add k (v: t) env = M.add k v env + + let find k env : t = + try M.find k env with + Not_found -> raise (Var_not_found k) + + let empty = M.empty +end + +(** Predefined types *) + +let new_y () = + let y_name = Name.create ~name:"a" () in + let n = GenericVar y_name in + Arrow(Arrow(n,n),n) + +let int_name = Name.create ~name:"int" () +let int = Const int_name + +let ref_name = Name.create ~name:"ref" () +let ref = Const ref_name + +let (@->) x y = Arrow (x,y) diff --git a/src/hm/typing.ml b/src/hm/typing.ml new file mode 100644 index 0000000..3bfe125 --- /dev/null +++ b/src/hm/typing.ml @@ -0,0 +1,152 @@ +open Syntax +module T = Type + +let fail fmt = + Zoo.error ~kind:"Type error" fmt + +let new_var level = T.Var (ref (T.Unbound(Name.create (), level))) +let new_gen_var () = T.GenericVar(Name.create ()) + +let occurs_check_adjust_levels tvar_id tvar_level ty = + let rec f : T.t -> _ = function + | T.Var {contents = T.Link ty} -> f ty + | T.GenericVar _ -> assert false + | T.Var ({contents = T.Unbound(other_id, other_level)} as other_tvar) -> + if other_id = tvar_id then + fail "Recursive types" + else + other_tvar := Unbound(other_id, min tvar_level other_level) + | T.App(ty, ty_arg) -> + f ty ; + f ty_arg + | T.Arrow(param_ty, return_ty) -> + f param_ty ; + f return_ty + | T.Const _ -> () + in + f ty + + +let rec unify + = fun ty1 ty2 -> match ty1, ty2 with + | _, _ when ty1 == ty2 -> () + + | T.Const name1, T.Const name2 when Syntax.Name.equal name1 name2 -> () + + | T.App(ty1, ty_arg1), T.App(ty2, ty_arg2) -> + unify ty1 ty2 ; + unify ty_arg1 ty_arg2 + + | T.Arrow(param_ty1, return_ty1), T.Arrow(param_ty2, return_ty2) -> + unify param_ty1 param_ty2 ; + unify return_ty1 return_ty2 + + | T.Var {contents = Link ty1}, ty2 -> unify ty1 ty2 + | ty1, T.Var {contents = Link ty2} -> unify ty1 ty2 + + | T.Var {contents = Unbound(id1, _)}, + T.Var {contents = Unbound(id2, _)} when id1 = id2 -> + (* There is only a single instance of a particular type variable. *) + assert false + + | T.Var ({contents = Unbound(id, level)} as tvar), ty + | ty, T.Var ({contents = Unbound(id, level)} as tvar) -> + occurs_check_adjust_levels id level ty ; + tvar := Link ty + + | _, _ -> + fail "Cannot unify types %a and %a@." Printer.typ ty1 Printer.typ ty2 + + + +let rec generalize level = function + | T.Var {contents = Unbound(id, other_level)} when other_level > level -> + T.GenericVar id + | T.App(ty, ty_arg) -> + App(generalize level ty, generalize level ty_arg) + | T.Arrow(param_ty, return_ty) -> + Arrow(generalize level param_ty, generalize level return_ty) + + | T.Var {contents = Link ty} -> generalize level ty + + | ( T.GenericVar _ + | T.Var {contents = Unbound _} + | T.Const _ + ) as ty -> ty + +(** The real generalization function that is aware of the value restriction. *) +let generalize level ty exp = + if Syntax.is_value exp then + generalize level ty + else + ty + +let instantiate level ty = + let id_var_map = Hashtbl.create 10 in + let rec f = function + | T.Const _ as ty -> ty + | T.Var {contents = Link ty} -> f ty + | T.GenericVar id -> + begin try + Hashtbl.find id_var_map id + with Not_found -> + let var = new_var level in + Hashtbl.add id_var_map id var ; + var + end + | T.Var {contents = Unbound _} as ty -> ty + | T.App(ty, ty_arg) -> + App(f ty, f ty_arg) + | T.Arrow(param_ty, return_ty) -> + Arrow(f param_ty, f return_ty) + in + f ty + +let constant = let open T in function + | Int _ -> int + | Plus -> int @-> int @-> int + | NewRef -> + let a = new_gen_var () in + a @-> T.App (ref, a) + | Get -> + let a = new_gen_var () in + T.App (ref, a) @-> a + | Set -> + let a = new_gen_var () in + T.App (ref, a) @-> a @-> a + +let rec infer_value env level = function + | Constant c -> instantiate level @@ constant c + | Y -> instantiate level @@ T.new_y () + | Lambda(param, body_expr) -> + let param_ty = new_var level in + let fn_env = T.Env.add param param_ty env in + let return_ty = infer fn_env level body_expr in + T.Arrow (param_ty, return_ty) + | Ref v -> + T.App (T.ref, infer_value env level !v) + +and infer env level = function + | V v -> infer_value env level v + | Var name -> + instantiate level @@ T.Env.find name env + | Let(var_name, value_expr, body_expr) -> + let var_ty = infer env (level + 1) value_expr in + let generalized_ty = generalize level var_ty value_expr in + infer (T.Env.add var_name generalized_ty env) level body_expr + | App(fn_expr, arg) -> + let f_ty = infer env level fn_expr in + infer_app env level f_ty arg + +and infer_app env level f_ty = function + | [] -> f_ty + | e::t -> + let param_ty = infer env level e in + let return_ty = new_var level in + unify f_ty (T.Arrow (param_ty, return_ty)) ; + infer_app env level return_ty t + +let infer_top env e = + let ty = infer env 1 e in + let ty = generalize 0 ty e in + ty