Stefan pushed to branch master at Stefan / Typer

Commits: 79cd9b86 by Stefan Monnier at 2017-02-28T02:08:42-05:00 * src/pexp.ml (pexp): Remove type

(pexp_location, pexp_name, pexp_parse, pexp_unparse, pexp_string) (pexp_print): Remove functions.

* src/lparse.ml (pexp_fatal, pexp_error): Remove functions.

- - - - -

6 changed files:

- src/REPL.ml - src/debug.ml - src/debug_util.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml

Changes:

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -106,7 +106,7 @@ type lexpr = lexp

(* Grouping declaration together will enable us to support mutually recursive * declarations while bringing us closer to normal typer *) -let ipexp_parse (sxps: sexp list): (pdecl list * pexp list) = +let ipexp_parse (sxps: sexp list): (pdecl list * sexp list) = let rec _pxp_parse sxps dacc pacc = match sxps with | [] -> (List.rev dacc), (List.rev pacc) @@ -120,7 +120,7 @@ let ipexp_parse (sxps: sexp list): (pdecl list * pexp list) = _pxp_parse tl (List.append (pexp_p_decls sxp) dacc) pacc

(* Expression *) - | _ -> _pxp_parse tl dacc ((pexp_parse sxp)::pacc) in + | _ -> _pxp_parse tl dacc (sxp::pacc) in _pxp_parse sxps [] []

===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -114,13 +114,13 @@ let debug_sexp_print_all tokens = (* Print a Pexp with debug info *) let debug_pexp_print ptop = print_string " "; - let l = pexp_location ptop in + let l = sexp_location ptop in let print_info msg loc pex = print_string msg; print_string "["; loc_print loc; print_string "]\t"; - pexp_print pex in - print_info (pexp_name ptop) l ptop + sexp_print pex in + print_info (sexp_name ptop) l ptop

let debug_pexp_decls decls = let loc_print l = print_string "["; loc_print l; print_string "] " in @@ -130,12 +130,12 @@ let debug_pexp_decls decls =

let _ = match e with | Pexpr ((l, name), pxp) -> - lalign_print_string (pexp_name pxp) 15; - loc_print l; print_string " = "; pexp_print pxp + lalign_print_string (sexp_name pxp) 15; + loc_print l; print_string " = "; sexp_print pxp

| Ptype ((l, name), ptp) -> - lalign_print_string (pexp_name ptp) 15; - loc_print l; print_string " : "; pexp_print ptp + lalign_print_string (sexp_name ptp) 15; + loc_print l; print_string " : "; sexp_print ptp

| Pmcall((l, op), args) -> lalign_print_string "Macro Decls" 15;

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -218,7 +218,7 @@ let format_source () = (* merged declaration, allow us to process declaration in multiple pass *) (* first detect recursive decls then lexp decls*) type mdecl = - | Ldecl of symbol * pexp option * pexp option + | Ldecl of symbol * sexp option * sexp option | Lmcall of symbol * sexp list

let lexp_detect_recursive pdecls = @@ -370,14 +370,14 @@ let main () = lalign_print_string s 20;

let _ = match ptp with - | Some pxp -> pexp_print pxp; + | Some pxp -> sexp_print pxp; | None -> print_string " " in

print_string "\n"; lalign_print_string s 20;

let _ = match pxp with - | Some pxp -> pexp_print pxp; + | Some pxp -> sexp_print pxp; | None -> print_string " " in

