Stefan pushed to branch master at Stefan / Typer

Commits: b035fe3e by Stefan Monnier at 2017-02-27T21:33:29-05:00 * src/lparse.ml (sform_arrow): New special form

(register_special_forms): Register it under all three names.

* src/pexp.ml (pexp): Remove Parrow.

- - - - -

3 changed files:

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

Changes:

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -378,8 +378,15 @@ let rec lexp_unparse lxp = -> Pcall (pdatacons, [pexp_unparse (lexp_unparse t); Symbol (l, name)]) | Lambda (kind, vdef, ltp, body) -> Plambda(kind, vdef, Some (lexp_unparse ltp), lexp_unparse body) - | Arrow (arg_kind, vdef, ltp1, loc, ltp2) -> - Parrow(arg_kind, vdef, lexp_unparse ltp1, loc, lexp_unparse ltp2) + | Arrow (arg_kind, vdef, ltp1, loc, ltp2) + -> let ut1 = pexp_unparse (lexp_unparse ltp1) in + Pimm (Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_" + | Aimplicit -> "_=>_" + | Aerasable -> "_≡>_"), + [(match vdef with None -> ut1 + | Some v -> Node (Symbol (loc, "_:_"), + [Symbol v; ut1])); + pexp_unparse (lexp_unparse ltp2)]))

| Let (loc, ldecls, body) -> (* (vdef * lexp * ltype) list *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -289,16 +289,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = (lexp_let_decls declss bdy nctx), mkSusp ltp s

- (* ------------------------------------------------------------------ *) - | Parrow (kind, ovar, tp, loc, expr) - -> let ltp = infer_type tp ctx ovar in - let nctx = ectx_extend ctx ovar Variable ltp in - - let lxp = infer_type expr nctx None in - - let v = mkArrow(kind, ovar, ltp, tloc, lxp) in - v, type0 - (* This case can be inferred. *) | Plambda (kind, var, Some ptype, body) -> let ltp = infer_type ptype ctx (Some var) in @@ -1197,6 +1187,21 @@ let sform_hastype ctx loc sargs ot = | _ -> sexp_error loc "##_:_ takes two arguments"; sform_dummy_ret loc

+let sform_arrow kind ctx loc sargs ot = + match sargs with + | [st1; st2] + -> let (v, st1) = match st1 with + | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (Some v, st1) + | _ -> (None, st1) in + let pt1 = pexp_parse st1 in + let pt2 = pexp_parse st2 in + let lt1 = infer_type pt1 ctx v in + let nctx = ectx_extend ctx v Variable lt1 in + let lt2 = infer_type pt2 nctx None in + (mkArrow (kind, v, lt1, loc, lt2), Lazy) + | _ -> 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 @@ -1238,6 +1243,9 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); + ("_->_", sform_arrow Aexplicit); + ("_=>_", sform_arrow Aimplicit); + ("_≡>_", sform_arrow Aerasable); ("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, ... *) | Plet of location * pdecl list * pexp - | Parrow of arg_kind * pvar option * pexp * location * pexp | Plambda of arg_kind * pvar * pexp option * pexp | Pcall of pexp * sexp list (* Curried call. *) (* The symbols are only used so that we can distinguish two @@ -65,7 +64,6 @@ let rec pexp_location e = (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s | Plet (l, _, _) -> l - | Parrow (_, _, _, l, _) -> l | Plambda (_,(l,_), _, _) -> l | Pcall (f, _) -> pexp_location f | Pcase (l, _, _) -> l @@ -74,7 +72,6 @@ let pexp_name e = match e with | Pimm _ -> "Pimm" | Plet (_, _, _) -> "Plet" - | Parrow (_, _, _, _, _) -> "Parrow" | Plambda (_,(_,_), _, _) -> "Plambda" | Pcall (_, _) -> "Pcall" | Pcase (_, _, _) -> "Pcase" @@ -96,17 +93,6 @@ let rec pexp_parse (s : sexp) : pexp = -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) -> pexp_error start "Unrecognized let expression"; Pimm (Symbol (start, "?")) - (* arrow *) - | Node (Symbol (start, (("_->_" | "_=>_" | "_≡>_") as arw)), [t1; t2]) - -> let kind = (match arw with - | "_->_" -> Aexplicit | "_=>_" -> Aimplicit | _ -> Aerasable) in - (match t1 with - | Node (Symbol (_, "_:_"), [Symbol v; t1]) - -> Parrow (kind, Some v, pexp_parse t1, start, pexp_parse t2) - | _ -> Parrow (kind, None, pexp_parse t1, start, pexp_parse t2)) - | Node (Symbol (start, ("_->_" | "_=>_" | "_≡>_")), _) - -> pexp_error start "Unrecognized arrow expression"; - Pimm (Symbol (start, "?")) (* lambda *) | Node (Symbol (start,(("lambda_->_" | "lambda_=>_" | "lambda_≡>_") as arw)), [arg; body]) @@ -267,14 +253,6 @@ and pexp_unparse (e : pexp) : sexp = | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body]) - | Parrow (kind, arg, t1, l, t2) -> - let ut1 = pexp_unparse t1 in - Node (Symbol (l, match kind with Aexplicit -> "_->_" - | Aimplicit -> "_=>_" - | Aerasable -> "_≡>_"), - [(match arg with None -> ut1 - | Some v -> Node (Symbol (l, "_:_"), [Symbol v; ut1])); - pexp_unparse t2]) | Plambda (ak, v, t, body) -> Node (Symbol (dummy_location, match ak with | Aexplicit -> "lambda_->_"

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