Stefan pushed to branch master at Stefan / Typer

Commits: baf904f3 by Stefan Monnier at 2017-02-27T21:16:37-05:00 * src/pexp.ml (pexp): Remove Pvar

Use `Pimm (Symbol ..)` 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 = Pvar (U.dummy_location, "##datacons") -let ptypecons = Pvar (U.dummy_location, "##typecons") +let pdatacons = Pimm (Symbol (U.dummy_location, "##datacons")) +let ptypecons = Pimm (Symbol (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 ((l,name), _, _) -> Pvar (l, "##" ^ name) - | Var ((loc, name), _) -> Pvar (loc, name) + | 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)]) | 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) -> Pvar (U.dummy_location, "##TypeLevel.z") + | SortLevel (SLz) -> Pimm (Symbol (U.dummy_location, "##TypeLevel.z")) | SortLevel (SLsucc l) - -> Pcall (Pvar (lexp_location l, "##TypeLevel.succ"), + -> Pcall (Pimm (Symbol (lexp_location l, "##TypeLevel.succ")), [pexp_unparse (lexp_unparse l)]) | SortLevel (SLlub (l1, l2)) - -> Pcall (Pvar (lexp_location l1, "##TypeLevel.∪"), + -> Pcall (Pimm (Symbol (lexp_location l1, "##TypeLevel.∪")), [pexp_unparse (lexp_unparse l1); pexp_unparse (lexp_unparse l2)]) - | Sort (l, StypeOmega) -> Pvar (l, "##Type_ω") - | Sort (l, StypeLevel) -> Pvar (l, "##Type_ℓ") + | Sort (l, StypeOmega) -> Pimm (Symbol (l, "##Type_ω")) + | Sort (l, StypeLevel) -> Pimm (Symbol (l, "##Type_ℓ")) | Sort (l, Stype sl) - -> Pcall (Pvar (lexp_location sl, "##Type_"), + -> Pcall (Pimm (Symbol (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 @@ -255,18 +255,8 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = _global_lexp_ctx := ctx;

match p with - (* Block/String/Integer/Float. *) - | Pimm v - -> (mkImm (v), - match v with - | Integer _ -> DB.type_int - | Float _ -> DB.type_float - | String _ -> DB.type_string; - | _ -> pexp_error tloc p "Could not find type"; - mkDummy_type tloc) - - | Pvar (l,name) when String.length name >= 1 - && String.get name 0 == '#' + | Pimm (Symbol (l,name)) + when String.length name >= 1 && String.get name 0 == '#' -> if String.length name > 2 && String.get name 1 == '#' then let name = string_sub name 2 (String.length name) in try SMap.find name (! BI.lmap) @@ -277,7 +267,8 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = mkDummy_infer l)

(* Symbol i.e identifier. *) - | Pvar (loc, name) when String.length name < 1 || String.get name 0 != '?' + | Pimm (Symbol (loc, name)) + when String.length name < 1 || String.get name 0 != '?' -> (try let idx = senv_lookup name ctx in let lxp = make_var name idx loc in @@ -331,11 +322,22 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = else infer_call ctx ft args

- | (Plambda _ | Pcase _ | Pvar _) + | (Plambda _ | Pcase _ | Pimm (Symbol _)) -> let t = newMetatype (pexp_location p) in let lxp = check p t ctx in (lxp, t)

+ (* Block/String/Integer/Float. *) + | Pimm v + -> (mkImm (v), + match v with + | Integer _ -> DB.type_int + | Float _ -> DB.type_float + | String _ -> DB.type_string; + | _ -> pexp_error tloc p "Could not find type"; + mkDummy_type tloc) + + and parse_special_form ctx f args ot = let loc = lexp_location f in let meta_ctx, _ = !global_substitution in @@ -510,9 +512,9 @@ and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = let (e, inferred_t) = infer_call ctx (f, ft) args in check_inferred ctx e inferred_t t

- | Pvar (l,"?") -> newMetavar l "v" t - | Pvar (l, name) when String.length name > 1 - && String.get name 0 = '?' + | Pimm (Symbol (l,"?")) -> newMetavar l "v" t + | Pimm (Symbol (l, name)) when String.length name > 1 + && String.get name 0 = '?' -> pexp_error l p "Named metavars not supported (yet)"; newMetavar l name t

@@ -693,7 +695,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match OL.lexp_whnf (mkVar (var, idx)) (ectx_to_lctx ctx) meta_ctx with | Cons _ (* It's indeed a constructor! *) - -> add_branch (Pvar var) [] + -> add_branch (Pimm (Symbol var)) [] | _ -> add_default (Some var) (* A named default branch. *) with Not_found -> add_default (Some var))

@@ -891,7 +893,7 @@ and sexp_decls_macro_print sxp_decls = | e -> sexp_print e; print_string "\n"

and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = - try let lxp, ltp = infer (Pvar (loc, mname)) ctx in + try let lxp, ltp = infer (Pimm (Symbol (loc, mname))) ctx in

(* FIXME: Check that (conv_p ltp Macro)! *) let ret = lexp_expand_macro loc lxp sargs ctx None in

===================================== 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, ... *) - | Pvar of pvar | Plet of location * pdecl list * pexp | Parrow of arg_kind * pvar option * pexp * location * pexp | Plambda of arg_kind * pvar * pexp option * pexp @@ -65,7 +64,6 @@ let rec pexp_location e = match e with (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s - | Pvar (l,_) -> l | Plet (l, _, _) -> l | Parrow (_, _, _, l, _) -> l | Plambda (_,(l,_), _, _) -> l @@ -75,7 +73,6 @@ let rec pexp_location e = let pexp_name e = match e with | Pimm _ -> "Pimm" - | Pvar (_,_) -> "Pvar" | Plet (_, _, _) -> "Plet" | Parrow (_, _, _, _, _) -> "Parrow" | Plambda (_,(_,_), _, _) -> "Plambda" @@ -93,14 +90,12 @@ let rec pexp_parse (s : sexp) : pexp = match s with (* This is an internal error because Epsilon does not have any location * information so it needs to be caught elsewhere. *) - | (Block _ | Integer _ | Float _ | String _) -> Pimm s - (* | Symbol (l, "Type") -> Psort (l, Type) *) - | Symbol s -> Pvar s + | (Block _ | Integer _ | Float _ | String _ | Symbol _) -> Pimm s (* let *) | Node (Symbol (start, "let_in_"), [decls; body]) -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) - -> pexp_error start "Unrecognized let expression"; Pvar (start, "?") + -> pexp_error start "Unrecognized let expression"; Pimm (Symbol (start, "?")) (* arrow *) | Node (Symbol (start, (("_->_" | "_=>_" | "_≡>_") as arw)), [t1; t2]) -> let kind = (match arw with @@ -110,7 +105,8 @@ let rec pexp_parse (s : sexp) : pexp = -> 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"; Pvar (start, "?") + -> pexp_error start "Unrecognized arrow expression"; + Pimm (Symbol (start, "?")) (* lambda *) | Node (Symbol (start,(("lambda_->_" | "lambda_=>_" | "lambda_≡>_") as arw)), [arg; body]) @@ -129,7 +125,8 @@ let rec pexp_parse (s : sexp) : pexp = (sexp_p_list arg ["_:_"]) (pexp_parse body) | Node (Symbol (start, "lambda_"), _) - -> pexp_error start "Unrecognized lambda expression"; Pvar (start, "?") + -> pexp_error start "Unrecognized lambda expression"; + Pimm (Symbol (start, "?")) (* cases analysis *) | Node (Symbol (start, "case_"), [Node (Symbol (_, "_|_"), e :: cases)]) @@ -138,11 +135,12 @@ let rec pexp_parse (s : sexp) : pexp = -> (pexp_p_pat pat, pexp_parse code) | _ -> let l = (sexp_location branch) in pexp_error l "Unrecognized simple case branch"; - (Ppatany l, Pvar (l, "?")) + (Ppatany l, Pimm (Symbol (l, "?"))) in Pcase (start, pexp_parse e, List.map parse_case cases) | Node (Symbol (start, "case_"), [e]) -> Pcase (start, pexp_parse e, []) | Node (Symbol (start, "case_"), _) - -> pexp_error start "Unrecognized case expression"; Pvar (start, "?") + -> pexp_error start "Unrecognized case expression"; + Pimm (Symbol (start, "?")) (* | Node (Symbol (_, "(_)"), [e]) -> pexp_parse e *) | Node (f, []) -> pexp_parse f | Node (f, args) -> Pcall (pexp_parse f, args) @@ -266,7 +264,6 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Ext) -> Symbol (l, "%Ext%") *) (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s - | Pvar v -> Symbol v | 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/baf904f35aacace8b5c6a1032be7aa1c4ff3...