Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Pp
type error = | TooLargeInductive of Names.Id.t | TooLargeCode
exception CompileError of error
let too_large_code () = raise (CompileError TooLargeCode)
(* Limit needed to make SWITCH work. The specific limit is arbitrary but nobody needs more than 0x1000000 constructors. *)
let max_nb_const = 0x1000000let max_nb_block = 0x1000000 + Obj.last_non_constant_constructor_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
(* NB: Declarations depends on Vmemitcodes which depends on too_large_code so we can't use Declarations.one_inductive_body here. Instead we pass the needed fields. *)let check_compilable_ind ~name ~mind_nb_args ~mind_nb_constant = if not (mind_nb_args <= max_nb_block && mind_nb_constant <= max_nb_const) then raise (CompileError (TooLargeInductive name))
let pr_error = function | TooLargeCode -> str "Cannot compile code for virtual machine as it exceeds string size limits." | TooLargeInductive name -> str "Cannot compile code for virtual machine as it uses inductive " ++ Names.Id.print name ++ str str_max_constructors
let () = CErrors.register_handler (function | CompileError e -> Some (pr_error e) | _ -> None)