Commit d64ec17f authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

move declaration rewriting from Trans to Decl

parent 9508894d
......@@ -371,6 +371,28 @@ let create_ind_decls idl =
| [_] -> [create_ind_decl idl]
| _ -> List.rev_map create_ind_decl (build idl)
(** Utilities *)
let decl_map fnT fnF d = match d.d_node with
| Dtype _ ->
d
| Dlogic l ->
let fn = function
| ls, Some ld ->
let vl,e = open_ls_defn ld in
make_ls_defn ls vl (e_map fnT fnF e)
| ld -> ld
in
create_logic_decl (List.map fn l)
| Dind l ->
let fn (pr,f) = pr, fnF f in
let fn (ps,l) = ps, List.map fn l in
create_ind_decl (List.map fn l)
| Dprop (k,pr,f) ->
create_prop_decl k pr (fnF f)
(** Known identifiers *)
exception KnownIdent of ident
......
......@@ -116,6 +116,10 @@ exception UnboundVars of Svs.t
exception ClashIdent of ident
exception EmptyDecl
(** Utilities *)
val decl_map : (term -> term) -> (fmla -> fmla) -> decl -> decl
(** Known identifiers *)
type known_map = decl Mid.t
......
......@@ -114,23 +114,5 @@ let decl_l fn =
let fn task acc = List.rev_map (List.fold_left add_decl acc) (fn task) in
map_l fn
let rewrite fnT fnF d = match d.d_node with
| Dtype _ ->
d
| Dlogic l ->
let fn = function
| ls, Some ld ->
let vl,e = open_ls_defn ld in
make_ls_defn ls vl (e_map fnT fnF e)
| ld -> ld
in
create_logic_decl (List.map fn l)
| Dind l ->
let fn (pr,f) = pr, fnF f in
let fn (ps,l) = ps, List.map fn l in
create_ind_decl (List.map fn l)
| Dprop (k,pr,f) ->
create_prop_decl k pr (fnF f)
let rewrite fnT fnF = decl (fun d -> [rewrite fnT fnF d])
let rewrite fnT fnF = decl (fun d -> [decl_map fnT fnF d])
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