print_string "\n")

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -371,30 +371,30 @@ let stypecons = Symbol (U.dummy_location, "##typecons") let rec lexp_unparse lxp = match lxp with | Susp _ as e -> lexp_unparse (nosusp e) - | Imm (sexp) -> Pimm (sexp) - | Builtin ((l,name), _, _) -> Pimm (Symbol (l, "##" ^ name)) - | Var ((loc, name), _) -> Pimm (Symbol (loc, name)) + | Imm (sexp) -> sexp + | Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name) + | Var ((loc, name), _) -> Symbol (loc, name) | Cons (t, (l, name)) - -> Pimm (Node (sdatacons, - [pexp_unparse (lexp_unparse t); Symbol (l, name)])) + -> Node (sdatacons, + [lexp_unparse t; Symbol (l, name)]) | Lambda (kind, vdef, ltp, body) -> let l = lexp_location lxp in - let st = pexp_unparse (lexp_unparse ltp) in - Pimm (Node (Symbol (l, match kind with - | Aexplicit -> "lambda_->_" - | Aimplicit -> "lambda_=>_" - | Aerasable -> "lambda_≡>_"), - [Node (Symbol (l, "_:_"), [Symbol vdef; st]); - pexp_unparse (lexp_unparse body)])) + let st = lexp_unparse ltp in + Node (Symbol (l, match kind with + | Aexplicit -> "lambda_->_" + | Aimplicit -> "lambda_=>_" + | Aerasable -> "lambda_≡>_"), + [Node (Symbol (l, "_:_"), [Symbol vdef; st]); + lexp_unparse body]) | Arrow (arg_kind, vdef, ltp1, loc, ltp2) - -> let ut1 = pexp_unparse (lexp_unparse ltp1) in - Pimm (Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_" - | Aimplicit -> "_=>_" - | Aerasable -> "_≡>_"), - [(match vdef with None -> ut1 - | Some v -> Node (Symbol (loc, "_:_"), - [Symbol v; ut1])); - pexp_unparse (lexp_unparse ltp2)])) + -> let ut1 = lexp_unparse ltp1 in + Node (Symbol (loc, match arg_kind with Aexplicit -> "_->_" + | Aimplicit -> "_=>_" + | Aerasable -> "_≡>_"), + [(match vdef with None -> ut1 + | Some v -> Node (Symbol (loc, "_:_"), + [Symbol v; ut1])); + lexp_unparse ltp2])

| Let (loc, ldecls, body) -> (* (vdef * lexp * ltype) list *) @@ -403,14 +403,13 @@ let rec lexp_unparse lxp = -> Ptype (vdef, lexp_unparse ltp) :: Pexpr(vdef, lexp_unparse lxp)::acc) [] ldecls in - Pimm (Node (Symbol (loc, "let_in_"), - [pexp_u_decls pdecls; - pexp_unparse (lexp_unparse body)])) + Node (Symbol (loc, "let_in_"), + [pexp_u_decls pdecls; + lexp_unparse body])

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

| Inductive(loc, label, lfargs, ctors) -> (* (arg_kind * vdef * ltype) list *) @@ -427,12 +426,12 @@ let rec lexp_unparse lxp = | None -> (kind, None, lexp_unparse ltp)) largs in ((loc, str), pargs) ) (SMap.bindings ctors) in - Pimm (Node (stypecons, - Node (Symbol label, List.map pexp_u_formal_arg pfargs) - :: List.map (fun ((l,name) as s, types) - -> Node (Symbol s, - List.map pexp_u_ind_arg types)) - ctors)) + Node (stypecons, + Node (Symbol label, List.map pexp_u_formal_arg pfargs) + :: List.map (fun ((l,name) as s, types) + -> Node (Symbol s, + List.map pexp_u_ind_arg types)) + ctors)

| Case (loc, target, bltp, branches, default) -> let bt = lexp_unparse bltp in @@ -448,8 +447,8 @@ let rec lexp_unparse lxp = args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) - in (Ppatcons (Pimm (Node (sdatacons, - [pexp_unparse bt; Symbol (loc, str)])), + in (Ppatcons (Node (sdatacons, + [bt; Symbol (loc, str)]), pat_args), lexp_unparse bch) ) (SMap.bindings branches) in @@ -461,36 +460,33 @@ let rec lexp_unparse lxp = lexp_unparse dft)::pbranch | None -> 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)) + Node (Symbol (loc, "case_"), + e :: List.map + (fun (pat, branch) -> + Node (Symbol (pexp_pat_location pat, "_=>_"), + [pexp_u_pat pat; branch])) + pbranch)

