Commit abafcb81 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

clear_but now only removes local context.

Factorizing get_local_declarations in transformations.
parent a8d1c6c3
......@@ -267,10 +267,7 @@ let unfold unf h =
end
| _ -> [d]) None
let sort task =
let local_decls =
let ut = Task.used_symbols (Task.used_theories task) in
Task.local_decls task ut in
let sort local_decls =
let l = ref [] in
Trans.decl
(fun d ->
......@@ -290,7 +287,7 @@ let sort task =
(* TODO is sort really needed ? It looked like it was for subst in some example where I wanted to subst the definition of a logic constant into an equality and it would fail because the equality is defined before the logic definition. This may be solved by current implementation of subst: to be tested *)
let sort =
Trans.store (fun task -> Trans.apply (sort task) task)
Trans.bind get_local sort
let get_local task =
let ut = Task.used_symbols (Task.used_theories task) in
......
......@@ -114,16 +114,19 @@ let remove_list name_list =
None
(* from task [delta, name1, name2, ... namen |- G] build the task [name1, name2, ... namen |- G] *)
let clear_but (l: prsymbol list) =
let clear_but (l: prsymbol list) local_decls =
Trans.decl
(fun d ->
match d.d_node with
| Dprop (Paxiom, pr, _t) when List.mem pr l ->
[d]
| Dprop (Paxiom, _pr, _t) ->
| Dprop (Paxiom, _pr, _t) when List.exists (fun x -> Decl.d_equal x d) local_decls ->
[]
| _ -> [d]) None
let clear_but (l: prsymbol list) =
Trans.bind get_local (clear_but l)
let use_th th =
Trans.add_tdecls [Theory.create_use th]
......
......@@ -76,3 +76,11 @@ let subst_forall_list t l =
| Tquant (Tforall, tq) ->
subst_quant_list Tforall tq l
| _ -> raise (Arg_trans "subst_forall_list")
(* Returns the list of local declarations as a transformation *)
let get_local =
Trans.store (fun task ->
let local_decls =
let ut = Task.used_symbols (Task.used_theories task) in
Task.local_decls task ut in
local_decls)
......@@ -34,3 +34,6 @@ val subst_forall: term -> term -> term
(* TODO remove subst_forall and subst_exist *)
(* Same as subst_forall with a list of term *)
val subst_forall_list: term -> term list -> term
(* Returns the list of local declarations *)
val get_local: Decl.decl list Trans.trans
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