--- a/Paper/Paper.thy Mon Mar 29 18:12:54 2010 +0200
+++ b/Paper/Paper.thy Mon Mar 29 22:26:19 2010 +0200
@@ -394,10 +394,9 @@
\caption{The term-language of System @{text "F\<^isub>C"}
\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
version of the term-language we made a modification by separating the
- grammars for type and coercion kinds, as well as types and coercion
- types. For this paper the interesting term-constructor is @{text "\<CASE>"}
- involving the binding of multiple type-, coercion- and term-variables from
- patterns.\label{corehas}}
+ grammars for type and coercion kinds, as well as for types and coercion
+ types. For this paper the interesting term-constructor is @{text "\<CASE>"},
+ which binds multiple type-, coercion- and term-variables.\label{corehas}}
\end{figure}
*}
@@ -431,7 +430,7 @@
and the inverse permutation of @{term p} as @{text "- p"}. The permutation
operation is defined by induction over the type-hierarchy, for example as follows
for products, lists, sets, functions and booleans (see \cite{HuffmanUrban10}):
-
+ %
\begin{equation}
\mbox{\begin{tabular}{@ {}cc@ {}}
\begin{tabular}{@ {}l@ {}}
@@ -1145,6 +1144,76 @@
section {* Examples *}
+text {*
+
+ \begin{figure}
+ \begin{boxedminipage}{\linewidth}
+ \small
+ \begin{tabular}{l}
+ \isacommand{atom\_decl}~@{text "var"}\\
+ \isacommand{atom\_decl}~@{text "cvar"}\\
+ \isacommand{atom\_decl}~@{text "tvar"}\\[1mm]
+ \isacommand{nominal\_datatype}~@{text "tkind ="}\\
+ \phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
+ \isacommand{and}~@{text "ckind ="}\\
+ \phantom{$|$}~@{text "CKSim ty ty"}\\
+ \isacommand{and}~@{text "ty ="}\\
+ \phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
+ $|$~@{text "TFun string ty_list"}~%
+ $|$~@{text "TAll tv::tvar tkind ty::ty"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
+ $|$~@{text "TArr ckind ty"}\\
+ \isacommand{and}~@{text "ty_lst ="}\\
+ \phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
+ \isacommand{and}~@{text "cty ="}\\
+ \phantom{$|$}~@{text "CVar cvar"}~%
+ $|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
+ $|$~@{text "CAll cv::cvar ckind cty::cty"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\
+ $|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
+ $|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
+ $|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
+ \isacommand{and}~@{text "co_lst ="}\\
+ \phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
+ \isacommand{and}~@{text "trm ="}\\
+ \phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
+ $|$~@{text "LAM_ty tv::tvar tkind t::trm"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
+ $|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
+ $|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
+ $|$~@{text "Lam v::var ty t::trm"} \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
+ $|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~{text x}~\isacommand{in}~{text t}\\
+ $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
+ \isacommand{and}~@{text "assoc_lst ="}\\
+ \phantom{$|$}~@{text ANil}~%
+ $|$~@{text "ACons p::pat t::trm assoc_lst"} \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
+ \isacommand{and}~@{text "pat ="}\\
+ \phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
+ \isacommand{and}~@{text "vt_lst ="}\\
+ \phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
+ \isacommand{and}~@{text "tvtk_lst ="}\\
+ \phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
+ \isacommand{and}~@{text "tvck_lst ="}\\
+ \phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
+ \isacommand{binder}\\
+ @{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
+ @{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+ @{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
+ @{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
+ \isacommand{where}\\
+ \phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
+ $|$~@{text "bv1 VTNil = []"}\\
+ $|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
+ $|$~@{text "bv2 TVTKNil = []"}\\
+ $|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
+ $|$~@{text "bv3 TVCKNil = []"}\\
+ $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
+ \end{tabular}
+ \end{boxedminipage}
+ \caption{\label{nominalcorehas}}
+ \end{figure}
+*}
+
+
+
+
section {* Adequacy *}
section {* Related Work *}
@@ -1181,7 +1250,9 @@
many discussions about Nominal Isabelle. We thank Peter Sewell for
making the informal notes \cite{SewellBestiary} available to us and
also for patiently explaining some of the finer points about the abstract
- definitions and about the implementation of the Ott-tool.
+ definitions and about the implementation of the Ott-tool. We
+ also thank Stephanie Weirich for suggesting to separate the subgrammars
+ of kinds and types in our Core-Haskell example.
Lookup: Merlin paper by James Cheney; Mark Shinwell PhD