churf/spec.txt
2023-03-27 16:07:11 +02:00

121 lines
2.6 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

---------------------------------------------------------------------------
-- * Parser
---------------------------------------------------------------------------
data Program = Program [Def]
data Def = DSig Ident Type | DBind Bind
data Bind = Bind Ident [Ident] Exp
data Exp
= EId Ident
| ELit Lit
| EAnn Exp Type
| ELet Ident Exp Exp
| EApp Exp Exp
| EAdd Exp Exp
| EAbs Ident Exp
data Lit = LInt Integer
| LChar Character
data Type
= TLit Ident -- τ
| TVar TVar -- α
| TFun Type Type -- A → A
| TAll TVar Type -- ∀α. A
| TEVar TEVar -- ά (internal)
data TVar = MkTVar Ident
data TEVar = MkTEVar Ident
---------------------------------------------------------------------------
-- * Type checker
---------------------------------------------------------------------------
-- • Def and DSig are removed in favor on just Bind
-- • Typed expressions
-- • TEVar is removed (NOT IMPLEMENTED)
newtype Program = Program [Bind]
data Bind = Bind Id [Id] ExpT
data Exp
= EId Ident
| ELit Lit
| ELet Bind ExpT
| EApp ExpT ExpT
| EAdd ExpT ExpT
| EAbs Ident ExpT
type Id = (Ident, Type)
type ExpT = (Exp, Type)
data Lit = LInt Integer
| LChar Character
data Type
= TLit Ident -- τ
| TVar TVar -- α
| TFun Type Type -- A → A
| TAll TVar Type -- ∀α. A
data TVar = MkTVar Ident
---------------------------------------------------------------------------
-- * Lambda lifter
---------------------------------------------------------------------------
-- • EAbs are removed (NOT IMPLEMENTED)
-- • ELet only allow constant expressions (NOT IMPLEMENTED)
newtype Program = Program [Bind]
data Bind = Bind Id [Id] ExpT
data Exp
= EId Ident
| ELit Lit
| ELet Ident ExpT ExpT
| EApp ExpT ExpT
| EAdd ExpT ExpT
type Id = (Ident, Type)
type ExpT = (Exp, Type)
data Lit = LInt Integer
| LChar Character
data Type
= TLit Ident -- τ
| TVar TVar -- α
| TFun Type Type -- A → A
| TAll TVar Type -- ∀α. A
data TVar = MkTVar Ident
---------------------------------------------------------------------------
-- * Monomorpher
---------------------------------------------------------------------------
-- • Polymorphic types are removed (NOT IMPLEMENTED)
newtype Program = Program [Bind]
data Bind = Bind Id [Id] ExpT
data Exp
= EId Ident
| ELit Lit
| ELet Ident ExpT ExpT
| EApp ExpT ExpT
| EAdd ExpT ExpT
type Id = (Ident, Type)
type ExpT = (Exp, Type)
data Lit = LInt Integer
| LChar Character
data Type = Type Ident