Stefan pushed to branch master at Stefan / Typer

Commits: 61d04393 by Stefan Monnier at 2017-02-28T01:34:25-05:00 * src/lparse.ml (sform_case): New function

(register_special_forms): Register it.

* src/pexp.ml (pexp): Remove Pcase.

- - - - -

3 changed files:

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

Changes:

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -458,7 +458,15 @@ let rec lexp_unparse lxp = | Some vdef -> Ppatsym vdef), lexp_unparse dft)::pbranch | None -> pbranch - in Pcase (loc, lexp_unparse target, pbranch) + in let e = lexp_unparse target in + Pimm (Node (Symbol (loc, "case_"), + pexp_unparse e + :: List.map + (fun (pat, branch) -> + Node (Symbol (pexp_pat_location pat, "_=>_"), + [pexp_u_pat pat; + pexp_unparse branch])) + pbranch))

(* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name), _)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -302,8 +302,9 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = else infer_call ctx ft args

- | (Pcase _ | Pimm (Symbol _)) - -> let t = newMetatype (pexp_location p) in + | Pimm (Symbol (_, name)) + -> assert (String.length name >= 1 || String.get name 0 = '?'); + let t = newMetatype (pexp_location p) in let lxp = check p t ctx in (lxp, t)

@@ -440,9 +441,6 @@ and unify_with_arrow ctx tloc lxp kind var aty = and check (p : pexp) (t : ltype) (ctx : elab_context): lexp =

match p with - | Pcase (loc, target, branches) - -> check_case t (loc, target, branches) ctx - | Pimm (Node (func, args)) -> let (f, ft) = infer (pexp_parse func) ctx in let meta_ctx, _ = !global_substitution in @@ -1220,6 +1218,26 @@ let sform_lambda kind ctx loc sargs ot' = | _ -> sexp_error loc "##lambda_->_ takes two arguments"; sform_dummy_ret loc

+let rec sform_case ctx loc sargs ot = match sargs with + | [Node (Symbol (_, "_|_"), se :: scases)] + -> let parse_case branch = match branch with + | Node (Symbol (_, "_=>_"), [pat; code]) + -> (pexp_p_pat pat, pexp_parse code) + | _ -> let l = (sexp_location branch) in + sexp_error l "Unrecognized simple case branch"; + (Ppatany l, Pimm (Symbol (l, "?"))) in + let pe = pexp_parse se in + let pcases = List.map parse_case scases in + let t = match ot with Some t -> t | None -> newMetatype loc in + let le = check_case t (loc, pe, pcases) ctx in + (le, match ot with Some _ -> Checked | None -> Inferred t) + + (* In case there are no branches, pretend there was a | anyway. *) + | [e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot + | _ -> sexp_error loc "Unrecognized case expression"; + sform_dummy_ret loc + + (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) * But it would be less efficient (such a lambda can't be passed as argument @@ -1267,6 +1285,7 @@ let register_special_forms () = ("_->_", sform_arrow Aexplicit); ("_=>_", sform_arrow Aimplicit); ("_≡>_", sform_arrow Aerasable); + ("case_", sform_case); ("Type_", sform_type); (* FIXME: We should add here `let_in_`, `case_`, etc... *) ("get-attribute", sform_get_attribute);

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -40,9 +40,6 @@ type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) | Plet of location * pdecl list * pexp - (* The symbols are only used so that we can distinguish two - * otherwise isomorphic types. *) - | Pcase of location * pexp * (ppat * pexp) list

and ppat = (* This data type allows nested patterns, but in reality we don't @@ -62,13 +59,11 @@ let rec pexp_location e = (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s | Plet (l, _, _) -> l - | Pcase (l, _, _) -> l

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

let rec pexp_pat_location e = match e with | Ppatany l -> l @@ -87,21 +82,6 @@ let rec pexp_parse (s : sexp) : pexp = -> Plet (start, pexp_p_decls decls, pexp_parse body) | Node (Symbol (start, ("let_in_" | "let" | "let_")), _) -> pexp_error start "Unrecognized let expression"; Pimm (Symbol (start, "?")) - (* cases analysis *) - | Node (Symbol (start, "case_"), - [Node (Symbol (_, "_|_"), e :: cases)]) - -> let parse_case branch = match branch with - | Node (Symbol (_, "_=>_"), [pat; code]) - -> (pexp_p_pat pat, pexp_parse code) - | _ -> let l = (sexp_location branch) in - pexp_error l "Unrecognized simple case branch"; - (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"; - Pimm (Symbol (start, "?")) - (* | Node (Symbol (_, "(_)"), [e]) -> pexp_parse e *) | Node (f, []) -> pexp_parse f | Node _ -> Pimm s

@@ -224,15 +204,6 @@ and pexp_unparse (e : pexp) : sexp = | Plet (start, decls, body) -> Node (Symbol (start, "let_in_"), [pexp_u_decls decls; pexp_unparse body]) - | Pcase (start, e, branches) -> - Node (Symbol (start, "case_"), - pexp_unparse e - :: List.map - (fun (pat, branch) -> - Node (Symbol (pexp_pat_location pat, "_=>_"), - [pexp_u_pat pat; - pexp_unparse branch])) - branches)

and pexp_u_decl decl = match decl with

View it on GitLab: https://gitlab.com/monnier/typer/commit/61d04393f190f3b7f9fce40a0819621e3d9d...