Theory Zippy_Paper
section ‹Zippy Paper Guide›
theory Zippy_Paper
imports
Pure
begin
paragraph ‹Summary›
text ‹Guide for the preprint\<^cite>‹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 2
▪ Nodes @{file "Gen_Zippers/Zippers5/Alternating_Zippers/Instances/Nodes/node.ML"}
▪ Section 2.1
▪ Categories and Arrows
@{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/Categories/category.ML"}
▪ Morphs
▪ Morphism Base @{file "Gen_Zippers/Zippers5/Morphs/morph_base.ML"}
▪ Morphisms @{file "Gen_Zippers/Zippers5/Morphs/morph.ML"}
▪ Zippers
▪ Zipper Morphs @{file "Gen_Zippers/Zippers5/Zippers/zipper_morphs.ML"}
▪ Zipper Data @{file "Gen_Zippers/Zippers5/Zippers/zipper_data.ML"}
▪ Zipper @{file "Gen_Zippers/Zippers5/Zippers/zipper.ML"}
▪ Linked Zippers
▪ Linked Zipper Morphs @{file "Gen_Zippers/Zippers5/Linked_Zippers/linked_zipper_morphs.ML"}
▪ Linked Zippers @{file "Gen_Zippers/Zippers5/Linked_Zippers/linked_zipper.ML"}
▪ Alternating Zippers
▪ Alternating Zipper Morphs
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/alternating_zipper_morphs.ML"}
▪ Alternating Zippers
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/alternating_zipper.ML"}
▪ Alternating Zipper Product
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/pair_alternating_zipper.ML"}
▪ Section 2.1.1
▪ Monads
@{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/typeclass_base.ML"}
▪ Kleisli Category
@{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/Categories/category_instance.ML"}
▪ Generating Alternating Zippers from Node Zippers
▪ Extending the Alternating Zipper
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/Instances/Nodes/alternating_zipper_nodes.ML"}
▪ Extending and Lifting the Input Zippers
@{file "Gen_Zippers/Zippers5/Zippers/extend_zipper_context.ML"}
▪ Generating Node Zippers
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/Instances/Nodes/alternating_zipper_nodes_simple_zippers.ML"}
▪ Section 2.2
▪ Lenses @{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/Lenses/lens.ML"}
▪ 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).
▪ Adding Goals @{file "Zippy/Goals/zippy_goals_mixin_base.ML"}
▪ Goal Clusters @{file "Zippy/Goals/Base/zippy_goal_clusters.ML"}
▪ Goal Cluster @{file "Zippy/Goals/Base/zippy_goal_cluster.ML"}
▪ Goal Focus @{file "Zippy/Goals/Base/zippy_goal_focus.ML"}
▪ Union Find @{file "Union_Find//imperative_union_find.ML"}
▪ 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