From 00894adf6fc11f4336a3ece0c347676bbf0b4c11 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Thu, 26 Mar 2015 19:00:00 +0100 Subject: allows the vm to deal with inductive type with 8388607 constant constructors and 8388851 non-constant constructor. --- kernel/cbytegen.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'kernel/cbytegen.ml') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 95ce2da34..0cd250113 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -335,8 +335,16 @@ let init_fun_code () = fun_code := [] exception TooLargeInductive of Id.t +let max_nb_const = 0x7FFFFF +let max_nb_block = 0x7FFFFF + max_tag - 1 + +let str_max_constructors = + Format.sprintf + " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block + let check_compilable ib = - if not (ib.mind_nb_args <= 0xFFFF && ib.mind_nb_constant <= 0xFFFF) then + + if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then raise (TooLargeInductive ib.mind_typename) (* Inv: arity > 0 *) @@ -778,8 +786,7 @@ let compile fail_on_error env c = let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ - Id.print tname ++ str - " which has more than 65535 constant constructors or more than 65535 non-constant constructors")); + Id.print tname ++ str str_max_constructors)); None) let compile_constant_body fail_on_error env = function -- cgit v1.2.3