úÎ*Ä(Á     (C) 2016 Csongor KissBSD3*Csongor Kiss <kiss.csongor.kiss@gmail.com> experimental non-portableSafe !"'(;>KLNShift the focus to the rightShift the focus to the leftyCreate a list from the Zipper by appending together the left lift, the focused element and the right list in this order.+Replace the focused element with a new one.Extract the focused element.ÕConstruct `Zipper a` from `[a]`. The list must contain at least one element for the Zipper to be valid. The resulting Zipper focuses on the first element of the list, the tail of the list is found to the right.Polymorphic list zipper.¤Some functions that operate on Zippers are partial. Instead of having to mess with promoted Maybes and whatnot, this constructor represent an erroneous operation.   (C) 2016 Csongor KissBSD3*Csongor Kiss <kiss.csongor.kiss@gmail.com> experimental non-portableSafe !"'(;>KLN8The ordinary replicate function lifted to the type-levelOMove the focused element of the zipper from a given global position to another2The ordinary max function lifted to the type-leveltRetrieve the number of registers required for running the instructions. This is needed for initialising the machine +Alias to avoid having to tick the promoted   constructor +Alias to avoid having to tick the promoted   constructor +Alias to avoid having to tick the promoted   constructor +Alias to avoid having to tick the promoted   constructor +Alias to avoid having to tick the promoted  constructor%The GADT representing the intructions+The following 3 instructions are supported:Inc r l - increments register r by 1, and then jumps to label l, (that is the instruction located at index l). Dec r l1 l2 - if the value of register r is 0, jumps to l2, otherwise decrements r and jumps to l1.Halt - halts the machine.The ' arguments are specifying the register. Some examples ,Inc (R 1) (L 1) Dec (R 1) (L 7) (L 12) Halt Pointer to a register.SInitialise a register machine (TODO) pre: at least one instruction has to be givenRun a list of instructions ()+If the program terminates, the result is a  machine. (See the  -https://en.wikipedia.org/wiki/Halting_problemHalting problem)^Otherwise the execution hangs the type-checker and eventually consumes all the available RAM.&GADT representing the register machine !"#$ %&     !"#$ %&'        ! "#regis_9FmX1X2LCXg46Cm8qloQ0kData.Type.ZipperLanguage.RM.TypeLevelRightLeftToListReplaceExtractFromListZipperZipInvalidHaltIncDecLRInstrPtrLabelRunMachineHalted ReplicateJumpMaxRequiredRegistersInitJump' AddressOfExecuteGadgetMIszero