skeptic.analysis.conditional-arms — org.clojars.nomicflux/skeptic 0.9.0-rc1

dispatch-incompatible-with-predicate? clj

(dispatch-incompatible-with-predicate? branches k pred-info raw-path polarity)

Inputs: [branches :- [#:s{Any s/Any}] k :- s/Int pred-info :- #:s{Keyword s/Any} raw-path :- [s/Any] polarity :- s/Bool] Returns: s/Bool

True when arm K's runtime dispatch is ruled out by user assertion (pred-info, raw-path, polarity) under s/conditional first-match semantics.

Path-type-predicate descriptors are positive (the arm's predicate must be true for the arm to fire). The dispatch-order rule says:

• K's own descriptor matches (pred, path): K can dispatch only when the user's polarity is true. polarity=false drops K.
• Any j < K with a matching descriptor: K can dispatch only when j's predicate is false on the value, i.e., polarity=false. polarity=true forces j to dispatch instead, dropping K.

effective-conditional-arms clj

(effective-conditional-arms cond-type)

Inputs: [cond-type :- at/SemanticType] Returns: [at/SemanticType]

Structural type of each surviving arm post-dispatch refinement. See effective-conditional-branches.

effective-conditional-branches clj

(effective-conditional-branches cond-type)

Inputs: [cond-type :- at/SemanticType] Returns: at/ConditionalBranches

Return live branches whose effective type is narrowed by the negation of all earlier arms' recognized descriptors. Branches whose effective type is BottomType are dropped (unreachable). Unrecognized earlier descriptors are skipped.

refine-by-descriptor clj

(refine-by-descriptor arm-type descriptor)

Inputs: [arm-type :- at/SemanticType descriptor :- (s/maybe #:s{Keyword s/Any})] Returns: at/SemanticType

route-conditional-by-values clj

(route-conditional-by-values cond-type path values polarity)

Inputs: [cond-type :- at/SemanticType path :- [s/Any] values :- [s/Any] polarity :- s/Bool] Returns: (s/maybe at/SemanticType)

Fast path for value-descriptor (enumerated tagged-dispatch) narrowing: if an arm's values-descriptor exactly matches (path, values), return that arm's effective type (polarity=true) or the conditional minus that arm (polarity=false). Returns nil when no descriptor matches so callers fall back to structural refinement.

Sound because values-descriptors define mutually exclusive enumerated sets at a single path; cf. the dropped predicate-descriptor variant, which assumed mutual exclusivity it could not guarantee.

unwrap-exact-path clj

(unwrap-exact-path path)

Convert path (vector of exact-key-query records) to the raw key vector that descriptors store. Returns nil if any element is not an exact query.