✐‹creator "Kevin Kappelmann"› section‹Zippy Paper Guide› theory Zippy_Paper imports
Pure begin
paragraph ‹Summary› text‹Guide for the preprintcite‹zippy››
text‹ ▪ General Information ▪ Unfortunately, employing the polymorphic record extension mechanism described in the paper
hits severe performance problems of the Poly/ML compiler.
To get around minute-long compilation times, all data fields of the zipper have to be
instantiated in one go rather than by repeated instantiation of polymorphic fields,
cf. @{file "Zippy/Instances/zippy_instance_base.ML"}.
Relevant issue on GitHub: https://github.com/polyml/polyml/issues/213
▪ Section 3 ▪ We implemented a generalisation of the state monad that also allows the state type to change
during computation. Such states are not monads but (Atkey) indexed monads. ▪ Atkey Indexed Monads @{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/itypeclass_base.ML"} ▪ Indexed State Monad @{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/State/istate.ML"} ▪ State Monad @{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/State/istate.ML"} ▪ Antiquotations ▪ Sources
@{file "ML_Typeclasses/Antiquotations/ML_Eval_Antiquotation.thy"}
@{file "ML_Typeclasses/Antiquotations/ML_Args_Antiquotations.thy"}
@{file "Antiquotations/ML_IMap_Antiquotation.thy"} ▪ Example Configuration and Follow-Up ML-Code Generation
@{file "Gen_Zippers/Zippers5/Morphs/ML_Morphs.thy"}
▪ Section 4. We highlight the differences/extensions to the paper description ▪ The zipper uses an additional "action cluster" layer that sits between a goal cluster and
an action. Action clusters collect related actions, e.g. one could create an action cluster for
classical reasoners, one for simplification actions, etc. This gives the search tree some more
structure but is not strictly necessary (it is thus omitted in the paper).
▪ Adding Actions @{file "Zippy/Actions/zippy_paction_mixin_base.ML"} ▪ Action nodes do not store a static cost and action but, more generally,
an "action with priority" (paction) that dynamically computes a priority, action pair. ▪ Action clusters store a "copy" morphism such that actions generating new children can move
their action siblings to the newly created child while updating their siblings' goal focuses
(since the number and order of goals may have changed in the new child).
▪ Lifting Tactics ▪ Lifting Isabelle Tactics to Zippy Tactics @{file "Zippy/Tactics/Base/zippy_ztactic.ML"} ▪ Lifting Zippy Tactics to Actions @{file "Zippy/Instances/zippy_instance_tactic.ML"}
▪ The Basic Search Tree Model @{file "Zippy/Instances/zippy_instance_base.ML"}
Since there are is always exactly one goal clusters node, we do not use lists for the topmost layer. ▪ List Zipper @{file "Gen_Zippers/Zippers5/Zippers/Instances/list_zipper.ML"}
▪ Adding Failure and State @{file "Zippy/Instances/Zippy_Instance_Pure.thy"} ▪ Option Monad and Transformers
@{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/typeclass_base_instance.ML"}
▪ Adding Positional Information ▪ Extending the Alternating Zipper @{file "Zippy/Positions/zippy_positions_mixin_base.ML"} ▪ Alternating (Global) Position Zipper
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/Instances/alternating_global_position_zipper.ML"}
▪ Running a Search ▪ Postorder Depth-First Enumeration for Zippers
@{file "Gen_Zippers/Zippers5/Zippers/Utils/df_postorder_enumerate_zipper.ML"} ▪ Postorder Depth-First Enumeration for Alternating Zippers
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/Utils/df_postorder_enumerate_alternating_zipper.ML"} ▪ Runs @{file "Zippy/Runs/zippy_run_mixin.ML"}
▪ Retrieving Theorems from the Tree
@{file "Zippy/Goals/Lists/zippy_lists_goals_results_top_meta_vars_mixin.ML"}
▪ Final example usages can be found here
@{file "Zippy/Instances/Zip/Examples/Zip_Examples.thy"}. ›
end
Messung V0.5 in Prozent
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.13Bemerkung:
(vorverarbeitet am 2026-09-29)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
