Change syntax for ind. data types and forbid the empty data type (#1684)

Closes #1644 #1635

docs/org/examples/validity-predicates/PolyFungibleToken.org

@@ -12,10 +12,9 @@ foreign ghc {
 -- Booleans
 --------------------------------------------------------------------------------
 
-inductive Bool {
-  true : Bool;
-  false : Bool;
-};
+type Bool :=
+     true : Bool
+  | false : Bool;
 
 infixr 2 ||;
 || : Bool → Bool → Bool;
@@ -139,10 +138,9 @@ infix 4 ==String;
 --------------------------------------------------------------------------------
 
 infixr 5 ∷;
-inductive List (A : Type) {
-  nil : List A;
-  ∷ : A → List A → List A;
-};
+type List (A : Type) :=
+  nil : List A
+  | ∷ : A → List A → List A;
 
 elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
 elem _ _ nil := false;
@@ -158,18 +156,16 @@ foldl f z (h ∷ hs) := foldl f (f z h) hs;
 
 infixr 4 ,;
 infixr 2 ×;
-inductive × (A : Type) (B : Type) {
+type × (A : Type) (B : Type) :=
   , : A → B → A × B;
-};
 
 --------------------------------------------------------------------------------
 -- Maybe
 --------------------------------------------------------------------------------
 
-inductive Maybe (A : Type) {
- nothing : Maybe A;
+type Maybe (A : Type) :=
+ nothing : Maybe A |
  just : A → Maybe A;
-};
 
 from-int : Int → Maybe Int;
 from-int i := if (i < 0) nothing (just i);

docs/org/language-reference/builtins.org

@@ -7,10 +7,9 @@ Juvix has support for the built-in natural type and a few functions that are com
 
    #+begin_example
    builtin nat
-   inductive Nat {
-     zero : Nat;
+   type Nat :=
+     zero : Nat |
      suc : Nat → Nat;
-   };
    #+end_example
 
 2. Builtin function definitions.

docs/org/language-reference/foreign-blocks.org

@@ -19,10 +19,9 @@ foreign c {
    \}
 };
 
-inductive Bool {
-    true : Bool;
+type Bool :=
+    true : Bool |
     false : Bool;
-};
 
 infix 4 <';
 axiom <' : Int -> Int -> Bool;

docs/org/language-reference/inductive-data-types.org

@@ -1,15 +1,16 @@
 * Inductive data types
 
 The =inductive= keyword is reserved for declaring inductive data types. An
-inductive type declaration requires a unique name for its type and its
-constructors, functions for building its terms. Constructors can be used as
-normal identifiers and also in patterns. As shown later, one can also provide
-type parameters to widen the family of inductive types one can define in Juvix.
+inductive type declaration requires a unique name for its type and a non-empty
+list of constructor declarations, functions for building the terms of the
+inductive data type. Constructors can be used as normal identifiers and also in
+patterns. As shown later, one can also provide type parameters to widen the
+family of inductive types one can define in Juvix.
 
-The simplest inductive type is the =Empty= type with no constructors.
+The simplest inductive type is the =Unit= type with one constructor called =unit=.
 
 #+begin_example
-inductive Empty {};
+type Unit := unit : Unit;
 #+end_example
 
 In the following example, we declare the inductive type =Nat=, the unary
@@ -18,10 +19,9 @@ namely =zero= and =suc=. A term of the type =Nat= is the number one, represented
 by =suc zero= or the number two represented by =suc (suc zero)=, etc.
 
 #+begin_example
-inductive Nat {
-    zero : Nat;
-    suc : Nat -> Nat;
-};
+type Nat :=
+    zero : Nat
+  | suc : Nat -> Nat;
 #+end_example
 
 The way to use inductive types is by declaring functions by pattern matching.
@@ -43,10 +43,9 @@ the following type taken from the Juvix standard library:
 
 #+begin_example
 infixr 5 ∷;
-inductive List (A : Type) {
-  nil : List A;
-  ∷ : A -> List A -> List A;
-};
+type List (A : Type) :=
+    nil : List A
+  | ∷ : A -> List A -> List A;
 
 elem : {A : Type} -> (A -> A -> Bool) -> A -> List A -> Bool;
 elem _ _ nil := false;

docs/org/notes/builtins.org

@@ -10,10 +10,9 @@ of definitions:
 1. Builtin inductive definitions. For example:
    #+begin_example
    builtin nat
-   inductive Nat {
-     zero : Nat;
+   type Nat :=
+     zero : Nat |
      suc : Nat → Nat;
-   };
    #+end_example
    We will call this the canonical definition of natural numbers.
 
@@ -41,10 +40,9 @@ what are the terms that refer to them. For instance, imagine that we find this
 definitions in a juvix module:
 #+begin_src text
 builtin nat
-inductive MyNat {
-    z : MyNat;
+type MyNat :=
+    z : MyNat |
     s : MyNat → MyNat;
-};
 #+end_src
 We need to take care of the following:
 1. Check that the definition =MyInt= is up to renaming equal to the canonical

docs/org/notes/monomorphization.org

@@ -31,10 +31,9 @@
 * More examples
 ** Mutual recursion
 #+begin_src juvix
-inductive List (A : Type) {
-  nil : List A;
+type List (A : Type) :=
+  nil : List A |
   cons : A → List A → List A;
-};
 
 even : (A : Type) → List A → Bool;
 even A nil := true ;

docs/org/notes/strictly-positive-data-types.org

@@ -2,27 +2,28 @@
 
 We follow a syntactic description of strictly positive inductive data types.
 
-An inductive type is said to be _strictly positive_ if it does not occur or occurs
-strictly positively in the types of the arguments of its constructors. A name
-qualified as strictly positive for an inductive type if it never occurs at a negative
-position in the types of the arguments of its constructors. We refer to a negative
-position as those occurrences on the left of an arrow in a type constructor argument.
+An inductive type is said to be _strictly positive_ if it does not occur or
+occurs strictly positively in the types of the arguments of its constructors. A
+name qualified as strictly positive for an inductive type if it never occurs at
+a negative position in the types of the arguments of its constructors. We refer
+to a negative position as those occurrences on the left of an arrow in a type
+constructor argument.
 
-In the example below, the type =X= occurs strictly positive in =c0= and negatively at
-the constructor =c1=. Therefore, =X= is not strictly positive.
+In the example below, the type =X= occurs strictly positive in =c0= and
+negatively at the constructor =c1=. Therefore, =X= is not strictly positive.
 
 #+begin_src minijuvix
 axiom B : Type;
-inductive X {
-  c0 : (B -> X) -> X;
-  c1 : (X -> X) -> X;
-};
+type X :=
+    c0 : (B -> X) -> X
+  | c1 : (X -> X) -> X;
 #+end_src
 
-We could also refer to positive parameters as such parameters occurring in no negative positions.
-For example, the type =B= in the =c0= constructor above is on the left of the arrow =B->X=.
-Then, =B= is at a negative position. Negative parameters need to be considered when checking strictly
-positive data types as they may allow to define non-strictly positive data types.
+We could also refer to positive parameters as such parameters occurring in no
+negative positions. For example, the type =B= in the =c0= constructor above is
+on the left of the arrow =B->X=. Then, =B= is at a negative position. Negative
+parameters need to be considered when checking strictly positive data types as
+they may allow to define non-strictly positive data types.
 
 In the example below, the type =T0= is strictly positive. However, the type =T1= is not.
 Only after unfolding the type application =T0 (T1 A)= in the data constructor =c1=, we can
@@ -30,13 +31,9 @@ find out that =T1= occurs at a negative position because of =T0=. More precisely
 the type parameter =A= of =T0= is negative.
 
 #+begin_src minijuvix
-inductive T0 (A : Type) {
-  c0 : (A -> T0 A) -> T0 A;
-};
+type T0 (A : Type) := c0 : (A -> T0 A) -> T0 A;
 
-inductive T1 {
-  c1 : T0 T1 -> T1;
-};
+type T1 := c1 : T0 T1 -> T1;
 #+end_src
 
 
@@ -50,37 +47,25 @@ when typechecking a =Juvix= File.
 $ cat tests/negative/MicroJuvix/NoStrictlyPositiveDataTypes/E5.mjuvix
 module E5;
   positive
-  inductive T0 (A : Type){
+  type T0 (A : Type) :=
     c0 : (T0 A -> A) -> T0 A;
-  };
 end;
 #+end_example
 
 ** Examples of non-strictly data types
 
-- =NSPos= is at a negative position in =c=.
-  #+begin_src minijuvix
-  inductive Empty {};
-  inductive NSPos {
-    c : ((NSPos -> Empty) -> NSPos) -> NSPos;
-  };
-  #+end_src
-
 - =Bad= is not strictly positive beceause of the negative parameter =A= of =Tree=.
   #+begin_src minijuvix
-  inductive Tree (A : Type) {
-    leaf : Tree A;
-    node : (A -> Tree A) -> Tree A;
-  };
+  type Tree (A : Type) :=
+      leaf : Tree A
+    | node : (A -> Tree A) -> Tree A;
 
-  inductive Bad {
+  type Bad :=
     bad : Tree Bad -> Bad;
-  };
   #+end_src
 
 - =A= is a negative parameter.
   #+begin_src minijuvix
-  inductive B (A : Type) {
+  type B (A : Type) :=
     b : (A -> B (B A -> A)) -> B A;
-  };
   #+end_src

examples/milestone/Hanoi/Hanoi.juvix

@@ -43,11 +43,10 @@ showList : List Nat → String;
 showList xs := "[" ++str intercalate "," (map natToStr xs) ++str "]";
 
 --- A Peg represents a peg in the towers of Hanoi game
-inductive Peg {
-  left : Peg;
-  middle : Peg;
-  right : Peg;
-};
+type Peg :=
+    left : Peg
+  | middle : Peg
+  | right : Peg;
 
 showPeg : Peg → String;
 showPeg left := "left";
@@ -56,9 +55,7 @@ showPeg right := "right";
 
 
 --- A Move represents a move between pegs
-inductive Move {
-  move : Peg → Peg → Move;
-};
+type Move := move : Peg → Peg → Move;
 
 showMove : Move → String;
 showMove (move from to) := showPeg from ++str " -> " ++str showPeg to;

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -6,9 +6,8 @@ open import Logic.Symbol public;
 open import Logic.Extra;
 
 --- A 3x3 grid of ;Square;s
-inductive Board {
+type Board :=
   board : List (List Square) → Board;
-};
 
 --- Returns the list of numbers corresponding to the empty ;Square;s
 possibleMoves : List Square → List Nat;

examples/milestone/TicTacToe/Logic/GameState.juvix

@@ -4,18 +4,16 @@ open import Stdlib.Prelude;
 open import Logic.Extra;
 open import Logic.Board;
 
-inductive Error {
+type Error :=
 --- no error occurred
-  noError : Error;
+  noError : Error |
 --- a non-fatal error occurred
-  continue : String → Error;
+continue : String → Error |
 --- a fatal occurred
-  terminate : String → Error;
-};
+terminate : String → Error;
 
-inductive GameState {
+type GameState :=
   state : Board → Symbol → Error → GameState;
-};
 
 --- Textual representation of a ;GameState;
 showGameState : GameState → String;

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -6,12 +6,12 @@ open import Stdlib.Data.Nat.Ord;
 open import Logic.Extra;
 
 --- A square is each of the holes in a board
-inductive Square {
+type Square :=
   --- An empty square has a ;Nat; that uniquely identifies it
-  empty : Nat → Square;
-  --- An occupied square has a ;Symbol; in it
-  occupied : Symbol → Square;
-};
+  empty : Nat → Square
+  -- TODO: Check the line below using Judoc
+  -- - An occupied square has a ;Symbol; in it
+  | occupied : Symbol → Square;
 
 --- Equality for ;Square;s
 ==Square : Square → Square → Bool;

examples/milestone/TicTacToe/Logic/Symbol.juvix

@@ -4,12 +4,11 @@ module Logic.Symbol;
 open import Stdlib.Prelude;
 
 --- A symbol represents a token that can be placed in a square
-inductive Symbol {
+type Symbol :=
 --- The circle token
-  O : Symbol;
+  O : Symbol |
 --- The cross token
   X : Symbol;
-};
 
 --- Equality for ;Symbol;s
 ==Symbol : Symbol → Symbol → Bool;

examples/milestone/TicTacToe/Web/TicTacToe.juvix

@@ -93,11 +93,10 @@ lightBackgroundColor := "#c7737a";
 
 -- Rendering
 
-inductive Align {
-  left : Align;
-  right : Align;
-  center : Align;
-};
+type Align :=
+    left : Align
+  | right : Align
+  | center : Align;
 
 alignNum : Align → Nat;
 alignNum left := zero;

juvix-stdlib

@@ -1 +1 @@
-Subproject commit a2790ca49ceeb569559224abe1587305ea1861fa
+Subproject commit bdcf1ef0889a08de1ec334a598efbbf622607884

src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs

@@ -279,7 +279,7 @@ goInductive ty@InductiveDef {..} = do
             _inductiveBuiltin = _inductiveBuiltin,
             _inductiveName = goSymbol _inductiveName,
             _inductiveType = fromMaybe (Abstract.ExpressionUniverse (smallUniverse loc)) _inductiveType',
-            _inductiveConstructors = _inductiveConstructors',
+            _inductiveConstructors = toList _inductiveConstructors',
             _inductiveExamples = _inductiveExamples',
             _inductivePositive = ty ^. inductivePositive
           }

