Added extensible variants.

tomprimozic · Jun 16, 2014 · 4403586 · 4403586
1 parent 6d5fcab
commit 4403586
Show file tree

Hide file tree

Showing 6 changed files with 127 additions and 3 deletions.
diff --git a/extensible_rows2/core.ml b/extensible_rows2/core.ml
@@ -22,7 +22,8 @@ let core =
 	assume "zero" "int" ;
 	assume "half" "float" ;
 	assume "succ" "int -> int" ;
-	assume "plus" "(int, int) -> inc" ;
+	assume "plus" "(int, int) -> int" ;
+	assume "minus" "(int, int) -> int" ;
 	assume "eq" "forall[a] (a, a) -> bool" ;
 	assume "eq_curry" "forall[a] a -> a -> bool" ;
 	assume "not" "bool -> bool" ;
@@ -38,5 +39,7 @@ let core =
 	assume "apply_curry" "forall[a b] (a -> b) -> a -> b" ;
 	assume "choose" "forall[a] (a, a) -> a" ;
 	assume "choose_curry" "forall[a] a -> a -> a" ;
+	assume "fix" "forall[a b] ((a -> b) -> a -> b) -> a -> b" ;
+	assume "if" "forall[a] (bool, a, a) -> a" ;
 
 	!core_ref
diff --git a/extensible_rows2/expr.ml b/extensible_rows2/expr.ml
@@ -22,6 +22,16 @@ type expr =
 	| RecordExtend of (expr list) LabelMap.t * expr    (* extending a record: `{a = 1, b = 2 | r}` *)
 	| RecordRestrict of expr * name         (* deleting a label: `{r - a}` *)
 	| RecordEmpty                           (* empty record: `{}` *)
+	| Variant of name * expr                (* new variant value: `:X a` *)
+	| Case of expr * (name * name * expr) list * (name * expr) option
+			(* a pattern-matching case expression:
+					match e {
+							:X a -> expr1
+						| :Y b -> expr2
+						...
+						| z -> default_expr (optional)
+					}
+			*)
 
 type id = int
 type level = int
@@ -31,7 +41,8 @@ type ty =
 	| TApp of ty * ty list              (* type application: `list[int]` *)
 	| TArrow of ty list * ty            (* function type: `(int, int) -> int` *)
 	| TVar of tvar ref                  (* type variable *)
-	| TRecord of row                    (* record type: `{<...>}` *)
+	| TRecord of row                    (* record type: `{...}` *)
+	| TVariant of row                   (* variant type: `[...]` *)
 	| TRowEmpty                         (* empty row: `<>` *)
 	| TRowExtend of (ty list) LabelMap.t * row    (* row extension: `<a : _ , b : _ | ...>` *)
 
@@ -118,6 +129,22 @@ let string_of_expr expr : string =
 					| expr -> " | " ^ f false expr
 				in
 				"{" ^ label_expr_str ^ rest_expr_str ^ "}"
+		| Variant(label, value) ->
+				let variant_str = ":" ^ label ^ " " ^ f true value in
+				if is_simple then "(" ^ variant_str ^ ")" else variant_str
+		| Case(expr, cases, maybe_default_case) ->
+				let cases_str_list = List.map
+					(fun (label, var_name, expr) ->
+						"| :" ^ label ^ " " ^ var_name ^ " -> " ^ f false expr)
+					cases
+				in
+				let all_cases_str = match (cases_str_list, maybe_default_case) with
+					| ([], Some (var_name, expr)) -> var_name ^ " -> " ^ f false expr
+					| (cases_str_list, None) -> String.concat "" cases_str_list
+					| (cases_str_list, Some (var_name, expr)) ->
+							String.concat "" cases_str_list ^ " | " ^ var_name ^ " -> " ^ f false expr
+				in
+				"match " ^ f false expr ^ " { " ^ all_cases_str ^ " } "
 	in
 	f false expr
 
@@ -159,6 +186,7 @@ let string_of_ty ty : string =
 		| TVar {contents = Unbound(id, _)} -> "_" ^ string_of_int id
 		| TVar {contents = Link ty} -> f is_simple ty
 		| TRecord row_ty -> "{" ^ f false row_ty ^ "}"
