Remove some asserts which are now useless

AeneasVerif · Dec 21, 2023 · d9f91cf · d9f91cf
1 parent 435fe4c
commit d9f91cf
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 8 deletions.
diff --git 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
@@ -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
@@ -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