generation.tex

%\chapter{The Generator}
\Chapter{The Generator }{Graph theories to generated constructions}
\label{ch:generation}

The flattener compiles theory expressions into a graph of flat theories and morphisms between them. The generator uses the flat theories and manipulate them in order to generate some constructions that are useful when working with algebraic structures. The algorithms used to generate these constructions correspond to how universal algebra defines the constructions.

In Section~\ref{sec:genFrameReqs}, we discuss the requirements of a generation framework that is capable of generating these constructions. In Section~\ref{sec:togFamework}, we present how we have handled those requirements using Tog as the object language. We discuss the generation of the constructions in Section~\ref{sec:generatedConstructions}. We further discuss our approach in Section~\ref{sec:generation:discussion}. 

\section{Generation Framework}
\label{sec:genFrameReqs}

Generating information based on the content of a theory requires dealing with theories as data, and therefore working at the meta-level. Meta programming frameworks differ in their capabilities. We lay out here some basic operations that are required to manipulate theories based on universal algebra definitions.  Section~\ref{sec:gen:reqs:eqtheories} discusses how theories are preprocessed so information can be generated from them. The requirements needed to generate this information are presented in details in Section~\ref{sec:gen:reqs:constructions} and summarized in Section~\ref{sec:gen:reqs:summary}. 

%In Section~\ref{sec:gen:eqtheories}, we discuss how the output theories of the flattener are presented as The constructions we generate are either record types (signature, products, homomorphisms, relational interpretations), inductive datatypes (term languages), or functions (simplifiers and evaluators of term languages). We discuss the requirements for generating each of these constructions. 

\subsection{Equational Theories}
\label{sec:gen:reqs:eqtheories}
Theories of the graph are instances of \lstmath{GTheory} type; see Section~\ref{subsec:theoriesMorphisms}, which is a representation of telescopes as in Equation~\ref{eq:telescope}. In this representation, declarations of a theory are represented as members of the  \lstmath{[Constr]} type, where each \lstmath{Constr} has a name and an expression denoting its type. 
Universal algbera has a different representation of theories, which is discussed in Section~\ref{sec:eqtheory}. It separates declarations that describe sorts, functions symbols, and axioms. The first requirement to be able to process theories based on universal algebra definitions is to be able to classify theory declarations into these three groups. 

\subsection{Constructions}
\label{sec:gen:reqs:constructions}
After presenting a theory as described by universal algebra, it can be used to generate the constructions we present in Section~\ref{sec:toBeGenerated} and possibly more. We implemented the generation of signatures, product theories, homomorphisms, relational interpretations, and term languages as well as some functions to operate on them. We discuss the requirements of generating each of them in the sequel of this section, where constructions with similar requirements are discussed together.  
%We group similar constructions and discuss them together  

\subsubsection{Signatures and Product Theories}
Figure~\ref{fig:monoid-sig-prod} shows how the theory presentation of \lstmath{Monoid} can be manipulated to generate signature and product theories. When computing the signature of a theory, one only needs to drop the axioms. Product theories are obtained by replacing every occurrence of the sort \lstmath{A} with the sort \lstmath{Prod A A}. To generate them we need to be able to alter the definitions in a theory, by dropping and by substitution. 

\begin{figure}
\input{figures/monoid-sig-prod.tex}
\caption{Manipulating \lstinline|Monoid| theory presentation to generate its signature and product theories.}
\label{fig:monoid-sig-prod}
\end{figure}

\subsubsection{Homomorphisms and Relational Interpretations}
\begin{figure}
\input{figures/monoid-hom-rel.tex}
\caption{Manipulating the \lstinline|Monoid| theory presentation to generate its homomorphism.}
\label{fig:monoid-hom-rel}
\end{figure}

Homomorphisms are structure-preserving mappings between the carriers of two algebras. Relational interpretations are structure-preserving relations between them. Figure~\ref{fig:monoid-hom-rel} shows how components of the definitions of \lstmath{Monoid} are used to generate its corresponding homomorphism theory. To generate them we need the following: 
\begin{itemize}
\item A representation of $2$ instances of a theory with the necessary bindings to define these instances.  
\item A function/relation between elements of the carriers of the two instances. 
\item Preservation axioms for every function symbol. To generate these axioms, we need the following:  
    \begin{itemize}
    \item Projection fields of the instances. The names of these projections are qualified if they are fields within a record. Otherwise, they are unqualified.   
    \item Given a function symbol of the theory, with information about its name and type, a representation of function application of that symbol.  
    \end{itemize}
