diff options
author | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-25 16:37:12 -0700 |
---|---|---|
committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-25 16:37:12 -0700 |
commit | a732a632287074e74a1dd394149b36e83526a0cf (patch) | |
tree | 9770cb8127d4bf9d8348a5da54922d32f3d29fdb /Dafny/RefinementTransformer.cs | |
parent | 032662d0adb823376b1abd49a0c46ba3276f8721 (diff) |
Dafny: fixed resolution bug for inductive datatypes (previous check did not handle generic datatypes correctly)
Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code)
Dafny: added "codatatype" declaration (syntax only for now)
Diffstat (limited to 'Dafny/RefinementTransformer.cs')
-rw-r--r-- | Dafny/RefinementTransformer.cs | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs index a10cb4bf..c73ffda8 100644 --- a/Dafny/RefinementTransformer.cs +++ b/Dafny/RefinementTransformer.cs @@ -136,11 +136,17 @@ namespace Microsoft.Dafny { if (d is ArbitraryTypeDecl) {
var dd = (ArbitraryTypeDecl)d;
return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, null);
- } else if (d is DatatypeDecl) {
- var dd = (DatatypeDecl)d;
+ } else if (d is IndDatatypeDecl) {
+ var dd = (IndDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var ctors = dd.Ctors.ConvertAll(CloneCtor);
- var dt = new DatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
+ var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
+ return dt;
+ } else if (d is CoDatatypeDecl) {
+ var dd = (CoDatatypeDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var ctors = dd.Ctors.ConvertAll(CloneCtor);
+ var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
return dt;
} else if (d is ClassDecl) {
var dd = (ClassDecl)d;
|