(* FIXME: The cases below are all broken! *) | Metavar (idx, subst, (loc, name), _) - -> Pimm (Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx - ^ "[" ^ subst_string subst ^ "]")) + -> Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx + ^ "[" ^ subst_string subst ^ "]")

- | SortLevel (SLz) -> Pimm (Symbol (U.dummy_location, "##TypeLevel.z")) + | SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") | SortLevel (SLsucc l) - -> Pimm (Node (Symbol (lexp_location l, "##TypeLevel.succ"), - [pexp_unparse (lexp_unparse l)])) + -> Node (Symbol (lexp_location l, "##TypeLevel.succ"), + [lexp_unparse l]) | SortLevel (SLlub (l1, l2)) - -> Pimm (Node (Symbol (lexp_location l1, "##TypeLevel.∪"), - [pexp_unparse (lexp_unparse l1); - pexp_unparse (lexp_unparse l2)])) - | Sort (l, StypeOmega) -> Pimm (Symbol (l, "##Type_ω")) - | Sort (l, StypeLevel) -> Pimm (Symbol (l, "##Type_ℓ")) + -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), + [lexp_unparse l1; lexp_unparse l2]) + | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") + | Sort (l, StypeLevel) -> Symbol (l, "##Type_ℓ") | Sort (l, Stype sl) - -> Pimm (Node (Symbol (lexp_location sl, "##Type_"), - [pexp_unparse (lexp_unparse sl)])) + -> Node (Symbol (lexp_location sl, "##Type_"), + [lexp_unparse sl])

(* FIXME: ¡Unify lexp_print and lexp_string! *) -and lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) +and lexp_string lxp = sexp_string (lexp_unparse lxp)

and subst_string s = match s with | S.Identity -> "Id"

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -78,8 +78,6 @@ let debug_message error_type type_name type_string loc expr message = let lexp_fatal = debug_message fatal lexp_name lexp_string let lexp_warning = debug_message warning lexp_name lexp_string let lexp_error = debug_message error lexp_name lexp_string -let pexp_fatal = debug_message fatal pexp_name pexp_string -let pexp_error = debug_message error pexp_name pexp_string let value_fatal = debug_message fatal value_name value_string

(** Builtin Macros i.e, special forms. *) @@ -246,28 +244,28 @@ let mkDummy_check loc t = newMetavar loc "dummy" t let mkDummy_infer loc = let t = newMetatype loc in (mkDummy_check loc t, t)

-let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = +let rec infer (p : sexp) (ctx : elab_context): lexp * ltype =

- let tloc = pexp_location p in + let tloc = sexp_location p in

(* Save current trace in a global variable. If an error occur, we will be able to retrieve the most recent trace and context. *) _global_lexp_ctx := ctx;

match p with - | Pimm (Symbol (l,name)) + | 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) with Not_found - -> pexp_error l p ("Unknown builtin `" ^ name ^ "`"); + -> sexp_error l ("Unknown builtin `" ^ name ^ "`"); mkDummy_infer l - else (pexp_error l p ("Invalid special identifier `" ^ name ^ "`"); + else (sexp_error l ("Invalid special identifier `" ^ name ^ "`"); mkDummy_infer l)

(* Symbol i.e identifier. *) - | Pimm (Symbol (loc, name)) + | Symbol (loc, name) when String.length name < 1 || String.get name 0 != '?' -> (try let idx = senv_lookup name ctx in @@ -278,11 +276,13 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = lxp, ltp

with Not_found -> - (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); + (sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); mkDummy_infer loc))

- | Pimm (Node (func, args)) - -> let (f, t) as ft = infer (pexp_parse func) ctx in + | Node (se, []) -> infer se ctx + + | Node (func, args) + -> let (f, t) as ft = infer func ctx in let meta_ctx, _ = !global_substitution in if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t type_special_form) then parse_special_form ctx f args None @@ -294,20 +294,20 @@ let rec infer (p : pexp) (ctx : elab_context): lexp * ltype = else infer_call ctx ft args

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

