Merge pull request #20 from h0nzZik/parsing-integration-1

Towards concrete syntax parser integration

.github/workflows/build-and-profile.yml

@@ -24,9 +24,11 @@ concurrency:
 jobs:
   build:
 
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
 
     steps:
+    - run: echo "APPIMAGE_EXTRACT_AND_RUN=1" >> $GITHUB_ENV
+
     - uses: actions/checkout@v3
 
     - name: Install Nix
@@ -43,6 +45,9 @@ jobs:
     - name: 'Run standalone examples'
       run: nix develop -L '.#examples-standalone' --command ./examples-standalone/test.sh
 
+    - name: 'Run hybrid examples'
+      run: nix develop -L '.#examples-hybrid' --command ./examples-hybrid/test.sh
+
     - name: 'Build Docker image'
       run: nix build -L '.#minuska-docker' --out-link ./result-minuska-docker
 

README.md

@@ -53,3 +53,22 @@ These include support for concrete syntax of programming languages, formalizatio
 See the [ideas document](./doc/ideas.md)
 
 
+
+# Troubleshooting
+
+## NixOS
+
+If you get
+```
+dlopen(): error loading libfuse.so.2
+
+(null)
+```
+when running a generated interpreter, it is probably because your NixOS system does not support `AppImage`s.
+In that case, see the [NixOS AppImage wiki](https://nixos.wiki/wiki/Appimage),
+and add
+```nix
+programs.appimage.enable = true;
+programs.appimage.binfmt = true;
+```
+into your system's `configuration.nix`.

examples-hybrid/coqfiles/imp.v

@@ -0,0 +1,71 @@
+
+Require Import Minuska.default_everything.
+Existing Instance default_everything.DSM.
+Definition myContext := (context-template (@t_term _ _ "c" [(HOLE); (t_over (notations.inject_variable "STATE"))]) with HOLE).
+Definition isValue (X : Expression2) := (e_binary b_or (e_unary b_isZ (X)) (e_binary b_or (e_unary b_isBool (X)) (e_binary b_or (e_binary b_have_same_symbol (X) (e_ground (@t_term symbol builtin_value "unitValue" []))) (e_unary b_isString (X))))).
+
+
+#[local]
+Instance LangDefaults : Defaults := {|
+    default_cseq_name := "builtin.cseq" ;
+    default_empty_cseq_name := "builtin.empty_cseq" ;
+    default_context_template := myContext ;
+
+    default_isValue := isValue ;
+|}.
+
+Definition frame_simple : (variable*(TermOver BuiltinOrVar)) := ("X",(@t_term symbol BuiltinOrVar "c" [(@t_term symbol BuiltinOrVar "builtin.cseq" [(t_over (bov_variable "X")); (t_over (bov_variable "REST"))]); (t_over (bov_variable "STATE"))])).
+Definition Lang_Decls : list Declaration := [
+(decl_strict (mkStrictnessDeclaration DSM "plus" 2 [0; 1] isValue myContext))
+;(decl_strict (mkStrictnessDeclaration DSM "minus" 2 [0; 1] isValue myContext))
+;(decl_strict (mkStrictnessDeclaration DSM "assign" 2 [1] isValue myContext))
+;(decl_strict (mkStrictnessDeclaration DSM "seq" 2 [0] isValue myContext))
+;(decl_strict (mkStrictnessDeclaration DSM "ite" 3 [0] isValue myContext))
+;(decl_strict (mkStrictnessDeclaration DSM "eq" 2 [0; 1] isValue myContext))
+;(decl_strict (mkStrictnessDeclaration DSM "le" 2 [0; 1] isValue myContext))
+;(decl_strict (mkStrictnessDeclaration DSM "lt" 2 [0; 1] isValue myContext))
+;(decl_strict (mkStrictnessDeclaration DSM "neg" 1 [0] isValue myContext))
+] ++ [
+(basic_rule "init" (@t_term symbol BuiltinOrVar "builtin.init" [(t_over (bov_variable "X"))]) (@t_term symbol Expression2 "c" [(@t_term symbol Expression2 "builtin.cseq" [(@t_over symbol Expression2(e_variable "X")); (@t_term symbol Expression2 "builtin.empty_cseq" [])]); (@t_over symbol Expression2(e_nullary b_map_empty))]) (e_nullary b_true))
+; (framed_rule frame_simple "aexpr.plus" (@t_term symbol BuiltinOrVar "plus" [(t_over (bov_variable "X")); (t_over (bov_variable "Y"))]) (@t_over symbol Expression2(e_binary b_Z_plus (e_variable "X") (e_variable "Y"))) (e_binary b_and (e_unary b_isZ (e_variable "X")) (e_unary b_isZ (e_variable "Y"))))
+; (framed_rule frame_simple "aexpr.minus" (@t_term symbol BuiltinOrVar "minus" [(t_over (bov_variable "X")); (t_over (bov_variable "Y"))]) (@t_over symbol Expression2(e_binary b_Z_minus (e_variable "X") (e_variable "Y"))) (e_binary b_and (e_unary b_isZ (e_variable "X")) (e_unary b_isZ (e_variable "Y"))))
+; (basic_rule "var.assign" (@t_term symbol BuiltinOrVar "c" [(@t_term symbol BuiltinOrVar "builtin.cseq" [(@t_term symbol BuiltinOrVar "assign" [(t_over (bov_variable "X")); (t_over (bov_variable "V"))]); (t_over (bov_variable "REST"))]); (t_over (bov_variable "STATE"))]) (@t_term symbol Expression2 "c" [(@t_term symbol Expression2 "builtin.cseq" [(@t_term symbol Expression2 "unitValue" []); (@t_over symbol Expression2(e_variable "REST"))]); (@t_over symbol Expression2(e_ternary b_map_update (e_variable "STATE") (e_variable "X") (e_variable "V")))]) (e_binary b_and (e_binary b_have_same_symbol (e_variable "X") (e_ground (@t_term symbol builtin_value "var" []))) (e_binary b_or (e_unary b_isZ (e_variable "V")) (e_unary b_isString (e_variable "V")))))
+; (basic_rule "var.lookup" (@t_term symbol BuiltinOrVar "c" [(@t_term symbol BuiltinOrVar "builtin.cseq" [(t_over (bov_variable "X")); (t_over (bov_variable "REST"))]); (t_over (bov_variable "STATE"))]) (@t_term symbol Expression2 "c" [(@t_term symbol Expression2 "builtin.cseq" [(@t_over symbol Expression2(e_binary b_map_lookup (e_variable "STATE") (e_variable "X"))); (@t_over symbol Expression2(e_variable "REST"))]); (@t_over symbol Expression2(e_variable "STATE"))]) (e_binary b_have_same_symbol (e_variable "X") (e_ground (@t_term symbol builtin_value "var" []))))
+; (framed_rule frame_simple "stmt.seq" (@t_term symbol BuiltinOrVar "seq" [(@t_term symbol BuiltinOrVar "unitValue" []); (t_over (bov_variable "X"))]) (@t_over symbol Expression2(e_variable "X")) (e_nullary b_true))
+; (framed_rule frame_simple "bexpr.eq" (@t_term symbol BuiltinOrVar "eq" [(t_over (bov_variable "X")); (t_over (bov_variable "Y"))]) (@t_over symbol Expression2(e_binary b_eq (e_variable "X") (e_variable "Y"))) (e_binary b_and (e_unary b_isZ (e_variable "X")) (e_unary b_isZ (e_variable "Y"))))
+; (framed_rule frame_simple "bexpr.le" (@t_term symbol BuiltinOrVar "le" [(t_over (bov_variable "X")); (t_over (bov_variable "Y"))]) (@t_over symbol Expression2(e_binary b_Z_isLe (e_variable "X") (e_variable "Y"))) (e_binary b_and (e_unary b_isZ (e_variable "X")) (e_unary b_isZ (e_variable "Y"))))
+; (framed_rule frame_simple "bexpr.lt" (@t_term symbol BuiltinOrVar "lt" [(t_over (bov_variable "X")); (t_over (bov_variable "Y"))]) (@t_over symbol Expression2(e_binary b_Z_isLt (e_variable "X") (e_variable "Y"))) (e_binary b_and (e_unary b_isZ (e_variable "X")) (e_unary b_isZ (e_variable "Y"))))
+; (framed_rule frame_simple "bexpr.neg" (@t_term symbol BuiltinOrVar "not" [(t_over (bov_variable "X"))]) (@t_over symbol Expression2(e_unary b_bool_neg (e_variable "X"))) (e_unary b_isBool (e_variable "X")))
+; (framed_rule frame_simple "stmt.ite.true" (@t_term symbol BuiltinOrVar "ite" [(t_over (bov_variable "B")); (t_over (bov_variable "X")); (t_over (bov_variable "Y"))]) (@t_over symbol Expression2(e_variable "X")) (e_binary b_and (e_unary b_isBool (e_variable "B")) (e_binary b_eq (e_variable "B") (e_nullary b_true))))
+; (framed_rule frame_simple "stmt.ite.false" (@t_term symbol BuiltinOrVar "ite" [(t_over (bov_variable "B")); (t_over (bov_variable "X")); (t_over (bov_variable "Y"))]) (@t_over symbol Expression2(e_variable "Y")) (e_binary b_and (e_unary b_isBool (e_variable "B")) (e_binary b_eq (e_variable "B") (e_nullary b_false))))
+; (framed_rule frame_simple "while.unfold" (@t_term symbol BuiltinOrVar "while" [(t_over (bov_variable "B")); (t_over (bov_variable "S"))]) (@t_term symbol Expression2 "ite" [(@t_over symbol Expression2(e_variable "B")); (@t_term symbol Expression2 "seq" [(@t_over symbol Expression2(e_variable "S")); (@t_term symbol Expression2 "while" [(@t_over symbol Expression2(e_variable "B")); (@t_over symbol Expression2(e_variable "S"))])]); (@t_term symbol Expression2 "unitValue" [])]) (e_nullary b_true))
+
+].
+Definition T := Eval vm_compute in (to_theory Act (process_declarations Act default_act Lang_Decls)). 
+Definition lang_interpreter : StepT := global_naive_interpreter (fst T).
+
+    (* This lemma asserts well-formedness of the definition *)
+    Lemma language_well_formed: isSome(RewritingTheory2_wf_heuristics (fst T)).
+    Proof.
+      (* This is the main syntactic check. If this fails, the semantics contain a bad rule. *) ltac1:(compute_done).
+    Qed.
+    (* This lemma asserts soundness of the generated interpreter. *)
+    (* Unfortunately, we cannot rely on the extraction here.
+    Lemma interp_sound:
+        Interpreter_sound'
+        (fst T)
+        lang_interpreter
+    .
+    Proof.
+        apply @global_naive_interpreter_sound.
+        { apply _. }
+        ltac1:(assert(Htmp: isSome(RewritingTheory2_wf_heuristics (fst T)))).
+        {
+            apply language_well_formed.
+        }
+        unfold is_true, isSome in Htmp.
+        destruct (RewritingTheory2_wf_heuristics (fst T)) eqn:Heq>[|inversion Htmp].
+        assumption.
+    Qed.
+    *)
+

examples-hybrid/languages

@@ -0,0 +1 @@
+../languages/

examples-hybrid/test.sh

@@ -0,0 +1,43 @@
+#!/usr/bin/env bash
+
+set -e
+
+# https://stackoverflow.com/a/246128/6209703
+SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
+
+pushd "$SCRIPT_DIR"
+
+TIME=$(which time)
+
+
+testInCoq() {
+  rm -rf coqfiles
+  mkdir -p coqfiles
+
+  echo "Generating *.v files"
+  minuska def2coq ./languages/imp/imp.m coqfiles/imp.v
+  minuska gt2coq ./imp-ast/count-1.imp coqfiles/count1.v
+  minuska gt2coq ./imp-ast/count-2.imp coqfiles/count2.v
+  minuska gt2coq ./imp-ast/count-3.imp coqfiles/count3.v
+  minuska gt2coq ./imp-ast/count-4.imp coqfiles/count4.v
+  minuska gt2coq ./imp-ast/count-5.imp coqfiles/count5.v
+  minuska gt2coq ./imp-ast/count-6.imp coqfiles/count6.v
+  minuska gt2coq ./imp-ast/count-7.imp coqfiles/count7.v
+
+  pushd coqfiles > /dev/null
+  for vfile in *.v; do
+    echo "Compiling $vfile"
+    coqc -R . Test "$vfile" > /dev/null
+  done 
+  popd > /dev/null
+  cp test-imp/testCount*.v ./coqfiles/
+  pushd coqfiles > /dev/null
+  for testvfile in testCount*.v; do
+    echo "coqc $testvfile"
+    "$TIME" --output "$testvfile.time" --format "%e" coqc -R . Test "$testvfile" 2> /dev/null
+    cat "$testvfile.time"
+  done
+  popd > /dev/null
+}
+
+testInCoq

examples-standalone/languages

@@ -0,0 +1 @@
+../languages/

examples-standalone/test.sh

@@ -8,11 +8,22 @@ SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
 pushd "$SCRIPT_DIR"
 
 TEMPDIR="$(pwd)/_temp"
+LOGFILEOUT="$TEMPDIR/log-stdout.txt"
+LOGFILEERR="$TEMPDIR/log-stderr.txt"
 TIME=$(which time)
 
 rm -rf "$TEMPDIR"
 mkdir -p "$TEMPDIR"
 
+> "$LOGFILEOUT"
+> "$LOGFILEERR"
+
+printlogs() {
+  cat "$LOGFILEERR"
+  cat "$LOGFILEOUT"
+}
+# Enable this when debugging
+#trap printlogs 0
 
 run10times() {
   for run in {1..10}; do "$@"; done
@@ -27,85 +38,62 @@ runCase() {
 
   output=$(mktemp)
   echo "Running test '$name'"
-  "$TIME" --output "$output.time" --format "%e" "$interpreter" --depth "$depth" --output-file "$output" "$input" 2>/dev/null >/dev/null
-  diff "$output" "$expout"
+  "$TIME" --output "$output.time" --format "%e" "$interpreter" --depth "$depth" --output-file "$output" "$input" 2>>"$LOGFILEERR" >>"$LOGFILEOUT"
+  if [[ -e "$expout" ]]; then
+    diff "$output" "$expout"
+  fi
   cat "$output.time"
   rm -f "$output"
 }
 
 doCompile() {
-  local cmd="$@"
-  echo "Compiling: minuska compile $cmd" 
-  minuska compile $cmd 2>/dev/null >/dev/null && echo "Compilation finished."
+  local lang="$1"
+  echo "Compiling: minuska generate-interpreter $lang" 
+  mkdir -p interpreters
+  pushd interpreters
+  minuska generate-interpreter ../languages/$lang/lang.scm 2>>"$LOGFILEERR" >>"$LOGFILEOUT" && echo "Compilation finished."
+  local state=$?
+  readelf -d "$lang-interpreter" || true
+  popd
+  return $state
 }
 
 
 testNative() {
   rm -rf ./interpreters
   mkdir -p ./interpreters
 
-  if doCompile ./m/fail-invalid-semantics.m interpreters/invalid.exe ; then
+  if doCompile fail-invalid-semantics ; then
     echo "ERROR: an invalid language definition compiles!"
     exit 1
   fi
 
 
-  doCompile ./m/decrement.m ./interpreters/decrement
+  doCompile decrement
   echo "Decrement tests"
-  runCase "dec into 2" ./interpreters/decrement ./m/decrement.d/three 2 ./m/decrement.d/two
-  runCase "dec into 1" ./interpreters/decrement ./m/decrement.d/three 3 ./m/decrement.d/one
+  runCase "dec into 2" ./interpreters/decrement-interpreter ./languages/decrement/tests/three.dec 2 DONOTTTEST
+  runCase "dec into 1" ./interpreters/decrement-interpreter ./languages/decrement/tests/three.dec 3 DONOTTTEST
 
 
-  doCompile ./m/decrement-builtin.m ./interpreters/decrement-builtin
-  runCase "dec builtin into -1" ./interpreters/decrement-builtin ./m/decrement-builtin.d/cfg_3 5 ./m/decrement-builtin.d/cfg_minus_1
+  doCompile decrement-builtin
+  runCase "dec builtin into -1" ./interpreters/decrement-builtin-interpreter ./languages/decrement-builtin/tests/cfg_3.decb 5 ./languages/decrement-builtin/tests/cfg_minus_1
 
-  doCompile ./m/arith.m ./interpreters/arith
-  runCase "arith-01" ./interpreters/arith ./m/arith.d/01 20 ./m/arith.d/01.result
+  doCompile arith
+  runCase "arith-01" ./interpreters/arith-interpreter ./languages/arith/tests/01.arith 20 ./languages/arith/tests/01.result
 
-  doCompile ./m/imp.m ./interpreters/imp
-  runCase "imp-01" ./interpreters/imp ./m/imp.d/01 20 ./m/imp.d/01.result
-  runCase "imp-lookup" ./interpreters/imp ./m/imp.d/00-assign-lookup-trivial.imp 20 ./m/imp.d/00-assign-lookup-trivial.result
-  runCase "imp-count-10" ./interpreters/imp ./m/imp.d/03-count-10.imp 1000 ./m/imp.d/03-count-10.result
+  doCompile imp
+  runCase "imp-01" ./interpreters/imp-interpreter ./languages/imp/tests/01.imp 20 ./languages/imp/tests/01.result
+  #runCase "imp-lookup" ./interpreters/imp-interpreter ./languages/imp/tests/00-assign-lookup-trivial.imp 20 ./languages/imp/tests/00-assign-lookup-trivial.result
+  runCase "imp-count-10" ./interpreters/imp-interpreter ./languages/imp/tests/03-count-10.imp 1000 ./languages/imp/tests/03-count-10.result
 
 
-  doCompile ./m/two-counters.m ./interpreters/two-counters
-  runCase "two-counters.10" ./interpreters/two-counters ./m/two-counters.d/10         50000000 ./m/two-counters.d/10.result
-  runCase "two-counters.100" ./interpreters/two-counters ./m/two-counters.d/100       50000000 ./m/two-counters.d/100.result
-  runCase "two-counters.1'000" ./interpreters/two-counters ./m/two-counters.d/1000     50000000 ./m/two-counters.d/1000.result
-  runCase "two-counters.10'000" ./interpreters/two-counters ./m/two-counters.d/10000   50000000 ./m/two-counters.d/10000.result
-  runCase "two-counters.100'000" ./interpreters/two-counters ./m/two-counters.d/100000  50000000 ./m/two-counters.d/100000.result
-  runCase "two-counters.1'000'000" ./interpreters/two-counters ./m/two-counters.d/1000000 50000000 ./m/two-counters.d/1000000.result
-}
-
-testInCoq() {
-  rm -rf coqfiles
-  mkdir -p coqfiles
-
-  echo "Generating *.v files"
-  minuska def2coq ./m/imp.m coqfiles/imp.v
-  minuska gt2coq ./m/imp.d/count-1.imp coqfiles/count1.v
-  minuska gt2coq ./m/imp.d/count-2.imp coqfiles/count2.v
-  minuska gt2coq ./m/imp.d/count-3.imp coqfiles/count3.v
-  minuska gt2coq ./m/imp.d/count-4.imp coqfiles/count4.v
-  minuska gt2coq ./m/imp.d/count-5.imp coqfiles/count5.v
-  minuska gt2coq ./m/imp.d/count-6.imp coqfiles/count6.v
-  minuska gt2coq ./m/imp.d/count-7.imp coqfiles/count7.v
-
-  pushd coqfiles > /dev/null
-  for vfile in *.v; do
-    echo "Compiling $vfile"
-    coqc -R . Test "$vfile" > /dev/null
-  done 
-  popd > /dev/null
-  cp test-imp/testCount*.v ./coqfiles/
-  pushd coqfiles > /dev/null
-  for testvfile in testCount*.v; do
-    echo "coqc $testvfile"
-    "$TIME" --output "$testvfile.time" --format "%e" coqc -R . Test "$testvfile" 2> /dev/null
-    cat "$testvfile.time"
-  done
-  popd > /dev/null
+  doCompile two-counters
+  runCase "two-counters.10"        ./interpreters/two-counters-interpreter ./languages/two-counters/tests/10.tc      50000000 ./languages/two-counters/tests/10.result
+  runCase "two-counters.100"       ./interpreters/two-counters-interpreter ./languages/two-counters/tests/100.tc     50000000 ./languages/two-counters/tests/100.result
+  runCase "two-counters.1'000"     ./interpreters/two-counters-interpreter ./languages/two-counters/tests/1000.tc    50000000 ./languages/two-counters/tests/1000.result
+  runCase "two-counters.10'000"    ./interpreters/two-counters-interpreter ./languages/two-counters/tests/10000.tc   50000000 ./languages/two-counters/tests/10000.result
+  runCase "two-counters.100'000"   ./interpreters/two-counters-interpreter ./languages/two-counters/tests/100000.tc  50000000 ./languages/two-counters/tests/100000.result
+  runCase "two-counters.1'000'000" ./interpreters/two-counters-interpreter ./languages/two-counters/tests/1000000.tc 50000000 ./languages/two-counters/tests/1000000.result
 }
 
-testInCoq
 testNative