diff options
| author | Pierre-Marie Pédrot | 2018-11-05 15:18:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-20 16:12:15 +0100 |
| commit | a181bcb8d8050984e57f4a21cc7e97c043feb043 (patch) | |
| tree | 707f2516e87102ca44912524cba5b15201ae3fd0 | |
| parent | c4ec9bd2c8a31f5eddea87bbc3f1605ca731d598 (diff) | |
Add a check that the return stack of an FProd is indeed empty.
| -rw-r--r-- | kernel/typeops.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index a87355e927..c9acd168e8 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -151,6 +151,11 @@ let type_of_abstraction _env name var ty = let make_judgev c t = Array.map2 make_judge c t +let rec check_empty_stack = function +| [] -> true +| CClosure.Zupdate _ :: s -> check_empty_stack s +| _ -> false + let type_of_apply env func funt argsv argstv = let open CClosure in let len = Array.length argsv in @@ -159,7 +164,9 @@ let type_of_apply env func funt argsv argstv = let rec apply_rec i typ = if Int.equal i len then term_of_fconstr typ else - let typ, _ = whd_stack infos tab typ [] in + let typ, stk = whd_stack infos tab typ [] in + (** The return stack is known to be empty *) + let () = assert (check_empty_stack stk) in match fterm_of typ with | FProd (_, c1, c2, e) -> let arg = argsv.(i) in |