smart dr g - uses VPatch drawing function dr after converting g to a VPatch It will add boundary joins regardless of the drawing function. Examples:

smart draw g

smart (labelled draw) g

smart (labelSize normal draw) g

select the halftile faces of a Tgraph with a join edge on the boundary. Useful for drawing join edges only on the boundary.

draw boundary join edges of a Tgraph using a given VPatch

Given a list of faces and a VPatch with suitable locations, draw just the dashed joins for those faces. Will raise an error if any vertex in the faces does not have a location in the VPatch.

same as draw except adding dashed lines on boundary join edges.

restrictSmart g dr vp - assumes vp has locations for vertices in g. It uses the VPatch drawing function dr to draw g and adds dashed boundary joins. This can be used instead of smart when an appropriate vp is already available.

smartRotateBefore vfun a g - a tricky combination of smart with rotateBefore. Uses vfun to produce a Diagram after converting g to a rotated VPatch but also adds the dashed boundary join edges of g.

Example: smartRotateBefore (labelled draw) angle g

smartAlignBefore vfun (a,b) g - a tricky combination of smart with alignBefore. Uses vfun to produce a Diagram after converting g to an aligned VPatch but also adds the dashed boundary join edges of g.

Example: smartAlignBefore (labelled draw) (a,b) g

applies partCompose to a Tgraph g, then draws the composed graph along with the remainder faces (in lime). (Relies on the vertices of the composition and remainder being subsets of the vertices of g.) This will raise an error if the composed faces have a crossing boundary or are disconnected.

drawForce g is a diagram showing the argument g in red overlayed on force g. It adds dashed join edges on the boundary of g. It will raise an error if the force fails with an incorrect/stuck Tgraph

drawSuperForce g is a diagram showing the argument g in red overlayed on force g in black overlaid on superForce g in blue. It adds dashed join edges on the boundary of g. It will raise an error if the initial force fails with an incorrect/stuck Tgraph

drawWithMax g - draws g and overlays the maximal composition of force g in red. This relies on g and all compositions of force g having vertices in force g. It will raise an error if forcing fails (g is an incorrect Tgraph).

addBoundaryAfter f g - displaying the boundary of a Tgraph g in lime (overlaid on g drawn with f).

drawCommonFaces (g1,e1) (g2,e2) uses commonFaces (g1,e1) (g2,e2) to find the common faces and emphasizes them on the background g1.

emphasizeFaces fcs g emphasizes the given faces (that are in g) overlaid on the background draw g.

For illustrating an unsound version of composition which defaults to kites when there are unknown dart wings on the boundary. This is unsound in that it can create an incorrect Tgraph from a correct Tgraph. E.g. when applied to force queenGraph.

compForce is a partial function similar to (compose . force), i.e it does a force then compose (raising an error if the force fails with an incorrect Tgraph). However it produces an explicitly Forced Tgraph, and is more efficient because it omits the check for connected, and no crossing boundaries (and uses getDartWingInfoForced instead of getDartWingInfo) This relies on a proof that composition does not need to be checked for a forced Tgraph. (We also have a proof that the result must be a forced Tgraph when the initial force succeeds.) This will raise an error if the initial force fails with an incorrect Tgraph.

allCompForce g produces a list of the non-null iterated (forced) compositions of force g. It will raise an error if the initial force fails with an incorrect Tgraph. The list will be [] if g is the emptyTgraph, otherwise the list begins with force g (when the force succeeds). The definition relies on (1) a proof that the composition of a forced Tgraph is forced and (2) a proof that composition does not need to be checked for a forced Tgraph.

maxCompForce g produces the maximally composed (non-null) Tgraph starting from force g, provided g is not the emptyTgraph and just the emptyTgraph otherwise. It will raise an error if the initial force fails with an incorrect Tgraph.

allForceDecomps g - produces an infinite list (starting with g) of forced decompositions of g (raising an error if a force fails with an incorrect Tgraph).

forcedBoundaryECovering g - produces a list of all boundary covers of force g. Each boundary cover is a forced Tgraph that extends force g and covers the entire boundary directed edges of force g. (So the boundary of force g is entirely internal edges in each boundary cover). The covers include all possible ways faces can be added on the boundary of force g except combinations which are found to be incorrect. The common faces of the covers constitute an empire (level 1) of g. This will raise an error if the initial force fails with an incorrect/stuck Tgraph.

