Parse 100% of .t files

Cargo.toml

@@ -12,10 +12,18 @@ path = "scripts/format.rs"
 [dependencies]
 walkdir = "2.5.0"
 jwalk = "0.5"
+tree-sitter-raven = { path = "./tools/tree-sitter-raven/" }
+tree-sitter = { git = "https://github.com/tree-sitter/tree-sitter.git", tag = "v0.22.6" }
 
 [dev-dependencies]
 ravenfmt = { path = "./tools/ravenfmt/" }
 
+[[bin]]
+name = "tscheck"
+test = false
+bench = false
+path = "scripts/tscheck.rs"
+
 [workspace]
 members = [
   "tools/tree-sitter-raven",

build.rs

@@ -0,0 +1,6 @@
+use std::process::{Command, exit};
+
+fn main() -> std::io::Result<()> {
+    println!("cargo::rerun-if-changed=tools/tree-sitter-raven/grammar.js");
+    exit(Command::new("make").arg("-C").arg("tools/tree-sitter-raven/").spawn().expect("Failed to run ravenfmt").wait()?.code().unwrap());
+}

scripts/format.rs

@@ -1,35 +1,8 @@
-use std::io::{Error, ErrorKind};
-use std::path::{Path, PathBuf};
-use std::collections::VecDeque;
-use std::collections::HashSet;
+#![allow(unused)]
+mod system;
+use system::all_test_files;
 use std::process::Command;
-
-fn all_test_files() -> std::io::Result<Vec<PathBuf>> {
-    let mut out = Vec::new();
-    let cwd = std::env::current_dir()?;
-    let mut map = HashSet::from([cwd.clone()]);
-    let mut queue = VecDeque::from([cwd]);
-    while let Some(dir) = queue.pop_back() {
-        for entry in walkdir::WalkDir::new(&dir).into_iter().filter_map(|e| e.ok()) {
-            if entry.path().is_dir() && !map.contains(entry.path()) {
-                map.insert(entry.path().to_owned());
-                queue.push_back(entry.path().to_owned());
-            } else if let Some(filename) = entry.file_name().to_str() {
-                if filename.ends_with(".t") {
-                    let without_extension = &filename[0..filename.len() - 2];
-                    let raven_file = format!("{}.rav", without_extension);
-                    let raven_path = entry.path().parent()
-                        .ok_or(Error::new(ErrorKind::NotFound, format!("parent directory of file {} not found", entry.path().to_str().unwrap_or("UNFORMATTABLE"))))?
-                        .join(raven_file);
-                    if Path::is_file(&raven_path) {
-                        out.push(raven_path)
-                    }
-                }
-            }
-        }
-    }
-    Ok(out)
-}
+use std::io::{Error, ErrorKind};
 
 /// Find all .rav files, and run "rustfmt" on them.
 fn main() -> std::io::Result<()> {

scripts/system.rs

@@ -0,0 +1,39 @@
+use std::fs::File;
+use std::io::{Error, ErrorKind, Read};
+use std::path::{Path, PathBuf};
+use std::collections::VecDeque;
+use std::collections::HashSet;
+
+pub fn all_test_files() -> std::io::Result<Vec<PathBuf>> {
+    let mut out = Vec::new();
+    let cwd = std::env::current_dir()?;
+    let mut map = HashSet::from([cwd.clone()]);
+    let mut queue = VecDeque::from([cwd]);
+    while let Some(dir) = queue.pop_back() {
+        for entry in walkdir::WalkDir::new(&dir).into_iter().filter_map(|e| e.ok()) {
+            if entry.path().is_dir() && !map.contains(entry.path()) {
+                map.insert(entry.path().to_owned());
+                queue.push_back(entry.path().to_owned());
+            } else if let Some(filename) = entry.file_name().to_str() {
+                if filename.ends_with(".t") {
+                    let without_extension = &filename[0..filename.len() - 2];
+                    let raven_file = format!("{}.rav", without_extension);
+                    let raven_path = entry.path().parent()
+                        .ok_or(Error::new(ErrorKind::NotFound, format!("parent directory of file {} not found", entry.path().to_str().unwrap_or("UNFORMATTABLE"))))?
+                        .join(raven_file);
+                    if Path::is_file(&raven_path) {
+                        out.push(raven_path)
+                    }
+                }
+            }
+        }
+    }
+    Ok(out)
+}
+
+pub fn read_file<P: AsRef<Path>>(path: P, s: &mut String) -> std::io::Result<()> {
+    let mut file = File::open(path)?;
+    s.clear();
+    file.read_to_string(s)?;
+    Ok(())
+}

scripts/tscheck.rs

@@ -0,0 +1,40 @@
+mod system;
+use system::{all_test_files, read_file};
+use std::io::{Error, ErrorKind};
+use tree_sitter_raven::language;
+use std::collections::VecDeque;
+
+fn parse_status<S: AsRef<[u8]>>(parser: &mut tree_sitter::Parser, buf: S) -> std::io::Result<String> {
+    match parser.parse(buf, None) {
+        None => Err(Error::new(ErrorKind::Other, "Parse error: no parse tree could be created")),
+        Some(tree) => {
+            let mut queue = VecDeque::from([tree.root_node()]);
+            while let Some(node) = queue.pop_back() {
+                if node.is_error() {
+                    let msg = format!("Error at {}-{}", node.start_position(), node.end_position());
+                    return Err(Error::new(ErrorKind::Other, msg));
+                }
+                let mut cursor = node.walk();
+                for child in node.children(&mut cursor) {
+                    queue.push_front(child);
+                }
+            }
+            Ok("success".to_string())
+        }
+    }
+}
+
+/// Find all .rav files, and run "rustfmt" on them.
+fn main() -> std::io::Result<()> {
+    let mut buf = String::new();
+    for file in all_test_files()? {
+        let file_name = file.clone().into_os_string().into_string().map_err(|e| Error::new(ErrorKind::Other, format!("could not format {:?} as string", e)))?;
+        println!("checking {}", file_name);
+        read_file(&file, &mut buf)?;
+        let mut parser = tree_sitter::Parser::new();
+        parser.set_language(&language()).map_err(|e| Error::new(ErrorKind::Other, format!("{:?}", e)))?;
+        let parse_status = parse_status(&mut parser, &buf.as_bytes())?;
+        println!("parse status: {}", parse_status);
+    }
+    Ok(())
+}

test/list_predicates.rav

@@ -1,3 +1,138 @@
+// No null values
+// No support for implications outside of iterated star
+// Evaluate the new command
+
+field key: Int
+field next: Ref
+
+// try insertion with this
 pred list(start: Ref, end: Ref, nmap: Map[Ref, Ref]) {
-  1 + 2
+  (start == end) ? true : 
+    (own(start, next, nmap[start], 1.0) && list(nmap[start], end, nmap))
 } 
+
+proc append(x: Ref, y: Ref, z: Ref, nmap: Map[Ref, Ref]) 
+  requires list(x, y, nmap)
+  requires list(y, z, nmap)
+  ensures list(x, z, nmap)
+{
+  if (x != y) {
+    unfold list(x,y, nmap);
+    var x_next: Ref = x.next;
+    append(x_next, y, z, nmap);
+    assert list(x_next, z, nmap);
+    fold list(x, z, nmap);
+    // assert false;
+  }
+  // assert false;
+}
+
+proc deque(x: Ref, y: Ref, nmap: Map[Ref, Ref]) 
+  returns (xn: Ref)
+  requires list(x, y, nmap)
+  requires x != y
+  ensures list(xn, y, nmap)
+{
+  unfold list(x, y, nmap);
+  xn := x.next;
+}
+
+proc insert(x: Ref, y: Ref, z: Ref, n: Ref, nmap: Map[Ref, Ref])
+  returns (nmap1: Map[Ref, Ref])
+  requires list(x, y, nmap)
+  requires own(n, next, nmap[n], 1.0)
+  requires n != y
+  ensures list(n, y, nmap1)
+  ensures nmap1[n] == x
+  ensures forall a: Ref :: a != n ==> nmap1[a] == nmap[a]  
+{
+  n.next := x;
+  nmap1 := nmap[n := x];
+  // nmap1[n] := x;
+
+  assert 
+    (n == y) ? true : 
+    (own(n, next, nmap1[n], 1.0) && list(nmap1[n], y, nmap1));
+  fold list(n, y, nmap1);
+}
+
+// pred list_seg(start: Ref, end: Ref, i: Int, j: Int, l: Map[Int, Int], nmap: Map[Ref, Ref], kmap: Map[Ref, Int]) {
+//   ((start == end) ? true :
+//     (own(start, next, nmap[start], 1.0) && own(start, key, kmap[start], 1.0) 
+//       && l[i] == kmap[start] && list_seg(nmap[start], end, i+1, j, l, nmap, kmap)))
+// }
+
+// proc append2(x: Ref, y: Ref, z: Ref, l1: Int, l2: Int, l3: Int, ls: Map[Int, Int], nmap: Map[Ref, Ref], kmap: Map[Ref, Int])
+//   requires list_seg(x, y, l1, l2, ls, nmap, kmap)
+//   requires list_seg(y, z, l2, l3, ls, nmap, kmap)
+//   ensures list_seg(x, z, l1, l3, ls, nmap, kmap)
+// {
+//   if (x != y) {
+//     unfold list_seg(x, y, l1, l2, ls, nmap, kmap);
+//     append2(x.next, y, z, l1+1, l2, l3, ls, nmap, kmap);
+
+//     assert list_seg(x.next, z, l1+1, l3, ls, nmap, kmap);
+//     fold list_seg(x, z, l1, l3, ls, nmap, kmap);
+//     // assert false;
+//   }
+
+//   // assert false;
+
+// }
+
+// proc deque(x: Ref, y: Ref, i: Int, j: Int, l: Map[Int, Int], nmap: Map[Ref, Ref], kmap: Map[Ref, Int])
+//   returns (xn: Ref)
+//   requires (x != y)
+//   requires list_seg(x, y, i, j, l, nmap, kmap)
+//   ensures list_seg(xn, y, i+1, j, l, nmap, kmap)
+// {
+//   unfold list_seg(x, y, i, j, l, nmap, kmap);
+//   xn := x.next;
+//   // assert false;
+// }
+
+// proc insert(x: Ref, y: Ref, i: Int, j: Int, l: Map[Int, Int], nmap: Map[Ref, Ref], kmap: Map[Ref, Int], k : Int)
+//   returns (l1: Map[Int, Int], idx: Int, nmap1: Map[Ref, Ref], kmap1: Map[Ref, Int])
+//   requires (x != y)
+//   requires list_seg(x, y, i, j, l, nmap, kmap)
+//   requires forall i1 : Int :: i <= i1 < j ==> l[i1] <= l[i1+1]
+//   requires kmap[x] < k <= kmap[y]
+//   ensures i < idx <= j
+//   ensures list_seg(x, y, i, j+1, l1, nmap1, kmap1)
+//   ensures l1[idx] == k
+//   ensures forall i1 : Int :: i <= i1 < idx ==> l1[i1] == l[i]
+//   ensures forall i1 : Int :: idx < i1 <= j+1 ==> l1[i1] == l[i-1]
+// {
+//   var prev : Ref;
+//   var curr : Ref;
+//   var currkey : Int;
+
+//   prev := x;
+//   curr := x;
+//   unfold list_seg(x, y, i, j, l, nmap, kmap);
+//   currkey := curr.key;
+//   idx := i;
+
+//   fold list_seg(x, prev, i, idx, l, nmap, kmap);
+//   fold list_seg(curr, y, idx, j, l, nmap, kmap);
+
+//   while (currkey < k)
+//     invariant list_seg(x, prev, i, idx, l, nmap, kmap)
+//     invariant list_seg(curr, y, idx, j, l, nmap, kmap)
+//     invariant curr != y
+//   {
+//     prev := curr;
+
+//     unfold list_seg(curr, y, idx, j, l, nmap, kmap);
+
+//     curr := curr.next;
+//     currkey := curr.key;
+
+//     idx := idx + 1;
+//   }
+
+//   var n: Ref;
+//   n := new(key: k, next: curr);
+//   prev.next := n;
+
+// }

test/rustbelt/lifetimes.rav

@@ -0,0 +1,6 @@
+interface Lifetime {
+  rep type T1
+  rep type T2
+
+  func hello(a: T1) returns (b: T2)
+}