Map unique strings to (incrementing) numbers in MongoDB

Question

Assume that I have documents with timestamp, sensor_name, and value (modelling some measurements) such as

{
  timestamp: 1,
  sensor_name: "Sensor A",
  value: 10
}
{
  timestamp: 2,
  sensor_name: "Sensor B",
  value: 11
}
{
  timestamp: 7,
  sensor_name: "Sensor A",
  value: 5
}
{
  timestamp: 10,
  sensor_name: "Sensor A",
  value: 13
}
{
  timestamp: 12,
  sensor_name: "Sensor B",
  value: 20
}

How could I map each unique sensor_name to a unique number and query it in the form

{
  timestamp: 1,
  sensor_nr: 1,
  value: 10
}
{
  timestamp: 2,
  sensor_nr: 2,
  value: 11
}
{
  timestamp: 7,
  sensor_nr: 1,
  value: 5
}
{
  timestamp: 10,
  sensor_nr: 1,
  value: 13
}
{
  timestamp: 12,
  sensor_nr: 2,
  value: 20
}

In general, I do not care if Sensor A becomes 1 and Sensor B becomes 2 or vice-versa.

The answer should be general, there could be more than 20 sensors, no "hardcoding" of possible sensor names, they may not follow a certain naming pattern.

Answer 1

I'm hoping someone provides a better solution than this - my gut feeling is that it is horribly inefficient, but it works!

db.collection.aggregate([
  {
    "$group": {
      "_id": null,
      "sensor_names": {
        "$addToSet": "$sensor_name"
      }
    }
  },
  {
    "$lookup": {
      "from": "collection",
      "pipeline": [],
      "as": "coll"
    }
  },
  {
    "$unwind": "$coll"
  },
  {
    "$set": {
      "coll.sensor_nr": {
        "$indexOfArray": [
          "$sensor_names",
          "$coll.sensor_name"
        ]
      }
    }
  },
  {
    "$replaceWith": "$coll"
  },
  {
    "$unset": [
      "_id",
      "sensor_name"
    ]
  }
])

Try it on mongoplayground.net.