+		| TVariant row_ty -> "[" ^ f false row_ty ^ "]"
 		| TRowEmpty -> ""
 		| TRowExtend _ as row_ty ->
 				let (label_ty_map, rest_ty) = match_row_ty row_ty in

diff --git a/extensible_rows2/infer.ml b/extensible_rows2/infer.ml
@@ -49,6 +49,7 @@ let occurs_check_adjust_levels tvar_id tvar_level ty =
 				List.iter f param_ty_list ;
 				f return_ty
 		| TRecord row -> f row
+		| TVariant row -> f row
 		| TRowExtend(label_ty_map, rest_ty) ->
 				LabelMap.iter (fun _ -> List.iter f) label_ty_map ;
 				f rest_ty
@@ -75,6 +76,7 @@ let rec unify ty1 ty2 =
 				occurs_check_adjust_levels id level ty ;
 				tvar := Link ty
 		| TRecord row1, TRecord row2 -> unify row1 row2
+		| TVariant row1, TVariant row2 -> unify row1 row2
 		| TRowEmpty, TRowEmpty -> ()
 		| (TRowExtend _ as row1), (TRowExtend _ as row2) -> unify_rows row1 row2
 		| TRowEmpty, TRowExtend(label_ty_map, _) | TRowExtend(label_ty_map, _), TRowEmpty ->
@@ -150,6 +152,7 @@ let rec generalize level = function
 			TArrow(List.map (generalize level) param_ty_list, generalize level return_ty)
 	| TVar {contents = Link ty} -> generalize level ty
 	| TRecord row -> TRecord (generalize level row)
+	| TVariant row -> TVariant (generalize level row)
 	| TRowExtend(label_ty_map, rest_ty) ->
 			TRowExtend(LabelMap.map (List.map (generalize level)) label_ty_map, generalize level rest_ty)
 	| TVar {contents = Generic _} | TVar {contents = Unbound _} | TConst _ | TRowEmpty as ty -> ty
@@ -173,6 +176,7 @@ let instantiate level ty =
 		| TArrow(param_ty_list, return_ty) ->
 				TArrow(List.map f param_ty_list, f return_ty)
 		| TRecord row -> TRecord (f row)
+		| TVariant row -> TVariant (f row)
 		| TRowEmpty -> ty
 		| TRowExtend(label_ty_map, rest_ty) ->
 				TRowExtend(LabelMap.map (List.map f) label_ty_map, f rest_ty)
@@ -256,3 +260,34 @@ let rec infer env level = function
 			let rest_row_ty = new_var level in
 			unify (TRecord rest_row_ty) (infer env level record_expr) ;
 			TRecord (TRowExtend(label_ty_map, rest_row_ty))
+	| Variant(label, expr) ->
+			(* inlined code for Call of function with type "forall [a r] a -> [label : a | r]" *)
+			let rest_row_ty = new_var level in
+			let variant_ty = new_var level in
+			let param_ty = variant_ty in
+			let return_ty = TVariant (TRowExtend(LabelMap.singleton label [variant_ty], rest_row_ty)) in
+			unify param_ty (infer env level expr) ;
+			return_ty
+	| Case(expr, cases, None) ->
+			let return_ty = new_var level in
+			let expr_ty = infer env level expr in
+			let cases_row = infer_cases env level return_ty TRowEmpty cases in
+			unify expr_ty (TVariant cases_row) ;
+			return_ty
+	| Case(expr, cases, Some (default_var_name, default_expr)) ->
+			let default_variant_ty = new_var level in
+			let return_ty =
+				infer (Env.extend env default_var_name (TVariant default_variant_ty)) level default_expr
+			in
+			let expr_ty = infer env level expr in
+			let cases_row = infer_cases env level return_ty default_variant_ty cases in
+			unify expr_ty (TVariant cases_row) ;
+			return_ty
+
+and infer_cases env level return_ty rest_row_ty cases = match cases with
+	| [] -> rest_row_ty
+	| (label, var_name, expr) :: other_cases ->
+			let variant_ty = new_var level in
+			unify return_ty (infer (Env.extend env var_name variant_ty) level expr) ;
+			let other_cases_row = infer_cases env level return_ty rest_row_ty other_cases in
+			TRowExtend(LabelMap.singleton label [variant_ty], other_cases_row)
diff --git a/extensible_rows2/lexer.mll b/extensible_rows2/lexer.mll
@@ -16,6 +16,7 @@ rule token = parse
 	| "let"                 { LET }
 	| "in"                  { IN }
 	| "forall"              { FORALL }
