From 7cc7e91ed86879f6a5a4f11fd3d5c134e788e5f9 Mon Sep 17 00:00:00 2001 From: Evgenii Akentev Date: Fri, 18 Jan 2019 20:28:24 +0100 Subject: [PATCH 1/1] init --- .boring | 6 + Makefile | 18 ++ NetworkAndService.lagda | 69 +++++ Prelude.agda | 70 +++++ Semantics.lagda | 160 +++++++++++ Syntax.lagda | 238 +++++++++++++++++ Theorems.lagda | 213 +++++++++++++++ Typesystem.lagda | 178 ++++++++++++ Typingrules.lagda | 101 +++++++ latex/agda.sty | 580 ++++++++++++++++++++++++++++++++++++++++ latex/iu.jpg | Bin 0 -> 89491 bytes thesis.bib | 396 +++++++++++++++++++++++++++ thesis.lagda | 294 ++++++++++++++++++++ 13 files changed, 2323 insertions(+) create mode 100755 .boring create mode 100755 Makefile create mode 100755 NetworkAndService.lagda create mode 100755 Prelude.agda create mode 100755 Semantics.lagda create mode 100755 Syntax.lagda create mode 100755 Theorems.lagda create mode 100755 Typesystem.lagda create mode 100755 Typingrules.lagda create mode 100755 latex/agda.sty create mode 100755 latex/iu.jpg create mode 100755 thesis.bib create mode 100755 thesis.lagda diff --git a/.boring b/.boring new file mode 100755 index 0000000..4ec1722 --- /dev/null +++ b/.boring @@ -0,0 +1,6 @@ +*~ +latex +*.aux +*.pdf +*.agdai +*.log diff --git a/Makefile b/Makefile new file mode 100755 index 0000000..c59980d --- /dev/null +++ b/Makefile @@ -0,0 +1,18 @@ +AGDA=agda +AFLAGS=-i/Users/ak3n/Develop/agda-stdlib/src -i. --latex --allow-unsolved-metas +SOURCE=thesis +LATEX=latexmk -pdf -use-make -e '$$pdflatex=q/lualatex %O %S/' + +all: + $(AGDA) $(AFLAGS) Prelude.agda + $(AGDA) $(AFLAGS) NetworkAndService.lagda + $(AGDA) $(AFLAGS) Syntax.lagda + $(AGDA) $(AFLAGS) Typesystem.lagda + $(AGDA) $(AFLAGS) Typingrules.lagda + $(AGDA) $(AFLAGS) Semantics.lagda + $(AGDA) $(AFLAGS) Theorems.lagda + $(AGDA) $(AFLAGS) thesis.lagda + cp thesis.bib latex/thesis.bib + cd latex/ && \ + $(LATEX) $(SOURCE).tex && \ + mv $(SOURCE).pdf .. diff --git a/NetworkAndService.lagda b/NetworkAndService.lagda new file mode 100755 index 0000000..0c1bc2a --- /dev/null +++ b/NetworkAndService.lagda @@ -0,0 +1,69 @@ +\if{False} +\begin{code} +-- Imports + +open import Prelude +open import Syntax +open import Typesystem +open import Typingrules +\end{code} +\fi + +\section{Service layer} + +The service layer contains the structures for handling communication, while entities are processes and services. + +At first, we need to define the \AgdaDatatype{MessageQueue}. It's simply just a queue of \AgdaDatatype{Message}s, where \AgdaDatatype{Message} is a tuple of three elements: \AgdaDatatype{Channel}, \AgdaDatatype{Operation} and \AgdaDatatype{String}. To simplify the representation of \AgdaDatatype{Message} I chose it to be a \AgdaDatatype{List} from standard library. + +\begin{code} +Queue : (A : Set) → Set +Queue A = List A + +Message : Set +Message = Channel × Operation × String + +MessageQueue : Set +MessageQueue = Queue Message +\end{code} + +Now we can define the \AgdaDatatype{Process}: + +\begin{code} +data Process : Set where + _∙_∙_ : Behaviour → List Variable → MessageQueue → Process + nil : Process + _∥_ : Process → Process → Process +\end{code} + +The first constructor \AgdaInductiveConstructor{\_∙\_∙\_} represents the process which consists of a behaviour, a list of variables and messages. +The \AgdaDatatype{Process} may be empty: \AgdaInductiveConstructor{nil}. It means that it does nothing at all, has no state and no message queue. It can't even receive messages. \AgdaInductiveConstructor{\_\textdoublevertline\_} is a constructor of the \AgdaDatatype{Process} type for parallel processes. + +Next, I define the \AgdaDatatype{Deployment}, which consists of \AgdaDatatype{AliasingFunction} and \AgdaDatatype{Context}. The deployment contains information about correlation sets for processes running by the service, while each set has variables which are used to identify a process. The \AgdaDatatype{AliasingFunction} is for extracting the location of correlation values for an operation from a message, but it's not required for this project, so it has no constructors. The \AgdaDatatype{Context} will be defined in chapter 3. + +\begin{code} +data AliasingFunction : Set where + +Deployment : Set +Deployment = AliasingFunction × Context +\end{code} + +Finally, \AgdaDatatype{Service} can be defined. It has only one constructor which takes a behaviour, a deployment and a process. + +\begin{code} +data Service : Set where + _▹_-_ : {m : ℕ} → Behaviour → Deployment → Process → Service +\end{code} + +\AgdaDatatype{Service} may behave as a client or as a server. If its behaviour is \AgdaInductiveConstructor{nil}, the service will take a role of a client. If its behaviour is \textit{input choice}, the service will take a role of a server. + +\section{Network layer} + +The network layer describes the structure of a network in a Jolie program. A network is a one or more services running in parallel. Each service is running on a unique location. + +\begin{code} +data Network : Set where + [_]_ : Service → Location → Network + νr : Network → Network + _∥_ : Network → Network → Network + nil : Network +\end{code} diff --git a/Prelude.agda b/Prelude.agda new file mode 100755 index 0000000..161d4df --- /dev/null +++ b/Prelude.agda @@ -0,0 +1,70 @@ +module Prelude where + +open import Data.Empty +open import Function +open import Level using (_⊔_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; setoid) public + +open import Agda.Builtin.List public + using (List; []; _∷_) + +¬_ : ∀ {ℓ} → Set ℓ → Set ℓ +¬ P = P → ⊥ + +data Bool : Set where + true false : Bool + +data String : Set where + +open import Agda.Builtin.Nat public + using ( zero; suc; _+_; _*_ ) + renaming ( Nat to ℕ + ; _-_ to _∸_ ) + +open import Agda.Builtin.Int public + using () + renaming ( Int to ℤ + ; negsuc to -[1+_] -- -[1+ n ] stands for - (1 + n). + ; pos to +_ ) + + +infixr 5 _∷_ +data Vec {a} (A : Set a) : ℕ → Set a where + [] : Vec A zero + _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n) + +infix 4 _∈-Vec_ + +data _∈-Vec_ {a} {A : Set a} : A → {n : ℕ} → Vec A n → Set a where + here : ∀ {n} {x} {xs : Vec A n} → x ∈-Vec x ∷ xs + there : ∀ {n} {x y} {xs : Vec A n} (x∈xs : x ∈-Vec xs) → x ∈-Vec y ∷ xs + +toList : ∀ {a n} {A : Set a} → Vec A n → List A +toList [] = List.[] +toList (x ∷ xs) = List._∷_ x (toList xs) + +infixr 4 _,_ +infixr 2 _×_ +record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where + constructor _,_ + field + proj₁ : A + proj₂ : B proj₁ + +infix 2 Σ-syntax + +Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b) +Σ-syntax = Σ + +syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B + +∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b) +∃ = Σ _ + +∃-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b) +∃-syntax = ∃ + +syntax ∃-syntax (λ x → B) = ∃[ x ] B + +_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b) +A × B = Σ[ x ∈ A ] B diff --git a/Semantics.lagda b/Semantics.lagda new file mode 100755 index 0000000..7cafc6d --- /dev/null +++ b/Semantics.lagda @@ -0,0 +1,160 @@ +\chapter{Semantics of behavioural layer} + +\if{False} +\begin{code} +open import Prelude +open import Typesystem +open import Syntax +\end{code} +\fi + +This chapter describes the semantics of behaviour layer of Jolie, which is described with a labelled transition system. The labels with semantics rules are required for the type preservation property. + +\section{Labels} + +Before the description of the labels, I have to define the type of state. Since actions between behaviours are performed in processes, there is a need to keep the state of them. However, since this project is not an interpreter of Jolie, I don't care what the type of state is, so I chose it to be a natural number. + +\begin{code} +State : Set +State = ℕ +\end{code} + +The semantics of Jolie are described with a labelled transition system. A transition between behaviours can have one of the following labels: + +\begin{code} +data Label : Set where +\end{code} + +The first label \AgdaInductiveConstructor{lb-nil} denotes the lack of action. + +\begin{code} + lb-nil : Label +\end{code} + +Label \AgdaInductiveConstructor{lb-assign} denotes the action of evaluating expression $e$ and the assignment the result to the variable $x$. + +\begin{code} + ---- x = e + lb-assign : Variable → Expr → Label +\end{code} + +Label \AgdaInductiveConstructor{lb-read} denotes reading the state $t$ of the underlying process. + +\begin{code} + ---- read t + lb-read : State → Label +\end{code} + +The two following labels are dual. Their purpose is unidirectional communication and in the first part of bidirectional communication. Label \AgdaInductiveConstructor{lb-send} denotes sending an expression $e$ through an operation $o$ to a location $l$ over a fresh channel $r$. + +\begin{code} + ---- νr o@l(e) + lb-send : Channel → Operation → Location → Expr → Label +\end{code} + +Label \AgdaInductiveConstructor{lb-store} denotes storing storing in a variable $x$ a message received through an operation $o$ over a channel $r$. + +\begin{code} + ---- r : o(x) + lb-store : Channel → Operation → Variable → Label +\end{code} + +The next two labels are dual too. They are intended for the second of part of bidirectional communication. Label \AgdaInductiveConstructor{lb-write} denotes writing a variable $x$ at channel $r$ as part of an operation $o$. + +\begin{code} + ---- (r, o)!x + lb-write : Channel → Operation → Variable → Label +\end{code} + +And the last one label \AgdaInductiveConstructor{lb-read-write} denotes reading a message from channel $r$ as part of an operation $o$ and storing it in a variable $x$. + +\begin{code} + ---- (r, o@l)?x + lb-read-write : Channel → Operation → Location → Variable → Label +\end{code} + +There are also five more labels, but they are used in the service layer. + +\section{Semantic rules} + +There were created 17 semantic rules for the behavioural layer, but I present only the subset of them. + +Since semantic rules use the current state of processes, there is a need in such function which allows getting the value of expression at the current state. I express such function as a type: + +\begin{code} +data _⟨_⟩≔_ : Expr → State → Expr → Set where + stub : ∀ {e₁ s e₂} → e₁ ⟨ s ⟩≔ e₂ +\end{code} + +The \AgdaInductiveConstructor{stub} constructor is very simple and should be replaced with a normal mechanism for working with states in the future. It's needed to make the type inhabited. + +The following type expresses the semantic rules (transitions). It consists of two behaviours and a label. + +\begin{code} +data _↝_∶_ : Behaviour → Behaviour → Label → Set where +\end{code} + +The first constructor is intended for the \AgdaInductiveConstructor{nil} behaviour. It constructs the type with two \AgdaInductiveConstructor{nil}s and one \AgdaInductiveConstructor{lb-nil} label. + +\begin{code} + b-nil : nil ↝ nil ∶ lb-nil +\end{code} + +The \AgdaInductiveConstructor{b-assign} rule takes a variable $x$ and an expression $e$ and constructs the type with the variable $x$, the expression $e$, the behaviour \AgdaInductiveConstructor{nil} and the label \AgdaInductiveConstructor{lb-assign}. It means that the assignment action is performed in the transition to the \AgdaInductiveConstructor{nil} behaviour. + +\begin{code} + b-assign : {x : Variable} {e : Expr} + → (x ≃ e) ↝ nil ∶ lb-assign x e +\end{code} + +The constructor is pretty simple. It checks if the value of an expression $e$ is true, then it takes a transition from the \AgdaInductiveConstructor{if\_then\_else} behaviour to the $b_1$ behaviour. Its label is \AgdaInductiveConstructor{lb-read} because it needs to get the value of the expression from the state. + +\begin{code} + b-if-then : {e : Expr} {t : State} {b₁ b₂ : Behaviour} + → e ⟨ t ⟩≔ (constant (bool true)) + → (if e then b₁ else b₂) ↝ b₁ ∶ lb-read t +\end{code} + +This rule is similar to the previous one. The difference is that it's indended for the case when the value of the expression $e$ is false. The result of a transition is the $b_2$ behaviour. + +\begin{code} + b-if-else : {e : Expr} {t : State} {b₁ b₂ : Behaviour} + → e ⟨ t ⟩≔ (constant (bool false)) + → (if e then b₁ else b₂) ↝ b₂ ∶ lb-read t +\end{code} + +The two following rules are standard. They describe the behaviour of the \AgdaInductiveConstructor{while[\_]\_} statement. They are under the \AgdaInductiveConstructor{lb-read} label too. \AgdaInductiveConstructor{b-iteration} iterates if the value of the expression is true and \AgdaInductiveConstructor{b-no-iteration} does nothing if the value is false. + +\begin{code} + b-iteration : {e : Expr} {t : State} {b : Behaviour} + → e ⟨ t ⟩≔ (constant (bool true)) + → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ lb-read t + + b-no-iteration : {e : Expr} {t : State} {b : Behaviour} + → e ⟨ t ⟩≔ (constant (bool false)) + → (while[ e ] b) ↝ nil ∶ lb-read t +\end{code} + +The semantic rules for the parallel and sequence behaviours are standard too. If there is a transition $ B_1 \xrightarrow{\eta} B_1' $, then the resulting transition is possible for both semantic rules. + +\begin{code} + b-seq : {b₁ b₂ b₁′ : Behaviour} {η : Label} + → b₁ ↝ b₁′ ∶ η + → (b₁ ∶ b₂) ↝ (b₁′ ∶ b₂) ∶ η + + b-par : {b₁ b₂ b₁′ : Behaviour} {η : Label} + → b₁ ↝ b₁′ ∶ η + → (b₁ ∥ b₂) ↝ (b₁′ ∥ b₂) ∶ η +\end{code} + +The last semantic rule is called \AgdaInductiveConstructor{b-struct}. It means that if there are two equal behaviours $b_1$ and $b_2$, a transition $ b_2 \xrightarrow{\eta} b_2' $ and $b_1'$ is equal to $b_2'$, then there is a transition $ b_1 \xrightarrow{\eta} b_1' $. This rule states that behaviours that are structurally congruent have the same transitions. + +\begin{code} + b-struct : {b₁ b₂ b₁′ b₂′ : Behaviour} {η : Label} + → b₁ ≡ b₂ + → b₂ ↝ b₂′ ∶ η + → b₁′ ≡ b₂′ + → b₁ ↝ b₁′ ∶ η +\end{code} + +The definition of structural congruence for behaviours is given in the next chapter with the lemma and its proof. diff --git a/Syntax.lagda b/Syntax.lagda new file mode 100755 index 0000000..018dfc1 --- /dev/null +++ b/Syntax.lagda @@ -0,0 +1,238 @@ +\chapter{Syntax} + +\if{False} +\begin{code} +-- Imports + +open import Prelude +\end{code} +\fi + +Formal syntax and semantic of Jolie are based on SOCK process calculi~\cite{Gui07,Guidi}. +SOCK was created for designing service-oriented systems and was inspired by notable $\pi$-calculus \cite{Milner1999} and WS-BPEL~\cite{BPEL}. +Primitives in SOCK are able to express one-way and request-response communication, parallel and sequential behaviour of processes and control primitives. + +SOCK (so a formalization of Jolie program) comprises of three layers: + +\begin{itemize} +\item \textit{Behavioural layer}: specifies with internal actions of a process and communication +performs as seen from the process’ point of view. +\item \textit{Service layer}: it deals with underlying +architectural instructions, states, service instances and correlation sets. +\item \textit{Network layer}: is in charge of connecting and interacting of communicating services. +\end{itemize} + +This chapter has three sections about the syntax of layers of Jolie. They contain the definition of abstract syntax tree in Agda and their description. + + +\section{Behaviour layer} + +The most important type of statements in behavioural level regards performing communications and handling data. Statements in this layer are called behaviours. Also, there are variables and expressions. + +\subsubsection{Handling data} +Communication messages in Jolie are represented by trees. Variables are paths in data trees and the type of the a data tree is a tree too. Communications are type checked at run-time when a message is received, and such type checking is formally defined at ~\cite{nielsen2013type}. For example: + +\begin{center} + amount = 12\\ + amount.fruit.apple = 2\\ + amount.fruit.description = "Apple"\\ +\end{center} + +The \textit{amount} variable represents the following tree: + +\Tree [ .{amount = 12} [ .fruit [ .{apple = 2} ] + [ .{description = "Apple"} ] ] ] + +\vspace{0.5cm} + +To simplify further operations with variables, we propose their enumeration. Let $ J $ be a Jolie program, +$ V = vars(J) $ -- variables in $ J $, then $ V_i = i$ where $i \in \mathbb{N} $. +Then the example above will look like: + +\Tree [ .$V_0$ [ .$V_1$ ] + [ .$V_2$ ]] + +\begin{center} + $V_0 =$ amount = 12 \Rightarrow\ 0\\ + $V_1 =$ amount.fruit.apple = 2 \Rightarrow\ 1\\ + $V_2 =$ amount.fruit.description = "Apple" \Rightarrow\ 2\\ +\end{center} + +After this simplification, the type of variables can be defined. The type of natural numbers \AgdaDatatype{ℕ} is located in the standard library of Agda~\cite{agdastdlib}. + +\begin{code} +Variable : Set +Variable = ℕ +\end{code} + +Next, I define the possible values in Jolie. They are usual as in almost every programming language: strings, ints, booleans, doubles, longs and void. \AgdaDatatype{String}, \AgdaDatatype{Bool} and \AgdaDatatype{ℤ} are datatypes from the standard library. + +\begin{code} +data Value : Set where + string : String → Value + int : ℤ → Value + bool : Bool → Value + double : ℤ → ℤ → Value + long : ℤ → Value + void : Value +\end{code} + +Usually, there are binary and unary operations. Binary operations may be arithmetical (plus, minus, multiplication, division and power) and logical (equality, and, or). I define only one unary operation: $not$. + +\begin{code} +data BinaryOp : Set where + -- Arithmetical + plus minus mult div power : BinaryOp + -- Logical operations + equal and or : BinaryOp + +data UnaryOp : Set where + not : UnaryOp +\end{code} + +Next, I define the type of expressions. Expressions may contain variables, binary operations, unary operations and constants. + +\begin{code} +data Expr : Set where + var : Variable → Expr + binary : BinaryOp → Expr → Expr → Expr + unary : UnaryOp → Expr → Expr + constant : Value → Expr +\end{code} + +Here are some examples of expressions which are possible to construct: + +\begin{itemize} + +\item $ 2 + 2 $ + +\begin{code} +2+2 : Expr +2+2 = binary plus (constant (int (+ 2))) (constant (int (+ 2))) +\end{code} + +\item $x + 1$ +\begin{code} +x : Variable +x = 0 + +x+1 : Expr +x+1 = binary plus (var x) (constant (int (+ 1))) +\end{code} + +\item $ A \land B $ + +\begin{code} +A B : Variable +A = 0 +B = 1 + +A∧B : Expr +A∧B = binary and (var A) (var B) +\end{code} + +\end{itemize} + +\subsubsection{Communications} + +There are two types of communication statements in Jolie: input and output statements, both can be uni-directional (one-way operations) and bi-directional (request-response operations). In the case of output statements, we use the notion of an output port name (location) which is necessary for binding the communicated data to it. The data is made use by communication statements as variable paths and expressions described above. + +Operation names, channel names and locations (usually are URLs) are represented by strings. + +\begin{code} +Operation Location Channel : Set +Operation = String +Location = String +Channel = String +\end{code} + + +The following two types are called communication ports. They define how communications with other services are performed. There are two kinds of ports: + +\if{False} +\begin{code} +data Behaviour : Set +\end{code} +\fi + +\begin{itemize} +\item \textit{Input ports}: they deal with exposing input operations to other services. + +\begin{code} +data η : Set where + -- o(x) -- One-way + _[_] : Operation → Variable → η + + -- o(x)(x'){B} -- Request-response + _[_][_]_ : Operation → Variable → Variable → Behaviour → η +\end{code} + +\item \textit{Output ports}: they define how to invoke a set of operations of other services. + +\begin{code} +data η^ : Set where + -- o@l(e) -- Notification + _at_[_] : Operation → Location → Expr → η^ + + -- o@l(e)(x) -- Solicit-response + _at_[_][_] : Operation → Location → Expr → Variable → η^ +\end{code} + +\end{itemize} + +\subsubsection{Behaviour} + +The behavioural layer has both ordinary control--flow statements ('if-then-else', 'while', 'assign') +and special statements to control parallelism and communication ('inputchoice', 'parallel', 'input', 'output', etc). + +\begin{code} +data Behaviour where + if_then_else_ : Expr → Behaviour → Behaviour → Behaviour + while[_]_ : Expr → Behaviour → Behaviour + -- Sequence + _∶_ : Behaviour → Behaviour → Behaviour + -- Parallel + _∥_ : Behaviour → Behaviour → Behaviour + -- Assign + _≃_ : Variable → Expr → Behaviour + nil : Behaviour + -- [η₁]{B₁}⋯[ηₐ]{Bₐ} + inputchoice : List (η × Behaviour) → Behaviour + wait : Channel → Operation → Location → Variable → Behaviour + exec : Channel → Operation → Variable → Behaviour → Behaviour + input : η → Behaviour + output : η^ → Behaviour +\end{code} + +The \textit{input choices} behaviour is a list of options where each element represents the tuple of guard $\eta$ and the behaviour $b$, which is executed if $\eta$ allows. \textit{wait} and \textit{exec} are runtime behaviours. They are required for the preservation property of the type system. + +Here are some examples of behaviours which are possible to construct: + +\begin{itemize} + +\item The first example is a \AgdaDatatype{nothing} function. It takes any behaviour and does nothing. + +\begin{code} +nothing : Behaviour → Behaviour +nothing _ = nil +\end{code} + +\item + +Notice, that \AgdaDatatype{Behaviour} has only \AgdaInductiveConstructor{if\_then\_else} constructor, but not \AgdaDatatype{if\_then} without `else` branch. This can be solved by defining a function \AgdaDatatype{if-then} which takes an expression and a behaviour for the branch, which is called when the expression is true. + +\begin{code} +if-then : Expr → Behaviour → Behaviour +if-then condition behaviour = if condition then behaviour else nil +\end{code} + +\item The last example is the \AgdaDatatype{always} function. It's an infinite while loop which executes a given behaviour. + +\begin{code} +always : Behaviour → Behaviour +always behaviour = while[ constant (bool true) ] behaviour +\end{code} + +\end{itemize} + +\input{NetworkAndService} diff --git a/Theorems.lagda b/Theorems.lagda new file mode 100755 index 0000000..7ca3ff5 --- /dev/null +++ b/Theorems.lagda @@ -0,0 +1,213 @@ +\chapter{Proofs of properties} + +\if{False} +\begin{code} +-- Imports +{-# OPTIONS --allow-unsolved-metas #-} +open import Prelude + +open import Syntax +open import Typesystem +open import Typingrules +open import Semantics +\end{code} +\fi + +According to the Curry-Howard isomorphism~\cite{Sorensen}, types of the programs are propositions and terms are proofs. For example, the type $ A \rightarrow B $ corresponds to the implication from $ A $ to $ B $, and, at the same time, such function $ f $ that takes an element of type $ A $ and returns an element of type $ B $ will be a proof of this theorem. + +To demonstrate the correctness of the typing rules given before, I provide the proof of the lemma called "Structural Congruence for Behaviours"~\cite{nielsen2013type,engelfriet} and the proofs of particular cases of "Type preservation of behaviours". + +\section{Structural Congruence for Behaviours}\label{sec:strcongr} + +Since Jolie~\cite{montesi2010jolie} is based on $\pi$-calculus~\cite{Milner1999}, it should have the same properties. $\pi$-calculus has the following structural congruence rules, which apply at behaviour layer in Jolie: + +$$ (B_1\ |\ B_2)\ |\ B_3 \equiv B_1\ |\ (B_2\ |\ B_3) $$ +$$ 0\ ;\ B\ \equiv B $$ +$$ B_1\ |\ B_2 \equiv B_2\ |\ B_1 $$ +$$ B\ |\ 0 \equiv B $$ + +Two structural congruent behaviours are typable with respect to the same environment and they make the same updates to the environment during type checking: + +\newpage + +\begin{lemma} Structural Congruence for Behaviours + +\begin{center} +\textit{Let} $ \Gamma \vdash B_1 \rhd \Gamma' $ \\ +\textit{If} $ B_1 \equiv B_2 $ \\ +\textit{then} $ \Gamma \vdash B_2 \rhd \Gamma' $ +\end{center} + +\end{lemma} + +\begin{proof} +The proof is the case analysis of all possible behaviours $ B_1 $ and $ B_2 $ according to the rules provided above. + +\begin{itemize} + +\item \textit{Case} $ B_1 \equiv B_2 $ + +The proof is done by Agda's pattern matching mechanism. Since \AgdaDatatype{b_1 ≡ b_2}, Agda replaces $b_1$ in the term t to $b_2$. + +\begin{code} +struct-cong-b₁≡b₂ : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour} + → Γ ⊢B b₁ ▹ Γ₁ + → b₁ ≡ b₂ + → Γ ⊢B b₂ ▹ Γ₁ +struct-cong-b₁≡b₂ t refl = t +\end{code} + +\item \textit{Case} $ 0; B \equiv B $ + +This proof is done by decomposing the term by pattern matching. + +\begin{code} +struct-cong-nil∶b→b : {Γ Γ₁ : Context} {b : Behaviour} + → Γ ⊢B nil ∶ b ▹ Γ₁ + → Γ ⊢B b ▹ Γ₁ +struct-cong-nil∶b→b (t-seq t-nil x) = x +\end{code} + +\item \textit{Case} $ B \equiv 0 ; B $ + +In this proof, instead of decomposition, I construct the resulting term by using $x$. + +\begin{code} +struct-cong-b→nil∶b : {Γ Γ₁ : Context} {b : Behaviour} + → Γ ⊢B b ▹ Γ₁ + → Γ ⊢B nil ∶ b ▹ Γ₁ +struct-cong-b→nil∶b x = t-seq t-nil x +\end{code} + +\item \textit{Case} $ B \parallel 0 \equiv B $ +\begin{code} +struct-cong-b∥nil→b : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b : Behaviour} + → & Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ & Γ₁' Γ₂' + → Γ₁ ⊢B b ▹ Γ₁' +struct-cong-b∥nil→b (t-par x _) = x +\end{code} + +\item \textit{Case} $ B \equiv B \parallel 0 $ + +\begin{code} +struct-cong-b→b∥nil : {Γ₁ Γ₂ Γ₃ : Context} {b : Behaviour} + → Γ₁ ⊢B b ▹ Γ₂ + → & Γ₁ Γ₃ ⊢B (b ∥ nil) ▹ & Γ₂ Γ₃ +struct-cong-b→b∥nil x = t-par x t-nil +\end{code} + +\item \textit{Case} $ B_1 \parallel B_2 \equiv B_2 \parallel B_1 $ + +In this case, I just swap terms $t_1$ and $t_2$. + +\begin{code} +struct-cong-par-comm : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour} + → & Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ & Γ₁' Γ₂' + → & Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ & Γ₂' Γ₁' +struct-cong-par-comm (t-par t₁ t₂) = t-par t₂ t₁ +\end{code} + +\item \textit{Case} $ (B_1 \parallel B_2) \parallel B_3 \equiv B_1 \parallel (B_2 \parallel B_3) $ + +The last proof is the most complex one, but it's just a swapping of terms too. + +\begin{code} +struct-cong-par-assoc : {Γ₁ Γ₂ Γ₃ Γ₁' Γ₂' Γ₃' : Context} {b₁ b₂ b₃ : Behaviour} + → & (& Γ₁ Γ₂) Γ₃ ⊢B (b₁ ∥ b₂) ∥ b₃ ▹ & (& Γ₁' Γ₂') Γ₃' + → & Γ₁ (& Γ₂ Γ₃) ⊢B b₁ ∥ (b₂ ∥ b₃) ▹ & Γ₁' (& Γ₂' Γ₃') +struct-cong-par-assoc (t-par (t-par t1 t2) t3) = t-par t1 (t-par t2 t3) +\end{code} + +The proof for $ B_1 \parallel (B_2 \parallel B_3) \equiv (B_1 \parallel B_2) \parallel B_3 $ is similar. + +\end{itemize} +\end{proof} + +\section{Type preservation for behaviours} + +Type preservation is a property such that if a well-typed behaviour takes a transition then the resulting behaviour is well-typed too. Since the typing rule (or judgement) for behaviours is a Hoare triple which consists of an initial environment, a behaviour and a resulting environment, type preservation property requires that the resulting environment for a behaviour after a transition is equal to the resulting environment for the behaviour before the transition. + +At first, I need to define what a transition or a side effect is. The type preservation property takes place when a behaviour takes a transition. Actions are performed during the transitions, therefore the transition function is defined with respect to the performed action. + +Let $B$ and $B'$ be two behaviours and $\eta$ is a label defined before in chapter 4. Suppose that there is a transition $ B \xrightarrow{\eta} B' $, $B$ is typed with respect to $\Gamma$, $B'$ is typed with respect to $\Gamma'$, then the relation between $\Gamma$ and $\Gamma'$ is defined as a side effect of $\eta$. It is described as the type \AgdaDatatype{\_↦⟨\_⟩\_}: + +\begin{code} +data _↦⟨_⟩_ : Context → Label → Context → Set where +\end{code} + +The first constructor of that type is \AgdaInductiveConstructor{s-nil}. It shows that nothing is done to the context since the label is \AgdaInductiveConstructor{lb-nil}. + +\begin{code} + s-nil : {Γ : Context} + → Γ ↦⟨ lb-nil ⟩ Γ +\end{code} + +The same thing is with \AgdaInductiveConstructor{lb-read} label. It has no any side effects. + +\begin{code} + s-read : {Γ : Context} {t : State} + → Γ ↦⟨ lb-read t ⟩ Γ +\end{code} + +The \AgdaInductiveConstructor{s-assign} constructor is for the assignment behaviour when the variable is already in the context. It does not effect the context. + +\begin{code} + s-assign : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + → Γ ⊢ₑ e ∶ Tₑ + → x ∶ Tₓ ∈ Γ + → Tₓ ≡ Tₑ + → Γ ↦⟨ lb-assign x e ⟩ Γ +\end{code} + +The next three constructors are cases of adding a variable in the context for the assignment behaviour. They are similar to typing rules for the assignment behaviour. The first one is for simple context and the two last are for a disjoint union context. It's important to notice that the label is \AgdaInductiveConstructor{lb-assign} $x$ $e$. It depends on the variable $x$ and the expression $e$. + +\begin{code} + s-assign-upd : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + → ⋆ Γ ⊢ₑ e ∶ Tₑ + → ¬ (x ∶ Tₓ ∈ ⋆ Γ) + → ⋆ Γ ↦⟨ lb-assign x e ⟩ ⋆ ((x ∶ Tₓ) ∷ Γ) + + s-assign-upd-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} + {e : Expr} {Tₓ Tₑ : Type} + → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ + → ¬ (x ∶ Tₓ ∈ & (⋆ Γ) (⋆ Γ₁)) + → & (⋆ Γ) (⋆ Γ₁) ↦⟨ lb-assign x e ⟩ & (⋆ ((x ∶ Tₓ) ∷ Γ)) (⋆ Γ₁) + + s-assign-upd-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} + {e : Expr} {Tₓ Tₑ : Type} + → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ + → ¬ (x ∶ Tₓ ∈ & (⋆ Γ) (⋆ Γ₁)) + → & (⋆ Γ) (⋆ Γ₁) ↦⟨ lb-assign x e ⟩ & (⋆ Γ) (⋆ ((x ∶ Tₓ) ∷ Γ₁)) +\end{code} + + +Assume that $B$ is a well-typed behaviour typed with respect to an environment $\Gamma$ and $\Gamma'$ is a resulting environment. Suppose that there is a behaviour $B'$ such that $ B \xrightarrow{\eta} B' $. Then there is an environment $\Gamma''$ which is an update of $\Gamma$, caused by as a result of side effect with label $\eta$ and $ B'$ is typed with respect to the environments $\Gamma''$ and $\Gamma'$: + +\begin{theorem} Type Preservation for Behaviours +\begin{center} +\textit{If} $ \Gamma \vdash _{B} B \rhd \Gamma' $ \\ +\textit{and} $ B \xrightarrow{\eta} B' $ \\ +\textit{then} $ \Gamma'' \vdash _{B} B' \rhd \Gamma' $ \\ +\textit{where} $ \Gamma'' =$ \textit{sideEffect} $ (\eta,\ \Gamma) $ +\end{center} +\end{theorem} + + +\begin{proof} The proofs of simple cases are a case analysis of a typing rule, a side effect and a semantic rule. The type is almost the same as the theorem, but there is one difference. In the theorem, $\Gamma''$ may be replaced with the \textit{sideEffect} $ (\eta,\ \Gamma) $, but in the type of \AgdaDatatype{type-preservation}, I use a side effect as an additional argument. + +\begin{code} +type-preservation : {Γ Γ′ Γ′′ : Context} {b b′ : Behaviour} {η : Label} + → Γ ⊢B b ▹ Γ′ + → b ↝ b′ ∶ η + → Γ ↦⟨ η ⟩ Γ′′ + → Γ′′ ⊢B b′ ▹ Γ′ +type-preservation t-nil b-nil s-nil = t-nil +type-preservation (t-if x t t₁) (b-if-then _) s-read = t +type-preservation (t-if x t t₁) (b-if-else _) s-read = t₁ +type-preservation (t-assign-exists _ _ _) (b-assign) (s-assign _ _ _) = t-nil +type-preservation = {!!} +\end{code} + +The last line is a type hole. It means that the proof is not complete, not all cases of arguments are covered. Other cases are intended for the future research. + +\end{proof} diff --git a/Typesystem.lagda b/Typesystem.lagda new file mode 100755 index 0000000..5c45d63 --- /dev/null +++ b/Typesystem.lagda @@ -0,0 +1,178 @@ +\chapter{Type system}\label{sec:typesys} + +\if{False} +\begin{code} +-- Imports +open import Prelude + +open import Syntax +\end{code} +\fi + +Jolie type system consists of trees because they are matched to variables, which are trees. Variables are simplified by enumeration, as it was mentioned before, and so types too. + +Therefore, basic types of Jolie are just usual types, which are commonly-used native types such as \jkeyw{int}, \jkeyw{double}, \jkeyw{long}, \jkeyw{boolean} and \jkeyw{string}. Also, Jolie has the following types: + +\begin{itemize} +\item \jkeyw{raw}, representing raw data streams as byte arrays. +\item \jkeyw{void}, indicating no value. +\item \jkeyw{any}, as a placeholder for any native types. +\end{itemize} + +In order to be able to do type checking of a Jolie program, I provide the implementation of types and typing rules in Agda. + +\section{Types declaration} + +The main Jolie native types (excluding any) are expressed in the following way: + +\begin{code} +data Type : Set where + bool int double long string raw void : Type +\end{code} + +Usually, the context of a program is a list of variables, but to service all three layers (comprising communication of services) there is a special type called \AgdaDatatype{TypeDecl}. It has five constructors: the first two (unidirectional and bidirectional) are for output communication. The left part of such bindings consists of an operation name and a location of a hosting service. The next two are for input communication and the last one is for variables. + +\begin{code} +data TypeDecl : Set where + -- o@l : + _at_∶<_> : Operation → Location → Type → TypeDecl + + -- o@l : + _at_∶<_,_> : Operation → Location → Type → Type → TypeDecl + + -- o : + _∶<_> : Operation → Type → TypeDecl + + -- o : + _∶<_,_> : Operation → Type → Type → TypeDecl + + -- x : T + _∶_ : Variable → Type → TypeDecl +\end{code} + +Therefore, the type of context is a vector of \AgdaDatatype{TypeDecl}. + +\begin{code} +Ctx : ℕ → Set +Ctx = Vec TypeDecl +\end{code} + +Although the type of context is defined, it's not enough, because programs in Jolie can be parallel. In ~\cite{nielsen2013type}, there is a constructor of a disjoint union of the \AgdaDatatype{TypeDecl} to make programs parallel. In this project, the disjoint union is defined as a wrapper of \AgdaDatatype{TypeDecl}. I define one more type called \AgdaDatatype{Context} to cover such situations. It has only two constructors: the first one just takes \AgdaDatatype{Ctx\ n} and the second one consists of two elements of itself. + +\begin{code} +data Context : Set where + ⋆ : ∀ {n} → Ctx n → Context + & : Context → Context → Context +\end{code} + +The type of context is not a vector anymore, so here is the definition of such type that will express the fact of the presence of \AgdaDatatype{TypeDecl} in \AgdaDatatype{Context}: + +\begin{code} +infix 4 _∈_ +data _∈_ : TypeDecl → Context → Set where +\end{code} + +I define the type \AgdaDatatype{\_\in\_} to be infix with priority $4$. This type takes other two types: \AgdaDatatype{TypeDecl} and \AgdaDatatype{Context}. It means that by constructing the type $ T \in C $, where $ T $ has type \AgdaDatatype{TypeDecl} and $ C $ has type \AgdaDatatype{Context}, the proposition "T is an element of C" is being formulated. + +Let's start with the first constructor of \AgdaDatatype{Context}: \AgdaInductiveConstructor{⋆}. It is the simple case when the context is just a \AgdaDatatype{Ctx} $n$. The constructor \AgdaInductiveConstructor{here-⋆} means that some element $x$ is the first element of context. In the second case, \AgdaInductiveConstructor{there-⋆} takes the term of type $x ∈ ⋆ xs$, which states that $x$ is an element of $xs$ with type \AgdaDatatype{Ctx} $n$, and states that we can add any element to $xs$. +\begin{code} + here-⋆ : ∀ {n} {x} {xs : Ctx n} + → x ∈ ⋆ (x ∷ xs) + + there-⋆ : ∀ {n} {x y} {xs : Ctx n} + (x∈xs : x ∈ ⋆ xs) + → x ∈ ⋆ (y ∷ xs) +\end{code} + +The constructors \AgdaInductiveConstructor{here-left-\&} and \AgdaInductiveConstructor{here-right-\&} are for the second case when the context is a disjoint union. They state that $x$ is an element of the left context or the right context of the disjoint union. + +\begin{code} + here-left-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} + → x ∈ & (⋆ (x ∷ xs)) (⋆ ys) + + here-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} + → x ∈ & (⋆ xs) (⋆ (x ∷ ys)) +\end{code} + +The two last constructors are similar to \AgdaInductiveConstructor{there-⋆}, but for the disjoint union. + +\begin{code} + there-left-& : ∀ {n m} {x y} {xs : Ctx n} {ys : Ctx m} + (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) + → x ∈ & (⋆ (y ∷ xs)) (⋆ ys) + + there-right-& : ∀ {n m} {x y} {xs : Ctx n} {ys : Ctx m} + (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) + → x ∈ & (⋆ xs) (⋆ (y ∷ ys)) +\end{code} + +To demonstrate the examples of using the type of context and the type of presence described before I need to define preliminary types. Let $y$ and $z$ are variables: + +\begin{code} +y z : Variable +y = 0 +z = 1 +\end{code} + +The type of variables doesn't matter in this case, so it's just a boolean. + +\begin{code} +Ty : Type +Ty = bool +\end{code} + +$C1$, $C2$, $C3$ and $C4$ are contexts. $C1$ is a simple context with only one element \AgdaDatatype{y} $:$ \AgdaDatatype{Ty} (variable \AgdaDatatype{y} with type \AgdaDatatype{Ty}), while $C2$ is a simple context too, but with two variables \AgdaDatatype{z} and \AgdaDatatype{y}. $C3$ and $C4$ are disjoint union context for parallel behaviours. $C3$ has $C1$ as a left context and its right context is empty. $C4$ has $C2$ as a right context and its left context is empty. + +\begin{code} +C1 C2 C3 C4 : Context +C1 = ⋆ (y ∶ Ty ∷ []) +C2 = ⋆ (z ∶ Ty ∷ y ∶ Ty ∷ []) +C3 = & C1 (⋆ []) +C4 = & (⋆ []) C2 +\end{code} + +Here are examples which use the type of context and the type of presence items in context: + +\begin{itemize} + +\item The first example is pretty simple. I state that the variable \AgdaDatatype{y} of type \AgdaDatatype{Ty} is an element of the context $C1$. The proof of such statement, which is a type at the same time, is just a term \AgdaInductiveConstructor{here-⋆} because $C1$ has only one element and \AgdaInductiveConstructor{here-⋆} states that \AgdaDatatype{y} $:$ \AgdaDatatype{Ty} is the first element of $C1$. + +\begin{code} +y∈C1 : (y ∶ Ty) ∈ C1 +y∈C1 = here-⋆ +\end{code} + +\item In $C2$ the variable \AgdaDatatype{y} is the second element. To express that fact I need to use \AgdaInductiveConstructor{there-⋆}, because \AgdaDatatype{\_\in\_} is an inductive type. \AgdaInductiveConstructor{there-⋆} takes the term of type $x$ \AgdaDatatype{\in} \AgdaInductiveConstructor{⋆} $xs$, which is \AgdaInductiveConstructor{here-⋆} in this case, and states that $x$ is somewhere in this context. + +\begin{code} +y∈C2 : (y ∶ Ty) ∈ C2 +y∈C2 = there-⋆ here-⋆ +\end{code} + +\item In this case, \AgdaDatatype{y} is the first element of the left context of the disjoint union context $C3$, that's why \AgdaInductiveConstructor{here-left-\&} is used. + +\begin{code} +y∈C3 : (y ∶ Ty) ∈ C3 +y∈C3 = here-left-& +\end{code} + +\item The last example is similar to examples with $C2$ and $C3$. $C4$ is a disjoint union context where the \AgdaDatatype{y} variable is in the right context on the second place. + +\begin{code} +y∈C4 : (y ∶ Ty) ∈ C4 +y∈C4 = there-right-& here-right-& +\end{code} + +\end{itemize} + +Next, I define the type of a correctly typed expression with variables from context $ \Gamma $. + +\begin{code} +data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where + expr-t : {s : Expr} {b : Type} + → Γ ⊢ₑ s ∶ b +\end{code} + +The \AgdaInductiveConstructor{expr-t} constructor is a simplified version because it should check all variables in the expression $s$ from context $ \Gamma $. In this work, it's assumed that all given expressions are correct. + +\input{Typingrules} diff --git a/Typingrules.lagda b/Typingrules.lagda new file mode 100755 index 0000000..577a3de --- /dev/null +++ b/Typingrules.lagda @@ -0,0 +1,101 @@ +\section{Typing rules for behaviour layer} + +\if{False} +\begin{code} +-- Imports +open import Prelude +open import Syntax +open import Typesystem +\end{code} +\fi + +There were created 28 typing rules for behaviour layer during the development. Some of them are almost similar to the rules from the basement of this work~\cite{nielsen2013type}. I demonstrate the subset of the typing rules. + +In ~\cite{nielsen2013type}, if a behaviour $b$ is typed with respect to an environment $\Gamma$ and changes it during type checking to an environment $\Gamma_1$, then it is written as $\Gamma \vdash_{B} b \vartriangleright \Gamma_1$ in the form of Hoare triple. + +\begin{code} +data _⊢B_▹_ : Context → Behaviour → Context → Set where +\end{code} + +The following constructors of this type express the typing rules and they are used for type checking behaviours. The first constructor is for the \AgdaInductiveConstructor{nil} behaviour. Since \AgdaInductiveConstructor{nil} does nothing, the context before and the context after are equal. + +\begin{code} + t-nil : {Γ : Context} + → Γ ⊢B nil ▹ Γ +\end{code} + +The \AgdaInductiveConstructor{t-if} constructor is intended for \AgdaInductiveConstructor{if\_then\_else} behaviour. It takes three arguments: a type which states that the expression $e$ has type \AgdaInductiveConstructor{bool}, two types which state that the behaviours $b_1$ and $b_2$ are well-typed. The result of this constructor is well typed \AgdaInductiveConstructor{if\_then\_else} behaviour. + +\begin{code} + t-if : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour} {e : Expr} + → Γ ⊢ₑ e ∶ bool + → Γ ⊢B b₁ ▹ Γ₁ + → Γ ⊢B b₂ ▹ Γ₁ + → Γ ⊢B if e then b₁ else b₂ ▹ Γ₁ +\end{code} + +To construct a well-typed \AgdaInductiveConstructor{while[\_]\_} behaviour there is the \AgdaInductiveConstructor{t-while} constructor which takes a well-typed with respect to the environment expression $e$ and a well-typed behaviour $b$. The typing rule does not change the environment after the behaviour. + +\begin{code} + t-while : {Γ : Context} {b : Behaviour} {e : Expr} + → Γ ⊢ₑ e ∶ bool + → Γ ⊢B b ▹ Γ + → Γ ⊢B while[ e ] b ▹ Γ +\end{code} + +The following constructor is for sequential programs. It takes two well typed behaviours and returns a well-typed \AgdaInductiveConstructor{seq} behaviour. Notice how contexts of typing rules are arranged. $\Gamma \vdash_{B} b_1 \vartriangleright \Gamma_1$ and $\Gamma_1 \vdash_{B} b_2 \vartriangleright \Gamma_2$ are connected into $\Gamma \vdash_{B} b_1 : b_2 \vartriangleright \Gamma_2$. + +\begin{code} + t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour} + → Γ ⊢B b₁ ▹ Γ₁ + → Γ₁ ⊢B b₂ ▹ Γ₂ + → Γ ⊢B b₁ ∶ b₂ ▹ Γ₂ +\end{code} + +The \AgdaInductiveConstructor{t-par} constructor is for \AgdaInductiveConstructor{\_∥\_} (`parallel`) behaviour. The parallel behaviour is typable if each its thread is well typed and the resulting environments are disjoint. In this work, I assume that the last statement is true. + +\begin{code} + t-par : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour} + → Γ₁ ⊢B b₁ ▹ Γ₁' + → Γ₂ ⊢B b₂ ▹ Γ₂' + → (& Γ₁ Γ₂) ⊢B b₁ ∥ b₂ ▹ (& Γ₁' Γ₂') +\end{code} + +The next four constructors are for assignment behaviour. I start with the \AgdaInductiveConstructor{t-assign-new} typing rule which is intended for a simple context. It takes a fact that an expression $e$ is well-typed with respect to an environment $\Gamma$, a fact that a variable $x$ is not in $\Gamma$ and returns an assignment behaviour where the resulting environment has variable $x$ with the type of expression $e$. + +\begin{code} + t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + → ⋆ Γ ⊢ₑ e ∶ Tₑ + → ¬ (x ∶ Tₓ ∈ ⋆ Γ) + → ⋆ Γ ⊢B x ≃ e ▹ ⋆ (x ∶ Tₑ ∷ Γ) +\end{code} + +This constructor is for the case when the initial context is a disjoint union and the assignment of variable $x$ is done in the left context. + +\begin{code} + t-assign-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} + {e : Expr} {Tₓ Tₑ : Type} + → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ + → ¬ (x ∶ Tₓ ∈ & (⋆ Γ) (⋆ Γ₁)) + → & (⋆ Γ) (⋆ Γ₁) ⊢B x ≃ e ▹ & (⋆ (x ∶ Tₑ ∷ Γ)) (⋆ Γ₁) +\end{code} + +The constructor \AgdaInductiveConstructor{t-assign-new-right} is similar to the previous one. It adds variable $x$ in the right context of a disjoint union. + +\begin{code} + t-assign-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} + {e : Expr} {Tₓ Tₑ : Type} + → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ + → ¬ (x ∶ Tₓ ∈ & (⋆ Γ) (⋆ Γ₁)) + → & (⋆ Γ) (⋆ Γ₁) ⊢B x ≃ e ▹ & (⋆ Γ) (⋆ (x ∶ Tₑ ∷ Γ₁)) +\end{code} + +The next constructor is for an assignment behaviour when the variable is already defined in the initial context. It requires a type of expression to be equal to a type of variable. + +\begin{code} + t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type} + → Γ ⊢ₑ e ∶ Tₑ + → x ∶ Tₓ ∈ Γ + → Tₑ ≡ Tₓ + → Γ ⊢B x ≃ e ▹ Γ +\end{code} diff --git a/latex/agda.sty b/latex/agda.sty new file mode 100755 index 0000000..3de1003 --- /dev/null +++ b/latex/agda.sty @@ -0,0 +1,580 @@ +% ---------------------------------------------------------------------- +% Some useful commands when doing highlighting of Agda code in LaTeX. +% ---------------------------------------------------------------------- + +\ProvidesPackage{agda} + +\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox} + +% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation +\newif\ifxetexorluatex +\ifxetex + \xetexorluatextrue +\else + \ifluatex + \xetexorluatextrue + \else + \xetexorluatexfalse + \fi +\fi + +% XeLaTeX or LuaLaTeX +\ifxetexorluatex + + % Hack to get the amsthm package working. + % https://tex.stackexchange.com/questions/130491/xelatex-error-paragraph-ended-before-tempa-was-complete + \let\AgdaOpenBracket\[\let\AgdaCloseBracket\] + \RequirePackage{fontspec} + \let\[\AgdaOpenBracket\let\]\AgdaCloseBracket + \RequirePackage{unicode-math} + + \tracinglostchars=2 % If the font is missing some symbol, then say + % so in the compilation output. + \setmainfont + [ Ligatures = TeX + , BoldItalicFont = xits-bolditalic.otf + , BoldFont = xits-bold.otf + , ItalicFont = xits-italic.otf + ] + {xits-regular.otf} + + \setmathfont{xits-math.otf} + \setmonofont[Mapping=tex-text]{FreeMono.otf} + + % Make mathcal and mathscr appear as different. + % https://tex.stackexchange.com/questions/120065/xetex-what-happened-to-mathcal-and-mathscr + \setmathfont[range={\mathcal,\mathbfcal},StylisticSet=1]{xits-math.otf} + \setmathfont[range=\mathscr]{xits-math.otf} + + \providecommand{\DeclareUnicodeCharacter}[2]{\relax} + +% pdfLaTeX +\else + \RequirePackage{ucs, amsfonts, amssymb} + \RequirePackage[safe]{tipa} % See page 12 of the tipa manual for what + % safe does. + + % https://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex + \RequirePackage[T1]{fontenc} + \RequirePackage[utf8x]{inputenc} +\fi + +% ---------------------------------------------------------------------- +% Options + +\DeclareOption{bw} {\newcommand{\AgdaColourScheme}{bw}} +\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}} + +\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse +\DeclareOption{references}{ + \@AgdaEnableReferencestrue +} + +\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse +\DeclareOption{links}{ + \@AgdaEnableLinkstrue +} + +\ProcessOptions\relax + +% ---------------------------------------------------------------------- +% Colour schemes. + +\providecommand{\AgdaColourScheme}{standard} + +% ---------------------------------------------------------------------- +% References to code (needs additional post-processing of tex files to +% work, see wiki for details). + +\if@AgdaEnableReferences + \RequirePackage{catchfilebetweentags, xstring} + \newcommand{\AgdaRef}[2][]{% + \StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]% + \ifthenelse{\isempty{#1}}% + {\ExecuteMetaData{AgdaTag-\tmp}}% + {\ExecuteMetaData{#1}{AgdaTag-\tmp}} + } +\fi + +\providecommand{\AgdaRef}[2][]{#2} + +% ---------------------------------------------------------------------- +% Links (only done if the option is passed and the user has loaded the +% hyperref package). + +\if@AgdaEnableLinks + \@ifpackageloaded{hyperref}{ + + % List that holds added targets. + \newcommand{\AgdaList}[0]{} + + \newtoggle{AgdaIsElem} + \newcounter{AgdaIndex} + \newcommand{\AgdaLookup}[3]{% + \togglefalse{AgdaIsElem}% + \setcounter{AgdaIndex}{0}% + \renewcommand*{\do}[1]{% + \ifstrequal{#1}{##1}% + {\toggletrue{AgdaIsElem}\listbreak}% + {\stepcounter{AgdaIndex}}}% + \dolistloop{\AgdaList}% + \iftoggle{AgdaIsElem}{#2}{#3}% + } + + \newcommand*{\AgdaTargetHelper}[1]{% + \AgdaLookup{#1}% + {\PackageError{agda}{``#1'' used as target more than once}% + {Overloaded identifiers and links do not% + work well, consider using unique% + \MessageBreak identifiers instead.}% + }% + {\listadd{\AgdaList}{#1}% + \hypertarget{Agda\theAgdaIndex}{}% + }% + } + + \newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}} + + \newcommand{\AgdaLink}[1]{% + \AgdaLookup{#1}% + {\hyperlink{Agda\theAgdaIndex}{#1}}% + {#1}% + } + }{\PackageError{agda}{Load the hyperref package before the agda package}{}} +\fi + +\providecommand{\AgdaTarget}[1]{} +\providecommand{\AgdaLink}[1]{#1} + +% ---------------------------------------------------------------------- +% Font styles. + +\ifxetexorluatex + \newcommand{\AgdaFontStyle}[1]{\ensuremath{\mathsf{#1}}} + \ifthenelse{\equal{\AgdaColourScheme}{bw}}{ + \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}} + }{ + \newcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathsf{#1}}} + } + \newcommand{\AgdaStringFontStyle}[1]{\ensuremath{\texttt{#1}}} + \newcommand{\AgdaCommentFontStyle}[1]{\ensuremath{\texttt{#1}}} + \newcommand{\AgdaBoundFontStyle}[1]{\ensuremath{\mathit{#1}}} + +\else + \newcommand{\AgdaFontStyle}[1]{\textsf{#1}} + \ifthenelse{\equal{\AgdaColourScheme}{bw}}{ + \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}} + }{ + \newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}} + } + \newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}} + \newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}} + \newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}} +\fi + +% ---------------------------------------------------------------------- +% Colours. + +% ---------------------------------- +% The black and white colour scheme. +\ifthenelse{\equal{\AgdaColourScheme}{bw}}{ + + % Aspect colours. + \definecolor{AgdaComment} {HTML}{000000} + \definecolor{AgdaOption} {HTML}{000000} + \definecolor{AgdaKeyword} {HTML}{000000} + \definecolor{AgdaString} {HTML}{000000} + \definecolor{AgdaNumber} {HTML}{000000} + \definecolor{AgdaSymbol} {HTML}{000000} + \definecolor{AgdaPrimitiveType}{HTML}{000000} + \definecolor{AgdaOperator} {HTML}{000000} + + % NameKind colours. + \definecolor{AgdaBound} {HTML}{000000} + \definecolor{AgdaInductiveConstructor} {HTML}{000000} + \definecolor{AgdaCoinductiveConstructor}{HTML}{000000} + \definecolor{AgdaDatatype} {HTML}{000000} + \definecolor{AgdaField} {HTML}{000000} + \definecolor{AgdaFunction} {HTML}{000000} + \definecolor{AgdaMacro} {HTML}{000000} + \definecolor{AgdaModule} {HTML}{000000} + \definecolor{AgdaPostulate} {HTML}{000000} + \definecolor{AgdaPrimitive} {HTML}{000000} + \definecolor{AgdaRecord} {HTML}{000000} + \definecolor{AgdaArgument} {HTML}{000000} + + % Other aspect colours. + \definecolor{AgdaDottedPattern} {HTML}{000000} + \definecolor{AgdaUnsolvedMeta} {HTML}{D3D3D3} + \definecolor{AgdaTerminationProblem}{HTML}{BEBEBE} + \definecolor{AgdaIncompletePattern} {HTML}{D3D3D3} + \definecolor{AgdaError} {HTML}{696969} + + % Misc. + \definecolor{AgdaHole} {HTML}{BEBEBE} + +% ---------------------------------- +% Conor McBride's colour scheme. +}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{ + + % Aspect colours. + \definecolor{AgdaComment} {HTML}{B22222} + \definecolor{AgdaOption} {HTML}{000000} + \definecolor{AgdaKeyword} {HTML}{000000} + \definecolor{AgdaString} {HTML}{000000} + \definecolor{AgdaNumber} {HTML}{000000} + \definecolor{AgdaSymbol} {HTML}{000000} + \definecolor{AgdaPrimitiveType}{HTML}{0000CD} + \definecolor{AgdaOperator} {HTML}{000000} + + % NameKind colours. + \definecolor{AgdaBound} {HTML}{A020F0} + \definecolor{AgdaInductiveConstructor} {HTML}{8B0000} + \definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000} + \definecolor{AgdaDatatype} {HTML}{0000CD} + \definecolor{AgdaField} {HTML}{8B0000} + \definecolor{AgdaFunction} {HTML}{006400} + \definecolor{AgdaMacro} {HTML}{006400} + \definecolor{AgdaModule} {HTML}{006400} + \definecolor{AgdaPostulate} {HTML}{006400} + \definecolor{AgdaPrimitive} {HTML}{006400} + \definecolor{AgdaRecord} {HTML}{0000CD} + \definecolor{AgdaArgument} {HTML}{404040} + + % Other aspect colours. + \definecolor{AgdaDottedPattern} {HTML}{000000} + \definecolor{AgdaUnsolvedMeta} {HTML}{FFD700} + \definecolor{AgdaTerminationProblem}{HTML}{FF0000} + \definecolor{AgdaIncompletePattern} {HTML}{A020F0} + \definecolor{AgdaError} {HTML}{F4A460} + + % Misc. + \definecolor{AgdaHole} {HTML}{9DFF9D} + +% ---------------------------------- +% The standard colour scheme. +}{ + % Aspect colours. + \definecolor{AgdaComment} {HTML}{B22222} + \definecolor{AgdaOption} {HTML}{000000} + \definecolor{AgdaKeyword} {HTML}{CD6600} + \definecolor{AgdaString} {HTML}{B22222} + \definecolor{AgdaNumber} {HTML}{A020F0} + \definecolor{AgdaSymbol} {HTML}{404040} + \definecolor{AgdaPrimitiveType}{HTML}{0000CD} + \definecolor{AgdaOperator} {HTML}{000000} + + % NameKind colours. + \definecolor{AgdaBound} {HTML}{000000} + \definecolor{AgdaInductiveConstructor} {HTML}{008B00} + \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500} + \definecolor{AgdaDatatype} {HTML}{0000CD} + \definecolor{AgdaField} {HTML}{EE1289} + \definecolor{AgdaFunction} {HTML}{0000CD} + \definecolor{AgdaMacro} {HTML}{458B74} + \definecolor{AgdaModule} {HTML}{A020F0} + \definecolor{AgdaPostulate} {HTML}{0000CD} + \definecolor{AgdaPrimitive} {HTML}{0000CD} + \definecolor{AgdaRecord} {HTML}{0000CD} + \definecolor{AgdaArgument} {HTML}{404040} + + % Other aspect colours. + \definecolor{AgdaDottedPattern} {HTML}{000000} + \definecolor{AgdaUnsolvedMeta} {HTML}{FFFF00} + \definecolor{AgdaTerminationProblem}{HTML}{FFA07A} + \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3} + \definecolor{AgdaError} {HTML}{FF0000} + + % Misc. + \definecolor{AgdaHole} {HTML}{9DFF9D} +}} + +% ---------------------------------------------------------------------- +% Commands. + +\newcommand{\AgdaNoSpaceMath}[1] + {\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup} + +% Aspect commands. +\newcommand{\AgdaComment} [1] + {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}} +\newcommand{\AgdaOption} [1] + {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaOption}{#1}}}} +\newcommand{\AgdaKeyword} [1] + {\AgdaNoSpaceMath{\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}} +\newcommand{\AgdaString} [1] + {\AgdaNoSpaceMath{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}} +\newcommand{\AgdaNumber} [1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaNumber}{#1}}}} +\newcommand{\AgdaSymbol} [1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaSymbol}{#1}}}} +\newcommand{\AgdaPrimitiveType}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}} +\newcommand{\AgdaOperator} [1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaOperator}{#1}}}} + +% NameKind commands. + +% The user can control the typesetting of (certain) individual tokens +% by redefining the following command. The first argument is the token +% and the second argument the thing to be typeset (sometimes just the +% token, sometimes \AgdaLink{}). Example: +% +% \usepackage{ifthen} +% +% % Insert extra space before some tokens. +% \DeclareRobustCommand{\AgdaFormat}[2]{% +% \ifthenelse{ +% \equal{#1}{≡⟨} \OR +% \equal{#1}{≡⟨⟩} \OR +% \equal{#1}{∎} +% }{\ }{}#2} +% +% Note the use of \DeclareRobustCommand. + +\newcommand{\AgdaFormat}[2]{#2} + +\newcommand{\AgdaBound}[1] + {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaBound}{\AgdaFormat{#1}{#1}}}}} +\newcommand{\AgdaInductiveConstructor}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} +\newcommand{\AgdaCoinductiveConstructor}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} +\newcommand{\AgdaDatatype}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} +\newcommand{\AgdaField}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaField}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} +\newcommand{\AgdaFunction}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} +\newcommand{\AgdaMacro}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaMacro}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} +\newcommand{\AgdaModule}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} +\newcommand{\AgdaPostulate}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} +\newcommand{\AgdaPrimitive}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitive}{\AgdaFormat{#1}{#1}}}}} +\newcommand{\AgdaRecord}[1] + {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}} +\newcommand{\AgdaArgument}[1] + {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaArgument}{\AgdaFormat{#1}{#1}}}}} + +% Other aspect commands. +\newcommand{\AgdaFixityOp} [1]{\AgdaNoSpaceMath{$#1$}} +\newcommand{\AgdaDottedPattern} [1]{\textcolor{AgdaDottedPattern}{#1}} +\newcommand{\AgdaUnsolvedMeta} [1] + {\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}} +\newcommand{\AgdaTerminationProblem}[1] + {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}} +\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}} +\newcommand{\AgdaError} [1] + {\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}} + +% Misc. +\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}} +\long\def\AgdaHide#1{\ignorespaces} % Used to hide code from LaTeX. + +% ---------------------------------------------------------------------- +% The code environment. + +\newcommand{\AgdaCodeStyle}{\fontsize{12pt}{14pt}} +% \newcommand{\AgdaCodeStyle}{\tiny} + +\ifdefined\mathindent + {} +\else + \newdimen\mathindent\mathindent\leftmargini +\fi + +% Adds the given amount of vertical space and starts a new line. +% +% The implementation comes from lhs2TeX's polycode.fmt, written by +% Andres Löh. +\newcommand{\AgdaNewlineWithVerticalSpace}[1]{% + {\parskip=0pt\parindent=0pt\par\vskip #1\noindent}} + +% 0: No space around code. 1: Space around code. +\newcounter{Agda@SpaceAroundCode} + +% Use this command to avoid extra space around code blocks. +\newcommand{\AgdaNoSpaceAroundCode}{% + \setcounter{Agda@SpaceAroundCode}{0}} + +% Use this command to include extra space around code blocks. +\newcommand{\AgdaSpaceAroundCode}{% + \setcounter{Agda@SpaceAroundCode}{1}} + +% By default space is inserted around code blocks. +\AgdaSpaceAroundCode{} + +% Sometimes one might want to break up a code block into multiple +% pieces, but keep code in different blocks aligned with respect to +% each other. Then one can use the AgdaAlign environment. Example +% usage: +% +% \begin{AgdaAlign} +% \begin{code} +% code +% code (more code) +% \end{code} +% Explanation... +% \begin{code} +% aligned with "code" +% code (aligned with (more code)) +% \end{code} +% \end{AgdaAlign} +% +% Note that AgdaAlign environments should not be nested. +% +% Sometimes one might also want to hide code in the middle of a code +% block. This can be accomplished in the following way: +% +% \begin{AgdaAlign} +% \begin{code} +% visible +% \end{code} +% \AgdaHide{ +% \begin{code} +% hidden +% \end{code}} +% \begin{code} +% visible +% \end{code} +% \end{AgdaAlign} +% +% However, the result may be ugly: extra space is perhaps inserted +% around the code blocks. +% +% The AgdaSuppressSpace environment ensures that extra space is only +% inserted before the first code block, and after the last one (but +% not if \AgdaNoSpaceAroundCode{} is used). +% +% The environment takes one argument, the number of wrapped code +% blocks (excluding hidden ones). Example usage: +% +% \begin{AgdaAlign} +% \begin{code} +% code +% more code +% \end{code} +% Explanation... +% \begin{AgdaSuppressSpace}{2} +% \begin{code} +% aligned with "code" +% aligned with "more code" +% \end{code} +% \AgdaHide{ +% \begin{code} +% hidden code +% \end{code}} +% \begin{code} +% also aligned with "more code" +% \end{code} +% \end{AgdaSuppressSpace} +% \end{AgdaAlign} +% +% Note that AgdaSuppressSpace environments should not be nested. +% +% There is also a combined environment, AgdaMultiCode, that combines +% the effects of AgdaAlign and AgdaSuppressSpace. + +% 0: AgdaAlign is not active. 1: AgdaAlign is active. +\newcounter{Agda@Align} +\setcounter{Agda@Align}{0} + +% The current code block. +\newcounter{Agda@AlignCurrent} + +\newcommand{\Agda@AlignStart}{% + \setcounter{Agda@Align}{1}% + \setcounter{Agda@AlignCurrent}{1}} + +\newcommand{\Agda@AlignEnd}{\setcounter{Agda@Align}{0}} + +\newenvironment{AgdaAlign}{% + \Agda@AlignStart{}}{% + \Agda@AlignEnd{}% + \ignorespacesafterend} + +% 0: AgdaSuppressSpace is not active. 1: AgdaSuppressSpace is active. +\newcounter{Agda@Suppress} +\setcounter{Agda@Suppress}{0} + +% The current code block. +\newcounter{Agda@SuppressCurrent} + +% The expected number of code blocks. +\newcounter{Agda@SuppressLast} + +\newcommand{\Agda@SuppressStart}[1]{% + \setcounter{Agda@Suppress}{1}% + \setcounter{Agda@SuppressLast}{#1}% + \setcounter{Agda@SuppressCurrent}{1}} + +\newcommand{\Agda@SuppressEnd}{\setcounter{Agda@Suppress}{0}} + +\newenvironment{AgdaSuppressSpace}[1]{% + \Agda@SuppressStart{#1}}{% + \Agda@SuppressEnd{}% + \ignorespacesafterend} + +\newenvironment{AgdaMultiCode}[1]{% + \Agda@AlignStart{}% + \Agda@SuppressStart{#1}}{% + \Agda@SuppressEnd{}% + \Agda@AlignEnd{}% + \ignorespacesafterend} + +% The code environment. +% +% The implementation is based on plainhscode in lhs2TeX's +% polycode.fmt, written by Andres Löh. +\newenvironment{code}{% + \ifthenelse{\value{Agda@SpaceAroundCode} = 0 \or% + \not \(\value{Agda@Suppress} = 0 \or% + \value{Agda@SuppressCurrent} = 1\)}{% + \AgdaNewlineWithVerticalSpace{0pt}}{% + \AgdaNewlineWithVerticalSpace{\abovedisplayskip}}% + \advance\leftskip\mathindent% + \AgdaCodeStyle% + \pboxed% + \ifthenelse{\value{Agda@Align} = 0}{}{% + \ifthenelse{\value{Agda@AlignCurrent} = 1}{% + \savecolumns}{% + \restorecolumns}}}{% + \endpboxed% + \ifthenelse{\value{Agda@SpaceAroundCode} = 0 \or% + \not \(\value{Agda@Suppress} = 0 \or% + \value{Agda@SuppressCurrent} =% + \value{Agda@SuppressLast}\)}{% + \AgdaNewlineWithVerticalSpace{0pt}}{% + \AgdaNewlineWithVerticalSpace{\belowdisplayskip}}% + \stepcounter{Agda@AlignCurrent}% + \stepcounter{Agda@SuppressCurrent}% + \ignorespacesafterend} + +% Space inserted after tokens. +\newcommand{\AgdaSpace}{ } + +% Space inserted to indent something. +\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$} + +% Default column for polytable. +\defaultcolumn{@{}l@{\AgdaSpace{}}} + +% \AgdaIndent expects a non-negative integer as its only argument. +% This integer should be the distance, in code blocks, to the thing +% relative to which the text is indented. +% +% The default implementation only indents if the thing that the text +% is indented relative to exists in the same code block or is wrapped +% in the same AgdaAlign or AgdaMultiCode environment. +\newcommand{\AgdaIndent}[1]{% + \ifthenelse{#1 = 0 + \OR + \( \value{Agda@Align} = 1 + \AND + #1 < \value{Agda@AlignCurrent} + \)}{\AgdaIndentSpace{}}{}} + +\endinput diff --git a/latex/iu.jpg b/latex/iu.jpg new file mode 100755 index 0000000000000000000000000000000000000000..0efe4d2a5f32e88ac886af27b8719e42112b17dd GIT binary patch literal 89491 zcmeFYcT|+yvIn@y86-=PMxua#NECrqkqjbPK%xVYp4F8acBk{F*P(X z1T-`>AQD6Z0L_9c29e%30I;wC@&Ev4Ku<>tXaN8`002F!BY*|~Ky&!ViW|@$@&G7F zTJikF0{}pXwb2D}69at>l`|R|il>!S05r#b#YA5paoO6^(8S!}PZjLO=H3B;v_}B& z4+srDta8QCNu22`pam>|5vTy*<{om>!p6|{P^XE3zWAZuL;f%9j{eyqFr;XFSzP=t z`F{)C?l*%&0id}I08qW|5#kO2O*{a=FCz5jp&SnY;JfB~$kQI$$`^da(Fp+Bqldib zKlqb>miY&N?vTIkA8;K2+QT;AyzYPfkZ%V7JO~f-xDEiFIRM~(xVJ|H0Cd9u04cvP ze{TTjh=+CkJ={V7pl3gnhkCes0YHBW0Kgt>Ypo9ey$%4(?4JL^U;7t6)FU$V&}#j_ zo410!J-tH3Pq@p8tDHHbC2s5y;pY(=s(9JW-PbMny10Iz|4p}mTLApS=0Cynf9db^xGz`j_ll1_1T<0604NmrUw409^3^ z)b;<1JpzaE;uRWtQ(IX%A|gV`+rwSy(4qgt|7(H&2L9!FN{7$;XS|DF^tj;`<`*h{ z7}f59et}`Z;vqNP+&#n<|7#Hck1PHQ{-qr!tvzmd1bYOydx+b6dqj8#c#7)>23+?J z^$rXW_YU|!kIKLBKdkm&@Q=6#0PyBh0UtsM9O>r+bQ@m)Jue%eyPAENFaFtY<}CK$ zaO63_mj4m=f8sE;{1?!o0RXfi-kyKPkG{37xO-S|_&*9A4okoQSOFK{142LyNP-hU z5u65^;4C-?41g)H1h&8txB_?J1^huUhyXF*4!92t%5ww6# z&=!c(4mdG&D3!G#oU%G(t2m8fh8@n$t8|G$ZX(0I}W z(1g*%(A=eYM3X|3N%MxLgr<_Ffu@C~n`VG!f@YRxh2}TS0WBRZJ1rmWF2PiSAz=F+~Ut)p$B?WG-|ouOT$-Jt_?Y;*#2$LSR5wCMEd zEa{x+ZqNnOA?Xt7p3~*hRnUE)>!KT?o1t5$+oxxw=cN~?SEN5nZ%l7T?@k{?kEDN0 zpGjX#Uq|0gKSV!EkEf?Ha4?86C@^R-c9FaMqf5hzw@<`T^h9hG~cDQ-DRk$s={kb1=mvVP= z|Kwrfk>N4mxy}>MlgHD>GtW!ME6J&|;f_q0rj-ET}aWwHL z=IF@L10iuC10i3bWTASYX<>R{d0{Kz2;pqu4&ikXK9RE`?jngIRU(t3w4(B&)}qm( zd7@uLcaDi2GdgzjSjMroW9wo9V&}ws#GZ*Yi><(TVR|rc*fSUwwkpmqeqP*9{DpYC zIR3ckapU7*$KM?PdYmL7D`6)QCxMZemSmOGlDr}LOtMuHF9nmbkcyEilbV!fk=By- zl1`WIlHQY%m2r?skg1pXDSK4bL^evcO!oT;juY?`K__xg49hXfY03G@y^{MTPb;r3 z?*QcprPQc@JeCeB*V!wCj(CAo*YwTS3Iv6u2`lxt0bUgt`w(Kuk=eLjlQz|?vrYdnNA5?yymOt%&I_vbXDu=3}DoXXeDnU&_%|k6)ZCssK z-9kMHu_}D zU~FcbY&>Ri%*5TK!~}1uX&P(VZpLnAW0q+)XD)9ZZ2rN5*22^x)#Cdl=}Q5Z>Men# ziDjzg^kv!0L6<*TFtJaj!$JeF_h-blIe z(^J_;n?Vz+Ee6U$?VF*o#OUV0BzR;VYU&2m=-3yxy*9*@ICq~#uR7Y}021I_j zC4cMTt>q}gsDfzvX!q#WnBy^bVrFB{$G$<*Ag>`?QIe>5)Z%TU+r@WS@A%&7i#rvU z61RQV;qHg{WAV4+=kFQaE4$BmKluJw!r6qJ2lNlTAAEhN`Y_`mHSv04&!bb1o}U^33_tl$yc-nI{PW((}1U=$?)Xj6z-I$l=)PP)VgQl&k~<)ryfKh%Cy`dHL>yfLeZzX{#U+8o~uVWY4+pKg9yZ}DuIZ$-3DwOwf&ZntXx z+F{o5xzn(-t?PUj_OtHi#%}HIh90e+`d*FRx-aTqYWvjtYQJiHt?Sq9fB)^ww+{n4 z1I>f*!Iq(mL!HAW!@VPyMg~UhM#smlj?Ii;AOAVwH$j*TpCnD){?70{ar(&g^BzO1nBqUEupQVZME&zoy$8vcKvrrdx=CLV)4G#e%FD+ z!7?d=%tU@ck)wQ|no++){tyIB0ewJALv#4~5705t9fFabo{oWuk%{S$m|56Zn3-9b znV48PSXtTF+1c5dSU9;j*f|gRLnVjR4{OoUF|so=F&~!r{|4w2;AW;BWGtqmkpQ&Z zG<4iFP&qPsg13jy~7npC->_fH$1((eL_OR!XqMYMcs|RcR%65!^D)-XKByVUu0zF z=H(X@78RG2R#n&3*44jn_|V$c-qG3hxw~g@Xn16FYFMa14(+0$jW{g8P0w&#g^}mH6_Z;Kuf*v) z%zPJ;-&D4+NUB=n`L6{JunI`2%}NsvP5aZb|DIuS|0B!(Y1m(OO#*g08bHfU#|_|s zLe5P*0sf}Heeib-{2c>-$H3n)@OKRSZ^Zyh2jH_Y8)*DSS3GUCtah2MeqhPQ>orrL zT2|6&M|Lv>jxGIQu_~BwPbOQ)qNeLp8_kfRLyS9!r)d7R@Fx< zs@A2%pm#uX{}|({s%tEY{aORQoc1{#0_XcYt|F%(z`9}CH@9Yk{^j%? z{`>J*vO{8(sgrG|HM-nbxi33SPpr=;=BN*PkO%c{3R;3mz9Jn?6OQ zo>{#~^|qXEvvqx!LgCyCD)`~cW=u?} z`+uK0ykjoYm9Wjda8|oao8BjF6c)jsRFi5Ub+e76oCzj8Y3uJUo!x56Pcn&bk#6 zZ%kJST)_G^!0@s(a6*4)qhuFMP{)jLdby9l*i`D%_o}B}^CY2&RPw5fNP|dTcGdPc z8r`N;Am9ISPjatj5dtZBJM2X*F9(|no|Fii)psek4nUwg&{kyo!HrY4u)PPEX3Xay3+w?|VfKykXnNls zrZ)s3@*d3_c5fjU`%%nuuV?L-F@;wdkCJ>-A(>gW6^;n?gMdJ+^cncDgo;gO@KV;tE#1!pR#z+S4Jy@Xqe`Wg%e71#Nv9SSS?(0@*qxU? z+gGyd*5kwzJ(y4$=XCRV(L`#G)0TpzKB2jCHia{*%qQxWD7xB3=L!Uxjo+$hHl27e z_exVcc)4&gcBopS;AmfPpG;%F4Ssp!5ka|?gzTT^u>PZ|qGx)UO1-cCvzZ?Paaoa5 zCh{K&U%g%>pc{YKO!eRr>u}`oW^dl1ybuKjyBjxVz!~)&A(Uv401KwfU0zvMR(j8L z4X=k1X%$kELqdR!X(>0AG?FtH+dH#Kl;^s)bNXTVPvPd2zLw|+v-e}GNW-oHi>S>z z5b!}KV2|`DWzCfSJEmN?iK}DlmD5Vy}za+Nzp@fZ^$})$j1RF=3579pzDnv@>!sFZr>*?U4~LiGgjb zzqHVQke3CTSI$CU;WI_mi06dI@wEHrkFEI5A>y%Bs4g^ZBWgl>1ABkoCP&8K=F45e zLxGF%2kJYTt+8jjCOwMLolfcZcVz57rCZjg$gx1cD}|5BT1#4HC*06HT@#cM=67~e zssXvzt4w}Mj@Fy~uEhAe&E0#{B^Rgpy#o8&y{1n~Pp-ycDo0*N!`nyu^7w0}0b`h2 z4X`rc`?W&e`!8t6F5G1aQp8TuyOK1OEDJBG z4vVF!rapEyrJ7Dsb`jC?+?Px=12tpy*02ryWY76>k=Y*!G6fZ@;Z7Eh;ZeRB7kzWi zXTOc6N%36_Ov2*rTr^Ep9f@2f{?=}3!cTI`kGD_sgJa7FdJk!IMN=w0@hh6$7HDY-EogsPQ%f=p9% zEayhIk4R4~ddSc0-shdpSd)sACWu^(9K0F)emD*}-ysOw89Y#d!0UDe`+h1*5x#J0 zb0w;vixN8QA#|8aFx_RuvmHl!D(aN-r8Pf3TfpIZCJxeI0+F697FMl8FR#^E#aojq z(0!H4O(&jXE!H70lZ|8cgTRs%kLKIVv?*kE0Nix6ijt_uKaMKHUwS$Yf$XdW2z+}n z`i#u<718CCvK@jVT~jHUzhU0Ys*Wg)gTU0pzUPwlKGunHt&)=7EV4rUO=g+Z(-s_@ zeF}m39^Y$SGkfu&{lr~-eS#uksAtH{9BJkMpn>WyKDx$|Q^krGT>No6am3Zr?m2-ZR3&7l3BVDdu0 zQvHMPMmBRD@RUSyE}CWtK9dDw_fuJ#T61_0f$XsbPb!hkMJA2JMwS~?StJ@x8XjBz z@IDKE*VrIxgn!+Q2umo202hPV@+C#ehH7tl$HX)OEocJ)x)gGzR+HpzFrG19aJ`ug z-{{wLbfxkvn#d~$FAo!TNC>5HgpZF;Okm8<({_<>mpya%n9%#~1!~6najZo80$Qy3 zEUzh34)_#4N5B<0=3D88mHh4MKlD|c}*v{0)%#RM() zYOgR+`|JuRxq7gcJ#yI00tBL+>R=>Y&y&5(^<^+J3o4@~_>24GGb~<^YUFNka}YU% z<8UM4jx-+8#nvmLh#xSr8*cbcCG3%yV?-Z3Y+)qz>nXMRLBYXct?LEugoxzB-X z3GJtDNv1_CM1}D$29g3}WGwe{)L^al@WD5zsj^wo*qE?9s+b!DCVXJr9%eBXa55)+ z$!WH6dgERR1mYH{M&(wn7jX6Ut$Yy3m^UL!ynw)Znh2`poF11fxnCGH>wgoq`^xB` z@0lXO7K^`*`Z92{Idr$x4gxJ95Re=%#s~!xPgu5eKpeG%U zQDpED0`qq8HA4#soDap~ufxA!b}V&JTTBiRVCW~KeR3PkA<$xgWXF)dzJtKbhb;&s z*;tbKd}lsEAY%|t7I1|CArrA?Zw7($&;HbbT741?fpd0P{8b3-^G+3Gj==F&xVRbA z=bt%5g(e8htL5N-bHzbmTU(jRiop{5ly|D7An>{eK|Bpxg74_-LEyDKjwp{JKm5h# zkN|Rmb1%xBaKRH@J&g~lENEjAEXu)LYucoEfN zq{o)C|B4p^3=vrJjXMxv5F(yJErp^Xz>uCpzL9e4fDW_5L^vrgR<;Wk0(= zgUM|6XQGIr zs4so^Uq1D%!w~o+O*JaAat(rQpzw9B*>HT(d~qlC%g9HrN%U+*Nd%t&RTm#$Z9Xe` zzU+L%_)Ea}D}T3K@|DN$LG>93Z2W{k#>*<5PVHVUbqEBQk)P~1^Wj6RzHxFy89g^K zxCMb0#AI{}78cge@2z)iL^8_}?^+&`=PMkF{n${G$&$^psQM+~a$3++BhgbHVt39l z@LBy$|3)8(DsSk|`&ZNkqB+!e&18t7snb7POs{7~XuB+#sgRp)(-j~)sgvDH$WE-l z80iQ5C==DV5Ai4mZ)i9L0S0-ZFLgH`{yRP59IPn~A4ukx+n7PX=aF;SRDwL$clWz{nanvx(8Zw&5>bP&plRF>~_o;UQITDWAh(wMD7|4Cojn(_)XxXTRCF`-S}jp zw*hLZjQpe&_0Vaj|DZ3>K9#c8%|-3AT_zapj2-k&mB4?bWgU!i{fCD5G?N%>)UC#w zw)6N7<>b<_x63D|&?SYGifX;_STB;>&fBItm`XM3n9<~#>PEsSx(?=~dpnxfaw9bM zpJnpKnf|RswB_=%4UF5)R(`S*lKJ4mH3NYp9gBLBW-C&5STmHQk*+fVfo9v$ns@5* zXKfxK6PMHrOcR&Nr1_Ty$zQOw1G^u#EqHfjh}by}tS1pQXS^3mvZ$XxZM!+GZCes$ zm^#Z5-sx@jnNju8udJu`B`YZkBYCY2wSlv4rEpR(;uV^gyF=(0*Sx!&(P)0)p6l}c z*a~#**s!)TnR|2Y9(DA?2>I9_O>HjylIRvU$(@RNLkPqvuBC2JzY%uReb;tlRhGLb zI}#4%Ms3;RW%yZ-tsq2}QNja)?7d=gKUgo9N*ND`Tx}00J{;2(WEa3g@i}_ec>uuC0kE`gquAlaC$`fu4H8P_G(M(9g>~ z4`Ul5%9|percj&%F#*oYx`1(aMM*a^tk)1*u(m6 zJZBs!DmGW+Jp=~sl?~_3)cGsV*%dYiqewpFelhHm48G6;!?(>=W)Lt7#KVtM$1Xhy zPirkc+4l)t&!l7z!acFz=TQ<@oQ~uTqsY+cQ1}bem6~bJUPFtz@bJ2_p(E{;=x+`s zMlGxu;`^E=aon<088RgAfW zzAGe!)J~J$N`$}^%BH(~K08`bZmn>RH-by1nn)xd3(Hn<{rnbv-Jz_ zk`KlV3Q;YhF;+@?6Z5)^xUufq=YGg&-)+{!?UG2dws*vm9@lDA0a~g4@kL9s;0*Jn-Xi$dA zi9GlWuC;@xIrAu%Q8&VMtlW?4d@Ia5FVo9L)KG}~bly9^r&?bDUFlmmGx-u8*Ut8+ zI23l|XVmx6;})$~5FNpzv(@#HhG#=+E3@D0r8OXYEg9dvyAmeI&zExPKq+gjuB)~G z*v>?w!|Bvi|5{(oF@H_m7iu*14B4Mxw7v%chNHw+a~P)8Jtw7xBI3NGN*~MqbsLn% z&uPmZLj8re%<2?YhpoG$8)*3M7_kD5osUKAU^B6KtGO2vPrRo6oBnM+;L@U0N|21! zlL*%EO`^U%;%ko&*$M)2S|*FA789gU&VeryuB-jiVPkB=Byblykv^w(r9Wdf$wFl< z%ftXFhH8sqS*oh0Q%MYLwlVT*#@j z+U@Bjc?1xBXEz_lcsY<@Z3j!`AAeDvbUJQrPZnacN@is>dl@1YP+oSsp?UpQ#T6S9 zNa?`CirZKYWGh0b(XoCV%Nb)K_AAG)o&=*lk#oH}iy=xyboNCAPS(5@+d}QGm+wt>eVrqI6mNw9OvF^VUMFx*7WHYrf8$wfRr41-j?B%~ zITnqo)A5{*7Nu-f8R(9}Hw&J8+~j~j3unz)f9w?Oh`Mk8CY!FtS;Xh+Zr2em&XCm) zr2?+OiDYHer~Q`>kFHAV8$Gf{O+UuX0Ge4+YlllgmWT_O8Gi0(p&bDR&X|V#g?1&0<8O zz+J?hnB&)a2WAHq2OuE8l1j{6S3EiU?#{Ki6SGNCQa=1fGYS)LW)^USO1UTl>{qkj zdV&1g_g~kv{oxD&zCkh{VhJfjjNWx7=FF8BwjE~dBEuEgUGo(o2;4b+kK+3QzenbE zn2&f+S4EWZHJ&P)#!a@>ua?Vf4q_1}FgFtJ?)#yVoPxI(5qWwc{M)zt7O9)}i(sza zNb86D5wB4#$Eb=vQx+r3@u9W9WUWO>XBe5Ps*BiPh z+k~;7Vf^ct@mTR9!UgM{RLaSiU4_oCa%Fhicz7E#1U9~RwI6Vix%FE|NvK+#z&Vlr z&DiIoB7PLjTWOPC2)wane3T)s2Gwd+>W-PL6>oq5);MiPTElyAQYOXl%DmO{8(JVb zbN9qe4Slnj)~@ASNdFw&hXmz^YvjlYjF}MxOpFP~*r+Tmc!#zrb3LZ&R|z&@w?cw) zS{5X?D~9wb&zpsbfq~;OG&4ViqO=BPyy2U<`P5p?M3grwL62#gQacX;h85|kM|}a4 zy!)zmU4!OOM0xlpF6QSXhxQFx|0ZO6D#CMRA#WLvDf)yDgYVz{gdv5e?_b z<24Z$I7_XrgR$($bSft=o}(mi9YsTICXujynLmc$F6BxJtM9(^z8bbKx|ibWZM0QM zcweFYd8OIs{rmcb?^uPL*UualaS!1$vm4izZw^oeSL#sHzJ30`;HTbok=Je$l*xki z^I{c_exWE@ZxslzJZZgk9cI0i27xZ$$v3mvu{Lu>M-RG@N!gr|9hbxk@WaoVjw@3d zBzHLz$>#_#vViPv9D&)xQbfP76W8LIH&L|E$9syr7C#1onb$B89lMVk2)-DfJ0Bjo zSesexU$k$E(&N67LREAM+CE(3=$tf4ax{nEGt6(Yb)bHSfaKn4mCktr(|P=hzzvHK z%){yqJj zUS4yVA z6Wlc0&EzJcoyJ|hFB6_fz@5mNO#BkHQQI-FUI&7&#X&HpPxVtfaU}~rQR(vd`Xwr3V9=6w85F=WiY-x{iLMOzWwe&lUtV$&>#Qaj| z2v8_%R>T;$AgzqXo%+cFL-U4ZImcsQh0D~~nl3*Su3N0Z!kx<6N7!_fr7DEgBw^#G zOsdS0dRBp>&A#@NJ_ddcWk&JArYKIHoUbfY?;PF4`DUpy!h9*YNP1r_+OP})40Oby ziqvJYDZx4b0y)vxY6$#%SNmlZSJTxVctn8ujR1k9z=*J|o!$(1));MhVzP+(>Ojv; zHEe<*_jV#8MK6Ls`$iZx=|PFIV>i`rWSDGK;+vGUap7P~*L+GY9}h?E z`cRlL3lQLyMoPCsU@GSzKz1)Du5xkai!cN*IS1jMTS+8)bRBgH&VyR1Puj5@r8-g3 zzWW`-Z#h%&x|~NxV{kr%+S!9&%_suq=V~)M#r#BWBKVvBeLh%3YCBOr&Y&N^hCue@ zu~pm#JS`7GE5oPJGU8ad#ub7f~*gli4a z@40Ru>4coXvRt>Rrz$9l^R5TFF>TA-hUaR}Ql*f6NIGKMoU@C2haUgH4&}mE8h`fs zZ~HBh?9Ks0zvn}EKX1Bp@F)4{$`34*@k>wSkIjX;1*PGKcHeuyH}mbNS>GG+38o4W zrDysX{HdLI^nJBgIT7noSC6<;_pMyc%~k7I&ijkBXrR1CYyDM?>(`ckOiO=22Aso4 z5wK*woEcc#CkRX;1R6Q}U_Z})x^l%5L#4fGGz`@2+*(<6lqnIe(yLf%q0 z6S3Bjm}SjQINnP6Nw%IMrGVhxWgtZwm|U%z=={-f{6v2AwMJ|^Qgu|vJ#04#VK-ds zSp8}*UHPo%YWv~S_#9AO?b0g(5YXi9YL9$m3U7UlD>M6TPDMAmldhAch^Y6z2wokg zBI8%r(p~C!ku2CCGQ%yzWB5!JygKJ@y+VwBf>lP8QPE0z`q}0um3|QDD#IUh$~VM> zaLrz#g?E;piE>0fCa8!>xg+r222s=0VoEL{f-EYHM_l~=!8Kui+UNY9<4OOSdsx92 zry$U*@I}WN0!-qcG?nh+a~@}@D?d;^@ycPa~!dM8*^%J!`=YEtmgreDqTqa2$)SmBYT4UyJ*pWvYhdK~=r@%?c zj^odjg`HNoHLt9zMH_StWNQQw)nl@g5+k+LH)e^JGI@BnH(Msu2t5>UhfoIs%?nTU z{av}9eS*?V)rcI(BI(Z+J()mk8ZlO?*ZA)kXEQefa$nqtqR{t)+U#OK6JiDyHUTiLu{Wow!b@^4ExRmR1DF`GBy6D6?HuacLqL84fgYZKs;u*?*9BHhgrv(>{#qCR5{8hj66&I z^4#JratOuc7MM}dXj%A1w!!y(*AC|A@8*+~qkm5t|Gr7%(3gJ6ZwIR0^}K5l%f-Gz zP2}kbP|B#V?&DLGthwnkFOr8m7H(1PDEtmvS@VvFSqN+}m0e1_m?`_9FpRD;aS=`J zJqH^IL%Kttg1$|keG4Y-Qc?bwD?k?N$r zRp0G-_5BP8FrD^V3cQ12uVqJdRWyYJ=2)J_MNkJZr8C)xjSsA*tD7i%b=Mpl1U!f9 z)0fbn6*iofuQd8T>V5dD=;>lXroLqTaJF~icO_CituLZJ&!Vc9A%Ve8%F1mn?UtwoCXcFX!0|&p<#v|Eo#+ zD-m@G4WAEn@B-8F%)IA8vi2RuNtYF_+YFRl{A$v=usU8;(s3avGg*Y+Q)=#tQJ-=7 zWSLxtX;QNJ;xm)9y3D7dw(=pCh8UllI)r? z`N&e+I=0HNRz-9=vT(6whjw%T^+J88|8W@q09mqhx^l9vF2vmOwXN)d!xt>x&_#6} zRwt+KpUB+)MHaS$r(*!2fAuDh8?x?9q|KmkQ0x6xBDy%KBYOUqiaN#KCpS$b-6xBg+hb*8H}Yx z&15-Q?iOuK;hS|ECMpaxDI|6XkQ9+5hu$1NJ}U$8H~ss3z)#+$jvZ+3%5Jz5w1-6O zaUD^)C%W*D8iEe4Vc+Wg-CJC>cKuSW4W@OoxH&wOvhTenSh(r`&u6CDe{ZUyrhT4N* z-z@asa*4Dtdv3oI;>{g6roNR!7R0qdU%QOeMrO}_+6 zy0d0+dxNBHilwF|T7$LpH|h>ioRh;e$!?(9T5bw4RFac&N&24O@PiQ-;X?b*g~6BT zOUDlfblHvUBq!03ho`jEPiq)B7#5ZJtDC&6eyE+9>@3O8TIap$^Te_Jm8H9-VezwH ze2ab~c~62)D%{9tk|@iwO&l*h<8v{?SzW%)2l!m{srl;kRL1a7@7=>0@-V6JS6kD4 zD9gK6U|(u4`WY=gf_ zeOj=YkGd@?Twmy&?$oy)z8k(L=)fZ?b-D9;gx;rMpZyevGaeRAM;4+YwbWO$0p)J9 zYK#fpiXe?M1Y^zSHV3ljSl$Lv05S*mH95At;3nKfaxCjba^j_zAaA`y5K_( z3mGN+Tji=rnp+L#L3~U@8g*flDE3@1e(N!U)GUynj&ulYDnrVCzP*%Po=Jh>WyvBN z%Du7=o23o0Kkk|jnt86AOyQykx^~Z?h{wlT0@?liO~{UOny^S$p9@E)eu^89a}l`@ z#`@+OFMakR^Gn0=9f!wL#RulH@uDUVh%23$)a~>|F;61wDeFYp2fgH57+1yGq=LT1 zw%GC45A(wh80g1-<;1~fvUBL0#Wtv4iQco`!tf7cqqs?S-L0Efmwz-N+NgpY!VI3R>TAiARyKKm$r?mJ2n zpVb0?H`b~AfJVfe7&y1|#PXwJ=gZwn&4ESMqAiRI-jd9Xnnyp}jjgx9Lm@90Af44v)^W%Cd z9N}k$IGae|eW0-UAP6ySg`P`;0PiXu$$PUx#4g@Cc2Uj@AAq~l6T?eXn1#T^=4?|! zJXzUSG5b+rhVapajKY}D8 z&^GwSRPBU;A-9QCT8i1ll%FYZ6$s2EPr`RGWIpBD$$16#^y+MFzjyE54(=ct?1)_u zpuao-uR#TD$iy~K`v(In^fDgxLSQnDbjC63-+ABuw=S!53`kj2i>n&fI*NFL>B&*0 z;bt?DwE585kw`f1Z)-7j}-l?h$@qPtfryAgvU~lI{2FF8-gfr{aUyKfcKyKMf2*kBS22y#jL>X+yBbSejuap$NpvKsWJ^N=DM^R+% zu6FJ<_&ZdBzg@isIu_+MPs;z^I8H8PB4BJObz}tyuwd8y3C<>LA1w4+wclEy54`-P z$5D(e732y`Rp&qnx%v?)(^F4gbX!(z1@nn|t)JB#V zZ3eK~HD7(6p1f-<_qp`vjznhu;hN}hIdu7MW>lTepUXDJ0w#&Fvg`%sOx7#;FYdZ%^6vq);hVFxi^L-+?BS68!V@M#@9A?U2tud z6ZLa~odReoH-e5>-Ok-T=**$y{YGqYB>c`VV}5mop#rg}6f2jh%EY$e5+x_^`U!=X zQFT5SV;n|d9PpV35U3GsrxTfuj4;91HolS`RX0vYhbHtrjb*)yI3J@4fx97r1-};v z5$(NZsLd&_180kz{J{_NR7&PP*;DxX3xD}*61crUWs1yldBV(>W!`cfopfRojw0W+ zlvpQ!E(lQzX=&Y=a28{ZAr>a$-bDOR-yt(%a2aeBv)?KtLUUgrJ; zst8f9(~G*%G9-~XgPL-rgHv@8Dvt;V#iBy7mrGPDL>B7K_E7|@s(j{H3A6IcoQ3o` zBpn$}JU(xk_^WId%}mT{H}8TG6o+I!(5+e-!;+%0Z5X2D@&*lotv8i=1hcMi3%*!a zj$)|8y^Vg1B`zYDyM)_>bLC5mTZ@l^DAur;PUVg-p*3w*k7J$F7kl?%Cin0ObjO11 z7L_mN?QbDH7h!D>AZiwMI;B7Vae{bfwn9RK=#%&xcN94VXVu~OxbZ{#+jTGM z?+Nq37tz;_EbEOdMRk$+@6LW$-911idCXY^ul~9oCzCkv$GwafC%Ti{I4$=$BFCRd z^!(Iws-4LRxQ_c?(XUY#6qmnY{WfrN1>4{gtBW}Ng^|CGwHnv>{b*GPs7wdB=TBkokat7W2oXxxB6P1$zOZPpXH zf78Fy2jmtA#O)9RyNOLR$D9MnNUyC)&#|5?6m^v1yM6FyaBoNYZe-IFL(2RifL0*& zUcl{)YURN8>Ax{9laHi2J_(#C>&OgP@AaPZeDBe3kTN=Lw8rZ&>3V$N8bRhxY|&Lz z@v!1TT`GDuOdh3=$cEw1`}_OvpdV&B8%KQCFLE)A-!*J-5Jyd2q$q3$Wcr_d4NskR zw#Yg^^6PDYpxt@G^g7Ys}n%bAov~Q`nn`k9#RAROIUTr(- z+foTnPaTJj@IB$e`lO;XcLUFe<94>!Q=));a+fuI;)wVe{&g4&Y9<>ds;9BUPZU+an<_;KI)IXumPXpE`AIF z+~jYSmj=(>;AmI5-6q`k3JB2ooKe!`Cd*qR!>dR?5-CdA&>d zQH=ZCCSSi8n~_(g_w&K1#UQB{2gV93sCy{9IoE9zlTO_LRgie&*4(1!h=jlOW!w*r z;Omp9>CUs)nw^E_0_@C8K*P6p0V~Zsz z-y^Hfaq(PT4ooXp`Tavn??sXcCKoAyYB>r4ufT_$XW+BU5Qq=|YL0|}bMyTn&r!wB zKyolPYP(5(O#j`J(Vo#CUq`v?wElQ(B+PX#4 zqJ{_UNI61$Z*P*3&8Z8PRZ}M~a$W0MJ6!fEJf4r) z7b&*=O4`B#<5r!aaF_7{skDhAgUJ5JhnKN%))=7%=XS!XjWW4%m%isJrX87}$BI-W>LbE!hj4Bnm7rcs8 zBhV*z@8#bAIdu_d`^bly_B*m);CE(}+pIQvzyPTPfjbMMb6-xX6$vW0pb(NfAsvV# zH89$?CEuu}#1;9&t7U-BA3JT>G2YFIZU(fv`76A@HyPd9~=#gL(N)qV3?$M+iu6VuVmF zZaS)N4WTgRHK$}z#-{gA`Yf@%OD~a#d$-_+KCFNrslDBs@2w{~;2w~)&>eCb0-rMC zATXcyyEo@~Zb(PWr~{(f z*;=D->{siQ>LkT-8dzKrn8<|71Zmu)y2x7Jh1n0iA*!a!gliTTy4Wr^%r!?f!}%XZ zwA(&|K>HMVVs@;~M#rI?D@pmbAv;`p0b-qIG zi9l05m8E5NlW2_fLo<~r{apVsw?V0M?y-dcF535_^qY;!ZEuv?T=VY3Pd2+RKG>4F zl{;W>!}hBoz_2yy{(&Idc1%rk)8D^VB>n2Pqws_+1Quj4gFfVJ2*iC~^L>jPi}HUP zEI{qWPuFlZ%pNOxpITJnU^$2_=lX&6hd>+)F=QRZ(ugYEfB<^h^~aE2v#m6Cw|)%~ zKK1PZxbLeAUrjV1;2Rmf^h2$mb4`tBdxuSgT6^#j@d%5zfB>)l z3}z~1ma?!>bq16Fu3Oh>jz#esQc+@TgCC&ILICfKqer!JL4ZM(__#Dnd?d5i<`KGS zX`=Ni1aK{~iwHS|>kjJ(vVbO)#f)IKJ4C6hQRa<-4{p~Ddf>kcXg_&_DmL69auTI^eVO# z*GH|G{5rjyX_;FrMWw|esT`;lb_jSX$BWrk5%tzO#@@{f>K(^Mm*cM3TxTLYY0k!T zwc^;xa)YR9vhwUSTU)p!-THw`ynRp*^@|U~t@r)B@7@iunOg7oDD0q;Ly7ipYs=J{ z)FB|bzf07F0R1gWZu9AVYo{2k5w){tPFZ}#N_by875!pK!Uh5~`UqR{aR}V?Y_ur8 z6%x5NXa6W4!>|#0R!BLcsd2*myk&DI%(eD_Vh~fI+U_@5@$8m2Mml1z2LdU&raH=T z2?S+jhrph$b_g(|W^UuEH`@^M7S5Llf=Ly5Z33g}8c!5|3`{+^ubUOo?7PZ!4^a(o z!`^vXN<91N|6uPuqnhg4b>ZbBh?S^_2nbO`P^wB3gycb_iwGiBh*E_Jh)55K0)o^C z2q++t-ib76fzS~t0clc0k=_#Og0ye=yx-pYJ?D(Gf9(D4U+4LgtTi&%9BbTTT*R2u{4mHh!PSC~x zge02L7ad~L-X!i!%c-B>wVcY|=11%zqCt9R|?uAfOt1iaCvBz`M|mjCzEBgZ-do<~q`vTjt^5sf z@=ht*(Mod$0g4eL<*eJ&7OKyN^S^Xd8}B4)TsGO%*?Y6!ZzzbIxjrG{#wo7v`mILw zGPo?=ypiu<+Rn)Lbz}i-TNqyEPa+q=rxM}aVH%~dERY<~b$F}!;tN<6UZLN0zJJZ! z?_*YFqFQ{6iB#9NXkt{-WmJ*)wH9lfyhuhC3m}Zrhi8Tg4bus~$oWu(qLC?*LhEE=>MY8w#EM?`L%V*#FN zF&XGM{_Vm^n~T_8gtx>Qq0&b{6Zr!3p)ZCf`cN6V9eARMsOW;G;U<*Y^;?6&B~*>B#;H5D)C-L3OimD zBK;y1K%Gio9T~9-v~g-;WV}AZR6JB8_P2ZJUn~TR$AR-x`rtk0QST=8QNq%QHO^AE)PSckz z0=7+(z(4DxytCDYOKDJ(nv#P8Z0<^sSwtD46dqv<2GW$hq2`I|i8F>hD|3~03-;IW zANOuP`BR|fe=o-34xc86!l0BhF#GaCM_<#{KdY*=hU>!a=}(HcD?76Q_TwOC%D?@I zNGAR+0a9Y|VTM$rU4eam!rLdC%TCdiwj*@XKRJ#CPz1>ByxnD&s50YE@!=>W3t*R{ za()(&6*#E-qlY3~9bJ?mIKzJinj<&Elw;(TkenBbDV5*xSW#*!N?Aa=S=)mfnb6=B1~(Pc%mO&Q{}39PsLELM<{fo^8C~Ol zCK*?665~C@JbIO~-ozi@>a1_|(fg0?{tTa8M^Cr41NhfcB97xJ8V;U{_BJv4RXLGp zzmMMYiG#b(jh^Uvc_q;p11un>l$4ufg!x043d^7p>D%3xA9UR831^nz@e z|K;E|Y38@5X%srGA5|ea6jpxB)PiYdYTfncR_EjEP(x(r7*$V2e6o~Nkwo1!O*UHD z7yVwhFf8c&%+62}Pmz}BQYoxb}oLd{MQQkYA zLo$y^FHEx$k{L`_angzU8rmfpOf(O^mz9aBHPG@M{Pz9M%i*j2L(7&N%5O(AZ~OKa z`1*^9jfkB7iR{!K0#?7B&u-(Fr4WB84-J29GZ{lR4l8k4k(GecX z5hZMsK>j=wl!OG_OQLo(@hwUH+>SgqdcAET=7?!53qW-SQn-gP4QG^HT07d%yzvi5 z`A3~RdoiaZ1QnAOH|pVh0Il(#ii05h;1pGNx*`a*4r-!K*!VkD9rF_Ct@YeJnWM=; zd4dq3>oBtFE_(-WAoXl42g(K?gp|F8HGT2rzF&ZuG{g5gbx`#KWHJ21{y5VgTMR?N zb`O`5H~TK

