Add if/else statements to Bolt

Resolves #52

src/parsing/lexer.mll

@@ -63,6 +63,9 @@ rule read_token =
   | "bool" { TYPE_BOOL } 
   | "true" { TRUE }
   | "false" { FALSE }
+  | "if" {IF}
+  | "then" {THEN}
+  | "else" {ELSE}
   | whitespace { read_token lexbuf }
   | "(*" { comment lexbuf } 
   | int { INT (int_of_string (Lexing.lexeme lexbuf))}

src/parsing/parsed_ast.ml

@@ -17,6 +17,7 @@ type expr =
   | Constructor of loc * Class_name.t * constructor_arg list
   | Consume     of loc * expr
   | FinishAsync of loc * expr * expr * expr
+  | If          of loc * expr * expr * expr
 
 and constructor_arg = ConstructorArg of Field_name.t * expr
 

src/parsing/parsed_ast.mli

@@ -18,6 +18,7 @@ type expr =
   | Consume     of loc * expr
   | FinishAsync of loc * expr * expr * expr
       (** first async expr, second async expr, next expr after async exection completed *)
+  | If          of loc * expr * expr * expr  (** If ___ then ___ else ___ *)
 
 and constructor_arg = ConstructorArg of Field_name.t * expr  (** read as (f: ___) *)
 

src/parsing/parser.mly

@@ -38,6 +38,9 @@
 %token TYPE_BOOL
 %token TRUE
 %token FALSE
+%token IF
+%token THEN
+%token ELSE
 %token  EOF 
 
 
@@ -133,7 +136,9 @@ expr:
 | FINISH LBRACE ASYNC expr ASYNC expr RBRACE SEMICOLON expr {FinishAsync($startpos, $4, $6, $9)}
 | LBRACE separated_list(SEMICOLON, expr) RBRACE { Block($startpos, $2)}
 | ID  args {App($startpos, Function_name.of_string $1, $2)} 
-| ID DOT ID args {ObjMethod($startpos, Var_name.of_string $1, Function_name.of_string $3, $4)}
+| ID DOT ID args {ObjMethod($startpos, Var_name.of_string $1, Function_name.of_string $3, $4) }
+| IF expr option(THEN) expr ELSE expr {If($startpos, $2, $4, $6)}
+
 
 
 constructor_arg:

src/parsing/pprint_parser_tokens.ml

@@ -36,3 +36,6 @@ let pprint_tokens ppf = function
   | CLASS     -> Fmt.pf ppf "CLASS@."
   | ASYNC     -> Fmt.pf ppf "ASYNC@."
   | ASSIGN    -> Fmt.pf ppf "ASSIGN@."
+  | IF        -> Fmt.pf ppf "IF@."
+  | THEN      -> Fmt.pf ppf "THEN@."
+  | ELSE      -> Fmt.pf ppf "ELSE@."

src/parsing/pprint_past.ml

@@ -49,6 +49,11 @@ let rec pprint_expr ppf ~indent expr =
       pprint_expr ppf ~indent:new_indent async_expr1 ;
       pprint_expr ppf ~indent:new_indent async_expr2 ;
       pprint_expr ppf ~indent:new_indent next_expr
+  | If (_, cond_expr, then_expr, else_expr) ->
+      print_expr "If" ;
+      pprint_expr ppf ~indent:new_indent cond_expr ;
+      pprint_expr ppf ~indent:new_indent then_expr ;
+      pprint_expr ppf ~indent:new_indent else_expr
 
 and pprint_constructor_arg ppf ~indent (ConstructorArg (field_name, expr)) =
   let new_indent = indent_space ^ indent in

src/typing/core_lang/pprint_tast.ml

@@ -62,6 +62,12 @@ let rec pprint_expr ppf ~indent expr =
       pprint_expr ppf ~indent:new_indent async_expr1 ;
       pprint_expr ppf ~indent:new_indent async_expr2 ;
       pprint_expr ppf ~indent:new_indent next_expr
