Merge branch 'language-improvements'

wies · Feb 8, 2019 · 3924bf0 · 3924bf0
2 parents 5876a74 + 4de1357
commit 3924bf0
Show file tree

Hide file tree

Showing 66 changed files with 4,155 additions and 1,843 deletions.
diff --git a/LICENSE b/LICENSE
@@ -1,6 +1,6 @@
-Copyright (c) 2013-2018
+Copyright (c) 2013-2019
   Thomas Wies ([email protected])
-  Damien Zufferey (zufferey@csail.mit.edu)
+  Damien Zufferey (zufferey@mpi-sws.org)
   Siddharth Krishna ([email protected])
   Ari Holtzman ([email protected])
 All rights reserved.
@@ -141,3 +141,37 @@ ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * The views and conclusions contained in the software and documentation are those of the
 authors and should not be interpreted as representing official policies, either expressed
 or implied, of Andrea Leofreddi.
+
+----
+
+GRASShopper's Emacs major mode integrates a modified version of the
+line indentation function from the Dafny major mode provided by
+boogie-friends. See file emacs-mode/spl-mode.el.
+
+Its copyright:
+
+Copyright (C) 2015 Cl�ment Pit--Claudel
+Author: Cl�ment Pit--Claudel <[email protected]>
+URL: https://github.com/boogie-org/boogie-friends/
+
+Keywords: convenience, languages
+
+This file is not part of GNU Emacs.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/README.md b/README.md
@@ -2,7 +2,7 @@
 
 GRASShopper
 =======
-![Version 0.4](https://img.shields.io/badge/version-0.4-green.svg)
+![Version 0.5](https://img.shields.io/badge/version-0.5-green.svg)
 [![BSD licensed](https://img.shields.io/badge/license-BSD-blue.svg)](https://raw.githubusercontent.com/wies/grasshopper/master/LICENSE)
 [![Build Status](https://travis-ci.org/wies/grasshopper.svg?branch=master)](https://travis-ci.org/wies/grasshopper)
 
@@ -68,26 +68,19 @@ To see the available command line options, run
 ./grasshopper.native -help
 ```
 
-Emacs Modes
+Emacs Major Mode
 -------------------------
-GRASShopper provides two emacs modes for GRASShopper programs:
 
-- SPL mode: this mode provides syntax highlighting and automatic
-  indentation for the GRASShopper input programs (see tests/spl for
-  examples).
+GRASShopper provides an Emacs major mode for GRASShopper programs.
+The mode provides syntax highlighting and automatic indentation for
+the GRASShopper input programs (see tests/spl for examples).
 
-- GHP mode: this mode provides syntax highlighting for the intermediate 
-  representation of programs inside GRASShopper. Such programs can be
-  generated by running GRASShopper with the option `-dumpghp n`.
-  Here, n=0,1,2,3 refers to the n-th simplification stage of
-  verification condition generation.
-
-To use the emacs modes, copy the files in the directory emacs-mode to
-your site-lisp directory and add the following lines to your `.emacs` file:
+To use the Emacs mode, copy the files in the directory emacs-mode to
+your site-lisp directory and add the following line to your `.emacs`
+file:
 
 ```elisp
-(load "spl-mode")   
-(load "ghp-mode")
+(load "spl-mode")
 ```
 
 Optional: Flycheck minor mode

diff --git a/bin/regression-tests b/bin/regression-tests
@@ -2,7 +2,7 @@
 
 source bin/osx_gnu.sh
 
-# Format: <test name> <spl file> <options> <expected result>
+# Format: <test name> <spl file> <procedure> <expected result>
 TESTS="
 soudness0               tests/spl/soundness/soundness0.spl              ''      fail
 soudness1               tests/spl/soundness/soundness1.spl              ''      fail
@@ -48,16 +48,16 @@ sls_merge_sort          tests/spl/sls/sls_merge_sort.spl                ''
 sls_quicksort           tests/spl/sls/sls_quicksort.spl                 ''      pass
 sls_strand_sort         tests/spl/sls/sls_strand_sort.spl               ''      pass
 union_find              tests/spl/sl/union_find.spl                     ''      pass
-list_set_contains       tests/spl/list_set/contains.spl                 '-stratify'      pass
-list_set_delete         tests/spl/list_set/delete.spl                   '-stratify'      pass
-list_set_difference     tests/spl/list_set/difference.spl               '-stratify'      pass
-list_set_insert         tests/spl/list_set/insert.spl                   '-stratify'      pass
-list_set_traverse       tests/spl/list_set/traverse.spl                 '-stratify'      pass
-list_set_union          tests/spl/list_set/union.spl                    '-stratify'      pass
-assoc_list_contains     tests/spl/assoc/contains.spl                    '-stratify'      pass
-assoc_list_insert       tests/spl/assoc/insert.spl                      '-stratify'      pass
-assoc_list_lookup       tests/spl/assoc/lookup.spl                      '-stratify'      pass
-assoc_list_remove       tests/spl/assoc/remove.spl                      '-stratify'      pass
+list_set_contains       tests/spl/list_set/contains.spl                 ''      pass
+list_set_delete         tests/spl/list_set/delete.spl                   ''      pass
+list_set_difference     tests/spl/list_set/difference.spl               ''      pass
+list_set_insert         tests/spl/list_set/insert.spl                   ''      pass
+list_set_traverse       tests/spl/list_set/traverse.spl                 ''      pass
+list_set_union          tests/spl/list_set/union.spl                    ''      pass
+assoc_list_contains     tests/spl/assoc/contains.spl                    ''      pass
+assoc_list_insert       tests/spl/assoc/insert.spl                      ''      pass
+assoc_list_lookup       tests/spl/assoc/lookup.spl                      ''      pass
+assoc_list_remove       tests/spl/assoc/remove.spl                      ''      pass
 array_bsearch           tests/spl/array/bsearch.spl                     ''      pass
 array_bubble            tests/spl/array/bubble.spl                      ''      pass
 array_checkSorted       tests/spl/array/checkSorted.spl                 ''      pass
@@ -71,7 +71,7 @@ array_reverse           tests/spl/array/reverse.spl                     ''
 array_selection_sort    tests/spl/array/selection_sort.spl              ''      pass
 array_test              tests/spl/array/test.spl                        ''      pass
 array_traverse_with_nodes tests/spl/array/traverse_with_nodes.spl       ''      pass
-recursive_def_lists     tests/spl/recursive_defs/list.spl               '-abspreds'      pass
+recursive_def_lists     tests/spl/recursive_defs/list.spl               ''      pass
 adt_lists               tests/spl/adt/lists.spl                         ''      pass
 "
 

diff --git a/bin/run-tests b/bin/run-tests
@@ -36,7 +36,12 @@ run_test()
 {
     echo -ne "Checking benchmark ${1}..."
     ulimit -St 600
-    ./grasshopper.native $2 ${3//\'/} $OPTIONS 2> /dev/null
+    if [ $3 == "''" ]; then
+        PROC=""
+    else
+        PROC="-procedure ${3//\'/}"
+    fi
+    ./grasshopper.native $2 $PROC $OPTIONS 2> /dev/null
     res=$?
     ulimit -St unlimited
     if [ $res -gt 128 ]; then

diff --git a/emacs-mode/ghp-mode.el b/emacs-mode/ghp-mode.el