+	| "match"               { MATCH }
 	| ident                 { IDENT (Lexing.lexeme lexbuf) }
 	| '('     { LPAREN }
 	| ')'     { RPAREN }
@@ -41,6 +42,7 @@ let string_of_token = function
 	| LET -> "let"
 	| IN -> "in"
 	| FORALL -> "forall"
+	| MATCH -> "match"
 	| IDENT ident -> ident
 	| LPAREN -> "("
 	| RPAREN -> ")"

diff --git a/extensible_rows2/parser.mly b/extensible_rows2/parser.mly
@@ -49,6 +49,7 @@ let replace_ty_constants_with_vars var_name_list ty =
 		| TApp(ty, ty_arg_list) -> TApp(f ty, List.map f ty_arg_list)
 		| TArrow(param_ty_list, return_ty) -> TArrow(List.map f param_ty_list, f return_ty)
 		| TRecord row -> TRecord (f row)
+		| TVariant row -> TVariant (f row)
 		| TRowEmpty -> ty
 		| TRowExtend(label_ty_map, row) ->
 				TRowExtend(LabelMap.map (List.map f) label_ty_map, f row)
@@ -58,7 +59,7 @@ let replace_ty_constants_with_vars var_name_list ty =
 %}
 
 %token <string> IDENT
-%token FUN LET IN FORALL
+%token FUN LET IN FORALL MATCH
 %token LPAREN RPAREN LBRACKET RBRACKET LBRACE RBRACE
 %token ARROW EQUALS COMMA DOT MINUS PIPE COLON
 %token EOF
@@ -85,6 +86,11 @@ expr:
 	| simple_expr                         { $1 }
 	| LET IDENT EQUALS expr IN expr       { Let($2, $4, $6) }
 	| FUN ident_list ARROW expr           { Fun($2, $4) }
+	| COLON IDENT simple_expr             { Variant($2, $3) }
+	| MATCH expr LBRACE match_case_list RBRACE      {
+			let cases, maybe_default_case = $4 in
+			Case($2, cases, maybe_default_case)
+		}
 
 simple_expr:
 	| IDENT                                             { Var $1 }
@@ -109,6 +115,20 @@ record_label_expr_list:
 	| IDENT EQUALS expr                               { [($1, $3)] }
 	| record_label_expr_list COMMA IDENT EQUALS expr  { ($3, $5) :: $1 }
 
+match_case_list:
+	| match_case                        { ([$1], None) }
+	| match_default_case                { ([], Some $1) }
+	| match_case PIPE match_case_list   {
+			let cases, maybe_default_case = $3 in
+			($1 :: cases, maybe_default_case)
+		}
+
+match_case:
+	| COLON IDENT IDENT ARROW expr     { ($2, $3, $5) }
+
+match_default_case:
+	| IDENT ARROW expr     { ($1, $3) }
+
 ty_forall:
 	| ty                                        { $1 }
 	| FORALL LBRACKET ident_list RBRACKET ty    { replace_ty_constants_with_vars $3 $5 }
@@ -127,6 +147,10 @@ simple_ty:
 	| LBRACE IDENT RBRACE                           { TRecord (TConst $2) }
 	| LBRACE ty_row PIPE ty RBRACE                  { TRecord (ty_row_extend $2 $4) }
 	| LBRACE ty_row RBRACE                          { TRecord (ty_row_extend $2 TRowEmpty) }
