Stefan pushed to branch master at Stefan / Typer
Commits: 36afff9d by Stefan Monnier at 2017-02-27T20:42:38-05:00 * src/pexp.ml (pexp): Remove Pbuiltin
Use a Pvar starting ith "##" 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,16 +364,16 @@ let lexp_name e = | Sort _ -> "Sort" | SortLevel _ -> "SortLevel"
-let pdatacons = Pbuiltin (U.dummy_location, "datacons") -let ptypecons = Pbuiltin (U.dummy_location, "typecons") +let pdatacons = Pvar (U.dummy_location, "##datacons") +let ptypecons = Pvar (U.dummy_location, "##typecons")
(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = match lxp with | Susp _ as e -> lexp_unparse (nosusp e) | Imm (sexp) -> Pimm (sexp) - | Builtin (s, _, _) -> Pbuiltin s - | Var ((loc, name), _) -> Pvar((loc, name)) + | Builtin ((l,name), _, _) -> Pvar (l, "##" ^ name) + | Var ((loc, name), _) -> Pvar (loc, name) | Cons (t, (l, name)) -> Pcall (pdatacons, [pexp_unparse (lexp_unparse t); Symbol (l, name)]) | Lambda (kind, vdef, ltp, body) -> @@ -450,17 +450,17 @@ let rec lexp_unparse lxp = -> Pimm (Symbol (loc, "?<" ^ name ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]>"))
- | SortLevel (SLz) -> Pbuiltin (U.dummy_location, "TypeLevel.z") + | SortLevel (SLz) -> Pvar (U.dummy_location, "##TypeLevel.z") | SortLevel (SLsucc l) - -> Pcall (Pbuiltin (lexp_location l, "TypeLevel.succ"), + -> Pcall (Pvar (lexp_location l, "##TypeLevel.succ"), [pexp_unparse (lexp_unparse l)]) | SortLevel (SLlub (l1, l2)) - -> Pcall (Pbuiltin (lexp_location l1, "TypeLevel.∪"), + -> Pcall (Pvar (lexp_location l1, "##TypeLevel.∪"), [pexp_unparse (lexp_unparse l1); pexp_unparse (lexp_unparse l2)]) - | Sort (l, StypeOmega) -> Pbuiltin (l, "Type_ω") - | Sort (l, StypeLevel) -> Pbuiltin (l, "Type_ℓ") + | Sort (l, StypeOmega) -> Pvar (l, "##Type_ω") + | Sort (l, StypeLevel) -> Pvar (l, "##Type_ℓ") | Sort (l, Stype sl) - -> Pcall (Pbuiltin (lexp_location sl, "Type_"), + -> Pcall (Pvar (lexp_location sl, "##Type_"), [pexp_unparse (lexp_unparse sl)])
(* FIXME: ¡Unify lexp_print and lexp_string! *)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -265,8 +265,11 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = | _ -> pexp_error tloc p "Could not find type"; mkDummy_type tloc)
- | Pbuiltin (l,name) - -> (try SMap.find name (! BI.lmap) + | Pvar (l,name) when String.length name > 2 + && String.get name 0 == '#' + && String.get name 1 == '#' + -> let name = string_sub name 2 (String.length name) in + (try SMap.find name (! BI.lmap) with Not_found -> pexp_error l p ("Unknown builtin `" ^ name ^ "`"); mkDummy_infer l)
===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -39,7 +39,6 @@ type pvar = symbol type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) - | Pbuiltin of symbol | Pvar of pvar | Phastype of location * pexp * pexp | Pmetavar of pvar @@ -68,7 +67,6 @@ let rec pexp_location e = match e with (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s - | Pbuiltin (l,_) -> l | Pvar (l,_) -> l | Phastype (l,_,_) -> l | Pmetavar (l, _) -> l @@ -81,7 +79,6 @@ let rec pexp_location e = let pexp_name e = match e with | Pimm _ -> "Pimm" - | Pbuiltin _ -> "Pbuiltin" | Pvar (_,_) -> "Pvar" | Phastype (_,_,_) -> "Phastype" | Pmetavar (_, _) -> "Pmetavar" @@ -106,18 +103,6 @@ let rec pexp_parse (s : sexp) : pexp = (* | Symbol (l, "Type") -> Psort (l, Type) *) | Symbol (l, name) when String.length name > 0 && String.get name 0 == '?' -> Pmetavar (l, String.sub name 1 (String.length name - 1)) - | Symbol (l, name) when String.length name > 2 - && String.get name 0 == '#' - && String.get name 1 == '#' - -> Pbuiltin (l, string_sub name 2 (String.length name)) - (* | Node (Symbol (start, "##"), [Symbol s]) - * -> Pbuiltin s - * | Node (Symbol (start, "##"), [e]) - * -> pexp_error (sexp_location e) "Non-symbol argument to `##`"; - * Pmetavar (start, "") - * | Node (Symbol (start, "##"), _) - * -> pexp_error start "`##` takes exactly one argument"; - * Pmetavar (start, "") *) | Symbol s -> Pvar s | Node (Symbol (start, "_:_"), [e; t]) -> Phastype (start, pexp_parse e, pexp_parse t) @@ -291,8 +276,6 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Ext) -> Symbol (l, "%Ext%") *) (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s - | Pbuiltin (l,name) -> Symbol (l, "##" ^ name) - (* | Pbuiltin ((l,_) as s) -> Node (Symbol (l, "##"), [Symbol s]) *) | Pvar v -> Symbol v | Pmetavar (l,name) -> Symbol (l, "?" ^ name) | Phastype (l,e,t)
View it on GitLab: https://gitlab.com/monnier/typer/commit/36afff9d215abb6cc9a15fb93b9c2a250226...