src/contracts.bend source
src/contracts.bend on the hub · documented module
import Basetype Param is Data: Param{name: String, value: String}type Match is Data: Matched{params: List<&2, Param>} NoMatch{}def prepend(name: String, value: String, result: Match) -> Match: match result: case Matched{params}: Matched{Param{name, value} <> params} case NoMatch{}: NoMatch{}def literal(same: Bool, next: Unit -> Match) -> Match: match same: case True{}: next(Unit{}) case False{}: NoMatch{}def capture(parameter: Bool, pattern: String, +name: String, +value: String, next: Unit -> Match) -> Match: match parameter: case True{}: literal(Bool.and(Bool.not(String.is_empty(name)), Bool.not(String.is_empty(value))), u => prepend(name, value, next(Unit{}))) case False{}: literal(String.eq(pattern, value), next)def segment(pattern: String, +value: String, next: Unit -> Match) -> Match: match pattern: case SNil{}: literal(String.is_empty(value), next) case SCon{+head, +tail}: capture(Char.is_eq(head, ':'), SCon{head, tail}, tail, value, next)def values(patterns: List<&2, String>, path: List<&2, String>) -> Match: match patterns path: case Nil{} Nil{}: Matched{Nil{}} case Con{pattern, tail} Con{head, rest}: segment(pattern, head, u => values(tail, rest)) case other other_path: NoMatch{}def match_path(pattern: String, path: String) -> Match: values(String.split(pattern, '/'), String.split(path, '/'))def param_step(found: Bool, value: String, next: Unit -> Maybe<String>) -> Maybe<String>: match found: case True{}: Some{value} case False{}: next(Unit{})def param(+name: String, params: List<&2, Param>) -> Maybe<String>: match params: case Nil{}: None{} case Con{Param{key, value}, tail}: param_step(String.eq(name, key), value, u => param(name, tail))def has_method(+name: String, names: List<&2, String>) -> Bool: match names: case Nil{}: False{} case head <> tail: Bool.or(String.eq(name, head), has_method(name, tail))def unique(found: Bool, name: String, names: List<&2, String>) -> List<&2, String>: match found: case True{}: names case False{}: name <> names# Metadata is data, not an effectful handler registry. IDs are application-owned.type Route is Data: Route{id: Nat, method: String, pattern: String, protected: Bool, statuses: List<&2, Nat>}type Selection is Data: Found{route: Route, params: List<&2, Param>} Missing{} WrongMethod{methods: List<&2, String>}type Response<-B: Data> is Data: Reply{status: Nat, body: B} Error{status: Nat, code: String, allow: List<&2, String>}type Decision<-S: Data, -B: Data> is Data: Decision{state: S, response: Response<B>}def add_allowed(+method: String, result: Selection) -> Selection: match result: case Found{route, params}: Found{route, params} case Missing{}: WrongMethod{[method]} case WrongMethod{+methods}: WrongMethod{unique(has_method(method, methods), method, methods)}def chosen(same: Bool, +route: Route, params: List<&2, Param>, rest: Selection) -> Selection: match same: case True{}: Found{route, params} case False{}: match route: case Route{id, method, pattern, protected, statuses}: add_allowed(method, rest)def matched(result: Match, same: Bool, route: Route, rest: Selection) -> Selection: match result: case Matched{params}: chosen(same, route, params, rest) case NoMatch{}: restdef select(routes: List<&2, Route>, +method: String, +path: String) -> Selection: match routes: case Nil{}: Missing{} case +route <> tail: match route: case Route{id, +verb, pattern, protected, statuses}: matched(match_path(pattern, path), String.eq(verb, method), route, select(tail, method, path))def readonly(+method: String) -> Bool: Bool.or(String.eq(method, "GET"), String.eq(method, "HEAD"))# Restore the complete modeled state for reads. There are no effects to undo.def preserve(-S: Data, -B: Data, read: Bool, original: S, proposed: Decision<S, B>) -> Decision<S, B>: match read: case True{}: match proposed: case Decision{state, response}: Decision{original, response} case False{}: proposed# The guard receives a pure continuation, never IO. Denial cannot execute it.def authorize(-S: Data, -B: Data, protected: Bool, valid: Bool, +state: S, next: S -> Decision<S, B>) -> Decision<S, B>: match protected valid: case True{} False{}: Decision{state, Error{401n, "unauthorized", Nil{}}} case other other_valid: next(state)def run(-S: Data, -B: Data, selection: Selection, read: Bool, valid: Bool, +state: S, next: Route -> List<&2, Param> -> S -> Decision<S, B>) -> Decision<S, B>: match selection: case Missing{}: Decision{state, Error{404n, "not_found", Nil{}}} case WrongMethod{methods}: Decision{state, Error{405n, "method_not_allowed", methods}} case Found{+route, params}: match route: case Route{id, method, pattern, protected, statuses}: authorize(S, B, protected, valid, state, +s => preserve(S, B, read, s, next(route, params, s)))def dispatch(-S: Data, -B: Data, routes: List<&2, Route>, +method: String, path: String, valid: Bool, state: S, next: Route -> List<&2, Param> -> S -> Decision<S, B>) -> Decision<S, B>: run(S, B, select(routes, method, path), readonly(method), valid, state, next)def state(-S: Data, -B: Data, decision: Decision<S, B>) -> S: match decision: case Decision{state, response}: statedef response(-S: Data, -B: Data, decision: Decision<S, B>) -> Response<B>: match decision: case Decision{state, response}: responsedef status(-B: Data, response: Response<B>) -> Nat: match response: case Reply{status, body}: status case Error{status, code, allow}: statusdef contains(statuses: List<&2, Nat>, +status: Nat) -> Bool: match statuses: case Nil{}: False{} case head <> tail: Bool.or(Nat.is_eq(head, status), contains(tail, status))# Declare 401 on protected routes; 404/405 belong to the router, not a handler.# This observation does not repair a wrong status: prove it True in app laws.def declared(-B: Data, route: Route, response: Response<B>) -> Bool: match route: case Route{id, method, pattern, protected, statuses}: contains(statuses, status(B, response))