From 5ff215e051073819364f1e79fa09d2db22836758 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Thu, 10 Aug 2023 20:31:53 -0400 Subject: [PATCH] env doesn't really need to be an Instance, it seems --- bedrock2/src/bedrock2/Semantics.v | 2 +- bedrock2/src/bedrock2Examples/Trace.v | 1 - compiler/src/compiler/ExprImpEventLoopSpec.v | 4 ++-- 3 files changed, 3 insertions(+), 4 deletions(-) diff --git a/bedrock2/src/bedrock2/Semantics.v b/bedrock2/src/bedrock2/Semantics.v index 0fb71d63..28f773eb 100644 --- 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 index 03731bba..495cf29d 100644 --- 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 index 6d6d480f..9fd05641 100644 --- 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);