Site keyword generation

.github/workflows/static.yml

@@ -34,50 +34,58 @@ jobs:
       url: ${{ steps.deployment.outputs.page_url }}
     runs-on: ubuntu-latest
     steps:
-      # Step 1: Check out the repository
+      # Check out the repository
       - name: Checkout
         uses: actions/checkout@v4
 
-      # Step 2: Set up Python environment
+      # Set up Python environment
       - name: Set up Python
         uses: actions/setup-python@v4
         with:
           python-version: '3.13.1'
 
-      # Step 3: Install dependencies
+      # Install dependencies
       - name: Install dependencies
         run: |
           python -m pip install --upgrade pip
           pip install -r ./gh_pages/requirements.txt
 
-      # Step 4: Run the Python convert script
+      # Run the Python convert script
       - name: Run convert script
-        run: python ./gh_pages/doc/convert.py
+        run: python ./gh_pages/scripts/convert.py
 
-      # Step 5: Run the Python index generate script
+      # Run the Python index generate script
       - name: Run index generate script
-        run: python ./gh_pages/doc/index_generate.py
+        run: python ./gh_pages/scripts/index_generate.py
 
-      # Step 6: Run the Python lib generate script
+      # Run the Python keywords script
+      - name: Check known tokens
+        run: python ./gh_pages/scripts/keywords.py
+
+        # Run the Python lib generate script
+      - name: Run lib generate script
+        run: python ./gh_pages/scripts/lib_generate.py
+
+        # Run the Python code block syntax generate script
       - name: Run lib generate script
-        run: python ./gh_pages/doc/lib_generate.py
+        run: python ./gh_pages/scripts/code_block_syntax_generate.py
 
-      # Step 7: Convert scss to css
+      # Convert scss to css
       - name: Convert scss to css
         run: pysassc ./gh_pages/css/style-dev.css ./gh_pages/css/style.css && pysassc ./gh_pages/css/stdlib-dev.css ./gh_pages/css/stdlib.css
 
-      # Step 8: Setup Pages
+      # Setup Pages
       - name: Setup Pages
         uses: actions/configure-pages@v5
 
-      # Step 9: Upload artifact
+      # Upload artifact
       - name: Upload artifact
         uses: actions/upload-pages-artifact@v3
         with:
           # Upload entire repository
           path: './gh_pages'
 
-      # Step 10: Deploy to gh pages
+      # Deploy to gh pages
       - name: Deploy to GitHub Pages
         id: deployment
         uses: actions/deploy-pages@v4

docs/knowledge-base/site-maintenance.md

@@ -10,7 +10,7 @@ For your convenience, we've split up this doc into different sections to make it
 
 ## Updating site content
 
-Most of the pages on the site are generated into html from the markdown files found in the `/gh_pages/doc` directory. If you want to update the content for those pages, just update the markdown file and `/gh_pages/doc/convert.py` will do the rest for you.
+Most of the pages on the site are generated into html from the markdown files found in the `/gh_pages/doc` directory. If you want to update the content for those pages, just update the markdown file and `/gh_pages/scripts/convert.py` will do the rest for you.
 
 The only three pages that are not automatically generated from the markdown files are
 

docs/knowledge-base/what-to-update.md

@@ -12,7 +12,7 @@ Any changes to the Deduce syntax should be reflected in the following places:
 - `parser.py`: code for the lark parser
 - `recursive-descent.py`: code for the recursive descent parser
 - `abstract_syntax.py`: code for all of the AST nodes
-- `gh_pages/doc/lib_generate.py`: generates the html files for the stdlib. (The list of known tokens mapping to token type should be updated and the safeHTMLify for additional operator symbols.)
+- `gh_pages/scripts/keywords.py`: The list of known tokens mapping to token type should be updated.
 - `gh_pages/js/codeUtils.js`: syntax highlighting for the site codeblocks.
 - `gh_pages/js/sandbox.js`: syntax highlighting for live code monaco editor.
 

gh_pages/js/codeUtils.js

