package elpi

  1. Overview
  2. Docs

Commodity API for representing simple ADT: no binders! * * Example of: pred getenv i:string, o:option string. * * (* define the ADT for "option a" *) * let option_adt a = * ty = TyApp("option",a.ty,[]); * doc = "The option type (aka Maybe)"; * constructors = [ * * K("none","nothing in this case", * N, (* no arguments *) * None, (* builder *) * (fun ~ok ~ko -> function None -> ok | _ -> ko)); (* matcher *) * K("some","something in this case", * A(a,N), (* one argument of type a *) * (fun x -> Some x), (* builder *) * (fun ~ok ~ko -> function Some x -> ok x | _ -> ko)); (* matcher *) * ] * * (* compile the ADT to data types to be used in predicate signatures *) * let option a : a data = adt (option_adt a) * * (* define a predicate using "option" *) * let getenv : t = * Pred("getenv", * In(string, "VarName", * Out(option string, "Value", * Easy "Like Sys.getenv")), * (fun name _ ~depth -> * try !: (Some (Sys.getenv name)) * with Not_found -> !: None)) *

type ('matched, 't) match_t = ok:'matched -> ko:(Data.solution -> Data.custom_state * Data.term * extra_goals) -> 't -> Data.solution -> Data.custom_state * Data.term * extra_goals
type ('builder, 'matcher, 'self) constructor_arguments =
  1. | N : ('self, Data.solution -> Data.custom_state * Data.term * extra_goals, 'self) constructor_arguments
  2. | A : 'a data * ('b, 'm, 'self) constructor_arguments -> ('a -> 'b, 'a -> 'm, 'self) constructor_arguments
  3. | S : ('b, 'm, 'self) constructor_arguments -> ('self -> 'b, 'self -> 'm, 'self) constructor_arguments
type 't constructor =
  1. | K : name * doc * ('build_t, 'matched_t, 't) constructor_arguments * 'build_t * ('matched_t, 't) match_t -> 't constructor
type 't adt = {
  1. ty : ty_ast;
  2. doc : doc;
  3. constructors : 't constructor list;
}