module Complete
(
    complete
)
where

import Isomorphism
import MonadF
import Package

-- Figure 5: Code to complete a constructed interpreter
-- (Part I, continued in module Main)

complete :: Prepackage t v (IdMonadF ut t) (IdMonadF uv v) ve ut uv
         -> Package ut uv ut uv ve
complete prepkg @ Prepackage { isom_t'' = prepkg_isom_t''
                             , isom_v'' = prepkg_isom_v'' } = top where
    vroom = prepackageI (prepkg_isom_t'' =.= wisom) (prepkg_isom_v'' =.= wisom)
               prepkg_isom_t'' prepkg_isom_v'' identityI identityI identityI
    Prepackage { finalize = finalizer } = iso vroom prepkg
    top = finalizer top