Commit 8779c1b2 authored by Andrei Paskevich's avatar Andrei Paskevich

make Theory.meta a visible private record

parent fb04881a
......@@ -375,7 +375,7 @@ let print_tdecl fmt td = match td.td_node with
(print_list comma print_inst_pr) pm
| Meta (m,al) ->
fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
(meta_name m) (print_list comma print_meta_arg) al
m.meta_name (print_list comma print_meta_arg) al
let print_theory fmt th =
fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
......
......@@ -57,7 +57,7 @@ let mm_find mm t =
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
let mm_add mm t td = if t.meta_excl
then Mmeta.add t (tds_singleton td) mm
else Mmeta.add t (tds_add td (mm_find mm t)) mm
......@@ -216,7 +216,7 @@ let task_decls = task_fold (fun acc td ->
exception NotTaggingMeta of meta
let find_tagged_ts t tds acc =
begin match meta_arg_type t with
begin match t.meta_type with
| [MTtysymbol] -> ()
| _ -> raise (NotTaggingMeta t)
end;
......@@ -225,7 +225,7 @@ let find_tagged_ts t tds acc =
| _ -> assert false) tds.tds_set acc
let find_tagged_ls t tds acc =
begin match meta_arg_type t with
begin match t.meta_type with
| [MTlsymbol] -> ()
| _ -> raise (NotTaggingMeta t)
end;
......@@ -234,7 +234,7 @@ let find_tagged_ls t tds acc =
| _ -> assert false) tds.tds_set acc
let find_tagged_pr t tds acc =
begin match meta_arg_type t with
begin match t.meta_type with
| [MTprsymbol] -> ()
| _ -> raise (NotTaggingMeta t)
end;
......@@ -245,7 +245,7 @@ let find_tagged_pr t tds acc =
exception NotExclusiveMeta of meta
let get_meta_excl t tds =
if not (is_meta_excl t) then raise (NotExclusiveMeta t);
if not t.meta_excl then raise (NotExclusiveMeta t);
Stdecl.fold (fun td _ -> match td.td_node with
| Meta (s,arg) when s = t -> Some arg
| _ -> assert false) tds.tds_set None
......@@ -258,8 +258,8 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| GoalFound -> Format.fprintf fmt "The task already ends with a goal"
| GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
| NotTaggingMeta m ->
Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" (meta_name m)
Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" m.meta_name
| NotExclusiveMeta m ->
Format.fprintf fmt "Metaproperty '%s' is not exclusive" (meta_name m)
Format.fprintf fmt "Metaproperty '%s' is not exclusive" m.meta_name
| _ -> raise exn)
......@@ -97,13 +97,14 @@ type meta_arg =
| MAint of int
type meta = {
meta_tag : int;
meta_name : string;
meta_arg_type : meta_arg_type list;
meta_type : meta_arg_type list;
meta_excl : bool;
meta_tag : int;
}
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
......@@ -115,40 +116,35 @@ exception UnknownMeta of string
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 mk_meta =
let c = ref (-1) in
fun s al excl -> {
meta_name = s;
meta_type = al;
meta_excl = excl;
meta_tag = (incr c; !c) }
let register_meta s al excl =
try
let al' = Hashtbl.find meta_table s in
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 m = Hashtbl.find meta_table s in
if al = m.meta_type && excl = m.meta_excl then m
else raise (KnownMeta m)
with Not_found ->
let m = mk_meta s al excl in
Hashtbl.add meta_table s m;
m
let register_meta_excl s al = register_meta s al true
let register_meta s al = register_meta s al false
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 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 _ v acc -> v::acc) meta_table []
(** Theory *)
type theory = {
......@@ -670,9 +666,9 @@ let create_meta m al =
let mt = get_meta_arg_type a in
if at = mt then a else raise (MetaTypeMismatch (m,at,mt))
in
let al = try List.map2 get_meta_arg m.meta_arg_type al
let al = try List.map2 get_meta_arg m.meta_type al
with Invalid_argument _ ->
raise (BadMetaArity (m, List.length m.meta_arg_type, List.length al))
raise (BadMetaArity (m, List.length m.meta_type, List.length al))
in
mk_tdecl (Meta (m,al))
......
......@@ -54,7 +54,12 @@ type meta_arg =
| MAstr of string
| MAint of int
type meta
type meta = private {
meta_name : string;
meta_type : meta_arg_type list;
meta_excl : bool;
meta_tag : int;
}
module Smeta : Set.S with type elt = meta
module Mmeta : Map.S with type key = meta
......@@ -64,13 +69,9 @@ 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
val lookup_meta : string -> meta
val list_metas : unit -> meta list
(** Theory *)
......
......@@ -54,8 +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;
......
......@@ -79,7 +79,7 @@ let add_opt_goal x = match !opt_theory with
let add_opt_trans x = opt_trans := x::!opt_trans
let add_opt_meta meta =
let meta_name, meta_arg =
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
......@@ -175,15 +175,15 @@ let option_list = Arg.align [
" Stop after type checking";
"--debug", Arg.Set opt_debug,
" Set the debug flag";
"-a", Arg.String add_opt_trans,
"-a", Arg.String add_opt_trans,
"<transformation> Add a transformation to apply to the task" ;
"--apply-transform", Arg.String add_opt_trans,
"--apply-transform", Arg.String add_opt_trans,
" same as -a" ]
let () =
Arg.parse option_list add_opt_file usage_msg;
(* TODO? : Since drivers can dynlink ml code they can add printer,
(* TODO? : Since drivers can dynlink ml code they can add printer,
transformations, ... So drivers should be loaded before listing *)
if !opt_list_transforms then begin
printf "@[<hov 2>Transed non-splitting transformations:@\n%a@]@\n@."
......@@ -200,10 +200,10 @@ let () =
end;
if !opt_list_formats then begin
let print1 fmt s = fprintf fmt "%S" s in
let print fmt (p, l) =
let print fmt (p, l) =
fprintf fmt "%s [%a]" p (Pp.print_list Pp.comma print1) l
in
printf "@[<hov 2>Known input formats:@\n%a@]@."
printf "@[<hov 2>Known input formats:@\n%a@]@."
(Pp.print_list Pp.newline print)
(List.sort Pervasives.compare (Env.list_formats ()))
end;
......@@ -215,14 +215,14 @@ let () =
end;
if !opt_list_metas then begin
let metas = list_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 fold acc m = match m.meta_type with
| [MTstring] when m.meta_excl -> 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_iter1 Smeta.iter Pp.newline
(fun fmt m -> pp_print_string fmt (meta_name m)))
(Pp.print_iter1 Smeta.iter Pp.newline
(fun fmt m -> pp_print_string fmt m.meta_name))
metas
end;
if !opt_list_transforms || !opt_list_printers || !opt_list_provers ||
......@@ -281,7 +281,7 @@ let () =
opt_driver := Some prover.driver
| None ->
() end;
let add_meta task (meta,s) =
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
......@@ -330,16 +330,16 @@ let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
close_out cout
let do_tasks env drv fname tname th trans task =
let lookup acc t =
let lookup acc t =
(try t, Trans.singleton (Trans.lookup_transform t env) with
Trans.UnknownTrans _ -> t, Trans.lookup_transform_l t env) :: acc
in
let transl = List.fold_left lookup [] trans in
let apply tasks (s, tr) =
let apply tasks (s, tr) =
try
if debug then Format.eprintf "apply transformation %s@." s;
let l = List.fold_left
(fun acc task ->
let l = List.fold_left
(fun acc task ->
List.rev_append (Trans.apply tr task) acc) [] tasks in
List.rev l (* In order to keep the order for 1-1 transformation *)
with e when not debug ->
......@@ -364,12 +364,12 @@ let do_theory env drv fname tname th trans glist =
(pr,trans)::accm,accs
in
let drv = Util.of_option drv in
if Queue.is_empty glist
then
if Queue.is_empty glist
then
let tasks = List.rev (split_theory ~init:!opt_task th None) in
let do_tasks = do_tasks env drv fname tname th trans in
List.iter do_tasks tasks
else
else
let prtrans,prs = Queue.fold add ([],Decl.Spr.empty) glist in
let tasks = split_theory ~init:!opt_task th (Some prs) in
let recover_pr mpr task =
......@@ -408,13 +408,13 @@ let do_input env drv = function
in
let report = Env.report ?name:!opt_parser fname in
try
let m =
Env.read_channel ?name:!opt_parser ~debug:!opt_debug
let m =
Env.read_channel ?name:!opt_parser ~debug:!opt_debug
~parse_only:!opt_parse_only ~type_only:!opt_type_only
env fname cin
env fname cin
in
close_in cin;
if !opt_type_only then
if !opt_type_only then
()
else if Queue.is_empty tlist then
let glist = Queue.create () in
......@@ -423,7 +423,7 @@ let do_input env drv = function
Ident.Mid.iter do_th (Mnm.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_local_theory env drv fname m) tlist
with
with
| Loc.Located (loc, e) ->
eprintf "@[%a%a@]@." Loc.report_position loc report e; exit 1
| e ->
......
......@@ -950,9 +950,7 @@ and add_decl env lenv th = function
| PMAint i -> MAint (int_of_string i)
in
let al = List.map convert al in
begin try
let m = lookup_meta s in
add_meta th m al
begin try add_meta th (lookup_meta s) al
with e -> raise (Loc.Located (loc,e)) end
and type_and_add_theory env lenv pt =
......
......@@ -389,7 +389,7 @@ let print_tdecl fmt td = match td.td_node with
(print_list comma print_inst_pr) pm
| Meta (m,al) ->
fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
(meta_name m) (print_list comma print_meta_arg) al
m.meta_name (print_list comma print_meta_arg) al
let print_task pr thpr syn fmt task =
forget_all ();
......
......@@ -50,8 +50,7 @@ let enco_gen opt env =
try
(Hashtbl.find opt.table s) env
with Not_found -> failwith
(Format.sprintf "encoding : %s wrong argument %s"
(meta_name opt.meta) s))
(Format.sprintf "encoding : %s wrong argument %s" opt.meta.meta_name s))
let enco_select = enco_gen select_opt
let enco_kept = enco_gen kept_opt
......
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