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

Eliminate_algebraic: move "Use" tdecls for tuple theories

eliminate_match may move forward tuple type declarations.
This patch makes is move the corresponding Use tdecls along,
to stay compatible with the logic of Task.local_decls, fixing #183.
parent 06d18eed
......@@ -68,7 +68,7 @@ let compile_match = Trans.decl (fun d -> [decl_map rewriteT d]) None
type state = {
mt_map : lsymbol Mts.t; (* from type symbols to selector functions *)
pj_map : lsymbol list Mls.t; (* from constructors to projections *)
tp_map : decl Mid.t; (* skipped tuple symbols *)
tp_map : (decl*theory) Mid.t; (* skipped tuple symbols *)
inf_ts : Sts.t; (* infinite types *)
ma_map : bool list Mts.t; (* material type arguments *)
keep_t : bool; (* keep algebraic type definitions *)
......@@ -410,14 +410,19 @@ let comp t (state,task) = match t.task_decl.td_node with
comp t (state,task)
let comp t (state,task) = match t.task_decl.td_node with
| Use {th_decls = [{td_node = Decl ({d_node = Ddata [ts,_]})}]}
when is_ts_tuple ts ->
state, task
| Decl ({ d_node = Ddata [ts,_] } as d) when is_ts_tuple ts ->
let tp_map = Mid.add ts.ts_name d state.tp_map in
let th = tuple_theory (List.length ts.ts_args) in
let tp_map = Mid.add ts.ts_name (d,th) state.tp_map in
{ state with tp_map = tp_map }, task
| Decl d ->
let rstate,rtask = ref state, ref task in
let add _ d () =
let add _ (d,th) () =
let t = Opt.get (add_decl None d) in
let state,task = comp t (!rstate,!rtask) in
let task = add_tdecl task (create_use th) in
rstate := state ; rtask := task ; None
in
let tp_map = Mid.diff add state.tp_map d.d_syms in
......
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