src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs

@@ -411,9 +411,9 @@ goInductive def = do
     inductiveHeader =
       runReader defaultOptions (ppInductiveSignature def) >>= ppCodeHtml
 
-goConstructors :: forall r. Members '[Reader HtmlOptions, Reader NormalizedTable] r => [InductiveConstructorDef 'Scoped] -> Sem r Html
+goConstructors :: forall r. Members '[Reader HtmlOptions, Reader NormalizedTable] r => NonEmpty (InductiveConstructorDef 'Scoped) -> Sem r Html
 goConstructors cc = do
-  tbl' <- table . tbody <$> mconcatMapM goConstructor cc
+  tbl' <- table . tbody <$> mconcatMapM goConstructor (toList cc)
   return $
     Html.div ! Attr.class_ "subs constructors" $
       (p ! Attr.class_ "caption" $ "Constructors")

src/Juvix/Compiler/Concrete/Keywords.hs

@@ -36,6 +36,7 @@ import Juvix.Data.Keyword.All
     kwMapsTo,
     kwModule,
     kwOpen,
+    kwPipe,
     kwPositive,
     kwPostfix,
     kwPublic,
@@ -76,6 +77,7 @@ allKeywords =
     kwLet,
     kwModule,
     kwOpen,
+    kwPipe,
     kwPostfix,
     kwPublic,
     kwRightArrow,

