278278 list or pair but not like int. So far there is no support for
279279 data with binder using this API. The type of each constructor is
280280 described using a GADT so that the code to build or match the data
281- can be given the right type. Example: define the ADT for "option a" {|
282-
281+ can be given the right type. Example: define the ADT for "option a"
282+ {[
283283 let option_declaration a = {
284284 ty = TyApp("option",a.ty,[]);
285285 doc = "The option type (aka Maybe)";
298298 ]
299299 }
300300
301- | }
301+ ] }
302302
303303 [K] stands for "constructor", [B] for "build", [M] for "match".
304304 Variants [BS] and [MS] give read/write access to the state.
@@ -327,7 +327,8 @@ module AlgebraicData : sig
327327 (* * GADT for describing the type of the constructor:
328328 - N is the terminator
329329 - A(a,...) is an argument of type a (a is a Conversion.t)
330- -
330+ - S stands for self
331+ - C stands for container
331332 *)
332333 type ('stateful_builder,'builder, 'stateful_matcher, 'matcher, 'self) constructor_arguments =
333334 (* No arguments *)
367368 * built-in (Elpi code with comments).
368369 *
369370 * Example: built-in "div" taking two int and returning their division and
370- * remainder. {|
371+ * remainder. {[
371372 *
372373 * Pred("div",
373374 * In(int, "N",
376377 * Out(int, "R",
377378 * Easy "division of N by M gives D with reminder R")))),
378379 * (fun n m _ _ -> !: (n div m) +! (n mod n)))
379- * | }
380+ * ] }
380381 *
381382 * In( type, documentation, ... ) declares an input of a given type.
382383 * In the example above both "n" and "m" are declare as input, and
508509 and extract the output from the solution found by Elpi.
509510
510511 Example: "foo data Output" where [data] has type [t] ([a] is [t Conversion.t])
511- and [Output] has type [v] ([b] is a [v Conversion.t]) can be described as: {|
512+ and [Output] has type [v] ([b] is a [v Conversion.t]) can be described as:
513+ {[
512514
513515 let q : (v * unit) t = Query {
514516 predicate = "foo";
@@ -517,16 +519,17 @@ end
517519 N))
518520 }
519521
520- | }
522+ ] }
521523
522524 Then [compile q] can be used to obtain the compiled query such that the
523- resulting solution has a fied output of type [(v * unit)]. Example: {|
525+ resulting solution has a fied output of type [(v * unit)]. Example:
526+ {[
524527
525528 Query.compile q |> Compile.link |> Execute.once |> function
526529 | Execute.Success { output } -> output
527530 | _ -> ...
528531
529- | } *)
532+ ] } *)
530533module Query : sig
531534
532535 type name = string
@@ -628,7 +631,8 @@ module FlexibleData : sig
628631 val show : t -> string
629632 end
630633
631- (* * Example from Hol-light + elpi: {|
634+ (* * Example from Hol-light + elpi:
635+ {[
632636
633637 module UV2STV = FlexibleData.Map(struct
634638 type t = int
@@ -662,7 +666,7 @@ module FlexibleData : sig
662666 ]
663667 }
664668
665- | }
669+ ] }
666670
667671 In this way an Elpi term containig a variable [X] twice gets read back
668672 using [Stv i] for the same [i].
0 commit comments