Introduce Semtype witness

compiler/modules/bir/bir.bal

@@ -384,7 +384,8 @@ public type StringOperand StringConstOperand|Register;
 public type FunctionOperand FunctionRef|Register;
 
 public function operandHasType(t:Context tc, Operand operand, t:SemType semType) returns boolean {
-    return t:isSubtype(tc, operand.semType, semType);
+    t:WitnessCollector witness = new(tc);
+    return t:isSubtypeWitness(tc, operand.semType, semType, witness);
 }
 
 # Perform a arithmetic operand on ints with two operands.

compiler/modules/comm.lib/random.bal

@@ -29,7 +29,7 @@ public isolated class Random {
 
     public function randomStringValue(int len) returns string {
         int[] codePoints = [];
-        foreach int _ in 0 ... len {
+        foreach int _ in 0 ..< len {
             int r = self.nextRange(52);
             boolean upper = r < 26;
             int c = upper ? (65 + r) : (97 + r - 26); // ('A' + c) or ('a' + c)

compiler/modules/front.syntax/parseTypeTest.bal

@@ -9,6 +9,11 @@ public type TypeTest record {
     Identifier|TypeProjection right;
 };
 
+public type TypeTestWitness record {
+    *TypeTest;
+    string witness;
+};
+
 public type SubtypeTestOp "<" | "=" | "<>";
 
 public type Identifier string;
@@ -36,6 +41,21 @@ public function parseTypeTest(string str) returns TypeTest|error {
 
 }
 
+public function parseTypeTestWitness(string str) returns TypeTestWitness|error {
+    SourceFile file = createSourceFile([str], { filename: "<internal>" });
+    Tokenizer tok = new(file);
+    check tok.advance();
+    Identifier|TypeProjection left = check parseTypeProjection(tok);
+    Token? t = tok.current();
+    if t is "<" {
+        check tok.advance();
+        Identifier|TypeProjection right = check parseTypeProjection(tok);
+        string witness = check parseTypeWitness(tok);
+        return { op: "<", left, right, witness };
+    }
+    return parseError(tok);
+}
+
 function parseTypeProjection(Tokenizer tok) returns Identifier|TypeProjection|error {
     Identifier identifier = check tok.expectIdentifier();
     if tok.current() is "[" {
@@ -54,3 +74,37 @@ function parseTypeProjection(Tokenizer tok) returns Identifier|TypeProjection|er
     }
     return identifier;
 }
+
+function parseTypeWitness(Tokenizer tok) returns string|error {
+    check tok.expect("|");
+    string[] words = [];
+    while tok.curTok != () {
+        Token? curTok = tok.curTok;
+        check tok.advance();
+        if curTok != () {
+            match curTok {
+                [STRING_LITERAL, var value] => {
+                    words.push(string `"${value}"`);
+                }
+                [DECIMAL_FP_NUMBER, var digits, var suffix] => {
+                    words.push(digits.toLowerAscii() + (suffix ?: ""));
+                }
+                [_, var str] => {
+                    words.push(str);
+                }
+                var str => {
+                    string val = <string>str;
+                    if val == "}" {
+                        words.push(" ");
+                    }
+                    words.push(val);
+                    if val == "," || val == "{" || val == ":" {
+                        words.push(" ");
+                    }
+
+                }
+            }
+        }
+    }
+    return "".join(...words);
+}

compiler/modules/front.syntax/witnessExpr.bal

@@ -0,0 +1,82 @@
+import wso2/nballerina.types as t;
+
+public function typeWitnessToString(t:WitnessCollector witness) returns string {
+    t:WitnessValue value = witness.get();
+    if value is string {
+        return value;
+    }
+    else if value == () {
+        return "";
+    }
+    else {
+        Expr expr = nonStringWitnessToExpr(value);
+        return exprToString(expr);
+    }
+}
+
+public function typeWitnessToExpr(t:WitnessValue value) returns Expr {
+    if value == () || value is string {
+        return { startPos: 0, endPos: 0, value };
+    }
+    else {
+        return nonStringWitnessToExpr(value);
+    }
+}
+
+function nonStringWitnessToExpr(t:WrappedSingleValue|map<t:WitnessValue>|t:ListWitnessValue value) returns Expr {
+    if value is t:WrappedSingleValue {
+        return singleValueToLiteral(value);
+    }
+    else if value is map<t:WitnessValue> {
+        return mappingWitnessToLiteral(value);
+    }
+    else if value is t:ListWitnessValue {
+        return listWitnessToLiteral(value);
+    }
+}
+
+function listWitnessToLiteral(t:ListWitnessValue value) returns ListConstructorExpr {
+    var { memberValues, indices, fixedLen } = value;
+    Expr[] members = [];
+    foreach int i in 0 ..< memberValues.length() {
+        Expr m = typeWitnessToExpr(memberValues[i]);
+        members.push(m);
+        if i + 1 < indices.length() {
+            int nextIndex = indices[i + 1];
+            foreach var _ in members.length() ..< nextIndex {
+                members.push(m);
+            }
+        }
+    }
+
+    foreach int i in members.length() ..< fixedLen {
+        members.push(typeWitnessToExpr(memberValues[memberValues.length() - 1]));
+    }
+    return { startPos: 0, endPos: 0, opPos: 0, members };
+}
+
+function mappingWitnessToLiteral(map<t:WitnessValue> value) returns MappingConstructorExpr {
+    int startPos = 0;
+    int endPos = 0;
+    Field[] fields = from var [name, val] in value.entries()
+        select { startPos, endPos, colonPos: startPos, isIdentifier: true, name, value: typeWitnessToExpr(val) };
+    return { startPos, endPos, opPos: startPos, fields };
+}
+
+function singleValueToLiteral(t:WrappedSingleValue value) returns LiteralExpr|NumericLiteralExpr {
+    t:SingleValue v = value.value;
+    int startPos = 0;
+    int endPos = 0;
+    if v == () || v is string || v is boolean {
+        return { startPos, endPos, value: v };
+    }
+    else if v is int {
+        return { startPos, endPos, base: 10, digits: v.toString() };
+    }
+    else if v is float {
+        return { startPos, endPos, typeSuffix: "f", untypedLiteral: v.toString() };
+    }
+    else if v is decimal {
+        return { startPos, endPos, typeSuffix: "d", untypedLiteral: v.toString() };
+    }
+}

compiler/modules/types/common.bal

@@ -37,31 +37,31 @@ function and(Atom atom, Conjunction? next) returns Conjunction {
     return { atom, next };
 }
 
-type BddPredicate function(Context cx, Conjunction? pos, Conjunction? neg) returns boolean;
+type BddPredicate function(Context cx, Conjunction? pos, Conjunction? neg, WitnessCollector witness) returns boolean;
 
 // A Bdd represents a disjunction of conjunctions of atoms, where each atom is either positive or
 // negative (negated). Each path from the root to a leaf that is true represents one of the conjunctions
 // We walk the tree, accumulating the positive and negative conjunctions for a path as we go.
 // When we get to a leaf that is true, we apply the predicate to the accumulated conjunctions.
-function bddEvery(Context cx, Bdd b, Conjunction? pos, Conjunction? neg, BddPredicate predicate) returns boolean {
+function bddEvery(Context cx, Bdd b, Conjunction? pos, Conjunction? neg, BddPredicate predicate, WitnessCollector witness) returns boolean {
     if b is boolean {
-        return !b || predicate(cx, pos, neg);
+        return !b || predicate(cx, pos, neg, witness);
     }
     else {
-        return bddEvery(cx, b.left, and(b.atom, pos), neg, predicate)
-          && bddEvery(cx, b.middle, pos, neg, predicate)
-          && bddEvery(cx, b.right, pos, and(b.atom, neg), predicate); 
+        return bddEvery(cx, b.left, and(b.atom, pos), neg, predicate, witness)
+          && bddEvery(cx, b.middle, pos, neg, predicate, witness)
+          && bddEvery(cx, b.right, pos, and(b.atom, neg), predicate, witness); 
     }
 }
 
-function bddEveryPositive(Context cx, Bdd b, Conjunction? pos, Conjunction? neg, BddPredicate predicate) returns boolean {
+function bddEveryPositive(Context cx, Bdd b, Conjunction? pos, Conjunction? neg, BddPredicate predicate, WitnessCollector witness) returns boolean {
     if b is boolean {
-        return !b || predicate(cx, pos, neg);
+        return !b || predicate(cx, pos, neg, witness);
     }
     else {
-        return bddEveryPositive(cx, b.left, andIfPositive(b.atom, pos), neg, predicate)
-          && bddEveryPositive(cx, b.middle, pos, neg, predicate)
-          && bddEveryPositive(cx, b.right, pos, andIfPositive(b.atom, neg), predicate); 
+        return bddEveryPositive(cx, b.left, andIfPositive(b.atom, pos), neg, predicate, witness)
+          && bddEveryPositive(cx, b.middle, pos, neg, predicate, witness)
+          && bddEveryPositive(cx, b.right, pos, andIfPositive(b.atom, neg), predicate, witness); 
     }
 }
 

compiler/modules/types/core.bal

@@ -167,6 +167,7 @@ public isolated class Env {
 public type BddMemo record {|
     readonly Bdd bdd;
     boolean? isEmpty = ();
+    WitnessValue? witness = ();
 |};
 
 type BddMemoTable table<BddMemo> key(bdd);
@@ -248,6 +249,7 @@ type UniformSubtype [UniformTypeCode, ProperSubtypeData];
 type BinOp function(SubtypeData t1, SubtypeData t2) returns SubtypeData;
 type UnaryOp function(SubtypeData t) returns SubtypeData;
 type UnaryTypeCheckOp function(Context cx, SubtypeData t) returns boolean;
+type UnaryTypeCheckWitnessOp function(Context cx, SubtypeData t, WitnessCollector w) returns boolean;
 
 function binOpPanic(SubtypeData t1, SubtypeData t2) returns SubtypeData {
     panic error("binary operation should not be called");
@@ -261,12 +263,17 @@ function unaryTypeCheckOpPanic(Context cx, SubtypeData t) returns boolean {
     panic error("unary boolean operation should not be called");
 }
 
+function unaryTypeCheckOpWitnessPanic(Context cx, SubtypeData t, WitnessCollector w) returns boolean {
+    panic error("unary boolean operation should not be called");
+}
+
 type UniformTypeOps readonly & record {|
     BinOp union = binOpPanic;
     BinOp intersect = binOpPanic;
     BinOp diff = binOpPanic;
     UnaryOp complement = unaryOpPanic;
     UnaryTypeCheckOp isEmpty = unaryTypeCheckOpPanic;
+    UnaryTypeCheckWitnessOp? isEmptyWitness = ();
 |};
 
 final readonly & (UniformSubtype[]) EMPTY_SUBTYPES = [];
@@ -769,11 +776,47 @@ public function isEmpty(Context cx, SemType t) returns boolean {
         return true;
     }
 }
+
+public function isEmptyWitness(Context cx, SemType t, WitnessCollector w) returns boolean {
+    if t is UniformTypeBitSet {
+        boolean noBits = t == 0;
+        if !noBits {
+            w.allOfTypes(t);
+        }
+        return noBits;
+    }
+    else {
+        if t.all != 0 {
+            // includes all of one or more uniform types
+            w.allOfTypes(t.all);
+            return false;
+        }
+        foreach var st in unpackComplexSemType(t) {
+            var [code, data] = st;
+            var isEmptyWitness = ops[code].isEmptyWitness;
+            if isEmptyWitness != () {
+                if !isEmptyWitness(cx, data, w) {
+                    return false;
+                }
+            }
+            var isEmpty = ops[code].isEmpty;
+            if !isEmpty(cx, data) {
+                return false;
+            }
+
+        }
+        return true;
+    }
+}
 
 public function isSubtype(Context cx, SemType t1, SemType t2) returns boolean { 
     return isEmpty(cx, diff(t1, t2));
 }
 
+public function isSubtypeWitness(Context cx, SemType t1, SemType t2, WitnessCollector w) returns boolean { 
+    return isEmptyWitness(cx, diff(t1, t2), w);
+}
+
 public function includesSome(SemType t1, SemType t2) returns boolean {
     return !isNever(intersect(t1, t2));
 }

compiler/modules/types/error.bal

@@ -42,8 +42,37 @@ function errorSubtypeIsEmpty(Context cx, SubtypeData t) returns boolean {
             return res;
         }
     }
-    boolean isEmpty = bddEveryPositive(cx, b, (), (), mappingFormulaIsEmpty);
+    // todo: Need to handle witness handling for this scenario
+    WitnessCollector witness = new(cx);
+    boolean isEmpty = bddEveryPositive(cx, b, (), (), mappingFormulaIsEmpty, witness);
     m.isEmpty = isEmpty;
+    m.witness = witness.get();
+    return isEmpty;    
+}
+
+function errorSubtypeIsEmptyWitness(Context cx, SubtypeData t, WitnessCollector witness) returns boolean {
+    Bdd b = bddFixReadOnly(<Bdd>t);
+    BddMemo? mm = cx.mappingMemo[b];
+    BddMemo m;
+    if mm == () {
+        m = { bdd: b };
+        cx.mappingMemo.add(m);
+        // todo: memoize witness
+    }
+    else {
+        m = mm;
+        boolean? res = m.isEmpty;
+        if res == () {
+            return true;
+        }
+        else {
+            return res;
+        }
+    }
+    // todo: Need to handle witness handling for this scenario
+    boolean isEmpty = bddEveryPositive(cx, b, (), (), mappingFormulaIsEmpty, witness);
+    m.isEmpty = isEmpty;
+    m.witness = witness.get();
     return isEmpty;    
 }
 
@@ -52,7 +81,8 @@ final UniformTypeOps errorOps = {
     intersect: bddSubtypeIntersect,
     diff: bddSubtypeDiff,
     complement: bddSubtypeComplement,
-    isEmpty: errorSubtypeIsEmpty
+    isEmpty: errorSubtypeIsEmpty,
+    isEmptyWitness: errorSubtypeIsEmptyWitness
 };
 
 

compiler/modules/types/function.bal

@@ -28,12 +28,17 @@ public class FunctionDefinition {
 }
 
 function functionSubtypeIsEmpty(Context cx, SubtypeData t) returns boolean {
+    return functionSubtypeIsEmptyWitness(cx, t, new(cx));    
+}
+
+function functionSubtypeIsEmptyWitness(Context cx, SubtypeData t, WitnessCollector witness) returns boolean {
     Bdd b = <Bdd>t;
     BddMemo? mm = cx.functionMemo[b];
     BddMemo m;
     if mm == () {
         m = { bdd: b };
         cx.functionMemo.add(m);
+        // todo: memoize witness
     }
     else {
         m = mm;
@@ -48,12 +53,13 @@ function functionSubtypeIsEmpty(Context cx, SubtypeData t) returns boolean {
             return res;
         }
     }
-    boolean isEmpty = bddEvery(cx, b, (), (), functionFormulaIsEmpty);
+    boolean isEmpty = bddEvery(cx, b, (), (), functionFormulaIsEmpty, witness);
     m.isEmpty = isEmpty;
+    m.witness = witness.get();
     return isEmpty;    
 }
 
-function functionFormulaIsEmpty(Context cx, Conjunction? pos, Conjunction? neg) returns boolean {
+function functionFormulaIsEmpty(Context cx, Conjunction? pos, Conjunction? neg, WitnessCollector? witness) returns boolean {
     return functionPathIsEmpty(cx, functionUnionParams(cx, pos), pos, neg);
 }
 
@@ -112,5 +118,6 @@ UniformTypeOps functionOps =  {
     intersect: bddSubtypeIntersect,
     diff: bddSubtypeDiff,
     complement: bddSubtypeComplement,
-    isEmpty: functionSubtypeIsEmpty
+    isEmpty: functionSubtypeIsEmpty,
+    isEmptyWitness:  functionSubtypeIsEmptyWitness
 };