Type Inference

* fixed type inference for conditional expressions etc. - realted to ref sealangdotorg/sea#20 * updated error codes * added additional type check in the consistency check pass
casm-lang · May 18, 2017 · 0387bf1 · 0387bf1
1 parent 1fa9732
commit 0387bf1
Show file tree

Hide file tree

Showing 4 changed files with 122 additions and 7 deletions.
diff --git a/src/Codes.h b/src/Codes.h
@@ -117,6 +117,10 @@ namespace libcasm_fe
         TypeInferenceInvalidIfExpression = 0x1003,
         TypeInferenceInvalidForallExpression = 0x1004
 
+        ,
+        TypeInferenceInvalidConditionalExpressionCondition = 0x1005,
+        TypeInferenceInvalidConditionalExpressionPaths = 0x1006
+
         ,
         TypeCheckUseOfUndeclaredFunctionInInitially = 0xc000
 
@@ -153,6 +157,12 @@ namespace libcasm_fe
         UpdateSetClash = 0x7000,
         UpdateSetMergeConflict = 0x7001
 
+        // --------------------------------------------------------- 9*** ...
+        // unsorted run-time errors
+        ,
+        ConditionalRuleInvalidCondition = 0x9000,
+        ConditionalExpressionInvalidCondition = 0x9001
+
         // --------------------------------------------------------- fff* ...
         // not categorized errors
         ,

diff --git a/src/analyze/ConsistencyCheckPass.cpp b/src/analyze/ConsistencyCheckPass.cpp
@@ -62,6 +62,10 @@ class ConsistencyCheckVisitor final : public RecursiveVisitor
     void visit( FunctionDefinition& node ) override;
 
     void visit( ReferenceAtom& node ) override;
+    void visit( ValueAtom& node ) override;
+    void visit( UndefAtom& node ) override;
+
+    void verify( const TypedNode& node ) const;
 
   private:
     Logger& m_log;
@@ -135,9 +139,28 @@ void ConsistencyCheckVisitor::visit( ReferenceAtom& node )
         throw CompiletimeException( node.identifier()->sourceLocation(),
             node.identifier()->path(), Code::Unspecified );
     }
-    else
+
+    verify( node );
+}
+
+void ConsistencyCheckVisitor::visit( ValueAtom& node )
+{
+    RecursiveVisitor::visit( node );
+    verify( node );
+}
+
+void ConsistencyCheckVisitor::visit( UndefAtom& node )
+{
+    RecursiveVisitor::visit( node );
+    verify( node );
+}
+
+void ConsistencyCheckVisitor::verify( const TypedNode& node ) const
+{
+    if( not node.type() )
     {
-        assert( node.type() );
+        m_log.error( { node.sourceLocation() }, "found node without a type",
+            Code::Unspecified );
     }
 }
 

diff --git a/src/analyze/TypeInferencePass.cpp b/src/analyze/TypeInferencePass.cpp
@@ -552,6 +552,7 @@ class TypeInferenceVisitor final : public RecursiveVisitor
     void visit( DerivedDefinition& node ) override;
     void visit( RuleDefinition& node ) override;
 
+    void visit( UndefAtom& node ) override;
     void visit( ValueAtom& node ) override;
     void visit( ReferenceAtom& node ) override;
     void visit( DirectCallExpression& node ) override;
@@ -654,6 +655,11 @@ void TypeInferenceVisitor::visit( RuleDefinition& node )
     }
 }
 
+void TypeInferenceVisitor::visit( UndefAtom& node )
+{
+    RecursiveVisitor::visit( node );
+}
+
 void TypeInferenceVisitor::visit( ValueAtom& node )
 {
     RecursiveVisitor::visit( node );
@@ -936,8 +942,6 @@ void TypeInferenceVisitor::visit( DirectCallExpression& node )
             break;
         }
     }
-
-    // assert( node.type() );
 }
 
 void TypeInferenceVisitor::visit( IndirectCallExpression& node )
