Fix conflict
This commit is contained in:
parent
d85a0d26b8
commit
43e0f67fe2
5 changed files with 213 additions and 4 deletions
|
|
@ -6,7 +6,7 @@ EId. Exp3 ::= Ident ;
|
||||||
EInt. Exp3 ::= Integer ;
|
EInt. Exp3 ::= Integer ;
|
||||||
EApp. Exp2 ::= Exp2 Exp3 ;
|
EApp. Exp2 ::= Exp2 Exp3 ;
|
||||||
EAdd. Exp1 ::= Exp1 "+" Exp2 ;
|
EAdd. Exp1 ::= Exp1 "+" Exp2 ;
|
||||||
EAbs. Exp ::= "\\" Ident "->" Exp ;
|
EAbs. Exp ::= "\\" Ident "." Exp ;
|
||||||
|
|
||||||
coercions Exp 3 ;
|
coercions Exp 3 ;
|
||||||
|
|
||||||
|
|
|
||||||
56
src/Grammar/Doc.txt
Normal file
56
src/Grammar/Doc.txt
Normal file
|
|
@ -0,0 +1,56 @@
|
||||||
|
The Language Grammar
|
||||||
|
BNF Converter
|
||||||
|
|
||||||
|
|
||||||
|
%Process by txt2tags to generate html or latex
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
This document was automatically generated by the //BNF-Converter//. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place).
|
||||||
|
|
||||||
|
==The lexical structure of Grammar==
|
||||||
|
===Identifiers===
|
||||||
|
Identifiers //Ident// are unquoted strings beginning with a letter,
|
||||||
|
followed by any combination of letters, digits, and the characters ``_ '``
|
||||||
|
reserved words excluded.
|
||||||
|
|
||||||
|
|
||||||
|
===Literals===
|
||||||
|
Integer literals //Integer// are nonempty sequences of digits.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
===Reserved words and symbols===
|
||||||
|
The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions.
|
||||||
|
|
||||||
|
The reserved words used in Grammar are the following:
|
||||||
|
| ``main`` | | |
|
||||||
|
|
||||||
|
The symbols used in Grammar are the following:
|
||||||
|
| = | + | \ | .
|
||||||
|
| ( | ) | |
|
||||||
|
|
||||||
|
===Comments===
|
||||||
|
Single-line comments begin with --.Multiple-line comments are enclosed with {- and -}.
|
||||||
|
|
||||||
|
==The syntactic structure of Grammar==
|
||||||
|
Non-terminals are enclosed between < and >.
|
||||||
|
The symbols -> (production), **|** (union)
|
||||||
|
and **eps** (empty rule) belong to the BNF notation.
|
||||||
|
All other symbols are terminals.
|
||||||
|
|
||||||
|
| //Program// | -> | ``main`` ``=`` //Exp//
|
||||||
|
| //Exp3// | -> | //Ident//
|
||||||
|
| | **|** | //Integer//
|
||||||
|
| | **|** | ``(`` //Exp// ``)``
|
||||||
|
| //Exp2// | -> | //Exp2// //Exp3//
|
||||||
|
| | **|** | //Exp3//
|
||||||
|
| //Exp1// | -> | //Exp1// ``+`` //Exp2//
|
||||||
|
| | **|** | //Exp2//
|
||||||
|
| //Exp// | -> | ``\`` //Ident// ``.`` //Exp//
|
||||||
|
| | **|** | //Exp1//
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
%% File generated by the BNF Converter (bnfc 2.9.4.1).
|
||||||
153
src/Grammar/Print.hs
Normal file
153
src/Grammar/Print.hs
Normal file
|
|
@ -0,0 +1,153 @@
|
||||||
|
-- File generated by the BNF Converter (bnfc 2.9.4.1).
|
||||||
|
|
||||||
|
{-# LANGUAGE CPP #-}
|
||||||
|
{-# LANGUAGE FlexibleInstances #-}
|
||||||
|
{-# LANGUAGE LambdaCase #-}
|
||||||
|
#if __GLASGOW_HASKELL__ <= 708
|
||||||
|
{-# LANGUAGE OverlappingInstances #-}
|
||||||
|
#endif
|
||||||
|
|
||||||
|
-- | Pretty-printer for Grammar.
|
||||||
|
|
||||||
|
module Grammar.Print where
|
||||||
|
|
||||||
|
import Prelude
|
||||||
|
( ($), (.)
|
||||||
|
, Bool(..), (==), (<)
|
||||||
|
, Int, Integer, Double, (+), (-), (*)
|
||||||
|
, String, (++)
|
||||||
|
, ShowS, showChar, showString
|
||||||
|
, all, elem, foldr, id, map, null, replicate, shows, span
|
||||||
|
)
|
||||||
|
import Data.Char ( Char, isSpace )
|
||||||
|
import qualified Grammar.Abs
|
||||||
|
|
||||||
|
-- | The top-level printing method.
|
||||||
|
|
||||||
|
printTree :: Print a => a -> String
|
||||||
|
printTree = render . prt 0
|
||||||
|
|
||||||
|
type Doc = [ShowS] -> [ShowS]
|
||||||
|
|
||||||
|
doc :: ShowS -> Doc
|
||||||
|
doc = (:)
|
||||||
|
|
||||||
|
render :: Doc -> String
|
||||||
|
render d = rend 0 False (map ($ "") $ d []) ""
|
||||||
|
where
|
||||||
|
rend
|
||||||
|
:: Int -- ^ Indentation level.
|
||||||
|
-> Bool -- ^ Pending indentation to be output before next character?
|
||||||
|
-> [String]
|
||||||
|
-> ShowS
|
||||||
|
rend i p = \case
|
||||||
|
"[" :ts -> char '[' . rend i False ts
|
||||||
|
"(" :ts -> char '(' . rend i False ts
|
||||||
|
"{" :ts -> onNewLine i p . showChar '{' . new (i+1) ts
|
||||||
|
"}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
|
||||||
|
"}" :ts -> onNewLine (i-1) p . showChar '}' . new (i-1) ts
|
||||||
|
[";"] -> char ';'
|
||||||
|
";" :ts -> char ';' . new i ts
|
||||||
|
t : ts@(s:_) | closingOrPunctuation s
|
||||||
|
-> pending . showString t . rend i False ts
|
||||||
|
t :ts -> pending . space t . rend i False ts
|
||||||
|
[] -> id
|
||||||
|
where
|
||||||
|
-- Output character after pending indentation.
|
||||||
|
char :: Char -> ShowS
|
||||||
|
char c = pending . showChar c
|
||||||
|
|
||||||
|
-- Output pending indentation.
|
||||||
|
pending :: ShowS
|
||||||
|
pending = if p then indent i else id
|
||||||
|
|
||||||
|
-- Indentation (spaces) for given indentation level.
|
||||||
|
indent :: Int -> ShowS
|
||||||
|
indent i = replicateS (2*i) (showChar ' ')
|
||||||
|
|
||||||
|
-- Continue rendering in new line with new indentation.
|
||||||
|
new :: Int -> [String] -> ShowS
|
||||||
|
new j ts = showChar '\n' . rend j True ts
|
||||||
|
|
||||||
|
-- Make sure we are on a fresh line.
|
||||||
|
onNewLine :: Int -> Bool -> ShowS
|
||||||
|
onNewLine i p = (if p then id else showChar '\n') . indent i
|
||||||
|
|
||||||
|
-- Separate given string from following text by a space (if needed).
|
||||||
|
space :: String -> ShowS
|
||||||
|
space t s =
|
||||||
|
case (all isSpace t', null spc, null rest) of
|
||||||
|
(True , _ , True ) -> [] -- remove trailing space
|
||||||
|
(False, _ , True ) -> t' -- remove trailing space
|
||||||
|
(False, True, False) -> t' ++ ' ' : s -- add space if none
|
||||||
|
_ -> t' ++ s
|
||||||
|
where
|
||||||
|
t' = showString t []
|
||||||
|
(spc, rest) = span isSpace s
|
||||||
|
|
||||||
|
closingOrPunctuation :: String -> Bool
|
||||||
|
closingOrPunctuation [c] = c `elem` closerOrPunct
|
||||||
|
closingOrPunctuation _ = False
|
||||||
|
|
||||||
|
closerOrPunct :: String
|
||||||
|
closerOrPunct = ")],;"
|
||||||
|
|
||||||
|
parenth :: Doc -> Doc
|
||||||
|
parenth ss = doc (showChar '(') . ss . doc (showChar ')')
|
||||||
|
|
||||||
|
concatS :: [ShowS] -> ShowS
|
||||||
|
concatS = foldr (.) id
|
||||||
|
|
||||||
|
concatD :: [Doc] -> Doc
|
||||||
|
concatD = foldr (.) id
|
||||||
|
|
||||||
|
replicateS :: Int -> ShowS -> ShowS
|
||||||
|
replicateS n f = concatS (replicate n f)
|
||||||
|
|
||||||
|
-- | The printer class does the job.
|
||||||
|
|
||||||
|
class Print a where
|
||||||
|
prt :: Int -> a -> Doc
|
||||||
|
|
||||||
|
instance {-# OVERLAPPABLE #-} Print a => Print [a] where
|
||||||
|
prt i = concatD . map (prt i)
|
||||||
|
|
||||||
|
instance Print Char where
|
||||||
|
prt _ c = doc (showChar '\'' . mkEsc '\'' c . showChar '\'')
|
||||||
|
|
||||||
|
instance Print String where
|
||||||
|
prt _ = printString
|
||||||
|
|
||||||
|
printString :: String -> Doc
|
||||||
|
printString s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"')
|
||||||
|
|
||||||
|
mkEsc :: Char -> Char -> ShowS
|
||||||
|
mkEsc q = \case
|
||||||
|
s | s == q -> showChar '\\' . showChar s
|
||||||
|
'\\' -> showString "\\\\"
|
||||||
|
'\n' -> showString "\\n"
|
||||||
|
'\t' -> showString "\\t"
|
||||||
|
s -> showChar s
|
||||||
|
|
||||||
|
prPrec :: Int -> Int -> Doc -> Doc
|
||||||
|
prPrec i j = if j < i then parenth else id
|
||||||
|
|
||||||
|
instance Print Integer where
|
||||||
|
prt _ x = doc (shows x)
|
||||||
|
|
||||||
|
instance Print Double where
|
||||||
|
prt _ x = doc (shows x)
|
||||||
|
|
||||||
|
instance Print Grammar.Abs.Ident where
|
||||||
|
prt _ (Grammar.Abs.Ident i) = doc $ showString i
|
||||||
|
instance Print Grammar.Abs.Program where
|
||||||
|
prt i = \case
|
||||||
|
Grammar.Abs.Program exp -> prPrec i 0 (concatD [doc (showString "main"), doc (showString "="), prt 0 exp])
|
||||||
|
|
||||||
|
instance Print Grammar.Abs.Exp where
|
||||||
|
prt i = \case
|
||||||
|
Grammar.Abs.EId id_ -> prPrec i 3 (concatD [prt 0 id_])
|
||||||
|
Grammar.Abs.EInt n -> prPrec i 3 (concatD [prt 0 n])
|
||||||
|
Grammar.Abs.EApp exp1 exp2 -> prPrec i 2 (concatD [prt 2 exp1, prt 3 exp2])
|
||||||
|
Grammar.Abs.EAdd exp1 exp2 -> prPrec i 1 (concatD [prt 1 exp1, doc (showString "+"), prt 2 exp2])
|
||||||
|
Grammar.Abs.EAbs id_ exp -> prPrec i 0 (concatD [doc (showString "\\"), prt 0 id_, doc (showString "."), prt 0 exp])
|
||||||
|
|
@ -39,7 +39,7 @@ eval cxt = \case
|
||||||
|
|
||||||
EInt i -> pure $ VInt i
|
EInt i -> pure $ VInt i
|
||||||
|
|
||||||
-- γ ⊢ e ⇓ let δ in λx → f
|
-- γ ⊢ e ⇓ let δ in λx. f
|
||||||
-- γ ⊢ e₁ ⇓ v
|
-- γ ⊢ e₁ ⇓ v
|
||||||
-- δ,x=v ⊢ f ⇓ v₁
|
-- δ,x=v ⊢ f ⇓ v₁
|
||||||
-- ------------------------------
|
-- ------------------------------
|
||||||
|
|
@ -54,7 +54,7 @@ eval cxt = \case
|
||||||
|
|
||||||
--
|
--
|
||||||
-- -----------------------------
|
-- -----------------------------
|
||||||
-- γ ⊢ λx → f ⇓ let γ in λx → f
|
-- γ ⊢ λx. f ⇓ let γ in λx. f
|
||||||
|
|
||||||
EAbs x e -> pure $ VClosure cxt x e
|
EAbs x e -> pure $ VClosure cxt x e
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -2,4 +2,4 @@
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
main = (\x -> x + x + 3) ((\x -> x) 2)
|
main = (\x. x + x + 3) ((\x. x) 2)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue