Stefan pushed to branch master at Stefan / Typer

Commits: 69727028 by Stefan Monnier at 2017-02-28T01:45:03-05:00 * src/lparse.ml (sform_letin): New function

(register_special_forms): Register it.

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

- - - - -

4 changed files:

- src/lexp.ml - src/lparse.ml - src/pexp.ml - − tests/pexp_test.ml

Changes:

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -403,7 +403,9 @@ let rec lexp_unparse lxp = -> Ptype (vdef, lexp_unparse ltp) :: Pexpr(vdef, lexp_unparse lxp)::acc) [] ldecls in - Plet (loc, pdecls, lexp_unparse body) + Pimm (Node (Symbol (loc, "let_in_"), + [pexp_u_decls pdecls; + pexp_unparse (lexp_unparse body)]))

| Call(lxp, largs) -> (* (arg_kind * lexp) list *) let pargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -281,14 +281,6 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); mkDummy_infer loc))

- (* Let, Variable declaration + local scope. *) - | Plet (loc, decls, body) - -> let declss, nctx = lexp_p_decls decls ctx in - let bdy, ltp = infer body nctx in - let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in - (lexp_let_decls declss bdy nctx), - mkSusp ltp s - | Pimm (Node (func, args)) -> let (f, t) as ft = infer (pexp_parse func) ctx in let meta_ctx, _ = !global_substitution in @@ -1237,6 +1229,18 @@ let rec sform_case ctx loc sargs ot = match sargs with | _ -> sexp_error loc "Unrecognized case expression"; sform_dummy_ret loc

+let sform_letin ctx loc sargs ot = match sargs with + | [sdecls; sbody] + -> let pdecls = pexp_p_decls sdecls in + let pbody = pexp_parse sbody in + let declss, nctx = lexp_p_decls pdecls ctx in + (* FIXME: Use `elaborate`. *) + let bdy, ltp = infer pbody nctx in + let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in + (lexp_let_decls declss bdy nctx, + Inferred (mkSusp ltp s)) + | _ -> sexp_error loc "Unrecognized let_in_ expression"; + sform_dummy_ret loc

(* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) @@ -1286,6 +1290,7 @@ let register_special_forms () = ("_=>_", sform_arrow Aimplicit); ("_≡>_", sform_arrow Aerasable); ("case_", sform_case); + ("let_in_", sform_letin); ("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 @@ -39,7 +39,6 @@ type pvar = symbol type pexp = (* | Psort of location * sort *) | Pimm of sexp (* Used for strings, ... *) - | Plet of location * pdecl list * pexp

and ppat = (* This data type allows nested patterns, but in reality we don't @@ -58,12 +57,10 @@ let rec pexp_location e = match e with (* | Psort (l,_) -> l *) | Pimm s -> sexp_location s - | Plet (l, _, _) -> l

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

let rec pexp_pat_location e = match e with | Ppatany l -> l @@ -77,11 +74,6 @@ let rec pexp_parse (s : sexp) : pexp = (* This is an internal error because Epsilon does not have any location * information so it needs to be caught elsewhere. *) | (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"; Pimm (Symbol (start, "?")) | Node (f, []) -> pexp_parse f | Node _ -> Pimm s

@@ -201,9 +193,6 @@ and pexp_unparse (e : pexp) : sexp = (* | Psort (l,Ext) -> Symbol (l, "%Ext%") *) (* | Psort (l,Type) -> Symbol (l, "%Type%") *) | Pimm s -> s - | Plet (start, decls, body) -> - Node (Symbol (start, "let_in_"), - [pexp_u_decls decls; pexp_unparse body])

and pexp_u_decl decl = match decl with

===================================== tests/pexp_test.ml deleted ===================================== --- a/tests/pexp_test.ml +++ /dev/null @@ -1,22 +0,0 @@ -open Pexp -open Utest_lib - - -let _ = (add_test "PEXP" "Type Parsing" (fun () -> - - let dcode = " - let a : Nat; a = 1; b : Nat; b = 3; in a + b;" in - - let ret = pexp_expr_str dcode in - match ret with - | [expr] ->( - match expr with - | Plet(_, arg, _) -> (match arg with - | Ptype(_, tp)::_ ->success () - | _ -> failure ()) - | _ -> failure ()) - | _ -> failure ()) -) - - -let _ = run_all ()

View it on GitLab: https://gitlab.com/monnier/typer/commit/6972702846972e9a2ca16c311f3abdf503ff...