Merge pull request #200 from imitator-model-checker/feature/menhir

Use menhir instead of ocamlyacc for parsing
imitator-model-checker · Nov 8, 2024 · 4b25e6e · 4b25e6e
2 parents 3a89763 + 029dc24
commit 4b25e6e
Show file tree

Hide file tree

Showing 5 changed files with 50 additions and 40 deletions.
diff --git a/.github/scripts/build.sh b/.github/scripts/build.sh
@@ -5,43 +5,43 @@ set -a
 # check OS
 case $(uname) in
 'Linux')
-    RUNNER_OS='Linux'
-    ;;
+  RUNNER_OS='Linux'
+  ;;
 'Darwin')
-    RUNNER_OS='macOS'
-    ;;
+  RUNNER_OS='macOS'
+  ;;
 *)
-    echo "This script only supports Linux or OSX"
-    exit 1
-    ;;
+  echo "This script only supports Linux or OSX"
+  exit 1
+  ;;
 esac
 
 # ignore sudo commands when the user is root
 sudo() {
-    [[ $EUID = 0 ]] || set -- command sudo "$@"
-    "$@"
+  [[ $EUID = 0 ]] || set -- command sudo "$@"
+  "$@"
 }
 
 # script folder
 if [ -z "${GITHUB_WORKSPACE}" ]; then
-    SCRIPT_FOLDER=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &>/dev/null && pwd)
-    PATCH_FOLDER="$(dirname $SCRIPT_FOLDER)/patches"
-    ROOT_FOLDER="$(dirname $(dirname $SCRIPT_FOLDER))"
-    cd "$ROOT_FOLDER"
+  SCRIPT_FOLDER=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &>/dev/null && pwd)
+  PATCH_FOLDER="$(dirname $SCRIPT_FOLDER)/patches"
+  ROOT_FOLDER="$(dirname $(dirname $SCRIPT_FOLDER))"
+  cd "$ROOT_FOLDER"
 else
-    SCRIPT_FOLDER="${GITHUB_WORKSPACE}/.github/scripts"
-    PATCH_FOLDER="${GITHUB_WORKSPACE}/.github/patches"
+  SCRIPT_FOLDER="${GITHUB_WORKSPACE}/.github/scripts"
+  PATCH_FOLDER="${GITHUB_WORKSPACE}/.github/patches"
 fi
 
 # install dependencies
 if [[ "$RUNNER_OS" = "Linux" ]]; then
-    DEBIAN_FRONTEND=noninteractive
-    sudo apt-get update -qq
-    sudo apt-get install -qq wget unzip curl build-essential libtinfo-dev g++ m4 opam python3 \
-        libgmp-dev libmpfr-dev libppl-dev \
-        graphviz plotutils
+  DEBIAN_FRONTEND=noninteractive
+  sudo apt-get update -qq
+  sudo apt-get install -qq wget unzip curl build-essential libtinfo-dev g++ m4 opam python3 \
+    libgmp-dev libmpfr-dev libppl-dev \
+    graphviz plotutils
 elif [[ "$RUNNER_OS" = "macOS" ]]; then
-    brew install opam gmp ppl graphviz plotutils
+  brew install opam gmp ppl graphviz plotutils
 fi
 
 # python fix
@@ -50,7 +50,7 @@ fi
 # install opam and ocaml libraries
 [[ ${DOCKER_RUNNING} ]] && opam init -a --disable-sandboxing || opam init -a
 
-opam install -y extlib fileutils oasis alcotest
+opam install -y extlib fileutils oasis alcotest menhir
 eval $(opam env)
 
 # install mlgmp
@@ -61,16 +61,16 @@ eval $(opam env)
 
 # patch oasis for OSX
 if [[ "$RUNNER_OS" = "macOS" ]]; then
-    patch -p0 <"${PATCH_FOLDER}/oasis-config.patch"
+  patch -p0 <"${PATCH_FOLDER}/oasis-config.patch"
 fi
 
 # Build IMITATOR
 dune build
 
 # rename artefact
 if [ ! -z "${GITHUB_WORKSPACE}" ]; then
-    cd bin
-    platform=$(echo "${RUNNER_OS}" | awk '{print tolower($1)}')
-    tag="${GITHUB_REF_NAME##*/}"
-    mv "imitator" "imitator-${tag}-${platform}-amd64"
+  cd bin
+  platform=$(echo "${RUNNER_OS}" | awk '{print tolower($1)}')
+  tag="${GITHUB_REF_NAME##*/}"
+  mv "imitator" "imitator-${tag}-${platform}-amd64"
 fi
diff --git a/dune-project b/dune-project
@@ -1,4 +1,5 @@
 (lang dune 3.6)
+(using menhir 2.1)
 
 (name IMITATOR)
 
@@ -25,9 +26,13 @@
    (>= 4.08))
   dune
   oasis
+  menhir
   mlgmp
   ppl
   extlib
   fileutils)
+
  (tags
   ("model-checking" "parametric timed automata")))
+
+
diff --git a/src/lib/ModelParser.mly b/src/lib/ModelParser.mly
@@ -22,11 +22,12 @@ open ImitatorUtilities;;
 open DiscreteType;;
 
 
-let parse_error _ =
-	let symbol_start = symbol_start () in
-	let symbol_end = symbol_end () in
-	raise (ParsingError (symbol_start, symbol_end))
-;;
+(*** TODO (Jaime): What is symbol_start ? ***)
+(* let parse_error _ = *)
+(* 	let symbol_start = symbol_start () in *)
+(* 	let symbol_end = symbol_end () in *)
+(* 	raise (ParsingError (symbol_start, symbol_end)) *)
+(* ;; *)
 
 (*** TODO (Jaime): is it included twice ? ***)
 let include_list = ref [];;

diff --git a/src/lib/PropertyParser.mly b/src/lib/PropertyParser.mly
@@ -20,11 +20,12 @@ open ImitatorUtilities
 open ParsingStructure
 
 
-let parse_error _ =
-	let symbol_start = symbol_start () in
-	let symbol_end = symbol_end () in
-	raise (ParsingError (symbol_start, symbol_end))
-;;
+(*** TODO (Jaime): What is symbol_start ? ***)
+(* let parse_error _ = *)
+(* 	let symbol_start = symbol_start () in *)
+(* 	let symbol_end = symbol_end () in *)
+(* 	raise (ParsingError (symbol_start, symbol_end)) *)
+(* ;; *)
 
 
 

diff --git a/src/lib/dune b/src/lib/dune
@@ -10,11 +10,14 @@
 
   )
 
+(menhir
+  (modules ModelParser PropertyParser))
+
  (ocamllex
  (modules ModelLexer PropertyLexer))
 
-(ocamlyacc
- (modules ModelParser PropertyParser))
+; (ocamlyacc
+;  (modules ModelParser PropertyParser))
 
 (env
  (dev
@@ -26,4 +29,4 @@
  (deps
   (:gen ../../gen_build_info.py))
  (action
-  (run python %{gen})))
+  (run python %{gen})))