libsail 0.15 · OCaml Package

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

val specialize : 
  specialization ->
  Type_check.Env.t ->
  Type_check.tannot Ast_defs.ast ->
  Effects.side_effect_info ->
  Type_check.tannot Ast_defs.ast * Type_check.Env.t * Effects.side_effect_info

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.

val specialize_passes : 
  int ->
  specialization ->
  Type_check.Env.t ->
  Type_check.tannot Ast_defs.ast ->
  Effects.side_effect_info ->
  Type_check.tannot Ast_defs.ast * Type_check.Env.t * Effects.side_effect_info

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

val instantiations_of : 
  specialization ->
  Ast.id ->
  Type_check.tannot Ast_defs.ast ->
  Ast.typ_arg Ast_util.KBindings.t list

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

package libsail