[NF] Improve error checking of when-clauses.

Compiler/NFFrontEnd/NFExpression.mo

@@ -133,27 +133,45 @@ public
 	    ock := match ick
 	      local
 	        Expression i, ic, r, c, si, sm;
-	      case (INFERRED_CLOCK()) then DAE.INFERRED_CLOCK();
-	      case (INTEGER_CLOCK(i, r)) then DAE.INTEGER_CLOCK(Expression.toDAE(i), Expression.toDAE(r));
-	      case (REAL_CLOCK(i)) then DAE.REAL_CLOCK(Expression.toDAE(i));
-	      case (BOOLEAN_CLOCK(c, si)) then DAE.BOOLEAN_CLOCK(Expression.toDAE(c), Expression.toDAE(si));
-	      case (SOLVER_CLOCK(c, sm)) then DAE.SOLVER_CLOCK(Expression.toDAE(c), Expression.toDAE(sm));
+	      case INFERRED_CLOCK()     then DAE.INFERRED_CLOCK();
+	      case INTEGER_CLOCK(i, r)  then DAE.INTEGER_CLOCK(Expression.toDAE(i), Expression.toDAE(r));
+	      case REAL_CLOCK(i)        then DAE.REAL_CLOCK(Expression.toDAE(i));
+	      case BOOLEAN_CLOCK(c, si) then DAE.BOOLEAN_CLOCK(Expression.toDAE(c), Expression.toDAE(si));
+	      case SOLVER_CLOCK(c, sm)  then DAE.SOLVER_CLOCK(Expression.toDAE(c), Expression.toDAE(sm));
 	    end match;
 	  end toDAE;
 
-    function toString
+    function toDebugString
       input ClockKind ick;
       output String ock;
     algorithm
       ock := match ick
         local
           Expression i, ic, r, c, si, sm;
-        case (INFERRED_CLOCK()) then "INFERRED_CLOCK()";
-        case (INTEGER_CLOCK(i, r)) then "INTEGER_CLOCK(" + Expression.toString(i) + ", " + Expression.toString(r) + ")";
-        case (REAL_CLOCK(i)) then "REAL_CLOCK(" + Expression.toString(i) + ")";
-        case (BOOLEAN_CLOCK(c, si)) then "BOOLEAN_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(si) + ")";
-        case (SOLVER_CLOCK(c, sm)) then "SOLVER_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(sm) + ")";
+        case INFERRED_CLOCK()     then "INFERRED_CLOCK()";
+        case INTEGER_CLOCK(i, r)  then "INTEGER_CLOCK(" + Expression.toString(i) + ", " + Expression.toString(r) + ")";
+        case REAL_CLOCK(i)        then "REAL_CLOCK(" + Expression.toString(i) + ")";
+        case BOOLEAN_CLOCK(c, si) then "BOOLEAN_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(si) + ")";
+        case SOLVER_CLOCK(c, sm)  then "SOLVER_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(sm) + ")";
+      end match;
+    end toDebugString;
+
+    function toString
+      input ClockKind ck;
+      output String str;
+    algorithm
+      str := match ck
+        local
+          Expression e1, e2;
+
+        case INFERRED_CLOCK()      then "";
+        case INTEGER_CLOCK(e1, e2) then Expression.toString(e1) + ", " + Expression.toString(e2);
+        case REAL_CLOCK(e1)        then Expression.toString(e1);
+        case BOOLEAN_CLOCK(e1, e2) then Expression.toString(e1) + ", " + Expression.toString(e2);
+        case SOLVER_CLOCK(e1, e2)  then Expression.toString(e1) + ", " + Expression.toString(e2);
       end match;
+
+      str := "Clock(" + str + ")";
     end toString;
 	end ClockKind;
 
@@ -1480,7 +1498,7 @@ public
       case ENUM_LITERAL(ty = t as Type.ENUMERATION())
         then Absyn.pathString(t.typePath) + "." + exp.name;
 
-      case CLKCONST(clk) then "CLKCONST(" + ClockKind.toString(clk) + ")";
+      case CLKCONST(clk) then ClockKind.toString(clk);
 
       case CREF() then ComponentRef.toString(exp.cref);
       case TYPENAME() then Type.typenameString(Type.arrayElementType(exp.ty));