\end{itemize}

\subsubsection{Term Languages}
Some of the constructions we generate for a theory are term languages. 
We differentiate between $4$ different forms of term languages that differ in their expressive power, as shown in Figure~\ref{fig:term-lang-4-forms}. 
\begin{figure}
    \input{figures/term-lang-4-forms.tex}
    \caption{The term language of \lstmath{Monoid} expressed in $4$ different ways.}
    \label{fig:term-lang-4-forms}
\end{figure}

The \lstmath{Basic} term language defines expressions created using the function symbols of the theory. At this level of abstraction, referring to elements of the carrier is not possible.
Considering, for example, the binary operation of the basic \lstmath{Monoid} term language in Figure~\ref{fig:term-lang-4-forms}, \lstmath{op}. Its arguments are either the constant \lstmath{e} or another call for \lstmath{op}. 
\lstmath{Closed} term languages solve this problem by providing the \lstmath{sing} constructor, abbreviation for \emph{singleton}, that lifts an element of type \lstmath{A} to an instance of the closed term language. Assuming that the carrier is the type of natural numbers \lstmath{Nat}, a possible term in the language would be \lstmath{op (sing (suc zero)) e}. 

\lstmath{Open} term languages provides extra constructor to represent variables, represented using the \lstmath{Fin} type of finite sets, which depends on a number \lstmath{n : Nat} representing the size of the set of variables. This representation has the advantage that one can easily add fresh variables by incrementing \lstmath{n}. 
The two open term languages are shown on the right hand side of Figure~\ref{fig:term-lang-4-forms}.  

For all 4 versions, we need to generate a constructor for every function symbol of the theory. The term languages that support referring to elements of the carrier would have an extra constructor for singleton elements with arguments of type \lstmath{A}; and those that support language with variables would have an extra constructor whose arguments has the type \lstmath{Fin n}. 

The requirements for generating these term languages is: 
\begin{itemize}
\item A representation for inductive types and constructors.  
\item A representation of types for natural numbers~\lstmath{Nat}, finite sets~\lstmath{Fin}, and vectors~\lstmath{Vec}. 
\end{itemize}

\subsubsection{Functions on Term Languages}
\label{sec:gen:reqs:funcs}
After generating the term languages, we generate functions that manipulate them. These functions are simplifier, evaluator, induction principle, staged term languages, and staging using representation type that abstracts over the stage. Generating these functions requires the following: 
\begin{itemize}
\item Pattern matching on the constructors of the term language.  
\item Constructing recursive calls on the arguments of the pattern. 
\end{itemize} 

\subsection{Requirements}
\label{sec:gen:reqs:summary}
We summarize the different points presented in this section as requirements for the generation framework: 
\begin{enumerate}
\item A representation of equational theories.  
\item A mechanism to manipulate the declarations in a theory, by dropping and by substitution. 
\item A representation of instances of a theory. 
\item A mechanism to project fields of the instances. 
\item A function/relation between elements of the carriers of the two instances. 
\item A representation of function application of this field.  
\item Computing patterns and recursive calls of a function declaration. 
\item Creating inductive types and their constructors. 
\item A representation of natural numbers, finite sets and vector types.    
\end{enumerate}

  

%The resulting flat theories are then used by the generator to produce some useful tools (constructions) related to them. In this chapter, we introduce the generator and answer the first and second research questions asked in Section~\ref{sec:questions}.

%The graph contains theories represented as telescopes as described in Section~\ref{sec:background:theory}. This representation is different than the one for equational theories used in universal algebra and defined in Section~\ref{sec:eqtheory}. The first step we need here is to represent the dependently-typed telescopes as equational theories highlighting their three components: sorts, function symbols, and axioms. Then, we can manipulate the theories to generate the definitions of their related constructions, like homomorphisms, term algebras and other summarized in Section~\ref{sec:toBeGenerated}. 

