Add extensions for core language and enable test

.github/workflows/haskell.yml

@@ -48,4 +48,5 @@ jobs:
       run: |
         cd bootstrap
         stack build
+        stack test
         cd ..

bootstrap/src/Driver/Inference.hs

@@ -4,7 +4,7 @@ module Driver.Inference
 where
 
 -- import Tlang.Inference.Kind (NormalKind)
-import Tlang.AST (Symbol (..), type (@:) (..), Kind (..), Symbol)
+import Tlang.AST (type (@:) (..), Kind (..))
 
 -- defaultEnv :: [NormalKind :@ Symbol]
 defaultEnv = undefined

bootstrap/src/Driver/Parser.hs

@@ -28,6 +28,7 @@ import Tlang.AST
 import Tlang.Parser
 import Tlang.Extension
 import Tlang.Generic ((:+:))
+import Tlang.Constraint (Prefix (..), Prefixes (..))
 import qualified Data.Kind as D (Type)
 
 import Capability.Accessors
@@ -47,25 +48,25 @@ import GHC.Generics (Generic)
 import Text.Megaparsec (MonadParsec, ParseErrorBundle, ParsecT, runParserT, lookAhead)
 import Text.Megaparsec.Debug (MonadParsecDbg)
 
-type TypeAST = StandardType Label (Bound Name) Name Name
+type TypeAST = StandardType Label (Prefix Name) Name Name
 type ASTGPat typ = Pattern (LiteralText :+: LiteralInteger :+: LiteralNumber) ((@:) typ :+: PatGroup) Label Name
 type ASTPat typ = Pattern (LiteralText :+: LiteralInteger :+: LiteralNumber) ((@:) typ) Label Name
 
 type ASTExpr typ = Expr
   ( Let (ASTPat typ)
-  :+: Lambda (ASTGPat typ) (Bounds Name typ)
-  :+: Lambda (Grp (ASTPat typ)) (Bounds Name typ)
+  :+: Equation (ASTGPat typ) (Prefixes Name typ)
+  :+: Equation (Grp (ASTPat typ)) (Prefixes Name typ)
   :+: Apply :+: Tuple :+: Record Label
   :+: LiteralText :+: LiteralInteger :+: LiteralNumber
-  :+: VisibleType typ :+: Selector Label :+: Constructor Label
+  :+: Value typ :+: Selector Label :+: Constructor Label
   :+: (@:) typ
   ) Name
 
 type ASTDeclExt typ expr = UserItem
-  :+: UserType typ [Bound Name typ]
+  :+: UserType typ [Prefix Name typ]
   :+: UserFFI typ
   :+: UserValue expr (Maybe typ)
-  :+: UserData [Bound Name typ] (UserDataDef (UserPhantom :+: UserCoerce :+: UserEnum Label :+: UserStruct Label) typ)
+  :+: UserData [Prefix Name typ] (UserDataDef (UserPhantom :+: UserCoerce :+: UserEnum Label :+: UserStruct Label) typ)
 type ASTDecl typ expr = Decl (ASTDeclExt typ expr) Name
 
 type PredefExprVal = ASTExpr TypeAST

bootstrap/src/Tlang/AST.hs

@@ -3,7 +3,6 @@ module Tlang.AST
 
     -- ** useful data
     None (..)
-  , Symbol (..)
   , Label (..)
   , Name (..)
 
@@ -49,9 +48,6 @@ type StandardType label bound = Type (TypBindPlugin bound) (TypPlugin label)
 -- | a place holder for every parametric data type
 data None a = None deriving (Show, Eq, Functor, Foldable, Traversable)
 
--- | used to represent type name reference, both for operator and normal name
-data Symbol = Symbol String | Op String deriving (Eq)
-
 -- | a wrapper for name reference
 newtype Name = Name Text deriving (Eq, Ord) deriving IsString via Text
 instance Show Name where
@@ -62,17 +58,3 @@ newtype Label = Label Text deriving (Eq, Ord) deriving IsString via Text
 instance Show Label where
   show (Label text) = unpack text
 
-instance Show Symbol where
-  show (Symbol s) = s
-  show (Op s) = s
-
-instance Ord Symbol where
-  compare (Symbol s1) (Symbol s2) = compare s1 s2
-  compare (Op s1) (Symbol s2) = compare s1 s2
-  compare (Symbol s1) (Op s2) = compare s1 s2
-  compare (Op s1) (Op s2) = compare s1 s2
-
-instance Labellable Symbol where
-  toLabelValue (Symbol name) = toLabelValue name
-  toLabelValue (Op name) = toLabelValue name
-

