ed4427c · jibb · git.iko.soy

git.iko.soy/jibb

Show where unface meets S1 step 1

ed4427cClaude13 hours ago

tests/golden/inline-unface-labelled-slot/about.txtnew file+4

@@ -0,0 +1,4 @@

1+source: docs/spec/grammar.md, Expressions, Unface: "`(unface e)` is `e` with every face removed from its type, so a gate or record fits where other names are expected"

2+tests: An unfaced gate passed to a slot that writes its own labels: a closed gate fits, as "an unnamed position can unify with a faced position" allows; a generic one still fails, because its capital A meets the faced x=@ud, and a capital binding only the type under a face is S1 step 1, not part of this rule.

3+expect: parses

4+expect-types: a partial inference report

tests/golden/inline-unface-labelled-slot/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-labelled-slot/source.jibbnew file+5

@@ -0,0 +1,5 @@

1+++ lt-a |= [a=@ud b=@ud] (gth b a)

2+++ lth2 |= [x=A y=A] (gth y x)

3+++ take-xy |= f=$-([x=@ud y=@ud] ?) (f 1 2)

4+++ closed (take-xy (unface lt-a))

5+++ generic (take-xy (unface lth2))

tests/golden/inline-unface-labelled-slot/tokens.txtnew file+76

@@ -0,0 +1,76 @@

1+1:1 glyph ++

2+1:4 name lt-a

3+1:9 glyph |=

4+1:12 glyph [

5+1:13 tight name a

6+1:14 tight glyph =

7+1:15 tight aura @ud

8+1:19 name b

9+1:20 tight glyph =

10+1:21 tight aura @ud

11+1:24 tight glyph ]

12+1:26 glyph (

13+1:27 tight name gth

14+1:31 name b

15+1:33 name a

16+1:34 tight glyph )

17+2:1 NEWLINE

18+2:1 glyph ++

19+2:4 name lth2

20+2:9 glyph |=

21+2:12 glyph [

22+2:13 tight name x

23+2:14 tight glyph =

24+2:15 tight tvar A

25+2:17 name y

26+2:18 tight glyph =

27+2:19 tight tvar A

28+2:20 tight glyph ]

29+2:22 glyph (

30+2:23 tight name gth

31+2:27 name y

32+2:29 name x

33+2:30 tight glyph )

34+3:1 NEWLINE

35+3:1 glyph ++

36+3:4 name take-xy

37+3:12 glyph |=

38+3:15 name f

39+3:16 tight glyph =

40+3:17 tight glyph $-(

41+3:20 tight glyph [

42+3:21 tight name x

43+3:22 tight glyph =

44+3:23 tight aura @ud

45+3:27 name y

46+3:28 tight glyph =

47+3:29 tight aura @ud

48+3:32 tight glyph ]

49+3:34 glyph ?

50+3:35 tight glyph )

51+3:37 glyph (

52+3:38 tight name f

53+3:40 lit 1

54+3:42 lit 2

55+3:43 tight glyph )

56+4:1 NEWLINE

57+4:1 glyph ++

58+4:4 name closed

59+4:11 glyph (

60+4:12 tight name take-xy

61+4:20 glyph (

62+4:21 tight name unface

63+4:28 name lt-a

64+4:32 tight glyph )

65+4:33 tight glyph )

66+5:1 NEWLINE

67+5:1 glyph ++

68+5:4 name generic

69+5:12 glyph (

70+5:13 tight name take-xy

71+5:21 glyph (

72+5:22 tight name unface

73+5:29 name lth2

74+5:33 tight glyph )

75+5:34 tight glyph )

76+5:35 NEWLINE

tests/golden/inline-unface-labelled-slot/tree.txtnew file+37

@@ -0,0 +1,37 @@

1+(module

2+ (value 1:1 lt-a

3+ (gate 1:9

4+ (cell 1:12

5+ (face 1:13 a (aura 1:15 @ud))

6+ (face 1:19 b (aura 1:21 @ud)))

7+ (group 1:26

8+ (call 1:27 (wing 1:27 gth) (wing 1:31 b) (wing 1:33 a)))))

9+ (value 2:1 lth2

10+ (gate 2:9

11+ (cell 2:12

12+ (face 2:13 x (tvar 2:15 A))

13+ (face 2:17 y (tvar 2:19 A)))

14+ (group 2:22

15+ (call 2:23 (wing 2:23 gth) (wing 2:27 y) (wing 2:29 x)))))

16+ (value 3:1 take-xy

17+ (gate 3:12

18+ (face 3:15 f

19+ (fn 3:17

20+ (cell 3:20

21+ (face 3:21 x (aura 3:23 @ud))

22+ (face 3:27 y (aura 3:29 @ud)))

23+ (flag 3:34)))

24+ (group 3:37

25+ (call 3:38 (wing 3:38 f) (lit 3:40 1) (lit 3:42 2)))))

26+ (value 4:1 closed

27+ (group 4:11

28+ (call 4:12

29+ (wing 4:12 take-xy)

30+ (group 4:20

31+ (call 4:21 (wing 4:21 unface) (wing 4:28 lt-a))))))

32+ (value 5:1 generic

33+ (group 5:12

34+ (call 5:13

35+ (wing 5:13 take-xy)

36+ (group 5:21

37+ (call 5:22 (wing 5:22 unface) (wing 5:29 lth2)))))))

