skeptic.analysis.origin — org.clojars.nomicflux/skeptic 0.8.0

apply-assumption-to-root-type clj

(apply-assumption-to-root-type type assumption)

Inputs: [type :- ats/SemanticType assumption :- aos/Assumption] Returns: ats/SemanticType

apply-guard-assumption clj

(apply-guard-assumption ctx assumption)

Inputs: [ctx :- s/Any assumption :- (s/maybe aos/Assumption)] Returns: s/Any

assumption-base-type clj

(assumption-base-type assumption assumptions)

Inputs: [assumption :- aos/RootedAssumption assumptions :- [aos/Assumption]] Returns: ats/SemanticType

assumption-root? clj

(assumption-root? assumption root)

Inputs: [assumption :- aos/Assumption root :- aos/RootOrigin] Returns: s/Bool

assumption-truth clj

(assumption-truth assumption assumptions)

Inputs: [assumption :- aos/Assumption assumptions :- [aos/Assumption]] Returns: aos/AssumptionTruth

blank-check-assumption clj

(blank-check-assumption root polarity)

Inputs: [root :- s/Any polarity :- s/Bool] Returns: aos/BlankCheckAssumption

branch-local-envs clj

(branch-local-envs ctx locals assumptions conjuncts)

Inputs: [ctx :- s/Any locals :- s/Any assumptions :- [aos/Assumption] conjuncts :- aos/Conjuncts] Returns: aos/BranchEnvs

branch-origin clj

(branch-origin test then-origin else-origin)

Inputs: [test :- s/Any then-origin :- s/Any else-origin :- s/Any] Returns: aos/BranchOrigin

call-arg-contract-assumptions clj

(call-arg-contract-assumptions node)

Inputs: [node :- (s/maybe aas/AnnotatedNode)] Returns: [aos/TypePredicateAssumption]

conjunction-assumption clj

(conjunction-assumption parts)

Inputs: [parts :- s/Any] Returns: aos/ConjunctionAssumption

contains-key-assumption clj

(contains-key-assumption root key polarity)

Inputs: [root :- s/Any key :- s/Any polarity :- s/Bool] Returns: aos/ContainsKeyAssumption

contains-key-test-assumption clj

(contains-key-test-assumption ctx target-node key)

Inputs: [ctx :- s/Any target-node :- s/Any key :- s/Any] Returns: (s/maybe aos/Assumption)

disjunction-assumption clj

(disjunction-assumption parts)

Inputs: [parts :- s/Any] Returns: aos/DisjunctionAssumption

effective-type clj

(effective-type ctx sym entry assumptions)

Inputs: [ctx :- s/Any sym :- s/Any entry :- s/Any assumptions :- [aos/Assumption]] Returns: ats/SemanticType

guard-assumption clj

(guard-assumption stmt-node)

Inputs: [stmt-node :- s/Any] Returns: (s/maybe aos/Assumption)

if-test-conjuncts clj

(if-test-conjuncts ctx test-node locals)

Inputs: [ctx :- s/Any test-node :- s/Any locals :- s/Any] Returns: aos/Conjuncts

invert-assumption clj

(invert-assumption assumption)

Inputs: [assumption :- aos/Assumption] Returns: (s/maybe aos/Assumption)

local-binding-init-assumption clj

(local-binding-init-assumption ctx test-node locals)

Inputs: [ctx :- s/Any test-node :- s/Any locals :- s/Any] Returns: (s/maybe aos/Assumption)

local-root-origin clj

(local-root-origin ctx node)

Inputs: [ctx :- s/Any node :- s/Any] Returns: (s/maybe aos/RootOrigin)

map-key-lookup-origin clj

(map-key-lookup-origin root path defaults)

Inputs: [root :- s/Any path :- s/Any defaults :- s/Any] Returns: aos/MapKeyLookupOrigin

map-key-lookup-origin-value clj

(map-key-lookup-origin-value origin)

Inputs: [origin :- s/Any] Returns: s/Any

node-origin clj

(node-origin node)

Inputs: [node :- s/Any] Returns: (s/maybe aos/Origin)