(* Block/String/Integer/Float. *) - | Pimm v + | 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"; + | _ -> sexp_error tloc "Could not find type"; mkDummy_type tloc)

@@ -361,8 +361,7 @@ and get_implicit_arg ctx loc name t = | _ -> value_fatal loc v "default attribute should return a sexp" in

(* lparse the argument *) - let parg = pexp_parse lsarg in - check parg t ctx + check lsarg t ctx | None -> newMetavar loc name t

(* Build the list of implicit arguments to instantiate. *) @@ -430,11 +429,13 @@ and unify_with_arrow ctx tloc lxp kind var aty = (mkDummy_type l, mkDummy_type l) | Some subst -> global_substitution := subst; arg, body

-and check (p : pexp) (t : ltype) (ctx : elab_context): lexp = +and check (p : sexp) (t : ltype) (ctx : elab_context): lexp =

match p with - | Pimm (Node (func, args)) - -> let (f, ft) = infer (pexp_parse func) ctx in + | Node (se, []) -> check se t ctx + + | Node (func, args) + -> let (f, ft) = infer func ctx in let meta_ctx, _ = !global_substitution in if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ft type_special_form) then let (e, _) = parse_special_form ctx f args (Some t) in e @@ -445,10 +446,10 @@ 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

- | 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)"; + | Symbol (l,"?") -> newMetavar l "v" t + | Symbol (l, name) when String.length name > 1 + && String.get name 0 = '?' + -> sexp_error l "Named metavars not supported (yet)"; newMetavar l name t

| _ -> infer_and_check p ctx t @@ -513,7 +514,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); constructors - | _ -> lexp_error (pexp_location target) tlxp + | _ -> lexp_error (sexp_location target) tlxp ("Can't `case` on objects of this type: " ^ lexp_string tltp); SMap.empty in @@ -530,7 +531,7 @@ and check_case rtype (loc, target, ppatterns) ctx = lbranches, Some (v, lexp) in

let add_branch pctor pargs = - let loc = pexp_location pctor in + let loc = sexp_location pctor in let lctor, ct = infer pctor ctx in let meta_ctx, _ = !global_substitution in match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with @@ -563,7 +564,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match (pargs, cargs) with | (_, []) when not (SMap.is_empty pe) -> let pending = SMap.bindings pe in - pexp_error loc pctor + sexp_error loc ("Explicit pattern args `" ^ String.concat ", " (List.map (fun (l, _) -> l) pending) @@ -575,7 +576,7 @@ and check_case rtype (loc, target, ppatterns) ctx = "Too many pattern args to the constructor"; make_nctx ctx s [] [] pe acc | (_, Ppatcons (p, _))::pargs, cargs - -> lexp_error (pexp_location p) lctor + -> lexp_error (sexp_location p) lctor "Nested patterns not supported!"; make_nctx ctx s pargs cargs pe acc | (_, (ak, Some (_, fname), fty)::cargs) @@ -596,13 +597,12 @@ and check_case rtype (loc, target, ppatterns) ctx = | ((Some (l, fname), fpat)::pargs, cargs) -> let var = match fpat with Ppatsym v -> Some v | _ -> None in if SMap.mem fname pe then - pexp_error l pctor - ("Duplicate explicit field `" ^ fname ^ "`"); + sexp_error l ("Duplicate explicit field `" ^ fname ^ "`"); make_nctx ctx s pargs cargs (SMap.add fname var pe) acc | pargs, (ak, fname, fty)::cargs -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in if ak = Aexplicit then - pexp_error loc pctor + sexp_error loc ("Missing pattern for normal field" ^ (match fname with Some (_,n) -> " `" ^ n ^ "`" | _ -> "")); @@ -628,7 +628,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 (Pimm (Symbol var)) [] + -> add_branch (Symbol var) [] | _ -> add_default (Some var) (* A named default branch. *) with Not_found -> add_default (Some var))

@@ -646,13 +646,7 @@ and handle_macro_call ctx func args t = | v -> value_fatal (lexp_location func) v "Macros should return a Sexp" in

