Support assertion

lib/back/closure_translator.ml

@@ -52,6 +52,8 @@ let ff_is_equal_aux = C.VARIABLE "ff_is_equal_aux"
 
 let ff_is_zero = C.VARIABLE "ff_is_zero"
 
+let ff_assert = C.VARIABLE "ff_assert"
+
 let ff_is_not_equal = C.VARIABLE "ff_is_not_equal"
 
 let ff_get_mem = C.VARIABLE "ff_get_member"
@@ -72,9 +74,11 @@ let ff_match_constr = C.VARIABLE "ff_match_constr"
 
 let ff_match_tuple = C.VARIABLE "ff_match_tuple"
 
-let header = {|
-#include"fun_rt.hpp"
-#include<stdio.h>
+let header =
+  {|
+#include "fun_rt.hpp"
+#include <stdio.h>
+#include <stdexcept>
 
 |}
 
@@ -332,6 +336,14 @@ and trans_expr ctx e =
       let _e0_v, e0_stmts = trans_expr ctx e0 in
       let e1_v, e1_stmts = trans_expr ctx e1 in
       (e1_v, e0_stmts @ e1_stmts)
+  | EAssert e0 ->
+      let e0_v, e0_stmts = trans_expr ctx e0 in
+      let is_true_v = create_decl "is_true" ctx in
+      let assert_stmt =
+        make_assign (VARIABLE is_true_v)
+          (CALL (ff_assert, [ VARIABLE e0_v ]))
+      in
+      (is_true_v, e0_stmts @ [ assert_stmt ])
   | EStruct _ -> ("todo", [])
 
 and trans_const (c : S.constant) =
@@ -515,11 +527,20 @@ let translate (main, (fns : func list)) =
   Cprint1.print buf fn_defs;
   let prog = Buffer.contents buf in
   let driver =
-    Printf.sprintf {|
+    Printf.sprintf
+      {|
 int main()
 {
-  %s(nullptr);
+  try
+  {
+    %s(nullptr);
+  }
+  catch (const std::runtime_error& error)
+  {
+    printf("Runtime error: %%s", error.what());
+  }
 }
-|} main_name
+|}
+      main_name
   in
   header ^ prog ^ driver

lib/clos/closure.ml

@@ -24,6 +24,7 @@ type expr =
   | EField of expr * string
   | ECmp of T.cmp_op * expr * expr
   | ESeq of expr * expr
+  | EAssert of expr
 
 and pattern = L.pattern
 

lib/clos/lift.ml

@@ -87,6 +87,9 @@ let rec lift ?(hint = "temp") (e : L.expr) (vars : string list) :
   | L.EField (e, name) ->
       let e', fns = lift e vars ~hint in
       (C.EField (e', name), fns)
+  | L.EAssert e ->
+      let e', fns = lift e vars ~hint in
+      (C.EAssert e', fns)
 
 and lift_letrec binds vars =
   let xs = List.map fst binds in

lib/lam/compile.ml

@@ -24,6 +24,7 @@ let rec compile_expr (e : T.expr) =
   | T.EFieldCons (_, _, id, _) -> L.ECons id
   | T.ECmp (op, e1, e2, _) -> L.ECmp (op, compile_expr e1, compile_expr e2)
   | T.ESeq (e0, e1, _) -> L.ESeq (compile_expr e0, compile_expr e1)
+  | T.EAssert (e, _) -> L.EAssert (compile_expr e)
 
 and compile_lam (x, e, _) = ([ x ], compile_expr e, ref [])
 
@@ -141,6 +142,7 @@ let rec fva_expr e vars =
       let fvs_in_binds = fva_letrec binds vars in
       capture fvs_in_binds xs @ capture (fva_expr e (xs @ vars)) xs
   | L.EField (e, _) -> fva_expr e vars
+  | L.EAssert e -> fva_expr e vars
 
 and fva_lambda x e vars =
   let vars = x @ vars in

lib/lam/tree.ml

@@ -21,6 +21,7 @@ type expr =
   | EField of expr * string
   | ECmp of T.cmp_op * expr * expr
   | ESeq of expr * expr
+  | EAssert of expr
 
 and pattern =
   | PVar of string

lib/syntax/lexer.mll

@@ -59,6 +59,7 @@ rule token = parse
     | "functor"         { FUNCTOR }
     | "fun"             { FUN }
     | "of"              { OF }
+    | "assert"          { ASSERT }
     | "->"              { ARROW }
     | "="               { EQ }
     | "<>"              { NEQ }

lib/syntax/parser.mly

@@ -53,6 +53,7 @@ let mk_type_ref fon t_args =
 %token LBRACE
 %token RBRACE
 %token SEMI
+%token ASSERT
 
 %nonassoc LET TYPE
 %nonassoc over_TOP
@@ -248,6 +249,7 @@ expr:
        }
     | e=bin_expr { e }
     | e=expr COLON te=type_expr { make_node (EAnn (e, te)) $startpos $endpos }
+    | ASSERT e=expr %prec over_TOP { make_node (EAssert e) $startpos $endpos }
     ;
 
 bin_expr:

lib/syntax/parsetree.ml

@@ -60,6 +60,7 @@ and expr_desc =
   | EFieldCons of mod_expr * string
   | ECmp of cmp_op * expr * expr
   | ESeq of expr * expr
+  | EAssert of expr
 
 and pattern =
   | PVal of constant

lib/typing/check.ml

@@ -50,6 +50,7 @@ let rec check_expr (e : T.expr) (env : Env.t) : expr =
     | T.EFieldCons (p, c) -> check_field_cons p c env
     | T.ECmp (op, e0, e1) -> check_cmp op e0 e1 env
     | T.ESeq (e0, e1) -> check_seq e0 e1 env
+    | T.EAssert e -> check_assert e env
   with
   | err -> Report.wrap_and_reraise err e.start_loc e.end_loc env
 
@@ -66,6 +67,11 @@ and check_var x env =
   let t = P.inst bind in
   EVar (x, t)
 
+and check_assert e env =
+  let e_typed = check_expr e env in
+  U.unify I.bool_ty (get_ty e_typed);
+  EAssert (e_typed, I.unit_ty)
+
 (* pattern will create bindings under context's type *)
 and check_pattern p te env : pattern * (string * I.ty) list =
   let check_PCons_aux (cons_ty : I.ty) (p (* payload pattern *) : T.pattern)

lib/typing/render.ml

@@ -149,6 +149,10 @@ module MakePP (Config : PPConfig) = struct
         Fmt.fprintf fmt " ;@\n";
         pp_expr fmt e1;
         Fmt.fprintf fmt "@]"
+    | EAssert (e, _te) ->
+        Fmt.fprintf fmt "@[assert ";
+        pp_expr fmt e;
+        Fmt.fprintf fmt "@]"
 
   and pp_lam fmt (x, e, _te) =
     Fmt.fprintf fmt "@[<v 2>fun %s -> @\n" x;

lib/typing/typedtree.ml

@@ -27,6 +27,7 @@ type expr =
       * ty
   | ECmp of T.cmp_op * expr * expr * ty
   | ESeq of expr * expr * ty
+  | EAssert of expr * ty
 
 and lambda_typed = string * expr * ty
 
@@ -76,7 +77,8 @@ let get_ty = function
   | ECons (_, _, ty)
   | EFieldCons (_, _, _, ty)
   | ECmp (_, _, _, ty)
-  | ESeq (_, _, ty) ->
+  | ESeq (_, _, ty)
+  | EAssert (_, ty) ->
       ty
 
 let rec get_mod_ty (me : mod_expr) =

runtime/include/fun_rt_core.hpp

@@ -185,4 +185,6 @@ ff_obj_t ff_is_not_equal(ff_obj_t x, ff_obj_t y);
 
 bool ff_is_zero(ff_obj_t x);
 
+ff_obj_t ff_assert(ff_obj_t x);
+
 #endif

runtime/src/fun_rt_core.cpp

@@ -5,6 +5,7 @@
 #include <cstdio>
 #include <cstring>
 #include <stddef.h>
+#include <stdexcept>
 #include <stdint.h>
 #include <stdio.h>
 #include <stdlib.h>
@@ -200,3 +201,11 @@ bool ff_is_zero(ff_obj_t x) {
     auto val = ff_get_int(x);
     return val == 0;
 }
+
+ff_obj_t ff_assert(ff_obj_t x) {
+    auto val = ff_get_int(x);
+    if (val != 0) {
+        throw std::runtime_error("Assertion failed!");
+    }
+    return ff_make_int(0);
+}

tests/cram/test_dirs/assert.t/run.t

@@ -0,0 +1,58 @@
+
+
+  $ ff test_assert.fun -o test_assert.cpp
+
+  $ cat test_assert.cpp
+
+  #include "fun_rt.hpp"
+  #include <stdio.h>
+  #include <stdexcept>
+
+  ff_obj_t main_1__fn(ff_fvs_t fvs_1);
+
+  ff_obj_t main_1__fn(ff_fvs_t fvs_1)
+  {
+  	ff_obj_t mod_12;
+  	ff_obj_t x_11;
+  	ff_obj_t is_true_10;
+  	ff_obj_t temp_9;
+  	ff_obj_t x_8;
+  	ff_obj_t temp_7;
+  	ff_obj_t app_res_6;
+  	ff_obj_t x_5;
+  	ff_obj_t is_true_4;
+  	ff_obj_t temp_3;
+  	ff_obj_t println_str_2;
+  	println_str_2 = ff_builtin_println_str;
+  	temp_3 = ff_make_int(1);
+  	is_true_4 = ff_assert(temp_3);
+  	x_5 = is_true_4;
+  	temp_7 = ff_make_str("A true asserted!");
+  	app_res_6 = ff_apply_generic(println_str_2, temp_7);
+  	x_8 = app_res_6;
+  	temp_9 = ff_make_int(0);
+  	is_true_10 = ff_assert(temp_9);
+  	x_11 = is_true_10;
+  	mod_12 = ff_make_mod_obj(4, {"println_str", "x", "x", "x"},
+  		{println_str_2, x_5, x_8, x_11});
+  	return mod_12;
+  }
+
+
+  int main()
+  {
+    try
+    {
+      main_1__fn(nullptr);
+    }
+    catch (const std::runtime_error& error)
+    {
+      printf("Runtime error: %s", error.what());
+    }
+  }
+
+  $ $FF test_assert.fun
+
+  $ ./test_assert.fun.out
+  Runtime error: Assertion failed!
+

tests/cram/test_dirs/assert.t/test_assert.fun

@@ -0,0 +1,7 @@
+external println_str : string -> unit = "ff_builtin_println_str"
+
+let x = assert true
+
+let x = println_str "A true asserted!"
+
+let x = assert false

tests/cram/test_dirs/equality.t/run.t

@@ -2,8 +2,9 @@
 
   $ cat test_equality.fun.cpp
 
-  #include"fun_rt.hpp"
-  #include<stdio.h>
+  #include "fun_rt.hpp"
+  #include <stdio.h>
+  #include <stdexcept>
 
   ff_obj_t main_1__fn(ff_fvs_t fvs_1);
 
@@ -84,7 +85,14 @@
 
   int main()
   {
-    main_1__fn(nullptr);
+    try
+    {
+      main_1__fn(nullptr);
+    }
+    catch (const std::runtime_error& error)
+    {
+      printf("Runtime error: %s", error.what());
+    }
   }
 
   $ ./test_equality.fun.out

tests/cram/test_dirs/external.t/run.t

@@ -1,8 +1,9 @@
 
   $ ff test_external.fun --stdout
 
-  #include"fun_rt.hpp"
-  #include<stdio.h>
+  #include "fun_rt.hpp"
+  #include <stdio.h>
+  #include <stdexcept>
 
   ff_obj_t main_1__fn(ff_fvs_t fvs_1);
 
@@ -18,16 +19,24 @@
 
   int main()
   {
-    main_1__fn(nullptr);
+    try
+    {
+      main_1__fn(nullptr);
+    }
+    catch (const std::runtime_error& error)
+    {
+      printf("Runtime error: %s", error.what());
+    }
   }
 
 
   $ $FF test_add_external.fun --stdout
 
   $ cat test_add_external.fun.cpp
 
-  #include"fun_rt.hpp"
-  #include<stdio.h>
+  #include "fun_rt.hpp"
+  #include <stdio.h>
+  #include <stdexcept>
 
   ff_obj_t main_1__fn(ff_fvs_t fvs_1);
 
@@ -60,7 +69,14 @@
 
   int main()
   {
-    main_1__fn(nullptr);
+    try
+    {
+      main_1__fn(nullptr);
+    }
+    catch (const std::runtime_error& error)
+    {
+      printf("Runtime error: %s", error.what());
+    }
   }
 
   $ ./test_add_external.fun.out

tests/cram/test_dirs/hello.t/run.t

@@ -7,8 +7,9 @@
 
   $ cat hello.fun.cpp
 
-  #include"fun_rt.hpp"
-  #include<stdio.h>
+  #include "fun_rt.hpp"
+  #include <stdio.h>
+  #include <stdexcept>
 
   ff_obj_t main_1__fn(ff_fvs_t fvs_1);
 
@@ -33,5 +34,12 @@
 
   int main()
   {
-    main_1__fn(nullptr);
+    try
+    {
+      main_1__fn(nullptr);
+    }
+    catch (const std::runtime_error& error)
+    {
+      printf("Runtime error: %s", error.what());
+    }
   }