Remove @?

Package.juvix

@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "stdlib";
     version := mkVersion 0 0 1;
     dependencies := []

Stdlib/Cairo/Ec.juvix

@@ -60,7 +60,7 @@ double (point : Point) : Point :=
             slope := (3 * x * x + StarkCurve.ALPHA) / (2 * y);
             r_x := slope * slope - x - x;
             r_y := slope * (x - r_x) - y;
-          in mkPoint@?{
+          in mkPoint@{
                x := r_x;
                y := r_y;
              };

Stdlib/Data/Bool.juvix

@@ -8,27 +8,12 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 
 {-# specialize: true, inline: case #-}
-instance
-eqBoolI : Eq Bool :=
-  mkEq@{
-    eq (x y : Bool) : Bool :=
-      case x, y of
-        | true, true := true
-        | false, false := true
-        | _ := false;
-  };
+deriving instance
+eqBoolI : Eq Bool;
 
 {-# specialize: true, inline: case #-}
-instance
-ordBoolI : Ord Bool :=
-  mkOrd@{
-    cmp (x y : Bool) : Ordering :=
-      case x, y of
-        | false, false := Equal
-        | false, true := LessThan
-        | true, false := GreaterThan
-        | true, true := Equal;
-  };
+deriving instance
+ordBoolI : Ord Bool;
 
 instance
 showBoolI : Show Bool :=

Stdlib/Data/Field.juvix

@@ -1,7 +1,7 @@
 module Stdlib.Data.Field;
 
 import Stdlib.Data.Field.Base open using {Field} public;
-import Stdlib.Data.Field.Base as Field;
+import Stdlib.Data.Field.Base as Field public;
 import Stdlib.Data.String.Base open;
 import Stdlib.Data.Nat;
 

Stdlib/Data/Int.juvix

@@ -1,8 +1,13 @@
 module Stdlib.Data.Int;
 
-import Stdlib.Data.Int.Base open hiding {+; -; *; div; mod} public;
--- should be re-exported qualified
-import Stdlib.Data.Int.Base as Int;
+import Stdlib.Data.Int.Base open hiding {module Int; +; -; *; div; mod} public;
+
+module Int;
+  open Stdlib.Data.Int.Base.Int public;
+
+  import Stdlib.Data.Int.Base open public;
+  import Stdlib.Data.Int.Ord open public;
+end;
 
 import Stdlib.Data.String open;
 import Stdlib.Data.Bool open;
@@ -15,9 +20,6 @@ import Stdlib.Trait.FromNatural open;
 import Stdlib.Trait.Integral open;
 import Stdlib.Trait.DivMod open;
 
--- should be re-exported qualified
-import Stdlib.Data.Int.Ord as Int;
-
 --- Converts an ;Int; into ;String;.
 builtin int-to-string
 axiom intToString : Int -> String;

Stdlib/Data/List.juvix

@@ -21,6 +21,7 @@ phead {A} {{Partial}} : List A -> A
   | (x :: _) := x
   | nil := fail "head: empty list";
 
+{-# specialize: true, inline: case #-}
 instance
 eqListI {A} {{Eq A}} : Eq (List A) :=
   let
@@ -37,6 +38,7 @@ eqListI {A} {{Eq A}} : Eq (List A) :=
 isMember {A} {{Eq A}} (elem : A) (list : List A) : Bool :=
   isElement (Eq.eq) elem list;
 
+{-# specialize: true, inline: case #-}
 instance
 ordListI {A} {{Ord A}} : Ord (List A) :=
   let
@@ -71,7 +73,7 @@ functorListI : Functor List :=
     map := listMap;
   };
 
-{-# specialize: true, inline: true #-}
+{-# specialize: true, inline: case #-}
 instance
 monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A :=
   fromPolymorphicFunctor;
@@ -84,7 +86,7 @@ polymorphicFoldableListI : Polymorphic.Foldable List :=
     rfor := listRfor;
   };
 
-{-# specialize: true, inline: true #-}
+{-# specialize: true, inline: case #-}
 instance
 foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;
 

Stdlib/Data/Map.juvix

@@ -32,6 +32,7 @@ value {Key Value} (binding : Binding Key Value) : Value :=
 toPair {Key Value} (binding : Binding Key Value) : Pair Key Value :=
   key binding, value binding;
 
+{-# specialize: true, inline: case #-}
 instance
 bindingKeyOrdering {Key Value} {{Ord Key}} : Ord (Binding Key Value) :=
   mkOrd@{

Stdlib/Data/Maybe.juvix

@@ -14,15 +14,8 @@ import Stdlib.Data.String.Base open;
 import Stdlib.Data.Pair.Base open;
 
 {-# specialize: true, inline: case #-}
-instance
-eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
-  mkEq@{
-    eq (m1 m2 : Maybe A) : Bool :=
-      case m1, m2 of
-        | nothing, nothing := true
-        | just a1, just a2 := Eq.eq a1 a2
-        | _ := false;
-  };
+deriving instance
+eqMaybeI {A} {{Eq A}} : Eq (Maybe A);
 
 instance
 showMaybeI {A} {{Show A}} : Show (Maybe A) :=
@@ -34,16 +27,8 @@ showMaybeI {A} {{Show A}} : Show (Maybe A) :=
   };
 
 {-# specialize: true, inline: case #-}
-instance
-ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
-  mkOrd@{
-    cmp (m1 m2 : Maybe A) : Ordering :=
-      case m1, m2 of
-        | nothing, nothing := Equal
-        | just a1, just a2 := Ord.cmp a1 a2
-        | nothing, just _ := LessThan
-        | just _, nothing := GreaterThan;
-  };
+deriving instance
+ordMaybeI {A} {{Ord A}} : Ord (Maybe A);
 
 {-# specialize: true, inline: case #-}
 instance

Stdlib/Data/Nat.juvix

@@ -1,9 +1,15 @@
 module Stdlib.Data.Nat;
 
-import Juvix.Builtin.V1.Nat open public;
-import Stdlib.Data.Nat.Base open hiding {+; *; div; mod} public;
--- should be re-exported qualified
-import Stdlib.Data.Nat.Base as Nat;
+import Juvix.Builtin.V1.Nat open hiding {module Nat} public;
+import Stdlib.Data.Nat.Base open hiding {module Nat; +; *; div; mod} public;
+
+module Nat;
+  open Stdlib.Data.Nat.Base.Nat public;
+
+  import Stdlib.Data.Nat.Base open public;
+  import Stdlib.Data.Nat.Ord open public;
+end;
+
 import Stdlib.Data.String.Base open;
 
 import Stdlib.Trait.Eq open public;
@@ -13,9 +19,6 @@ import Stdlib.Trait.Natural open public;
 import Stdlib.Trait.FromNatural open public;
 import Stdlib.Trait.DivMod open public;
 
--- should be re-exported qualified
-import Stdlib.Data.Nat.Ord as Nat;
-
 --- Converts a ;Nat; into a ;String;.
 builtin nat-to-string
 axiom natToString : Nat -> String;

Stdlib/Data/Ordering.juvix

@@ -0,0 +1,38 @@
+module Stdlib.Data.Ordering;
+
+import Stdlib.Trait.Eq open;
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Trait.Show open;
+
+builtin ordering
+type Ordering :=
+  | LessThan
+  | Equal
+  | GreaterThan;
+
+isLessThan (ordering : Ordering) : Bool :=
+  case ordering of
+    | LessThan := true
+    | _ := false;
+
+isEqual (ordering : Ordering) : Bool :=
+  case ordering of
+    | Equal := true
+    | _ := false;
+
+isGreaterThan (ordering : Ordering) : Bool :=
+  case ordering of
+    | GreaterThan := true
+    | _ := false;
+
+deriving instance
+orderingEqI : Eq Ordering;
+
+instance
+orderingShowI : Show Ordering :=
+  mkShow@{
+    show : Ordering -> String
+      | Equal := "Equal"
+      | LessThan := "LessThan"
+      | GreaterThan := "GreaterThan";
+  };

Stdlib/Data/Pair.juvix

@@ -9,27 +9,12 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 
 {-# specialize: true, inline: case #-}
-instance
-eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B)
-  | {{mkEq eqA}} {{mkEq eqB}} :=
-    mkEq@{
-      eq (p1 p2 : Pair A B) : Bool :=
-        case p1, p2 of (a1, b1), a2, b2 := eqA a1 a2 && eqB b1 b2;
-    };
+deriving instance
+eqProductI {A B} {{Eq A}} {{Eq B}} : Eq (Pair A B);
 
 {-# specialize: true, inline: case #-}
-instance
-ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
-  | {{mkOrd cmpA}} {{mkOrd cmpB}} :=
-    mkOrd@{
-      cmp (p1 p2 : Pair A B) : Ordering :=
-        case p1, p2 of
-          (a1, b1), a2, b2 :=
-            case cmpA a1 a2 of
-              | LessThan := LessThan
-              | GreaterThan := GreaterThan
-              | Equal := cmpB b1 b2;
-    };
+deriving instance
+ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B);
 
 instance
 showProductI {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)

Stdlib/Data/Result.juvix

@@ -11,28 +11,12 @@ import Stdlib.Trait.Show open;
 import Stdlib.Trait open;
 
 {-# specialize: true, inline: case #-}
-instance
-ordResultI
-  {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value) :=
-  mkOrd@{
-    cmp (result1 result2 : Result Error Value) : Ordering :=
-      case result1, result2 of
-        | error a1, error a2 := Ord.cmp a1 a2
-        | ok b1, ok b2 := Ord.cmp b1 b2
-        | error _, ok _ := LessThan
-        | ok _, error _ := GreaterThan;
-  };
+deriving instance
+ordResultI {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value);
 
 {-# specialize: true, inline: case #-}
-instance
-eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value) :=
-  mkEq@{
-    eq (result1 result2 : Result Error Value) : Bool :=
-      case result1, result2 of
-        | error a1, error a2 := a1 == a2
-        | ok b1, ok b2 := b1 == b2
-        | _, _ := false;
-  };
+deriving instance
+eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value);
 
 instance
 showResultI

Stdlib/Data/Unit.juvix

@@ -10,17 +10,11 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 import Stdlib.Trait.Foldable open;
 
-instance
-eqUnitI : Eq Unit :=
-  mkEq@{
-    eq (_ _ : Unit) : Bool := true;
-  };
+deriving instance
+eqUnitI : Eq Unit;
 
-instance
-ordUnitI : Ord Unit :=
-  mkOrd@{
-    cmp (_ _ : Unit) : Ordering := Equal;
-  };
+deriving instance
+ordUnitI : Ord Unit;
 
 instance
 showUnitI : Show Unit :=

Stdlib/Trait/Eq.juvix

@@ -4,8 +4,13 @@ import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.Fixity open;
 
 --- A trait defining equality
+builtin eq
 trait
-type Eq A := mkEq@{eq : A -> A -> Bool};
+type Eq A :=
+  mkEq@{
+    builtin isEqual
+    eq : A -> A -> Bool;
+  };
 
 syntax operator == comparison;
 syntax operator /= comparison;

Stdlib/Trait/Foldable/Monomorphic.juvix

@@ -19,7 +19,7 @@ open Foldable public;
 
 --- Make a monomorphic ;Foldable; instance from a polymorphic one.
 --- All polymorphic types that are an instance of ;Poly.Foldable; should use this function to create their monomorphic ;Foldable; instance.
-{-# inline: case #-}
+{-# inline: always #-}
 fromPolymorphicFoldable
   {F : Type -> Type}
   {{foldable : Poly.Foldable F}}

Stdlib/Trait/Functor/Monomorphic.juvix

@@ -15,7 +15,7 @@ type Functor (Container Elem : Type) :=
 
 open Functor public;
 
-{-# inline: case #-}
+{-# inline: always #-}
 fromPolymorphicFunctor
   {F : Type -> Type} {{Poly.Functor F}} {Elem} : Functor (F Elem) Elem :=
   mkFunctor@{