From d061dc8a39884a5efb517e87b7f3ab6c4bcfe89e Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 15 Mar 2022 10:18:13 +0100 Subject: [PATCH] add translation from abstract to MiniHaskell --- src/MiniJuvix/Syntax/Abstract/Language.hs | 1 + src/MiniJuvix/Syntax/Concrete/Name.hs | 14 +- src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs | 3 + .../Syntax/Concrete/Scoped/Pretty/Base.hs | 2 +- .../Syntax/Concrete/Scoped/Scoper.hs | 2 +- src/MiniJuvix/Syntax/MiniHaskell/Language.hs | 23 +-- .../Translation/AbstractToMiniHaskell.hs | 134 ++++++++++++++++++ 7 files changed, 160 insertions(+), 19 deletions(-) create mode 100644 src/MiniJuvix/Translation/AbstractToMiniHaskell.hs diff --git a/src/MiniJuvix/Syntax/Abstract/Language.hs b/src/MiniJuvix/Syntax/Abstract/Language.hs index 3619d5a4a..2ecde1746 100644 --- a/src/MiniJuvix/Syntax/Abstract/Language.hs +++ b/src/MiniJuvix/Syntax/Abstract/Language.hs @@ -161,3 +161,4 @@ makeLenses ''FunctionClause makeLenses ''InductiveDef makeLenses ''ModuleBody makeLenses ''InductiveConstructorDef +makeLenses ''ConstructorApp diff --git a/src/MiniJuvix/Syntax/Concrete/Name.hs b/src/MiniJuvix/Syntax/Concrete/Name.hs index 19948fc9e..13e4bd900 100644 --- a/src/MiniJuvix/Syntax/Concrete/Name.hs +++ b/src/MiniJuvix/Syntax/Concrete/Name.hs @@ -63,16 +63,16 @@ makeLenses ''QualifiedName -- | A.B.C corresponds to TopModulePath [A,B] C data TopModulePath = TopModulePath - { modulePathDir :: [Symbol], - modulePathName :: Symbol + { _modulePathDir :: [Symbol], + _modulePathName :: Symbol } deriving stock (Show, Eq, Ord, Generic) instance HasLoc TopModulePath where getLoc TopModulePath {..} = - case modulePathDir of - [] -> getLoc modulePathName - (x : _) -> getLoc x <> getLoc modulePathName + case _modulePathDir of + [] -> getLoc _modulePathName + (x : _) -> getLoc x <> getLoc _modulePathName topModulePathToFilePath :: FilePath -> TopModulePath -> FilePath topModulePathToFilePath = topModulePathToFilePath' (Just ".mjuvix") @@ -81,8 +81,8 @@ topModulePathToFilePath' :: Maybe String -> FilePath -> TopModulePath -> FilePath topModulePathToFilePath' ext root mp = absPath where - relDirPath = foldr (() . toPath) mempty (modulePathDir mp) - relFilePath = relDirPath toPath (modulePathName mp) + relDirPath = foldr (() . toPath) mempty (_modulePathDir mp) + relFilePath = relDirPath toPath (_modulePathName mp) absPath = case ext of Nothing -> root relFilePath Just e -> root relFilePath <.> e diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs index 86b0182ae..c1a781b66 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs @@ -106,6 +106,9 @@ isConstructor Name' {..} = case _nameKind of fromQualifiedName :: C.QualifiedName -> C.Symbol fromQualifiedName (C.QualifiedName _ s) = s +topModulePathName :: TopModulePath -> Symbol +topModulePathName = over nameConcrete C._modulePathName + symbolText :: Symbol -> Text symbolText = C._symbolText . _nameConcrete diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs index 038e9acac..2314338cf 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs @@ -378,7 +378,7 @@ annSDef S.Name' {..} = annotate (AnnDef (S.absTopModulePath _nameDefinedIn) _nam instance PrettyCode TopModulePath where ppCode TopModulePath {..} = - dotted <$> mapM ppSymbol (modulePathDir ++ [modulePathName]) + dotted <$> mapM ppSymbol (_modulePathDir ++ [_modulePathName]) instance PrettyCode Symbol where ppCode = return . pretty . _symbolText diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs index d8a9a2c1c..a6e85bee8 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs @@ -461,7 +461,7 @@ checkTopModule m@(Module path params body) = do _nameId <- freshNameId let _nameDefinedIn = S.topModulePathToAbsPath path _nameConcrete = path - _nameDefined = getLoc $ modulePathName path + _nameDefined = getLoc (_modulePathName path) _nameKind = S.KNameTopModule _nameFixity = Nothing _namePublicAnn = NoPublic diff --git a/src/MiniJuvix/Syntax/MiniHaskell/Language.hs b/src/MiniJuvix/Syntax/MiniHaskell/Language.hs index bc8478203..0745741d0 100644 --- a/src/MiniJuvix/Syntax/MiniHaskell/Language.hs +++ b/src/MiniJuvix/Syntax/MiniHaskell/Language.hs @@ -29,6 +29,9 @@ instance Ord Name where instance Hashable Name where hashWithSalt salt = hashWithSalt salt . _nameId +instance HasNameKind Name where + getNameKind = _nameKind + data Module = Module { _moduleName :: Name, _moduleBody :: ModuleBody @@ -54,21 +57,19 @@ data Iden = IdenDefined Name | IdenConstructor Name | IdenVar VarName - | IdenAxiom Name data Expression = ExpressionIden Iden | ExpressionApplication Application - | ExpressionFunction Function data Application = Application { - _appLeft :: Expression, - _appRight :: Expression + _appFunction :: FunctionName, + _appArguments :: [Expression] } -data Function = Function - { _funParameter :: Type, - _funReturn :: Type +data Function = Function { + _funParameters :: NonEmpty Type, + _funReturn :: Type } -- | Fully applied constructor in a pattern. @@ -84,17 +85,19 @@ data Pattern data InductiveDef = InductiveDef { _inductiveName :: InductiveName, - _inductiveType :: Maybe Expression, _inductiveConstructors :: [InductiveConstructorDef] } data InductiveConstructorDef = InductiveConstructorDef { _constructorName :: ConstrName, - _constructorType :: Type + _constructorParameters :: [Type] } +newtype TypeIden = + TypeIdenInductive InductiveName + data Type = - TypeInductive InductiveName + TypeIden TypeIden | TypeFunction Function makeLenses ''Module diff --git a/src/MiniJuvix/Translation/AbstractToMiniHaskell.hs b/src/MiniJuvix/Translation/AbstractToMiniHaskell.hs new file mode 100644 index 000000000..ce441b010 --- /dev/null +++ b/src/MiniJuvix/Translation/AbstractToMiniHaskell.hs @@ -0,0 +1,134 @@ +module MiniJuvix.Translation.AbstractToMiniHaskell where + +import MiniJuvix.Prelude +import qualified MiniJuvix.Syntax.Abstract.Language.Extra as A +import qualified MiniJuvix.Syntax.Usage as A +import MiniJuvix.Syntax.MiniHaskell.Language +import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S +import qualified Data.HashMap.Strict as HashMap + +translateModule :: A.TopModule -> Module +translateModule m = Module { + _moduleName = goTopModuleName (m ^. A.moduleName), + _moduleBody = goModuleBody (m ^. A.moduleBody) + } + +goTopModuleName :: A.TopModuleName -> Name +goTopModuleName = goSymbol . S.topModulePathName + +goName :: S.Name -> Name +goName = goSymbol . S.nameUnqualify + +goSymbol :: S.Symbol -> Name +goSymbol s = Name { + _nameText = S.symbolText s, + _nameId = S._nameId s, + _nameKind = getNameKind s + } + +unsupported :: Text -> a +unsupported thing = error ("Not yet supported: " <> thing) + +goModuleBody :: A.ModuleBody -> ModuleBody +goModuleBody b + | not (HashMap.null (b ^. A.moduleLocalModules)) = unsupported "local modules" + | otherwise = ModuleBody { + _moduleInductives = HashMap.fromList [ (d ^. inductiveName, d) + | d <- map goInductiveDef (toList (b ^. A.moduleInductives))], + _moduleFunctions = HashMap.fromList [] + } + +goTypeIden :: A.Iden -> TypeIden +goTypeIden i = case i of + A.IdenDefined {} -> unsupported "functions in types" + A.IdenConstructor {} -> unsupported "constructors in types" + A.IdenVar {} -> unsupported "type variables" + A.IdenInductive d -> TypeIdenInductive (goName d) + A.IdenAxiom {} -> unsupported "axioms in types" + +goFunctionParameter :: A.FunctionParameter -> Type +goFunctionParameter f = case f ^. A.paramName of + Just {} -> unsupported "named function arguments" + _ -> case f ^. A.paramUsage of + A.UsageOmega -> goType (f ^. A.paramType) + _ -> unsupported "usages" + +goFunction :: A.Function -> Function +goFunction = uncurry Function . viewFunctionType + +goFunctionDef :: A.FunctionDef -> FunctionDef +goFunctionDef f = FunctionDef { + _funDefName = goSymbol (f ^. A.funDefName), + _funDefTypeSig = goType (f ^. A.funDefTypeSig), + _funDefClauses = fmap goFunctionClause (f ^. A.funDefClauses) + } + +goFunctionClause :: A.FunctionClause -> FunctionClause +goFunctionClause c = FunctionClause { + _clausePatterns = map goPattern (c ^. A.clausePatterns), + _clauseBody = goExpression (c ^. A.clauseBody) + } + +goPattern :: A.Pattern -> Pattern +goPattern p = case p of + A.PatternVariable v -> PatternVariable (goSymbol v) + A.PatternConstructorApp c -> PatternConstructorApp (goConstructorApp c) + A.PatternWildcard -> PatternWildcard + A.PatternEmpty -> unsupported "pattern empty" + +goConstructorApp :: A.ConstructorApp -> ConstructorApp +goConstructorApp c = ConstructorApp (goName (c ^. A.constrAppConstructor)) + (map goPattern (c ^. A.constrAppParameters)) + +goType :: A.Expression -> Type +goType e = case e of + A.ExpressionIden i -> TypeIden (goTypeIden i) + A.ExpressionUniverse {} -> unsupported "universes in types" + A.ExpressionApplication {} -> unsupported "application in types" + A.ExpressionFunction f -> TypeFunction (goFunction f) + +goApplication :: A.Application -> Application +goApplication (A.Application f x) = Application (goExpression f) (goExpression x) + +goIden :: A.Iden -> Iden +goIden i = case i of + A.IdenDefined n -> IdenDefined (goName n) + A.IdenConstructor c -> IdenConstructor (goName c) + A.IdenVar v -> IdenVar (goSymbol v) + A.IdenAxiom {} -> unsupported "axiom identifier" + A.IdenInductive {} -> unsupported "inductive identifier" + +goExpression :: A.Expression -> Expression +goExpression e = case e of + A.ExpressionIden i -> ExpressionIden (goIden i) + A.ExpressionUniverse {} -> unsupported "universes in expression" + A.ExpressionFunction {} -> unsupported "function type in expressions" + A.ExpressionApplication a -> ExpressionApplication (goApplication a) + +goInductiveDef :: A.InductiveDef -> InductiveDef +goInductiveDef i = case i ^. A.inductiveType of + Just {} -> unsupported "inductive indices" + _ -> InductiveDef { + _inductiveName = indName, + _inductiveConstructors = map goConstructorDef (i ^. A.inductiveConstructors) + } + where + indName = goSymbol (i ^. A.inductiveName) + goConstructorDef :: A.InductiveConstructorDef -> InductiveConstructorDef + goConstructorDef c = InductiveConstructorDef { + _constructorName = goSymbol (c ^. A.constructorName), + _constructorParameters = goConstructorType (c ^. A.constructorType) + } + goConstructorType :: A.Expression -> [Type] + goConstructorType = fst . viewExpressionFunctionType + +viewExpressionFunctionType :: A.Expression -> ([Type], Type) +viewExpressionFunctionType e = case e of + A.ExpressionFunction f -> first toList (viewFunctionType f) + A.ExpressionIden i -> ([], TypeIden (goTypeIden i)) + A.ExpressionApplication {} -> unsupported "application in a type" + A.ExpressionUniverse {} -> unsupported "universe in a type" + +viewFunctionType :: A.Function -> (NonEmpty Type, Type) +viewFunctionType (A.Function p r) = (goFunctionParameter p :| args, ret) + where (args, ret) = viewExpressionFunctionType r