- let pxp = try pexp_parse sxp - with e -> - error dloc "An error occurred while expanding a macro"; - sexp_print sxp; - raise e in - - check pxp t ctx + check sxp t ctx

(* Identify Call Type and return processed call. *) and infer_call ctx (func, ltp) (sargs: sexp list) = @@ -670,8 +664,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) when SMap.mem aname pending -> let sarg = SMap.find aname pending in - let parg = pexp_parse sarg in - let larg = check parg arg_type ctx in + let larg = check sarg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs (SMap.remove aname pending) (L.mkSusp ret_type (S.substitute larg)) @@ -680,8 +673,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = Arrow (ak, _, arg_type, _, ret_type) when (aname = "_") (* Explicit-implicit argument. *) - -> let parg = pexp_parse sarg in - let larg = check parg arg_type ctx in + -> let larg = check sarg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg))

@@ -724,8 +716,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = largs, ltp

| sarg :: sargs, Arrow (Aexplicit, _, arg_type, _, ret_type) - -> let parg = pexp_parse sarg in - let larg = check parg arg_type ctx in + -> let larg = check sarg arg_type ctx in handle_fun_args ((Aexplicit, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg))

@@ -741,7 +732,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx =

- let make_args (args:(arg_kind * pvar option * pexp) list) ctx + let make_args (args:(arg_kind * pvar option * sexp) list) ctx : (arg_kind * vname option * ltype) list = let rec loop args acc ctx = match args with @@ -826,7 +817,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 (Pimm (Symbol (loc, mname))) ctx in + try let lxp, ltp = infer (Symbol (loc, mname)) ctx in

(* FIXME: Check that (conv_p ltp Macro)! *) let ret = lexp_expand_macro loc lxp sargs ctx None in @@ -847,7 +838,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) =

and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) - (defs : (vname * pexp * ltype) list) + (defs : (vname * sexp * ltype) list) : (vname * lexp * ltype) list * elab_context = let (declmap, nctx) = List.fold_right @@ -873,7 +864,7 @@ and lexp_decls_1 (ectx : elab_context) (* External ctx. *) (nctx : elab_context) (* New context. *) (pending_decls : (location * ltype) SMap.t) (* Pending type decls. *) - (pending_defs : (vname * pexp * ltype) list) (* Pending definitions. *) + (pending_defs : (vname * sexp * ltype) list) (* Pending definitions. *) : (vname * lexp * ltype) list * pdecl list * elab_context =

match pdecls with @@ -947,11 +938,11 @@ and lexp_p_decls pdecls ctx: ((vname * lexp * ltype) list list * elab_context) = let declss, nnctx = lexp_p_decls pdecls nctx in decls :: declss, nnctx

-and lexp_parse_all (p: pexp list) (ctx: elab_context) : lexp list = +and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = List.map (fun pe -> let e, _ = infer pe ctx in e) p

and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = - let e, _ = infer (pexp_parse e) ctx in e + let e, _ = infer e ctx in e

