Commit 8b07467f authored by Andrei Paskevich's avatar Andrei Paskevich

add "exclusive metaproperties" to support metas-options: adding

a meta of an exclusive kind removes the previous meta of this 
kind (if any) from task_meta.

Discuss: should driver-imposed exclusive metas have a low priority
(i.e. driver does not add an exclusive meta if the task already 
contains one of this kind) or should we just trust the driver
authors not to put exclusive metas in drivers? 
parent de0c3057
......@@ -40,8 +40,12 @@ module Hstds = Hashcons.Make (struct
end)
let mk_tds s = Hstds.hashcons { tds_set = s; tds_tag = -1 }
let empty_tds = mk_tds Stdecl.empty
let tds_add td s = mk_tds (Stdecl.add td s.tds_set)
let tds_singleton td = mk_tds (Stdecl.singleton td)
let tds_equal = (==)
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mstr.t
......@@ -52,7 +56,10 @@ let mm_find mm t =
try Mstr.find t mm with Not_found -> ignore (lookup_meta t); empty_tds
let cm_add cm th td = Mid.add th.th_name (tds_add td (cm_find cm th)) cm
let mm_add mm t td = Mstr.add t (tds_add td (mm_find mm t)) mm
let mm_add mm t td = if is_meta_exc t
then Mstr.add t (tds_singleton td) mm
else Mstr.add t (tds_add td (mm_find mm t)) mm
(** Task *)
......@@ -217,6 +224,14 @@ let find_tagged t tds acc =
| Meta (s, [MARid id]) when s = t -> Sid.add id acc
| _ -> assert false) tds.tds_set acc
exception NotExclusiveMeta of string
let get_meta_exc t tds =
if not (is_meta_exc t) then raise (NotExclusiveMeta t);
Stdecl.fold (fun td _ -> match td.td_node with
| Meta (s,_) when s = t -> Some td
| _ -> assert false) tds.tds_set None
(* Exception reporting *)
let () = Exn_printer.register (fun fmt exn -> match exn with
......@@ -226,5 +241,7 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
| NotTaggingMeta s ->
Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" s
| NotExclusiveMeta s ->
Format.fprintf fmt "Metaproperty '%s' is not exclusive" s
| _ -> raise exn)
......@@ -31,6 +31,8 @@ type tdecl_set = private {
tds_tag : int;
}
val tds_equal : tdecl_set -> tdecl_set -> bool
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mstr.t
......@@ -99,6 +101,12 @@ exception NotTaggingMeta of string
val find_tagged : string -> tdecl_set -> Sid.t -> Sid.t
(* special selector for exclusive metaproperties *)
exception NotExclusiveMeta of string
val get_meta_exc : string -> tdecl_set -> tdecl option
(* exceptions *)
exception GoalNotFound
......
......@@ -107,16 +107,22 @@ exception BadMetaArity of string * int * int
exception MetaTypeMismatch of string * meta_arg_type * meta_arg_type
let meta_table = Hashtbl.create 17
let meta_exc = Hashtbl.create 17
let register_meta s al =
try let al' = Hashtbl.find meta_table s in
if al <> al' then raise (KnownMeta s)
with Not_found -> Hashtbl.add meta_table s al
let register_meta_exc s al =
register_meta s al; Hashtbl.add meta_exc s ()
let lookup_meta s =
try Hashtbl.find meta_table s
with Not_found -> raise (UnknownMeta s)
let is_meta_exc s = Hashtbl.mem meta_exc s
let list_meta () = Hashtbl.fold (fun k _ acc -> k::acc) meta_table []
......
......@@ -59,9 +59,11 @@ type meta_arg_real =
| MARstr of string
| MARint of int
val register_meta : string -> meta_arg_type list -> unit
val register_meta : string -> meta_arg_type list -> unit
val register_meta_exc : string -> meta_arg_type list -> unit
val lookup_meta : string -> meta_arg_type list
val is_meta_exc : string -> bool
val list_meta : unit -> string list
......
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