Check a Unison type witness's typeLinks against its constructors' indices, and a hand-kept list of a GADT's constructors, through ucm transcript.fork

unison-witness.nu

#!/usr/bin/env nu

# Checks a Unison type witness against the function that links its types,
# and optionally a hand-kept list of a GADT's constructors against the GADT.
#
# A witness is a GADT with one constructor per type, each fixing its index:
#
#     type Stored a where
#       SubmissionS : Stored Submission
#       AccountS : Stored Account
#
# and a function pairs each constructor with that type's link:
#
#     Stored.link : Stored a -> Link.Type
#     Stored.link = cases
#       SubmissionS -> typeLink Submission
#       AccountS -> typeLink Account
#
# The compiler checks every use of a witness against its index, but not the
# links: `typeLink` is a value, and `SubmissionS -> typeLink Account`
# compiles. A unit test could repeat the expected links, but that is another
# hand-written mapping to keep up to date. Instead, this asks UCM to `view`
# the two definitions and compares each arm's `typeLink` with its
# constructor's declared index, as text: both are printed with the same
# names.
#
# It checks a source form, not what the function computes, so each arm must
# return its link directly:
#
#     SubmissionS -> typeLink Submission
#
# or, with `--wrapper StoredType.StoredType`, inside that one data
# constructor, with any string literals around exactly one `typeLink` (a
# first string literal must name the same type, fully or by a suffix):
#
#     SubmissionS -> StoredType "Submission" (typeLink Submission)
#
# The wrapper is asked of UCM, and must be a data constructor: a function
# there could ignore the link it is given. An arm in any other shape - an
# `if`, a `match`, a helper call, two links - is rejected rather than
# guessed at.
#
# `--tables` and `--list` check a second thing the compiler leaves alone: a
# hand-kept list of a GADT's constructors, wrapped to hide their indices,
#
#     type Table k v where
#       Submissions : Table SubmissionId Submission
#       Accounts : Table AccountId Account
#
#     Table.all : [SomeTable]
#     Table.all = [SomeTable Submissions, SomeTable Accounts]
#
# Unison checks that a `match` covers every constructor, but cannot list a
# type's constructors as values, so a constructor left out of the list
# compiles. This fails on one left out, an entry that names none, and one
# listed twice.
#
#     nu unison-witness.nu @me/myapp/main myapp.db.Stored myapp.db.Stored.link
#     nu unison-witness.nu @me/myapp/main myapp.db.Stored myapp.db.Stored.link \
#       --tables myapp.db.Table --list myapp.db.Table.all --load scratch.u
#     nu unison-witness.nu @me/myapp/main myapp.db.Stored myapp.db.Stored.describe \
#       --wrapper StoredType.StoredType
#
# It runs `ucm transcript.fork`, which works on a copy of the codebase, so it
# needs no lock and can run while UCM is open. `--load` loads and updates a
# scratch file in the fork first, so a change can be checked before it is
# applied. A transcript that fails - a scratch file that does not typecheck,
# a name that does not exist - fails the check before anything is read from
# it. Exits 1 on any disagreement, or on anything it cannot read, so a check
# that read nothing cannot pass.
#
# In AlygnApp, `cargo xtask release` runs it on the service's table
# witnesses and table list (crates/xtask/src/unison_witness.rs), and
# `nu scripts/unison-witness.nu self-test` runs its tests, which an xtask
# unit test runs with the rest (crates/xtask/src/nu_scripts.rs).

use std/assert

# Every run of whitespace made one space, so a signature or an arm the
# printer wrapped reads as one line.
export def flatten-answer []: string -> string {
    str replace --all --regex '\s+' ' '
}

# The text between `start` and the first of `ends` after it, or null when
# there is no `start`.
def between [start: string, ends: list<string>]: string -> any {
    let text = $in
    let from = $text | str index-of $start
    if $from < 0 { return null }
    let rest = $text | str substring ($from + ($start | str length))..
    let cuts = $ends | each {|end| $rest | str index-of $end } | where {|at| $at >= 0 }
    if ($cuts | is-empty) { $rest } else { $rest | str substring ..<($cuts | math min) }
}

