Compare commits
2 Commits
master
...
new-syntax
Author | SHA1 | Date |
---|---|---|
James T. Martin | 950466c3e8 | |
James T. Martin | b53b1eb4d7 |
|
@ -1,26 +1,173 @@
|
|||
#!/usr/bin/env -S ivo -c
|
||||
|
||||
// syntax for algebraic data types
|
||||
type ℕ
|
||||
+ 0
|
||||
+ 1+ ℕ
|
||||
|
||||
type List a
|
||||
+ []
|
||||
+ _∷_ a (List a)
|
||||
|
||||
// syntax for algebraic codata types
|
||||
type Stream a
|
||||
& Head a
|
||||
& Tail (Stream a)
|
||||
|
||||
// syntax for generalized algebraic (co)data types
|
||||
type Vec a : ℕ → Type
|
||||
[] : Vec a 0
|
||||
_∷_ : ∀ n → a → Vec a n → Vec a (1+ n)
|
||||
|
||||
// syntax for mutually-recursive types
|
||||
types
|
||||
Even Odd : ℕ → Type
|
||||
|
||||
0even : Even 0
|
||||
1+odd : ∀ n → Odd n → Even (1+ n)
|
||||
1+even : ∀ n → Even n → Odd (1+ n)
|
||||
|
||||
// syntax for higher-inductive type
|
||||
type Multiset a
|
||||
empty : Multiset a
|
||||
singleton : a → Multiset a
|
||||
append : Multiset a → Multiset a → Multiset a
|
||||
|
||||
append_commutative : (x y : Multiset a) → append x y ≡ append y x
|
||||
|
||||
// syntax for inductive-recursive types? (needs work)
|
||||
types a _#_
|
||||
DList : Type
|
||||
Fresh : a → Dlist a → Type
|
||||
|
||||
[] : DList a
|
||||
_∷_#_ : (head : a) → (tail : DList a) → Fresh head tail → DList a
|
||||
|
||||
fresh[] : (x : a) → Fresh x []
|
||||
fresh∷ : (x : a) → (head : a) → (tail : DList a) → (p : Fresh head tail) → x # head → Fresh x tail → Fresh x (head ∷ tail # p)
|
||||
|
||||
// syntax for traits
|
||||
trait Functor f
|
||||
map : ∀ a b → (a → b) → f a → f b
|
||||
|
||||
// short for `open data type List a`
|
||||
// short for `open implicit trait Functor f`
|
||||
|
||||
// generated signatures
|
||||
sig
|
||||
ℕ : Type
|
||||
ℕ_Sig : Sig
|
||||
ℕ_Impl : ℕ_Sig
|
||||
|
||||
0 : ℕ
|
||||
1+ : ℕ → ℕ
|
||||
|
||||
pattern 0 1+
|
||||
complete 0 1+
|
||||
|
||||
ℕ_rec : ∀ a ⇒ a → ( a → a ) → ℕ → a
|
||||
ℕ_ind : (C : ℕ → Type) ⇒ C 0 → (∀ n → C n → C (1+ n)) → (n : ℕ) → C n
|
||||
|
||||
recurse : Sig → ...
|
||||
induct : Sig → ...
|
||||
baseFunctor : Sig → Sig
|
||||
|
||||
sig
|
||||
Functor : Type → Sig
|
||||
|
||||
map : ∀ f ⇒ Functor f ⇒ ∀ a b ⇒ (a → b) → f a → f b
|
||||
|
||||
|
||||
inductive type
|
||||
|
||||
type List a
|
||||
+ []
|
||||
+ _:+_ a (List a)
|
||||
|
||||
type Stream a
|
||||
& Head a
|
||||
& Tail (Stream a)
|
||||
|
||||
type Vec a : ℕ → Type
|
||||
[] : Vec a 0
|
||||
_:+_ : ∀ n → a → Vec a n → Vec a (1+ n)
|
||||
|
||||
sig
|
||||
ℕ : Type
|
||||
Z : ℕ
|
||||
S : ℕ → ℕ
|
||||
|
||||
sig
|
||||
List : Type → Type
|
||||
[] : ∀ a → List a
|
||||
_:+_ : ∀ a → a → List a → List a
|
||||
|
||||
sig
|
||||
Stream : Type → Type
|
||||
Head : ∀ a → Stream a → a
|
||||
Tail : ∀ a → Stream a → Stream a
|
||||
|
||||
iterate : ∀ a → (a → a) → a → ℕ → a
|
||||
iterate f x
|
||||
0 → []
|
||||
1+ n → x :+ iterate f (f x) n
|
||||
|
||||
iterate = \ f x n → case n {
|
||||
0 → [];
|
||||
1+ n → x :+ iterate f (f x) n;
|
||||
};
|
||||
|
||||
iterate f x = \case
|
||||
0 -> []
|
||||
1+ n -> x : iterate f (f x) n
|
||||
|
||||
append : ∀ a → List a → List a → List a
|
||||
append xs ys = case xs
|
||||
[] → ys
|
||||
x :+ xs → x :+ append xs ys
|
||||
|
||||
reverse : ∀ a → List a → List a
|
||||
reverse
|
||||
[] → []
|
||||
x :+ xs → append (reverse xs) [ x ]
|
||||
|
||||
churchℕ : Type
|
||||
churchℕ = ∀ a → (a → a) → a → a
|
||||
|
||||
churchS : churchℕ → churchℕ
|
||||
churchS n f x = f (n f x)
|
||||
|
||||
church+ : churchℕ → churchℕ → churchℕ
|
||||
church+ n = n churchS
|
||||
|
||||
// Create a list by iterating `f` `n` times:
|
||||
letrec iterate = \f x.
|
||||
{ Z -> []
|
||||
; S n -> (x :: iterate f (f x) n)
|
||||
};
|
||||
iterate = λ f x {
|
||||
Z → [];
|
||||
1+ n → x :+ iterate f (f x) n;
|
||||
};
|
||||
|
||||
// Use the iterate function to count to 10:
|
||||
let countToTen : [Nat] =
|
||||
let countTo = iterate S 1
|
||||
countToTen : [Nat] =
|
||||
let countTo = iterate +1 1
|
||||
in countTo 10;
|
||||
|
||||
// Append two lists together:
|
||||
letrec append = \xs ys.
|
||||
{ [] -> ys
|
||||
; (x :: xs) -> (x :: append xs ys)
|
||||
} xs;
|
||||
append = λ xs ys → case xs {
|
||||
[] → ys;
|
||||
x :+ xs → x :+ append xs ys;
|
||||
};
|
||||
|
||||
// Reverse a list:
|
||||
letrec reverse =
|
||||
{ [] -> []
|
||||
; (x :: xs) -> append (reverse xs) [x]
|
||||
};
|
||||
reverse = λ {
|
||||
[] → [];
|
||||
_:+_ x xs → append (reverse xs) [ x ]
|
||||
};
|
||||
|
||||
// Basic operations on church-encoded naturals.
|
||||
churchS = λ n f x → f (n f x);
|
||||
church+ = λ n → n churchS;
|
||||
|
||||
main =
|
||||
|
||||
// Now we can reverse `"reverse"`:
|
||||
let reverseReverse : [Char] = reverse "reverse";
|
||||
|
|
|
@ -41,6 +41,7 @@ default-extensions:
|
|||
- PatternSynonyms
|
||||
- ScopedTypeVariables
|
||||
- StandaloneDeriving
|
||||
- TupleSections
|
||||
- TypeFamilies
|
||||
- ViewPatterns
|
||||
|
||||
|
|
|
@ -1,152 +1,236 @@
|
|||
-- | The language's abstract syntax.
|
||||
--
|
||||
-- This source code does not document the concrete syntax in any detail;
|
||||
-- please refer to the language reference for more information about that.
|
||||
--
|
||||
-- This abstract syntax may include features which have not been implemented yet.
|
||||
-- The abstract syntax is very forward-thinking
|
||||
-- in that it's designed to accomodate for features
|
||||
-- which haven't been implemented yet,
|
||||
-- partly to make sure that I won't need to change it in a way
|
||||
-- that will involve rewriting lots of other code when I do implement those features.
|
||||
-- Plus, this serves as documentation for what the syntax /will/
|
||||
-- be and why I designed it to be the way it is.
|
||||
--
|
||||
-- That means that not all of this syntax is necessarily supported by the parser,
|
||||
-- and that even if it /is/, that the associated feature isn't necessarily
|
||||
-- implemented by the typechecker, interpreter, or compiler.
|
||||
module Ivo.Syntax.Base
|
||||
( Expr (..), ExprF (..), Ctr (..), Pat, Def, DefF (..), PatF (..), VoidF, Text, NonEmpty (..)
|
||||
, Type (..), TypeF (..), Scheme (..), tapp
|
||||
, substitute, substitute1, rename, rename1, free, bound, used
|
||||
, Parse, AST, ASTF, ASTX, ASTXF (..), NonEmptyDefFs (..)
|
||||
, pattern LetFP, pattern LetRecP, pattern LetRecFP
|
||||
, pattern PNat, pattern PNatF, pattern PList, pattern PListF, pattern PChar, pattern PCharF
|
||||
, pattern PStr, pattern PStrF, pattern HoleP, pattern HoleFP
|
||||
, simplify
|
||||
( Text, NonEmpty (..)
|
||||
, Scope (..), TopLevel (..), Definition (..), PublicOrPrivate (..)
|
||||
, Kind, Type, Expr (..), Sig (..), Sig' (..), Lit (..)
|
||||
, Pattern (..), Guard, CaseBranch (..)
|
||||
, FlexibleSeparatorSyntax
|
||||
) where
|
||||
|
||||
import Ivo.Expression.Base
|
||||
import Data.List.NonEmpty (NonEmpty (..))
|
||||
import Data.Text (Text)
|
||||
|
||||
import Data.Functor.Foldable (embed, project)
|
||||
import Data.List.NonEmpty (NonEmpty (..), toList)
|
||||
import Data.Text qualified as T
|
||||
newtype Scope = Scope [Definition]
|
||||
deriving Show
|
||||
|
||||
data Parse
|
||||
-- | The abstract syntax tree reflects the structure of the externally-visible syntax.
|
||||
--
|
||||
-- It includes syntactic sugar, which allows multiple ways to express many constructions,
|
||||
-- e.g. multiple definitions in a single let expression or multiple names bound by one abstraction.
|
||||
type AST = Expr Parse
|
||||
-- There is no technical reason that the AST can't allow nullary applications and so forth,
|
||||
-- nor is there any technical reason that the parser couldn't parse them,
|
||||
-- but the parser *does* reject them to avoid confusing edge cases like `let x=in`,
|
||||
-- so they're forbidden here too so that the syntax tree can't contain data
|
||||
--
|
||||
-- that the parser would refuse to accept.
|
||||
-- As a matter of curiosity, here's why `let x=in` was syntactically valid:
|
||||
-- 1. Parentheses in `let` statements are optional, infer them: `let x=()in()`.
|
||||
-- 2. Insert optional whitespace: `let x = () in ()`.
|
||||
-- 3. Nullary application expands to the identity function because
|
||||
-- the identity function is the left identity of function application:
|
||||
-- `let x=(\x.x) in \x.x`.
|
||||
type instance AppArgs Parse = NonEmpty AST
|
||||
type instance AbsArgs Parse = NonEmpty Text
|
||||
type instance LetArgs Parse = NonEmpty (Def Parse)
|
||||
type instance CtrArgs Parse = [AST]
|
||||
type instance AnnX Parse = ()
|
||||
type instance XExpr Parse = ASTX
|
||||
data Definition = Definition Visibility Item
|
||||
|
||||
type ASTX = ASTXF AST
|
||||
-- | 'Public' is written with @pub@;
|
||||
-- 'Private' indicates the abscence of an access modifier.
|
||||
data Visibility = Public | Private
|
||||
|
||||
type ASTF = ExprF Parse
|
||||
type instance AppArgsF Parse = NonEmpty
|
||||
type instance LetArgsF Parse = NonEmptyDefFs
|
||||
type instance CtrArgsF Parse = []
|
||||
type instance XExprF Parse = ASTXF
|
||||
data Item
|
||||
-- | @<name> <patterns...> = <expression>@
|
||||
-- or @<name> <patterns...> <case branches>@
|
||||
= Def Text [Pattern] CaseBranches
|
||||
-- | @<names...> : <type>@
|
||||
| Decl (NonEmpty Text) Type
|
||||
-- | @open <expr> <using>? <hiding>? <renaming>?
|
||||
| Open Expr (Maybe OpenUsing) (Maybe OpenHiding) (Maybe OpenRenaming)
|
||||
-- | @<pat|copat> <name> <names...> = <pattern>@
|
||||
| PatSyn Bool Text [Text] Pattern
|
||||
-- | @<pat|copat> <names...> [: <type>]?@
|
||||
| PatDecl Bool [Text] (Maybe Type)
|
||||
-- | @complete <names...> [: <type>]?@
|
||||
| Complete [Text] (Maybe Type)
|
||||
-- | @infix <fixity> <names...>@
|
||||
| FixityDecl Fixity (NonEmpty Text)
|
||||
-- | @implicit <expr> [: <type>]?@
|
||||
| Implicit Expr (Maybe Type)
|
||||
-- | @data <expr>@
|
||||
| DataStmt Expr
|
||||
-- | @axiom <expr>@
|
||||
| AxiomStmt Expr
|
||||
-- | @axioms <scope>@
|
||||
| AxiomsStmt Scope
|
||||
-- | @type <type decl>@
|
||||
| TypeStmt TypeDecl
|
||||
-- | @types <scope>@
|
||||
| TypesStmt Scope
|
||||
-- | @trait <trait decl>@
|
||||
| TraitStmt TraitDecl
|
||||
-- | @record <record impl>@
|
||||
| RecordStmt RecordImpl
|
||||
deriving Show
|
||||
|
||||
data ASTXF r
|
||||
-- | A let expression where the definitions may reference each other recursively.
|
||||
= LetRecP_ !(Text, r) !r
|
||||
-- | A natural number literal, e.g. `10`.
|
||||
| PNat_ Int
|
||||
-- | A list literal, e.g. `[x, y, z]`.
|
||||
| PList_ [r]
|
||||
-- | A character literal, e.g. `'a`.
|
||||
| PChar_ Char
|
||||
-- | A string literal, e.g. `"abcd"`.
|
||||
| PStr_ Text
|
||||
-- | A type hole.
|
||||
| HoleP_
|
||||
deriving (Eq, Functor, Foldable, Traversable, Show)
|
||||
-- | @using (pub? pat? <name>; ...)@
|
||||
type OpenUsing = [(Visibility, Bool, Text)]
|
||||
|
||||
instance RecursivePhase Parse where
|
||||
projectLetArgs = NonEmptyDefFs
|
||||
embedLetArgs = getNonEmptyDefFs
|
||||
-- | @hiding (complete <name>+ or @pat? <name>; ...)@
|
||||
type OpenHiding = [Either [Text] (Bool, Text)]
|
||||
|
||||
newtype NonEmptyDefFs r = NonEmptyDefFs { getNonEmptyDefFs :: NonEmpty (Text, r) }
|
||||
deriving (Eq, Functor, Foldable, Traversable, Show)
|
||||
-- | @renaming (pat? <name> → pub? <fixity>? <name>; ...)@
|
||||
type OpenRenaming = [(Text, Text)]
|
||||
|
||||
pattern LetFP :: NonEmpty (Text, r) -> r -> ASTF r
|
||||
pattern LetFP ds e = LetF (NonEmptyDefFs ds) e
|
||||
-- | @fixity <associativity>? <precedence>@
|
||||
data Fixity = Fixity (Maybe Associativity) Precedence
|
||||
|
||||
pattern LetRecP :: (Text, AST) -> AST -> AST
|
||||
pattern LetRecP d e = ExprX (LetRecP_ d e)
|
||||
-- | @<left|right>@
|
||||
data Associativity = AssocLeft | AssocRight
|
||||
|
||||
pattern LetRecFP :: (Text, r) -> r -> ASTF r
|
||||
pattern LetRecFP d e = ExprXF (LetRecP_ d e)
|
||||
-- | @<+|->?digit+[.digit+]?@
|
||||
type Precedence = Text
|
||||
|
||||
pattern PNat :: Int -> AST
|
||||
pattern PNat n = ExprX (PNat_ n)
|
||||
-- | An expression which represents the type of a type.
|
||||
type Kind = Type
|
||||
-- | An expression which represents the type of a value.
|
||||
type Type = Expr
|
||||
| Complete [Text] (Maybe Type)
|
||||
-- | @infix <fixity> <names...>@
|
||||
| FixityDecl Fixity (NonEmpty Text)
|
||||
-- | @implicit <expr> [: <type>]?@
|
||||
| Implicit Expr (Maybe Type)
|
||||
-- | @data <expr>@
|
||||
| DataStmt Expr
|
||||
-- | @axiom <expr>@
|
||||
| AxiomStmt Expr
|
||||
-- | @axioms <scope>@
|
||||
| AxiomsStmt Scope
|
||||
-- | @type <type decl>@
|
||||
| TypeStmt TypeDecl
|
||||
-- | @types <scope>@
|
||||
| TypesStmt Scope
|
||||
-- | @trait <trait decl>@
|
||||
| TraitStmt TraitDecl
|
||||
-- | @record <record impl>@
|
||||
| RecordStmt RecordImpl
|
||||
deriving Show
|
||||
|
||||
pattern PNatF :: Int -> ASTF r
|
||||
pattern PNatF n = ExprXF (PNat_ n)
|
||||
-- | @using (pub? pat? <name>; ...)@
|
||||
type OpenUsing = [(Visibility, Bool, Text)]
|
||||
|
||||
pattern PList :: [AST] -> AST
|
||||
pattern PList es = ExprX (PList_ es)
|
||||
-- | @hiding (complete <name>+ or @pat? <name>; ...)@
|
||||
type OpenHiding = [Either [Text] (Bool, Text)]
|
||||
|
||||
pattern PListF :: [r] -> ASTF r
|
||||
pattern PListF es = ExprXF (PList_ es)
|
||||
-- | @renaming (pat? <name> → pub? <fixity>? <name>; ...)@
|
||||
type OpenRenaming = [(Text, Text)]
|
||||
|
||||
pattern PChar :: Char -> AST
|
||||
pattern PChar c = ExprX (PChar_ c)
|
||||
-- | @fixity <associativity>? <precedence>@
|
||||
data Fixity = Fixity (Maybe Associativity) Precedence
|
||||
|
||||
pattern PCharF :: Char -> ASTF r
|
||||
pattern PCharF c = ExprXF (PChar_ c)
|
||||
-- | @<left|right>@
|
||||
data Associativity = AssocLeft | AssocRight
|
||||
|
||||
pattern PStrF :: Text -> ASTF r
|
||||
pattern PStrF s = ExprXF (PStr_ s)
|
||||
-- | @<+|->?digit+[.digit+]?@
|
||||
type Precedence = Text
|
||||
|
||||
pattern PStr :: Text -> AST
|
||||
pattern PStr s = ExprX (PStr_ s)
|
||||
-- | An expression which represents the type of a type.
|
||||
type Kind = Type
|
||||
-- | An expression which represents the type of a value.
|
||||
type Type = Expr
|
||||
|
||||
pattern HoleP :: AST
|
||||
pattern HoleP = ExprX HoleP_
|
||||
data Expr
|
||||
= Data Expr
|
||||
| Axiom Expr
|
||||
-- | A signature literal. See 'ADT', 'GADT', and 'Sig' for examples.
|
||||
| SigE Sig
|
||||
| Mod [Either (NonEmpty Text, Kind) Text] (Maybe Type) [TopLevel]
|
||||
| Access Expr Text
|
||||
|
||||
pattern HoleFP :: ASTF r
|
||||
pattern HoleFP = ExprXF HoleP_
|
||||
---
|
||||
--- Expressions pertaining to types
|
||||
---
|
||||
|
||||
{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, AnnF, ExprXF #-}
|
||||
{-# COMPLETE Var, App, Abs, Let, Ctr, Case, Ann, LetRecP, PNat, PList, PChar, PStr, HoleP #-}
|
||||
{-# COMPLETE VarF, AppF, AbsF, LetF , CtrF, CaseF, AnnF, LetRecFP, PNatF, PListF, PCharF, PStrF, HoleFP #-}
|
||||
{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, AnnF, LetRecFP, PNatF, PListF, PCharF, PStrF, HoleFP #-}
|
||||
| Forall (NonEmpty (Either (NonEmpty Text, Kind) Text)) Type
|
||||
| Arrow [Text] Type Type
|
||||
-- | Type annotations (or kind annotations; they are the same thing).
|
||||
--
|
||||
-- > foo : bar
|
||||
| Ann Expr Type
|
||||
| Hole
|
||||
|
||||
-- TODO: Implement Substitutable for AST.
|
||||
---
|
||||
--- Expressions pertaining to values
|
||||
---
|
||||
|
||||
-- | Combine nested expressions into compound expressions or literals when possible.
|
||||
simplify :: AST -> AST
|
||||
simplify = simplify' . embed . fmap simplify . project
|
||||
where
|
||||
-- Combine sequences of nat constructors into literals.
|
||||
simplify' (Ctr CZero []) = PNat 0
|
||||
simplify' (Ctr CSucc [PNat n]) = PNat (n + 1)
|
||||
-- Combine sequences of string constructors into string literals.
|
||||
simplify' (Ctr CChar [PNat n]) = PChar (toEnum n)
|
||||
simplify' o@(Ctr CCons [PChar c, PList []])
|
||||
| c /= '"' = PStr (T.singleton c)
|
||||
| otherwise = o
|
||||
simplify' o@(Ctr CCons [PChar c, PStr cs])
|
||||
| c /= '"' = PStr (T.cons c cs)
|
||||
| otherwise = o
|
||||
-- Combine sequences of list contructors into list literals.
|
||||
simplify' (Ctr CNil []) = PList []
|
||||
simplify' (Ctr CCons [x, PList xs]) = PList (x : xs)
|
||||
-- Move applications into constructors.
|
||||
simplify' (App (Ctr ctr es1) es2) = simplify' $ Ctr ctr (es1 <> toList es2)
|
||||
-- Combine reducible applications into let expressions.
|
||||
simplify' (App (Abs (nx :| ns) eb) (ex :| es)) = simplify' $ app' es $ Let ((nx, ex) :| []) $ abs' ns eb
|
||||
where app' [] e = e
|
||||
app' (ex2:es2) e = App e (ex2 :| es2)
|
||||
| TypeLam (NonEmpty (Either (NonEmpty Text, Kind) Text)) Expr
|
||||
| TypeApp Expr Type
|
||||
| Lam [Pattern] [CaseBranch]
|
||||
-- | A lambda with only one, trivial branch, e.g. @λ x y z -> e@.
|
||||
--
|
||||
-- See 'Lam'.
|
||||
| LamBlock [Pattern] Expr
|
||||
| App Expr (NonEmpty Expr)
|
||||
| AppI Text (NonEmpty Expr)
|
||||
| Let [TopLevel] Expr
|
||||
| Case [Expr] [CaseBranch]
|
||||
-- | A case with only one, trivial branch, e.g.
|
||||
-- @case x | y of a , b | c , d → e@.
|
||||
--
|
||||
-- See 'Case'.
|
||||
| CaseBlock [Expr] [Pattern] Expr
|
||||
-- | Integer, string, character, and list literals.
|
||||
| Lit (Lit Expr)
|
||||
-- | Variables.
|
||||
| Var Text
|
||||
deriving Show
|
||||
|
||||
abs' [] e = e
|
||||
abs' (nx2:ns2) e = Abs (nx2 :| ns2) e
|
||||
-- Combine sequences of nested applications into n-ary applications.
|
||||
simplify' (App (App f es1) es2) = simplify' $ App f (es1 <> es2)
|
||||
-- Combine sequences of nested abstractions into n-argument abstractions.
|
||||
simplify' (Abs ns1 (Abs ns2 e)) = simplify' $ Abs (ns1 <> ns2) e
|
||||
-- Combine sequences of nested let expressions into n-definition let expressions.
|
||||
simplify' (Let ds1 (Let ds2 e)) = simplify' $ Let (ds1 <> ds2) e
|
||||
simplify' e = e
|
||||
data Sig
|
||||
= SigQs [Either (NonEmpty Text, Kind) Text] Sig'
|
||||
deriving Show
|
||||
|
||||
data Sig'
|
||||
= ADT Bool Text (Maybe Kind) [(Text, [Type])]
|
||||
| GADT Text (Maybe Kind) [(NonEmpty Text, Type)]
|
||||
| Sig [Either (NonEmpty Text, Type) TopLevel]
|
||||
deriving Show
|
||||
|
||||
data Pattern
|
||||
= PatVar Text (Maybe Type)
|
||||
-- | @_@
|
||||
| Irrelevant
|
||||
-- | @!@
|
||||
| Impossible
|
||||
| PatApp Text [Pattern]
|
||||
| PatAppI Text (NonEmpty Pattern)
|
||||
-- | @<pat> ← <expr>@
|
||||
| View Expr Pattern
|
||||
| PatLit (Lit Pattern)
|
||||
deriving Show
|
||||
|
||||
-- | @<pat> [| <pat> ...]? <refinements...>? [<guard>? → <expr>]?@
|
||||
data CaseBranch
|
||||
= Refinement [Pattern] [Expr] (NonEmpty CaseBranch)
|
||||
|
||||
| Guards [Pattern] (NonEmpty (Guard, Expr))
|
||||
-- | A case branch without refinement or guards.
|
||||
| PlainCase [Pattern] Expr
|
||||
deriving Show
|
||||
|
||||
type Guard = [Either (Pattern, Expr) Expr]
|
||||
|
||||
-- | Special syntactic support for a few very important types.
|
||||
data Lit r
|
||||
-- | @12310@, @+1338848@, @-131@
|
||||
= LitInt Integer
|
||||
-- | @'a@, @'#@, @'\n@,
|
||||
| LitChar Char
|
||||
-- | @"And so I said, \"this language SUCKS!\""@
|
||||
| LitStr Text
|
||||
-- | @[ x ; y ; z ]@, @[ ]@
|
||||
--
|
||||
-- Note that to minimize the number of reserved characters,
|
||||
-- (so that e.g. @[]@ can be a constructor name and not just syntax)
|
||||
-- square brackets are /keywords/ and not /tokens/,
|
||||
-- so e.g. in @[x ; y]@, @[x@ and @y]@ are /identifiers/.
|
||||
-- You /must/ leave a space: @[ x ; y ]@.
|
||||
--
|
||||
-- This uses 'FlexibleSeparatorSyntax'.
|
||||
| LitList [r]
|
||||
deriving Show
|
||||
|
|
|
@ -1,305 +1,606 @@
|
|||
module Ivo.Syntax.Parser
|
||||
( ParseError, parse
|
||||
, Declaration, TopLevelAST, ProgramAST
|
||||
, parseAST, parseTopLevel, parseProgram
|
||||
, typeParser, schemeParser, astParser, topLevelParser, programParser
|
||||
, programParser, replParser
|
||||
) where
|
||||
|
||||
import Ivo.Syntax.Base
|
||||
|
||||
import Data.Functor.Identity (Identity)
|
||||
import Data.List.NonEmpty (fromList)
|
||||
import Data.Text qualified as T
|
||||
import Prelude hiding (succ, either)
|
||||
import Text.Parsec hiding (label, token, spaces)
|
||||
import Text.Parsec hiding (label, token, spaces, tokens, anyToken)
|
||||
import Text.Parsec qualified
|
||||
import Text.Parsec.Expr
|
||||
import Text.Parsec.Text (Parser)
|
||||
|
||||
spaces :: Parser ()
|
||||
spaces = Text.Parsec.spaces >> optional (try (comment >> spaces))
|
||||
where
|
||||
comment, lineComment, blockComment :: Parser ()
|
||||
comment = blockComment <|> lineComment
|
||||
lineComment = label "line comment" $ do
|
||||
_ <- try (string "//")
|
||||
_ <- many1 (noneOf "\n")
|
||||
pure ()
|
||||
blockComment = label "block comment" $ do
|
||||
_ <- try (string "/*")
|
||||
_ <- many1 $ notFollowedBy (string "*/") >> anyChar
|
||||
_ <- string "*/"
|
||||
pure ()
|
||||
-- | Parse the contents of a file containing Ivo source code,
|
||||
-- with an optional shebang.
|
||||
--
|
||||
-- See 'Scope'.
|
||||
programParser :: Parser Scope
|
||||
programParser = do
|
||||
optional shebang
|
||||
scope
|
||||
|
||||
label :: String -> Parser a -> Parser a
|
||||
label = flip Text.Parsec.label
|
||||
-- | Parse REPL input (which consists of top-level statements and expressions).
|
||||
--
|
||||
-- See 'TopLevel' and 'Expr'.
|
||||
replParser :: Parser [Either TopLevel Expr]
|
||||
replParser = sepEndBy ((Left <$> topLevel) <|> (Right <$> ambiguous)) (token ";")
|
||||
|
||||
token :: Char -> Parser ()
|
||||
token ch = label [ch] $ char ch *> spaces
|
||||
|
||||
keywords :: [Text]
|
||||
keywords = ["let", "in", "Left", "Right", "S", "Z", "forall", "Char", "Void", "Unit", "Nat", "Char"]
|
||||
|
||||
-- | A keyword is an exact string which is not part of an identifier.
|
||||
keyword :: Text -> Parser ()
|
||||
keyword kwd = label (T.unpack kwd) $ do
|
||||
try do
|
||||
_ <- string $ T.unpack kwd
|
||||
notFollowedBy letter
|
||||
spaces
|
||||
|
||||
-- | An identifier is a sequence of letters which is not a keyword.
|
||||
identifier :: Parser Text
|
||||
identifier = label "identifier" $ do
|
||||
notFollowedBy anyKeyword
|
||||
T.pack <$> (many1 letter <* spaces)
|
||||
where anyKeyword = choice $ map keyword keywords
|
||||
|
||||
variable :: Parser AST
|
||||
variable = label "variable" $ Var <$> identifier
|
||||
|
||||
tvariable :: Parser Type
|
||||
tvariable = label "variable" $ TVar <$> identifier
|
||||
|
||||
many1' :: Parser a -> Parser (NonEmpty a)
|
||||
many1' p = fromList <$> many1 p
|
||||
|
||||
many2 :: Parser a -> Parser (a, NonEmpty a)
|
||||
many2 p = (,) <$> p <*> many1' p
|
||||
|
||||
grouping :: Parser AST
|
||||
grouping = label "grouping" $ between (token '(') (token ')') ambiguous
|
||||
|
||||
tgrouping :: Parser Type
|
||||
tgrouping = label "grouping" $ between (token '(') (token ')') tambiguous
|
||||
|
||||
application :: Parser AST
|
||||
application = label "application" $ uncurry App <$> many2 block
|
||||
|
||||
tapplication :: Parser Type
|
||||
tapplication = label "application" $ uncurry tapp' <$> many2 tblock
|
||||
where tapp' t1 (t2 :| ts) = tapp (t1 : t2 : ts)
|
||||
|
||||
abstraction :: Parser AST
|
||||
abstraction = label "lambda abstraction" $ Abs <$> between lambda (token '.') (many1' identifier) <*> ambiguous
|
||||
where lambda = label "lambda" $ (char '\\' <|> char 'λ') *> spaces
|
||||
|
||||
definition :: Parser (Def Parse)
|
||||
definition = label "definition" $ do
|
||||
name <- identifier
|
||||
token '='
|
||||
value <- ambiguous
|
||||
pure (name, value)
|
||||
|
||||
let_ :: Parser AST
|
||||
let_ = label "let expression" $ letrecstar <|> letstar
|
||||
where
|
||||
letrecstar = LetRecP <$> between (try (keyword "letrec")) (keyword "in") definition <*> ambiguous
|
||||
letstar = Let <$> between (keyword "let") (keyword "in") definitions <*> ambiguous
|
||||
|
||||
definitions :: Parser (NonEmpty (Def Parse))
|
||||
definitions = fromList <$> sepBy1 definition (token ';')
|
||||
|
||||
ctr :: Parser AST
|
||||
ctr = label "data constructor" $ pair <|> unit <|> either <|> nat <|> list <|> str
|
||||
where
|
||||
unit, pairCtr, tuple, either, left, right,
|
||||
zero, succ, natLit, consCtr, cons, charCtr, charLit, strLit :: Parser AST
|
||||
unit = Ctr CUnit [] <$ keyword "()"
|
||||
pair = pairCtr <|> tuple
|
||||
pairCtr = Ctr CPair [] <$ keyword "(,)"
|
||||
tuple = try $ between (token '(') (token ')') do
|
||||
e1 <- ambiguous
|
||||
token ','
|
||||
e2 <- ambiguous
|
||||
pure $ Ctr CPair [e1, e2]
|
||||
either = left <|> right
|
||||
left = Ctr CLeft [] <$ keyword "Left"
|
||||
right = Ctr CRight [] <$ keyword "Right"
|
||||
nat = zero <|> succ <|> natLit
|
||||
zero = Ctr CZero [] <$ keyword "Z"
|
||||
succ = Ctr CSucc [] <$ keyword "S"
|
||||
natLit = (PNat . read <$> many1 digit) <* spaces
|
||||
list = cons <|> consCtr <|> listLit
|
||||
consCtr = Ctr CCons [] <$ keyword "(::)"
|
||||
cons = try $ between (token '(') (token ')') do
|
||||
e1 <- ambiguous
|
||||
keyword "::"
|
||||
e2 <- ambiguous
|
||||
pure $ Ctr CCons [e1, e2]
|
||||
listLit = fmap PList $ between (token '[') (token ']') $ sepEndBy ambiguous (token ',')
|
||||
str = charCtr <|> charLit <|> strLit
|
||||
charCtr = Ctr CChar [] <$ keyword "Char"
|
||||
charLit = fmap PChar $ char '\'' *> anyChar <* spaces
|
||||
strLit = fmap (PStr . T.pack) $ between (token '"') (token '"') $ many (noneOf "\"")
|
||||
|
||||
pat :: Parser (Pat Parse)
|
||||
pat = label "case alternate" $ do
|
||||
(c, ns) <- label "pattern" $
|
||||
pair <|> unit <|> left <|> right <|> zero <|> succ <|> nil <|> cons <|> char'
|
||||
keyword "->"
|
||||
e <- ambiguous
|
||||
pure $ Pat c ns e
|
||||
where
|
||||
pair = try $ between (token '(') (token ')') do
|
||||
e1 <- identifier
|
||||
token ','
|
||||
e2 <- identifier
|
||||
pure (CPair, [e1, e2])
|
||||
unit = (CUnit, []) <$ keyword "()"
|
||||
left = do
|
||||
keyword "Left"
|
||||
e <- identifier
|
||||
pure (CLeft, [e])
|
||||
right = do
|
||||
keyword "Right"
|
||||
e <- identifier
|
||||
pure (CRight, [e])
|
||||
zero = (CZero, []) <$ keyword "Z"
|
||||
succ = do
|
||||
keyword "S"
|
||||
e <- identifier
|
||||
pure (CSucc, [e])
|
||||
nil = (CNil, []) <$ keyword "[]"
|
||||
cons = try $ between (token '(') (token ')') do
|
||||
e1 <- identifier
|
||||
keyword "::"
|
||||
e2 <- identifier
|
||||
pure (CCons, [e1, e2])
|
||||
char' = do
|
||||
keyword "Char"
|
||||
e <- identifier
|
||||
pure (CChar, [e])
|
||||
|
||||
case_ :: Parser AST
|
||||
case_ = label "case patterns" $ do
|
||||
token '{'
|
||||
pats <- sepEndBy pat (token ';')
|
||||
token '}'
|
||||
pure $ Case pats
|
||||
|
||||
ann :: Parser AST
|
||||
ann = label "type annotation" $ do
|
||||
e <- block
|
||||
token ':'
|
||||
t <- tambiguous
|
||||
pure (Ann () e t)
|
||||
|
||||
hole :: Parser AST
|
||||
hole = label "hole" $ HoleP <$ token '_'
|
||||
|
||||
tlist :: Parser Type
|
||||
tlist = between (token '[') (token ']') $ ((TApp TList <$> tambiguous) <|> pure TList)
|
||||
|
||||
tinfix :: Parser Type
|
||||
tinfix = buildExpressionParser ttable tblock
|
||||
where
|
||||
ttable :: [[Operator Text () Identity Type]]
|
||||
ttable = [ [Infix (binop TAbs <$ arrSym) AssocRight]
|
||||
, [Infix (binop TProd <$ token '*') AssocRight]
|
||||
, [Infix (binop TSum <$ token '+') AssocRight]
|
||||
]
|
||||
|
||||
arrSym :: Parser ()
|
||||
arrSym = token '→' <|> keyword "->"
|
||||
|
||||
binop :: Type -> Type -> Type -> Type
|
||||
binop c t1 t2 = TApp (TApp c t1) t2
|
||||
|
||||
tctr :: Parser Type
|
||||
tctr = tlist <|> tunit <|> tvoid <|> tnat <|> tchar
|
||||
where
|
||||
tunit = TUnit <$ (keyword "Unit" <|> keyword "⊤")
|
||||
tvoid = TVoid <$ (keyword "Void" <|> keyword "⊥")
|
||||
tnat = TNat <$ (keyword "Nat" <|> keyword "ℕ")
|
||||
tchar = TChar <$ keyword "Char"
|
||||
|
||||
tfinite :: Parser Type
|
||||
tfinite = tvariable <|> tlist <|> tctr <|> tgrouping
|
||||
|
||||
tblock :: Parser Type
|
||||
tblock = tfinite
|
||||
|
||||
tambiguous :: Parser Type
|
||||
tambiguous = try tinfix <|> try tapplication <|> tblock
|
||||
|
||||
tforall :: Parser Scheme
|
||||
tforall = do
|
||||
keyword "forall" <|> token '∀'
|
||||
names <- many1 (identifier <* spaces)
|
||||
token '.'
|
||||
ty <- tambiguous
|
||||
pure $ TForall names ty
|
||||
|
||||
scheme :: Parser Scheme
|
||||
scheme = tforall <|> (TForall [] <$> tambiguous)
|
||||
|
||||
-- | Guaranteed to consume a finite amount of input
|
||||
finite :: Parser AST
|
||||
finite = label "finite expression" $ variable <|> hole <|> ctr <|> case_ <|> grouping
|
||||
|
||||
-- | Guaranteed to consume input, but may continue until it reaches a terminator
|
||||
block :: Parser AST
|
||||
block = label "block expression" $ abstraction <|> let_ <|> finite
|
||||
|
||||
-- | Not guaranteed to consume input at all, may continue until it reaches a terminator
|
||||
ambiguous :: Parser AST
|
||||
ambiguous = label "any expression" $ try ann <|> try application <|> block
|
||||
|
||||
typeParser :: Parser Type
|
||||
typeParser = tambiguous
|
||||
|
||||
schemeParser :: Parser Scheme
|
||||
schemeParser = scheme
|
||||
|
||||
astParser :: Parser AST
|
||||
astParser = ambiguous
|
||||
|
||||
parseAST :: Text -> Either ParseError AST
|
||||
parseAST = parse (spaces *> ambiguous <* eof) "input"
|
||||
|
||||
type Declaration = (Text, Maybe Type, AST)
|
||||
|
||||
definitionAnn :: Parser Declaration
|
||||
definitionAnn = do
|
||||
name <- identifier
|
||||
ty <- optionMaybe $ token ':' *> tambiguous
|
||||
token '='
|
||||
e <- ambiguous
|
||||
pure (name, ty, e)
|
||||
|
||||
declaration :: Parser Declaration
|
||||
declaration = notFollowedBy (try let_) >> (declrec <|> decl)
|
||||
where
|
||||
declrec = do
|
||||
try $ keyword "letrec"
|
||||
(name, ty, expr) <- definitionAnn
|
||||
pure (name, ty, LetRecP (name, expr) (Var name))
|
||||
decl = do
|
||||
keyword "let"
|
||||
definitionAnn
|
||||
|
||||
-- | A program is a series of declarations and expressions to execute.
|
||||
type ProgramAST = [Declaration]
|
||||
type TopLevelAST = [Either Declaration AST]
|
||||
|
||||
topLevel :: Parser (Either Declaration AST)
|
||||
topLevel = try (Left <$> declaration) <|> (Right <$> ambiguous)
|
||||
|
||||
topLevelParser :: Parser TopLevelAST
|
||||
topLevelParser = spaces *> sepEndBy topLevel (token ';') <* eof
|
||||
---
|
||||
--- This is a very long module which does not even document the
|
||||
--- syntactic constructs which it is implementing.
|
||||
--- On the other hand, 'Ivo.Syntax.Base' goes into great detail'
|
||||
--- about the syntax while hardly containing any actual code.
|
||||
--- Thus, to assist with navigation, the order
|
||||
--- in which parsers are defined in this module
|
||||
--- is the same as the order in which they are described in 'Ivo.Syntax.Base'.
|
||||
--- I would recommend keeping both files open at once while working on this code
|
||||
--- so you can cross-reference the informal description of the syntax
|
||||
--- with the parsers.
|
||||
---
|
||||
|
||||
shebang :: Parser ()
|
||||
shebang = do
|
||||
shebang = label "shebang" do
|
||||
try $ keyword "#!"
|
||||
skipMany (noneOf "\n")
|
||||
spaces
|
||||
|
||||
programParser :: Parser ProgramAST
|
||||
programParser = shebang *> sepEndBy declaration (token ';') <* eof
|
||||
-- | 'Scope'
|
||||
scope :: Parser Scope
|
||||
scope = Scope <$> many (topLevel <* token ";")
|
||||
|
||||
parseTopLevel :: Text -> Either ParseError TopLevelAST
|
||||
parseTopLevel = parse topLevelParser "input"
|
||||
topLevel, tlOpen, tlDef, tlData, tlAxiom, tlSig :: Parser TopLevel
|
||||
|
||||
parseProgram :: Text -> Either ParseError ProgramAST
|
||||
parseProgram = parse programParser "input"
|
||||
-- | 'TopLevel'
|
||||
topLevel = tlOpen <|> tlDef <|> tlData <|> tlAxiom <|> tlSig
|
||||
|
||||
-- | 'Open'
|
||||
tlOpen = label "open statement" $
|
||||
Open <$> publicOrPrivate
|
||||
<*> ambiguous
|
||||
<*> openUsing
|
||||
<*> openHiding
|
||||
<*> openRenaming
|
||||
where
|
||||
openUsing, openHiding :: Parser [(Text, Maybe (Maybe [Text]))]
|
||||
openRenaming :: Parser [(Text, Text)]
|
||||
|
||||
openUsing = option [] do
|
||||
keyword "using"
|
||||
flexibleParens openId
|
||||
|
||||
openHiding = option [] do
|
||||
keyword "hiding"
|
||||
flexibleParens openId
|
||||
|
||||
openId = do
|
||||
name <- identifier
|
||||
ctrs <- optionMaybe $ openAll <|> openCtrs
|
||||
pure (name, ctrs)
|
||||
|
||||
openRenaming = option [] do
|
||||
keyword "renaming"
|
||||
flexibleParens $ cobetween identifier tkArr identifier
|
||||
|
||||
openAll, openCtrs :: Parser (Maybe [Text])
|
||||
|
||||
openAll = Nothing <$ keyword ".."
|
||||
|
||||
openCtrs = optionMaybe $ flexibleParens identifier
|
||||
|
||||
-- | 'Define'
|
||||
tlDef = Define <$> publicOrPrivate <*> definition
|
||||
|
||||
-- | 'TLData'
|
||||
tlData = TLData <$> data_
|
||||
|
||||
-- | 'TLAxiom'
|
||||
tlAxiom = TLAxiom <$> axiom
|
||||
|
||||
-- | 'TLSig'
|
||||
tlSig = TLSig <$> sig
|
||||
|
||||
-- | 'PublicOrPrivate'
|
||||
publicOrPrivate :: Parser PublicOrPrivate
|
||||
publicOrPrivate = (Public <$ keyword "pub") <|> pure Private
|
||||
|
||||
-- | 'Definition'
|
||||
definition :: Parser Definition
|
||||
definition = label "definition" do
|
||||
name <- identifier
|
||||
ty <- optionMaybe typeSig
|
||||
token "="
|
||||
expr <- ambiguous
|
||||
pure $ Definition name ty expr
|
||||
|
||||
ambiguous, block, finite :: Parser Expr
|
||||
-- | 'Expr's which are not guaranteed to consume input before recursing.
|
||||
ambiguous = label "expression" $
|
||||
exAccess <|> exArrow <|> exAnn <|> exAppI <|> exApp <|> exTypeApp
|
||||
|
||||
-- | 'Expr's with a terminal symbol on its left.
|
||||
block = label "block expression" $
|
||||
exData <|> exAxiom <|> exForall <|> exTypeLam <|> exBlockLam <|>
|
||||
exLet <|> exBlockCase <|> finite
|
||||
|
||||
-- | 'Expr's with a terminal symbol on both the left /and/ right.
|
||||
finite = label "finite expression" $
|
||||
exSig <|> exMod <|> exHole <|> exFiniteCase <|> exFiniteLam <|>
|
||||
exLit <|> exVar <|> exGroup
|
||||
|
||||
exAccess, exArrow, exAnn, exAppI, exApp, exTypeApp,
|
||||
exData, exAxiom, exForall, exTypeLam, exBlockLam, exFiniteLam, exLet,
|
||||
exSig, exMod, exHole, exBlockCase, exFiniteCase, exLit, exVar, exGroup
|
||||
:: Parser Expr
|
||||
|
||||
exGroup = label "parenthetical expression" $ betweenParens ambiguous
|
||||
|
||||
typeSig, kindSig, modSig :: Parser Type
|
||||
|
||||
typeSig = label "type signature" $ keyword ":" *> ambiguous
|
||||
|
||||
kindSig = label "kind signature" typeSig
|
||||
|
||||
modSig = label "signature" typeSig
|
||||
|
||||
-- | 'Data'
|
||||
exData = Data <$> data_
|
||||
|
||||
data_ :: Parser Expr
|
||||
data_ = label "data expression" do
|
||||
keyword "data"
|
||||
ambiguous
|
||||
|
||||
-- | 'Axiom'
|
||||
exAxiom = Axiom <$> axiom
|
||||
|
||||
axiom :: Parser Expr
|
||||
axiom = label "axiom expression" do
|
||||
keyword "axiom"
|
||||
ambiguous
|
||||
|
||||
-- | 'SigE'
|
||||
exSig = SigE <$> sig
|
||||
|
||||
-- | 'Mod'
|
||||
exMod = label "module expression" do
|
||||
keyword "mod"
|
||||
params <- sigParams
|
||||
sig <- optionMaybe modSig
|
||||
body <- flexibleBraces topLevel
|
||||
pure $ Mod params sig body
|
||||
|
||||
-- | 'Access'
|
||||
exAccess = label "field access" $ try do
|
||||
expr <- block
|
||||
tkColCol
|
||||
name <- identifier
|
||||
pure $ Access expr name
|
||||
|
||||
-- | @∷@
|
||||
tkColCol :: Parser ()
|
||||
tkColCol = label "∷" $ token "∷" <|> token "::"
|
||||
|
||||
-- | 'Forall'
|
||||
exForall = label "∀ type" $ do
|
||||
tkForall
|
||||
uncurry Forall <$> typeBinder
|
||||
|
||||
-- | @∀@
|
||||
tkForall :: Parser ()
|
||||
tkForall = label "∀" $ keyword "∀" <|> keyword "forall"
|
||||
|
||||
-- | Everything about @forall@ and @^@ is the same
|
||||
-- except for the token and whether a type or expr
|
||||
-- (which are also syntactically the same object)
|
||||
-- comes next.
|
||||
--
|
||||
-- This factors out all of that stuff they have in common.
|
||||
typeBinder :: Parser (NonEmpty (Either (NonEmpty Text, Kind) Text), Expr)
|
||||
typeBinder = do
|
||||
vars <- many1' typeBinder'
|
||||
tkArr
|
||||
ty <- ambiguous
|
||||
pure (vars, ty)
|
||||
where
|
||||
typeBinder', kindedBinder, plainBinder
|
||||
:: Parser (Either (NonEmpty Text, Kind) Text)
|
||||
|
||||
typeBinder' = kindedBinder <|> plainBinder
|
||||
|
||||
kindedBinder = betweenParens $ do
|
||||
names <- many1' identifier
|
||||
kind <- kindSig
|
||||
pure $ Left (names, kind)
|
||||
|
||||
plainBinder = Right <$> identifier
|
||||
|
||||
-- | 'Arrow'
|
||||
exArrow = label "→ type" $ try do
|
||||
(names, argTy) <- arrowArgs
|
||||
tkArr
|
||||
rTy <- ambiguous
|
||||
pure $ Arrow names argTy rTy
|
||||
|
||||
where
|
||||
arrowArgs, namedArgs, typeArg :: Parser ([Text], Type)
|
||||
|
||||
arrowArgs = namedArgs <|> typeArg
|
||||
|
||||
namedArgs = betweenParens do
|
||||
names <- many1 identifier
|
||||
ty <- kindSig
|
||||
pure (names, ty)
|
||||
|
||||
typeArg = ([],) <$> block
|
||||
|
||||
-- | @→@
|
||||
tkArr :: Parser ()
|
||||
tkArr = label "→" $ keyword "→" <|> keyword "->"
|
||||
|
||||
-- | 'Ann'
|
||||
exAnn = label "annotated expression" $ try do
|
||||
expr <- block
|
||||
ty <- typeSig
|
||||
pure $ Ann expr ty
|
||||
|
||||
-- | 'Hole'
|
||||
exHole = label "hole" $ Hole <$ keyword "_"
|
||||
|
||||
-- | 'TypeLam'
|
||||
exTypeLam = label "type Λ" $ do
|
||||
tkBigLam
|
||||
uncurry TypeLam <$> typeBinder
|
||||
|
||||
-- | @Λ@
|
||||
tkBigLam :: Parser ()
|
||||
tkBigLam = label "Λ" $ keyword "Λ" <|> keyword "^"
|
||||
|
||||
-- | 'TypeApp'
|
||||
exTypeApp = label "type application" $ try do
|
||||
expr <- block
|
||||
token "@"
|
||||
arg <- ambiguous
|
||||
pure $ TypeApp expr arg
|
||||
|
||||
-- | 'Lam' with only one undelimited case branch
|
||||
exBlockLam = label "λ expression" $ try do
|
||||
tkLam
|
||||
args <- many pattern_
|
||||
tkArr
|
||||
body <- ambiguous
|
||||
pure $ LamBlock args body
|
||||
|
||||
-- | 'Lam' with delimited case branches
|
||||
exFiniteLam = label "λ-case expression" $ try do
|
||||
tkLam
|
||||
simpleArgs <- many pattern_
|
||||
body <- caseBranches
|
||||
pure $ Lam simpleArgs body
|
||||
|
||||
tkLam :: Parser ()
|
||||
tkLam = label "λ" $ keyword "λ" <|> keyword "\\"
|
||||
|
||||
-- | 'App'
|
||||
exApp = label "application" $ try do
|
||||
ef <- finite
|
||||
exs <- many finite
|
||||
exfinal <- block
|
||||
pure $ App ef (snoc' exs exfinal)
|
||||
|
||||
-- | 'AppI'
|
||||
exAppI = label "infix application" $
|
||||
fail "infix expressions not yet supported"
|
||||
|
||||
-- | 'Let'
|
||||
exLet = label "let expression" do
|
||||
keyword "let"
|
||||
decls <- flexibleSepBy1 (token ";") topLevel
|
||||
keyword "in"
|
||||
body <- ambiguous
|
||||
pure $ Let decls body
|
||||
|
||||
-- | 'Case' with only one undelimited case branch
|
||||
exBlockCase = label "case expression" $ try do
|
||||
keyword "case"
|
||||
exprs <- flexibleSepBy (keyword "|") ambiguous
|
||||
body <- caseBranches
|
||||
pure $ Case exprs body
|
||||
|
||||
-- | 'Case'
|
||||
exFiniteCase = label "case-of expression" $ try do
|
||||
keyword "case"
|
||||
exprs <- flexibleSepBy1 (keyword "|") ambiguous
|
||||
keyword "of"
|
||||
pats <- flexibleSepBy1 (keyword "|") pattern_
|
||||
tkArr
|
||||
body <- ambiguous
|
||||
pure $ CaseBlock exprs pats body
|
||||
|
||||
-- | 'Lit'
|
||||
exLit = label "literal" $ Lit <$> lit ambiguous
|
||||
|
||||
-- | 'Var'
|
||||
exVar = label "variable" $ Var <$> identifier
|
||||
|
||||
-- | 'Sig'
|
||||
sig, sigADT, sigGADT, sigSig :: Parser Sig
|
||||
sig = label "signature" $ sigADT <|> sigGADT <|> sigSig
|
||||
|
||||
sigParams :: Parser [Either (NonEmpty Text, Kind) Text]
|
||||
sigParams = label "signature parameters" $ many $ annParam <|> unannParam
|
||||
where
|
||||
annParam, unannParam :: Parser (Either (NonEmpty Text, Kind) Text)
|
||||
|
||||
annParam = betweenParens do
|
||||
names <- many1' identifier
|
||||
kind <- kindSig
|
||||
pure $ Left (names, kind)
|
||||
|
||||
unannParam = Right <$> identifier
|
||||
|
||||
-- | 'ADT'
|
||||
sigADT = label "adt" do
|
||||
keyword "adt"
|
||||
name <- identifier
|
||||
params <- sigParams
|
||||
kind <- optionMaybe kindSig
|
||||
(codataQ, body) <- betweenBraces $
|
||||
emptyData <|> emptyCodata <|> dataCtrs <|> codataElims
|
||||
pure $ SigQs params $ ADT codataQ name kind body
|
||||
where
|
||||
emptyData, emptyCodata, dataCtrs, codataElims
|
||||
:: Parser (Bool, [(Text, [Type])])
|
||||
|
||||
emptyData = try $ (False, []) <$ keyword "+"
|
||||
emptyCodata = try $ (True, []) <$ keyword "&"
|
||||
|
||||
dataCtrs = try $ (False,) <$> flexibleSepBy1 (keyword "+") do
|
||||
name <- identifier
|
||||
ctrs <- many $ notFollowedBy (keyword "+") >> finite
|
||||
pure (name, ctrs)
|
||||
|
||||
codataElims = try $ (True,) <$> flexibleSepBy1 (keyword "&") do
|
||||
name <- identifier
|
||||
elims <- many $ notFollowedBy (keyword "&") >> finite
|
||||
pure (name, elims)
|
||||
|
||||
-- | 'GADT'
|
||||
sigGADT = label "gadt" do
|
||||
keyword "gadt"
|
||||
name <- identifier
|
||||
params <- sigParams
|
||||
kind <- optionMaybe kindSig
|
||||
ctrs <- flexibleBraces declaration
|
||||
pure $ SigQs params $ GADT name kind ctrs
|
||||
|
||||
-- | 'Sig'
|
||||
sigSig = label "sig" do
|
||||
keyword "sig"
|
||||
params <- sigParams
|
||||
ctrs <- flexibleBraces $ (Left <$> declaration) <|> (Right <$> topLevel)
|
||||
pure $ SigQs params $ Sig ctrs
|
||||
|
||||
declaration :: Parser (NonEmpty Text, Type)
|
||||
declaration = label "declaration" $ (,) <$> many1' identifier <*> typeSig
|
||||
|
||||
pattern_, finitePattern, patVar, patIrr, patImp, patApp,
|
||||
patAppI, patView, patLit, patGroup :: Parser Pattern
|
||||
|
||||
-- | 'Pattern'
|
||||
pattern_ = label "pattern" $
|
||||
patApp <|> patAppI <|> patView <|> finitePattern
|
||||
|
||||
finitePattern =
|
||||
patIrr <|> patImp <|> patLit <|> patVar <|> patGroup
|
||||
|
||||
patGroup = betweenParens pattern_
|
||||
|
||||
-- | 'PatVar'
|
||||
patVar = label "pattern variable" $ PatVar <$> identifier <*> optionMaybe typeSig
|
||||
|
||||
-- | 'Irrelevant'
|
||||
patIrr = label "irrelevant pattern" $ Irrelevant <$ keyword "_"
|
||||
|
||||
-- | 'Impossible'
|
||||
patImp = label "impossible pattern" $ Impossible <$ keyword "!"
|
||||
|
||||
-- | 'PatApp'
|
||||
patApp = label "pattern application" $ do
|
||||
name <- identifier
|
||||
pats <- many1 finitePattern
|
||||
pure $ PatApp name pats
|
||||
|
||||
-- FIXME: Implement infix pattern application
|
||||
-- | 'PatAppI'
|
||||
patAppI = label "infix pattern application" $
|
||||
fail "infix pattern application not yet implemented"
|
||||
|
||||
-- | 'View'
|
||||
patView = label "view pattern" $ try $ View <$> block <*> (tkArr *> pattern_)
|
||||
|
||||
-- | 'PatLit'
|
||||
patLit = label "literal pattern" $ PatLit <$> lit pattern_
|
||||
|
||||
caseBranches :: Parser [CaseBranch]
|
||||
caseBranches = label "case branches" $ flexibleBraces caseBranch
|
||||
|
||||
caseBranch :: Parser CaseBranch
|
||||
caseRefinement, caseGuards, casePlain :: [Pattern] -> Parser CaseBranch
|
||||
|
||||
-- | 'CaseBranch'
|
||||
caseBranch = label "case branch" do
|
||||
pats <- many1 pattern_
|
||||
caseRefinement pats <|> caseGuards pats <|> casePlain pats
|
||||
|
||||
-- FIXME: Implement case refinement
|
||||
-- | 'Refinement'
|
||||
caseRefinement pats = label "case refinement" $
|
||||
fail "case refinement not implemented"
|
||||
|
||||
-- FIXME: Implement case guards
|
||||
-- | 'Guards'
|
||||
caseGuards pats = label "guard clauses" $
|
||||
fail "case guards not yet implemented"
|
||||
|
||||
-- | 'PlainCase'
|
||||
casePlain pats = do
|
||||
tkArr
|
||||
PlainCase pats <$> ambiguous
|
||||
|
||||
-- FIXME: Implement guard clauses
|
||||
-- | 'Guard'
|
||||
guard :: Parser Guard
|
||||
guard = label "guard clause" $
|
||||
fail "guard clauses not yet implemented"
|
||||
|
||||
lit, litList :: Parser a -> Parser (Lit a)
|
||||
litInt, litChar, litStr :: Parser (Lit a)
|
||||
|
||||
-- | 'Lit'
|
||||
lit m = label "literal" $ litInt <|> litChar <|> litStr <|> litList m
|
||||
|
||||
-- | 'LitInt'
|
||||
litInt = label "integer literal" $ LitInt . read <$> try do
|
||||
sign <- optionMaybe $ char '+' <|> char '-'
|
||||
digits <- many1 digit
|
||||
pure $ maybe digits (: digits) sign
|
||||
|
||||
-- | 'LitChar'
|
||||
litChar = label "character literal" $
|
||||
fmap LitChar $ between (char '\'') (char '\'') $ noneOf "\\'\n"
|
||||
|
||||
-- | 'LitStr'
|
||||
litStr = label "string literal" $ fmap (LitStr . T.pack) $
|
||||
between (char '"') (char '"') $ many1 $ noneOf "\\\"\n"
|
||||
|
||||
-- | 'LitList'
|
||||
litList m = label "list literal" $ LitList <$> flexibleBrackets m
|
||||
|
||||
-- | 'FlexibleSeparatorSyntax'
|
||||
flexibleSepBy :: Parser a -> Parser b -> Parser [b]
|
||||
flexibleSepBy delim m = do
|
||||
optional delim
|
||||
sepEndBy m delim
|
||||
|
||||
-- | 'FlexibleSeparatorSyntax'
|
||||
flexibleSepBy1 :: Parser a -> Parser b -> Parser [b]
|
||||
flexibleSepBy1 delim m = do
|
||||
optional delim
|
||||
sepEndBy1 m delim
|
||||
|
||||
flexibleParens, flexibleBrackets, flexibleBraces :: Parser a -> Parser [a]
|
||||
|
||||
-- | 'FlexibleSeparatorSyntax', with the @;@ separator between @(@ @)@
|
||||
flexibleParens = betweenParens . flexibleSepBy (token ";")
|
||||
|
||||
-- | 'FlexibleSeparatorSyntax', with the @;@ separator between @[@ @]@
|
||||
flexibleBrackets = betweenBrackets . flexibleSepBy (token ";")
|
||||
|
||||
-- | 'FlexibleSeparatorSyntax', with the @;@ separator between @{@ @}@
|
||||
flexibleBraces = betweenBraces . flexibleSepBy (token ";")
|
||||
|
||||
---
|
||||
--- Helper parsers which aren't explicitly specified by the AST
|
||||
---
|
||||
|
||||
-- | An identifier is a sequence of characters with no token which is not a keyword.
|
||||
identifier :: Parser Text
|
||||
identifier = label "identifier" $ try do
|
||||
notFollowedBy anyKeyword
|
||||
name <- T.pack <$> (notFollowedBy anyToken *> many1 anyChar <* spaces)
|
||||
if any ((`elem` keywords) . T.unpack) $ T.splitOn "_" name
|
||||
then fail "identifier contained keywords"
|
||||
else pure name
|
||||
|
||||
token :: String -> Parser ()
|
||||
token tk = label tk $ string tk *> spaces
|
||||
|
||||
anyToken :: Parser ()
|
||||
anyToken = label "any token" $ choice $ map token tokens
|
||||
|
||||
-- | Tokens which are reserved by syntax
|
||||
-- and may not appear /anywhere/ in an identifier.
|
||||
tokens :: [String]
|
||||
tokens =
|
||||
[ "//", "/*", "*/"
|
||||
, "(", ")", "{", "}"
|
||||
, ";", "∷", "::", "@"
|
||||
, " ", "\r", "\n", "\t"
|
||||
, "```"
|
||||
]
|
||||
|
||||
-- | A keyword is an exact string which is not part of an identifier.
|
||||
keyword :: String -> Parser ()
|
||||
keyword kwd = label kwd $ do
|
||||
try do
|
||||
_ <- string kwd
|
||||
notFollowedBy (notFollowedBy anyToken >> anyChar)
|
||||
spaces
|
||||
|
||||
anyKeyword :: Parser ()
|
||||
anyKeyword = label "any keyword" $ choice $ map keyword keywords
|
||||
|
||||
-- | Keywords are reserved by syntax and are not allowed to be used as identifiers
|
||||
-- or as a part of a `_`-separated identifier.
|
||||
--
|
||||
-- However, they may be used as /part/ of an identifier.
|
||||
keywords :: [String]
|
||||
keywords =
|
||||
[ "open", "using", "hiding", "renaming", "..", "pub"
|
||||
, "data", "axiom", "adt", "gadt", "sig", "mod"
|
||||
, "forall"
|
||||
, "let", "in", "case"
|
||||
, "[", "]"
|
||||
, ":", "∀", "Λ", "^", "λ", "\\", "→", "->"
|
||||
, "|", "?", "!", "_", "..."
|
||||
]
|
||||
|
||||
spaces :: Parser ()
|
||||
spaces = label "whitespace or comments" $
|
||||
Text.Parsec.spaces >> optional (try (comment >> spaces))
|
||||
|
||||
comment, lineComment, blockComment :: Parser ()
|
||||
|
||||
comment = label "comment" $ lineComment <|> blockComment
|
||||
|
||||
lineComment = label "line comment" $ do
|
||||
_ <- try (string "//")
|
||||
_ <- many1 (noneOf "\n")
|
||||
pure ()
|
||||
|
||||
blockComment = label "block comment" $ do
|
||||
_ <- try (string "/*")
|
||||
_ <- many1 $ notFollowedBy (string "*/") >> anyChar
|
||||
_ <- string "*/"
|
||||
pure ()
|
||||
|
||||
-- | The opposite of `between`: ignore the middle, keep the sides
|
||||
cobetween :: Parser a -> Parser b -> Parser c -> Parser (a, c)
|
||||
cobetween a b c = do
|
||||
x <- a
|
||||
_ <- b
|
||||
y <- c
|
||||
pure (x, y)
|
||||
|
||||
-- the parens/brackets/braces word choice is totally meaningless
|
||||
betweenParens, betweenBrackets, betweenBraces :: Parser a -> Parser a
|
||||
|
||||
-- | Between @(@ @)@
|
||||
betweenParens = between (token "(") (token ")")
|
||||
|
||||
-- | Between @[@ @]@
|
||||
betweenBrackets = between (keyword "[") (keyword "]")
|
||||
|
||||
-- | Between @{@ @}@
|
||||
betweenBraces = between (keyword "{") (keyword "}")
|
||||
|
||||
many1' :: Parser a -> Parser (NonEmpty a)
|
||||
many1' = fmap fromList . many1
|
||||
|
||||
snoc' :: [a] -> a -> NonEmpty a
|
||||
snoc' xs x = fromList $ xs ++ [x]
|
||||
|
||||
label :: String -> Parser a -> Parser a
|
||||
label = flip Text.Parsec.label
|
||||
|
|
|
@ -1,4 +1,7 @@
|
|||
module Ivo.Syntax.Printer (unparseAST, unparseType, unparseScheme) where
|
||||
-- | Turn abstract syntax into the corresponding concrete syntax.
|
||||
--
|
||||
-- This is /not/ a pretty-printer; it uses minimal whitespace)
|
||||
module Ivo.Syntax.Printer (unparseScope, unparseTopLevel, unparseExpr) where
|
||||
|
||||
import Ivo.Syntax.Base
|
||||
|
||||
|
@ -10,6 +13,99 @@ import Data.Text.Lazy (fromStrict, toStrict, intercalate, unwords, singleton)
|
|||
import Data.Text.Lazy.Builder (Builder, fromText, fromLazyText, toLazyText, fromString)
|
||||
import Prelude hiding (unwords)
|
||||
|
||||
unparseScope :: Scope -> Text
|
||||
unparseScope = unambiguous . scope
|
||||
|
||||
unparseTopLevel :: TopLevel -> Text
|
||||
unparseTopLevel = unambiguous . topLevel
|
||||
|
||||
unparseExpr :: Expr -> Text
|
||||
unparseExpr = unambiguous . expr
|
||||
|
||||
type Unparser a = a -> Tagged Builder
|
||||
|
||||
scope :: Unparser Scope
|
||||
scope (Scope tls) = tag Ambiguous $ unmany (topLevel <? ";\n") tls
|
||||
|
||||
(<?) :: Unparser a -> Text -> Unparser a
|
||||
u <? txt = \x -> u x <> fromText txt
|
||||
|
||||
topLevel :: Unparser TopLevel
|
||||
topLevel = \case
|
||||
Open pub expr use hide rename ->
|
||||
publicOrPrivate pub <>
|
||||
unambiguousExpr expr <> " " <>
|
||||
openUsing use <> " "
|
||||
openHiding hide <> " "
|
||||
openRenaming rename
|
||||
Define pub def ->
|
||||
publicOrPrivate pub <>
|
||||
definition def
|
||||
TLData expr -> data_ expr
|
||||
TLAxiom expr -> axiom expr
|
||||
TLSig s -> sig s
|
||||
|
||||
publicOrPrivate :: PublicOrPrivate -> Builder
|
||||
publicOrPrivate Public = "pub "
|
||||
publicOrPrivate Private = ""
|
||||
|
||||
openUsing, openHiding :: [(Text, Maybe (Maybe [Text]))] -> Builder
|
||||
|
||||
-- FIXME
|
||||
openUsing _ = "using (some stuff) "
|
||||
|
||||
-- FIXME
|
||||
openHiding _ = "hiding (some stuff) "
|
||||
|
||||
-- FIXME
|
||||
openRenaming :: [(Text, Text)]
|
||||
openRenaming _ = "renaming (some stuff) "
|
||||
|
||||
definition :: Unparser Definition
|
||||
definition (Definition name ty expr) =
|
||||
fromText name <> " " <> typeSig ty <> "= " <> unambiguousExpr expr
|
||||
|
||||
expr :: Unparser Expr
|
||||
expr = \case
|
||||
Data expr -> tag Block $ data_ expr
|
||||
Axiom expr -> tag Block $ axiom expr
|
||||
SigE s -> tag Block $ sig s
|
||||
-- FIXME
|
||||
Mod _ _ _ -> tag Block $ error "I don't know how to unparse modules"
|
||||
Access expr name -> tag Ambiguous $ blockExpr expr <> "::" <> fromText name
|
||||
Forall binders ty -> tag Block $ "∀ " <> typeBinders binders <> "→ " <> ambiguousExpr ty
|
||||
Arrow [] arg ty -> tag Ambiguous $ blockExpr arg <> "→ " <> ambiguousExpr ty
|
||||
Ann expr ty -> tag Ambiguous $ blockExpr expr <> ": " <> ambiguousExpr ty
|
||||
Hole -> tag Finite "_"
|
||||
TypeLam binders ty -> tag Block $ "Λ " <> typeBinders binders <> "→ " <> ambiguousExpr ty
|
||||
TypeApp expr ty -> tag Ambiguous $ blockExpr <> "@" <> finiteExpr ty
|
||||
Lam pats cases -> tag Block $ "λ " <> unmany1 pattern_ pats <> caseBranches cases
|
||||
|
||||
data_ = undefined
|
||||
|
||||
axiom = undefined
|
||||
|
||||
typeBinders :: Unparser (NonEmpty (Either (NonEmpty Text, Kind) Text))
|
||||
typeBinders = error "Whatever"
|
||||
|
||||
sig :: Unparser Sig
|
||||
sig = error "I don't know how to unparse signatures"
|
||||
|
||||
pattern_ :: Unparser Pattern
|
||||
pattern_ = error "I don't know how to unparse patterns"
|
||||
|
||||
caseBranch :: Unparser CaseBranch
|
||||
caseBranch = error "I don't know how to unparse case branches"
|
||||
|
||||
caseBranches :: Unparser [CaseBranch]
|
||||
caseBranches = error "I don't know how to unparse case branches"
|
||||
|
||||
guard :: Unparser Guard
|
||||
guard = error "I don't know how to unparse guard clauses"
|
||||
|
||||
lit :: Unparser a -> Unparser (Lit a)
|
||||
lit u = error "I don't know how to unparse literals"
|
||||
|
||||
-- I'm surprised this isn't in base somewhere.
|
||||
unsnoc :: NonEmpty a -> ([a], a)
|
||||
unsnoc = cata \case
|
||||
|
@ -47,78 +143,13 @@ ambiguous :: Tagged Builder -> Builder
|
|||
ambiguous (Finite, t) = t
|
||||
ambiguous (_, t) = group t
|
||||
|
||||
-- | Turn an abstract syntax tree into the corresponding concrete syntax.
|
||||
--
|
||||
-- This is *not* a pretty-printer; it uses minimal whitespace.
|
||||
unparseAST :: AST -> Text
|
||||
unparseAST = toStrict . toLazyText . snd . cata \case
|
||||
VarF name -> tag Finite $ fromText name
|
||||
AppF ef exs -> unparseApp ef exs
|
||||
AbsF names body -> tag Block $
|
||||
let names' = fromLazyText (unwords $ map fromStrict $ toList names)
|
||||
in "λ" <> names' <> ". " <> unambiguous body
|
||||
LetFP defs body -> tag Block $ "let " <> unparseDefs defs <> " in " <> unambiguous body
|
||||
LetRecFP def body -> tag Block $ "letrec " <> unparseDef def <> " in " <> unambiguous body
|
||||
CtrF ctr e -> unparseCtr ctr e
|
||||
CaseF pats ->
|
||||
let pats' = fromLazyText $ intercalate "; " $ map (toLazyText . unparsePat) pats
|
||||
in tag Finite $ "{ " <> pats' <> " }"
|
||||
AnnF () e t -> tag Ambiguous $ final e <> " : " <> fromText (unparseType t)
|
||||
PNatF n -> tag Finite $ fromString $ show n
|
||||
PListF es ->
|
||||
let es' = fromLazyText $ intercalate ", " $ map (toLazyText . unambiguous) es
|
||||
in tag Finite $ "[" <> es' <> "]"
|
||||
PStrF s -> tag Finite $ "\"" <> fromText s <> "\""
|
||||
PCharF c -> tag Finite $ "'" <> fromLazyText (singleton c)
|
||||
HoleFP -> tag Finite "_"
|
||||
where
|
||||
unparseApp :: Tagged Builder -> NonEmpty (Tagged Builder) -> Tagged Builder
|
||||
unparseApp ef (unsnoc -> (exs, efinal))
|
||||
= tag Ambiguous $ foldr (\e es' -> ambiguous e <> " " <> es') (final efinal) (ef : exs)
|
||||
ambiguousExpr, blockExpr, finiteExpr :: Expr -> Builder
|
||||
|
||||
unparseDef (name, val) = fromText name <> " = " <> unambiguous val
|
||||
unparseDefs defs = fromLazyText (intercalate "; " $ map (toLazyText . unparseDef) $ toList defs)
|
||||
ambiguousExpr = ambiguous . expr
|
||||
|
||||
unparseCtr :: Ctr -> [Tagged Builder] -> Tagged Builder
|
||||
-- Fully-applied special syntax forms
|
||||
unparseCtr CPair [x, y] = tag Finite $ "(" <> unambiguous x <> ", " <> unambiguous y <> ")"
|
||||
unparseCtr CCons [x, y] = tag Finite $ "(" <> unambiguous x <> " :: " <> unambiguous y <> ")"
|
||||
-- Partially-applied syntax forms
|
||||
unparseCtr CUnit [] = tag Finite "()"
|
||||
unparseCtr CPair [] = tag Finite "(,)"
|
||||
unparseCtr CLeft [] = tag Finite "Left"
|
||||
unparseCtr CRight [] = tag Finite "Right"
|
||||
unparseCtr CZero [] = tag Finite "Z"
|
||||
unparseCtr CSucc [] = tag Finite "S"
|
||||
unparseCtr CNil [] = tag Finite "[]"
|
||||
unparseCtr CCons [] = tag Finite "(::)"
|
||||
unparseCtr CChar [] = tag Finite "Char"
|
||||
unparseCtr ctr (x:xs) = unparseApp (unparseCtr ctr []) (x :| xs)
|
||||
blockExpr = final . expr
|
||||
|
||||
unparsePat (Pat ctr ns e)
|
||||
= unambiguous (unparseCtr ctr (map (tag Finite . fromText) ns)) <> " -> " <> unambiguous e
|
||||
finiteExpr = unambiguous . expr
|
||||
|
||||
-- HACK
|
||||
pattern TApp2 :: Type -> Type -> Type -> Type
|
||||
pattern TApp2 tf tx ty = TApp (TApp tf tx) ty
|
||||
|
||||
-- TODO: Improve these printers.
|
||||
unparseType :: Type -> Text
|
||||
unparseType (TVar name) = name
|
||||
unparseType (TApp2 TAbs a b) = "(" <> unparseType a <> " -> " <> unparseType b <> ")"
|
||||
unparseType (TApp2 TProd a b) = "(" <> unparseType a <> " * " <> unparseType b <> ")"
|
||||
unparseType (TApp2 TSum a b) = "(" <> unparseType a <> " + " <> unparseType b <> ")"
|
||||
unparseType (TApp TList a) = "[" <> unparseType a <> "]"
|
||||
unparseType (TApp a b) = "(" <> unparseType a <> " " <> unparseType b <> ")"
|
||||
unparseType TAbs = "(->)"
|
||||
unparseType TProd = "(*)"
|
||||
unparseType TSum = "(+)"
|
||||
unparseType TUnit = "★"
|
||||
unparseType TVoid = "⊥"
|
||||
unparseType TNat = "Nat"
|
||||
unparseType TList = "[]"
|
||||
unparseType TChar = "Char"
|
||||
|
||||
unparseScheme :: Scheme -> Text
|
||||
unparseScheme (TForall [] t) = unparseType t
|
||||
unparseScheme (TForall names t) = "∀" <> T.unwords names <> ". " <> unparseType t
|
||||
unmany :: Foldable t => Unparser a -> t a -> Builder
|
||||
unmany u xs = error "fuck it, implement this later"
|
||||
|
|
Loading…
Reference in New Issue