Merge branch 'jan' into qtt

.gitignore

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

examples/FirstMilestone.mjuvix

@@ -0,0 +1,184 @@
+module Example1;
+
+module M;
+-- This creates a module called M,
+-- which it must be closed with:
+end;
+
+open M;  -- comments can follow after ;
+
+-- import moduleName {names} hiding {names};
+import Primitives;       -- imports all the public names.
+import Backend {LLVM};   -- imports to local scope a var. called LLVM.
+import Prelude hiding {Nat, Vec, Empty, Unit};
+	-- same as before, but without the names inside `hiding`
+
+-- Judgement decl.
+-- `x : M;`
+
+-- Nonindexed inductive type declaration:
+inductive Nat ;
+{ zero : Nat ;
+	suc : Nat -> Nat ;
+};
+
+-- Term definition uses := instead of =.
+-- = is not a reserved name.
+-- == is not a reserved name.
+-- === is a reserved symbol for def. equality.
+zero' : Nat;
+zero' :=
+zero;
+
+-- Axioms/definitions.
+axiom A : Type;
+axiom a : A;
+
+f : Nat -> A;
+f := \x -> match x
+{
+	zero ↦ a  ;
+	suc  -> a' ;
+};
+
+g : Nat -> A;
+g Nat.zero    := a;
+g (Nat.suc t) := a';
+
+-- Qualified names for pattern-matching seems convenient.
+-- For example, if we define a function without a type sig.
+-- that also matches on inductive type with constructor names
+-- appearing in another type, e.g. Nat and Fin.
+
+inductive Fin (n : Nat) {
+	zero : Fin Nat.zero;
+	suc  : (n : Nat) -> Fin (Nat.suc n);
+};
+
+infixl 10 + ; -- fixity notation as in Agda or Haskell.
++ : Nat → Nat → Nat ;
++ Nat.zero m    := m;
++ (Nat.suc n) m := Nat.suc (n + m) ;
+
+-- Unicode is possible.
+ℕ : Type;
+ℕ := Nat;
+-- Maybe consider alises for types and data constructors:
+-- `alias ℕ := Nat` ;
+
+-- The function `g` should be transformed to
+-- a function of the form f. (aka. case-tree compilation)
+
+-- Examples we must have to make things interesting:
+-- Recall ; goes after any declarations.
+
+inductive Unit { tt : Unit;};
+
+-- Indexed inductive type declarations:
+inductive Vec (n : Nat) (A : Type)
+{
+	zero : Vec Nat.zero A;
+	succ : A -> Vec n A -> Vec (Nat.succ n) A;
+};
+
+Vec' : Nat -> Type -> Type;
+Vec' Nat.zero A      := Unit;
+Vec' (Vec'.suc n) A := A -> Vec' n A;
+
+inductive Empty{};
+
+exfalso : (A : Type) -> Empty -> A;
+exfalso A e := match e {};
+
+neg : Type -> Type;
+neg := A -> Empty;
+
+-- projecting fields values.
+h'' : Person -> String;
+h'' p := Person.name p;
+
+-- So far, we haven't used quantites, here is some examples.
+-- We mark a type judgment `x : M` of quantity n as `x :n M`.
+-- If the quantity n is not explicit, then the judgement
+-- is `x :Any M`.
+
+-- The following says that the term z of type A has quantity 0.
+axiom z :0 A;
+axiom B : (x :1 A) -> Type;   -- type family
+axiom em : (x :1 A) -> B;
+
+axiom C : Type;
+axiom D : Type;
+
+-- More inductive types.
+inductive Id (A : Type) (x : A)
+{
+	refl : Id A x;
+};
+
+-- Usages
+-- Minijuvix: 0,1,ω
+-- Juvix: i<ω, ω
+
+record Tensor (A : Type) (B : (x :1 A) → Type) {
+	proj1 : A;
+	proj2 :0 B proj1;
+}
+
+inductive Tensor' (A : Type) (B : (x :1 A) → Type) {
+	mkTensor : (proj1 : A) → (B proj1) → Tensor' A B;
+}
+
+proj1 : Tensor' A B → A
+proj1 (mkTensor p1 _) = p1
+
+proj1 : (t : Tensor' A B) → B (proj1 t)
+proj1 (mkTensor _ p2) = p2
+
+a-is-a : a = a;
+a-is-a := refl;
+
+-- Where
+
+a-is-a' : a = a;
+a-is-a' := helper
+  where {
+    open somemodule;
+    helper : a = a;
+    helper := a-is-a;
+    };
+
+a-is-a'' : a = a;
+a-is-a'' := helper
+where {
+helper : a = a;
+helper := a-is-a';
+}
+
+-- `Let` can appear in type level definition
+-- but also in term definitions.
+
+a-is-a-3 : a = a;
+a-is-a-3 := let { helper : a = a;
+                  helper := a-is-a;} in helper;
+
+a-is-a-4 : let {
+typeId : (M : Type) -> (x : M) -> Type;
+typeId M x := x = x;
+} in typeId A a;
+a-is-a-4 := a-is-a;
+
+end;
+
+-- future:
+-- module M' (X : Type);
+-- x-is-x : (x : X) -> x = x;
+-- x-is-x x := refl;
+-- end M';
+-- open M' A;
+-- a-is-a-5 := a = a;
+-- a-is-a-5 = x-is-x a;
+-- Also, for debugging:
+
+-- print e; print out the internal representation for e, without normalising it.
+-- eval e;  compute e and print it out;

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

hie.yaml

@@ -1,10 +1,16 @@
 cradle:
-  cabal:
-    - path: "src"
-      component: "lib:MiniJuvix"
+  stack:
+    - path: "./src"
+      component: "MiniJuvix:lib"
 
-    - path: "src/app/Main.hs"
+    - path: "./src/app/Main.hs"
       component: "MiniJuvix:exe:MiniJuvix"
 
-    - path: "src/test"
-      component: "MiniJuvix:test:MiniJuvix-test"
+    - path: "./src/app/Options.hs"
+      component: "MiniJuvix:exe:MiniJuvix"
+
+    - path: "./src/app/Paths_MiniJuvix.hs"
+      component: "MiniJuvix:exe:MiniJuvix"
+
+    - path: "./src/test"
+      component: "MiniJuvix:test:curry-test"

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,109 +1,90 @@
-{-# 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
   | ModuleDeclaration Module
   | OpenModuleDeclaration OpenModule
-  | FunctionDeclaration Function
+  | FunctionClause FunctionClause
   deriving stock (Show, Read, Eq)
 
 --------------------------------------------------------------------------------
--- Fixity declaration
+-- Operator syntax declaration
 --------------------------------------------------------------------------------
 
 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)
 
-------------------------------------------------------------------------------
--- Type signature declaration
---------------------------------------------------------------------------------
-
-data TypeSignature
-  = TypeSignature
-      { termName :: Name,
-        termQuantity :: Maybe Expression,
-        termContext :: [Expression],
-        termType :: Expression
+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
+      {
+        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]
-      }
-  deriving stock (Show, Read, Eq)
-
-------------------------------------------------------------------------------
--- Record type declaration
-------------------------------------------------------------------------------
-
-type RecordFieldName = Name
-
-type RecordTypeName = Name
-
-data RecordField = RecordField RecordFieldName RecordTypeName Expression
-  deriving stock (Show, Read, Eq)
-
-data RecordType
-  = RecordType
-      { recordTypeName :: Name,
-        recordTypeConstructorName :: Name,
-        recordTypeParameters :: [Expression],
-        recordFields :: [RecordField]
+        dataTypeArgs :: [Expression],
+        dataTypeConstructors :: [DataConstructorDef]
       }
   deriving stock (Show, Read, Eq)
 
@@ -111,30 +92,18 @@ data RecordType
 -- Function binding declaration
 --------------------------------------------------------------------------------
 
-type PreTypeName = Name
-
-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]
+  | 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 +114,7 @@ data Function
 data Module
   = Module
       { moduleName :: Name,
-        moduleParameters :: [Expression],
+        moduleArgs :: [Expression],
         body :: [TopLevel]
       }
   deriving stock (Show, Read, Eq)
