Stefan pushed to branch master at Stefan / Typer

Commits: 5aff0bb4 by Stefan Monnier at 2017-02-28T01:11:29-05:00 * src/pexp.ml (pexp): Remove Pcall

Use `Pimm (Node ..)` instead.

- - - - -

3 changed files:

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

Changes:

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -364,8 +364,8 @@ let lexp_name e = | Sort _ -> "Sort" | SortLevel _ -> "SortLevel"

-let pdatacons = Pimm (Symbol (U.dummy_location, "##datacons")) -let ptypecons = Pimm (Symbol (U.dummy_location, "##typecons")) +let sdatacons = Symbol (U.dummy_location, "##datacons") +let stypecons = Symbol (U.dummy_location, "##typecons")

(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = @@ -375,7 +375,8 @@ let rec lexp_unparse lxp = | Builtin ((l,name), _, _) -> Pimm (Symbol (l, "##" ^ name)) | Var ((loc, name), _) -> Pimm (Symbol (loc, name)) | Cons (t, (l, name)) - -> Pcall (pdatacons, [pexp_unparse (lexp_unparse t); Symbol (l, name)]) + -> Pimm (Node (sdatacons, + [pexp_unparse (lexp_unparse t); Symbol (l, name)])) | Lambda (kind, vdef, ltp, body) -> let l = lexp_location lxp in let st = pexp_unparse (lexp_unparse ltp) in @@ -407,7 +408,7 @@ let rec lexp_unparse lxp = | Call(lxp, largs) -> (* (arg_kind * lexp) list *) let pargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in let sargs = List.map (fun elem -> pexp_unparse elem) pargs in - Pcall(lexp_unparse lxp, sargs) + Pimm (Node (pexp_unparse (lexp_unparse lxp), sargs))

| Inductive(loc, label, lfargs, ctors) -> (* (arg_kind * vdef * ltype) list *) @@ -424,12 +425,12 @@ let rec lexp_unparse lxp = | None -> (kind, None, lexp_unparse ltp)) largs in ((loc, str), pargs) ) (SMap.bindings ctors) in - Pcall (ptypecons, - Node (Symbol label, List.map pexp_u_formal_arg pfargs) - :: List.map (fun ((l,name) as s, types) - -> Node (Symbol s, - List.map pexp_u_ind_arg types)) - ctors) + Pimm (Node (stypecons, + Node (Symbol label, List.map pexp_u_formal_arg pfargs) + :: List.map (fun ((l,name) as s, types) + -> Node (Symbol s, + List.map pexp_u_ind_arg types)) + ctors))

| Case (loc, target, bltp, branches, default) -> let bt = lexp_unparse bltp in @@ -445,8 +446,8 @@ let rec lexp_unparse lxp = args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) - in (Ppatcons (Pcall (pdatacons, - [pexp_unparse bt; Symbol (loc, str)]), + in (Ppatcons (Pimm (Node (sdatacons, + [pexp_unparse bt; Symbol (loc, str)])), pat_args), lexp_unparse bch) ) (SMap.bindings branches) in @@ -466,16 +467,17 @@ let rec lexp_unparse lxp =

| SortLevel (SLz) -> Pimm (Symbol (U.dummy_location, "##TypeLevel.z")) | SortLevel (SLsucc l) - -> Pcall (Pimm (Symbol (lexp_location l, "##TypeLevel.succ")), - [pexp_unparse (lexp_unparse l)]) + -> Pimm (Node (Symbol (lexp_location l, "##TypeLevel.succ"), + [pexp_unparse (lexp_unparse l)])) | SortLevel (SLlub (l1, l2)) - -> Pcall (Pimm (Symbol (lexp_location l1, "##TypeLevel.∪")), - [pexp_unparse (lexp_unparse l1); pexp_unparse (lexp_unparse l2)]) + -> Pimm (Node (Symbol (lexp_location l1, "##TypeLevel.∪"), + [pexp_unparse (lexp_unparse l1); + pexp_unparse (lexp_unparse l2)])) | Sort (l, StypeOmega) -> Pimm (Symbol (l, "##Type_ω")) | Sort (l, StypeLevel) -> Pimm (Symbol (l, "##Type_ℓ")) | Sort (l, Stype sl) - -> Pcall (Pimm (Symbol (lexp_location sl, "##Type_")), - [pexp_unparse (lexp_unparse sl)]) + -> Pimm (Node (Symbol (lexp_location sl, "##Type_"), + [pexp_unparse (lexp_unparse sl)]))

(* FIXME: ¡Unify lexp_print and lexp_string! *) and lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp))

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