%flat theory presentations in DTT. We know that those theories describe algebraic structures and therefore they can be represented in unisorted equational logic as described by universal algebra. In Chapter~\ref{ch:ualgebra} we introduced theories and their related constructions in universal algebra. Here we discuss our framework that uses this knowledge to generate information from theory presentations. We use the Haskell type \lstmath{EqTheory} to describe the structure of equational theories. Because this type is built using the tog abstract syntax, manipulating it is more or less manipulating tog syntax. The output of the generator is guaranteed to be well-formed. The tog type checker is run on this input to check for well-typedness. 

%There are some commonalities in how the generation of constructions manipulate the tog syntax. We provide functions that perform these common tasks. The functions that compute the constructions uses them. This leads to a three-layer hierarchy as in Figure~\ref{fig:generator_hierarch}.  

\begin{comment}
\begin{figure}
\centering{
\includegraphics[scale=0.35]{figures/genetaor_hierarch.png}}
\caption{Three layered hierarchy of the generator.}
\label{fig:generator_hierarch}
\end{figure}
\end{comment}
%In Section~\ref{sec:toBeGenerated} we introduce a list of operations that can be generated from flattened theory presentations. 
%The infrastructure layer in introduced in Section~\ref{sec:togFamework}.
% we introduce the functions that provides the basic manipulation. 
%Any meta-programming environment that provides these facilities should be able to generate the constructions that we generate here. We discuss the generation algorithms in Section~\ref{sec:generatedConstructions}. 

\section{Tog Infrastructure}
\label{sec:togFamework}

The generative framework we present here uses Haskell as a meta language to generate construction in Tog, the object language.  
%Generating these constructions is done by writing programs in the meta language (Haskell) that generates constructions in the object language (Tog). 
We mainly manipulate the types in Figure~\ref{fig:togRepr}. In this Section we discuss how we implement the requirements that we laid out in the previous section. 
 
%With so many constructions to be generated, we provide functions that implements common operations needed to generate them. The meta-theory that governs our generation algorithms is universal algebra. 
%In order to be able to manipulate While we use Tog for generating the constructions, a framework with reflections mechanism that has --- at least --- the following abilities would still be able to generate this knowledge: 

We create a type \lstmath{EqTheory} to describe first order equational theories as in Chapter~\ref{ch:ualgebra}. In Secion~\ref{subsec:generation:eqTheories} we describe this type, our definition of an instance of a theory, and how we project fields of an instance. This Section covers requirements 1, 3, and 4. Note that requirement 2 for substitutions is done using the \lstmath{gmap} function built for the \lstmath{rename} combinator as explained in Section~\ref{subsec:combinatorsImpl}. 

In Section~\ref{subsec:generation:functions} we describe how we implement requirements 5, 6 and 7, which are related to function definitions and applications. Requirements 8 and 9 are discussed in Sections~\ref{subsec:generation:datatypes} and~\ref{subsec:generation:prelude}.   
%Functions and datatypes are some of the building blocks of the constructions we generate. We provide utility functions for manipulating them in Sections~\ref{subsec:generation:functions} and~\ref{subsec:generation:datatypes}, resepectively.   
 
%Another important operation that we use in the generator is renaming, which we discuss in Section~\ref{subsec:generation:renaming}. 
%Some of the definitions we generate may depend on definitions of standard operations, like looking up a value in a vector. We discuss how to add definitions to a prelude in Section~\ref{subsec:generation:prelude}. 

%As we discussed in Chapter~\ref{ch:tog}, Tog provides us with the internal representations of dependent records, which we use to represent theories. We extend the Tog implementation to generate algebraic constructions by providing metaprograms that operate on Tog internal representation of dependent records. In this section we discuss some of the basic utiities that we use in the generation algorithms. 

\subsection{Equational Theories}
\label{subsec:generation:eqTheories}
An equational theory in universal algebra abstracts over theory presentations of algebraic structures and consists of a sort, a list of function symbols and a list of axioms, as discussed in Section~\ref{sec:background:theory}. We capture this definition of equational theories by the type \lstmath{EqTheory}. 
\begin{hscode}
data EqTheory = EqTheory {
  _thyName    :: Name_  ,   -- the name of the theory 
  _sort       :: Constr ,   -- the sort of the theory 
  _funcTypes  :: [Constr],  -- the set of function symbols 
  _axioms     :: [Constr],  -- the set of axioms 
  _waist      :: Int }      -- the number of parameters 
