Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: af4ba9f6 by Jonathan Graveline at 2018-06-29T20:41:33Z Correction of Array functions and simplification

- - - - -

3 changed files:

- btl/builtins.typer - src/eval.ml - tests/array_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -206,7 +206,7 @@ Array_append = Built-in "Array.append" : (a : Type) ≡> a -> Array a -> Array a Array_create = Built-in "Array.create" : (a : Type) ≡> Int -> a -> Array a; Array_length = Built-in "Array.length" : (a : Type) ≡> Array a -> Int; Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a; -Array_get = Built-in "Array.get" : (a : Type) ≡> Int -> Array a -> a; +Array_get = Built-in "Array.get" : (a : Type) ≡> a -> Int -> Array a -> a;

% let Typer deduce the value of (a : Type) Array_empty = Built-in "Array.empty" : (a : Type) ≡> Unit -> Array a;

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -751,11 +751,8 @@ let is_constructor loc depth args_val = match args_val with | _ -> error loc "Elab.isconstructor takes an Elab_Context and a String as arguments"

let array_append loc depth args_val = match args_val with - | [v; Varray a] -> if (a = (Array.make 0 Vundefined)) then - let a = (Array.make 0 v) in - Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v)) - else - Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v)) + | [v; Varray a] -> + Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v)) | _ -> error loc "Array.append takes a value followed by an Array as arguments"

let array_create loc depth args_val = match args_val with @@ -763,34 +760,31 @@ let array_create loc depth args_val = match args_val with | _ -> error loc "Array.make takes an Int and a value and as arguemnts"

let array_length loc depth args_val = match args_val with - | [Varray a] -> if (a = (Array.make 0 Vundefined)) - then - (Vint 0) - else - Vint (Array.length a) + | [Varray a] -> Vint (Array.length a) | _ -> error loc "Array.length takes an Array as argument"

let array_set loc depth args_val = match args_val with - | [Vint idx; v; Varray a] -> if (a = (Array.make 0 Vundefined)) + | [Vint idx; v; Varray a] -> if (idx > (Array.length a) || idx < 0) then - let a = (Array.make 0 v) in - let copy = (Array.map (fun v -> v) a) in - (Array.set copy idx v; Varray copy) + (warning loc "Array.set index out of bounds (array unchanged)"; + (Varray a)) else let copy = (Array.map (fun v -> v) a) in (Array.set copy idx v; Varray copy) | _ -> error loc "Array.set takes an Int, a value and an Array as arguments"

let array_get loc depth args_val = match args_val with - | [Vint idx; Varray a] -> if (a = (Array.make 0 Vundefined)) - || (idx > (Array.length a)) - || (idx < 0) + | [dflt; Vint idx; Varray a] -> if (idx > (Array.length a)) || (idx < 0) then - error loc "Array.get index out of bounds" + dflt else Array.get a idx - | _ -> error loc "Array.get takes an Int followed by an Array as arguments" + | _ -> error loc "Array.get takes a default value, an Int and an Array as arguments" +

+(* Vundefined is used in array_empty because we have no default value + ("array_create 0 0" has a default value v (Vint 0)). +*) let array_empty loc depth args_val = match args_val with | [_] -> Varray (Array.make 0 Vundefined) | _ -> error loc "Array.empty takes a Unit as single argument" @@ -834,7 +828,7 @@ let register_builtin_functions () = ("Array.create" , array_create,2); ("Array.length" , array_length,1); ("Array.set" , array_set,3); - ("Array.get" , array_get,2); + ("Array.get" , array_get,3); ("Array.empty" , array_empty,1); ] let _ = register_builtin_functions ()

===================================== tests/array_test.ml ===================================== --- a/tests/array_test.ml +++ b/tests/array_test.ml @@ -100,18 +100,21 @@ let _ = (add_test "ARRAY" "Array.set" (fun () -> a = Array_create 101 0;

b = Array_set 57 1 a; + + % should throw a warning (out of bounds) + c = Array_set 102 1 a; " in

let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in

- let ecode = "a; b;" in + let ecode = "a; b; c;" in

let ret = Elab.eval_expr_str ecode ectx rctx in

match ret with - | [Varray a; Varray b] -> let + | [Varray a; Varray b; Varray c] -> let aa = Array.make 101 (Vint 0) - in if (a = aa) && (Array.set aa 57 (Vint 1); b = aa) + in if (a = aa) && (Array.set aa 57 (Vint 1); b = aa) && (a = c) then success () else failure () | _ -> failure ()) @@ -121,18 +124,24 @@ let _ = (add_test "ARRAY" "Array.get" (fun () -> let dcode = " a = Array_create 101 0;

- b = Array_set 57 1 a; + aa = Array_set 57 1 a; + + b = Array_get (-1) 57 aa; + + c = Array_get (-1) 102 aa; + + d = Array_get (-1) 0 aa; " in

let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in

- let ecode = "b;" in + let ecode = "b; c; d;" in

let ret = Elab.eval_expr_str ecode ectx rctx in

match ret with - | [Varray b] -> - if ((Array.get b 57) = (Vint 1)) && ((Array.get b 58) = (Vint 0)) + | [Vint b; Vint c; Vint d] -> + if (b = 1 && c = (-1) && d = 0) then success () else failure () | _ -> failure ())

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