Support for nondeterminism in language specifications (#28)

h0nzZik · Jul 10, 2024 · 65f49b2 · 65f49b2
1 parent dce78bb
commit 65f49b2
Show file tree

Hide file tree

Showing 45 changed files with 1,726 additions and 6,362 deletions.
diff --git a/bench-hybrid/coqfiles/imp.v b/bench-hybrid/coqfiles/imp.v
@@ -58,7 +58,7 @@ Definition lang_interpreter : StepT := global_naive_interpreter (fst T).
     .
     Proof.
         apply @global_naive_interpreter_sound.
-        { apply _. }
+        (*{ apply _. }*)
         ltac1:(assert(Htmp: isSome(RewritingTheory2_wf_heuristics (fst T)))).
         {
             apply language_well_formed.

diff --git a/bench-hybrid/test-imp/testCount1.v b/bench-hybrid/test-imp/testCount1.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     imp.lang_interpreter
     steps
     count1.given_groundterm

diff --git a/bench-hybrid/test-imp/testCount2.v b/bench-hybrid/test-imp/testCount2.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     imp.lang_interpreter
     steps
     count2.given_groundterm

diff --git a/bench-hybrid/test-imp/testCount3.v b/bench-hybrid/test-imp/testCount3.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     imp.lang_interpreter
     steps
     count3.given_groundterm

diff --git a/bench-hybrid/test-imp/testCount4.v b/bench-hybrid/test-imp/testCount4.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     imp.lang_interpreter
     steps
     count4.given_groundterm

diff --git a/bench-hybrid/test-imp/testCount5.v b/bench-hybrid/test-imp/testCount5.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     imp.lang_interpreter
     steps
     count5.given_groundterm

diff --git a/bench-hybrid/test-imp/testCount6.v b/bench-hybrid/test-imp/testCount6.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     imp.lang_interpreter
     steps
     count6.given_groundterm

diff --git a/bench-hybrid/test-imp/testCount7.v b/bench-hybrid/test-imp/testCount7.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     imp.lang_interpreter
     steps
     count7.given_groundterm

diff --git a/bench-hybrid/test-tc/testTC10.v b/bench-hybrid/test-tc/testTC10.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     twocounters.lang_interpreter
     steps
     tc10.given_groundterm

diff --git a/bench-hybrid/test-tc/testTC100.v b/bench-hybrid/test-tc/testTC100.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     twocounters.lang_interpreter
     steps
     tc100.given_groundterm

diff --git a/bench-hybrid/test-tc/testTC20.v b/bench-hybrid/test-tc/testTC20.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     twocounters.lang_interpreter
     steps
     tc20.given_groundterm

diff --git a/bench-hybrid/test-tc/testTC50.v b/bench-hybrid/test-tc/testTC50.v
@@ -12,6 +12,8 @@ Import Ascii.
 Time Compute (let steps := 10000 in
   @interp_loop.interp_loop
     default_everything.DSM
+    spec.nondet_gen
+    0
     twocounters.lang_interpreter
     steps
     tc50.given_groundterm

diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -44,6 +44,7 @@
               coqPackages.coq.ocamlPackages.core_unix
               coqPackages.coq.ocamlPackages.ppx_jane
               coqPackages.coq.ocamlPackages.ppx_sexp_conv
+              coqPackages.coq.ocamlPackages.base_quickcheck
               coqPackages.coq.ocamlPackages.benchmark
            ] ++ coqLibraries ; in
            let wrapped = coqPackages.callPackage  ( { coq, stdenv }: coqPackages.mkCoqDerivation {
@@ -72,6 +73,7 @@
               inherit coqLibraries;
 	    };
 
+
             postPatch = ''
               substituteInPlace bin/main.ml \
                 --replace-fail "/coq/user-contrib/Minuska" "/coq/${coqVersion}/user-contrib/Minuska" \
@@ -86,7 +88,17 @@
               runHook postBuild
             '';
 
+            #installFlags = [ "COQLIB=$(out)/lib/coq/${coqPackages.coq.coq-version}/" ];
+
+            #installPhase = ''
+            #  mkdir -p $out
+            #  runHook preInstall
+            #  dune install --prefix $out
+            #  runHook postInstall
+            #'';
+
             postInstall = ''
+              dune install --prefix $out libminuska
               wrapProgram $out/bin/minuska \
                 --set OCAMLFIND_DESTDIR $OCAMLFIND_DESTDIR \
                 --set OCAMLPATH $OCAMLPATH \

diff --git a/languages-in-coq/theories/examples.v b/languages-in-coq/theories/examples.v
@@ -93,7 +93,7 @@ Module two_counters.
 
     Definition interp_loop_number fuel := 
         fun (m n : nat) =>
-        let fg' := ((interp_loop interp fuel) ∘ pair_to_state) (m,n) in
+        let fg' := ((interp_loop nondet_gen 0 interp fuel) ∘ pair_to_state) (m,n) in
         state_to_pair fg'.2
     .
     Compute (interp_loop_number 100 10 10).
@@ -157,7 +157,7 @@ Module two_counters_Z.
 
     Definition interp_loop_number (fuel : nat) := 
         fun (m n : Z) =>
-        let fg' := (((interp_in_from Γ fuel)) ∘ pair_to_state) (m,n) in
+        let fg' := (((interp_in_from Γ nondet_gen fuel)) ∘ pair_to_state) (m,n) in
         state_to_pair fg'.1.2
     .
 
@@ -314,7 +314,7 @@ Module arith.
     .
 
     Definition interp_from (fuel : nat) from
-        := interp_in_from Γ fuel from
+        := interp_in_from Γ nondet_gen fuel from
     .
 
     Definition interp_list (fuel : nat) (x : Z) (ly : list Z)
@@ -436,7 +436,7 @@ Module fib_native.
 
 
     Definition interp_from (fuel : nat) from
-        := interp_in_from Γ fuel from
+        := interp_in_from Γ nondet_gen fuel from
     .
 
     Definition initial0 (x : TermOver builtin_value) :=
@@ -446,7 +446,7 @@ Module fib_native.
     .
 
     Definition fib_interp_from (fuel : nat) (from : Z)
-        := interp_in_from Γ fuel (ground (initial0
+        := interp_in_from Γ nondet_gen fuel (ground (initial0
                 (t_over (bv_Z from))))
     .
 
@@ -791,7 +791,7 @@ Module imp.
 
     Definition initial0 (x : TermOver builtin_value) :=
         (ground (
-            u_cfg [ u_state [ u_cseq [x; u_emptyCseq [] ] ; (builtin_nullary_function_interp b_map_empty) ] ]
+            u_cfg [ u_state [ u_cseq [x; u_emptyCseq [] ] ; (builtin_nullary_function_interp b_map_empty (nondet_gen 0)) ] ]
         ))
     .
 
@@ -813,7 +813,7 @@ Module imp.
     Qed.
 
     Definition imp_interp_from (fuel : nat) (from : (TermOver builtin_value))
-        := interp_loop (naive_interpreter Γ.1) fuel (ground (initial0 from))
+        := interp_loop nondet_gen 1 (naive_interpreter Γ.1) fuel (ground (initial0 from))
     .
 
     (*  

diff --git a/languages-in-coq/theories/examples_unary_nat.v b/languages-in-coq/theories/examples_unary_nat.v
@@ -199,7 +199,7 @@ Module unary_nat.
     .
 
     Definition interp_fact(fuel : nat) (from : nat)
-    := let r := interp_loop (naive_interpreter Γfact.1) fuel (initial_fact from) in
+    := let r := interp_loop nondet_gen 1 (naive_interpreter Γfact.1) fuel (initial_fact from) in
         (r.1, (final r.2))
     .
     (* Time Compute ((interp_fact 500 4)). *)
@@ -261,7 +261,7 @@ Module unary_nat.
 
     Definition interp_fib (fuel : nat) (from : nat)
     := 
-        let r := interp_loop (naive_interpreter Γfib.1) fuel ((initial_fib from)) in
+        let r := interp_loop nondet_gen 1 (naive_interpreter Γfib.1) fuel ((initial_fib from)) in
         (r.1, (final r.2))
     .
 

diff --git a/minuska/bin/dune b/minuska/bin/dune
@@ -1,5 +1,6 @@
 (executable
  (public_name minuska)
+ (package libminuska)
  (name main)
  (modules main)
  (libraries

diff --git a/minuska/bin/main.ml b/minuska/bin/main.ml
@@ -111,7 +111,7 @@ let compile input_filename interpreter_name oparserexe parser_builder () =
   fprintf oux_coqfile "Extraction \"%s\" lang_interpreter.\n" ("interpreter.ml");
   Out_channel.close oux_coqfile;
   (* extract coq into ocaml *)
-  let libdir = Filename.dirname (Filename_unix.realpath (Sys_unix.executable_name)) ^ "/../lib" in
+  let libdir = (Filename_unix.realpath (Filename.dirname (Filename_unix.realpath (Sys_unix.executable_name)) ^ "/../lib")) in
   let minuska_dir = libdir ^ "/coq/user-contrib/Minuska" in
   let coq_minuska_dir = libdir ^ "/coq-minuska" in
   let _ = coq_minuska_dir in
@@ -120,11 +120,12 @@ let compile input_filename interpreter_name oparserexe parser_builder () =
   (if rv <> 0 then failwith "`coqc` failed. Is the language definition well-formed?");
   (* compile the main ocaml file (after adding an entry command) *)
   let _ = Out_channel.with_file ~append:true mlfile ~f:(fun outc -> fprintf outc "let _ = (Libminuska.Miskeleton.main %s lang_interpreter)\n" oparseexestr) in
+  (*let _ = run [ "env" ] in*)
   (*let _ = run ["cat "; mlfile] in*)
   let _ = run [
           "cd "; mldir; "; ";
           "env OCAMLPATH="; libdir; ":$OCAMLPATH ";
-          "ocamlfind ocamlopt -thread -package coq-minuska -package zarith -linkpkg -g -o ";
+          "ocamlfind ocamlopt -thread -package libminuska -package zarith -linkpkg -g -o ";
           "interpreter.exe"; " "; (String.append mlfile "i"); " "; mlfile] in
   (* Filename.dirname Sys.argv.(0) ^ "../lib" *)
   let _ = Core_unix.mkdir_p appdir in

diff --git a/minuska/coq-minuska.opam b/minuska/coq-minuska.opam
@@ -1,24 +1,14 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 version: "0.2"
-synopsis: "A formally verified programming language framework"
-description:
-  "Minuska is a programming language framework capable of generating interpreters from operational semantics."
 maintainer: ["Jan Tušil <[email protected]>"]
 authors: ["Jan Tušil <[email protected]>"]
 license: "MIT"
-tags: ["operational semantics" "interpreters"]
 homepage: "https://github.com/h0nzZik/minuska"
 bug-reports: "https://github.com/h0nzZik/minuska/issues"
 depends: [
   "dune" {>= "3.14"}
-  "benchmark"
-  "coq"
-  "menhir"
-  "core"
-  "zarith"
-  "core_unix"
-  "yaml"
+  "cpq"
   "odoc" {with-doc}
 ]
 build: [

diff --git a/minuska/dune-project b/minuska/dune-project
@@ -2,7 +2,7 @@
 (using coq 0.8)
 
 
-(name coq-minuska)
+(name libminuska)
 (version 0.2)
 
 (using menhir 3.0)
@@ -19,7 +19,14 @@
 (license MIT)
 
 (package
- (name coq-minuska)
+  (name coq-minuska)
+  (depends
+     cpq
+  )
+)
+
+(package
+ (name libminuska)
  (depends
     benchmark
     coq

diff --git a/minuska/lib/dune b/minuska/lib/dune
@@ -20,7 +20,7 @@
 
 (library
  (name libminuska)
- (public_name coq-minuska)
+ (public_name libminuska)
  (modules syntax parser lexer miparse micoqprint miunparse miskeleton libminuska dsm)
  (libraries
     benchmark

diff --git a/minuska/theories/BuiltinValue.v b/minuska/theories/BuiltinValue.v
@@ -170,8 +170,8 @@ Section sec.
         revert x Hsz y.
         induction sz; intros x Hsz y.
         {
-            abstract(destruct x; simpl in Hsz; try ltac1:(lia);
-            destruct m; simpl in Hsz; try ltac1:(lia)).
+            (*abstract( *)destruct x; simpl in Hsz; try ltac1:(lia);
+            destruct m; simpl in Hsz; try ltac1:(lia) (* ) *) .
         }
         {
             destruct x.