search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Type Simplification Interface #58

Closed DavePearce closed 7 years ago

DavePearce commented 7 years ago

The concept of type simplification is largely orthogonal to the issues of subtype checking and type extraction (see #57). In essence, the main purposes are:

  1. Beautification. The primary purpose of type simplification is to give types a more readable form for the purposes of presentation (e.g. by collapsing unnecessary elements). For example, we might simply want to view int|int as int, arguing that this is more intuitive to the user.
  2. Navigation. A type simplifier could also potentially provide a means for navigating a type. In particular, by allow us to unroll the type one level at a time.
  3. Complexity. A type simplifier can also help to ensure that a type does grow arbitrarily large after successive things are added. For example, if we repeatedly intersect Expr with Value, we could end up with ((Expr&Value)&Value)&Value and if left unchecked this could lead to some kind of counting loop in the verifier.

The purpose of this issue is simply to introduce a proper type simplification interface, to go alongside the concept of an effective type and a type extractor.

DavePearce commented 7 years ago

This would be useful in the type checker when dealing with flow typing. That's because it currently creates potentially large types when dealing with boolean connectives.

DavePearce commented 7 years ago

Done as part of #84.