Module `BuiltInPredicate.ADT`Source

Sourcetype ('match_stateful_t, 'match_t, 't) match_t =

| M of ok:'match_t -> ko:(unit -> term) -> 't -> term
| MS of ok:'match_stateful_t -> ko:(State.t -> State.t * term * Conversion.extra_goals) -> 't -> State.t -> State.t * term * Conversion.extra_goals

Sourcetype ('build_stateful_t, 'build_t) build_t =

| B of 'build_t
| BS of 'build_stateful_t

type ('stateful_builder, 'builder, 'stateful_matcher, 'matcher, 'self, 'hyps, 'constraints)
  constructor_arguments =

| N : (State.t -> State.t * 'self, 'self, State.t -> State.t * term * Conversion.extra_goals, term, 'self, 'hyps, 'constraints) constructor_arguments
| A : 'a Conversion.t * ('bs, 'b, 'ms, 'm, 'self, 'hyps, 'constraints) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, 'self, 'hyps, 'constraints) constructor_arguments
| CA : ('a, 'hyps, 'constraints) ContextualConversion.t * ('bs, 'b, 'ms, 'm, 'self, 'hyps, 'constraints) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, 'self, 'hyps, 'constraints) constructor_arguments
| S : ('bs, 'b, 'ms, 'm, 'self, 'hyps, 'constraints) constructor_arguments -> ('self -> 'bs, 'self -> 'b, 'self -> 'ms, 'self -> 'm, 'self, 'hyps, 'constraints) constructor_arguments
| C : (('self, 'hyps, 'constraints) ContextualConversion.t -> ('a, 'hyps, 'constraints) ContextualConversion.t) * ('bs, 'b, 'ms, 'm, 'self, 'hyps, 'constraints) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, 'self, 'hyps, 'constraints) constructor_arguments

Sourcetype ('t, 'h, 'c) constructor =

| K : name * doc * ('build_stateful_t, 'build_t, 'match_stateful_t, 'match_t, 't, 'h, 'c) constructor_arguments * ('build_stateful_t, 'build_t) build_t * ('match_stateful_t, 'match_t, 't) match_t -> ('t, 'h, 'c) constructor

Sourcetype ('t, 'h, 'c) declaration = {

ty : Conversion.ty_ast;
doc : doc;
pp : Format.formatter -> 't -> unit;
constructors : ('t, 'h, 'c) constructor list;

}

Sourcetype ('b, 'm, 't, 'h, 'c) compiled_constructor_arguments =

| XN : (State.t -> State.t * 't, State.t -> State.t * term * Conversion.extra_goals, 't, 'h, 'c) compiled_constructor_arguments
| XA : ('a, 'h, 'c) ContextualConversion.t * ('b, 'm, 't, 'h, 'c) compiled_constructor_arguments -> ('a -> 'b, 'a -> 'm, 't, 'h, 'c) compiled_constructor_arguments

Source

type ('match_t, 't) compiled_match_t =
  ok:'match_t ->
  ko:(State.t -> State.t * term * Conversion.extra_goals) ->
  't ->
  State.t ->
  State.t * term * Conversion.extra_goals

Sourcetype ('t, 'h, 'c) compiled_constructor =

| XK : ('build_t, 'matched_t, 't, 'h, 'c) compiled_constructor_arguments * 'build_t * ('matched_t, 't) compiled_match_t -> ('t, 'h, 'c) compiled_constructor

Source

type ('t, 'h, 'c) compiled_adt =
  ('t, 'h, 'c) compiled_constructor Elpi_util.Util.Constants.Map.t

Source

val buildk : 
  mkConst:(Elpi_util.Util.constant -> term) ->
  Elpi_util.Util.constant ->
  term list ->
  term

Source

val readback_args : 
  'a 'm 't 'h 'c. look:(depth:int -> term -> term) ->
  Conversion.ty_ast ->
  depth:int ->
  'h ->
  'c ->
  State.t ->
  Conversion.extra_goals list ->
  term ->
  ('a, 'm, 't, 'h, 'c) compiled_constructor_arguments ->
  'a ->
  term list ->
  State.t * 't * Conversion.extra_goals

Source

val readback : 
  't 'h 'c. mkinterval:(int -> int -> int -> term list) ->
  look:(depth:int -> term -> term) ->
  alloc:(?name:string -> State.t -> State.t * 'uk) ->
  mkUnifVar:('uk -> args:term list -> State.t -> term) ->
  Conversion.ty_ast ->
  ('t, 'h, 'c) compiled_adt ->
  depth:int ->
  'h ->
  'c ->
  State.t ->
  term ->
  State.t * 't * Conversion.extra_goals

Source

val adt_embed_args : 
  'm 'a 't 'h 'c. mkConst:(int -> term) ->
  Conversion.ty_ast ->
  ('t, 'h, 'c) compiled_adt ->
  Elpi_util.Util.constant ->
  depth:int ->
  'h ->
  'c ->
  ('a, 'm, 't, 'h, 'c) compiled_constructor_arguments ->
  (State.t -> State.t * term * Conversion.extra_goals) list ->
  'm

Source

val embed : 
  'a 'h 'c. mkConst:(int -> term) ->
  Conversion.ty_ast ->
  (Format.formatter -> 'a -> unit) ->
  ('a, 'h, 'c) compiled_adt ->
  depth:int ->
  'h ->
  'c ->
  State.t ->
  'a ->
  State.t * term * Conversion.extra_goals

Source

val compile_arguments : 
  'b 'bs 'm 'ms 't 'h 'c. ('bs, 'b, 'ms, 'm, 't, 'h, 'c) constructor_arguments ->
  ('t, 'h, 'c) ContextualConversion.t ->
  ('bs, 'ms, 't, 'h, 'c) compiled_constructor_arguments

Source

val compile_builder_aux : 
  'bs 'b 'm 'ms 't 'h 'c. ('bs, 'b, 'ms, 'm, 't, 'h, 'c) constructor_arguments ->
  'b ->
  'bs

Source

val compile_builder : 
  'bs 'b 'm 'ms 't 'h 'c. ('bs, 'b, 'ms, 'm, 't, 'h, 'c) constructor_arguments ->
  ('bs, 'b) build_t ->
  'bs

Source

val compile_matcher_ok : 
  'bs 'b 'm 'ms 't 'h 'c. ('bs, 'b, 'ms, 'm, 't, 'h, 'c) constructor_arguments ->
  'ms ->
  Conversion.extra_goals ref ->
  State.t ref ->
  'm

Sourceval compile_matcher_ko : ('a -> 'a * 'b * 'c) -> 'c ref -> 'a ref -> unit -> 'b

Source

val compile_matcher : 
  'bs 'b 'm 'ms 't 'h 'c. ('bs, 'b, 'ms, 'm, 't, 'h, 'c) constructor_arguments ->
  ('ms, 'm, 't) match_t ->
  ('ms, 't) compiled_match_t

Source

val tyargs_of_args : 
  'a 'b 'c 'd 'e. string ->
  ('a, 'b, 'c, 'd, 'e) compiled_constructor_arguments ->
  (bool * string * string) list

Source

val compile_constructors : 
  Conversion.ty_ast ->
  ('a, 'b, 'c) ContextualConversion.t ->
  string ->
  ('a, 'b, 'c) constructor list ->
  ('a, 'b, 'c) compiled_constructor Elpi_util.Util.Constants.Map.t
  * (bool * string * string) list Elpi_util.Util.StrMap.t

Source

val document_constructor : 
  Fmt.formatter ->
  string ->
  string ->
  (bool * string * string) list ->
  unit

Sourceval document_kind : Fmt.formatter -> Conversion.ty_ast -> unit

Source

val document_adt : 
  string ->
  Conversion.ty_ast ->
  ('a, 'b, 'c) constructor list ->
  (bool * string * string) list Elpi_util.Util.StrMap.t ->
  Fmt.formatter ->
  unit ->
  unit

Source

val adt : 
  mkinterval:(int -> int -> int -> term list) ->
  look:(depth:int -> term -> term) ->
  mkConst:(int -> term) ->
  alloc:(?name:string -> State.t -> State.t * 'a) ->
  mkUnifVar:('a -> args:term list -> State.t -> term) ->
  ('b, 'c, 'd) declaration ->
  ('b, 'c, 'd) ContextualConversion.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/elpi.runtime/Elpi_runtime/Data/BuiltInPredicate/ADT/index.html

Module `BuiltInPredicate.ADT`Source

package elpi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/elpi.runtime/Elpi_runtime/Data/BuiltInPredicate/ADT/index.html

Module BuiltInPredicate.ADTSource

Module `BuiltInPredicate.ADT`Source