Merge pull request #26 from h0nzZik/rm-lowlang

Naive interpreter is now implemented directly and avoids translation to lowlang
h0nzZik · Jul 6, 2024 · de73b75 · de73b75
2 parents be1776a + aec57e5
commit de73b75
Show file tree

Hide file tree

Showing 10 changed files with 1,918 additions and 1,884 deletions.
diff --git a/flake.nix b/flake.nix
@@ -208,6 +208,17 @@
                 packages = [minuska minuska.coqPackages.coq-lsp minuska.coqPackages.coq];
               };
 
+          languages-in-coq =
+            let
+              languages-in-coq = self.outputs.packages.${system}.languages-in-coq;
+            in
+              pkgs.mkShell {
+                inputsFrom = [languages-in-coq];
+                packages = [
+                  languages-in-coq.coqPackages.coq-lsp
+                ];
+              };
+
           examples-coq =
             let
               examples-coq = self.outputs.packages.${system}.examples-coq;

diff --git a/languages-in-coq/theories/examples.v b/languages-in-coq/theories/examples.v
@@ -802,9 +802,7 @@ Module imp.
         (naive_interpreter Γ.1) 
     .
     Proof.
-        Check @naive_interpreter_sound.
-        apply @naive_interpreter_sound.
-        { apply _. }
+        apply naive_interpreter_sound.
         ltac1:(assert(Htmp: isSome(RewritingTheory2_wf_heuristics (Γ.1)))).
         {
             ltac1:(compute_done).

diff --git a/minuska/_CoqProject b/minuska/_CoqProject
@@ -9,8 +9,8 @@ theories/spec_syntax.v
 theories/varsof.v
 theories/syntax_properties.v
 theories/semantics_properties.v
-theories/spec_lowlang_interpreter.v
 theories/spec_interpreter.v
+theories/valuation_merge.v
 
 theories/minuska.v
 theories/string_variables.v

diff --git a/minuska/bin/main.ml b/minuska/bin/main.ml
@@ -36,7 +36,7 @@ let append_definition input_filename output_channel =
     .
     Proof.
         apply @global_naive_interpreter_sound.
-        { apply _. }
+        (*{ apply _. }*)
         ltac1:(assert(Htmp: isSome(RewritingTheory2_wf_heuristics (fst T)))).
         {
             apply language_well_formed.