+  | If (_, type_expr, cond_expr, then_expr, else_expr) ->
+      print_expr "Finish_async" ;
+      pprint_type_expr ppf ~indent:new_indent type_expr ;
+      pprint_expr ppf ~indent:new_indent cond_expr ;
+      pprint_expr ppf ~indent:new_indent then_expr ;
+      pprint_expr ppf ~indent:new_indent else_expr
 
 and pprint_constructor_arg ppf indent (ConstructorArg (type_expr, field_name, expr)) =
   let new_indent = indent_space ^ indent in

src/typing/core_lang/type_expr.ml

@@ -211,6 +211,35 @@ let rec infer_type_expr class_defns trait_defns function_defns (expr : Parsed_as
       ( Typed_ast.FinishAsync
           (loc, next_expr_type, typed_async_expr1, typed_async_expr2, typed_next_expr)
       , next_expr_type )
+  | Parsed_ast.If (loc, cond_expr, then_expr, else_expr) -> (
+      infer_type_with_defns cond_expr env
+      >>= fun (typed_cond_expr, cond_expr_type) ->
+      infer_type_with_defns then_expr env
+      >>= fun (typed_then_expr, then_expr_type) ->
+      infer_type_with_defns else_expr env
+      >>= fun (typed_else_expr, else_expr_type) ->
+      if not (then_expr_type = else_expr_type) then
+        Error
+          (Error.of_string
+             (Fmt.str
+                "%s Type error - If statement branches' types' not consistent - then branch has type %s but else branch has type %s@."
+                (string_of_loc loc)
+                (string_of_type then_expr_type)
+                (string_of_type else_expr_type)))
+      else
+        match cond_expr_type with
+        | TEBool ->
+            Ok
+              ( Typed_ast.If
+                  (loc, then_expr_type, typed_cond_expr, typed_then_expr, typed_else_expr)
+              , then_expr_type )
+        | _      ->
+            Error
+              (Error.of_string
+                 (Fmt.str
+                    "%s Type error - If statement condition expression should have boolean type but instead has type %s@."
+                    (string_of_loc loc)
+                    (string_of_type cond_expr_type))) )
 
 (* Top level statement to infer type of overall program expr *)
 let type_expr class_defns trait_defns function_defns (expr : Parsed_ast.expr) =

src/typing/core_lang/typed_ast.ml

@@ -20,6 +20,7 @@ type expr =
   | Constructor of loc * type_expr * Class_name.t * constructor_arg list
   | Consume     of loc * type_expr * expr (* type is that of the expr being consumed *)
   | FinishAsync of loc * type_expr * expr * expr * expr
+  | If          of loc * type_expr * expr * expr * expr
 
 (* overall type is that of the next_expr *)
 and constructor_arg = ConstructorArg of type_expr * Field_name.t * expr

src/typing/core_lang/typed_ast.mli

@@ -22,6 +22,7 @@ type expr =
   | Consume     of loc * type_expr * expr  (** type is that of the expr being consumed *)
   | FinishAsync of loc * type_expr * expr * expr * expr
       (** overall type is that of the next_expr *)
+  | If          of loc * type_expr * expr * expr * expr
 
 and constructor_arg = ConstructorArg of type_expr * Field_name.t * expr
 

src/typing/data_race/type_async_expr.ml

@@ -104,6 +104,10 @@ let rec type_async_expr_helper class_defns trait_defns expr =
            constructor_args)
       >>| union_envs
   | Consume (_, _, expr) -> type_async_expr_with_defns expr
+  | If (_, _, cond_expr, then_expr, else_expr) ->
+      Result.all
+        (List.map ~f:type_async_expr_with_defns [cond_expr; then_expr; else_expr])
+      >>| union_envs
   | FinishAsync (loc, _, async_expr1, async_expr2, next_expr) ->
       type_async_expr_with_defns async_expr1
       >>= fun async_expr1_env ->