\end{hscode}
The \lstmath{waist} is used in the same way as in \lstmath{GTheory} from Section~\ref{sec:impl:expressions}. 

%The input to the generator is a list of tog dependent records representing the flattened theories described by the combinators as presented in the previous chapter. The first step the generator needs to do is to cast them into instances of \lstmath{EqTheory}, i.e. deal with a DTT context as an equational logic theory. 
\begin{comment}
This is done using the function \lstmath{recordToEqTheory}. 
\begin{hscode}
recordToEqTheory :: TRecord -> Eq.EqTheory
recordToEqTheory record@(TRecord nm params _) =
  Eq.build (nm^.name) 
    (getRecordSort record)
    (getRecordComps isFunc record)
    (getRecordComps isAxiom record)
    (paramsNum params)
\end{hscode}
In Tog, records definitions are declared using the \lstmath{Record} constructor of the type \lstmath{Decl}, which contains many other constructors used to define functions, types, and others. We prefer to use a type dedicated to records, and therefore use the \lstmath{TRecord} type instead. \lstmath{TRecord} has the exact same parameters as the \lstmath{Record} constructor. 
\end{comment}

\subsubsection*{Instances of Theories}
\label{sec:instances_theories}
We define a representation of an instance in terms of its name, the bindings that constitute its parameters and the expression representing the type of this instance. 
\begin{hscode}
type EqInstance = (Name_,[Binding],Expr) 
\end{hscode}
\noindent For example, an instance \lstmath{m : Monoid A} would be represented as: 
\begin{lstlisting} 
         (m,[A : Set], Monoid A)
\end{lstlisting} 

Instances are computed by the function \lstmath{eqInstance}, where the second argument is used to index the instance in cases where more than one is needed. In this case, both the name of the instances and the names of the bindings are indexed using the input number. 
\begin{hscode} 
eqInstance :: EqTheory -> Maybe Int -> EqInstance 
eqInstance thry indx =
  let iname i = twoCharName (thry ^. thyName) i 
      binds i =
        let bs = map fldsToHiddenBinds (args thry)
        in if i == 0 then bs else indexBindings i bs
      expr i =
        let bnames = getBindingsNames (binds i)
        in App ~$\$$~ mkArg (thry ^. thyName) : map mkArg bnames
   in case indx of
    Nothing -> (iname 0, binds 0, expr 0)
    Just i  -> (iname i, binds i, expr i)
\end{hscode}
\noindent The value of \lstmath{expr} denotes the type of the instance by applying the name of the theory to the bindings. 

% ======================= 
\subsubsection*{Projecting Fields}
Based on whether a declaration of a theory components is a parameter or a field, referring to it will be different. For an instance \lstmath{m : Monoid A} of a \lstmath{Monoid} theory that has the carrier as the only parameter, one would refer to the carrier with its name \lstmath{A}, but would refer to the constant \lstmath{e} of theory as \lstmath{m.e}. 
We provide the function \lstmath{projectConstr} to compute the projection of one of the declarations of a theory. 
\begin{hscode} 
projectConstr :: EqTheory -> EqInstance -> Constr -> Expr 
projectConstr thry (instName,binds,_) c@(Constr n _)  =
  if isArg thry c then App [mkArg ~$\$$~ findInBindings binds c]
  else App [mkArg (n ^. name),mkArg instName]
\end{hscode}  
\noindent Checking whether the declaration is a an argument or a field is done by the function \lstmath{isArg} that checks for the \lstmath{waist} of the \lstmath{EqTheory}. 

A variant of \lstmath{projConstr} is the function \lstmath{applyProjConstr} projects the declaration and applies it to variables based on its arity. Its return type is \lstmath{([Binding],Expr)} where \lstmath{[Binding]} represents the variables to which the declaration is applied  

%The input to this function is the definition of the theory, and in some cases an integer number. This is useful in case many instances of the theory are needed, and so they are indexed by number. The instance is represented as a tuple of two components \lstmath{([Binding],Expr)}. The \lstmath{Binding} list is useful when the theory has parameter, i.e.: \lstmath{waist > 0}. In this case the  bindings are the arguments to the theory instance. The \lstmath{Expr} corresponds to the instance expression of the theory. The instance expression is represented using the constructor \lstmath{App [Expr]}, where the first element of the list is the constructor. If there are any arguments, they follow after it. 

