Commit 5ae69cd3 authored by Andrei Paskevich's avatar Andrei Paskevich

make the meta_desc field immutable

Provers will have native polymorphism support long before people will
start writing third-party polymorphism encoding procedures for Why3.
(And it's not that I have high hopes about the former.)
parent 5e2eebf4
...@@ -102,8 +102,8 @@ type meta = { ...@@ -102,8 +102,8 @@ type meta = {
meta_name : string; meta_name : string;
meta_type : meta_arg_type list; meta_type : meta_arg_type list;
meta_excl : bool; meta_excl : bool;
meta_desc : Pp.formatted;
meta_tag : int; meta_tag : int;
mutable meta_desc : Pp.formatted;
} }
let print_meta_desc fmt m = let print_meta_desc fmt m =
...@@ -133,8 +133,8 @@ let mk_meta = ...@@ -133,8 +133,8 @@ let mk_meta =
meta_name = s; meta_name = s;
meta_type = al; meta_type = al;
meta_excl = excl; meta_excl = excl;
meta_tag = (incr c; !c);
meta_desc = desc; meta_desc = desc;
meta_tag = (incr c; !c);
} }
let register_meta ~desc s al excl = let register_meta ~desc s al excl =
...@@ -156,8 +156,6 @@ let lookup_meta s = ...@@ -156,8 +156,6 @@ let lookup_meta s =
let list_metas () = Hashtbl.fold (fun _ v acc -> v::acc) meta_table [] let list_metas () = Hashtbl.fold (fun _ v acc -> v::acc) meta_table []
let set_meta_desc f m = m.meta_desc <- f
(** Theory *) (** Theory *)
type theory = { type theory = {
......
...@@ -62,8 +62,8 @@ type meta = private { ...@@ -62,8 +62,8 @@ type meta = private {
meta_name : string; meta_name : string;
meta_type : meta_arg_type list; meta_type : meta_arg_type list;
meta_excl : bool; meta_excl : bool;
meta_desc : Pp.formatted;
meta_tag : int; meta_tag : int;
mutable meta_desc : Pp.formatted;
} }
val print_meta_desc : Pp.formatter -> meta -> unit val print_meta_desc : Pp.formatter -> meta -> unit
...@@ -75,16 +75,16 @@ module Hmeta : Hashtbl.S with type key = meta ...@@ -75,16 +75,16 @@ module Hmeta : Hashtbl.S with type key = meta
val meta_equal : meta -> meta -> bool val meta_equal : meta -> meta -> bool
val meta_hash : meta -> int val meta_hash : meta -> int
val register_meta : val register_meta :
desc:Pp.formatted -> string -> meta_arg_type list -> meta desc:Pp.formatted -> string -> meta_arg_type list -> meta
val register_meta_excl : val register_meta_excl :
desc:Pp.formatted -> string -> meta_arg_type list -> meta desc:Pp.formatted -> string -> meta_arg_type list -> meta
(** Register exclusive meta, each new setting remove the previous one. (** With exclusive metas, each new meta cancels the previous one.
Useful for transformation or printer parameters *) Useful for transformation or printer parameters *)
val lookup_meta : string -> meta val lookup_meta : string -> meta
val list_metas : unit -> meta list val list_metas : unit -> meta list
val set_meta_desc : Pp.formatted -> meta -> unit
(** Theory *) (** Theory *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment