aboutsummaryrefslogtreecommitdiff
path: root/lib/syntax/check.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/syntax/check.ml')
-rw-r--r--lib/syntax/check.ml13
1 files changed, 13 insertions, 0 deletions
diff --git a/lib/syntax/check.ml b/lib/syntax/check.ml
index a5db091..9292a7a 100644
--- a/lib/syntax/check.ml
+++ b/lib/syntax/check.ml
@@ -123,6 +123,7 @@ end
module Make (A : App) = struct
let identifier = "main_checker"
let description = "Internal module"
+ let is_global = false
let active = ref false
type context = result Array.t
@@ -136,6 +137,18 @@ module Make (A : App) = struct
let value = S.initialize () in
R { value; witness = context })
+ let finalize : result Array.t -> (string * Report.t) list =
+ fun context_array ->
+ let _, report =
+ Array.fold_left A.t ~init:(0, [])
+ ~f:(fun (i, acc) (E { module_ = (module S); context; _ }) ->
+ let result = Array.get context_array i in
+ let local_context = Option.get (get context result) in
+ let reports = S.finalize local_context in
+ (i + 1, List.rev_append reports acc))
+ in
+ report
+
(* Global variable for the whole module *)
let len = Array.length A.t