[Git][monnier/typer][master] * src/pexp.ml (pexp): Remove Pmetavar - Typer

27 Fév 2017

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...

    