[Git][monnier/typer][master] * src/lparse.ml (_lexp_p_check): Check inferred type with conv_p
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
participants (1)
-
Stefan