Documentation

A class for Category, Functor and NaturalTransformation, defining some functions useful for common handling of all three data structures.

Minimal complete definition : get_id, struct_str and sdns_lens.

(Namespace a) is a type synonym for a Map from String to a. In our case a is either Category, Functor or NaturalTransformation, and the map will map an id string to the corresponding defined structure.

SDNamespace consists of a 3-tuple of Namespaces, one for Category, one for Functor and one for NaturalTransformation.

All functors in the functor Namespace are assumed to be basic functors. All natural transformations in the natural transformation Namespace are assumed to be basic natural transformations.

An SDNamespace where all Namespaces are empty.

A lens from an SDNamespace into the Namespace of defined categories.

A lens from an SDNamespace into the Namespace of defined functors.

A lens from an SDNamespace into the Namespace of defined natural transformations.

The obvious action: given a lens from an object of type a to an object of type b and a state action taking a state of type b and outputting a new state of type b along with an object of type c, we get a new state action by taking a state of type a, using the lens to view this to get an object of type b, running the given state action to get a new object of type b and an object of type c, and finally, using the lens to set this new object of type b back into the original state of type a.

Viewing the lens get action as a state action which does not change the underlying state.

sdns_lookup takes a String and a lens from SDNamespace into one of its component Namespaces, and attempts to lookup the string in that namespace.

A helper function for insert_action.

(insert_action obj) is the State (SDNamespace a) (IO ()) which adds the key value pair (get_id obj, obj) to the correct namespace if (get_id obj) is not already a key in the namespace, and gives the IO action printing an error message to stderr otherwise.

A partial function on SDCommands which were constructed using DefineCat. See handle_sdc.

A partial function on SDCommands which were constructed using DefineFunc. See handle_sdc.

A partial function on SDCommands which were constructed using DefineNat. See handle_sdc.

A lens from a Category to its string of options.

A lens from a Functor to its string of options.

A lens from a NaturalTransformation to its string of options.

(sdns_lookup_add str lns1 added lns2) looks up str from the Namespace extracted using lns1 from the SDNamespace, then modifies the looked-up object o by adding ","++added to the end of lns2 of the object o.

(sdns_chain_lookup_func id opt) attempts to lookup the id in the functor Namespace and adds the options opt to the options of the looked up functor. If it cannot find id in the functor namespace, it looks up id in the category Namespace and returns the identity functor of the resulting category.

(sdns_chain_lookup_nat id opt) attemps to lookup the id in the natural transformation Namespace and adds the options opt to the options of the looked up natural transformation. If it cannot find id in the natural transformation namespace, it looks up id in the functor namespace, and returns the identity natural transformation of the functor if it finds it there. If it cannot find id in either the natural transformation or functor namespaces, it looks up id in the category namespace, and returns the identity natural transformation of the identity functor of the category if it finds it there.

A class for errors which have error messages.

FunctorReadError is the type of error that can be thrown by read_functor_line. Either some of the functors in the lookup do no exist, or the list of functors do not compose.

LookupFunctorError list says that there are functors which cannot be found in the SDNamespace. Here list is a list of pairs (n,id) where n is the position in the functor line where the given id cannot be found.

ComposeFunctorError list says that the composition could not be determined. Here, list is empty if the functor line has no functors, i.e. it specifies an empty composition. Otherwise, it is a list of 4-tuples (n1,id1,n2,id2) where n1 is the position of id1 and n2 is the position of id2, and the functors specified by id1 and id2 do not compose.

A helper function used to define error_msg of a LookupFunctorError

A helper function used to define error_msg of a ComposeFunctorError

read_functor_line takes a list of CompElements representing a collection of functors or empty spaces, either throws a FunctorReadError or returns a pair (f,ff) where f is the composite Functor and ff is the FunctorFormatting associated to f described by the spacing in the original list of CompElements. See the user's manual for how ff and f are determined.

list_ce_to_funcs is used in read_functor_line. It takes a list of CompElements either throws a LookupFunctorError or gives a list of (n,id,f) for each non-Empty CompElement in the list, where n is the index in the original list the non-Empty CompElement resides (with indexing starting at 0), id is the id of the functor, and f is the functor from the SDNamespace corresponding to the CompElement.

compose_funcs is used in read_functor_line. It takes an object of type [(Int,String,Functor)] which is outputted by list_ce_to_funcs, and attempts to compose the functors in the list. It either throws a ComposeFunctorError or gives a pair (f,l) where f is the composite functor and l is the list of the positions of the non-identity functors in the original list.

Here all the functors in the original list are assumed to either be of the form (Functor i d b o) or be an identity functor.

NatTransReadError is the type of error which can be thrown by read_nat_trans.

