Module `Extraction_plugin.Mlutil`Source

Sourceval reset_meta_count : unit -> unit

Sourceval new_meta : 'a -> Miniml.ml_type

Sourceval type_subst_list : Miniml.ml_type list -> Miniml.ml_type -> Miniml.ml_type

Sourceval type_subst_vect : Miniml.ml_type array -> Miniml.ml_type -> Miniml.ml_type

Sourceval instantiation : Miniml.ml_schema -> Miniml.ml_type

Sourceval needs_magic : (Miniml.ml_type * Miniml.ml_type) -> bool

Sourceval put_magic_if : bool -> Miniml.ml_ast -> Miniml.ml_ast

val put_magic : 
  (Miniml.ml_type * Miniml.ml_type) ->
  Miniml.ml_ast ->
  Miniml.ml_ast

Sourceval generalizable : Miniml.ml_ast -> bool

Sourcemodule Mlenv : sig ... end

Sourceval type_mem_kn : Names.MutInd.t -> Miniml.ml_type -> bool

Sourceval type_maxvar : Miniml.ml_type -> int

Sourceval type_decomp : Miniml.ml_type -> Miniml.ml_type list * Miniml.ml_type

Sourceval type_recomp : (Miniml.ml_type list * Miniml.ml_type) -> Miniml.ml_type

Sourceval var2var' : Miniml.ml_type -> Miniml.ml_type

Sourcetype abbrev_map = Names.GlobRef.t -> Miniml.ml_type option

Sourceval type_expand : abbrev_map -> Miniml.ml_type -> Miniml.ml_type

Sourceval type_simpl : Miniml.ml_type -> Miniml.ml_type

Sourceval type_to_sign : abbrev_map -> Miniml.ml_type -> Miniml.sign

Sourceval type_to_signature : abbrev_map -> Miniml.ml_type -> Miniml.signature

Sourceval type_expunge : abbrev_map -> Miniml.ml_type -> Miniml.ml_type

Source

val type_expunge_from_sign : 
  abbrev_map ->
  Miniml.signature ->
  Miniml.ml_type ->
  Miniml.ml_type

Sourceval eq_ml_type : Miniml.ml_type -> Miniml.ml_type -> bool

Sourceval isTdummy : Miniml.ml_type -> bool

Sourceval isMLdummy : Miniml.ml_ast -> bool

Sourceval isKill : Miniml.sign -> bool

Source

val case_expunge : 
  Miniml.signature ->
  Miniml.ml_ast ->
  Miniml.ml_ident list * Miniml.ml_ast

Source

val term_expunge : 
  Miniml.signature ->
  (Miniml.ml_ident list * Miniml.ml_ast) ->
  Miniml.ml_ast

Sourceval anonymous_name : Names.Id.t

Sourceval dummy_name : Names.Id.t

Sourceval id_of_name : Names.Name.t -> Names.Id.t

Sourceval id_of_mlid : Miniml.ml_ident -> Names.Id.t

Sourceval tmp_id : Miniml.ml_ident -> Miniml.ml_ident

Sourceval collect_lams : Miniml.ml_ast -> Miniml.ml_ident list * Miniml.ml_ast

Source

val collect_n_lams : 
  int ->
  Miniml.ml_ast ->
  Miniml.ml_ident list * Miniml.ml_ast

Sourceval remove_n_lams : int -> Miniml.ml_ast -> Miniml.ml_ast

Sourceval nb_lams : Miniml.ml_ast -> int

Sourceval named_lams : Miniml.ml_ident list -> Miniml.ml_ast -> Miniml.ml_ast

Sourceval dummy_lams : Miniml.ml_ast -> int -> Miniml.ml_ast

Sourceval anonym_or_dummy_lams : Miniml.ml_ast -> Miniml.signature -> Miniml.ml_ast

Sourceval eta_args_sign : int -> Miniml.signature -> Miniml.ml_ast list

Sourceval mlapp : Miniml.ml_ast -> Miniml.ml_ast list -> Miniml.ml_ast

Source

val ast_map : 
  (Miniml.ml_ast -> Miniml.ml_ast) ->
  Miniml.ml_ast ->
  Miniml.ml_ast

Source

val ast_map_lift : 
  (int -> Miniml.ml_ast -> Miniml.ml_ast) ->
  int ->
  Miniml.ml_ast ->
  Miniml.ml_ast

Sourceval ast_iter : (Miniml.ml_ast -> unit) -> Miniml.ml_ast -> unit

Sourceval ast_occurs : int -> Miniml.ml_ast -> bool

Sourceval ast_occurs_itvl : int -> int -> Miniml.ml_ast -> bool

Sourceval ast_lift : int -> Miniml.ml_ast -> Miniml.ml_ast

Sourceval ast_pop : Miniml.ml_ast -> Miniml.ml_ast

Sourceval ast_subst : Miniml.ml_ast -> Miniml.ml_ast -> Miniml.ml_ast

Source

val ast_glob_subst : 
  Miniml.ml_ast Table.Refmap'.t ->
  Miniml.ml_ast ->
  Miniml.ml_ast

Sourceval dump_unused_vars : Miniml.ml_ast -> Miniml.ml_ast

Sourceval normalize : Miniml.ml_ast -> Miniml.ml_ast

Sourceval optimize_fix : Miniml.ml_ast -> Miniml.ml_ast

Sourceval inline : Names.GlobRef.t -> Miniml.ml_ast -> bool

Sourceval is_basic_pattern : Miniml.ml_pattern -> bool

Sourceval has_deep_pattern : Miniml.ml_branch array -> bool

Sourceval is_regular_match : Miniml.ml_branch array -> bool

Sourceexception Impossible

Sourcetype sign_kind =

| EmptySig
| NonLogicalSig
| SafeLogicalSig
| UnsafeLogicalSig

Sourceval sign_kind : Miniml.signature -> sign_kind

Sourceval sign_no_final_keeps : Miniml.signature -> Miniml.signature

Install

Dune Dependency

Authors

Maintainers

Sources

doc/extraction_plugin/Extraction_plugin/Mlutil/index.html

Module `Extraction_plugin.Mlutil`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/extraction_plugin/Extraction_plugin/Mlutil/index.html

Module Extraction_plugin.MlutilSource

Module `Extraction_plugin.Mlutil`Source