Stefan pushed to branch master at Stefan / Typer
Commits: 00232ca1 by Stefan Monnier at 2016-11-11T12:45:13-05:00 Misc minor changes, relating to var names and test names
* src/inverse_subst.ml (counter, impossible): New vars. (mkVar): Give vars a name. (fill.genDummyVar): Use `impossible`.
* src/lparse.ml (_lexp_p_check.unify_with_arrow): Give location and var name in arrow. (lexp_case.check_uniqueness): Use SMap.mem.
* tests/eval_test.ml ("Monads"): Take advantage of type inference.
* tests/inverse_test.ml (generate_tests): Shorten test names.
- - - - -
4 changed files:
- src/inverse_subst.ml - src/lparse.ml - tests/eval_test.ml - tests/inverse_test.ml
Changes:
===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -67,8 +67,12 @@ let transfo (s: lexp S.subst) : substIR option = let rec sizeOf (s: (int * int) list): int = List.length s
(** Returns a dummy variable with the db_index idx -*) -let mkVar (idx: int): lexp = Var((U.dummy_location, ""), idx) + *) +let counter = ref 0 +let mkVar (idx: int) : lexp = + counter := !counter + 1; + Var((U.dummy_location, "<anon" ^ string_of_int idx ^ ">"), idx) +let impossible = Imm Epsilon
(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -82,7 +86,7 @@ let mkVar (idx: int): lexp = Var((U.dummy_location, ""), idx) let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = let rec genDummyVar (beg_: int) (end_: int) (l: lexp S.subst): lexp S.subst = (* Create the filler variables *) if beg_ < end_ - then S.cons (mkVar (nbVar + 1)) (genDummyVar (beg_ + 1) end_ l) + then S.cons impossible (genDummyVar (beg_ + 1) end_ l) else l in let fill_before (l: (int * int) list) (s: lexp S.subst) (nbVar: int): lexp S.subst option = (* Fill if the first var is not 0 *)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -385,7 +385,8 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = let arg = match aty with | None -> newMetatype () | Some laty -> laty in - let arrow = mkArrow (kind, None, arg, Util.dummy_location, body) in + let l, _ = var in + let arrow = mkArrow (kind, Some var, arg, l, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) subst with | Some subst -> global_substitution := subst; arg, body | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp @@ -429,7 +430,6 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = | Plambda (kind, var, def_arg_type, body) -> infer_lambda_body kind var def_arg_type body subst
- (* This is mostly for the case where no branches are provided *) | Pcase (loc, target, branches) -> lexp_case t (loc, target, branches) ctx trace
@@ -467,8 +467,7 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = ^ " is a duplicate. It will override previous pattern.") in
let check_uniqueness pat name map = - try let _ = SMap.find name map in uniqueness_warn pat - with e -> () in + if SMap.mem name map then uniqueness_warn pat in
(* get target and its type *) let tlxp, tltp = lexp_infer target ctx in @@ -764,7 +763,9 @@ and lexp_expand_macro_ macro_funct sargs ctx trace expand_fun =
and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = try (* Lookup macro declaration *) - let idx = senv_lookup mname ctx in + let idx = senv_lookup mname ctx in + (* FIXME: We should only check that `ltp` is Macro, and not look + * at `lxp` here (just like we do for expression macros). *) let ltp = env_lookup_type ctx ((loc, mname), idx) in let lxp = env_lookup_expr ctx ((loc, mname), idx) in
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -302,8 +302,7 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> let _ = (add_test "EVAL" "Monads" (fun () ->
let dcode = " - c = bind (a := FileHandle) (b := Unit) - (open "./_build/w_file.txt" "w") + c = bind (open "./_build/w_file.txt" "w") (lambda f -> write f "Hello2"); " in
===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -112,8 +112,11 @@ let generate_tests (name: string) in List.map (fun (sub, res) -> idx := !idx + 1; add_test name - ((U.padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) - (fun () -> if res then success () else failure ())) + ((U.padding_left (string_of_int (!idx)) 2 '0') + (* FIXME: It's nice to see the actual tests when they fail + * but it's too verbose otherwise. *) + (* ^ " - " ^ sub *)) + (fun () -> if res then success () else failure ())) (test input_gen fmt tester)
@@ -121,7 +124,8 @@ let get_dim lst = let max i s = max i (String.length s) in List.fold_left - (fun (acs, acs', acc) (s, s', comp) -> ((max acs s), (max acs' s'), (max acc comp))) + (fun (acs, acs', acc) (s, s', comp) + -> ((max acs s), (max acs' s'), (max acc comp))) (0,0,0) lst
View it on GitLab: https://gitlab.com/monnier/typer/commit/00232ca10ce25b30d3b887889f1352d0aa44...