# A dotted name with its dots escaped for a regex.
def escaped []: string -> string { str replace --all "." '\.' }

# Whether `printed` names `index`: the same name, or one ending in the other
# at a namespace boundary (`myapp.coach.Submission` for `coach.Submission`,
# or `Submission` for `coach.Submission`).
export def names-type [printed: string, index: string]: nothing -> bool {
    let ends = {|longer, shorter| $longer == $shorter or ($longer | str ends-with $".($shorter)") }
    (do $ends $printed $index) or (do $ends $index $printed)
}

# Each constructor of `witness` and the type its index fixes, read from the
# flattened answer.
export def witness-constructors [witness: string, links: string, prompt: string]: string -> record {
    let flat = $in
    let short = $witness | split row "." | last
    let declaration = $flat | between $"type ($witness) a where " ["{{" $"($links) :" $prompt "```"]
    if $declaration == null {
        return {constructors: [], problems: [$"UCM printed no `type ($witness) a where` declaration"]}
    }
    let constructors = $declaration
        | parse --regex ('(?<name>\w+) : (?:[\w.]*\.)?' + ($short | escaped) + ' (?<index>[\w.]+)')
    if ($constructors | is-empty) {
        {constructors: [], problems: [$"read no constructors of ($witness)"]}
    } else {
        {constructors: $constructors, problems: []}
    }
}

# Each arm of `links`: its constructor, its first string literal (or null)
# and the type its one `typeLink` names. An arm in another shape is a
# problem, not an arm.
export def link-arms [links: string, prompt: string, wrapper?: string]: string -> record {
    let flat = $in
    let body = $flat | between $"($links) = cases " ["```" $prompt]
    if $body == null { return {arms: [], problems: [$"UCM printed no `($links) = cases`"]} }
    let pairs = $body | split row " -> " | window 2
    let count = $pairs | length
    let read = $pairs | enumerate | each {|at|
        let constructor = $at.item.0 | split row " " | last | split row "." | last
        # Each arm's text runs on to the next arm's constructor; drop it.
        let words = $at.item.1 | str trim | split row " "
        let rhs = if $at.index < ($count - 1) { $words | drop 1 | str join " " } else { $words | str join " " }
        let direct = $rhs | parse --regex '^typeLink (?<link>[\w.]+)$'
        let wrapped = if $wrapper == null { [] } else {
            let named = $wrapper | split row "." | last | escaped
            $rhs | parse --regex ('^(?:[\w.]*\.)?' + $named + '(?<strings>(?: "[^"]*")*) \(typeLink (?<link>[\w.]+)\)(?: "[^"]*")*$')
        }
        if ($direct | length) == 1 {
            {arm: {constructor: $constructor, printed: null, link: $direct.0.link}}
        } else if ($wrapped | length) == 1 {
            let printed = $wrapped.0.strings | parse --regex '"(?<text>[^"]*)"' | get text | first 1
            {arm: {constructor: $constructor, printed: ($printed | get 0?), link: $wrapped.0.link}}
        } else {
            let shapes = if $wrapper == null { "`C -> typeLink T`" } else { $"`C -> typeLink T`, or `C -> ($wrapper | split row '.' | last) \"name\" \(typeLink T\)`" }
            {problem: $"the arm for `($constructor)` is not one of the supported shapes \(($shapes)\): ($rhs)"}
        }
    }
    {
        arms: ($read | where {|row| 'arm' in $row } | get arm)
        problems: ($read | where {|row| 'problem' in $row } | get problem)
    }
}

# Every disagreement between the witness's constructors and the arms.
export def link-mismatches [constructors: list, arms: list, links: string]: nothing -> list<string> {
    let wrong = $arms | each {|arm|
        let match = $constructors | where name == $arm.constructor
        if ($match | is-empty) {
            $"`($arm.constructor)` has an arm in ($links) but is not a constructor"
        } else if $match.0.index != $arm.link {
            $"`($arm.constructor)` stands for `($match.0.index)`, but ($links) links `($arm.link)`"
        } else if $arm.printed != null and not (names-type $arm.printed $match.0.index) {
            $"`($arm.constructor)` stands for `($match.0.index)`, but ($links) prints it as \"($arm.printed)\""
        }
    } | compact
    let missing = $constructors
        | where {|constructor| $constructor.name not-in ($arms | get constructor) }
        | each {|constructor| $"`($constructor.name)` has no arm in ($links)" }
    $wrong | append $missing
}

# Every constructor of `tables` the list leaves out, every entry naming
# none, and every constructor listed twice. Reads either way UCM prints a
# list: one entry a line (`[ SomeTable A , SomeTable B ]` once flattened)
# or, for a short one, on one line (`[SomeTable A, SomeTable B]`).
export def list-problems [tables: string, list: string, prompt: string]: string -> record {
    let flat = $in
    let short = $tables | split row "." | last
    let declared_at = $flat | parse --regex ('type ' + ($tables | escaped) + '(?: \w+)* where (?<body>.*)')
    if ($declared_at | is-empty) {
        return {tables: 0, problems: [$"UCM printed no `type ($tables) ... where` declaration"]}
    }
    let declaration = $declared_at.0.body | between "" [$"($list) :" $prompt "{{" "```"]
    let declared = $declaration | parse --regex ('(?<name>\w+) : (?:[\w.]*\.)?' + ($short | escaped) + ' ') | get name
    if ($declared | is-empty) { return {tables: 0, problems: [$"read no constructors of ($tables)"]} }
    let listed = $flat | between $"($list) = [" ["]"]
    if $listed == null { return {tables: ($declared | length), problems: [$"UCM printed no `($list) = [ ... ]`"]} }
    let entries = $listed | split row "," | each {|entry| $entry | str trim | split row " " | last | split row "." | last }
    let left_out = $declared | where {|name| $name not-in $entries }
        | each {|name| $"`($name)` is a constructor of ($tables), but ($list) leaves it out" }
    let unknown = $entries | where {|entry| $entry not-in $declared }
        | each {|entry| $"($list) lists `($entry)`, which is not a constructor of ($tables)" }
    let twice = $declared | where {|name| ($entries | where {|entry| $entry == $name } | length) > 1 }
        | each {|name| $"($list) lists `($name)` more than once" }
    {tables: ($declared | length), problems: ($left_out | append $unknown | append $twice)}
}

# Whether UCM's `names` answer for `wrapper` shows a data constructor: a
# term whose hash carries a constructor index (`#abc#0`). A function's
# hash has none, and a function could ignore the link it is given.
export def wrapper-problems [wrapper: string, prompt: string]: string -> list<string> {
    let flat = $in
    let answer = $flat | between $"($prompt) names ($wrapper) " [$prompt "```"]
    if $answer == null { return [$"UCM printed no `names` answer for ($wrapper)"] }
    if ($answer | parse --regex '#\w+#\d+ Term ' | is-empty) {
        [$"`($wrapper)` is not a data constructor, so an arm wrapping a link in it is not checked: ($answer | str trim)"]
    } else { [] }
}

# The whole check over one transcript answer: how many types and tables it
# read, and every problem it found.
export def check-answer [
    answer: string
    project_branch: string
    witness: string
    links: string
    tables?: string
    list?: string
    wrapper?: string
]: nothing -> record {
    let prompt = $"($project_branch)>"
    let flat = $answer | flatten-answer
    let read = $flat | witness-constructors $witness $links $prompt
    let arms = $flat | link-arms $links $prompt $wrapper
    let wrapping = if $wrapper == null { [] } else { $flat | wrapper-problems $wrapper $prompt }
    let listing = if $tables == null { {tables: 0, problems: []} } else { $flat | list-problems $tables $list $prompt }
    let mismatches = if ($read.problems | is-empty) and ($arms.problems | is-empty) {
        link-mismatches $read.constructors $arms.arms $links
    } else { [] }
    {
        types: ($read.constructors | length)
        tables: $listing.tables
        problems: ($wrapping | append $read.problems | append $arms.problems | append $mismatches | append $listing.problems)
    }
}