+	| LBRACKET RBRACKET                             { TVariant TRowEmpty }
+	| LBRACKET IDENT RBRACKET                       { TVariant (TConst $2) }
+	| LBRACKET ty_row PIPE ty RBRACKET              { TVariant (ty_row_extend $2 $4) }
+	| LBRACKET ty_row RBRACKET                      { TVariant (ty_row_extend $2 TRowEmpty) }
 
 ty_comma_list:
 	| ty                        { [$1] }

diff --git a/extensible_rows2/test_infer.ml b/extensible_rows2/test_infer.ml
@@ -56,6 +56,11 @@ let test_cases = [
 	("let const = fun x -> fun y -> x in const", OK "forall[a b] a -> b -> a");
 	("let apply = fun f x -> f(x) in apply", OK "forall[a b] (a -> b, a) -> b");
 	("let apply_curry = fun f -> fun x -> f(x) in apply_curry", OK "forall[a b] (a -> b) -> a -> b");
+	("let fib1 = fun fib -> fun n -> " ^
+	 "if(eq(n, one), one, " ^
+	 "if(eq(n, zero), one, " ^
+	 "plus(fib(minus(n, one)), fib(minus(n, succ(one)))))) in " ^
+	 "fix(fib1)", OK "int -> int");
 
 	(* records *)
 	("{}", OK "{}");
@@ -111,6 +116,33 @@ let test_cases = [
 	 "choose({b = true, a = one, c = one, b = half | r}, {b = false, c = one, a = one, b = half | s})",
 		OK "forall[a] ({a}, {a}) -> {a : int, b : bool, b : float, c : int | a}");
 	("fun r -> {x = r | r}", OK "forall[a] {a} -> {x : {a} | a}");
+
+	(* variants *)
+	(":X one", OK "forall[a] [X : int | a]");
+	("choose(choose(:x one, :Y true), choose(:X half, :y nil))",
+		OK "forall[a b] [X : float, Y : bool, x : int, y : list[a] | b]");
+	("choose(:X one, :X true)", error "cannot unify types int and bool");
+	("choose(:X {x = one, y = false}, :Y {w = half})",
+		OK "forall[a] [X : {x : int, y : bool}, Y : {w : float} | a]");
+	("let e = choose(choose(:x one, :Y true), choose(:X half, :y nil)) in " ^
+	 "match e { :x i -> i | :Y y -> zero}", error "row does not contain label X");
+	("fun x y -> match x {:a i -> one | :b i -> zero | :c i -> y}",
+		OK "forall [a b c] ([a : a, b : b, c : c], int) -> int");
+	("fun a -> match a {:X i -> i | r -> one}", OK "forall[a] [X : int | a] -> int");
+	("let f = fun m -> match m {:y a -> one | :Y b -> zero | :z z -> zero} in " ^
+	 "fun e -> match e { :x i -> i | :X f -> one | r -> f(r)}",
+	 OK "forall[a b c d] [X : a, Y : b, x : int, y : c, z : d] -> int");
+	("let e = choose(choose(:x one, :Y true), choose(:X half, :y nil)) in " ^
+	 "let f = fun m -> match m {:y a -> one | :Y b -> zero | :z z -> zero} in " ^
+	 "match e { :x i -> i | :X f -> one | r -> f(r)}", OK "int");
+	("fun e -> match e {:X a -> one | :X i -> i}", OK "forall[a] [X : a, X : int] -> int");
+	("let f = fun g -> fun e -> match e { :x i -> i | :Y a -> one | r -> g(r)} in " ^
+	 "let g = fun s -> match s {:x j -> head(j) | :X a -> zero} in " ^
+	 "f(g)", OK "forall[a b] [X : a, Y : b, x : int, x : list[int]] -> int");
+	("fun e -> match e { :X a -> plus(a.x, one) }", OK "forall[a] [X : {x : int | a}] -> int");
+	("let count1 = fun count -> fun x -> " ^
+	 " match x {:Cons a -> plus(one, count(a.tail)) | :Nil _ -> zero} in " ^
+	 "fix(count1)", error "recursive types");
 	]