Refactoring: renamed DerivedTypeDecl to NewtypeDecl

9 files changed, 57 insertions, 57 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 32138bf9..9f13abf6 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -34,12 +34,12 @@ namespace Microsoft.Dafny
         var dd = (TypeSynonymDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

         return new TypeSynonymDecl(Tok(dd.tok), dd.Name, tps, m, CloneType(dd.Rhs), CloneAttributes(dd.Attributes));

-      } else if (d is DerivedTypeDecl) {

-        var dd = (DerivedTypeDecl)d;

+      } else if (d is NewtypeDecl) {

+        var dd = (NewtypeDecl)d;

         if (dd.Var == null) {

-          return new DerivedTypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes));

+          return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes));

         } else {

-          return new DerivedTypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes));

+          return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes));

         }

       } else if (d is TupleTypeDecl) {

         var dd = (TupleTypeDecl)d;

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 3f0c37b3..af9cce11 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -117,8 +117,8 @@ namespace Microsoft.Dafny {
             Error("Opaque type ('{0}') cannot be compiled", at.FullName);

           } else if (d is TypeSynonymDecl) {

             // do nothing, just bypass type synonyms in the compiler

-          } else if (d is DerivedTypeDecl) {

-            // do nothing, just bypass derived types in the compiler

+          } else if (d is NewtypeDecl) {

+            // do nothing, just bypass newtypes in the compiler

           } else if (d is DatatypeDecl) {

             var dt = (DatatypeDecl)d;

             Indent(indent);

@@ -970,8 +970,8 @@ namespace Microsoft.Dafny {
         return "BigInteger";

       } else if (type is RealType) {

         return "Dafny.BigRational";

-      } else if (type.AsDerivedType != null) {

-        return TypeName(type.AsDerivedType.BaseType);

+      } else if (type.AsNewtype != null) {

+        return TypeName(type.AsNewtype.BaseType);

       } else if (type is ObjectType) {

         return "object";

       } else if (type.IsArrayType) {

@@ -1062,8 +1062,8 @@ namespace Microsoft.Dafny {
         return "BigInteger.Zero";

       } else if (type is RealType) {

         return "Dafny.BigRational.ZERO";

-      } else if (type.AsDerivedType != null) {

-        return DefaultValue(type.AsDerivedType.BaseType);

+      } else if (type.AsNewtype != null) {

+        return DefaultValue(type.AsNewtype.BaseType);

       } else if (type.IsRefType) {

         return string.Format("({0})null", TypeName(type));

       } else if (type.IsDatatype) {

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index e52e7e5b..bb995c8d 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -469,8 +469,8 @@ NewtypeDecl<ModuleDefinition module, out TopLevelDecl td>
     NoUSIdent<out bvId>

     [ ":" Type<out baseType> ]       (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false); } .)

     "|"

-    Expression<out wh, false, true>  (. td = new DerivedTypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)

-  | Type<out baseType>               (. td = new DerivedTypeDecl(id, id.val, module, baseType, attrs); .)

+    Expression<out wh, false, true>  (. td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)

+  | Type<out baseType>               (. td = new NewtypeDecl(id, id.val, module, baseType, attrs); .)

   )

   [ SYNC ";"

       // In a future version of Dafny, including the following warning message:

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 59bb4d49..41bbeee4 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -370,7 +370,7 @@ namespace Microsoft.Dafny {
       if (opProxy != null) {

         return (opProxy.AllowInts || opProxy.AllowReals) && !opProxy.AllowSeq && !opProxy.AllowSetVarieties;

       }

-      return t.IsIntegerType || t.IsRealType || t.AsDerivedType != null;

+      return t.IsIntegerType || t.IsRealType || t.AsNewtype != null;

     }

     public enum NumericPersuation { Int, Real }

     public bool IsNumericBased(NumericPersuation p) {

@@ -390,7 +390,7 @@ namespace Microsoft.Dafny {
             return p == NumericPersuation.Real;

           }

         }

-        var d = t.AsDerivedType;

+        var d = t.AsNewtype;

         if (d == null) {

           return false;

         }

@@ -428,10 +428,10 @@ namespace Microsoft.Dafny {
         return udt == null ? null : udt.ResolvedClass as ArrayClassDecl;

       }

     }

-    public DerivedTypeDecl AsDerivedType {

+    public NewtypeDecl AsNewtype {

       get {

         var udt = NormalizeExpand() as UserDefinedType;

-        return udt == null ? null : udt.ResolvedClass as DerivedTypeDecl;

+        return udt == null ? null : udt.ResolvedClass as NewtypeDecl;

       }

     }

     public TypeSynonymDecl AsTypeSynonym {

@@ -450,7 +450,7 @@ namespace Microsoft.Dafny {
         if (udt == null) {

           return null;

         } else {

-          return (RedirectingTypeDecl)(udt.ResolvedClass as TypeSynonymDecl) ?? udt.ResolvedClass as DerivedTypeDecl;

+          return (RedirectingTypeDecl)(udt.ResolvedClass as TypeSynonymDecl) ?? udt.ResolvedClass as NewtypeDecl;

         }

       }

     }

@@ -1015,7 +1015,7 @@ namespace Microsoft.Dafny {
 

     public override bool SupportsEquality {

       get {

-        if (ResolvedClass is ClassDecl || ResolvedClass is DerivedTypeDecl) {

+        if (ResolvedClass is ClassDecl || ResolvedClass is NewtypeDecl) {

           return true;

         } else if (ResolvedClass is CoDatatypeDecl) {

           return false;

@@ -2217,12 +2217,12 @@ namespace Microsoft.Dafny {
     string Name { get; }

   }

 

-  public class DerivedTypeDecl : TopLevelDecl, RedirectingTypeDecl

+  public class NewtypeDecl : TopLevelDecl, RedirectingTypeDecl

   {

     public readonly Type BaseType;

     public readonly BoundVar Var;  // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType))

     public readonly Expression Constraint;  // is null iff Var is

-    public DerivedTypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes)

+    public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes)

       : base(tok, name, module, new List<TypeParameter>(), attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -2230,7 +2230,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(baseType != null);

       BaseType = baseType;

     }

-    public DerivedTypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes)

+    public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes)

       : base(tok, name, module, new List<TypeParameter>(), attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -2253,7 +2253,7 @@ namespace Microsoft.Dafny {
     string ICallable.NameRelativeToModule { get { return Name; } }

     Specification<Expression> ICallable.Decreases {

       get {

-        // The resolver checks that a DerivedTypeDecl sits in its own SSC in the call graph.  Therefore,

+        // The resolver checks that a NewtypeDecl sits in its own SSC in the call graph.  Therefore,

         // the question of what its Decreases clause is should never arise.

         throw new cce.UnreachableException();

       }

@@ -2309,7 +2309,7 @@ namespace Microsoft.Dafny {
     string ICallable.NameRelativeToModule { get { return Name; } }

     Specification<Expression> ICallable.Decreases {

       get {

-        // The resolver checks that a DerivedTypeDecl sits in its own SSC in the call graph.  Therefore,

+        // The resolver checks that a NewtypeDecl sits in its own SSC in the call graph.  Therefore,

         // the question of what its Decreases clause is should never arise.

         throw new cce.UnreachableException();

       }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 78ab9c14..a78d90a1 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -562,10 +562,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false); } 

 			Expect(8);

 			Expression(out wh, false, true);

-			td = new DerivedTypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); 

+			td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); 

 		} else if (StartOf(3)) {

 			Type(out baseType);

-			td = new DerivedTypeDecl(id, id.val, module, baseType, attrs); 

+			td = new NewtypeDecl(id, id.val, module, baseType, attrs); 

 		} else SynErr(137);

 		if (la.kind == 9) {

 			while (!(la.kind == 0 || la.kind == 9)) {SynErr(138); Get();}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 516eeade..2ec40e08 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -140,8 +140,8 @@ namespace Microsoft.Dafny {
           PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());

           wr.Write(EqualitySupportSuffix(at.EqualitySupport));

           wr.WriteLine();

-        } else if (d is DerivedTypeDecl) {

-          var dd = (DerivedTypeDecl)d;

+        } else if (d is NewtypeDecl) {

+          var dd = (NewtypeDecl)d;

           if (i++ != 0) { wr.WriteLine(); }

           Indent(indent);

           PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, new List<TypeParameter>());

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 69dfb03d..5f116779 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -163,10 +163,10 @@ namespace Microsoft.Dafny
                   if (nw.TypeArgs.Count != d.TypeArgs.Count) {

                     reporter.Error(nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);

                   }

-                } else if (nw is DerivedTypeDecl) {

+                } else if (nw is NewtypeDecl) {

                   // fine, as long as "nw" does not take any type parameters

                   if (nw.TypeArgs.Count != 0) {

-                    reporter.Error(nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a derived type, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s");

+                    reporter.Error(nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a newtype, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s");

                   }

                 } else if (nw is CoDatatypeDecl) {

                   reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index e76044b0..a9da389a 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -797,7 +797,7 @@ namespace Microsoft.Dafny
           // nothing more to register

         } else if (d is TypeSynonymDecl) {

           // nothing more to register

-        } else if (d is DerivedTypeDecl) {

+        } else if (d is NewtypeDecl) {

           // nothing more to register

 

         } else if (d is IteratorDecl) {

@@ -1474,8 +1474,8 @@ namespace Microsoft.Dafny
               typeRedirectionDependencies.AddEdge(syn, s);

             }

           });

-        } else if (d is DerivedTypeDecl) {

-          var dd = (DerivedTypeDecl)d;

+        } else if (d is NewtypeDecl) {

+          var dd = (NewtypeDecl)d;

           ResolveType(dd.tok, dd.BaseType, dd, ResolveTypeOptionEnum.DontInfer, null);

           dd.BaseType.ForeachTypeComponent(ty => {

             var s = ty.AsRedirectingType;

@@ -1520,7 +1520,7 @@ namespace Microsoft.Dafny
       if (cycle != null) {

         Contract.Assert(cycle.Count != 0);

         var erste = cycle[0];

-        Error(erste.Tok, "Cycle among redirecting types (derived types, type synonyms): {0} -> {1}", Util.Comma(" -> ", cycle, syn => syn.Name), erste.Name);

+        Error(erste.Tok, "Cycle among redirecting types (newtypes, type synonyms): {0} -> {1}", Util.Comma(" -> ", cycle, syn => syn.Name), erste.Name);

       }

     }

 

@@ -1551,16 +1551,16 @@ namespace Microsoft.Dafny
         } else if (d is ClassDecl) {

           var cl = (ClassDecl)d;

           ResolveClassMemberBodies(cl);

-        } else if (d is DerivedTypeDecl) {

-          var dd = (DerivedTypeDecl)d;

+        } else if (d is NewtypeDecl) {

+          var dd = (NewtypeDecl)d;

           // this check can be done only after it has been determined that the redirected types do not involve cycles

           if (!dd.BaseType.IsNumericBased()) {

-            Error(dd.tok, "derived types must be based on some numeric type (got {0})", dd.BaseType);

+            Error(dd.tok, "newtypes must be based on some numeric type (got {0})", dd.BaseType);

           }

           // type check the constraint, if any

           if (dd.Var != null) {

-            Contract.Assert(object.ReferenceEquals(dd.Var.Type, dd.BaseType));  // follows from DerivedTypeDecl invariant

-            Contract.Assert(dd.Constraint != null);  // follows from DerivedTypeDecl invariant

+            Contract.Assert(object.ReferenceEquals(dd.Var.Type, dd.BaseType));  // follows from NewtypeDecl invariant

+            Contract.Assert(dd.Constraint != null);  // follows from NewtypeDecl invariant

             scope.PushMarker();

             var added = scope.Push(dd.Var.Name, dd.Var);

             Contract.Assert(added);

@@ -1591,8 +1591,8 @@ namespace Microsoft.Dafny
           } else if (d is ClassDecl) {

             var cl = (ClassDecl)d;

             cl.Members.Iter(CheckTypeInference_Member);

-          } else if (d is DerivedTypeDecl) {

-            var dd = (DerivedTypeDecl)d;

+          } else if (d is NewtypeDecl) {

+            var dd = (NewtypeDecl)d;

             if (dd.Var != null) {

               Contract.Assert(dd.Constraint != null);

               CheckTypeInference(dd.Constraint);

@@ -1900,8 +1900,8 @@ namespace Microsoft.Dafny
                 }

               }

             }

-          } else if (d is DerivedTypeDecl) {

-            var dd = (DerivedTypeDecl)d;

+          } else if (d is NewtypeDecl) {

+            var dd = (NewtypeDecl)d;

             if (dd.Module.CallGraph.GetSCCSize(dd) != 1) {

               var cycle = Util.Comma(" -> ", dd.Module.CallGraph.GetSCC(dd), clbl => clbl.NameRelativeToModule);

               Error(dd.tok, "recursive dependency involving a newtype: " + cycle);

@@ -4158,8 +4158,8 @@ namespace Microsoft.Dafny
             if (d is OpaqueTypeDecl) {

               what = "opaque type";

               t.ResolvedParam = ((OpaqueTypeDecl)d).TheType;  // resolve like a type parameter, and it may have type parameters if it's an opaque type

-            } else if (d is DerivedTypeDecl) {

-              var dd = (DerivedTypeDecl)d;

+            } else if (d is NewtypeDecl) {

+              var dd = (NewtypeDecl)d;

               var caller = context as ICallable;

               if (caller != null) {

                 caller.EnclosingModule.CallGraph.AddEdge(caller, dd);

@@ -7894,7 +7894,7 @@ namespace Microsoft.Dafny
     bool ResolveAsTypeConversion(IdentifierSequence e, ResolveOpts opts, TopLevelDecl decl, IToken id, ref Expression r) {

       var tpArgs = decl.TypeArgs.ConvertAll(_ => (Type)new InferredTypeProxy());

       var ty = new UserDefinedType(e.tok, decl.Name, decl, tpArgs);

-      if (ty.AsDerivedType == null) {

+      if (ty.AsNewtype == null) {

         return false;

       } else {

         if (e.Arguments.Count != 1) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b7da7a5c..8beadb51 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -383,8 +383,8 @@ namespace Microsoft.Dafny {
         currentDeclaration = d;

         if (d is OpaqueTypeDecl) {

           AddTypeDecl((OpaqueTypeDecl)d);

-        } else if (d is DerivedTypeDecl) {

-          AddTypeDecl((DerivedTypeDecl)d);

+        } else if (d is NewtypeDecl) {

+          AddTypeDecl((NewtypeDecl)d);

         } else if (d is DatatypeDecl) {

           AddDatatype((DatatypeDecl)d);

         } else {

@@ -396,8 +396,8 @@ namespace Microsoft.Dafny {
           currentDeclaration = d;

           if (d is OpaqueTypeDecl) {

             AddTypeDecl((OpaqueTypeDecl)d);

-          } else if (d is DerivedTypeDecl) {

-            AddTypeDecl((DerivedTypeDecl)d);

+          } else if (d is NewtypeDecl) {

+            AddTypeDecl((NewtypeDecl)d);

           } else if (d is TypeSynonymDecl) {

             // do nothing, just bypass type synonyms in the translation

           } else if (d is DatatypeDecl) {

@@ -464,7 +464,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(td != null);

       AddTypeDecl_Aux(td.tok, nameTypeParam(td.TheType), td.TypeArgs);

     }

-    void AddTypeDecl(DerivedTypeDecl dd) {

+    void AddTypeDecl(NewtypeDecl dd) {

       Contract.Requires(dd != null);

       AddTypeDecl_Aux(dd.tok, dd.FullName, new List<TypeParameter>());

       AddWellformednessCheck(dd);

@@ -3934,7 +3934,7 @@ namespace Microsoft.Dafny {
       codeContext = null;

     }

 

-    void AddWellformednessCheck(DerivedTypeDecl decl) {

+    void AddWellformednessCheck(NewtypeDecl decl) {

       Contract.Requires(decl != null);

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(currentModule == null && codeContext == null);

@@ -3944,7 +3944,7 @@ namespace Microsoft.Dafny {
       if (decl.Var == null) {

         return;

       }

-      Contract.Assert(decl.Constraint != null);  // follows from the test above and the DerivedTypeDecl class invariant

+      Contract.Assert(decl.Constraint != null);  // follows from the test above and the NewtypeDecl class invariant

 

       currentModule = decl.Module;

       codeContext = decl;

@@ -5086,7 +5086,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);

       Contract.Requires(etran != null);

       bool needIntegerCheck = expr.Type.IsNumericBased(Type.NumericPersuation.Real) && toType.IsNumericBased(Type.NumericPersuation.Int);

-      var dd = toType.AsDerivedType;

+      var dd = toType.AsNewtype;

       if (!needIntegerCheck && dd == null) {

         return;

       }

@@ -5114,14 +5114,14 @@ namespace Microsoft.Dafny {
         CheckResultToBeInType_Aux(tok, new BoogieWrapper(be, dafnyType), dd, builder, etran);

       }

     }

-    void CheckResultToBeInType_Aux(IToken tok, Expression expr, DerivedTypeDecl dd, StmtListBuilder builder, ExpressionTranslator etran) {

+    void CheckResultToBeInType_Aux(IToken tok, Expression expr, NewtypeDecl dd, StmtListBuilder builder, ExpressionTranslator etran) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

       Contract.Requires(dd != null);

       Contract.Requires(builder != null);

       Contract.Requires(etran != null);

       // First, check constraints of base types

-      var baseType = dd.BaseType.AsDerivedType;

+      var baseType = dd.BaseType.AsNewtype;

       if (baseType != null) {

         CheckResultToBeInType_Aux(tok, expr, baseType, builder, etran);

       }

@@ -6434,11 +6434,11 @@ namespace Microsoft.Dafny {
           // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type

           return predef.RefType;

         }

-        var d = type.AsDerivedType;

+        var d = type.AsNewtype;

         if (d == null) {

           break;

         } else {

-          type = d.BaseType;  // the Boogie type to be used for the derived type is the same as for the base type

+          type = d.BaseType;  // the Boogie type to be used for the newtype is the same as for the base type

         }

       }