summaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--example/example_02_nectar/example.nc5
-rw-r--r--include/CompilerKit/AST.h1
-rw-r--r--proofs/Makefile13
-rw-r--r--proofs/NectarDriver/Impl.v11
-rw-r--r--proofs/NectarDriver/Traits.v10
-rw-r--r--proofs/_CoqProject4
-rw-r--r--src/CompilerKit/src/Frontends/NectarCompiler+AMD64.cpp6
-rw-r--r--src/CompilerKit/src/Frontends/NectarCompiler+Chk.cpp4
-rw-r--r--src/CompilerKit/src/Frontends/NectarCompiler+PTX.cpp6
9 files changed, 12 insertions, 48 deletions
diff --git a/example/example_02_nectar/example.nc b/example/example_02_nectar/example.nc
index 5e95c44..b9e13d3 100644
--- a/example/example_02_nectar/example.nc
+++ b/example/example_02_nectar/example.nc
@@ -2,6 +2,9 @@ extern exit;
const main()
{
- let foo := exit(0);
+ let _ := exit(0);
+ if (_ === 0): {
+ return 0;
+ }
return 0;
}
diff --git a/include/CompilerKit/AST.h b/include/CompilerKit/AST.h
index c1313ce..27f57be 100644
--- a/include/CompilerKit/AST.h
+++ b/include/CompilerKit/AST.h
@@ -46,6 +46,7 @@ enum struct KeywordKind {
kKeywordKindIf,
kKeywordKindVariableAssign,
kKeywordKindVariableDec,
+ kKeywordKindVariableEquals,
kKeywordKindVariableInc,
kKeywordKindTypedef,
kKeywordKindEndLine, // Optional in Nectar.
diff --git a/proofs/Makefile b/proofs/Makefile
deleted file mode 100644
index 1efedbc..0000000
--- a/proofs/Makefile
+++ /dev/null
@@ -1,13 +0,0 @@
-COQMAKEFILE ?= Makefile.coq
-
-all: $(COQMAKEFILE)
- $(MAKE) -f $(COQMAKEFILE)
-
-$(COQMAKEFILE): _CoqProject
- coq_makefile -f _CoqProject -o $(COQMAKEFILE)
-
-clean: $(COQMAKEFILE)
- $(MAKE) -f $(COQMAKEFILE) clean
- rm -f $(COQMAKEFILE) $(COQMAKEFILE).conf
-
-.PHONY: all clean \ No newline at end of file
diff --git a/proofs/NectarDriver/Impl.v b/proofs/NectarDriver/Impl.v
deleted file mode 100644
index 37b8878..0000000
--- a/proofs/NectarDriver/Impl.v
+++ /dev/null
@@ -1,11 +0,0 @@
-(*
- NectarDriver: Impl keyword.
-
- The Impl keyword defines methods and/or traits associated with a specific identifier N.
-
- Author: Amlal El Mahrouss
- Formalization: January 2026
-*)
-
-Require Import Logic.Classical_Prop.
-Require Import NectarDriver.Traits. \ No newline at end of file
diff --git a/proofs/NectarDriver/Traits.v b/proofs/NectarDriver/Traits.v
deleted file mode 100644
index 2c5bb9c..0000000
--- a/proofs/NectarDriver/Traits.v
+++ /dev/null
@@ -1,10 +0,0 @@
-(*
- NectarDriver: Traits keyword.
-
- The Traits keyword defines formal semantic rules associated with a specific identifier N.
-
- Author: Amlal El Mahrouss
- Formalization: January 2026
-*)
-
-Require Import Logic.Classical_Prop.
diff --git a/proofs/_CoqProject b/proofs/_CoqProject
deleted file mode 100644
index 3715404..0000000
--- a/proofs/_CoqProject
+++ /dev/null
@@ -1,4 +0,0 @@
--R NectarDriver NectarDriver
-
-NectarDriver/Impl.v
-NectarDriver/Traits.v \ No newline at end of file
diff --git a/src/CompilerKit/src/Frontends/NectarCompiler+AMD64.cpp b/src/CompilerKit/src/Frontends/NectarCompiler+AMD64.cpp
index baf7e2f..97b5161 100644
--- a/src/CompilerKit/src/Frontends/NectarCompiler+AMD64.cpp
+++ b/src/CompilerKit/src/Frontends/NectarCompiler+AMD64.cpp
@@ -348,10 +348,7 @@ CompilerKit::SyntaxLeafList::SyntaxLeaf CompilerFrontendNectarAMD64::Compile(
}
std::vector<std::pair<CompilerKit::STLString, CompilerKit::STLString>> operators = {
- {"=:", "jne"},
- {"!=:", "je"},
- {">:", "jl"},
- {"<:", "jg"},
+ {"!==", "ne"}, {"===", "eq"}, {">", "jl"}, {"<", "jg"}, {">=", "jle"}, {"<=", "jge"},
};
for (auto& op : operators) {
@@ -1650,6 +1647,7 @@ NECTAR_MODULE(CompilerNectarAMD64) {
kKeywords.emplace_back("(", CompilerKit::KeywordKind::kKeywordKindFunctionStart);
kKeywords.emplace_back(")", CompilerKit::KeywordKind::kKeywordKindFunctionEnd);
kKeywords.emplace_back(":=", CompilerKit::KeywordKind::kKeywordKindVariableAssign);
+ kKeywords.emplace_back(":==", CompilerKit::KeywordKind::kKeywordKindVariableEquals);
kKeywords.emplace_back("+=", CompilerKit::KeywordKind::kKeywordKindVariableInc);
kKeywords.emplace_back("-=", CompilerKit::KeywordKind::kKeywordKindVariableDec);
kKeywords.emplace_back("const", CompilerKit::KeywordKind::kKeywordKindVariable);
diff --git a/src/CompilerKit/src/Frontends/NectarCompiler+Chk.cpp b/src/CompilerKit/src/Frontends/NectarCompiler+Chk.cpp
index c636f3a..c3faf49 100644
--- a/src/CompilerKit/src/Frontends/NectarCompiler+Chk.cpp
+++ b/src/CompilerKit/src/Frontends/NectarCompiler+Chk.cpp
@@ -58,7 +58,9 @@ CK_IMPORT_C bool NectarCheckLine(CompilerKit::STLString& input) {
if (input.find("(") != CompilerKit::STLString::npos &&
input.find("const") == CompilerKit::STLString::npos &&
- input.find("let") == CompilerKit::STLString::npos) {
+ input.find("let") == CompilerKit::STLString::npos &&
+ input.find("if") == CompilerKit::STLString::npos &&
+ input.find("else") == CompilerKit::STLString::npos) {
if (input.find(";") == CompilerKit::STLString::npos) {
Detail::print_error("A function call must always end with ';'", "check");
return false;
diff --git a/src/CompilerKit/src/Frontends/NectarCompiler+PTX.cpp b/src/CompilerKit/src/Frontends/NectarCompiler+PTX.cpp
index 8b2b3bb..4583dfe 100644
--- a/src/CompilerKit/src/Frontends/NectarCompiler+PTX.cpp
+++ b/src/CompilerKit/src/Frontends/NectarCompiler+PTX.cpp
@@ -355,10 +355,7 @@ CompilerKit::SyntaxLeafList::SyntaxLeaf CompilerFrontendNectarPTX::Compile(
}
std::vector<std::pair<CompilerKit::STLString, CompilerKit::STLString>> operators = {
- {"=:", "ne"},
- {"!=:", "eq"},
- {">:", "lt"},
- {"<:", "gt"},
+ {"!==", "ne"}, {"===", "eq"}, {">", "lt"}, {"<", "gt"}, {">=", "lte"}, {"<=", "gte"},
};
for (auto& op : operators) {
@@ -1594,6 +1591,7 @@ NECTAR_MODULE(CompilerNectarPTX) {
kKeywords.emplace_back("->", CompilerKit::KeywordKind::kKeywordKindAccessChecked);
kKeywords.emplace_back("(", CompilerKit::KeywordKind::kKeywordKindFunctionAccess);
kKeywords.emplace_back(";", CompilerKit::KeywordKind::kKeywordKindEndLine);
+ kKeywords.emplace_back(":==", CompilerKit::KeywordKind::kKeywordKindVariableEquals);
kKeywords.emplace_back("return", CompilerKit::KeywordKind::kKeywordKindReturn);
kKeywords.emplace_back("extern", CompilerKit::KeywordKind::kKeywordKindExtern);
kKeywords.emplace_back("import", CompilerKit::KeywordKind::kKeywordKindImport);