Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: 4c682c42 by Jonathan Graveline at 2018-06-28T21:57:57Z New type and value for Array with some functions

- - - - -

6 changed files:

- btl/builtins.typer - btl/pervasive.typer - src/builtin.ml - src/env.ml - src/eval.ml - + tests/array_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -200,6 +200,17 @@ Sexp_dispatch = Built-in "Sexp.dispatch"

Parser_default = Built-in "Parser.default" : Sexp -> List Sexp;

+%%%% Array (without IO, but they could be added easily) + +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; + +% let Typer deduce the value of (a : Type) +Array_empty = Built-in "Array.empty" : (a : Type) ≡> Unit -> Array a; + %%%% Monads

%% Builtin bind

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -416,9 +416,6 @@ test3 = test4; %%%% %%%% Macro : do %%%% -%%%% This file may not be up to date with version -%%%% in pervasive.typer -%%%%

%% %% Here's an example : @@ -521,4 +518,18 @@ do = macro (lambda args -> (IO_return (set-fun (get-decl args))) );

+%%%% +%%%% Array from List +%%%% + +List->Array : (a : Type) ≡> List a -> Array a; +List->Array xs = let + + helper : List a -> Array a -> Array a; + helper xs a = case xs + | cons x xs => helper xs (Array_append x a) + | nil => a; + +in (helper xs (Array_empty ())); + %%% pervasive.typer ends here.

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -169,6 +169,9 @@ let register_builtin_types () = let _ = new_builtin_type "Ref" (mkArrow (Aexplicit, (dloc, None), DB.type0, dloc, DB.type0)) in + let _ = new_builtin_type + "Array" (mkArrow (Aexplicit, (dloc, None), + DB.type0, dloc, DB.type0)) in let _ = new_builtin_type "FileHandle" DB.type0 in let _ = new_builtin_type "Eq" type_eq in ()

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -65,6 +65,7 @@ type value_type = | Vcommand of (unit -> value_type) | Vref of (value_type ref) | Velabctx of DB.elab_context + | Varray of (value_type array)

(* Runtime Environ *) and runtime_env = (vname * (value_type ref)) M.myers @@ -97,6 +98,8 @@ let rec value_equal a b =

| Velabctx (e1), Velabctx (e2) -> (e1 = e2)

+ | Varray (a1), Varray (a2) -> (a1 = a2) + | _ -> false

let rec value_eq_list a b = @@ -129,6 +132,7 @@ let rec value_name v = | Vcommand _ -> "Vcommand" | Vref v -> ("Vref of "^(value_name (!v))) | Velabctx _ -> ("Velabctx") + | Varray _ -> ("Varray")

let rec value_string v = match v with @@ -151,6 +155,12 @@ let rec value_string v = "(" ^ s ^ args ^ ")" | Vref (v) -> ("Ref of "^(value_string (!v))) | Velabctx _ -> ("Velabctx") + | Varray a -> if ( (Array.length a) = 0 ) + then "[]" + else ( let + str = (Array.fold_left + (fun str v -> (str^(value_string v)^";")) "" a) + in ("["^(String.sub str 0 ((String.length str) - 1))^"]") )

let value_print (vtp: value_type) = print_string (value_string vtp)

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -750,6 +750,51 @@ let is_constructor loc depth args_val = match args_val with | _ -> (Vint 0) ) | _ -> 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)) + | _ -> error loc "Array.append takes a value followed by an Array as arguments" + +let array_create loc depth args_val = match args_val with + | [Vint len; v] -> Varray (Array.make len v) + | _ -> 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) + | _ -> 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)) + then + let a = (Array.make 0 v) in + let copy = (Array.map (fun v -> v) a) in + (Array.set copy idx v; Varray copy) + 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) + then + error loc "Array.get index out of bounds" + else + Array.get a idx + | _ -> error loc "Array.get takes an Int followed by an Array as arguments" + +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" + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ @@ -783,8 +828,14 @@ let register_builtin_functions () = ("Ref.write" , ref_write, 2); ("gensym" , gensym, 1); ("Elab.getenv" , getenv, 1); - ("Elab.isbound" , is_bound, 2); + ("Elab.isbound" , is_bound, 2); ("Elab.isconstructor", is_constructor, 2); + ("Array.append" , array_append,2); + ("Array.create" , array_create,2); + ("Array.length" , array_length,1); + ("Array.set" , array_set,3); + ("Array.get" , array_get,2); + ("Array.empty" , array_empty,1); ] let _ = register_builtin_functions ()

