diff --git a/README.md b/README.md index c53f837..508c0cf 100644 --- a/README.md +++ b/README.md @@ -63,10 +63,6 @@ tricu eval --format decode program.tri tricu eval --output result.txt program.tri ``` -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: ```sh @@ -75,13 +71,6 @@ tricu arboricx import --file program.arboricx --module program tricu arboricx export --module prelude --output prelude.arboricx ``` -Inspect store aliases: - -```sh -tricu store alias list --kind modules -tricu store alias get --kind modules prelude -``` - ### REPL Running `tricu` with no subcommand starts the REPL. The REPL uses the same diff --git a/lib/base.tri b/lib/base.tri index c0b5992..a00f13f 100644 --- a/lib/base.tri +++ b/lib/base.tri @@ -39,10 +39,10 @@ snd p = matchPair takeSecond p where takeSecond a b = b resultIsOk result = - matchResult (err rest : false) (val rest : true) result + matchResult (errR rest : false) (val rest : true) result resultIsErr result = - matchResult (err rest : true) (val rest : false) result + matchResult (errR rest : true) (val rest : false) result not? = matchBool false true and? = matchBool id (_ : false) @@ -638,25 +638,52 @@ zipWith = f xs ys : y zipWith_ f xs ys -- The second argument is the conventional "rest" slot. On success a contract -- returns the checked value wrapped in the standard ok shape; on failure it -- returns a diagnostic wrapped in the standard err shape. +-- +-- The contract kernel is a globally configurable function selected by the +-- runner. It decides whether to accept the contract result, replace it, log +-- it, or transform the diagnostic. The default kernel is the identity on the +-- contract Result. +-- +-- The runner may rebind 'kernel' to a different kernel before evaluating +-- user code (e.g. via --contract-kernel). -- --------------------------------------------------------------------------- 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) - --- Apply a contract and continue with either the onOk or onFail branch. -withContract = (contract value onOk onFail : +-- Default contract kernel. Return the contract Result unchanged. +defaultKernel = (contract value result : matchResult - (msg _ : onFail msg) - (checked _ : onOk checked) - (contract value t)) + (msg rest : err msg rest) + (v rest : ok v rest) + result) + +-- The active kernel. The runner may rebind this name to a different kernel +-- before evaluating user code (e.g. via --contract-kernel). Internally, +-- withContract dispatches through this binding, so rebinding 'kernel' changes +-- the behaviour of every contract boundary in the program. +kernel = defaultKernel + +-- Skip-everything kernel. Resume with the original value on failure. +skipKernel = (contract value result : + matchResult + (msg rest : ok value rest) + (v rest : ok v rest) + result) + +-- Apply a contract and pass the raw Result to the kernel. +withContract = (contract value : + kernel contract value (contract value t)) + +-- Apply a contract and return the checked value or the diagnostic message. +check contract value = + matchResult + (msg _ : msg) + (v _ : v) + (withContract contract value) + +-- Apply a contract and return the raw Result (kernel is bypassed). +checkContract = (contract value : contract value t) -- --------------------------------------------------------------------------- -- Basic contracts @@ -774,29 +801,34 @@ pairOf = (c1 c2 p rest : fnContract = (argC resC f rest : contractOk (x : (rest1 : - withContract argC x - (x' : - withContract resC (f x') - (y : contractOk y rest1) - (msg : contractErr msg rest1)) - (msg : contractErr msg rest1))) + matchResult + (msg _ : contractErr msg rest1) + (x' _ : + matchResult + (msg _ : contractErr msg rest1) + (y _ : contractOk y rest1) + (withContract resC (f x'))) + (withContract argC x))) rest) fn2 = (arg1C arg2C resC f rest : contractOk (x : (rest1 : - withContract arg1C x - (x' : + matchResult + (msg _ : contractErr msg rest1) + (x' _ : contractOk (y : (rest2 : - withContract arg2C y - (y' : - withContract resC (f x' y') - (z : contractOk z rest2) - (msg : contractErr msg rest2)) - (msg : contractErr msg rest2))) + matchResult + (msg _ : contractErr msg rest2) + (y' _ : + matchResult + (msg _ : contractErr msg rest2) + (z _ : contractOk z rest2) + (withContract resC (f x' y'))) + (withContract arg2C y))) rest1) - (msg : contractErr msg rest1))) + (withContract arg1C x))) rest) -- --------------------------------------------------------------------------- diff --git a/notes/contract-design.md b/notes/contract-design.md new file mode 100644 index 0000000..3ae0e53 --- /dev/null +++ b/notes/contract-design.md @@ -0,0 +1,328 @@ +# Contract Kernel Design + +## Status + +Implemented. The contract system uses a configurable kernel defined in +`lib/base.tri`. All contract logic lives in pure tree calculus. + +## Goals + +1. **User code stays ergonomic.** `@`/`=@` syntax remains. Calling a guarded + function looks the same as calling an unguarded one. +2. **No stringly-dynamic failures.** A contract boundary returns a structured + `Result`. The kernel decides whether to abort, resume with a replacement, + log, or otherwise transform the result. +3. **All evaluation logic in pure tree calculus.** The evaluator does not treat + contracts specially; contracts are ordinary functions and the desugarer + emits ordinary tricu code. +4. **Optional contract enforcement.** A CLI/REPL flag can disable contract + syntax entirely by stripping annotations at desugar time. +5. **Configurable failure semantics.** A global kernel, supplied by the user + via CLI/REPL, determines how contract failures are handled for the + session. + +## Core idea + +A contract annotation on a definition desugars into a runtime guard. The +runtime guard applies a contract predicate to a value and passes the resulting +`Result` to the current `kernel`. The `kernel` returns another `Result`, which +the wrapper inspects: + +- `ok value` means the guard succeeded; continue with `value`. +- `err msg` means the guard failed; abort and propagate the error. + +The default kernel is the identity on the contract `Result`. A custom kernel +can transform failures into successes, wrap diagnostics, or log failures before +aborting. + +## Kernel + +### Signature + +```tricu +kernel contract value result -> Result +``` + +- `contract`: the contract predicate being checked. +- `value`: the unevaluated original value passed to the contract. +- `result`: the `Result` produced by evaluating `contract value t`. + +### Default kernel + +`lib/base.tri` defines both `defaultKernel` and the active `kernel`: + +```tricu +defaultKernel = (contract value result : + matchResult + (msg rest : err msg rest) + (v rest : ok v rest) + result) + +kernel = defaultKernel +``` + +The runner may rebind `kernel` to a different value before evaluating user +code (e.g. via `--contract-kernel`). Because `withContract` looks up `kernel` +dynamically at application time, rebinding it changes the behaviour of every +contract boundary. + +### Skip kernel + +Resume with the original value whenever a contract fails: + +```tricu +skipKernel = (contract value result : + matchResult + (msg rest : ok value rest) + (v rest : ok v rest) + result) +``` + +### Logging kernel + +Abort but also emit a log entry: + +```tricu +loggingKernel = (contract value result : + matchResult + (msg rest : pair (logMsg msg) (err msg rest)) + (v rest : ok v rest) + result) +``` + +### Resume-with-default kernel + +```tricu +resumeWithZero = (contract value result : + matchResult + (msg rest : ok 0 rest) + (v rest : ok v rest) + result) +``` + +## Runtime guard primitive + +`withContract` is the primitive emitted by the desugarer: + +```tricu +withContract = (contract value : + kernel contract value (contract value t)) +``` + +`check` is a convenience wrapper that extracts the value or the diagnostic +message: + +```tricu +check contract value = + matchResult + (msg _ : msg) + (v _ : v) + (withContract contract value) +``` + +## Desugaring + +Desugaring runs **before** import selection so that names introduced by the +desugarer (`withContract`, `matchResult`, `err`, `ok`, etc.) are included in +the selected exports of imported modules. This ensures that a module using +contract annotations imports everything it needs from `base`/`prelude`. + +### Phantom annotations + +```tricu +add @nat? @nat? =@nat? addRaw +``` + +desugars to: + +```tricu +add = (x y : + matchResult + (msg _ : \_ : err msg t) + (x' _ : + matchResult + (msg _ : err msg t) + (y' _ : + matchResult + (msg _ : err msg t) + (r _ : r) + (withContract nat? (addRaw x' y'))) + (withContract nat? y)) + (withContract nat? x)) +``` + +The first failure continuation is absorbing (`\_ : err msg t`) because `add` +is curried and a failure on the first argument should consume the second +argument without producing garbage. + +`addRaw` is the locally-let-bound raw helper, as in the current phantom +implementation. + +### Named-binder annotations + +```tricu +safeDiv a@nat? b@(andC nat? nonZero?) =@nat? div a b +``` + +desugars to: + +```tricu +safeDiv = (a b : + matchResult + (msg _ : \_ : err msg t) + (a' _ : + matchResult + (msg _ : err msg t) + (b' _ : + matchResult + (msg _ : err msg t) + (r _ : r) + (withContract nat? (div a' b'))) + (withContract (andC nat? nonZero?) b)) + (withContract nat? a)) +``` + +### No return contract + +```tricu +head xs@(nonEmptyListOf anyC) =@anyC headRaw +``` + +desugars to: + +```tricu +head = (xs : + matchResult + (msg _ : err msg t) + (xs' _ : + matchResult + (msg _ : err msg t) + (r _ : r) + (withContract anyC (headRaw xs'))) + (withContract (nonEmptyListOf anyC) xs)) +``` + +### No annotations + +Definitions without `@`/`=@` are emitted unchanged. + +## Failure propagation + +When a non-final argument contract fails, the wrapper returns a function that +absorbs the next argument and then returns the failed `Result`. This prevents +partial-application accidents like `gt? "the" 3` reducing to a garbage number. + +When the final argument or result contract fails, the wrapper returns +`\msg -> err msg t`, which is the failure constructor awaiting its `rest` +slot. + +## Skip-contracts flag + +When the `--skip-contracts` flag is set, the desugarer strips all `@`/`=@` +annotations and emits the raw function body. This is faster than running the +skip kernel because no contract code is generated at all. + +### CLI + +```bash +tricu eval --skip-contracts program.tri +tricu repl --skip-contracts +``` + +### REPL + +```tricu +> :set skip-contracts +> add 1 2 +3 +> :unset skip-contracts +> add "bad" 2 +[t, "not a natural number"] +``` + +## Kernel selection + +### CLI + +```bash +tricu eval --contract-kernel resumeWithZero program.tri +``` + +### REPL + +```tricu +> :set contract-kernel resumeWithZero +> add "bad" 2 +2 +``` + +### Resolution + +The kernel name is resolved like any other top-level binding in the program or +its imports. The runner prepends `kernel = ` to the program AST (or +inserts it into the environment) after imports are resolved. If the name is +not found, evaluation fails with an undefined-variable error. + +## Base library changes + +1. `withContract` becomes the runtime guard primitive shown above. +2. `check` extracts the checked value or diagnostic message from the kernel + `Result`. +3. Contract predicates (`nat?`, `nonZero?`, `bool?`, etc.) remain pure + functions returning `Result`. +4. Guarded base functions (`add`, `sub`, `head`, `div`, etc.) use the new + desugaring. +5. Raw helpers (`addRaw`, `subRaw`, etc.) remain for internal use and recursion. + +## Custom contracts + +Users write ordinary predicates returning `Result`: + +```tricu +positive? = (n rest : + ifThenElse (gte? n 1) + (ok n rest) + (err "expected positive integer" rest)) +``` + +and use them with the same syntax: + +```tricu +fact n@positive? =@nat? y (self n : ...) +``` + +Contract combinators (`andC`, `orC`, `guardC`) compose in the obvious way. + +## Limitations + +1. **Global kernel only.** There is no local kernel override. A module or + function cannot install a different kernel for part of the program. + Workarounds: split into separate evaluation sessions, or use explicit + `withContract` calls with a local handler function. +2. **Kernel must return `Result`.** A kernel that returns a plain value is a + bug. The `defaultKernel`/`skipKernel` templates show the required shape. +3. **Failures are first-class `Result` values.** A caller that ignores a + returned `err msg` and treats it as data will operate on the `Result` tree. + This is inherent to any value-level error mechanism. +4. **Function contracts are advanced.** Contracts on function arguments + (e.g. `f @ (nat? -> nat?)`) require intensional/quantified contracts. The + simple predicate model covers most use cases. + +## Implementation notes + +- `Frontend.ContractDesugar` emits `matchResult`/`withContract`/`err`/`ok` + instead of continuation-passing `withContract`. +- `FileEval.loadFile'` desugars before computing selected exports, so + imported modules bring in the runtime helpers needed by annotations. +- `Eval.injectKernel` is a fallback that binds `kernel` to `defaultKernel` + when `kernel` is missing from the environment. + +## Open questions + +1. **Should `--skip-contracts` strip annotations or just bind the skip + kernel?** Currently stripping is the intended design; not yet implemented. +2. **Should we provide a small set of built-in kernel names?** `default`, + `skip`, `strict`, `log` would cover common cases without requiring the user + to define them. +3. **How do we expose the current kernel to introspection?** A top-level + `currentContractKernel` binding might be useful for debugging. diff --git a/src/Eval.hs b/src/Eval.hs index b973b0b..1b3861b 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -73,6 +73,19 @@ evalTricu env x = go env (reorderDefs env (map recoverParams (desugarContracts x go env' (def:xs) = evalTricu (evalSingle env' def) xs +-- | Ensure the contract kernel is bound. If the environment already defines +-- 'kernel', leave it alone. Otherwise, bind 'kernel' to 'defaultKernel' if +-- that is available. This lets the default kernel live in a .tri file while +-- still providing a fallback for code that imports the base library. +injectKernel :: Env -> Env +injectKernel env = + case Map.lookup "kernel" env of + Just _ -> env + Nothing -> + case Map.lookup "defaultKernel" env of + Just k -> Map.insert "kernel" k env + Nothing -> env + evalASTSync :: Env -> TricuAST -> T evalASTSync env term = case term of SLambda _ _ -> evalASTSync env (elimLambda term) diff --git a/src/FileEval.hs b/src/FileEval.hs index 739df0e..0967f2e 100644 --- a/src/FileEval.hs +++ b/src/FileEval.hs @@ -16,7 +16,8 @@ module FileEval ) where import ContentStore -import Eval (evalTricu, freeVars, result) +import Eval (evalTricu, freeVars, result, injectKernel) +import Frontend.ContractDesugar (desugarContracts) import Lexer import Module.Manifest import Module.Resolver @@ -80,7 +81,7 @@ evaluateFile = evaluateFileWithStore Nothing evaluateFileWithStore :: Maybe StorePath -> FilePath -> IO Env evaluateFileWithStore mStore filePath = do loaded <- maybe loadFile loadFileWithStore mStore filePath - pure $ evalTricu (loadedImports loaded) (loadedAst loaded) + pure $ evalTricu (injectKernel (loadedImports loaded)) (loadedAst loaded) evaluateFileWithContext :: Env -> FilePath -> IO Env evaluateFileWithContext = evaluateFileWithContextWithStore Nothing @@ -90,7 +91,7 @@ evaluateFileWithContextWithStore mStore env filePath = do loaded <- case mStore of Nothing -> loadFile filePath Just store -> loadFileWithStore store filePath - pure $ evalTricu (Map.union (loadedImports loaded) env) (loadedAst loaded) + pure $ evalTricu (injectKernel (Map.union (loadedImports loaded) env)) (loadedAst loaded) preprocessFile :: FilePath -> IO [TricuAST] preprocessFile p = loadedAst <$> loadFile p @@ -126,15 +127,16 @@ loadFile' ctx currentPath = do Left err -> errorWithoutStackTrace (handleParseError tokens err) Right ast -> let (nonImports, importTargets) = processImports ast + desugaredNonImports = desugarContracts nonImports in do - let reexportOnlyModule = null (topLevelDefinitions nonImports) && not (null importTargets) + let reexportOnlyModule = null desugaredNonImports && not (null importTargets) resolvedModules <- mapM (\(target, name) -> do ensureWorkspaceModule ctx target - resolveModuleImportSelecting (loadResolver ctx) (selectedExportsForImport reexportOnlyModule target name nonImports) target name) importTargets + resolveModuleImportSelecting (loadResolver ctx) (selectedExportsForImport reexportOnlyModule target name desugaredNonImports) target name) importTargets let moduleEnv = resolvedModulesEnv resolvedModules pure LoadedSource { loadedImports = moduleEnv - , loadedAst = nonImports + , loadedAst = desugaredNonImports , loadedModules = resolvedModules } diff --git a/src/Frontend/ContractDesugar.hs b/src/Frontend/ContractDesugar.hs index d38b57e..a9ad8c3 100644 --- a/src/Frontend/ContractDesugar.hs +++ b/src/Frontend/ContractDesugar.hs @@ -3,7 +3,6 @@ module Frontend.ContractDesugar ( desugarContracts , viewExprToAst - , withContractE ) where import Research @@ -17,8 +16,8 @@ import Research -- 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. +-- recreated on every call. The wrapper only needs 'withContract' and +-- 'matchResult' from the contract library. desugarContracts :: [TricuAST] -> [TricuAST] desugarContracts asts = concatMap desugarTopItem asts where @@ -46,36 +45,45 @@ desugarDefAnn name args ret body where body' = wrapReturn ret body - okCont = SLambda ["r"] (SVar "r" Nothing) - -- | Failure continuation used for the final argument contract or the - -- result contract. It returns the diagnostic message directly because - -- no further arguments are expected. - errContFinal = SLambda ["msg"] (SVar "msg" Nothing) - -- | Failure continuation used for non-final argument contracts. It - -- returns a function that ignores the next argument and then returns the - -- diagnostic message. This prevents a failed partial application from - -- being treated as the final result when the remaining arguments are - -- eventually supplied. - errContAbsorb = SLambda ["msg"] (SLambda ["_"] (SVar "msg" Nothing)) - isPhantom (DefPhantom _) = True isPhantom _ = False getPhantom (DefPhantom c) = c getPhantom _ = error "expected phantom annotation" + -- | Build: matchResult onFail (\value _ -> body) result + bindResult result valueName body onFail = + matchResultE + onFail + (SLambda [valueName, "_"] body) + result + + -- | Build: matchResult (\msg _ -> err msg t) (\r _ -> r) result + returnResult result = + matchResultE + (SLambda ["msg", "_"] errResult) + (SLambda ["r", "_"] (SVar "r" Nothing)) + result + + -- | Build: \msg _ -> \_ -> err msg t + absorbErr = + SLambda ["msg", "_"] (SLambda ["_"] errResult) + + errResult = SApp (SApp (SVar "err" Nothing) (SVar "msg" Nothing)) TLeaf + wrapReturn Nothing b = b - wrapReturn (Just c) b = - withContractE (viewExprToAst c) b okCont errContFinal + wrapReturn (Just c) b = returnResult (withContractE (viewExprToAst c) b) wrapArgs [] b = b wrapArgs (DefBinder nm Nothing : rest) b = SLambda [nm] (wrapArgs rest b) wrapArgs (DefBinder nm (Just c) : rest) b = - let onFail = if null rest then errContFinal else errContAbsorb + let onFail = if null rest then SLambda ["msg", "_"] errResult else absorbErr in SLambda [nm] $ - withContractE (viewExprToAst c) (SVar nm Nothing) - (SLambda [nm] (wrapArgs rest b)) - onFail + bindResult + (withContractE (viewExprToAst c) (SVar nm Nothing)) + nm + (wrapArgs rest b) + onFail wrapArgs (DefPhantom _ : _) _ = error "phantom contract arguments are not yet supported by the frontend" @@ -96,12 +104,15 @@ viewExprToAst = \case VEExists _ _ -> error "exists annotations are not supported by the frontend" -- | Build an application of 'withContract' from the contract library. -withContractE :: TricuAST -> TricuAST -> TricuAST -> TricuAST -> TricuAST -withContractE contract value onOk onFail = +withContractE :: TricuAST -> TricuAST -> TricuAST +withContractE contract value = + SApp (SApp (SVar "withContract" Nothing) contract) value + +-- | Build an application of 'matchResult' from the contract library. +matchResultE :: TricuAST -> TricuAST -> TricuAST -> TricuAST +matchResultE errCase okCase result = SApp (SApp - (SApp - (SApp (SVar "withContract" Nothing) contract) - value) - onOk) - onFail + (SApp (SVar "matchResult" Nothing) errCase) + okCase) + result diff --git a/test/Spec.hs b/test/Spec.hs index f6d07f6..d817886 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -58,7 +58,7 @@ allTestLibsEnv = unsafePerformIO $ do io <- evaluateFile "./lib/io.tri" sock <- evaluateFile "./lib/socket.tri" intensional <- evaluateFile "./lib/intensionalContracts.tri" - pure (Map.unions [base, bytes, bin, http, arbor, io, sock, intensional]) + pure (injectKernel (Map.unions [base, bytes, bin, http, arbor, io, sock, intensional])) {-# NOINLINE allTestLibsEnv #-} tests :: TestTree @@ -1261,7 +1261,7 @@ contractsTests = testGroup "Contracts library tests" , "main = boom" ] env = evalTricu allTestLibsEnv (parseTricu input) - result env @?= ofString "boom" + decodeResult (result env) @?= "[t, \"boom\"]" , testCase "@ argument annotation passes" $ do let input = unlines @@ -1277,7 +1277,7 @@ contractsTests = testGroup "Contracts library tests" , "main = idNat 5" ] env = evalTricu allTestLibsEnv (parseTricu input) - result env @?= ofString "bad" + decodeResult (result env) @?= "[t, \"bad\"]" ] arithmetic :: TestTree @@ -2023,7 +2023,7 @@ contentStoreTests = testGroup "Content Store Tests" result env @?= ofNumber 5 writeFile mainPath "!import \"util\" Util\n\nmain = Util.badId 5\n" envFail <- evaluateFileWithStore (Just store) mainPath - decodeResult (result envFail) @?= "\"nope\"" + decodeResult (result envFail) @?= "[t, \"nope\"]" , testCase "Module imports: resolve manifest exports from store" $ withSystemTempDirectory "tricu-module-import" $ \dir -> do