fix: solve todos

sillydan1 · Mar 20, 2023 · 9017577 · 9017577
1 parent 4e80daa
commit 9017577
Show file tree

Hide file tree

Showing 9 changed files with 49 additions and 28 deletions.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -34,6 +34,7 @@ option(ENABLE_Z3 "Enables the download and compilation of the expr::z3_driver dr
 CPMAddPackage("gh:yalibs/yaoverload@1.0.0")
 CPMAddPackage("gh:yalibs/yahashcombine@1.0.0")
 CPMAddPackage("gh:yalibs/yatree@1.2.1")
+CPMAddPackage("gh:yalibs/yauuid@1.0.1")
 # demo dependencies
 CPMAddPackage("gh:yalibs/yatimer@1.0.0")
 CPMAddPackage("gh:sillydan1/argvparse@1.2.3")
@@ -66,6 +67,7 @@ target_include_directories(${PROJECT_NAME} PUBLIC
         ${yatimer_SOURCE_DIR}/include
         ${yaoverload_SOURCE_DIR}/include
         ${yahashcombine_SOURCE_DIR}/include
+        ${yauuid_SOURCE_DIR}/include
         ${argvparse_SOURCE_DIR}/include
         ${z3_SOURCE_DIR}/src/api/c++
         ${z3_SOURCE_DIR}/include

diff --git a/cmake/Z3.cmake b/cmake/Z3.cmake
@@ -1,17 +1,17 @@
 # warning, only tested with: z3-4.11.2
 function(get_z3_zip_file vnum)
     message(STATUS "Looking for Z3 release for platform: ${CMAKE_SYSTEM_NAME} ${CMAKE_SYSTEM_PROCESSOR}")
-    set(z3vstr "gh:Z3Prover/z3#${vnum}" PARENT_SCOPE)
+    set(z3vstr "Z3_NOT_FOUND" PARENT_SCOPE)
     if (CMAKE_SYSTEM_NAME STREQUAL "Linux")
         set(z3vstr "https://github.com/Z3Prover/z3/releases/download/${vnum}/${vnum}-x64-glibc-2.31.zip" PARENT_SCOPE)
     elseif (CMAKE_SYSTEM_NAME STREQUAL "Windows")
-        if (CMAKE_SYSTEM_PROCESSOR STREQUAL "x64")
+        if (CMAKE_SYSTEM_PROCESSOR STREQUAL "x64" OR CMAKE_SYSTEM_PROCESSOR STREQUAL "x86_64")
             set(z3vstr "https://github.com/Z3Prover/z3/releases/download/${vnum}/${vnum}-x64-win.zip" PARENT_SCOPE)
-        elseif (CMAKE_SYSTEM_PROCESSOR STREQUAL "x86")
+        elseif (CMAKE_SYSTEM_PROCESSOR STREQUAL "x86" or CMAKE_SYSTEM_PROCESSOR STREQUAL "x86_32")
             set(z3vstr "https://github.com/Z3Prover/z3/releases/download/${vnum}/${vnum}-x86-win.zip" PARENT_SCOPE)
         endif()
     elseif (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
-        if (CMAKE_SYSTEM_PROCESSOR STREQUAL "x64")
+        if (CMAKE_SYSTEM_PROCESSOR STREQUAL "x64" OR CMAKE_SYSTEM_PROCESSOR STREQUAL "x86_64")
             set(z3vstr "https://github.com/Z3Prover/z3/releases/download/${vnum}/${vnum}-x64-osx-10.16.zip" PARENT_SCOPE)
         elseif (CMAKE_SYSTEM_PROCESSOR STREQUAL "arm64")
             set(z3vstr "https://github.com/Z3Prover/z3/releases/download/${vnum}/${vnum}-arm64-osx-11.0.zip" PARENT_SCOPE)

diff --git a/src/driver/evaluator.cpp b/src/driver/evaluator.cpp
@@ -53,7 +53,7 @@ namespace expr {
                 },
                 [&](const operator_t& o) {
                     switch (o.operator_type) {
-                        // FIX: This this does not consider if children().size() > 2 
+                        // TODO:: This this does not consider if children().size() > 2 
                         case operator_type_t::minus:    return op.sub(evaluate(tree.children()[0]), evaluate(tree.children()[1]));
                         case operator_type_t::plus:     return op.add(evaluate(tree.children()[0]), evaluate(tree.children()[1]));
                         case operator_type_t::star:     return op.mul(evaluate(tree.children()[0]), evaluate(tree.children()[1]));

diff --git a/src/driver/z3/z3-driver.cpp b/src/driver/z3/z3-driver.cpp
@@ -21,12 +21,22 @@
  * SOFTWARE.
  */
 #include "z3-driver.h"
+#include "implementation/uuid.h"
 #include "symbol_table.h"
+#include <uuid>
 
 namespace expr {
-    // TODO: delay_identfier should be randomly generated to avoid known/unknown collissions
+    auto generate_unique_identifier(const symbol_table_t& env0, const symbol_table_t& env1) -> std::string {
+        // Reroll until you hit something that hasn't been declared yet. 
+        // (this breaks if the environments declare ALL POSSIBLE UUIDv4 combinations, but that is very unlikely, so I consider that out-of-scope)
+        auto result = ya::uuid_v4();
+        while(env0.contains(result) || env1.contains(result))
+            result = ya::uuid_v4(); 
+        return result;
+    }
+
     z3_driver::z3_driver(const symbol_table_t& known, const symbol_table_t& unknown) 
-     : c{}, s{c}, delay_identifier{"d"}, known{known}, unknown{unknown} {} 
+     : c{}, s{c}, delay_identifier{generate_unique_identifier(known, unknown)}, known{known}, unknown{unknown} {} 
 
     auto z3_driver::find_solution(const syntax_tree_t& expression) -> std::optional<symbol_table_t> {
         s.add(as_z3(expression)); // NOTE: Only accepts boolean expressions (will throw if not)

diff --git a/src/expr-lang/ast-factory.cpp b/src/expr-lang/ast-factory.cpp
@@ -54,15 +54,5 @@ namespace expr {
     auto ast_factory::build_root(const syntax_tree_t& child) -> syntax_tree_t {
         return syntax_tree_t{}.concat(child);
     }
-
-    auto ast_factory::build_declaration(const std::string &identifier, const syntax_tree_t &tree, const symbol_access_modifier_t& access_modifier) -> syntax_tree_t {
-        return build_declaration(identifier, tree, symbol_type_name_t::_auto, access_modifier);
-    }
-
-    auto ast_factory::build_declaration(const std::string& identifier, const syntax_tree_t& tree, const symbol_type_name_t& type_name, const symbol_access_modifier_t& access_modifier) -> syntax_tree_t {
-        // TODO: add the thing to the thing
-        std::cout << identifier << " " << type_name << " " << access_modifier << ": " << tree << std::endl;
-        return tree;
-    }
 }
 
diff --git a/src/expr-lang/ast-factory.h b/src/expr-lang/ast-factory.h
@@ -38,9 +38,6 @@ namespace expr {
         virtual auto build_literal(const symbol_value_t& value) -> syntax_tree_t;
         virtual auto build_identifier(const std::string& identifier) -> syntax_tree_t;
         virtual auto build_root(const syntax_tree_t& child) -> syntax_tree_t;
-
-        virtual auto build_declaration(const std::string& identifier, const syntax_tree_t& tree, const symbol_access_modifier_t& access_modifier) -> syntax_tree_t;
-        virtual auto build_declaration(const std::string& identifier, const syntax_tree_t& tree, const symbol_type_name_t& type_name = symbol_type_name_t::_auto, const symbol_access_modifier_t& access_modifier = symbol_access_modifier_t::_private) -> syntax_tree_t;
     };
 }
 

diff --git a/src/expr-lang/expr.y b/src/expr-lang/expr.y
@@ -148,12 +148,34 @@ lit:
 /* ================================================== */
 
 void expr::parser::error(const location_type& l, const std::string& msg) {
-    // TODO: This assumes that the input string is always 1 line - it will not look good on multiline inputs
+    // TODO: We should print to the injected stream instead of directly to cerr
+    // TODO: This should provide a WINDOW to peek into rather than print the entire file/expression
+    // TODO: This is a mess... I can't use yylineno and l.begin/end.line is always just '1' so this insane code will suffice for now
     if(args.expression) {
-        std::cerr << msg << "\n" << args.expression.value() << "\n"; 
-        for(int i = 0; i < l.begin.column - 1; i++)
-            std::cerr << "_";
-        std::cerr << "^\n";
+        std::cerr << msg << " between column " << l.begin.column << " and " << l.end.column << ":\n";
+        auto& e = args.expression.value();
+        int i = 0; int offset = 0;
+        for(; i < l.begin.column - 1; i++, offset++) {
+            if(e[i] == '\n')
+                offset = 0;
+            std::cerr << e[i];
+        }
+        for(; i < l.end.column - 1; i++)
+            std::cerr << e[i];
+        for(; i < e.size() - 1; i++) {
+            if(e[i] == '\n')
+                break;
+            std::cerr << e[i];
+        }
+        std::cerr << "\n";
+        for(int j = 0; j < offset-1; j++)
+            std::cerr << "~";
+        for(int j = l.begin.column - 1; j < l.end.column-1; j++)
+            std::cerr << "^";
+        std::cerr << "\n";
+        for(i++; i < e.size() - 1; i++)
+            std::cerr << e[i];
+        std::cerr << "\n";
     } else
         std::cerr << msg << " at " << l << "\n"; // boring
 }

diff --git a/src/expr-lang/language-builder.cpp b/src/expr-lang/language-builder.cpp
@@ -39,7 +39,7 @@ namespace expr {
     }
 
     auto declaration_tree_builder::build() -> result_t {
-        return result; // TODO: check for proper build
+        return result;
     }
 }
 
diff --git a/src/generic-driver.cpp b/src/generic-driver.cpp
@@ -97,7 +97,7 @@ namespace expr {
         parser_args pa{s, &sc, &factory, &builder};
         parser p{pa};
         if(p.parse() != 0)
-            throw std::logic_error("unable to parse the expression(s)" + s);
+            throw std::logic_error("unable to parse the expression(s)");
         auto res = builder.build();
         for(auto& e : res.declarations)
             declarations[e.first] = e.second.tree;
@@ -113,7 +113,7 @@ namespace expr {
         parser_args pa{s, &sc, &factory, &builder};
         parser p{pa};
         if(p.parse() != 0)
-            throw std::logic_error("unable to parse the expression(s): " + s);
+            throw std::logic_error("unable to parse the expression(s)");
         auto res = builder.build();
         symbol_operator op{};
         evaluator e{{}, op};