- | Pcall (func, args) - -> let (f, t) as ft = infer func ctx in + | Pimm (Node (func, args)) + -> let (f, t) as ft = infer (pexp_parse func) ctx in let meta_ctx, _ = !global_substitution in if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t type_special_form) then parse_special_form ctx f args None else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t (BI.get_predef "Macro" ctx)) then - let t = newMetatype (pexp_location func) in + let t = newMetatype (sexp_location func) in let lxp = handle_macro_call ctx f args t in (lxp, t) else @@ -443,8 +443,8 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = | Pcase (loc, target, branches) -> check_case t (loc, target, branches) ctx

- | Pcall (func, args) - -> let (f, ft) = infer func ctx in + | Pimm (Node (func, args)) + -> let (f, ft) = infer (pexp_parse func) ctx in let meta_ctx, _ = !global_substitution in if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ft type_special_form) then let (e, _) = parse_special_form ctx f args (Some t) in e

===================================== 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 - | Pcall of pexp * sexp list (* Curried call. *) (* The symbols are only used so that we can distinguish two * otherwise isomorphic types. *) | Pcase of location * pexp * (ppat * pexp) list @@ -63,14 +62,12 @@ let rec pexp_location e = (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s | Plet (l, _, _) -> l - | Pcall (f, _) -> pexp_location f | Pcase (l, _, _) -> l

let pexp_name e = match e with | Pimm _ -> "Pimm" | Plet (_, _, _) -> "Plet" - | Pcall (_, _) -> "Pcall" | Pcase (_, _, _) -> "Pcase"

let rec pexp_pat_location e = match e with @@ -106,7 +103,7 @@ let rec pexp_parse (s : sexp) : pexp = Pimm (Symbol (start, "?")) (* | Node (Symbol (_, "(_)"), [e]) -> pexp_parse e *) | Node (f, []) -> pexp_parse f - | Node (f, args) -> Pcall (pexp_parse f, args) + | Node _ -> Pimm s

and pexp_p_actual_arg arg : (arg_kind * pvar option * pexp) = match arg with @@ -206,11 +203,11 @@ and pexp_p_decls e: pdecl list = | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, pexp_parse t)] | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, pexp_parse t)] | Node (Symbol (l, "_=_"), [Node (Symbol s, args) as d; t]) -> - [Pexpr(s, Pcall (Pimm (Symbol (sexp_location d, "lambda_->_")), - [(match args with - | [] -> Sexp.dummy_epsilon - | arg::args -> Node (arg, args)); - t]))] + [Pexpr(s, Pimm (Node (Symbol (sexp_location d, "lambda_->_"), + [(match args with + | [] -> Sexp.dummy_epsilon + | arg::args -> Node (arg, args)); + t])))] (* everything else is considered a macro * An error will be produced during lexp_parsing if the macro does not exist * once expanded the Pmcall macro will produce a list of pdecl *) @@ -227,7 +224,6 @@ and pexp_unparse (e : pexp) : sexp = | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body]) - | Pcall (f, args) -> Node (pexp_unparse f, args) | Pcase (start, e, branches) -> Node (Symbol (start, "case_"), pexp_unparse e

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