archetype
val decompile : (T.dprogram * env) -> M.model * env