src/Juvix/Compiler/Concrete/Language.hs

@@ -249,7 +249,7 @@ data InductiveDef (s :: Stage) = InductiveDef
     _inductiveName :: InductiveName s,
     _inductiveParameters :: [InductiveParameter s],
     _inductiveType :: Maybe (ExpressionType s),
-    _inductiveConstructors :: [InductiveConstructorDef s],
+    _inductiveConstructors :: NonEmpty (InductiveConstructorDef s),
     _inductivePositive :: Bool
   }
 

src/Juvix/Compiler/Concrete/Pretty/Base.hs

@@ -108,13 +108,16 @@ groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
         symbolParsed sym = case sing :: SStage s of
           SParsed -> sym
           SScoped -> sym ^. S.nameConcrete
+
         syms :: InductiveDef s -> [Symbol]
-        syms InductiveDef {..} = case sing :: SStage s of
-          SParsed -> _inductiveName : map (^. constructorName) _inductiveConstructors
-          SScoped ->
-            _inductiveName
-              ^. S.nameConcrete
-              : map (^. constructorName . S.nameConcrete) _inductiveConstructors
+        syms InductiveDef {..} =
+          let constructors = toList _inductiveConstructors
+           in case sing :: SStage s of
+                SParsed -> _inductiveName : map (^. constructorName) constructors
+                SScoped ->
+                  _inductiveName
+                    ^. S.nameConcrete
+                    : map (^. constructorName . S.nameConcrete) constructors
 
 instance SingI s => PrettyCode [Statement s] where
   ppCode ss = vsep2 <$> mapM (fmap vsep . mapM (fmap endSemicolon . ppCode)) (groupStatements ss)
@@ -288,8 +291,19 @@ instance SingI s => PrettyCode (InductiveDef s) where
   ppCode d@InductiveDef {..} = do
     doc' <- mapM ppCode _inductiveDoc
     sig' <- ppInductiveSignature d
-    inductiveConstructors' <- ppBlock _inductiveConstructors
-    return $ doc' ?<> sig' <+> inductiveConstructors'
+    inductiveConstructors' <- ppConstructorBlock _inductiveConstructors
+    return $
+      doc' ?<> sig'
+        <+> kwAssign
+          <> line
+          <> (indent' . align) inductiveConstructors'
+    where
+      ppConstructorBlock ::
+        NonEmpty (InductiveConstructorDef s) -> Sem r (Doc Ann)
+      ppConstructorBlock cs =
+        do
+          concatWith (\x y -> x <> softline <> kwPipe <+> y)
+          <$> mapM ppCode (toList cs)
 
 dotted :: Foldable f => f (Doc Ann) -> Doc Ann
 dotted = concatWith (surround kwDot)

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -496,10 +496,16 @@ inductiveDef _inductiveBuiltin = do
   _inductivePositive <- isJust <$> optional (kw kwPositive)
   kw kwInductive
   _inductiveDoc <- getJudoc
-  _inductiveName <- symbol
-  _inductiveParameters <- P.many inductiveParam
-  _inductiveType <- optional (kw kwColon >> parseExpressionAtoms)
-  _inductiveConstructors <- braces $ P.sepEndBy constructorDef (kw kwSemicolon)
+  _inductiveName <- symbol P.<?> "<type name>"
+  _inductiveParameters <-
+    P.many inductiveParam
+      P.<?> "<type parameter e.g. '(A : Type)'>"
+  _inductiveType <-
+    optional (kw kwColon >> parseExpressionAtoms)
+      P.<?> "<type annotation e.g. ': Type'>"
+  kw kwAssign P.<?> "<assignment symbol ':='>"
+  _inductiveConstructors <-
+    P.sepBy1 constructorDef (kw kwPipe) P.<?> "<constructor definition>"
   return InductiveDef {..}
 
 inductiveParam :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (InductiveParameter 'Parsed)
@@ -512,9 +518,10 @@ inductiveParam = parens $ do
 constructorDef :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (InductiveConstructorDef 'Parsed)
 constructorDef = do
   _constructorDoc <- optional stashJudoc >> getJudoc
-  _constructorName <- symbol
-  kw kwColon
-  _constructorType <- parseExpressionAtoms
+  _constructorName <- symbol P.<?> "<constructor name>"
+  _constructorType <-
+    kw kwColon >> parseExpressionAtoms
+      P.<?> "<constructor type signature (:)>"
   return InductiveConstructorDef {..}
 
 wildcard :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r Wildcard

src/Juvix/Data/Keyword/All.hs

@@ -94,6 +94,9 @@ kwRightArrow = unicodeKw Str.toAscii Str.toUnicode
 kwSemicolon :: Keyword
 kwSemicolon = asciiKw Str.semicolon
 
+kwPipe :: Keyword
+kwPipe = asciiKw Str.pipe
+
 kwType :: Keyword
 kwType = asciiKw Str.type_
 

src/Juvix/Extra/Strings.hs

@@ -33,7 +33,7 @@ in_ :: IsString s => s
 in_ = "in"
 
 inductive :: IsString s => s
-inductive = "inductive"
+inductive = "type"
 
 function :: IsString s => s
 function = "function"

test/Termination/Negative.hs

@@ -65,12 +65,6 @@ tests =
       $(mkRelFile "TerminatingG.juvix")
       $ \case
         ErrNoLexOrder {} -> Nothing,
-    NegTest
-      "f x := f x is not terminating"
-      $(mkRelDir ".")
-      $(mkRelFile "ToEmpty.juvix")
-      $ \case
-        ErrNoLexOrder {} -> Nothing,
     NegTest
       "Tree"
       $(mkRelDir ".")

test/Termination/Positive.hs

@@ -71,10 +71,6 @@ tests =
 testsWithKeyword :: [PosTest]
 testsWithKeyword =
   [ PosTest
-      "terminating added to fx:=fx"
-      $(mkRelDir ".")
-      $(mkRelFile "ToEmpty.juvix"),
-    PosTest
       "terminating for all functions in the mutual block"
       $(mkRelDir ".")
       $(mkRelFile "Mutual.juvix"),

tests/Asm/negative/test002.jva

@@ -1,6 +1,6 @@
 -- invalid memory access
 
-inductive list {
+type list {
   nil : list;
   cons : * -> list -> list;
 }

tests/Asm/negative/test003.jva

@@ -1,6 +1,6 @@
 -- no matching case branch
 
-inductive list {
+type list {
   nil : list;
   cons : * -> list -> list;
 }

tests/Asm/negative/vtest008.jva

@@ -1,6 +1,6 @@
 -- case stack height mismatch
 
-inductive list {
+type list {
   nil : list;
   cons : * -> list -> list;
 }

tests/Asm/negative/vtest009.jva

@@ -1,6 +1,6 @@
 -- case type mismatch
 
-inductive list {
+type list {
   nil : list;
   cons : * -> list -> list;
 }

tests/Asm/positive/test009.jva

@@ -1,6 +1,6 @@
 -- case
 
-inductive list {
+type list {
   nil : list;
   cons : * -> list -> list;
 }

tests/Asm/positive/test014.jva

@@ -1,6 +1,6 @@
 -- trees
 
-inductive tree {
+type tree {
   node1 : tree -> tree;
   node2 : tree -> tree -> tree;
   node3 : tree -> tree -> tree -> tree;

tests/Asm/positive/test028.jva

@@ -1,6 +1,6 @@
 -- lists
 
-inductive list {
+type list {
   nil : list;
   cons : * -> list -> list;
 }

tests/Asm/positive/test029.jva

@@ -1,6 +1,6 @@
 -- structural equality
 
-inductive list {
+type list {
   nil : list;
   cons : * -> list -> list;
 }

tests/Asm/positive/test031.jva

@@ -1,6 +1,6 @@
 -- temporary stack with branching
 
-inductive tree {
+type tree {
   leaf : tree;
   node : tree -> tree -> tree;
 }

tests/Asm/positive/test032.jva

@@ -1,6 +1,6 @@
 -- Church numerals
 
-inductive Pair {
+type Pair {
   pair : * -> * -> Pair;
 }
 

tests/Asm/positive/test035.jva

@@ -1,6 +1,6 @@
 -- Nested lists
 
-inductive list {
+type list {
   nil : list;
   cons : * -> list -> list;
 }

tests/Asm/positive/test036.jva

@@ -1,6 +1,6 @@
 -- streams without memoization
 
-inductive stream {
+type stream {
   cons : integer -> (unit -> stream) -> stream;
 }
 

tests/Core/positive/test007.jvc

@@ -1,6 +1,6 @@
 -- case
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };

tests/Core/positive/test012.jvc

@@ -1,6 +1,6 @@
 -- trees
 
-inductive tree : Type {
+type tree : Type {
   node1 : tree -> tree;
   node2 : tree -> tree -> tree;
   node3 : tree -> tree -> tree -> tree;

tests/Core/positive/test023.jvc

@@ -1,6 +1,6 @@
 -- lists
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };

tests/Core/positive/test024.jvc

@@ -1,6 +1,6 @@
 -- structural equality
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };

tests/Core/positive/test026.jvc

@@ -1,6 +1,6 @@
 -- nested case, let & if
 
-inductive tree {
+type tree {
   leaf : tree;
   node : tree -> tree -> tree;
 };

tests/Core/positive/test028.jvc

@@ -1,6 +1,6 @@
 -- functional queues
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };
@@ -15,7 +15,7 @@ def rev' := \l \acc case l of {
 
 def rev := \l rev' l nil;
 
-inductive Queue {
+type Queue {
   queue : list -> list -> Queue;
 };
 

tests/Core/positive/test029.jvc

@@ -1,6 +1,6 @@
 -- Church numerals
 
-inductive Pair {
+type Pair {
   pair : any -> any -> Pair;
 };
 

tests/Core/positive/test030.jvc

@@ -1,10 +1,10 @@
 -- streams without memoization
 
-inductive Unit {
+type Unit {
   unit : Unit;
 };
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };

tests/Core/positive/test033.jvc

@@ -1,6 +1,6 @@
 -- nested lists
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };

tests/Core/positive/test035.jvc

@@ -1,11 +1,11 @@
 -- merge sort
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };
 
-inductive product {
+type product {
   pair : any -> any -> product;
 };
 

tests/Core/positive/test037.jvc

@@ -1,6 +1,6 @@
 -- global variables
 
-inductive Unit {
+type Unit {
   unit : Unit;
 };
 

tests/Core/positive/test039.jvc

@@ -1,6 +1,6 @@
 -- eta-expansion of builtins and constructors
 
-inductive stream {
+type stream {
   cons : any -> any -> stream;
 };
 

tests/Core/positive/test041.jvc

@@ -1,6 +1,6 @@
 -- match
 
-inductive list {
+type list {
   cons : any -> list -> list;
   nil : list;
 };
@@ -14,7 +14,7 @@ def sum2 := \x {
   }
 };
 
-inductive tree {
+type tree {
   leaf : tree;
   node : tree -> tree -> tree;
 };

tests/Core/positive/test042.jvc

@@ -1,6 +1,6 @@
 -- type annotations
 
-inductive list : Π A : Type, Type {
+type list : Π A : Type, Type {
   cons : Π A : Type, A → list A → list A;
   nil : Π A : Type, list A;
 };

tests/Core/positive/test045.jvc

@@ -1,6 +1,6 @@
 -- type application and abstraction
 
-inductive list : Π A : Type, Type {
+type list : Π A : Type, Type {
   cons : Π A : Type, A → list A → list A;
   nil : Π A : Type, list A;
 };

tests/Core/positive/test046.jvc

@@ -1,6 +1,6 @@
 -- applications with lets and cases in function position
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };

tests/Internal/positive/FunctionReturnConstructor.juvix

@@ -1,8 +1,7 @@
 module FunctionReturnConstructor;
 
-inductive Foo {
+type Foo :=
   foo : Foo;
-};
 
 main : Foo;
 main := foo;

tests/Internal/positive/FunctionType.juvix

@@ -1,8 +1,7 @@
 module FunctionType;
 
-inductive A {
+type A :=
   a : A;
-};
 
 main : Type;
 main := (A : Type) -> (B : Type) -> A -> B;

tests/Internal/positive/Inductive.juvix

@@ -1,8 +1,7 @@
 module Inductive;
 
-inductive A (B : Type) {
+type A (B : Type) :=
   a : A B;
-};
 
 main : Type -> Type;
 main := A;

tests/Internal/positive/MatchConstructor.juvix

@@ -2,10 +2,9 @@ module MatchConstructor;
 
 open import Stdlib.Prelude;
 
-inductive Foo {
-  foo1 : Nat → Foo;
+type Foo :=
+  foo1 : Nat → Foo |
   foo2 : Foo;
-};
 
 toNat : Foo → Nat;
 toNat (foo1 n) := n;

tests/benchmark/fold/core/fold.jvc

@@ -1,6 +1,6 @@
 -- fold a list of N integers
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };

tests/benchmark/mapfold/core/mapfold.jvc

@@ -1,6 +1,6 @@
 -- map and fold a list of N integers K times
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };

tests/benchmark/mapfun/core/mapfun.jvc

@@ -1,6 +1,6 @@
 -- successively map K functions to a list of N integers
 
-inductive list {
+type list {
   nil : list;
   cons : * -> list -> list;
 };

tests/benchmark/maybe/core/maybe.jvc

@@ -1,11 +1,11 @@
 -- optionally sum N integers from a binary tree K times
 
-inductive tree {
+type tree {
   node : int -> tree -> tree -> tree;
   leaf : tree;
 };
 
-inductive maybe {
+type maybe {
   just : any -> maybe;
   nothing : maybe;
 };

tests/benchmark/maybe/juvix/maybe.juvix

@@ -6,10 +6,9 @@ open import Stdlib.Prelude;
 open import Data.Int;
 open import Data.Int.Ops;
 
-inductive Tree {
-  leaf : Tree;
+type Tree :=
+  leaf : Tree |
   node : Int -> Tree -> Tree -> Tree;
-};
 
 mknode : Int -> Tree -> Tree;
 mknode n t := node n t t;

tests/benchmark/mergesort/core/mergesort.jvc

@@ -1,11 +1,11 @@
 -- merge sort
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };
 
-inductive product {
+type product {
   pair : any -> any -> product;
 };
 

tests/benchmark/prime/core/prime.jvc

@@ -1,6 +1,6 @@
 -- Compute the Nth prime
 
-inductive list {
+type list {
   nil : list;
   cons : any -> list -> list;
 };

tests/negative/230/Foo/Data/Bool.juvix

@@ -2,10 +2,9 @@ module Foo.Data.Bool;
 
 import Stdlib.Data.Bool;
 
-  inductive Bool {
-    true : Bool;
+  type Bool :=
+    true : Bool |
     false : Bool;
-  };
 
   not : Bool → Bool;
   not true := false;

tests/negative/258/M.juvix

@@ -1,9 +1,8 @@
 module M;
 
-inductive Nat {
-  O : Nat;
+type Nat :=
+  O : Nat |
   S : Nat -> Nat;
-};
 
 fun : Nat -> Nat;
 fun (S {S {x}}) := x;

tests/negative/265/M.juvix

@@ -1,13 +1,11 @@
 module M;
 
-inductive Bool {
-  false : Bool;
-  true : Bool;
-};
+type Bool :=
+     true : Bool
+  | false : Bool;
 
-inductive Pair (A : Type) (B : Type) {
+type Pair (A : Type) (B : Type) :=
   mkPair : A → B → Pair A B;
-};
 
 f : _ → _;
 f (mkPair false true) := true;

tests/negative/AmbiguousConstructor.juvix

@@ -1,14 +1,12 @@
 module AmbiguousConstructor;
   module M;
-    inductive T1 {
+    type T1 :=
       A : T1;
-    };
   end;
 
   module N;
-    inductive T2 {
+    type T2 :=
       A : T2;
-    };
   end;
 
   open M;

tests/negative/AmbiguousExport.juvix

@@ -2,9 +2,8 @@ module AmbiguousExport;
 
   module N;
     module O;
-      inductive T {
+      type T :=
         A : T;
-      };
     end;
   end;
 

tests/negative/AmbiguousSymbol.juvix

@@ -3,9 +3,7 @@ module AmbiguousSymbol;
   axiom A : Type;
 
   module O;
-    inductive T {
-      A : T;
-    };
+    type T := A : T;
   end;
   open O;
 

tests/negative/BindGroupConflict/Clause.juvix

@@ -1,8 +1,7 @@
 module Clause;
 
-  inductive Pair (a : Type) (b : Type) {
-   mkPair : a → b → Pair a b
-  };
+  type Pair (a : Type) (b : Type) :=
+   mkPair : a → b → Pair a b;
 
   fst : (a : Type) → (b : Type) → Pair a b → a ;
   fst _ _ (mkPair _ _ x x) := x;

tests/negative/BindGroupConflict/Lambda.juvix

@@ -1,8 +1,6 @@
 module Lambda;
 
-  inductive Pair (a : Type) (b : Type) {
-   mkPair : a → b → Pair a b
-  };
+  type Pair (a : Type) (b : Type) := mkPair : a → b → Pair a b;
 
   fst : (a : Type) → (b : Type) → Pair a b → a ;
   fst := λ { _ _ (mkPair _ _ x x) := x };

tests/negative/CompileBlocks/Sample/Definitions.juvix

@@ -2,10 +2,9 @@ module Sample.Definitions;
 
 axiom A : Type;
 
-inductive Nat {
-zero : Nat;
+type Nat :=
+zero : Nat |
 suc : Nat -> Nat;
-};
 
 f : A -> Nat;
 f a := zero;

tests/negative/DuplicateInductiveParameterName.juvix

@@ -1,5 +1,5 @@
 module DuplicateInductiveParameterName;
 
-inductive T (A : Type) (B : Type) (A : Type) {};
+type T (A : Type) (B : Type) (A : Type) := c : T A B A;
 
 end;

tests/negative/InfixErrorP.juvix

@@ -2,9 +2,8 @@ module InfixErrorP;
 
   infix 5 , ;
 
-  inductive Pair {
-   , : Type → Type → Pair
-  };
+  type Pair :=
+   , : Type → Type → Pair;
 
   fst : Pair → Type;
   fst (x , ) := x;

tests/negative/Internal/ExpectedExplicitArgument.juvix

@@ -1,7 +1,6 @@
 module ExpectedExplicitArgument;
-  inductive T (A : Type) {
+  type T (A : Type) :=
     c : A → T A;
-  };
 
   f : {A : Type} → A →  T A;
   f {A} a := c {A} {a};

tests/negative/Internal/ExpectedExplicitPattern.juvix

@@ -1,7 +1,6 @@
 module ExpectedExplicitPattern;
-  inductive T (A : Type) {
+  type T (A : Type) :=
     c : A → T A;
-  };
 
   f : {A : Type} → T A → A;
   f {_} {c a} := a;

tests/negative/Internal/ExpectedFunctionType.juvix

@@ -1,11 +1,9 @@
 module ExpectedFunctionType;
-  inductive Pair (A : Type) {
+  type Pair (A : Type) :=
     mkPair : A → A → Pair A;
-  };
 
-  inductive B {
+  type B :=
     b : B;
-  };
 
   f : Pair B → Pair B;
   f (mkPair a b) := a b;

tests/negative/Internal/FunctionApplied.juvix

@@ -1,7 +1,6 @@
 module FunctionApplied;
-  inductive T (A : Type) {
+  type T (A : Type) :=
     c : A → T A;
-  };
 
   f : {A : Type} → A → T A;
   f {A} a := c {(A → A) A} a;

tests/negative/Internal/FunctionPattern.juvix

@@ -1,7 +1,6 @@
 module FunctionPattern;
-  inductive T {
+  type T :=
     A : T;
-  };
 
   f : (T → T) → T;
   f A := A;

tests/negative/Internal/LhsTooManyPatterns.juvix

@@ -1,7 +1,6 @@
 module LhsTooManyPatterns;
-  inductive T {
+  type T :=
     A : T;
-  };
 
   f : T → T;
   f A x := A;

tests/negative/Internal/MultiWrongType.juvix

@@ -1,11 +1,9 @@
 module MultiWrongType;
-  inductive A {
+  type A :=
     a : A;
-  };
 
-  inductive B {
+  type B :=
     b : B;
-  };
 
   f : A;
   f := b;

tests/negative/Internal/PatternConstructor.juvix

@@ -1,11 +1,9 @@
 module PatternConstructor;
-  inductive A {
+  type A :=
     a : A;
-  };
 
-inductive B {
+type B :=
     b : B;
-  };
 
   f : A → B;
   f b := b;

tests/negative/Internal/Positivity/E1.juvix

@@ -1,8 +1,7 @@
 module E1;
 
 axiom B : Type;
-inductive X  {
+type X :=
   c : (X -> B) -> X;
-};
 
 end;

tests/negative/Internal/Positivity/E10.juvix

@@ -1,14 +1,11 @@
 module E10;
 
-inductive T0 (A : Type) {
+type T0 (A : Type) :=
 t : (A -> T0 A) -> T0 A;
-};
 
 alias : Type -> Type;
 alias := T0;
 
-inductive T1 {
-  c : (alias T1 -> T1;
-};
+type T1 := c : alias T1 -> T1;
 
 end;

tests/negative/Internal/Positivity/E11.juvix

@@ -1,14 +1,12 @@
 module E11;
 
-inductive T0 (A : Type) {
+type T0 (A : Type) :=
 t : (A -> T0 A) -> T0 _;
-};
 
 alias : Type -> Type -> Type;
 alias A B := A -> B;
 
-inductive T1 {
+type T1 :=
   c : alias T1 T1 -> _;
-};
 
 end;

tests/negative/Internal/Positivity/E2.juvix

@@ -2,8 +2,7 @@ module E2;
 
 open import NegParam;
 
-inductive D {
+type D :=
 d : T D -> D;
-};
 
 end;

tests/negative/Internal/Positivity/E3.juvix

@@ -1,8 +1,7 @@
 module E3;
 
 axiom B : Type;
-inductive X  {
+type X  :=
   c : B -> (X -> B) -> X;
-};
 
 end;

tests/negative/Internal/Positivity/E4.juvix

@@ -1,12 +1,10 @@
 module E4;
 
-inductive Tree (A : Type) {
-  leaf : Tree A;
+type Tree (A : Type) :=
+  leaf : Tree A |
   node : (A -> Tree A) -> Tree A;
-};
 
-inductive Bad {
+type Bad :=
   bad : Tree Bad -> Bad;
-};
 
 end;

tests/negative/Internal/Positivity/E5.juvix

@@ -1,16 +1,13 @@
 module E5;
 
-inductive T0 (A : Type){
+type T0 (A : Type) :=
 c0 : (A -> T0 A) -> T0 A;
-};
 
 axiom B : Type;
-inductive T1 (A : Type) {
+type T1 (A : Type) :=
 c1 : (B -> T0 A) -> T1 A;
-};
 
-inductive T2 {
+type T2 :=
 c2 : (B -> (B -> T1 T2)) -> T2;
-};
 
 end;

tests/negative/Internal/Positivity/E6.juvix

@@ -1,8 +1,7 @@
 module E6;
 
 axiom A : Type;
-inductive T (A : Type) {
+type T (A : Type) :=
 c : (A -> (A -> (T A -> A))) -> T A;
-};
 
 end;

tests/negative/Internal/Positivity/E7.juvix

@@ -1,11 +1,9 @@
 module E7;
 
-inductive T0 (A : Type) (B : Type) {
+type T0 (A : Type) (B : Type) :=
 c0 : (B -> A) -> T0 A B;
-};
 
-inductive T1 (A : Type) {
+type T1 (A : Type) :=
 c1 : (A -> T0 A (T1 A)) -> T1 A;
-};
 
 end;

tests/negative/Internal/Positivity/E8.juvix

@@ -1,5 +1,4 @@
 module E8;
-inductive B (A : Type) {
+type B (A : Type) :=
 b : (A -> B (B A -> A)) -> B A;
-};
 end;

tests/negative/Internal/Positivity/E9.juvix

@@ -1,11 +1,9 @@
 module E9;
 
-inductive B {
+type B :=
 b : B;
-};
 
-inductive T {
+type T :=
   c : ((B → T) -> T) -> T;
-};
 
 end;

tests/negative/Internal/Positivity/NegParam.juvix

@@ -1,5 +1,4 @@
 module NegParam;
-inductive T (A : Type) {
+type T (A : Type) :=
 c : (A -> T A) -> T A;
-};
 end;

tests/negative/Internal/Positivity/errorE5.test

@@ -1,6 +1,6 @@
 $ juvix typecheck tests/negative/Internal/Positivity/E5.juvix --no-colors
->2 /.*\.juvix\:13:21\-23\: error\:
+>2 /.*\.juvix\:11:21\-23\: error\:
 The type T2 is not strictly positive.
 It appears at a negative position in one of the arguments of the constructor c2.
 /
->= 1
+>= 1 

tests/negative/Internal/Positivity/errorE9.test

@@ -1,5 +1,5 @@
 $ juvix typecheck tests/negative/Internal/Positivity/E9.juvix --no-colors
->2 /.*\.juvix\:8:13\-14\: error\:
+>2 /.*\.juvix\:7:13\-14\: error\:
 The type T is not strictly positive.
 It appears at a negative position in one of the arguments of the constructor c.
 /

tests/negative/Internal/TooManyArguments.juvix

@@ -1,7 +1,6 @@
 module TooManyArguments;
-  inductive T (A : Type) {
+  type T (A : Type) :=
     c : A → T A;
-  };
 
   f : {A : Type} → A → T A;
   f {A} a := c {A} a a {a} ;

tests/negative/Internal/UnsolvedMeta.juvix

@@ -1,8 +1,7 @@
 module UnsolvedMeta;
 
-inductive Proxy (A : Type) {
+type Proxy (A : Type) :=
   x : Proxy A;
-};
 
 t : Proxy _;
 t := x;

tests/negative/Internal/WrongConstructorArity.juvix

@@ -1,7 +1,6 @@
 module WrongConstructorArity;
-  inductive T {
+  type T :=
     A : T → T;
-  };
 
   f : T → T;
   f (A i x) := i;

tests/negative/Internal/WrongReturnType.juvix

@@ -1,8 +1,7 @@
 module WrongReturnType;
 
 axiom B : Type;
-inductive A {
+type A :=
 c : B;
-};
 
 end;