From 19ea68ecafcee5199dde1b044fd4be9edc211673 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 11 Jun 2019 10:49:25 +0200 Subject: Reify libobject containers We make a few libobject constructions (Module, Module Type, Include,...) first-class and rephrase their handling in direct style (removing the inversion of control). This makes it easier to define iterators over objects without hacks like inspecting the tags of dynamic objects. --- checker/values.ml | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) (limited to 'checker/values.ml') diff --git a/checker/values.ml b/checker/values.ml index cde2db2721..8dc09aed87 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -345,8 +345,26 @@ let v_compiled_lib = (** Library objects *) let v_obj = Dyn -let v_libobj = Tuple ("libobj", [|v_id;v_obj|]) -let v_libobjs = List v_libobj + +let rec v_aobjs = Sum("algebraic_objects", 0, + [| [|v_libobjs|]; + [|v_mp;v_subst|] + |]) +and v_substobjs = + Tuple("*", [|List v_uid;v_aobjs|]) +and v_libobjt = Sum("Libobject.t",0, + [| [| v_substobjs |]; + [| v_substobjs |]; + [| v_aobjs |]; + [| v_libobjs |]; + [| v_bool; v_mp |]; + [| v_obj |] + |]) + +and v_libobj = Tuple ("libobj", [|v_id;v_libobjt|]) + +and v_libobjs = List v_libobj + let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|]) (** STM objects *) -- cgit v1.2.3