env doesn't really need to be an Instance, it seems

mit-plv · Aug 11, 2023 · 5ff215e · 5ff215e
1 parent fb4def2
commit 5ff215e
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 4 deletions.
diff --git a/bedrock2/src/bedrock2/Semantics.v b/bedrock2/src/bedrock2/Semantics.v
@@ -75,7 +75,7 @@ Section binops.
     end.
 End binops.
 
-#[export] Instance env: map.map String.string Syntax.func := SortedListString.map _.
+Definition env: map.map String.string Syntax.func := SortedListString.map _.
 #[export] Instance env_ok: map.ok env := SortedListString.ok _.
 
 Section semantics.

diff --git a/bedrock2/src/bedrock2Examples/Trace.v b/bedrock2/src/bedrock2Examples/Trace.v
@@ -20,7 +20,6 @@ Module Import IOMacros.
     word :> Word.Interface.word width;
     mem :> map.map word Byte.byte;
     locals :> map.map String.string word;
-    env :> map.map String.string (list String.string * list String.string * cmd);
     ext_spec :> ExtSpec;
 
     (* macros to be inlined to read or write a word

diff --git a/compiler/src/compiler/ExprImpEventLoopSpec.v b/compiler/src/compiler/ExprImpEventLoopSpec.v
@@ -37,12 +37,12 @@ Section Params1.
   {
     funs_valid: valid_src_funs e = true;
     init_code: Syntax.cmd.cmd;
-    get_init_code: map.get (map.of_list e) init_f = Some (nil, nil, init_code);
+    get_init_code: map.get (map.of_list e : env) init_f = Some (nil, nil, init_code);
     init_code_correct: forall m0 mc0,
         mem_available spec.(datamem_start) spec.(datamem_pastend) m0 ->
         MetricSemantics.exec (map.of_list e) init_code nil m0 map.empty mc0 (hl_inv spec);
     loop_body: Syntax.cmd.cmd;
-    get_loop_body: map.get (map.of_list e) loop_f = Some (nil, nil, loop_body);
+    get_loop_body: map.get (map.of_list e : env) loop_f = Some (nil, nil, loop_body);
     loop_body_correct: forall t m l mc,
         hl_inv spec t m l mc ->
         MetricSemantics.exec (map.of_list e) loop_body t m l mc (hl_inv spec);