add translation from abstract to MiniHaskell

src/MiniJuvix/Syntax/Abstract/Language.hs

@@ -161,3 +161,4 @@ makeLenses ''FunctionClause
 makeLenses ''InductiveDef
 makeLenses ''ModuleBody
 makeLenses ''InductiveConstructorDef
+makeLenses ''ConstructorApp

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

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
 

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

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

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,20 +57,18 @@ 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,
+data Function = Function {
+  _funParameters :: NonEmpty Type,
   _funReturn :: Type
   }
 
@@ -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

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