Compiler/NFFrontEnd/NFInst.mo

@@ -100,6 +100,7 @@ import Record = NFRecord;
 import Variable = NFVariable;
 import OperatorOverloading = NFOperatorOverloading;
 import EvalConstants = NFEvalConstants;
+import VerifyModel = NFVerifyModel;
 
 public
 function instClassInProgram
@@ -160,6 +161,8 @@ algorithm
   flat_model := SimplifyModel.simplify(flat_model);
   funcs := Flatten.collectFunctions(flat_model, name);
 
+  VerifyModel.verify(flat_model);
+
   // Collect package constants that couldn't be substituted with their values
   // (e.g. because they where used with non-constant subscripts), and add them
   // to the model.
@@ -2738,11 +2741,6 @@ algorithm
       algorithm
         exp1 := instExp(scodeEq.expLeft, scope, info);
         exp2 := instExp(scodeEq.expRight, scope, info);
-
-        if ExpOrigin.flagSet(origin, ExpOrigin.WHEN) and not checkLhsInWhen(exp1) then
-          Error.addSourceMessage(Error.WHEN_EQ_LHS, {Expression.toString(exp1)}, info);
-          fail();
-        end if;
       then
         Equation.EQUALITY(exp1, exp2, Type.UNKNOWN(), makeSource(scodeEq.comment, info));
 
@@ -3052,23 +3050,6 @@ algorithm
   scope := InstNode.addIterator(iterator, scope);
 end addIteratorToScope;
 
-function checkLhsInWhen
-  input Expression exp;
-  output Boolean isValid;
-algorithm
-  isValid := match exp
-    case Expression.CREF() then true;
-    case Expression.TUPLE()
-      algorithm
-        for e in exp.elements loop
-          checkLhsInWhen(e);
-        end for;
-      then
-        true;
-    else false;
-  end match;
-end checkLhsInWhen;
-
 function insertGeneratedInners
   "Inner elements can be generated automatically during instantiation if they're
    missing, and are stored in the cache of the top scope since that's easily
@@ -3144,7 +3125,7 @@ algorithm
       algorithm
         for c in cls_tree.components loop
           if not InstNode.isEmpty(c) then
-          updateImplicitVariabilityComp(c, evalAllParams);
+            updateImplicitVariabilityComp(c, evalAllParams);
           end if;
         end for;
 

Compiler/NFFrontEnd/NFType.mo

@@ -237,6 +237,16 @@ public
     end match;
   end isString;
 
+  function isClock
+    input Type ty;
+    output Boolean isClock;
+  algorithm
+    isClock := match ty
+      case CLOCK() then true;
+      else false;
+    end match;
+  end isClock;
+
   function isScalar
     input Type ty;
     output Boolean isScalar;

Compiler/NFFrontEnd/NFTyping.mo

@@ -136,6 +136,7 @@ package ExpOrigin
   constant Type CONNECT         = intBitLShift(1, 17); // Part of connect argument.
   constant Type NOEVENT         = intBitLShift(1, 18); // Part of noEvent argument.
   constant Type ASSERT          = intBitLShift(1, 19); // Part of assert argument.
+  constant Type CLOCKED         = intBitLShift(1, 20); // Part of a clocked equation.
 
   // Combined flags:
   constant Type EQ_SUBEXPRESSION = intBitOr(EQUATION, SUBEXPRESSION);
@@ -2348,24 +2349,8 @@ algorithm
       Integer next_origin;
       SourceInfo info;
 