@@ -159,28 +128,11 @@ newtype OpenModule
 --------------------------------------------------------------------------------
 
 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?
+  = ExprIdentifier Name
+  | ExprApplication Application
+  | ExprLambda Lambda
+  | ExprLetBlock LetBlock
+  | ExprUniverse Universe
   deriving stock (Show, Read, Eq)
 
 --------------------------------------------------------------------------------
@@ -191,10 +143,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 +177,8 @@ data Lambda
 
 data Application
   = Application
-      { applicationName :: Expression,
-        applicationArgs :: NonEmpty Expression
+      { applicationFun :: Expression,
+        applicationArg :: Expression
       }
   deriving stock (Show, Read, Eq)
 
@@ -226,17 +186,10 @@ data Application
 -- Let block expression
 --------------------------------------------------------------------------------
 
-newtype LetBlock = LetBlock Expression
+newtype LetBlock = LetBlock [LetClause]
   deriving stock (Show, Read, Eq)
 
---------------------------------------------------------------------------------
--- Infix expression
---------------------------------------------------------------------------------
-
-data Infix
-  = Infix
-      { leftPart :: Expression,
-        infixOp :: Name,
-        rightPart :: Expression
-      }
+data LetClause =
+  LetTypeSig TypeSignature
+  | LetDefinition FunctionClause
   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
 --------------------------------------------------------------------------------