Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: 6fbec92e by Jonathan Graveline at 2018-06-14T02:27:39Z Added built in function Ref_make, Ref_read, Ref_write - - - - -

1 changed file:

- src/eval.ml

Changes:

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -703,6 +703,19 @@ let nop_fun loc _ vs = match vs with | [v] -> v | _ -> error loc "Wrong number of argument to nop"

+let ref_make loc depth args_val = match args_val with + | [v] -> Vcommand (fun () -> Vref (ref v)) + | _ -> error loc "Ref.make takes a single value as argument" + +let ref_read loc depth args_val = match args_val with + | [Vref (v)] -> Vcommand (fun () -> !v) + | _ -> error loc "Ref.read takes a single Ref as argument" + +let ref_write loc depth args_val = match args_val with + | [value; Vref (actual)] -> + ((actual := value); Vcommand (fun () -> Vcons ((dloc,"()"),[]))) + | _ -> error loc "Ref.write takes a value and a Ref as argument" + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -731,6 +744,9 @@ let register_builtin_functions () = ("Eq.refl" , arity0_fun, 0); ("Eq.cast" , nop_fun, 1); ("Y" , y_operator, 1); + ("Ref.make" , ref_make, 1); + ("Ref.read" , ref_read, 1); + ("Ref.write" , ref_write, 2); ] let _ = register_builtin_functions ()

View it on GitLab: https://gitlab.com/monnier/typer/commit/6fbec92e9df2cd94e73728a5b4fb92f01a8e...