array bound 是 abstract 的 Expr

a.hs

{-# 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
--   main
--
-- 重點:本檔若能「編譯通過」,就已經證明 array 上下界的靜態型別是
-- Syntax.Abstract.Expr —— 因為下面 arrayBounds 的簽章寫死成 (A.Expr, A.Expr),
-- 而 termExpr 寫死成 Typed.Expr。型別對不上的話 GHC 會直接拒編。

module Main where

import Control.Exception (evaluate)
import GCL.Dependency (evalDependencyResolution)
import GCL.Type2.ToTyped (runToTyped)
import qualified Data.Text as T
import qualified Syntax.Abstract as A
import qualified Syntax.Concrete.Instances.ToAbstract as CA
import qualified Syntax.Parser as P
import qualified Syntax.Typed as Typed

-- | 最小可 elaborate 的程式:
--   con N 讓 N 在 scope;尾端一段 body 讓它成為完整 program。
src :: T.Text
src =
  T.unlines
    [ "con N : Int",
      "con A : array [0 .. N) of Int",
      "var x : Int",
      "{ True }",
      "x := x",
      "{ True }"
    ]

-- | Pipeline:parse → abstract → dependency resolution → elaborate(Type2)。
--   注意簽章是 Typed.Program —— 這是「已 elaborate」的結果。
elaborated :: Typed.Program
elaborated =
  let prog = either (error . show) id (P.scanAndParse P.program "min" src)
      abs1 = either (error . show) id (evalDependencyResolution (CA.runAbstractTransform prog))
      (typed, _) = either (error . show) id (runToTyped abs1 mempty)
   in typed

-- | 從 elaborated 的 Typed.Program 鑽進 array 型別,取出上下界。
--   簽章 (A.Expr, A.Expr) 就是「編譯期證明」:若 bound 其實是 Typed.Expr,這裡編不過。
arrayBounds :: (A.Expr, A.Expr)
arrayBounds =
  let Typed.Program _ decls _ _ _ = elaborated
      Typed.ConstDecl _ ty _ _ = decls !! 1 -- con A 的 Type
      A.TArray (A.Interval lo hi _) _ _ = ty -- 拆 array → 區間
   in (endpointExpr lo, endpointExpr hi)
  where
    endpointExpr (A.Including e) = e
    endpointExpr (A.Excluding e) = e

-- | 對照組:同一棵樹裡 term 層 (x := x) 的 x,簽章是 Typed.Expr。
termExpr :: Typed.Expr
termExpr =
  let Typed.Program _ _ _ stmts _ = elaborated
      Typed.Assign _ (e : _) _ = stmts !! 1
   in e

main :: IO ()
main = do
  -- 先強制跑完一次 elaboration,把 codebase 內既有的 debug trace
  -- (GCL.Type2.ToTyped.findName 裡的 `traceM $ show env`)沖掉,
  -- 以免它跟下面的輸出交錯。這串 trace 與本 demo 無關,可忽略。
  putStrLn "--- (以下到下一條分隔線之間是 codebase 既有的 traceM 輸出,可忽略) ---"
  _ <- evaluate (length (show elaborated))
  putStrLn "------------------------------------------------------------------"
  let (loE, hiE) = arrayBounds
  putStrLn "=== array bounds (取自 elaborated 的 Typed.Program) ==="
  putStrLn ("lower bound :: A.Expr       = " ++ show loE)
  putStrLn ("upper bound :: A.Expr       = " ++ show hiE)
  putStrLn ""
  putStrLn "=== 對照:term 層 expr ==="
  putStrLn ("x in (x := x) :: Typed.Expr = " ++ show termExpr)
  putStrLn ""
  putStrLn "本檔能編譯 = 型別系統已證明:array bound 是 Abstract.Expr,term 是 Typed.Expr。"

ghci.txt

ghci> main
--- (以下到下一條分隔線之間是 codebase 既有的 traceM 輸出,可忽略) ---
defns: []
decls: [con N: Int, con A: array [ 0 .. N ) of Int, var x: Int]
exprs: []
stmts: [{ True }, x:= x, { True }]
A :: array [ 0 .. N ) of Int
N :: Int
x :: Int
------------------------------------------------------------------
=== array bounds (取自 elaborated 的 Typed.Program) ===
lower bound :: A.Expr       = Lit (Num 0) (Just 2:16-17)
upper bound :: A.Expr       = Const (Name "N" (Just 2:21-22)) (Just 2:21-22)

=== 對照:term 層 expr ===
x in (x := x) :: Typed.Expr = Var (Name "x" (Just 5:6-7)) (TBase TInt (Just 3:9-12)) (Just 5:6-7)

本檔能編譯 = 型別系統已證明:array bound 是 Abstract.Expr,term 是 Typed.Expr。
ghci>