package libsail

  1. Overview
  2. Docs

Rewrites for removing polymorphism from specifications

val opt_ddump_spec_ast : (string * int) option ref
type specialization
val typ_ord_specialization : specialization

Only specialize Type- and Ord- kinded polymorphism.

val int_specialization : specialization

(experimental) specialise Int-kinded definitions

val int_specialization_with_externs : specialization

(experimental) specialise Int-kinded definitions, including externs

val polymorphic_functions : specialization -> 'a Ast.def list -> Ast_util.IdSet.t

Returns an IdSet with the function ids that have X-kinded parameters, e.g. val f : forall ('a : X). 'a -> 'a. The first argument specifies what X should be - it should be one of: is_int_kopt, is_order_kopt, or is_typ_kopt from Ast_util, or some combination of those.

val add_initial_calls : Ast_util.IdSet.t -> unit
val get_initial_calls : unit -> Ast.id list

specialize returns an AST with all the Order and Type polymorphism removed, as well as the environment produced by type checking that AST with Type_check.initial_env. The env parameter is the environment to return if there is no polymorphism to remove, in which case specialize returns the AST unmodified.

specialize' n performs at most n specialization passes. Useful for int_specialization which is not guaranteed to terminate.

return all instantiations of a function id, with the instantiations filtered according to the specialization.

val string_of_instantiation : Ast.typ_arg Ast_util.KBindings.t -> string
OCaml

Innovation. Community. Security.