merge testnet3

.github/workflows/acl2.yml

@@ -21,7 +21,18 @@ jobs:
 
       - name: Generate asts
         run: |
-          cargo -q run -p leo-test-framework --bin tgc
+          # This currently has to be on testnet3 to work:
+          cd compiler/parser
+          cargo -q install --path . --example parser
+          # To ensure full file tests,
+          # just do compiler tests and remove expectation: Fail tests
+          cd ../../tests/compiler
+          find . -type f -exec grep -q 'expectation *: *Fail' {} \; -delete
+          find . -name '*.leo' -execdir parser {} \; > /dev/null
+          # Show how many there are:
+          echo "Counts (.leo / .json):"
+          find . -name '*.leo' -print | wc -l
+          find . -name '*.json' -print | wc -l
 
       # Pull the latest release from the leo-acl2-bin repo, and put it into the
       # repo/acl2 directory. After it's done, unpack the tgz file locally.
@@ -29,7 +40,7 @@ jobs:
         run: |
           mkdir acl2 && cd acl2;
           wget $( curl -s https://api.github.com/repos/AleoHQ/leo-acl2-bin/releases/latest \
-                  | jq -r '.assets[0].browser_download_url' )
+                  | jq -r '.assets[].browser_download_url|scan("^.*leo-acl2--v.*\\.tgz$")' )
 
           echo "Unpacking $(ls):"
           tar -xvzf $(ls)
@@ -37,28 +48,31 @@ jobs:
       # Run theorem generation and checking using the prepared ASTs and the pulled and unzipped leo-acl2 tarball.
       - name: Run tgc over ASTs
         run: |
-          canonicalization_errors=();
-          type_inference_errors=();
-          num_dirs=0;
-          for dir in `ls tmp/tgc`;
+          parsing_errors=();
+          num_cases=0;
+          # Note that PWD gets reset at the beginning of each the step
+          # to /home/runner/work/leo/leo
+          acl2dir="${PWD}"/acl2
+          cd tests/compiler;
+          for tc in `find ${PWD} -name '*.leo' -print`;
           do
-            cd tmp/tgc/$dir; # enter the directory
-            num_dirs=$((num_dirs + 1));
-            ./../../../acl2/tgc canonicalization initial_ast.json canonicalization_ast.json canonicalization-theorem.lisp > canonicalization_result.out || canonicalization_errors+=("$dir");
-            ./../../../acl2/tgc type-inference canonicalization_ast.json type_inferenced_ast.json type-inference-theorem.lisp > type_inference_result.out || type_inference_errors+=("$dir");
-            cd ../../..
+            cd "${tc%/*}";  # enter the directory
+            leofile="${tc##*/}";
+            jsonfile="${leofile%.leo}.json";
+            num_cases=$((num_cases + 1));
+            "$acl2dir"/tgc parsing "$leofile" "$jsonfile" parsing-theorem.lisp > parsing_result.out || parsing_errors+=("$tc");
           done;
 
           echo "----------------"
-          echo "Ran tgc in ${num_dirs} directories."
+          echo "Ran tgc on ${num_cases} programs."
           echo "----------------"
-          if [ ${#canonicalization_errors[@]} -eq 0 ]; then
-            echo "Canonicalization - Success!"
+          if [ ${#parsing_errors[@]} -eq 0 ]; then
+            echo "Parsing - Total Success!"
           else
-            echo "Canonicalization Failures (total: ${#canonicalization_errors[@]}):"
-            for dir in ${canonicalization_errors[@]};
+            echo "Parsing Failures (total: ${#parsing_errors[@]}):"
+            for tc in ${parsing_errors[@]};
             do
-              echo $dir
+              echo $tc
             done;
 
             #echo "Attaching logs:"
@@ -69,24 +83,7 @@ jobs:
             #done;
           fi
 
-          echo "----------------"
-          if [ ${#type_inference_errors[@]} -eq 0 ]; then
-            echo "Type Inference - Success!"
-          else
-            echo "Type Inference Failures (total: ${#type_inference_errors[@]}):"
-            for dir in ${type_inference_errors[@]};
-            do
-              echo $dir
-            done;
-
-            #echo "Attaching logs:"
-            #for dir in ${type_inference_errors[@]};
-            #do
-            # cat tmp/tgc/$dir/type_inference_result.out
-            #done;
-          fi
-
-          if [[ ${#canonicalization_errors[@]} -ne 0 || ${#type_inference_errors[@]} -ne 0 ]]; then
+          if [[ ${#parsing_errors[@]} -ne 0 ]]; then
             echo "----------------"
             echo "Exiting with status 1 due to at least one tgc error."
             exit 1

Cargo.lock

@@ -2006,9 +2006,9 @@ dependencies = [
 
 [[package]]
 name = "regex"
-version = "1.5.5"
+version = "1.5.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1a11647b6b25ff05a515cb92c365cec08801e83423a235b51e231e1808747286"
+checksum = "d83f127d94bdbcda4c8cc2e50f6f84f4b611f69c902699ca385a39c3a75f9ff1"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -2023,9 +2023,9 @@ checksum = "6c230d73fb8d8c1b9c0b3135c5142a8acee3a0558fb8db5cf1cb65f8d7862132"
 
 [[package]]
 name = "regex-syntax"
-version = "0.6.25"
+version = "0.6.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f497285884f3fcff424ffc933e56d7cbca511def0c9831a7f9b5f6153e3cc89b"
+checksum = "49b3de9ec5dc0a3417da371aab17d729997c15010e7fd24ff707773a33bddb64"
 
 [[package]]
 name = "remove_dir_all"

docs/grammar/abnf-grammar.txt

@@ -375,7 +375,7 @@ input-expression = literal
 
 input-item = identifier ":" input-type "=" input-expression ";"
 
-input-title = "[" identifier "]"
+input-title = "[" ( %s"public" / %s"private" / %s"constant" / %s"const" ) "]"
 
 input-section = input-title *input-item