From e595763f9135a70e2676634da87722bdf8285915 Mon Sep 17 00:00:00 2001 From: James Eversole Date: Tue, 1 Sep 2026 10:33:54 -0500 Subject: [PATCH] Attach contracts to definitions Contracts now live directly on definitions via @ / =@ annotations and travel automatically with exported values. - Remove !export from lexer/parser/AST/evaluator/manifest/resolver and CLI. - Simplify workspace module export logic: export all top-level local definitions by default. - Update Frontend.ContractDesugar: - Named binder annotations (x@nat?) expand to per-argument withContract. - Phantom annotations (@nat?) expand to a local raw helper plus a wrapper, keeping fixed points shared and only depending on withContract. - Merge lib/guardedBase.tri into lib/base.tri and annotate partial/sensitive base functions: head, tail, last, add, sub, mul, div, mod, pow, min, max, length, sum, product. - Add check contract helper to lib/base.tri. - Update demos/contractBasics.tri and README to reflect @/=@-only design. - Update test suite: remove guardedBase import, replace explicit !export test with a test verifying that contract annotations on an exported definition are enforced on import. - Fix remaining base.tri definitions (div/mod/pow) to stay point-free. --- README.md | 5 +-- demos/contractBasics.tri | 38 ++++++-------------- lib/base.tri | 35 ++++++++++-------- lib/guardedBase.tri | 22 ------------ lib/intensionalContracts.tri | 1 - src/Eval.hs | 10 ++---- src/FileEval.hs | 29 +++------------ src/Frontend/ContractDesugar.hs | 63 ++++++++++++++++++++------------- src/Lexer.hs | 4 --- src/Main.hs | 1 - src/Module/Manifest.hs | 27 ++++---------- src/Module/Resolver.hs | 1 - src/Parser.hs | 16 ++------- src/Research.hs | 9 ++--- test/Spec.hs | 42 +++++++--------------- 15 files changed, 105 insertions(+), 198 deletions(-) delete mode 100644 lib/guardedBase.tri diff --git a/README.md b/README.md index 641c2e0..c53f837 100644 --- a/README.md +++ b/README.md @@ -63,8 +63,9 @@ tricu eval --format decode program.tri tricu eval --output result.txt program.tri ``` -Annotations are parsed but currently ignored at runtime; the contract layer -is not yet wired into evaluation or workspace module auto-builds. +Contract annotations (`@` and `=@`) attach guards directly to definitions. +When a workspace module is built, those guarded definitions become the +exported values, so contracts travel with imports automatically. Compile/import/export Arboricx bundles: diff --git a/demos/contractBasics.tri b/demos/contractBasics.tri index 479362a..de284fa 100644 --- a/demos/contractBasics.tri +++ b/demos/contractBasics.tri @@ -1,8 +1,6 @@ !import "prelude" !Local --- A custom 'and' combinator written directly against base.matchResult. --- It succeeds only when *both* contracts succeed, threading the checked value --- from the first into the second. This makes the Result pair structure explicit. +-- Custom contract combinators built directly on matchResult. myAndC = (c1 c2 value rest : matchResult (msg _ : contractErr msg rest) @@ -13,29 +11,15 @@ myAndC = (c1 c2 value rest : natural? = guardC "natural" (n : gte? n 0) nonZero? = guardC "non-zero" (n : not? (isZero? n)) --- Safe wrappers around partial base / list functions. --- The frontend desugars @ and =@ into runtime withContract applications. -safeDiv a@natural? b@(myAndC natural? nonZero?) =@natural? div a b +-- Phantom annotations let point-free definitions carry their own contracts. +-- The base library now uses the same syntax, so head/tail/div etc. are +-- guarded by default. +myHead @(nonEmptyListOf anyC) =@anyC head +myTail @(listOf anyC) =@(listOf anyC) tail +myDiv @natural? @(myAndC natural? nonZero?) =@natural? div -safeHead xs@(nonEmptyListOf anyC) =@anyC head xs -safeTail xs@(nonEmptyListOf anyC) =@(listOf anyC) tail xs +-- The `check` helper applies a contract to any value and returns the +-- checked value (or the diagnostic message on failure). +checkedSuccessor = check natural? (add 1 2) --- A higher-order wrapper: the supplied function must satisfy a contract, --- the input list must satisfy a contract, and the result list is guaranteed. -checkedMap f@(fnContract anyC natural?) xs@(listOf anyC) =@(listOf natural?) map f xs - --- Advertise the safe wrappers in the module manifest with their own contracts. -!export safeDiv : fn2 natural? nonZero? natural? -!export safeHead : fnContract (nonEmptyListOf anyC) anyC -!export checkedMap : fn2 (fnContract anyC natural?) (listOf anyC) (listOf natural?) - --- A small interaction-tree pipeline that uses contracts as recoverable effects. -pipeline = (input : - do bindM - scaled <- checkM natural? (mul input 2) - half <- handleM "contract" - (_ : pureM 1) - (checkM nonZero? (sub scaled 4)) - pureM (div scaled half)) - -main = runM (pipeline 5) +main = pair checkedSuccessor (myDiv 10 2) diff --git a/lib/base.tri b/lib/base.tri index 43be9c8..11f4b3c 100644 --- a/lib/base.tri +++ b/lib/base.tri @@ -190,14 +190,14 @@ pred = y (self : triage isZero? = triage true (_ : false) (_ _ : false) -add = y (self x y : +add @nat? @nat? =@nat? (y (self x y : triage y (_ : succ y) (_ _ : succ (self (pred x) y)) - x) + x)) -sub = y (self a b : +sub @nat? @nat? =@nat? y (self a b : ifLazy (isZero? b) (_ : a) @@ -222,13 +222,13 @@ lt? = a b : gt? = a b : lt? b a -mul = y (self a b : +mul @nat? @nat? =@nat? y (self a b : ifLazy (isZero? b) (_ : 0) (_ : add a (self a (pred b)))) -div = y (self a b : +div @nat? @nat? =@nat? y (self a b : ifLazy (isZero? b) (_ : 0) @@ -237,7 +237,7 @@ div = y (self a b : (_ : 0) (_ : succ (self (sub a b) b)))) -mod = y (self a b : +mod @nat? @nat? =@nat? y (self a b : ifLazy (isZero? b) (_ : 0) @@ -246,7 +246,7 @@ mod = y (self a b : (_ : a) (_ : self (sub a b) b))) -pow = y (self a b : +pow @nat? @nat? =@nat? y (self a b : ifLazy (isZero? b) (_ : 1) @@ -260,9 +260,9 @@ even? n = (triage odd? = (n : not? (even? n)) -min = (a b : ifLazy (lte? a b) (_ : a) (_ : b)) +min @nat? @nat? =@nat? (a b : ifLazy (lte? a b) (_ : a) (_ : b)) -max = (a b : ifLazy (lte? a b) (_ : b) (_ : a)) +max @nat? @nat? =@nat? (a b : ifLazy (lte? a b) (_ : b) (_ : a)) -- --------------------------------------------------------------------------- -- Result combinators @@ -299,8 +299,8 @@ resultMapErr = (f result : matchList = a b : triage a _ b emptyList? = matchList true (_ _ : false) -head = matchList t (head _ : head) -tail = matchList t (_ tail : tail) +head xs@(nonEmptyListOf anyC) =@anyC matchList t (h _ : h) xs +tail xs@(nonEmptyListOf anyC) =@(listOf anyC) matchList t (_ r : r) xs append_ self xs ys = matchList @@ -353,7 +353,7 @@ length_ self xs = 0 (_ r : succ (self r)) xs -length = xs : y length_ xs +length @(listOf anyC) =@nat? y length_ reverse_ self xs acc = matchList @@ -389,7 +389,7 @@ last_ self xs = (self r) (emptyList? r)) xs -last = xs : y last_ xs +last @(nonEmptyListOf anyC) =@anyC y last_ all?_ self pred xs = matchList @@ -526,8 +526,8 @@ contains?_ self needle haystack = (startsWith? needle haystack) contains? = needle haystack : y contains?_ needle haystack -sum = foldl (acc x : add x acc) 0 -product = foldl (acc x : mul x acc) 1 +sum @(listOf nat?) =@nat? foldl (acc x : add x acc) 0 +product @(listOf nat?) =@nat? foldl (acc x : mul x acc) 1 -- --------------------------------------------------------------------------- -- Generic separators @@ -634,6 +634,11 @@ zipWith = f xs ys : y zipWith_ f xs ys contractOk = (value : (rest : ok value rest)) contractErr = (msg : (rest : err msg rest)) +check contract value = + withContract contract value + (x : x) + (msg : msg) + -- Apply a contract with the conventional rest slot and return the raw Result. checkContract = (contract value : contract value t) diff --git a/lib/guardedBase.tri b/lib/guardedBase.tri deleted file mode 100644 index 4be71c7..0000000 --- a/lib/guardedBase.tri +++ /dev/null @@ -1,22 +0,0 @@ -!import "prelude" !Local -!import "intensional" !Local - --- Runtime-guarded wrappers around partial or structurally-sensitive base/list --- functions. Each wrapper uses the frontend @ / =@ desugaring and is exported --- with an advertised contract so manifests carry the contract terms. - -safeHead xs@(nonEmptyListOf anyC) =@anyC head xs -safeTail xs@(nonEmptyListOf anyC) =@(listOf anyC) tail xs - -safeDiv a@nat? b@(andC nat? nonZero?) =@nat? div a b - -safeHalf n@(andC nat? evenC?) =@nat? div n 2 - --- last is only guaranteed to return the maximum if the input list is sorted. -sortedMax xs@(sortedList? nat?) =@nat? last xs - -!export safeHead : fnContract (nonEmptyListOf anyC) anyC -!export safeTail : fnContract (nonEmptyListOf anyC) (listOf anyC) -!export safeDiv : fn2 nat? nonZero? nat? -!export safeHalf : fnContract (andC nat? evenC?) nat? -!export sortedMax : fnContract (sortedList? nat?) nat? diff --git a/lib/intensionalContracts.tri b/lib/intensionalContracts.tri index 93ad477..ef2e22d 100644 --- a/lib/intensionalContracts.tri +++ b/lib/intensionalContracts.tri @@ -1,5 +1,4 @@ !import "prelude" !Local -!import "contracts" !Local -- Structural contracts that exploit Tree Calculus's intensional nature. -- These are not simple type tags; they recursively inspect the tree shape. diff --git a/src/Eval.hs b/src/Eval.hs index 554a6e0..b973b0b 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -68,14 +68,10 @@ evalTricu env x = go env (reorderDefs env (map recoverParams (desugarContracts x where go env' [] = env' go env' [def] = - let updatedEnv = evalSingle (trace ("evaluating: " ++ defName' def) env') def + let updatedEnv = evalSingle env' def in Map.insert "!result" (result updatedEnv) updatedEnv go env' (def:xs) = - evalTricu (evalSingle (trace ("evaluating: " ++ defName' def) env') def) xs - - defName' (SDef name _ _) = name - defName' (SDefAnn name _ _ _) = name - defName' _ = "" + evalTricu (evalSingle env' def) xs evalASTSync :: Env -> TricuAST -> T evalASTSync env term = case term of @@ -209,8 +205,6 @@ freeVars (SDefAnn _ args ret body) = , Set.singleton "withContract" ]) (Set.fromList (annotatedBinders args)) -freeVars (SExport _ Nothing) = Set.empty -freeVars (SExport _ (Just c)) = freeVarsViewExpr c freeVars (TStem t) = freeVars t freeVars (TFork t u) = Set.union (freeVars t) (freeVars u) freeVars (SList xs) = foldMap freeVars xs diff --git a/src/FileEval.hs b/src/FileEval.hs index 170a086..739df0e 100644 --- a/src/FileEval.hs +++ b/src/FileEval.hs @@ -16,8 +16,7 @@ module FileEval ) where import ContentStore -import Eval (evalASTSync, evalTricu, freeVars, result) -import Frontend.ContractDesugar (viewExprToAst) +import Eval (evalTricu, freeVars, result) import Lexer import Module.Manifest import Module.Resolver @@ -159,37 +158,25 @@ buildWorkspaceModule ctx store moduleName sourcePath = do loaded <- loadFile' ctx sourcePath let asts = loadedAst loaded env = evalTricu (loadedImports loaded) asts - explicitExports = topLevelExports asts localNames = topLevelDefinitions asts - names = if not (null explicitExports) - then explicitExports - else if null localNames - then map (\n -> (n, Nothing)) (filter (/= "!result") (Map.keys env)) - else map (\n -> (n, Nothing)) localNames + names = if null localNames + then filter (/= "!result") (Map.keys env) + else localNames exports <- mapM (buildExport env) names manifestHash <- putManifest store (ModuleManifest [] exports) writeAlias store ModuleAlias (T.pack moduleName) (ObjectRef (unDomain manifestDomain) manifestHash) where - buildExport env (name, mContract) = case Map.lookup name env of + buildExport env name = case Map.lookup name env of Nothing -> errorWithoutStackTrace $ "Workspace module export not found after evaluation: " ++ name Just term -> do rootRef <- putTreeTerm store term - mContractRef <- case mContract of - Nothing -> return Nothing - Just c -> do - cterm <- evaluateContract env c - chash <- putTreeTerm store cterm - return (Just (ObjectRef (unDomain treeTermDomain) chash)) return ModuleExport { moduleExportName = T.pack name , moduleExportObject = ObjectRef (unDomain treeTermDomain) rootRef , moduleExportAbi = "arboricx.abi.tree.v1" - , moduleExportContract = mContractRef } - evaluateContract env c = return $ evalASTSync env (viewExprToAst c) - topLevelDefinitions :: [TricuAST] -> [String] topLevelDefinitions = mapMaybe go where @@ -197,12 +184,6 @@ topLevelDefinitions = mapMaybe go go (SDefAnn name _ _ _) = Just name go _ = Nothing -topLevelExports :: [TricuAST] -> [(String, Maybe ViewExpr)] -topLevelExports = mapMaybe go - where - go (SExport name mContract) = Just (name, mContract) - go _ = Nothing - defaultStorePath :: IO StorePath defaultStorePath = do home <- getHomeDirectory diff --git a/src/Frontend/ContractDesugar.hs b/src/Frontend/ContractDesugar.hs index f812eb2..52df607 100644 --- a/src/Frontend/ContractDesugar.hs +++ b/src/Frontend/ContractDesugar.hs @@ -10,39 +10,54 @@ import Research -- | Convert source-level contract annotations into runtime boundary checks. -- --- A definition such as +-- Named binder annotations (e.g. @x@nat?) wrap each argument as it is +-- received and the result before it is returned. -- --- addPos x@positive? y@positive? =@positive? (add x y) --- --- is desugared to a plain definition whose body wraps every annotated --- argument and the result with 'withContract' from the contract library: --- --- addPos = \x -> withContract positive? x --- (\x -> \y -> withContract positive? y --- (\y -> withContract positive? (add x y) --- (\r -> r) --- (\msg _ -> msg)) --- (\msg _ -> msg)) --- (\msg _ -> msg) --- --- This makes annotated source depend on the existing 'withContract' helper, --- which is an ordinary 'tricu' function from 'lib/contracts.tri'. Files that --- use annotations should import the contract library (or another library that --- re-exports 'withContract'). +-- Phantom annotations (e.g. @nat? on a point-free definition) are turned +-- into a fresh local raw value plus a wrapper definition that uses named +-- binder annotations. The raw value is bound with a local 'let' so that +-- fixed points (such as definitions built with 'y') are shared rather than +-- recreated on every call. The wrapper only needs 'withContract', which is +-- already required by any source-level annotation. desugarContracts :: [TricuAST] -> [TricuAST] -desugarContracts asts = map desugarTopItem asts +desugarContracts asts = concatMap desugarTopItem asts where desugarTopItem (SDefAnn name args ret body) = desugarDefAnn name args ret body - desugarTopItem other = other + desugarTopItem other = [other] -desugarDefAnn :: String -> [DefArg] -> Maybe ViewExpr -> TricuAST -> TricuAST -desugarDefAnn name args ret body = SDef name [] (wrapArgs args body') +-- | Fresh internal name for the raw, contract-free helper introduced by +-- phantom annotations. It is bound locally with 'SLet' so it never escapes +-- into the final environment. +rawNameFor :: String -> String +rawNameFor name = "_" ++ name ++ "_raw" + +desugarDefAnn :: String -> [DefArg] -> Maybe ViewExpr -> TricuAST -> [TricuAST] +desugarDefAnn name args ret body + | all isPhantom args = + let argContracts = map getPhantom args + rawNm = rawNameFor name + rawVar = SVar rawNm Nothing + argNames = take (length args) ["x","y","z"] + newArgs = zipWith DefBinder argNames (map Just argContracts) + wrappedBody = foldl SApp rawVar (map (\n -> SVar n Nothing) argNames) + wrapper = wrapArgs newArgs (wrapReturn ret wrappedBody) + in [ SDef name [] (SLet rawNm body wrapper) ] + | otherwise = [ SDef name [] (wrapArgs args body') ] where body' = wrapReturn ret body + okCont = SLambda ["r"] (SVar "r" Nothing) + errCont = SLambda ["msg"] (SVar "msg" Nothing) + + isPhantom (DefPhantom _) = True + isPhantom _ = False + + getPhantom (DefPhantom c) = c + getPhantom _ = error "expected phantom annotation" + wrapReturn Nothing b = b wrapReturn (Just c) b = - withContractE (viewExprToAst c) b (SLambda ["r"] (SVar "r" Nothing)) errCont + withContractE (viewExprToAst c) b okCont errCont wrapArgs [] b = b wrapArgs (DefBinder nm Nothing : rest) b = SLambda [nm] (wrapArgs rest b) @@ -54,8 +69,6 @@ desugarDefAnn name args ret body = SDef name [] (wrapArgs args body') wrapArgs (DefPhantom _ : _) _ = error "phantom contract arguments are not yet supported by the frontend" - errCont = SLambda ["msg"] (SVar "msg" Nothing) - -- | Turn a source annotation expression into an ordinary AST expression. -- Contract annotations are written with the same surface syntax as terms, -- so the mapping is mostly structural. diff --git a/src/Lexer.hs b/src/Lexer.hs index 8014e7f..ef58f13 100644 --- a/src/Lexer.hs +++ b/src/Lexer.hs @@ -36,7 +36,6 @@ tricuLexer = do , try dot , try identifierWithHash , try keywordT - , try lExport , try identifier , try namespace , try integerLiteral @@ -131,9 +130,6 @@ lImport = do name <- importAlias return (LImport path name) -lExport :: Lexer LToken -lExport = string "!export" *> notFollowedBy alphaNumChar $> LExport - importAlias :: Lexer String importAlias = string "!Local" <|> do first <- letterChar <|> char '_' diff --git a/src/Main.hs b/src/Main.hs index d3d9947..b455560 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -442,7 +442,6 @@ runImport opts = do name (treeTermRef root) "arboricx.abi.tree.v1" - Nothing | (name, root) <- roots ] moduleName = T.pack $ maybe (takeBaseName file) id (importModule opts) diff --git a/src/Module/Manifest.hs b/src/Module/Manifest.hs index ce339f2..37598e4 100644 --- a/src/Module/Manifest.hs +++ b/src/Module/Manifest.hs @@ -41,7 +41,6 @@ data ModuleExport = ModuleExport { moduleExportName :: Text , moduleExportObject :: ObjectRef , moduleExportAbi :: Text - , moduleExportContract :: Maybe ObjectRef } deriving (Eq, Ord, Show) manifestDomain :: Domain @@ -59,17 +58,13 @@ encodeManifest manifest = encodeUtf8 $ Text.unlines $ , esc (objectRefKind $ moduleReferenceRef ref) , esc (objectRefHash $ moduleReferenceRef ref) ] - encodeExport ex = - let base = Text.intercalate "\t" - [ "export" - , esc (moduleExportName ex) - , esc (objectRefKind $ moduleExportObject ex) - , esc (objectRefHash $ moduleExportObject ex) - , esc (moduleExportAbi ex) - ] - in case moduleExportContract ex of - Nothing -> base - Just ref -> base <> "\t" <> esc (objectRefKind ref) <> "\t" <> esc (objectRefHash ref) + encodeExport ex = Text.intercalate "\t" + [ "export" + , esc (moduleExportName ex) + , esc (objectRefKind $ moduleExportObject ex) + , esc (objectRefHash $ moduleExportObject ex) + , esc (moduleExportAbi ex) + ] -- | Parse the canonical manifest encoding. decodeManifest :: ByteString -> Either String ModuleManifest @@ -92,14 +87,6 @@ decodeManifest bs = do <$> unesc name <*> (ObjectRef <$> unesc kind <*> unesc hash) <*> unesc abi - <*> pure Nothing - Right manifest { moduleManifestExports = moduleManifestExports manifest ++ [ex] } - ["export", name, kind, hash, abi, ckind, chash] -> do - ex <- ModuleExport - <$> unesc name - <*> (ObjectRef <$> unesc kind <*> unesc hash) - <*> unesc abi - <*> (Just <$> (ObjectRef <$> unesc ckind <*> unesc chash)) Right manifest { moduleManifestExports = moduleManifestExports manifest ++ [ex] } _ -> Left $ "invalid module manifest row: " ++ Text.unpack line diff --git a/src/Module/Resolver.hs b/src/Module/Resolver.hs index 22e9a01..f15c129 100644 --- a/src/Module/Resolver.hs +++ b/src/Module/Resolver.hs @@ -84,7 +84,6 @@ resolveModuleExport resolver namespace ex = do , resolvedExportLocalName = nsVariable namespace (T.unpack sourceName) , resolvedExportObject = ref , resolvedExportAbi = moduleExportAbi ex - , resolvedExportContract = moduleExportContract ex , resolvedExportTerm = term } diff --git a/src/Parser.hs b/src/Parser.hs index 94add63..56f0a93 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -69,12 +69,9 @@ manyItemsP = do topItemP :: TokParser TricuAST topItemP = do toks <- getInput - case toks of - LExport : _ -> exportP - _ -> - case definitionHeadTop toks of - Just _ -> definitionP - Nothing -> exprTopP + case definitionHeadTop toks of + Just _ -> definitionP + Nothing -> exprTopP definitionHeadTop :: [LToken] -> Maybe (String, [String]) definitionHeadTop toks = @@ -221,13 +218,6 @@ importP = do isImport (LImport _ _) = True isImport _ = False -exportP :: TokParser TricuAST -exportP = do - void (tok (== LExport) "export") - name <- identifierNameP - mContract <- optional (tok (== LColon) ":" *> annotationTypeP) - pure (SExport name mContract) - exprTopP :: TokParser TricuAST exprTopP = do toks <- getInput diff --git a/src/Research.hs b/src/Research.hs index 5eb64c5..b097852 100644 --- a/src/Research.hs +++ b/src/Research.hs @@ -19,10 +19,9 @@ import qualified Data.Text as T data T = Leaf | Stem T | Fork T T deriving (Show, Eq, Ord) --- Contract source annotations --- ViewType, ViewRef, and ViewProvenance were removed with the old View Contract --- checker. Source annotations are still parsed into ViewExpr but are not --- interpreted by a separate static checker. +-- Contract source annotations for @ and =@ syntax. ViewExpr carries the +-- surface syntax of a contract until Frontend.ContractDesugar turns it into a +-- runtime contract application. data ViewExpr = VEName String | VEVar String @@ -61,7 +60,6 @@ data TricuAST | SLet String TricuAST TricuAST | SEmpty | SImport String String - | SExport String (Maybe ViewExpr) deriving (Show, Eq, Ord) -- Lexer Tokens @@ -71,7 +69,6 @@ data LToken | LKeywordT | LNamespace String | LImport String String - | LExport | LAssign | LAssignAt | LAt diff --git a/test/Spec.hs b/test/Spec.hs index 3caa9a3..f6d07f6 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -19,7 +19,7 @@ import qualified Network.Socket as NS import Control.Monad (forM, forM_) import Control.Monad.IO.Class (liftIO) import System.IO.Temp (withSystemTempDirectory) -import System.Directory (createDirectory, doesFileExist, doesDirectoryExist, listDirectory) +import System.Directory (createDirectory, doesFileExist, doesDirectoryExist, listDirectory, getCurrentDirectory) import System.FilePath (()) import Data.Bits (xor) import Data.Char (digitToInt) @@ -58,8 +58,7 @@ allTestLibsEnv = unsafePerformIO $ do io <- evaluateFile "./lib/io.tri" sock <- evaluateFile "./lib/socket.tri" intensional <- evaluateFile "./lib/intensionalContracts.tri" - guarded <- evaluateFile "./lib/guardedBase.tri" - pure (Map.unions [base, bytes, bin, http, arbor, io, sock, intensional, guarded]) + pure (Map.unions [base, bytes, bin, http, arbor, io, sock, intensional]) {-# NOINLINE allTestLibsEnv #-} tests :: TestTree @@ -1678,7 +1677,7 @@ demos = testGroup "Test provided demo functionality" decodeResult res @?= "[t t, 10]" , testCase "Safe base wrappers demo" $ do res <- liftIO $ evaluateFileResult "./demos/contractBasics.tri" - decodeResult res @?= "[t t, 1]" + decodeResult res @?= "[3, t t, t, t t]" ] decoding :: TestTree @@ -1942,7 +1941,6 @@ contentStoreTests = testGroup "Content Store Tests" "main" (ObjectRef (unDomain treeTermDomain) root) "arboricx.abi.tree.v1" - Nothing ] root <- putTreeTerm store term h <- putManifest store (manifestFor root) @@ -1959,7 +1957,6 @@ contentStoreTests = testGroup "Content Store Tests" "value" (ObjectRef (unDomain treeTermDomain) termH) "arboricx.abi.tree.v1" - Nothing ] manifestBytes = encodeManifest manifest manifestH = hashObject manifestDomain manifestBytes @@ -2013,32 +2010,20 @@ contentStoreTests = testGroup "Content Store Tests" Nothing -> assertFailure "expected workspace module manifest" Just manifest -> map moduleExportName (moduleManifestExports manifest) @?= ["value"] - , testCase "Workspace modules: explicit !export with contract" $ - withSystemTempDirectory "tricu-workspace-explicit-export" $ \dir -> do + , testCase "Workspace modules: contract annotations travel with exported definitions" $ + withSystemTempDirectory "tricu-workspace-contract-export" $ \dir -> do let store = StorePath (dir "store") libPath = dir "util.tri" mainPath = dir "main.tri" - writeFile (dir "tricu.workspace") "module util = util.tri\n" - writeFile libPath "alwaysOk = (x : x)\n\naddOne x = x\n!export addOne : alwaysOk\n" - writeFile mainPath "!import \"util\" Util\n\nmain = Util.addOne 5\n" + cwd <- getCurrentDirectory + writeFile (dir "tricu.workspace") ("module base = \"" ++ cwd "lib/base.tri\"\nmodule util = \"" ++ dir "util.tri\"\n") + writeFile libPath "!import \"base\" !Local\n\nalwaysOk = (value rest : ok value rest)\n\nneverOk = (value rest : err \"nope\" rest)\n\nsafeId n@alwaysOk =@alwaysOk n\n\nbadId n@neverOk =@neverOk n\n" + writeFile mainPath "!import \"util\" Util\n\nmain = Util.safeId 5\n" env <- evaluateFileWithStore (Just store) mainPath result env @?= ofNumber 5 - mAlias <- readAlias store ModuleAlias "util" - case mAlias of - Nothing -> assertFailure "expected workspace build to write util module alias" - Just ref -> do - mManifest <- getManifest store (objectRefHash ref) - case mManifest of - Nothing -> assertFailure "expected workspace module manifest" - Just manifest -> do - map moduleExportName (moduleManifestExports manifest) @?= ["addOne"] - case moduleManifestExports manifest of - [ex] -> do - assertBool "expected contract ref" (moduleExportContract ex /= Nothing) - case moduleExportContract ex of - Just cref -> objectRefKind cref @?= unDomain treeTermDomain - Nothing -> assertFailure "expected contract ref" - _ -> assertFailure "expected exactly one export" + writeFile mainPath "!import \"util\" Util\n\nmain = Util.badId 5\n" + envFail <- evaluateFileWithStore (Just store) mainPath + decodeResult (result envFail) @?= "\"nope\"" , testCase "Module imports: resolve manifest exports from store" $ withSystemTempDirectory "tricu-module-import" $ \dir -> do @@ -2050,7 +2035,6 @@ contentStoreTests = testGroup "Content Store Tests" "value" (ObjectRef (unDomain treeTermDomain) root) "arboricx.abi.tree.v1" - Nothing ] root <- putTreeTerm store term manifestHash <- putManifest store (manifestFor root) @@ -2083,7 +2067,7 @@ contentStoreTests = testGroup "Content Store Tests" , testCase "Module resolver diagnostics: missing tree term names export and hash" $ do let root = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" manifest = ModuleManifest [] - [ ModuleExport "value" (ObjectRef (unDomain treeTermDomain) root) "arboricx.abi.tree.v1" Nothing ] + [ ModuleExport "value" (ObjectRef (unDomain treeTermDomain) root) "arboricx.abi.tree.v1" ] resolver = ObjectResolver { resolverAlias = \kind name -> return $ if kind == ModuleAlias && name == "demo" then Just (ObjectRef (unDomain manifestDomain) "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb")