Skip to content

Commit

Permalink
Rewrite givens in new style
Browse files Browse the repository at this point in the history
  • Loading branch information
@propensive
propensive committed Jun 12, 2024
1 parent 3a14273 commit 9538dc5
Show file tree
Hide file tree
Showing 3 changed files with 113 additions and 108 deletions.
17 changes: 11 additions & 6 deletions src/core/guillotine.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,9 +35,11 @@ import java.io as ji

import language.experimental.pureFunctions

object CommandOutput extends PosixCommandOutputs
object Intelligible extends PosixCommands

erased trait CommandOutput[+ExecType <: Label, +ResultType]
erased trait Intelligible:
type Self <: Label
type Result

object Executor:
given stream: Executor[LazyList[Text]] = proc =>
Expand Down Expand Up @@ -168,6 +170,9 @@ class Process[+ExecType <: Label, ResultType](process: java.lang.Process) extend
osProcess.cpuUsage[InstantType]
catch case _: PidError => Unset


infix type into [BaseType <: { type Result }, ResultType] = BaseType { type Result = ResultType }

sealed trait Executable:
type Exec <: Label

Expand All @@ -180,11 +185,11 @@ sealed trait Executable:

fork[ResultType]().await()

def apply[ResultType]()(using erased commandOutput: CommandOutput[Exec, ResultType])
(using working: WorkingDirectory, executor: Executor[ResultType])
: ResultType binds GenericLogger raises ExecError =
def apply()(using erased intelligible: Exec is Intelligible)
(using working: WorkingDirectory, executor: Executor[intelligible.Result])
: intelligible.Result binds GenericLogger raises ExecError =

fork[ResultType]().await()
fork[intelligible.Result]().await()

def apply(command: Executable): Pipeline = command match
case Pipeline(commands*) => this match
Expand Down
202 changes: 101 additions & 101 deletions src/core/posix.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the
License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND,
License" is distributed on an ) as IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND,
either express or implied. See the License for the specific language governing permissions
and limitations under the License.
*/
Expand All @@ -21,105 +21,105 @@ import anticipation.*

import language.experimental.captureChecking

trait PosixCommandOutputs:
erased given alias: CommandOutput["alias", Text] = ###
erased given ar: CommandOutput["ar", Text] = ###
erased given at: CommandOutput["at", Text] = ###
erased given awk: CommandOutput["awk", Text] = ###
erased given basename: CommandOutput["basename", Text] = ###
erased given batch: CommandOutput["batch", Text] = ###
erased given bc: CommandOutput["bc", Text] = ###
erased given cat: CommandOutput["cat", LazyList[Text]] = ###
erased given chgrp: CommandOutput["chgrp", ExitStatus] = ###
erased given chmod: CommandOutput["chmod", ExitStatus] = ###
erased given chown: CommandOutput["chown", ExitStatus] = ###
erased given cksum: CommandOutput["cksum", Text] = ###
erased given cmp: CommandOutput["cmp", Text] = ###
erased given comm: CommandOutput["comm", Text] = ###
erased given command: CommandOutput["command", Text] = ###
erased given cp: CommandOutput["cp", ExitStatus] = ###
erased given crontab: CommandOutput["crontab", Text] = ###
erased given csplit: CommandOutput["csplit", Text] = ###
erased given cut: CommandOutput["cut", Text] = ###
erased given date: CommandOutput["date", Text] = ###
erased given dd: CommandOutput["dd", Text] = ###
erased given df: CommandOutput["df", Text] = ###
erased given diff: CommandOutput["diff", Text] = ###
erased given dirname: CommandOutput["dirname", Text] = ###
erased given du: CommandOutput["du", Text] = ###
erased given echo: CommandOutput["echo", Text] = ###
erased given ed: CommandOutput["ed", Text] = ###
erased given env: CommandOutput["env", Text] = ###
erased given expand: CommandOutput["expand", Text] = ###
erased given expr: CommandOutput["expr", Text] = ###
erased given file: CommandOutput["file", Text] = ###
erased given find: CommandOutput["find", Text] = ###
erased given fold: CommandOutput["fold", Text] = ###
erased given gencat: CommandOutput["gencat", Text] = ###
erased given getconf: CommandOutput["getconf", Text] = ###
erased given getopts: CommandOutput["getopts", Text] = ###
erased given grep: CommandOutput["grep", LazyList[Text]] = ###
erased given hash: CommandOutput["hash", Text] = ###
erased given head: CommandOutput["head", LazyList[Text]] = ###
erased given iconv: CommandOutput["iconv", Text] = ###
erased given id: CommandOutput["id", Text] = ###
erased given join: CommandOutput["join", Text] = ###
erased given kill: CommandOutput["kill", ExitStatus] = ###
erased given ln: CommandOutput["ln", ExitStatus] = ###
erased given locale: CommandOutput["locale", Text] = ###
erased given localedef: CommandOutput["localedef", Text] = ###
erased given logger: CommandOutput["logger", Text] = ###
erased given logname: CommandOutput["logname", Text] = ###
erased given lp: CommandOutput["lp", Text] = ###
erased given ls: CommandOutput["ls", LazyList[Text]] = ###
erased given m4: CommandOutput["m4", Text] = ###
erased given mailx: CommandOutput["mailx", Text] = ###
erased given man: CommandOutput["man", LazyList[Text]] = ###
erased given mesg: CommandOutput["mesg", Text] = ###
erased given mkdir: CommandOutput["mkdir", ExitStatus] = ###
erased given mkfifo: CommandOutput["mkfifo", ExitStatus] = ###
erased given mv: CommandOutput["mv", ExitStatus] = ###
erased given newgrp: CommandOutput["newgrp", ExitStatus] = ###
erased given od: CommandOutput["od", Text] = ###
erased given paste: CommandOutput["paste", Text] = ###
erased given patch: CommandOutput["patch", Text] = ###
erased given patchchk: CommandOutput["patchchk", Text] = ###
erased given pax: CommandOutput["pax", Text] = ###
erased given pr: CommandOutput["pr", Text] = ###
erased given printf: CommandOutput["printf", Text] = ###
erased given ps: CommandOutput["ps", Text] = ###
erased given pwd: CommandOutput["pwd", Text] = ###
erased given read: CommandOutput["read", Text] = ###
erased given renice: CommandOutput["renice", Text] = ###
erased given rm: CommandOutput["rm", ExitStatus] = ###
erased given rmdir: CommandOutput["rmdir", ExitStatus] = ###
erased given sed: CommandOutput["sed", LazyList[Text]] = ###
erased given sleep: CommandOutput["sleep", ExitStatus] = ###
erased given sort: CommandOutput["sort", LazyList[Text]] = ###
erased given split: CommandOutput["split", Text] = ###
erased given strings: CommandOutput["strings", LazyList[Text]] = ###
erased given stty: CommandOutput["stty", Text] = ###
erased given tabs: CommandOutput["tabs", Text] = ###
erased given tail: CommandOutput["tail", LazyList[Text]] = ###
erased given tee: CommandOutput["tee", Text] = ###
erased given test: CommandOutput["test", Text] = ###
erased given touch: CommandOutput["touch", ExitStatus] = ###
erased given tput: CommandOutput["tput", Text] = ###
erased given tr: CommandOutput["tr", Text] = ###
erased given tsort: CommandOutput["tsort", Text] = ###
erased given tty: CommandOutput["tty", Text] = ###
erased given umask: CommandOutput["umask", Text] = ###
erased given unalias: CommandOutput["unalias", Text] = ###
erased given uname: CommandOutput["uname", Text] = ###
erased given unexpand: CommandOutput["unexpand", Text] = ###
erased given uniq: CommandOutput["uniq", LazyList[Text]] = ###
erased given uudecode: CommandOutput["uudecode", Text] = ###
erased given uuencode: CommandOutput["uuencode", Text] = ###
erased given waitCommand: CommandOutput["wait", Text] = ###
erased given wc: CommandOutput["wc", Text] = ###
trait PosixCommands:
erased given ("alias" is Intelligible into Text) as alias = ###
erased given ("ar" is Intelligible into Text) as ar = ###
erased given ("at" is Intelligible into Text) as at = ###
erased given ("awk" is Intelligible into Text) as awk = ###
erased given ("basename" is Intelligible into Text) as basename = ###
erased given ("batch" is Intelligible into Text) as batch = ###
erased given ("bc" is Intelligible into Text) as bc = ###
erased given ("cat" is Intelligible into LazyList[Text]) as cat = ###
erased given ("chgrp" is Intelligible into ExitStatus) as chgrp = ###
erased given ("chmod" is Intelligible into ExitStatus) as chmod = ###
erased given ("chown" is Intelligible into ExitStatus) as chown = ###
erased given ("cksum" is Intelligible into Text) as cksum = ###
erased given ("cmp" is Intelligible into Text) as cmp = ###
erased given ("comm" is Intelligible into Text) as comm = ###
erased given ("command" is Intelligible into Text) as command = ###
erased given ("cp" is Intelligible into ExitStatus) as cp = ###
erased given ("crontab" is Intelligible into Text) as crontab = ###
erased given ("csplit" is Intelligible into Text) as csplit = ###
erased given ("cut" is Intelligible into Text) as cut = ###
erased given ("date" is Intelligible into Text) as date = ###
erased given ("dd" is Intelligible into Text) as dd = ###
erased given ("df" is Intelligible into Text) as df = ###
erased given ("diff" is Intelligible into Text) as diff = ###
erased given ("dirname" is Intelligible into Text) as dirname = ###
erased given ("du" is Intelligible into Text) as du = ###
erased given ("echo" is Intelligible into Text) as echo = ###
erased given ("ed" is Intelligible into Text) as ed = ###
erased given ("env" is Intelligible into Text) as env = ###
erased given ("expand" is Intelligible into Text) as expand = ###
erased given ("expr" is Intelligible into Text) as expr = ###
erased given ("file" is Intelligible into Text) as file = ###
erased given ("find" is Intelligible into Text) as find = ###
erased given ("fold" is Intelligible into Text) as fold = ###
erased given ("gencat" is Intelligible into Text) as gencat = ###
erased given ("getconf" is Intelligible into Text) as getconf = ###
erased given ("getopts" is Intelligible into Text) as getopts = ###
erased given ("grep" is Intelligible into LazyList[Text]) as grep = ###
erased given ("hash" is Intelligible into Text) as hash = ###
erased given ("head" is Intelligible into LazyList[Text]) as head = ###
erased given ("iconv" is Intelligible into Text) as iconv = ###
erased given ("id" is Intelligible into Text) as id = ###
erased given ("join" is Intelligible into Text) as join = ###
erased given ("kill" is Intelligible into ExitStatus) as kill = ###
erased given ("ln" is Intelligible into ExitStatus) as ln = ###
erased given ("locale" is Intelligible into Text) as locale = ###
erased given ("localedef" is Intelligible into Text) as localedef = ###
erased given ("logger" is Intelligible into Text) as logger = ###
erased given ("logname" is Intelligible into Text) as logname = ###
erased given ("lp" is Intelligible into Text) as lp = ###
erased given ("ls" is Intelligible into LazyList[Text]) as ls = ###
erased given ("m4" is Intelligible into Text) as m4 = ###
erased given ("mailx" is Intelligible into Text) as mailx = ###
erased given ("man" is Intelligible into LazyList[Text]) as man = ###
erased given ("mesg" is Intelligible into Text) as mesg = ###
erased given ("mkdir" is Intelligible into ExitStatus) as mkdir = ###
erased given ("mkfifo" is Intelligible into ExitStatus) as mkfifo = ###
erased given ("mv" is Intelligible into ExitStatus) as mv = ###
erased given ("newgrp" is Intelligible into ExitStatus) as newgrp = ###
erased given ("od" is Intelligible into Text) as od = ###
erased given ("paste" is Intelligible into Text) as paste = ###
erased given ("patch" is Intelligible into Text) as patch = ###
erased given ("patchchk" is Intelligible into Text) as patchchk = ###
erased given ("pax" is Intelligible into Text) as pax = ###
erased given ("pr" is Intelligible into Text) as pr = ###
erased given ("printf" is Intelligible into Text) as printf = ###
erased given ("ps" is Intelligible into Text) as ps = ###
erased given ("pwd" is Intelligible into Text) as pwd = ###
erased given ("read" is Intelligible into Text) as read = ###
erased given ("renice" is Intelligible into Text) as renice = ###
erased given ("rm" is Intelligible into ExitStatus) as rm = ###
erased given ("rmdir" is Intelligible into ExitStatus) as rmdir = ###
erased given ("sed" is Intelligible into LazyList[Text]) as sed = ###
erased given ("sleep" is Intelligible into ExitStatus) as sleep = ###
erased given ("sort" is Intelligible into LazyList[Text]) as sort = ###
erased given ("split" is Intelligible into Text) as split = ###
erased given ("strings" is Intelligible into LazyList[Text]) as strings = ###
erased given ("stty" is Intelligible into Text) as stty = ###
erased given ("tabs" is Intelligible into Text) as tabs = ###
erased given ("tail" is Intelligible into LazyList[Text]) as tail = ###
erased given ("tee" is Intelligible into Text) as tee = ###
erased given ("test" is Intelligible into Text) as test = ###
erased given ("touch" is Intelligible into ExitStatus) as touch = ###
erased given ("tput" is Intelligible into Text) as tput = ###
erased given ("tr" is Intelligible into Text) as tr = ###
erased given ("tsort" is Intelligible into Text) as tsort = ###
erased given ("tty" is Intelligible into Text) as tty = ###
erased given ("umask" is Intelligible into Text) as umask = ###
erased given ("unalias" is Intelligible into Text) as unalias = ###
erased given ("uname" is Intelligible into Text) as uname = ###
erased given ("unexpand" is Intelligible into Text) as unexpand = ###
erased given ("uniq" is Intelligible into LazyList[Text]) as uniq = ###
erased given ("uudecode" is Intelligible into Text) as uudecode = ###
erased given ("uuencode" is Intelligible into Text) as uuencode = ###
erased given ("wait" is Intelligible into Text) as waitCommand = ###
erased given ("wc" is Intelligible into Text) as wc = ###

erased given which[PathType](using erased PathType is SpecificPath)
: CommandOutput["which", PathType] = ###
erased given [PathType](using erased PathType is SpecificPath)
=> ("which" is Intelligible into PathType) as which = ###

erased given who: CommandOutput["who", Text] = ###
erased given write: CommandOutput["write", Text] = ###
erased given ("who" is Intelligible into Text) as who = ###
erased given ("write" is Intelligible into Text) as write = ###
2 changes: 1 addition & 1 deletion src/core/soundness+guillotine.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,5 +16,5 @@

package soundness

export guillotine.{sh, PosixCommandOutputs, CommandOutput, Executor, ProcessRef, OsProcess, Process,
export guillotine.{sh, Intelligible, Executor, ProcessRef, OsProcess, Process,
Executable, Command, Pipeline, ExecError, PidError, Parameterizable}

0 comments on commit 9538dc5

Please sign in to comment.