Theory Zippy.Zippy_Base

✐‹creator "Kevin Kappelmann"›
section ‹Zippy Base›
theory Zippy_Base
  imports
    ML_Alternating_Zipper_Utils
    Zippy_Exceptions
    Zippy_Loggers
    Zippy_Shows
    Zippy_States
begin

ML_file‹zippy_monad_util.ML›

ML_file‹zippy_base_base.ML›
ML_file‹zippy_base.ML›

ML‹
(*Grounding utilities needed to store zippy data/functions as context data (since only monomorphic
data can be stored in the generic context). Note that both ParaT and ZipperT arguments are grounded.

FIXME: generalise loading of ML code dependent on the grounding such that it can be re-loaded with
different ground types.
*)
structure ML_Gen =
struct
open ML_Gen
val ground_zipper_types =
  let val mk_groundT = K "unit"
  in ML_Gen.setup_zipper_args' (NONE, SOME mk_groundT) (NONE, SOME mk_groundT) end
val reset_zipper_types = ML_Gen.setup_zipper_args' (NONE, NONE) (NONE, NONE)
end
›

end