aboutsummaryrefslogtreecommitdiff
path: root/lib/checks/check.mli
diff options
context:
space:
mode:
authorChimrod <>2024-12-02 09:05:18 +0100
committerChimrod <>2024-12-02 09:05:18 +0100
commit53c02501935b3cb2db78e79deb4d38c997505a95 (patch)
tree88a75e012ee186ffb6c6e3e0c53ba80610ec3b0b /lib/checks/check.mli
parent9e7b9de243e488e15d2c7528ce64e569eba8add2 (diff)
Moved the checks in a dedicated library
Diffstat (limited to 'lib/checks/check.mli')
-rw-r--r--lib/checks/check.mli69
1 files changed, 69 insertions, 0 deletions
diff --git a/lib/checks/check.mli b/lib/checks/check.mli
new file mode 100644
index 0000000..321b67b
--- /dev/null
+++ b/lib/checks/check.mli
@@ -0,0 +1,69 @@
+(** This module is a meta-checker. It will take many checkers and aggregate
+ their result together before providing an unified result.
+
+ The modules required to be declared before being used, using the [build]
+ method, and provided as an array :
+
+ {[
+ let _, e1 = build (module …)
+ let _, e2 = build (module …)
+
+ module Check = Make (struct
+ let t = [| e1; e2 |]
+ end)
+ ]}
+*)
+
+module Id : sig
+ type 'a t
+ (** The type created on-the-fly. *)
+end
+
+type t =
+ | E : {
+ module_ :
+ (module Qsp_syntax.S.Analyzer
+ with type Expression.t = 'a
+ and type Expression.t' = 'b
+ and type Instruction.t = 'c
+ and type Instruction.t' = 'd
+ and type Location.t = 'e
+ and type context = 'f);
+ expr_witness : 'a Id.t;
+ expr' : 'b Id.t;
+ instr_witness : 'c Id.t;
+ instr' : 'd Id.t;
+ location_witness : 'e Id.t;
+ context : 'f Id.t;
+ }
+ -> t (** Type of check to apply *)
+
+val build :
+ (module Qsp_syntax.S.Analyzer
+ with type Expression.t = _
+ and type Expression.t' = _
+ and type Instruction.t = _
+ and type Instruction.t' = _
+ and type Location.t = 'a
+ and type context = _) ->
+ 'a Id.t * t
+(** Build a new check from a module following S.Analyzer signature.
+ypeid
+ Return the result type which hold the final result value, and checker
+ itself. *)
+
+val get_module : t -> (module Qsp_syntax.S.Analyzer)
+
+type result
+
+val get : 'a Id.t -> result -> 'a option
+(** The method [get] can be used to get the internal value for one of the
+ checker used.
+ *)
+
+module Make (A : sig
+ val t : t array
+end) : sig
+ include Qsp_syntax.S.Analyzer with type Location.t = result array
+end
+[@@warning "-67"]