Skip to content

Commit

Permalink
[refactor] Decl -> FuncDecl; move out from Syntax.Common (#414)
Browse files Browse the repository at this point in the history
* [refactor] Decl -> FuncDecl; move out from Syntax.Common

* [refactor] TermDecl -> CoreFuncDecl
  • Loading branch information
croyzor committed Jul 22, 2024
1 parent c64dec9 commit 4f37947
Show file tree
Hide file tree
Showing 13 changed files with 98 additions and 93 deletions.
1 change: 1 addition & 0 deletions brat/Brat/Checker/Clauses.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ import Brat.Naming
import Brat.Syntax.Abstractor
import Brat.Syntax.Common
import Brat.Syntax.Core
import Brat.Syntax.FuncDecl (FunBody(..))
import Brat.Syntax.Simple
import Brat.Syntax.Value
import Brat.UserName
Expand Down
2 changes: 1 addition & 1 deletion brat/Brat/Compiler.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,9 @@ import Brat.Error
import Brat.Load
import Brat.Naming (root, split)

import qualified Data.ByteString.Lazy as BS
import Control.Monad (when)
import Control.Monad.Except
import qualified Data.ByteString.Lazy as BS
import System.Exit (die)

printDeclsHoles :: [FilePath] -> String -> IO ()
Expand Down
24 changes: 13 additions & 11 deletions brat/Brat/Elaborator.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,9 @@ import Data.Map (empty)

import Brat.FC
import Brat.Syntax.Common
import Brat.Syntax.Raw
import Brat.Syntax.Concrete
import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..))
import Brat.Syntax.Raw
import Brat.Error

assertSyn :: Dirable d => WC (Raw d k) -> Either Error (WC (Raw Syn k))
Expand Down Expand Up @@ -202,16 +203,17 @@ elabBody (FNoLhs e) _ = do
_ -> (assertUVerb e) >>= \e -> pure $ ThunkOf (WC (fcOf e) (NoLhs e))
elabBody FUndefined _ = pure Undefined

elabDecl :: FDecl -> Either Error RawDecl
elabDecl d = do
elabFunDecl :: FDecl -> Either Error RawFuncDecl
elabFunDecl d = do
rc <- elabBody (fnBody d) (fnLoc d)
pure $ Decl { fnName = fnName d
, fnLoc = fnLoc d
, fnSig = fnSig d
, fnBody = rc
, fnRT = fnRT d
, fnLocality = fnLocality d
}
pure $ FuncDecl
{ fnName = fnName d
, fnLoc = fnLoc d
, fnSig = fnSig d
, fnBody = rc
, fnLocality = fnLocality d
}


elabEnv :: FEnv -> Either Error RawEnv
elabEnv (ds, x) = (,x,empty) <$> forM ds elabDecl
elabEnv (ds, x) = (,x,empty) <$> forM ds elabFunDecl
3 changes: 2 additions & 1 deletion brat/Brat/Load.hs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ import Brat.Parser
import Brat.Syntax.Common
import Brat.Syntax.Concrete (FEnv)
import Brat.Syntax.Core
import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..), Locality(..))
import Brat.Syntax.Raw
import Brat.Syntax.Value
import Brat.UserName
Expand Down Expand Up @@ -60,7 +61,7 @@ emptyMod = (M.empty, [], [], initStore, (M.empty, []))
-- the box that is created for it. For simple `NoLhs` definitions, we return
-- Nothing.
checkDecl :: Prefix -> VDecl -> [(Tgt, BinderType Brat)] -> Checking ()
checkDecl pre (VDecl Decl{..}) to_define = localFC fnLoc $ do
checkDecl pre (VDecl FuncDecl{..}) to_define = localFC fnLoc $ do
trackM "\nCheckDecl:"
unless (fnLocality == Local) $ err $ InternalError "checkDecl called on ext function"
getFunTy fnSig >>= \case
Expand Down
34 changes: 17 additions & 17 deletions brat/Brat/Parser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import qualified Brat.Lexer.Token as Lexer
import Brat.Syntax.Abstractor
import Brat.Syntax.Common hiding (end)
import qualified Brat.Syntax.Common as Syntax
import Brat.Syntax.FuncDecl (FuncDecl(..), Locality(..))
import Brat.Syntax.Concrete
import Brat.Syntax.Raw
import Brat.Syntax.Simple
Expand Down Expand Up @@ -515,8 +516,7 @@ cnoun pe = do

