pingu/Alisaie
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Haha

Browse Source
This commit is contained in:
pingu
2025-11-28 10:49:36 +01:00
parent 37ce925067
commit 6f80ac585c
22 changed files with 5350 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
.envrc Normal file
View File

@ -0,0 +1 @@
use flake

11
.gitignore vendored
View File

@ -1,6 +1,14 @@
# ---> Agda # ---> Agda
*.agdai **.agdai
MAlonzo/** MAlonzo/**
**.hi
**/*.hi
**/*.o
**/*.log
**/*.aux
**/*.dvi
**/*.agdai
Alisaie/Test
# ---> Nix # ---> Nix
# Ignore build outputs from performing a nix-build or `nix build` command # Ignore build outputs from performing a nix-build or `nix build` command
@ -10,3 +18,4 @@ result-*
# Ignore automatically generated direnv output # Ignore automatically generated direnv output
.direnv .direnv
Main

44
Alisaie.cf Normal file
View File

@ -0,0 +1,44 @@
Prog. Program ::= [Definition];
Def. Definition ::= Ident ":" Type "\n" Ident [Ident] "=" Exp;
KStar. Kind ::= "*";
KArr. Kind1 ::= Kind "→" Kind;
_. Kind1 ::= Kind;
token UIdent (upper (letter | digit | '_')*);
TString. Type1 ::= "String";
TInt. Type1 ::= "Int";
TDouble. Type1 ::= "Double";
TChar. Type1 ::= "Char";
TCustom. Type1 ::= UIdent;
TArr. Type ::= Type1 "→" Type;
TForall. Type ::= "∀" Ident ":" Kind "." Type;
TLambda. Type ::= "λ" Ident ":" Kind "." Type;
coercions Type 1;
terminator Definition "";
terminator Ident "";
EVar. Exp4 ::= Ident;
EInt. Exp4 ::= Integer;
EDouble. Exp4 ::= Double;
EChar. Exp4 ::= Char;
EText. Exp4 ::= String;
EApp. Exp2 ::= Exp2 Exp3; -- TODO: Fix shift reduce conflicts from these
ETApp. Exp2 ::= Exp2 Type; -- TODO: Fix shift reduce conflicts from these
EAdd. Exp1 ::= Exp1 "+" Exp2;
ESub. Exp1 ::= Exp1 "-" Exp2;
ELt. Exp1 ::= Exp1 "<" Exp2;
EIf. Exp ::= "if" Exp "then" Exp "else" Exp;
ETAbs. Exp ::= "Λ" Ident ":" Kind "." Exp;
EAbs. Exp ::= "λ" Ident ":" Type "." Exp;
coercions Exp 4;
comment "--";
comment "{-" "-}";

136
Alisaie/AST.agda Normal file
View File

@ -0,0 +1,136 @@
-- File generated by the BNF Converter (bnfc 2.9.6.1).
-- Agda bindings for the Haskell abstract syntax data types.
module Alisaie.AST where
open import Agda.Builtin.Char using (Char)
open import Agda.Builtin.Float public using () renaming (Float to Double)
open import Agda.Builtin.Int public using () renaming (Int to Integer)
open import Agda.Builtin.Int using () renaming (pos to #pos)
open import Agda.Builtin.List using ([]; _∷_) renaming (List to #List)
open import Agda.Builtin.String using () renaming
( String to #String
; primStringFromList to #stringFromList
)
String = #List Char
{-# FOREIGN GHC import Prelude (Bool, Char, Double, Integer, String, (.)) #-}
{-# FOREIGN GHC import qualified Data.Text #-}
{-# FOREIGN GHC import qualified Alisaie.Abs #-}
{-# FOREIGN GHC import Alisaie.Print (printTree) #-}
data Ident : Set where
ident : #String → Ident
{-# COMPILE GHC Ident = data Alisaie.Abs.Ident (Alisaie.Abs.Ident) #-}
data UIdent : Set where
uIdent : #String → UIdent
{-# COMPILE GHC UIdent = data Alisaie.Abs.UIdent (Alisaie.Abs.UIdent) #-}
mutual
data Program : Set where
prog : (ds : #List Definition) → Program
{-# COMPILE GHC Program = data Alisaie.Abs.Program (Alisaie.Abs.Prog) #-}
data Definition : Set where
def : (x₁ : Ident) (t : Type) (x₂ : Ident) (xs : #List Ident) (e : Exp) → Definition
{-# COMPILE GHC Definition = data Alisaie.Abs.Definition (Alisaie.Abs.Def) #-}
data Kind : Set where
kStar : Kind
kArr : (k₁ k₂ : Kind) → Kind
{-# COMPILE GHC Kind = data Alisaie.Abs.Kind
( Alisaie.Abs.KStar
| Alisaie.Abs.KArr
) #-}
data Type : Set where
tString : Type
tInt : Type
tDouble : Type
tChar : Type
tCustom : (x : UIdent) → Type
tArr : (t₁ t₂ : Type) → Type
tForall : (x : Ident) (k : Kind) (t : Type) → Type
tLambda : (x : Ident) (k : Kind) (t : Type) → Type
{-# COMPILE GHC Type = data Alisaie.Abs.Type
( Alisaie.Abs.TString
| Alisaie.Abs.TInt
| Alisaie.Abs.TDouble
| Alisaie.Abs.TChar
| Alisaie.Abs.TCustom
| Alisaie.Abs.TArr
| Alisaie.Abs.TForall
| Alisaie.Abs.TLambda
) #-}
data Exp : Set where
eVar : (x : Ident) → Exp
eInt : (x : Integer) → Exp
eDouble : (x : Double) → Exp
eChar : (x : Char) → Exp
eText : (x : String) → Exp
eApp : (e₁ e₂ : Exp) → Exp
eTApp : (e : Exp) (t : Type) → Exp
eAdd : (e₁ e₂ : Exp) → Exp
eSub : (e₁ e₂ : Exp) → Exp
eLt : (e₁ e₂ : Exp) → Exp
eIf : (e₁ e₂ e₃ : Exp) → Exp
eTAbs : (x : Ident) (k : Kind) (e : Exp) → Exp
eAbs : (x : Ident) (t : Type) (e : Exp) → Exp
{-# COMPILE GHC Exp = data Alisaie.Abs.Exp
( Alisaie.Abs.EVar
| Alisaie.Abs.EInt
| Alisaie.Abs.EDouble
| Alisaie.Abs.EChar
| Alisaie.Abs.EText
| Alisaie.Abs.EApp
| Alisaie.Abs.ETApp
| Alisaie.Abs.EAdd
| Alisaie.Abs.ESub
| Alisaie.Abs.ELt
| Alisaie.Abs.EIf
| Alisaie.Abs.ETAbs
| Alisaie.Abs.EAbs
) #-}
-- Binding the pretty printers.
postulate
printProgram : Program → #String
printDefinition : Definition → #String
printKind : Kind → #String
printType : Type → #String
printListDefinition : #List Definition → #String
printListIdent : #List Ident → #String
printExp : Exp → #String
printIdent : Ident → #String
printChar : Char → #String
printDouble : Double → #String
printInteger : Integer → #String
printString : String → #String
printUIdent : UIdent → #String
{-# COMPILE GHC printProgram = \ p -> Data.Text.pack (printTree (p :: Alisaie.Abs.Program)) #-}
{-# COMPILE GHC printDefinition = \ d -> Data.Text.pack (printTree (d :: Alisaie.Abs.Definition)) #-}
{-# COMPILE GHC printKind = \ k -> Data.Text.pack (printTree (k :: Alisaie.Abs.Kind)) #-}
{-# COMPILE GHC printType = \ t -> Data.Text.pack (printTree (t :: Alisaie.Abs.Type)) #-}
{-# COMPILE GHC printListDefinition = \ ds -> Data.Text.pack (printTree (ds :: [Alisaie.Abs.Definition])) #-}
{-# COMPILE GHC printListIdent = \ xs -> Data.Text.pack (printTree (xs :: [Alisaie.Abs.Ident])) #-}
{-# COMPILE GHC printExp = \ e -> Data.Text.pack (printTree (e :: Alisaie.Abs.Exp)) #-}
{-# COMPILE GHC printIdent = \ x -> Data.Text.pack (printTree (x :: Alisaie.Abs.Ident)) #-}
{-# COMPILE GHC printChar = \ x -> Data.Text.pack (printTree (x :: Char)) #-}
{-# COMPILE GHC printDouble = \ x -> Data.Text.pack (printTree (x :: Double)) #-}
{-# COMPILE GHC printInteger = \ x -> Data.Text.pack (printTree (x :: Integer)) #-}
{-# COMPILE GHC printString = \ x -> Data.Text.pack (printTree (x :: String)) #-}
{-# COMPILE GHC printUIdent = \ x -> Data.Text.pack (printTree (x :: Alisaie.Abs.UIdent)) #-}

56
Alisaie/Abs.hs Normal file
View File

@ -0,0 +1,56 @@
-- File generated by the BNF Converter (bnfc 2.9.6.1).
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-- | The abstract syntax of language Alisaie.
module Alisaie.Abs where
import Prelude (Char, Double, Integer, String)
import qualified Prelude as C (Eq, Ord, Show, Read)
import qualified Data.String
import qualified Data.Text
data Program = Prog [Definition]
deriving (C.Eq, C.Ord, C.Show, C.Read)
data Definition = Def Ident Type Ident [Ident] Exp
deriving (C.Eq, C.Ord, C.Show, C.Read)
data Kind = KStar | KArr Kind Kind
deriving (C.Eq, C.Ord, C.Show, C.Read)
data Type
= TString
| TInt
| TDouble
| TChar
| TCustom UIdent
| TArr Type Type
| TForall Ident Kind Type
| TLambda Ident Kind Type
deriving (C.Eq, C.Ord, C.Show, C.Read)
data Exp
= EVar Ident
| EInt Integer
| EDouble Double
| EChar Char
| EText String
| EApp Exp Exp
| ETApp Exp Type
| EAdd Exp Exp
| ESub Exp Exp
| ELt Exp Exp
| EIf Exp Exp Exp
| ETAbs Ident Kind Exp
| EAbs Ident Type Exp
deriving (C.Eq, C.Ord, C.Show, C.Read)
newtype Ident = Ident Data.Text.Text
deriving (C.Eq, C.Ord, C.Show, C.Read, Data.String.IsString)
newtype UIdent = UIdent Data.Text.Text
deriving (C.Eq, C.Ord, C.Show, C.Read, Data.String.IsString)

105
Alisaie/Doc.txt Normal file
View File

@ -0,0 +1,105 @@
The Language Alisaie
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 Alisaie==
===Identifiers===
Identifiers //Ident// are unquoted strings beginning with a letter,
followed by any combination of letters, digits, and the characters ``_ '``
reserved words excluded.
===Literals===
Character literals //Char// have the form
``'``//c//``'``, where //c// is any single character.
Double-precision float literals //Double// have the structure
indicated by the regular expression ``digit+ '.' digit+ ('e' ('-')? digit+)?`` i.e.\
two sequences of digits separated by a decimal point, optionally
followed by an unsigned or negative exponent.
Integer literals //Integer// are nonempty sequences of digits.
String literals //String// have the form
``"``//x//``"``}, where //x// is any sequence of any characters
except ``"`` unless preceded by ``\``.
UIdent literals are recognized by the regular expression
`````upper ('_' | digit | letter)*`````
===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 Alisaie are the following:
| ``Char`` | ``Double`` | ``Int`` | ``String``
| ``else`` | ``if`` | ``then`` | ``Λ``
| ``λ`` | | |
The symbols used in Alisaie are the following:
| : | = | * | →
| ∀ | . | ( | )
| + | - | < |
===Comments===
Single-line comments begin with --.Multiple-line comments are enclosed with {- and -}.
==The syntactic structure of Alisaie==
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// | -> | //[Definition]//
| //Definition// | -> | //Ident// ``:`` //Type// //Ident// //[Ident]// ``=`` //Exp//
| //Kind// | -> | ``*``
| //Kind1// | -> | //Kind// ``→`` //Kind//
| | **|** | //Kind//
| //Type1// | -> | ``String``
| | **|** | ``Int``
| | **|** | ``Double``
| | **|** | ``Char``
| | **|** | //UIdent//
| | **|** | ``(`` //Type// ``)``
| //Type// | -> | //Type1// ``→`` //Type//
| | **|** | ``∀`` //Ident// ``:`` //Kind// ``.`` //Type//
| | **|** | ``λ`` //Ident// ``:`` //Kind// ``.`` //Type//
| | **|** | //Type1//
| //[Definition]// | -> | **eps**
| | **|** | //Definition// //[Definition]//
| //[Ident]// | -> | **eps**
| | **|** | //Ident// //[Ident]//
| //Exp4// | -> | //Ident//
| | **|** | //Integer//
| | **|** | //Double//
| | **|** | //Char//
| | **|** | //String//
| | **|** | ``(`` //Exp// ``)``
| //Exp2// | -> | //Exp2// //Exp3//
| | **|** | //Exp2// //Type//
| | **|** | //Exp3//
| //Exp1// | -> | //Exp1// ``+`` //Exp2//
| | **|** | //Exp1// ``-`` //Exp2//
| | **|** | //Exp1// ``<`` //Exp2//
| | **|** | //Exp2//
| //Exp// | -> | ``if`` //Exp// ``then`` //Exp// ``else`` //Exp//
| | **|** | ``Λ`` //Ident// ``:`` //Kind// ``.`` //Exp//
| | **|** | ``λ`` //Ident// ``:`` //Type// ``.`` //Exp//
| | **|** | //Exp1//
| //Exp3// | -> | //Exp4//
%% File generated by the BNF Converter (bnfc 2.9.6.1).

44
Alisaie/ErrM.hs Normal file
View File

@ -0,0 +1,44 @@
-- File generated by the BNF Converter (bnfc 2.9.6.1).
{-# LANGUAGE CPP #-}
-- | BNF Converter: Error Monad.
--
-- Module for backwards compatibility.
--
-- The generated parser now uses @'Either' String@ as error monad.
-- This module defines a type synonym 'Err' and pattern synonyms
-- 'Bad' and 'Ok' for 'Left' and 'Right'.
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
module Alisaie.ErrM where
import Prelude (id, const, Either(..), String)
import Control.Monad (MonadPlus(..))
import Control.Applicative (Alternative(..))
#if __GLASGOW_HASKELL__ >= 808
import Control.Monad (MonadFail(..))
#endif
-- | Error monad with 'String' error messages.
type Err = Either String
pattern Bad msg = Left msg
pattern Ok a = Right a
#if __GLASGOW_HASKELL__ >= 808
instance MonadFail Err where
fail = Bad
#endif
instance Alternative Err where
empty = Left "Err.empty"
(<|>) Left{} = id
(<|>) x@Right{} = const x
instance MonadPlus Err where
mzero = empty
mplus = (<|>)

56
Alisaie/IOLib.agda Normal file
View File

@ -0,0 +1,56 @@
-- File generated by the BNF Converter (bnfc 2.9.6.1).
-- Basic I/O library.
module Alisaie.IOLib where
open import Agda.Builtin.IO public using (IO)
open import Agda.Builtin.List public using (List; []; _∷_)
open import Agda.Builtin.String public using (String)
renaming (primStringFromList to stringFromList)
open import Agda.Builtin.Unit public using (⊤)
-- I/O monad.
postulate
return : ∀ {a} {A : Set a} → A → IO A
_>>=_ : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B
{-# COMPILE GHC return = \ _ _ -> return #-}
{-# COMPILE GHC _>>=_ = \ _ _ _ _ -> (>>=) #-}
infixl 1 _>>=_ _>>_
_>>_ : ∀ {b} {B : Set b} → IO ⊤ → IO B → IO B
_>>_ = λ m m' → m >>= λ _ → m'
-- Co-bind and functoriality.
infixr 1 _=<<_ _<$>_
_=<<_ : ∀ {a b} {A : Set a} {B : Set b} → (A → IO B) → IO A → IO B
k =<< m = m >>= k
_<$>_ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → IO A → IO B
f <$> m = do
a ← m
return (f a)
-- Binding basic I/O functionality.
{-# FOREIGN GHC import qualified Data.Text #-}
{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# FOREIGN GHC import qualified System.Exit #-}
{-# FOREIGN GHC import qualified System.Environment #-}
{-# FOREIGN GHC import qualified System.IO #-}
postulate
exitFailure : ∀{a} {A : Set a} → IO A
getArgs : IO (List String)
putStrLn : String → IO ⊤
readFiniteFile : String → IO String
{-# COMPILE GHC exitFailure = \ _ _ -> System.Exit.exitFailure #-}
{-# COMPILE GHC getArgs = fmap (map Data.Text.pack) System.Environment.getArgs #-}
{-# COMPILE GHC putStrLn = System.IO.putStrLn . Data.Text.unpack #-}
{-# COMPILE GHC readFiniteFile = Data.Text.IO.readFile . Data.Text.unpack #-}

564
Alisaie/Lex.hs Normal file
View File

File diff suppressed because one or more lines are too long

270
Alisaie/Lex.x Normal file
View File

@ -0,0 +1,270 @@
-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6.1).
-- Lexer definition for use with Alex 3
{
{-# OPTIONS -Wno-incomplete-patterns #-}
{-# OPTIONS_GHC -w #-}
{-# LANGUAGE PatternSynonyms #-}
module Alisaie.Lex where
import Prelude
import qualified Data.Text
import qualified Data.Bits
import Data.Char (ord)
import Data.Function (on)
import Data.Word (Word8)
}
-- Predefined character classes
$c = [A-Z\192-\222] # [\215] -- capital isolatin1 letter (215 = \times)
$s = [a-z\223-\255] # [\247] -- small isolatin1 letter (247 = \div )
$l = [$c $s] -- letter
$d = [0-9] -- digit
$i = [$l $d _ '] -- identifier character
$u = [. \n] -- universal: any character
-- Symbols and non-identifier-like reserved words
@rsyms = \λ | \Λ | \: | \= | \* | \→ | \∀ | \. | \( | \) | \+ | \- | \<
:-
-- Line comment "--"
"--" [.]* ;
-- Block comment "{-" "-}"
\{ \- [$u # \-]* \- ([$u # [\- \}]] [$u # \-]* \- | \-)* \} ;
-- Whitespace (skipped)
$white+ ;
-- Symbols
@rsyms
{ tok (eitherResIdent TV) }
-- token UIdent
$c (\_ | ($d | $l)) *
{ tok (eitherResIdent T_UIdent) }
-- Keywords and Ident
$l $i*
{ tok (eitherResIdent TV) }
-- String
\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | r | f)))* \"
{ tok (TL . unescapeInitTail) }
-- Char
\' ($u # [\' \\] | \\ [\\ \' n t r f]) \'
{ tok TC }
-- Integer
$d+
{ tok TI }
-- Double
$d+ \. $d+ (e (\-)? $d+)?
{ tok TD }
{
-- | Create a token with position.
tok :: (Data.Text.Text -> Tok) -> (Posn -> Data.Text.Text -> Token)
tok f p = PT p . f
-- | Token without position.
data Tok
= TK {-# UNPACK #-} !TokSymbol -- ^ Reserved word or symbol.
| TL !Data.Text.Text -- ^ String literal.
| TI !Data.Text.Text -- ^ Integer literal.
| TV !Data.Text.Text -- ^ Identifier.
| TD !Data.Text.Text -- ^ Float literal.
| TC !Data.Text.Text -- ^ Character literal.
| T_UIdent !Data.Text.Text
deriving (Eq, Show, Ord)
-- | Smart constructor for 'Tok' for the sake of backwards compatibility.
pattern TS :: Data.Text.Text -> Int -> Tok
pattern TS t i = TK (TokSymbol t i)
-- | Keyword or symbol tokens have a unique ID.
data TokSymbol = TokSymbol
{ tsText :: Data.Text.Text
-- ^ Keyword or symbol text.
, tsID :: !Int
-- ^ Unique ID.
} deriving (Show)
-- | Keyword/symbol equality is determined by the unique ID.
instance Eq TokSymbol where (==) = (==) `on` tsID
-- | Keyword/symbol ordering is determined by the unique ID.
instance Ord TokSymbol where compare = compare `on` tsID
-- | Token with position.
data Token
= PT Posn Tok
| Err Posn
deriving (Eq, Show, Ord)
-- | Pretty print a position.
printPosn :: Posn -> String
printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c
-- | Pretty print the position of the first token in the list.
tokenPos :: [Token] -> String
tokenPos (t:_) = printPosn (tokenPosn t)
tokenPos [] = "end of file"
-- | Get the position of a token.
tokenPosn :: Token -> Posn
tokenPosn (PT p _) = p
tokenPosn (Err p) = p
-- | Get line and column of a token.
tokenLineCol :: Token -> (Int, Int)
tokenLineCol = posLineCol . tokenPosn
-- | Get line and column of a position.
posLineCol :: Posn -> (Int, Int)
posLineCol (Pn _ l c) = (l,c)
-- | Convert a token into "position token" form.
mkPosToken :: Token -> ((Int, Int), Data.Text.Text)
mkPosToken t = (tokenLineCol t, tokenText t)
-- | Convert a token to its text.
tokenText :: Token -> Data.Text.Text
tokenText t = case t of
PT _ (TS s _) -> s
PT _ (TL s) -> Data.Text.pack (show s)
PT _ (TI s) -> s
PT _ (TV s) -> s
PT _ (TD s) -> s
PT _ (TC s) -> s
Err _ -> Data.Text.pack "#error"
PT _ (T_UIdent s) -> s
-- | Convert a token to a string.
prToken :: Token -> String
prToken t = Data.Text.unpack (tokenText t)
-- | Finite map from text to token organized as binary search tree.
data BTree
= N -- ^ Nil (leaf).
| B Data.Text.Text Tok BTree BTree
-- ^ Binary node.
deriving (Show)
-- | Convert potential keyword into token or use fallback conversion.
eitherResIdent :: (Data.Text.Text -> Tok) -> Data.Text.Text -> Tok
eitherResIdent tv s = treeFind resWords
where
treeFind N = tv s
treeFind (B a t left right) =
case compare s a of
LT -> treeFind left
GT -> treeFind right
EQ -> t
-- | The keywords and symbols of the language organized as binary search tree.
resWords :: BTree
resWords =
b "Double" 11
(b "." 6
(b "*" 3 (b ")" 2 (b "(" 1 N N) N) (b "-" 5 (b "+" 4 N N) N))
(b "=" 9 (b "<" 8 (b ":" 7 N N) N) (b "Char" 10 N N)))
(b "then" 16
(b "else" 14 (b "String" 13 (b "Int" 12 N N) N) (b "if" 15 N N))
(b "\8594" 19
(b "\955" 18 (b "\923" 17 N N) N) (b "\8704" 20 N N)))
where
b s n = B bs (TS bs n)
where
bs = Data.Text.pack s
-- | Unquote string literal.
unescapeInitTail :: Data.Text.Text -> Data.Text.Text
unescapeInitTail = Data.Text.pack . unesc . tail . Data.Text.unpack
where
unesc s = case s of
'\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs
'\\':'n':cs -> '\n' : unesc cs
'\\':'t':cs -> '\t' : unesc cs
'\\':'r':cs -> '\r' : unesc cs
'\\':'f':cs -> '\f' : unesc cs
'"':[] -> []
c:cs -> c : unesc cs
_ -> []
-------------------------------------------------------------------
-- Alex wrapper code.
-- A modified "posn" wrapper.
-------------------------------------------------------------------
data Posn = Pn !Int !Int !Int
deriving (Eq, Show, Ord)
alexStartPos :: Posn
alexStartPos = Pn 0 1 1
alexMove :: Posn -> Char -> Posn
alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1)
alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1
alexMove (Pn a l c) _ = Pn (a+1) l (c+1)
type Byte = Word8
type AlexInput = (Posn, -- current position,
Char, -- previous char
[Byte], -- pending bytes on the current char
Data.Text.Text) -- current input string
tokens :: Data.Text.Text -> [Token]
tokens str = go (alexStartPos, '\n', [], str)
where
go :: AlexInput -> [Token]
go inp@(pos, _, _, str) =
case alexScan inp 0 of
AlexEOF -> []
AlexError (pos, _, _, _) -> [Err pos]
AlexSkip inp' len -> go inp'
AlexToken inp' len act -> act pos (Data.Text.take len str) : (go inp')
alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)
alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))
alexGetByte (p, _, [], s) =
case Data.Text.uncons s of
Nothing -> Nothing
Just (c,s) ->
let p' = alexMove p c
(b:bs) = utf8Encode c
in p' `seq` Just (b, (p', c, bs, s))
alexInputPrevChar :: AlexInput -> Char
alexInputPrevChar (p, c, bs, s) = c
-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
utf8Encode :: Char -> [Word8]
utf8Encode = map fromIntegral . go . ord
where
go oc
| oc <= 0x7f = [oc]
| oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6)
, 0x80 + oc Data.Bits..&. 0x3f
]
| oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12)
, 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
, 0x80 + oc Data.Bits..&. 0x3f
]
| otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18)
, 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)
, 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
, 0x80 + oc Data.Bits..&. 0x3f
]
}

22
Alisaie/Main.agda Normal file
View File

@ -0,0 +1,22 @@
-- File generated by the BNF Converter (bnfc 2.9.6.1).
-- Test for Agda binding of parser. Requires Agda >= 2.5.4.
module Alisaie.Main where
open import Alisaie.IOLib
open import Alisaie.AST using (printProgram)
open import Alisaie.Parser using (Err; parseProgram)
main : IO ⊤
main = do
file ∷ [] ← getArgs where
_ → do
putStrLn "usage: Main <SourceFile>"
exitFailure
Err.ok result ← parseProgram <$> readFiniteFile file where
Err.bad msg → do
putStrLn "PARSE FAILED\n"
putStrLn (stringFromList msg)
exitFailure
putStrLn "PARSE SUCCESSFUL\n"
putStrLn (printProgram result)

1272
Alisaie/Par.hs Normal file
View File

File diff suppressed because one or more lines are too long

2041
Alisaie/Par.info Normal file
View File

File diff suppressed because it is too large Load Diff

182
Alisaie/Par.y Normal file
View File

@ -0,0 +1,182 @@
-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6.1).
-- Parser definition for use with Happy
{
{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
{-# LANGUAGE PatternSynonyms #-}
module Alisaie.Par
( happyError
, myLexer
, pProgram
, pDefinition
, pKind
, pKind1
, pType1
, pType
, pListDefinition
, pListIdent
, pExp4
, pExp2
, pExp1
, pExp
, pExp3
) where
import Prelude
import qualified Alisaie.Abs
import Alisaie.Lex
import qualified Data.Text
}
%name pProgram Program
%name pDefinition Definition
%name pKind Kind
%name pKind1 Kind1
%name pType1 Type1
%name pType Type
%name pListDefinition ListDefinition
%name pListIdent ListIdent
%name pExp4 Exp4
%name pExp2 Exp2
%name pExp1 Exp1
%name pExp Exp
%name pExp3 Exp3
-- no lexer declaration
%monad { Err } { (>>=) } { return }
%tokentype {Token}
%token
'(' { PT _ (TS _ 1) }
')' { PT _ (TS _ 2) }
'*' { PT _ (TS _ 3) }
'+' { PT _ (TS _ 4) }
'-' { PT _ (TS _ 5) }
'.' { PT _ (TS _ 6) }
':' { PT _ (TS _ 7) }
'<' { PT _ (TS _ 8) }
'=' { PT _ (TS _ 9) }
'Char' { PT _ (TS _ 10) }
'Double' { PT _ (TS _ 11) }
'Int' { PT _ (TS _ 12) }
'String' { PT _ (TS _ 13) }
'else' { PT _ (TS _ 14) }
'if' { PT _ (TS _ 15) }
'then' { PT _ (TS _ 16) }
'Λ' { PT _ (TS _ 17) }
'λ' { PT _ (TS _ 18) }
'→' { PT _ (TS _ 19) }
'∀' { PT _ (TS _ 20) }
L_Ident { PT _ (TV $$) }
L_charac { PT _ (TC $$) }
L_doubl { PT _ (TD $$) }
L_integ { PT _ (TI $$) }
L_quoted { PT _ (TL $$) }
L_UIdent { PT _ (T_UIdent $$) }
%%
Ident :: { Alisaie.Abs.Ident }
Ident : L_Ident { Alisaie.Abs.Ident $1 }
Char :: { Char }
Char : L_charac { (read (Data.Text.unpack $1)) :: Char }
Double :: { Double }
Double : L_doubl { (read (Data.Text.unpack $1)) :: Double }
Integer :: { Integer }
Integer : L_integ { (read (Data.Text.unpack $1)) :: Integer }
String :: { String }
String : L_quoted { (Data.Text.unpack $1) }
UIdent :: { Alisaie.Abs.UIdent }
UIdent : L_UIdent { Alisaie.Abs.UIdent $1 }
Program :: { Alisaie.Abs.Program }
Program : ListDefinition { Alisaie.Abs.Prog $1 }
Definition :: { Alisaie.Abs.Definition }
Definition
: Ident ':' Type Ident ListIdent '=' Exp { Alisaie.Abs.Def $1 $3 $4 $5 $7 }
Kind :: { Alisaie.Abs.Kind }
Kind : '*' { Alisaie.Abs.KStar }
Kind1 :: { Alisaie.Abs.Kind }
Kind1 : Kind '→' Kind { Alisaie.Abs.KArr $1 $3 } | Kind { $1 }
Type1 :: { Alisaie.Abs.Type }
Type1
: 'String' { Alisaie.Abs.TString }
| 'Int' { Alisaie.Abs.TInt }
| 'Double' { Alisaie.Abs.TDouble }
| 'Char' { Alisaie.Abs.TChar }
| UIdent { Alisaie.Abs.TCustom $1 }
| '(' Type ')' { $2 }
Type :: { Alisaie.Abs.Type }
Type
: Type1 '→' Type { Alisaie.Abs.TArr $1 $3 }
| '∀' Ident ':' Kind '.' Type { Alisaie.Abs.TForall $2 $4 $6 }
| 'λ' Ident ':' Kind '.' Type { Alisaie.Abs.TLambda $2 $4 $6 }
| Type1 { $1 }
ListDefinition :: { [Alisaie.Abs.Definition] }
ListDefinition
: {- empty -} { [] } | Definition ListDefinition { (:) $1 $2 }
ListIdent :: { [Alisaie.Abs.Ident] }
ListIdent : {- empty -} { [] } | Ident ListIdent { (:) $1 $2 }
Exp4 :: { Alisaie.Abs.Exp }
Exp4
: Ident { Alisaie.Abs.EVar $1 }
| Integer { Alisaie.Abs.EInt $1 }
| Double { Alisaie.Abs.EDouble $1 }
| Char { Alisaie.Abs.EChar $1 }
| String { Alisaie.Abs.EText $1 }
| '(' Exp ')' { $2 }
Exp2 :: { Alisaie.Abs.Exp }
Exp2
: Exp2 Exp3 { Alisaie.Abs.EApp $1 $2 }
| Exp2 Type { Alisaie.Abs.ETApp $1 $2 }
| Exp3 { $1 }
Exp1 :: { Alisaie.Abs.Exp }
Exp1
: Exp1 '+' Exp2 { Alisaie.Abs.EAdd $1 $3 }
| Exp1 '-' Exp2 { Alisaie.Abs.ESub $1 $3 }
| Exp1 '<' Exp2 { Alisaie.Abs.ELt $1 $3 }
| Exp2 { $1 }
Exp :: { Alisaie.Abs.Exp }
Exp
: 'if' Exp 'then' Exp 'else' Exp { Alisaie.Abs.EIf $2 $4 $6 }
| 'Λ' Ident ':' Kind '.' Exp { Alisaie.Abs.ETAbs $2 $4 $6 }
| 'λ' Ident ':' Type '.' Exp { Alisaie.Abs.EAbs $2 $4 $6 }
| Exp1 { $1 }
Exp3 :: { Alisaie.Abs.Exp }
Exp3 : Exp4 { $1 }
{
type Err = Either String
happyError :: [Token] -> Err a
happyError ts = Left $
"syntax error at " ++ tokenPos ts ++
case ts of
[] -> []
[Err _] -> " due to lexer error"
t:_ -> " before `" ++ (prToken t) ++ "'"
myLexer :: Data.Text.Text -> [Token]
myLexer = tokens
}

68
Alisaie/Parser.agda Normal file
View File

@ -0,0 +1,68 @@
-- File generated by the BNF Converter (bnfc 2.9.6.1).
-- Agda bindings for the Haskell parsers.
module Alisaie.Parser where
open import Agda.Builtin.Char using (Char)
open import Agda.Builtin.List using ([]; _∷_) renaming (List to #List)
open import Agda.Builtin.String using () renaming
( String to #String
; primStringFromList to #stringFromList
)
open import Alisaie.AST using
( Program
; Definition
; Kind
; Type
; Ident
; Exp
)
{-# FOREIGN GHC import Prelude (Bool, Char, Double, Integer, String, (.)) #-}
{-# FOREIGN GHC import qualified Data.Text #-}
{-# FOREIGN GHC import qualified Alisaie.ErrM #-}
{-# FOREIGN GHC import Alisaie.Par #-}
-- Error monad of BNFC
data Err A : Set where
ok : A → Err A
bad : #List Char → Err A
{-# COMPILE GHC Err = data Alisaie.ErrM.Err
( Alisaie.ErrM.Ok
| Alisaie.ErrM.Bad
) #-}
-- Happy parsers
postulate
parseProgram : #String → Err Program
parseDefinition : #String → Err Definition
parseKind : #String → Err Kind
parseKind1 : #String → Err Kind
parseType1 : #String → Err Type
parseType : #String → Err Type
parseListDefinition : #String → Err (#List Definition)
parseListIdent : #String → Err (#List Ident)
parseExp4 : #String → Err Exp
parseExp2 : #String → Err Exp
parseExp1 : #String → Err Exp
parseExp : #String → Err Exp
parseExp3 : #String → Err Exp
{-# COMPILE GHC parseProgram = pProgram . myLexer #-}
{-# COMPILE GHC parseDefinition = pDefinition . myLexer #-}
{-# COMPILE GHC parseKind = pKind . myLexer #-}
{-# COMPILE GHC parseKind1 = pKind1 . myLexer #-}
{-# COMPILE GHC parseType1 = pType1 . myLexer #-}
{-# COMPILE GHC parseType = pType . myLexer #-}
{-# COMPILE GHC parseListDefinition = pListDefinition . myLexer #-}
{-# COMPILE GHC parseListIdent = pListIdent . myLexer #-}
{-# COMPILE GHC parseExp4 = pExp4 . myLexer #-}
{-# COMPILE GHC parseExp2 = pExp2 . myLexer #-}
{-# COMPILE GHC parseExp1 = pExp1 . myLexer #-}
{-# COMPILE GHC parseExp = pExp . myLexer #-}
{-# COMPILE GHC parseExp3 = pExp3 . myLexer #-}

188
Alisaie/Print.hs Normal file
View File

@ -0,0 +1,188 @@
-- File generated by the BNF Converter (bnfc 2.9.6.1).
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
-- | Pretty-printer for Alisaie.
module Alisaie.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 Alisaie.Abs
import qualified Data.Text
-- | 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
(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 Alisaie.Abs.Ident where
prt _ (Alisaie.Abs.Ident i) = doc $ showString (Data.Text.unpack i)
instance Print Alisaie.Abs.UIdent where
prt _ (Alisaie.Abs.UIdent i) = doc $ showString (Data.Text.unpack i)
instance Print Alisaie.Abs.Program where
prt i = \case
Alisaie.Abs.Prog definitions -> prPrec i 0 (concatD [prt 0 definitions])
instance Print Alisaie.Abs.Definition where
prt i = \case
Alisaie.Abs.Def id_1 type_ id_2 ids exp -> prPrec i 0 (concatD [prt 0 id_1, doc (showString ":"), prt 0 type_, prt 0 id_2, prt 0 ids, doc (showString "="), prt 0 exp])
instance Print Alisaie.Abs.Kind where
prt i = \case
Alisaie.Abs.KStar -> prPrec i 0 (concatD [doc (showString "*")])
Alisaie.Abs.KArr kind1 kind2 -> prPrec i 1 (concatD [prt 0 kind1, doc (showString "\8594"), prt 0 kind2])
instance Print Alisaie.Abs.Type where
prt i = \case
Alisaie.Abs.TString -> prPrec i 1 (concatD [doc (showString "String")])
Alisaie.Abs.TInt -> prPrec i 1 (concatD [doc (showString "Int")])
Alisaie.Abs.TDouble -> prPrec i 1 (concatD [doc (showString "Double")])
Alisaie.Abs.TChar -> prPrec i 1 (concatD [doc (showString "Char")])
Alisaie.Abs.TCustom uident -> prPrec i 1 (concatD [prt 0 uident])
Alisaie.Abs.TArr type_1 type_2 -> prPrec i 0 (concatD [prt 1 type_1, doc (showString "\8594"), prt 0 type_2])
Alisaie.Abs.TForall id_ kind type_ -> prPrec i 0 (concatD [doc (showString "\8704"), prt 0 id_, doc (showString ":"), prt 0 kind, doc (showString "."), prt 0 type_])
Alisaie.Abs.TLambda id_ kind type_ -> prPrec i 0 (concatD [doc (showString "\955"), prt 0 id_, doc (showString ":"), prt 0 kind, doc (showString "."), prt 0 type_])
instance Print [Alisaie.Abs.Definition] where
prt _ [] = concatD []
prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
instance Print [Alisaie.Abs.Ident] where
prt _ [] = concatD []
prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
instance Print Alisaie.Abs.Exp where
prt i = \case
Alisaie.Abs.EVar id_ -> prPrec i 4 (concatD [prt 0 id_])
Alisaie.Abs.EInt n -> prPrec i 4 (concatD [prt 0 n])
Alisaie.Abs.EDouble d -> prPrec i 4 (concatD [prt 0 d])
Alisaie.Abs.EChar c -> prPrec i 4 (concatD [prt 0 c])
Alisaie.Abs.EText str -> prPrec i 4 (concatD [printString str])
Alisaie.Abs.EApp exp1 exp2 -> prPrec i 2 (concatD [prt 2 exp1, prt 3 exp2])
Alisaie.Abs.ETApp exp type_ -> prPrec i 2 (concatD [prt 2 exp, prt 0 type_])
Alisaie.Abs.EAdd exp1 exp2 -> prPrec i 1 (concatD [prt 1 exp1, doc (showString "+"), prt 2 exp2])
Alisaie.Abs.ESub exp1 exp2 -> prPrec i 1 (concatD [prt 1 exp1, doc (showString "-"), prt 2 exp2])
Alisaie.Abs.ELt exp1 exp2 -> prPrec i 1 (concatD [prt 1 exp1, doc (showString "<"), prt 2 exp2])
Alisaie.Abs.EIf exp1 exp2 exp3 -> prPrec i 0 (concatD [doc (showString "if"), prt 0 exp1, doc (showString "then"), prt 0 exp2, doc (showString "else"), prt 0 exp3])
Alisaie.Abs.ETAbs id_ kind exp -> prPrec i 0 (concatD [doc (showString "\923"), prt 0 id_, doc (showString ":"), prt 0 kind, doc (showString "."), prt 0 exp])
Alisaie.Abs.EAbs id_ type_ exp -> prPrec i 0 (concatD [doc (showString "\955"), prt 0 id_, doc (showString ":"), prt 0 type_, doc (showString "."), prt 0 exp])

64
Alisaie/Skel.hs Normal file
View File

@ -0,0 +1,64 @@
-- File generated by the BNF Converter (bnfc 2.9.6.1).
-- Templates for pattern matching on abstract syntax
{-# OPTIONS_GHC -Wno-unused-matches #-}
module Alisaie.Skel where
import Prelude (($), Either(..), String, (++), Show, show)
import qualified Alisaie.Abs
type Err = Either String
type Result = Err String
failure :: Show a => a -> Result
failure x = Left $ "Undefined case: " ++ show x
transIdent :: Alisaie.Abs.Ident -> Result
transIdent x = case x of
Alisaie.Abs.Ident string -> failure x
transUIdent :: Alisaie.Abs.UIdent -> Result
transUIdent x = case x of
Alisaie.Abs.UIdent string -> failure x
transProgram :: Alisaie.Abs.Program -> Result
transProgram x = case x of
Alisaie.Abs.Prog definitions -> failure x
transDefinition :: Alisaie.Abs.Definition -> Result
transDefinition x = case x of
Alisaie.Abs.Def ident1 type_ ident2 idents exp -> failure x
transKind :: Alisaie.Abs.Kind -> Result
transKind x = case x of
Alisaie.Abs.KStar -> failure x
Alisaie.Abs.KArr kind1 kind2 -> failure x
transType :: Alisaie.Abs.Type -> Result
transType x = case x of
Alisaie.Abs.TString -> failure x
Alisaie.Abs.TInt -> failure x
Alisaie.Abs.TDouble -> failure x
Alisaie.Abs.TChar -> failure x
Alisaie.Abs.TCustom uident -> failure x
Alisaie.Abs.TArr type_1 type_2 -> failure x
Alisaie.Abs.TForall ident kind type_ -> failure x
Alisaie.Abs.TLambda ident kind type_ -> failure x
transExp :: Alisaie.Abs.Exp -> Result
transExp x = case x of
Alisaie.Abs.EVar ident -> failure x
Alisaie.Abs.EInt integer -> failure x
Alisaie.Abs.EDouble double -> failure x
Alisaie.Abs.EChar char -> failure x
Alisaie.Abs.EText string -> failure x
Alisaie.Abs.EApp exp1 exp2 -> failure x
Alisaie.Abs.ETApp exp type_ -> failure x
Alisaie.Abs.EAdd exp1 exp2 -> failure x
Alisaie.Abs.ESub exp1 exp2 -> failure x
Alisaie.Abs.ELt exp1 exp2 -> failure x
Alisaie.Abs.EIf exp1 exp2 exp3 -> failure x
Alisaie.Abs.ETAbs ident kind exp -> failure x
Alisaie.Abs.EAbs ident type_ exp -> failure x

77
Alisaie/Test.hs Normal file
View File

@ -0,0 +1,77 @@
-- File generated by the BNF Converter (bnfc 2.9.6.1).
-- | Program to test parser.
module Main where
import Prelude
( ($), (.)
, Either(..)
, Int, (>)
, String, (++), concat, unlines
, Show, show
, IO, (>>), (>>=), mapM_, putStrLn
, FilePath
)
import Data.Text.IO ( getContents, readFile )
import qualified Data.Text
import System.Environment ( getArgs )
import System.Exit ( exitFailure )
import Control.Monad ( when )
import Alisaie.Abs ()
import Alisaie.Lex ( Token, mkPosToken )
import Alisaie.Par ( pProgram, myLexer )
import Alisaie.Print ( Print, printTree )
import Alisaie.Skel ()
type Err = Either String
type ParseFun a = [Token] -> Err a
type Verbosity = Int
putStrV :: Verbosity -> String -> IO ()
putStrV v s = when (v > 1) $ putStrLn s
runFile :: (Print a, Show a) => Verbosity -> ParseFun a -> FilePath -> IO ()
runFile v p f = putStrLn f >> readFile f >>= run v p
run :: (Print a, Show a) => Verbosity -> ParseFun a -> Data.Text.Text -> IO ()
run v p s =
case p ts of
Left err -> do
putStrLn "\nParse Failed...\n"
putStrV v "Tokens:"
mapM_ (putStrV v . showPosToken . mkPosToken) ts
putStrLn err
exitFailure
Right tree -> do
putStrLn "\nParse Successful!"
showTree v tree
where
ts = myLexer s
showPosToken ((l,c),t) = concat [ show l, ":", show c, "\t", show t ]
showTree :: (Show a, Print a) => Int -> a -> IO ()
showTree v tree = do
putStrV v $ "\n[Abstract Syntax]\n\n" ++ show tree
putStrV v $ "\n[Linearized tree]\n\n" ++ printTree tree
usage :: IO ()
usage = do
putStrLn $ unlines
[ "usage: Call with one of the following argument combinations:"
, " --help Display this help message."
, " (no arguments) Parse stdin verbosely."
, " (files) Parse content of files verbosely."
, " -s (files) Silent mode. Parse content of files silently."
]
main :: IO ()
main = do
args <- getArgs
case args of
["--help"] -> usage
[] -> getContents >>= run 2 pProgram
"-s":fs -> mapM_ (runFile 0 pProgram) fs
fs -> mapM_ (runFile 2 pProgram) fs

47
Makefile Normal file
View File

@ -0,0 +1,47 @@
## File generated by the BNF Converter (bnfc 2.9.6.1).
# Makefile for building the parser and test program.
AGDA = agda
GHC = ghc
HAPPY = happy
HAPPY_OPTS = --array --info --ghc --coerce
ALEX = alex
ALEX_OPTS = --ghc
# List of goals not corresponding to file names.
.PHONY : all clean distclean
# Default goal.
all : Alisaie/Test Main
# Rules for building the parser.
Alisaie/Abs.hs Alisaie/Lex.x Alisaie/Par.y Alisaie/Print.hs Alisaie/Test.hs Alisaie/AST.agda Alisaie/Parser.agda Alisaie/IOLib.agda Alisaie/Main.agda : Alisaie.cf
bnfc --haskell -d --agda Alisaie.cf
%.hs : %.y
${HAPPY} ${HAPPY_OPTS} $<
%.hs : %.x
${ALEX} ${ALEX_OPTS} $<
Alisaie/Test : Alisaie/Abs.hs Alisaie/Lex.hs Alisaie/Par.hs Alisaie/Print.hs Alisaie/Test.hs
${GHC} ${GHC_OPTS} $@
Main : Alisaie/Main.agda Alisaie/AST.agda Alisaie/Parser.agda Alisaie/IOLib.agda Alisaie/ErrM.hs Alisaie/Lex.hs Alisaie/Par.hs Alisaie/Print.hs
${AGDA} --no-libraries --ghc --ghc-flag=-Wwarn $<
# Rules for cleaning generated files.
clean :
-rm -f Alisaie/*.hi Alisaie/*.o Alisaie/*.log Alisaie/*.aux Alisaie/*.dvi Alisaie/*.agdai
-rm -rf MAlonzo
distclean : clean
-rm -f Alisaie/Abs.hs Alisaie/Abs.hs.bak Alisaie/ComposOp.hs Alisaie/ComposOp.hs.bak Alisaie/Doc.txt Alisaie/Doc.txt.bak Alisaie/ErrM.hs Alisaie/ErrM.hs.bak Alisaie/Layout.hs Alisaie/Layout.hs.bak Alisaie/Lex.x Alisaie/Lex.x.bak Alisaie/Par.y Alisaie/Par.y.bak Alisaie/Print.hs Alisaie/Print.hs.bak Alisaie/Skel.hs Alisaie/Skel.hs.bak Alisaie/Test.hs Alisaie/Test.hs.bak Alisaie/XML.hs Alisaie/XML.hs.bak Alisaie/AST.agda Alisaie/AST.agda.bak Alisaie/Parser.agda Alisaie/Parser.agda.bak Alisaie/IOLib.agda Alisaie/IOLib.agda.bak Alisaie/Main.agda Alisaie/Main.agda.bak Alisaie/Alisaie.dtd Alisaie/Alisaie.dtd.bak Alisaie/Test Alisaie/Lex.hs Alisaie/Par.hs Alisaie/Par.info Alisaie/ParData.hs Main Makefile
-rmdir -p Alisaie/
# EOF

2
example.ali Normal file
View File

@ -0,0 +1,2 @@
main : IO ()
main = putStrLn "Hejsan"

61
flake.lock generated Normal file
View File

@ -0,0 +1,61 @@
{
"nodes": {
"flake-parts": {
"inputs": {
"nixpkgs-lib": "nixpkgs-lib"
},
"locked": {
"lastModified": 1763759067,
"narHash": "sha256-LlLt2Jo/gMNYAwOgdRQBrsRoOz7BPRkzvNaI/fzXi2Q=",
"owner": "hercules-ci",
"repo": "flake-parts",
"rev": "2cccadc7357c0ba201788ae99c4dfa90728ef5e0",
"type": "github"
},
"original": {
"owner": "hercules-ci",
"repo": "flake-parts",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1764242076,
"narHash": "sha256-sKoIWfnijJ0+9e4wRvIgm/HgE27bzwQxcEmo2J/gNpI=",
"owner": "nixos",
"repo": "nixpkgs",
"rev": "2fad6eac6077f03fe109c4d4eb171cf96791faa4",
"type": "github"
},
"original": {
"owner": "nixos",
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-lib": {
"locked": {
"lastModified": 1761765539,
"narHash": "sha256-b0yj6kfvO8ApcSE+QmA6mUfu8IYG6/uU28OFn4PaC8M=",
"owner": "nix-community",
"repo": "nixpkgs.lib",
"rev": "719359f4562934ae99f5443f20aa06c2ffff91fc",
"type": "github"
},
"original": {
"owner": "nix-community",
"repo": "nixpkgs.lib",
"type": "github"
}
},
"root": {
"inputs": {
"flake-parts": "flake-parts",
"nixpkgs": "nixpkgs"
}
}
},
"root": "root",
"version": 7
}

40
flake.nix Normal file
View File

@ -0,0 +1,40 @@
{
description = "Alisaie";
inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
flake-parts.url = "github:hercules-ci/flake-parts";
};
outputs = inputs@{ nixpkgs, flake-parts, ... }:
flake-parts.lib.mkFlake {inherit inputs;} {
systems = [
"x86_64-linux"
];
perSystem = {self', pkgs, system, ...}: {
# packages.default = self'.packages.alisaie;
# packages.alisaie = pkgs.stdenv.mkDerivation {
# pname = "Alisaie";
# version = "0.0.1";
# src = ./.;
# nativeBuildInputs = with pkgs; [ ];
# buildInputs = [ ];
# };
devShells.default = pkgs.mkShell {
packages = with pkgs; [
(agda.withPackages (p: with p; [ standard-library ]))
(haskellPackages.BNFC)
(haskellPackages.alex)
(haskellPackages.happy)
];
};
};
};
}