tests/golden/inline-unface-labelled-slot/types.txtnew file+12

@@ -0,0 +1,12 @@

1+partial inference; module not checked

2+++ lt-a: $-([a=@ud b=@ud] ?)

3+++ lth2: $-([x=A y=A] ?) where A is an atom

4+++ take-xy: $-($-([x=@ud y=@ud] ?) ?)

5+++ closed: ?

6+++ generic: call's sample and argument types do not unify

7+/tests/golden/inline-unface-labelled-slot/source.jibb:5:13: called gate has type $-($-([x=@ud y=@ud] ?) ?)

8+++ generic (take-xy (unface lth2))

9+ ^

10+/tests/golden/inline-unface-labelled-slot/source.jibb:5:21: argument has type $-([A A] ?) where A is an atom

11+++ generic (take-xy (unface lth2))

12+ ^

tests/golden/inline-unface-lambda/about.txtnew file+4

@@ -0,0 +1,4 @@

1+source: docs/spec/grammar.md, Expressions, Unface: "`(unface e)` is `e` with every face removed from its type, so a gate or record fits where other names are expected"

2+tests: A lambda that names its sample k and v fails turn's slot over [p=@t q=@ud] and fits it once unfaced. turn's capital A then binds the faced p=@t, so the result keeps p=: that is S1 step 1 (a capital binds only the type under a face), which this rule leaves to the review's unification work.

3+expect: parses

4+expect-types: a partial inference report

tests/golden/inline-unface-lambda/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-lambda/source.jibbnew file+3

@@ -0,0 +1,3 @@

1+++ pairs ^- (list [p=@t q=@ud]) ~[["a" 1]]

2+++ keys-labelled (turn pairs |=([k v] k))

3+++ keys (turn pairs (unface |=([k v] k)))

tests/golden/inline-unface-lambda/tokens.txtnew file+52

@@ -0,0 +1,52 @@

1+1:1 glyph ++

2+1:4 name pairs

3+1:10 glyph ^-

4+1:13 glyph (

5+1:14 tight name list

6+1:19 glyph [

7+1:20 tight name p

8+1:21 tight glyph =

9+1:22 tight aura @t

10+1:25 name q

11+1:26 tight glyph =

12+1:27 tight aura @ud

13+1:30 tight glyph ]

14+1:31 tight glyph )

15+1:33 glyph ~[

16+1:35 tight glyph [

17+1:36 tight str "a"

18+1:40 lit 1

19+1:41 tight glyph ]

20+1:42 tight glyph ]

21+2:1 NEWLINE

22+2:1 glyph ++

23+2:4 name keys-labelled

24+2:18 glyph (

25+2:19 tight name turn

26+2:24 name pairs

27+2:30 glyph |=(

28+2:33 tight glyph [

29+2:34 tight name k

30+2:36 name v

31+2:37 tight glyph ]

32+2:39 name k

33+2:40 tight glyph )

34+2:41 tight glyph )

35+3:1 NEWLINE

36+3:1 glyph ++

37+3:4 name keys

38+3:9 glyph (

39+3:10 tight name turn

40+3:15 name pairs

41+3:21 glyph (

42+3:22 tight name unface

43+3:29 glyph |=(

44+3:32 tight glyph [

45+3:33 tight name k

46+3:35 name v

47+3:36 tight glyph ]

48+3:38 name k

49+3:39 tight glyph )

50+3:40 tight glyph )

51+3:41 tight glyph )

52+3:42 NEWLINE

tests/golden/inline-unface-lambda/tree.txtnew file+28

@@ -0,0 +1,28 @@

1+(module

2+ (value 1:1 pairs

3+ (cast 1:10

4+ (apply 1:13 list

5+ (cell 1:19

6+ (face 1:20 p (aura 1:22 @t))

7+ (face 1:25 q (aura 1:27 @ud))))

8+ (list 1:33

9+ (tuple 1:35 (str 1:36 "a") (lit 1:40 1)))))

10+ (value 2:1 keys-labelled

11+ (group 2:18

12+ (call 2:19

13+ (wing 2:19 turn)

14+ (wing 2:24 pairs)

15+ (gate-wide 2:30

16+ (cell 2:33 (bind 2:34 k) (bind 2:36 v))

17+ (wing 2:39 k)))))

18+ (value 3:1 keys

19+ (group 3:9

20+ (call 3:10

21+ (wing 3:10 turn)

22+ (wing 3:15 pairs)

23+ (group 3:21

24+ (call 3:22

25+ (wing 3:22 unface)

26+ (gate-wide 3:29

27+ (cell 3:32 (bind 3:33 k) (bind 3:35 v))

28+ (wing 3:38 k))))))))

tests/golden/inline-unface-lambda/types.txtnew file+10

@@ -0,0 +1,10 @@

1+partial inference; module not checked

2+++ pairs: (list [p=@t q=@ud])

3+++ keys-labelled: call's sample and argument types do not unify

4+/tests/golden/inline-unface-lambda/source.jibb:2:19: called gate has type $-([(list A) $-(A B)] (list B))

5+++ keys-labelled (turn pairs |=([k v] k))

6+ ^

7+/tests/golden/inline-unface-lambda/source.jibb:2:30: argument has type $-([k=A v=B] A)

8+++ keys-labelled (turn pairs |=([k v] k))

9+ ^

10+++ keys: (list [p=@t])