bootstrap/src/Tlang/AST/Type.hs

@@ -11,9 +11,6 @@ module Tlang.AST.Type
   , type (>|) (..)
 
   , Variance (..)
-
-  , Bound (..)
-  , Bounds (..)
   )
 where
 
@@ -102,17 +99,6 @@ instance
   show (TypBnd binder body) = "Bind { " <> show binder <> " = " <> show body <> " }"
   show (TypCon t ts) = "(" <> show t <> " " <> show ts <> ")"
 
--- | MLF bounded quantifier
-data Bound name typ
-  = name :~ typ -- ^ equality relation
-  | name :> typ -- ^ lower bound or subsume
-  deriving (Show, Ord, Eq, Functor, Traversable, Foldable)
-$(deriveBifunctor ''Bound)
-
--- | type Prefixs qual name typ = [Prefix qual name typ]
-newtype Bounds name typ = Bounds [Bound name typ] deriving (Show, Ord, Eq, Functor, Traversable, Foldable)
-$(deriveBifunctor ''Bounds)
-
 -- | type variance
 data Variance = InVar | CoVar | ContraVar deriving (Show, Eq, Ord)
 

bootstrap/src/Tlang/Constraint.hs

@@ -3,6 +3,8 @@ module Tlang.Constraint
   , ConstraintF (..)
   , (:<>) (..)
   , (:>>) (..)
+  , Prefix (..)
+  , Prefixes (..)
   )
 where
 
@@ -30,32 +32,31 @@ deriving instance Traversable rel => Traversable (Constraint rel term name)
 deriving instance (Show (rel typ), Show term, Show name, Show typ) => Show (Constraint rel name term typ)
 deriving instance (Eq (rel typ), Eq term, Eq name, Eq typ) => Eq (Constraint rel name term typ)
 
-type FoldFunctor f = (Functor f, Traversable f, Foldable f)
-makeBaseFunctor $ fixQ [d| instance (FoldFunctor rel) => Recursive (Constraint rel name term typ) |]
+makeBaseFunctor $ fixQ [d| instance (Functor rel) => Recursive (Constraint rel name term typ) |]
 $(deriveBifunctor ''Constraint)
 
 -- | constraint concatenation
 data a :<> b = a :<> b deriving (Show, Eq, Functor, Foldable, Traversable)
 -- | first order substitution
 data a :>> b = a :>> b deriving (Show, Eq, Functor, Foldable, Traversable)
 
+-- | MLF bounded quantifier
+data Prefix name typ
+  = name :~ typ -- ^ equality relation, rigid binding
+  | name :> typ -- ^ lower bound or subsume, flexible binding
+  deriving (Show, Ord, Eq, Functor, Traversable, Foldable)
+
+newtype Prefixes name typ = Prefixes [Prefix name typ]
+  deriving (Show, Ord, Eq, Functor, Traversable, Foldable)
+
 -- data Prefix qual name typ
 --   = typ :~ name  -- ^ `name` is rigid bound to `typ`
 --   | typ :< name  -- ^ `name` is an instance of `typ`
 --   | qual typ :? name  -- ^ `name` is qualified by `qual typ`
 --   deriving (Show, Eq)
 
--- data Prefix label name typ
---   = Prefix (Bound name typ)
---   | RowRec (Bound name [(label, typ)])        -- ^ record row
---   | RowVar (Bound name [(label, Maybe typ)])  -- ^ variant row
---   deriving (Show, Eq)
-
--- data Qualify label typ
---   = AllOf [(label, typ)]        -- ^ for record
---   | AnyOf [(label, Maybe typ)]  -- ^ for variant
-
--- $(deriveBifunctor ''Prefix)
+$(deriveBifunctor ''Prefix)
+$(deriveBifunctor ''Prefixes)
 $(deriveBifunctor ''(:<>))
 $(deriveBifunctor ''(:>>))
 

bootstrap/src/Tlang/Emit.hs

@@ -22,6 +22,7 @@ import LLVM.IRBuilder
 import Tlang.AST hiding (Type)
 import Tlang.Generic ((:+:) (..))
 import Tlang.Extension
+import Tlang.Constraint (Prefix (..), Prefixes (..))
 
 import Data.Maybe (fromMaybe)
 import Data.Kind (Constraint, Type)
@@ -60,8 +61,8 @@ instance (OperandGen f, OperandGen g) => OperandGen (f :+: g) where
   genOperand (Inl fv) = genOperand fv
   genOperand (Inr fv) = genOperand fv
 