opaque-origin clj

(opaque-origin type)

Inputs: [type :- ats/SemanticType] Returns: aos/Origin

opposite-assumption? clj

(opposite-assumption? left right)

Inputs: [left :- aos/Assumption right :- aos/Assumption] Returns: s/Bool

opposite-polarity clj

(opposite-polarity assumption)

Inputs: [assumption :- aos/Assumption] Returns: (s/maybe aos/Assumption)

origin-type clj

(origin-type origin assumptions)

Inputs: [origin :- aos/Origin assumptions :- [aos/Assumption]] Returns: ats/SemanticType

path-type-predicate-assumption clj

(path-type-predicate-assumption root path pred-info polarity)

Inputs: [root :- s/Any path :- s/Any pred-info :- aos/PredInfo polarity :- s/Bool] Returns: aos/PathTypePredicateAssumption

path-value-equality-assumption clj

(path-value-equality-assumption root path values polarity)

Inputs: [root :- s/Any path :- s/Any values :- [s/Any] polarity :- s/Bool] Returns: aos/PathValueEqualityAssumption

refine-locals-for-assumption clj

(refine-locals-for-assumption ctx locals assumptions)

Inputs: [ctx :- s/Any locals :- s/Any assumptions :- [aos/Assumption]] Returns: s/Any

refine-root-type clj

(refine-root-type root assumptions)

Inputs: [root :- aos/RootOrigin assumptions :- [aos/Assumption]] Returns: ats/SemanticType

region-conjuncts clj

(region-conjuncts ctx node locals)

(region-conjuncts ctx node locals alias-map)

Inputs: ([ctx :- s/Any node :- s/Any locals :- s/Any] [ctx :- s/Any node :- s/Any locals :- s/Any alias-map :- s/Any]) Returns: aos/Conjuncts

Return {:then-conjuncts [...] :else-conjuncts [...]} of conjuncts known true in each region (truthy/falsy) of node, derived structurally from let+if shapes. No and/or vocabulary: the only signal is which branch of an if carries the test-local. Truth tables: (if g g y) — false-region: ¬g ∧ ¬y (conjunction); true-region: ¬g ∨ ¬y (disjunction) (if g y g) — true-region: g ∧ y (conjunction); false-region: ¬g ∨ ¬y (disjunction) alias-map maps let-bound syms to their init expressions so when a let-bound local appears as the if-test we narrow on the underlying expression.

root-origin clj

(root-origin sym type)

Inputs: [sym :- s/Any type :- ats/SemanticType] Returns: aos/RootOrigin

root-origin-value clj

(root-origin-value origin)

Inputs: [origin :- s/Any] Returns: s/Any

same-assumption-proposition? clj

(same-assumption-proposition? a b)

Inputs: [a :- aos/Assumption b :- aos/Assumption] Returns: s/Bool

Same narrowed fact on the same root, ignoring branch polarity.

same-assumption? clj

(same-assumption? left right)

Inputs: [left :- aos/Assumption right :- aos/Assumption] Returns: s/Bool

simplify-assumptions clj

(simplify-assumptions assumptions)

Inputs: [assumptions :- [aos/Assumption]] Returns: [aos/Assumption]

Simplify environment assumptions. This is a pure query pass: it asks assumption-truth, which may reach type refinement, but it does not mutate state or recursively invoke simplification.

test->assumption clj

(test->assumption ctx test-node)

Inputs: [ctx :- s/Any test-node :- s/Any] Returns: (s/maybe aos/Assumption)

truthy-local-assumption clj

(truthy-local-assumption root polarity)

Inputs: [root :- s/Any polarity :- s/Bool] Returns: aos/TruthyLocalAssumption

type-predicate-assumption clj

(type-predicate-assumption root pred-info polarity)

Inputs: [root :- s/Any pred-info :- aos/PredInfo polarity :- s/Bool] Returns: aos/TypePredicateAssumption

value-equality-assumption clj

(value-equality-assumption root values polarity)

Inputs: [root :- s/Any values :- [s/Any] polarity :- s/Bool] Returns: aos/ValueEqualityAssumption