Change syntax for ind. data types and forbid the empty data type

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,41 +2,38 @@
 
 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
 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;

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
           }