Skip to content

Commit 777b5a6

Browse files
robby-phdrobby-phd
committed
Rewriting system
1 parent 9ddc820 commit 777b5a6

File tree

2 files changed

+193
-59
lines changed

2 files changed

+193
-59
lines changed

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

+192-58
Original file line numberDiff line numberDiff line change
@@ -127,14 +127,8 @@ object RewritingSystem {
127127
case _ => halt(s"Infeasible: expected typed expression")
128128
}
129129
case e: AST.Exp.Tuple =>
130-
if (e.args.size == 1) {
131-
return rec(e.args(0), funStack, localMap)
132-
} else {
133-
val t = e.typedOpt.get
134-
return AST.CoreExp.Apply(
135-
AST.CoreExp.ObjectVarRef(AST.CoreExp.tupleOwner, e.args.size.string, t),
136-
for (arg <- e.args) yield rec(arg, funStack, localMap), t)
137-
}
130+
return if (e.args.size == 1) rec(e.args(0), funStack, localMap)
131+
else AST.CoreExp.Tuple(for (arg <- e.args) yield rec(arg, funStack, localMap))
138132
case e: AST.Exp.Ident =>
139133
e.resOpt.get match {
140134
case res: AST.ResolvedInfo.LocalVar =>
@@ -157,11 +151,8 @@ object RewritingSystem {
157151
case _ => halt(s"Infeasible: $e")
158152
}
159153
case e: AST.Exp.Unary =>
160-
val t = e.typedOpt.get.subst(sm)
161-
return AST.CoreExp.Apply(AST.CoreExp.ObjectVarRef(AST.CoreExp.unaryOwner, e.opString, t),
162-
ISZ(rec(e.exp, funStack, localMap)), t)
154+
return AST.CoreExp.Unary(e.op, rec(e.exp, funStack, localMap))
163155
case e: AST.Exp.Binary =>
164-
val t = e.typedOpt.get.subst(sm)
165156
e.attr.resOpt.get match {
166157
case res: AST.ResolvedInfo.BuiltIn =>
167158
val left = rec(e.left, funStack, localMap)
@@ -175,8 +166,7 @@ object RewritingSystem {
175166
return AST.CoreExp.If(left, right, AST.CoreExp.LitB(T), AST.Typed.b)
176167
case _ =>
177168
}
178-
return AST.CoreExp.Apply(AST.CoreExp.ObjectVarRef(AST.CoreExp.binaryOwner, e.op, t),
179-
ISZ(left, right), t)
169+
return AST.CoreExp.Binary(left, e.op, right)
180170
case _ => halt(s"TODO: $e")
181171
}
182172
case e: AST.Exp.If =>
@@ -246,7 +236,10 @@ object RewritingSystem {
246236
return rec(exp, Stack.empty, HashSMap.empty)
247237
}
248238

249-
@pure def unifyExp(localPatterns: LocalPatternSet, pattern: AST.CoreExp, exp: AST.CoreExp,
239+
@pure def unifyExp(silent: B,
240+
localPatterns: LocalPatternSet,
241+
pattern: AST.CoreExp,
242+
exp: AST.CoreExp,
250243
init: UnificationMap,
251244
pendingApplications: MBox[PendingApplications],
252245
errorMessages: MBox[UnificationErrorMessages]): UnificationMap = {
@@ -261,15 +254,24 @@ object RewritingSystem {
261254
}
262255
var map = init
263256
def err(p: AST.CoreExp, e: AST.CoreExp): Unit = {
264-
errorMessages.value = errorMessages.value :+
265-
st"""Could not unify '${p.prettyST}' with '${e.prettyST}' in
266-
|${pattern.prettyST}, and
267-
|${exp.prettyST}""".render
257+
if (silent) {
258+
if (errorMessages.value.isEmpty) {
259+
errorMessages.value = errorMessages.value :+ ""
260+
}
261+
} else {
262+
errorMessages.value = errorMessages.value :+
263+
st"Could not unify '${p.prettyST}' with '${e.prettyST}' in '${pattern.prettyST}' and '${exp.prettyST}'".render
264+
}
268265
}
269266
def err2(id: String, e1: AST.CoreExp, e2: AST.CoreExp): Unit = {
270-
errorMessages.value = errorMessages.value :+
271-
st"""Could not unify local pattern '$id' with multiple expressions:
272-
|* ${(ISZ(e1.prettyST, e2.prettyST), "\n* ")}""".render
267+
if (silent) {
268+
if (errorMessages.value.isEmpty) {
269+
errorMessages.value = errorMessages.value :+ ""
270+
}
271+
} else {
272+
errorMessages.value = errorMessages.value :+
273+
st"Could not unify local pattern '$id' with both '${e1.prettyST}' and '${e2.prettyST}'".render
274+
}
273275
}
274276
def matchPatternLocals(p: AST.CoreExp, e: AST.CoreExp): Unit = {
275277
if (errorMessages.value.nonEmpty) {
@@ -301,12 +303,47 @@ object RewritingSystem {
301303
if (!(p.id == e.id && p.owner == e.owner)) {
302304
err(p, e)
303305
}
306+
case (p: AST.CoreExp.Binary, e: AST.CoreExp.Binary) =>
307+
if (p.op != e.op) {
308+
err(p, e)
309+
} else {
310+
matchPatternLocals(p.left, e.left)
311+
matchPatternLocals(p.right, e.right)
312+
}
313+
case (p: AST.CoreExp.Unary, e: AST.CoreExp.Unary) =>
314+
if (p.op != e.op) {
315+
err(p, e)
316+
} else {
317+
matchPatternLocals(p.exp, e.exp)
318+
}
319+
case (p: AST.CoreExp.Tuple, e: AST.CoreExp.Tuple) =>
320+
if (p.args.size != e.args.size) {
321+
err(p, e)
322+
} else {
323+
for (i <- 0 until p.args.size) {
324+
matchPatternLocals(p.args(i), e.args(i))
325+
}
326+
}
304327
case (p: AST.CoreExp.Select, e: AST.CoreExp.Select) =>
305328
if (p.id != e.id) {
306329
err(p, e)
307330
} else {
308331
matchPatternLocals(p.exp, e.exp)
309332
}
333+
case (p: AST.CoreExp.Update, e: AST.CoreExp.Update) =>
334+
if (p.id != e.id) {
335+
err(p, e)
336+
} else {
337+
matchPatternLocals(p.exp, e.exp)
338+
matchPatternLocals(p.arg, e.arg)
339+
}
340+
case (p: AST.CoreExp.Indexing, e: AST.CoreExp.Indexing) =>
341+
matchPatternLocals(p.exp, e.exp)
342+
matchPatternLocals(p.index, e.index)
343+
case (p: AST.CoreExp.IndexingUpdate, e: AST.CoreExp.IndexingUpdate) =>
344+
matchPatternLocals(p.exp, e.exp)
345+
matchPatternLocals(p.index, e.index)
346+
matchPatternLocals(p.arg, e.arg)
310347
case (p: AST.CoreExp.If, e: AST.CoreExp.If) =>
311348
matchPatternLocals(p.cond, e.cond)
312349
matchPatternLocals(p.tExp, e.tExp)
@@ -381,28 +418,35 @@ object RewritingSystem {
381418
return map
382419
}
383420

384-
@pure def unify(th: TypeHierarchy, localPatterns: LocalPatternSet, patterns: ISZ[AST.CoreExp], exps: ISZ[AST.CoreExp]): UnificationResult = {
421+
@pure def unify(silent: B, th: TypeHierarchy, localPatterns: LocalPatternSet, patterns: ISZ[AST.CoreExp], exps: ISZ[AST.CoreExp]): UnificationResult = {
385422
val errorMessages: MBox[UnificationErrorMessages] = MBox(ISZ())
386423
val pendingApplications: MBox[PendingApplications] = MBox(ISZ())
387424
var m: UnificationMap = HashSMap.empty
388425
for (i <- 0 until patterns.size) {
389-
m = unifyExp(localPatterns, patterns(i), exps(i), m, pendingApplications, errorMessages)
426+
m = unifyExp(silent, localPatterns, patterns(i), exps(i), m, pendingApplications, errorMessages)
390427
if (errorMessages.value.nonEmpty) {
391428
return Either.Right(errorMessages.value)
392429
}
393430
}
394431

395-
while (pendingApplications.value.nonEmpty) {
432+
/* while (pendingApplications.value.nonEmpty) */ {
396433
val pas = pendingApplications.value
397434
pendingApplications.value = ISZ()
398435
for (pa <- pas) {
399436
val (context, id, args, e) = pa
400437
m.get((context, id)) match {
401438
case Some(f: AST.CoreExp.Fun) =>
402439
simplify(th, SimplicationConfig.funApplicationOnly, AST.CoreExp.Apply(f, args, e.tipe)) match {
403-
case Some(pattern) => m = unifyExp(localPatterns, pattern, e, m, pendingApplications, errorMessages)
404-
case _ => errorMessages.value = errorMessages.value :+
405-
st"Could not reduce '$f(${(for (arg <- args) yield arg.prettyST, ", ")})'".render
440+
case Some(pattern) => m = unifyExp(silent, localPatterns, pattern, e, m, pendingApplications, errorMessages)
441+
case _ =>
442+
if (silent) {
443+
if (errorMessages.value.isEmpty) {
444+
errorMessages.value = errorMessages.value :+ ""
445+
}
446+
} else {
447+
errorMessages.value = errorMessages.value :+
448+
st"Could not reduce '$f(${(for (arg <- args) yield arg.prettyST, ", ")})'".render
449+
}
406450
}
407451
case Some(f) => errorMessages.value = errorMessages.value :+ s"Expecting to infer a function, but found '$f'"
408452
case _ =>
@@ -414,7 +458,13 @@ object RewritingSystem {
414458
}
415459

416460
for (localPattern <- localPatterns.elements if !m.contains(localPattern)) {
417-
errorMessages.value = errorMessages.value :+ s"Could not find any matching expression for '${localPattern._2}'"
461+
if (silent) {
462+
if (errorMessages.value.isEmpty) {
463+
errorMessages.value = errorMessages.value :+ ""
464+
}
465+
} else {
466+
errorMessages.value = errorMessages.value :+ s"Could not find any matching expression for '${localPattern._2}'"
467+
}
418468
}
419469
return if (errorMessages.value.nonEmpty) Either.Right(errorMessages.value)
420470
else Either.Left(m)
@@ -552,44 +602,44 @@ object RewritingSystem {
552602
case lit1 => halt(st"TODO: ${lit1.prettyST} $op ${lit2.prettyST}".render)
553603
}
554604

555-
@strictpure def evalUnary(op: String, lit: AST.CoreExp.Lit): AST.CoreExp.Lit =
605+
@strictpure def evalUnary(op: AST.Exp.UnaryOp.Type, lit: AST.CoreExp.Lit): AST.CoreExp.Lit =
556606
lit match {
557607
case lit: AST.CoreExp.LitB =>
558608
op match {
559-
case "!" => AST.CoreExp.LitB(!lit.value)
560-
case "~" => AST.CoreExp.LitB(~lit.value)
609+
case AST.Exp.UnaryOp.Not => AST.CoreExp.LitB(!lit.value)
610+
case AST.Exp.UnaryOp.Complement => AST.CoreExp.LitB(~lit.value)
561611
case _ => halt(s"Infeasible $op on B")
562612
}
563613
case lit: AST.CoreExp.LitZ =>
564614
op match {
565-
case "+" => AST.CoreExp.LitZ(lit.value)
566-
case "-" => AST.CoreExp.LitZ(-lit.value)
615+
case AST.Exp.UnaryOp.Plus => AST.CoreExp.LitZ(lit.value)
616+
case AST.Exp.UnaryOp.Minus => AST.CoreExp.LitZ(-lit.value)
567617
case _ => halt(s"Infeasible $op on Z")
568618
}
569619
case lit: AST.CoreExp.LitC =>
570620
op match {
571-
case "~" => AST.CoreExp.LitC(~lit.value)
621+
case AST.Exp.UnaryOp.Complement => AST.CoreExp.LitC(~lit.value)
572622
case _ => halt(s"Infeasible $op on C")
573623
}
574624
case lit: AST.CoreExp.LitF32 =>
575625
op match {
576-
case "+" => AST.CoreExp.LitF32(lit.value)
577-
case "-" => AST.CoreExp.LitF32(lit.value)
626+
case AST.Exp.UnaryOp.Plus => AST.CoreExp.LitF32(lit.value)
627+
case AST.Exp.UnaryOp.Minus => AST.CoreExp.LitF32(lit.value)
578628
case _ => halt(s"Infeasible $op on F32")
579629
}
580630
case lit: AST.CoreExp.LitF64 =>
581631
op match {
582-
case "+" => AST.CoreExp.LitF64(lit.value)
583-
case "-" => AST.CoreExp.LitF64(-lit.value)
632+
case AST.Exp.UnaryOp.Plus => AST.CoreExp.LitF64(lit.value)
633+
case AST.Exp.UnaryOp.Minus => AST.CoreExp.LitF64(-lit.value)
584634
case _ => halt(s"Infeasible $op on F64")
585635
}
586636
case lit: AST.CoreExp.LitR =>
587637
op match {
588-
case "+" => AST.CoreExp.LitR(lit.value)
589-
case "-" => AST.CoreExp.LitR(-lit.value)
638+
case AST.Exp.UnaryOp.Plus => AST.CoreExp.LitR(lit.value)
639+
case AST.Exp.UnaryOp.Minus => AST.CoreExp.LitR(-lit.value)
590640
case _ => halt(s"Infeasible $op on R")
591641
}
592-
case lit => halt(st"TODO: $op ${lit.prettyST}".render)
642+
case lit => halt(st"TODO: $op ${lit.prettyST}".render)
593643
}
594644

595645
@pure def simplify(th: TypeHierarchy, config: SimplicationConfig, exp: AST.CoreExp): Option[AST.CoreExp] = {
@@ -605,11 +655,111 @@ object RewritingSystem {
605655
case _ => return None()
606656
}
607657
case _: AST.CoreExp.ObjectVarRef => return None()
658+
case e: AST.CoreExp.Binary =>
659+
var changed = F
660+
val left: AST.CoreExp = rec(deBruijnMap, e.left) match {
661+
case Some(l) =>
662+
changed = T
663+
l
664+
case _ => e.left
665+
}
666+
val right: AST.CoreExp = rec(deBruijnMap, e.right) match {
667+
case Some(r) =>
668+
changed = T
669+
r
670+
case _ => e.right
671+
}
672+
if (config.constantPropagation) {
673+
(left, right) match {
674+
case (left: AST.CoreExp.Lit, right: AST.CoreExp.Lit) => return Some(evalBinary(left, e.op, right))
675+
case _ =>
676+
}
677+
}
678+
return if (changed) Some(e(left = left, right = right)) else None()
679+
case e: AST.CoreExp.Unary =>
680+
var changed = F
681+
val ue: AST.CoreExp = rec(deBruijnMap, e.exp) match {
682+
case Some(exp2) =>
683+
changed = T
684+
exp2
685+
case _ => e.exp
686+
}
687+
if (config.constantPropagation) {
688+
ue match {
689+
case exp: AST.CoreExp.Lit => return Some(evalUnary(e.op, exp))
690+
case _ =>
691+
}
692+
}
693+
return if (changed) Some(e(exp = ue)) else None()
608694
case e: AST.CoreExp.Select =>
609695
rec(deBruijnMap, e.exp) match {
610696
case Some(receiver) => return Some(e(exp = receiver))
611697
case _ => return None()
612698
}
699+
case e: AST.CoreExp.Update =>
700+
var changed = F
701+
val receiver: AST.CoreExp = rec(deBruijnMap, e.exp) match {
702+
case Some(exp2) =>
703+
changed = T
704+
exp2
705+
case _ => e.exp
706+
}
707+
val arg: AST.CoreExp = rec(deBruijnMap, e.arg) match {
708+
case Some(arg2) =>
709+
changed = T
710+
arg2
711+
case _ => e.arg
712+
}
713+
return if (changed) Some(e(exp = receiver, arg = arg)) else None()
714+
case e: AST.CoreExp.Indexing =>
715+
var changed = F
716+
val receiver: AST.CoreExp = rec(deBruijnMap, e.exp) match {
717+
case Some(exp2) =>
718+
changed = T
719+
exp2
720+
case _ => e.exp
721+
}
722+
val index: AST.CoreExp = rec(deBruijnMap, e.index) match {
723+
case Some(index2) =>
724+
changed = T
725+
index2
726+
case _ => e.index
727+
}
728+
return if (changed) Some(e(exp = receiver, index = index)) else None()
729+
case e: AST.CoreExp.IndexingUpdate =>
730+
var changed = F
731+
val receiver: AST.CoreExp = rec(deBruijnMap, e.exp) match {
732+
case Some(exp2) =>
733+
changed = T
734+
exp2
735+
case _ => e.exp
736+
}
737+
val index: AST.CoreExp = rec(deBruijnMap, e.index) match {
738+
case Some(index2) =>
739+
changed = T
740+
index2
741+
case _ => e.index
742+
}
743+
val arg: AST.CoreExp = rec(deBruijnMap, e.arg) match {
744+
case Some(arg2) =>
745+
changed = T
746+
arg2
747+
case _ => e.arg
748+
}
749+
return if (changed) Some(e(exp = receiver, index = index, arg = arg)) else None()
750+
case e: AST.CoreExp.Tuple =>
751+
var changed = F
752+
var args = ISZ[AST.CoreExp]()
753+
for (arg <- e.args) {
754+
rec(deBruijnMap, arg) match {
755+
case Some(arg2) =>
756+
args = args :+ arg2
757+
changed = T
758+
case _ =>
759+
args = args :+ arg
760+
}
761+
}
762+
return if (changed) Some(e(args = args)) else None()
613763
case e: AST.CoreExp.If =>
614764
var changed = F
615765
var cond = e.cond
@@ -656,22 +806,6 @@ object RewritingSystem {
656806
}
657807
}
658808
op match {
659-
case op: AST.CoreExp.ObjectVarRef =>
660-
if (config.constantPropagation) {
661-
op.owner match {
662-
case AST.CoreExp.binaryOwner =>
663-
args match {
664-
case ISZ(lit1: AST.CoreExp.Lit, lit2: AST.CoreExp.Lit) => return Some(evalBinary(lit1, op.id, lit2))
665-
case _ =>
666-
}
667-
case AST.CoreExp.unaryOwner =>
668-
args match {
669-
case ISZ(lit: AST.CoreExp.Lit) => return Some(evalUnary(op.id, lit))
670-
case _ =>
671-
}
672-
case _ =>
673-
}
674-
}
675809
case f: AST.CoreExp.Fun if config.funApplication =>
676810
var params = ISZ[(String, AST.Typed)]()
677811
def recParams(fe: AST.CoreExp): AST.CoreExp = {

‎shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -393,7 +393,7 @@ import InceptionPlugin._
393393
exps = exps :+ org.sireum.logika.RewritingSystem.translate(logika.th, to, HashMap.empty)
394394
}
395395
val localPatternSet = HashSSet ++ (for (id <- paramIds.elements) yield (context, id))
396-
org.sireum.logika.RewritingSystem.unify(logika.th, localPatternSet, patterns, exps) match {
396+
org.sireum.logika.RewritingSystem.unify(F, logika.th, localPatternSet, patterns, exps) match {
397397
case Either.Left(m) if !ok =>
398398
reporter.error(posOpt, Logika.kind,
399399
st"""Diff result: {

0 commit comments

Comments
 (0)