update documentation regarding CASE with type guards

doc/wiki/Original-report-refinements.md

@@ -67,4 +67,48 @@ All variables have zero as a default value (before first assignment). For pointe
     VAR r: RECORD field: INTEGER END;
     BEGIN
         ASSERT(r.field = 0);
-    END m.
+    END m.
+
+3. CASE with type guards
+------------------------
+CASE with type guard has notorious loophole allowing to violate type system. Consider following example:
+
+    MODULE test;
+    TYPE
+        Base = RECORD END; 
+        Derived1 = POINTER TO RECORD(Base) derived1Field: INTEGER END;
+        Derived2 = POINTER TO RECORD(Base) END;
+    VAR p: POINTER TO Base; p1: Derived1; p2: Derived2;
+
+    PROCEDURE assignToDerived2();
+    BEGIN
+        NEW(p2);
+        p := p2;
+    END assignToDerived2;
+
+    PROCEDURE check();
+    BEGIN
+        CASE p OF
+            Derived1: 
+                assignToDerived2(); (* p is not Derived1 anymore *)
+                p.derived1Field := 123; (* type system violation *)
+        END;
+    END check;
+
+    BEGIN
+        NEW(p1);
+        p := p1;
+        check();
+    END test.
+
+Oberonjs does not change the type of pointer passed as VAR argument in CASE to reduce most unexpected bugs (referenced pointer can be changed indirectly):
+
+    PROCEDURE check(VAR p: PBase);
+    BEGIN
+        CASE p OF
+            Derived1: 
+                (* this code is compiled successfully but 'p' has type PBase here, not Derived1 *)
+        END;
+    END check;
+
+I would recommend to use Eberon's [[implicit type narrowing|Eberon-implicit-type-narrowing]] instead of CASE with type guards - it is as efficient as CASE but does not have described problem. 

doc/wiki/eberon-implicit-type-narrowing.md

@@ -1,21 +1,4 @@
-Original Oberon-07 has no facility for runtime type testing combined with type casting into single operation. It leads to extra code to write (for a person) and extra operations to run (for a computer). Consider following example:
-
-    TYPE
-        Base = RECORD END;
-        PBase = POINTER TO Base;
-        Derived = RECORD (Base) derivedField: INTEGER END;
-        PDerived = POINTER TO Derived;
-    VAR
-        pb: PBase;
-    BEGIN
-        IF pb IS PDerived THEN
-            pb(PDerived).derivedField := 123;
-        END;
-
-        ASSERT(~(pb IS PDerived) OR (pb(PDerived).derivedField = 123));
-    END.
-
-As you can see here there are two separate operations - type test and then type cast. *Implicit type narrowing* is introduced to resolve this problem.
+Original Oberon-07 CASE with type guards has [[notorious loophole|Original-report-refinements#3-case-with-type-guards]]. *Implicit type narrowing* is introduced as alternative solution without possible type violation problem.
 
 The idea of *implicit type narrowing* is to make the compiler smart enough to comprehend that type testing (using IS) and following IF branch or logical conjunction (&) in expression narrows just tested variable type. The same type narrowing happens in the inverse case: logical not (~) for IS operation and following ELSE branch or logical disjunction (OR). Also compiler should guarantee that tested variable is not modified after type narrowing so there is no loopholes to corrupt type system by chance. That guarantee is easy to reach in case of [[In Place Variables|eberon-in-place-variables]] because their scope is very local and they cannot be modified by local procedures. Type narrowing is also appling to procedure arguments because they [[cannot be modified|Eberon-non-VAR-arguments-are-read-only]]. So if the example will use *pb* variable as *in place* variable then it will be compiled without addition type casts: