392 \end{center} |
392 \end{center} |
393 \end{boxedminipage} |
393 \end{boxedminipage} |
394 \caption{The term-language of System @{text "F\<^isub>C"} |
394 \caption{The term-language of System @{text "F\<^isub>C"} |
395 \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this |
395 \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this |
396 version of the term-language we made a modification by separating the |
396 version of the term-language we made a modification by separating the |
397 grammars for type and coercion kinds, as well as types and coercion |
397 grammars for type and coercion kinds, as well as for types and coercion |
398 types. For this paper the interesting term-constructor is @{text "\<CASE>"} |
398 types. For this paper the interesting term-constructor is @{text "\<CASE>"}, |
399 involving the binding of multiple type-, coercion- and term-variables from |
399 which binds multiple type-, coercion- and term-variables.\label{corehas}} |
400 patterns.\label{corehas}} |
|
401 \end{figure} |
400 \end{figure} |
402 *} |
401 *} |
403 |
402 |
404 section {* A Short Review of the Nominal Logic Work *} |
403 section {* A Short Review of the Nominal Logic Work *} |
405 |
404 |
429 acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"}, |
428 acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"}, |
430 the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, |
429 the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, |
431 and the inverse permutation of @{term p} as @{text "- p"}. The permutation |
430 and the inverse permutation of @{term p} as @{text "- p"}. The permutation |
432 operation is defined by induction over the type-hierarchy, for example as follows |
431 operation is defined by induction over the type-hierarchy, for example as follows |
433 for products, lists, sets, functions and booleans (see \cite{HuffmanUrban10}): |
432 for products, lists, sets, functions and booleans (see \cite{HuffmanUrban10}): |
434 |
433 % |
435 \begin{equation} |
434 \begin{equation} |
436 \mbox{\begin{tabular}{@ {}cc@ {}} |
435 \mbox{\begin{tabular}{@ {}cc@ {}} |
437 \begin{tabular}{@ {}l@ {}} |
436 \begin{tabular}{@ {}l@ {}} |
438 @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm] |
437 @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm] |
439 @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\ |
438 @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\ |
1143 \end{itemize} |
1142 \end{itemize} |
1144 *} |
1143 *} |
1145 |
1144 |
1146 section {* Examples *} |
1145 section {* Examples *} |
1147 |
1146 |
|
1147 text {* |
|
1148 |
|
1149 \begin{figure} |
|
1150 \begin{boxedminipage}{\linewidth} |
|
1151 \small |
|
1152 \begin{tabular}{l} |
|
1153 \isacommand{atom\_decl}~@{text "var"}\\ |
|
1154 \isacommand{atom\_decl}~@{text "cvar"}\\ |
|
1155 \isacommand{atom\_decl}~@{text "tvar"}\\[1mm] |
|
1156 \isacommand{nominal\_datatype}~@{text "tkind ="}\\ |
|
1157 \phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ |
|
1158 \isacommand{and}~@{text "ckind ="}\\ |
|
1159 \phantom{$|$}~@{text "CKSim ty ty"}\\ |
|
1160 \isacommand{and}~@{text "ty ="}\\ |
|
1161 \phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\ |
|
1162 $|$~@{text "TFun string ty_list"}~% |
|
1163 $|$~@{text "TAll tv::tvar tkind ty::ty"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\ |
|
1164 $|$~@{text "TArr ckind ty"}\\ |
|
1165 \isacommand{and}~@{text "ty_lst ="}\\ |
|
1166 \phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\ |
|
1167 \isacommand{and}~@{text "cty ="}\\ |
|
1168 \phantom{$|$}~@{text "CVar cvar"}~% |
|
1169 $|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\ |
|
1170 $|$~@{text "CAll cv::cvar ckind cty::cty"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\ |
|
1171 $|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\ |
|
1172 $|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\ |
|
1173 $|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\ |
|
1174 \isacommand{and}~@{text "co_lst ="}\\ |
|
1175 \phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\ |
|
1176 \isacommand{and}~@{text "trm ="}\\ |
|
1177 \phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\ |
|
1178 $|$~@{text "LAM_ty tv::tvar tkind t::trm"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\ |
|
1179 $|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\ |
|
1180 $|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\ |
|
1181 $|$~@{text "Lam v::var ty t::trm"} \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\ |
|
1182 $|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~{text x}~\isacommand{in}~{text t}\\ |
|
1183 $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\ |
|
1184 \isacommand{and}~@{text "assoc_lst ="}\\ |
|
1185 \phantom{$|$}~@{text ANil}~% |
|
1186 $|$~@{text "ACons p::pat t::trm assoc_lst"} \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\ |
|
1187 \isacommand{and}~@{text "pat ="}\\ |
|
1188 \phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\ |
|
1189 \isacommand{and}~@{text "vt_lst ="}\\ |
|
1190 \phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\ |
|
1191 \isacommand{and}~@{text "tvtk_lst ="}\\ |
|
1192 \phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\ |
|
1193 \isacommand{and}~@{text "tvck_lst ="}\\ |
|
1194 \phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\ |
|
1195 \isacommand{binder}\\ |
|
1196 @{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~% |
|
1197 @{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\ |
|
1198 @{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~% |
|
1199 @{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\ |
|
1200 \isacommand{where}\\ |
|
1201 \phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\ |
|
1202 $|$~@{text "bv1 VTNil = []"}\\ |
|
1203 $|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\ |
|
1204 $|$~@{text "bv2 TVTKNil = []"}\\ |
|
1205 $|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\ |
|
1206 $|$~@{text "bv3 TVCKNil = []"}\\ |
|
1207 $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\ |
|
1208 \end{tabular} |
|
1209 \end{boxedminipage} |
|
1210 \caption{\label{nominalcorehas}} |
|
1211 \end{figure} |
|
1212 *} |
|
1213 |
|
1214 |
|
1215 |
|
1216 |
1148 section {* Adequacy *} |
1217 section {* Adequacy *} |
1149 |
1218 |
1150 section {* Related Work *} |
1219 section {* Related Work *} |
1151 |
1220 |
1152 text {* |
1221 text {* |
1179 \noindent |
1248 \noindent |
1180 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for |
1249 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for |
1181 many discussions about Nominal Isabelle. We thank Peter Sewell for |
1250 many discussions about Nominal Isabelle. We thank Peter Sewell for |
1182 making the informal notes \cite{SewellBestiary} available to us and |
1251 making the informal notes \cite{SewellBestiary} available to us and |
1183 also for patiently explaining some of the finer points about the abstract |
1252 also for patiently explaining some of the finer points about the abstract |
1184 definitions and about the implementation of the Ott-tool. |
1253 definitions and about the implementation of the Ott-tool. We |
|
1254 also thank Stephanie Weirich for suggesting to separate the subgrammars |
|
1255 of kinds and types in our Core-Haskell example. |
1185 |
1256 |
1186 Lookup: Merlin paper by James Cheney; Mark Shinwell PhD |
1257 Lookup: Merlin paper by James Cheney; Mark Shinwell PhD |
1187 |
1258 |
1188 Future work: distinct list abstraction |
1259 Future work: distinct list abstraction |
1189 |
1260 |