Allow @ in constructor declarations (#127)

Reformats the standard library for * anoma/juvix#3099
anoma · Oct 22, 2024 · 481579d · 481579d
1 parent ff35179
commit 481579d
Show file tree

Hide file tree

Showing 23 changed files with 25 additions and 25 deletions.
diff --git a/Stdlib/Cairo/Ec.juvix b/Stdlib/Cairo/Ec.juvix
@@ -24,7 +24,7 @@ end;
 
 builtin ec_point
 type Point :=
-  mkPoint {
+  mkPoint@{
     x : Field;
     y : Field
   };

diff --git a/Stdlib/Cairo/Poseidon.juvix b/Stdlib/Cairo/Poseidon.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.List open;
 
 builtin poseidon_state
 type PoseidonState :=
-  mkPoseidonState {
+  mkPoseidonState@{
     s0 : Field;
     s1 : Field;
     s2 : Field

diff --git a/Stdlib/Data/BinaryTree.juvix b/Stdlib/Data/BinaryTree.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.List open;
 
 type BinaryTree (A : Type) :=
   | leaf
-  | node {
+  | node@{
       left : BinaryTree A;
       element : A;
       right : BinaryTree A

diff --git a/Stdlib/Data/Map.juvix b/Stdlib/Data/Map.juvix
@@ -20,7 +20,7 @@ open AVL using {AVLTree};
 import Stdlib.Data.BinaryTree as Tree;
 
 type Binding Key Value :=
-  mkBinding {
+  mkBinding@{
     key : Key;
     value : Value
   };

diff --git a/Stdlib/Data/Queue/Base.juvix b/Stdlib/Data/Queue/Base.juvix
@@ -19,7 +19,7 @@ import Stdlib.Trait.Foldable open;
 
 --- A first-in-first-out data structure
 type Queue (A : Type) :=
-  mkQueue {
+  mkQueue@{
     front : List A;
     back : List A
   };

diff --git a/Stdlib/Data/Range.juvix b/Stdlib/Data/Range.juvix
@@ -10,13 +10,13 @@ import Stdlib.Data.Nat open;
 
 --- An inclusive range of naturals
 type Range N :=
-  mkRange {
+  mkRange@{
     low : N;
     high : N
   };
 
 type StepRange N :=
-  mkStepRange {
+  mkStepRange@{
     range : Range N;
     step : N
   };

diff --git a/Stdlib/Data/Set/AVL.juvix b/Stdlib/Data/Set/AVL.juvix
@@ -24,7 +24,7 @@ type AVLTree (A : Type) :=
   | --- An empty AVL tree.
     empty
   | --- A node of an AVL tree.
-    node {
+    node@{
       element : A;
       height : Nat;
       left : AVLTree A;

diff --git a/Stdlib/Data/Tree.juvix b/Stdlib/Data/Tree.juvix
@@ -11,7 +11,7 @@ Forest (A : Type) : Type := List (Tree A);
 
 --- N-Ary tree.
 type Tree (A : Type) :=
-  node {
+  node@{
     element : A;
     children : List (Tree A)
   };

diff --git a/Stdlib/Data/UnbalancedSet.juvix b/Stdlib/Data/UnbalancedSet.juvix
@@ -8,7 +8,7 @@ import Stdlib.Data.BinaryTree as Tree;
 open Tree using {BinaryTree; leaf; node};
 
 type UnbalancedSet (A : Type) :=
-  mkUnbalancedSet {
+  mkUnbalancedSet@{
     order : Ord A;
     tree : BinaryTree A
   };

diff --git a/Stdlib/Trait/Applicative.juvix b/Stdlib/Trait/Applicative.juvix
@@ -12,7 +12,7 @@ import Stdlib.Data.Unit.Base open;
 
 trait
 type Applicative (F : Type -> Type) :=
-  mkApplicative {
+  mkApplicative@{
     {{functor}} : Functor F;
     pure : {A : Type} -> A -> F A;
     ap : {A B : Type} -> F (A -> B) -> F A -> F B

diff --git a/Stdlib/Trait/DivMod.juvix b/Stdlib/Trait/DivMod.juvix
@@ -2,7 +2,7 @@ module Stdlib.Trait.DivMod;
 
 trait
 type DivMod A :=
-  mkDivMod {
+  mkDivMod@{
     {-# isabelle-operator: {name: "div", prec: 70, assoc: left} #-}
     div : A -> A -> A;
     {-# isabelle-operator: {name: "mod", prec: 70, assoc: left} #-}

diff --git a/Stdlib/Trait/Eq.juvix b/Stdlib/Trait/Eq.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Fixity open;
 
 --- A trait defining equality
 trait
-type Eq A := mkEq {eq : A -> A -> Bool};
+type Eq A := mkEq@{eq : A -> A -> Bool};
 
 syntax operator == comparison;
 syntax operator /= comparison;

diff --git a/Stdlib/Trait/Foldable/Monomorphic.juvix b/Stdlib/Trait/Foldable/Monomorphic.juvix
@@ -7,7 +7,7 @@ import Stdlib.Trait.Foldable.Polymorphic as Poly;
 {-# specialize: true #-}
 trait
 type Foldable (Container Elem : Type) :=
-  mkFoldable {
+  mkFoldable@{
     syntax iterator for {init := 1; range := 1};
     for : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B;
 

diff --git a/Stdlib/Trait/Foldable/Polymorphic.juvix b/Stdlib/Trait/Foldable/Polymorphic.juvix
@@ -5,7 +5,7 @@ import Stdlib.Function open;
 --- A trait for combining elements into a single result, processing one element at a time.
 trait
 type Foldable (F : Type -> Type) :=
-  mkFoldable {
+  mkFoldable@{
     syntax iterator for {init := 1; range := 1};
     for : {A B : Type} -> (B -> A -> B) -> B -> F A -> B;
 

diff --git a/Stdlib/Trait/Functor/Monomorphic.juvix b/Stdlib/Trait/Functor/Monomorphic.juvix
@@ -7,7 +7,7 @@ import Stdlib.Trait.Functor.Polymorphic as Poly;
 {-# specialize: true #-}
 trait
 type Functor (Container Elem : Type) :=
-  mkFunctor {
+  mkFunctor@{
     syntax iterator map {init := 0; range := 1};
     {-# specialize: [1] #-}
     map : (Elem -> Elem) -> Container -> Container

diff --git a/Stdlib/Trait/Functor/Polymorphic.juvix b/Stdlib/Trait/Functor/Polymorphic.juvix
@@ -6,7 +6,7 @@ import Stdlib.Data.Unit open;
 {-# specialize: true #-}
 trait
 type Functor (F : Type -> Type) :=
-  mkFunctor {
+  mkFunctor@{
     syntax iterator map {init := 0; range := 1};
     {-# specialize: [1] #-}
     map : {A B : Type} -> (A -> B) -> F A -> F B

diff --git a/Stdlib/Trait/Integral.juvix b/Stdlib/Trait/Integral.juvix
@@ -6,7 +6,7 @@ import Stdlib.Trait.Natural open;
 
 trait
 type Integral A :=
-  mkIntegral {
+  mkIntegral@{
     naturalI : Natural A;
     syntax operator - additive;
     {-# isabelle-operator: {name: "-", prec: 65, assoc: left} #-}

diff --git a/Stdlib/Trait/Monad.juvix b/Stdlib/Trait/Monad.juvix
@@ -5,7 +5,7 @@ import Stdlib.Trait.Applicative open;
 
 trait
 type Monad (M : Type -> Type) :=
-  mkMonad {
+  mkMonad@{
     {{applicative}} : Applicative M;
     builtin monad-bind
     bind : {A B : Type} -> M A -> (A -> M B) -> M B

diff --git a/Stdlib/Trait/Numeric.juvix b/Stdlib/Trait/Numeric.juvix
@@ -5,7 +5,7 @@ import Stdlib.Trait.Integral open;
 
 trait
 type Numeric A :=
-  mkNumeric {
+  mkNumeric@{
     integralI : Integral A;
     syntax operator / multiplicative;
     / : A -> A -> A

diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix
@@ -36,7 +36,7 @@ orderingEqI : Eq Ordering :=
 
 --- A trait for defining a total order
 trait
-type Ord A := mkOrd {cmp : A -> A -> Ordering};
+type Ord A := mkOrd@{cmp : A -> A -> Ordering};
 
 syntax operator <= comparison;
 

diff --git a/Stdlib/Trait/Partial.juvix b/Stdlib/Trait/Partial.juvix
@@ -4,7 +4,7 @@ import Stdlib.Data.String.Base open;
 import Stdlib.Debug.Fail as Debug;
 
 trait
-type Partial := mkPartial {fail : {A : Type} -> String -> A};
+type Partial := mkPartial@{fail : {A : Type} -> String -> A};
 
 open Partial public;
 

diff --git a/Stdlib/Trait/Show.juvix b/Stdlib/Trait/Show.juvix
@@ -3,4 +3,4 @@ module Stdlib.Trait.Show;
 import Stdlib.Data.String.Base open;
 
 trait
-type Show A := mkShow {show : A -> String};
+type Show A := mkShow@{show : A -> String};
diff --git a/test/Test/AVL.juvix b/test/Test/AVL.juvix
@@ -5,7 +5,7 @@ import Stdlib.Prelude open;
 
 import Stdlib.Data.Set.AVL as AVL open;
 
-type Box := mkBox {b : Nat};
+type Box := mkBox@{b : Nat};
 
 instance
 BoxOrdI : Ord Box := mkOrd (Ord.cmp on Box.b);
@@ -24,7 +24,7 @@ mkTests {A} (descr : TestDescr A) : List Test :=
          ];
 
 type TestDescr (A : Type) :=
-  mkTestDescr {
+  mkTestDescr@{
     testTitle : String;
     testLen : Nat;
     testSet : AVLTree A