Skip to content

Commit 698c493

Browse files
robby-phdrobby-phd
committed
Rewriting system.
1 parent d18eca1 commit 698c493

File tree

1 file changed

+160
-25
lines changed

1 file changed

+160
-25
lines changed

‎shared/src/main/scala/org/sireum/logika/RewritingSystem.scala

+160-25
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@
2626
package org.sireum.logika
2727

2828
import org.sireum._
29-
import org.sireum.lang.symbol.Info
29+
import org.sireum.lang.symbol.{Info, TypeInfo}
3030
import org.sireum.lang.{ast => AST}
3131
import org.sireum.lang.tipe.TypeHierarchy
3232

@@ -359,7 +359,7 @@ object RewritingSystem {
359359
}
360360
case e: AST.Exp.Tuple =>
361361
return if (e.args.size == 1) rec(e.args(0), funStack, localMap)
362-
else AST.CoreExp.Tuple(for (arg <- e.args) yield rec(arg, funStack, localMap))
362+
else AST.CoreExp.Constructor(e.typedOpt.get, for (arg <- e.args) yield rec(arg, funStack, localMap))
363363
case e: AST.Exp.Ident =>
364364
e.resOpt.get match {
365365
case res: AST.ResolvedInfo.LocalVar =>
@@ -450,27 +450,86 @@ object RewritingSystem {
450450
return recStmt(e.block, funStack, localMap)._1.get
451451
case e: AST.Exp.Invoke =>
452452
val args: ISZ[AST.CoreExp.Base] = for (arg <- e.args) yield rec(arg, funStack, localMap)
453+
e.attr.resOpt.get match {
454+
case res: AST.ResolvedInfo.Method if res.mode == AST.MethodMode.Constructor =>
455+
res.mode match {
456+
case AST.MethodMode.Spec =>
457+
case AST.MethodMode.Method =>
458+
case AST.MethodMode.Constructor =>
459+
return AST.CoreExp.Constructor(e.typedOpt.get, args)
460+
case AST.MethodMode.Select =>
461+
e.receiverOpt match {
462+
case Some(receiver) => return AST.CoreExp.Indexing(rec(receiver, funStack, localMap),
463+
rec(e.args(0), funStack, localMap), e.typedOpt.get)
464+
case _ => return AST.CoreExp.Indexing(rec(e.ident, funStack, localMap),
465+
rec(e.args(0), funStack, localMap), e.typedOpt.get)
466+
}
467+
case AST.MethodMode.Store =>
468+
val ie = rec(e.args(0), funStack, localMap)
469+
val tuple = ie.tipe.asInstanceOf[AST.Typed.Tuple]
470+
val index = AST.CoreExp.Select(ie, "_1", tuple.args(0))
471+
val value = AST.CoreExp.Select(ie, "_2", tuple.args(1))
472+
e.receiverOpt match {
473+
case Some(receiver) => return AST.CoreExp.IndexingUpdate(rec(receiver, funStack, localMap),
474+
index, value, e.typedOpt.get)
475+
case _ => return AST.CoreExp.IndexingUpdate(rec(e.ident, funStack, localMap),
476+
index, value, e.typedOpt.get)
477+
}
478+
case AST.MethodMode.Extractor => halt("TODO")
479+
case AST.MethodMode.Ext => halt("TODO")
480+
case AST.MethodMode.ObjectConstructor => halt("TODO")
481+
case AST.MethodMode.Just => halt("Infeasible")
482+
case AST.MethodMode.Copy => halt("Infeasible")
483+
}
484+
case _ =>
485+
}
453486
e.receiverOpt match {
454487
case Some(receiver) =>
455-
return AST.CoreExp.Apply(
456-
AST.CoreExp.Select(rec(receiver, funStack, localMap), e.ident.id.value,
457-
e.ident.typedOpt.get), args, e.typedOpt.get)
458-
case _ => return AST.CoreExp.Apply(rec(e.ident, funStack, localMap),
488+
return AST.CoreExp.Apply(T, rec(e.ident, funStack, localMap),
489+
rec(receiver, funStack, localMap) +: args, e.typedOpt.get)
490+
case _ => return AST.CoreExp.Apply(F, rec(e.ident, funStack, localMap),
459491
args, e.typedOpt.get)
460492
}
461493
case e: AST.Exp.InvokeNamed =>
462-
val args = MS.create[Z, AST.CoreExp.Base](e.args.size, AST.CoreExp.LitB(F))
463-
for (arg <- e.args) {
464-
args(arg.index) = rec(arg.arg, funStack, localMap)
494+
def getArgs: ISZ[AST.CoreExp.Base] = {
495+
val args = MS.create[Z, AST.CoreExp.Base](e.args.size, AST.CoreExp.LitB(F))
496+
for (arg <- e.args) {
497+
args(arg.index) = rec(arg.arg, funStack, localMap)
498+
}
499+
return args.toISZ
500+
}
501+
e.attr.resOpt.get match {
502+
case res: AST.ResolvedInfo.Method if res.mode == AST.MethodMode.Constructor =>
503+
res.mode match {
504+
case AST.MethodMode.Constructor =>
505+
return AST.CoreExp.Constructor(e.typedOpt.get, getArgs)
506+
case AST.MethodMode.Spec =>
507+
case AST.MethodMode.Method =>
508+
case AST.MethodMode.Copy =>
509+
var r: AST.CoreExp.Base = e.receiverOpt match {
510+
case Some(receiver) => rec(receiver, funStack, localMap)
511+
case _ => rec(e.ident, funStack, localMap)
512+
}
513+
val t = e.typedOpt.get
514+
for (arg <- e.args) {
515+
r = AST.CoreExp.Update(r, arg.id.value, r, t)
516+
}
517+
return r
518+
case AST.MethodMode.Ext => halt("TODO")
519+
case AST.MethodMode.Extractor => halt("TODO")
520+
case AST.MethodMode.ObjectConstructor => halt("TODO")
521+
case AST.MethodMode.Just => halt("Infeasible")
522+
case AST.MethodMode.Select => halt("Infeasible")
523+
case AST.MethodMode.Store => halt("Infeasible")
524+
}
525+
case _ =>
465526
}
466527
e.receiverOpt match {
467528
case Some(receiver) =>
468-
return AST.CoreExp.Apply(
469-
AST.CoreExp.Select(rec(receiver, funStack, localMap), e.ident.id.value,
470-
e.ident.typedOpt.get),
471-
args.toISZ, e.typedOpt.get)
472-
case _ => return AST.CoreExp.Apply(rec(e.ident, funStack, localMap),
473-
args.toISZ, e.typedOpt.get)
529+
return AST.CoreExp.Apply(T, rec(e.ident, funStack, localMap),
530+
rec(receiver, funStack, localMap) +: getArgs, e.typedOpt.get)
531+
case _ => return AST.CoreExp.Apply(F, rec(e.ident, funStack, localMap),
532+
getArgs, e.typedOpt.get)
474533
}
475534
case e => halt(s"TODO: $e")
476535
}
@@ -618,8 +677,8 @@ object RewritingSystem {
618677
} else {
619678
matchPatternLocals(p.exp, e.exp)
620679
}
621-
case (p: AST.CoreExp.Tuple, e: AST.CoreExp.Tuple) =>
622-
if (p.args.size != e.args.size) {
680+
case (p: AST.CoreExp.Constructor, e: AST.CoreExp.Constructor) =>
681+
if (p.args.size != e.args.size || p.tipe != e.tipe) {
623682
err(p, e)
624683
} else {
625684
for (i <- 0 until p.args.size) {
@@ -691,7 +750,7 @@ object RewritingSystem {
691750
}
692751
e match {
693752
case e: AST.CoreExp.Apply =>
694-
if (p.args.size != e.args.size) {
753+
if (p.hasReceiver != e.hasReceiver || p.args.size != e.args.size) {
695754
err(p, e)
696755
} else {
697756
matchPatternLocals(p.exp, e.exp)
@@ -740,7 +799,7 @@ object RewritingSystem {
740799
val (context, id, args, e) = pa
741800
m.get((context, id)) match {
742801
case Some(f: AST.CoreExp.Fun) =>
743-
evalBase(th, EvalConfig.funApplicationOnly, AST.CoreExp.Apply(f, args, e.tipe)) match {
802+
evalBase(th, EvalConfig.funApplicationOnly, AST.CoreExp.Apply(F, f, args, e.tipe)) match {
744803
case Some(pattern) =>
745804
m = unifyExp(silent, th, localPatterns, pattern, e, m, pendingApplications, substMap, errorMessages)
746805
case _ =>
@@ -1025,10 +1084,66 @@ object RewritingSystem {
10251084
}
10261085
return if (changed) Some(e(exp = ue)) else None()
10271086
case e: AST.CoreExp.Select =>
1028-
rec(deBruijnMap, e.exp) match {
1029-
case Some(receiver) => return Some(e(exp = receiver))
1030-
case _ => return None()
1087+
var changed = F
1088+
val receiver: AST.CoreExp.Base = rec(deBruijnMap, e.exp) match {
1089+
case Some(exp2) =>
1090+
changed = T
1091+
exp2
1092+
case _ => e.exp
10311093
}
1094+
if (config.tupleProjection && receiver.tipe.isInstanceOf[AST.Typed.Tuple]) {
1095+
receiver match {
1096+
case receiver: AST.CoreExp.Constructor =>
1097+
val n = Z(ops.StringOps(e.id).substring(1, e.id.size)).get - 1
1098+
return Some(receiver.args(n))
1099+
case _ =>
1100+
}
1101+
}
1102+
if (config.fieldAccess) {
1103+
val rt = receiver.tipe.asInstanceOf[AST.Typed.Name]
1104+
receiver match {
1105+
case receiver: AST.CoreExp.Update =>
1106+
if (receiver.id == e.id) {
1107+
return Some(receiver.arg)
1108+
} else {
1109+
return evalBase(th, config, e(exp = receiver))
1110+
}
1111+
case receiver: AST.CoreExp.IndexingUpdate => return evalBase(th, config, e(exp = receiver.exp))
1112+
case receiver: AST.CoreExp.Constructor =>
1113+
if (e.id == "size" && (rt.ids == AST.Typed.isName || rt.ids == AST.Typed.msName)) {
1114+
return Some(AST.CoreExp.LitZ(receiver.args.size))
1115+
} else {
1116+
val info = th.typeMap.get(rt.ids).get.asInstanceOf[TypeInfo.Adt]
1117+
val paramIndexMap = HashMap.empty[String, Z] ++ (for (i <- 0 until info.ast.params.size) yield
1118+
(info.ast.params(i).id.value, i))
1119+
paramIndexMap.get(e.id) match {
1120+
case Some(i) => return Some(receiver.args(i))
1121+
case _ =>
1122+
}
1123+
}
1124+
case _ =>
1125+
}
1126+
th.typeMap.get(rt.ids).get match {
1127+
case info: TypeInfo.SubZ =>
1128+
e.id match {
1129+
case "Name" => return Some(AST.CoreExp.LitString(st"${(rt.ids, ".")}".render))
1130+
case "isBitVector" => return Some(AST.CoreExp.LitB(info.ast.isBitVector))
1131+
case "hasMin" => return Some(AST.CoreExp.LitB(info.ast.hasMin))
1132+
case "hasMax" => return Some(AST.CoreExp.LitB(info.ast.hasMax))
1133+
case "BitWidth" if info.ast.isBitVector => return Some(AST.CoreExp.LitZ(info.ast.bitWidth))
1134+
case "Min" if info.ast.hasMin => return Some(AST.CoreExp.LitZ(info.ast.min))
1135+
case "Max" if info.ast.hasMax => return Some(AST.CoreExp.LitZ(info.ast.max))
1136+
case "isIndex" => return Some(AST.CoreExp.LitB(info.ast.isIndex))
1137+
case "Index" => return Some(AST.CoreExp.LitZ(info.ast.index))
1138+
case "isSigned" => return Some(AST.CoreExp.LitB(info.ast.isSigned))
1139+
case "isZeroIndex" => return Some(AST.CoreExp.LitB(info.ast.isZeroIndex))
1140+
case _ => halt(s"Infeasible: ${e.id}")
1141+
}
1142+
case info: TypeInfo.Enum => halt("TODO")
1143+
case _ =>
1144+
}
1145+
}
1146+
return if (changed) Some(e(exp = receiver)) else None()
10321147
case e: AST.CoreExp.Update =>
10331148
var changed = F
10341149
val receiver: AST.CoreExp.Base = rec(deBruijnMap, e.exp) match {
@@ -1043,6 +1158,13 @@ object RewritingSystem {
10431158
arg2
10441159
case _ => e.arg
10451160
}
1161+
if (config.fieldAccess) {
1162+
receiver match {
1163+
case receiver: AST.CoreExp.Update if receiver.id == e.id =>
1164+
return Some(e(exp = receiver.exp, arg = arg))
1165+
case _ =>
1166+
}
1167+
}
10461168
return if (changed) Some(e(exp = receiver, arg = arg)) else None()
10471169
case e: AST.CoreExp.Indexing =>
10481170
var changed = F
@@ -1058,6 +1180,13 @@ object RewritingSystem {
10581180
index2
10591181
case _ => e.index
10601182
}
1183+
if (config.seqIndexing) {
1184+
receiver match {
1185+
case receiver: AST.CoreExp.IndexingUpdate if index == receiver.index =>
1186+
return Some(receiver.arg)
1187+
case _ =>
1188+
}
1189+
}
10611190
return if (changed) Some(e(exp = receiver, index = index)) else None()
10621191
case e: AST.CoreExp.IndexingUpdate =>
10631192
var changed = F
@@ -1079,8 +1208,15 @@ object RewritingSystem {
10791208
arg2
10801209
case _ => e.arg
10811210
}
1211+
if (config.seqIndexing) {
1212+
receiver match {
1213+
case receiver: AST.CoreExp.IndexingUpdate if index == receiver.index =>
1214+
return Some(e(exp = receiver.exp, index = index, arg = arg))
1215+
case _ =>
1216+
}
1217+
}
10821218
return if (changed) Some(e(exp = receiver, index = index, arg = arg)) else None()
1083-
case e: AST.CoreExp.Tuple =>
1219+
case e: AST.CoreExp.Constructor =>
10841220
var changed = F
10851221
var args = ISZ[AST.CoreExp.Base]()
10861222
for (arg <- e.args) {
@@ -1207,8 +1343,7 @@ object RewritingSystem {
12071343
}
12081344
case e: AST.CoreExp.Quant if e.kind == AST.CoreExp.Quant.Kind.ForAll =>
12091345
return toCondEquivH(evalBase(th, EvalConfig.quantApplicationOnly,
1210-
AST.CoreExp.Apply(
1211-
e,
1346+
AST.CoreExp.Apply(F, e,
12121347
ISZ(AST.CoreExp.LocalVarRef(T, ISZ(), paramId(e.param.id), e.param.tipe)),
12131348
AST.Typed.b)).get)
12141349
case e: AST.CoreExp.If =>

0 commit comments

Comments
 (0)