Views? Never heard of 'em. Just contracts.

This commit is contained in:
2026-08-31 15:24:19 -05:00
parent c6e4a43178
commit 073ed17eb7
59 changed files with 1739 additions and 7700 deletions

View File

@@ -1,18 +1,16 @@
module Main where
import Check (checkFile, checkFileWithStore, instrumentIOContinuations)
import ContentStore
import ContentStore.Bundle
import Module.Manifest
import System.Exit (die)
import Eval (evalTricu, mainResult, result)
import FileEval
( ContractMode(..)
, LoadedSource(..)
( LoadedSource(..)
, defaultStorePath
, evaluateFileWithContextWithStoreAndMode
, evaluateFileWithContextWithStore
, evaluateFileWithStore
, loadFileWithStoreMode
, loadFileWithStore
, compileFileWithStore
)
import IODriver (IOPermissions(..), runIO)
@@ -47,16 +45,11 @@ data AppArgs = AppArgs
data TricuArgs
= Repl
| Check
{ checkInput :: FilePath
, checkStore :: Maybe FilePath
}
| Eval
{ evalFiles :: [FilePath]
, evalStore :: Maybe FilePath
, evalFormat :: EvaluatedForm
, evalOutput :: FilePath
, evalUnchecked :: Bool
, evalIo :: Bool
, evalAllowRead :: [FilePath]
, evalAllowWrite :: [FilePath]
@@ -112,16 +105,6 @@ readEvaluatedForm = eitherReader $ \s -> case s of
"string" -> Right StringLit
_ -> Left $ "Unknown format: " ++ s ++ ". Expected: tree, fsl, ast, ternary, ascii, decode, number, string"
checkParser :: Parser TricuArgs
checkParser = Check
<$> argument str (metavar "FILE")
<*> optional (option str
( long "store"
<> short 's'
<> metavar "PATH"
<> help "Content-addressed store path for module import resolution"
))
evalParser :: Parser TricuArgs
evalParser = Eval
<$> many (argument str (metavar "FILE..."))
@@ -145,10 +128,6 @@ evalParser = Eval
<> value ""
<> help "Write output to file instead of stdout"
)
<*> switch
( long "unchecked"
<> help "Evaluate as untyped code: ignore View Contract annotations and do not publish unchecked view refs"
)
<*> switch
( long "io"
<> help "Interpret the result as an IO action tree and execute it"
@@ -325,9 +304,7 @@ tricuParser = AppArgs
<**> infoOption versionStr (long "version" <> help "Show version"))
where
topCommands = mconcat
[ command "check" (info (checkParser <**> helper)
(progDesc "Check View Contract annotations and report ok or diagnostics"))
, command "eval" (info (evalParser <**> helper)
[ command "eval" (info (evalParser <**> helper)
(progDesc "Evaluate tricu source and print the result of the final expression"))
, command "arboricx" (info (arboricxParser <**> helper)
(progDesc "Arboricx bundle operations"))
@@ -374,7 +351,6 @@ main = do
args = applyGlobalStore mGlobalStore (appCommand appArgs)
case args of
Repl -> runReplWithStore mGlobalStore
Check {} -> runCheck args
Eval {} -> runEval args
ArboricxCompile {} -> runCompile args
ArboricxImport {} -> runImport args
@@ -390,7 +366,6 @@ main = do
applyGlobalStore :: Maybe FilePath -> TricuArgs -> TricuArgs
applyGlobalStore mGlobal args = case args of
Repl -> Repl
Check {} -> args { checkStore = preferLocal (checkStore args) }
Eval {} -> args { evalStore = preferLocal (evalStore args) }
ArboricxCompile {} -> args { compileStore = preferLocal (compileStore args) }
ArboricxImport {} -> args { importStore = preferLocal (importStore args) }
@@ -413,22 +388,6 @@ runReplWithStore mStore = do
Nothing -> repl
Just store -> replWithStore (StorePath store)
runCheck :: TricuArgs -> IO ()
runCheck opts = do
output <- case checkStore opts of
Nothing -> checkFile (checkInput opts)
Just storePath -> checkFileWithStore (StorePath storePath) (checkInput opts)
putStrLn output
evaluateCheckedIOFile :: StorePath -> ContractMode -> Env -> FilePath -> IO Env
evaluateCheckedIOFile store mode env filePath = do
loaded <- loadFileWithStoreMode mode store filePath
checkedAst <- case instrumentIOContinuations (loadedAst loaded) of
Left err -> die err
Right asts -> pure asts
viewEnv <- evaluateFileWithStore (Just store) "./lib/view.tri"
pure $ evalTricu (Map.unions [viewEnv, loadedImports loaded, env]) checkedAst
runEval :: TricuArgs -> IO ()
runEval opts = do
let files = evalFiles opts
@@ -441,12 +400,7 @@ runEval opts = do
return $ result env
_ -> do
mStoreOpt <- traverse (pure . StorePath) (evalStore opts)
let contractMode = if evalUnchecked opts then IgnoreContracts else EnforceContracts
finalEnv <- if evalIo opts && contractMode == EnforceContracts
then do
store <- maybe defaultStorePath pure mStoreOpt
foldM (evaluateCheckedIOFile store contractMode) Map.empty files
else foldM (evaluateFileWithContextWithStoreAndMode contractMode mStoreOpt) Map.empty files
finalEnv <- foldM (evaluateFileWithContextWithStore mStoreOpt) Map.empty files
return $ mainResult finalEnv
finalT <- if evalIo opts
then do
@@ -489,7 +443,6 @@ runImport opts = do
(treeTermRef root)
"arboricx.abi.tree.v1"
Nothing
Nothing
| (name, root) <- roots
]
moduleName = T.pack $ maybe (takeBaseName file) id (importModule opts)