Commit 157f4a5c authored by Andrei Paskevich's avatar Andrei Paskevich

Reworking tags and transformations, stage 2:

- dependent transformations (ones that depend on cloning history
  and/or metaproperties) have now the same type Trans.trans and
  can be registered via Trans, too.
- load_driver accumulates appropriate tdecls to be appended to
  tasks before transformation/printing.

At this moment, we have almost everything in place and are ready
to remove Register module (subsumed by Trans and Printer in core/)
and Prover module (its functions will move to Driver), and convert
all printers and transformations to use the new infrastructure. 

Not implemented yet:
- appending driver-imposed tdecls to tasks - when and where?
- metas-options - what is the best way to implement them?
- syntax/typing for metas in theories and drivers.
parent d31c675c
......@@ -489,9 +489,9 @@ let find_prop kn pr =
let find_prop_decl kn pr =
match (Mid.find pr.pr_name kn).d_node with
| Dind dl ->
| Dind dl ->
let test (_,l) = List.mem_assq pr l in
Pskip, List.assq pr (snd (List.find test dl))
Paxiom, List.assq pr (snd (List.find test dl))
| Dprop (k,_,f) -> k,f
| _ -> assert false
......
......@@ -150,9 +150,9 @@ let get_remove_set task =
| _ -> assert false
in
let s = Sid.empty in
let s = Stdecl.fold add (find_meta task meta_remove_type) s in
let s = Stdecl.fold add (find_meta task meta_remove_logic) s in
let s = Stdecl.fold add (find_meta task meta_remove_prop) s in
let s = Stdecl.fold add (find_meta task meta_remove_type).tds_set s in
let s = Stdecl.fold add (find_meta task meta_remove_logic).tds_set s in
let s = Stdecl.fold add (find_meta task meta_remove_prop).tds_set s in
s
let get_syntax_map task =
......@@ -161,8 +161,8 @@ let get_syntax_map task =
| _ -> assert false
in
let m = Mid.empty in
let m = Stdecl.fold add (find_meta task meta_syntax_type) m in
let m = Stdecl.fold add (find_meta task meta_syntax_logic) m in
let m = Stdecl.fold add (find_meta task meta_syntax_type).tds_set m in
let m = Stdecl.fold add (find_meta task meta_syntax_logic).tds_set m in
m
(** {2 exceptions to use in transformations and printers} *)
......
......@@ -24,10 +24,35 @@ open Term
open Decl
open Theory
(** Task *)
(** Clone and meta history *)
type tdecl_set = {
tds_set : Stdecl.t;
tds_tag : int;
}
module Hstds = Hashcons.Make (struct
type t = tdecl_set
let equal s1 s2 = Stdecl.equal s1.tds_set s2.tds_set
let hs_td td acc = Hashcons.combine acc td.td_tag
let hash s = Stdecl.fold hs_td s.tds_set 0
let tag n s = { s with tds_tag = n }
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)
type clone_map = Stdecl.t Mid.t
type meta_map = Stdecl.t Mstr.t
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mstr.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 -> 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
(** Task *)
type task = task_hd option
......@@ -74,24 +99,19 @@ 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 find_clone task th =
try Mid.find th.th_name (task_clone task) with Not_found -> Stdecl.empty
let find_meta task t =
try Mstr.find t (task_meta task) with Not_found -> Stdecl.empty
let find_clone task th = cm_find (task_clone task) th
let find_meta task t = mm_find (task_meta task) t
let add_decl task d td =
let kn = known_add_decl (task_known task) d in
mk_task td task kn (task_clone task) (task_meta task)
let add_clone task th td =
let st = Stdecl.add td (find_clone task th) in
let cl = Mid.add th.th_name st (task_clone task) in
let cl = cm_add (task_clone task) th td in
mk_task td task (task_known task) cl (task_meta task)
let add_meta task t td =
let st = Stdecl.add td (find_meta task t) in
let mt = Mstr.add t st (task_meta task) in
let mt = mm_add (task_meta task) t td in
mk_task td task (task_known task) (task_clone task) mt
(* add_decl with checks *)
......@@ -146,7 +166,7 @@ and flat_tdecl task td = match td.td_node with
and use_export task th =
let td = create_null_clone th in
if Stdecl.mem td (find_clone task th) then task else
if Stdecl.mem td (find_clone task th).tds_set then task else
let task = List.fold_left flat_tdecl task th.th_decls in
add_clone task th td
......@@ -185,18 +205,18 @@ let task_decls = task_fold (fun acc td ->
(* TO BE REMOVED *)
let old_task_clone task =
Mid.fold (fun _ -> Stdecl.fold (function
Mid.fold (fun _ x -> Stdecl.fold (function
| { td_node = Clone (_,cl) } ->
Mid.fold (fun id id' m ->
let s = try Mid.find id' m with Not_found -> Sid.empty in
Mid.add id' (Sid.add id s) m) cl
| _ -> assert false)) (task_clone task) Mid.empty
| _ -> assert false) x.tds_set) (task_clone task) Mid.empty
let old_task_use task =
Mid.fold (fun _ -> Stdecl.fold (function
Mid.fold (fun _ x -> Stdecl.fold (function
| { td_node = Clone (th,cl) } -> (fun m ->
if Mid.is_empty cl then Mid.add th.th_name th m else m)
| _ -> assert false)) (task_clone task) Mid.empty
| _ -> assert false) x.tds_set) (task_clone task) Mid.empty
let rec last_use task = match task with
| Some {task_decl={td_node=Clone(_,cl)}} when Mid.is_empty cl -> task
......
......@@ -24,10 +24,17 @@ open Term
open Decl
open Theory
(** Task *)
(** Clone and meta history *)
type tdecl_set = private {
tds_set : Stdecl.t;
tds_tag : int;
}
type clone_map = Stdecl.t Mid.t
type meta_map = Stdecl.t Mstr.t
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mstr.t
(** Task *)
type task = task_hd option
......@@ -47,8 +54,8 @@ val task_known : task -> known_map
val task_clone : task -> clone_map
val task_meta : task -> meta_map
val find_clone : task -> theory -> Stdecl.t
val find_meta : task -> string -> Stdecl.t
val find_clone : task -> theory -> tdecl_set
val find_meta : task -> string -> tdecl_set
(** {2 constructors} *)
......
......@@ -30,15 +30,14 @@ open Task
type 'a trans = task -> 'a
type 'a tlist = 'a list trans
let identity x = x
let identity x = x
let identity_l x = [x]
let conv_res c f x = c (f x)
let singleton f x = [f x]
let compose f g x = g (f x)
let compose f g x = g (f x)
let compose_l f g x = list_apply g (f x)
let apply f x = f x
......@@ -106,3 +105,74 @@ let tdecl_l = gen_decl_l add_tdecl
let rewrite fnT fnF = decl (fun d -> [decl_map fnT fnF d])
(** dependent transformations *)
module Wtds = Hashweak.Make (struct
type t = tdecl_set
let tag s = s.tds_tag
end)
let on_theory th fn =
let fn = Wtds.memoize 17 fn in
fun task -> fn (find_clone task th) task
let on_meta t fn =
let fn = Wtds.memoize 17 fn in
fun task -> fn (find_meta task t) task
let on_theories tl fn =
let rec pass acc = function
| th::tl -> on_theory th (fun st -> pass (Mid.add th.th_name st acc) tl)
| [] -> fn acc
in
pass Mid.empty tl
let on_metas tl fn =
let rec pass acc = function
| t::tl -> on_meta t (fun st -> pass (Mstr.add t st acc) tl)
| [] -> fn acc
in
pass Mstr.empty tl
let on_theories_metas thl tl fn =
on_theories thl (fun cm -> on_metas tl (fn cm))
(** register transformations *)
open Env
module Wenv = Hashweak.Make (struct
type t = env
let tag = env_tag
end)
exception UnknownTrans of string
exception KnownTrans of string
let transforms : (string, env -> task trans) Hashtbl.t = Hashtbl.create 17
let transforms_l : (string, env -> task tlist) Hashtbl.t = Hashtbl.create 17
let register_transform s p =
if Hashtbl.mem transforms s then raise (KnownTrans s);
Hashtbl.replace transforms s (Wenv.memoize 3 p)
let register_transform_l s p =
if Hashtbl.mem transforms_l s then raise (KnownTrans s);
Hashtbl.replace transforms_l s (Wenv.memoize 3 p)
let lookup_transform s =
try Hashtbl.find transforms s with Not_found -> raise (UnknownTrans s)
let lookup_transform_l s =
try Hashtbl.find transforms_l s with Not_found -> raise (UnknownTrans s)
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
let list_transforms_l () = Hashtbl.fold (fun k _ acc -> k::acc) transforms_l []
let () = Exn_printer.register (fun fmt exn -> match exn with
| KnownTrans s ->
Format.fprintf fmt "Transformation '%s' is already registered" s
| UnknownTrans s ->
Format.fprintf fmt "Unknown transformation '%s'" s
| e -> raise e)
......@@ -19,20 +19,20 @@
open Term
open Decl
open Task
open Theory
open Task
(** Task transformation *)
type 'a trans
type 'a tlist = 'a list trans
val store : (task -> 'a) -> 'a trans
val apply : 'a trans -> (task -> 'a)
val identity : task trans
val identity_l : task tlist
val apply : 'a trans -> (task -> 'a)
val store : (task -> 'a) -> 'a trans
val singleton : 'a trans -> 'a tlist
val compose : task trans -> 'a trans -> 'a trans
......@@ -61,3 +61,25 @@ val tdecl_l : (decl -> tdecl list list) -> task -> task tlist
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_theories : theory list -> (clone_map -> 'a trans) -> 'a trans
val on_metas : string list -> (meta_map -> 'a trans) -> 'a trans
val on_theories_metas : theory list -> string list ->
(clone_map -> meta_map -> 'a trans) -> 'a trans
(** {2 Registration} *)
val register_transform : string -> (Env.env -> task trans) -> unit
val register_transform_l : string -> (Env.env -> task tlist) -> unit
val lookup_transform : string -> Env.env -> task trans
val lookup_transform_l : string -> Env.env -> task tlist
val list_transforms : unit -> string list
val list_transforms_l : unit -> string list
......@@ -123,6 +123,8 @@ type driver = {
drv_syntax : string Mid.t;
drv_remove : Sid.t;
drv_remove_cl : Sid.t;
drv_meta : Stdecl.t Mid.t; (* the same as clone_map *)
drv_meta_cl : Stdecl.t Mid.t;
drv_regexps : (Str.regexp * Call_provers.prover_answer) list;
drv_exitcodes : (int * Call_provers.prover_answer) list;
drv_tag : int
......@@ -186,6 +188,8 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
let syntax = ref Mid.empty in
let remove = ref Sid.empty in
let remove_cl = ref Sid.empty in
let meta = ref Mid.empty in
let meta_cl = ref Mid.empty in
let qualid = ref [] in
let find_pr th (loc,q) = try ns_find_pr th.th_export q with Not_found ->
......@@ -197,6 +201,10 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
let find_ts th (loc,q) = try ns_find_ts th.th_export q with Not_found ->
errorm ~loc "unknown type symbol %s" (string_of_qualid !qualid q)
in
let add_meta th td m =
let s = try Mid.find th.th_name !m with Not_found -> Stdecl.empty in
m := Mid.add th.th_name (Stdecl.add td s) !m
in
let add_syntax loc k (_,q) id n s =
check_syntax loc s n;
if Mid.mem id !syntax then
......@@ -213,24 +221,42 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
let add_local th (loc,rule) = match rule with
| Rprelude s ->
let l = try Mid.find th.th_name !thprelude with Not_found -> [] in
thprelude := Mid.add th.th_name (s::l) !thprelude
thprelude := Mid.add th.th_name (l @ [s]) !thprelude
| Rsyntaxls (q,s) ->
let ls = find_ls th q in
add_meta th (Printer.remove_logic ls) meta;
add_meta th (Printer.syntax_logic ls s) meta;
add_syntax loc "logic" q ls.ls_name (List.length ls.ls_args) s
| Rsyntaxts (q,s) ->
let ts = find_ts th q in
add_syntax loc "type" q ts.ts_name (List.length ts.ts_args) s
add_meta th (Printer.remove_type ts) meta;
add_meta th (Printer.syntax_type ts s) meta;
add_syntax loc "type" q ts.ts_name (List.length ts.ts_args) s
| Rremovepr (c,q) ->
let td = Printer.remove_prop (find_pr th q) in
add_meta th td (if c then meta_cl else meta);
let sr = if c then remove_cl else remove in
sr := Sid.add (find_pr th q).pr_name !sr
| Rtagts (c,q,s) -> add_tag c (find_ts th q).ts_name s
| Rtagls (c,q,s) -> add_tag c (find_ls th q).ls_name s
| Rtagpr (c,q,s) -> add_tag c (find_pr th q).pr_name s
| Rtagts (c,q,s) ->
let td = create_meta s [MAts (find_ts th q)] in
add_meta th td (if c then meta_cl else meta);
add_tag c (find_ts th q).ts_name s
| Rtagls (c,q,s) ->
let td = create_meta s [MAls (find_ls th q)] in
add_meta th td (if c then meta_cl else meta);
add_tag c (find_ls th q).ls_name s
| Rtagpr (c,q,s) ->
let td = create_meta s [MApr (find_pr th q)] in
add_meta th td (if c then meta_cl else meta);
add_tag c (find_pr th q).pr_name s
in
let add_local th (loc,rule) =
try add_local th (loc,rule) with e -> raise (Loc.Located (loc,e))
in
let add_theory { thr_name = (loc,q); thr_rules = trl } =
let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
let th = try Env.find_theory env f id with Env.TheoryNotFound (l,s) ->
errorm ~loc "theory %s.%s not found" (String.concat "." l) s
let th =
try Env.find_theory env f id with e -> raise (Loc.Located (loc,e))
in
qualid := q;
List.iter (add_local th) trl
......@@ -250,6 +276,8 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
drv_syntax = !syntax;
drv_remove = !remove;
drv_remove_cl = !remove_cl;
drv_meta = !meta;
drv_meta_cl = !meta_cl;
drv_regexps = !regexps;
drv_exitcodes = !exitcodes;
drv_tag = !driver_tag;
......
......@@ -220,3 +220,5 @@ let print_goal drv fmt (id, f, task) =
print_task drv fmt task;
fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla drv) f
let () = Theory.register_meta "AC" [Theory.MTlsymbol]
......@@ -367,3 +367,6 @@ let t_all = Register.store_env
Trans.tdecl (decl tenv) init_task)
let () = Register.register_transform "encoding_decorate_every_simple" t_all
let () = Theory.register_meta "encoding_decorate : kept" [Theory.MTtysymbol]
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