Stefan pushed to branch master at Stefan / Typer
Commits: 36b070f5 by Stefan Monnier at 2016-11-06T11:18:40-05:00 * src/lparse.ml (_lexp_p_check): Check inferred type with conv_p
* btl/types.typer (head): Make it total. (tail): Fix up minor type error.
* src/lexp.ml (lexp_unparse): Print `Sort` with more details.
* src/lparse.ml (_lexp_p_check): Check inferred type with conv_p.
* tests/eval_test.ml (Lists): Adjust to new `head` type. (Monads): Fix type arguments.
- - - - -
4 changed files:
- btl/types.typer - src/lexp.ml - src/lparse.ml - tests/eval_test.ml
Changes:
===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -78,18 +78,23 @@ length = lambda a ≡> | nil => 0 | cons hd tl => (1 + (length (a := a) tl));
-head : (a : Type) ≡> List a -> a; +% ML's typical `head` function is not total, so can't be defined +% as-is in Typer. There are several workarounds: +% - Provide a default value : (a : Type) ≡> List a -> a -> a; +% - Disallow problem case : (a : Type) ≡> (l : List a) -> (l != nil) -> a; +% - Return an Option/Error. +head : (a : Type) ≡> List a -> Option a; head = lambda a ≡> lambda xs -> case xs - | nil => nil - | cons hd tl => hd; + | nil => None (a := a) + | cons hd tl => Some (a := a) hd;
tail : (a : Type) ≡> List a -> List a; tail = lambda a ≡> lambda xs -> case xs - | nil => nil + | nil => nil (a := a) | cons hd tl => tl;
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -399,11 +399,15 @@ let rec lexp_unparse lxp = | None -> pbranch in Pcase (loc, lexp_unparse target, pbranch)
- (* - | SortLevel of sort_level - | Sort of U.location * sort *) - - | _ as e -> Pimm (Symbol(lexp_location e, "Type")) + (* FIXME: The cases below are all broken! *) + + | SortLevel (SLz) -> Pimm (Integer (U.dummy_location, 0)) + | SortLevel (SLsucc sl) -> Pcall (Pimm (Symbol (U.dummy_location, "<S>")), + [pexp_unparse (lexp_unparse sl)]) + | Sort (l, StypeOmega) -> Pimm (Symbol (l, "<SortOmega>")) + | Sort (l, StypeLevel) -> Pimm (Symbol (l, "<SortLevel>")) + | Sort (l, Stype sl) -> Pcall (Pimm (Symbol (l, "<Type>")), + [pexp_unparse (lexp_unparse sl)])
let lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) (*
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -385,7 +385,13 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = (* FIXME: Handle *macro* pcalls here! *) (* | Pcall (fname, _args) -> *)
- | _ -> let (e, inferred_t) = lexp_infer p ctx in e + | _ -> let (e, inferred_t) = lexp_infer p ctx in + if not (OL.conv_p (ectx_to_lctx ctx) inferred_t t) then + lexp_error (pexp_location p) e + ("Type mismatch! Context expected `" + ^ lexp_string t ^ "` but expression has type `" + ^ lexp_string inferred_t ^ "`\n"); + e
(* Lexp.case can sometimes be inferred, but we prefer to always check. *) and lexp_case rtype (loc, target, ppatterns) ctx i =
===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -254,7 +254,7 @@ let _ = test_eval_eqv_named head (a := Int) my_list; head (a := Int) (tail (a := Int) my_list)"
- "4; 1; 2" + "4; Some (a := Int) 1; Some (a := Int) 2"
(* * Special forms @@ -299,14 +299,14 @@ let _ = (add_test "EVAL" "Infinite Recursion failure" (fun () -> let _ = (add_test "EVAL" "Monads" (fun () ->
let dcode = " - c = bind (a := Type) (b := Type) (open "./_build/w_file.txt" "w") - (lambda (f : FileHandle) -> - write f "Hello2"); + c = bind (a := FileHandle) (b := Unit) + (open "./_build/w_file.txt" "w") + (lambda f -> write f "Hello2"); " in
let rctx, lctx = eval_decl_str dcode lctx rctx in
- let rcode = "run-io (a := Type) (b := Unit) c Unit" in + let rcode = "run-io (a := Unit) (b := Int) c 2" in
(* Eval defined lambda *) let ret = eval_expr_str rcode lctx rctx in
View it on GitLab: https://gitlab.com/monnier/typer/commit/36b070f5599567db10fee0374efdec3cca19...
Afficher les réponses par date