Bvcsuy7Yv2ZrHb4eBcWwm{A?Sn#eiAd8Y$Zck+k2^7 zsL*_0dR!e-G6n^YeZqlz`1!G!Myt#93eq;K=@UtFETH{m0#nDQ{JDqC4`v7nvg-sj zUqB%#qs>r=6zY?^Mt@mF_nEQ!Z+PbNso?zp7hQ(waczF zV`}co&M)3|UDP|LYc0B{=kk8>Ds~r{Cc<@YTuhW!eu*&>x^LV&)~e>D^lmGMq%(Ye z<7ZTQE<`8lH*t#G&ASRYl%e9pvuOVDo3k8Ab}8y!RyC*3aTmB)SVnAa&hpdb4L*hw z*I=egIkzhp@2Qlsq2+s7@QK1+l4L8~JhX0Giv{?msUV+z`1UN0%YP|uzhAV_m5Y}T zc7oD5AxDjmPPdpR4d9=YU~c18k3vzUGm&pc*1b8`jF3BsFdKIr8;Z6K&UnS{%S;S}-rH+OdMr&&ONg10oy zbtkiKKmg;Fx)A%la8Ve0{!g^n5A?%q7Qh}utwFMYGWqb-wj1rPpBKKb1QxiHE|oeg z^ED!W5GOuYGCHUT*aMdJe05hIxk{z*fT+{_ic`{%(Kw--yk@ z85}4{+%#*|s+TC*JI>g%o zsh4fmZl$wa__-c27EqtRju>68CsMw^Z4vzDVlMIB9W)J?;sclE>um!DAv1{gE5&5U@r`k=i^RnUR!&ZoI+0e2FXwK^Lyz$fAG4jSyfAX3No)Zi%MLnF+ z6RjV-HjY$^Oi4g0ceunp`gRH1`B=-a?RBzXhOviOWAdXV*_iR#lS$f^iSLa(z1}UI zE$(uaaBsRW7NgM+*OqfB(C}eaV)Z!#^)vPV#$&_wTTk5kq3id-x-vkud?xN-I`%f? z5FveS9V~mONKRdapV!u2B1J3^2Y|M|*2c zzJ>M$ZN*ekU7Hc0h)8*Ms0gLI)*-i5@$7Dn^K9E^yRiavjk-6yS^pLK259_fc|xGS z;0ZR+ZFVo71?+C$z!jo1?|&E2x^#h}x{gS25IkyInM7j0YLE~+haHzhFJ2-Q#{EcW zO5HnnF-vg|xka8-llZjaV1Ko(H2v5i!j2Aop8Iw4lo;*&L&e*c z8HpHo<;3^1N6ei%kbn~gs5TEFYA)7g26;Ol!%N`8zHJ6EohJGT8&-nm$vV4cBR zA9dZz`8S+&BKMhcRY7lmsW>Uc+zU=GOmqJh8L4qkOmh)5a>)Gs(92f194uW0`O-$R z_4;0(&W(IPafRXz2&0tq;w-@5Z)kxVHN*ngazV`RsD`sjZ%^(eTxeEWp$zGWp7`@BwgWYnSbDU13a5_=N697BJeqOev;GpO~tR zveZ)06Q%E(%tSp_3Xl+*-`hh_+Ry%`uRS7#L0*7 z)i;wEP@e_ZvjA?hJlB+w9fnpOc&o<|ol5CO?PHE_%5N8;Z4`4>K4DRy){msIpYz`1KDul{!gA5ot`vbfx$G zlau@T(AbGTz_w}EU!KxdgYG#kQ6UBRs_3|DGv6*Lm`r)V0=O2e9>FgEC}a3? z*E^=NfIF42c_4M49Z`r{r@A(jpl*Pv(-25|4fC?XkI__@qSsNabQ4E9l1&fMGK|K2 zvMskff7wU1rEJEpb#a(hM5RMQvZD$$9u>zLFR}oDaRqdy`JxoT(AhSTf)VzaNgt&& zA939N!VxUgm}8_ipy_^~QCZaV;8PdLS^gNUWTl(iY|oL@UwUDS%Is83Gx4~z@;YQW zG5&q?Z2Xb8QTn^FYZdgvdJ__@GYjC-|fZ}WDJ1IekFn7ZGqj*_O3 zm`6jVEg>BtEqr=WHAg4qTB>N0ZT+u~D)fjkkPEKChzdj#E)@L;F$(?Z74z61_t3zV zRQB;YjW ztfg=%-Njh&b5z+r?d5vjt$=^x>wgf|rx7cu6c#Yu_EDs8s)oBJHrDGY(GCa8jOEAD zhVggODydayeqQ}y>%~^LRpCUsR_;9+l@qDN*q5hzJD}%3V{KmG=R@yK|l1 z)52nDYyiaX|sCWxr8EPs94sD{fK}ZZ%ApzRcI875!iV z^@v|d%IA&MLbD50W@m}xEPxZ``CDC^tHFgqOWPvRoHZ<MMSDdWApF6MBUgQyKh{}sl4P;F9+c@8B`Sr4%}7RhrjpzAGD{?36U z>SO&GD^V7}eiwYr0uH;bWcp>dc2@|B)K&DoPk$1p#yiG1+Em5@hzL!S`E~l)gVQ`a zZO!E4-d6IRzLJ4ty>jrzJ=*Q)rToK}Ms%1pnfGKTbDL~qtll!_lFtaG3dDzWV@k4r zJD|)EWnKYW_WC#Y3ypb2ANeoXxXSC(-S~*M`I{K#k;{}_=4r?Xm%)%Q_8RD=`y!Gt zoFybjpV`dc3MjksZ-naa?|*HjjQA88ln`wqjCsRb4BB?%Ek&lNebCys=u(rhhtp)r zeRv3hQcSeNoJ!N2vwZqJvFyA*S$IzEcLFGo`Wf<;IGGGRWir*aYLKoeo?%=k6s9L= z?`n3f_rRKclpG6q&BwTnZ~1i0xSBFp;gD;l)nnzjnb~=ov-n#Cuc`mxLqwZ8L9m-V zE&XcC*|&$gV(?jNZKU=r+gpCeUEYS>GY2R*Iye8+JY9%*zMvfJb0&rs#C<9r^mgON z%%tegBVCnVlC&4}(>PQqETEPQBhdXR-SN`}uegX89BPc_<4w%G9IE zT;5OdGd8eVwa`N`rRg7KHpez_#jUz!<+NS8ixro3ifG<3g<35UJjw3P#*8VUv~SSq z^Y4%EMtU};YcK(nJJq4lXHXyF9cb9cb1UMi)WUfdP|k11Pd!u@0wP!dyWYSSS&H0J z&0Unsqvr8=;!eHq`)BFUR8_>qg8tc*S~@PwJtD7z-O2#FF+pVk^_D|pMP5^zV*PbT zFwy&wl%}0_(1(iXh-zy-yQ5I@Tw)u#WmdYNfGY5hPOSa&d>Gx?Y`F(^mf3Hm2*Pai zAk8Ml!)-shJvUd27cQaRkn$#JL(9C;hLMVvVb3@EiEa0T$ZpCq# z9b=5xEV>v5#ooWZjwrMxIK7P ztsgsg6Sm{phY@rK?>!l;qcC%Mb>l|i?N1Lo46ov4Cb3~;iVl`*;SXKx5#(8`3$JVo z%Sro}hrY1I^84$G{-|>SUsJN1iAT4gC1AK(f0<9{MOfbfqgX~Otw5ze8d1z`V%94` zSI^dV$T1rsn{~>!vp4HXynx&;I1Ga`5b9}_o%s7n|Ie3z_#YVb-*X+%LyrJaxW!Kg|C-7HfO1rVD2^5XPCc69Vqmc@3& z=xDp6w!)^bbQdvti*PA$=O+tr+6i!-+d|B5sMr%PVw_yx=2QK4-cTLhUh+ts*kH_* zzog;WOv6OzHtO&Ph%9n>LUSJlyW>SQEKr|WH6?>n|~pTDBOH2 z>W^P30mL-O0I3HL3Rg4{K@BFGQ}tH#YErXr^x>a0O1-=^^NwTwQr-;40ULs&%x1)HsNy z2HQ2ds+@HgKz9YBCmrj~)BhYS=|cF&Qyb5GyVwGI(}DKzp7`mGr_jjRf282f~`ac@l71_ zXf5R(C^O@X4Rf9zb(rpWGWYH#&$Txi`}Q)Yb}!~{xSoCCTJYF$=5u+*3JYkG-teRi zZ#=RLo@;75S=TYt%K{oICQ#iXT{rau&8B^$U9R~KZFc71aIM9kE6!}Elnzd(RQypA z$Mtkj_N=R~Z8XS>-FV1eD8LAfsWl;qNf+?Cl9+sQde8YQx91HwF!Y+(zXMH$?7 zH!skPeY@80ndS4`8I;4ifF?9gx;khv+nCsaG`>#Vu{7d;)Akt^%JJm{)@k2jN}tYs ztPw4`u}U|{p73^={c@Z-x73d_G~z&H^@b)rQ05E zJl%di+$|IzW@4E_r0D;2Syr064&|TH-l4@*@u@Jb-wHemIZ2ixH_Pv!#Y!Ljv4KgqJg_PhnayMi z!kIJNFH>U=n)h@rD(UZ~uWPP>3GKT5`^Obd8OFyYNKX?iMSq071nSnbQ&DapD%^>^ywJIvt7I9mwB2KH6wG zAODaAR5TLXM;b}9(wm6cP532prtB8}OPvg+;Sx&w^AQ&USHTDvF#e*$ z&M(~Jv&umhkng^x<1ao-d<#EDP^aV@BO#}sR>y~XboW=kPCtEMoIf4nA#5`DF`IKv z5&88-Y}h&hz3l;xfn%O#VU0v`Lnb+UqD%=gY%wK{a%Fr*Nly)8JIksGW_XR8G+7KG z0rpW{Oy#G^%6)zf4&Ws>Wr%)ieR6GpDjKzxM*G>jat^y|`zeHZ8^G?o@$X1vv^6Q` zFAXCG?Q55cSisIwFB(6G4r~CWZ31?FOt`Rs%V`WmC)mb3IzYX741OGx=jC}BG14+J z`RhRS6`w8Pu4v}>p)M9s0&RkW=9n_CH?mpS&T@-^nrb#w);WxCJ?)wvk#fAy~Ntn$s z^qRre>?4{cBE{EvYy_6>>V=eP@IVT69nX2*TmA0g>ut7!h%Z(mlx=)CN-@XLqmE5^9;C$BX6sPf3%?>dK#>a!wQ&t`&%D!EY(?21Z zy&-$n$(Ll-0k0EN$5D%T4Gs^=p7r&8WK(P zj(n|eaT6(})}_r`v$%#$gBah^Cwcl=mThj%vR^kF)ij0g8T9O2 zh*I4*S@e+(=dC;4)0$}xL$B0r6)+u%GUP_;WpBp^69{)23z&qKmYK|v8lm8op=Rme zU~&K3OYk#`?XRr+OB@a|K8BERUgRx&Zrw>tgCYJ%4H|H-D`^)AQ9J-d1l~a_#`AGQM!?ItSJq|=m+ZlSRJ3Z{8SD!_a47WO6H2p_7t+a4c{J8?q&j_0Omf z^6S32acS=t$5MWo-xvJAN%@GQCI3sR^Pkh6e_#J=`kDT9C{-d|garh7O`~zs`QAID z-eC~2$=CIjZ`s>ffUn927T}h@mbWQAvNB8WU0Pka}Tg$ulm`VmZ;Wd^Ndu z%-rfuX_MIbf}HvrUtmEeksF%rEZ`=-20r--$_t;80WB4RrA5YbyzO3vxb0<>ztHhe zyv6^5T91&p&+$9?=>i^}PyrPjXKo$#TC#$?kn+SP>M9;SvHg=~F>J1eNX&QZLN6_k z2xNzD-RhEO9$qW(I4n3a%>$Jvu8y;VHJ=uzB6s3JNgvuR)UzR!s88)o-@K%w3FQMCjF2=J{5EN2JG$~cRr-{qBKV- zk;G+FtKv{FduK#0l07k{bkO&&fpth;1KCJxFeRmwHt1d1q9r9`_C2%=$@j-}iqwGu zs+_XE>0kH9;I%6D1+ys`W{l;l_vIsPR9&tc9t$H`ggvh;u)8xN*S$OC+D1A{=dIl& zDBzv=OeL!(O~|fSS%8zscZL3lp?(&?ftf4-_T=ks_SBwP;xpNN`iLo<@6S_?f|b(x z2Ay^{tgdvGWIq$IPp9Ke86@?k0y;^TBiZ^I3uub}RDp1#u~TYhDuU25Klhk?Lj`g- zc-$NDCDRv~{dysY+;c@=iDzHdI?Zd;1uu0^`&s1hzkJbjQTq}sHRJ+Ad_g}DL3sdy zqHb-fkoCZJxzs&s8+Z)ny)SFl zOz3i|TV(+JT6Vu8s3GJEM?p&Ag^@bBxtt5u(;LUZ>1Uq z1qB5+3OH2-(}>0$n~wxxxUUWU53sSdwZ@BkGK)FZj>cHIt0IJuf8R!&LvW$|9Viu3 z%);qoGt9`0QQ289=NlDwBDm;xTa5g^;J@R!kO@}OQ~_q8zvw5w+(+6Tx3USP^w5H}d!wrr*a4_aCVE5*bziLJAR1V4MBE_}Lk@@Y$hiwct zwN`HDKn?%=3@IW`CLoS5+p>@;H!897)vhZYLYfpQL1V#|ug6)ymx1jTcMJzpz=D1m zv`Yg$$&Qv%!!}+9%_Y!8O&0K4(FPpS{<}ZH|8D2~AGn7mBfcs$kU=BNd5!aMrp zY#6C_uiqHG@VdYPJa&)!I&T-ihli${$!su5N8hE7ClZO#{(LN;!@{fHE$Y|vdW_H6 zx^@PkjuX@P9fa*?7FcZSACIrW9-Q+&Eck*6aIk<^enSng2lqLaRwGxG;@&Hq-O!Y) zZIp=Cimb9Vym45ifkP4h4nB#8mTH3`lp=E5h-DqaqVb9$C`9l3S=$ImOiUaxphQYQopRsAE&wDFd0BH zl-OQGe63g^yU`?2egn$zuNu8;kkOYuqd293_K_oN-&8fW#Z!VzVhfnt^x3fb{#0Wl zr+gjBER2G+V}Fxz+|lnp!b`U`!p0s9&d8-yoSCgG620?wQ1+}-w0*%gPIfz`B#z5; zP&z!~!Qga`WQ&T6jG0bo88Tte_nofUvYd+j?q5h4KK;x~ma4cva6s`4)y?dCXaK;^ktyHc2O>)Lo9IN zxi_pW8WE0kdp%ee#{vRuQ4)g$A8H59dT{rC-%EYYJd*$AvaZ7fcbwGt*XSzKfKE=0 zfeVZ&L=h$A?ZxAZ)4D~8=^s2xr*z((3nPY>0PpvV%pT;*i;Q^Y zNk{;hLv~!sv~kJg;A-OQ_4!I(1bFm~KFI0U!;$v)sbl|i#Ml4e^{}`G8v|)zMFU5IXxNJBPqkMqqwL zz_#|z@Dit8pTOwbtfgK*jwKH0wM#Ku2gWcB8Z5wefRR(j-o;3A!B3M;gw*~pg`}Y2 zKF%z_`OI<5*W6J#aE+E49X$}&6KD4%Aj4CR!EQ23rgM{bZo0lf!&tzZ=qZ|Iod8u9 z?4JomTky}dOSj!giYGao=z9@HUym$-J3?2Fia*S#Rf5NpzK>(u>6%l!S1?XJ=55;h zFB3W(W?kCaZkxX#g{4)T*{;NQ%-*59$c1;PXqD0i*m1Jk2^0T-up>+Al?7BuMTZvK zg+z_ww9>iXJkpn>Z^l^uy^Xg~cey$}T^h7~p|T+JH}yOqr>wVb*5PI-vHg2jU;Mc= z`kqDD@0@n!U)=O}?ph>IT<)gsy6N}O0wm9%xo zW~F92e~t0=9W(arFqD`dEPknHV>(9Z4)L320VmBI&7BDeiNWbg78a_|iFl0*V%S`{ z{dJlYovoCSjOJXd6R6mjB^c~PYRqcV{U3edA7%8u%4dF$+QWY!PQJ&LgqxYOfX42j zLeH+}_(Oqb!oOeq-tLawsZ!sW@a2}F^n+ex z>tKh(@V*v4nncpZwjw5ic;*?C6LqU!Zn>*)$7s~`$TR+rNkI|*`i3&Ej;tb*(87c3 z$`<$ur^KKxH~*ZweWZ&_QJdH;!KPQ@!z{oV5k;hw6EKX}?5??|=Eut1;#}jG&{)yb zgKN3-ue5GDQIqsw7PQL3smQEEhf}R@Z*(_L0xH`0er%}I@DyuZ>b*En=`RI`KaBjcCVPtgk)k5?IJ_3nDmG*KO_A*6wP_lU2?uZR|ouuXxHg(*cq>;pKBtvmdJafhtf~hci7Cn zhpbhy(M~pfMdpJElzA<%YEsgo$$UF+!cnQK#^O=4Z=4FRzWsw>wa4(k$!bL3Cah)AQ|^LSS0Z;G#6{tHmqn` zbEHgD|qzF%J-(|0MxhxeuM>#w(ThNVV)rZe=HKK%Bk`(g7bIko-p$sxpSq|8GSfV zd)T-^JP^#CCLdcuAE0WarY)a!U);}1xHW2NaktXj_CWvyjDi>-u+&3$C=VH=01He) z#|Hf4&A#CISR0iVUztJa3U8uZU-eMsKw^ejzKTP(WDDw74(=jfYXHemvc;jWMa7{Y z^Uk1L_%h5%Jz=7B(8;&!AIQ~QHYG3iHYJ0H`!6)~*1yL^8#o1XQdOvR5ECgburga* zb~8F_{-P`FFN?|VRI0;VX}quZZ!Y><{F~0O2MywD6Nfo2E7Up^wkSIMr3FT^ ze;BGnHxf%ShgS8e_P6}r&S4w(uUkY~O}$W%LYtmp0qDD@R#LH#A@AwuL6buI3oty( z+oox!b=k0g_GeZ1xBD-CD6WK63GZ{x|3S3HI6z+U!B++-+4_{asJh1$g3jZ8Qp3_k z=T2-?3;_qa2aet{8KQU{WdTp8{mVUQIVupPx)_!l?t7CsDjdW!`F)g2)WmY-#eSB{=h{W5d|SHnlc_59&`5P_>x zrpBjIp)ErrgV~}Vef&js+QwCT4K(fU0|$Fd))$2fu%n*6=hx$yZU{AI1Lh!cN`z{Z zBGrGfD=La65y&Z0)i$wzL6HS`W7VuwC^J*DyUpu-rcV=n?WgzkGQWLq42<{OF^C0i z3eh3nTn)x>PWr_sX^X{sp1!EtvZM+3fe$R8tU1QN3qbx)a-hHG{y({aSoUGod&grEA~6D4*0!{S4_O zi!WP|XqV7EAyb~UjL>{NEM&>>`I>j}2P#n|y7I(g!wiQav5Z{r1LFj{GRh-I)%riQ z+cQw<18JfIe!dZ2hX|zaJD(vxUU?l413Q>Ub6Eh}HVX)TL+MXZruZk~&OfDKGDn(; z@)gh0*IrN9LSJs%?I~WoPG+_d%N$08Dk$h0*zn22TQwi~*Q0u_Z$q1wU{*D%`$|=A zl}e_0QjrhS>B_yc^NKL2OrtJGm`Oz4*1p^vaZ&{`FZn4oIxa5m{X3(Glj!%emH1vV zC=R7_nUy0}rNfAj6$MLR2qyHyxsUODX(;*%Q)=VNaz~Vx!{$R5@eNd)SZ+|>qR}2~ zfvG<&f#r_15#%~en30OH99pWD`BN{^w`<*O8Robw=TnmAU0m=~Vr#pyV7oH+>~!%z z;Av(eMYLcF=A@qV55_3VHk=)ruY3<(Ms?f%3lt;SQ&K9pQz`_v{@P#v#xzu4(8RX7 zL)T3`Go8@90)(04vbSKv6hlU?0Z<*nY5p0F-pSfFP9LyRp}zbtDL} z@U`Rw`RBVYzc54g9LF(10_phUezw1*;%s+0Kl>Sqp z>EA`S|50@NKOKuFC@s)0n|`12W)Pbzvf#pV^#W9u6Sj=6gn#(9pofyA@=Oh;QaV~H z%wd^=!-b<_lc?BKT2Wow)-R7kMAiIPjL&F}5xPC4sAXenP~tUGJaBnJo(0$u)dH6e zb2Q~-i5eS=eSdLyG7w?T?7)=;&~KMuRR^;l4i)yD{5}tL{S&_RSU}T_R0Ojal)Z(A zEG3*(c&F{^;WVdc?G~&dpswzyJmNp*by8bG=JvGKugI{nXa8WOzwUD^M4}xq4TdaW zG9H`Wo&nac!($9_=` z)46##TcUjb_p#J+EFeIe1vr0Ar5>AtC9*G{tsI~$KKsBUFoJw20L^_GGOCx%^R(Sqxi<#-;Tme?ynjG5j&s6Z~h1O_$3OUa|nWYH5l2 z!Q_f_dEzQ64tSW6{!zK`=^0t7+oqNfsj*##5Z zDHXig1p^WP*bw6il^;E1Pf4!e{_Wl>{+uAVZQW~ITN!oECdM)A@!PkVAAcqTz^@p; zhn5F*2vm(yWY*%>1fKmjTlws@4 zF^~LpSJkQAfj4Rn5?nyAE4(`ms|b zoi`e%9>$DsyVh*7fM9c87Eq2|6}hB~JL-*|nO6)qtchSuv~t60KSbfYirh9G;+Ss6 zD14z4C|bWC(hNC0vZ(Y-Qf{E{vBO$x?J(BvU<|Ty`-F4=;?O$mhIh9LOrU4DDOB3! zHkHk1mD#(%fmbttAduN7*DJjL-K51a{6e6mLw_zM1!;NsLnn*=jbMdl4 zk$uo}=~paZxXp%~y7Khktc96yadp&F+Zf)|$JB2T52IgyyAY+yQHjrmJ77ngq|XcU zN!1EJUw$MklPuvi5!j=>+OsnswioZm^Y!CQjC_>V&wTOYH=_GbE$f+jCPy9qb!y}l z{7>;|9C(FHKW(GS$UM8-YIQJb=ni%5c!m6!x=iFg_29y1$9^t}-AbQ)@@gqESn$IITxjPF-w$3M1%52xBR#tnbrAba zWGTP@^G>3LkM>KnA1rZ!@bl4w=Is>GT(*H<-$N;G1y7GGPWyIqS!Y;;wf-)y=rP;8 zXNFX95mQeo{Y@>U3x2L!A{t16Oc8KzW)yzHTVK0!P!8F&(RQ-2nP9Jdj-C^!TzZmY zTD%u-jR!@^QSfIBAKShs&d^5Bjc2t(MQO0xHhFglycsOO?j8sK#}_g*2u+IF4m-w( zCLFGo4%(ugk7ZXFi2(h&)Z3_9;CasH=|`(>9u&q|NKWm4$R@!(1@?*hn{b`U?gOn3 zlGfrApCEI~(pT_|ss+MCNFurcO3@>6GTW+^eZPJlWL}`o_M2ArhuMpt)a>H^a!IT< zJXywlS9JvTp-T;uqnc@^>+T`zxkJhI5snVXJJ28F&AqALMjUa$@D+@}LnbUNFPFqV z@*j5Pcz!DndN0GH{u{pM+D~&+U#B>3TkImCLcGZi^qzYD&LGGaUAXOuw1+)WGnUnN^{&l6e!v1G`bPVAVL$Pj|E2%=-}v}n!^i(y+#n*1 z&lrbu=!@N6gcAAVl8nOHJb@yaDd$WY0))=?#lm1f( zKNB1Z33Av_4SS1HH&(WDhE9#y%zoeu7g55h_4`F#IrvLoq*i7!dzCu}C3F2J!Y45} zH2Lu6M`!;T(F&R<_O5%1Omp4oItsd2E;!Tqa$&#doUwqWHRLwL`evS>{$2~g(re0N(^F~LJyCg@sdKp~ZP4cTk+rZB1j=rhY`B2CdOwftPJ+R@#@40k zFH5{ycFF-KP;rxRs1y0bHs-6N*NJ2D%0EB2ggw8dw7X6+NI8tpgmE!@`1G4IqDF34 zdlp9UJMz!I-)|+iY%LE39CDOREEUSUX%v`kAd(WP^1w0?E`xC)fkKG4bzDg#F4Ps8 zLl{A+D&Co!=#%?X8Zkb@gq`#~Fvoca8jpWHf7<+!_VHeVVRMVXIqts}n@c~4Sz&wG zI|D2rz?`ngC=sgcpRHg4L5S98M3JiOW`%p>b-g^tt}V7-qyU^8+>Z{`sdFGqI~AVOa=JJB5aCLdm_C5pFZ6u~D`$fsF=jisRmRU~Gp4(cdx zv0UvfW7-wF5&Xh3}X2>8D-`~ww!t@ay z$+nF--#aV?;htpNPRErR^wY(#oO7FP82dH|+?oD$z^5)0<5T04!Z9^|mIbsVju$0m z4qGmnM{Wi1`&pPKI%d1~K0I@}dH*QmBI6Bl^6i61a=0*LHJytEObx9#q~%ZsKkjt-n(kO46DD>2-BMC5&V@pDPXfep+FCKH7G&DFTj&;y zEZKFoy?7=4ggmG4IBQPlRTAxv|1`W>WkdBGJ{e^&ZK>AkOGp^W?5{{Ld~V4Cf_xA3 zYJQon3v@n3v$amEvMH{m2F?WMQ|&i9-Z8K`k)_;;3T!OEheTCaxW$=4Vd|N0V7kST z^%zbM_}h``pNn67A{$~f&PA~^HwBxvRZ3Mg^g{^Je$%zqC*b-OF-vPxUo#xZWBUjC zW9#wx=tJ~FC7^D$f10b*x_RXzJvVIpMMm?MV0JG3RUfEF@wyA@XY6_ANl9lNT;*{g zDyKBj@>lnM4O#we(fJ>+K`cLaTh}<({*&6LZ7QhX{D8d2AZ;UDIH>c_%o!WTtJ>|`XzC2V}d{5 zBItU@@o&OW>MCkiCj%FpjQ*_w+#!H_hR8{DqUmnyx}H+oQLOgQeH`VUixL^I;J zRrYd^LyY)5DGXC)jGyVf{3)Ixt@|uDN}jQ@%pCQFu0<&}j6agf&mTu7Y*<=7((`b; z+R-i^Z%@}V`D}~U6Vx*;D@$a~-FzISofQ|5CKT@=`sHAuAEr@%80m<;Prb1(>v@#C ze+|oELyP8o<~%qhTJNko?eV>PwBTi&YszfG`b z0Q?M2cv|%+qE!l-K4zm--n9qWrug6swj`+0<V)e0V}Jd5sb8H3F`_w#l=fme26INY4o-_*Kzye0?6Z2xB9p4PHt=1-Cx0v6Qreb@YwuKA7 zGE>>VVpCCr%emR0H?WKM{Au-nWE}eM5|RI%h3WsDxtPJ6W4)wxw=6w(^)!kXjrylj zHIcP_OyEHlenm_mpp#vUb+l9*#Z6@uQeyJrQEwRJ1;*-&i)HvT$NpS0+a|}wqt-5}L>$!&2z7Zc@gtBPLhGk&e{&Og(#ud^=*xd2 z(2GCl*NQkb+8CKFqUH9$Gj^UOZ{KLhxI%Yl$%vSgZ|uYXAzVbb187=p{J--2_`fsu zo}DoWIIsgocubEgPFu$&38D(DoYgAM`Zl*{^nSUP(L!`71^I`GfB_&i~O_y2kUL(rl>Y$B8<5^ZhZ{tBYtSz5_J=bcc*7xL6Kg2MnLss&8XYv#xToCFYG@^(Zlstk2s+`dJ}J&qrDirKTQg_=_y7B`=# z-loQSJ3M`lxw1#*gf80PV~xS}cD5{%o*##4hk&k?d^QJ3f6wD(>^*d0EN`%G_YR`- zZGBin^+`XotXEg(UY-4K+iD+un8RN&Oe{y=pb5;4&FK+57eYQlKpe)#4?z;u-$^41 zPYwS;vLu8{A;1=lVff6ur=N)uj4gIFIzF#kOEwP?zVcFS0tIHAq+^*HQD z&w*&US9Ft9?3|1Z1iU`XxsuynkMbJ0V92idJ0kVIeVR|-bP zou$s>7hNG>Z7QGd)^7;t^24r`Upr=WyG-2oJg>lY&A$Ihp(4qviN5D~^RvYl9RJ7r zBU3u&sIszLQEbwE;6z5VYOlrhT+_ZT{zIqq6L)(K=AFn4qVmb!>z`|=8@w_WXz6wN z?v? zDf7yL>oI+)3mygE?62;lzvnVCM^RmcC!H6`mZ~1Fz0x_}&XZQ38&2!`qt32o%9wO7 zT{~Iu_Z1(zE`MowmvU+_{#>-zTYEKAi6YNy{5jcaMl~Vq=d^t0uLBBAn`+p_kI{zP zLMp)B|Fkv#RxYvy8z}rCG)}LZ%8I96?`gLrVX1w= zrIeT>dK}&N0tPvSU|_oiHl|YZ$s_&dioq*mU}_+$K|j^;qLfX-pT#?$6MKSnivIzO z%rWxxUr|$CsH6%M9BLY4&#ytkZrh-&&F^j#+$gPGw%F)2;If62xI=`hH0#s1bc+QEF2$oO1 z`yQ4v&Amg-n?{O3D^qU8x_RU+CRm@4$nUc60K5kNd(4T^?{Pgl9{nqcZ6aF^Pm2)8 zt{pXce1>k4_5$l$Xr|9uX@xDBOgDv7*;c*ZI7|Dk9W^rNoTgi+O>5ey78g40x+wJB zZ3qoBq_lIl8(dU10Y`)x=^+WJ~fW^N^K^|dDw@=HyJ3HxY5tK>Qbf~@EJ#)Kgfi7?@d37m6 zGe}Vi0z`n3oI30=vh;jeg#HUsSq^I6gi z1k2}@_T}h}S|X}DbOQp4!ED+J1dP+g)Bo05ex~@>Vi4d-QF}GX9>?@Rz{(w9?Od5E zf~+>ZJn2cw;&cC4_19+Qr$~nTe`Aa3xG*Gp++rUDRP=Be>w1=>pU~byz#_|NdKdzH zjY1({d9W}S#2e60rL*w`W|RJAlMMf%C+WYGE8jYBt-t5_ml2G92J$tyCOJ}VdzANN z07;+Gz7QY@uYdq+WeE6FU26Q|FEin$Bfcb0!mmp$A-AXqPK-0ak!2}Um~q^Ts-~_* zL8wu<2-4)m1rhUBXRgHf)FrGJhT7-;+Y-R(miNRiSa!)$&UvlE6fd9_dXy0+IE$C+Ux5U zVPpi0LWY?Nt#i(z;mN)R&5{-B5b!mn(&x--0N;uB4(2`d)weAC5v`*Tu)0*84*?FP z-P|mF+FJa_3~d2quXmKf7bla>UHR}>iLhWL67{i^^Zyhk9423Od@pd2T}^ab*~if7 zb#)niHmGG;+-co*UokB1vL0SZtR(O?z;6|N@X`;WkRj6!Y@i>CL1UkJ&7v&e_z`LBo@)QDi z8-B(wT6=VTGw+#l|8^nLXRtKtsv%jA5z<4nhlOUO#WdbQj-R&;PXdVE_} zI_tYI4j7*2iov?WgwUAb=d}Y><|UO3blb<#@4XhSO|OC3Zl+=Krr2S`6onXHW1-lN z2#52;+ei0lYQA%GY@s-bw<{&DzLp`ey;SJ9Hbm5$bqMfZYgt%5ua2_8zlZU1&fMa~ zs$TNjsSh+IVQbV@+$jQa5O8cuVQ=@thALWol(P8^JKnr!4T<~`P5=UKCSEsnP6$Yq z?Zt?rZ_AuQ*_D40Uz+KXx35kAkWit2=E9GFB!86+v~H}I)2+j6*e@)-&XRsXL%xVF zM#)A6GqbK2b5XK0zX|TrLAnsIe-#3P5@)TF@bTbYSB>%tOkh;{Oq z$Bvoz`Ghj%w_=yr8DJn?Ko=~X`iW?VOAIJ%8NeP#8n}A$*gY|{{e4OO!2Ls~gZJz= z-T0Qbz=k99f^?YsFk|HT|wa=PFRP4FKc7jQ=o6B_vg(|LUXfvx#MjRP_@2LzYGC(jwQ$lyxiEkfIt!5RL|MmAt%*ez=@LNgMP!qx0>O#pKGUAf6rviY!PmPzSIIzs_)U#mU%n`JVA@ns1*23=e_`b!#msE5imiQ=4x6Q?giuI(2*a#ZEC4Lm7mXD^|9X{JldLYQ2kfUvJ}$? zBrz`1D~~R0pAyLryZ8Y{wm9Aolk}EN!>J4Y(7Yrzb?_^t5%Hih6?+7!fBExInICbd zZNhoY=B1V_>aE|AHV8jGcB*b0Gs;tI5Ro=-=TwxP?7x?!SljnEe`jLD$(AT56s!mL zWilQk%Ff}4j`$U~)(1~6_;!6|ejdB6RDa&I=yu%+K82kZC!|Ce)hB{W>5Ia;?{qn zPVe)2NTAiv=U+c`Izb0voIpRp+X?^K@Yu49gX&sG6xAYP3g?9aA8(^{1G{oJaA~Pa ztL|kv(eeudpZ|KcuENOfjF4Uku$v6d7>-kU-)Fht@tUu`dbr`;S2N0^F;Btdkg6N1 zm*h7D+Of0;NHKKa@J#(+RacDVd8E=p^}{Qw3FrSb=yswxxd?yev8*k>acnxjy>SQIIKR{an|>r)(7StzHb$|h#LYQe z{bjfT0V2#XhCOY-cDgE@@FMtblm5M;Uzcrh(&u0gl<@(q5YU#cDS=$muG7}W)$HtY zeqg$P5NJ{@F2wcz>z}cOm(C!5MZO+3LB?sJ^3a;Jj=8E*q)xt5>iIbXt$gm>_YxnH zUjg5wU+qyTM5ZEX4qr_xg^3$w);%(++jAujyNC%UzlGQ7Z?w!6Unx5@ zBglQ{M8x>BkGXFg-`?QOW%FX90W@nz>ibN|y7*C0wA#WKvCi?`aN+Ne59 zYnV6xUC}Kujy=nST@05&dk;Qur03(b%qdYat{vXu51lATySU6}0@vQ}S+LSBOYshp z_~Yt!_Q8ugx6B-9g@|df0mOXk28X2vnz$LH`eFcj=J^MGiq`&Y)EH|I_0|r;ubIWE zTAvM1D>A!Zma5jq#qp~FP4oQrSqvoGyR4<{$9A2hZhqhzg#+|lG_eth!CEl7_xOEF z%whX%Y6tYGp zDzOewQ*Xe2OyJqh3aOX5&Dqe`u0a>#lTq8XeZ4N$Kdx4HL7 zTyAfNk&dr{dQ}2D^hO9EDsWElRU7?*@w0qS%cstIWMM6~@evr!1lOIW!!2xG^t=3p zjF0bLeAcr=U&7AEV8a4%ZNwwacW38*?f4`@zy(WOUjod9rAeO&asRpSR&7y!qFEeV z)v1}=l;zqwL5H;wk2>>Iuusze)qR$&VOsCU)0uYimeLi^8w+)}N&VzPB^Vkl46c-c zw{DLa3=&GJr&7YFiqz_?rr3u%f}&{hjBl=i-#^neNOhlbc4c_L`gp{NPHoNM+3q$% zB(D}RJ^Z&92ga!i{I};cCm0RJsj_&6cr^9yqK&zfU6MLrXQyt$m3{CX62a-56rOxy zLYtk59edDaZwY#Ioo0}JXkSA8;r@KR77-5tm4*>mhm}1StD;z4UGH`CLT~zSOM9Qj za>pkGPI!~U_hvE z0nUbvq~QdC_hs%B*os0nnjiEp@$2psX?5B?8?&djp*|(%=+!;f7WBNN9xs-sM$suO|2iDkDh>U32WK#Z}`7wz94d>BhW( zPUM_ir|(J)1aKW<*|6WM6#rD5{*~uXBeuNGxOy;a+B>HGkA!97#!XV$2=~e_9=Mum zo3#>{Oi_%?Xc<835KtD3_au+H0r%(iZ}1QMln|vx275U-d8^f8OD-P@`-HvoA5J@8 zm)uWaApP+2N3$8%S_n{wO(U?e>iCVVZsy{3G(uePI{(lz(Ofc|3May=mL+ zBJchw7EASwso}h-neX3xFVF)EgMj0RLC%KImzhlld~nmS%`ghP_%*rbh~W-vX=8XA zAFG({2m!sT5%-QA!!&vkvf-j=y`)~Mxz<<9eG&Tww;0<+_XPT|uOXl^zGgZ+Vp*eO zMox)Iyi)19{D4)r8@&qwQ=}DL6xBGq-)!C0?L%u`tA|)bZv+jG!QWxwK_|K*+x%$2 z-op@pco%ex)c5h??jDN2yo_Ei@_ePGCa0u$~(L}yId1L_PMz3^AYUl;;?<69%yiH z5yFY5E-@gWX{RBUHZJEMUA~*byb4xuj=nnzu8z;V=?r=)%98JspTmM@w_}LYax@5t zYIb42ThW1ye@$b_FGS~DZ1fwjOSX>?b-vU`_CjhzBbgCb@MsDc#uc! zDc27TfiX))Y7ILX;h+%MdHI4T(lUp8%ZuXj4=0Y>coPDpZ3VkVb5h&GiXTD@z14&pZXOWekac?7H#MR?U z>lHs9U&Vr=N`%Yc2J?xZFT(;v`ck@2Jh}5MHgcsjSF=n-_^Zsb*kfH{NA;%w{V7wy z>B%EXV?#tW>{KBHNGQS;F@4F7MnC!-Ief8BjB+VAliC*qO)7J&T$m9WI8bfm$w-5M zU?R(&{k}>*(hC9vt^H25{b;}O@sApx`{{f1Ijb_6#PU}!j0Lt2pu5Waf+3)NH)g`w zbT}jI_uIy88T%Vja|Hq2-LxOou_-(rc%tz$65Ite>KoF2b6LD;ZZZP2Did?oqaEmqjjoys&g#u z)1o{Xy{BZAyUseO13f==BjC?_@;G*~nqW)g9WHnv8d!!{$TYsG*PFFx=+5P`*{R)V z2JXP({I+WyRtb3(R1M5is!84{$?-(Uj*Y@I3igGvKVjY6c{$(6kA3=Im-u~TATIaciN2O+`aacu{<%Mw z*wOZ<{D)!t(D&HYjo$P=hRKl1x2gWwZ%^PIaZM$*Jq7CS#i{VE4Okpp6$KO03M}%= zL^dZeO@=P=b+mujl+7tvj=ofs`w9>*Hq@m{aI;3PE{zPRK18?>?aZ5dnW~_K;hJML z2?EYUuPyz=+7>oKz^Li;5(EV5R3dhGP4kSC{!IpUfv8X6n-~K#{Skb@fZns)lMdj zN%>6|F#eVZM35@63wVe}2EPZU!FEi;6+p&Y&! z;D+O0kKuf#+&W_$g&_N!(X)B`7BKKRu~Q5ITriexJgOhd+AZ! zT;I7woh{hHbLs&9)FZdA0&4WNm2nDztk!YV8g**L^zBuiDl9kN(9clmQ|lICJ2C7x5?C;)$Mbf3WP0oO!f-|)Tp&6AV}~7 z1Mopxul>HMFQ?r$i(l;t^zS)VHLUG#vj1|@hhvL_tY&Nr90FYMqL>z#&ilUZuQE`Cdr6&&hUk~P zIbHTBWnOq20+xm+@DahNB#8^ep(^y&m&$*v_qz}JF@ucJjKUmx&bL>ohbxx zAKUjCWF+}Lv&(d1ig%h@YKzuGK-S;}HlF1!Q@JAj@`|T7Z<&r^_RpX~`l*(a5O9Pg z<(t>NE}V9$E8Zp{Xow|%d~loa3l^8Amc>Ko&;GEeq|!7STPn6_S-ZKl|E0hSPlL!c ztpgBn;1C_w%4dIW%ls^zKdkn`C&RN#k;4soXVkxPmX7i(t#1+P;1aBBeVFs0q9OfY zgijjTI{!%OVbgUvJ^P1;POl%5B%b7)2HRxD8eZi3-eC|x8G#kLKr23W-*ipn>JWn8 zuX>74gJKT16xaDwRM&l2jc0jUV{d1Yof-RaPPAOqzeNjOZuFoA$xi2ocpDyBB8OEc z=lrSuY&~ghr8-iY9d}o=d=r2Lu>Mx=d;#B~;ypwyH`&B$XP7u*~YgQcA{E0lmB)UGE41V4g+7WfrB zD66=P{{UW>sjj7)V?hlnhg-7a zKe?+au%ji4uL~C+cFIJ{k|yF0S*z~LPnUmguOdZX785DFo3kJHB9j6EkOH>Fh4^-4iyE5{k5x~4jUISo_&bs^kEWJB>VryF}T z<(O|9QT*cMnxonc2yhxM@VhY;(SAZ#US?_79|8gR|?n~ zr6o&wzPpgji=|dwhdZ&Wu~YF9C&9L9)TAIwp}dCH9W!-9sV^ID{jT_kdfWrnr`sOu zDeeAKual_j=|~e0O9>~F!(&RF)ObS+0|PVF6B6|7^&TEt);Ylz2i;q<&h#tXOS9mw zay@RVAYJ`Xl29juTE}sCe3_~ipfV%6lJ1k{F5X0lzwmSLi_UAt$Zh@1eYo^{7YrZ% zXx}PK5^*qufcLT_4&mP3PIud-h@| zFJJm^L=JXjjq#PnwK7Umy9b8Q<}IFB-WX68E3aK&tsHx`ClD36e(&YSTY9I1h40GC z!>A`0`|hf%er>R5CPP3lHw3ikRT+-#V^DgYHV_jr66oswk8rDljIr%i(*BzuAa4kU(4f*|^{Unp!1+V9>>=ttI z_9#Js(P4yl+IH-vm#zvN0LMcia$0 zSd-uAn(__XLI^p38d(tWW)ud>%DX$bZG8U{AQz0ildiw~YFDuhqcq6!FBLbm8dOn0 zJ*?HtYiO?JevhRI0Z+T!*~hDPTxny|deN?-7>Dpi z9SNm(WON$@*bxTs5fMz~>8uC_ZWCLvkjimSU*8FQX0_UV&-U$RanxCX6&~g-KU;=9 z?Rds^6oJ>MT!~EX2(Klk2@7`C3Bx~3?fE82)NWS%uYNjjdc(t1P0epwirICN@(S?l zpD#l|zj?Sgu0Yh3ov|~|_{RQBAfgat0pnrbe(ckc?~DNPLg@=9qub@F72o1kCKckN z<I#PYROX&|?fh zKyaVm80BNR|9jTu0Yxp?^wpT_Dm>Wn#f&#Ir#9f5hXRT|!s^_7;+Y)oZu;CtD{*fn z{;=6k>4#wJLR`NrojkT|f8)1XB4szsrf0Za!*>}+N1ByKFLqDk+U1MQ2edqIOm}^g zN;JGKq!+B+VL$Rq)|$?rO)0fNu^;YkJZ!FY?fX4`uixPOmi;q*#3SSP$z3T10ctEI zLZ`s44B{x3mfi#bR4;6s2^?DdnCSW_5!;QXHlX$}q)+wj4 zk!ux;rB*rWeFkA>=jC1!)wFek=n$~KxrvEn$+Y28HScpaOutz3f~M5xacZDm$GNWV zpLxF!3=8HY=dkVcitTmyCC*^qmV(-k_#b+V28Rd??`Y?ga%_B7mB;UUyX)BlDu=GT zg9jED=GIhI#pPv~3(4J#zWk$|1^`J02FP;|&|=rDJdPG;$Bkc@am066{H%_WI^X7h zFX`75jFI}gaEn(jAm_d*g}^#~9}5FB3=pl!-|`(j)OBlN3LPMflvR-bN$Bd*FaQS9 zz2}l-{WESoyBqFOuH{SUhD9JwtS4YLX2mNuWbbS%Mj%drH9v@o4&C?PIr~Q=OyRIe ztdk#1zZL?rh7yT$Iq#_5JAzw;T{<2DbgOJxdzv_XpwzTx?CM5kv2S;o?TPaL(8EZU z&ZB$WRQ>%Qdq-*Bd|vrVnr!>GN>8zeN@KO&Dw(wHsmU0QLT1afAvc)ZJ~_&S53-X# z8U!+2nbq#=gVn3#kzdM{)akSZsn-qx$2d~Ao^NQCN{;@mqrHNRXclItbFMf(DubUy-yw@4)-Oyz0KJ}_00AME zECH(GVU{(REgP*ROTqEAsm3^esxHnmv`@ZN>k@WZF8JEATyEV3_S+IfBwn!6JAx^G+e3*+it`HEozAe0ymWO!-0WB(xPaxnhG8}!! zcPE&u3Si$PPU~NSXXZr9z4|xzg8V#|oX_Dt@SeppWJjBbVFaN%oDrDJ3io`6{5N_R z*aE4CPQSc8C5ogyoFp%Cgt{4KgIfA1X%t~G`7ADHO_;~~ob8+-1l*(Q!?F%v6R=>p z&>T8YaY&=2#q~v0aYG^R=bsnCKBSM#R4C1qOTW#kD|B&W^H#I-wjdzNv>8)gZ1u!V zeLch_3^A_TiYrsrMR(KYDXLW18r*%J6Lcd4%LZBV1NpTN<^n*#xE9eZcH=Z#a zhtVG4K$+)G@NBy5bXI1SrT4FzY)jeuE1qt-bVZ?UyH)x1T*d?Xj4w$|rI}*+KaH>vl2i(4Vw!zG!QYpl3|NpiB3B+TDISE^Xn-$uygO z9H$BM3frQKoys^LsJ-0|iwMAszNzXg&l$_#{k7t;7e`q%=d!-Dk$@5IcM0%7c54}j zw9i(J^IqQ!5?Li0_pnZ#XuBF)acnDKsdp1q&o;d=1_96T6^60B1@sw8= z?;g@n(-`A6`=d8ul+a=QT*8hKf~GQW+*eqyU6_-#OWX+K*k%+unHS&8-&r%ldUewz1&HMU^DM6qox(!#Ia?(7TtJ4Pi;c*7MqzcD=2t&%;ikHNco!J?0O=HI5%4 z5cHtKBvqWWxn%Ru3bZ9szEa^YTPKJQs6l{xvE9Z*2 z75XL^Xe%b6XckKTn9dz$;Ib$Ag6;d-E!cWL`>*@?9V%Df?nTc}v4o#I$GyDezJ8es z7C4Q&!wIjP+~Kl>fMFHR^=3^72#&$FsJe2L^XB8x0uJKDnA}Gfvu%X9GkV0I=;?UutG@Y!|A9 zq;Q<3K!@cN<{dDGVNPFkCToRL4eQAnshLuOe4DoAoTb=zWe0U+3#4I6HNAP|^-03n zNy6FBlJq1~97n{C=*%1m2(cvFq+>-E}!7CZ#z8lD)2y@-zrhgo2 zF{ap-A#%SX{xhL<=R|cXJ%pdQIje%vK`Vh#XQg(^gO$SUC?|ate-nJv z!K=FN$Cm#?9HDX!v!~t1wyF2yiqSgd5mq$AHtpTedYLajn+ppJs$6e&v0miJv|W}E zjz0K3)dcKrojCt%GK2U4F%?E8Fz^u^sSW%^S54aY-+l4#yBo9+)8mL%3x(>;JhRb- z4DYwkC;Gd3~EKCFz&v z7lrTZNOYDMU4tb+0L>ITiqc^xbCf{r6IyAB1u}x=F1G9ihM)OdA4;0@w*_szQw|xm zCV*dBaRM{}T=hRY5MW)k<<1gIAwYnQBZBMxvVToR0jcb0A5mND0Ck0en7|O{Gk&f< zg!h6dy3BG}>0JDi&o>wUc>Wf{wVN*GsLpZ?*b@&o?xC`dAAo>e2w(@WM?&XL>~a@` zXt{H^WhufeMdo3aWm8Q8=?dlq@fx)#A}k>hR3glGwQw$xP3Lz-*jo?~T<|+6jdQq* zo^d}58Rjm)QAhqHhOlfBh-wgE@i8zMo=?NYRMgDv#t#360NPz5csBnPMg!y^an^`l zF96MT!Ki$B7;HA-Hw={Q zfB;6?vRb}A1Q?-uAplo;bx{;%rhByIXpUUYY3`!jJ=gvK`9`|tXZ}VVo5R&;C!^?! zZD}Hi$Sdy<7JaM#lvLMzy3l(S{zCvxO|%$zz(ql<{G{C7g-9AY^MH-n9n5Yn}Oq(W%}FUje!4ikDsSc&XVmdh{% zR3d}V{GMzcJYyZm8eiI~FOqclfu)%t1P!JqM?^cic`C6^wVz&py{c(2BaI^o?V8S* zhN7Rm`#aCpL}Tn!oiA||0%-TKC+@PxZx}#8-`8TgLo58^ugT1;FhTGT>ifXt&uIojB~#DB3#(<=smLAo4+AoMlVNFJ2?7W@sYp!NYnH5h$(C+ z2M%gbb?BI|{G|-n))S*1M;t;EI{no975EVrvz$|`2i5mX?q_>KotTKYL=HEzzVI$ z+N@_GN@nXkM&y|ongc6p*O2Ys1_AH6Ij2$or&oYp^bSn_>*dtcE@JhgqmaxU;<$jz1Mba*wK!wQeNb zVNq#Z9l{sNp2q8)mwfBi&DYm7Je}Xs_t}!-`q{hF&n+d`K4Oi)5>)OW(*6M*NF?l= zGs%W6yD@kgp{{sCio;h+k6_6(9|uc(?MmnRZt!k?pTLG;GKYFc!ZCgj(9$j;Q`^Tm zh}JIGvvKz)bZJFp3Fp>4&8Hnzn@7HZiw&pyZ0v3k2D`zlH>UZvvYE2kwwng)cqL?8T42Rk3avt7m{C(?EezfFeXh0r>B4V|3g5O z`e4iFSz^9a0Z`U3vQdXdpddnLz_6)t*u$(R+;c;q;ycMrR<$~psvVrr^wA;7-iIRu1sVuWyYG+$EO)<7v2IOuuC z9AEyADb*GNTBt;Ry>U>H`e?uH>24ACKJ~hP3x44#QtcH4m zIllb3>AYzR5>!V{`I0h6mMb+4EW{t)KibN9TvhA&C%f4c{?&|b-QWrV2Lfm@KXTl8 zmU>C!Nsdne||5&{JAf-lFD~E*QKF2ztH;e4i#$H6w%mktkBa<`}M4ZWlLu#*I zm}2~gkq90~z5DugHqm?}ZiZpSGz>dWis z+pkMqy(XhlJ?tqm?JvM26*1|EoL|5mY3*y=BvJD#|F{>)DAVTKCM1|dg`gA66PSL9 zi|n{&IZMCH)*3V3{TAVPdD!R01c$Tgr#9r;QnccycG@xfnrO`xo*x%Yd{1hG#g@8z zx_Su5TlybQ`1;-d;i1zZzfc4k1VqqlX4!H_x+mR7k&FTwam9mHKiS?aS}XTk51aqJ zZAHUncmi?w#%F-{U&GeSKso*%d?(76dY^FnUTOy+9 ztzZbU9ADwPA~g*GWYqMg#$1eSiUyE2bo7$4*&V%ccVn#;n>K;#heXcm{JCPJ`v8`P zrFr=@u)~;|EQMsBK91}g0oH*4RyOEO7lk9&5Xg-V%o}XWIC+>MyG*1--~UM&ZGq$e zxFch+{Fu{)O4YN!)gb^r7+WJJ`+JffE=3o*?D1u069V8>%oV1FAp<|U@g)h{Z7ATh zvNLuIweuGArf#;Q3E5mVHGhBNdDzkW*h)?pk?#WpWM!S~7u~3g9Bh}iV1KY@B9>RE z3y67qgvvoy=?B8>+VpV8j|1&tX%6yPrlnXzWYzO<#Zh0%UBw9`k8>z?O1g^W1;Qwy zsgH{8aV+JYB1+|6AKSE?p6uxPCSm`(;p$U=>#E%r2-t5(H=^sct%)i<0PQhh zv=4cVg}}lbt5?ouzwd~9c#foYGM8gPt-}$S`x!b&tH-`3<&&2ByuG9=%IEc^ynmN{ zcp5CQUyxiW%?X4{`F+h#XU{_bD$h?3r)A&Mpiyx?a+Mdxr5%J?>;~m)mUF$CA}rqw z&8v2Be!6LTP>$76pVs#{)dBq4%^$$lt=KJD7#=IAW&3I(=8I^3MyD>mr-mhH%i+Gk zwKB+rSL4biq|kaaIX$NmDdL)nkie0N*OPvt&o>kGr!=CO*NF)bFfz~KK0q-X;bN50 z=G$@nZnYZEC+-*9%&p)|J|(=?uJGCU$4;LMRRll$Kz{cNxQ{;EhNv8F!SeYrTgagS z`Qd0&TZwF&7fp9A&5B`pBU=&&)=NtA6HvFmQxZpvbWhw2^OI#Aw`7oN*s&1cP`vVN zJUgw!q825-caS!=dT7qxn%>S&9eEeiIfWWy=@3T2N7ow%Rpj54Y_j28b#+;fLc^~d zNRQeCjv*t7HNz`s3NXW1v9+q5#y?(nPrGd1H9^oeEj^WJD)f;fdtR4 zmwkW$n3kmtC;!K1T3q9|7Pp6i%Yo?LTS4gl_#?whdG;WpRm1(2*7?6I>pvoH$+=^C z4h|^pmG}vv0Xa$BwfEe8rO!&D5I7_#?^fYa1_3P(5RQjeKR7+dk;onONdeNPFK>p> zZW@86-70H%nlW-mpRmFO0d}XXA)r5WYnI53ISdw4eX6}6fagz5M&$xdDR+-eh&m}< z>PXaEF*m8JRF&7+Tf;2TVdfFgm+@B)6ScsB(L?2frVS4}ZcCgWsGOI+Sn%oYex)yy z%fe;P9ANE{U7eoD!IM$hqkay0RsEG?nokgh>l)Ctf`olk6i8LC$!u`@xvvz(9 z(SfCzDDtv2Xepgd6jy`+jS**`o!`(jbkl>B1$>LNi<&w&lLefuijPbUa?-`zVA(=I zNOSWs@Zv5Cd5EP>*Nb}|I_+k#=v3{At?#?l2LY2t-0S|tsSV2tDSvE5Y5hk(K5C93 zC$j_oTwZzmdNfN3#}QDgg9S1?!m;(cM_`^4XG?k~`OiF!RuoZ8Tgs!Sig z%g(Z?X?`v#?AGXFAFjG=ezJo{;At1$2r0S<0afnpe{-nDXc^HhDYx=Y49?|yN~GJ^ zpajE7`qeci-r?hirS5DMArK2r)%SmPz(??32)tW$eS)_ZiDL%yRC_=XZa8_kCaA`@Zgf-|y?3>pIu< zKIgn&@5l4`da@63qKi=jQOx&ruwhtyL|2%;>*o+!7R*Q#rQxg@yB5(S}ew|-U)%CM$AiS;g|0Tb%OE!)nlsJCPd0bH6?52ff zYpSozbP|&q!o7lt-N+l%T-(SMJ+GZp#fkDHLMJKB_+U_=sIuie=bY310AnknE|rt~ zWS>rZqTY29He$zkTilM?zeq38#<_2GjJ#k<|3j$dwYdDnAePg9V3FfjT7Q?UH1<~-Y~M_U=2)@8_$ zc&90F@UmCX6Ys-q70Q3C^i=~d=zU^|$l zD@h}cj*v}fF-P^D@o{|4b^g|U_ka9+Ja=ay=H$LCmlhKn=S+`fNV6xVS)r1XawFl| z)#$H`-rxO|AF@#L!cXsN8Qzb%Ucidg#Ywfo0PklQaA!KR%}Fr8S^Q6x(7uEk=6oK* z5F%S(UVurAkHldovH>EKGlW|4x#(PbD2)jm}nIcNc4 z^0Af^wQ8+7;W^K=7p0|OK<1Y=Q%=Xo`04f($xO?7+%5f(RcY-wKJ$%bTp@r!8$AMrxe7A~ zF@No(tWZx!nWuGsH3uDdULc2`^q6zv0hY<++1)sA7^wThJqiPF9GUWT3s%??WAU4h zOkviX;ud-)7-tRxbpuKBSU)b`?C6zX7)XnKmNm;s`~e2vDdAZ~jFFpgPUPf}h0Xb{ zJin|4d^kd#xUB6yh*VzNW_Ad%)rqI5A9k}=v-D|Nv&oJr|LSHRtGFZ^L>KQus1N5W zOT}Lc&-JqxciyZo?!(f@YX>MCEExvU2CBxHJk{Jz&ReeN5Ko!mn5EY0{HFue2oiBc z&JnXdw(Z01i-m&I!jwOEaOz*i<8#Ra7mMtZmC8@&cpnt@N#L>4Sr(obsR(-1WmD2NSkL*%~Ovds5 zh&#B4+2$}{^iDe)pLLt_9R`A4{D*j<18bE0S#Kl`->aJ|Hz(55RPWi%HXSrFJMdrK zDegWD)OFUJPi{yRfK;FTiYu+|_B2gVYdG&Z@B?3ao0@`q#=Zi*YkdCCwOPm)T+dlX zL02}cE=zR%?7ODmc;flixX7DY0o&U9Ip+a2 z?p;w5o_Y2;V#`>;^~-3lHPVeZ+5?J#&bWX0{o{h===vYygPhYMn6e%=3#`NYb|(;v z$xQ-2eA<|xxEkW@PkwHoqy38;rN~qe(!9b&8H_n|-YLR>LB8?|<~rqDXa2*uoq_lZ&5nAkYBQ^!UeqoXSyA3vBGAZ8 zquys-NCyP4+q$4iKTA0Cr8Qyk+>gX_{7?>a4F&>z^>R>tE=xvn4Z+O)zy6!krxtv(K!A;@XxoM2+H$^|jnbfw{b1ZntVz*73uZ|7K#_A3sv z@1>s--(lyElAc{81vjh67Q_q~RIDzQq9&*$#iZ6PFEK)UYcVo!az{lT}@M#77S1_i7@bWwucowikEVr?)TRc%F4WRy!6xK zpoYfb&QMzf2X|8tCkq30Q^*x{E*V^(CBVRpuP5mIq~POOESBcdW&Gx!YmB#{R+6K~ z-}&|euUV@7?!WZvzQEJ~xr<}-aVB@kI(W6Qgz0`-5N|DMiz_V2Do4rXhD z`1@g4PTJ?0Ui^9!a!te}=S$nB9&;520zq@OwL#P&tah(5D1NhYS!Mrj!^b-)9d~$j z*p|W<)#+L_?=GZxDpWV#*U>y}9e+u}vAK3MoA<-D@jXO`oGI#{9`jf!RDE#d1iih= zi+eKI+u~~3gPsRMoHt)QoM|(DA`s!76@n~r*EIDZVnoGeH?y(~2K*{mmg>|A_eiO% z`_5vaCJ7Iz?LHgJ^TgUMr^vHhSF5jd0oqbAUA0+cuHpt!ZtQfP1$S-*x%6{=?d2El z5k`l-yTgW?`H+shTK%Maq^{D;e>hoCv$FS{uGL88P1#J(w{=hD-ZdE3f0OAlJ5O0J zZTU1=rYD{>#5oS>GQ4j=VLU)0oj^yrKFJps69T<2SIq#WCb=cb)n~0A?(y<^r5noSa$w%>d0o?NTw^=iezD~r$F9ceHBtXV z0LCy~WVZNC9SQb)G%}8E9g<-HOuW>u%4JkgfwDcfMvktEC1F414hGF!SVUq zsbg|Ww@;)M|8Ii`TYOvQsA z0+N2mS)wJSth{#8#5QZvh;A@2Iv!5_3D%wTcTnB%G?WJ?*3{Xn5UMG; zgiX~+3QLYu{Ff@i@bY5!ur^^}*FZVTZs9Dw_ip7{?lv4DOp)uYRE`kZ$&@@$4^KA` zz?Xn^T3oRf3N8xI4p+FiE9%RM|I)+lb+j1`1A#NxO4b#wfFvVksI}DQZ#=LyE3PLt z1@6O@hly?ki*^^`zZ3cg*gP;06j0^nNq|mxzgc{rsG2n= zA7x=?K<*`i%8wTAMAgFpq&djFPAw#GTp5VffAe%M(FHlW>bxm{`%7FWHG*UVLc`Wy z^EjD6V(Ic8@HhS&3{XBJw|#PZh-Je3S9@zDx}Lg*M)oQ^nYj);&knm8{NK%vSeyR~ z7>H4$EwgrxfHR@_spU}-_?4UfmN4+xoXpw3wu5cJ6J#mz#@|OfRMY5pTSxZjbX>ky z*z|ei7XoxX;XjB&W89TGwfA@j-EXBL6hbektMJI8g5#+%iejb7|= zl6mWwIHF3APaa?9e{LpQXtyW*+r0QMQ>%ft%Ji}j-4inn9off-Jjl^>D*X;wj9W_- zd8saNNL4*5#4N7vvdOO>m<98wRws|EoAOq#BgLw z?xMk&B&lTc?rQzvurI-7ONPAQeoW(rfUYJ&Jp>xkf;6%DB5Mpg~k?A_AftboxsD%fq~IrqBJ=Au|}Q_ z1C7b$Mb1)KiM!p8!(hO)!_0Ev>1~=E^V73?ojIXOGTvWK@tlhX;_c6Chrz&`L2eSd z8~jOTAB2JXkYaux*q| zGXpMyGXpFdQIj}2Z9x7B19fMnW4)-*kD@v}i)F0xiha7XN_S=iAMABl@tqGs<2ge{ zqOlz5=jaMio}@wH7dOjEcY2S9t_#AzuK8p#=S__WaidE4F}T7{DMW|DK;8M{tJ~=@ z;2tV#M5K$%y=u0>Kcn_vI|x5l9~`YPE<(`JsK^(&*JO|K!hpgUVg5NW1__-evNK5I zS)BJgFrYt{J0~Vut0}=yGQ4m@Ke2##iF|CESr6c4VW3_Q26pq6ma0yHO;^63L849* zWvyQ z9lQN0EO%VpVQ^8xPVwFOy-o}MP7bmHF41$p)89^L@w~1tXPS)fw)r~5uBUH=)-1PL zwXn4OZ&GS@V+W`f9WVE3h_GXC^q(1SzSZWY>WTbxQEnIibRJv4du-9nPio#YclpJ{ zS=6rICbvFI@2_1u!pyI{+M!moJ6m$=AzgVqGm0@?*E#3w=%aD=RcZX){`h|=ow=;f zXGWv0@0BUW`LLxK$Fu3g#@?;W=(8a-WL!54xf;6;tGqwK&&C82LskGU|{R!IwUq0CEAi^L1-JX!Xk$W zR1Bnv<{D~@Avh6*Ffc1cS)G2=>XsJ3yREDA|0Q213j@<(+@CODEf7_VBjNcbw<(F> zKdIGUZzznf|Igbkgfa#3i$S(taVqLnk1?MVqBxYDL~bOo#5_?P`FLX3 z7PlMeD7>kTe}`cz&EdE7RY0+|2YZu8Bp7X5(qEt1VoOGS!#G?R2r^)!VSo=+M+{$_ z@(CBp%G^P|)8vXF%ix$WP?vlMRks`&^t1PTt{-k{DpM+A0oU27D^|d}{VwSspK?^0 zi=0oz*vOYD7vqBeP{N3_jjDb~-@U$^MJaNB|SgIpBNn8)np9&t>SV8}%D z#?l1$tXOJq{e2Qzl5|07&d*a?ah>>u+d}RVZZ^kYj%=QgryZQ zs&o0`%SsO2Qr{<(iHtufj6C|TOr+rZXWuwcy4T!fe&(sh&s&uFDE8r57}#wB1Hl3e z7cP0^LU$FB7g||vr#Ce<;*ZDWX!G{3;1;|u0z!e0%MjJpnCOQJDH8*p6KL_3mfej) z@?nqqa++%=&d7bZHX&k~WoyJ~Ho^$NK;3TSX!gBr2LbWfCnxqbA1VL)bbj4TDE`>h z*n1Wtd%o~~`}0lv^6eOxgPFK2PDYJ}4qbUHqBpa~A}OQxj6;V8yXaF?mEHz=8SzEt zR^D=V+omIzzmjFB@3VbEOV%l?mnoe8)r{M?89BIl1+3-W2*&x&ab;Ol)t9Noi>a!` z<%~T!o&i3m642f;=T}>gw*FagYeQwrCylE|39oPZdFKAn3;}t`Kd3s6j?N10OQ@WyU38b}TNOKK8EaA>lDDtqsx5%0?X9cxec}?lZG5!;2-}P3| ztmkYo=WrtZA$dS_F;+b_+>U{;&@eu^Q(wPZvC(K6iWHWAqNgbTqqKv{>nW&OYb90s zZ_V#Yz!g*pptp}_2TD?Y-B!!stbD4zV$y2VAgOUbgyHflGX6G8L?P%u)muYt#@l^V zC%wo>AGd7$t=>XSv2p4U;V+hi!*iZD7A~lW(o$+dGxP&|JY}jgKBF{OuQ)}>8I^xZ z?E~=j#M4A4#GsTFC%;CaJ;2-5lQ(2-!+tH`Oo?2{TNim7X-NyW_P=UH(mODZpm}|U zGszjyc*W+m_Q}OoHg`3o&z4;1qq_b3UGunQ^Py(+N!zDl57Z6-@&PLJ9PYj$hHT;J zpaJ2qzxzKALEmSBu1~%}Pu8#axq)v`3T?X?UD}TjX6k->NVF6&R-z(XGD?I+Eb<6n zr|(CyqQxv>V6@E#*aYoo2Iof)AUEXnlm*i1OJST^73UC-B z@9S&v32^hi1s#*R6*>}cLi!V)in{LtoVtq4tP$s=yx{IW01mw7X)tR zUUZC(^>cZpX18QZRH=3?!eju_))Q+Jp-6if$PXw--}SIeH7V2&G$` zDv-t7>+Wy?dzHTLI`;|&qD^8jSa*}Mu5|&waH;uA`!vKUB1Oj6=Uo2G)rvjF9(n&B zy)I@Y$1(=%u4o^?_4(y%+Kl;m^)h!wnRN{=B!vNI)RbT#7jO~3H+O|UQSZk|waqyw zc~lA&0SXd|1X{!|lo=@$K|@YcRz{>bp-W0_=hTuQWs=pd9&IToeq6s-MZU1AR5M37 zUUy;6_uOX}y*(wh57n2%96(QUM^ke9EZFu$g08XCm*U` zQE7_1R=e8a746H|cvZKcH(N}MO0O)9w9hn^i_=NZ{_|5aP`Da7p1_vu8AtF#LMt#Z z1_RBOh~~rVMYgw!Qj8lG(=$f)cq!Bm{S_l$tG+%hX(K5&?Hp*9T0I&SdI2ZRFpQgu zrJ)4$FTBfsG<>{2?|5BG(D@g>^vkk9z~2gSDX zWuC;Am4N}p40N=uneSYln z%Os4c9x4efG<55BR=>_vpfnphMr+h~`3C;~br_ z$fDCu!imnO#cBOfEtg^7rc9Lc*JH%<#8Em%ydT?T#7SAseMUVPp9I+;eUDSKY#w>Z zu^E_ezLp`bD;(t&G*>7((YT4ad+{1)!pp2GSFJ;B+Y9#v@rQVIOAVWt^pAGfU*V+t zSWb3Pa_{GKzPpT-1eFY#{LQ$O&1(NH<-i8byMHfi4)?LYevv+Wg6BA~!+KJ9N$NTb zd{Dr1Tu_`{4}avP-|Vz!{`m7S{@^ZIl6{VPhwV0T!|E+!SjPt0CSjQU_Gd`Wv|H$N z&1bT+Pb~QH0W-r}vW@=H&R^TJhFhFn_kCy=I5cwUV2+&7-Xm*r|A+=TzmfLK{i#%% z#eK)aH(UqjJ5~Rt^Ow$D(MXSMr+!_~TgANR?l(A>rMY}Gbh)=MlQ=o;qYENEnK01A zxN$-U|7laru%Ja6?L#Lv4J0%~;8b)BV_$@?v`DgI37$`8*%iGqHKC_dJmuAz>12U} z(b7)O)LE(^{)&nTPBeq zM51XdsL(T4Iu@e+?QhV}ZjL(t9C8V`w&2HojN_p!BG}SYr2%dmRd8{`e-)c#3Xt!W z{MrdJ7@HK@B$zoO$S6?@gN%hgThro9-EW!<+&$nrRcbJ>s3KZj)WL8+b*$m3%!$P; zni%IJSf>F_%20P87d}INFkl$J&UU0QAHu*c+Pg2?VpIP;dL|~QP#nT!m)qVhr}_2U zc6hn|9H`)DuWe^>PR^A$`+OB!tj*2Q9OeCb-TNI`cL|dqS7-<4Rk3rQ9+S(E&2z9; zf&^%u6I{8D)6si_Wzkemht#l+wrK$v&>WE)di7v$s@xbx%xQ4dpZJG}21f^%2Urcn zeYkVj%3AHC#L}*34E6=*Z$lOrZ%tH`stFe^X}*lMQ*iGl75TUAV4KnjVL#DRgxhp{ zxaO}n$g(4A-|x1ivjo$KiO5ipZsZ(cCG*c|;S^WJU#Ij}>AmRdHAgB=9*BH>4R_F2 zXt%Fj2n>v-BM)aPPx+%6t1wWVH-z9M6*1qY8gCs*Bl7xRVg;}*$_9xvy9j*ug@Q}l z&Bi-4)mbk7sItK+|LY77{POcccNmB=o)R)|)2A0-Gx*0}!hke3^=g2pB-mV8 zjbJ7)A`6@*hM*j)q)U4w&9?5GVZ*@fOYgKFZVQ@g5|yS>)&Xdu8UlEridD>flb>l~-Mr_0ErKLmA_xV5g z?srpqy3kBsyd1`T#Fl}9-3Aaxrs^yV)XzbmXAkl3N|mp4k8-n!T_@b8m$DCbjmPz2 z)Mzl!sISIZ^c{zR@Eqn_i>$Q_T~K=)Z3n(%KPy+B^1sg*N-girnuY;cf*zf;IL-8M5QfiQ{B3Bx~Sv77Wk2eTG+X8@7ijOAztzQ{>QR(-PQ61baWbsCXzq#GnWP|c5 zb3?5S8>@j4^*{~GRhkwA11~6%a-XO!i>6ww$eYB`C|TtM3=9Om@kbPgdPI)Ml|1E@ zSBhE0KmLNRCuZGd^TI&TeekKJHO;O$PiH*8+**Mc%og1@U=@7+UD5N)A3HxyKI5)5 z@RV6|He-2}YH@6npM8l49vG-=bFt81i?C>7jc1F(?Y_^f-qxcZ?au2$ZghQTJ8o_} zl4_RQ7h4DmQcMyjX^lK6%rs+6H^^9_j***_G`C#J1}hh0MLyZ_lt(^{yn5v$VVpP) z)d zo)25y!UUw>~kaueBSeKZ7ViH#($vL-S3-(SH|jTY-$ZVTRqJVGdX? z<&zB+HkoBKM|`W@NKo~|uITP_&9;5|ZTuDAtlpUg91^U`QRlsNA=`XV0E@|q+!0xN`kI#SIiXXU}eLf4}iu*kq3j;enB{vAO z_le>#F!~PQdrh6Vc2?oDL z7R41^IEoJ;(tYw%&L%KDD@6)Qjc6wfUe_0JTaO^V^RB2v?wB48w)9CD*v0B5IurUt z?}gSgodd@4p%e@~#=fNU^sMLZTm7eCU{1OqTtvfrkIx_&D*rhRw5vw zNg)$20Sj*ZcfvS@E8D}m2X@x_Tfsp6k5w3meAv#*cm>1{~M3UsM@i$nX)YuF!XNb)j8MdoS*D==1J- zm*it#@tW0kaQ?tRkiDuxkG7Qmql(8PI?sLmZw-f^GLA>QvSByjQqiplx*oFcAB%aC z^L9-|*eYm&dzx{OOqef_HS49>TrHW{YC3S^{Uxb}=sH67Ja)mhKI}y1j{k|^xw2K_J}c{FTcI&A)d(Yh<-(lO_UkFW6#p?}$fC8~|h4`3iXVmuS0 zLl}02foNsjd#T1-f76I@!xGF&=)=r6whp7gy?eeC!?yJF)mXG)2>u=(UzSYuoA*Yt zEoD0{p=L+IxK2gR19%ddLef@!nc|ro#XViID8)=+G`y~Ct~vE2k~pv-4UVr{)cpak z;3(`-bg87?m~rC!qec%RPTZG4xt6o7o!*yAd30z%oYP_#l&V9fKE`Fmc>kS z^c-^?SM(2@l}dm3;A)oiODUItIzqLkCrf9zANzFPf?-mfjWM-nF1xH)SyoM)kQ}J& zW4G4=p7KKLo2uiegG1Qq=F26;UScnc!&?ZM0vkGiCI@Bvt&NV0s5!1Ra0Rb+=Bpzi zrDW8;7mV2v!R{r+$H<-eEfC2}45uxz?Y%4AhM z#pJJb{7DJNn+@NO5pOyE#a(3YEQFGUnZZBwob#`inVt=i z1;Dw%K;2O4>Ch%>0l8i>+P^%ZsgUof;zy))?5b=Cai`-3iYwH%vPSOD8I#GTnd1*w z-bpX#a|{Gmj&VI9(?_jtG%?P0=RhqOn5g6O!a(2aFEB7$!OvC8VV&o^a{Bg*^G2Jm z;oNz*hEWwhnM03r1hs){TMvy7Mvw;@xQ2E#G$*VgiyLErX$k{V7 z-;_tlAQ#SlgMpdwB(^AFgbb z^q7o1VuXj`0O3tBp9|5p<{`4&cJ62j=*0! zESXEOls}$S|HinaFXyQx`Dnl1_govPb6r~LT)rHZFE*UZM`D>{y=f*v)0U-s@OXxtkL^h1WzGI?VT7#21g&sE4t*O;2IIIg{|yVZX5}QYmf7 zkn1?QX0{Y+m@v6iy~@Dtlx0RZIva+?!|tNoVltg zZcSxgz8uD9Gr zX#xwu1$K=Rlw0fA z6|*4W`Yl{UhIvM2O6JuPCPVdx?jeNnP;85Q(!aE@j%&IH@A0mv!N6{0_fnM{4D7xM zu^hZ2_C<^@T6r1|%U8zSc(Sf%yrxdV%F%?5TKx6{+_w&M1Ysa34+cg*n`Jdnqr{0t zdZDMDmC=b22L!J)=J7vsNcwo|Scn~II1+nboi{5{^x2dy?~2}4hGvqrlkFAkG~1ES zzFmYR1_OK8?7N*F_`#4XDGpC;LK`S}o5W@uNlkyJPYw*c7|_)YTf|g*QO=HBjcGV$ zaPZZ+%NHge`vqR6tk}T7u0>9^3YQ1h#TBL$3q&dFO9Jh3^pQhOBc>pwxE(m{P#jqrTkXS@u^j~$)+e;p zIhi=zDr-e%P_6Kva-O|>&#L4*cSPX{G=jz?h$`$7?AVI zh5<|r49wUTIvO-1S2UjE*EdzUA&wWy+lBkdkeUY!G_66yFz{GL0|ss%Cs1#*1z;dZ z1DvSve+dIWg_2<)LlnK7v3){3rhD+=-VPaln9Y&>*M7^L-?4BI&2WMN!ElB*H!Q0WWS?{fp-BY2k0=4o{P5R< zf%^Cj7>G2%b>we98!_C2^OJj8?K=zvXEWqtqc$bCFYwi9fPn!5ErXOW<$o7?3j@p8 z$c61RHLWjh_&zZ)b}5#J`2mVXCQSM3FuGu%nqZ0Gq*mwD;bk>_l&(vWWY0R0QU==V zV4#0Cdw0}KY8d+}1Tw&8iQSrH32X)ojP%$cS?YeF4ckpb<;zY^VPi4iMlm0X+m8Aa zyMB6wDRa43KVKp8khN6GaNv(9H^)s53?hJ(?e>GJbMAXDs4&udGdZalAY)tL=^Ow3Pr1?23Sa zk5)J`3^0#6Ahrx-0z@tM*wLpwofP8QKD0~eoE%TLt)d8;I{VV&^La2Nai_GNU(!O+`D+PD;mFF*NOB4haX&EeE|pZBVszfzum zDnI|!v<2;!{Mj=0wLQh*9SP-IPP(`~Y!7I0JY4lk3nL-y>->hgV=xzmkz{*tvT=%! zHb+p6&ayi1$8CvTW$bV1sr3aM44S@9n4!o@Q=C0mzXzmpBqvIfE*v^B)AR`Obr12! zGNcjI>`Q7ChUC%p9CNFlVio5H6?juoE6lJ~dt;?%c#q}3OQ&4E?1-%eya-Lg(8Vq; zU)>K}6TWm$@wnE7dL8;Qt!ZIkB+>IQZtCyW^=FlZ)}4=TwI37O5vj|gfZ#XFiBz1< z!}Wr7si1h#GVeT9x=7}x{o>6WPN?R&--BqkfNB@iV{f5=TQc*EyETn45O@sNbpcn6D+a%_2`b#b;3h2%RG%^T~O zJJ(xqr2ZS)?HHkh$Lj1j`MvDvS1prJdZRvfDdWs`HFwuqjcFUk1^vAl)1)&#$(nYw z#`z6Tzt=EONO_0dV8%k>yor+#t2vvyRPKgk`d$jP-g5rt{irkX?L(s&{ZW3dKHG=& zkbUnJGJzpSYT+)wJx$_v6AnO8EJL2PX_N5=8uO3KU3kcVr}?3DBh z#I{S{88lnw8Vu~-L-$^^W9dSQV=(aA(-F1b0p$Nub2vWB=0tq&_`OPdo(8EvlWY9u zM^1f<_*b!RjEVCwx;MOjVnj+gIf#0)l+5#w{`Zdtb7 z<#lrmfq~E)xK`rYRc%plOx+O%8XuHd#262Sx_=&llrh)jPMPK9-chxu=U2MmPz z-nOS4xWO9NXqRhs*&%JCL6Q<`7ZvK^T!XS|535GxW|j7wA2k2Hbg$|3TEpd3{-r|~ z6icCveTjy6ue$!7A@$|{U1Go%FI&yDKMAzt&e0J*7g69?QZ4T?}Hsw1> zXL$8&zKk)hkB!(bha_YXRGzLZQ-cP$9+m((P5qDXUV=%um)#<)x>r z9j1h%DP6Ow)3aC@Bepc|6gr& z_TEy)R!K%yu8X5cR5E0;Ak@z7SfIWh--Z3`yKBH^esHKkUi7+G#pOjC?N5ZIH9OM@TP z{mV9&C_MoK1yfP9sA(Rq&ORLt znu28xCM*6o*Nixtiu_3p14qAt#i)=PX~?#BrU7(`b-et>bt&p*S5GM3{piev?E0XH zrQhlCVw|^FR6SFhmtK;bHtRL-m^s6YHZ{9S^g8tP>f7`_rPmNzm9D{j2D!7&*_U4S zZXoW2P_;~SzCwAp&cCk(5_i=?Vq5Q7y#FBZ>~)j3*oH_%j%kN-7DBU(j(ED1kL%zz>2^h#2$e%s>_;ST^IOpfxP6iBwXx{DAFD_L+ z*>G|+h^x-YK_{>uaNcPPvfX;DV4xYpuPqIw-}|uS*lyeqpMaL%+9XJVy@ehuu{Q98 zwiv@?n5fap&gs%TNh4OSqSqpL*#}5WrxF-I)78eF2WVb;fn?q;=Vgl`nSLdt1iJay z59`d~oqga!k>8mqBp&34a$ZuC!`AQu*z_ef)hLP663XQpq{|NBmdAt}8n^7d#$muF z=L5G6-0ehK;)+3n$l=Z}2$qU;?xm>aVNp`ame!jDwD-M%f!d78B!^wD+X2-V0bygS z-7GV(&ccJd6YI9I-F1Jd3(eSFf5`liQ3d(#-)r{oXb!wj)egx^m+<4MQ3qk5PK{_s zmfi#hF?+Z&bKJXko^IR-0acO1Ls^JmYZz!qN7_)gG+^Kj9=bCC1B`>4k1V*z{QRsQ z=Wj_4$IHvhKUBqBk%&QC$LMRu=>J8@Q-(40yBJ7=G@i9MmN&bVnw>V{e-84NQzjGU zdn5Ky&VpSTIZiQddN;2;onM^};vDx^1+`0wqJtD$4+F(D&j-N!B&v@17wd6g;! z_;c8!t(dqH&G*g6%*7NO7aqNn>oep;~p}vSs3G{!-@AWp&3Gz%Th7AT{w~ zM=k#srSA{#@#c5x+Ux(nAWSU~gP@x_Z|d5S$ShG+7+A9ekF2L$PZLwf>oWT-`TR0x z6$XNyfKL%Y_#!e}G^f#w*r*y@vxAXIa2y|;zvaB1!auMwchQ7|vUz)Z2J_g?P2%G2 zzH#|(U5j*vM7{Rul|O-0&hvHEy-=kT&iQ*gi0XuaI(ZndJ#-g6DqL@~g|(%?z}p-b zuB?~07%0XBBKNIdNvZT7tll}|aCWx*qJ?U$00cNs}`T4E2cokD$) zBy_7n3d?LMDF%|6Oevxs^#4EF`}Sz4{_pQ2q9l`Ba-Bj{l#o;|2PK#4BMG5Qg@mMX zEzA+QhfwK5HAQk68bTr&j7u&hmt00=29;~h$mL|tob#;te%I%D*7|;a&mYfkeV?_S zXRYrav-bRR&N}bC_c`yq-+RAa+oz(BEQ=ajI%og!nxswYmwM406YFZUg_V|9Hrnz~Y0uDqmpoR^o6b`Jm zf-7!(Drr(CAhcZ9-v|8TH!6Mn+M?^&&ymecQk%W{tHoONO1r`5yLPXMtzNTfI3P5@ z&sl{K&gp)Nq!FQLGI*_arvD4q!sxTHy6W{o#WI_lJr+hA>S415{ZY5=I1qIn`{1Vk$&Gswk%CjERt{GG zB*bXlcP3DEThLgRHwaQ0^38DW|PZxCyQEfAM|)^`Az@ep;!E z7fu{=O2yW0;c7Rll=3K;#J4}L!*6p5@1Ad;FReyn5n{c|kERhR<^)-xJIH^7uT$5z z;ZxqP($AbZZIENRNvm~Glo!sA^Pq+o%G)?N5FbcaB=>CWVpG-)zx-^*8vKC+3HPZf zrf&lGy^81DJ>h8-{Y}~SXIvvC(nJU$X$xVD6bMJ<6sI1L;^C`5_hzTqRBWA z)de+Fz9LnU5-R-@NvnpB!po_Z!oDT$j7+he3$tYRj$`Y1!(o|V=w8*dlu>uTP8@h~ z^7yBEYzG;{I-w18Pk)6Y?2-7d>p6tzp!l{`>rcFAOGRF-(@^y&oZ#HIAIw^wL$(f} z($mLzvHHA&jFry@E;I&3vQxdT^48DnW3TH;mFCY_=}#SclN(M(-ve;ql-pidIGUqv znrY2ZPkM$#AEEF(ALn@~eW|6K8eeTYs@b%tji@cpv{KJh{NiWOB50eqYX|)3?paDs z%WAK-!58lHV@(tVRD(0!c&r2g-Fho$_a0vx=B*2->%BU(FLapL$dZ^OsgOTH^TQn4 zgu)>lh;qQ*KbG%vuk9rZhimuFscWrQ+--HrIMDm(Ep&2#U$r6*QBGzAb=5;L zdR0{9@+bO|O&Qx3*-D>bvuvd&YrZGJhHP?X@x=i<(y6aZB$&B>RwIGYx?}fIDs|gg z%gvGAVY|N@PyGv&ak|zJBrMSbs!RMMHUT&r2i8(am`eGQX8`ffk-ryRuaDGg52>=_ zW=b{|P}bK9vOz)h*XR9AFJ@hGJipLP@A$P>;En$Sr0dv^{1={viv zX5Bn-K>Ri@6Pg&oBq6rmKN2V#gOKfd2vR~9cKJQD?5AfV*RQ8^o6-#*vOL7Z#_#N>z2leI z;!tUZBd?mQZgy3vmZ=>bsKmKgV{awbx7WZ{M^TO5T4VZ;9*A`pDpyaqQMC~V024w&?tXiXTQko@Bd&C( zSvQwGhcrp$sWUjh(O!DPc}6B8-YmLAXvfJ5qSN`Vvay58$$MHQ8Y#2y+Upj%T{s{V zhy&5#GoX8k?=j>aCu-~u4%n1^rhM{-L-ntUk@anT)~|2=_)PPvxB6i7bBhNt@392z zmI~v5S=^D2fsYIh^~|=Yl$TZ>@eQSaIV51o(zJQ#e)c;bZSxm2|1UVD;Fva|NkS!j z*>k9jUPHIrnRX)$j<#jh?nz~hSCLko57YdDlr0|#k6Mizd8FsBzJ~*k=7ycHHIrO3 ztl_}>AE>&rVBaD^e7I~LwSIbNB_&N)JjK(Zb3ZoIp>VZVabWR_#nGGxyw0r>!6FFeuZseCEXgsWj?0~74}+M2Wx2Tf?}YB~BiKNmpD#&nkAK|W$HA3_u9H8` z1|_`PeR;&NJ_Uvh+Vd%;g%u4vqn4r1)TqZV3=$+t{h zlMC1JSc8Ta%~kAN#b{jd2tMGK{P>aAnx^2T(qf&%#`jDGVg3t>wBmqJIu1mimSVTY zFVN#j6`4zysRgHMzMKkG?supzk2PzrM02|xb$ck$jVT`w9A zxpaC=j;Z(2Zfnq4Fu_HWYmNi48i*ba97<)UVv_wJ>XV9`hoZp+D{K=Euy^wHSY-U? z>DF^_6=t0o2hGU(;Xuy)s=`v!`=x4Eb6ORBWF!vDn6dyvfj|BlB%2etpRR}+R&m^R zNjPdwv3a{`zf)bL9V+-ayM* zk*y?DDx;YQpGakvAB1Bw&)uk#F0W3UZgy$hvccO?pj@4l|41b&E#J|dQd8W)yY79! z;Z<~=%is`0sq)c7YoQG-d!N}Ah!%;Q1q9*ZkyYq^c)5`$#nodR5Km%%F}R*FljV6g z_|9cxR}UXq4W+BD4tB}6zI1`SVsN~lycHUx7D1D0m8jFevJ7-inCh-y(zp9F^K(o0 zF|h*W{dTc(&bC4utTw}DG=smJE8+0iQB2!+xf~N4!hv)%PA|rgx5eVC`Ex{YdJ+es1aW|I?R@~pmo4-5UTSkv=&Gq2`~wCqdruv_RQruMP~e>ZO*%Aq9HfQn?k+V5z$P@I&qB?YC~ARo%2oP9|xWBwH8TF)7wyWHRbBN%uNa&`vZ7l zcGk_i!34@i#Gn}zGICW<8Z8ky4S%3r7|dcgl->U@MJ&FyqZG9u-+~%II;$l31|ezz z2UelhS^i~%hfBS0Fbgx=;;)o`$klQ3hlDud{5C|FLknaF-)%f z<>&|Yg=9L*#;U9Gx>rg~8!|B4pUKrib-H(jPix1S2$p9*M~pyk1@d{L{tQ$MKAQU- z4vBG{epU}H*}ORZ9eg;agagF>THn?)ZuEjl$jd+O7Y_$kA^JG*wc9ThYjgO<%f#f5 zEn`ZE4E^gzKU=J~a9rH|w-jf<8I+%=OXC2|1^cj-mu@2cei_?@8v8HT?!N#nJu=0C zGFszW!h1NMT^Lu_ zAFH;TVLX^HSq-&G!2Z0*8Tx{`lY<>|*wWKaad)fY?#8F8$jTc$HN+2p31;B(O4rqNm49?92vv`P7yx^C2R75+VuG|CI--; z2%jWBfx6sNO^TzeLZ#rusVV=ph(TkWY}TT~F14P(2U=M{C#=NXEwlvGB5z!%DJr0< zm?v&40%)@Qwg((&H^hvgp#vNOmc2`pxudQuml+yoUDLa`&NXaWVZ!a}cjo98EdzRTV;xVJ32iV_i3H+=3^{`HslH-P z2KtEvcS5rVj2{FLJ3|;$K`#9Z&EIC3C^#gg<=#QMOR&MBp7Q=AD-7cR6$xX7;=q@W zC6-v5V-AmkiU|BRl448aK!{}(k-Jr2;xy`p1f0D}{5h~db9jvuvPn^2iP$I3<+nMZ zA-1=@KG17Y0IYq}x9skdl3}8}lf>0V@`V+lmW(YC;7e937JVAalS8UbF|xREfaaRm~lmpA@RBQ22}t(+)ZN2 z{_7rm5@JZ9ayXD<3Af_FT3;fj@66S$PLaaaD&WAjS{?-lX3TrQh5H9q)C&=au>##% zFg&Jrq^!I*aCpuAb*@LO95?OEwTn4qA>d%j0sxt76>7iynH@_uFmbjDKIn)if}$yJxI6Q*|jn0x;2?I3V1GUgo9icktZVA1Gm*u=*`o zR_Z-ZMoOG5`_z_vf4wsu3m0f;v1xsjyK*V#x!utaFy0`^1@RtT7*Wo9GR@rC-v0E{ z?2F?3 zx{97@rPbi}{Y?5t*%VA1u^hc)HtH{m_&1sBR30vTe(-w54T8=enwdBdtBDxkz@bbw z1(RF?QJ?&KPk#|(AjO}#b+5dirtg1xccZmLv}W|jsC_DRTM=GA)Iz7e)mS=?xIWQL zBF5GMFC`<`B5@_EUlxZqJ*(wqU>kjevQuN}gdZBTKiSiVyM8DsX0D^`z=4KWr1@C- zEgV?nl;FVR)Jk0uuK@HM5yXawtAkSGaA3oNVMG|irRThr$8V3SI}vS9ul};!q3ke_ z_HJB~;LMs6nxKoLhW@z-WYx2H(o#0`4AXlriRWRLp%J)RYUi5t`_1h3srv_ZdcMB;+9 zg{LznSMrjVG76pR+DcxqE^6Fty>M9IZmPK^H|j-5D``!w2Iue|Td7bIqfX^ii$sv| zUWNMH;ZFO+_q{VtI_Ln_0>Uoqg5gK0x3JyTK}$*7nl{#{C(HXA1C2=)auH*|^&*Af z!>l#CMr^;JW*_U+CR$IxOJ#Y}S>bW3Mq9q^Qtf)W{7$LfN z`4U+cH7tK^`$kJyp*(qD;?UXNZ|4GFr%@5K0`+YqZ-F{&Tj=@Tkk^QSEmq#3ECDT7 z_y*v>O9yA@f_7{baoR)~QNn?L?1OEV+fHLvRGRKl%s zfkbhau5%@O?o0+tIJa(*bOvl%iqVcr*DH#dPl^h(1_NQOq9ppFCN1Z^_eER2IeB2IHS930v z*09qx)2WvsmSeXm4!{RcDh@r`b=z#v{pxJ!yT7&24%~k+|A@jtRaL5H;f{8Oki=lO^Ihm_pPfaZT#U4x>0hK2 z|1PQMKTBXo=(UUp*4jUtb_q%;$@7s9EIs4wHk{Y|w$tNUszOw8{_D-rZf0CratkO@ zr#LAw{Z$#Ug$K+Awq!5gNO{Cg(sX?d3v9ZlA`S{#$Y@`yAzF3w=ZgGac;0{4y8nN= tkD_fdc!3@VO6oh-abzQnq-Z3oYXkBralS#C#Nf2Gyo))BcR+mTe*lLbiq`-D literal 0 HcmV?d00001 diff --git a/thesis.bib b/thesis.bib new file mode 100755 index 0000000..f02110a --- /dev/null +++ b/thesis.bib @@ -0,0 +1,396 @@ +@article{DBLP:journals/corr/DragoniGLMMMS16, + author = {Nicola Dragoni and + Saverio Giallorenzo and + Alberto Lluch{-}Lafuente and + Manuel Mazzara and + Fabrizio Montesi and + Ruslan Mustafin and + Larisa Safina}, + title = {Microservices: yesterday, today, and tomorrow}, + journal = {CoRR}, + volume = {abs/1606.04036}, + year = {2016}, + url = {http://arxiv.org/abs/1606.04036}, + timestamp = {Sat, 02 Jul 2016 18:16:28 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/DragoniGLMMMS16}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{Kumar:2014:CVI:2578855.2535841, + author = {Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott}, + title = {CakeML: A Verified Implementation of ML}, + journal = {SIGPLAN Not.}, + issue_date = {January 2014}, + volume = {49}, + number = {1}, + month = jan, + year = {2014}, + issn = {0362-1340}, + pages = {179--191}, + numpages = {13}, + url = {http://doi.acm.org/10.1145/2578855.2535841}, + doi = {10.1145/2578855.2535841}, + acmid = {2535841}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {ML, compiler bootstrapping, compiler verification, machine code verification, read-eval-print loop, verified garbage collection., verified parsing, verified type checking}, +} + +@MastersThesis{montesi2010jolie, + author = "Fabrizio Montesi", + title = "{J}{O}{L}{I}{E}: a {S}ervice-oriented {P}rogramming {L}anguage", + school = "University of Bologna", + year = {2010}, + url = {\url{http://www.fabriziomontesi.com/files/m10.pdf}} +} + +@article{nielsen2013type, + title={A type system for the jolie language}, + author={Nielsen, Julie Meinicke}, + journal={Technical University of Denmark Informatics and Mathematical Modelling}, + year={2013} +} + +@online{agdastdlib, + title = {The {Agda} standard library}, + howpublished = {\url{https://github.com/agda/agda-stdlib}} +} + +@inproceedings{bove, + author = {Bove, Ana and Dybjer, Peter and Norell, Ulf}, + title = {A Brief Overview of Agda --- A Functional Language with Dependent Types}, + booktitle = {Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics}, + series = {TPHOLs '09}, + year = {2009}, + isbn = {978-3-642-03358-2}, + location = {Munich, Germany}, + pages = {73--78}, + numpages = {6}, + url = {http://dx.doi.org/10.1007/978-3-642-03359-9_6}, + doi = {10.1007/978-3-642-03359-9_6}, + acmid = {1616085}, + publisher = {Springer-Verlag}, + address = {Berlin, Heidelberg}, +} + +@book{lof, + title = "Intuitionistic type theory", + author = "Martin-Löf, Per and Sambin, Giovanni", + series = "Studies in proof theory", + publisher = "Bibliopolis", + address = "Napoli", + url = "http://opac.inria.fr/record=b1093069", + isbn = "88-7088-105-9", + year = 1984 +} + +@book{nordstrom90, + address = {USA}, + author = {Nordstr\"{o}m, Bengt and Petersson, Kent and Smith, Jan M.}, + citeulike-linkout-0 = {http://www.cs.chalmers.se/Cs/Research/Logic/book/}, + citeulike-linkout-1 = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20\&path=ASIN/0198538146}, + citeulike-linkout-10 = {http://www.librarything.com/isbn/0198538146}, + citeulike-linkout-2 = {http://www.amazon.de/exec/obidos/redirect?tag=citeulike01-21\&path=ASIN/0198538146}, + citeulike-linkout-3 = {http://www.amazon.fr/exec/obidos/redirect?tag=citeulike06-21\&path=ASIN/0198538146}, + citeulike-linkout-4 = {http://www.amazon.jp/exec/obidos/ASIN/0198538146}, + citeulike-linkout-5 = {http://www.amazon.co.uk/exec/obidos/ASIN/0198538146/citeulike00-21}, + citeulike-linkout-6 = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20\&path=ASIN/0198538146}, + citeulike-linkout-7 = {http://www.worldcat.org/isbn/0198538146}, + citeulike-linkout-8 = {http://books.google.com/books?vid=ISBN0198538146}, + citeulike-linkout-9 = {http://www.amazon.com/gp/search?keywords=0198538146\&index=books\&linkCode=qs}, + day = {19}, + edition = {0}, + howpublished = {Hardcover}, + isbn = {0198538146}, + keywords = {type-theory}, + month = jul, + posted-at = {2008-08-07 16:37:39}, + priority = {2}, + publisher = {Oxford University Press}, + title = {{Programming in Martin-L\"{o}f's Type Theory: An Introduction}}, + url = {http://www.cs.chalmers.se/Cs/Research/Logic/book/}, + year = {1990} +} + +@book{Sorensen, + author = {S{\o}rensen, Morten Heine and Urzyczyn, Pawel}, + title = {Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics)}, + year = {2006}, + isbn = {0444520775}, + publisher = {Elsevier Science Inc.}, + address = {New York, NY, USA}, +} + +@inproceedings{Guidi, + author = {Guidi, Claudio and Lucchi, Roberto and Gorrieri, Roberto and Busi, Nadia and Zavattaro, Gianluigi}, + title = {SOCK: A Calculus for Service Oriented Computing}, + booktitle = {Proceedings of the 4th International Conference on Service-Oriented Computing}, + series = {ICSOC'06}, + year = {2006}, + isbn = {3-540-68147-7, 978-3-540-68147-2}, + location = {Chicago, IL}, + pages = {327--338}, + numpages = {12}, + url = {http://dx.doi.org/10.1007/11948148_27}, + doi = {10.1007/11948148_27}, + acmid = {2087316}, + publisher = {Springer-Verlag}, + address = {Berlin, Heidelberg}, +} + +@book{Milner1999, + author = {Milner, Robin}, + title = {Communicating and Mobile Systems: The $\pi$-calculus}, + year = {1999}, + isbn = {0-521-65869-1}, + publisher = {Cambridge University Press}, + address = {New York, NY, USA}, +} +@PHDTHESIS{Gui07, + title = {{Formalizing languages for Service Oriented Computing}}, + author = {{Claudio} {Guidi}}, + abstract = {Service Oriented Computing is a new programming paradigm for addressing + distributed system design issues. Services are autonomous computational entities + which can be dynamically discovered and composed in order to form more complex + systems able to achieve different kinds of task. E-government, e-business and + e-science are some examples of the IT areas where Service Oriented Computing + will be exploited in the next years. At present, the most credited Service + Oriented Computing technology is that of Web Services, whose specifications are + enriched day by day by industrial consortia without following a precise and + rigorous approach. This PhD thesis aims, on the one hand, at modelling Service + Oriented Computing in a formal way in order to precisely define the main + concepts it is based upon and, on the other hand, at defining a new approach, + called bipolar approach, for addressing system design issues by synergically + exploiting choreography and orchestration languages related by means of a + mathematical relation called conformance. Choreography allows us to describe + systems of services from a global view point whereas orchestration supplies a + means for addressing such an issue from + a local perspective. In this work we present SOCK, a process algebra + based language inspired by the Web Service orchestration language + WS-BPEL which catches the essentials of Service Oriented Computing. From the + definition of SOCK we will able to define a general model for dealing with + Service Oriented Computing where services and systems of services are related to + the design of finite state automata and process algebra concurrent systems, + respectively. Furthermore, we introduce a formal language for dealing with + choreography. Such a language is equipped with a formal semantics and it forms, + together with a subset of the SOCK calculus, the bipolar framework. Finally, we + present JOLIE which is a Java implentation of a subset of the SOCK calculus and + it is part of the bipolar framework we intend to promote.}, + series = {UBLCS}, + volume = {2007-07}, + year = {2007}, + url = {http://www.cs.unibo.it/pub/TR/UBLCS/2007/2007-07.pdf}, + institution = {Computer Science Department - University +of Bologna}, + partner = {UNIBO}, + status = {public}, + task = {T2.1, T2.2, T2.3, T5.2}, +} + +@misc{BPEL, +title = {{WS-BPEL} {OASIS} {W}eb {S}ervices {B}usiness {P}rocess {E}xecution {L}anguage. Accessed {April} 2016.}, +howpublished = +{\url{http://docs.oasis-open.org/wsbpel/2.0/wsbpel-specification-draft.html}} +} + +@Misc{jolierepo, + author = {Evgenii Akentev}, + title = "{Verified type checker for Jolie programming language}", + note = {\url{https://github.com/welltyped/jolie}} +} + +@article{Neis, + author = {Neis, Georg and Hur, Chung-Kil and Kaiser, Jan-Oliver and McLaughlin, Craig and Dreyer, Derek and Vafeiadis, Viktor}, + title = {Pilsner: A Compositionally Verified Compiler for a Higher-order Imperative Language}, + journal = {SIGPLAN Not.}, + issue_date = {September 2015}, + volume = {50}, + number = {9}, + month = aug, + year = {2015}, + issn = {0362-1340}, + pages = {166--178}, + numpages = {13}, + url = {http://doi.acm.org/10.1145/2858949.2784764}, + doi = {10.1145/2858949.2784764}, + acmid = {2784764}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {Compositional compiler verification, abstract types, higher-order state, parametric simulations, recursive types, transitivity}, +} + +@article{Leroy, + author = {Leroy, Xavier}, + title = {A Formally Verified Compiler Back-end}, + journal = {J. Autom. Reason.}, + issue_date = {December 2009}, + volume = {43}, + number = {4}, + month = dec, + year = {2009}, + issn = {0168-7433}, + pages = {363--446}, + numpages = {84}, + url = {http://dx.doi.org/10.1007/s10817-009-9155-4}, + doi = {10.1007/s10817-009-9155-4}, + acmid = {1666216}, + publisher = {Springer-Verlag New York, Inc.}, + address = {Secaucus, NJ, USA}, + keywords = {Compiler transformations and optimizations, Compiler verification, Formal methods, Program proof, Semantic preservation, The Coq theorem prover}, +} + +@Misc{agda, + author = {Chalmers University of Technology. Accessed April 2017.}, + title = "{Agda}", + note = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}} +} + +@incollection{MGZ14, + author = {Fabrizio Montesi and + Claudio Guidi and + Gianluigi Zavattaro}, + title = {{Service-Oriented Programming with Jolie}}, + booktitle = {Web Services Foundations}, + publisher = {Springer}, + pages = {81--107}, + year = {2014} +} + +@book{engelfriet, + title={Structural Congruence in the Pi-calculus with Potential Replication}, + author={Engelfriet, J. and Gelsema, T. and Rijksuniversiteit te Leiden. LIACS Leiden Institute of Advanced Computer Science}, + series={Technical report LIACS Leiden Institute of Advanced Computer Science}, + url={https://books.google.ru/books?id=QZ1wnQEACAAJ}, + year={2000}, + publisher={Leiden University} +} + +@inproceedings{zhao2012formalizing, + title={Formalizing the LLVM intermediate representation for verified program transformations}, + author={Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo MK and Zdancewic, Steve}, + booktitle={ACM SIGPLAN Notices}, + volume={47}, + number={1}, + pages={427--440}, + year={2012}, + organization={ACM} +} + +@Misc{redprl, + author = {Jon Sterling}, + title = {The {People}'s {Refinement} {Logic}}, + note = {\url{http://www.redprl.org}} +} + +@Misc{coq, + title={The Coq Proof Assistant}, + author={Gérard Huet, Thierry Coquand}, + note={\url{https://coq.inria.fr}} +} + +@Misc{isabelle, + title={The Isabelle theorem prover}, + author = {Lawrence Paulson}, + note = {\url{http://isabelle.in.tum.de}} +} + + +@inproceedings{de2015lean, + title={The Lean theorem prover (system description)}, + author={de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and Van Doorn, Floris and von Raumer, Jakob}, + booktitle={International Conference on Automated Deduction}, + pages={378--388}, + year={2015}, + organization={Springer} +} + +@phdthesis{altenkirch1993constructions, + title={Constructions, inductive types and strong normalization}, + author={Altenkirch, Thorsten}, + school={Citeseer} +} + +@incollection{crole1993deriving, + title={Deriving category theory from type theory}, + author={Crole, Roy L}, + booktitle={Theory and Formal Methods 1993}, + pages={15--26}, + year={1993}, + publisher={Springer} +} + +@article{coquand1988calculus, + title={The calculus of constructions}, + author={Coquand, Thierry and Huet, G{\'e}rard}, + journal={Information and computation}, + volume={76}, + number={2-3}, + pages={95--120}, + year={1988}, + publisher={Elsevier} +} + +@misc{hottwebsite, + title={Homotopy {Type} {Theory}}, + note={\url{http://homotopytypetheory.org}} + } + +@article{voevodsky2006very, + title={A very short note on the homotopy $\lambda$-calculus}, + author={Voevodsky, Vladimir}, + year={2006} +} + +@inproceedings{pfenning1990inductively, + title={Inductively defined types in the Calculus of Constructions}, + author={Pfenning, Frank and Paulin-Mohring, Christine}, + booktitle={Mathematical Foundations of Programming Semantics}, + pages={209--228}, + year={1990}, + organization={Springer} +} + +@inproceedings{constable2011trimuph, + title={The trimuph of types: Creating a logic of computational reality}, + author={Constable, Robert L} +} + +@book{constable1986implementing, + title={Implementing mathematics}, + author={Constable, RL and Allen, SF and Bromley, HM and Cleaveland, WR and Cremer, JF and Harper, RW and Howe, DJ and Knoblock, TB and Mendler, NP and Panangaden, P and others} +} + +@incollection{constable2002naive, + title={Naive computational type theory}, + author={Constable, Robert L}, + booktitle={Proof and System-Reliability}, + pages={213--259}, + year={2002}, + publisher={Springer} +} + +@article{gordon1979edinburgh, + title={Edinburgh lcf}, + author={Gordon, Michael}, + journal={A Mechanized Logic of Computation}, + year={1979}, + publisher={Springer-Verlag} +} + +@article{cohen2016cubical, + title={Cubical type theory: a constructive interpretation of the univalence axiom}, + author={Cohen, Cyril and Coquand, Thierry and Huber, Simon and M{\"o}rtberg, Anders}, + journal={arXiv preprint arXiv:1611.02108}, + year={2016} +} + +@book{milner1997definition, + title={The definition of standard ML: revised}, + author={Milner, Robin}, + year={1997} +} + +@online{literateagda, + title={Literate Agda}, + howpublished={\url{http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda}} +} \ No newline at end of file diff --git a/thesis.lagda b/thesis.lagda new file mode 100755 index 0000000..b5dd1dd --- /dev/null +++ b/thesis.lagda @@ -0,0 +1,294 @@ +\documentclass[a4paper,14pt]{report} +\usepackage{extsizes} +\usepackage[dvips]{graphicx} +\usepackage{geometry} +\geometry{left=25mm} +\geometry{right=20mm} +\geometry{top=20mm} +\geometry{bottom=20mm} +\graphicspath{{image/}} +\usepackage[usenames]{color} +\usepackage{colortbl} +\usepackage{multirow} +\usepackage{setspace} +\usepackage{xargs} +\usepackage{mathtools} +\usepackage{qtree} +\onehalfspacing + +\usepackage{ragged2e} +\justifying + +\usepackage{etoolbox} +\patchcmd{\chapter}{\thispagestyle{plain}}{\thispagestyle{fancy}}{}{} + +\usepackage{fancyhdr} +\pagestyle{fancy} +\fancyhf{} +\fancyfoot[R]{\thepage} +\renewcommand{\headrulewidth}{0pt} +\renewcommand{\footrulewidth}{0pt} + +\usepackage{ucs} +\usepackage{amssymb} +\usepackage{amsthm} +\usepackage[english]{babel} +\usepackage[references]{agda} +\usepackage{unicode-math} +\usepackage[hidelinks,colorlinks=false]{hyperref} +\usepackage[titletoc,title]{appendix} +\usepackage[nottoc]{tocbibind} +\usepackage{makeidx} +\usepackage{setspace} +\usepackage{authblk} +\usepackage{titlepic} +\usepackage{float} +\usepackage{textgreek} +\usepackage{tabularx} + +\floatstyle{ruled} +\newfloat{program}{thp}{lop} +\floatname{program}{Program} +\newtheorem{theorem}{Theorem}[section] +\newtheorem{corollary}{Corollary}[theorem] +\newtheorem{lemma}[theorem]{Lemma} +% set font +\setmainfont{XITS} +\setmathfont{XITS Math} +\setsansfont[Scale=MatchLowercase]{DejaVuSansMono.ttf} + +\newcommand{\jkeyw}[1]{\texttt{\bfseries #1}} +\newcommand{\jol}[1]{\texttt{#1}} + +\begin{document} +\begin{titlepage} +\begin{table}[] + \centering + \begin{tabular}{rcl} + Автономная некоммерческая & + \multirow{4}{*}{\includegraphics[width=40mm]{image/logo.eps}} + & Autonomous noncommercial \\ + организация высшего & & organization of higher \\ + образования & & education \\ + «Университет Иннополис» & + & «Innopolis University» \\ + \hline + \hline + \end{tabular} + \label{tab:my_label} +\end{table} +\vline +\vspace{5mm} + +\begin{center} +\textbf{ +ВЫПУСКНАЯ КВАЛИФИКАЦИОННАЯ РАБОТА \\ +ПО НАПРАВЛЕНИЮ ПОДГОТОВКИ \\ +09.03.01 --- «ИНФОРМАТИКА И ВЫЧИСЛИТЕЛЬНАЯ ТЕХНИКА»} +\vspace{5mm} + +\textbf{GRADUATE THESIS \\ +MAJOR: "COMPUTER SCIENCE"} +\end{center} +\vspace{20mm} + + + \begin{tabular}{ll +|>{\columncolor[gray]{.8}}l|} +\cline{3-3} +\textbf{Тема:} & + \makebox[0.5mm] & + \makebox[135mm][l]{Верифицированный тайпчекер для языка программирования + } \\ + && Jolie\\ + && \\ + && \\ +\cline{3-3} + \end{tabular} +\vspace{5mm} + + \begin{tabular}{ll +|>{\columncolor[gray]{.8}}l|} +\cline{3-3} +\textbf{Topic:} & + & + \makebox[135mm][l]{Verified type checker for Jolie programming language} \\ + &&\\ + && \\ + && \\ +\cline{3-3} + \end{tabular} +\vspace{5mm} + + + \begin{tabular}{ll +|>{\columncolor[gray]{.8}}l|l +|>{\columncolor[gray]{.8}}l|} +\cline{3-3} \cline{5-5} +Работу выполнил / & + \makebox[0.5mm] & + \makebox[66mm][l]{Акентьев Евгений Андреевич /} & + & \\ +Thesis is executed by & + \makebox[0.5mm] & + \makebox[66mm][l]{Akentev Evgenii Andreevich} & + & + \makebox[40mm]{\textcolor[gray]{.6}{подпись / signature}} \\ +\cline{3-3} \cline{5-5} \\ + \end{tabular} +\vspace{5mm} + + \begin{tabular}{ll +|>{\columncolor[gray]{.8}}l|l +|>{\columncolor[gray]{.8}}l|} +\cline{3-3} \cline{5-5} +Научный руководитель / & + & + \makebox[57mm][l]{Мануэль Маццара /} & + & \\ +Thesis supervisor & + & + \makebox[57mm][l]{Manuel Mazzara} & + & + \makebox[40mm]{\textcolor[gray]{.6}{подпись / signature}} \\ +\cline{3-3} \cline{5-5} \\ + \end{tabular} +\vspace{\fill} + +\begin{center} +Иннополис, Innopolis, 2017 +\end{center} +\end{titlepage} + +\begin{abstract} +Jolie is a service-oriented programming language which comes with the formal specification of its type system ~\cite{nielsen2013type}. However, there is no tool to ensure that programs in Jolie are well-typed. I provide the results of building a part of Jolie syntax, type system and semantics formal model in Agda proof assistant, which are intended for building a verified type checker. +\end{abstract} + +\chapter*{Acknowledgements} + +I would like to thank Manuel Mazzara, Alexander Tchitchigin and Larisa Safina for their help in writing this thesis. + +\tableofcontents +\thispagestyle{empty} + +\newpage + +\if{False} +\begin{code} +-- Imports +open import Syntax +open import Typesystem +open import Typingrules +open import Semantics +open import Theorems +\end{code} +\fi + +\chapter{Introduction} + +Microservices architecture is a modern paradigm in software development using a composition of autonomous entities for creating systems~\cite{DBLP:journals/corr/DragoniGLMMMS16}. +It has been developed as the answer to the problems arisen in applications built in monolithic or Service-Oriented Architecture styles including difficulties with scalability, complexity and dependencies of the evolving application. Microservices implement only a limited and cohesive functionalities, run their own processes, and use lightweight communication mechanisms. + +In the fast-growing landscape of microservices, Jolie~\cite{montesi2010jolie} appears to be a good candidate to play the role of a paradigmatic programming language~\cite{MGZ14}. +Since every program in Jolie is a microservice, everything can be reused or recomposed for obtaining new microservices easing the creation of simple services as well as complex architectural compositions. This may help to scale programs easily, thus supports distributed architecture with the simple managing of components, reducing maintenance and lower development costs. + +However, communication between microservices in Jolie is obtained by means of sending and receiving messages whose type correspondence is checked only at runtime. Having a formalized type system of programming language gives an opportunity to implement type checking mechanism and use it before the runtime. Also, such a formalized type system can serve a ground for experiments. + +The idea of this work is to augment Jolie with a static type-checking mechanism based on type system specification. In ~\cite{nielsen2013type}, Nielsen described the type system of Jolie. She covered the syntax of behavioural, network and service layers and their semantics. Nielsen's work extended the semantic rules at the service layer for receiving a message with a dynamic type check. The described type system is provided with typing rules for the core of programming language (excluding subtyping, recursive types and some other primitives). + +I decided to study the application of type theory as a foundation for the formalization of Jolie. Type theory is a branch of mathematical logic, which operates not only with terms but with their types too. Type theory is a formal language with an explicit set of rules for rewriting strings of symbols, which describe computations. Therefore, type theory may serve as: + +\begin{itemize} + +\item foundations of mathematics + +\item programming language, because of Curry-Howard correspondence~\cite{Sorensen} (type theory should be constructive) + +\item calculus for category theory~\cite{crole1993deriving} + +\end{itemize} + +Therefore, there are different types of type theories. Here are the popular ones: + +\begin{itemize} + +\item Per Martin-L{\"o}f's dependent type theory (intuitionistic type theory)~\cite{lof, nordstrom90} is a version with dependents types which supports constructive mathematics. + +\item Calculus of Constructions~\cite{coquand1988calculus} is a type theory developed by Thierry Coquand and Gerard Huet. It solved some problems of Martin-L{\"o}f's type theory and was used as a basis for Coq~\cite{coq} proof assistant. + +\item Homotopy type theory~\cite{hottwebsite} is an improvement of intensional~\cite{constable2011trimuph} dependent type theory, which started as a homotopy $\lambda$-calculus~\cite{voevodsky2006very}. The main idea is to interpret identity types as path space objects in homotopy theory. + +\end{itemize} + +There are many implementations of type theories. Here are some of them: + +\begin{itemize} +\item + +NuPRL ("new pearl")~\cite{constable1986implementing} is a proof system based on \textit{Computational Type Theory}~\cite{constable2002naive}, extended Martin-L{\"o}f's intuitionistic type theory developed in the 1980s by Robert Lee Constable. It has tactics in the spirit of Edinburgh LCF~\cite{gordon1979edinburgh}. + +\item + +Coq~\cite{coq} is a formal proof system written in OCaml. It's based on Calculus of Inductive Constructions~\cite{pfenning1990inductively, altenkirch1993constructions} and was initiated by Thierry Coquand. There are two inner languages: Gallina and Ltac. Gallina is a purely functional programming language for programs, specifications and proofs. Ltac is a tactical language for building and searching proofs and can be used interactively. + +\item + +Agda~\cite{agda, bove} is a dependently typed functional programming language written in Haskell. It has many features of modern functional programming languages such as inductive families (data types which depend on values), Unicode characters, parametrised modules, mixfix operators. Also, Agda is a proof assistant, because it's based on Martin-L{\"o}f's intuitionistic type theory. + + +\item + +Lean~\cite{de2015lean} is a new open source theorem prover written in C++ being developed at Microsoft Research and Carnegie Mellon University. Lean's kernel is based on dependent type theory with configuration options. It depends on impredicative sort \textbf{Prop}. With that sort, kernel provides a version of the Calculus of Inductive Constructions and a version Martin-L{\"o}f's type theory without \textbf{Prop}. +\item + +RedPRL~\cite{redprl} is a currently in work proof assistant for Computational Cubical Type Theory~\cite{cohen2016cubical} being developed Jon Sterling inspired by NuPRL. It uses a multi-sorted version of abstract binding trees and a dependent version of LCF apparatus. + +\end{itemize} + +Proof assistants and proof systems are becoming more popular in various spheres of software engineering. Usually, there are applied in critical spheres such as medicine, avionics and transport, where the correctness of a program is very important. + +One of such spheres is programming languages. The compilers, virtual machines and interpreters should have no bugs, since they are used by a lot of people who are making their programs for different purposes. Here are the examples of such projects: + +\begin{itemize} + +\item + +CompCert~\cite{Leroy} is a formally verified optimizing ISO C 99 compiler. The main idea behind this project is compiling safety-critical and mission-critical software written in C and meeting high levels of assurance. It supports generating machine code for ARM, PowerPC, and x86 architectures. + +\item +CakeML~\cite{Kumar:2014:CVI:2578855.2535841} is the verified implementation of the subset of Standard ML~\cite{milner1997definition}. It has a proven-correct compiler and runtime system. CakeML supports different architectures such as x86-64, ARM, MIPS, and RISC-V. + +\item +Vellvm (\textit{verified LLVM})~\cite{zhao2012formalizing} is a framework mechanized formal semantics of LLVM’s intermediate representation, type system, and properties of SSA form. Vellvm is built using the Coq theorem prover. + +\end{itemize} + +I decided to use Agda ~\cite{bove,agda} as a proof assistant because it's comfortable and rich functional programming language with allows to extract programs into Haskell. Therefore, it's possible to create a type checker as a command line utility in the future. + +The structure of this thesis is as follows: +chapter 2 describes the syntax of behavioural, service and network layers of Jolie. In chapter 3 I present the type system with typing rules. Chapter 4 is about the semantics of behavioural layer, which is necessary for type checking process. Chapter 5 contains proof of the "Structural Congruence for Behaviours" lemma and particular cases of the theorem about type preserving of the behavioural layer. +Finally, in the last chapter, I conclude and describe the possible directions of future work. + +This thesis is written in Literate Agda~\cite{literateagda}. The whole formalization is available at~\cite{jolierepo}. + +\include{Syntax} + +\include{Typesystem} + +\include{Semantics} + +\include{Theorems} + +\chapter{Conclusions and Future Work}\label{sec:concl} + +In this thesis, I presented the approach in creating a formal model of Jolie programming language which is currently dynamically type-checked. I developed the formalization for the subset of Jolie by means of Agda proof assistant. I expressed Jolie's syntax, type system, typing rules and semantics of behaviour layer in order to be able to build a static type checker to check the type correspondence of messages which are used for interaction of microservices in Jolie. I have provided the proof of structural congruence lemma and particular cases of type preservation property for behaviours. During this project, there were discovered several problems in the original work~\cite{nielsen2013type}. + +Standard quality attributes are not very suitable for the evaluation of this project. For example, the performance of the current implementation is not a good metric, because there are almost no computations. Mostly, the program is a bunch of declarations of data types, except the types where lists are used. One of such types is a type that expresses the presence of an element in the list. Another such example is a security attribute, which can't be applied to this work. The results of this project are also reusable. For example, the implemented data types for the syntax may be used in writing a verified parser for Jolie. Also, since this project is written in Agda, which has a backend for the Haskell, the code can be used from Haskell. The correctness attribute means that the current implementation should be correct with respect to the specification ~\cite{nielsen2013type}. Since some of the properties were omitted to simplify the implementation, it does not fully correspond to the specification, but it may be fixed and extended in the future work. + +The current implementation covers only a small subset of Jolie and has limitations. The provided implementation of expressions is synthetic and not complete. Also, the typing rule for expressions should check that the given expression is well typed with respect to its environment. There is a need in full support of variables as trees and therefore the support of subtyping in the type system. The current typing rule for parallel behaviour lacks the check of that the resulting environments are disjoint. Also, there is a need to replace the stub with a normal mechanism for working with states. +Another important direction leads to the complete formalization of the service and network levels of Jolie. By accomplishing this, it would be possible to build the type checker to type-check Jolie program thoroughly, which may even lead to implementing of a verifiable compiler for Jolie similar to~\cite{Neis,Leroy}. + +\bibliographystyle{unsrt} +\bibliography{thesis} + +\end{document} -- 2.50.1