Commit 9ec17e16 authored by Andrei Paskevich's avatar Andrei Paskevich

add clone_fold to Theory for Francois

parent dac07ed0
......@@ -429,6 +429,22 @@ let cl_add_decl cl inst d = match d.d_node with
let pr',f' = cl_new_prop cl (pr,f) in
Some (create_prop_decl k' pr' f')
let clone_fold add_tdecl v th inst =
let cl = cl_init th inst in
let add acc td = match td with
| Decl d ->
begin match cl_add_decl cl inst d with
| Some d -> add_tdecl acc (Decl d)
| None -> acc
end
| Use _ | Clone _ ->
add_tdecl acc td
in
let (res,clmap) = List.fold_left add v th.th_decls in
let add_idid id id' acc = (id,id') :: acc in
let sl = Hid.fold add_idid cl.id_table [] in
res, merge_clone clmap th sl
let cl_add_tdecl cl inst uc td = match td with
| Decl d ->
let decls = match cl_add_decl cl inst d with
......@@ -436,10 +452,8 @@ let cl_add_tdecl cl inst uc td = match td with
| None -> uc.uc_decls
in
{ uc with uc_decls = decls }
| Use _ ->
| Use _ | Clone _ ->
{ uc with uc_decls = td :: uc.uc_decls }
| Clone (th,sl) ->
add_clone uc th sl
let clone_export uc th inst =
let cl = cl_init th inst in
......
......@@ -88,6 +88,9 @@ val empty_inst : th_inst
val use_export : theory_uc -> theory -> theory_uc
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
val clone_fold : (('a * clone_map) -> tdecl -> ('a * clone_map)) ->
('a * clone_map) -> theory -> th_inst -> ('a * clone_map)
val merge_clone : clone_map -> theory -> (ident * ident) list -> clone_map
(* exceptions *)
......
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