Revert "Avoid defining unsized platform Tasks"

This reverts commit d3732b4440.
This commit is contained in:
Anton-4 2024-08-28 16:37:01 +02:00
parent d3732b4440
commit ca7d1cb3fa
No known key found for this signature in database
GPG key ID: 0971D718C0A9B937
18 changed files with 105 additions and 109 deletions

View file

@ -5,9 +5,7 @@ import pf.PlatformTasks
# adapted from https://github.com/koka-lang/koka/blob/master/test/bench/haskell/cfold.hs
main : Task {} []
main =
{ value, isError } =
PlatformTasks.getInt
|> Task.mapErr! \_ -> crash "unreachable"
{ value, isError } = PlatformTasks.getInt!
inputResult =
if isError then
Err GetIntError
@ -21,15 +19,13 @@ main =
optimized = eval (constFolding (reassoc e))
unoptimized
|> Num.toStr
|> Str.concat " & "
|> Str.concat (Num.toStr optimized)
|> PlatformTasks.putLine
|> Task.mapErr! \_ -> crash "unreachable"
|> Num.toStr
|> Str.concat " & "
|> Str.concat (Num.toStr optimized)
|> PlatformTasks.putLine
Err GetIntError ->
PlatformTasks.putLine "Error: Failed to get Integer from stdin."
|> Task.mapErr! \_ -> crash "unreachable"
Expr : [
Add Expr Expr,

View file

@ -7,9 +7,7 @@ IO a : Task a []
main : Task {} []
main =
{ value, isError } =
PlatformTasks.getInt
|> Task.mapErr! \_ -> crash "unreachable"
{ value, isError } = PlatformTasks.getInt!
inputResult =
if isError then
Err GetIntError
@ -29,7 +27,6 @@ main =
Err GetIntError ->
PlatformTasks.putLine "Error: Failed to get Integer from stdin."
|> Task.mapErr! \_ -> crash "unreachable"
nestHelp : I64, (I64, Expr -> IO Expr), I64, Expr -> IO Expr
nestHelp = \s, f, m, x ->
@ -170,7 +167,5 @@ deriv = \i, f ->
Num.toStr (i + 1)
|> Str.concat " count: "
|> Str.concat (Num.toStr (count fprime))
PlatformTasks.putLine line
|> Task.mapErr! \_ -> crash "unreachable"
PlatformTasks.putLine! line
Task.ok fprime

View file

@ -11,4 +11,3 @@ main =
Issue2279Help.asText 42
PlatformTasks.putLine text
|> Task.mapErr! \_ -> crash "unreachable"

View file

@ -4,9 +4,7 @@ import pf.PlatformTasks
main : Task {} []
main =
{ value, isError } =
PlatformTasks.getInt
|> Task.mapErr! \_ -> crash "unreachable"
{ value, isError } = PlatformTasks.getInt!
inputResult =
if isError then
Err GetIntError
@ -16,13 +14,11 @@ main =
when inputResult is
Ok n ->
queens n # original koka 13
|> Num.toStr
|> PlatformTasks.putLine
|> Task.mapErr! \_ -> crash "unreachable"
|> Num.toStr
|> PlatformTasks.putLine
Err GetIntError ->
PlatformTasks.putLine "Error: Failed to get Integer from stdin."
|> Task.mapErr! \_ -> crash "unreachable"
ConsList a : [Nil, Cons a (ConsList a)]

View file

@ -2,8 +2,8 @@ hosted PlatformTasks
exposes [putLine, putInt, getInt]
imports []
putLine : Str -> Task {} {}
putLine : Str -> Task {} *
putInt : I64 -> Task {} {}
putInt : I64 -> Task {} *
getInt : Task { value : I64, isError : Bool } {}
getInt : Task { value : I64, isError : Bool } *

File diff suppressed because one or more lines are too long

View file

@ -39,9 +39,7 @@ fold = \f, tree, b ->
main : Task {} []
main =
{ value, isError } =
PlatformTasks.getInt
|> Task.mapErr! \_ -> crash "unreachable"
{ value, isError } = PlatformTasks.getInt!
inputResult =
if isError then
Err GetIntError
@ -59,17 +57,14 @@ main =
val = fold (\_, v, r -> if v then r + 1 else r) head 0
val
|> Num.toStr
|> PlatformTasks.putLine
|> Task.mapErr! \_ -> crash "unreachable"
|> Num.toStr
|> PlatformTasks.putLine
Nil ->
PlatformTasks.putLine "fail"
|> Task.mapErr! \_ -> crash "unreachable"
Err GetIntError ->
PlatformTasks.putLine "Error: Failed to get Integer from stdin."
|> Task.mapErr! \_ -> crash "unreachable"
insert : Tree (Num k) v, Num k, v -> Tree (Num k) v
insert = \t, k, v -> if isRed t then setBlack (ins t k v) else ins t k v

View file

@ -12,9 +12,7 @@ ConsList a : [Nil, Cons a (ConsList a)]
main : Task {} []
main =
{ value, isError } =
PlatformTasks.getInt
|> Task.mapErr! \_ -> crash "unreachable"
{ value, isError } = PlatformTasks.getInt!
inputResult =
if isError then
Err GetIntError
@ -27,13 +25,11 @@ main =
val = fold (\_, v, r -> if v then r + 1 else r) m 0
val
|> Num.toStr
|> PlatformTasks.putLine
|> Task.mapErr! \_ -> crash "unreachable"
|> Num.toStr
|> PlatformTasks.putLine
Err GetIntError ->
PlatformTasks.putLine "Error: Failed to get Integer from stdin."
|> Task.mapErr! \_ -> crash "unreachable"
boom : Str -> a
boom = \_ -> boom ""

View file

@ -8,9 +8,8 @@ main =
tree = insert 0 {} Empty
tree
|> show
|> PlatformTasks.putLine
|> Task.mapErr! \_ -> crash "unreachable"
|> show
|> PlatformTasks.putLine
show : RedBlackTree I64 {} -> Str
show = \tree -> showRBTree tree Num.toStr (\{} -> "{}")

View file

@ -5,8 +5,7 @@ import AStar
main : Task {} []
main =
PlatformTasks.putLine (showBool test1)
|> Task.mapErr! \_ -> crash "unreachable"
PlatformTasks.putLine! (showBool test1)
showBool : Bool -> Str
showBool = \b ->

View file

@ -8,19 +8,10 @@ IO a : Task a []
main : IO {}
main =
when Base64.fromBytes (Str.toUtf8 "Hello World") is
Err _ ->
PlatformTasks.putLine "sadness"
|> Task.mapErr! \_ -> crash "unreachable"
Err _ -> PlatformTasks.putLine "sadness"
Ok encoded ->
PlatformTasks.putLine (Str.concat "encoded: " encoded)
|> Task.mapErr! \_ -> crash "unreachable"
PlatformTasks.putLine! (Str.concat "encoded: " encoded)
when Base64.toStr encoded is
Ok decoded ->
PlatformTasks.putLine (Str.concat "decoded: " decoded)
|> Task.mapErr! \_ -> crash "unreachable"
Err _ ->
PlatformTasks.putLine "sadness"
|> Task.mapErr! \_ -> crash "unreachable"
Ok decoded -> PlatformTasks.putLine (Str.concat "decoded: " decoded)
Err _ -> PlatformTasks.putLine "sadness"