summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--language/l2.ott4
-rw-r--r--language/l2_parse.ott4
-rw-r--r--src/lem_interp/interp.lem44
-rw-r--r--src/lem_interp/interp_lib.lem2
-rw-r--r--src/test/test1.sail8
5 files changed, 40 insertions, 22 deletions
diff --git a/language/l2.ott b/language/l2.ott
index f0edda3f..5d1994e2 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -561,7 +561,7 @@ exp :: 'E_' ::=
% here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn
% the expi and the result are both of type vector of 'a
- | [ num1 = exp1 , ... , numn = expn , opt_default ] :: :: vector_indexed {{ com vector (indexed consecutively) }}
+ | [ num1 = exp1 , ... , numn = expn opt_default ] :: :: vector_indexed {{ com vector (indexed consecutively) }}
% num1 .. numn must be a consecutive list of naturals
% we pick [ ] not { } for vector literals for consistency with their
@@ -661,7 +661,7 @@ opt_default :: 'Def_val_' ::=
{{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }}
{{ aux _ annot }} {{ auxparam 'a }}
| :: :: empty
- | default = exp :: :: dec
+ | ; default = exp :: :: dec
pexp :: 'Pat_' ::=
{{ com Pattern match }}
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index f1149301..03c50d08 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -452,7 +452,7 @@ exp :: 'E_' ::=
% here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn
% the expi and the result are both of type vector of 'a
- | [ exp1 , ... , expn , opt_default ] :: :: vector_indexed {{ com vector (indexed consecutively) }}
+ | [ exp1 , ... , expn opt_default ] :: :: vector_indexed {{ com vector (indexed consecutively) }}
% num1 .. numn must be a consecutive list of naturals
% we pick [ ] not { } for vector literals for consistency with their
@@ -550,7 +550,7 @@ opt_default :: 'Def_val_' ::=
{{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }}
{{ aux _ l }}
| :: :: empty
- | default = exp :: :: dec
+ | ; default = exp :: :: dec
pexp :: 'Pat_' ::=
{{ com Pattern match }}
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 8ce1c354..f9a64da1 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1,8 +1,8 @@
open import Pervasives
import Map
-import Map_extra
-import List_extra
-open import String_extra
+import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *)
+import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
+open import String_extra (* for 'show' to convert nat to string) *)
open import Interp_ast
@@ -100,7 +100,7 @@ instance (Eq value)
let (<>) n1 n2 = not (value_eq n1 n2)
end
-(*Constant unit value, for frequent uses in interpreter *)
+(*Constant unit value, for use in interpreter *)
let unitv = V_lit (L_aux L_unit Unknown)
(* Store for local memory of ref cells *)
@@ -448,7 +448,7 @@ let add_to_top_frame e_builder stack =
let top_hole stack : bool =
match stack with
- | Hole_frame _ (E_aux (E_id (Id_aux (Id "1") _)) _) _ _ _ _ -> true
+ | Hole_frame _ (E_aux (E_id (Id_aux (Id "0") _)) _) _ _ _ Top -> true
| _ -> false
end
@@ -1108,7 +1108,6 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| Nothing -> Error l "Internal error, unrecognized read, no reg" end
| _ -> update_stack a (add_to_top_frame (fun e -> E_aux(E_field e id) (l,annot))) end)
| E_vector_access vec i ->
- (*Need to update to read one position of a register*)
resolve_outcome (interp_main mode t_level l_env l_mem i)
(fun iv lm le ->
match iv with
@@ -1120,13 +1119,19 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| V_vector_sparse _ _ _ _ _ -> (Value (access_vector vvec n) Tag_empty,lm,le)
| V_unknown -> (Value V_unknown Tag_empty,lm,le)
| _ -> (Error l "Vector access of non-vector",lm,le)end)
- (fun a -> update_stack a
- (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)))))
+ (fun a ->
+ match a with
+ | Action (Read_reg reg Nothing) stack ->
+ if (top_hole stack)
+ then Action (Read_reg reg (Just(n,n))) stack
+ else Action (Read_reg reg Nothing) (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot))) stack)
+ | _ ->
+ update_stack a
+ (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)))) end)
| V_unknown -> (Value V_unknown Tag_empty,lm,le)
| _ -> (Error l "Vector access not given a number for index",lm,l_env) end)
(fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_access vec i) (l,annot))))
| E_vector_subrange vec i1 i2 ->
- (*Need to update to read a slice of a register*)
resolve_outcome (interp_main mode t_level l_env l_mem i1)
(fun i1v lm le ->
match i1v with
@@ -1142,12 +1147,21 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| V_vector_sparse _ _ _ _ _ -> (Value (slice_vector vvec n1 n2) Tag_empty, lm,le)
| V_unknown -> (Value V_unknown Tag_empty,lm,le)
| _ -> (Error l "Vector slice of non-vector",lm,le)end)
- (fun a -> update_stack a
- (add_to_top_frame
- (fun v -> (E_aux (E_vector_subrange v
- (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
- (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
- (l,annot)))))
+ (fun a ->
+ match a with
+ | Action (Read_reg reg Nothing) stack ->
+ if (top_hole stack)
+ then Action (Read_reg reg (Just(n1,n2))) stack
+ else Action (Read_reg reg Nothing) (add_to_top_frame (fun v -> (E_aux (E_vector_subrange v
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
+ (l,annot))) stack)
+ | _ -> update_stack a
+ (add_to_top_frame
+ (fun v -> (E_aux (E_vector_subrange v
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
+ (l,annot)))) end)
| V_unknown -> (Value V_unknown Tag_empty, lm,le)
| _ -> (Error l "vector slice given non number for last index",lm,le) end)
(fun a -> update_stack a
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 13aa728f..c4087edb 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -1,7 +1,7 @@
open import Pervasives
open import Interp
open import Interp_ast
-import Assert_extra Maybe_extra
+import Assert_extra Maybe_extra (* For failwith for error reporting while debugging; and for fromJust when we know it's not Nothing *)
open import Num
open import List
open import Word
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 18863ce2..1ca615c5 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -19,7 +19,7 @@ let ( bit [32] ) v2 = 0xABCDEF01
val forall Type 'a. 'a -> 'a effect pure identity
function forall Type 'a. 'a identity i = i
-function unit ignore(x) = ()
+(*function unit ignore(x) = ()*)
(* scattered function definition and union definition *)
scattered typedef ast = const union
@@ -41,5 +41,9 @@ function unit a (bit) b = if identity(b) then (identity()) else ()
function bit sw s = switch s { case 0 -> bitzero }
-function bit main _ = {ignore(sw(0)); ignore((nat) v2); v1[0] }
+let colors rgb = red
+
+function bit enu (red) = 0
+
+function bit main _ = {ignore(sw(0)); ignore((nat) v2); ignore(enu(0)); v1[0] }
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:03:41 +0000