def main [
    project_branch: string # the project and branch, e.g. @me/myapp/main
    witness: string        # the witness type, fully qualified
    links: string          # the function from the witness to links, fully qualified
    --codebase: path       # the directory holding .unison (default: your home)
    --load: path           # a scratch file to load and update in the fork first
    --tables: string       # a GADT whose constructors `--list` must list, fully qualified
    --list: string         # the hand-kept list of its constructors, fully qualified
    --wrapper: string      # a data constructor an arm may wrap its link in, as UCM names it
] {
    if ($tables == null) != ($list == null) {
        print -e "--tables and --list go together"
        exit 1
    }
    let dir = mktemp -d
    let script = $dir | path join "witness.md"
    let loaded = if $load == null { "" } else {
        $"($project_branch)> load ($load | path expand)\n($project_branch)> update\n"
    }
    let listing = if $tables == null { "" } else { $"($project_branch)> view ($tables) ($list)\n" }
    let naming = if $wrapper == null { "" } else { $"($project_branch)> names ($wrapper)\n" }
    $"```ucm\n($loaded)($project_branch)> view ($witness) ($links)\n($listing)($naming)```\n" | save $script
    let codebase = $codebase | default $nu.home-dir
    let ran = do { cd $dir; ^ucm --codebase $codebase transcript.fork $script } | complete
    let answer_file = $dir | path join "witness.output.md"
    # A failed `load` or `update` would leave the `view`s reading what the
    # codebase already held, so a failed transcript is never parsed.
    if $ran.exit_code != 0 or not ($answer_file | path exists) {
        rm -rf $dir
        print -e $"the transcript failed \(exit ($ran.exit_code)\):\n($ran.stdout | lines | last 12 | str join "\n")"
        exit 1
    }
    let answer = open --raw $answer_file
    rm -rf $dir
    let result = check-answer $answer $project_branch $witness $links $tables $list $wrapper
    if ($result.problems | is-empty) {
        print $"($result.types) types: every arm of ($links) links its constructor's own type"
        if $tables != null { print $"($result.tables) constructors of ($tables): ($list) lists each once" }
    } else {
        print -e ($result.problems | str join "\n")
        exit 1
    }
}

