Clef.Spec.Witnesses

Spec: operation witnesses

How an operation finds its implementation. A model of the witness resolution in Inference and Constraint Solving: statically resolved member constraints are solved against the native witness hierarchy, at compile time.

From Clef Require Import Spec.Types Spec.Runtime.

The operations a program can apply: operators and statically resolved members.

Parameter op : Type.

References

Used by

The result type of an operation at an argument type, or None where the type has no witness for it. It is a function, so resolution has at most one answer.

Parameter witness : op -> ty -> option ty.

References

Uses

ty
op
option

Used by

What an operation computes on a value, or None where it is stuck.

Parameter apply : op -> val -> option val.

References

Uses

val
op
option

Used by

A witness is implemented, and its implementation has the type the witness declares. An operation applied at a type with a witness returns a value of the witness's result type.

Axiom witness_sound :

  forall (o : op) (a r : ty) (v : val),
    witness o a = Some r -> has_ty v a ->
    exists w, apply o v = Some w /\ has_ty w r.

References

Uses

Used by

specialization_is_safe