diff --git a/.gitignore b/.gitignore index 7fb45e13..13a14a5e 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,4 @@ yarn-error.log .merlin .parcel-cache .DS_Store +.auctex-auto diff --git a/syntax/README.md b/syntax/README.md new file mode 100644 index 00000000..4a12efba --- /dev/null +++ b/syntax/README.md @@ -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. diff --git a/syntax/default.nix b/syntax/default.nix new file mode 100644 index 00000000..e164fdff --- /dev/null +++ b/syntax/default.nix @@ -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 + ''; + } diff --git a/syntax/spec/appendix.tex b/syntax/spec/appendix.tex new file mode 100644 index 00000000..177c4b4d --- /dev/null +++ b/syntax/spec/appendix.tex @@ -0,0 +1,5 @@ +\documentclass[../main.tex]{subfiles} +\begin{document} +\section{Appendix} + +\end{document} diff --git a/syntax/spec/biblio.bib b/syntax/spec/biblio.bib new file mode 100644 index 00000000..4f2c3d64 --- /dev/null +++ b/syntax/spec/biblio.bib @@ -0,0 +1,5 @@ +@book{@PFPL, + author = {Robert Harper}, + title = {Practical Foundations for Programming Languages}, + year = {2016} +} diff --git a/syntax/spec/introduction.tex b/syntax/spec/introduction.tex new file mode 100644 index 00000000..4d018394 --- /dev/null +++ b/syntax/spec/introduction.tex @@ -0,0 +1,5 @@ +\documentclass[../main.tex]{subfiles} +\begin{document} +\section{Design goals of Squiggle} + +\end{document} diff --git a/syntax/spec/main.tex b/syntax/spec/main.tex new file mode 100644 index 00000000..b9268f39 --- /dev/null +++ b/syntax/spec/main.tex @@ -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} diff --git a/syntax/spec/semantics.tex b/syntax/spec/semantics.tex new file mode 100644 index 00000000..efad6de3 --- /dev/null +++ b/syntax/spec/semantics.tex @@ -0,0 +1,5 @@ +\documentclass[../main.tex]{subfiles} +\begin{document} +\section{Semantics}\label{section:semantics} + +\end{document} diff --git a/syntax/spec/syntax.tex b/syntax/spec/syntax.tex new file mode 100644 index 00000000..21fd743a --- /dev/null +++ b/syntax/spec/syntax.tex @@ -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} & ::= & \\ + \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} + ::= + "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} + ::= + "+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. $$) will be provided, not concrete syntax (i.e. including sugar). + +\end{document}