functor (M : Memory.Model) -> Mcfg.S