Index: src/AST/Convert.cpp =================================================================== --- src/AST/Convert.cpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/Convert.cpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -205,5 +205,10 @@ ftype->parameters = get().acceptL(node->params); - ftype->forall = get().acceptL( node->type->forall ); + ftype->forall = get().acceptL( node->type_params ); + if (!node->assertions.empty()) { + assert(!ftype->forall.empty()); + // find somewhere to place assertions back, for convenience it is the last slot + ftype->forall.back()->assertions = get().acceptL(node->assertions); + } visitType(node->type, ftype); @@ -602,11 +607,6 @@ for (decltype(src->begin()) src_i = src->begin(); src_i != src->end(); src_i++) { - rslt->add( src_i->first, + rslt->add( src_i->first.typeString(), get().accept1(src_i->second) ); - } - - for (decltype(src->beginVar()) src_i = src->beginVar(); src_i != src->endVar(); src_i++) { - rslt->addVar( src_i->first, - get().accept1(src_i->second) ); } @@ -1212,5 +1212,25 @@ // ty->returnVals = get().acceptL( node->returns ); // ty->parameters = get().acceptL( node->params ); - ty->forall = get().acceptL( node->forall ); + + auto types = get().acceptL( node->forall ); + for (auto t : types) { + auto newT = new TypeDecl(*t->baseType); + newT->name = t->name; // converted by typeString() + for (auto asst : newT->assertions) delete asst; + newT->assertions.clear(); + ty->forall.push_back(newT); + } + auto assts = get().acceptL( node->assertions ); + if (!assts.empty()) { + assert(!types.empty()); + for (auto asst : assts) { + auto newDecl = new ObjectDecl(*strict_dynamic_cast(asst->var)); + delete newDecl->type; + newDecl->type = asst->result->clone(); + newDecl->storageClasses.is_extern = true; // hack + ty->forall.back()->assertions.push_back(newDecl); + } + } + return visitType( node, ty ); } @@ -1299,5 +1319,5 @@ ty = new TypeInstType{ cv( node ), - node->name, + node->typeString(), get().accept1( node->base ), get().acceptL( node->attributes ) @@ -1306,5 +1326,5 @@ ty = new TypeInstType{ cv( node ), - node->name, + node->typeString(), node->kind == ast::TypeDecl::Ftype, get().acceptL( node->attributes ) @@ -1431,5 +1451,5 @@ /// at conversion stage, all created nodes are guaranteed to be unique, therefore /// const_casting out of smart pointers is permitted. - std::unordered_map< const BaseSyntaxNode *, ast::ptr > cache = {}; + std::unordered_map< const BaseSyntaxNode *, ast::readonly > cache = {}; // Local Utilities: @@ -1565,4 +1585,16 @@ // can function type have attributes? seems not to be the case. // visitType(old->type, ftype); + + // collect assertions and put directly in FunctionDecl + std::vector> assertions; + for (auto & param: forall) { + for (auto & asst: param->assertions) { + assertf(asst->unique(), "newly converted decl must be unique"); + assertions.emplace_back(asst); + } + auto mut = param.get_and_mutate(); + assertf(mut == param, "newly converted decl must be unique"); + mut->assertions.clear(); + } auto decl = new ast::FunctionDecl{ @@ -1584,4 +1616,5 @@ cache.emplace( old, decl ); + decl->assertions = std::move(assertions); decl->withExprs = GET_ACCEPT_V(withExprs, Expr); decl->stmts = GET_ACCEPT_1(statements, CompoundStmt); @@ -2066,8 +2099,12 @@ } + // TypeSubstitution shouldn't exist yet in old. ast::TypeSubstitution * convertTypeSubstitution(const TypeSubstitution * old) { - + if (!old) return nullptr; - + if (old->empty()) return nullptr; + assert(false); + + /* ast::TypeSubstitution *rslt = new ast::TypeSubstitution(); @@ -2077,10 +2114,6 @@ } - for (decltype(old->beginVar()) old_i = old->beginVar(); old_i != old->endVar(); old_i++) { - rslt->addVar( old_i->first, - getAccept1(old_i->second) ); - } - return rslt; + */ } @@ -2610,5 +2643,14 @@ ty->params.emplace_back(v->get_type()); } - ty->forall = GET_ACCEPT_V( forall, TypeDecl ); + // xxx - when will this be non-null? + // will have to create dangling (no-owner) decls to be pointed to + auto foralls = GET_ACCEPT_V( forall, TypeDecl ); + + for (auto & param : foralls) { + ty->forall.emplace_back(new ast::TypeInstType(param->name, param)); + for (auto asst : param->assertions) { + ty->assertions.emplace_back(new ast::VariableExpr({}, asst)); + } + } visitType( old, ty ); } Index: src/AST/Decl.cpp =================================================================== --- src/AST/Decl.cpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/Decl.cpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -50,20 +50,22 @@ FunctionDecl::FunctionDecl( const CodeLocation & loc, const std::string & name, - std::vector>&& forall, - std::vector>&& params, std::vector>&& returns, - CompoundStmt * stmts, Storage::Classes storage, Linkage::Spec linkage, - std::vector>&& attrs, Function::Specs fs, bool isVarArgs) - : DeclWithType( loc, name, storage, linkage, std::move(attrs), fs ), params(std::move(params)), returns(std::move(returns)), - stmts( stmts ) { - FunctionType * ftype = new FunctionType(static_cast(isVarArgs)); - for (auto & param : this->params) { - ftype->params.emplace_back(param->get_type()); - } - for (auto & ret : this->returns) { - ftype->returns.emplace_back(ret->get_type()); - } - ftype->forall = std::move(forall); - this->type = ftype; - } + std::vector>&& forall, + std::vector>&& params, std::vector>&& returns, + CompoundStmt * stmts, Storage::Classes storage, Linkage::Spec linkage, + std::vector>&& attrs, Function::Specs fs, bool isVarArgs) +: DeclWithType( loc, name, storage, linkage, std::move(attrs), fs ), params(std::move(params)), returns(std::move(returns)), + type_params(std::move(forall)), stmts( stmts ) { + FunctionType * ftype = new FunctionType(static_cast(isVarArgs)); + for (auto & param : this->params) { + ftype->params.emplace_back(param->get_type()); + } + for (auto & ret : this->returns) { + ftype->returns.emplace_back(ret->get_type()); + } + for (auto & tp : this->type_params) { + ftype->forall.emplace_back(new TypeInstType(tp->name, tp)); + } + this->type = ftype; +} Index: src/AST/Decl.hpp =================================================================== --- src/AST/Decl.hpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/Decl.hpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -132,4 +132,7 @@ std::vector< ptr > withExprs; + std::vector> type_params; + std::vector> assertions; + FunctionDecl( const CodeLocation & loc, const std::string & name, std::vector>&& forall, std::vector>&& params, std::vector>&& returns, Index: src/AST/Expr.cpp =================================================================== --- src/AST/Expr.cpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/Expr.cpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -206,40 +206,5 @@ assert( aggregate->result ); - // Deep copy on result type avoids mutation on transitively multiply referenced object. - // - // Example, adapted from parts of builtins and bootloader: - // - // forall(dtype T) - // struct __Destructor { - // T * object; - // void (*dtor)(T *); - // }; - // - // forall(dtype S) - // void foo(__Destructor(S) &d) { - // if (d.dtor) { // here - // } - // } - // - // Let e be the "d.dtor" guard espression, which is MemberExpr after resolve. Let d be the - // declaration of member __Destructor.dtor (an ObjectDecl), as accessed via the top-level - // declaration of __Destructor. Consider the types e.result and d.type. In the old AST, one - // is a clone of the other. Ordinary new-AST use would set them up as a multiply-referenced - // object. - // - // e.result: PointerType - // .base: FunctionType - // .params.front(): ObjectDecl, the anonymous parameter of type T* - // .type: PointerType - // .base: TypeInstType - // let x = that - // let y = similar, except start from d.type - // - // Consider two code lines down, genericSubstitution(...).apply(result). - // - // Applying this chosen-candidate's type substitution means modifying x, substituting - // S for T. This mutation should affect x and not y. - - result = deepCopy(mem->get_type()); + result = mem->get_type(); // substitute aggregate generic parameters into member type Index: src/AST/ForallSubstitutionTable.cpp =================================================================== --- src/AST/ForallSubstitutionTable.cpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ (revision ) @@ -1,54 +1,0 @@ -// -// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo -// -// The contents of this file are covered under the licence agreement in the -// file "LICENCE" distributed with Cforall. -// -// ForallSubstitutionTable.cpp -- -// -// Author : Aaron B. Moss -// Created On : Thu Jun 27 14:00:00 2019 -// Last Modified By : Aaron B. Moss -// Last Modified On : Thu Jun 27 14:00:00 2019 -// Update Count : 1 -// - -#include "ForallSubstitutionTable.hpp" - -#include -#include - -#include "Copy.hpp" // for shallowCopy -#include "Decl.hpp" -#include "Node.hpp" -#include "Type.hpp" -#include "Visitor.hpp" - -namespace ast { - -std::vector< ptr< TypeDecl > > ForallSubstitutionTable::clone( - const std::vector< ptr< TypeDecl > > & forall, Visitor & v -) { - std::vector< ptr< TypeDecl > > new_forall; - new_forall.reserve( forall.size() ); - - for ( const ast::TypeDecl * d : forall ) { - // create cloned type decl and insert into substitution map before further mutation - auto new_d = shallowCopy( d ); - decls.insert( d, new_d ); - // perform other mutations and add to output - auto newer_d = v.visit( new_d ); - assert( new_d == newer_d && "Newly cloned TypeDecl must retain identity" ); - new_forall.emplace_back( new_d ); - } - - return new_forall; -} - -} - -// Local Variables: // -// tab-width: 4 // -// mode: c++ // -// compile-command: "make install" // -// End: // Index: src/AST/ForallSubstitutionTable.hpp =================================================================== --- src/AST/ForallSubstitutionTable.hpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ (revision ) @@ -1,57 +1,0 @@ -// -// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo -// -// The contents of this file are covered under the licence agreement in the -// file "LICENCE" distributed with Cforall. -// -// ForallSubstitutionTable.hpp -- -// -// Author : Aaron B. Moss -// Created On : Thu Jun 27 14:00:00 2019 -// Last Modified By : Aaron B. Moss -// Last Modified On : Thu Jun 27 14:00:00 2019 -// Update Count : 1 -// - -#pragma once - -#include - -#include "Node.hpp" // for ptr -#include "Common/ScopedMap.h" - -namespace ast { - -class TypeDecl; -class Visitor; - -/// Wrapper for TypeDecl substitution table -class ForallSubstitutionTable { - ScopedMap< const TypeDecl *, const TypeDecl * > decls; - -public: - /// Replaces given declaration with value in the table, if present, otherwise returns argument - const TypeDecl * replace( const TypeDecl * d ) { - auto it = decls.find( d ); - if ( it != decls.end() ) return it->second; - return d; - } - - /// Builds a new forall list mutated according to the given visitor - std::vector< ptr< TypeDecl > > clone( - const std::vector< ptr< TypeDecl > > & forall, Visitor & v ); - - /// Introduces a new lexical scope - void beginScope() { decls.beginScope(); } - - /// Concludes a lexical scope - void endScope() { decls.endScope(); } -}; - -} - -// Local Variables: // -// tab-width: 4 // -// mode: c++ // -// compile-command: "make install" // -// End: // Index: src/AST/ForallSubstitutor.hpp =================================================================== --- src/AST/ForallSubstitutor.hpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ (revision ) @@ -1,70 +1,0 @@ -// -// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo -// -// The contents of this file are covered under the licence agreement in the -// file "LICENCE" distributed with Cforall. -// -// ForallSubstitutor.hpp -- -// -// Author : Aaron B. Moss -// Created On : Wed Jun 26 15:00:00 2019 -// Last Modified By : Aaron B. Moss -// Last Modified On : Wed Jun 26 15:00:00 2019 -// Update Count : 1 -// - -#include "Pass.hpp" - -namespace ast { - -class Expr; - -/// Visitor that correctly substitutes TypeDecl while maintaining TypeInstType bindings. -/// Also has some convenience methods to mutate fields. -struct ForallSubstitutor : public WithForallSubstitutor, public WithVisitorRef { - /// Substitute TypeInstType base type - readonly< TypeDecl > operator() ( const readonly< TypeDecl > & o ) { - return subs.replace( o ); - } - - /// Make new forall-list clone - FunctionType::ForallList operator() ( const FunctionType::ForallList & o ) { - return subs.clone( o, *visitor ); - } - - template - std::vector> operator() (const std::vector> & o) { - std::vector> n; - n.reserve(o.size()); - for (const node_t * d : o) { n.emplace_back(d->accept(*visitor)); } - return n; - } - - /* - - /// Substitute parameter/return type - std::vector< ptr< DeclWithType > > operator() ( const std::vector< ptr< DeclWithType > > & o ) { - std::vector< ptr< DeclWithType > > n; - n.reserve( o.size() ); - for ( const DeclWithType * d : o ) { n.emplace_back( d->accept( *visitor ) ); } - return n; - } - - /// Substitute type parameter list - std::vector< ptr< Expr > > operator() ( const std::vector< ptr< Expr > > & o ) { - std::vector< ptr< Expr > > n; - n.reserve( o.size() ); - for ( const Expr * d : o ) { n.emplace_back( d->accept( *visitor ) ); } - return n; - } - - */ -}; - -} // namespace ast - -// Local Variables: // -// tab-width: 4 // -// mode: c++ // -// compile-command: "make install" // -// End: // Index: src/AST/Pass.hpp =================================================================== --- src/AST/Pass.hpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/Pass.hpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -34,6 +34,4 @@ #include "AST/SymbolTable.hpp" - -#include "AST/ForallSubstitutionTable.hpp" // Private prelude header, needed for some of the magic tricks this class pulls off @@ -66,5 +64,4 @@ // | WithVisitorRef - provides an pointer to the templated visitor wrapper // | WithSymbolTable - provides symbol table functionality -// | WithForallSubstitutor - maintains links between TypeInstType and TypeDecl under mutation // // Other Special Members: @@ -258,8 +255,4 @@ container_t< ptr > call_accept( const container_t< ptr > & container ); - /// Mutate forall-list, accounting for presence of type substitution map - template - void mutate_forall( const node_t *& ); - public: /// Logic to call the accept and mutate the parent if needed, delegates call to accept @@ -398,9 +391,4 @@ }; -/// Use when the templated visitor needs to keep TypeInstType instances properly linked to TypeDecl -struct WithForallSubstitutor { - ForallSubstitutionTable subs; -}; - } Index: src/AST/Pass.impl.hpp =================================================================== --- src/AST/Pass.impl.hpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/Pass.impl.hpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -367,20 +367,4 @@ } - - template< typename core_t > - template< typename node_t > - void ast::Pass< core_t >::mutate_forall( const node_t *& node ) { - if ( auto subs = __pass::forall::subs( core, 0 ) ) { - // tracking TypeDecl substitution, full clone - if ( node->forall.empty() ) return; - - node_t * mut = __pass::mutate( node ); - mut->forall = subs->clone( node->forall, *this ); - node = mut; - } else { - // not tracking TypeDecl substitution, just mutate - maybe_accept( node, &node_t::forall ); - } - } } @@ -504,9 +488,10 @@ __pass::symtab::addId( core, 0, func ); VISIT( - // parameter declarations are now directly here + // parameter declarations maybe_accept( node, &FunctionDecl::params ); maybe_accept( node, &FunctionDecl::returns ); - // foralls are still in function type - maybe_accept( node, &FunctionDecl::type ); + // type params and assertions + maybe_accept( node, &FunctionDecl::type_params ); + maybe_accept( node, &FunctionDecl::assertions ); // First remember that we are now within a function. ValueGuard< bool > oldInFunction( inFunction ); @@ -1758,6 +1743,7 @@ VISIT({ - guard_forall_subs forall_guard { *this, node }; - mutate_forall( node ); + // guard_forall_subs forall_guard { *this, node }; + // mutate_forall( node ); + maybe_accept( node, &FunctionType::assertions ); maybe_accept( node, &FunctionType::returns ); maybe_accept( node, &FunctionType::params ); @@ -1981,5 +1967,5 @@ { bool mutated = false; - std::unordered_map< std::string, ast::ptr< ast::Type > > new_map; + std::unordered_map< ast::TypeInstType::TypeEnvKey, ast::ptr< ast::Type > > new_map; for ( const auto & p : node->typeEnv ) { guard_symtab guard { *this }; @@ -1994,20 +1980,4 @@ } } - - { - bool mutated = false; - std::unordered_map< std::string, ast::ptr< ast::Expr > > new_map; - for ( const auto & p : node->varEnv ) { - guard_symtab guard { *this }; - auto new_node = p.second->accept( *this ); - if (new_node != p.second) mutated = true; - new_map.insert({ p.first, new_node }); - } - if (mutated) { - auto new_node = __pass::mutate( node ); - new_node->varEnv.swap( new_map ); - node = new_node; - } - } ) Index: src/AST/Pass.proto.hpp =================================================================== --- src/AST/Pass.proto.hpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/Pass.proto.hpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -413,13 +413,4 @@ static inline auto leave( core_t &, long, const ast::FunctionType * ) {} - // Get the substitution table, if present - template - static inline auto subs( core_t & core, int ) -> decltype( &core.subs ) { - return &core.subs; - } - - template - static inline ast::ForallSubstitutionTable * subs( core_t &, long ) { return nullptr; } - // Replaces a TypeInstType's base TypeDecl according to the table template Index: src/AST/Print.cpp =================================================================== --- src/AST/Print.cpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/Print.cpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -155,4 +155,13 @@ } + void print( const ast::FunctionType::AssertionList & assts ) { + if (assts.empty()) return; + os << "with assertions" << endl; + ++indent; + printAll(assts); + os << indent; + --indent; + } + void print( const std::vector> & attrs ) { if ( attrs.empty() ) return; @@ -206,6 +215,5 @@ void preprint( const ast::NamedTypeDecl * node ) { if ( ! node->name.empty() ) { - if( deterministic_output && isUnboundType(node->name) ) os << "[unbound]:"; - else os << node->name << ": "; + os << node->name << ": "; } @@ -261,4 +269,5 @@ void preprint( const ast::FunctionType * node ) { print( node->forall ); + print( node->assertions ); print( node->qualifiers ); } @@ -1375,5 +1384,5 @@ virtual const ast::Type * visit( const ast::TypeInstType * node ) override final { preprint( node ); - const auto & _name = deterministic_output && isUnboundType(node) ? "[unbound]" : node->name; + const auto & _name = deterministic_output && isUnboundType(node) ? "[unbound]" : node->typeString(); os << "instance of type " << _name << " (" << (node->kind == ast::TypeDecl::Ftype ? "" : "not ") << "function type)"; @@ -1502,15 +1511,7 @@ os << indent << "Types:" << endl; for ( const auto& i : *node ) { - os << indent+1 << i.first << " -> "; + os << indent+1 << i.first.typeString() << " -> "; indent += 2; safe_print( i.second ); - indent -= 2; - os << endl; - } - os << indent << "Non-types:" << endl; - for ( auto i = node->beginVar(); i != node->endVar(); ++i ) { - os << indent+1 << i->first << " -> "; - indent += 2; - safe_print( i->second ); indent -= 2; os << endl; Index: src/AST/SymbolTable.cpp =================================================================== --- src/AST/SymbolTable.cpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/SymbolTable.cpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -414,5 +414,11 @@ void SymbolTable::addFunction( const FunctionDecl * func ) { - addTypes( func->type->forall ); + for (auto & td : func->type_params) { + addType(td); + } + for (auto & asst : func->assertions) { + addId(asst); + } + // addTypes( func->type->forall ); addIds( func->returns ); addIds( func->params ); Index: src/AST/Type.cpp =================================================================== --- src/AST/Type.cpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/Type.cpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -21,5 +21,4 @@ #include "Decl.hpp" -#include "ForallSubstitutor.hpp" // for substituteForall #include "Init.hpp" #include "Common/utility.h" // for copy, move @@ -92,24 +91,5 @@ // GENERATED END -// --- ParameterizedType - -void FunctionType::initWithSub( - const FunctionType & o, Pass< ForallSubstitutor > & sub -) { - forall = sub.core( o.forall ); -} - // --- FunctionType - - -FunctionType::FunctionType( const FunctionType & o ) -: Type( o.qualifiers, copy( o.attributes ) ), returns(), params(), - isVarArgs( o.isVarArgs ) { - Pass< ForallSubstitutor > sub; - initWithSub( o, sub ); // initialize substitution map - returns = sub.core( o.returns ); // apply to return and parameter types - params = sub.core( o.params ); -} - namespace { bool containsTtype( const std::vector> & l ) { @@ -199,16 +179,5 @@ // TODO: once TypeInstType representation is updated, it should properly check // if the context id is filled. this is a temporary hack for now - return isUnboundType(typeInst->name); - } - return false; -} - -bool isUnboundType(const std::string & tname) { - // xxx - look for a type name produced by renameTyVars. - - // TODO: once TypeInstType representation is updated, it should properly check - // if the context id is filled. this is a temporary hack for now - if (std::count(tname.begin(), tname.end(), '_') >= 3) { - return true; + return typeInst->formal_usage > 0; } return false; Index: src/AST/Type.hpp =================================================================== --- src/AST/Type.hpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/Type.hpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -36,6 +36,4 @@ template< typename T > class Pass; - -struct ForallSubstitutor; class Type : public Node { @@ -272,10 +270,9 @@ /// Type of a function `[R1, R2](*)(P1, P2, P3)` class FunctionType final : public Type { - protected: - /// initializes forall with substitutor - void initWithSub( const FunctionType & o, Pass< ForallSubstitutor > & sub ); -public: - using ForallList = std::vector>; +public: + using ForallList = std::vector>; + using AssertionList = std::vector>; ForallList forall; + AssertionList assertions; std::vector> returns; @@ -292,5 +289,5 @@ : Type(q), returns(), params(), isVarArgs(va) {} - FunctionType( const FunctionType & o ); + FunctionType( const FunctionType & o ) = default; /// true if either the parameters or return values contain a tttype @@ -397,5 +394,26 @@ public: readonly base; + // previously from renameTyVars; now directly use integer fields instead of synthesized strings + // a nonzero value of formal_usage indicates a formal type (only used in function type) + // a zero value of formal_usage indicates an actual type (referenced inside body of parametric structs and functions) TypeDecl::Kind kind; + int formal_usage; + int expr_id; + + // compact representation used for map lookups. + struct TypeEnvKey { + const TypeDecl * base; + int formal_usage; + int expr_id; + + TypeEnvKey() = default; + TypeEnvKey(const TypeDecl * base, int formal_usage = 0, int expr_id = 0): base(base), formal_usage(formal_usage), expr_id(expr_id) {} + TypeEnvKey(const TypeInstType & inst): base(inst.base), formal_usage(inst.formal_usage), expr_id(inst.expr_id) {} + std::string typeString() const { return std::string("_") + std::to_string(formal_usage) + "_" + std::to_string(expr_id) + "_" + base->name; } + bool operator==(const TypeEnvKey & other) const { return base == other.base && formal_usage == other.formal_usage && expr_id == other.expr_id; } + + }; + + bool operator==(const TypeInstType & other) const { return base == other.base && formal_usage == other.formal_usage && expr_id == other.expr_id; } TypeInstType( @@ -409,4 +427,7 @@ TypeInstType( const TypeInstType & o ) = default; + TypeInstType( const TypeEnvKey & key ) + : BaseInstType(key.base->name), base(key.base), kind(key.base->kind), formal_usage(key.formal_usage), expr_id(key.expr_id) {} + /// sets `base`, updating `kind` correctly void set_base( const TypeDecl * ); @@ -418,4 +439,9 @@ const Type * accept( Visitor & v ) const override { return v.visit( this ); } + + std::string typeString() const { + if (formal_usage > 0) return std::string("_") + std::to_string(formal_usage) + "_" + std::to_string(expr_id) + "_" + name; + else return name; + } private: TypeInstType * clone() const override { return new TypeInstType{ *this }; } @@ -510,6 +536,18 @@ bool isUnboundType(const Type * type); -bool isUnboundType(const std::string & tname); - + +} + +namespace std { + template<> + struct hash { + size_t operator() (const ast::TypeInstType::TypeEnvKey & x) const { + const size_t p = 1000007; + size_t res = reinterpret_cast(x.base); + res = p * res + x.formal_usage; + res = p * res + x.expr_id; + return res; + } + }; } Index: src/AST/TypeEnvironment.cpp =================================================================== --- src/AST/TypeEnvironment.cpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/TypeEnvironment.cpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -52,5 +52,5 @@ for ( const auto & i : open ) { if ( first ) { first = false; } else { out << ' '; } - out << i.first << "(" << i.second << ")"; + out << i.first.typeString() << "(" << i.second << ")"; } } @@ -62,6 +62,9 @@ if(first) first = false; else out << " "; - if( deterministic_output && isUnboundType(var) ) out << "[unbound]"; - else out << var; + + if( deterministic_output ) out << "[unbound]"; + else out << "_" << var.formal_usage << "_" << var.expr_id << "_"; + + out << var.base->name; } out << ")"; @@ -79,5 +82,5 @@ } -const EqvClass * TypeEnvironment::lookup( const std::string & var ) const { +const EqvClass * TypeEnvironment::lookup( const TypeInstType::TypeEnvKey & var ) const { for ( ClassList::const_iterator i = env.begin(); i != env.end(); ++i ) { if ( i->vars.find( var ) != i->vars.end() ) return &*i; @@ -106,5 +109,5 @@ void TypeEnvironment::add( const FunctionType::ForallList & tyDecls ) { - for ( const TypeDecl * tyDecl : tyDecls ) { + for ( auto & tyDecl : tyDecls ) { env.emplace_back( tyDecl ); } @@ -119,12 +122,14 @@ void TypeEnvironment::writeToSubstitution( TypeSubstitution & sub ) const { for ( const auto & clz : env ) { - std::string clzRep; + TypeInstType::TypeEnvKey clzRep; + bool first = true; for ( const auto & var : clz.vars ) { if ( clz.bound ) { sub.add( var, clz.bound ); - } else if ( clzRep.empty() ) { + } else if ( first ) { clzRep = var; + first = false; } else { - sub.add( var, new TypeInstType{ clzRep, clz.data.kind } ); + sub.add( var, new TypeInstType{ clzRep } ); } } @@ -141,8 +146,8 @@ struct Occurs : public ast::WithVisitorRef { bool result; - std::set< std::string > vars; + std::unordered_set< TypeInstType::TypeEnvKey > vars; const TypeEnvironment & tenv; - Occurs( const std::string & var, const TypeEnvironment & env ) + Occurs( const TypeInstType::TypeEnvKey & var, const TypeEnvironment & env ) : result( false ), vars(), tenv( env ) { if ( const EqvClass * clz = tenv.lookup( var ) ) { @@ -154,7 +159,7 @@ void previsit( const TypeInstType * typeInst ) { - if ( vars.count( typeInst->name ) ) { + if ( vars.count( *typeInst ) ) { result = true; - } else if ( const EqvClass * clz = tenv.lookup( typeInst->name ) ) { + } else if ( const EqvClass * clz = tenv.lookup( *typeInst ) ) { if ( clz->bound ) { clz->bound->accept( *visitor ); @@ -165,5 +170,5 @@ /// true if `var` occurs in `ty` under `env` - bool occurs( const Type * ty, const std::string & var, const TypeEnvironment & env ) { + bool occurs( const Type * ty, const TypeInstType::TypeEnvKey & var, const TypeEnvironment & env ) { Pass occur{ var, env }; maybe_accept( ty, occur ); @@ -280,10 +285,10 @@ // remove references from bound type, so that type variables can only bind to value types ptr target = bindTo->stripReferences(); - auto tyvar = open.find( typeInst->name ); + auto tyvar = open.find( *typeInst ); assert( tyvar != open.end() ); if ( ! tyVarCompatible( tyvar->second, target ) ) return false; - if ( occurs( target, typeInst->name, *this ) ) return false; - - auto it = internal_lookup( typeInst->name ); + if ( occurs( target, *typeInst, *this ) ) return false; + + auto it = internal_lookup( *typeInst ); if ( it != env.end() ) { if ( it->bound ) { @@ -308,5 +313,5 @@ } else { env.emplace_back( - typeInst->name, target, widen.first && widen.second, data ); + *typeInst, target, widen.first && widen.second, data ); } return true; @@ -318,6 +323,6 @@ WidenMode widen, const SymbolTable & symtab ) { - auto c1 = internal_lookup( var1->name ); - auto c2 = internal_lookup( var2->name ); + auto c1 = internal_lookup( *var1 ); + auto c2 = internal_lookup( *var2 ); // exit early if variables already bound together @@ -333,5 +338,5 @@ if ( c1 != env.end() ) { if ( c1->bound ) { - if ( occurs( c1->bound, var2->name, *this ) ) return false; + if ( occurs( c1->bound, *var2, *this ) ) return false; type1 = c1->bound; } @@ -340,5 +345,5 @@ if ( c2 != env.end() ) { if ( c2->bound ) { - if ( occurs( c2->bound, var1->name, *this ) ) return false; + if ( occurs( c2->bound, *var1, *this ) ) return false; type2 = c2->bound; } @@ -378,15 +383,15 @@ } else if ( c1 != env.end() ) { // var2 unbound, add to env[c1] - c1->vars.emplace( var2->name ); + c1->vars.emplace( *var2 ); c1->allowWidening = widen1; c1->data.isComplete |= data.isComplete; } else if ( c2 != env.end() ) { // var1 unbound, add to env[c2] - c2->vars.emplace( var1->name ); + c2->vars.emplace( *var1 ); c2->allowWidening = widen2; c2->data.isComplete |= data.isComplete; } else { // neither var bound, create new class - env.emplace_back( var1->name, var2->name, widen1 && widen2, data ); + env.emplace_back( *var1, *var2, widen1 && widen2, data ); } @@ -452,5 +457,5 @@ } -TypeEnvironment::ClassList::iterator TypeEnvironment::internal_lookup( const std::string & var ) { +TypeEnvironment::ClassList::iterator TypeEnvironment::internal_lookup( const TypeInstType::TypeEnvKey & var ) { for ( ClassList::iterator i = env.begin(); i != env.end(); ++i ) { if ( i->vars.count( var ) ) return i; Index: src/AST/TypeEnvironment.hpp =================================================================== --- src/AST/TypeEnvironment.hpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/TypeEnvironment.hpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -55,7 +55,7 @@ /// recorded. More investigation is needed. struct AssertCompare { - bool operator()( const DeclWithType * d1, const DeclWithType * d2 ) const { - int cmp = d1->name.compare( d2->name ); - return cmp < 0 || ( cmp == 0 && d1->get_type() < d2->get_type() ); + bool operator()( const VariableExpr * d1, const VariableExpr * d2 ) const { + int cmp = d1->var->name.compare( d2->var->name ); + return cmp < 0 || ( cmp == 0 && d1->result < d2->result ); } }; @@ -70,8 +70,8 @@ /// Set of assertions pending satisfaction -using AssertionSet = std::map< readonly, AssertionSetValue, AssertCompare >; +using AssertionSet = std::map< const VariableExpr *, AssertionSetValue, AssertCompare >; /// Set of open variables -using OpenVarSet = std::unordered_map< std::string, TypeDecl::Data >; +using OpenVarSet = std::unordered_map< TypeInstType::TypeEnvKey, TypeDecl::Data >; /// Merges one set of open vars into another @@ -89,5 +89,5 @@ /// they bind to. struct EqvClass { - std::set< std::string > vars; + std::unordered_set< TypeInstType::TypeEnvKey > vars; ptr bound; bool allowWidening; @@ -101,13 +101,13 @@ /// Singleton class constructor from TypeDecl - EqvClass( const TypeDecl * decl ) - : vars{ decl->name }, bound(), allowWidening( true ), data( decl ) {} + EqvClass( const TypeInstType * inst ) + : vars{ *inst }, bound(), allowWidening( true ), data( inst->base ) {} /// Singleton class constructor from substitution - EqvClass( const std::string & v, const Type * b ) + EqvClass( const TypeInstType::TypeEnvKey & v, const Type * b ) : vars{ v }, bound( b ), allowWidening( false ), data( TypeDecl::Dtype, false ) {} /// Single-var constructor (strips qualifiers from bound type) - EqvClass( const std::string & v, const Type * b, bool w, const TypeDecl::Data & d ) + EqvClass( const TypeInstType::TypeEnvKey & v, const Type * b, bool w, const TypeDecl::Data & d ) : vars{ v }, bound( b ), allowWidening( w ), data( d ) { reset_qualifiers( bound ); @@ -115,5 +115,5 @@ /// Double-var constructor - EqvClass( const std::string & v, const std::string & u, bool w, const TypeDecl::Data & d ) + EqvClass( const TypeInstType::TypeEnvKey & v, const TypeInstType::TypeEnvKey & u, bool w, const TypeDecl::Data & d ) : vars{ v, u }, bound(), allowWidening( w ), data( d ) {} @@ -131,5 +131,5 @@ public: /// Finds the equivalence class containing a variable; nullptr for none such - const EqvClass * lookup( const std::string & var ) const; + const EqvClass * lookup( const TypeInstType::TypeEnvKey & var ) const; /// Add a new equivalence class for each type variable @@ -207,5 +207,5 @@ /// Private lookup API; returns array index of string, or env.size() for not found - ClassList::iterator internal_lookup( const std::string & ); + ClassList::iterator internal_lookup( const TypeInstType::TypeEnvKey & ); }; Index: src/AST/TypeSubstitution.cpp =================================================================== --- src/AST/TypeSubstitution.cpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/TypeSubstitution.cpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -39,5 +39,4 @@ void TypeSubstitution::initialize( const TypeSubstitution &src, TypeSubstitution &dest ) { dest.typeEnv.clear(); - dest.varEnv.clear(); dest.add( src ); } @@ -47,26 +46,23 @@ typeEnv[ i->first ] = i->second; } // for - for ( VarEnvType::const_iterator i = other.varEnv.begin(); i != other.varEnv.end(); ++i ) { - varEnv[ i->first ] = i->second; - } // for } -void TypeSubstitution::add( std::string formalType, const Type *actualType ) { - typeEnv[ formalType ] = actualType; +void TypeSubstitution::add( const TypeInstType * formalType, const Type *actualType ) { + typeEnv[ *formalType ] = actualType; } -void TypeSubstitution::addVar( std::string formalExpr, const Expr *actualExpr ) { - varEnv[ formalExpr ] = actualExpr; +void TypeSubstitution::add( const TypeInstType::TypeEnvKey & key, const Type * actualType) { + typeEnv[ key ] = actualType; } -void TypeSubstitution::remove( std::string formalType ) { - TypeEnvType::iterator i = typeEnv.find( formalType ); +void TypeSubstitution::remove( const TypeInstType * formalType ) { + TypeEnvType::iterator i = typeEnv.find( *formalType ); if ( i != typeEnv.end() ) { - typeEnv.erase( formalType ); + typeEnv.erase( *formalType ); } // if } -const Type *TypeSubstitution::lookup( std::string formalType ) const { - TypeEnvType::const_iterator i = typeEnv.find( formalType ); +const Type *TypeSubstitution::lookup( const TypeInstType * formalType ) const { + TypeEnvType::const_iterator i = typeEnv.find( *formalType ); // break on not in substitution set @@ -75,11 +71,9 @@ // attempt to transitively follow TypeInstType links. while ( const TypeInstType *actualType = i->second.as()) { - const std::string& typeName = actualType->name; - // break cycles in the transitive follow - if ( formalType == typeName ) break; + if ( *formalType == *actualType ) break; // Look for the type this maps to, returning previous mapping if none-such - i = typeEnv.find( typeName ); + i = typeEnv.find( *actualType ); if ( i == typeEnv.end() ) return actualType; } @@ -90,5 +84,5 @@ bool TypeSubstitution::empty() const { - return typeEnv.empty() && varEnv.empty(); + return typeEnv.empty(); } @@ -98,8 +92,10 @@ TypeSubstitution * newEnv; EnvTrimmer( const TypeSubstitution * env, TypeSubstitution * newEnv ) : env( env ), newEnv( newEnv ){} - void previsit( TypeDecl * tyDecl ) { + void previsit( FunctionType * ftype ) { // transfer known bindings for seen type variables - if ( const Type * t = env->lookup( tyDecl->name ) ) { - newEnv->add( tyDecl->name, t ); + for (auto & formal : ftype->forall) { + if ( const Type * t = env->lookup( formal ) ) { + newEnv->add( formal, t ); + } } } @@ -130,8 +126,8 @@ const Type * TypeSubstitution::Substituter::postvisit( const TypeInstType *inst ) { - BoundVarsType::const_iterator bound = boundVars.find( inst->name ); + BoundVarsType::const_iterator bound = boundVars.find( *inst ); if ( bound != boundVars.end() ) return inst; - TypeEnvType::const_iterator i = sub.typeEnv.find( inst->name ); + TypeEnvType::const_iterator i = sub.typeEnv.find( *inst ); if ( i == sub.typeEnv.end() ) { return inst; @@ -141,5 +137,5 @@ // TODO: investigate preventing type variables from being bound to themselves in the first place. if ( const TypeInstType * replacement = i->second.as() ) { - if ( inst->name == replacement->name ) { + if ( *inst == *replacement ) { return inst; } @@ -156,24 +152,15 @@ } -const Expr * TypeSubstitution::Substituter::postvisit( const NameExpr * nameExpr ) { - VarEnvType::const_iterator i = sub.varEnv.find( nameExpr->name ); - if ( i == sub.varEnv.end() ) { - return nameExpr; - } else { - subCount++; - return i->second; - } // if -} - void TypeSubstitution::Substituter::previsit( const FunctionType * ptype ) { GuardValue( boundVars ); // bind type variables from forall-qualifiers if ( freeOnly ) { - for ( const TypeDecl * tyvar : ptype->forall ) { - boundVars.insert( tyvar->name ); + for ( auto & tyvar : ptype->forall ) { + boundVars.insert( *tyvar ); } // for } // if } +/* void TypeSubstitution::Substituter::handleAggregateType( const BaseInstType * type ) { GuardValue( boundVars ); @@ -184,5 +171,5 @@ if ( ! type->params.empty() ) { for ( const TypeDecl * tyvar : decl->params ) { - boundVars.insert( tyvar->name ); + boundVars.insert( *tyvar ); } // for } // if @@ -198,4 +185,5 @@ handleAggregateType( aggregateUseType ); } +*/ } // namespace ast Index: src/AST/TypeSubstitution.hpp =================================================================== --- src/AST/TypeSubstitution.hpp (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/TypeSubstitution.hpp (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -69,11 +69,10 @@ } - void add( std::string formalType, const Type *actualType ); + void add( const TypeInstType * formalType, const Type *actualType ); + void add( const TypeInstType::TypeEnvKey & key, const Type *actualType ); void add( const TypeSubstitution &other ); - void remove( std::string formalType ); - const Type *lookup( std::string formalType ) const; + void remove( const TypeInstType * formalType ); + const Type *lookup( const TypeInstType * formalType ) const; bool empty() const; - - void addVar( std::string formalExpr, const Expr *actualExpr ); template< typename FormalIterator, typename ActualIterator > @@ -101,8 +100,6 @@ friend class Pass; - typedef std::unordered_map< std::string, ptr > TypeEnvType; - typedef std::unordered_map< std::string, ptr > VarEnvType; + typedef std::unordered_map< TypeInstType::TypeEnvKey, ptr > TypeEnvType; TypeEnvType typeEnv; - VarEnvType varEnv; public: @@ -113,10 +110,7 @@ auto end() const -> decltype( typeEnv. end() ) { return typeEnv. end(); } - auto beginVar() -> decltype( varEnv.begin() ) { return varEnv.begin(); } - auto endVar() -> decltype( varEnv. end() ) { return varEnv. end(); } - auto beginVar() const -> decltype( varEnv.begin() ) { return varEnv.begin(); } - auto endVar() const -> decltype( varEnv. end() ) { return varEnv. end(); } }; +// this is the only place where type parameters outside a function formal may be substituted. template< typename FormalIterator, typename ActualIterator > void TypeSubstitution::add( FormalIterator formalBegin, FormalIterator formalEnd, ActualIterator actualBegin ) { @@ -129,5 +123,5 @@ if ( const TypeExpr *actual = actualIt->template as() ) { if ( formal->name != "" ) { - typeEnv[ formal->name ] = actual->type; + typeEnv[ formal ] = actual->type; } // if } else { @@ -135,11 +129,10 @@ } // if } else { - // TODO: type check the formal and actual parameters - if ( (*formalIt)->name != "" ) { - varEnv[ (*formalIt)->name ] = *actualIt; - } // if + } // if } // for } + + template< typename FormalIterator, typename ActualIterator > @@ -147,4 +140,5 @@ add( formalBegin, formalEnd, actualBegin ); } + } // namespace ast @@ -164,18 +158,17 @@ const Type * postvisit( const TypeInstType * aggregateUseType ); - const Expr * postvisit( const NameExpr * nameExpr ); /// Records type variable bindings from forall-statements void previsit( const FunctionType * type ); /// Records type variable bindings from forall-statements and instantiations of generic types - void handleAggregateType( const BaseInstType * type ); + // void handleAggregateType( const BaseInstType * type ); - void previsit( const StructInstType * aggregateUseType ); - void previsit( const UnionInstType * aggregateUseType ); + // void previsit( const StructInstType * aggregateUseType ); + // void previsit( const UnionInstType * aggregateUseType ); const TypeSubstitution & sub; int subCount = 0; bool freeOnly; - typedef std::unordered_set< std::string > BoundVarsType; + typedef std::unordered_set< TypeInstType::TypeEnvKey > BoundVarsType; BoundVarsType boundVars; Index: src/AST/module.mk =================================================================== --- src/AST/module.mk (revision 361bf012e550db91b38f772bfbc7cb7ed2e49033) +++ src/AST/module.mk (revision 8ba363e6454b54630aee996eb4e6f65ade4609d3) @@ -33,7 +33,4 @@ AST/Expr.cpp \ AST/Expr.hpp \ - AST/ForallSubstitutionTable.cpp \ - AST/ForallSubstitutionTable.hpp \ - AST/ForallSubstitutor.hpp \ AST/FunctionSpec.hpp \ AST/Fwd.hpp \