Stefan pushed to branch master at Stefan / Typer
Commits: 3a54a263 by Stefan Monnier at 2017-02-27T20:56:07-05:00 * src/pexp.ml (pexp): Remove Pmetavar
Use Pvar with a leading ? instead. Reserve identifiers starting with # for future use.
- - - - -
3 changed files:
- src/lexp.ml - src/lparse.ml - src/pexp.ml
Changes:
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -447,8 +447,8 @@ let rec lexp_unparse lxp =
(* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name), _) - -> Pimm (Symbol (loc, "?<" ^ name ^ "-" ^ string_of_int idx - ^ "[" ^ subst_string subst ^ "]>")) + -> Pimm (Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx + ^ "[" ^ subst_string subst ^ "]"))
| SortLevel (SLz) -> Pvar (U.dummy_location, "##TypeLevel.z") | SortLevel (SLsucc l)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -265,17 +265,19 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = | _ -> pexp_error tloc p "Could not find type"; mkDummy_type tloc)
- | Pvar (l,name) when String.length name > 2 + | Pvar (l,name) when String.length name >= 1 && 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) + -> 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) + with Not_found + -> pexp_error l p ("Unknown builtin `" ^ name ^ "`"); + mkDummy_infer l + else (pexp_error l p ("Invalid special identifier `" ^ name ^ "`"); + mkDummy_infer l)
(* Symbol i.e identifier. *) - | Pvar (loc, name) + | Pvar (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 @@ -333,7 +335,7 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = -> let ltp = infer_type ptp ctx None in (check pxp ltp ctx, ltp)
- | (Plambda _ | Pcase _ | Pmetavar _) + | (Plambda _ | Pcase _ | Pvar _) -> let t = newMetatype (pexp_location p) in let lxp = check p t ctx in (lxp, t) @@ -512,8 +514,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
- | Pmetavar (l,"") -> newMetavar l "v" t - | Pmetavar (l, name) + | Pvar (l,"?") -> newMetavar l "v" t + | Pvar (l, name) when String.length name > 1 + && String.get name 0 = '?' -> pexp_error l p "Named metavars not supported (yet)"; newMetavar l name t
===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -41,7 +41,6 @@ type pexp = | Pimm of sexp (* Used for strings, ... *) | Pvar of pvar | Phastype of location * pexp * pexp - | Pmetavar 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 @@ -69,7 +68,6 @@ let rec pexp_location e = | Pimm s -> sexp_location s | Pvar (l,_) -> l | Phastype (l,_,_) -> l - | Pmetavar (l, _) -> l | Plet (l, _, _) -> l | Parrow (_, _, _, l, _) -> l | Plambda (_,(l,_), _, _) -> l @@ -81,7 +79,6 @@ let pexp_name e = | Pimm _ -> "Pimm" | Pvar (_,_) -> "Pvar" | Phastype (_,_,_) -> "Phastype" - | Pmetavar (_, _) -> "Pmetavar" | Plet (_, _, _) -> "Plet" | Parrow (_, _, _, _, _) -> "Parrow" | Plambda (_,(_,_), _, _) -> "Plambda" @@ -101,8 +98,6 @@ let rec pexp_parse (s : sexp) : pexp = * information so it needs to be caught elsewhere. *) | (Block _ | Integer _ | Float _ | String _) -> Pimm s (* | 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 s -> Pvar s | Node (Symbol (start, "_:_"), [e; t]) -> Phastype (start, pexp_parse e, pexp_parse t) @@ -110,7 +105,7 @@ let rec pexp_parse (s : sexp) : pexp = | 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"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized let expression"; Pvar (start, "?") (* arrow *) | Node (Symbol (start, (("_->_" | "_=>_" | "_≡>_") as arw)), [t1; t2]) -> let kind = (match arw with @@ -120,7 +115,7 @@ 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"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized arrow expression"; Pvar (start, "?") (* lambda *) | Node (Symbol (start,(("lambda_->_" | "lambda_=>_" | "lambda_≡>_") as arw)), [arg; body]) @@ -139,7 +134,7 @@ let rec pexp_parse (s : sexp) : pexp = (sexp_p_list arg ["_:_"]) (pexp_parse body) | Node (Symbol (start, "lambda_"), _) - -> pexp_error start "Unrecognized lambda expression"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized lambda expression"; Pvar (start, "?") (* cases analysis *) | Node (Symbol (start, "case_"), [Node (Symbol (_, "_|_"), e :: cases)]) @@ -148,11 +143,11 @@ 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, Pmetavar (l, "_")) + (Ppatany l, Pvar (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"; Pmetavar (start, "_") + -> pexp_error start "Unrecognized case expression"; Pvar (start, "?") (* | Node (Symbol (_, "(_)"), [e]) -> pexp_parse e *) | Node (f, []) -> pexp_parse f | Node (f, args) -> Pcall (pexp_parse f, args) @@ -277,7 +272,6 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s | Pvar v -> Symbol v - | Pmetavar (l,name) -> Symbol (l, "?" ^ name) | Phastype (l,e,t) -> Node (Symbol (l, "_:_"), [pexp_unparse e; pexp_unparse t]) | Plet (start, decls, body) ->
View it on GitLab: https://gitlab.com/monnier/typer/commit/3a54a26388826075d9b183e39d40abb1a25b...