Commit 75779176 authored by Andrei Paskevich's avatar Andrei Paskevich

remove "built-in" propositions early

also preserve proposition names in split_premise when possible
parent 1e402289
......@@ -32,7 +32,7 @@ let add_id q (ld,id) = function
| ls, _ when Sls.mem ls q -> (ls, None)::ld, id
| d -> ld, d::id
let elim q d = match d.d_node with
let elim q spr d = match d.d_node with
| Dlogic l ->
[create_logic_decl (List.map (add_ld q) l)]
| Dind l ->
......@@ -40,11 +40,13 @@ let elim q d = match d.d_node with
let ld = if ld = [] then [] else [create_logic_decl (List.rev ld)] in
let id = if id = [] then [] else [create_ind_decl (List.rev id)] in
ld @ id
| Dprop (Paxiom,pr,_) when Spr.mem pr spr -> []
| _ -> [d]
let eliminate_builtin =
Trans.on_tagged_ls Printer.meta_syntax_logic
(fun rem_ls -> Trans.decl (elim rem_ls) None)
Trans.on_tagged_ls Printer.meta_syntax_logic (fun rem_ls ->
Trans.on_tagged_pr Printer.meta_remove_prop (fun rem_pr ->
Trans.decl (elim rem_ls rem_pr) None))
let () = Trans.register_transform "eliminate_builtin" eliminate_builtin
......
......@@ -141,9 +141,10 @@ let split_goal ro pr f =
let split_axiom ro pr f =
let make_prop f =
let pr = create_prsymbol (id_clone pr.pr_name) in
create_prop_decl Paxiom pr f
in
List.map make_prop (split_pos ro [] f)
create_prop_decl Paxiom pr f in
match split_pos ro [] f with
| [f] -> [create_prop_decl Paxiom pr f]
| fl -> List.map make_prop fl
let split_all ro d = match d.d_node with
| Dprop (Pgoal, pr,f) -> split_goal ro pr f
......
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