June 2018 Update

Task/Pangram-checker/ATS/pangram-checker-2.ats

@@ -0,0 +1,19 @@
+fn is_pangram{n:nat}(s: string(n)): bool = loop(s, i2sz(0)) where {
+  val letters: arrayref(bool, 26) = arrayref_make_elt<bool>(i2sz(26), false)
+  fn check(): bool = loop(0) where {
+    fun loop{i:int | i >= 0 && i <= 26}(i: int(i)) =
+      if i < 26 then
+        if letters[i] then loop(i+1) else
+        false
+      else true
+  }
+  fun add{c:int}(c: char(c)): void =
+    if (c >= 'A') * (c <= 'Z') then letters[char2int1(c) - char2int1('A')] := true else
+    if (c >= 'a') * (c <= 'z') then letters[char2int1(c) - char2int1('a')] := true
+  fun loop{i:nat | i <= n}.<n-i>.(s: string(n), i: size_t(i)): bool =
+    if string_is_atend(s, i) then check() else
+    begin
+      add(s[i]);
+      loop(s, succ(i))
+    end
+}