metas become a record instead of just a string

share/zsh/_why3

@@ -29,7 +29,7 @@ _arguments -s -S \
      "(-L --library -I)"'-I'"[same as -L (obsolete)]:Mlpost lib path (obsolete use -L):_files -/  "\
      "(-D --driver -P -prover)"'-P'"[<prover> Prove or print (with -o) the selected goals]:<prover>:->provers"\
      "(-D --driver -P -prover)"'--prover'"[same as -P]:<prover>:->provers"\
-     '*-M'"[<meta_name> <string> Add a meta option to each tasks]:<meta_name>:->metas:<meta_arg>:"\
+     '*-M'"[<meta_name>=<string> Add a meta option to each tasks]:<meta_name>=<meta_arg>:->metas"\
      "(-F --format)"'-F'"[<format> Input format (default: \"why\")]:<input format>:"\
      "(-F --format)"'--format'"[same as -F]:<input format>:"\
      "(-t --timelimit)"'-t'"[<sec> Set the prover\'s time limit (default=10, no limit=0)]:<timeout s>:"\
@@ -74,7 +74,7 @@ case $state in
         ;;
     metas)
         _message "<metas>";
-        METAS="$($cmd --list-metas | egrep -E "^  [a-z]" | sed "s/^[ ]*//")";
+        METAS="$($cmd --list-metas | egrep -E "^  [a-z]" | sed -e "s/^[ ]*//" -e "s/$/=/")";
         METAS=(${(f)METAS});
         compadd $METAS;
         return 0

src/core/pretty.ml

@@ -373,9 +373,9 @@ let print_tdecl fmt td = match td.td_node with
         print_th th (print_list comma print_inst_ts) tm
                     (print_list comma print_inst_ls) lm
                     (print_list comma print_inst_pr) pm
-  | Meta (t,al) ->
+  | Meta (m,al) ->
       fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
-        t (print_list comma print_meta_arg) al
+        (meta_name m) (print_list comma print_meta_arg) al
 
 let print_theory fmt th =
   fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."

src/core/printer.mli

@@ -46,9 +46,9 @@ val list_printers : unit -> string list
 val print_prelude : prelude pp
 val print_th_prelude : task -> prelude_map pp
 
-val meta_remove_type : string
-val meta_remove_logic : string
-val meta_remove_prop : string
+val meta_remove_type : meta
+val meta_remove_logic : meta
+val meta_remove_prop : meta
 
 val remove_type : tysymbol -> tdecl
 val remove_logic : lsymbol -> tdecl

src/core/task.ml

@@ -48,18 +48,18 @@ 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
+type meta_map = tdecl_set Mmeta.t
 
 let cm_find cm th = try Mid.find th.th_name cm with Not_found -> empty_tds
 
 let mm_find mm t =
-  try Mstr.find t mm with Not_found -> ignore (lookup_meta t); empty_tds
+  try Mmeta.find t mm with Not_found -> 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 = if is_meta_excl t
-  then Mstr.add t (tds_singleton td) mm
-  else Mstr.add t (tds_add td (mm_find mm t)) mm
+  then Mmeta.add t (tds_singleton td) mm
+  else Mmeta.add t (tds_add td (mm_find mm t)) mm
 
 (** Task *)
 