\subsection{Functions}
\label{subsec:generation:functions}
%Most of the constructions we generate manipulates function symbols of an \lstmath{EqTheory}.  
A function symbol has the type \lstmath{Constr} which consists of its name and an expression describing its type. We use the type \lstmath{FApp} to describe the application of this function symbol to some variables.
\begin{hscode}
type FType = Constr
type FApp = ([Binding],Expr)
\end{hscode}
\noindent The \lstmath{[Binding]} in \lstmath{FApp} refers to the variables the function is being applied to. 

A function application is generated by \lstmath{fapp}. The types of all the bindings is set to be the sort of the theory. The expression is the name of the constr applied to its arguments 
\begin{hscode} 
fapp :: FType -> FApp
fapp (Constr n typ) =
 let nm = n ^. name
     arity = farity typ
     vars = genVars arity
 in if (arity == 0) then ([],App [mkArg nm])
    else ([HBind (map mkArg vars) (etyp typ)],
          App ~$\$$~ mkArg nm : map mkArg vars) 
\end{hscode} 
\noindent The arguments of the functions are generated using the \lstmath{genVars} function and are used to create the bindings and the function application expression. %\lstmath{vars} is the list of variables generated according to the arity of the function symbol. Their types are determined based on the type of any of the arguments of the function. As we work in a unisorted environment, we don't need to check the types of all function arguments. 

When generating functions that manipulate the terms of the theory, like simplifiers and evaluators, one need to pattern match on the function symbols. One common operation on functions is pattern matching. We define the type class \lstmath{MkPattern} and its two instances for \lstmath{FType} and \lstmath{Expr}. 
\begin{hscode}
class MkPattern a where
  mkPattern :: a -> Pattern
\end{hscode} 
The pattern depends on the arity of the function symbol, and is generally the application of the name of the function symbol to its parameters. 
\begin{hscode} 
 if (arity == 0)
 then IdP ~$\$$~ mkQName nm 
 else ConP (mkQName nm) ~$\$$~ map (IdP . mkQName) vars 
\end{hscode} 

