diff options
| -rw-r--r-- | src/lem_interp/run_interp.ml | 3 | ||||
| -rw-r--r-- | src/lexer.mll | 1 | ||||
| -rw-r--r-- | src/test/test3.sail | 6 |
3 files changed, 10 insertions, 0 deletions
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml index ab5cc9f7..5708834d 100644 --- a/src/lem_interp/run_interp.ml +++ b/src/lem_interp/run_interp.ml @@ -54,6 +54,8 @@ let act_to_string = function | Write_mem (id, args, sub, value) -> sprintf "write_mem %s(%s)%s = %s" (id_to_string id) (val_to_string args) (sub_to_string sub) (val_to_string value) + | Call_extern (name, arg) -> + "extern call to " ^ name ;; module Reg = struct @@ -75,6 +77,7 @@ let perform_action ((reg, mem) as env) = function V_lit L_unit, (Reg.update id value reg, mem) | Write_mem (id, args, None, value) -> V_lit L_unit, (reg, Mem.update (id, args) value mem) + | Call_extern (name, arg) -> failwith "extern calls not implemented" (* XXX *) | _ -> failwith "partial read/write not implemented" (* XXX *) ;; diff --git a/src/lexer.mll b/src/lexer.mll index 4a8058e5..7821b2b3 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -71,6 +71,7 @@ let kw_table = ("end", (fun _ -> End)); ("enumerate", (fun _ -> Enumerate)); ("else", (fun _ -> Else)); + ("extern", (fun _ -> Extern)); ("false", (fun _ -> False)); ("forall", (fun _ -> Forall)); ("foreach", (fun _ -> Foreach)); diff --git a/src/test/test3.sail b/src/test/test3.sail index 6a88ced9..19a2d5d2 100644 --- a/src/test/test3.sail +++ b/src/test/test3.sail @@ -6,6 +6,9 @@ val ( nat -> nat effect { wmem , rmem } ) MEM val ( nat -> nat effect { wmem , rmem } ) MEM_GPU val ( ( nat * nat ) -> nat effect { wmem , rmem } ) MEM_SIZE +(* extern function *) +val extern ( nat -> nat pure ) add = "add" + function nat main _ = { (* left-hand side function call = memory write *) MEM(0) := 0; @@ -24,4 +27,7 @@ function nat main _ = { (* extra-parentheses are needed here *) MEM_SIZE( (0,1) ) := 4; MEM_SIZE( (0,1) ); + + (* extern calls *) + add(5); } |