-    case Equation.EQUALITY()
-      algorithm
-        info := ElementSource.getInfo(eq.source);
-        (e1, ty1) := typeExp(eq.lhs, ExpOrigin.setFlag(origin, ExpOrigin.LHS), info);
-        (e2, ty2) := typeExp(eq.rhs, ExpOrigin.setFlag(origin, ExpOrigin.RHS), info);
-        (e1, e2, ty, mk) := TypeCheck.matchExpressions(e1, ty1, e2, ty2);
-
-        if TypeCheck.isIncompatibleMatch(mk) then
-          Error.addSourceMessage(Error.EQUATION_TYPE_MISMATCH_ERROR,
-            {Expression.toString(e1) + " = " + Expression.toString(e2),
-             Type.toString(ty1) + " = " + Type.toString(ty2)}, info);
-          fail();
-        end if;
-      then
-        Equation.EQUALITY(e1, e2, ty, eq.source);
-
-    case Equation.CONNECT()
-      then typeConnect(eq.lhs, eq.rhs, origin, eq.source);
+    case Equation.EQUALITY() then typeEqualityEquation(eq.lhs, eq.rhs, origin, eq.source);
+    case Equation.CONNECT()  then typeConnect(eq.lhs, eq.rhs, origin, eq.source);
 
     case Equation.FOR()
       algorithm
@@ -2385,24 +2370,7 @@ algorithm
         Equation.FOR(eq.iterator, SOME(e1), body, eq.source);
 
     case Equation.IF() then typeIfEquation(eq.branches, origin, eq.source);
-
-    case Equation.WHEN()
-      algorithm
-        next_origin := ExpOrigin.setFlag(origin, ExpOrigin.WHEN);
-
-        tybrs := list(
-          match br
-            case Equation.Branch.BRANCH(condition = cond, body = body)
-              algorithm
-                (e1, var) := typeCondition(cond, origin, eq.source,
-                  Error.WHEN_CONDITION_TYPE_ERROR, allowVector = true);
-                eqs1 := list(typeEquation(beq, next_origin) for beq in body);
-              then
-                Equation.makeBranch(e1, eqs1, var);
-          end match
-        for br in eq.branches);
-      then
-        Equation.WHEN(tybrs, eq.source);
+    case Equation.WHEN() then typeWhenEquation(eq.branches, origin, eq.source);
 
     case Equation.ASSERT()
       algorithm
@@ -2543,6 +2511,23 @@ algorithm
   end match;
 end checkConnectorForm;
 
+function checkLhsInWhen
+  input Expression exp;
+  output Boolean isValid;
+algorithm
+  isValid := match exp
+    case Expression.CREF() then true;
+    case Expression.TUPLE()
+      algorithm
+        for e in exp.elements loop
+          checkLhsInWhen(e);
+        end for;
+      then
+        true;
+    else false;
+  end match;
+end checkLhsInWhen;
+
 function typeAlgorithm
   input output Algorithm alg;
   input ExpOrigin.Type origin;
@@ -2686,34 +2671,61 @@ algorithm
   end match;
 end typeStatement;
 
+function typeEqualityEquation
+  input Expression lhsExp;
+  input Expression rhsExp;
+  input ExpOrigin.Type origin;
+  input DAE.ElementSource source;
+  output Equation eq;
+protected
+  SourceInfo info = ElementSource.getInfo(source);
+  Expression e1, e2;
+  Type ty1, ty2, ty;
+  MatchKind mk;
+algorithm
+  if ExpOrigin.flagSet(origin, ExpOrigin.WHEN) and
+     ExpOrigin.flagNotSet(origin, ExpOrigin.CLOCKED) then
+    if checkLhsInWhen(lhsExp) then
+      Expression.fold(lhsExp, Inst.markStructuralParamsSubs, 0);
+    else
+      Error.addSourceMessage(Error.WHEN_EQ_LHS, {Expression.toString(lhsExp)}, info);
+      fail();
+    end if;
+  end if;
+
+  (e1, ty1) := typeExp(lhsExp, ExpOrigin.setFlag(origin, ExpOrigin.LHS), info);
+  (e2, ty2) := typeExp(rhsExp, ExpOrigin.setFlag(origin, ExpOrigin.RHS), info);
+  (e1, e2, ty, mk) := TypeCheck.matchExpressions(e1, ty1, e2, ty2);
+
+  if TypeCheck.isIncompatibleMatch(mk) then
+    Error.addSourceMessage(Error.EQUATION_TYPE_MISMATCH_ERROR,
+      {Expression.toString(e1) + " = " + Expression.toString(e2),
+       Type.toString(ty1) + " = " + Type.toString(ty2)}, info);
+    fail();
+  end if;
+
+  eq := Equation.EQUALITY(e1, e2, ty, source);
+end typeEqualityEquation;
+
 function typeCondition
   input output Expression condition;
   input ExpOrigin.Type origin;
   input DAE.ElementSource source;
   input Error.Message errorMsg;
   input Boolean allowVector = false;