# The script's tests, over answers shaped as UCM prints them.
def "main self-test" [] {
    let prompt = "@me/myapp/main>"
    let viewed = '@me/myapp/main> view myapp.db.Stored myapp.db.Stored.describe

  {{
  A witness of each type a table stores.
  }}
  type myapp.db.Stored a where
    SubmissionAt_2_5_0S :
      db.Stored schema_2_5_0.Submission
    SubmissionS : db.Stored coach.Submission
    TextS : db.Stored Text

  myapp.db.Stored.describe : db.Stored a -> StoredType
  myapp.db.Stored.describe = cases
    SubmissionAt_2_5_0S ->
      StoredType
        "myapp.legacy.schema_2_5_0.Submission"
        (typeLink schema_2_5_0.Submission)
    SubmissionS ->
      StoredType "Submission" (typeLink coach.Submission)
    TextS -> StoredType "Text" (typeLink Text)
'
    let tables = '@me/myapp/main> view myapp.db.Table myapp.db.Table.all

  type myapp.db.Table k v where
    Submissions : db.Table SubmissionId coach.Submission
    SubmissionsAt_2_5_0 :
      db.Table SubmissionId schema_2_5_0.Submission
    Notes :
      db.Table
        NoteId
        Note

  myapp.db.Table.all : [SomeTable]
  myapp.db.Table.all =
    [ SomeTable Submissions
    , SomeTable Notes
    , SomeTable SubmissionsAt_2_5_0
    ]
```
'
    let named = '@me/myapp/main> names StoredType.StoredType

  Hash            Kind   Names
  #puvp0d9mtd#0   Term   lib.store.StoredType.StoredType
```
'
    let answer = "``` ucm\n" + $viewed + "\n" + ($tables | str replace "```\n" "") + $named
    let check = {|text| check-answer $text "@me/myapp/main" myapp.db.Stored myapp.db.Stored.describe myapp.db.Table myapp.db.Table.all StoredType.StoredType }

    # The answer as printed passes, through the printer's wrapping.
    let passed = do $check $answer
    assert equal $passed {types: 3, tables: 3, problems: []}

    # A link to another type, and a printed name of another type, are named.
    let swapped = $answer | str replace '"Submission" (typeLink coach.Submission)' '"Submission" (typeLink schema_2_5_0.Submission)'
    assert equal (do $check $swapped).problems ["`SubmissionS` stands for `coach.Submission`, but myapp.db.Stored.describe links `schema_2_5_0.Submission`"]
    let misnamed = $answer | str replace 'StoredType "Text"' 'StoredType "Nat"'
    assert equal (do $check $misnamed).problems ["`TextS` stands for `Text`, but myapp.db.Stored.describe prints it as \"Nat\""]
    assert (names-type "Submission" "coach.Submission")
    assert not (names-type "OldSubmission" "coach.Submission")

    # A constructor with no arm is named.
    let short = $answer | str replace "    TextS -> StoredType \"Text\" (typeLink Text)\n" ""
    assert equal (do $check $short).problems ["`TextS` has no arm in myapp.db.Stored.describe"]

    # An arm in another shape is rejected, never read: two links, an `if`,
    # or anything after the link.
    for odd in [
        'TextS -> if true then typeLink Nat else typeLink Text'
        'TextS -> StoredType "Text" (typeLink Text) |> withLink (typeLink Nat)'
        'TextS -> describeText'
        'TextS -> replaceLink (typeLink Text)'
    ] {
        let found = (do $check ($answer | str replace 'TextS -> StoredType "Text" (typeLink Text)' $odd)).problems
        assert equal ($found | length) 1
        assert str contains $found.0 "is not one of the supported shapes"
    }

    # A bare `typeLink` arm reads too.
    let bare = $answer | str replace 'TextS -> StoredType "Text" (typeLink Text)' 'TextS -> typeLink Text'
    assert equal (do $check $bare).problems []

    # A table left out of the list, and one listed twice, are named.
    let missing = $answer | str replace "    , SomeTable Notes\n" ""
    assert equal (do $check $missing).problems ["`Notes` is a constructor of myapp.db.Table, but myapp.db.Table.all leaves it out"]
    let twice = $answer | str replace "    , SomeTable Notes\n" "    , SomeTable Notes\n    , SomeTable Notes\n"
    assert equal (do $check $twice).problems ["myapp.db.Table.all lists `Notes` more than once"]

    # A list short enough for one line reads the same.
    let one_line = $answer | str replace "    [ SomeTable Submissions\n    , SomeTable Notes\n    , SomeTable SubmissionsAt_2_5_0\n    ]" "    [SomeTable Submissions, SomeTable Notes, SomeTable SubmissionsAt_2_5_0]"
    assert not ($one_line == $answer)
    assert equal (do $check $one_line) {types: 3, tables: 3, problems: []}

    # Without `--wrapper`, only bare arms are accepted.
    let unwrapped = check-answer $answer "@me/myapp/main" myapp.db.Stored myapp.db.Stored.describe
    assert equal ($unwrapped.problems | length) 3
    assert str contains $unwrapped.problems.0 "(`C -> typeLink T`)"

    # A wrapper that is a function, not a data constructor, is named.
    let helper = $answer | str replace '#puvp0d9mtd#0   Term' '#fbp9g5a18i     Term'
    assert str contains (do $check $helper).problems.0 "is not a data constructor"

    # An answer without the definitions is a problem, not a pass.
    assert equal ((check-answer "``` ucm\n```\n" "@me/myapp/main" myapp.db.Stored myapp.db.Stored.describe).problems | length) 2

    print "unison-witness.nu: self-test passed"
}