package elpi
Library
Module
Module type
Parameter
Class
Class type
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_goalstype ('builder, 'matcher, 'self) constructor_arguments = | N : ('self, Data.solution -> Data.custom_state * Data.term * extra_goals, 'self) constructor_arguments| A : 'a data * ('b, 'm, 'self) constructor_arguments -> ('a -> 'b, 'a -> 'm, 'self) constructor_arguments| S : ('b, 'm, 'self) constructor_arguments -> ('self -> 'b, 'self -> 'm, 'self) constructor_arguments
type 't constructor = | K : name * doc * ('build_t, 'matched_t, 't) constructor_arguments * 'build_t * ('matched_t, 't) match_t -> 't constructor