@@ -1353,37 +1353,37 @@ object evaluator extends EvaluationRules with Immutable {
13531353 (axioms, triggers, mostRecentTrig)
13541354 }
13551355
1356- /* Evaluate a sequence of expressions in Order
1356+ /* Evaluate a sequence of expressions in Order
13571357 * The constructor determines when the evaluation stops
13581358 * Only Or and And are supported for the constructor
13591359 */
1360- private def evalSeqShortCircuit (constructor : Seq [Term ] => Term ,
1361- s : State ,
1362- exps : Seq [ast.Exp ],
1363- pve : PartialVerificationError ,
1360+ private def evalSeqShortCircuit (constructor : Seq [Term ] => Term ,
1361+ s : State ,
1362+ exps : Seq [ast.Exp ],
1363+ pve : PartialVerificationError ,
13641364 v : Verifier )
13651365 (Q : (State , Term , Verifier ) => VerificationResult )
13661366 : VerificationResult = {
13671367 if (constructor != Or && constructor != And ) {
13681368 sys.error(" Only Or and And are supported as constructors for evalSeqShortCircuit" )
13691369 }
13701370 type brFun = (State , Verifier ) => VerificationResult
1371- val (default, stop, swapIfAnd) =
1372- if (constructor == Or ) (False (), True (), (a : brFun, b : brFun) => (a,b))
1371+ val (default, stop, swapIfAnd) =
1372+ if (constructor == Or ) (False (), True (), (a : brFun, b : brFun) => (a,b))
13731373 else (True (), False (), (a : brFun, b : brFun) => (b,a))
13741374 if (exps.size== 0 )
13751375 Q (s, default, v)
13761376 else
13771377 eval(s, exps.head, pve, v)((s1, t0, v1) =>
13781378 t0 match {
13791379 case `stop` => Q (s1, t0, v1)
1380- case _ =>
1380+ case _ =>
13811381 joiner.join[Term , Term ](s1, v1)((s2, v2, QB ) =>
13821382 brancher.branch(s2, t0, v2, true ) _ tupled swapIfAnd(
13831383 (s3, v3) => QB (s3, constructor(Seq (t0)), v3),
13841384 (s3, v3) => evalSeqShortCircuit(constructor, s3, exps.tail, pve, v3)(QB ))
13851385 ){case Seq (ent) => (ent.s, ent.data)
1386- case Seq (ent1, ent2) => (ent1.s.merge(ent2.s),
1386+ case Seq (ent1, ent2) => (ent1.s.merge(ent2.s),
13871387 constructor(Seq (ent1.data, ent2.data)))
13881388 case ents => sys.error(s " Unexpected join data entries $ents" )
13891389 }(Q )
0 commit comments