diff options
| author |  Benjamin Gregoire <Benjamin.Gregoire@inria.fr> | 2015-03-26 19:00:00 +0100 |
|---|---|---|
| committer | Benjamin Gregoire <Benjamin.Gregoire@inria.fr> | 2015-03-26 19:00:00 +0100 |
| commit | 00894adf6fc11f4336a3ece0c347676bbf0b4c11 (patch) | |
| tree | a3d46465df90fac47629a483f6cd75be40d9656e /kernel/cbytegen.ml | |
| parent | f920ae56ffacf80f85dcf33d3f1ccf0acb4375b1 (diff) | |
allows the vm to deal with inductive type with 8388607 constant constructors and 8388851 non-constant constructor.
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 13 |
1 files changed, 10 insertions, 3 deletions
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 |