-type instance CodeGenEnv m (VisibleType typ) = (MonadFail m)
-instance OperandGen (VisibleType typ) where
+type instance CodeGenEnv m (Value typ) = (MonadFail m)
+instance OperandGen (Value typ) where
   genOperand _ = fail "VisibleType is not supported for now"
 
 type instance CodeGenEnv m Apply = (MonadFail m)
@@ -193,8 +194,8 @@ instance OperandGen (Constructor l) where
   genOperand _ = do
     error "constructor not defined"
 
-type instance CodeGenEnv m (Lambda pattern' prefix) = ()
-instance OperandGen pattern' => OperandGen (Lambda pattern' prefix) where
+type instance CodeGenEnv m (Equation pattern' prefix) = ()
+instance OperandGen pattern' => OperandGen (Equation pattern' prefix) where
   genOperand _ = do
     error "lambda not defined"
 
@@ -219,8 +220,8 @@ instance (GlobalGen f a, GlobalGen g a) => GlobalGen (f :+: g) a where
   genGlobal (Inl fv) = genGlobal fv
   genGlobal (Inr fv) = genGlobal fv
 
-type instance GlobalGenEnv m (UserType typ [Bound Name typ]) a = ()
-instance GlobalGen (UserType typ [Bound Name typ]) a where
+type instance GlobalGenEnv m (UserType typ [Prefix Name typ]) a = ()
+instance GlobalGen (UserType typ [Prefix Name typ]) a where
   genGlobal _ = return Nothing
 
 type instance GlobalGenEnv m UserItem a = ()
@@ -235,9 +236,9 @@ type instance GlobalGenEnv m (UserValue expr (Maybe typ)) a = ()
 instance GlobalGen (UserValue expr (Maybe typ)) a where
   genGlobal _ = return Nothing
 
-type instance GlobalGenEnv m (UserData [Bound Name typ] def) a = ()
-instance GlobalGen (UserData [Bound Name typ] def) a where
+type instance GlobalGenEnv m (UserData [Prefix Name typ] def) a = ()
+instance GlobalGen (UserData [Prefix Name typ] def) a where
   genGlobal _ = return Nothing
 
 
---   :+: UserData [Bound Name typ] (UserDataDef (UserPhantom :+: UserCoerce :+: UserEnum Label :+: UserStruct Label) typ)
+--   :+: UserData [Prefix Name typ] (UserDataDef (UserPhantom :+: UserCoerce :+: UserEnum Label :+: UserStruct Label) typ)

bootstrap/src/Tlang/Extension.hs

@@ -10,6 +10,8 @@ module Tlang.Extension
     -- ** common structure
   , Tuple (..)
   , Record (..)
+  , Value (..)
+  , Cast (..)
 
     -- ** reexport other extensions
   , module Type
@@ -38,6 +40,14 @@ newtype LiteralNatural a = LiteralNatural (Literal Integer a) deriving (Show, Eq
 newtype LiteralInteger a = LiteralInteger (Literal Integer a) deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
 newtype LiteralNumber a = LiteralNumber (Literal Double a) deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
 
+-- | Inject any constant into the expression
+newtype Value val a = Value val
+  deriving (Eq, Ord, Functor, Foldable, Traversable)
+  deriving Show via val
+
+-- | Type or Kind casting
+data Cast t a = Cast t a
+  deriving (Show, Eq, Functor)
 
 -- | builtin tuple
 newtype Tuple a

bootstrap/src/Tlang/Extension/Expr.hs

@@ -2,30 +2,49 @@ module Tlang.Extension.Expr
   (
     -- ** expresion structure
     Let (..)
-  , Lambda (..)
+  , Letrec (..)
+  , Equation (..)
   , Apply (..)
   , Selector (..)
   , Constructor (..)
 
-  , VisibleType (..)
-  , TypeApply (..)
-
-  , Inst (..)
+  , Lambda (..)
+  , Coerce (..)
+  , Match (..)
   )
 where
 
+-- ** Surface Language
 
 -- | local name binding
 data Let binder expr
   = Let (binder expr) expr expr
   deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
 
--- | Lambda computation block, support both light and heavy notation
-data Lambda pattern' prefix expr
-  = Lambda prefix (pattern' expr, expr) [(pattern' expr, expr)]
+-- | a helper to distinguish recursive and non-recursive binding
+data Letrec binder expr
+  = Letrec [(binder expr, expr)] expr
+
+-- | equation group, syntax of lambda for surface language.
+-- it supports both light and heavy notation.
+--
+-- e.g.
+--    identity: [ ?a = a ]
+--    identity2: \ ?a => a
+--    const: [ ?v, _ = v ]
+--    const2: \ ?v, _ => v
+--    const3: \ ?v => \_ => v
+data Equation bind prefix expr
+  = Equation prefix
+      (bind expr, expr)
+      [(bind expr, expr)]
   deriving (Show, Eq, Functor, Foldable, Traversable)
 
