From d9f91cfcd538525f024c6019d7c8250dda8d76fd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Dec 2023 15:25:06 +0100
Subject: Remove some asserts which are now useless

---
 compiler/Extract.ml         | 4 ----
 compiler/PureMicroPasses.ml | 3 ---
 compiler/PureUtils.ml       | 5 ++++-
 3 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 46cf8c4a..8d35f039 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1475,8 +1475,6 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
        *)
       let inputs_lvs =
         let all_inputs = (Option.get def.body).inputs_lvs in
-        (* TODO: *)
-        assert (not !Config.return_back_funs);
         let num_fwd_inputs =
           def.signature.fwd_info.fwd_info.num_inputs_with_fuel_with_state
         in
@@ -1523,8 +1521,6 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   if has_decreases_clause && !backend = Lean then (
     let def_body = Option.get def.body in
     let all_vars = List.map (fun (v : var) -> v.id) def_body.inputs in
-    (* TODO: *)
-    assert (not !Config.return_back_funs);
     let num_fwd_inputs =
       def.signature.fwd_info.fwd_info.num_inputs_with_fuel_with_state
     in
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 34597d32..63436e7d 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1337,9 +1337,6 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
             let fwd_info = fun_sig.fwd_info in
             let fwd_effect_info = fwd_info.effect_info in
 
-            (* TODO: *)
-            assert (not !Config.return_back_funs);
-
             (* Generate the loop definition *)
             let loop_fwd_effect_info = fwd_effect_info in
 
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 6579e84c..d4aaba16 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -332,7 +332,10 @@ let mk_app (app : texpression) (arg : texpression) : texpression =
   match app.ty with
   | TArrow (ty0, ty1) ->
       (* Sanity check *)
-      if ty0 <> arg.ty then raise_or_return "App: wrong input type"
+      if
+        (* TODO: we need to normalize the types *)
+        !Config.type_check_pure_code && ty0 <> arg.ty
+      then raise_or_return "App: wrong input type"
       else
         let e = App (app, arg) in
         let ty = ty1 in
-- 
cgit v1.2.3