Stefan pushed to branch master at Stefan / Typer

Commits: fa5e92ad by Stefan Monnier at 2017-02-27T21:08:16-05:00 * src/lparse.ml (sform_hastype): New function

(register_special_forms): Record it. * src/pexp.ml (pexp): Remove Phastype.

- - - - -

2 changed files:

- src/lparse.ml - src/pexp.ml

Changes:

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -331,10 +331,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = else infer_call ctx ft args

- | Phastype (_, pxp, ptp) - -> let ltp = infer_type ptp ctx None in - (check pxp ltp ctx, ltp) - | (Plambda _ | Pcase _ | Pvar _) -> let t = newMetatype (pexp_location p) in let lxp = check p t ctx in @@ -1189,6 +1185,16 @@ let sform_typecons ctx loc sargs ot = let map_ctor = lexp_parse_inductive ctors nctx in (mkInductive (loc, label, formals, map_ctor), Lazy)

+let sform_hastype ctx loc sargs ot = + match sargs with + | [se; st] -> let pe = pexp_parse se in + let pt = pexp_parse st in + let lt = infer_type pt ctx None in + let le = check pe lt ctx in + (le, Inferred lt) + | _ -> sexp_error loc "##_:_ takes two arguments"; + sform_dummy_ret loc + (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) * But it would be less efficient (such a lambda can't be passed as argument @@ -1229,6 +1235,7 @@ let register_special_forms () = ("Built-in", sform_built_in); ("datacons", sform_datacons); ("typecons", sform_typecons); + ("_:_", sform_hastype); ("Type_", sform_type); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute);

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -40,7 +40,6 @@ type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) | Pvar of pvar - | Phastype of location * pexp * pexp | Plet of location * pdecl list * pexp | Parrow of arg_kind * pvar option * pexp * location * pexp | Plambda of arg_kind * pvar * pexp option * pexp @@ -67,7 +66,6 @@ let rec pexp_location e = (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s | Pvar (l,_) -> l - | Phastype (l,_,_) -> l | Plet (l, _, _) -> l | Parrow (_, _, _, l, _) -> l | Plambda (_,(l,_), _, _) -> l @@ -78,7 +76,6 @@ let pexp_name e = match e with | Pimm _ -> "Pimm" | Pvar (_,_) -> "Pvar" - | Phastype (_,_,_) -> "Phastype" | Plet (_, _, _) -> "Plet" | Parrow (_, _, _, _, _) -> "Parrow" | Plambda (_,(_,_), _, _) -> "Plambda" @@ -99,8 +96,6 @@ let rec pexp_parse (s : sexp) : pexp = | (Block _ | Integer _ | Float _ | String _) -> Pimm s (* | Symbol (l, "Type") -> Psort (l, Type) *) | Symbol s -> Pvar s - | Node (Symbol (start, "_:_"), [e; t]) - -> Phastype (start, pexp_parse e, pexp_parse t) (* let *) | Node (Symbol (start, "let_in_"), [decls; body]) -> Plet (start, pexp_p_decls decls, pexp_parse body) @@ -272,8 +267,6 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s | Pvar v -> Symbol v - | Phastype (l,e,t) - -> Node (Symbol (l, "_:_"), [pexp_unparse e; pexp_unparse t]) | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body])

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