From 518d44f759c0cb9c117f52d030c041bcf6fef030 Mon Sep 17 00:00:00 2001 From: aarne Date: Sat, 18 Sep 2004 09:24:51 +0000 Subject: [PATCH] doc --- examples/gfcc/Imper.gf | 15 +++-- examples/gfcc/ImperC.gf | 45 +++++++++----- examples/gfcc/ImperJVM.gf | 41 ++++++++---- examples/gfcc/ResImper.gf | 29 +++++++-- examples/gfcc/complin.tex | 127 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 220 insertions(+), 37 deletions(-) create mode 100644 examples/gfcc/complin.tex diff --git a/examples/gfcc/Imper.gf b/examples/gfcc/Imper.gf index e67e504f8..fca632cc4 100644 --- a/examples/gfcc/Imper.gf +++ b/examples/gfcc/Imper.gf @@ -8,18 +8,21 @@ abstract Imper = { fun Decl : (A : Typ) -> (Var A -> Stm) -> Stm ; - Assign : (A : Typ) -> Var A -> Exp A -> Stm ; + Assign : (A : Typ) -> Var A -> Exp A -> Stm -> Stm ; Return : (A : Typ) -> Exp A -> Stm ; - While : Exp TInt -> Stm -> Stm ; - Block : Stm -> Stm ; - None : Stm ; - Next : Stm -> Stm -> Stm ; + While : Exp TInt -> Stm -> Stm -> Stm ; + Block : Stm -> Stm -> Stm ; + End : Stm ; EVar : (A : Typ) -> Var A -> Exp A ; EInt : Int -> Exp TInt ; EFloat : Int -> Int -> Exp TFloat ; EAddI : Exp TInt -> Exp TInt -> Exp TInt ; EAddF : Exp TFloat -> Exp TFloat -> Exp TFloat ; + EMulI : Exp TInt -> Exp TInt -> Exp TInt ; + EMulF : Exp TFloat -> Exp TFloat -> Exp TFloat ; + ELtI : Exp TInt -> Exp TInt -> Exp TInt ; + ELtF : Exp TFloat -> Exp TFloat -> Exp TInt ; TInt : Typ ; TFloat : Typ ; @@ -43,7 +46,7 @@ abstract Imper = { BodyCons : (A : Typ) -> (AS : Typs) -> (Var A -> Body AS) -> Body (ConsTyp A AS) ; - EApp : (args : Typs) -> (val : Typ) -> Fun args val -> Exps args -> Exp val ; + EApp : (AS : Typs) -> (V : Typ) -> Fun AS V -> Exps AS -> Exp V ; NilExp : Exps NilTyp ; ConsExp : (A : Typ) -> (AS : Typs) -> diff --git a/examples/gfcc/ImperC.gf b/examples/gfcc/ImperC.gf index 9fdf6f6af..ec78504f3 100644 --- a/examples/gfcc/ImperC.gf +++ b/examples/gfcc/ImperC.gf @@ -3,36 +3,44 @@ concrete ImperC of Imper = open Prelude, Precedence, ResImper in { flags lexer=codevars ; unlexer=code ; startcat=Stm ; + +-- code inside function bodies + lincat Stm = SS ; Typ = SS ; - Exp = {s : PrecTerm} ; + Exp = PrecExp ; Var = SS ; lin Decl typ cont = continue (typ.s ++ cont.$0) cont ; - Assign _ x exp = statement (x.s ++ "=" ++ ex exp) ; + Assign _ x exp = continue (x.s ++ "=" ++ ex exp) ; Return _ exp = statement ("return" ++ ex exp) ; - While exp loop = statement ("while" ++ paren (ex exp) ++ loop.s) ; - Block stm = ss ("{" ++ stm.s ++ "}") ; - None = ss ";" ; - Next stm cont = ss (stm.s ++ cont.s) ; - + While exp loop = continue ("while" ++ paren (ex exp) ++ loop.s) ; + Block stm = continue ("{" ++ stm.s ++ "}") ; + End = statement [] ; + EVar _ x = constant x.s ; EInt n = constant n.s ; EFloat a b = constant (a.s ++ "." ++ b.s) ; + EMulI = infixL p3 "*" ; + EMulF = infixL p3 "*" ; EAddI = infixL p2 "+" ; EAddF = infixL p2 "+" ; + ELtI = infixN p1 "<" ; + ELtF = infixN p1 "<" ; TInt = ss "int" ; TFloat = ss "float" ; + +-- top-level code consisting of function definitions lincat Program = SS ; Typs = SS ; Fun = SS ; - Body = {s,s2 : Str} ; - Exps = SS ; + Body = {s,s2 : Str ; size : Size} ; + Exps = {s : Str ; size : Size} ; lin Empty = ss [] ; @@ -43,12 +51,21 @@ flags lexer=codevars ; unlexer=code ; startcat=Stm ; cont.s ) ; - BodyNil stm = stm ** {s2 = []} ; - BodyCons typ _ body = {s = body.s ; s2 = typ.s ++ body.$0 ++ "," ++ body.s2} ; + NilTyp = ss [] ; + ConsTyp = cc2 ; + + BodyNil stm = stm ** {s2 = [] ; size = Zero} ; + BodyCons typ _ body = { + s = body.s ; + s2 = typ.s ++ body.$0 ++ separator "," body.size ++ body.s2 ; + size = nextSize body.size + } ; EApp args val f exps = constant (f.s ++ paren exps.s) ; - NilExp = ss [] ; - ConsExp _ _ e es = ss (ex e ++ "," ++ es.s) ; - + NilExp = ss [] ** {size = Zero} ; + ConsExp _ _ e es = { + s = ex e ++ separator "," es.size ++ es.s ; + size = nextSize es.size + } ; } diff --git a/examples/gfcc/ImperJVM.gf b/examples/gfcc/ImperJVM.gf index 10457fbfe..9acbfa263 100644 --- a/examples/gfcc/ImperJVM.gf +++ b/examples/gfcc/ImperJVM.gf @@ -4,25 +4,40 @@ concrete ImperJVM of Imper = open Prelude, Precedence, ResImper in { flags lexer=codevars ; unlexer=code ; startcat=Stm ; lincat - Stm = SS ; + Stm = Instr ; Typ = SS ; Exp = SS ; Var = SS ; lin - Decl typ cont = ss [] ; ---- - Assign t x exp = statement (exp.s ++ t.s ++ "_store" ++ x.s) ; - Return t exp = statement (exp.s ++ t.s ++ "_return") ; - While exp loop = statement ("TEST:" ++ exp.s ++ "ifzero_goto" ++ - "END" ++ ";" ++ loop.s ++ "END") ; - Block stm = stm ; - Next stm cont = ss (stm.s ++ cont.s) ; + Decl typ cont = instrc ( + "alloc_" ++ typ.s ++ cont.$0 + ) cont ; + Assign t x exp = instrc ( + exp.s ++ + t.s ++ "_store" ++ x.s + ) ; + Return t exp = instr ( + exp.s ++ + t.s ++ "_return") ; + While exp loop = instrc ( + "TEST:" ++ exp.s ++ + "ifzero_goto" ++ "END" ++ ";" ++ + loop.s ++ + "END" + ) ; + Block stm = instrc stm.s ; + End = ss [] ** {s3 = []} ; - EVar t x = statement (t.s ++ "_load" ++ x.s) ; - EInt n = statement ("i_push" ++ n.s) ; - EFloat a b = statement ("f_push" ++ a.s ++ "." ++ b.s) ; - EAddI x y = statement (x.s ++ y.s ++ "iadd") ; - EAddF x y = statement (x.s ++ y.s ++ "fadd") ; + EVar t x = instr (t.s ++ "_load" ++ x.s) ; + EInt n = instr ("ipush" ++ n.s) ; + EFloat a b = instr ("fpush" ++ a.s ++ "." ++ b.s) ; + EAddI = binop "iadd" ; + EAddF = binop "fadd" ; + EMulI = binop "imul" ; + EMulF = binop "fmul" ; + ELtI = binop ("call" ++ "ilt") ; + ELtF = binop ("call" ++ "flt") ; TInt = ss "i" ; TFloat = ss "f" ; diff --git a/examples/gfcc/ResImper.gf b/examples/gfcc/ResImper.gf index d77322d75..8cdd4f8b7 100644 --- a/examples/gfcc/ResImper.gf +++ b/examples/gfcc/ResImper.gf @@ -1,13 +1,34 @@ resource ResImper = open Prelude, Precedence in { oper + PrecExp : Type = {s : PrecTerm} ; continue : Str -> SS -> SS = \s -> infixSS ";" (ss s); statement : Str -> SS = \s -> postfixSS ";" (ss s); - ex : {s : PrecTerm} -> Str = \exp -> exp.s ! p0 ; - infixL : - Prec -> Str -> {s : PrecTerm} -> {s : PrecTerm} -> {s : PrecTerm} = + ex : PrecExp -> Str = \exp -> exp.s ! p0 ; + infixL : Prec -> Str -> PrecExp -> PrecExp -> PrecExp = \p,h,x,y -> {s = mkInfixL h p x.s y.s} ; + infixN : Prec -> Str -> PrecExp -> PrecExp -> PrecExp = + \p,h,x,y -> {s = mkInfix h p x.s y.s} ; - constant : Str -> {s : PrecTerm} = \c -> {s = mkConst c} ; + constant : Str -> PrecExp = \c -> {s = mkConst c} ; + + param + Size = Zero | One | More ; + oper + nextSize : Size -> Size = \n -> case n of { + Zero => One ; + _ => More + } ; + separator : Str -> Size -> Str = \t,n -> case n of { + Zero => [] ; + _ => t + } ; + +-- for JVM + Instr : Type = {s, s3 : Str} ; -- code, labels + instr : Str -> Instr = \s -> statement s ** {s3 = []} ; ---- + instrc : Str -> Instr -> Instr = \s,i -> statement (s ++ i.s) ** {s3 = i.s3} ; ---- + binop : Str -> SS -> SS -> SS = \op, x, y -> + ss (x.s ++ y.s ++ op ++ ";") ; } \ No newline at end of file diff --git a/examples/gfcc/complin.tex b/examples/gfcc/complin.tex new file mode 100644 index 000000000..8fb2a0221 --- /dev/null +++ b/examples/gfcc/complin.tex @@ -0,0 +1,127 @@ +\documentclass[12pt]{article} + +\usepackage{isolatin1} + +\setlength{\oddsidemargin}{0mm} +%\setlength{\evensidemargin}{0mm} +\setlength{\evensidemargin}{-2mm} +\setlength{\topmargin}{-16mm} +\setlength{\textheight}{240mm} +\setlength{\textwidth}{158mm} + +%\setlength{\parskip}{2mm} +%\setlength{\parindent}{0mm} + +\input{macros} + +\newcommand{\begit}{\begin{itemize}} +\newcommand{\enit}{\end{itemize}} +\newcommand{\newone}{} %%{\newpage} +\newcommand{\heading}[1]{\subsection{#1}} +\newcommand{\explanation}[1]{{\small #1}} +\newcommand{\empha}[1]{{\em #1}} + +\newcommand{\nocolor}{} %% {\color[rgb]{0,0,0}} + + +\title{{\bf Single-Source Language Definitions and Compilation as Linearization}} + +\author{Aarne Ranta \\ + Department of Computing Science \\ + Chalmers University of Technology and the University of Gothenburg\\ + {\tt aarne@cs.chalmers.se}} + +\begin{document} + +\maketitle + + +\section{Introduction} + +In this paper, we will describe a compiler that translates a +subset of C into JVM-like byte code. The compiler has a number of +unusual, yet attractive features: +\bequ +The front end is defined by a grammar of C as its single source. + +The grammar defines both abstract and concrete syntax, and also +semantic well-formedness (types, variable scopes). + +The back end is implemented by means of a grammar of JVM providing +another concrete syntax to the abstract syntax of C. + +As a result of the way JVM is defined, only semantically well formed +JVM programs are generated. + +The JVM grammar can also be used as a decompiler, which translates +JVM code back into C code. + +The language has an interactive editor that also supports incremental +compilation. +\enqu +The theoretical ideas making this kind of a compiler possible +are familiar from various sources. +The grammar that is +powerful enough to enable a single-source language definition +uses \empha{dependent types} and \empha{higher-order abstract syntax} +in the same way as \empha{logical frameworks} \cite{harper,ALF,twelf}. +The very idea of using a common abstract syntax for different +languages was clearly exposed in \cite{landin}. The view of +code generation as linearization is a central aspect of +the classic compiler textbook \cite{aho-ullman}. The use +of the same grammar both for parsing and linearization +is a guiding principle of unification-based linguistic grammar +formalisms \cite{pereira}. Interactive editors derived from +grammars have been used in various programming and proof +assistants \cite{teitelbaum-reps,metal,ALF}. + +Even though the different ideas are well-known, they are +applied less in practive than in theory. In particular, +we have not seen them used together to construct a complete +compiler. In our view, putting these ideas together is +a satisfactory approach to compiling, since a compiler written +in this way is completele declarative and therefore easy to +modify and to port. It is also self-documenting. since the +human-readable grammar defines the syntax and static +semantics that is actually used in the implementation. + +The tool that we have used for writing our compiler is GF, the +\empha{Grammatical Framework} \cite{gf-jfp}. GF +is a grammar formalism designed to help building multilingual +translation systems for natural languages and also +between formal and natural languages. One goal of this work +has been to investigate if GF is capable of implementing +compilers using the ideas of single-source language definition +and code generation as linearization. The working hypothesis +was that it \textit{is} capable but inconvenient, and that, +working out a complete example, we would find out what +should be done to extend GF into a compiler construction tool. + +The various shortcomings and their causes will be explained in +the relevant sections of this report. To summarize, +\bequ +The scoping conditions resulting from HOAS are slightly different +from the standard ones of C. + +Our JVM syntax is forced to be slightly different from original. + +Using HOAS to encode bindings of functions is somewhat cumbersome. + +The C parser derived from the GF grammar does not recognize all +valid programs. +\enqu +The first two shortcomings seem to us inherent to the techniques +we use. The real JVM syntax, however, is easy to obtain by simple +string processing from our one. The latter two shortcomings +suggest that GF should be fine-tuned to give better support +to compiler construction, which, after all is not an intended +use of GF as it is now. + + + + +\end{document} + +\begin{verbatim} +\end{verbatim} +