Abstract structure.
This commit is contained in:
parent
ec46543398
commit
ec5e66564c
|
@ -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
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue