better encode/decode of builtin values

h0nzZik · Apr 20, 2024 · dd357ba · dd357ba
1 parent 63e2651
commit dd357ba
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 5 deletions.
diff --git a/minuska-examples/theories/examples.v b/minuska-examples/theories/examples.v
@@ -1,5 +1,5 @@
 From Coq.Logic Require Import ProofIrrelevance.
-
+From stdpp Require Import countable.
 
 From Minuska Require Import
     prelude
@@ -31,6 +31,10 @@ Module two_counters.
     #[local]
     Instance Σ : StaticModel := default_model (default_builtin.β).
 
+    Set Printing Implicit.
+    Check @encode.
+    Compute (@encode (Term' (@symbol Σ) BuiltinValue.BuiltinValue0) _ (@Term'_countable (@symbol Σ) string_eq_dec string_countable BuiltinValue.BuiltinValue0 _ (@BuiltinValue.BuiltinValue0_countable (@symbol Σ) string_eq_dec string_countable)) (uglify' (t_term "ahoj" [t_over (BuiltinValue.bv_Z 3)]))).
+    Compute (@encode (@TermOver' (@symbol Σ) BuiltinValue.BuiltinValue0)) _ (@TermOver_count (@symbol Σ) BuiltinValue.BuiltinValue0 string_eq_dec _ string_countable (@BuiltinValue.BuiltinValue0_countable (@symbol Σ) string_eq_dec string_countable)) ((t_term "ahoj" [t_over (BuiltinValue.bv_Z 3)])).
 
     Definition M : variable := "M".
     Definition N : variable := "N".

diff --git a/minuska/bin/main.ml b/minuska/bin/main.ml
@@ -82,7 +82,7 @@ let compile input_filename interpreter_name () =
   let _ = run [
           "cd "; mldir; "; ";
           "env OCAMLPATH="; libdir; ":$OCAMLPATH ";
-          "ocamlfind ocamlopt -thread -package coq-minuska -package zarith -linkpkg -g -w -20 -w -26 -o ";
+          "ocamlfind ocamlopt -thread -package coq-minuska -package zarith -linkpkg -g -o ";
           "interpreter.exe"; " "; (String.append mlfile "i"); " "; mlfile] in
   let _ = run ["mv "; mldir; "/interpreter.exe"; " "; real_interpreter_name] in
   let _ = input_filename in

diff --git a/minuska/theories/builtins.v b/minuska/theories/builtins.v
@@ -276,6 +276,8 @@ Module default_builtin.
             x y
         .
 
+        Definition my_encode := ((@encode (@TermOver' (symbol) BuiltinValue.BuiltinValue0)) _ (@TermOver_count (symbol) BuiltinValue.BuiltinValue0 (@symbol_eqdec symbol symbols) _ (@symbol_countable symbol symbols) (@BuiltinValue.BuiltinValue0_countable (symbol) (@symbol_eqdec symbol symbols) (@symbol_countable symbol symbols)))).
+
         #[local]
         Instance β
             : Builtin
@@ -382,7 +384,7 @@ Module default_builtin.
                 | b_map_hasKey =>
                     match v1 with
                     | t_over (bv_pmap m) =>
-                        let p := encode (uglify' v2) in
+                        let p := my_encode (v2) in
                         match m !! p with
                         | Some _ => (t_over (bv_bool true))
                         | None => (t_over (bv_bool false))
@@ -392,7 +394,7 @@ Module default_builtin.
                 | b_map_lookup =>
                     match v1 with
                     | t_over (bv_pmap m) =>
-                        let p := encode (uglify' v2) in
+                        let p := my_encode (v2) in
                         match m !! p with
                         | Some v => (prettify v)
                         | None => err
@@ -423,7 +425,7 @@ Module default_builtin.
                 | b_map_update =>
                     match v1 with
                     | t_over (bv_pmap m) =>
-                        let p := encode (uglify' v2) in
+                        let p := my_encode (v2) in
                         let m' := <[ p := (uglify' v3) ]>m in
                         t_over (bv_pmap m')
                     | _ => err