(* -------------------------------------------------------------------------- * Special forms implementation @@ -959,8 +950,7 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp =

and sform_new_attribute ctx loc sargs ot = match sargs with - | [t] -> let ptp = pexp_parse t in - let ltp = infer_type ptp ctx None in + | [t] -> let ltp = infer_type t ctx None in let meta_ctx, _ = !global_substitution in (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` * is False, for example): Should be a type like `AttributeMap t` @@ -1048,8 +1038,7 @@ let builtin_value_types : ltype option SMap.t ref = ref SMap.empty let sform_built_in ctx loc sargs ot = match !_parsing_internals, sargs with | true, [String (_, name); stp] - -> let ptp = pexp_parse stp in - let ltp = infer_type ptp ctx None in + -> let ltp = infer_type stp ctx None in let meta_ctx, _ = !global_substitution in let ltp' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp in let bi = mkBuiltin ((loc, name), ltp', None) in @@ -1067,8 +1056,7 @@ let sform_built_in ctx loc sargs ot = let sform_datacons ctx loc sargs ot = match sargs with | [t; Symbol ((sloc, cname) as sym)] - -> let pt = pexp_parse t in - let idt, _ = infer pt ctx in + -> let idt, _ = infer t ctx in (mkCons (idt, sym), Lazy)

| [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; @@ -1122,10 +1110,8 @@ let sform_typecons ctx loc sargs ot =

let sform_hastype ctx loc sargs ot = match sargs with - | [se; st] -> let pe = pexp_parse se in - let pt = pexp_parse st in - let lt = infer_type pt ctx None in - let le = check pe lt ctx in + | [se; st] -> let lt = infer_type st ctx None in + let le = check se lt ctx in (le, Inferred lt) | _ -> sexp_error loc "##_:_ takes two arguments"; sform_dummy_ret loc @@ -1136,11 +1122,9 @@ let sform_arrow kind ctx loc sargs ot = -> let (v, st1) = match st1 with | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (Some v, st1) | _ -> (None, st1) in - let pt1 = pexp_parse st1 in - let pt2 = pexp_parse st2 in - let lt1 = infer_type pt1 ctx v in + let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in - let lt2 = infer_type pt2 nctx None in + let lt2 = infer_type st2 nctx None in (mkArrow (kind, v, lt1, loc, lt2), Lazy) | _ -> sexp_error loc "##_->_ takes two arguments"; sform_dummy_ret loc @@ -1156,10 +1140,9 @@ let sform_lambda kind ctx loc sargs ot' = match sargs with | [sargs; sbody] -> let sargs = sexp_p_list sargs ["_:_"] in - let pbody = pexp_parse sbody in

let rec do_all_args sargs ctx ot = match sargs with - | [] -> elaborate ctx pbody ot + | [] -> elaborate ctx sbody ot | sarg :: sargs -> let (arg, ost1) = match sarg with | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (arg, Some st) @@ -1169,7 +1152,7 @@ let sform_lambda kind ctx loc sargs ot' = ((dummy_location, "_"), None) in

let olt1 = match ost1 with - | Some st -> Some (infer_type (pexp_parse st) ctx (Some arg)) + | Some st -> Some (infer_type st ctx (Some arg)) | _ -> None in

let lt1, olt2 = @@ -1214,14 +1197,13 @@ 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) + -> (pexp_p_pat pat, 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 + (Ppatany l, Symbol (l, "?")) 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 + let le = check_case t (loc, se, pcases) ctx in (le, match ot with Some _ -> Checked | None -> Inferred t)

(* In case there are no branches, pretend there was a | anyway. *) @@ -1232,10 +1214,9 @@ let rec sform_case ctx loc sargs ot = match sargs with 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 bdy, ltp = infer sbody 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)) @@ -1250,8 +1231,7 @@ let sform_letin ctx loc sargs ot = match sargs with * allow such a lambda. *) let sform_type ctx loc sargs ot = match sargs with - | [l] -> let l = pexp_parse l in - let l, _ = infer l ctx in + | [l] -> let l, _ = infer l ctx in (mkSort (loc, Stype l), Inferred (mkSort (loc, Stype (SortLevel (SLsucc l))))) | _ -> sexp_error loc "##Type_ expects one argument";

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -36,78 +36,55 @@ type pvar = symbol (* type sort = Type | Ext *) (* type tag = string *)

-type pexp = - (* | Psort of location * sort *) - | Pimm of sexp (* Used for strings, ... *) - and ppat = (* This data type allows nested patterns, but in reality we don't * support them. I.e. we don't want Ppatcons within Ppatcons. *) | Ppatany of location | Ppatsym of pvar (* A named default pattern, or a 0-ary constructor. *) - | Ppatcons of pexp * (symbol option * ppat) list + | Ppatcons of sexp * (symbol option * ppat) list

and pdecl = - | Ptype of symbol * pexp (* identifier : expr *) - | Pexpr of symbol * pexp (* identifier = expr *) + | Ptype of symbol * sexp (* identifier : expr *) + | Pexpr of symbol * sexp (* identifier = expr *) | Pmcall of symbol * sexp list (* identifier [sexp] *)

-let rec pexp_location e = - match e with - (* | Psort (l,_) -> l *) - | Pimm s -> sexp_location s - -let pexp_name e = - match e with - | Pimm _ -> "Pimm" - let rec pexp_pat_location e = match e with | Ppatany l -> l | Ppatsym (l,_) -> l - | Ppatcons (e, _) -> pexp_location e - -(* In the following "pexp_p" the prefix for "parse a sexp, returning a pexp" - * and "pexp_u" is the prefix for "unparse a pexp, returning a sexp". *) -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 _ | Symbol _) -> Pimm s - | Node (f, []) -> pexp_parse f - | Node _ -> Pimm s - -and pexp_p_actual_arg arg : (arg_kind * pvar option * pexp) = + | Ppatcons (e, _) -> sexp_location e + +and pexp_p_actual_arg arg : (arg_kind * pvar option * sexp) = match arg with | Node (Symbol (_, ":≡"), [Symbol s; e]) - -> (Aerasable, Some s, pexp_parse e) + -> (Aerasable, Some s, e) | Node (Symbol (_, ":="), [Symbol s; e]) - -> (Aimplicit, Some s, pexp_parse e) + -> (Aimplicit, Some s, e) | Node (Symbol (_, ":-"), [Symbol s; e]) - -> (Aexplicit, Some s, pexp_parse e) - | e -> (Aexplicit, None, pexp_parse e) + -> (Aexplicit, Some s, e) + | e -> (Aexplicit, None, e)

-and pexp_p_formal_arg arg : (arg_kind * pvar * pexp option) = +and pexp_p_formal_arg arg : (arg_kind * pvar * sexp option) = match arg with | Node (Symbol (_, "_:::_"), [Symbol s; e]) - -> (Aerasable, s, Some (pexp_parse e)) + -> (Aerasable, s, Some e) | Node (Symbol (_, "_::_"), [Symbol s; e]) - -> (Aimplicit, s, Some (pexp_parse e)) + -> (Aimplicit, s, Some e) | Node (Symbol (_, "_:_"), [Symbol s; e]) - -> (Aexplicit, s, Some (pexp_parse e)) + -> (Aexplicit, s, Some e) | Symbol s -> (Aexplicit, s, None) | _ -> sexp_print arg; (pexp_error (sexp_location arg) "Unrecognized formal arg"); (Aexplicit, (sexp_location arg, "{arg}"), None)

-and pexp_u_formal_arg (arg : arg_kind * pvar * pexp option) = +and pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with | (Aexplicit, s, None) -> Symbol s | (ak, ((l,_) as s), t) -> Node (Symbol (l, match ak with Aerasable -> ":::" | Aimplicit -> "::" | Aexplicit -> ":"), - [Symbol s; match t with Some e -> pexp_unparse e + [Symbol s; match t with Some e -> e | None -> Symbol (l, "_")])

and pexp_p_id (x : location * string) : (location * string) option = @@ -122,21 +99,21 @@ and pexp_u_id (x : (location * string) option) : (location * string) =

and pexp_p_ind_arg s = match s with | Node (Symbol (_,"_:_"), [Symbol s; t]) - -> (Aexplicit, pexp_p_id s, pexp_parse t) + -> (Aexplicit, pexp_p_id s, t) | Node (Symbol (_,"_::_"), [Symbol s; t]) - -> (Aimplicit, pexp_p_id s, pexp_parse t) + -> (Aimplicit, pexp_p_id s, t) | Node (Symbol (_,"_:::_"), [Symbol s; t]) - -> (Aerasable, pexp_p_id s, pexp_parse t) - | _ -> (Aexplicit, None, pexp_parse s) + -> (Aerasable, pexp_p_id s, t) + | _ -> (Aexplicit, None, s)

and pexp_u_ind_arg arg = match arg with - | (Aexplicit, None, t) -> pexp_unparse t + | (Aexplicit, None, t) -> t | (k, s, t) -> let (l,_) as id = pexp_u_id s in Node (Symbol (l, match k with Aexplicit -> "_:_" | Aimplicit -> "_::_" | Aerasable -> "_:::_"), - [Symbol id; pexp_unparse t]) + [Symbol id; t])

and pexp_p_pat_arg (s : sexp) = match s with | Symbol _ -> (None, pexp_p_pat s) @@ -158,28 +135,28 @@ and pexp_p_pat (s : sexp) : ppat = match s with | Symbol (l, "_") -> Ppatany l | Symbol s -> Ppatsym s | Node (c, args) - -> Ppatcons (pexp_parse c, List.map pexp_p_pat_arg args) + -> Ppatcons (c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in pexp_error l "Unknown pattern"; Ppatany l

and pexp_u_pat (p : ppat) : sexp = match p with | Ppatany l -> Symbol (l, "_") | Ppatsym s -> Symbol s - | Ppatcons (c, args) -> Node (pexp_unparse c, List.map pexp_u_pat_arg args) + | Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args)

and pexp_p_decls e: pdecl list = match e with | Symbol (_, "") -> [] | Node (Symbol (_, ("_;_" | "_;" | ";_")), decls) -> List.concat (List.map pexp_p_decls decls) - | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, pexp_parse t)] - | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, pexp_parse t)] + | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, t)] + | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, t)] | Node (Symbol (l, "_=_"), [Node (Symbol s, args) as d; t]) -> - [Pexpr(s, Pimm (Node (Symbol (sexp_location d, "lambda_->_"), - [(match args with - | [] -> Sexp.dummy_epsilon - | arg::args -> Node (arg, args)); - t])))] + [Pexpr (s, Node (Symbol (sexp_location d, "lambda_->_"), + [(match args with + | [] -> Sexp.dummy_epsilon + | arg::args -> Node (arg, args)); + t]))] (* everything else is considered a macro * An error will be produced during lexp_parsing if the macro does not exist * once expanded the Pmcall macro will produce a list of pdecl *) @@ -188,19 +165,13 @@ and pexp_p_decls e: pdecl list = print_string ((sexp_name e) ^ ": ""); sexp_print e; print_string ""\n"; pexp_error (sexp_location e) ("Unknown declaration"); []

-and pexp_unparse (e : pexp) : sexp = - match e with - (* | Psort (l,Ext) -> Symbol (l, "%Ext%") *) - (* | Psort (l,Type) -> Symbol (l, "%Type%") *) - | Pimm s -> s - and pexp_u_decl decl = match decl with | Pexpr (s, v) -> - Node (Symbol (dummy_location, "_=_"), [Symbol s; pexp_unparse v]) + Node (Symbol (dummy_location, "_=_"), [Symbol s; v])

| Ptype (s, v) -> - Node (Symbol (dummy_location, "_:_"), [Symbol s; pexp_unparse v]) + Node (Symbol (dummy_location, "_:_"), [Symbol s; v])

| Pmcall(s, args) -> Node (Symbol s, args) @@ -212,13 +183,6 @@ and pexp_u_decls (ds: pdecl list) = | _ -> Node (Symbol (dummy_location, "_;_"), List.map pexp_u_decl ds)

-and pexp_string e = sexp_string (pexp_unparse e) -and pexp_print e = print_string (pexp_string e) - -(* Parse All Pexp as a list *) -let pexp_parse_all (nodes: sexp list) = - List.map pexp_parse nodes - let pexp_decls_all (nodes: sexp list): pdecl list = let rec loop nodes acc = match nodes with @@ -235,8 +199,7 @@ let pexp_decls_all (nodes: sexp list): pdecl list = (* Lexp helper *) let _pexp_expr_str (str: string) (tenv: token_env) (grm: grammar) (limit: string option) = - let sxps = _sexp_parse_str str tenv grm limit in - pexp_parse_all sxps + _sexp_parse_str str tenv grm limit

(* specialized version *) let pexp_expr_str str =

View it on GitLab: https://gitlab.com/monnier/typer/commit/79cd9b8661fb7d5b4a83e698d1b45f1b52d2...