halt command (#1256)

Closes #392 .  Adds a command `halt : actor -> cmd unit` which halts the given robot if it is within a distance of 1 (no distance limit for system robots or in creative mode).  `halt self` works too.  Privileged robots (i.e. system robots, or when in creative mode) can halt any other robot.  Unprivileged robots cannot halt system robots.

data/entities.yaml

@@ -1293,3 +1293,19 @@
     example `key "Down"` or `key "C-S-x"`.
   properties: [portable]
   capabilities: [handleinput]
+
+- name: halting oracle
+  display:
+    attr: device
+    char: '?'
+  description:
+  - A device to solve the halting problem. When asked if a
+    particular robot program will halt, it always answers YES.
+    And it is always correct... or else!
+  - |
+    Enables the command `halt : actor -> cmd unit` which takes
+    a robot as an argument and, if it is up to one cell away,
+    cancels its currently running program (if any).  In creative mode,
+    there is no distance limitation.
+  properties: [portable]
+  capabilities: [halt]

data/recipes.yaml

@@ -840,3 +840,10 @@
   - [16, key]
   out:
   - [1, keyboard]
+
+- in:
+  - [1, branch predictor]
+  - [1, grabber]
+  - [1, toolkit]
+  out:
+  - [1, halting oracle]

data/scenarios/Testing/00-ORDER.txt

@@ -32,4 +32,5 @@
 1171-resonate-command.yaml
 1207-scout-command.yaml
 1218-stride-command.yaml
-1234-push-command.yaml
+1234-push-command.yaml
+1256-halt-command.yaml

data/scenarios/Testing/1256-halt-command.yaml

@@ -0,0 +1,57 @@
+version: 1
+name: Halting test
+creative: false
+description: Stop a robot using halt
+objectives:
+  - goal:
+      - The robot next to you is holding a flower, but is stuck in an
+        infinite loop.  Get the flower!
+    condition: |
+      as base {has "flower"}
+solution: |
+  mr <- meet;
+  case mr (\_. return ()) (\r. halt r; turn west; move; salvage )
+robots:
+  - name: base
+    dir: [0,-1]
+    display:
+      char: Ω
+      attr: robot
+    devices:
+      - compass
+      - dictionary
+      - grabber
+      - toolkit
+      - logger
+      - tank treads
+      - antenna
+      - ADT calculator
+      - halting oracle
+  - name: infinitebot
+    dir: [0,1]
+    display:
+      invisible: false
+    devices:
+      - strange loop
+      - dictionary
+      - treads
+    inventory:
+      - [1, flower]
+    program: |
+      def forever = \c. c ; forever c end;
+      forever ( turn right )
+world:
+  default: [blank]
+  palette:
+    'Ω': [grass, null, base]
+    '^': [grass, null, infinitebot]
+    '.': [grass]
+  upperleft: [0, 0]
+  map: |
+   .........
+   .........
+   .........
+   ...^Ω....
+   .........
+   .........
+   .........

editors/emacs/swarm-mode.el

@@ -77,6 +77,7 @@
                "view"
                "appear"
                "create"
+               "halt"
                "time"
                "scout"
                "whereami"

editors/vscode/syntaxes/swarm.tmLanguage.json

@@ -58,7 +58,7 @@
 				},
 				{
 				"name": "keyword.other",
-				"match": "\\b(?i)(self|parent|base|if|inl|inr|case|fst|snd|force|undefined|fail|not|format|chars|split|charat|tochar|key|noop|wait|selfdestruct|move|push|stride|turn|grab|harvest|place|give|equip|unequip|make|has|equipped|count|drill|build|salvage|reprogram|say|listen|log|view|appear|create|time|scout|whereami|detect|resonate|sniff|chirp|watch|surveil|heading|blocked|scan|upload|ishere|isempty|meet|meetall|whoami|setname|random|run|return|try|swap|atomic|instant|installkeyhandler|teleport|as|robotnamed|robotnumbered|knows)\\b"
+				"match": "\\b(?i)(self|parent|base|if|inl|inr|case|fst|snd|force|undefined|fail|not|format|chars|split|charat|tochar|key|noop|wait|selfdestruct|move|push|stride|turn|grab|harvest|place|give|equip|unequip|make|has|equipped|count|drill|build|salvage|reprogram|say|listen|log|view|appear|create|halt|time|scout|whereami|detect|resonate|sniff|chirp|watch|surveil|heading|blocked|scan|upload|ishere|isempty|meet|meetall|whoami|setname|random|run|return|try|swap|atomic|instant|installkeyhandler|teleport|as|robotnamed|robotnumbered|knows)\\b"
 				}
 			]
 			},

src/Swarm/Game/Step.hs

@@ -1682,6 +1682,31 @@ execConst c vs s k = do
 
         return $ Out VUnit s k
       _ -> badConst
+    Halt -> case vs of
+      [VRobot targetID] -> do
+        myID <- use robotID
+        case myID == targetID of
+          -- To halt ourselves, just return a cancelled CESK machine.
+          -- It will be reinstalled as our current machine; then,
+          -- based on the fact that our CESK machine is done we will
+          -- be put to sleep and the REPL will be reset if we are the
+          -- base robot.
+          True -> return $ cancel $ Out VUnit s k
+          False -> do
+            -- Make sure the other robot exists and is close enough.
+            target <- getRobotWithinTouch targetID
+            -- Make sure either we are privileged, OR the target robot
+            -- is NOT.  In other words unprivileged bots should not be
+            -- able to halt privileged ones.
+            omni <- isPrivilegedBot
+            case omni || not (target ^. systemRobot) of
+              True -> do
+                -- Cancel its CESK machine, and put it to sleep.
+                robotMap . at targetID . _Just . machine %= cancel
+                sleepForever targetID
+                return $ Out VUnit s k
+              False -> throwError $ cmdExn c ["You are not authorized to halt that robot."]
+      _ -> badConst
     Ishere -> case vs of
       [VText name] -> do
         loc <- use robotLocation

src/Swarm/Language/Capability.hs

@@ -151,6 +151,8 @@ data Capability
     CDebug
   | -- | Capability to handle keyboard input.
     CHandleinput
+  | -- | Capability to make other robots halt.
+    CHalt
   | -- | God-like capabilities.  For e.g. commands intended only for
     --   checking challenge mode win conditions, and not for use by
     --   players.
@@ -245,6 +247,7 @@ constCaps = \case
   Heading -> Just COrient
   Key -> Just CHandleinput
   InstallKeyHandler -> Just CHandleinput
+  Halt -> Just CHalt
   -- ----------------------------------------------------------------
   -- Text operations
   Format -> Just CText

src/Swarm/Language/Syntax.hs

@@ -257,6 +257,8 @@ data Const
   | -- | Create an entity out of thin air. Only
     --   available in creative mode.
     Create
+  | -- | Tell a robot to halt.
+    Halt
   | -- Sensing / generation
 
     -- | Get current time
@@ -644,6 +646,7 @@ constInfo c = case c of
   Create ->
     command 1 short . doc "Create an item out of thin air." $
       ["Only available in creative mode."]
+  Halt -> command 1 short "Tell a robot to halt."
   Time -> command 0 Intangible "Get the current time."
   Scout ->
     command 1 short . doc "Detect whether a robot is within line-of-sight in a direction." $

src/Swarm/Language/Typecheck.hs

@@ -578,6 +578,7 @@ inferConst c = case c of
   View -> [tyQ| actor -> cmd unit |]
   Appear -> [tyQ| text -> cmd unit |]
   Create -> [tyQ| text -> cmd unit |]
+  Halt -> [tyQ| actor -> cmd unit |]
   Time -> [tyQ| cmd int |]
   Scout -> [tyQ| dir -> cmd bool |]
   Whereami -> [tyQ| cmd (int * int) |]

test/integration/Main.hs

@@ -275,6 +275,7 @@ testScenarioSolution _ci _em =
         , testSolution Default "Testing/1207-scout-command"
         , testSolution Default "Testing/1218-stride-command"
         , testSolution Default "Testing/1234-push-command"
+        , testSolution Default "Testing/1256-halt-command"
         ]
     ]
  where