--- | application
+-- | application, this includes both value application and type application
+--
+-- e.g.
+--    ( \ ?a -> a) 3 := Apply (Lambda a -> a) 3 []
+--    List @int := Apply List int []
 data Apply expr
   = Apply expr expr [expr]
   deriving (Show, Eq, Functor, Foldable, Traversable)
@@ -35,20 +54,30 @@ newtype Selector name e = Selector name deriving (Show, Eq, Ord, Functor, Foldab
 -- | @`Variant@ for polymorphic variant, variant constructor
 data Constructor name e = Constructor name [e] deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
 
--- | type instantiation
-data Inst name typ
-  = InstOne       -- identity
-  | InstTyp typ   -- bottom
-  | InstNew name  -- abstract
-  | InstInside (Inst name typ)
-  | InstUnder name (Inst name typ)
-  | InstElim
-  | InstIntro
-  | InstSeq (Inst name typ) (Inst name typ)
+-- ** Core Language Extension
+
+-- | type computation.
+--
+-- this data type inserts witness of a type coercing instead of simply
+-- expressing "coercing" in the core language.
+--
+-- e.g.
+--    (forall (a > ⊥). a) < int := (forall a. a) (CoerceTrans (CoerceIn (CoerceBot int)) CoerceElim)
+--                              := int
+data Coerce name typ
+  = CoerceRefl      -- ^ identity
+  | CoerceBot typ   -- ^ bottom, if target type is Bot then replace it with __typ__
+  | CoerceHyp name  -- ^ abstract, replace type t with a if a :> t
+  | CoerceIn  (Coerce name typ) -- ^ Inner instantiation
+  | CoerceOut (Coerce name typ) -- ^ Outer instantiation
+  | CoerceElim      -- ^ remove binder and substitution var with bounded typ
+  | CoerceIntro     -- ^ add a new binder
+  | CoerceTrans (Coerce name typ) (Coerce name typ) -- ^ sequel application of type computation
   deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
 
-data VisibleType typ e = VisibleType typ e deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
+-- | function block, basic computation block, support both type abstraction and value abstraction
+data Lambda bind e = Lambda (bind e) e deriving (Show, Eq, Ord, Functor)
 
--- | type application, this alters inner types of expression for codegen.
--- like reduce type variable of `Lambda`
-data TypeApply op expr = TypeApply op expr deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
+-- | pattern match expression
+data Match pat e
+  = Match e [(pat e, e)]

bootstrap/src/Tlang/Graph/Type.hs

@@ -15,7 +15,7 @@ import Data.GraphViz.Attributes.Complete (Label (StrLabel))
 import Data.Text.Lazy (pack)
 import Tlang.Graph.Core
 
-import Tlang.AST (Symbol (..), Variance (..))
+import Tlang.AST (Variance (..))
 
 -- | label for edge
 data GEdge a

bootstrap/src/Tlang/Inference/Graph.hs

@@ -53,6 +53,7 @@ import Data.Text (pack)
 import Tlang.Extension.Type as Ext
 import Tlang.Extension as Ext
 import Tlang.Generic
+import Tlang.Constraint (Prefix (..), Prefixes (..))
 
 import Tlang.Graph.Type
 import Tlang.Graph.Operation
@@ -73,7 +74,7 @@ simplify r g =
 
 runRestore
   :: forall label lit m rep bind a.
-    (Show label, MonadFail m, Forall (Bound Name) :<: bind, Scope (Bound Name) :<: bind
+    (Show label, MonadFail m, Forall (Prefix Name) :<: bind, Scope (Prefix Name) :<: bind
    , Const lit :<: rep, Record label :<: rep, Variant label :<: rep, Tuple :<: rep)
   => Node
   -> Gr (GNode (GNodeLabel lit label Name)) (GEdge Name)
@@ -93,7 +94,7 @@ injTypeLit = Type . inj
 restore
   :: ( MonadReader (Gr (GNode (GNodeLabel lit label name)) (GEdge name)) m
      , MonadState ([(Node, name)], Int) m, Show label, MonadFail m
-     , Forall (Bound name) :<: bind, Scope (Bound name) :<: bind
+     , Forall (Prefix name) :<: bind, Scope (Prefix name) :<: bind
      , Tuple :<: rep, Record label :<: rep, Variant label :<: rep, Const lit :<: rep
      , Eq name
      )