forcedBoundaryVCovering g - produces a list of all boundary covers of force g as with forcedBoundaryECovering g but covering all boundary vertices rather than just boundary edges. This will raise an error if the initial force fails with an incorrect/stuck Tgraph.

boundaryECovering - for an explicitly Forced BoundaryState fbd, produces a list of all possible covers of the boundary directed edges in fbd. A cover is an explicitly Forced extension (of fbd) such that the original boundary directed edges of fbd are all internal edges. Extensions are made by repeatedly adding a face to any edge on the original boundary that is still on the boundary and forcing, repeating this until the orignal boundary is all internal edges. The resulting covers account for all possible ways the boundary can be extended. This can raise an error if both choices on a boundary edge fail when forced (using atLeastOne).

In which case, fbd represents an important counter example to the hypothesis that successfully forced forcibles are correct.

boundaryVCovering fbd - similar to boundaryECovering, but produces a list of all possible covers of the boundary vertices in fbd (rather than just boundary edges). This can raise an error if both choices on a boundary edge fail when forced (using atLeastOne).

tryDartAndKite de b - returns the list of (2) results after adding a dart (respectively kite) to edge de of a Forcible b. Each of the results is a Try.

tryDartAndKiteForced de b - returns the list of (2) results after adding a dart (respectively kite) to edge de of a Forcible b and then tries forcing. Each of the results is a Try.

tryDartAndKiteF de b - returns the list of (2) results after adding a dart (respectively kite) to edge de of a Forcible b and then tries forcing. Each of the results is a Try of an explicitly Forced type.

tryCheckCasesDKF dedge fb (where fb is an explicitly forced Forcible and dedge is a directed boundary edge of fb) tries to add both a half kite and a half dart to the edge then tries forcing each result. It returns the list of only the successful Try results provided there is AT LEAST ONE. If there are no successes, this may be an important counter example and it will return Left with a failure report describing the counter example to the following:

Hypothesis: A successfully forced Tgraph is correct (a correct tiling).

(If both legal additions to a boundary edge are incorrect, then the (Forced) Forcible must be incorrect).

checkCasesDKF dedge fb (where fb is an explicitly forced Forcible and dedge is a directed boundary edge of fb) tries to add both a half kite and a half dart to the edge then tries forcing each result. It returns the list of only the successful results provided there is AT LEAST ONE. If there are no successes, this may be an important counter example and it will raise an error describing the counter example to the following:

Hypothesis: A successfully forced Tgraph is correct (a correct tiling).

(If both legal additions to a boundary edge are incorrect, then the (Forced) Forcible must be incorrect).

Make a set of the directed boundary edges from tilefaces

commonBdry des a - returns those directed edges in des that are boundary directed edges of a

returns the set of boundary vertices of a tilefaces

returns the set of internal vertices of a tilefaces

A test function to draw (as a column) the list of covers resulting from forcedBoundaryVCovering for a given Tgraph.

empire1 g - produces a TrackedTgraph representing the level 1 empire of g. Raises an error if force g fails with a stuck/incorrect Tgraph. The tgraph of the result is the first boundary vertex cover of force g which is arbitrarily chosen amongst the covers as the background setting, and the tracked list of the result has the common faces of all the boundary vertex covers (of force g) at the head, followed by the original faces of g.

empire2 g - produces a TrackedTgraph representing a level 2 empire of g. Raises an error if force g fails with a stuck/incorrect Tgraph. After finding all boundary edge covers of force g, boundary edge covers are then found for each boundary edge cover to form a list of doubly-extended boundary edge covers. The tgraph of the result is the first (doubly-extended) boundary edge cover (of force g) which is arbitrarily chosen amongst the (doubly-extended) covers as the background setting, and the tracked list of the result has the common faces of all the (doubly-extended) boundary edge covers at the head, followed by the original faces of g.

empire2Plus g - produces a TrackedTgraph representing an extended level 2 empire of g similar to empire2, but using boundaryVCovering instead of boundaryECovering. Raises an error if force g fails with a stuck/incorrect Tgraph.

drawEmpire e - produces a diagram for an empire e represented as a TrackedTgraph as calcultaed by e.g. empire1 or empire2 or empire2Plus. The diagram draws the underlying Tgraph (the background setting), with the first tracked faces (the starting Tgraph) shown red, and emphasising the second tracked faces (the common faces).

