Setepenre pushed to branch master at Stefan / Typer

Commits: 33279ef6 by Pierre Delaunay at 2016-03-30T09:53:57-04:00 Allow restricted type aliasing during type inference

In 'Nat = inductive_' We want to use the alias 'Nat' instead of the full declaration during type inference. It is restricted aliasing because only inductive type can be aliased that way.

Changes to be committed: * GNUmakefile: tests don't run when using make all * src/eval.ml: Call eval check for constructor before evaluating (Test - Nat Plus Work) * src/lparse.ml: - Type inference: Allow restricted type aliasing - Type inference: Call now allow partial application - Type inference: Cons are typed as function * src/lexer.ml: added (lex_str) and (sexp_parse_str) * src/pexp.ml: removed useless declaration/include * tests/eval_test.ml: - Mutually rec decl tests - Partial Application test

new file: * tests/sexp_test.ml: test _*_ and _+_ precedence which both seems to be buggy

- - - - -

13 changed files:

- GNUmakefile - src/REPL.ml - src/debug.ml - src/eval.ml - src/lexer.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - src/sexp.ml - tests/eval_test.ml - tests/lexp_test.ml - + tests/sexp_test.ml - tests/utest_main.ml

Changes:

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -6,7 +6,7 @@ TEST_FILES := $(wildcard ./tests/*_test.ml)

CFLAG = -cflag -rectypes -build-dir _build

-all: ityper typer debug tests +all: ityper typer debug tests-build

typer: # ============================ @@ -40,10 +40,7 @@ tests-build: @mv _build/tests/utest_main.native _build/tests/utests

tests-run: - # ============================ - # Run tests - # ============================ - @./_build/tests/utests --verbose= 3 + @./_build/tests/utests --verbose= 2

tests: tests-build tests-run

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -36,6 +36,7 @@ this program. If not, see http://www.gnu.org/licenses/. *) * * -------------------------------------------------------------------------- *)

+(* FIXME: Prevent ityper from crashing when an error is thrown *)

open Debug open Prelexer

===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -134,7 +134,7 @@ let debug_pexp_print ptop = | Pinductive (_, _, _) -> print_info "Pinductive " l ptop | Pcons (_,_) -> print_info "Pcons " l ptop | Pcase (_, _, _) -> print_info "Pcase " l ptop - | _ -> print_info "Not Impl " l ptop + (*| _ -> print_info "Not Impl " l ptop *) ;;

let debug_pexp_decls decls =

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -31,6 +31,7 @@ * --------------------------------------------------------------------------- *)

open Util +open Pexp (* Arg_kind *) open Lexp open Lparse open Myers @@ -197,6 +198,10 @@ let rec _eval lxp ctx i: (value_type) = let nctx = build_ctx decls ctx i in _eval inst (local_ctx nctx) (i + 1)

+ (* Built-in Function * ) + | Call(Builtin(v, name, ltp), args) -> + let nctx = build_arg_list args ctx i in *) + (* Function call *) | Call (lname, args) -> ( (* create a clean environment *) @@ -227,7 +232,7 @@ let rec _eval lxp ctx i: (value_type) = Imm(Integer(dloc, v))

(* This is a named function call *) - | Var((_, name), idx) -> + | Var((_, name), idx) -> ( (* get function's body from current context *) let body = get_rte_variable (Some name) idx ctx in

@@ -235,12 +240,18 @@ let rec _eval lxp ctx i: (value_type) = let arg_val = List.map (fun (k, e) -> _eval e ctx (i + 1)) args in

- (* Add args inside our clean context *) - let clean_ctx = - List.fold_left (fun c v -> add_rte_variable None v c) - clean_ctx arg_val in - - _eval body clean_ctx (i + 1) + match body with + (* If 'cons', build it back with evaluated args *) + | Cons _ -> + Call(lname, (List.map (fun g -> + (Aexplicit, g)) arg_val)) + | _ -> + (* Add args inside our clean context *) + let clean_ctx = + List.fold_left (fun c v -> add_rte_variable None v c) + clean_ctx arg_val in + + _eval body clean_ctx (i + 1))

(* TODO Everything else *) (* Which includes a call to a lambda *)

===================================== src/lexer.ml ===================================== --- a/src/lexer.ml +++ b/src/lexer.ml @@ -23,6 +23,7 @@ this program. If not, see http://www.gnu.org/licenses/. *) open Util open Prelexer open Sexp +open Grammar

(*************** The Lexer phase *********************)

@@ -42,7 +43,7 @@ let digit_p char = in Char.code '0' <= code && code <= Char.code '9'

type num_part = | NPint | NPfrac | NPexp - + let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos (* The returned Sexp may not be a Node. *) : sexp * pretoken list * bytepos * charpos = @@ -118,15 +119,19 @@ let lex tenv (pts : pretoken list) : sexp list = in gettokens pts bpos cpos (tok :: acc) in gettokens pts 0 0 [] ;; - -let lex_string (str: string) tenv = + +let _lex_str (str: string) tenv = let pretoks = prelex_string str in lex tenv pretoks ;;

-let node_parse_string (str: string) tenv grm limit = - let pretoks = prelex_string str in - let toks = lex tenv pretoks in +let lex_str str = _lex_str str default_stt + +let _sexp_parse_str (str: string) tenv grm limit = + let toks = _lex_str str tenv in sexp_parse_all_to_list grm toks limit ;; - + +let sexp_parse_str str = + _sexp_parse_str str default_stt default_grammar (Some ";") +

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -21,7 +21,6 @@ You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

open Util -open Lexer open Sexp open Pexp open Myers @@ -274,6 +273,8 @@ let rec lexp_location e = | Inductive (l,_,_,_) -> l | Cons (_,(l,_)) -> l | Case (l,_,_,_,_) -> l + | UnknownType l -> l + | Shift (_, l) -> lexp_location l (* | Susp (_, e) -> lexp_location e * | Metavar ((l,_),_,_) -> l *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -87,9 +87,7 @@ let default_lctx () = (* populate ctx *) List.fold_left (fun ctx (name, lxp) -> - let var = (dloc, name) in - let ctx = senv_add_var var ctx in - env_add_var_info (0, var, None, lxp) ctx) + env_extend ctx (dloc, name) None lxp) lctx lexp_builtins ;; @@ -477,21 +475,70 @@ and lexp_p_infer (p : pexp) (env : lexp_context): lexp * ltype = let tloc = pexp_location p in let lxp = lexp_parse p env in

- let rec get_return_type lxp = + let consume_args args lxp ctx = + let arg_n = List.length args in + let rec _implt args lxp i = match args, lxp with + (* No args left, return the remaining type *) + | [], _ -> lxp + | _, UnknownType _ -> lxp + + (* Basic case consume an arg and an arrow *) + | hd::tl, Arrow(_, _, ltp, _, ret_type) -> + (* FIXME: Check hd and ltp are of the same type *) + _implt tl ret_type (i + 1) + + (* We still have args to consume but type is not an arrow *) + | (_, hd)::tl, tp -> + lexp_error tloc ("Number of Arg mismatch. Expected: " ^ + (string_of_int i) ^ " arg(s). Got " ^ (string_of_int arg_n)); + tp in + _implt args lxp 0 in + + let is_type lxp = match lxp with - | Arrow(_, _, _, _, ret_type) -> (get_return_type ret_type) - | _ -> lxp in + | Inductive _ -> true + | _ -> false in

let rec get_type lxp ctx = match lxp with (* Leafs *) (* ------------ *) - | Var vrf -> env_lookup_type ctx vrf - | Cons (vrf, _) -> env_lookup_type ctx vrf + + (* Why don't we always return tp ? We want to be able to use *) + (* type aliases Nat = inductive_ *) + (* We want the type to be inferred as Nat not _inductive... *) + (* But sometimes we need tp to be return *) + | Var vrf -> let tp = env_lookup_type ctx vrf in + if (is_type tp) then lxp else tp + + (* I am not sure we should consider a constructor as a function *) + (* Another way to do what is done here is to handle cons in Call *) + | Cons (vrf, (_, n)) ->( + let rec build_arrow_type args acc = + match args with + | [] -> acc + | (kind, var, ltp)::tl -> + build_arrow_type tl (Arrow(kind, var, ltp, dloc, acc)) + in + + match env_lookup_type ctx vrf with + | Inductive(_, _, _, ctor_map) -> ( + try match SMap.find n ctor_map with + (* No Args *) + | [] -> Var(vrf) (* return its inductive type *) + (* Return a Constructor function *) + | args -> build_arrow_type (List.rev args) (Var(vrf)) + + with Not_found -> + (lexp_error tloc ("Constructor " ^ n ^ + " does not exist"); dltype)) + | _ -> (lexp_error tloc "Inductive type was expected"; dltype)) + | Imm sxp -> (match sxp with - (* FIXME use the ones that are already in the ctx *) - | Integer _ -> type_int - | Float _ -> type_float + | Integer _ -> let idx = senv_lookup "Int" ctx in + env_lookup_type ctx ((dloc, "Int"), idx) + | Float _ -> let idx = senv_lookup "Float" ctx in + env_lookup_type ctx ((dloc, "Float"), idx) | _ -> lexp_error tloc "Could not infer type"; dltype)

(* Types by definition *) @@ -503,17 +550,29 @@ and lexp_p_infer (p : pexp) (env : lexp_context): lexp * ltype = (* Nodes *) (* ------------ *) | Let (_, _, body) -> (get_type body ctx) - | Call(f, _) -> - (* FIXME: check arg and f type are compatible *) - (* FIXME: call cannot be partial *) - (get_return_type (get_type f ctx)) - - (* we need to check that all branches return the same type *) - | Case (_, _, _, branches, dflt) ->( - (* FIXME *) - match dflt with - | None -> lexp_error tloc "Could not infer type"; dltype - | Some expr -> (get_type expr ctx)) + | Call(f, args) -> + (consume_args args (get_type f ctx) ctx) + + + | Case (_, _, _, branches, dflt) -> + (* we need to check that all branches return the same type *) + let lst = SMap.bindings branches in + let types = List.map + (fun (_, (_, args, body)) -> + (* FIXME: We need to lookup arg type *) + let nctx = List.fold_left (fun c v -> + match v with + | None -> c + | Some (_, arg) -> env_extend ctx arg None dltype) + ctx args in + get_type body nctx) lst in + + let types = match dflt with + | None -> types + | Some expr -> (get_type expr ctx)::types in + let tp = List.hd types in + (* FIXME: do type checking *) + tp

| Lambda (kind, vdef, ltp, lxp) -> let nctx = env_extend ctx vdef (Some ltp) lxp in @@ -534,6 +593,7 @@ and lexp_p_check (p : pexp) (t : ltype) (env : lexp_context): lexp = -> let (e, inferred_t) = lexp_p_infer p env in (* FIXME: check that inferred_t = t! *) e + (* * Printing * --------------------- *) @@ -643,7 +703,6 @@ and lexp_print_ctors opt ctors = ctors

and lexp_print_type opt ltp = - let (_, _, prtp) = opt in match ltp with | Inductive(_, (_, l), _, _) -> print_string l; | _ -> lexp_print_adv opt ltp @@ -712,7 +771,6 @@ and print_lexp_trace () = and lexp_print_var_info ctx = let ((m, _), env, _) = ctx in let n = Myers.length env in - let sync_offset = m - n in

for i = 0 to n - 1 do ( let (_, (_, name), exp, tp) = Myers.nth i env in

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -21,9 +21,8 @@ You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

open Util -open Sexp +open Sexp (* Symbol *) open Lexer -open Prelexer open Grammar

let pexp_error = msg_error "PEXP" @@ -358,13 +357,6 @@ let pexp_parse_all (nodes: sexp list) = List.map pexp_parse nodes ;;

-let pexp_parse_string (str: string) tenv grm limit = - let pretoks = prelex_string str in - let toks = lex tenv pretoks in - let sxps = sexp_parse_all_to_list grm toks limit in - pexp_parse_all sxps -;; - let pexp_decls_all (nodes: sexp list): ((pvar * pexp * bool) list) = let rec loop nodes acc = match nodes with @@ -382,9 +374,7 @@ let pexp_decls_all (nodes: sexp list): ((pvar * pexp * bool) list) = (* Lexp helper *) let _pexp_expr_str (str: string) (tenv: bool array) (grm: grammar) (limit: string option) = - let pretoks = prelex_string str in - let toks = lex tenv pretoks in - let sxps = sexp_parse_all_to_list grm toks limit in + let sxps = _sexp_parse_str str tenv grm limit in pexp_parse_all sxps ;;

@@ -393,11 +383,8 @@ let pexp_expr_str str = _pexp_expr_str str default_stt default_grammar (Some ";") ;;

- let _pexp_decl_str (str: string) tenv grm limit = - let pretoks = prelex_string str in - let toks = lex tenv pretoks in - let sxps = sexp_parse_all_to_list grm toks limit in + let sxps = _sexp_parse_str str tenv grm limit in pexp_decls_all sxps ;;

===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -231,3 +231,7 @@ let sexp_parse_all_to_list grm tokens limit = sexp_parse_impl grm rest limit (sxp :: acc) in sexp_parse_impl grm tokens limit [] ;; + + + +

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -90,7 +90,7 @@ let _ = (add_test "EVAL" "Nested Lambda" (fun () -> * i.e the context should not grow *) let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> let code = " - infinity = lambda beyond -> (infinity beyond);" in + infinity = lambda (beyond : Int) -> (infinity beyond);" in

let rctx, lctx = eval_decl_str code lctx rctx in

@@ -109,7 +109,7 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> (* Cases + Inductive types * ------------------------ *)

-let _ = (add_test "EVAL" "Case" (fun () -> +let _ = (add_test "EVAL" "Inductive::Case" (fun () -> (* Inductive type declaration + Noisy declarations *) let code = " i = 90;\n @@ -146,9 +146,8 @@ let _ = (add_test "EVAL" "Case" (fun () -> success () else failure () - | _ -> failure ()) -) -;; + | _ -> failure () +));;

(* Those wil be used multiple times *) let nat_decl = " @@ -169,7 +168,7 @@ let bool_decl = " ;;

-let _ = (add_test "EVAL" "Recursive Call" (fun () -> +let _ = (add_test "EVAL" "Inductive::Recursive Call" (fun () ->

let code = nat_decl ^ " one = (succ zero); @@ -196,7 +195,9 @@ let _ = (add_test "EVAL" "Recursive Call" (fun () -> ) ;;

-let _ = (add_test "EVAL" "Nat Plus" (fun () -> +let _ = (add_test "EVAL" "Inductive::Nat Plus" (fun () -> + + _eval_max_recursion_depth := 80000;

let code = nat_decl ^ " one = (succ zero); @@ -213,7 +214,7 @@ let _ = (add_test "EVAL" "Nat Plus" (fun () -> let rcode = " (tonum (plus zero two)); (tonum (plus two zero)); - 5;"in + (tonum (plus two one));"in

(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in @@ -222,14 +223,76 @@ let _ = (add_test "EVAL" "Nat Plus" (fun () -> | [a; b; c] -> let t1 = expect_equal_int (get_int a) 2 in let t2 = expect_equal_int (get_int b) 2 in - let t3 = expect_equal_int (get_int c) 5 in + let t3 = expect_equal_int (get_int c) 3 in if t1 = 0 && t2 = 0 && t3 = 0 then success () else failure () - | _ -> failure ()) -) -;; + | _ -> failure () +));; + +(* TODO *) +let _ = (add_test "EVAL" "Mutually Recursive Definition" (fun () -> + + let dcode = nat_decl ^ " + one = (succ zero); + two = (succ one); + three = (succ three); + + odd : Int -> Int; + even : Int -> Int; + odd = lambda n -> case n + | zero => 0 + | succ y => (even y); + + even = lambda n -> case n + | zero => 1 + | succ y => (odd y);" in + + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let rcode = "(odd one); (even one); (odd two); (even two);" in + + (* Eval defined lambda *) + let ret = eval_expr_str rcode lctx rctx in + (* Expect a 3 results *) + match ret with + | [a; b; c; d] -> + let t1 = expect_equal_int (get_int a) 1 in + let t2 = expect_equal_int (get_int b) 0 in + let t3 = expect_equal_int (get_int c) 1 in + let t4 = expect_equal_int (get_int d) 0 in + if t1 = 0 && t2 = 0 && t3 = 0 && t4 = 0 then + success () + else + failure () + | _ -> failure () +));; + +let _ = (add_test "EVAL" "Partial Application" (fun () -> + + let dcode = " + mult = lambda x y -> (x * y); + twice = (mult 2);" in + + let rctx, lctx = eval_decl_str dcode lctx rctx in + + let rcode = "(twice 1); (twice 2); (twice 3);" in + + (* Eval defined lambda *) + let ret = eval_expr_str rcode lctx rctx in + (* Expect a 3 results *) + match ret with + | [a; b; c] -> + let t1 = expect_equal_int (get_int a) 2 in + let t2 = expect_equal_int (get_int b) 4 in + let t3 = expect_equal_int (get_int c) 6 in + if t1 = 0 && t2 = 0 && t3 = 0 then + success () + else + failure () + | _ -> failure () +));;

(* List = inductive (dList (a : Type)) (nil) (cons a (List a));

===================================== tests/lexp_test.ml ===================================== --- a/tests/lexp_test.ml +++ b/tests/lexp_test.ml @@ -5,10 +5,7 @@ open Pexp open Utest_lib

(* default environment *) -let lctx = make_lexp_context -let lctx = add_def "_+_" lctx -let lctx = add_def "_*_" lctx - +let lctx = default_lctx ()

let _ = (add_test "LEXP" "Built-in type Inference" (fun () ->

===================================== tests/sexp_test.ml ===================================== --- /dev/null +++ b/tests/sexp_test.ml @@ -0,0 +1,57 @@ +open Sexp +open Lexer +open Utest_lib + + +(* _+_ precedence is too low ? + * + * a = lambda x -> x + x + x + * is parsed to + * a = (_+_ (_+_ (lambda_->_ x x) x) x) <=> a = (lambda x -> x) + x + x + * instead of + * a = (lambda_->_ x (_+_ (_+_ x x) x)) *) +let _ = (add_test "SEXP" "lambda x -> x + x" (fun () -> + + let dcode = "lambda x -> x + x;" in + + let ret = sexp_parse_str dcode in + match ret with + | [n] ->(match n with + | Node(Symbol(_, "lambda"), [arg; body]) -> success () + (* arg = Symbol(_, "x") *) + (* body = Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")]) *) + | _ -> failure ()) + | _ -> failure () +));; + + +(* _*_ is not a binary operator + * + * b = lambda x -> (x * x * x); + * is parsed to + * b = (lambda_->_ x (_*_ x x x)) + * instead of + * b = (lambda_->_ x (_*_ (_*_ x x) x)) *) +let _ = (add_test "SEXP" "x * x * x" (fun () -> + + let dcode = "x * x * x;" in + + let ret = sexp_parse_str dcode in + match ret with + | [n] ->(match n with + | Node(Symbol(_, "_*_"), + [Node(Symbol(_, "_*_"), [Symbol(_, "x"); Symbol(_, "x")]); Symbol(_, "x")]) + -> success () + + | Node(Symbol(_, "_*_"), + [Symbol(_, "x"); Node(Symbol(_, "_*_"), [Symbol(_, "x")]); Symbol(_, "x")]) + -> success () + + | _ -> failure ()) + | _ -> failure () + +));; + +(* run all tests *) +run_all () +;;

===================================== tests/utest_main.ml ===================================== --- a/tests/utest_main.ml +++ b/tests/utest_main.ml @@ -119,7 +119,9 @@ let main () = failed_test := !failed_test + 1) else (if verbose 1 then print_file_name (!tests_n) files_n file true); - ) + ); + + (if verbose 2 then print_newline ());

) files;

@@ -127,7 +129,7 @@ let main () = print_string " Test Ran : "; print_int !tests_n; print_string "\n Test Failed : "; print_int !failed_test; print_string "\n Test Passed : "; print_int (!tests_n - !failed_test); - print_endline ""; + print_endline "\n"; ;;

main ();

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