Commit bcd79af4 authored by MARCHE Claude's avatar MARCHE Claude

separate the 'search' command from the naming tables

We do not record anymore the map id_decl in naming_tables

names_table renamed into naming_table, seems better to me
parent 6c4b0d6d
......@@ -35,7 +35,7 @@ type printer_mapping = {
}
type printer_args = {
name_table : names_table option;
name_table : Trans.naming_table option;
do_intros : bool;
env : Env.env;
prelude : prelude;
......
......@@ -36,7 +36,7 @@ type printer_mapping = {
}
type printer_args = {
name_table : names_table option;
name_table : Trans.naming_table option;
do_intros : bool;
env : Env.env;
prelude : prelude;
......
......@@ -342,25 +342,6 @@ let on_tagged_pr t task =
let tds = find_meta_tds task t in
Stdecl.fold add tds.tds_set Spr.empty
(* Printing tasks *)
type id_decl = (Decl.decl list) Ident.Mid.t
type names_table = {
namespace : namespace;
known_map : known_map;
printer : ident_printer;
(* Associate an id to a list of declarations in which it is used *)
id_decl : id_decl;
}
let empty_names_table = {
namespace = empty_ns;
known_map = Mid.empty;
printer = create_ident_printer [];
id_decl = Mid.empty;
}
exception Bad_name_table of string
(* Exception reporting *)
......@@ -373,8 +354,6 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" m.meta_name
| NotExclusiveMeta m ->
Format.fprintf fmt "Metaproperty '%s' is not exclusive" m.meta_name
| Bad_name_table s ->
Format.fprintf fmt "Names table associated to task was not generated in %s" s
| _ -> raise exn)
(* task1 : prefix
......
......@@ -126,23 +126,8 @@ val on_tagged_ts : meta -> task -> Sts.t
val on_tagged_ls : meta -> task -> Sls.t
val on_tagged_pr : meta -> task -> Spr.t
(** Printing tasks *)
type id_decl = (Decl.decl list) Ident.Mid.t
type names_table = {
namespace : namespace;
known_map : known_map;
printer : ident_printer;
(* Associate an id to a list of declarations in which it is used *)
id_decl : id_decl;
}
val empty_names_table : names_table
(** Exceptions *)
exception Bad_name_table of string
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta
......
......@@ -333,10 +333,26 @@ let list_transforms () =
let list_transforms_l () =
Hstr.fold (fun k (desc,_) acc -> (k, desc)::acc) transforms_l []
(** transformations with arguments *)
type trans_with_args = string list -> Env.env -> Task.names_table -> task trans
type trans_with_args_l = string list -> Env.env -> Task.names_table -> task tlist
type naming_table = {
namespace : namespace;
known_map : known_map;
printer : Ident.ident_printer;
}
exception Bad_name_table of string
let empty_naming_table = {
namespace = empty_ns;
known_map = Ident.Mid.empty;
printer = Ident.create_ident_printer [];
}
type trans_with_args = string list -> Env.env -> naming_table -> task trans
type trans_with_args_l = string list -> Env.env -> naming_table -> task tlist
let transforms_with_args = Hstr.create 17
let transforms_with_args_l = Hstr.create 17
......@@ -452,4 +468,6 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| TransFailure (s,e) ->
Format.fprintf fmt "Failure in transformation %s@\n%a" s
Exn_printer.exn_printer e
| Bad_name_table s ->
Format.fprintf fmt "Names table associated to task was not generated in %s" s
| e -> raise e)
......@@ -164,8 +164,23 @@ val named : string -> 'a trans -> 'a trans
*)
type trans_with_args = string list -> Env.env -> Task.names_table -> task trans
type trans_with_args_l = string list -> Env.env -> Task.names_table -> task tlist
(* In order to interpret, that is type, string arguments as symbols or terms,
a transformation needs a [naming_table], which is used for looking up strings (the namespace)
and also for printing (the printer), both must be coherent *)
type naming_table = {
namespace : namespace;
known_map : known_map;
printer : Ident.ident_printer;
}
exception Bad_name_table of string
val empty_naming_table : naming_table
type trans_with_args = string list -> Env.env -> naming_table -> task trans
type trans_with_args_l = string list -> Env.env -> naming_table -> task tlist
val list_transforms_with_args : unit -> (string * Pp.formatted) list
val list_transforms_with_args_l : unit -> (string * Pp.formatted) list
......@@ -188,5 +203,5 @@ val list_trans : unit -> string list
val apply_transform : string -> Env.env -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n, directly.*)
val apply_transform_args : string -> Env.env -> string list -> Task.names_table -> task -> task list
val apply_transform_args : string -> Env.env -> string list -> naming_table -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n or a trans with args, directly *)
......@@ -47,12 +47,12 @@ val print_task :
?old : in_channel ->
?cntexample : bool ->
?do_intros : bool ->
?name_table: Task.names_table ->
?name_table: Trans.naming_table ->
driver -> Format.formatter -> Task.task -> unit
val print_theory :
?old : in_channel ->
?name_table: Task.names_table ->
?name_table: Trans.naming_table ->
driver -> Format.formatter -> Theory.theory -> unit
(** produce a realization of the given theory using the given driver *)
......@@ -62,7 +62,7 @@ val prove_task :
?cntexample : bool ->
?old : string ->
?inplace : bool ->
?name_table : Task.names_table ->
?name_table : Trans.naming_table ->
driver -> Task.task -> Call_provers.prover_call
(** Split the previous function in two simpler functions *)
......@@ -70,7 +70,7 @@ val prepare_task : cntexample:bool -> driver -> Task.task -> Task.task
val print_task_prepared :
?old : in_channel ->
?name_table: Task.names_table ->
?name_table: Trans.naming_table ->
?do_intros : bool ->
driver -> Format.formatter -> Task.task -> Printer.printer_mapping
......@@ -79,7 +79,7 @@ val prove_task_prepared :
limit : Call_provers.resource_limit ->
?old : string ->
?inplace : bool ->
?name_table : Task.names_table ->
?name_table : Trans.naming_table ->
driver -> Task.task -> Call_provers.prover_call
......
......@@ -19,7 +19,6 @@ open Term
open Decl
open Printer
open Theory
open Task
(* Labels and locations can be printed by setting the appropriate flags *)
let debug_print_labels = Debug.register_info_flag "print_labels"
......@@ -28,7 +27,7 @@ let debug_print_labels = Debug.register_info_flag "print_labels"
let debug_print_locs = Debug.register_info_flag "print_locs"
~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
let id_unique tables id = id_unique_label tables.printer id
let id_unique tables id = id_unique_label tables.Trans.printer id
(*
let forget_tvs () =
......@@ -49,7 +48,7 @@ let print_tv tables fmt tv =
let print_vs tables fmt vs =
fprintf fmt "%s" (id_unique tables vs.vs_name)
let forget_var tables vs = forget_id tables.printer vs.vs_name
let forget_var tables vs = forget_id tables.Trans.printer vs.vs_name
(* theory names always start with an upper case letter *)
let print_th tables fmt th =
......@@ -102,7 +101,7 @@ let print_ty = print_ty_node false
(** Forgetting function for stability of errors *)
let print_forget_vsty tables fmt v =
if (Ident.known_id tables.printer v.vs_name) then
if (Ident.known_id tables.Trans.printer v.vs_name) then
fprintf fmt "%a: %a" (print_vs tables) v (print_ty tables) v.vs_ty
else
begin
......@@ -434,7 +433,7 @@ let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
(* forget_all (); *)
let tables = match args.name_table with
| None -> empty_names_table (* raise (Bad_name_table "Why3printer.print_task")*)
| None -> Trans.empty_naming_table (* raise (Bad_name_table "Why3printer.print_task")*)
| Some tables -> tables in
print_prelude fmt args.prelude;
fprintf fmt "theory Task@\n";
......@@ -493,7 +492,7 @@ let print_sequent args ?old:_ fmt task =
info := {info_syn = Discriminate.get_syntax_map task;
itp = true};
let tables = match args.name_table with
| None -> empty_names_table (* raise (Bad_name_table "Why3printer.print_sequent") *)
| None -> Trans.empty_naming_table (* raise (Bad_name_table "Why3printer.print_sequent") *)
| Some tables -> tables in
(* let tables = build_name_tables task in *)
let ut = Task.used_symbols (Task.used_theories task) in
......
......@@ -30,12 +30,12 @@
*)
val print_ls : Task.names_table -> Format.formatter -> Term.lsymbol -> unit
val print_tv : Task.names_table -> Format.formatter -> Ty.tvsymbol -> unit
val print_ts : Task.names_table -> Format.formatter -> Ty.tysymbol -> unit
val print_forget_vsty : Task.names_table -> Format.formatter -> Term.vsymbol -> unit
val print_pr : Task.names_table -> Format.formatter -> Decl.prsymbol -> unit
val print_pat : Task.names_table -> Format.formatter -> Term.pattern -> unit
val print_ty : Task.names_table -> Format.formatter -> Ty.ty -> unit
val print_term : Task.names_table -> Format.formatter -> Term.term -> unit
val print_decl : Task.names_table -> Format.formatter -> Decl.decl -> unit
val print_ls : Trans.naming_table -> Format.formatter -> Term.lsymbol -> unit
val print_tv : Trans.naming_table -> Format.formatter -> Ty.tvsymbol -> unit
val print_ts : Trans.naming_table -> Format.formatter -> Ty.tysymbol -> unit
val print_forget_vsty : Trans.naming_table -> Format.formatter -> Term.vsymbol -> unit
val print_pr : Trans.naming_table -> Format.formatter -> Decl.prsymbol -> unit
val print_pat : Trans.naming_table -> Format.formatter -> Term.pattern -> unit
val print_ty : Trans.naming_table -> Format.formatter -> Ty.ty -> unit
val print_term : Trans.naming_table -> Format.formatter -> Term.term -> unit
val print_decl : Trans.naming_table -> Format.formatter -> Decl.decl -> unit
......@@ -494,7 +494,7 @@ let schedule_transformation_r c id name args ~callback =
let apply_trans () =
let task = get_task c.controller_session id in
let table = match get_table c.controller_session id with
| None -> raise (Task.Bad_name_table "Controller_itp.schedule_transformation_r")
| None -> raise (Trans.Bad_name_table "Controller_itp.schedule_transformation_r")
| Some table -> table in
begin
try
......
......@@ -138,8 +138,8 @@ exception Number_of_arguments
let print_id s tables =
(* let tables = Args_wrapper.build_name_tables task in*)
let km = tables.Task.known_map in
let id = try find_any_id tables.Task.namespace s with
let km = tables.Trans.known_map in
let id = try find_any_id tables.Trans.namespace s with
| Not_found -> raise (Undefined_id s) in
let d =
try Ident.Mid.find id km with
......@@ -149,13 +149,9 @@ let print_id s tables =
let search s tables =
(*let tables = Args_wrapper.build_name_tables task in*)
let id_decl = tables.Task.id_decl in
let id = try find_any_id tables.Task.namespace s with
let id = try find_any_id tables.Trans.namespace s with
| Not_found -> raise (Undefined_id s) in
let l =
try Ident.Mid.find id id_decl with
| Not_found -> raise Not_found (* Should not happen *)
in
let l = Args_wrapper.search tables.Trans.known_map [id] in
let s_id = print_id s tables in
s_id ^ (Pp.string_of (Pp.print_list Pp.newline2 (Why3printer.print_decl tables)) l)
......@@ -171,7 +167,7 @@ let search_id _cont task args =
type query =
| Qnotask of (Controller_itp.controller -> string list -> string)
| Qtask of (Controller_itp.controller -> Task.names_table -> string list -> string)
| Qtask of (Controller_itp.controller -> Trans.naming_table -> string list -> string)
let help_on_queries fmt commands =
let l = Stdlib.Hstr.fold (fun c (h,_) acc -> (c,h)::acc) commands [] in
......@@ -333,7 +329,7 @@ let interp commands_table config cont id s =
| Qtask _, None -> QError "please select a goal first"
| Qtask f, Some id ->
let table = match Session_itp.get_table cont.Controller_itp.controller_session id with
| None -> raise (Task.Bad_name_table "Server_utils.interp")
| None -> raise (Trans.Bad_name_table "Server_utils.interp")
| Some table -> table in
let s = try Query (f cont table args) with
| Undefined_id s -> QError ("No existing id corresponding to " ^ s)
......
......@@ -24,11 +24,11 @@ exception Number_of_arguments
type query =
| Qnotask of (Controller_itp.controller -> string list -> string)
| Qtask of (Controller_itp.controller -> Task.names_table -> string list -> string)
| Qtask of (Controller_itp.controller -> Trans.naming_table -> string list -> string)
val print_id: 'a -> Task.names_table -> string list -> string
val search_id: 'a -> Task.names_table -> string list -> string
val print_id: 'a -> Trans.naming_table -> string list -> string
val search_id: 'a -> Trans.naming_table -> string list -> string
val list_provers: Controller_itp.controller -> _ -> string
val list_transforms: unit -> (string * Pp.formatted) list
......
......@@ -48,7 +48,7 @@ type proof_node = {
proofn_name : Ident.ident;
proofn_expl : string;
proofn_task : Task.task;
proofn_table : Task.names_table option;
proofn_table : Trans.naming_table option;
proofn_parent : proof_parent;
proofn_checksum : Termcode.checksum option;
proofn_shape : Termcode.shape;
......@@ -1358,7 +1358,7 @@ let add_registered_transformation s env old_tr goal_id =
Debug.dprintf debug "[merge_theory] trans not found@.";
let task = goal.proofn_task in
let tables = match goal.proofn_table with
| None -> raise (Task.Bad_name_table "Session_itp.add_registered_transformation")
| None -> raise (Trans.Bad_name_table "Session_itp.add_registered_transformation")
| Some tables -> tables in
let subgoals = Trans.apply_transform_args old_tr.transf_name env old_tr.transf_args tables task in
graft_transf s goal_id old_tr.transf_name old_tr.transf_args subgoals
......
......@@ -88,7 +88,7 @@ val is_below: session -> any -> any -> bool
type proof_parent = Trans of transID | Theory of theory
val get_task : session -> proofNodeID -> Task.task
val get_table : session -> proofNodeID -> Task.names_table option
val get_table : session -> proofNodeID -> Trans.naming_table option
val get_transformations : session -> proofNodeID -> transID list
val get_proof_attempt_ids :
......
......@@ -50,7 +50,7 @@ type symb =
| Pr of prsymbol
(* [add_unsafe s id tables] Add (s, id) to tables without any checking. *)
let add_unsafe (s: string) (id: symb) (tables: names_table) : names_table =
let add_unsafe (s: string) (id: symb) (tables: naming_table) : naming_table =
match id with
| Ts ty ->
{tables with
......@@ -66,7 +66,7 @@ let add_unsafe (s: string) (id: symb) (tables: names_table) : names_table =
}
(* Adds symbols that are introduced to a constructor *)
let constructor_add (cl: constructor list) tables : names_table =
let constructor_add (cl: constructor list) tables : naming_table =
List.fold_left
(fun tables ((ls, cl): constructor) ->
let tables = List.fold_left
......@@ -93,53 +93,9 @@ let ind_decl_add il tables =
il
tables
let rec insert l d =
match l with
| hd :: tl -> if hd == d then l else hd :: insert tl d
| [] -> [d]
let add_decls_id id d tables =
let l = try (Ident.Mid.find id tables.id_decl) with
| Not_found -> [] in
{tables with id_decl = Ident.Mid.add id (insert l d) tables.id_decl}
(* [add_id tables d t] To all identifiants id used in t, adds the associated
declaration d in the table.id_decl *)
let rec add_id tables d t =
match t.t_node with
| Tvar _ -> tables
| Tconst _ | Ttrue | Tfalse -> tables
| Tapp (l, tl) ->
let tables = add_decls_id l.ls_name d tables in
List.fold_left (fun tables t -> add_id tables d t) tables tl
| Tlet (t, tb) ->
let tables = add_id tables d t in
let (_v1, t1) = t_open_bound tb in
add_id tables d t1
| Tcase (t, tbl) ->
let tables = add_id tables d t in
List.fold_left (fun tables ob ->
let (_pat, t) = t_open_branch ob in
add_id tables d t) tables tbl
| Teps (tb) ->
let (_v, t) = t_open_bound tb in
add_id tables d t
| Tquant (_, tq) ->
let (_vl, _, t) = t_open_quant tq in
add_id tables d t
| Tbinop (_, t1, t2) ->
let tables = add_id tables d t1 in
add_id tables d t2
| Tnot (t) ->
add_id tables d t
| Tif (t1, t2, t3) ->
let tables = add_id tables d t1 in
let tables = add_id tables d t2 in
add_id tables d t3
(* [add d printer tables] Adds all new declaration of symbol inside d to tables.
It uses printer to give them a unique name and also register these new names in printer *)
let add (d: decl) (tables: names_table): names_table =
let add (d: decl) (tables: naming_table): naming_table =
match d.d_node with
| Dtype ty ->
(* only current symbol is new in the declaration (see create_ty_decl) *)
......@@ -181,22 +137,19 @@ let add (d: decl) (tables: names_table): names_table =
ind_decl_add tables ind)
tables
il
| Dprop (_, pr, t) ->
| Dprop (_, pr, _t) ->
(* Only pr is new in Dprop (see create_prop_decl) *)
let id = pr.pr_name in
let s = id_unique tables.printer id in
let tables = add_unsafe s (Pr pr) tables in
add_id tables d t
add_unsafe s (Pr pr) tables
let build_name_tables task : names_table =
let build_name_tables task : naming_table =
let pr = fresh_printer () in
let km = Task.task_known task in
let empty_decls = Ident.Mid.empty in
let tables = {
namespace = empty_ns;
known_map = km;
printer = pr;
id_decl = empty_decls
} in
(* We want conflicting names to be named as follows:
names closer to the goal should be named with lowest
......@@ -206,6 +159,38 @@ let build_name_tables task : names_table =
let l = Mid.fold (fun _id d acc -> d :: acc) km [] in
List.fold_left (fun tables d -> add d tables) tables l
(* searching ids in declarations *)
let occurs_in_type id = ty_s_any (fun ts -> Ident.id_equal ts.Ty.ts_name id)
let occurs_in_term id =
t_s_any (occurs_in_type id) (fun ls -> Ident.id_equal id ls.ls_name)
let occurs_in_constructor _id _c = false
let occurs_in_defn id (_,def) =
let (_vl,t) = open_ls_defn def in occurs_in_term id t
let occurs_in_ind_decl id (_,clauses) =
List.exists (fun (_,t) -> occurs_in_term id t) clauses
let occurs_in_decl d id =
match d.d_node with
| Dtype ts -> Ident.id_equal ts.Ty.ts_name id
| Ddata dl ->
List.exists
(fun ((_,c): data_decl) -> List.exists (occurs_in_constructor id) c)
dl
| Dparam _ls -> false
| Dlogic dl -> List.exists (occurs_in_defn id) dl
| Dind (_is, il) -> List.exists (occurs_in_ind_decl id) il
| Dprop (k, _, t) -> k = Paxiom && occurs_in_term id t
let search km idl =
Mid.fold
(fun _id d acc ->
if List.for_all (occurs_in_decl d) idl then d :: acc else acc) km []
(************* wrapper *************)
......@@ -382,7 +367,7 @@ let rec print_type : type a b. (a, b) trans_typ -> string =
exception Unnecessary_arguments of string list
let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> names_table -> task -> b =
let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> naming_table -> task -> b =
fun t f l env tables task ->
match t, l with
| Ttrans, []-> apply f task
......@@ -476,7 +461,8 @@ let wrap_l : type a. (a, task list) trans_typ -> a -> trans_with_args_l =
let wrap : type a. (a, task) trans_typ -> a -> trans_with_args =
fun t f l env tables -> Trans.store (wrap_to_store t f l env tables)
let wrap_any : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> Task.names_table -> b trans =
let wrap_any : type a b. (a, b) trans_typ -> a -> string list -> Env.env ->
Trans.naming_table -> b trans =
fun t f l env tables -> Trans.store (wrap_to_store t f l env tables)
let wrap_and_register : type a b. desc:Pp.formatted -> string -> (a, b) trans_typ -> a -> unit =
......
......@@ -11,7 +11,11 @@ exception Arg_hyp_not_found of string
(** Pre-processing of tasks, to build unique names for all declared
identifiers of a task.*)
val build_name_tables : Task.task -> Task.names_table
val build_name_tables : Task.task -> Trans.naming_table
val search : Decl.known_map -> Ident.ident list -> Decl.decl list
(** [search km ids] returns the set of declarations from [km] that
contain all the identifiers [ids] *)
type symbol =
| Tstysymbol of Ty.tysymbol
......
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