syntax init commit

This commit is contained in:
Quinn Dougherty 2022-03-25 13:50:40 -04:00
parent 11b40b8798
commit 1a77a1fac5
9 changed files with 132 additions and 0 deletions

1
.gitignore vendored
View File

@ -4,3 +4,4 @@ yarn-error.log
.merlin
.parcel-cache
.DS_Store
.auctex-auto

8
syntax/README.md Normal file
View File

@ -0,0 +1,8 @@
# The syntax and semantics of squiggle
We give the syntax in a BNF-like specification
``` sh
nix-build
```
shall dump `squiggle-spec.pdf` in the `result` directory.

30
syntax/default.nix Normal file
View File

@ -0,0 +1,30 @@
{ chan ? "a7ecde854aee5c4c7cd6177f54a99d2c1ff28a31" # 21.11 tag
, pkgs ? import (builtins.fetchTarball { url = "https://github.com/NixOS/nixpkgs/archive/${chan}.tar.gz"; }) {}
}:
# Style sheets https://github.com/citation-style-language/styles/
with pkgs;
let deps = [
(texlive.combine
{ inherit (texlive)
scheme-full;
}
)
];
in
stdenv.mkDerivation {
name = "render_squiggle-spec";
src = ./spec;
buildInputs = deps;
buildPhase = ''
echo rendering...
pdflatex main
biber main
pdflatex main
pdflatex main
echo rendered.
'';
installPhase = ''
mkdir -p $out
cp main.pdf $out/squiggle-spec.pdf
'';
}

5
syntax/spec/appendix.tex Normal file
View File

@ -0,0 +1,5 @@
\documentclass[../main.tex]{subfiles}
\begin{document}
\section{Appendix}
\end{document}

5
syntax/spec/biblio.bib Normal file
View File

@ -0,0 +1,5 @@
@book{@PFPL,
author = {Robert Harper},
title = {Practical Foundations for Programming Languages},
year = {2016}
}

View File

@ -0,0 +1,5 @@
\documentclass[../main.tex]{subfiles}
\begin{document}
\section{Design goals of Squiggle}
\end{document}

29
syntax/spec/main.tex Normal file
View File

@ -0,0 +1,29 @@
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{syntax}
\setlength{\grammarparsep}{2ex plus 0.1ex minus 0.05ex}
% \usepackage[T1]{fontenc}
\usepackage{bussproofs}
\usepackage{amsfonts}
\usepackage{subfiles}
\usepackage{hyperref}
\hypersetup{colorlinks = true, citecolor = blue}
\usepackage[backend=biber, hyperref=true, citestyle=authoryear]{biblatex}
\addbibresource{biblio.bib}
\title{pluto-spec}
\author{Platonic.Systems}
\date{February 2022}
\begin{document}
\maketitle{}
\nocite{*}
\subfile{introduction}
\subfile{syntax}
\subfile{semantics}
\subfile{appendix}
\printbibliography
\end{document}

View File

@ -0,0 +1,5 @@
\documentclass[../main.tex]{subfiles}
\begin{document}
\section{Semantics}\label{section:semantics}
\end{document}

44
syntax/spec/syntax.tex Normal file
View File

@ -0,0 +1,44 @@
\documentclass[../main.tex]{subfiles}
\begin{document}
\section{Syntax}\label{section:syntax}
\subsection{Base types and 44 ast nodes}
In regex notation, we provide the following means of describing literals as well as the specification of the constants T and F.
\begin{center}
\begin{tabular}{c c c}
\texttt{var} & ::= & [a-z][a-zA-Z0-9]* \\
\texttt{int} & ::= & "-"? [0-9]+ \\
\texttt{byte} & ::= & "0x" [0-9a-fA-F] \\
\texttt{bytestring} & ::= & "0x" [0-9a-fA-F]+ \\
\texttt{text} & ::= & <too tough to get latex to compile it lol> \\
\texttt{bool} & ::= & [TF] \\
\texttt{unit} & ::= & [()]
\end{tabular}
\end{center}
\label{tab:atomsregex}
Additionally, we have builtins as follows, (with semantics given in \ref{section:dynamics}). \textbf{Morgan: should a let ast node be in this list of builtins??}
\begin{grammar}
<builtin> ::=
"AddInteger" \alt "SubtractInteger" \alt "MultiplyInteger"
\alt "DivideInteger" \alt "QuotientInteger" \alt "RemainderInteger"
\alt "ModInteger" \alt "EqualsInteger" \alt "LessThanInteger"
\alt "LessThanEqualsInteger" \alt "AppendByteString"
\alt "ConsByteString" \alt "SliceByteString" \alt "LengthByteString"
\alt "IndexByteString" \alt "EqualsByteString" \alt "LessThanByteString"
\alt "LessThanEqualsByteString" \alt "Sha2_256" \alt "Sha3_256" \alt "Blake2b_256"
\alt "VerifySignature" \alt "AppendString" \alt "EqualsString"
\alt "EncodeUtf8" \alt "DecodeUtf8" \alt "IfThenElse" \alt "ChooseUnit"
\alt "MkCons" \alt "HeadList" \alt "TailList" \alt "NullList"
\alt "ChooseData" \alt "ConstrData" \alt "MapData" \alt "ListData"
\alt "IData" \alt "BData" \alt "UnConstrData" \alt "UnMapData"
\alt "EqualsData" \alt "MkPairData" \alt "MkNilData" \alt "MkNilPairData"
\end{grammar}
Many of which have syntax sugars for infix application, like so
\begin{grammar}
<infixbuiltin> ::=
"+i" \alt "-i" \alt "*i" \alt "/i" \alt "//i" \alt $\%$"i" \alt "==i" \alt "lti" \alt $\leq$"i" \alt "+b" \alt ":b" \alt "!b" \alt "==b" \alt "ltb" \alt $\leq$"b" \alt "+s" \alt "==s" \alt "==d"
\end{grammar}
\textit{Sorry, having trouble getting lessthan sign to render rn}. In the small step dynamics given in \ref{section:dynamics}, only abstract syntax (i.e. $<builtin>$) will be provided, not concrete syntax (i.e. including sugar).
\end{document}