add syntax example (without usages). Adapt Language.hs

.gitignore

@@ -61,3 +61,4 @@ agda/
 agda2hs/
 docs/*.html
 *.cabal
+/src/MiniJuvix/Utils/OldParser.hs

examples/syntax.miniju

@@ -0,0 +1,51 @@
+-- The syntax is very similar to that of Agda. However, we need some extra ';'
+module Example where
+
+   -- The natural numbers can be inductively defined thus:
+   data ℕ : Type 0 ;
+      | zero : ℕ
+      | suc : ℕ → ℕ ;
+
+   -- A list of elements with typed size:
+   data Vec (A : Type) : ℕ → Type 0 ;
+     | nil : A → Vec A zero
+     | cons : (n : ℕ) → A → Vec A n → Vec A (suc n) ;
+
+   module ℕ-Ops where
+     infixl 6 + ;
+     + : ℕ → ℕ → ℕ ;
+     + zero b = b ;
+     + (suc a) b = suc (a + b) ;
+
+     infixl 7 * ;
+     * : ℕ → ℕ → ℕ ;
+     * zero b = zero ;
+     * (suc a) b = b + a * b ;
+   end
+
+   module M1 (A : Type 0) where
+      aVec : ℕ → Type 0 ;
+      aVec = Vec A ;
+   end
+
+   module Bot where
+      data ⊥ : Type 0 ;
+   end
+
+   open module M1 ℕ ;
+
+   two : ℕ ;
+   two = suc (suc zero) ;
+
+   id : (A : Type) → A → A ;
+   id _ = λ x → x ;
+
+   natVec : aVec (cons zero) ;
+   natVec = cons (two * two + one) nil ;
+     -- The 'where' part belongs to the clause
+     where
+     open module ℕ-Ops ;
+     one : ℕ ;
+     one = suc zero ;
+
+end

package.yaml

@@ -23,11 +23,13 @@ dependencies:
 - containers == 0.6.*
 - filepath == 1.4.*
 - megaparsec == 9.2.*
+- parser-combinators == 1.3.*
 - prettyprinter == 1.7.*
 - prettyprinter-ansi-terminal == 1.1.*
 - process == 1.6.*
 - relude == 1.0.*
 - semirings == 0.6.*
+- text == 1.2.*
 - unordered-containers == 0.2.*
 - word8 == 0.1.*
 
@@ -37,7 +39,7 @@ ghc-options:
 - -Wall -Wcompat -Widentities -Wincomplete-uni-patterns
 - -Wincomplete-record-updates -fwrite-ide-info -hiedir=.hie
 - -Wderiving-defaults -Wredundant-constraints
-- -fhide-source-paths -Wpartial-fields
+- -fhide-source-paths
 - -Wmissing-deriving-strategies
 
 default-extensions:

src/MiniJuvix/Parsing/Language.hs

@@ -1,40 +1,26 @@
-{-# OPTIONS_GHC -Wno-missing-export-lists #-}
-
 -- | Adapted from heliaxdev/Juvix/library/StandardLibrary/src/Juvix
 module MiniJuvix.Parsing.Language where
 
---------------------------------------------------------------------------------
 
 import MiniJuvix.Utils.Prelude
 
---------------------------------------------------------------------------------
-
 newtype Symbol = Sym Text
   deriving stock (Show, Read, Eq)
 
 type Name = NonEmpty Symbol
 
---------------------------------------------------------------------------------
--- File header
---------------------------------------------------------------------------------
-
-data FileHeader topLevel
-  = FileHeader Name [topLevel]
-  | NoFileHeader [topLevel]
-  deriving stock (Show, Read, Eq)
-
 --------------------------------------------------------------------------------
 -- Top level declaration
 --------------------------------------------------------------------------------
 
 data TopLevel
-  = FixityDeclaration Fixity
+  = OperatorDef OperatorSyntaxDef
   | TypeSignatureDeclaration TypeSignature
   | DataTypeDeclaration DataType
-  | RecordTypeDeclaration RecordType
+  --- | RecordTypeDeclaration RecordType
   | ModuleDeclaration Module
   | OpenModuleDeclaration OpenModule
-  | FunctionDeclaration Function
+  | FunctionClause FunctionClause
   deriving stock (Show, Read, Eq)
 
 --------------------------------------------------------------------------------
@@ -45,45 +31,61 @@ type Precedence = Natural
 
 type Operator = Name
 
-data FixityMode
-  = NonAssociative Operator Precedence
-  | LeftAssociative Operator Precedence
-  | RightAssociative Operator Precedence
+data UnaryAssoc = PrefixOp | PostfixOp
   deriving stock (Show, Read, Eq)
 
-newtype Fixity = Fixity FixityMode
+data BinaryAssoc = None | LeftAssoc | RightAssoc
+  deriving stock (Show, Read, Eq)
+
+data OperatorArity =
+  Unary {
+   unaryAssoc :: UnaryAssoc
+  }
+  | Binary {
+    binaryAssoc :: BinaryAssoc
+  }
+  deriving stock (Show, Read, Eq)
+
+data OperatorSyntaxDef =
+  OperatorSyntaxDef {
+  opArity :: OperatorArity
+  , opSymbol :: Operator
+  , opPrecedence :: Int
+  }
   deriving stock (Show, Read, Eq)
 
 ------------------------------------------------------------------------------
 -- Type signature declaration
---------------------------------------------------------------------------------
+------------------------------------------------------------------------------
 
 data TypeSignature
   = TypeSignature
-      { termName :: Name,
-        termQuantity :: Maybe Expression,
-        termContext :: [Expression],
-        termType :: Expression
+      {
+        sigName :: Name,
+        sigQuantity :: Maybe Expression,
+        sigType :: Expression
       }
   deriving stock (Show, Read, Eq)
 
 -----------------------------------------------------------------------------
 -- Data type construction declaration
-------------------------------------------------------------------------------
+-----------------------------------------------------------------------------
 
 type DataConstructorName = Name
 
 type DataTypeName = Name
 
-data DataConstructor
-  = DataConstructor DataTypeName DataConstructorName Expression
+data DataConstructorDef = DataConstructorDef {
+  constructorName :: DataConstructorName
+  , constructorType :: Expression
+  }
   deriving stock (Show, Read, Eq)
 
 data DataType
   = DataType
       { dataTypeName :: DataTypeName,
-        dataTypeParameters :: [Expression],
-        dataTypeConstructors :: [DataConstructor]
+        dataTypeArgs :: [Expression],
+        dataTypeConstructors :: [DataConstructorDef]
       }
   deriving stock (Show, Read, Eq)
 
@@ -91,50 +93,48 @@ data DataType
 -- Record type declaration
 ------------------------------------------------------------------------------
 
-type RecordFieldName = Name
+-- type RecordFieldName = Name
 
-type RecordTypeName = Name
+-- type RecordTypeName = Name
 
-data RecordField = RecordField RecordFieldName RecordTypeName Expression
-  deriving stock (Show, Read, Eq)
+-- data RecordField = RecordField {
+--   recordFieldName :: RecordFieldName,
+--   recordType :: Expression
+--   }
+--   deriving stock (Show, Read, Eq)
 
-data RecordType
-  = RecordType
-      { recordTypeName :: Name,
-        recordTypeConstructorName :: Name,
-        recordTypeParameters :: [Expression],
-        recordFields :: [RecordField]
-      }
-  deriving stock (Show, Read, Eq)
+-- data RecordType
+--   = RecordType
+--       { recordTypeName :: Name,
+--         recordTypeConstructorName :: Name,
+--         recordTypeArgs :: [Expression],
+--         recordFields :: [RecordField]
+--       }
+--   deriving stock (Show, Read, Eq)
 
 --------------------------------------------------------------------------------
 -- Function binding declaration
 --------------------------------------------------------------------------------
 
-type PreTypeName = Name
+type PreTermName = Name
 
-newtype RecordFieldData = Set [(Name, Expression)]
-  deriving stock (Show, Read, Eq)
+-- newtype RecordFieldData = Set [(Name, Expression)]
+--   deriving stock (Show, Read, Eq)
 
 data Pattern
   = PatternName Name
-  | PatternData DataConstructorName [Pattern]
-  | PatternRecord RecordTypeName RecordFieldData
-  | PatternPreTerm PreTypeName Name
+  | PatternConstructor DataConstructorName [Pattern]
+  --- | PatternRecord RecordTypeName RecordFieldData
+  | PatternPreTerm PreTermName Name
+  | PatternWildcard
   deriving stock (Show, Read, Eq)
 
 data FunctionClause
-  = FunctionClause
+  = FunClause
       { ownerFunction :: Name,
         clausePatterns :: [Pattern],
-        clauseBody :: Expression
-      }
-  deriving stock (Show, Read, Eq)
-
-data Function
-  = Function
-      { functionName :: Name,
-        clauses :: [FunctionClause]
+        clauseBody :: Expression,
+        clauseWhere :: Maybe WhereBlock
       }
   deriving stock (Show, Read, Eq)
 
@@ -145,7 +145,7 @@ data Function
 data Module
   = Module
       { moduleName :: Name,
-        moduleParameters :: [Expression],
+        moduleArgs :: [Expression],
         body :: [TopLevel]
       }
   deriving stock (Show, Read, Eq)
@@ -162,25 +162,17 @@ data Expression
   = IdentifierExpr Name
   | ApplicationExpr Application
   | LambdaExpr Lambda
-  | PatternExpr Pattern
-  | WhereBlockExpr WhereBlock
   | LetBlockExpr LetBlock
-  | ModuleExpr Module
   | OpenModuleExpr OpenModule
-  | PreTypeExpr PreType
   | PreTermExpr PreTerm
   | UniverseExpr Universe
-  | Parened Expression
   deriving stock (Show, Read, Eq)
 
 --------------------------------------------------------------------------------
 -- Pre- types and terms (a.k.a primitive types and terms)
 --------------------------------------------------------------------------------
 
-newtype PreType = PreType TypeSignature
-  deriving stock (Show, Read, Eq)
-
-newtype PreTerm = PreTerm TypeSignature -- PreType should be here somehow?
+newtype PreTerm = PreTerm PreTermName -- PreType should be here somehow?
   deriving stock (Show, Read, Eq)
 
 --------------------------------------------------------------------------------
@@ -191,10 +183,18 @@ newtype Universe = Universe Natural
   deriving stock (Show, Read, Eq)
 
 --------------------------------------------------------------------------------
--- Where block expression
+-- Where block clauses
 --------------------------------------------------------------------------------
 
-newtype WhereBlock = WhereBlock {blockExpressions :: [Expression]}
+newtype WhereBlock = WhereBlock {
+  whereClauses :: [WhereClause]
+  }
+  deriving stock (Show, Read, Eq)
+
+data WhereClause =
+  WhereOpenModule OpenModule
+  | WhereTypeSig TypeSignature
+  | WhereFunClause FunctionClause
   deriving stock (Show, Read, Eq)
 
 --------------------------------------------------------------------------------
@@ -217,8 +217,8 @@ data Lambda
 
 data Application
   = Application
-      { applicationName :: Expression,
-        applicationArgs :: NonEmpty Expression
+      { applicationFun :: Expression,
+        applicationArg :: Expression
       }
   deriving stock (Show, Read, Eq)
 

src/MiniJuvix/Parsing/Parser.hs

@@ -28,8 +28,8 @@ kwImport
   , kwModule
   , kwOpen
   , kwDataType
-  , kwRecordType
-  , kwRecordTypeConstructor
+  -- , kwRecordType
+  -- , kwRecordTypeConstructor
   , kwPretype
   , kwPreterm
   , kwUniverse
@@ -45,8 +45,8 @@ kwLet = "let"
 kwModule = "mod"
 kwOpen = "open"
 kwDataType = "data"
-kwRecordType = "record"
-kwRecordTypeConstructor = "constructor"
+-- kwRecordType = "record"
+-- kwRecordTypeConstructor = "constructor"
 kwPretype = "Pretype"
 kwPreterm = "Preterm"
 kwTypeSignature = "sig"
@@ -65,8 +65,8 @@ reservedWords =
       kwModule,
       kwOpen,
       kwDataType,
-      kwRecordType,
-      kwRecordTypeConstructor,
+      -- kwRecordType,
+      -- kwRecordTypeConstructor,
       kwTypeSignature,
       kwWhere
     ]
@@ -119,18 +119,18 @@ breakComment = ByteString.breakSubstring symComment
 -- e.g. "mod Main where"
 --------------------------------------------------------------------------------
 
-fileHeaderCase :: Parser (FileHeader TopLevel)
-fileHeaderCase = do
-  reserved kwModule
-  name <- prefixSymbolDotSN
-  reserved kwWhere
-  FileHeader name <$> P.some topLevelSN
+-- fileHeaderCase :: Parser FileHeader
+-- fileHeaderCase = do
+--   reserved kwModule
+--   name <- prefixSymbolDotSN
+--   reserved kwWhere
+--   FileHeader name <$> P.some topLevelSN
 
-noFileHeaderCase :: Parser (FileHeader TopLevel)
-noFileHeaderCase = NoFileHeader <$> P.some topLevelSN
+-- noFileHeaderCase :: Parser FileHeader
+-- noFileHeaderCase = NoFileHeader <$> P.some topLevelSN
 
-fileHeader :: Parser (FileHeader TopLevel)
-fileHeader = P.try fileHeaderCase <|> noFileHeaderCase
+-- fileHeader :: Parser FileHeader
+-- fileHeader = P.try fileHeaderCase <|> noFileHeaderCase
 
 ----------------------------------------------------------------------------
 -- Top Level
@@ -141,21 +141,22 @@ topLevelSN = spaceLiner topLevel
 
 topLevel :: Parser TopLevel
 topLevel =
-  P.try (FixityDeclaration <$> fixity)
-    <|> P.try (TypeSignatureDeclaration <$> typeSignature)
+  P.try
+    -- (FixityDeclaration <$> fixity)
+     (TypeSignatureDeclaration <$> typeSignature)
     <|> P.try (DataTypeDeclaration <$> dataTypeConstructor)
-    <|> P.try (RecordTypeDeclaration <$> recordTypeConstructor)
+    -- <|> P.try (RecordTypeDeclaration <$> recordTypeConstructor)
     <|> P.try (ModuleDeclaration <$> moduleD)
     <|> P.try (OpenModuleDeclaration <$> openModuleD)
-    <|> P.try (FunctionDeclaration <$> function)
+    -- <|> P.try (FunctionDeclaration <$> function)
 
 --------------------------------------------------------------------------------
 -- Fixity declarations
 -- e.g. "infixr _*_ 100"
 --------------------------------------------------------------------------------
 
-fixityDeclaration :: Parser FixityMode
-fixityDeclaration = undefined 
+-- fixityDeclaration :: Parser FixityMode
+-- fixityDeclaration = undefined
   -- do
   -- _ <- P.string kwInfix
   -- fixityMode <-
@@ -167,8 +168,8 @@ fixityDeclaration = undefined
   -- name <- prefixSymbolSN
   -- fixityMode name . fromInteger <$> spaceLiner integer
 
-fixity :: Parser Fixity
-fixity = Fixity <$> fixityDeclaration
+-- fixity :: Parser Fixity
+-- fixity = Fixity <$> fixityDeclaration
 
 --------------------------------------------------------------------------------
 -- Type signature
@@ -209,7 +210,7 @@ typeSignature = undefined
 -- e.g. "type T where" or "type T v1 where One : (p : v1) -> T p"
 --------------------------------------------------------------------------------
 
-parseDataConstructors :: Parser [ DataConstructor ]
+parseDataConstructors :: Parser [DataConstructorDef]
 parseDataConstructors = undefined
 
 dataTypeConstructorSN :: Parser DataType
@@ -231,11 +232,11 @@ dataTypeConstructor = undefined
 --         a : (v : Δ) → T₁ v
 --------------------------------------------------------------------------------
 
-parseRecordFields :: Parser RecordField
-parseRecordFields = undefined
+-- parseRecordFields :: Parser RecordField
+-- parseRecordFields = undefined
 
-recordTypeConstructor :: Parser RecordType
-recordTypeConstructor = undefined
+-- recordTypeConstructor :: Parser RecordType
+-- recordTypeConstructor = undefined
     -- do
   --  reserved kwRecordType
   --  typeName <- prefixSymbolSN
@@ -287,9 +288,6 @@ letBlock = undefined
 -- Function
 --------------------------------------------------------------------------------
 
-function :: Parser Function
-function = undefined 
-
 --------------------------------------------------------------------------------
 -- Lambda
 --------------------------------------------------------------------------------
@@ -337,11 +335,6 @@ expressionSN = undefined
 
 --------------------------------------------------------------------------------
 
--- Unwrap the header from the rest of the definitions
-extractTopLevel :: FileHeader topLevel -> [topLevel]
-extractTopLevel (FileHeader _ decls) = decls
-extractTopLevel (NoFileHeader decls) = decls
-
 --------------------------------------------------------------------------------
 -- Symbol Handlers
 --------------------------------------------------------------------------------