@@ -1,32 +1,7 @@
-const operators = [
-    "->", "\\+\\+", "(?<!\\/|\\*)\\/(?!\\/|\\*)", "\\|", "&", "\\[\\+\\]", "\\[o\\]", "\\(=", 
-    "<=", ">=", "\\/=", "≠", "⊆", "≤", "≥", "∈", "∪", "\\+", "%", "(?<!\\/)\\*(?!\\/)", "⨄", 
-    "-", "∩", "∘", "λ", "@", ":", "&gt;", "&lt;", "\\(", "\\)", "{", "}", ",", "=", "\\.", "\\[", 
-    "\\]", ";", "#"
-]
-
-const prims = ["true", "false", "0", "[0-9]+", "empty"]
-
-const defines = ["node", "suc", "take", "set_of", "empty_no_members",
-    "single", "member_union", "single_equal", "length"]
-
-const primsSym = ["∅", "\\[0\\]", "\\?"]
-
-const types = ["MultiSet", "Option", "Pair", "Set", "List", "Int", "Nat", "int", "bool", "fn", "type"]
-
-const keywords = [
-    "define", "function", "fun", "switch", "case", "union", "if", "then", "else", "import",
-    "generic", "assert", "have", "transitive", "symmetric", "extensionality", "reflexive",
-    "injective", "sorry", "help", "conclude", "suffices", "enough", "by", "replace",
-    "conjunct", "induction", "where", "suppose", "with", "definition", "apply", "to", "cases",
-    "obtain", "stop", "equations", "of", "arbitrary", "choose", "term", "from",
-    "assume", "for", "recall", "in", "and", "or", "print", "not", "some", "all", "theorem",
-    "lemma", "proof", "end", "replace", "recursive", "expand", "auto", "array", "associative",
-    "evaluate", "export", "recfun", "show", "terminates", "postulate"
-]
-
+import { operators, prims, types, keywords, libs } from './codeKeywords.js'
 
 function getRegex(ls) {
+	if (ls.length == 0) return "$"
     let fullRegex = ls.reduce((a, s) => `\\b${s}\\b|` + a, "")
     return fullRegex.substring(0, fullRegex.length - 1)
 }
