From 3495584667fe763422b598d4984529afd19ccec0 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 8 Sep 2016 11:30:36 -0400 Subject: [PATCH] update rosette notes about Constant subtyping rule(s) --- turnstile/examples/rosette/rosette-notes.txt | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt index fa661e3..b58f9c6 100644 --- a/turnstile/examples/rosette/rosette-notes.txt +++ b/turnstile/examples/rosette/rosette-notes.txt @@ -1,6 +1,6 @@ 2016-09-08 -Typed Rosette tricky subtyping examples +Typed Rosette tricky subtyping examples: ) Both these should be true: @@ -21,7 +21,19 @@ But then, (U (Constant Int)) <: (U Int), which should *not* hold. Bad alternative: lift Constant out of U Con: non-constant values, eg (if b i1 i2) will be recognized as "constant" -Current solution: disallow first case +*Current design choice*: disallow first case + +Another alternative: get rid of Constant altogether? + +SUMMARY: +Here are the above two cases in canonical form: + +(Constant* (U* CInt)) <: (U* (Constant* (U* CInt)) (Constant* (U* CBool))) +(Constant* (U* CInt)) <: (U* CInt) + +The problem is that each case requires a different rule but the outer type +constructors are insufficient for determining which rule use. + 2016-09-02 --------------------