• (LookupNatTransError m list) is an error thrown when reading a line representing a horizontal composition of basic natural transformations and identity natural transformations. It says that some id could not be found in the SDNamespace. The number m is the line number where the error occurs is a list of pairs (n,id) where n is the position in the line where id could not be found in the SDNamespace.
• (ImputationError m n) is an error thrown when imputing identity natural transformations on line m. It says that the natural transformation in position n on this line could not be imputed due to the target functor of the previously specified lines is not the composition of enough basic functors.
• (HorzComposeNatTransError m list) is an error thrown when reading a line representing a horizontal composition of basic natural transformations and identity natural transformations. It says that the looked up functors could not be horizontally composed. The number m is the line number where the error occurs, and list is a list of 4-tuples (n1,str1,n2,str2), where n1 is the position in the line of id1 and n2 is the position in the line of id2 and the natural transformations specified by id1 and id2 cannot be horizontally composed. An empty list corresponding to an empty composition.
• NoLinesError is an error which is thrown when there are no lines when specifying the natural transformation.
• FirstLineImputationError is an error which is thrown when the first line in the specification of a natural transformation contains empty places, meaning that these places cannot be imputed.
• (FRE m fre) is an error which is thrown when line m is a line specifying a functor, and fre is a FunctorReadError thrown when reading this line.
• (TwoConsecutiveFunctorsError m) says that line m-1 and line m are both used to specify a functor.
• (IncompatibleLinesError m) says that line m is incompatible with the previously specified lines. If line m is a line specifying a functor, this means that the target of the natural transformation specified by the previous line is not equal to the functor specfied by line m. If line m is a line specifying a natural transformation, it says that the target of the natural transformation specified by the previous lines is not equal to the source of the natural transformation specified by line m.

A helper function in defining error_msg of a LookupNatTransError.

A helper function in defining error_msg of a HorzComposeNatTransError.

list_ce_to_nt takes a list of CompElements representing natural transformations and the current line number and either throws a LookupNatTransError or returns a list of Maybe NaturalTransformation gotten by mapping Empty to Nothing and (CompElement id opts) to Just the corresponding natural transformation from SDNamespace.

ce_to_nt of a CompElement gives Nothing if the CompElement is Nothing, gives Just the corresponding natural transformation from SDNamespace, or throws the id of the CompElement as an error if it could not be found in the SDNamespace.

impute_missing_nat takes the current line number, and a list of Maybe NaturalTransformation and a functor f which is putatively the source of the horizontal composition of the NaturalTransformations in the list. It replaces the Nothings in the list of Maybe NaturalTransformations by the identity natural transformation of the corresponding basic functor in the correct position in f, throwing an ImputationError if this cannot be done.

horz_compose_nats takes the current line number and a list of pairs (id,nt) where id is the id of the natural transformation nt and attempts to take a horizontal composition of the natural transformations. It throws a HorzComposeNatTransError if the natural transformations are not horizontally composable.

get_first_fff takes a list of SDDrawLines and returns the source of the functor they represent along with a FunctorFormatting which is used to format this source functor.

It throws a NoLinesError if there are no lines in the list, and a FirstLineImputationError if the first SDDrawLine is specifying a line for a natural transformation, and Empty is in the list of CompElements. It also throws errors if the first line cannot be read. (i.e. if the first line is a functor line, then it can throw an FRE error. If the first line is a natural transformation line, then it can throw a LookupNatTransError or a HorzComposeNatTransError).

combine_sddl is a helper function for read_nat_trans. It takes

• The current target functor of the previous lines
• A Bool which is true if the previous line was a functor line, and false if it was a natural transformation line
• The current line number
• The current SDDrawLine for this line

and it outputs a tuple of

• The target functor of the new natural transformation
• A Bool which is true if this line was a functor line and false otherwise
• The next line number
• The empty list if the current line was a functor line. A singleton list containing the horizontal composition of the current line for a natural transformation line.
• The empty list if the current line was a natural transformation line. A singleton list corresponding to the functor formatting of the current line if it is a functor line.

It throws a NatTransReadError if there was an error in processing this line.

read_nat_trans takes a list of SDDrawLines and returns a pair (nt,nf) where nt is the NaturalTransformation specified by this list of SDDrawLines, and nf is the NatFormatting specified by the list, used to format nt.

It throws a NatTransReadError if there was an error in processing the list.

A partial function on SDCommands which were constructed using DrawNat. See handle_sdc.

handle_sdc takse an SDCommand and does the corresponding action. For define commands, it adds the corresponding object to the SDNamespace state. For DrawNat commands, it writes the LaTeX code for the specified string diagram to the specified file.

It prints an error message to stderr describing the problem if the command could not be executed.

This function is broken up into the partially defined functions handle_def_cat, handle_def_fun, handle_def_nat and handle_draw_nat.