Stefan pushed to branch unification at Stefan / Typer

Commits: 89c67665 by Stefan Monnier at 2016-10-27T21:03:13-04:00 Fix some of the tests

- - - - -

3 changed files:

- src/lparse.ml - tests/lparse_test.ml - tests/unify_test.ml

Changes:

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -244,7 +244,8 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = lxp, ltp (* Return Macro[22] *)

with Not_found -> - (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); + (print_lexp_ctx (ectx_to_lctx ctx); + pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); (* Error recovery. The -1 index will raise an error later on *) (make_var name (-1) loc), dltype))

===================================== tests/lparse_test.ml ===================================== --- a/tests/lparse_test.ml +++ b/tests/lparse_test.ml @@ -30,7 +30,7 @@ let generate_tests (name: string) (test input_gen fmt tester)

(* let input = "y = lambda x -> x + 1;" *) -let input = "id = lambda (α : Type) ≡> lambda x : α -> x; +let input = "id = lambda (α : Type) ≡> lambda (x : α) -> x; res = id 3;"

let generate_lexp_from_str str =

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -58,7 +58,7 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = ) str_lst

(* Inputs for the test *) -let str_induct = "Nat = inductive_ (dNat) (zero) (succ Nat)" +let str_induct = "Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat)" let str_int_3 = "i = 3" let str_int_4 = "i = 4" let str_case = "i = case 0

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