@@ -1000,8 +1004,78 @@ void TypeInferenceVisitor::visit( ListExpression& node )
 }
 void TypeInferenceVisitor::visit( ConditionalExpression& node )
 {
+    const auto& resTypes = m_resultTypes[&node ];
+    for( auto type : resTypes )
+    {
+        m_resultTypes[ node.thenExpression().get() ].emplace_back( type );
+        m_resultTypes[ node.elseExpression().get() ].emplace_back( type );
+    }
+
     RecursiveVisitor::visit( node );
+
+    const auto& condExpr = *node.condition();
+    auto& thenExpr = *node.thenExpression();
+    auto& elseExpr = *node.elseExpression();
+
+    if( condExpr.type() )
+    {
+        if( *condExpr.type() != *BOOLEAN )
+        {
+            m_log.error( { condExpr.sourceLocation() },
+                "condition type of conditional expression is not of type "
+                "'Boolean', "
+                "found type '"
+                    + condExpr.type()->description()
+                    + "'",
+                Code::TypeInferenceInvalidConditionalExpressionCondition );
+        }
+    }
+
+    if( resTypes.size() > 0 )
+    {
+        inference( "conditional expression", 0, node );
+    }
+
+    if( thenExpr.type() and elseExpr.type() )
+    {
+        if( *thenExpr.type() != *elseExpr.type() )
+        {
+            m_log.error(
+                { thenExpr.sourceLocation(), elseExpr.sourceLocation() },
+                "types of conditional expression paths does not match, "
+                "found'"
+                    + thenExpr.type()->description()
+                    + "' at 'then' path, and '"
+                    + elseExpr.type()->description()
+                    + "' at 'else' path",
+                Code::TypeInferenceInvalidConditionalExpressionPaths );
+            return;
+        }
+    }
+
+    if( thenExpr.type() and elseExpr.id() == Node::ID::UNDEF_ATOM )
+    {
+        elseExpr.setType( thenExpr.type() );
+    }
+
+    if( thenExpr.id() == Node::ID::UNDEF_ATOM and elseExpr.type() )
+    {
+        thenExpr.setType( elseExpr.type() );
+    }
+
+    if( node.type() and thenExpr.id() == Node::ID::UNDEF_ATOM
+        and elseExpr.id() == Node::ID::UNDEF_ATOM )
+    {
+        thenExpr.setType( node.type() );
+        elseExpr.setType( node.type() );
+    }
+
+    if( not node.type() )
+    {
+        node.setType( thenExpr.type() );
+    }
 }
+
 void TypeInferenceVisitor::visit( UniversalQuantifierExpression& node )
 {
     RecursiveVisitor::visit( node );
@@ -1014,6 +1088,13 @@ void TypeInferenceVisitor::visit( ExistentialQuantifierExpression& node )
 void TypeInferenceVisitor::visit( LetRule& node )
 {
     node.variable()->accept( *this );
+
+    if( node.variable()->type() )
+    {
+        m_resultTypes[ node.expression().get() ].emplace_back(
+            node.variable()->type()->id() );
+    }
+
     push( *node.variable() );
     node.expression()->accept( *this );
 
@@ -1059,7 +1140,8 @@ void TypeInferenceVisitor::visit( UpdateRule& node )
 void TypeInferenceVisitor::assignment( const Node& node, TypedNode& lhs,
     TypedNode& rhs, const std::string& dst, const std::string& src )
 {
-    if( not rhs.type() and rhs.id() == Node::ID::UNDEF_ATOM and lhs.type() )
+    if( lhs.type()
+        and not rhs.type() ) // and rhs.id() == Node::ID::UNDEF_ATOM and  )
     {
         rhs.setType( lhs.type()->ptr_result() );
     }

diff --git a/src/execute/NumericExecutionPass.cpp b/src/execute/NumericExecutionPass.cpp
@@ -710,7 +710,7 @@ void ExecutionVisitor::visit( DirectCallExpression& node )
                     "builtin has thrown an exception: "
                         + std::string( e.what() ),
                     m_frameStack.generateBacktrace( node.sourceLocation() ),
-                    Code::Unspecified );
+                    Code::AssertInvalidExpression );
             }
             m_frameStack.pop();
             break;
@@ -873,7 +873,7 @@ void ExecutionVisitor::visit( ConditionalExpression& node )
         throw RuntimeException( node.condition()->sourceLocation(),
             "condition must be true or false but was undef",
             m_frameStack.generateBacktrace( node.sourceLocation() ),
-            Code::Unspecified );
+            Code::ConditionalExpressionInvalidCondition );
     }
     else if( condition.value() == true )
     {