decl :: Parser FDecl
decl = do
(WC fc (nm, ty, body, rt)) <- withFC (do
rt <- pure RtLocal -- runtime
(WC fc (nm, ty, body)) <- withFC (do
nm <- simpleName
ty <- try (functionType <&> \ty -> [Named "thunk" (Right ty)])
<|> (match TypeColon >> outputs)
Expand All @@ -526,14 +526,14 @@ decl = do
_ -> False
body <- if allow_clauses then (FClauses <$> clauses nm) <|> (FNoLhs <$> nbody nm)
else FNoLhs <$> nbody nm
pure (nm, ty, body, rt))
pure $ Decl { fnName = nm
, fnLoc = fc
, fnSig = ty
, fnBody = body
, fnRT = rt
, fnLocality = Local
}
pure (nm, ty, body))
pure $ FuncDecl
{ fnName = nm
, fnLoc = fc
, fnSig = ty
, fnBody = body
, fnLocality = Local
}
where
is_fun_ty :: RawVType -> Bool
is_fun_ty (RFn _) = True
Expand Down Expand Up @@ -665,13 +665,13 @@ pstmt = ((comment <?> "comment") <&> \_ -> ([] , []))
Just (ext, op) -> pure (intercalate "." ext, op)
Nothing -> fail $ "Malformed op name: " ++ symbol
pure (fnName, ty, (ext, op))
pure Decl { fnName = fnName
, fnSig = ty
, fnBody = FUndefined
, fnLoc = fc
, fnRT = RtLocal
, fnLocality = Extern symbol
}
pure FuncDecl
{ fnName = fnName
, fnSig = ty
, fnBody = FUndefined
, fnLoc = fc
, fnLocality = Extern symbol
}
where
nDecl = match TypeColon >> outputs
vDecl = (:[]) . Named "thunk" . Right <$> functionType
Expand Down
45 changes: 0 additions & 45 deletions brat/Brat/Syntax/Common.hs
Original file line number Diff line number Diff line change
@@ -1,19 +1,13 @@
{-# LANGUAGE AllowAmbiguousTypes, QuantifiedConstraints, UndecidableInstances #-}

module Brat.Syntax.Common (PortName,
Dir(..),
Kind(..),
Diry(..),
Kindy(..),
CType'(..),
pattern Extern, pattern Local, -- No reason not to export Locality if required
Decl'(..),
Import(..),
ImportSelection(..),
Runtime(RtLocal), -- No reason not to export others if required
Pattern(..),
Abstractor(..), occursInAbstractor,
FunBody(..),
TypeKind(..), KindOr,
showSig,
showRow,
Expand Down Expand Up @@ -52,7 +46,6 @@ import Brat.UserName

import Data.Bifunctor (first)
import Data.List (intercalate)
import Data.List.NonEmpty (NonEmpty(..))
import Data.Kind (Type)
import Data.Type.Equality (TestEquality(..), (:~:)(..))

Expand Down Expand Up @@ -161,17 +154,6 @@ deriving instance Eq io => Eq (CType' io)
instance Semigroup (CType' (PortName, ty)) where
(ss :-> ts) <> (us :-> vs) = (ss <> us) :-> (ts <> vs)

data Locality = Extern (String, String) | Local deriving (Eq, Show)

data Decl' (io :: Type) (body :: Type)
= Decl { fnName :: String
, fnSig :: io
, fnBody :: body
, fnLoc :: FC
, fnRT :: Runtime
, fnLocality :: Locality
}

data Import
= Import { importName :: WC UserName
, importQualified :: Bool
Expand All @@ -186,13 +168,6 @@ data ImportSelection
| ImportHiding [WC String]
deriving (Eq, Ord)

deriving instance
forall tm io.
(forall d k. Eq (tm d k), Eq io
,Eq (FunBody tm Noun)
,Eq (FunBody tm UVerb)
) => Eq (Decl' io (FunBody tm Noun))

instance Show Import where
show Import{..} =
let prefix = if importQualified then [] else ["open"]
Expand All @@ -203,26 +178,6 @@ instance Show Import where
showSelection (ImportPartial fns) = "(":(unWC <$> fns) ++ [")"]
showSelection (ImportHiding fns) = "hiding (":(unWC <$> fns) ++ [")"]


instance (Show io, Show (FunBody tm Noun))
=> Show (Decl' io (FunBody tm Noun)) where
show Decl{..} = unlines [fnName ++ " :: " ++ show fnSig
,fnName ++ " = " ++ show fnBody]

-- TODO: allow combinations thereof
-- default to local
data Runtime = RtTierkreis | RtLocal | RtKernel deriving (Eq, Show)

data FunBody (tm :: Dir -> Kind -> Type) (k :: Kind) where
-- lhs and rhs
ThunkOf :: WC (FunBody tm UVerb) -> FunBody tm Noun
Clauses :: NonEmpty (WC Abstractor, WC (tm Chk Noun)) -> FunBody tm UVerb
NoLhs :: (WC (tm Chk k)) -> FunBody tm k
Undefined :: FunBody tm k

deriving instance (forall d k. Show (tm d k)) => Show (FunBody tm k)
deriving instance (forall d k. Eq (tm d k)) => Eq (FunBody tm k)

showSig :: Show ty => [(String, ty)] -> String
showSig [] = "()"
showSig (x:xs)
Expand Down
3 changes: 2 additions & 1 deletion brat/Brat/Syntax/Concrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import Data.List.NonEmpty

import Brat.FC
import Brat.Syntax.Common
import Brat.Syntax.FuncDecl (FuncDecl(..))
import Brat.Syntax.Raw
import Brat.Syntax.Simple
import Brat.UserName
Expand All @@ -14,7 +15,7 @@ data FBody
| FUndefined
deriving Show

type FDecl = Decl' [RawIO] FBody
type FDecl = FuncDecl [RawIO] FBody
deriving instance Show FDecl
type FEnv = ([FDecl], [RawAlias])

Expand Down
5 changes: 3 additions & 2 deletions brat/Brat/Syntax/Core.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module Brat.Syntax.Core (Term(..)
,Output
,InOut
,CType
,Decl
,CoreFuncDecl
,Precedence(..)
,precedence
) where
Expand All @@ -16,6 +16,7 @@ import Brat.Constructors.Patterns (pattern CCons,
import Brat.FC
import Brat.Naming
import Brat.Syntax.Common
import Brat.Syntax.FuncDecl
import Brat.Syntax.Simple
import Brat.UserName

Expand All @@ -28,7 +29,7 @@ type InOut = (PortName, KindOr (Term Chk Noun))

type CType = CType' InOut

type Decl = Decl' [InOut] (FunBody Term Noun)
type CoreFuncDecl = FuncDecl [InOut] (FunBody Term Noun)

data Term :: Dir -> Kind -> Type where
Simple :: SimpleTerm -> Term Chk Noun
Expand Down
43 changes: 43 additions & 0 deletions brat/Brat/Syntax/FuncDecl.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}

module Brat.Syntax.FuncDecl where

import Brat.FC (FC, WC)
import Brat.Syntax.Abstractor (Abstractor)
import Brat.Syntax.Common (Dir(..), Kind(..))

import Data.Kind (Type)
import Data.List.NonEmpty (NonEmpty)

data Locality = Extern (String, String) | Local deriving (Eq, Show)

data FuncDecl (io :: Type) (body :: Type) = FuncDecl
{ fnName :: String
, fnSig :: io
, fnBody :: body
, fnLoc :: FC
, fnLocality :: Locality
}

deriving instance
forall tm io.
(forall d k. Eq (tm d k), Eq io
,Eq (FunBody tm Noun)
,Eq (FunBody tm UVerb)
) => Eq (FuncDecl io (FunBody tm Noun))


instance (Show io, Show (FunBody tm Noun))
=> Show (FuncDecl io (FunBody tm Noun)) where
show FuncDecl{..} = unlines [fnName ++ " :: " ++ show fnSig
,fnName ++ " = " ++ show fnBody]

data FunBody (tm :: Dir -> Kind -> Type) (k :: Kind) where
-- lhs and rhs
ThunkOf :: WC (FunBody tm UVerb) -> FunBody tm Noun
Clauses :: NonEmpty (WC Abstractor, WC (tm Chk Noun)) -> FunBody tm UVerb
NoLhs :: (WC (tm Chk k)) -> FunBody tm k
Undefined :: FunBody tm k

deriving instance (forall d k. Show (tm d k)) => Show (FunBody tm k)
deriving instance (forall d k. Eq (tm d k)) => Eq (FunBody tm k)
14 changes: 7 additions & 7 deletions brat/Brat/Syntax/Raw.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ import Brat.FC hiding (end)
import Brat.Naming
import Brat.Syntax.Common
import Brat.Syntax.Core
import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..))
import Brat.Syntax.Simple
import Brat.UserName
import Util (names, (**^))
Expand All @@ -41,8 +42,8 @@ type TypeAlias = TypeAliasF (Term Chk Noun)

type TypeAliasTable = M.Map UserName TypeAlias

type RawDecl = Decl' [RawIO] (FunBody Raw Noun)
type RawEnv = ([RawDecl], [RawAlias], TypeAliasTable)
type RawEnv = ([RawFuncDecl], [RawAlias], TypeAliasTable)
type RawFuncDecl = FuncDecl [RawIO] (FunBody Raw Noun)

addNames :: TypeRow ty -> [(PortName, ty)]
addNames tms = aux (fromList names) tms
Expand Down Expand Up @@ -307,9 +308,9 @@ desugarVBody (Clauses cs) = Clauses <$> mapM branch cs
desugarVBody (NoLhs rhs) = NoLhs <$> desugar rhs
desugarVBody Undefined = pure Undefined

instance Desugarable RawDecl where
type Desugared RawDecl = Decl
desugar' d@Decl{..} = do
instance Desugarable RawFuncDecl where
type Desugared RawFuncDecl = CoreFuncDecl
desugar' d@FuncDecl{..} = do
tys <- addNames <$> desugar' fnSig
noun <- desugarNBody fnBody
pure $ d { fnBody = noun
Expand All @@ -329,9 +330,8 @@ desugarAliases (a@(TypeAlias fc name _ _):as) = do
local (\((decls, aliases, aliasTbl), uz) -> ((decls, aliases, M.insert name a aliasTbl), uz)) $
(a :) <$> desugarAliases as

desugarEnv :: RawEnv -> Either Error ([Decl], [TypeAlias])
desugarEnv :: RawEnv -> Either Error ([CoreFuncDecl], [TypeAlias])
desugarEnv env@(decls, aliases, aliasTbl)
-- desugarEnv env@(decls, aliases)
= fmap fst
. runExcept
. flip runReaderT (env, B0)
Expand Down
9 changes: 5 additions & 4 deletions brat/Brat/Syntax/Value.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ module Brat.Syntax.Value {-(VDecl
import Brat.Error
import Brat.Syntax.Common
import Brat.Syntax.Core (Term (..))
import Brat.Syntax.FuncDecl (FunBody, FuncDecl(..))
import Brat.UserName
import Bwd
import Hasochism
Expand All @@ -34,14 +35,14 @@ import Data.Ord (comparing)
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))

newtype VDecl = VDecl (Decl' (Some (Ro Brat Z)) (FunBody Term Noun))
newtype VDecl = VDecl (FuncDecl (Some (Ro Brat Z)) (FunBody Term Noun))

instance MODEY Brat => Show VDecl where
show (VDecl decl) = show $ aux decl
where
aux :: Decl' (Some (Ro Brat Z)) body -> Decl' String body
aux (Decl { .. }) = case fnSig of
Some sig -> Decl { fnName = fnName, fnSig = (show sig), fnBody = fnBody, fnLoc = fnLoc, fnRT = fnRT, fnLocality = fnLocality }
aux :: FuncDecl (Some (Ro Brat Z)) body -> FuncDecl String body
aux (FuncDecl { .. }) = case fnSig of
Some sig -> FuncDecl { fnName = fnName, fnSig = (show sig), fnBody = fnBody, fnLoc = fnLoc, fnLocality = fnLocality }

------------------------------------ Variable Indices ------------------------------------
-- Well scoped de Bruijn indices
Expand Down
1 change: 1 addition & 0 deletions brat/brat.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,7 @@ library
Brat.Elaborator,
Brat.Syntax.Abstractor,
Brat.Syntax.Concrete,
Brat.Syntax.FuncDecl,
Brat.Syntax.Port,
Brat.Syntax.Simple,
Brat.UserName,
Expand Down
Loading

0 comments on commit 4f37947

Please sign in to comment.