SDNamespace

This module defines SDNamespace, a state which keeps track of the defined categories, functors and natural transformations.

The most important function in this module is handle_sdc, which takes a SDCommand and does the corresponding action, i.e. adding it to the SDNamespace state for define actions, and reading from the SDNamespace state and writing an output file for draw actions.

Documentation

class Structure a where

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.

Minimal complete definition

get_id, struct_str, sdns_lens

Methods

get_id

Arguments

:: a

-> String

gets an id string. For functors it is defined for basic functors and identity functors. For natural transformations, it is defined for basic natural transformations, identity natural transformations of basic functors, and identity natural transformations of identity functors of categories.

struct_str

Arguments

:: a

-> String

a string saying which type of structure the object is

sdns_lens

Arguments

:: a

-> Lens' SDNamespace (Namespace a)

A lens for getting the corresponding namespace in an SDNamespace

insertion_error_msg

Arguments

:: a

-> String

derived from get_id and struct_str

Instances

Structure NaturalTransformation

Defined in SDNamespace

Methods

get_id :: NaturalTransformation -> String

struct_str :: NaturalTransformation -> String

sdns_lens :: NaturalTransformation -> Lens' SDNamespace (Namespace NaturalTransformation)

insertion_error_msg :: NaturalTransformation -> String

Structure Functor

Defined in SDNamespace

Methods

get_id :: Functor -> String

struct_str :: Functor -> String

sdns_lens :: Functor -> Lens' SDNamespace (Namespace Functor)

insertion_error_msg :: Functor -> String

Structure Category

Defined in SDNamespace

Methods

get_id :: Category -> String

struct_str :: Category -> String

sdns_lens :: Category -> Lens' SDNamespace (Namespace Category)

insertion_error_msg :: Category -> String

type Namespace a = Map String a

(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.

type SDNamespace = (Namespace Category, Namespace Functor, Namespace NaturalTransformation)

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.

empty_sdns :: SDNamespace

An SDNamespace where all Namespaces are empty.

category :: Lens' SDNamespace (Namespace Category)

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

functor :: Lens' SDNamespace (Namespace Functor)

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

nat_trans :: Lens' SDNamespace (Namespace NaturalTransformation)

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

processing :: Lens' a b -> State b c -> State a c

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.

lens_get :: Lens' a b -> State a b

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

sdns_lookup :: Structure a => String -> Lens' SDNamespace (Namespace a) -> MaybeT (State SDNamespace) a

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.

insert_action' :: Structure a => a -> State (Namespace a) (IO ())

A helper function for insert_action.

insert_action :: Structure a => a -> State SDNamespace (IO ())

(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.

handle_def_cat :: SDCommand -> State SDNamespace (IO ())

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

handle_def_fun :: SDCommand -> State SDNamespace (IO ())

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

handle_def_nat :: SDCommand -> State SDNamespace (IO ())

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

cat_opt_lens :: Lens' Category String

A lens from a Category to its string of options.

func_opt_lens :: Lens' Functor String

A lens from a Functor to its string of options.

nat_opt_lens :: Lens' NaturalTransformation String

A lens from a NaturalTransformation to its string of options.

sdns_lookup_add :: Structure a => String -> Lens' SDNamespace (Namespace a) -> String -> Lens' a String -> MaybeT (State SDNamespace) a

(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 :: String -> String -> MaybeT (State SDNamespace) Functor

(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 :: String -> String -> MaybeT (State SDNamespace) NaturalTransformation

(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.

class Error a where

A class for errors which have error messages.

Methods

error_msg :: a -> String

Instances

Error NatTransReadError

Defined in SDNamespace

Methods

error_msg :: NatTransReadError -> String

Error FunctorReadError

Defined in SDNamespace

Methods

error_msg :: FunctorReadError -> String

data FunctorReadError

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.

Constructors

LookupFunctorError [(Int, String)]

ComposeFunctorError [(Int, String, Int, String)]

Instances

Error FunctorReadError

Defined in SDNamespace

Methods

error_msg :: FunctorReadError -> String

lfe_msg_helper :: (Int, String) -> String

A helper function used to define error_msg of a LookupFunctorError

cfe_msg_helper :: (Int, String, Int, String) -> String

A helper function used to define error_msg of a ComposeFunctorError

read_functor_line :: [CompElement] -> ExceptT FunctorReadError (State SDNamespace) (Functor, FunctorFormatting)

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 :: [CompElement] -> ExceptT FunctorReadError (State SDNamespace) [(Int, String, Functor)]

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 :: [(Int, String, Functor)] -> Except FunctorReadError (Functor, [Int])

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.

data NatTransReadError

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.

Constructors

LookupNatTransError Int [(Int, String)]

ImputationError Int Int

HorzComposeNatTransError Int [(Int, String, Int, String)]

NoLinesError

FirstLineImputationError

FRE Int FunctorReadError

TwoConsecutiveFunctorsError Int

IncompatibleLinesError Int

Instances

Error NatTransReadError

Defined in SDNamespace

Methods

error_msg :: NatTransReadError -> String

lnte_msg_helper :: (Int, String) -> String

A helper function in defining error_msg of a LookupNatTransError.

hcnte_msg_helper :: (Int, String, Int, String) -> String

A helper function in defining error_msg of a HorzComposeNatTransError.

list_ce_to_nt :: [CompElement] -> Int -> ExceptT NatTransReadError (State SDNamespace) [Maybe NaturalTransformation]

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 :: CompElement -> ExceptT String (State SDNamespace) (Maybe NaturalTransformation)

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 :: Int -> [Maybe NaturalTransformation] -> Functor -> Except NatTransReadError [NaturalTransformation]

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 :: Int -> [(String, NaturalTransformation)] -> Except NatTransReadError NaturalTransformation

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 :: [SDDrawLine] -> ExceptT NatTransReadError (State SDNamespace) (Functor, FunctorFormatting)

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 :: Functor -> Bool -> Int -> SDDrawLine -> ExceptT NatTransReadError (State SDNamespace) (Functor, Bool, Int, [NaturalTransformation], [FunctorFormatting])

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 :: [SDDrawLine] -> ExceptT NatTransReadError (State SDNamespace) (NaturalTransformation, NatFormatting)

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.

handle_draw_nat :: SDCommand -> State SDNamespace (IO ())

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

handle_sdc :: SDCommand -> State SDNamespace (IO ())

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.