diff --git a/demos/faulty/avl/Main.ml b/demos/faulty/avl/Main.ml
index ee1f4d3116a45c8409f4248812e1602cbf99a947..af0d2711052ee9d06cb2a90d82cc81a9e4c7c3e9 100644
--- a/demos/faulty/avl/Main.ml
+++ b/demos/faulty/avl/Main.ml
@@ -27,7 +27,7 @@ let check (_ : R.t) =
C.check, constant "check"
let set =
- declare_abstract_type ~check "set"
+ declare_abstract_type ~check ()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/faulty/bag_det/Main.ml b/demos/faulty/bag_det/Main.ml
index 52882e636dc167d502a8ed1374090e7cbc6c0eb4..b2f8e82a9d2659de9f3e488d731fcd5151cb40be 100644
--- a/demos/faulty/bag_det/Main.ml
+++ b/demos/faulty/bag_det/Main.ml
@@ -32,7 +32,7 @@ let element =
by the reference implementation and by the candidate implementation. *)
let bag =
- declare_abstract_type "bag"
+ declare_abstract_type()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/faulty/bag_nondet/Main.ml b/demos/faulty/bag_nondet/Main.ml
index 0350976a24defc658600e3af48a57a62e7bfb458..d168d953d3e5c652866336f820dbde839dab3729 100644
--- a/demos/faulty/bag_nondet/Main.ml
+++ b/demos/faulty/bag_nondet/Main.ml
@@ -32,7 +32,7 @@ let element =
by the reference implementation and by the candidate implementation. *)
let bag =
- declare_abstract_type "bag"
+ declare_abstract_type()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/faulty/generator/Main.ml b/demos/faulty/generator/Main.ml
index 6f1c2b72d1105f715d56beb5feb74fc6a3ca4e6c..fdbcfa53b5ed8a564ee8654eb18d564e2b790538 100644
--- a/demos/faulty/generator/Main.ml
+++ b/demos/faulty/generator/Main.ml
@@ -25,7 +25,7 @@ let check model =
C.check model, constant "check"
let t =
- declare_abstract_type "t" ~var:"g" ~check
+ declare_abstract_type ~var:"g" ~check ()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/faulty/map/Main.ml b/demos/faulty/map/Main.ml
index 4c8e168a6840cf532135a5a69c75bed190ce69c9..1af04b36f8497522242e1d3e2b3d39ff094cd462 100644
--- a/demos/faulty/map/Main.ml
+++ b/demos/faulty/map/Main.ml
@@ -27,7 +27,7 @@ let check model =
C.check model, constant "check"
let map =
- declare_abstract_type ~check "map"
+ declare_abstract_type ~check ()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/faulty/pairs/Main.ml b/demos/faulty/pairs/Main.ml
index a9c28abfe346503f53dfa0d5a6af43663acc8fc2..4a4ae669f36cb78b0bd233d0e2d7fb6a70019243 100644
--- a/demos/faulty/pairs/Main.ml
+++ b/demos/faulty/pairs/Main.ml
@@ -41,7 +41,7 @@ let index (s : _ R.t) =
ways by the reference implementation and by the candidate implementation. *)
let stack =
- declare_abstract_type "stack"
+ declare_abstract_type()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/faulty/parray/Main.ml b/demos/faulty/parray/Main.ml
index c6f0d12a209ef38ae199022d330f2d6dc2ac462a..bb0d88d17bfef972b50534322765da48bb7d5b47 100644
--- a/demos/faulty/parray/Main.ml
+++ b/demos/faulty/parray/Main.ml
@@ -44,7 +44,7 @@ let index_element_list =
(* Declare an abstract type [array] of persistent arrays. *)
let array =
- declare_abstract_type "array"
+ declare_abstract_type()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/faulty/parray_mini/Main.ml b/demos/faulty/parray_mini/Main.ml
index 61fbbf40b8fcfdba4886fd367f419e5d19041039..5e496add5c4445169951c3f42625a7ae90b19ed3 100644
--- a/demos/faulty/parray_mini/Main.ml
+++ b/demos/faulty/parray_mini/Main.ml
@@ -16,7 +16,7 @@ module R = Reference
module C = Candidate
let () =
(* Specs. *)
- let array = declare_abstract_type "array"
+ let array = declare_abstract_type()
and element = sequential()
and length = interval 0 16
and index a = interval 0 (R.length a) in
diff --git a/demos/faulty/sparray/Main.ml b/demos/faulty/sparray/Main.ml
index ef7fbb86e0861917627bf207fbf8b2d0d0e191bc..8811b3ae2e64ff7b4ded316f2c325edd73130954 100644
--- a/demos/faulty/sparray/Main.ml
+++ b/demos/faulty/sparray/Main.ml
@@ -31,7 +31,7 @@ let element =
(* Declare an abstract type [array] of persistent arrays. *)
let array =
- declare_abstract_type "array"
+ declare_abstract_type()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/misc/choose_and_remove_opt_deterministic/Main.ml b/demos/misc/choose_and_remove_opt_deterministic/Main.ml
index 06fa7b47f5beb39360ccc1e73c30ad92d94a6c75..ccc1659810a84bd797081db6a28ca1720eded93a 100644
--- a/demos/misc/choose_and_remove_opt_deterministic/Main.ml
+++ b/demos/misc/choose_and_remove_opt_deterministic/Main.ml
@@ -27,7 +27,7 @@ let check model =
C.check model, constant "check"
let map =
- declare_abstract_type ~check "map"
+ declare_abstract_type ~check ()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/misc/map_choose/Main.ml b/demos/misc/map_choose/Main.ml
index d2ed27c26f4ccc9a8de5e6a0b75146bc2a43d77f..bb09667bd178468092aa0444938d79314238e2c7 100644
--- a/demos/misc/map_choose/Main.ml
+++ b/demos/misc/map_choose/Main.ml
@@ -30,7 +30,7 @@ let check model =
C.check model, constant "check"
let map =
- declare_abstract_type ~check "map"
+ declare_abstract_type ~check ()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/misc/map_choose_opt/Main.ml b/demos/misc/map_choose_opt/Main.ml
index 01df4663da53d357eb16171aae869d8a5d685c3d..8bfe181a2e1a00334e115763d6ded7d2597e9844 100644
--- a/demos/misc/map_choose_opt/Main.ml
+++ b/demos/misc/map_choose_opt/Main.ml
@@ -30,7 +30,7 @@ let check model =
C.check model, constant "check"
let map =
- declare_abstract_type ~check "map"
+ declare_abstract_type ~check ()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/misc/seq1/Main.ml b/demos/misc/seq1/Main.ml
index afe6e864ca0888003e2a0160d2a89a3052b8a199..c76cd61a6aa89ea680949a9223b5d66886159ab5 100644
--- a/demos/misc/seq1/Main.ml
+++ b/demos/misc/seq1/Main.ml
@@ -20,7 +20,7 @@ let element =
sequential()
let stack =
- declare_abstract_type "stack"
+ declare_abstract_type()
let seq =
declare_seq (lt 16)
diff --git a/demos/misc/seq2/Main.ml b/demos/misc/seq2/Main.ml
index afe6e864ca0888003e2a0160d2a89a3052b8a199..c76cd61a6aa89ea680949a9223b5d66886159ab5 100644
--- a/demos/misc/seq2/Main.ml
+++ b/demos/misc/seq2/Main.ml
@@ -20,7 +20,7 @@ let element =
sequential()
let stack =
- declare_abstract_type "stack"
+ declare_abstract_type()
let seq =
declare_seq (lt 16)
diff --git a/demos/misc/seq3/Main.ml b/demos/misc/seq3/Main.ml
index afe6e864ca0888003e2a0160d2a89a3052b8a199..c76cd61a6aa89ea680949a9223b5d66886159ab5 100644
--- a/demos/misc/seq3/Main.ml
+++ b/demos/misc/seq3/Main.ml
@@ -20,7 +20,7 @@ let element =
sequential()
let stack =
- declare_abstract_type "stack"
+ declare_abstract_type()
let seq =
declare_seq (lt 16)
diff --git a/demos/misc/seq4/Main.ml b/demos/misc/seq4/Main.ml
index 1fc8e50b5cf4d58b3ce54fd235967f553ee44710..9ab96af8cbee13927baf75b35bdf3bfa5313e8e2 100644
--- a/demos/misc/seq4/Main.ml
+++ b/demos/misc/seq4/Main.ml
@@ -20,7 +20,7 @@ let aseq =
declare_affine_seq (lt 16)
let array =
- declare_abstract_type "array"
+ declare_abstract_type()
let () =
diff --git a/demos/misc/seq5/Main.ml b/demos/misc/seq5/Main.ml
index 0674545efae0e1334f1bcc838ede5224965dc751..ba84b1ecd246ace65305ee049999405ea26c371a 100644
--- a/demos/misc/seq5/Main.ml
+++ b/demos/misc/seq5/Main.ml
@@ -23,7 +23,7 @@ let aseq =
declare_affine_seq element
let array =
- declare_abstract_type "array"
+ declare_abstract_type()
let () =
diff --git a/demos/misc/seq6/Main.ml b/demos/misc/seq6/Main.ml
index 0674545efae0e1334f1bcc838ede5224965dc751..ba84b1ecd246ace65305ee049999405ea26c371a 100644
--- a/demos/misc/seq6/Main.ml
+++ b/demos/misc/seq6/Main.ml
@@ -23,7 +23,7 @@ let aseq =
declare_affine_seq element
let array =
- declare_abstract_type "array"
+ declare_abstract_type()
let () =
diff --git a/demos/working/bag/Main.ml b/demos/working/bag/Main.ml
index 0350976a24defc658600e3af48a57a62e7bfb458..d168d953d3e5c652866336f820dbde839dab3729 100644
--- a/demos/working/bag/Main.ml
+++ b/demos/working/bag/Main.ml
@@ -32,7 +32,7 @@ let element =
by the reference implementation and by the candidate implementation. *)
let bag =
- declare_abstract_type "bag"
+ declare_abstract_type()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/working/map/Main.ml b/demos/working/map/Main.ml
index 4a41cd5c43eb5f5e7fd8ff61045fe76733c73ca6..1845eca827e79ff0b5c89e43f9579dbb890df9dc 100644
--- a/demos/working/map/Main.ml
+++ b/demos/working/map/Main.ml
@@ -27,7 +27,7 @@ let check model =
C.check model, constant "check"
let map =
- declare_abstract_type ~check "map"
+ declare_abstract_type ~check ()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/working/parray/Main.ml b/demos/working/parray/Main.ml
index ccc93b66b996d9cbd22f00132d0d44f6c6b11cd1..fca3c4e64e037814e2b3e81f7fe164fd04ae267d 100644
--- a/demos/working/parray/Main.ml
+++ b/demos/working/parray/Main.ml
@@ -34,7 +34,7 @@ let index =
(* Declare an abstract type [array] of persistent arrays. *)
let array =
- declare_abstract_type "array"
+ declare_abstract_type()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/working/seq/Main.ml b/demos/working/seq/Main.ml
index 434921c9f2af7f4703510867a7a370c2d5d381aa..d9139f08865b04e2be1416be9ce73394e6f1ee6f 100644
--- a/demos/working/seq/Main.ml
+++ b/demos/working/seq/Main.ml
@@ -20,7 +20,7 @@ let element =
sequential()
let stack =
- declare_abstract_type "stack"
+ declare_abstract_type()
let seq =
declare_seq (lt 16)
diff --git a/demos/working/sparray/Main.ml b/demos/working/sparray/Main.ml
index ef7fbb86e0861917627bf207fbf8b2d0d0e191bc..8811b3ae2e64ff7b4ded316f2c325edd73130954 100644
--- a/demos/working/sparray/Main.ml
+++ b/demos/working/sparray/Main.ml
@@ -31,7 +31,7 @@ let element =
(* Declare an abstract type [array] of persistent arrays. *)
let array =
- declare_abstract_type "array"
+ declare_abstract_type()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/working/stack/Main.ml b/demos/working/stack/Main.ml
index 08337e7bdadc08d3f5d64d5d1a92d8a1d8126983..f5e99c7291cc554a1da2fc5c3e13e3747b958642 100644
--- a/demos/working/stack/Main.ml
+++ b/demos/working/stack/Main.ml
@@ -56,7 +56,7 @@ let check model =
C.check model, constant "check"
let stack =
- declare_abstract_type ~check "stack"
+ declare_abstract_type ~check ()
(* -------------------------------------------------------------------------- *)
diff --git a/demos/working/stack_prologue/Main.ml b/demos/working/stack_prologue/Main.ml
index b2a13a4775bf56e7d953d7bcc79ca796ee594207..87e5ca34d77119a55f760994988370f122ae5b94 100644
--- a/demos/working/stack_prologue/Main.ml
+++ b/demos/working/stack_prologue/Main.ml
@@ -38,7 +38,7 @@ let prologue () =
let stack =
let check model = C.check model, constant "check" in
- declare_abstract_type ~check "stack"
+ declare_abstract_type ~check ()
in
let nonfull s = not (R.is_full s) in
diff --git a/src/BuiltinAbstract.ml b/src/BuiltinAbstract.ml
index f3c2d3170a928d0045740af1dbed78e9fe560f6a..ac1adfc2a8e880c44f11714d9caaa1ad01a458ec 100644
--- a/src/BuiltinAbstract.ml
+++ b/src/BuiltinAbstract.ml
@@ -16,8 +16,7 @@ open Support.Fun
let abstract spec =
(* Declare this abstract type. *)
- let name = "<abstract>" in
- let aspec = declare_abstract_type ~var:"abs" name in
+ let aspec = declare_abstract_type ~var:"abs" () in
(* Declare an operation that maps this abstract type to its concrete
representation. Its implementation is the identity function. *)
Ops.declare "Sup.Fun.id" (aspec ^> spec) id id;
diff --git a/src/BuiltinSeq.ml b/src/BuiltinSeq.ml
index 29ac00a0e7ebc75af05d01faea39b278db00ae70..3856ad2178ff86e13afa11b5859d3f7af7648f8e 100644
--- a/src/BuiltinSeq.ml
+++ b/src/BuiltinSeq.ml
@@ -49,7 +49,7 @@ let declare_seq ?length:(length=16) element =
(* The deconstruction side. *)
begin
(* Declare an abstract type [seq]. *)
- let seq = declare_abstract_type ~var:"seq" "seq" in
+ let seq = declare_abstract_type ~var:"seq" () in
(* Declare the operation [to_option]. *)
let spec = seq ^> option (element *** seq) in
Ops.declare "Sup.Seq.to_option" spec
@@ -96,7 +96,7 @@ let declare_affine_seq ?length:(length=16) element =
(* The deconstruction side. *)
begin
(* Declare the abstract type [seq]. *)
- let seq = declare_abstract_type ~var:"seq" "affine_seq" in
+ let seq = declare_abstract_type ~var:"seq" () in
(* Declare the operation [to_option]. *)
let spec = VSeq.valid % seq ^> option (element *** seq) in
Ops.declare "Sup.Seq.to_option"
diff --git a/src/Monolith.mli b/src/Monolith.mli
index ebb80b37259ceb54efaa92b8fdc6c5ec425af349..98c63434303bbc408eff5cf04d129106c5b805c6 100644
--- a/src/Monolith.mli
+++ b/src/Monolith.mli
@@ -274,10 +274,9 @@ val deconstructible:
('t Print.printer) ->
('t, 't) spec
-(** [declare_abstract_type "t"] declares a new abstract type named "t". This
- name is used in certain error messages. Which types ['r] and ['c] are
- actually meant, in the reference implementation and in the candidate
- implementation, is inferred by the OCaml type-checker.
+(** [declare_abstract_type()] declares a new abstract type. Which types ['r]
+ and ['c] are actually meant, in the reference implementation and in the
+ candidate implementation, is inferred by the OCaml type-checker.
An abstract type may be implemented in different ways in the reference
implementation and in the candidate implementation, which explains why
@@ -299,12 +298,11 @@ val deconstructible:
performed.
The optional parameter [var] is a base name that is used for variables
- of type "t". If it is omitted, the first letter of the type's name is
- used. *)
+ of this type. *)
val declare_abstract_type:
?check: ('r -> ('c -> unit) code) ->
?var: string ->
- (* name: *) string ->
+ unit ->
('r, 'c) spec
(** [unit] represents the base type [unit]. This type is constructible
diff --git a/src/Spec.ml b/src/Spec.ml
index 097f0db4607df401a53d5fb6f7c50c627df22792..4626262a9beec6ee0a8c3b02c2e42f533fb366af 100644
--- a/src/Spec.ml
+++ b/src/Spec.ml
@@ -207,9 +207,6 @@ type (_, _) spec =
and ('r, 'c) abstract = {
- (* The name of this type, used only in informational messages. *)
- aty_name : string;
-
(* The base name used for a variable of this type. *)
aty_var : string;
@@ -300,27 +297,18 @@ let default_check : type r c . r -> (c -> unit) code =
fun _ ->
(fun _ -> ()), Code.constant "(fun _ -> ())"
-let default_var var name =
- match var with
- | Some var ->
- var
- | None ->
- (* Use the first letter of the type's name. *)
- String.sub name 0 1
+let default_var =
+ "x"
let declare_abstract_type
?check:(check=default_check)
- ?var
- name
+ ?var:(var=default_var)
+ ()
=
- (* Sanitize the type name. *)
- if name = "" then invalid_arg "declare_abstract_type: name is empty";
- (* If no [var] argument was provided, choose one, based on the type name. *)
- let var = default_var var name in
(* Create a new tag for this abstract type. *)
let tag = Tag.new_tag () in
(* Done. *)
- SpecBaseAbstract (tag, { aty_var = var; aty_name = name; aty_check = check })
+ SpecBaseAbstract (tag, { aty_var = var; aty_check = check })
(* -------------------------------------------------------------------------- *)