LCamel

  答案：sbv-11.0 確實能正確驅動 z3-4.16.0

  我把 sbv 官方整套 golden 測試（涵蓋 bitvector / real / array / quantifier / uninterpreted / optimize / set / string… 各種理論）打給你這顆 z3-4.16.0 跑。113
  個「失敗」逐一檢查後，沒有任何一個是 z3 算錯或 sbv 接不上 z3：

  A. 97 個 —— 純粹是「沒裝其他 solver」（與 z3 無關）

  ┌────────────────────┬────────┐
  │    缺的 solver     │ 失敗數 │
  ├────────────────────┼────────┤

LCamel

#!/usr/bin/env stack
{- stack script
   --resolver lts-23.28
   --package sbv
-}
{-# LANGUAGE ScopedTypeVariables #-}

-- 獨立的 SBV / z3 小測試。
--
-- 用 lts-23.28 內建的 sbv（11.0），後端呼叫 PATH 上的 z3。

LCamel

-- runghc -threaded TChanTest.hs
-- ghc -threaded TChanTest.hs && ./TChanTest
-- stack runghc -- -threaded TChanTest.hs

module Main where

import Control.Concurrent (forkIO, threadDelay)
import Control.Concurrent.STM (atomically)
import Control.Concurrent.STM.TChan (TChan, newTChan, readTChan, writeTChan)
import Control.Exception (SomeException, catch)

LCamel

  不改的壞處(全是工程債,無 soundness)

  1. 渲染邏輯被迫雙份維護(最實際的成本)
  Abstract 和 Typed 各有一份幾乎平行的 handleExpr(Render Expr),Pretty 也各一套。任何「表達式怎麼顯示」的調整要改兩處,且容易
  drift——現在兩份已有細微差異。

  2. 拔不掉 Abstract render/pretty cluster(你的原始目標被擋住)
  Render Expr/Chain/CaseClause/Interval/... 一整包得留著,純粹因為 array bound 還是 Abstract.Expr。死重量。

  3. 心智模型是假的,會誤導人

LCamel

{-# LANGUAGE OverloadedStrings #-}
-- 這幾個 OPTIONS 是為了讓 refutable 的 let/where pattern binding 不被
-- 專案的 -Werror=incomplete-patterns 擋下(純 demo,無所謂 totality)。
{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-incomplete-uni-patterns #-}
{-# OPTIONS_GHC -Wno-error=incomplete-patterns -Wno-error=incomplete-uni-patterns #-}

-- 用法:
--   cd gcl
--   stack ghci gcl:lib
--   :load a.hs

LCamel

genFib = function* () {
  let [curr, next] = [0, 1];
  while (true) {
    yield curr;
    [curr, next] = [next, curr + next];
  }
};

fib = genFib();
while (true) {

LCamel

digraph AgdaCoreTermHierarchy {
    rankdir=BT;
    fontname="Helvetica,Arial,sans-serif";
    
    nodesep=0.7;
    ranksep=0.9;

    node [shape=box, style="rounded,filled", fillcolor="#f0f8ff", fontname="Helvetica,Arial,sans-serif", penwidth=1.5, color="#4682b4"];
    edge [color="#d35400", fontname="Helvetica,Arial,sans-serif", fontsize=11, fontcolor="#d35400"];

LCamel

● 分析完成。252 個 orphan instances 分佈在 28 個檔案，可以分成三大類：

  ---
  結論：大部分 orphan 是架構上難以避免的

  1. 結構上必要的 orphan（~100+ 個）— 不建議動

  Pretty / Render instances 是最大宗。原因是經典的循環依賴問題：

  Syntax/Abstract/Types.hs  定義 Expr, Stmt, Type ...

LCamel

-- NextDidChange.csp
-- FDR4 model to verify the NextDidChange property of the GCL Server-Edit protocol.
--
-- Reference: https://github.com/scmlab/gcl-all/wiki/Server-Edit
--
-- Property (NextDidChange):
--   If workspace/applyEdit succeeds (client applied the edit),
--   then the next textDocument/didChange the server receives
--   belongs to that edit.
--

LCamel

{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE NamedFieldPuns #-}

module Server.Load2 where

import Data.IntMap (IntMap)
import Data.Text (Text)
import Error (Error (..))
import GCL.Predicate (Hole, PO, Spec)
import GCL.Range (Range)