showEmpire1 g - produces a diagram emphasising the common faces of all boundary covers of force g. This is drawn over one of the possible boundary covers and the faces of g are shown in red.

showEmpire2 g - produces a diagram emphasising the common faces of a doubly-extended boundary cover of force g. This is drawn over one of the possible doubly-extended boundary covers and the faces of g are shown in red.

superForce g - after forcing g this looks for single choice boundary edges. That is a boundary edge for which only a dart or only a kite addition occurs in all boundary edge covers. If there is at least one such edge, it makes the choice for the first such edge and recurses, otherwise it returns the forced result. This will raise an error if force encounters a stuck (incorrect) tiling or if both forced extensions fail for some boundary edge. Otherwise, the result has exactly two correct possible extensions for each boundary edge.

trySuperForce g - this looks for single choice edges after trying to force g. If there is at least one, it makes that choice and recurses. It returns a Left s if force fails or if both choices fail for some edge (where s is a failure report). Otherwise Right g' is returned where g' is the super forced g.

singleChoiceEdges bd - if bd is an explicitly Forced boundary state (of a forced Tgraph) this finds those boundary edges of bd which have a single choice (i.e. the other choice is incorrect), by inspecting boundary edge covers of bd. The result is a list of pairs of (edge,label) where edge is a boundary edge with a single choice and label indicates the choice as the common face label.

Tries to create a new Tgraph from all faces with a boundary vertex in a Tgraph. The resulting faces could have a crossing boundary and also could be disconnected if there is a hole in the starting Tgraph so these conditions are checked for, producing a Try result.

Returns a list of (looping) vertex trails for a BoundaryState. There will usually be a single trail, but more than one indicates the presence of boundaries round holes. Each trail starts with the lowest numbered vertex in that trail, and ends with the same vertex. The trails will have disjoint sets of vertices because of the no-crossing-boundaries condition of Tgraphs (and hence BoundaryStates).

Given a suitable vertex to location map and boundary loops (represented as a list of lists of vertices), this will return a (Diagrams) Path for the boundary. It will raise an error if any vertex listed is not a map key. (The resulting path can be filled when converted to a diagram.)

TrackedTgraph - introduced to allow tracking of subsets of faces in both force and decompose operations. Mainly used for drawing purposes but also for empires. A TrackedTgraph has a main Tgraph (tgraph) and a list of subsets (sublists) of faces (tracked). The list allows for tracking different subsets of faces at the same time.

newTrackedTgraph g creates a TrackedTgraph from a Tgraph g with an empty tracked list

makeTrackedTgraph g trackedlist creates a TrackedTgraph from a Tgraph g from trackedlist where each list in trackedlist is a subset of the faces of g. Any faces not in g are ignored.

trackFaces ttg - pushes the maingraph tilefaces onto the stack of tracked subsets of ttg

unionTwoTracked ttg - combines the top two lists of tracked tilefaces replacing them with the list union.

addHalfDartTracked ttg e - add a half dart to the tgraph of ttg on the given edge e, and push the new singleton face list onto the tracked list.

addHalfKiteTracked ttg e - add a half kite to the tgraph of ttg on the given edge e, and push the new singleton face list onto the tracked list.

decompose a TrackedTgraph - applies decomposition to all tracked subsets as well as the full Tgraph. Tracked subsets get the same numbering of new vertices as the main Tgraph.

To draw a TrackedTgraph, we use a list of functions each turning a VPatch into a diagram. The first function is applied to a VPatch for untracked faces. Subsequent functions are applied to VPatches for the respective tracked subsets. Each diagram is beneath later ones in the list, with the diagram for the untracked VPatch at the bottom. The VPatches are all restrictions of a single VPatch for the Tgraph, so consistent. (Any extra draw functions are applied to the VPatch for the main tgraph and the results placed atop.)

To draw a TrackedTgraph rotated. Same as drawTrackedTgraph but with additional angle argument for the rotation. This is useful when labels are being drawn. The angle argument is used to rotate the common vertex location map (anticlockwise) before drawing to ensure labels are not rotated.

To draw a TrackedTgraph aligned. Same as drawTrackedTgraph but with additional vertex pair argument for the (x-axis) alignment. This is useful when labels are being drawn. The vertex pair argument is used to align the common vertex location map before drawing (to ensure labels are not rotated). This will raise an error if either of the pair of vertices is not a vertex of (the tgraph of) the TrackedTgraph