rename unit type to unit (#697)

Closes #696.
This commit is contained in:
Brent Yorgey 2022-09-26 15:10:12 -05:00 committed by GitHub
parent cdd2966275
commit 5a01658883
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
20 changed files with 75 additions and 67 deletions

View File

@ -48,7 +48,7 @@ treeProgram =
moverProgram :: ProcessedTerm
moverProgram =
[tmQ|
let forever : cmd () -> cmd () = \c. c; forever c
let forever : cmd unit -> cmd unit = \c. c; forever c
in forever move
|]
@ -56,7 +56,7 @@ moverProgram =
circlerProgram :: ProcessedTerm
circlerProgram =
[tmQ|
let forever : cmd () -> cmd () = \c. c; forever c
let forever : cmd unit -> cmd unit = \c. c; forever c
in forever (
move;
turn right;

View File

@ -343,7 +343,7 @@
- A wild lambda. They are somewhat rare, but regrow when picked. Lambdas
are delicious when cooked into curry.
- Lambdas can also be used to create functions. For example,
- ' def thrice : cmd () -> cmd () = \c. c;c;c end'
- ' def thrice : cmd unit -> cmd unit = \c. c;c;c end'
- defines the function `thrice` which repeats a command three times.
properties: [portable, growable]
growth: [100, 200]
@ -780,7 +780,7 @@
which creates a name for an expression or command that is
available from then on, or with a `let` expression, which names an
expression or command locally within another expression.
- ' def m2 : cmd () = move; move end'
- ' def m2 : cmd unit = move; move end'
- ' let x : int = 3 in x^2 + 2*x + 1'
- The type annotations in `def` and `let` are optional.
@ -979,7 +979,7 @@
- |
`time : cmd int` returns the current time, measured in game ticks since the beginning of the game.
- |
`wait : int -> cmd ()` causes a robot to sleep for a specified amount of time (measured in game ticks).
`wait : int -> cmd unit` causes a robot to sleep for a specified amount of time (measured in game ticks).
properties: [portable]
capabilities: [time]

View File

@ -14,7 +14,7 @@ objectives:
as base {has "2048"}
} { return false }
solution: |
def makeN : int -> cmd () = \n.
def makeN : int -> cmd unit = \n.
if (n == 1)
{harvest; return ()}
{makeN (n/2); makeN (n/2); make (format n)}

View File

@ -6,9 +6,10 @@ objectives:
- |
Every command returns a value. However, some simple commands, like
`move`, do not have any meaningful
value to return. Since the unit type `()` has only one value, also
written `()`, returning this value does not convey any information.
Thus, the type of `move` is `cmd ()`.
value to return. Swarm has a special type, `unit`, with only one value,
called `()`. Since there is only one possible value of type
`unit`, returning it does not convey any information.
Thus, the type of `move` is `cmd unit`.
- |
Other commands do return a nontrivial value after executing.
For example, `grab` has type
@ -17,14 +18,18 @@ objectives:
- |
move; grab
- |
To use the result of a command later, you need the bind notation:
To use the result of a command later, you need bind notation, which
consists of a variable name and a leftwards-pointing arrow
before the command. For example:
- |
move; t <- grab; place t
- |
This can be useful, for example, if you do not care what you
grabbed and just want to move it to another cell; or if you
In the above example, the result returned by `grab` is assigned
to the variable name `t`, which can then be used later.
This could be useful, for example, if you do not care what you
grabbed and just want to move it to another cell, or if you
are not sure of the name of the thing being grabbed.
- Once you are done, do `place "Win"` to finish this challenge.
- Once you are done experimenting, do `place "Win"` to finish this challenge.
(Note, you might need to `grab` the entity you are standing on
or move to an empty cell first, since each cell can only
contain at most one entity.)

View File

@ -45,7 +45,7 @@ objectives:
- |
TIP: the two branches of an `if` must have the same type. In particular,
`if ... {grab} {}` is not
allowed, because `{grab}` has type `{cmd text}` whereas `{}` has type `{cmd ()}`.
allowed, because `{grab}` has type `{cmd text}` whereas `{}` has type `{cmd unit}`.
In this case `{grab; return ()}` has the right type.
condition: |
try {

View File

@ -11,8 +11,8 @@ objectives:
`move` and `turn` commands required. Your base has a `dictionary` device
that can be used to define new commands. For example:
- |
def m4 : cmd () = move; move; move; move end
- defines a new command `m4`, with type `cmd ()`, as four consecutive `move` commands.
def m4 : cmd unit = move; move; move; move end
- defines a new command `m4`, with type `cmd unit`, as four consecutive `move` commands.
With judicious
use of new definitions, it should be possible to complete this challenge
in just a few lines of code.

View File

@ -8,10 +8,10 @@ def forever = \c. c ; forever c end;
def ifC : cmd bool -> {cmd a} -> {cmd a} -> cmd a = \test. \then. \else.
b <- test; if b then else
end;
def while : cmd bool -> {cmd a} -> cmd () = \test. \body.
def while : cmd bool -> {cmd a} -> cmd unit = \test. \body.
ifC test {force body ; while test body} {}
end;
def giveall : robot -> text -> cmd () = \r. \thing.
def giveall : robot -> text -> cmd unit = \r. \thing.
while (has thing) {give r thing}
end;
def x4 = \c. c; c; c; c end;
@ -19,14 +19,14 @@ def m4 = x4 move end;
def x12 = \c. x4 (c;c;c) end;
def m12 = x12 move end;
def next_row = tB; m12; tL; move; tL end;
def plant_field : text -> cmd () = \thing.
def plant_field : text -> cmd unit = \thing.
log "planting";
x4 (
x12 (move; place thing; harvest);
next_row
)
end;
def harvest_field : text -> cmd () = \thing.
def harvest_field : text -> cmd unit = \thing.
x4 (
x12 (move; ifC (ishere thing) {harvest; return ()} {});
next_row

View File

@ -15,7 +15,7 @@ objectives:
function which takes an input (locally called `x`) and returns
`blah` as its output (`blah` can of course refer to `x`). For example:
- |
def x4 : cmd () -> cmd () = \c. c; c; c; c end
def x4 : cmd unit -> cmd unit = \c. c; c; c; c end
- That is, `x4` is defined as the function which takes a command, called `c`,
as input, and returns the command
`c; c; c; c` which consists of executing `c` four times.

View File

@ -11,9 +11,9 @@ objectives:
checks,
its type will be displayed in gray text at the top right of the window.
- For example, if you try typing `move`, you can see that it has
type `cmd ()`, which means that `move` is a command which
type `cmd unit`, which means that `move` is a command which
returns a value of the unit type (also written `()`).
- As another example, you can see that `turn` has type `dir -> cmd ()`,
- As another example, you can see that `turn` has type `dir -> cmd unit`,
meaning that `turn` is a function which takes a direction as input
and results in a command.
- "Here are a few more expressions for you to try (feel free to try others as well):"

View File

@ -2,12 +2,12 @@
// search, with robots spawning more robots. Fun, though not very practical
// in classic mode.
def repeat : int -> cmd () -> cmd () = \n.\c.
def repeat : int -> cmd unit -> cmd unit = \n.\c.
if (n == 0)
{}
{c ; repeat (n-1) c}
end;
def while : cmd bool -> cmd () -> cmd () = \test.\c.
def while : cmd bool -> cmd unit -> cmd unit = \test.\c.
b <- test;
if b {c ; while test c} {}
end;
@ -19,7 +19,7 @@ def getY : cmd int =
pos <- whereami;
return (snd pos);
end;
def gotoX : int -> cmd () = \tgt.
def gotoX : int -> cmd unit = \tgt.
cur <- getX;
if (cur == tgt)
{}
@ -30,7 +30,7 @@ def gotoX : int -> cmd () = \tgt.
gotoX tgt
}
end;
def gotoY : int -> cmd () = \tgt.
def gotoY : int -> cmd unit = \tgt.
cur <- getY;
if (cur == tgt)
{}
@ -41,8 +41,8 @@ def gotoY : int -> cmd () = \tgt.
gotoY tgt
}
end;
def goto : int -> int -> cmd () = \x. \y. gotoX x; gotoY y; gotoX x; gotoY y end;
def spawnfwd : {cmd ()} -> cmd () = \c.
def goto : int -> int -> cmd unit = \x. \y. gotoX x; gotoY y; gotoX x; gotoY y end;
def spawnfwd : {cmd unit} -> cmd unit = \c.
try {
move;
b <- isHere "tree";
@ -53,7 +53,7 @@ def spawnfwd : {cmd ()} -> cmd () = \c.
move
} { turn back }
end;
def clear : cmd () =
def clear : cmd unit =
grab;
repeat 4 (
spawnfwd {clear};

View File

@ -1,8 +1,8 @@
// A "cat" that wanders around randomly. Shows off use of the
// 'random' command.
let forever : cmd () -> cmd () = \c. c ; forever c in
let repeat : int -> cmd () -> cmd () =
let forever : cmd unit -> cmd unit = \c. c ; forever c in
let repeat : int -> cmd unit -> cmd unit =
\n. \c. if (n == 0) {} {c ; repeat (n-1) c} in
let randdir : cmd dir =
d <- random 4;

View File

@ -2,7 +2,7 @@ def ifC : forall a. cmd bool -> {cmd a} -> {cmd a} -> cmd a =
\test. \thn. \els. b <- test; if b thn els end
// Recursive DFS to harvest a contiguous forest
def dfs : cmd () =
def dfs : cmd unit =
ifC (ishere "tree") {
grab;
turn west;

View File

@ -1,6 +1,6 @@
// Defining simple recursive functions.
def repeat : int -> cmd () -> cmd () = \n.\c.
def repeat : int -> cmd unit -> cmd unit = \n.\c.
if (n == 0) {} {c ; repeat (n-1) c}
end

View File

@ -179,12 +179,12 @@ def index = \i.\xs.
{index (i-1) (tail xs)}
end
def for : int -> int -> (int -> cmd a) -> cmd () = \s.\e.\act.
def for : int -> int -> (int -> cmd a) -> cmd unit = \s.\e.\act.
if (s == e) {}
{act s; for (s+1) e act}
end
// for_each_i : int -> listI int -> (int * int -> cmd a) -> cmd ()
// for_each_i : int -> listI int -> (int * int -> cmd a) -> cmd unit
def for_each_i = \i.\xs.\act.
if (xs == nil) {}
{ let ht = headTail xs
@ -192,7 +192,7 @@ def for_each_i = \i.\xs.\act.
}
end
// for_each : listI int -> (int -> cmd a) -> cmd ()
// for_each : listI int -> (int -> cmd a) -> cmd unit
def for_each = \xs.\act.
for_each_i 0 xs (\i. act)
end
@ -311,4 +311,4 @@ end
def testLIST_ALL =
testLIST;
testLIST_BIG;
end
end

View File

@ -1,9 +1,9 @@
def forever : {cmd ()} -> cmd () =
def forever : {cmd unit} -> cmd unit =
\c. force c ; forever c
end
// Wander randomly forever.
def wander : cmd () =
def wander : cmd unit =
forever {
b <- random 2;
turn (if (b == 0) {left} {right});

View File

@ -81,7 +81,8 @@ reservedWords :: [Text]
reservedWords =
map (syntax . constInfo) (filter isUserFunc allConst)
++ map (dirSyntax . dirInfo) allDirs
++ [ "int"
++ [ "unit"
, "int"
, "text"
, "dir"
, "bool"
@ -203,7 +204,7 @@ parseType = makeExprParser parseTypeAtom table
parseTypeAtom :: Parser Type
parseTypeAtom =
TyUnit <$ symbol "()"
TyUnit <$ reserved "unit"
<|> TyVar <$> identifier
<|> TyInt <$ reserved "int"
<|> TyText <$ reserved "text"

View File

@ -55,7 +55,7 @@ pparens True = parens
pparens False = id
instance PrettyPrec BaseTy where
prettyPrec _ BUnit = "()"
prettyPrec _ BUnit = "unit"
prettyPrec _ BInt = "int"
prettyPrec _ BDir = "dir"
prettyPrec _ BText = "text"

View File

@ -459,43 +459,43 @@ decomposeFunTy ty = do
-- | Infer the type of a constant.
inferConst :: Const -> Polytype
inferConst c = case c of
Wait -> [tyQ| int -> cmd () |]
Noop -> [tyQ| cmd () |]
Selfdestruct -> [tyQ| cmd () |]
Move -> [tyQ| cmd () |]
Turn -> [tyQ| dir -> cmd () |]
Wait -> [tyQ| int -> cmd unit |]
Noop -> [tyQ| cmd unit |]
Selfdestruct -> [tyQ| cmd unit |]
Move -> [tyQ| cmd unit |]
Turn -> [tyQ| dir -> cmd unit |]
Grab -> [tyQ| cmd text |]
Harvest -> [tyQ| cmd text |]
Place -> [tyQ| text -> cmd () |]
Give -> [tyQ| robot -> text -> cmd () |]
Install -> [tyQ| robot -> text -> cmd () |]
Make -> [tyQ| text -> cmd () |]
Place -> [tyQ| text -> cmd unit |]
Give -> [tyQ| robot -> text -> cmd unit |]
Install -> [tyQ| robot -> text -> cmd unit |]
Make -> [tyQ| text -> cmd unit |]
Has -> [tyQ| text -> cmd bool |]
Installed -> [tyQ| text -> cmd bool |]
Count -> [tyQ| text -> cmd int |]
Reprogram -> [tyQ| robot -> {cmd a} -> cmd () |]
Reprogram -> [tyQ| robot -> {cmd a} -> cmd unit |]
Build -> [tyQ| {cmd a} -> cmd robot |]
Drill -> [tyQ| dir -> cmd () |]
Salvage -> [tyQ| cmd () |]
Say -> [tyQ| text -> cmd () |]
Drill -> [tyQ| dir -> cmd unit |]
Salvage -> [tyQ| cmd unit |]
Say -> [tyQ| text -> cmd unit |]
Listen -> [tyQ| cmd text |]
Log -> [tyQ| text -> cmd () |]
View -> [tyQ| robot -> cmd () |]
Appear -> [tyQ| text -> cmd () |]
Create -> [tyQ| text -> cmd () |]
Log -> [tyQ| text -> cmd unit |]
View -> [tyQ| robot -> cmd unit |]
Appear -> [tyQ| text -> cmd unit |]
Create -> [tyQ| text -> cmd unit |]
Time -> [tyQ| cmd int |]
Whereami -> [tyQ| cmd (int * int) |]
Blocked -> [tyQ| cmd bool |]
Scan -> [tyQ| dir -> cmd (() + text) |]
Upload -> [tyQ| robot -> cmd () |]
Scan -> [tyQ| dir -> cmd (unit + text) |]
Upload -> [tyQ| robot -> cmd unit |]
Ishere -> [tyQ| text -> cmd bool |]
Self -> [tyQ| robot |]
Parent -> [tyQ| robot |]
Base -> [tyQ| robot |]
Whoami -> [tyQ| cmd text |]
Setname -> [tyQ| text -> cmd () |]
Setname -> [tyQ| text -> cmd unit |]
Random -> [tyQ| int -> cmd int |]
Run -> [tyQ| text -> cmd () |]
Run -> [tyQ| text -> cmd unit |]
If -> [tyQ| bool -> {a} -> {a} -> a |]
Inl -> [tyQ| a -> a + b |]
Inr -> [tyQ| b -> a + b |]
@ -527,7 +527,7 @@ inferConst c = case c of
AppF -> [tyQ| (a -> b) -> a -> b |]
Swap -> [tyQ| text -> cmd text |]
Atomic -> [tyQ| cmd a -> cmd a |]
Teleport -> [tyQ| robot -> (int * int) -> cmd () |]
Teleport -> [tyQ| robot -> (int * int) -> cmd unit |]
As -> [tyQ| robot -> {cmd a} -> cmd a |]
RobotNamed -> [tyQ| text -> cmd robot |]
RobotNumbered -> [tyQ| int -> cmd robot |]

View File

@ -11,5 +11,7 @@ extra-deps:
- fused-effects-lens-1.2.0.1@sha256:675fddf183215b6f3c1f2a0823359a648756435fd1966284e61830ec28ad61fa,1466
- text-zipper-0.12@sha256:e96110598fc25e57a99ffcd8e583351af8b325b813aa5e3bd0adc627e3e02b6b,1472
- vty-5.36@sha256:dfbb78ea924ad0ef66cff4bc223918240234508c3de139b34780038dafb5fc53,20859
- criterion-1.6.0.0@sha256:76280dace017fe1fab4dae35d57992a48e70a3cfcdb2a4563923cd2502a7268c,5403
- criterion-measurement-0.2.0.0@sha256:8c6127b22a53aebc7d5a9dbf8fd870f128b93be3069fe7fed969e4c253cd9626,2121
resolver: lts-19.8

View File

@ -93,7 +93,7 @@ testLanguagePipeline =
"failure inside function call"
( process
"if true \n{} \n(move)"
"3: Can't unify {u0} and cmd ()"
"3: Can't unify {u0} and cmd unit"
)
, testCase
"parsing operators #236 - report failure on invalid operator start"
@ -159,7 +159,7 @@ testLanguagePipeline =
)
, testCase
"grabif"
(valid "def grabif : text -> cmd () = \\x. atomic (b <- ishere x; if b {grab; return ()} {}) end")
(valid "def grabif : text -> cmd unit = \\x. atomic (b <- ishere x; if b {grab; return ()} {}) end")
, testCase
"placeif"
(valid "def placeif : text -> cmd bool = \\thing. atomic (res <- scan down; if (res == inl ()) {place thing; return true} {return false}) end")