Reference. Reasonably programmable literal notation
General-purpose programming languages typically define literal notation for only a small number of common data structures, like lists. This is unsatisfying because there are many other data structures for which literal notation might be useful, e.g. finite maps, regular expressions, HTML elements, SQL queries, syntax trees for various languages and chemical structures. There may also be different implementations of each of these data structures behind a common interface that could all benefit from common literal notation. This paper introduces typed literal macros (TLMs) , which allow library providers to define new literal notation of nearly arbitrary design at any specified type or parameterized family of types. Compared to existing approaches, TLMs are uniquely reasonable . TLM clients can reason abstractly, i.e. without examining grammars or generated expansions, about types and binding. The system only needs to convey to clients, via secondary notation, the inferred segmentation of each literal body, which gives the locations and types of spliced subterms. TLM providers can reason modularly about syntactic ambiguity and expansion correctness according to clear criteria. This paper incorporates TLMs into Reason, an emerging alternative front-end for OCaml, and demonstrates, through several non-trivial case studies, how TLMs integrate with the advanced features of OCaml, including pattern matching and the module system. We also discuss optional integration with MetaOCaml, which allows TLM providers to be more confident about type correctness. Finally, we establish these abstract reasoning principles formally with a detailed type-theoretic account of expression and pattern TLMs for “core ML”.
Cite
Cited by (2)
Contextualized Programming Language Documentation potter-2022-contextualized
Filling typed holes with live GUIs omar-2021-filling
Cites 76 works (5 here)
With notes (5)
Hazelnut: a bidirectionally typed structure editor calculus omar-2017-hazelnut
Safely Composable Type-Specific Languages omar-2014-safely
Validating LR(1) Parsers jourdanValidatingLRParsers2012
An LR(1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar G and an automaton A, checks that A and G agree. Validating the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct A. The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.
Yacc: Yet another compiler-compiler Johnsonyacc
Computer program input generally has some structure; in fact, every computer program that does input can be thought of as defining an “input language” which it accepts. An input language may be as complex as a programming language, or as simple as a sequence of numbers. Unfortunately, usual input facilities are limited, difficult to use, and often are lax about checking their inputs for validity. Yacc provides a general tool for describing the input to a computer program. The Yacc user specifies the structures of his input, together with code to be invoked as each such structure is recognized. Yacc turns such a specification into a subroutine that handles the input process; frequently, it is convenient and appropriate to have most of the flow of control in the user’s application handled by this subroutine. The input subroutine produced by Yacc calls a user-supplied routine to return the next basic input item. Thus, the user can specify his input in terms of individual input characters, or in terms of higher level constructs such as names and numbers. The user-supplied routine may also handle idiomatic features such as comment and continuation conventions, which typically defy easy grammatical specification. Yacc is written in portable C. The class of specifications accepted is a very general one: LALR(1) grammars with disambiguating rules. In addition to compilers for C, APL, Pascal, RATFOR, etc., Yacc has also been used for less conventional languages, including a phototypesetter language, several desk calculator languages, a document retrieval system, and a Fortran debugging system.
Programming Techniques: Regular expression search algorithm thompsonProgrammingTechniquesRegular1968
A method for locating specific character strings embedded in character text is described and an implementation of this method in the form of a compiler is discussed. The compiler accepts a regular expression as source language and produces an IBM 7094 program as object language. The object program then accepts the text to be searched as input and produces a signal every time an embedded string in the text matches the given regular expression. Examples, problems, and solutions are also presented.
External (71)
- Markup.ml — Error-recovering streaming HTML5 and XML parsers for OCaml (2018)
- Merlin: a language server for OCaml (experience report) (2018)
- Staged Metaprogramming in stock OCaml (2018)
- Inferring type rules for syntactic sugar (2018)
- Reason Guide: What and Why? https://reasonml.github.io/docs/en/what-and-why.html (2018)
- Macros - Rust Documentation (2018)
- Inferring scope through syntactic sugar (2017)
- ppx_tools: Tools for authors of ppx rewriters (2017)
- Toward Semantic Foundations for Program Editors (2017)
- OWASP Top 10 2017 (2017)
- Sound type-dependent syntactic language extension (2016)
- The Menhir parser generator (2016)
- Information Technology Portable Operating System Interface (POSIX) Base Specifications, Issue 7 (2016)
- Towards the Essence of Hygiene (2015)
- Ur/Web: A Simple Model for Programming the Web (2015)
- Composable and hygienic typed syntax macros (2015)
- http://www.smlnj.org/doc/quote.html . Retrieved (2015)
- FLOPS 2014, Kanazawa, Japan, June 4-6 (2014)
- Scala macros: let our powers combine!: on how rich syntax and static types work with metaprogramming (2013)
- A framework for extensible languages (2013)
- New directions for Template Haskell (2013)
- Modular and automated type-soundness verification for language extensions (2013)
- Layout-sensitive language extensibility with SugarHaskell (2012)
- Creating languages in Racket (2012)
- Active Code Completion (2012)
- Practical Foundations for Programming Languages (2012)
- SugarJ: library-based syntactic language extensibility (2011)
- Ur: statically-typed metaprogramming with type-level record computation (2010)
- Debugging hygienic macros (2010)
- Verifiable composition of deterministic grammars (2009)
- Parsing Mixfix Operators (2008)
- Programming in Scala (2008)
- A Theory of Hygienic Macros (2008)
- Preventing injection attacks with syntax embeddings (2007)
- Why it's nice to be quoted: quasiquoting for haskell (2007)
- LINQ: reconciling object, relations and XML in the .NET framework (2006)
- Towards Efficient, Typed LR Parsers (2006)
- Syntactic abstraction in component interfaces (2005)
- A Gentle Introduction to Multi-stage Programming (2004)
- The Coq proof assistant reference manual, version 8.0 (2004)
- Camlp4 reference manual. Online (2003)
- Haskell 98 language and libraries: the revised report (2003)
- Staged Notational Definitions (2003)
- Template meta-programming for Haskell (2002)
- How to write seemingly unhygienic and referentially opaque macros with syntax-rules (2002)
- Macros as multi-stage computations: type-safe, generative, binding macros in MacroML (2001)
- Lots o'Ticks: real time high performance time series queries on billions of trades and quotes (2001)
- Local type inference (2000)
- Using MetaML: A Staged Programming Language (1999)
- Quasiquotation in Lisp (1999)
- The Definition of Standard ML (Revised) (1997)
- Programming in Standard ML (1997)
- A modal analysis of staged computation (1996)
- Syntactic abstraction in scheme (1993)
- Origin Tracking (1993)
- Higher-order functions for parsing (1992)
- Macros that work (1991)
- Object language embedding in Standard ML of New-Jersey (1991)
- Cognitive Dimensions of Notations (1989)
- Notational definition-a formal account (1988)
- Abstract types have existential type (1988)
- Hygienic macro expansion (1986)
- Types, abstraction and parametric polymorphism (1983)
- Notation as a tool of thought (1980)
- Practical LR error recovery (1979)
- History of LISP (1978)
- Explicit definitions and linguistic dominoes (1965)
- a line notation and computerized interpreter for chemical structures
- A history of mathematical notations
- MACRO Definitions for LISP. Report A. I. MEMO 57
- The OCaml system release 4.02 Documentation and user’s manual