Skip to content

Commit 17a82dd

Browse files
lukaszczpaulcadman
lukaszcz
and
paulcadman
authored
Update pragmas (#122)
* Closes #121 * Depends on anoma/juvix#2944 * Includes #123 * Adds `Stdlib.Data.Range` to the Prelude. Since now `for` and `rfor` are trait fields, there is no name clash anymore. --------- Co-authored-by: Paul Cadman <[email protected]>
1 parent 5424a48 commit 17a82dd

File tree

16 files changed

+94
-34
lines changed

16 files changed

+94
-34
lines changed

‎Stdlib/Data/Bool.juvix‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import Stdlib.Trait.Eq open;
55
import Stdlib.Trait.Ord open;
66
import Stdlib.Trait.Show open;
77

8+
{-# specialize: true, inline: case #-}
89
instance
910
boolEqI : Eq Bool :=
1011
mkEq
@@ -14,6 +15,7 @@ boolEqI : Eq Bool :=
1415
| _ _ := false
1516
};
1617

18+
{-# specialize: true, inline: case #-}
1719
instance
1820
boolOrdI : Ord Bool :=
1921
mkOrd

‎Stdlib/Data/Bool/Base.juvix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ import Juvix.Builtin.V1.Bool open public;
44
import Stdlib.Data.Fixity open;
55

66
--- Logical negation.
7-
{-# isabelle-function: {name: "¬"} #-}
7+
{-# isabelle-function: {name: "\\<not>"} #-}
88
not : Bool → Bool
99
| true := false
1010
| false := true;

‎Stdlib/Data/List.juvix‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,21 +53,25 @@ showListI {A} {{Show A}} : Show (List A) :=
5353
| s := "(" ++str go s ++str ")"
5454
};
5555

56+
{-# specialize: true, inline: case #-}
5657
instance
5758
functorListI : Functor List :=
5859
mkFunctor@{
5960
map := listMap
6061
};
6162

63+
{-# specialize: true, inline: true #-}
6264
instance
6365
monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A := fromPolymorphicFunctor;
6466

67+
{-# specialize: true, inline: case #-}
6568
instance
6669
polymorphicFoldableListI : Polymorphic.Foldable List :=
6770
Polymorphic.mkFoldable@{
6871
for := listFor;
6972
rfor := listRfor
7073
};
7174

75+
{-# specialize: true, inline: true #-}
7276
instance
7377
foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;

‎Stdlib/Data/Maybe.juvix‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import Stdlib.Trait.Functor open;
1010
import Stdlib.Data.Bool.Base open;
1111
import Stdlib.Data.String.Base open;
1212

13+
{-# specialize: true, inline: case #-}
1314
instance
1415
eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
1516
mkEq
@@ -27,6 +28,7 @@ showMaybeI {A} {{Show A}} : Show (Maybe A) :=
2728
| (just a) := "just " ++str Show.show a
2829
};
2930

31+
{-# specialize: true, inline: case #-}
3032
instance
3133
ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
3234
mkOrd
@@ -37,6 +39,7 @@ ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
3739
| (just _) nothing := GT
3840
};
3941

42+
{-# specialize: true, inline: case #-}
4043
instance
4144
functorMaybeI : Functor Maybe :=
4245
mkFunctor@{
@@ -45,5 +48,6 @@ functorMaybeI : Functor Maybe :=
4548
| (just a) := just (f a)
4649
};
4750

51+
{-# specizalize: true, inline: true #-}
4852
instance
4953
monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A := fromPolymorphicFunctor;

‎Stdlib/Data/Pair.juvix‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,12 @@ import Stdlib.Trait.Eq open;
88
import Stdlib.Trait.Ord open;
99
import Stdlib.Trait.Show open;
1010

11+
{-# specialize: true, inline: case #-}
1112
instance
1213
eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B)
1314
| {{mkEq eq-a}} {{mkEq eq-b}} := mkEq λ {(a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2};
1415

16+
{-# specialize: true, inline: case #-}
1517
instance
1618
ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
1719
| {{mkOrd cmp-a}} {{mkOrd cmp-b}} :=

‎Stdlib/Data/Range.juvix‎

Lines changed: 53 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -12,53 +12,81 @@ import Stdlib.Data.Nat open;
1212
type Range N :=
1313
mkRange {
1414
low : N;
15-
high : N;
16-
step : N
15+
high : N
1716
};
1817

19-
syntax iterator for {init := 1; range := 1};
20-
21-
{-# specialize: [1, 2, 3, 5] #-}
22-
for {A N} {{Ord N}} {{Natural N}} (f : A → N → A) (a : A) : Range N → A
23-
| mkRange@{low; high; step} :=
24-
let
25-
{-# specialize-by: [f] #-}
26-
terminating
27-
go (acc : A) (n : N) : A := ite (n > high) acc (go (f acc n) (n + step));
28-
in go a low;
18+
type StepRange N :=
19+
mkStepRange {
20+
range : Range N;
21+
step : N
22+
};
2923

3024
syntax operator to range;
3125

3226
--- `x to y` is the range [x..y]
3327
{-# inline: always #-}
34-
to {N} {{Natural N}} (l h : N) : Range N := mkRange l h 1;
28+
to {N} {{Natural N}} (l h : N) : Range N := mkRange l h;
3529

3630
syntax operator step step;
3731

3832
--- `x to y step s` is the range [x, x + s, ..., y]
3933
{-# inline: always #-}
40-
step {N} (r : Range N) (s : N) : Range N := r@Range{step := s};
34+
step {N} (r : Range N) (s : N) : StepRange N := mkStepRange r s;
35+
36+
-- This instance assumes that `low <= high`.
37+
{-# specialize: true, inline: case #-}
38+
instance
39+
foldableRangeI {N} {{Eq N}} {{Natural N}} : Foldable (Range N) N :=
40+
mkFoldable@{
41+
{-# specialize: [1, 3] #-}
42+
for {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B
43+
| (mkRange low high) :=
44+
let
45+
{-# specialize-by: [f, high] #-}
46+
terminating
47+
go (acc : B) (next : N) : B :=
48+
if
49+
| next == high := f acc next
50+
| else := go (f acc next) (next + 1);
51+
in go ini low;
52+
{-# specialize: [1, 3] #-}
53+
rfor {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B
54+
| (mkRange low high) :=
55+
let
56+
{-# specialize-by: [f, high] #-}
57+
terminating
58+
go (next : N) : B :=
59+
if
60+
| next == high := f ini next
61+
| else := f (go (next + 1)) next;
62+
in go low
63+
};
4164

4265
-- This instance assumes that (low + step*k > high) for some k.
66+
{-# specialize: true, inline: case #-}
4367
instance
44-
foldableRangeI {N} {{Ord N}} {{Natural N}} : Foldable (Range N) N :=
68+
foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N :=
4569
mkFoldable@{
46-
for {B : Type} (g : B -> N -> B) (ini : B) : Range N -> B
47-
| (mkRange low high step) :=
70+
{-# specialize: [1, 3] #-}
71+
for {B : Type} (f : B -> N -> B) (ini : B) : StepRange N -> B
72+
| (mkStepRange (mkRange low high) step) :=
4873
let
74+
{-# specialize-by: [f, high, step] #-}
4975
terminating
5076
go (acc : B) (next : N) : B :=
5177
if
52-
| next <= high := go (g acc next) (next + step)
53-
| else := acc;
78+
| next > high := acc
79+
| else := go (f acc next) (next + step);
5480
in go ini low;
55-
rfor {B : Type} (g : B -> N -> B) (ini : B) : Range N -> B
56-
| (mkRange low high step) :=
81+
{-# specialize: [1, 3] #-}
82+
rfor {B : Type} (f : B -> N -> B) (ini : B) : StepRange N -> B
83+
| (mkStepRange (mkRange low high) step) :=
5784
let
85+
{-# specialize-by: [f, high, step] #-}
5886
terminating
59-
go (base : B) (next : N) : B :=
87+
go (next : N) : B :=
6088
if
61-
| next <= high := g (go base (next + step)) next
62-
| else := base;
63-
in go ini low
89+
| next <= high := f (go (next + step)) next
90+
| else := ini;
91+
in go low
6492
};

‎Stdlib/Data/Result.juvix‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import Stdlib.Trait.Eq open;
77
import Stdlib.Trait.Ord open;
88
import Stdlib.Trait.Functor open;
99

10+
{-# specialize: true, inline: case #-}
1011
instance
1112
ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) :=
1213
mkOrd@{
@@ -17,6 +18,7 @@ ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) :=
1718
| (ok _) (error _) := GT
1819
};
1920

21+
{-# specialize: true, inline: case #-}
2022
instance
2123
eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) :=
2224
mkEq@{
@@ -26,12 +28,14 @@ eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) :=
2628
| _ _ := false
2729
};
2830

31+
{-# specialize: true, inline: case #-}
2932
instance
3033
functorResultI {err} : Functor (Result err) :=
3134
mkFunctor@{
3235
map := mapOk
3336
};
3437

38+
{-# specialize: true, inline: true #-}
3539
instance
3640
monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) res :=
3741
fromPolymorphicFunctor;

‎Stdlib/Data/Unit.juvix‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,12 @@ ordUnitI : Ord Unit := mkOrd λ {unit unit := EQ};
2121
instance
2222
showUnitI : Show Unit := mkShow λ {unit := "unit"};
2323

24+
{-# specialize: true, inline: case #-}
2425
instance
2526
foldableUnitI : Foldable Unit Unit :=
2627
mkFoldable@{
28+
{-# inline: true #-}
2729
rfor {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit;
30+
{-# inline: true #-}
2831
for {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit
2932
};

‎Stdlib/Prelude.juvix‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ import Stdlib.Data.Field open public;
1414
import Stdlib.Data.Pair open public;
1515
import Stdlib.Data.String open public;
1616
import Stdlib.Data.Result open public;
17+
import Stdlib.Data.Range open public;
1718
import Stdlib.Function open public;
1819
import Stdlib.System.IO open public;
1920

‎Stdlib/Trait/Eq.juvix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,5 +14,5 @@ syntax operator /= comparison;
1414
== {A} {{Eq A}} : A -> A -> Bool := Eq.eq;
1515

1616
--- Tests for inequality.
17-
{-# inline: always, isabelle-operator: {name: "≠", prec: 50, assoc: none} #-}
17+
{-# inline: always, isabelle-operator: {name: "\\<noteq>", prec: 50, assoc: none} #-}
1818
/= {A} {{Eq A}} (x y : A) : Bool := not (x == y);

0 commit comments

Comments
 (0)