@@ -106,7 +106,7 @@ let mk_task decl prev known clone meta = Some (Hstask.hashcons {
 
 let task_known = option_apply Mid.empty (fun t -> t.task_known)
 let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
-let task_meta  = option_apply Mstr.empty (fun t -> t.task_meta)
+let task_meta  = option_apply Mmeta.empty (fun t -> t.task_meta)
 
 let find_clone task th = cm_find (task_clone task) th
 let find_meta  task t  = mm_find (task_meta  task) t
@@ -213,38 +213,38 @@ let task_decls  = task_fold (fun acc td ->
 
 (* special selector for metaproperties of a single ident *)
 
-exception NotTaggingMeta of string
+exception NotTaggingMeta of meta
 
 let find_tagged_ts t tds acc =
-  begin match lookup_meta t with
+  begin match meta_arg_type t with
     | [MTtysymbol] -> ()
     | _ -> raise (NotTaggingMeta t)
   end;
   Stdecl.fold (fun td acc -> match td.td_node with
-    | Meta (s, [MAts ts]) when s = t -> Sts.add ts acc
+    | Meta (s, [MAts ts]) when meta_equal s t -> Sts.add ts acc
     | _ -> assert false) tds.tds_set acc
 
 let find_tagged_ls t tds acc =
-  begin match lookup_meta t with
+  begin match meta_arg_type t with
     | [MTlsymbol] -> ()
     | _ -> raise (NotTaggingMeta t)
   end;
   Stdecl.fold (fun td acc -> match td.td_node with
-    | Meta (s, [MAls ls]) when s = t -> Sls.add ls acc
+    | Meta (s, [MAls ls]) when meta_equal s t -> Sls.add ls acc
     | _ -> assert false) tds.tds_set acc
 
 let find_tagged_pr t tds acc =
-  begin match lookup_meta t with
+  begin match meta_arg_type t with
     | [MTprsymbol] -> ()
     | _ -> raise (NotTaggingMeta t)
   end;
   Stdecl.fold (fun td acc -> match td.td_node with
-    | Meta (s, [MApr pr]) when s = t -> Spr.add pr acc
+    | Meta (s, [MApr pr]) when meta_equal s t -> Spr.add pr acc
     | _ -> assert false) tds.tds_set acc
 
-exception NotExclusiveMeta of string
+exception NotExclusiveMeta of meta
 
-let get_meta_exc t tds =
+let get_meta_excl t tds =
   if not (is_meta_excl t) then raise (NotExclusiveMeta t);
   Stdecl.fold (fun td _ -> match td.td_node with
     | Meta (s,arg) when s = t -> Some arg
@@ -257,9 +257,9 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
   | SkipFound ->    Format.fprintf fmt "Task cannot contain a skip"
   | GoalFound ->    Format.fprintf fmt "The task already ends with a goal"
   | 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
+  | NotTaggingMeta m ->
+      Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" (meta_name m)
+  | NotExclusiveMeta m ->
+      Format.fprintf fmt "Metaproperty '%s' is not exclusive" (meta_name m)
   | _ -> raise exn)
 

src/core/task.mli

@@ -34,7 +34,7 @@ type tdecl_set = private {
 val tds_equal : tdecl_set -> tdecl_set -> bool
 
 type clone_map = tdecl_set Mid.t
-type meta_map = tdecl_set Mstr.t
+type meta_map = tdecl_set Mmeta.t
 
 (** Task *)
 
@@ -57,7 +57,7 @@ val task_clone : task -> clone_map
 val task_meta  : task -> meta_map
 
 val find_clone : task -> theory -> tdecl_set
-val find_meta  : task -> string -> tdecl_set
+val find_meta  : task -> meta -> tdecl_set
 
 (** {2 constructors} *)
 
@@ -66,7 +66,7 @@ val add_tdecl : task -> tdecl -> task
 
 val use_export : task -> theory -> task
 val clone_export : task -> theory -> th_inst -> task
-val add_meta : task -> string -> meta_arg list -> task
+val add_meta : task -> meta -> meta_arg list -> task
 
 (** {2 declaration constructors + add_decl} *)
 
@@ -97,17 +97,17 @@ val task_goal  : task -> prsymbol
 
 (* special selector for metaproperties of a single ident *)
 
-exception NotTaggingMeta of string
+exception NotTaggingMeta of meta
 
-val find_tagged_ts : string -> tdecl_set -> Sts.t -> Sts.t
-val find_tagged_ls : string -> tdecl_set -> Sls.t -> Sls.t
-val find_tagged_pr : string -> tdecl_set -> Spr.t -> Spr.t
+val find_tagged_ts : meta -> tdecl_set -> Sts.t -> Sts.t
+val find_tagged_ls : meta -> tdecl_set -> Sls.t -> Sls.t
+val find_tagged_pr : meta -> tdecl_set -> Spr.t -> Spr.t
 
 (* special selector for exclusive metaproperties *)
 
-exception NotExclusiveMeta of string
+exception NotExclusiveMeta of meta
 
-val get_meta_exc : string -> tdecl_set -> meta_arg list option
+val get_meta_excl : meta -> tdecl_set -> meta_arg list option
 
 (* exceptions *)
 

src/core/theory.ml

@@ -96,32 +96,57 @@ type meta_arg =
   | MAstr of string
   | MAint of int
 
-exception KnownMeta of string
+type meta = {
+  meta_tag : int;
+  meta_name : string;
+  meta_arg_type : meta_arg_type list;
+  meta_excl : bool;
+}
+
+module SMmeta = StructMake(struct type t = meta let tag m = m.meta_tag end)
+module Smeta = SMmeta.S
+module Mmeta = SMmeta.M
+module Hmeta = SMmeta.H
+
+let meta_equal m1 m2 = m1.meta_tag = m2.meta_tag
+
+exception KnownMeta of meta
 exception UnknownMeta of string
-exception BadMetaArity of string * int * int
-exception MetaTypeMismatch of string * meta_arg_type * meta_arg_type
+exception BadMetaArity of meta * int * int
+exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
 
+let meta_tag = let c =  ref (-1) in
+               fun () -> incr c; !c
 let meta_table = Hashtbl.create 17
-let meta_excl  = Hashtbl.create 17
 
-let register_meta s al =
-  begin try
+let register_meta s al excl =
+  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 end;
-  s
-
-let register_meta_excl s al =
-  Hashtbl.add meta_excl s ();
-  register_meta s al
+    if al <> al'.meta_arg_type ||
+      excl <> al'.meta_excl
+    then raise (KnownMeta al')
+    else al'
+  with Not_found -> 
+    let meta = { meta_tag = meta_tag ();
+                 meta_arg_type = al;
+                 meta_name = s;
+                 meta_excl = excl} in
+    Hashtbl.add meta_table s meta;
+    meta
+
+let register_meta_excl s al = register_meta s al true
+
+let register_meta s al = register_meta s al false
 
 let lookup_meta s =
   try Hashtbl.find meta_table s
   with Not_found -> raise (UnknownMeta s)
 
-let is_meta_excl s = Hashtbl.mem meta_excl s
+let is_meta_excl m = m.meta_excl
+let meta_arg_type m = m.meta_arg_type
+let meta_name m = m.meta_name
 
-let list_metas () = Hashtbl.fold (fun k v acc -> (k,v)::acc) meta_table []
+let list_metas () = Hashtbl.fold (fun _ v acc -> v::acc) meta_table []
 
 
 (** Theory *)
@@ -144,7 +169,7 @@ and tdecl_node =
   | Decl  of decl
   | Use   of theory
   | Clone of theory * tysymbol Mts.t * lsymbol Mls.t * prsymbol Mpr.t
-  | Meta  of string * meta_arg list
+  | Meta  of meta * meta_arg list
 
 (** Theory declarations *)
 
@@ -640,19 +665,16 @@ let get_meta_arg_type = function
   | MAstr _ -> MTstring
   | MAint _ -> MTint
 
-let create_meta s al =
-  let atl = try Hashtbl.find meta_table s
-    with Not_found -> raise (UnknownMeta s)
-  in
+let create_meta m al =
   let get_meta_arg at a =
     let mt = get_meta_arg_type a in
-    if at = mt then a else raise (MetaTypeMismatch (s,at,mt))
+    if at = mt then a else raise (MetaTypeMismatch (m,at,mt))
   in
-  let al = try List.map2 get_meta_arg atl al
+  let al = try List.map2 get_meta_arg m.meta_arg_type al
     with Invalid_argument _ ->
-      raise (BadMetaArity (s, List.length atl, List.length al))
+      raise (BadMetaArity (m, List.length m.meta_arg_type, List.length al))
   in
-  mk_tdecl (Meta (s,al))
+  mk_tdecl (Meta (m,al))
 
 let add_meta uc s al = add_tdecl uc (create_meta s al)
 
@@ -715,15 +737,16 @@ let () = Exn_printer.register
       Format.fprintf fmt "Symbol %s is already defined in the current scope" s
   | UnknownMeta s ->
       Format.fprintf fmt "Unknown metaproperty %s" s
-  | KnownMeta s ->
+  | KnownMeta m ->
       Format.fprintf fmt "Metaproperty %s is already registered with \
-        a conflicting signature" s
-  | BadMetaArity (s,i1,i2) ->
+        a conflicting signature" m.meta_name
+  | BadMetaArity (m,i1,i2) ->
       Format.fprintf fmt "Metaproperty %s requires %d arguments but \
-        is applied to %d" s i1 i2
-  | MetaTypeMismatch (s,t1,t2) ->
+        is applied to %d" m.meta_name i1 i2
+  | MetaTypeMismatch (m,t1,t2) ->
       Format.fprintf fmt "Metaproperty %s expects %a argument but \
-        is applied to %a" s print_meta_arg_type t1 print_meta_arg_type t2
+        is applied to %a"
+        m.meta_name print_meta_arg_type t1 print_meta_arg_type t2
   | _ -> raise exn
   end
 

src/core/theory.mli

@@ -54,13 +54,23 @@ type meta_arg =
   | MAstr of string
   | MAint of int
 
-val register_meta      : string -> meta_arg_type list -> string
-val register_meta_excl : string -> meta_arg_type list -> string
+type meta
 
-val lookup_meta  : string -> meta_arg_type list
-val is_meta_excl : string -> bool
+module Smeta : Set.S with type elt = meta
+module Mmeta : Map.S with type key = meta
+module Hmeta : Hashtbl.S with type key = meta
 
-val list_metas : unit -> (string * meta_arg_type list) list
+val meta_equal : meta -> meta -> bool
+
+val register_meta      : string -> meta_arg_type list -> meta
+val register_meta_excl : string -> meta_arg_type list -> meta
+val lookup_meta        : string -> meta
+
+val meta_name     : meta -> string
+val meta_arg_type : meta -> meta_arg_type list
+val is_meta_excl  : meta -> bool
+
+val list_metas : unit -> meta list
 
 (** Theory *)
 
@@ -82,7 +92,7 @@ and tdecl_node = private
   | Decl  of decl
   | Use   of theory
   | Clone of theory * tysymbol Mts.t * lsymbol Mls.t * prsymbol Mpr.t
-  | Meta  of string * meta_arg list
+  | Meta  of meta * meta_arg list
 
 module Stdecl : Set.S with type elt = tdecl
 module Mtdecl : Map.S with type key = tdecl
@@ -152,9 +162,9 @@ val create_null_clone : theory -> tdecl
 
 (** Meta *)
 
-val create_meta : string -> meta_arg list -> tdecl
+val create_meta : meta -> meta_arg list -> tdecl
 
-val add_meta : theory_uc -> string -> meta_arg list -> theory_uc
+val add_meta : theory_uc -> meta -> meta_arg list -> theory_uc
 
 val clone_meta : tdecl -> theory -> tdecl -> tdecl
 (* [clone_meta td_meta th td_clone] produces from [td_meta]
@@ -177,8 +187,8 @@ exception CloseTheory
 exception NoOpenedNamespace
 exception ClashSymbol of string
 
-exception KnownMeta of string
+exception KnownMeta of meta
 exception UnknownMeta of string
-exception BadMetaArity of string * int * int
-exception MetaTypeMismatch of string * meta_arg_type * meta_arg_type
+exception BadMetaArity of meta * int * int
+exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
 

src/core/trans.ml

@@ -54,7 +54,8 @@ let fold fn v =
   let rewind acc task =
 (*
     Format.printf "%c%d." (match task.task_decl.td_node with
-      Decl _ -> 'D' | Clone _ -> 'C' | Use _ -> 'U' | Meta _ -> 'M') task.task_tag;
+      Decl _ -> 'D' | Clone _ -> 'C' 
+  | Use _ -> 'U' | Meta _ -> 'M') task.task_tag;
 *)
     let acc = fn task acc in
     WHtask.set h task acc;
@@ -164,10 +165,10 @@ let on_theories tl fn =
 
 let on_metas tl fn =
   let rec pass acc = function
-    | t::tl -> on_meta t (fun st -> pass (Mstr.add t st acc) tl)
+    | t::tl -> on_meta t (fun st -> pass (Mmeta.add t st acc) tl)
     | []    -> fn acc
   in
-  pass Mstr.empty tl
+  pass Mmeta.empty tl
 
 let on_theories_metas thl tl fn =
   on_theories thl (fun cm -> on_metas tl (fn cm))

src/core/trans.mli

@@ -70,12 +70,12 @@ val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
 (* dependent transformatons *)
 
 val on_theory : theory -> (tdecl_set -> 'a trans) -> 'a trans
-val on_meta   : string -> (tdecl_set -> 'a trans) -> 'a trans
+val on_meta   : meta -> (tdecl_set -> 'a trans) -> 'a trans
 
 val on_theories : theory list -> (clone_map -> 'a trans) -> 'a trans
-val on_metas    : string list -> (meta_map  -> 'a trans) -> 'a trans
+val on_metas    : meta list -> (meta_map  -> 'a trans) -> 'a trans
 
-val on_theories_metas : theory list -> string list ->
+val on_theories_metas : theory list -> meta list ->
                         (clone_map -> meta_map -> 'a trans) -> 'a trans
 
 (** {2 Registration} *)

src/driver/driver.ml

@@ -144,7 +144,8 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
           | PMAstr s -> MAstr s
           | PMAint i -> MAint i
         in
-        let td = create_meta s (List.map convert al) in
+        let m = lookup_meta s in
+        let td = create_meta m (List.map convert al) in
         add_meta th td (if c then meta_cl else meta)
   in
   let add_local th (loc,rule) =

src/main.ml

@@ -78,7 +78,11 @@ let add_opt_goal x = match !opt_theory with
 
 let add_opt_trans x = opt_trans := x::!opt_trans
 
-let add_opt_meta meta_name meta_arg =
+let add_opt_meta meta =
+  let meta_name, meta_arg = 
+    let index = String.index meta '=' in
+    (String.sub meta 0 index),
+    (String.sub meta (index+1) (String.length meta - (index + 1))) in
   opt_metas := (meta_name,meta_arg)::!opt_metas
 
 let opt_config = ref None
@@ -141,11 +145,8 @@ let option_list = Arg.align [
       "<MiB> Set the prover's memory limit (default: no limit)";
   "--memlimit", Arg.Int (fun i -> opt_timelimit := Some i),
       " same as -m";
-  "-M", 
-  begin let meta_opt = ref "" in 
-        Arg.Tuple ([Arg.Set_string meta_opt;
-                    Arg.String (fun s -> add_opt_meta !meta_opt s)]) end,
-    "<meta_name>,<string> Add a meta option to each tasks";
+  "-M", Arg.String add_opt_meta,
+    "<meta_name>=<string> Add a meta option to each tasks";
   "-D", Arg.String (fun s -> opt_driver := Some s),
       "<file> Specify a prover's driver (conflicts with -P)";
   "--driver", Arg.String (fun s -> opt_driver := Some s),
@@ -214,15 +215,15 @@ let () =
   end;
   if !opt_list_metas then begin
     let metas = list_metas () in
-    let filter (s,args) =
-      match args with
-        | [MTstring] -> is_meta_excl s
-        | _ -> false in
-    let metas = List.filter filter metas in
-    let metas = List.map fst metas in
+    let fold acc m =
+      match meta_arg_type m with
+        | [MTstring] when is_meta_excl m -> Smeta.add m acc
+        | _ -> acc in
+    let metas = List.fold_left fold Smeta.empty metas in
     printf "@[<hov 2>Known metas:@\n%a@]@\n@."
-      (Pp.print_list Pp.newline Pp.string)
-      (List.sort String.compare metas)
+      (Pp.print_iter1 Smeta.iter Pp.newline 
+         (fun fmt m -> pp_print_string fmt (meta_name m)))
+      metas
   end;
   if !opt_list_transforms || !opt_list_printers || !opt_list_provers ||
      !opt_list_formats || !opt_list_metas
@@ -280,7 +281,9 @@ let () =
       opt_driver := Some prover.driver
   | None ->
     () end;
-  let add_meta task (meta,s) = add_meta task meta [MAstr s] in
+  let add_meta task (meta,s) = 
+    let meta = lookup_meta meta in
+    add_meta task meta [MAstr s] in
   opt_task := List.fold_left add_meta !opt_task !opt_metas
 
 let timelimit = match !opt_timelimit with

src/parser/typing.ml

@@ -950,7 +950,9 @@ and add_decl env lenv th = function
         | PMAint i -> MAint (int_of_string i)
       in
       let al = List.map convert al in
-      begin try add_meta th s al
+      begin try 
+              let m = lookup_meta s in
+              add_meta th m al
       with e -> raise (Loc.Located (loc,e)) end
 
 and type_and_add_theory env lenv pt =

src/printer/why3.ml

@@ -387,9 +387,9 @@ let print_tdecl fmt td = match td.td_node with
         print_th th (print_list comma print_inst_ts) tm
                     (print_list comma print_inst_ls) lm
                     (print_list comma print_inst_pr) pm
-  | Meta (t,al) ->
+  | Meta (m,al) ->
       fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
-        t (print_list comma print_meta_arg) al
+        (meta_name m) (print_list comma print_meta_arg) al
 
 let print_task pr thpr syn fmt task =
   forget_all ();

src/transform/eliminate_algebraic.mli

@@ -23,4 +23,4 @@ val eliminate_compiled_algebraic : Task.task Trans.trans
 
 val eliminate_algebraic : Task.task Trans.trans
 
-val meta_enum : string
+val meta_enum : Theory.meta

src/transform/encoding_decorate.mli

@@ -23,4 +23,4 @@
     Jean-Francois Couchot et Stephane Lescuyer *)
 
 val why_filename : string list
-val meta_kept : string
+val meta_kept : Theory.meta

src/transform/encoding_instantiate.ml

@@ -532,7 +532,7 @@ let mono_in_mono = Trans.tdecl mono_in_mono None
 
 let get_kept =
   Trans.on_meta meta_level (fun tds ->
-    match get_meta_exc meta_level tds with
+    match get_meta_excl meta_level tds with
       | None | Some [MAstr "goal"] -> mono_in_goal
       | Some [MAstr "kept"] -> Trans.identity
       | Some [MAstr "all"] -> mono_in_def
@@ -541,8 +541,9 @@ let get_kept =
 
 
 let create_trans_complete metas =
-  let tds_kept = Mstr.find meta_kept metas in
-  let complete = get_meta_exc meta_complete (Mstr.find meta_complete metas) in
+  let tds_kept = Mmeta.find meta_kept metas in
+  let complete = get_meta_excl meta_complete 
+    (Mmeta.find meta_complete metas) in
   let task = use_export None builtin_theory in
   let tenv = match complete with
     | None | Some [MAstr "yes"] -> Complete

src/transform/encoding_simple.mli

@@ -17,5 +17,5 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val meta_kept : string
+val meta_kept : Theory.meta