Abstract structure.

This commit is contained in:
Olivier 2023-02-10 15:47:00 +01:00
parent 712d2f882a
commit 05b3d73873
3 changed files with 83 additions and 3 deletions

View File

@ -190,16 +190,35 @@ module type GSTRUCTURE = sig
end
(* [GSTRUCTURE_OPT] describes the output of [Structure.Option] and
an input of [Generalization.Make]. *)
(* [GSTRUCTURE_ABS] describes the output of [Structure.Abstract]. *)
module type GSTRUCTURE_ABS = sig
module S : GSTRUCTURE
type 'a structure =
| Abstract of int
| User of 'a S.structure
(** @inline *)
include GSTRUCTURE with type 'a structure := 'a structure
val fresh_abstract : unit -> 'a structure
end
(* [GSTRUCTURE_OPT] describes the output of [Structure.Option]. *)
module type GSTRUCTURE_OPT = sig
module S : GSTRUCTURE
(** @inline *)
include GSTRUCTURE with type 'a structure = 'a S.structure option
end
(* [GSTRUCTURE_ABS_OPT] describes the input of [Generalization.Make] *)
module type GSTRUCTURE_ABS_OPT = sig
module S : GSTRUCTURE_ABS
include GSTRUCTURE_OPT with module S := S
end
(* -------------------------------------------------------------------------- *)

View File

@ -11,6 +11,61 @@
open Signatures
module Abstract (S : GSTRUCTURE) = struct
module S = S
type 'a structure =
| Abstract of int
| User of 'a S.structure
exception InconsistentConjunction =
S.InconsistentConjunction
let conjunction f s1 s2 =
match s1, s2 with
| Abstract n1, Abstract n2 ->
if Int.equal n1 n2 then s1
else raise InconsistentConjunction
| User s1, User s2 ->
User (S.conjunction f s1 s2)
| Abstract _, User _
| User _, Abstract _ ->
raise InconsistentConjunction
let iter f s =
match s with
| Abstract _ ->
()
| User s ->
S.iter f s
let fold f s acc =
match s with
| Abstract _ ->
acc
| User s ->
S.fold f s acc
let map f s =
match s with
| Abstract n ->
Abstract n
| User s ->
User (S.map f s)
let fresh_abstract_id =
Utils.gensym()
let fresh_abstract () =
Abstract (fresh_abstract_id ())
let pprint elem s =
match s with
| Abstract n -> PPrint.(string "abstract " ^^ string (string_of_int n))
| User s -> S.pprint elem s
end
module Option (S : GSTRUCTURE) = struct
module S = S

View File

@ -11,6 +11,12 @@
open Signatures
module Abstract (S : sig (** @inline *) include GSTRUCTURE end) : sig
(** @inline *)
include GSTRUCTURE_ABS with module S = S
end
(**This functor transforms a type ['a structure], equipped with [map],
[iter] and [conjunction] operations, into the type ['a structure option],
equipped with the same operations. The type ['a structure option] is