Merge branch 'master' into consistent-ide-cli-ru

Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs

@@ -57,4 +57,28 @@ public DefaultValueExpression(Cloner cloner, DefaultValueExpression original) :
  public DefaultValueExpression Clone(Cloner cloner) {
  return new DefaultValueExpression(cloner, this);
  }
+}
+
+/// TODO: This class is a bit sketchy. It should probably be used to replace DefaultValueExpression in some way.
+/// </summary>
+public class DefaultValueExpressionPreType : ConcreteSyntaxExpression {
+ public readonly Formal Formal;
+ public readonly Expression Receiver;
+ public readonly Dictionary<IVariable, Expression> SubstMap;
+ public readonly Dictionary<TypeParameter, PreType> PreTypeMap;
+
+ public DefaultValueExpressionPreType(IToken tok, Formal formal,
+ Expression/*?*/ receiver, Dictionary<IVariable, Expression> substMap, Dictionary<TypeParameter, PreType> preTypeMap)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(formal != null);
+ Contract.Requires(formal.DefaultValue != null);
+ Contract.Requires(substMap != null);
+ Contract.Requires(preTypeMap != null);
+ Formal = formal;
+ Receiver = receiver;
+ SubstMap = substMap;
+ PreTypeMap = preTypeMap;
+ PreType = formal.PreType.Substitute(preTypeMap);
+ }
 }

Source/DafnyCore/AST/Expressions/Variables/CasePattern.cs

@@ -86,6 +86,28 @@ public void AssembleExpr(List<Type> dtvTypeArgs) {
  }
  }
 