The functions \lstmath{functor} and \lstmath{functor'} support applying a functor to an expression, be it the name of a function symbol or a more complex expressions.

\subsection{Datatypes}
\label{subsec:generation:datatypes}
Some of the constructions that can be generated from theory presentations are represented as datatypes, like term languages. A datatype in Tog has the type \lstmath{Decl}. The type \lstmath{DTInst} captures the instances of a datatype in the same way as \lstmath{EqInstance}.
Similar to functions, we deal with datatypes in two different forms, definitions and instances. 
\begin{hscode}
type DTDef = Decl
type DTInstance = (Name_,[Binding],Expr) 
\end{hscode}
\noindent Instances are computed by the function \lstmath{tinstance}. The bindings are computed based on the parameters of the datatype. The expression denoting the type of the instance is computed by applying the name of the datatype to the bindings used the \lstmath{App} constructor. 

\begin{comment}
%\subsection{Renaming}
\label{subsec:generation:renaming}
In multiple positions what we do is substitution, i.e. traverse the datatype and replace the occurence of one variable with another. 

%\subsection{Bindings}
\label{subsec:generation:bindings}
Bindings are pervasive in definitions and are so important to deal with. We provide several utility functions for indexing bindings, repeating them, and other basic operations. 
The most interesting of all is the case when the bindings of two different entities need to be combined together, like in the case when both entities are arguments to a function.\ednote{Q: Is there literature on this?}  
\ednote{Q: How useful is the bindings section? Should I keep it?}
\end{comment}

\subsection{Prelude Definitions}
\label{subsec:generation:prelude}
The constructions that we defined here depends on some definitions that act as the prelude of the library. We define these as literals: 
\begin{hscode}
nat :: [String]
nat =
  ("data Nat : Set where { " ++ 
     "zero : Nat ;" ++ 
     "suc  : Nat -> Nat }") : []
\end{hscode}
\noindent These strings are parsed by the function \lstmath{parseDecl}, which turns it to a Tog definition of type \lstmath{Decl}. 

%In order to develop a meta program that generates the constructions above, and possible more, we need a way to manipulate theory presentations, i.e. a program that given a theory presentation would generate theories, types, and functions representing the constructions above. Therefore, the program 
%equality, substitution, .. 

\section{Constructions For Free!}
\label{sec:generatedConstructions}
By providing the appropriate tools to operate over the internal syntax of Tog, we are ready to generate the universal algebra constructions related to equational theory presentations. In the following sections we describe the generation of these constructions. 

\subsection{Signature}
Signatures represent the language of the theory, without any properties governing them. It is common in mathematics to talk about algebras over some signature. Signatures are obtained from theory presentations by dropping axioms. In Tog, the process of generating the signature is done in $3$ steps via the \lstmath{signature_} function. 
\begin{hscode}
signature_ :: Eq.EqTheory -> Eq.EqTheory
signature_ = set Eq.thyName ("Sig") . set Eq.axioms [] .  gmap ren
\end{hscode}
\noindent The function \lstmath{ren :: Name -> Name} renames the fields of a theory by adding a suffix \lstmath{"S"}. This is needed because the Tog scope checker would not accept overloaded names of fields within the same module. In case the code is exported into a system that supports this kind of overloading, the suffix can be removed. Note that this rename will be needed when generating any new construction. \lstmath{gmap} function traverses the \lstmath{EqTheory} applying \lstmath{ren} whenever a \lstmath{Name} type is encountered.  
The \lstmath{Eq.axioms} list is set to be empty, dropping the axioms of the theory. 

\subsection{Product Algebra} 
Product algebras group together algebras of the same theories. 
The type \lstmath{Prod} lifts a type \lstmath{A} to a type \lstmath{Prod A A}, where \lstmath{Prod} is standard product type. 
The lifting of the type \lstmath{A} is done via substitution of every \lstmath{A} with \lstmath{Prod A A}. 
The function \lstmath{productThry} uses this type to compute the product theory 
\begin{hscode}
productThry :: Eq.EqTheory -> Eq.EqTheory
productThry t =
 let sortName = getConstrName (t ^. Eq.sort)  
 in set Eq.thyName ("Product") ~$\$$~     
    gmap (prodType sortName) ~$\$$~
    gmap (ren sortName) t
\end{hscode}
The \lstmath{prodType} function does the type lifting for the sort as follows: 
\begin{hscode} 
prodType :: Name_ -> Expr -> Expr
prodType sortName (App [a]) =
  if (getArgName a) == sortName 
  then App [mkArg "Prod", a, a] else App [a] 
prodType _ x = x 
\end{hscode} 

\subsection{Homomorphism}
Theories are presented as record declarations in Tog, and so are their homomorphisms. The following function generates the homomorphism declaration: 
\begin{hscode} 
homomorphism :: Eq.EqTheory -> Decl
homomorphism thry =
  let nm = "Hom" 
      i1@(n1,b1,e1) = Eq.eqInstance thry (Just 1) 
      i2@(n2,b2,e2) = Eq.eqInstance thry (Just 2)
      fnc = homFunc thry i1 i2 (thry ^. Eq.sort)
      axioms = map (presAxiom thry i1 i2 fnc) (thry ^. Eq.funcTypes)  
  in Record (mkName nm)
   (mkParams ~$\$$~ b1 ++ b2 ++ 
               map (~$\backslash$~(n,e) -> Bind [mkArg n] e) [(n1,e1),(n2,e2)])
   (RecordDeclDef setType (mkName ~$\$$~ nm ++ "C") 
                  (mkField ~$\$$~ fnc : axioms))
\end{hscode} 
\noindent \lstmath{i1} and {i2} are the two instances of \lstmath{thry} created using \lstmath{eqInstance} as described in the Section~\ref{subsec:generation:eqTheories}. 
Those instances are used to create the parameters of the homomorphisms using the \lstmath{mkParams} function. 

The declarations of the homomorphism record are the homomorphism function and the preservation axioms. The function is generated by \lstmath{homFunc} which uses the function \lstmath{projectConstr}, described in Section~\ref{subsec:generation:eqTheories}, to project the carriers of the two instances. 
\begin{hscode} 
homFunc :: Eq.EqTheory -> Eq.EqInstance -> Eq.EqInstance -> Constr 
homFunc thry i1 i2 =
  let carrier = thry ^. Eq.sort
  in Constr (mkName homFuncName) ~$\$$~
       Fun (Eq.projectConstr thry i1 carrier) 
           (Eq.projectConstr thry i2 carrier) 
\end{hscode}

Equations of the preservation axioms are generated by the \lstmath{equation} function. It uses \lstmath{applyProjConstr}, explained in~\ref{subsec:generation:eqTheories}, which give the expression of function application as well as list of the variables its applied to. 
\begin{hscode} 
(bind1,expr1) = Eq.applyProjConstr thry i1 constr Nothing
    (_,expr2) = Eq.applyProjConstr thry i2 constr Nothing 
\end{hscode} 
\noindent These pieces are used to construct the \lstmath{Pi}-type as follows 
\begin{hscode}
Pi (Tel bind1) ~$\$$~ Eq (lhs homFunc expr1) (rhs homFunc expr2)
\end{hscode} 

\subsection{Relational Interpretation}
\label{sec:generation:relInterp}
A relational interpretation is a structure preserving relation. We discuss it in Section~\ref{sec:background:relInterp}.  
Its implementation looks very similar to that of homomorphism --- a structure preserving function. Some of the similarities are that they are both records and have the same parameters. However the fields are different. Instead of having a function between the two carriers, we have a relation. The function \lstmath{mkInterpType} generates the type of the relation field. It looks very similar to the function \lstmath{homFunc}, except the type is a relation from carriers to the type \lstmath{Set} as follows: 
\begin{hscode} 
Fun (Eq.projectConstr thry i1 carrier) ~$\$$~ 
     Fun (Eq.projectConstr thry i2 carrier) setTypeAsId
\end{hscode} 
Then, we generate the axioms that guarantees preserving structure. For a binary operation, this axiom would look as follows 
\begin{lstlisting} [mathescape]
 interp-op : {x1 x2 : A1} {y1 y2 : A2} $\to$ 
           interp x1 y1 $\to$  interp x2 y2 $\to$ 
           interp (op x1 x2) (op y1 y2)
\end{lstlisting}
\noindent To generate these axioms, we call \lstmath{applyProjConstr} to get the bindings and the function application expression, the same as done in homomorphism generation. Then, we align them into lists of the form \lstmath{[x1,x2,op x1 x2]} and \lstmath{[y1,y2,op y1 y2]}. The elements of the lists are used to create the axioms by applying the relation on the corresponding elements from the two lists 
\begin{hscode} 
 zipWith (\x y -> App [mkArg (interpName^.name),x,y]) args1 args2 
\end{hscode}

\input{term-algebra.tex}

\section{Discussion}
\label{sec:generation:discussion}
%We have introduced many constructions that can be derived from a theory presentation and implemented a framework in which we generate some of them. 
Knowledge representation is a key part of a generation framework. Our representation of \lstmath{EqTheory} follows from the axiomatic representation of algebraic structures as presented in universal algebra. The definitions of \lstmath{FType} and \lstmath{DType} corresponds to the representation of functions and datatype, respectively, in Tog. Less obvious was the representations of instances \lstmath{EqInstance} and \lstmath{DTInstance} and function application. 
Once the knowledge capture and utility functions presented in Section~\ref{sec:togFamework} are in place, generating new constructions becomes a straight forward task. 
%Given a tog dependent record, we have generated multiple constructions; some of which are records, like signatures, products, and homomorphisms, some are datatypes, like the different forms of term langauges, and others are functions, like all the utility functions for term languages. 
%Another interesting problem here is related to dealing with bindings of two different inputs, how to determine if they are the same, different, hidden or explicit. 

Another useful lesson we learn here is about the importance of having a strong and small core language for manipulating structures. Many things were easy to do in Tog because it is a small system. But we also faced difficulties due to the immaturity of some features in Tog.  
For example, the generated definition of induction is not accepted by Tog's type checker if the hidden argument \lstmath{\{p\}} is not passed explicitly. Most feature-rich systems, like Agda and Lean, will not need to have this argument defined. Another needed feature is treating constructors as functions, where they can be passed to higher order functions. Tog does not support that, although many systems do.  

Using this framework we are able to generate a library of $32459$ lines of code from the representation of $227$ theories. Appendix~\ref{appendix:generatedTog} shows the generated definition for \lstmath{Monoid} theory. All the generated files are present on github under~\url{https://github.com/ysharoda/Deriving-Definitions/tree/115462d85389/Library/generated}.