src/typing/data_race/type_linear_ownership.ml

@@ -105,6 +105,22 @@ let rec type_linear_ownership_helper class_defns trait_defns function_defns expr
       >>= fun () ->
       Result.ignore_m (type_linear_ownership_with_defns async_expr2)
       >>= fun () -> type_linear_ownership_with_defns next_expr
+  | If (_, _, cond_expr, then_expr, else_expr) ->
+      Result.ignore_m (type_linear_ownership_with_defns cond_expr)
+      (* this expression will be reduced to either the then_expr or else_expr value so we
+         don't care about the ownership of the bool expr *)
+      >>= fun () ->
+      type_linear_ownership_with_defns then_expr
+      >>= fun then_expr_ownership ->
+      type_linear_ownership_with_defns else_expr
+      >>| fun else_expr_ownership ->
+      (* we care if the returned type could be linear, so we'll be conservative and
+         propagate that type *)
+      if then_expr_ownership = LinearOwned || else_expr_ownership = LinearOwned then
+        LinearOwned
+      else if then_expr_ownership = LinearFree || else_expr_ownership = LinearFree then
+        LinearFree
+      else NonLinear
   | Let (loc, _, _, bound_expr) -> (
       type_linear_ownership_with_defns bound_expr
       >>= function

tests/alcotest/parsing/test_lexer.ml

@@ -29,7 +29,7 @@ let test_lex_tokens () =
     ; ("consume", CONSUME); ("finish", FINISH); ("async", ASYNC); ("class", CLASS)
     ; ("trait", TRAIT); ("require", REQUIRE); ("linear", LINEAR); ("thread", THREAD)
     ; ("read", READ); ("int", TYPE_INT); ("foo", ID "foo"); ("bool", TYPE_BOOL)
-    ; ("false", FALSE); ("true", TRUE) ]
+    ; ("false", FALSE); ("true", TRUE); ("if", IF); ("then", THEN); ("else", ELSE) ]
 
 let test_lex_int =
   QCheck.Test.make ~count:100 ~name:"Lex integers"

tests/expect/parsing/bad_expressions_not_terminated.ml

@@ -43,3 +43,12 @@ let%expect_test "Trait defn not terminated" =
     end
   " ;
   [%expect {| Line:11 Position:8: syntax error |}]
+
+let%expect_test "If Statement with no else branch" =
+  print_parsed_ast " 
+    if true {
+      3
+    }
+  " ;
+  [%expect {|
+    Line:5 Position:3: syntax error |}]

tests/expect/parsing/good_conditional_expr.ml

@@ -0,0 +1,46 @@
+open Core
+open Print_parsed_ast
+
+let%expect_test "Good if statement" =
+  print_parsed_ast
+    " 
+   {
+     let x = true;
+     if x {
+       0
+     }
+     else {
+       1
+     }
+   }
+  " ;
+  [%expect
+    {|
+      Program
+      └──Expr: Block
+         └──Expr: Let var: x
+            └──Expr: Bool:true
+         └──Expr: If
+            └──Expr: Variable: x
+            └──Expr: Block
+               └──Expr: Int:0
+            └──Expr: Block
+               └──Expr: Int:1 |}]
+
+let%expect_test "Good if then statement" =
+  print_parsed_ast " 
+   {
+     let x = true;
+     if x then 0 else 1
+   }
+  " ;
+  [%expect
+    {|
+      Program
+      └──Expr: Block
+         └──Expr: Let var: x
+            └──Expr: Bool:true
+         └──Expr: If
+            └──Expr: Variable: x
+            └──Expr: Int:0
+            └──Expr: Int:1 |}]

tests/expect/typing_core_lang/bad_conditional_expr.ml