+  input Boolean allowClock = false;
+        output Type ty;
         output Variability variability;
 protected
-  Type ty;
-  MatchKind mk;
   SourceInfo info;
+  Type ety;
 algorithm
   info := ElementSource.getInfo(source);
   (condition, ty, variability) := typeExp(condition, origin, info);
 
-  if allowVector and Type.isVector(ty) then
-    (_, _, mk) := TypeCheck.matchTypes(Type.arrayElementType(ty), Type.BOOLEAN(), condition);
-    if TypeCheck.isIncompatibleMatch(mk) then
-      (_, _, mk) := TypeCheck.matchTypes(Type.arrayElementType(ty), Type.CLOCK(), condition);
-    end if;
-  else
-    (_, _, mk) := TypeCheck.matchTypes(ty, Type.BOOLEAN(), condition);
-    if TypeCheck.isIncompatibleMatch(mk) then
-      (_, _, mk) := TypeCheck.matchTypes(ty, Type.CLOCK(), condition);
-    end if;
-  end if;
+  ety := if allowVector then Type.arrayElementType(ty) else ty;
 
-  if TypeCheck.isIncompatibleMatch(mk) then
+  if not (Type.isBoolean(ety) or (allowClock and Type.isClock(ety))) then
     Error.addSourceMessage(errorMsg,
       {Expression.toString(condition), Type.toString(ty)}, info);
     fail();
@@ -2736,7 +2748,7 @@ algorithm
   // Type the conditions of all the branches.
   for b in branches loop
     Equation.Branch.BRANCH(cond, _, eql) := b;
-    (cond, var) := typeCondition(cond, cond_origin, source, Error.IF_CONDITION_TYPE_ERROR);
+    (cond, _, var) := typeCondition(cond, cond_origin, source, Error.IF_CONDITION_TYPE_ERROR);
 
     if var > Variability.PARAMETER or isNonExpandableExp(cond) then
       // If the condition doesn't fulfill the requirements for allowing
@@ -2841,6 +2853,45 @@ algorithm
   end match;
 end isNonConstantIfCondition;
 
+function typeWhenEquation
+  input list<Equation.Branch> branches;
+  input ExpOrigin.Type origin;
+  input DAE.ElementSource source;
+  output Equation whenEq;
+protected
+  ExpOrigin.Type next_origin = ExpOrigin.setFlag(origin, ExpOrigin.WHEN);
+  list<Equation.Branch> accum_branches = {};
+  Expression cond;
+  list<Equation> body;
+  Type ty;
+  Variability var;
+algorithm
+  for branch in branches loop
+    Equation.Branch.BRANCH(cond, _, body) := branch;
+    (cond, ty, var) := typeCondition(cond, origin, source,
+      Error.WHEN_CONDITION_TYPE_ERROR, allowVector = true, allowClock = true);
+
+    if Type.isClock(ty) then
+      if listLength(branches) <> 1 then
+        if referenceEq(branch, listHead(branches)) then
+          Error.addSourceMessage(Error.ELSE_WHEN_CLOCK, {}, ElementSource.getInfo(source));
+        else
+          Error.addSourceMessage(Error.CLOCKED_WHEN_BRANCH, {}, ElementSource.getInfo(source));
+        end if;
+
+        fail();
+      else
+        next_origin := ExpOrigin.setFlag(origin, ExpOrigin.CLOCKED);
+      end if;
+    end if;
+
+    body := list(typeEquation(eq, next_origin) for eq in body);
+    accum_branches := Equation.makeBranch(cond, body, var) :: accum_branches;
+  end for;
+
+  whenEq := Equation.WHEN(listReverseInPlace(accum_branches), source);
+end typeWhenEquation;
+
 function typeOperatorArg
   input output Expression arg;
   input Type expectedType;