你如何循环字符串的索引？ [英] How do you loop over the indexes of a string?

问题描述

考虑：

val example = "1234567"

fn digit(c: char): int =
  case- c of
  | '0' => 0 | '1' => 1 | '2' => 2 | '3' => 3 | '4' => 4
  | '5' => 5 | '6' => 6 | '7' => 7 | '8' => 8 | '9' => 9

fn f(): int = loop(0, 0) where {
  fun loop(i: int, acc: int): int =
    if example[i] = '\000' then acc else
    loop(i + 1, acc + digit(example[i]))
}

implement main0() = () where {
  val () = println!("f: ", f())
}

这（尝试）循环遍历字符串的索引，将字符串的字符作为数字相加。我用 .foldleft 和 streamize_string_char 解决了几个类似的问题，但实际任务需要数学索引本身（即，如果i + 10处的字符为偶数数字，则它应该仅使用char，而不是使用每个字符。）

This (tries to) loop over the indices of a string, summing the characters of the string as digits. I've solved several similar problems with .foldleft and with streamize_string_char, but the actual task requires math on the indexes themselves (i.e., instead of using every char, it should only use a char if the char at i+10 is as an even-numbered digit).

实际上数学是相关的，因为它似乎强制 $ UNSAFE.cast2int ，因为 strlen的结果没有除法运算符（输入）：

Actually the math is relevant, because it seems to force $UNSAFE.cast2int, since there's no division operator for the result of strlen(input):

fn day2(): uint = loop(input, 0, 0) where {
  val len = $UNSAFE.cast2int(strlen(input))
  fn nextindex(i: int): int = (i + len/2) mod len
  fn get(i: int): char = input[i]  // <-- also broken at this point
  // this next line is just me slowly going mad
  fun loop{n:int}{i:nat | i <= n}(s: string(n), i: size_t(i), acc: uint): uint =
    if i >= len then acc else
    if s[i] = s[nextindex(i)] then loop(i+1, acc + digit(s[i])) else
    loop(i+1, acc)
}

如何在上面写上 f（）？请给我一个函数示例，它循环遍历字符串的索引并从字符串中通过索引获取字符。我再也不需要像

How should f() be written above? Please give me an example of a function that loops over the indexes of a string and fetches chars by index from the string. Again I don't need a solution like

typedef charint = (char, int)
fn day1(): int = sum where {
  val lastchar = input[strlen(input)-1]
  val res = input.foldleft(TYPE{charint})((lastchar, 0), (lam((last, sum): charint, c: char) =>
                if last = c then (c, sum + digit(c)) else (c, sum)))
  val sum = res.1
}

因为我需要根据指数测试属性。

because I need to test properties based on the indices.

编辑：

好吧我终于提出了一些类的解决方案，但看看它有多荒谬是。必须有正确和适当的ATS方式才能做到这一点。

Well I finally came up with some kind of solution, but look at how absurd it is. There must be a right and proper ATS way to do this.

#include "share/atspre_staload.hats"

val example = "1234567"

fn digit(c: char): int =
  case- c of
  | '0' => 0 | '1' => 1 | '2' => 2 | '3' => 3 | '4' => 4
  | '5' => 5 | '6' => 6 | '7' => 7 | '8' => 8 | '9' => 9

fn f(): int = loop(0, 0) where {
  fn get(i: int): char = loop(i, string2ptr(example)) where {
    fun loop(i: int, s: ptr): char =
      if i > 0 then loop(i-1, ptr0_succ<char>(s)) else
      $UNSAFE.ptr0_get<char>(s)
  }
  fun loop(i: int, acc: int): int =
    if get(i) = '\000' then acc else
    loop(i + 1, acc + digit(get(i)))
}

implement main0() = () where {
  val () = println!("f: ", f())
}

输出：

f: 28

EDIT2：

更少荒谬：

...
  val p = string2ptr(example)
  fn get(i: int): char = $UNSAFE.ptr0_get<char>(add_ptr_bsz(p, g0int2uint(i) * sizeof<char>))
...

EDIT3：

我可以再次使用 string [i]

overload + with add_ptr_bsz
fn string_get_at(str, i) = $UNSAFE.ptr0_get<charNZ>(string2ptr(str)+g0int2uint(i))
overload [] with string_get_at

这几乎是我我在前奏/ DATS / string.dats中看到的牙齿......有什么问题？

which is almost identical to what I see in prelude/DATS/string.dats ... what's the problem?

推荐答案

好的，以下实现 day2 是安全的：

Okay, the following implementation of day2 is safe:

fn
day2
(input: string): uint = let

val
[n:int]
input = g1ofg0(input)

val n0 = strlen(input)
val n0 = sz2i(n0) // int(n)

fun
nextindex
(
 i: natLt(n)
) : natLt(n) = nmod(i + n0/2, n0)

fun
loop(i: natLte(n), acc: uint): uint =
  if i >= n0 then acc else
  (
    if input[i] = input[nextindex(i)]
      then loop(i+1, acc + digit2uint(input[i]))
      else loop(i+1, acc)
  )

in
  loop(0, 0u)
end // end of [day2]

这篇关于你如何循环字符串的索引？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！