@@ -0,0 +1,34 @@
+open Core
+open Print_typed_ast
+
+let%expect_test "If statement with non-boolean condition" =
+  print_typed_ast
+    " 
+   {
+     if 1 { (* 1 is not a boolean value *)
+       0
+     }
+     else {
+       1
+     }
+   }
+  " ;
+  [%expect
+    {|
+      Line:3 Position:6 Type error - If statement condition expression should have boolean type but instead has type Int |}]
+
+let%expect_test "If statement then and else branches' types are different " =
+  print_typed_ast
+    " 
+   {
+     if true { 
+       0
+     }
+     else {
+       false
+     }
+   }
+  " ;
+  [%expect
+    {|
+      Line:3 Position:6 Type error - If statement branches' types' not consistent - then branch has type Int but else branch has type Bool |}]

tests/expect/typing_core_lang/good_conditional_expr.ml

@@ -0,0 +1,34 @@
+open Core
+open Print_typed_ast
+
+let%expect_test "Good if statement" =
+  print_typed_ast
+    " 
+   {
+     let x = true;
+     if x {
+       0
+     }
+     else {
+       1
+     }
+   }
+  " ;
+  [%expect
+    {|
+      Program
+      └──Expr: Block
+         └──Type expr: Int
+         └──Expr: Let var: x
+            └──Type expr: Bool
+            └──Expr: Bool:true
+         └──Expr: Finish_async
+            └──Type expr: Int
+            └──Expr: Variable: x
+               └──Type expr: Bool
+            └──Expr: Block
+               └──Type expr: Int
+               └──Expr: Int:0
+            └──Expr: Block
+               └──Type expr: Int
+               └──Expr: Int:1 |}]

tests/expect/typing_data_race/bad_linear_aliasing.ml

@@ -82,3 +82,41 @@ let%expect_test "Alias a linear variable in a method" =
   " ;
   [%expect {|
     Line:7 Position:7 Potential data race: aliasing a linear reference |}]
+
+let%expect_test "Alias a linear variable in then branch of if statement" =
+  print_data_race
+    " 
+    class Foo = linear Bar {
+      var f : int
+    }
+    linear trait Bar {
+      require var f : int
+    }
+    {
+      let x = new Foo(); 
+      let z = true;
+      let y = if z then x else  new Foo(); (* cannot alias linear reference in any branch *)
+      x
+    }
+  " ;
+  [%expect {|
+    Line:11 Position:7 Potential data race: aliasing a linear reference |}]
+
+let%expect_test "Alias a linear variable in else branch of if statement" =
+  print_data_race
+    " 
+    class Foo = linear Bar {
+      var f : int
+    }
+    linear trait Bar {
+      require var f : int
+    }
+    {
+      let x = new Foo(); 
+      let z = true;
+      let y = if z then new Foo() else x; (* cannot alias linear reference in any branch *)
+      x
+    }
+  " ;
+  [%expect {|
+    Line:11 Position:7 Potential data race: aliasing a linear reference |}]

tests/expect/typing_data_race/good_consume_variable.ml

@@ -30,7 +30,7 @@ let%expect_test "Consume variable" =
     {
       {
         let x = new Foo(f:4, g:5, h:6);
-        let y = consume x; (* Consume linear variable *)
+        let y = if true then new Foo(f:1, g:2, h:3) else consume x; (* Consume linear variable *)
         let z = 5;
         let w = consume z; (* Can consume an int *)
         y.h

tests/expect/typing_data_race/good_independent_threads.ml

@@ -44,8 +44,13 @@ let%expect_test "Consume variable" =
       let x = new Choco(f:5); 
       finish {
         async {
-            f(h());
-            g(true)
+          if g(true){
+            f(h())
+          }
+          else{
+            4
+          }
+
         }
         async{
           let y = new Choco(f:5); 
@@ -54,7 +59,7 @@ let%expect_test "Consume variable" =
           w.f := w.id(4)
         }
         };
-        x
+        let y = x
     }
   " ;
   [%expect {| |}]