diff options
| author | Son Ho | 2023-12-21 15:25:06 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-21 15:25:06 +0100 |
| commit | d9f91cfcd538525f024c6019d7c8250dda8d76fd (patch) | |
| tree | 511db3d6ab5036f0de1b665ff22923d9a068f41a | |
| parent | 435fe4cf63869448e2b25486b564ede9efa9a34b (diff) | |
Remove some asserts which are now useless
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 4 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 3 | ||||
| -rw-r--r-- | 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 |