stuff

Author: VictorTaelin

KIND2_GUIDE_AI.md

@@ -39,7 +39,7 @@ Since Kind2's core is so simple, it comes with many syntax sugars.
 Every .kind2 file must define ONE top-level function:
 
 ```
-name <p0: P0> <p1: P1> ...
+func <p0: P0> <p1: P1> ...
 - arg0: typ0
 - arg1: typ1
 - ...
@@ -74,7 +74,7 @@ Where:
 Top-Level datatypes desugar to λ-encodings. The λ-encoded constructors must be
 created manually, in separate files. See examples below.
 
-## Names, Paths and Use Aliases
+### Names, Paths and Use Aliases
 
 Kind2 doesn't need imports. Every file defines a single top-level definition,
 which can be addressed from any other file via its full path. Example:
@@ -145,13 +145,40 @@ switch x = expr {
 }: motive
 ```
 
+### Note on Parameters and Metavars 
+
+Top-level definitions can have N parameters, or erased arguments. Example:
+
+```
+// Pair/swap.kind2
+swap <A> <B>
+- pair: (Pair A B)
+...
+```
+
+There are two ways to call these functions.
+
+1. Filling the parameters explicitly:
+
+```
+(swap Nat (List Nat) (Pair/new Nat (List Nat) Nat/zero (List/nil Nat)))
+```
+
+2. Using metavars (`_`) to fill the parameters:
+
+```
+(swap _ _ (Pair/new _ _ Nat/zero (List/nil _)))
+
+As you can see, using metavars is much more concise. As a rule of thumb, always
+use metavars on the function body, but write it fully on its arglist. Remember
+to always count the arguments: you need one metavar (`_`) per parameter (`<>`).
+
 ### Other Sugars
 
 - Lists: `[a, b, c]` (desugars to cons/nil)
 - Strings: `"foo"` (desugars to lists of u48 codepoints)
 - Equality: `{a = b}` (desugars to `(Equal _ a b)`)
 - Function: `A -> B` (desugars to `∀(x_: A) B`)
-- Implicit: `(foo/ x y)` (desugars to `(foo _ _ ... x y)`, auto-filling erased args)
 - Comments: `// comment here`
 
 ## Kind2 Examples
@@ -416,7 +443,7 @@ List/fold <A> (P: *)
 : P
 
 match xs {
-  cons: (c xs.head (List/fold/ P c n xs.tail))
+  cons: (c xs.head (List/fold _ P c n xs.tail))
   nil: n
 }
 ```
@@ -500,6 +527,10 @@ Take a moment to notice how EVERY constructor and function application in Kind2
 requires a parenthesis, just like Lisp. Trying to write `(foo x y)` without the
 surrounding parenthesis is a syntax error. Confirm this is true and move on.
 
+Also, note that ERASED arguments can usually be inferred, so, a metavar ('_')
+can be used. Example: '(func _ _ ... arg0 arg1 ...)' can be writen instead of
+'(func A B ... arg0 arg1 ...)'. Prefer metavars on the body of the function.
+
 ### Sigma/_.kind2
 
 ```

kindcoder.mjs

@@ -167,13 +167,15 @@ Optionally, you can also include a SHORT, 1-paragraph <JUSTIFICATION/>.
   - map
   - fold
   - filter
+  - equal
   - zip
   - length
 - Nat/
   - match
   - fold
   - succ
   - zero
+  - compare
   - add
   - sub
   - mul
@@ -200,7 +202,8 @@ Optionally, you can also include a SHORT, 1-paragraph <JUSTIFICATION/>.
 Nat/equal is likely to be a pairwise comparison between Nats. As such, it must
 include Nat (obviously), as well as its constructor and match. It returns a
 Bool, so, it must also include its constructors and match. For completion, I've
-also added boolean AND and OR, since these are commonly used in comparison.
+also added bool AND and OR, since these are often used in comparison. Finally,
+Nat/compare and List/equal might be similar algorithms, so, I included them.
 </JUSTIFICATION>
 <DEPENDENCIES>
 Nat
@@ -213,18 +216,23 @@ Bool/false
 Bool/match
 Bool/and
 Bool/or
+Nat/compare
+List/equal
 </DEPENDENCIES>
 
 # HINTS
 
 - Attempt to include ALL files that might be relevant, directly or not.
 
+- Always include files that might be similar algorithms to the current one.
+  Example: 'Map/set' MUST include 'Mat/get'
+
 - If the file is the constructor of an ADT, then, INCLUDE its type.
   Example: 'List/cons' MUST include 'List'
 
 - When in doubt, prefer to include MORE, rather than LESS, potencial dependencies.
 
-- Try to include AT LEAST 8 dependencies, and AT MOST 32.
+- Try to include AT LEAST 4 dependencies, and AT MOST (only if needed) 16.
 
 - Sometimes the user will give hints in the file. Follow them.
 `.trim();
@@ -244,7 +252,7 @@ async function predictDependencies(name, fileContent) {
       }
       return null;
     }));
-    return files.filter(file => file !== null);
+    return files.filter(file => file !== null).map(file => ({...file, name: file.name.replace(/\/_$/, '')}));
   }
 
   // Function to build a tree structure from files
@@ -261,7 +269,7 @@ async function predictDependencies(name, fileContent) {
     return result;
   }
 
-  const allFiles = await getAllKind2Files(path.join(path.dirname(name), '..', '..', 'book'));
+  const allFiles = await getAllKind2Files("./");
   const defsTree = buildTree(allFiles);
 
   const aiInput = [
@@ -274,7 +282,7 @@ async function predictDependencies(name, fileContent) {
     '</DEFINITIONS>'
   ].join('\n').trim();
 
-  const aiOutput = await chat("h")(aiInput, { system: system_DepsPredictor, model: "h" });
+  const aiOutput = await chat("s")(aiInput, { system: system_DepsPredictor, model: "s" });
   console.log("");
 
   const dependenciesMatch = aiOutput.match(/<DEPENDENCIES>([\s\S]*)<\/DEPENDENCIES>/);
@@ -302,7 +310,7 @@ async function typeCheck(file) {
 async function main() {
   // Check for correct usage and parse command-line arguments
   if (process.argv.length < 3) {
-    console.log("Usage: kind-refactor <file> <request> [<model>]");
+    console.log("Usage: kindcoder <file> <request> [<model>]");
     process.exit(1);
   }
 
@@ -315,7 +323,12 @@ async function main() {
 
   // Get directory and file information
   let dir = path.dirname(file);
-  let fileContent = await fs.readFile(file, 'utf-8');
+  let fileContent;
+  try {
+    fileContent = await fs.readFile(file, 'utf-8');
+  } catch (e) {
+    fileContent = "";
+  }
   let dirContent = await fs.readdir(dir);
 
   // If the request is empty, replace it by a default request.