diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md new file mode 100644 index 0000000..c603a7f --- /dev/null +++ b/.github/copilot-instructions.md @@ -0,0 +1,43 @@ +# Copilot Instructions for the Diff Repository + +Before starting a task, check if you have ghc 9.14.1 available in the PATH. +If no, install it. + +## Build & Test Commands + +```bash +# Build the library (no LiquidHaskell) + +cabal build + +# Build the library with LiquidHaskell to run the static checks +# (requires ghc 9.14.1) +cd Diff-liquidhaskell && cabal build + +# Run the QuickCheck test suite +cabal test + +# Run benchmarks +cabal bench +``` + +## Repository Architecture + +### Two-package structure + +| Package | Cabal file | Purpose | +|---------|-----------|---------| +| `Diff` | `Diff.cabal` | The library itself — no LH dependency. | +| `Diff-liquidhaskell` | `Diff-liquidhaskell/Diff-liquidhaskell.cabal` | Shares `Diff`'s source tree (`src/`) to compile its modules with the LH GHC plugin enabled.| + +The `Diff-liquidhaskell` package exists to break the cyclic dependency +`Diff → liquidhaskell → liquidhaskell-boot → Diff`. +Source changes live in `src/`; the `Diff-liquidhaskell/` directory only has cabal metadata. + +### Source modules + +- `Data.Algorithm.Diff` — core Myers O(ND) diff algorithm and public API. +- `Data.Algorithm.DiffOutput` — pretty-printing utilities for regular `diff` output. +- `Data.Algorithm.DiffContext` — pretty-printing utilities for `diff -u` like output. +- `Internal.LiftedFunctions` — not always present depending on current git checkout: + utility functions used exclusively in LH logic (lifted using `reflect` or `measure` LH directives). diff --git a/.github/skills/haskell-toolchain/SKILL.md b/.github/skills/haskell-toolchain/SKILL.md new file mode 100644 index 0000000..321176a --- /dev/null +++ b/.github/skills/haskell-toolchain/SKILL.md @@ -0,0 +1,114 @@ +--- +name: haskell-toolchain +description: > + Install a specific version of GHC, cabal-install, and stack using ghcup, + plus a recent z3 binary from GitHub. Use this skill + whenever the user needs to set up or reproduce a Haskell build environment + in a container: version-pinned toolchains, CI images, LiquidHaskell setups, + or any task that starts with "install GHC". +compatibility: + os: Ubuntu 22.04 / 24.04 (Debian-based), x86_64 + network: downloads.haskell.org, hackage.haskell.org, github.com must be reachable +--- + +# Haskell Toolchain + +## 1. System prerequisites + +```bash +apt-get update -qq +apt-get install -y --no-install-recommends \ + curl ca-certificates \ + build-essential \ + libgmp-dev libffi-dev zlib1g-dev \ + libnuma-dev \ + pkg-config +``` + +`libnuma-dev` is required by some GHC bindists; omitting it causes a silent +link failure. + +## 2. Install ghcup (non-interactive) + +```bash +export BOOTSTRAP_HASKELL_NONINTERACTIVE=1 +export BOOTSTRAP_HASKELL_NO_UPGRADE=1 +# Do not install any default GHC/cabal yet — we pin versions below +export BOOTSTRAP_HASKELL_INSTALL_NO_STACK=1 +export GHCUP_INSTALL_BASE_PREFIX=/usr/local + +curl -sSf https://get-ghcup.haskell.org | sh + +# Make ghcup and installed tools available in the current shell +source /usr/local/.ghcup/env +# For subsequent RUN layers in a Dockerfile, persist it: +echo 'source /usr/local/.ghcup/env' >> /etc/profile.d/ghcup.sh +``` + +`BOOTSTRAP_HASKELL_NONINTERACTIVE=1` suppresses all prompts. +`GHCUP_INSTALL_BASE_PREFIX=/usr/local` installs system-wide rather than into +`~/.ghcup`. + +## 3. Install specific tool versions + +Replace the version strings with whatever the project requires. + +```bash +# Discover available versions if needed: +# ghcup list --tool ghc +# ghcup list --tool cabal +# ghcup list --tool stack + +GHC_VERSION=9.6.6 +CABAL_VERSION=3.10.3.0 +STACK_VERSION=2.15.7 + +ghcup install ghc $GHC_VERSION && ghcup set ghc $GHC_VERSION +ghcup install cabal $CABAL_VERSION && ghcup set cabal $CABAL_VERSION +ghcup install stack $STACK_VERSION && ghcup set stack $STACK_VERSION +``` + +`ghcup set` updates the unversioned symlinks (`ghc`, `cabal`, `stack`) so +nothing downstream needs to know the exact version. + +Verify: + +```bash +ghc --version # The Glorious Glasgow Haskell Compilation System, version +cabal --version # cabal-install version +stack --version # Version , ... +``` + +## 4. Prime the Hackage index + +```bash +cabal update +``` + +This is a network call to `hackage.haskell.org`. Run it once before the fist +`cabal build` invocations. + +## 5. Install a recent z3 binary + +The Ubuntu 24.04 apt package for z3 is 4.8.12 (2021). LiquidHaskell and +other SMT-backed tools benefit from a much newer release. Install from the +GitHub release binary instead. + +```bash +Z3_VERSION=4.16.0 # update to latest tag from github.com/Z3Prover/z3/releases +GLIBC_VERSION=2.39 + +curl -sSfL \ + "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-glibc-${GLIBC_VERSION}.zip" \ + -o /tmp/z3.zip + +apt-get install -y --no-install-recommends unzip +unzip -q /tmp/z3.zip -d /tmp/z3-bin +install -m 755 /tmp/z3-bin/z3-${Z3_VERSION}-x64-glibc-2.35/bin/z3 /usr/local/bin/z3 +rm -rf /tmp/z3.zip /tmp/z3-bin + +z3 --version # Z3 version 4.16.0 - 64 bit +``` + +The glibc-2.35 build runs on Ubuntu 22.04 and 24.04. Check the releases page +for the exact asset filename if the version changes. diff --git a/.github/skills/spec-writing/SKILL.md b/.github/skills/spec-writing/SKILL.md new file mode 100644 index 0000000..39a4a91 --- /dev/null +++ b/.github/skills/spec-writing/SKILL.md @@ -0,0 +1,92 @@ +--- +name: spec-writing +description: Liquid Haskell specification writing guidelines. Use this when asked to write or fix a Liquid Haskell specification/annotation or statically check invariants to a package/module/source-file/function. +--- + +# LiquidHaskell Specification Writing Guidelines + +## General approach + +1. Make sure the build succeeds with LiquidHaskell enabled by using + `ignore` or `lazy` annotations in error trowing functions depending + on the cause of the error: + - `{-@ lazy f @-}` disables termination checking only. + - `{-@ ignore f @-}` suppresses checking a function entirely. + This allows to approach incrementally. +2. Analyze the source, references and documentation comments to find function invariants in the form of pre-conditions or post-conditions. +3. When writing a new specification for an existing function, begin by marking it `{-@ assume f :: T @-}`: + - `{-@ assume f :: T @-}` skips body checking, trusting the spec. + This lets you design the postconditions top-down — verify that callers type-check under the assumed spec before investing effort in proving the function body. Once the interface is stable, remove `assume` and prove. +4. Proving the body of a function obeys its specification, and making callers type-check with it, might require some of the following techniques: + - Write new predicates in the form of lifted Haskell functions + - Define refinement (predicate or type) aliases to make specs more concise. + - Lemmas providing additional constraints in unused bindings. + - Refactoring of the function. + When attempting a refactoring, aim for changes that preserve existing semantics and improve code readability. Refactoring should always be the last resort. +5. Keeping check disabling annotations (like `ignore`, `lazy` and `assume`) in a codebase is a valid trade-off when the proof machinery required to remove them would disproportionately clutter the source. +6. Test your changes are correct by building the package successfully with LH enabled. + +## Other guidelines + +Before introducing a new specification, pick the one with the least code impact (i.e. the amount of new definitions plus the size and semantic effects of refactorings) +among two different approaches to prove it. + +**Prefer lifted helper functions over source refactoring.** When a +specification requires auxiliary reasoning (e.g. an intermediate invariant), +first try to express it with a new reflected predicate rather than restructuring +the source code. Refactoring is preferable when it simplifies spec writing +without altering semantics. + +### Choosing `inline`, `measure`, or `reflect` to lift a function into the LH logic + +| Annotation | What it does | When to use | +|------------|-------------|-------------| +| `inline` | Expands the definition as an SMT term (`ite`/arithmetic). Not visible inside `reflect`ed bodies. | Pure arithmetic or boolean helpers used in refinement types. Must be total and simple enough for SMT to reason about directly: they cannot be recursive and they can call other (non-recursive) inlined functions. | +| `measure` | Eagerly evaluated on constructor-applied data, attached to the type's constructors. | Single-argument functions defined by pattern matching on one ADT. | +| `reflect` | Lifts the definition into logic; PLE can unfold it at constructor-applied arguments. | The general-purpose choice for predicates and helpers used in specifications. Safe for any type, including `[SomeSpecificType]`. | + +**Rule of thumb:** start with `reflect`. Switch to `measure` only when you need +eager evaluation on constructors *and* the function's domain is a standalone ADT +(not a parameterised container with mixed element types). Switch to `inline` +only for small arithmetic/boolean combinators that SMT should reason about +equationally. + +## PLE and opaque terms + +PLE (Proof by Logical Evaluation) unfolds reflected functions **only** at +syntactically constructor-applied arguments. A variable — even one known to +equal a constructor via a measure — is opaque to PLE. + +Key consequences: + +- **Recursive call results are opaque.** In `f (x:xs) = … f xs …`, PLE can unfold `g (x:xs)` (the input) but NOT `g (f xs)` (the recursive result). Use postconditions on `f` to carry facts about `f xs` into the SMT context. + +- **Opaque function parameters don't flow into SMT.** For a guard `eq x y`, where`eq` is a binary operator that evaluates to a `Bool` at runtime, LH records **no** connection between the Boolean and `eq(x,y)` in SMT. Only built-in operations like `(==)` (mapped to SMT equality) produce usable facts. + +- **Measures on opaque terms stay as uninterpreted SMT terms.** `isFirst x` where `x` is constructor-applied evaluates eagerly; where `x` is a variable it becomes an uninterpreted function. Thread the needed fact via a postcondition on the function that produces `x`. + +- **Per-constructor function variants enable PLE.** When a function receives a value whose constructor is known only via a measure or a precondition, PLE cannot match the reflected definition's patterns. Split the function into per-constructor variants (e.g. `grabGroupF`, `grabGroupS`, `grabGroupB`) that pattern-match on the constructor explicitly so PLE can unfold. + +### Proving properties through recursive structures + +- **Carry invariants through postconditions, not PLE unfolding.** For + recursive functions, state the desired property of the recursive result in + the postcondition rather than expecting PLE to derive it. The SMT solver + can then combine the postcondition with locally unfolded facts. + +- **Biconditional head-constructor specs.** When a function transforms a list + and the proof depends on the head element's constructor, add `<=>` (not just + `=>`) postconditions: `headIsFirst xs <=> headIsFirst vs`. The forward + direction lets you prove positive properties; the backward direction + (contrapositive) lets you prove negative ones. + +- **Intermediate invariants for multi-stage pipelines.** When a pipeline involves stages that weaken and re-establish an invariant define an explicit intermediate predicate and type the stages accordingly. + +### Termination + +- Termination metrics are declared with `/ [expr]`. LH adds an implicit `expr >= 0` constraint at all call sites and requires strict decrease at recursive sites. +- **Mutually recursive functions need explicit `/ [len xs]` metrics.** Without them, LH may report "decreasing parameters should be of same type" even when types match. + +### Common pitfalls + +- GHC may infer a polymorphic type for a local binding (e.g. a numeric literal `0`). If the LH annotation specifies `Int`, add an explicit Haskell type signature to avoid "specified type does not refine Haskell type" errors. diff --git a/.github/workflows/liquidhaskell.yml b/.github/workflows/liquidhaskell.yml new file mode 100644 index 0000000..b8147e6 --- /dev/null +++ b/.github/workflows/liquidhaskell.yml @@ -0,0 +1,55 @@ +name: LiquidHaskell + +on: + pull_request: + branches: + - master + +jobs: + liquidhaskell: + name: Build / Run Checks + runs-on: ubuntu-latest + strategy: + matrix: + cabal: ["3.16.0.0"] + ghc: + - "9.14.1" + z3: + - "4.15.1" + steps: + - uses: actions/checkout@v7 + + - name: Setup z3-${{ matrix.z3 }} + uses: pavpanchekha/setup-z3@6b2d476d7a9227e0d8d2b94f73cd9fcba91b5e98 + with: + version: ${{ matrix.z3 }} + distribution: glibc-2.39 + + - name: Setup GHC and cabal-install + uses: haskell-actions/setup@v2 + with: + ghc-version: ${{ matrix.ghc }} + cabal-version: ${{ matrix.cabal }} + + - name: Configure cabal + working-directory: ./Diff-liquidhaskell + run: | + cabal update + # should produce a plan.json file + cabal build --dry-run + + - uses: actions/cache@v3 + with: + path: | + ~/.cabal/packages + ~/.cabal/store + ./Diff-liquidhaskell/dist-newstyle + key: ${{ runner.os }}-${{ matrix.ghc }}-cabal-${{ hashFiles('./Diff-liquidhaskell/dist-newstyle/cache/plan.json') }} + + - name: Install dependencies + working-directory: ./Diff-liquidhaskell + run: cabal build --dependencies-only -j Diff-liquidhaskell + + - name: Build (run LiquidHaskell checks) + working-directory: ./Diff-liquidhaskell + run: cabal build -j Diff-liquidhaskell diff --git a/.gitignore b/.gitignore index 2022b2b..a3ac1fc 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ -/dist-newstyle/ +dist-newstyle/ +cabal.project.local diff --git a/Diff-liquidhaskell/Diff-liquidhaskell.cabal b/Diff-liquidhaskell/Diff-liquidhaskell.cabal new file mode 100644 index 0000000..06eaeca --- /dev/null +++ b/Diff-liquidhaskell/Diff-liquidhaskell.cabal @@ -0,0 +1,38 @@ +cabal-version: 2.4 +name: Diff-liquidhaskell +version: 0.1.0.0 +synopsis: Liquid Haskell static checks for the Diff package +description: + Provides a test suite whose build executes Diff's Liquid Haskell refinement type + annotation checks. + Exists as a separate package to break the cyclic dependency: + Diff -> liquidhaskell -> liquidhaskell-boot -> Diff. +license: BSD-3-Clause +build-type: Simple + +tested-with: GHC == 9.14.1 + +library + default-language: Haskell2010 + -- Re-use the main Diff source tree so Liquid Haskell checks the real code. + hs-source-dirs: ../src + -- No modules are exposed because this package is intended + -- for checking the build only. + other-modules: + Data.Algorithm.Diff + Data.Algorithm.DiffOutput + Data.Algorithm.DiffContext + Internal.LiftedFunctions + build-depends: + base >= 4.22.0.0 && < 5 + , array + , pretty >= 1.1 + -- LH version scheme: 0.. + -- Update the corresponding versions in .github/workflows/liquidhaskell.yml + -- after upgrading GHC and LH to keep CI in sync. + , liquidhaskell ^>= 0.9.14.1.1 + -- Recompilation check is disabled to make sure changes to specification + -- annotations are checked by the LH plugin (otherwise they are silently ignored + -- if no source change is introduced). + -- All warnings are disabled to focus on LH output. + ghc-options: -fplugin=LiquidHaskell -O0 -fforce-recomp -w diff --git a/Diff.cabal b/Diff.cabal index 2866881..0af8a74 100644 --- a/Diff.cabal +++ b/Diff.cabal @@ -13,6 +13,7 @@ license-file: LICENSE author: Sterling Clover maintainer: David Fox Build-Type: Simple +extra-doc-files: README.md tested-with: GHC == 9.14.1 @@ -41,6 +42,7 @@ library Data.Algorithm.Diff Data.Algorithm.DiffOutput Data.Algorithm.DiffContext + other-modules: Internal.LiftedFunctions ghc-options: -Wall -funbox-strict-fields source-repository head diff --git a/README.md b/README.md new file mode 100644 index 0000000..0780354 --- /dev/null +++ b/README.md @@ -0,0 +1,47 @@ +## Diff + +This is an implementation of the standard diff algorithm in Haskell. + +Time complexity is O(ND) (input length * number of differences). Space complexity is O(D^2). Includes utilities for pretty printing. + +### Building & testing + +Build with + +```shell +cabal build +``` + +Test with + +```shell +cabal test +``` + +Benchmark with + +```shell +cabal bench +``` + +### Checking Diff with Liquid Haskell + +The Diff source code can we checked with [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell/). + +Liquid Haskell requires `ghc` version 9.14.1, and an SMT solver. We have tested +the checks with the [Z3](https://github.com/Z3Prover/z3) SMT solver (versions 4.16, +and 4.15.1). + +``` +cd Diff-liquidhaskell && cabal build +``` + +The `Diff-liquidhaskell` package is a device to avoid the circular dependency between +`liquidhaskell` and the `Diff` package. + +``` mermaid +flowchart LR + Diff --> liquidhaskell --> liquidhaskell-boot --> Diff +``` + +Contributions that update the Liquid Haskell checks are appreciated but not required at this point. diff --git a/cabal.project b/cabal.project new file mode 100644 index 0000000..55446bc --- /dev/null +++ b/cabal.project @@ -0,0 +1,9 @@ +with-compiler: ghc-9.14.1 + +-- To develop against a local LH checkout, list the LH sub-packages here. +packages: + . + ./Diff-liquidhaskell + +tests: True +benchmarks: True diff --git a/ses-check.md b/ses-check.md new file mode 100644 index 0000000..38b577b --- /dev/null +++ b/ses-check.md @@ -0,0 +1,145 @@ +# The case of the `ses` check + +After the "Verify Diff with Liquid Haskell" project,[^post] +several invariants are statically checked using Liquid Haskell specs,[^branch] +but the `ses` function +-- the entry point to the diff algorithm, standing for "shortest edit script" -- +might remain unchecked under an `ignore` annotation, +even though I have a working solution. + +[^post]: Read the write-up [here](https://www.tweag.io/blog/2026-06-11-diff-package-static-checks/) +[^branch]: The static checks are still being improved and revised on the [`static-checks` branch](https://github.com/tweag/Diff/tree/static-checks) of our `Diff` fork. + +`Diff` defines it as follows: + +```haskell +ses :: (a -> b -> Bool) -> [a] -> [b] -> [DI] +ses eq as bs = path . head . dropWhile (\dl -> poi dl /= lena || poj dl /= lenb) . + concat . iterate (dstep cd) . (:[]) . addsnake cd $ + DL {poi=0,poj=0,path=[]} + where cd = canDiag eq as bs lena lenb + lena = length as; lenb = length bs +``` + +The first complain LH has of the `ses` function is lacking _means_ to assert that `head` receives a non-empty list, +which in this context translates in `dropWhile` terminating. +So all that's left do is proving _there is always one element with coordinates `(lena, lenb)` in the node stream_. +To see why this is the case and why it is difficult to verify with LH +I'll go into some details about the relation between the paper's algorithm and this implementation. + +## Implementation vs paper specification + +The `ses` function implements Myers diff algorithm following a five stage pipeline, +as documented in the function haddock: + +```haskell +-- 1. __Seed__: create an initial 0-path wave front @[addsnake cd (DL 0 0 [])]@ +-- having a single node on the tip of the longest origin-sourced snake. +-- 2. __Iterate__: apply 'dstep' repeatedly via 'iterate', producing an +-- infinite list of wave fronts (one per edit distance D = 0, 1, 2, …). +-- 3. __Flatten__: 'concat' all wave fronts into a single stream of 'DL' nodes. +-- 4. __Find__: 'dropWhile' skips nodes until one reaches @(lena, lenb)@ — the +-- bottom-right corner of the edit graph — which is the terminal node of a +-- shortest edit script. +-- 5. __Extract__: 'head' returns that node; its 'path' field carries the edit +-- trace in reverse order. +``` + +In what follows I'll show how the notion of a _wave front_ relates this implementation with the algorithm specification. +This requires me to introduce some of the concepts that underlie the paper specification, +which translate _almost_ identically. + +## Prerequisites + +TODO: Edith graph, nodes, k-diagonals + +- A `k-diagonal` is a diagonal on the _edit grid_. + A node with coordinates `(x,y)` lies on the k-diagonal with $k = x - y$. + +## Wave front + +A wave front is represented in LH logic as a list of _nodes_ at the same edit distance on a specific set of _k-diagonals_ +using a refinement type alias. + +```haskell +-- A wave front is a list of 'DL' nodes, all at the same edit distance @D@, +-- with k-diagonals @K@, @K−2@, @K−4@, … +{-@ type WaveFront D K = {xs : [DLN D] | wfDiags K xs} @-} + +-- This refinement type alias represents a 'DL' value with a fixed /D-length/, +-- which we call a "D-path location node". +{-@ type DLN D = { x : DL | len (path x) = D } @-} + +{-@ wfDiags :: Int -> xs : [DL] -> Bool / [len xs] @-} +-- | Checks if succesive nodes of a wave front lie within k-diagonals +-- differing by 2 as described in the Myers algorithm. +wfDiags :: Int -> [DL] -> Bool +wfDiags _ [] = True +wfDiags k (dl:dls) = poi dl - poj dl == k && wfDiags (k - 2) dls +``` + +Wave fronts essentially reify the iterative steps of the original Myers algorithm, +which uses the fact that successive iterations of its inner loop produce nodes on disjoint diagonals to optimize space by writing to a single vector containing the furthest reaching node along each diagonal. +In contrast, `dstep` implements the inner loop logic with a separate list as output for each run of the outer loop, +and thus incurring in some space overhead. + +```haskell +dstep + :: (Int -> Int -> Bool) -- ^ Diagonal predicate + -> [DL] -- ^ A non-empty wave front of nodes at edit distance D + -> [DL] -- ^ A non-empty wave front of nodes at edit distance D+1 +``` + +So the correspondence is: +if the n-th iteration of the the Myers algorithm outer loop returns the minimal edit distance, +then the wave front produced by nth `dstep` iteration must contain a node with coordinates `(lena, lenb)`. + +This is the case because: + +1. Both specification and algorithm start by extending on `(0,0)`by a snake. +2. Successive iterations produce nodes con complementary diagonals: + this is shown by lemma x in the paper, and is statically check by the `dstep` spec: + ```haskell + {-@ + dstep + :: (Nat -> Nat -> Bool) + -> d : Nat + -> k : Int + -> {nodes : WaveFront d k | len nodes > 0} + -> {v : WaveFront (d + 1) (k + 1) | len v = len nodes + 1} + @-} + ``` + where the current iteration `n` is equal the current edit trace length `d` + and the higher diagonal on the wave front `k`; they redundancy comes from + using them to check different properties, and thus having different types. + +In the paper, termination is argued on the basis of the existance of a worst case edit script: +delete each line from the input, and insert each line of the output. +The algorithm must find a script shorter or equal to this. +Termination is expressed as the upper bound of the outer loop, as the sum of both inputs lengths. + +By comparison, `ses` can be refactored to use a `worstCaseEdits` parameter to bound the recursion in a similar way + +```haskell +ses :: (a -> b -> Bool) -> [a] -> [b] -> [DI] +ses eq as bs = search (worstCaseEdits + 1) 0 0 [addsnake worstCaseEdits cd (DL 0 0 [])] + where cd = canDiag eq as bs lena lenb + lena = length as; lenb = length bs + worstCaseEdits = lena + lenb + {-@ search :: fuel : Nat + -> d : Nat + -> k : Int + -> {dls : WaveFront d k | len dls > 0} + -> [DI] / [fuel] @-} + search :: Int -> Int -> Int -> [DL] -> [DI] + search 0 _ _ _ = error "search: unreachable because the trivial edit script is at iteration with fuel = 1" + search fuel _ _ [] = error "ses: The search must have a seed node" + search fuel currentD k wf = case findGoal wf of + Just p -> p + Nothing -> search (fuel - 1) (currentD + 1) (k + 1) (dstep worstCaseEdits cd currentD k wf) + findGoal [] = Nothing + findGoal (dl:dls) + | poi dl == lena && poj dl == lenb = Just (path dl) + | otherwise = findGoal dls +``` + diff --git a/shell.nix b/shell.nix new file mode 100644 index 0000000..103498a --- /dev/null +++ b/shell.nix @@ -0,0 +1,14 @@ +{ + pkgs ? import { }, +}: + +with pkgs; + +mkShell { + buildInputs = [ + haskell.compiler.ghc9141 + cabal-install + haskell-language-server + z3 + ]; +} diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs index 36a8c06..696a42d 100644 --- a/src/Data/Algorithm/Diff.hs +++ b/src/Data/Algorithm/Diff.hs @@ -1,3 +1,4 @@ +{-@ LIQUID "--ple" @-} ----------------------------------------------------------------------------- -- | -- Module : Data.Algorithm.Diff @@ -66,11 +67,17 @@ module Data.Algorithm.Diff -- * Finding chunks of differences , getGroupedDiff , getGroupedDiffBy + + -- * Predicates for LiquidHaskell specifications + , noStuttering + , noFFSS + , headIsFirst, headIsSecond, headIsBoth ) where import Prelude hiding (pi) import Data.Array (listArray, (!)) import Data.Bifunctor +import Internal.LiftedFunctions -- | /Diff Instruction/ — an internal enum recording the direction of a single -- non-diagonal edge traversed in the Myers edit graph. Every non-diagonal @@ -103,6 +110,7 @@ data DI = F | S deriving (Show, Eq) -- * 'Both' — the element is common to both inputs. -- Both the left and right values are retained so that the original -- elements can be recovered even when equality ignores some fields. +{-@ data PolyDiff a b = First a | Second b | Both a b @-} data PolyDiff a b = First a | Second b | Both a b deriving (Show, Eq) @@ -119,12 +127,77 @@ instance Bifunctor PolyDiff where -- | This is 'PolyDiff' specialized so both sides are the same type. type Diff a = PolyDiff a a +-- A valid list diff is such that any `Both` value has arguments of equal length. +{-@ type ValidListDiff a b = { d : PolyDiff [a] [b] | validListDiff d }@-} + +{-@ type GroupedDiff a b = { d : ValidListDiff a b | nonEmptyDiff d } @-} + +{-@ +inline validListDiff +define length x = len x +@-} +-- | True when, for a 'Both' value, both sides have the same length. +-- 'First' and 'Second' trivially satisfy this. +validListDiff :: PolyDiff [a] [b] -> Bool +validListDiff (Both xs ys) = length xs == length ys +validListDiff (First _) = True +validListDiff (Second _) = True + +{-@ inline nonEmptyDiff @-} +nonEmptyDiff :: PolyDiff [a] [b] -> Bool +nonEmptyDiff (First []) = False +nonEmptyDiff (Second []) = False +nonEmptyDiff (Both [] _) = False +nonEmptyDiff (Both _ []) = False +nonEmptyDiff _ = True + +{-@ reflect headIsFirst @-} +{-@ reflect headIsSecond @-} +{-@ reflect headIsBoth @-} +-- | Head-constructor predicates for 'PolyDiff' lists. +-- Reflected (not measures) to avoid sort errors: measures on @[PolyDiff a b]@ +-- would be attached to the polymorphic @[]@ constructor, clashing with +-- lists of other element types. +headIsFirst, headIsSecond, headIsBoth :: [PolyDiff a b] -> Bool +headIsFirst (First _ : _) = True +headIsFirst _ = False +headIsSecond (Second _ : _) = True +headIsSecond _ = False +headIsBoth (Both _ _ : _) = True +headIsBoth _ = False + +{-@ reflect noStuttering @-} +-- | True if the list does not contain adjacent 'Diff's of the same type. +-- Uses head-constructor measures so PLE can work with opaque tails. +noStuttering :: [PolyDiff a b] -> Bool +noStuttering [] = True +noStuttering (First _ : xs) = not (headIsFirst xs) && noStuttering xs +noStuttering (Second _ : xs) = not (headIsSecond xs) && noStuttering xs +noStuttering (Both _ _ : xs) = not (headIsBoth xs) && noStuttering xs + +{-@ reflect noFFSS @-} +-- | Like 'noStuttering' but allows Both-Both adjacencies. +-- This is the invariant preserved by @doPrefix@\/@doSuffix@ which may split +-- a single 'Both' into two consecutive 'Both' elements. +noFFSS :: [PolyDiff a b] -> Bool +noFFSS [] = True +noFFSS (First _ : xs) = not (headIsFirst xs) && noFFSS xs +noFFSS (Second _ : xs) = not (headIsSecond xs) && noFFSS xs +noFFSS (Both _ _ : xs) = noFFSS xs + -- | /D-path Location/ — a node on the wave front of the Myers O(ND) diff -- algorithm. -- -- Each wave front consists of one 'DL' per /k-diagonal/. A 'DL' stores the -- endpoint coordinates and the edit trace of a \( D \)-path, i.e. a path from the -- origin \( (0,0) \) that uses exactly \( D \) non-diagonal edges. +{-@ +data DL = DL + { poi :: Nat + , poj :: Nat + , path :: { p : [DI] | len p <= poi + poj } + } +@-} data DL = DL { poi :: !Int -- ^ /Position On I/ — the @x@-coordinate of the endpoint -- in the edit graph, i.e. the number of elements @@ -138,6 +211,28 @@ data DL = DL -- 'S' steps are stored. } deriving (Show, Eq) +-- This refinement type alias represents a 'DL' value with a fixed /D-length/, +-- which we call a "D-path location node". +{-@ type DLN D = { x : DL | len (path x) = D } @-} + +{-@ inline kdiag @-} +-- | Computes the k-diagonal of a node. +-- Used in LiquidHaskell logic as a predicate. +kdiag :: DL -> Int +kdiag dl = poi dl - poj dl + +{-@ reflect wfDiags @-} +{-@ wfDiags :: Int -> xs : [DL] -> Bool / [len xs] @-} +-- | Checks if succesive nodes of a wave front lie within k-diagonals +-- differing by 2 as described in the Myers algorithm. +wfDiags :: Int -> [DL] -> Bool +wfDiags _ [] = True +wfDiags k (dl:dls) = poi dl - poj dl == k && wfDiags (k - 2) dls + +-- A wave front is a list of 'DL' nodes, all at the same edit distance @D@, +-- with k-diagonals @K@, @K−2@, @K−4@, … +{-@ type WaveFront D K = {xs : [DLN D] | wfDiags K xs} @-} + -- | Select the furthest-reaching candidate of two 'DL' nodes competing for the -- same k-diagonal, as required by the Myers algorithm. -- @@ -152,6 +247,9 @@ data DL = DL -- and both argument nodes are within the same wave front, -- -- > length (path x) == length (path y) +{-@ furthestReaching :: x : DL + -> {y : DL | kdiag x = kdiag y} + -> {v : DL | v = x || v = y} @-} furthestReaching :: DL -> DL -> DL furthestReaching x y | poi x >= poi y = x @@ -166,13 +264,20 @@ furthestReaching x y -- -- The first two 'Int' parameters stand for the lengths of the input lists, -- which are captured from the outer scope to compute them only once. -canDiag :: (a -> b -> Bool) -> [a] -> [b] -> Int -> Int -> Int -> Int -> Bool -canDiag eq as bs lena lenb = \ i j -> - if i < lena && j < lenb then (arAs ! i) `eq` (arBs ! j) else False - where - -- Lists are converted into arrays to have O(1) lookups. - arAs = listArray (0,lena - 1) as - arBs = listArray (0,lenb - 1) bs +canDiag :: (a -> b -> Bool) -- ^ Custom equality predicate + -> [a] -- ^ First input + -> [b] -- ^ Second input + -> Int -- ^ First input's length + -> Int -- ^ Second input's lenth + -> (Int -> Int -> Bool) -- ^ Diagonal predicate on the edit grid +canDiag eq as bs lena lenb = \i j -> + (i < lena && j < lenb) && ((arAs ! i) `eq` (arBs ! j)) + where + -- Lists are converted into arrays to have O(1) lookups. + arAs = listArray (0,lena - 1) as + arBs = listArray (0,lenb - 1) bs + +{-@ assume error :: _ -> {_:_ | true} @-} -- | Perform one breadth-first search expansion step, advancing every wave front -- 'DL' node by one 'DI' edit (one non-diagonal edge) and then following @@ -193,22 +298,44 @@ canDiag eq as bs lena lenb = \ i j -> -- two members of each pair straddle the same diagonal from opposite sides. -- -- Precondition: The node list must be non-empty. +{-@ +dstep + :: fuel : Nat + -> (Nat -> Nat -> Bool) + -> d : Nat + -> k : Int + -> {nodes : WaveFront d k | len nodes > 0} + -> {v : WaveFront (d + 1) (k + 1) | len v = len nodes + 1} +@-} dstep - :: (Int -> Int -> Bool) -- ^ Diagonal predicate + :: Int -- ^ Fuel for 'addsnake' snake extension + -> (Int -> Int -> Bool) -- ^ Diagonal predicate + -> Int -- ^ The current D-length; used for the static check of wave front invariant. + -> Int -- ^ The k-diagonal of the head of the wave front (phantom for LH) -> [DL] -- ^ A non-empty wave front of nodes at edit distance D -> [DL] -- ^ A non-empty wave front of nodes at edit distance D+1 -dstep _ [] = error "dstep: Cannot perform expansion on an empty list of nodes" -dstep cd (dl:dls) = addsnake cd (hStep dl) : stepAndMerge dl dls +dstep _ _ d _ [] = error "dstep: Cannot perform expansion on an empty list of nodes" +dstep fuel cd _ _ (dl:dls) = addsnake fuel cd (hStep dl) : stepAndMerge dl dls where + {-@ hStep + :: x : DLN d + -> {v : DLN (d + 1) | poi v = poi x + 1 && poj v = poj x} @-} hStep node = node {poi = poi node + 1, path = F : path node} + {-@ vStep + :: x : DLN d + -> {v : DLN (d + 1) | poi v = poi x && poj v = poj x + 1} @-} vStep node = node {poj = poj node + 1, path = S : path node} -- Merge vertical step of previous node with horizontal step of next node, -- selecting the furthest-reaching candidate for each shared k-diagonal, -- and extend it along matching elements. - stepAndMerge :: DL -> [DL] -> [DL] - stepAndMerge prev [] = [addsnake cd $ vStep prev] + {-@ stepAndMerge + :: prev : DLN d + -> rest : WaveFront d (kdiag prev - 2) + -> {v : WaveFront (d + 1) (kdiag prev - 1) | len v = len rest + 1} + / [len rest] @-} + stepAndMerge prev [] = [addsnake fuel cd $ vStep prev] stepAndMerge prev (next:rest) = - addsnake cd (furthestReaching (vStep prev) (hStep next)) : stepAndMerge next rest + addsnake fuel cd (furthestReaching (vStep prev) (hStep next)) : stepAndMerge next rest -- | Follow a /snake/ from the current position of a 'DL' node. -- @@ -218,9 +345,20 @@ dstep cd (dl:dls) = addsnake cd (hStep dl) : stepAndMerge dl dls -- @(poi dl, poj dl)@, this function advances both 'poi' and 'poj' as long -- as consecutive elements match, leaving 'path' unchanged (diagonal moves -- are not recorded as edit steps). -addsnake :: (Int -> Int -> Bool) -> DL -> DL -addsnake cd dl - | cd pi pj = addsnake cd $ +{-@ +addsnake :: fuel : Nat + -> (Nat -> Nat -> Bool) + -> dl : DL + -> {v : DL | path v == path dl && kdiag v = kdiag dl} + / [fuel] +@-} +addsnake :: Int -- ^ Fuel for termination + -> (Int -> Int -> Bool) -- ^ Equality predicate, a.k.a. 'canDiag' + -> DL + -> DL +addsnake 0 _ dl = dl +addsnake fuel cd dl + | cd pi pj = addsnake (fuel - 1) cd $ dl {poi = pi + 1, poj = pj + 1, path = path dl} | otherwise = dl where pi = poi dl; pj = poj dl @@ -228,28 +366,27 @@ addsnake cd dl -- | Compute shortest edit script (SES), as the minimum sequence of 'DI' edit -- steps that transforms @as@ into @bs@, returned in reverse order. -- --- @ses eq as bs@ runs the Myers O(ND) diff algorithm following --- a five-step pipeline: +-- @ses eq as bs@ runs the Myers O(ND) diff algorithm: -- --- 1. __Seed__: create an initial 0-path wave front @[addsnake cd (DL 0 0 [])]@ +-- 1. __Seed__: create an initial 0-path wave front @[addsnake boundary cd (DL 0 0 [])]@ -- having a single node on the tip of the longest origin-sourced snake. --- 2. __Iterate__: apply 'dstep' repeatedly via 'iterate', producing an --- infinite list of wave fronts (one per edit distance D = 0, 1, 2, …). --- 3. __Flatten__: 'concat' all wave fronts into a single stream of 'DL' nodes. --- 4. __Find__: 'dropWhile' skips nodes until one reaches @(lena, lenb)@ — the --- bottom-right corner of the edit graph — which is the terminal node of a --- shortest edit script. --- 5. __Extract__: 'head' returns that node; its 'path' field carries the edit +-- 2. __Search__: for each wave front at edit distance \( D = 0, 1, \ldots \), +-- check whether any node has reached the goal @(lena, lenb)@. If not, +-- apply 'dstep' to advance to edit distance \( D+1 \). +-- 3. __Extract__: the first goal node's 'path' field carries the edit -- trace in reverse order. -- --- This implementation is purely functional: rather than updating a shared +-- The search loop uses a fuel counter bounded by @lena + lenb + 1@, +-- which is the maximum number of edit distances that need to be explored +-- (the worst case is deleting all of @as@ and inserting all of @bs@). +-- +-- This implementation deviates from the paper in the folowing way: rather than updating a shared -- diagonal frontier array in place, as in the original paper, it builds a new --- list of 'DL' nodes for each value of \( D \) and concatenates them into --- a single lazy stream. This is simpler but carries a larger per-node overhead: --- each 'DL' holds its own edit trace as a @['DI']@ list that structurally --- shares its tail with the parent node's trace (consing one step reuses the --- existing spine), rather than the paper's single-integer-per-diagonal --- representation. The asymptotic time +-- list of 'DL' nodes for each value of \( D \). This is simpler but carries a +-- larger per-node overhead: each 'DL' holds its own edit trace as a @['DI']@ +-- list that structurally shares its tail with the parent node's trace (consing +-- one step reuses the existing spine), rather than the paper's +-- single-integer-per-diagonal representation. The asymptotic time -- and space complexity — \( O(ND) \) and \( O(D^2) \) respectively — is -- unchanged. Unlike the paper, which selects the better candidate per -- diagonal before extending its snake, 'dstep' extends snakes on /both/ @@ -260,11 +397,25 @@ addsnake cd dl -- beyond the previous winner's endpoint. The total number of element -- comparisons across all snake extensions is therefore \( O(ND) \). ses :: (a -> b -> Bool) -> [a] -> [b] -> [DI] -ses eq as bs = path . head . dropWhile (\dl -> poi dl /= lena || poj dl /= lenb) . - concat . iterate (dstep cd) . (:[]) . addsnake cd $ - DL {poi=0,poj=0,path=[]} +ses eq as bs = search (worstCaseEdits + 1) 0 0 [addsnake worstCaseEdits cd (DL 0 0 [])] where cd = canDiag eq as bs lena lenb lena = length as; lenb = length bs + worstCaseEdits = lena + lenb + {-@ search :: fuel : Nat + -> d : Nat + -> k : Int + -> {dls : WaveFront d k | len dls > 0} + -> [DI] / [fuel] @-} + search :: Int -> Int -> Int -> [DL] -> [DI] + search 0 _ _ _ = error "search: unreachable because the trivial edit script is at iteration with fuel = 1" + search fuel _ _ [] = error "ses: The search must have a seed node" + search fuel currentD k wf = case findGoal wf of + Just p -> p + Nothing -> search (fuel - 1) (currentD + 1) (k + 1) (dstep worstCaseEdits cd currentD k wf) + findGoal [] = Nothing + findGoal (dl:dls) + | poi dl == lena && poj dl == lenb = Just (path dl) + | otherwise = findGoal dls -- | Takes two lists and returns a list of differences between them. This is -- 'getDiffBy' with '==' used as predicate. @@ -281,6 +432,8 @@ getDiff = getDiffBy (==) -- -- > > getGroupedDiff "abcde" "acdf" -- > [Both "a" "a",First "b",Both "cd" "cd",First "e",Second "f"] +{-@ getGroupedDiff :: Eq a => [a] -> [a] + -> {v:[GroupedDiff a a] | noStuttering v} @-} getGroupedDiff :: (Eq a) => [a] -> [a] -> [Diff [a]] getGroupedDiff = getGroupedDiffBy (==) @@ -300,20 +453,56 @@ getDiffBy eq a b = markup a b . reverse $ ses eq a b -- -- Postcondition: the output list is guaranteed to be /chunked/. i.e. no two adjacent -- elements share the same constructor. +{-@ getGroupedDiffBy :: (a -> b -> Bool) -> [a] -> [b] + -> {vs : [GroupedDiff a b] | noStuttering vs} @-} getGroupedDiffBy :: (a -> b -> Bool) -> [a] -> [b] -> [PolyDiff [a] [b]] -getGroupedDiffBy eq a b = go $ getDiffBy eq a b - where go (First x : xs) = let (fs, rest) = goFirsts xs in First (x:fs) : go rest - go (Second x : xs) = let (fs, rest) = goSeconds xs in Second (x:fs) : go rest - go (Both x y : xs) = let (fs, rest) = goBoth xs - (fxs, fys) = unzip fs - in Both (x:fxs) (y:fys) : go rest - go [] = [] - - goFirsts (First x : xs) = let (fs, rest) = goFirsts xs in (x:fs, rest) - goFirsts xs = ([],xs) - - goSeconds (Second x : xs) = let (fs, rest) = goSeconds xs in (x:fs, rest) - goSeconds xs = ([],xs) - - goBoth (Both x y : xs) = let (fs, rest) = goBoth xs in ((x,y):fs, rest) - goBoth xs = ([],xs) +getGroupedDiffBy eq a b = groupDiff $ getDiffBy eq a b + +{-@ groupDiff :: xs : [PolyDiff a b] + -> {vs : [GroupedDiff a b] | noStuttering vs + // The following predicates allow LiquidHaskell keep track + // of the head constructor in each recursive call. + && (headIsFirst xs <=> headIsFirst vs) + && (headIsSecond xs <=> headIsSecond vs) + && (headIsBoth xs <=> headIsBoth vs)} @-} +groupDiff :: [PolyDiff a b] -> [PolyDiff [a] [b]] +groupDiff (First x : xs) = let (fs, rest) = leadingFirsts xs + in First (x:fs) : groupDiff rest +groupDiff (Second x : xs) = let (sc, rest) = leadingSeconds xs + in Second (x:sc) : groupDiff rest +groupDiff (Both x y : xs) = let (bxs, bys, rest) = leadingBoths xs + in Both (x:bxs) (y:bys) : groupDiff rest +groupDiff [] = [] + +{-@ leadingFirsts :: xs : [PolyDiff a b] + -> {v : ([a], [PolyDiff a b]) | not (headIsFirst (snd v)) + // Here and in the analogous helpers, + // the length comparison is needed for termination check. + && len (snd v) <= len xs + && (headIsSecond xs => headIsSecond (snd v)) + && (headIsBoth xs => headIsBoth (snd v))} @-} +leadingFirsts :: [PolyDiff a b] -> ([a], [PolyDiff a b]) +leadingFirsts (First y : diffs) = let (firsts, rest) = leadingFirsts diffs + in (y:firsts, rest) +leadingFirsts diffs = ([],diffs) + +{-@ leadingSeconds :: xs : [PolyDiff a b] + -> {v : ([b], [PolyDiff a b]) | not (headIsSecond (snd v)) + && len (snd v) <= len xs + && (headIsFirst xs => headIsFirst (snd v)) + && (headIsBoth xs => headIsBoth (snd v))} @-} +leadingSeconds :: [PolyDiff a b] -> ([b], [PolyDiff a b]) +leadingSeconds (Second y : diffs) = let (seconds, rest) = leadingSeconds diffs + in (y:seconds, rest) +leadingSeconds diffs = ([],diffs) + +{-@ leadingBoths :: xs : [PolyDiff a b] + -> {v : ([a], [b], [PolyDiff a b]) | not (headIsBoth (thd3 v)) + && len (thd3 v) <= len xs + && (headIsFirst xs => headIsFirst (thd3 v)) + && (headIsSecond xs => headIsSecond (thd3 v)) + && len (fst3 v) == len (snd3 v)} @-} +leadingBoths :: [PolyDiff a b] -> ([a], [b], [PolyDiff a b]) +leadingBoths (Both w z : diffs) = let (as, bs, rest) = leadingBoths diffs + in (w:as, z:bs, rest) +leadingBoths diffs = ([], [], diffs) diff --git a/src/Data/Algorithm/DiffContext.hs b/src/Data/Algorithm/DiffContext.hs index 46b93e2..18806da 100644 --- a/src/Data/Algorithm/DiffContext.hs +++ b/src/Data/Algorithm/DiffContext.hs @@ -1,3 +1,5 @@ +{-@ LIQUID "--ple" @-} +{-@ LIQUID "--ple-with-undecided-guards" @-} ----------------------------------------------------------------------------- -- | -- Module : Data.Algorithm.DiffContext @@ -20,13 +22,17 @@ module Data.Algorithm.DiffContext , unNumberContextDiff ) where -import Data.Algorithm.Diff (PolyDiff(..), Diff, getGroupedDiff) +import Data.Algorithm.Diff (PolyDiff(..), Diff, getGroupedDiff, + noStuttering, noFFSS, + headIsFirst, headIsSecond) import Data.Bifunctor import Text.PrettyPrint (Doc, text, empty, hcat) +{-@ type ContextDiff c = [Hunk c] @-} -- | A diff consisting of disjoint 'Hunk's. type ContextDiff c = [Hunk c] +{-@ type Hunk c = { h : [ValidListDiff c c] | noStuttering h} @-} -- | A 'Hunk' is a list of adjacent 'Diff's. -- -- No two consecutive elements in a 'Hunk' are both applications @@ -35,13 +41,40 @@ type ContextDiff c = [Hunk c] type Hunk c = [Diff [c]] -- | Split a 'Diff' list at consecutive 'Both'-'Both' boundaries. +{-@ splitBothBoth :: {ds:[ValidListDiff c c] | noFFSS ds} -> [Hunk c] @-} splitBothBoth :: [Diff [c]] -> [Hunk c] splitBothBoth = go [] where + {-@ go + :: g:Hunk c + -> {xs : [ValidListDiff c c] | noFFSS xs && not (headAlike g xs) } + -> [Hunk c] / [len xs] + @-} go :: Hunk c -> [Diff [c]] -> [Hunk c] go g (x@Both{} : y@Both{} : xs) = reverse (x:g) : go [] (y:xs) + where + lemma = lemmaReverseStuttering (x:g) go g (x : xs) = go (x:g) xs go g [] = [reverse g] + where + lemma = lemmaReverseStuttering g + +{-@ type ContextSize = Nat @-} +type ContextSize = Int + +{-@ opaque-reflect reverse @-} + +{-@ assume lemmaReverseStuttering + :: xs:_ -> { noStuttering (reverse xs) = noStuttering xs } @-} +lemmaReverseStuttering :: Hunk c -> () +lemmaReverseStuttering _ = () + +{-@ reflect headAlike @-} +headAlike :: Hunk c -> Hunk c -> Bool +headAlike (Both{} : _) (Both{} : _) = True +headAlike (First{} : _) (First{} : _) = True +headAlike (Second{} : _) (Second{} : _) = True +headAlike _ _ = False data Numbered a = Numbered Int a deriving Show instance Eq a => Eq (Numbered a) where @@ -72,9 +105,17 @@ unnumber (Numbered _ a) = a -- > i -- > j -- > -k +{-@ getContextDiff :: Eq a - => Maybe Int -- ^ Context size. 'Nothing' means returning a whole-diff 'Hunk'. + => Maybe ContextSize + -> [a] + -> [a] + -> ContextDiff (Numbered a) +@-} +getContextDiff :: + Eq a + => Maybe ContextSize -- ^ Context size. 'Nothing' means returning a whole-diff 'Hunk'. -> [a] -> [a] -> ContextDiff (Numbered a) @@ -83,6 +124,7 @@ getContextDiff contextSize a b = -- | If for some reason you need the line numbers stripped from the -- result of 'getContextDiff' for backwards compatibility. +{-@ unNumberContextDiff :: ContextDiff (Numbered a) -> [[Diff [a]]] @-} unNumberContextDiff :: ContextDiff (Numbered a) -> ContextDiff a unNumberContextDiff = fmap (fmap (bimap (fmap unnumber) (fmap unnumber))) @@ -93,9 +135,17 @@ unNumberContextDiff = fmap (fmap (bimap (fmap unnumber) (fmap unnumber))) -- two hunks are merged when the number of common elements between them does not -- exceed twice the context size. Furthermore, if @contextSize@ is 'Nothing' -- a single hunk with the whole diff is produced. +{-@ getContextDiffNumbered :: Eq a - => Maybe Int -- ^ Context size. 'Nothing' means returning a whole-diff 'Hunk'. + => Maybe ContextSize + -> [Numbered a] + -> [Numbered a] + -> ContextDiff (Numbered a) +@-} +getContextDiffNumbered :: + Eq a + => Maybe ContextSize -- ^ Context size. 'Nothing' means returning a whole-diff 'Hunk'. -> [Numbered a] -> [Numbered a] -> ContextDiff (Numbered a) @@ -118,7 +168,11 @@ getContextDiffNumbered (Just contextSize) a0 b0 = -- be split into two other 'Both' diffs. This happens when their contents -- are too large compared with the contex size, resulting in some @a@ -- elements being dropped. - doPrefix :: Hunk a -> Hunk a + {-@ doPrefix :: h : Hunk c + -> {v : [ValidListDiff c c] | noFFSS v + && (headIsFirst h <=> headIsFirst v) + && (headIsSecond h <=> headIsSecond v)} / [len h, 0] @-} + doPrefix :: [Diff [c]] -> [Diff [c]] doPrefix [] = [] -- Trailing common elements are no prefix. -- This case corresponds to when both input lists are identical, so the @@ -129,12 +183,17 @@ getContextDiffNumbered (Just contextSize) a0 b0 = Both (drop (length xs - contextSize) xs) (drop (length ys - contextSize) ys) : doSuffix more -- Prefix finished, do the diff then the following suffix. - doPrefix (d : ds) = doSuffix (d : ds) + doPrefix (d : ds) = d : doSuffix ds + -- | Handle the common text following a diff. -- -- Precondition: The input does not start with a 'Both' diff. Otherwise, -- it behaves like @doPrefix@. - doSuffix :: Hunk a -> Hunk a + {-@ doSuffix :: h : Hunk c + -> {v : [ValidListDiff c c] | noFFSS v + && (headIsFirst h <=> headIsFirst v) + && (headIsSecond h <=> headIsSecond v)} / [len h, 1] @-} + doSuffix :: [Diff [c]] -> [Diff [c]] doSuffix [] = [] -- A trailing suffix. doSuffix [Both xs ys] = [Both (take contextSize xs) (take contextSize ys)] diff --git a/src/Data/Algorithm/DiffOutput.hs b/src/Data/Algorithm/DiffOutput.hs index 10e1a07..39c2877 100644 --- a/src/Data/Algorithm/DiffOutput.hs +++ b/src/Data/Algorithm/DiffOutput.hs @@ -1,3 +1,8 @@ +-- Enable PLE (Proof by Logical Evaluation) so that reflected predicates like +-- 'coherentDiff' are automatically unfolded when verifying refinement types. +-- Without this, LH cannot prove obligations like @coherentDiff (Both x x) = True@ +-- because the reflected function's definition is not instantiated in the SMT context. +{-@ LIQUID "--ple" @-} ----------------------------------------------------------------------------- -- | -- Module : Data.Algorithm.DiffOutput @@ -16,37 +21,70 @@ import Text.PrettyPrint hiding ((<>)) import Data.Char import Data.List +-- Non-empty lists as refinements of regular lists. +{-@ type NonEmpty a = {xs : [a] | len xs >0}@-} + +{-@ reflect coherentDiff @-} +-- | This functions checks that both contents match whenever we have a 'Both' +-- value. +coherentDiff :: Eq c => Diff c -> Bool +coherentDiff (Both x y) = x == y +coherentDiff (First _) = True +coherentDiff (Second _) = True + +-- This refinement type synonym encodes the invariants on the 'Diff' type +-- that we expect throughout this module. Namely: +-- +-- * They have non-empty contents +-- * 'Both' values have equal arguments +{-@ type StringDiff = {d : Diff (NonEmpty String) | coherentDiff d } @-} + -- | Converts 'Diff's to 'DiffOperation's. 'First' and 'Second' -- ocurrances are converted to 'Addition' and 'Deletion', respectively, while -- consecutive ocurrances of them are replaced by a 'Change'. +{-@ diffToLineRanges :: [StringDiff] -> [DiffOperation LineRange]@-} diffToLineRanges :: [Diff [String]] -> [DiffOperation LineRange] diffToLineRanges = toLineRange 1 1 where -- | In @toLineRange x y ds@, @x@ is the index of the current string in the -- left input of the diff @ds@, and @y@ is the index of the corresponding -- string in the right input of the diff @ds@. + {-@ toLineRange :: {l:Int | l >= 1} + -> {r:Int | r >= 1} + -> diffs : [StringDiff] + -> [DiffOperation LineRange] / [len diffs, 0] @-} toLineRange :: Int -> Int -> [Diff [String]] -> [DiffOperation LineRange] - toLineRange _ _ []=[] + toLineRange _ _ [] = [] -- If the lines are the same, we just move forward. - toLineRange leftLine rightLine (Both ls _:rs)= + toLineRange leftLine rightLine (Both ls _ : rs) = let lins=length ls in toLineRange (leftLine+lins) (rightLine+lins) rs -- A 'Change' is introduced when an addition is followed by a deletion, or vice versa. - toLineRange leftLine rightLine (Second lsS:First lsF:rs)= + toLineRange leftLine rightLine (Second lsS@(_:_) : First lsF@(_:_) : rs) = toChange leftLine rightLine lsF lsS rs - toLineRange leftLine rightLine (First lsF:Second lsS:rs)= + toLineRange leftLine rightLine (First lsF@(_:_) : Second lsS@(_:_) : rs) = toChange leftLine rightLine lsF lsS rs -- Introduce 'Addition's. - toLineRange leftLine rightLine (Second lsS:rs)= - let linesS=length lsS - diff=Addition (LineRange (rightLine,rightLine+linesS-1) lsS) (leftLine-1) - in diff : toLineRange leftLine (rightLine+linesS) rs + toLineRange leftLine rightLine (Second lsS@(_:_) : rs) = + let diff = Addition (mkLineRange rightLine lsS) (leftLine-1) + in diff : toLineRange leftLine (rightLine + length lsS) rs -- Introduce 'Deletion's. - toLineRange leftLine rightLine (First lsF:rs)= - let linesF=length lsF - diff=Deletion (LineRange (leftLine,leftLine+linesF-1) lsF) (rightLine-1) - in diff: toLineRange(leftLine+linesF) rightLine rs + toLineRange leftLine rightLine (First lsF@(_:_):rs)= + let diff = Deletion (mkLineRange leftLine lsF) (rightLine-1) + in diff : toLineRange (leftLine + length lsF) rightLine rs + -- Skip empty 'Second' and 'First' entries. + -- NOTE: Both these cases are unreachable. + toLineRange leftLine rightLine (Second [] : rs) = + toLineRange leftLine rightLine rs + toLineRange leftLine rightLine (First [] : rs) = + toLineRange leftLine rightLine rs -- | Build 'Change's from adjacent additions and deletions. + {-@ toChange :: {l:Int | l >= 1} + -> {r:Int | r >= 1} + -> {lf:[String] | len lf > 0} + -> {ls:[String] | len ls > 0} + -> diffs : [StringDiff] + -> [DiffOperation LineRange] / [len diffs, 1] @-} toChange :: Int -- ^ Current left line number. -> Int -- ^ Current right line number. -> [String] -- ^ Lines from the 'First' list (corresponding to deletions). @@ -54,11 +92,10 @@ diffToLineRanges = toLineRange 1 1 -> [Diff [String]] -- ^ Remaining 'Diff's. -> [DiffOperation LineRange] toChange leftLine rightLine lsF lsS rs= - let linesS=length lsS - linesF=length lsF - in Change (LineRange (leftLine,leftLine+linesF-1) lsF) (LineRange (rightLine,rightLine+linesS-1) lsS) - : toLineRange (leftLine+linesF) (rightLine+linesS) rs + Change (mkLineRange leftLine lsF) (mkLineRange rightLine lsS) + : toLineRange (leftLine + length lsF) (rightLine + length lsS) rs +{-@ ppDiff :: [StringDiff] -> String @-} -- | Pretty print the differences. The output is similar to the output of the @diff@ utility. -- -- > > putStr (ppDiff (getGroupedDiff ["a","b","c","d","e"] ["a","c","d","f"])) @@ -102,6 +139,7 @@ parsePrettyDiffs = reverse . doParse [] . lines where -- | Parsing entry point that iteratively accumulates 'DiffOperation's -- until the input is exhausted. + {-@ doParse :: [DiffOperation LineRange] -> diffs : [String] -> [DiffOperation LineRange] / [len diffs] @-} doParse :: [DiffOperation LineRange] -> [String] -> [DiffOperation LineRange] -- NOTE: Incorrectly formatted lines are ignored. doParse acc [] = acc @@ -111,6 +149,7 @@ parsePrettyDiffs = reverse . doParse [] . lines Just nd -> doParse (nd:acc) r _ -> doParse acc r + {-@ parseDiff :: s:{[String] | len s > 0} -> {v:(Maybe (DiffOperation LineRange), [String]) | len (snd v) < len s} @-} parseDiff :: [String] -> (Maybe (DiffOperation LineRange), [String]) parseDiff [] = (Nothing,[]) parseDiff (h:rs) = let @@ -125,38 +164,47 @@ parsePrettyDiffs = reverse . doParse [] . lines ('c':hrs2) -> parseChange r1 hrs2 rs _ -> (Nothing,rs) + {-@ parseDel :: (Nat, Nat) -> String -> rs:[String] -> {v:(Maybe (DiffOperation LineRange), [String]) | len (snd v) <= len rs} @-} parseDel :: (LineNo, LineNo) -> String -> [String] -> (Maybe (DiffOperation LineRange), [String]) parseDel r1 hrs2 rs = let - -- NOTE: the wildcard should correspond to the end of line, - -- but is ignored for simplicity. (r2,_) = parseRange hrs2 (ls,rs2) = span (isPrefixOf "<") rs - in (Just $ Deletion (LineRange r1 (map (drop 2) ls)) (fst r2), rs2) + contents = map (drop 2) ls + in case contents of + (_:_) -> (Just $ Deletion (mkLineRange (fst r1) contents) (fst r2), rs2) + _ -> (Nothing, rs2) + {-@ parseAdd :: (Nat, Nat) -> String -> rs:[String] -> {v:(Maybe (DiffOperation LineRange), [String]) | len (snd v) <= len rs} @-} parseAdd :: (LineNo, LineNo) -> String -> [String] -> (Maybe (DiffOperation LineRange), [String]) parseAdd r1 hrs2 rs = let - -- NOTE: the wildcard should correspond to the end of line, - -- but is ignored for simplicity. (r2,_) = parseRange hrs2 (ls,rs2) = span (isPrefixOf ">") rs - in (Just $ Addition (LineRange r2 (map (drop 2) ls)) (fst r1), rs2) + contents = map (drop 2) ls + in case contents of + (_:_) -> (Just $ Addition (mkLineRange (fst r2) contents) (fst r1), rs2) + _ -> (Nothing, rs2) + {-@ parseChange :: (Nat, Nat) -> String -> rs:[String] -> {v:(Maybe (DiffOperation LineRange), [String]) | len (snd v) <= len rs} @-} parseChange :: (LineNo, LineNo) -> String -> [String] -> (Maybe (DiffOperation LineRange), [String]) parseChange r1 hrs2 rs = let - -- NOTE: the wildcard should correspond to the end of line, - -- but is ignored for simplicity. (r2,_) = parseRange hrs2 (ls1,rs2) = span (isPrefixOf "<") rs in case rs2 of -- The left and right diff of a 'Change' are separated by a "---" line. ("---":rs3) -> let (ls2,rs4) = span (isPrefixOf ">") rs3 - in (Just $ Change (LineRange r1 (map (drop 2) ls1)) (LineRange r2 (map (drop 2) ls2)), rs4) + contents1 = map (drop 2) ls1 + contents2 = map (drop 2) ls2 + in case (contents1, contents2) of + (_:_, _:_) -> (Just $ Change (mkLineRange (fst r1) contents1) (mkLineRange (fst r2) contents2), rs4) + _ -> (Nothing, rs4) _ -> (Nothing,rs2) - parseRange :: String -> ((LineNo, LineNo),String) + {-@ parseRange :: String -> {v : ((Nat, Nat), String) | fst (fst v) <= snd (fst v)} @-} + parseRange :: String -> ((LineNo, LineNo), String) parseRange l = let (fstLine,rs) = span isDigit l + a = max 0 (read fstLine) (sndLine,rs3) = case rs of -- The comma is used to separate -- the start and end line numbers in a range, @@ -164,7 +212,8 @@ parsePrettyDiffs = reverse . doParse [] . lines -- i.e. the range is a single line. (',':rs2) -> span isDigit rs2 _ -> (fstLine,rs) - in ((read fstLine,read sndLine),rs3) + b = max a (read sndLine) + in ((a, b), rs3) -- | Line number alias. Always non-negative. type LineNo = Int @@ -177,11 +226,23 @@ type LineNo = Int -- > snd lrNumbers - fst lrNumbers + 1 == length lrContents -- -- which imply @lrContents@ cannot be empty. +{-@ +data LineRange = LineRange { lrNumbers :: {range : (Nat, Nat) | fst range <= snd range} + , lrContents :: {contents : [String] | snd lrNumbers - fst lrNumbers = len contents - 1} + } +@-} data LineRange = LineRange { lrNumbers :: (LineNo, LineNo) , lrContents :: [String] } deriving (Show, Read, Eq, Ord) +-- | Smart constructor for 'LineRange' that computes the end line from the +-- start line and the content length, guaranteeing that its content length and +-- range match. +{-@ mkLineRange :: start:Nat -> contents:{[String] | len contents > 0} -> LineRange @-} +mkLineRange :: Int -> [String] -> LineRange +mkLineRange start contents = LineRange (start, start + length contents - 1) contents + -- | Diff operation representing changes to apply. data DiffOperation a = Deletion a LineNo -- ^ Element deleted on the left input, line number diff --git a/src/Internal/LiftedFunctions.hs b/src/Internal/LiftedFunctions.hs new file mode 100644 index 0000000..958a489 --- /dev/null +++ b/src/Internal/LiftedFunctions.hs @@ -0,0 +1,25 @@ +-- | Utilify functions lifted into Liquid Haskell logic. +-- +-- The /raison d'être/ for this module is that functions need to be explicitly +-- /lifted/ into the LiquidHaskell logic before we can call them in refinement +-- predicates. +-- In general, we need access to a functions unfoldings for the relevant constraints +-- to be produced. At the time of writing, GHC does not reliable exposes dependency +-- unfoldings in interface files; so the most robust work around is +-- to reimplement certain functions locally. +-- For a detailed discussion see: +-- +module Internal.LiftedFunctions where + +-- | Measures for triplet projections. +{-@ +measure fst3 +measure snd3 +measure thd3 +@-} +fst3 :: (a, b, c) -> a +fst3 (x, _, _) = x +snd3 :: (a, b, c) -> b +snd3 (_, y, _) = y +thd3 :: (a, b, c) -> c +thd3 (_, _, z) = z