===================================== tests/array_test.ml ===================================== --- /dev/null +++ b/tests/array_test.ml @@ -0,0 +1,176 @@ + +open Util +open Utest_lib + +open Sexp +open Lexp + +open Eval (* reset_eval_trace *) + +open Builtin +open Env + +(* default environment *) +let ectx = Elab.default_ectx +let rctx = Elab.default_rctx + + +let _ = (add_test "ARRAY" "Array.create" (fun () -> + let dcode = " + % value_string should also be tested (it is used in interpreter) + + empty = Array_create 0 0; + + a = Array_create 1 1; + + b = Array_create 10 1; + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "empty; a; b;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + (* should I use value_equal here? *) + match ret with + | [Varray empty; Varray a; Varray b] -> + if (empty = (Array.make 0 (Vint 0))) + && (a = (Array.make 1 (Vint 1))) + && (b = (Array.make 10 (Vint 1))) + then success () + else failure () + | _ -> failure ()) +) + +let _ = (add_test "ARRAY" "Array.append" (fun () -> + let dcode = " + empty = Array_create 0 0; + + a = Array_append 1 empty; + + b = Array_create 1 1; + + c = Array_append 2 b; + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "a; c;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Varray a; Varray c] -> + if (a = (Array.make 1 (Vint 1))) + && (c = + (Array.append (Array.make 1 (Vint 1)) (Array.make 1 (Vint 2)))) + then success () + else failure () + | _ -> failure ()) +) + +let _ = (add_test "ARRAY" "Array.length" (fun () -> + let dcode = " + empty = Array_create 0 0; + + a = Array_create 101 0; + + lempty = Array_length empty; + + la = Array_length a; + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "lempty; la;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vint empty; Vint a] -> + if (empty = 0) && (a = 101) + then success () + else failure () + | _ -> failure ()) +) + +let _ = (add_test "ARRAY" "Array.set" (fun () -> + let dcode = " + a = Array_create 101 0; + + b = Array_set 57 1 a; + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "a; b;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Varray a; Varray b] -> let + aa = Array.make 101 (Vint 0) + in if (a = aa) && (Array.set aa 57 (Vint 1); b = aa) + then success () + else failure () + | _ -> failure ()) +) + +let _ = (add_test "ARRAY" "Array.get" (fun () -> + let dcode = " + a = Array_create 101 0; + + b = Array_set 57 1 a; + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "b;" 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)) + then success () + else failure () + | _ -> failure ()) +) + +let _ = (add_test "ARRAY" "Array.empty, List->Array" (fun () -> + let dcode = " + empty1 = Array_empty (); + + empty2 = List->Array nil; + + a = List->Array (cons "a" (cons "b" (cons "c" nil))); + + b = List->Array (cons 1 (cons 2 (cons 3 nil))); + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "empty1; empty2; a; b;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Varray empty1; Varray empty2; Varray a; Varray b] -> + if empty1 = empty2 + && (Array.length empty1) = 0 + && (Array.length empty2) = 0 + && (Array.get a 0) = (Vstring "a") + && (Array.get a 1) = (Vstring "b") + && (Array.get a 2) = (Vstring "c") + && (Array.get b 0) = (Vint 1) + && (Array.get b 1) = (Vint 2) + && (Array.get b 2) = (Vint 3) + then success () + else failure () + | _ -> failure ()) +) + + +(* run all tests *) +let _ = run_all ()

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