@@ -45,35 +20,44 @@ function replaceLeadingTabs(str) {
 function codeToHTML(code) {
     // scan to get user defined functions and variables
     const fncRe = new RegExp("(?<=\\bfunction\\s)\\w+(?=\\s*[\\(|<])", "g")
+	const funRe = new RegExp("(?<=\\bfun\\s)\\w+(?=\\s*[\\(|<])", "g")
     const recRe = new RegExp("(?<=\\brecursive\\s)\\w+(?=\\s*[\\(|<])", "g")
     const thmRe = new RegExp("(?<=\\btheorem\\s)\\w+(?=\\s*:)", "g")
     const uniRe = new RegExp("(?<=\\bunion\\s)\\w+(?=\\s*<)?", "g")
     const defRe = new RegExp("(?<=\\bdefine\\s)\\w+(?=\\s*:)?", "g")
-    let userDefs = []
+	const appRe = new RegExp("(\\w+)\\(", "g")
+    let defs = []
         .concat(Array.from(code.matchAll(fncRe)).flat())
+	    .concat(Array.from(code.matchAll(funRe)).flat())
         .concat(Array.from(code.matchAll(recRe)).flat())
         .concat(Array.from(code.matchAll(thmRe)).flat())
         .concat(Array.from(code.matchAll(uniRe)).flat())
         .concat(Array.from(code.matchAll(defRe)).flat())
-    userDefs = userDefs.filter(e => e !== undefined && e !== "operator")
-
+		.concat(Array.from(code.matchAll(appRe)).map(e => e[1]))
+    defs = defs.filter(e => e !== undefined && e !== "operator")
+
     // prep regex
     const ore = new RegExp(getRegexSymbols(operators), "g")
-    const pre = new RegExp(getRegex(prims) + "|" + getRegexSymbols(primsSym), "g")
-    const tre = new RegExp(getRegex(types), "g")
+    const pre = new RegExp(getRegex(prims), "g")
+    const tre = new RegExp(getRegex(types) + '|' + getRegex(libs), "g")
     const kre = new RegExp(getRegex(keywords), "g")
-    const dre = new RegExp(getRegex(defines.concat(userDefs)), "g")
-    const cre = new RegExp("(\\/\\*(.|\r|\n)+\\*\\/|\\/\\/.+)", "g")
+    const dre = new RegExp(getRegex(defs), "g")
+    const cre = new RegExp("(\\&sol;\\*(.|\r|\n)+\\*\\&sol;|\\&sol;\\&sol;[^\r\n]+)", "g")
     // remove first new line
     code = (code[0] == '\n' ? code.substring(1) : code)
     // fixing things for html
+	code = code.replaceAll(";", "(TEMPORARY_AMP)semi;");
+	code = code.replaceAll("&", "&amp;");
+	code = code.replaceAll("=", "&equals;");
+	code = code.replaceAll("/", "&sol;");
     code = code.replaceAll("<", "&lt;");
     code = code.replaceAll(">", "&gt;");
+	code = code.replaceAll("(TEMPORARY_AMP)", "&");
     // (heavy quote) lexing (heavy quote)
     code = code.replaceAll("\t", "    ");
     code = code.replaceAll(" ", "\x00"); // temporary
-    code = code.replaceAll(ore, "<span class=\"operator\">$&</span>");
     code = code.replaceAll(cre, "<span class=\"comment\">$&</span>");
+    code = code.replaceAll(ore, "<span class=\"operator\">$&</span>");
     code = code.replaceAll(pre, "<span class=\"prim\">$&</span>");
     code = code.replaceAll(tre, "<span class=\"type\">$&</span>");
     code = code.replaceAll(kre, "<span class=\"keyword\">$&</span>");
@@ -97,7 +81,7 @@ function codeToHTML(code) {
 }
 
 function removeImports(code){
-    split = code.split("\n");
+    let split = code.split("\n");
     // remove import statements
     while(split[0].trim().substring(0, 6) == "import") split.shift()
     // remove empty newlines
@@ -155,7 +139,10 @@ for (let cb of codeBlocks) {
                 htmlCode.innerHTML = code
                 make_button(htmlCode, codeText)
             })
-            .catch(err => htmlCode.innerHTML = "Error loading code block...")
+				.catch(err => {
+					console.log(err)
+					htmlCode.innerHTML = "Error loading code block..."
+				})
         }
     } catch (error) {
         console.error(error);

gh_pages/js/sandbox.js

@@ -1,3 +1,5 @@
+import { idents, types, prims, operators, keywords, whitespaces, comments, libs } from './codeKeywords.js'
+
 const isMobile = window.innerWidth < 990;
 
 let editor;
@@ -71,35 +73,18 @@ require(['vs/editor/editor.main'], function () {
         // Set defaultToken to invalid to see what you do not tokenize yet
         // defaultToken: 'invalid',
 
-        keywords: [
-            "define", "function", "fun", "switch", "case", "union", "if", "then", "else", "import",
-            "generic", "assert", "have", "transitive", "symmetric", "extensionality", "reflexive",
-            "injective", "sorry", "help", "conclude", "suffices", "enough", "by", "rewrite",
-            "conjunct", "induction", "where", "suppose", "with", "definition", "apply", "to", "cases",
-            "obtain", "stop", "equations", "of", "arbitrary", "choose", "term", "from",
-            "assume", "for", "recall", "in", "and", "or", "print", "not", "some", "all", "theorem",
-            "lemma", "proof", "end"
-        ],
+        keywords: keywords,
 
-        typeKeywords: [
-            "MultiSet", "Option", "Pair", "Set", "List", "Int", "Nat", "int", "bool", "fn", "type"
-        ],
+        typeKeywords: types.concat(libs),
 
-        operators: [
-            "->", "++", "/", "|", "&", "[+]", "[o]", "(=",
-            "<=", ">=", "/=", "≠", "⊆", "≤", "≥", "∈", "∪", "+", "%", "(?<!/)*(?!/)", "⨄",
-            "-", "∩", "∘", "λ", "@", ":", "<", ">", ",", "=", ".", ";", "#"
-        ],
+        operators: operators,
 
         defines: [
             "node", "suc", "take", "set_of", "empty_no_members",
             "single", "member_union", "single_equal", "length"
         ],
 
-        prims: ["true", "false", "empty"],
-
-        primSymbols: ["∅", "[0]", "?"],
-
+        prims: prims,
 
         // we include these common regular expressions
         symbols: /(=|>|<|!|~|\?|:|&|\||\+|-|\^|%|\)|\(|\]|\[|o|0|≠|⊆|≤|≥|∈|∪|∅|\.)/,
@@ -125,7 +110,6 @@ require(['vs/editor/editor.main'], function () {
                 // [/[<>](?!@symbols)/, '@brackets'],
                 [/[.@*=><!~?:&|+^%≤≥⇔∘∪∩⊆∈⨄∅-]+/, {
                     cases: {
-                        '@primSymbols': 'primitive',
                         '@operators': 'operator',
                         '@default': 'operator'
                     }
@@ -345,4 +329,4 @@ function download(filename, text) {
 
 // Not really necessary but hey
 themeUpdate(false)
-sizeUpdate(false)
+sizeUpdate(false)

gh_pages/sandbox.html

@@ -89,7 +89,8 @@
     </div>
 
 	<script src="https://cdnjs.cloudflare.com/ajax/libs/monaco-editor/0.29.1/min/vs/loader.js"></script>
-	<script src="./js/sandbox.js"></script>
+	<script src="./js/codeKeywords.js" type="module"></script>
+	<script src="./js/sandbox.js" type="module"></script>
     <script src="./js/cache.js"></script>
     <script src="./js/script.js"></script>
     <script src="./js/code.js"></script>

gh_pages/scripts/code_block_syntax_generator.py

@@ -0,0 +1,25 @@
+import os
+
+from keywords import get_known_tokens, get_pattern_types
+
+if __name__ == '__main__':
+    pattern_types = get_pattern_types()
+
+    with open('./gh_pages/js/codeKeywords.js', 'w') as f:
+
+        for pt, ps in pattern_types.items():
+            patterns = str(ps).replace(';', '(TEMPORARY_AMP)semi;')\
+                       .replace('&', '&')\
+                       .replace('=', '=')\
+                       .replace('/', '/')\
+                       .replace('<', '&lt;')\
+                       .replace('>', '&gt;')\
+                       .replace('(TEMPORARY_AMP)', '&')
+            f.write(f'const {pt}s = {patterns}\n\n')
+
+        libs = [lib.split('.pf')[0] for lib in os.listdir('./lib') if lib.endswith('.pf')]
+        f.write(f'const libs = {libs}\n\n')
+
+        exports = ', '.join(map(lambda k: k + 's', pattern_types.keys()))
+        f.write(f'export {{ {exports}, libs }}')
+

gh_pages/doc/convert.py → gh_pages/scripts/convert.py

@@ -149,7 +149,7 @@ def run(self, lines):
                     j += 1
 
         with open(f'./test/should-validate/doc_{mdToDeduceCode[self.fname]}.pf', 'w') as f:
-            f.write('// Generated by ./gh_pages/doc/convert.py\n\n')
+            f.write('// Generated by ./gh_pages/scripts/convert.py\n\n')
             for line in entangled_code:
                 line = line.replace(" ", "")
                 f.write(line)
@@ -356,7 +356,8 @@ def conclusion(md=True):
     <script src="{relative_path}/js/cache.js"></script>
     <script src="{relative_path}/js/script.js"></script>
     <script src="{relative_path}/js/code.js"></script>
-    <script src="{relative_path}/js/codeUtils.js"></script>
+    <script src="{relative_path}/js/codeKeywords.js" type="module"></script>
+    <script src="{relative_path}/js/codeUtils.js" type="module"></script>
 </body>
 
 </html>