+ /// <summary>
+ /// Sets the Expr field. Assumes the CasePattern and its arguments to have been successfully resolved, except for assigning
+ /// to Expr.
+ /// </summary>
+ public void AssembleExprPreType(List<PreType> dtvPreTypeArgs) {
+ Contract.Requires(Var != null || dtvPreTypeArgs != null);
+ if (Var != null) {
+ Contract.Assert(this.Id == this.Var.Name);
+ this.Expr = new IdentifierExpr(this.tok, this.Var) {
+ PreType = this.Var.PreType
+ };
+ } else {
+ var dtValue = new DatatypeValue(this.tok, this.Ctor.EnclosingDatatype.Name, this.Id,
+ this.Arguments == null ? new List<Expression>() : this.Arguments.ConvertAll(arg => arg.Expr)) {
+ Ctor = this.Ctor,
+ PreType = new DPreType(this.Ctor.EnclosingDatatype, dtvPreTypeArgs)
+ };
+ dtValue.InferredPreTypeArgs.AddRange(dtvPreTypeArgs); // resolve here
+ this.Expr = dtValue;
+ }
+ }
+
  public IEnumerable<VT> Vars {
  get {
  if (Var != null) {

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -125,7 +125,7 @@ private void ShowWarningsForIncludeCycles(Program program) {
  }
  }
 
- public static void AddParseResultToProgram(DfyParseResult parseResult, Program program) {
+ private static void AddParseResultToProgram(DfyParseResult parseResult, Program program) {
  var defaultModule = program.DefaultModuleDef;
  var fileModule = parseResult.Module;
  program.Files.Add(fileModule);

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -2933,8 +2933,13 @@ protected override void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool
  TrParenExpr("~", expr, wr, inLetExprBody, wStmts);
  break;
  case ResolvedUnaryOp.Cardinality:
- TrParenExpr("new BigInteger(", expr, wr, inLetExprBody, wStmts);
- wr.Write(".Count)");
+ if (expr.Type.AsCollectionType is MultiSetType) {
+ TrParenExpr(expr, wr, inLetExprBody, wStmts);
+ wr.Write(".ElementCount");
+ } else {
+ TrParenExpr("new BigInteger(", expr, wr, inLetExprBody, wStmts);
+ wr.Write(".Count)");
+ }
  break;
  default:
  Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression

Source/DafnyCore/Compilers/Dafny/AST.dfy

@@ -1,19 +1,21 @@
 module {:extern "DAST"} DAST {
  datatype Module = Module(name: string, body: seq<ModuleItem>)
 
- datatype ModuleItem = Module(Module) | Class(Class) | Newtype(Newtype) | Datatype(Datatype)
+ datatype ModuleItem = Module(Module) | Class(Class) | Trait(Trait) | Newtype(Newtype) | Datatype(Datatype)
 
  datatype Newtype = Newtype(name: string, base: Type)
 
  datatype Type = Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) | Tuple(seq<Type>) | Primitive(Primitive) | Passthrough(string) | TypeArg(Ident)
 
  datatype Primitive = String | Bool | Char
 
- datatype ResolvedType = Datatype(path: seq<Ident>) | Newtype
+ datatype ResolvedType = Datatype(path: seq<Ident>) | Trait(path: seq<Ident>) | Newtype
 
  datatype Ident = Ident(id: string)
 
- datatype Class = Class(name: string, body: seq<ClassItem>)
+ datatype Class = Class(name: string, superClasses: seq<Type>, body: seq<ClassItem>)
+
+ datatype Trait = Trait(name: string, typeParams: seq<Type>, body: seq<ClassItem>)
 
  datatype Datatype = Datatype(name: string, enclosingModule: Ident, typeParams: seq<Type>, ctors: seq<DatatypeCtor>, body: seq<ClassItem>, isCo: bool)
 
@@ -23,7 +25,7 @@ module {:extern "DAST"} DAST {
 
  datatype Formal = Formal(name: string, typ: Type)
 
- datatype Method = Method(isStatic: bool, name: string, typeParams: seq<Type>, params: seq<Formal>, body: seq<Statement>, outTypes: seq<Type>, outVars: Optional<seq<Ident>>)
+ datatype Method = Method(isStatic: bool, hasBody: bool, overridingPath: Optional<seq<Ident>>, name: string, typeParams: seq<Type>, params: seq<Formal>, body: seq<Statement>, outTypes: seq<Type>, outVars: Optional<seq<Ident>>)
 
  datatype Optional<T> = Some(T) | None
 
@@ -35,6 +37,7 @@ module {:extern "DAST"} DAST {
  Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Optional<seq<Ident>>) |
  Return(expr: Expression) |
  EarlyReturn() |
+ Halt() |
  Print(Expression)
 
  datatype Expression =
@@ -46,12 +49,15 @@ module {:extern "DAST"} DAST {
  DatatypeValue(path: seq<Ident>, variant: string, isCo: bool, contents: seq<(string, Expression)>) |
  This() |
  Ite(cond: Expression, thn: Expression, els: Expression) |
+ UnOp(unOp: UnaryOp, expr: Expression) |
  BinOp(op: string, left: Expression, right: Expression) |
  Select(expr: Expression, field: string, onDatatype: bool) |
  TupleSelect(expr: Expression, index: nat) |
  Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>) |
  TypeTest(on: Expression, dType: seq<Ident>, variant: string) |
  InitializationValue(typ: Type)
 
+ datatype UnaryOp = Not | BitwiseNot | Cardinality
+
  datatype Literal = BoolLiteral(bool) | IntLiteral(int) | DecLiteral(string) | StringLiteral(string)
 }

Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs

@@ -25,7 +25,7 @@ public ModuleBuilder Module(string name) {
  }
  }
 
- class ModuleBuilder : ClassContainer, NewtypeContainer, DatatypeContainer {
+ class ModuleBuilder : ClassContainer, TraitContainer, NewtypeContainer, DatatypeContainer {
  readonly ModuleContainer parent;
  readonly string name;
  readonly List<ModuleItem> body = new();
@@ -43,6 +43,10 @@ public void AddClass(Class item) {
  body.Add((ModuleItem)ModuleItem.create_Class(item));
  }
 
+ public void AddTrait(Trait item) {
+ body.Add((ModuleItem)ModuleItem.create_Trait(item));
+ }
+
  public void AddNewtype(Newtype item) {
  body.Add((ModuleItem)ModuleItem.create_Newtype(item));
  }
@@ -60,19 +64,21 @@ public object Finish() {
  interface ClassContainer {
  void AddClass(Class item);
 
- public ClassBuilder Class(string name) {
- return new ClassBuilder(this, name);
+ public ClassBuilder Class(string name, List<DAST.Type> superClasses) {
+ return new ClassBuilder(this, name, superClasses);
  }
  }
 
  class ClassBuilder : ClassLike {
  readonly ClassContainer parent;
  readonly string name;
+ readonly List<DAST.Type> superClasses;
  readonly List<ClassItem> body = new();
 
- public ClassBuilder(ClassContainer parent, string name) {
+ public ClassBuilder(ClassContainer parent, string name, List<DAST.Type> superClasses) {
  this.parent = parent;
  this.name = name;
+ this.superClasses = superClasses;
  }
 
  public void AddMethod(DAST.Method item) {
@@ -84,7 +90,57 @@ public void AddField(DAST.Formal item) {
  }
 
  public object Finish() {
- parent.AddClass((Class)Class.create(Sequence<Rune>.UnicodeFromString(this.name), Sequence<ClassItem>.FromArray(body.ToArray())));
+ parent.AddClass((Class)Class.create(
+ Sequence<Rune>.UnicodeFromString(this.name),
+ Sequence<DAST.Type>.FromArray(this.superClasses.ToArray()),
+ Sequence<ClassItem>.FromArray(body.ToArray())
+ ));
+ return parent;
+ }
+ }
+
+ interface TraitContainer {
+ void AddTrait(Trait item);
+
+ public TraitBuilder Trait(string name, List<DAST.Type> typeParams) {
+ return new TraitBuilder(this, name, typeParams);
+ }
+ }
+
+ class TraitBuilder : ClassLike {
+ readonly TraitContainer parent;
+ readonly string name;
+ readonly List<DAST.Type> typeParams;
+ readonly List<ClassItem> body = new();
+
+ public TraitBuilder(TraitContainer parent, string name, List<DAST.Type> typeParams) {
+ this.parent = parent;
+ this.name = name;
+ this.typeParams = typeParams;
+ }
+
+ public void AddMethod(DAST.Method item) {
+ // remove existing method with the same name, because we're going to define an implementation
+ for (int i = 0; i < body.Count; i++) {
+ if (body[i].is_Method && body[i].dtor_Method_a0.dtor_name.Equals(item.dtor_name)) {
+ body.RemoveAt(i);
+ break;
+ }
+ }
+
+ body.Add((ClassItem)ClassItem.create_Method(item));
+ }
+
+ public void AddField(DAST.Formal item) {
+ throw new NotImplementedException();
+ }
+
+ public object Finish() {
+ parent.AddTrait((Trait)Trait.create(
+ Sequence<Rune>.UnicodeFromString(this.name),
+ Sequence<DAST.Type>.FromArray(typeParams.ToArray()),
+ Sequence<ClassItem>.FromArray(body.ToArray()))
+ );
  return parent;
  }
  }
@@ -174,8 +230,15 @@ interface ClassLike {
 
  void AddField(DAST.Formal item);
 
- public MethodBuilder Method(bool isStatic, string name, List<DAST.Type> typeArgs, List<DAST.Formal> params_, List<DAST.Type> outTypes, List<ISequence<Rune>> outVars) {
- return new MethodBuilder(this, isStatic, name, typeArgs, params_, outTypes, outVars);
+ public MethodBuilder Method(
+ bool isStatic, bool hasBody,
+ ISequence<ISequence<Rune>> overridingPath,
+ string name,
+ List<DAST.Type> typeArgs,
+ List<DAST.Formal> params_,
+ List<DAST.Type> outTypes, List<ISequence<Rune>> outVars
+ ) {
+ return new MethodBuilder(this, isStatic, hasBody, overridingPath, name, typeArgs, params_, outTypes, outVars);
  }
 
  public object Finish();
@@ -185,15 +248,27 @@ class MethodBuilder : StatementContainer {
  readonly ClassLike parent;
  readonly string name;
  readonly bool isStatic;
+ readonly bool hasBody;
+ readonly ISequence<ISequence<Rune>> overridingPath;
  readonly List<DAST.Type> typeArgs;
  readonly List<DAST.Formal> params_;
  readonly List<DAST.Type> outTypes;
  readonly List<ISequence<Rune>> outVars;
  readonly List<object> body = new();
 
- public MethodBuilder(ClassLike parent, bool isStatic, string name, List<DAST.Type> typeArgs, List<DAST.Formal> params_, List<DAST.Type> outTypes, List<ISequence<Rune>> outVars) {
+ public MethodBuilder(
+ ClassLike parent,
+ bool isStatic, bool hasBody,
+ ISequence<ISequence<Rune>> overridingPath,
+ string name,
+ List<DAST.Type> typeArgs,
+ List<DAST.Formal> params_,
+ List<DAST.Type> outTypes, List<ISequence<Rune>> outVars
+ ) {
  this.parent = parent;
  this.isStatic = isStatic;
+ this.hasBody = hasBody;
+ this.overridingPath = overridingPath;
  this.name = name;
  this.typeArgs = typeArgs;
  this.params_ = params_;
@@ -221,6 +296,8 @@ public DAST.Method Build() {
 
  return (DAST.Method)DAST.Method.create(
  isStatic,
+ hasBody,
+ overridingPath != null ? Optional<ISequence<ISequence<Rune>>>.create_Some(overridingPath) : Optional<ISequence<ISequence<Rune>>>.create_None(),
  Sequence<Rune>.UnicodeFromString(this.name),
  Sequence<DAST.Type>.FromArray(typeArgs.ToArray()),
  Sequence<DAST.Formal>.FromArray(params_.ToArray()),