-
Notifications
You must be signed in to change notification settings - Fork 256
/
NestedMatchCaseExpr.cs
45 lines (36 loc) · 1.64 KB
/
NestedMatchCaseExpr.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.IO;
using System.Linq;
namespace Microsoft.Dafny;
public class NestedMatchCaseExpr : NestedMatchCase, IAttributeBearingDeclaration {
public Expression Body;
public Attributes Attributes { get; set; }
public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Attributes attrs) : base(tok, pat) {
Contract.Requires(body != null);
this.Body = body;
this.Attributes = attrs;
}
public override IEnumerable<INode> Children =>
(Attributes != null ? new Node[] { Attributes } : Enumerable.Empty<Node>()).Concat(new Node[] { Body, Pat });
public override IEnumerable<INode> PreResolveChildren => Children;
public void Resolve(ModuleResolver resolver,
ResolutionContext resolutionContext,
Type resultType,
Type sourceType) {
var beforeResolveErrorCount = resolver.reporter.ErrorCount;
Pat.Resolve(resolver, resolutionContext, sourceType, resolutionContext.IsGhost, false, false, false);
resolver.ResolveAttributes(this, resolutionContext);
var afterResolveErrorCount = resolver.reporter.ErrorCount;
if (beforeResolveErrorCount == afterResolveErrorCount) {
resolver.ResolveExpression(Body, resolutionContext);
resolver.ConstrainSubtypeRelation(resultType, Body.Type, Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", Body.Type, resultType);
}
}
public override string ToString() {
var writer = new StringWriter();
new Printer(writer, DafnyOptions.Default).PrintNestedMatchCase(false, false, this, false, false);
return writer.ToString();
}
}