Stefan pushed to branch master at Stefan / Typer

Commits: e060bdba by Stefan Monnier at 2017-07-01T00:18:01-04:00 Use sexps rather than pdecls

* src/lexp.ml (lexp_unparse.sdecls): Skip pexp_u_decls.

* src/elab.ml (instantiate_implicit): Use Eval.varname. (lexp_decls_macro): Don't return a new context any more. Return a sexp rather than a list of pdecls. (lexp_check_decls): Take a list of sexps rather than a list of pdecls. Simplify the macro call case since it can't return a new ctx any more. (lexp_p_decls): Take a list of sexps rather than a list of pdecls. (sform_letin, default_ectx.read_file, _lexp_decl_str): Pass the sexps directly to lexp_p_decls.

* src/debug_util.ml (format_source): Pass the sexps directly to lexp_p_decls. (mdecl, lexp_detect_recursive): Remove rather than fix. (main): Remove "pexp" debugging because there's no pexp any more. Remove "merge-debug" debugging because it's broken and it's not clear how to fix it. Pass the sexps directly to lexp_p_decls.

* src/debug.ml (debug_pexp_decls): Remove; there's no pexp to debug any more. (debug_pexp_print_all): Remove unused.

* src/REPL.ml (ipexp_parse): Use sexp rather then pdecl. (_raw_eval): Pass the sexps directly to lexp_p_decls.

* src/pexp.ml (pdecl, pexp_p_decls, pexp_u_decl, pexp_u_decls) (pexp_decls_all, _pexp_decl_str, pexp_decl_str): Remove.

- - - - -

6 changed files:

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

Changes:

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -105,18 +105,18 @@ 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 * sexp list) = +let ipexp_parse (sxps: sexp list): (sexp list * sexp list) = let rec _pxp_parse sxps dacc pacc = match sxps with | [] -> (List.rev dacc), (List.rev pacc) | sxp::tl -> match sxp with (* Declaration *) | Node (Symbol (_, ("_=_" | "_:_")), [Symbol s; t]) -> - _pxp_parse tl (List.append (pexp_p_decls sxp) dacc) pacc + _pxp_parse tl (sxp :: dacc) pacc

(* f arg1 arg2 = function body; *) | Node (Symbol (_, "_=_"), [Node (Symbol s, args); t]) -> - _pxp_parse tl (List.append (pexp_p_decls sxp) dacc) pacc + _pxp_parse tl (sxp :: dacc) pacc

(* Expression *) | _ -> _pxp_parse tl dacc (sxp::pacc) in @@ -161,8 +161,7 @@ let _raw_eval f str lctx rctx = let pres = (f str) in let sxps = lex default_stt pres in let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in - let pxps = pexp_decls_all nods in - let lxps, lctx = Elab.lexp_p_decls pxps lctx in + let lxps, lctx = Elab.lexp_p_decls nods lctx in let elxps = List.map OL.clean_decls lxps in (* At this point, `elxps` is a `(vname * elexp) list list`, where: * - each `(vname * elexp)` is a definition

===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -122,38 +122,6 @@ let debug_pexp_print 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 - - List.iter (fun e -> - print_string " "; - - let _ = match e with - | Pexpr ((l, name), pxp) -> - lalign_print_string (sexp_name pxp) 15; - loc_print l; print_string " = "; sexp_print pxp - - | Ptype ((l, name), 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; - loc_print l; sexp_print (Node(Symbol(l, op), args)) in - - print_string "\n") - - decls - - -(* Print a list of pexp *) -let debug_pexp_print_all pexps = - List.iter - (fun px -> - debug_pexp_print px; - print_string "\n") - pexps - let debug_lexp_decls decls = let sep = " : " in List.iter (fun e ->

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -194,9 +194,8 @@ let format_source () = let pretoks = prelex_file filename in let toks = lex default_stt pretoks in let nodes = sexp_parse_all_to_list default_grammar toks (Some ";") in - let pexps = pexp_decls_all nodes in let ctx = Elab.default_ectx in - let lexps, _ = Elab.lexp_p_decls pexps ctx in + let lexps, _ = Elab.lexp_p_decls nodes ctx in

print_string (make_sep '-'); print_string "\n";

@@ -214,88 +213,6 @@ let format_source () = ) else (List.iter (fun str -> print_string str; print_string "\n") result;)

-(* merged declaration, allow us to process declaration in multiple pass *) -(* first detect recursive decls then lexp decls*) -type mdecl = - | Ldecl of symbol * sexp option * sexp option - | Lmcall of symbol * sexp list - -let lexp_detect_recursive pdecls = - (* Pack mutually recursive declarations *) - (* mutually recursive def must use forward declarations *) - - let decls = ref [] in - let pending = ref [] in - let merged = ref [] in - - List.iter (fun expr -> - match expr with - | Pexpr((l, s), pxp) ->( - let was_forward = (List.exists - (fun (Ldecl((_, p), _, _)) -> p = s) !pending) in - - let is_empty = (List.length !pending) = 0 in - let is_one = (List.length !pending) = 1 in - - (* This is a standard declaration: not forwarded *) - if (was_forward = false) && is_empty then( - decls := [Ldecl((l, s), Some pxp, None)]::!decls; - ) - (* This is an annotated expression - * or the last element of a mutually rec definition *) - else if (was_forward && is_one) then ( - - (* we know that names match already *) - let ptp = (match (!pending) with - | Ldecl(_, _, ptp)::[] -> ptp - (* we already checked that len(pending) == 1*) - | Ldecl(_, _, ptp)::_ -> typer_unreachable "Unreachable" - | [] -> typer_unreachable "Unreachable" - | Lmcall _ :: _ -> typer_unreachable "Unreachable") in - - (* add declaration to merged decl *) - merged := Ldecl((l, s), Some pxp, ptp)::(!merged); - - (* append decls *) - decls := (List.rev !merged)::!decls; - - (* Reset State *) - pending := []; - merged := []; - ) - (* This is a mutually recursive definition *) - else ( - (* get pending element and remove it from the list *) - let elem, lst = List.partition - (fun (Ldecl((_, n), _, _)) -> n = s) !pending in - - let _ = (match elem with - (* nothing to merge *) - | [] -> - merged := Ldecl((l, s), Some pxp, None)::!merged; - - (* append new element to merged list *) - | Ldecl((l, s), _, Some ptp)::[] -> - merged := Ldecl((l, s), Some pxp, (Some ptp))::!merged; - - (* s should be unique *) - | _ -> error l "declaration must be unique") in - - (* element is not pending anymore *) - pending := lst; - )) - - | Ptype((l, s), ptp) -> - pending := Ldecl((l, s), None, Some ptp)::!pending - - (* macro will be handled later *) - | Pmcall(a, sargs) -> - decls := [Lmcall(a, sargs)]::!decls; - - ) pdecls; - - (List.rev !decls) - let main () = parse_args ();

@@ -345,50 +262,14 @@ let main () =

(* Parse All Declaration *) print_string yellow; - let pexps = pexp_decls_all nodes in print_string reset;

- (if (get_p_option "pexp") then( - print_string (make_title " Pexp "); - debug_pexp_decls pexps; print_string "\n")); - (* get lexp *) let octx = Elab.default_ectx in

- (* Debug declarations merging *) - (if (get_p_option "merge-debug") then( - let merged = lexp_detect_recursive pexps in - - List.iter (fun lst -> - print_string (make_line '-' 80); - print_string "\n"; - - List.iter (fun v -> - match v with - | Ldecl((l, s), pxp, ptp) -> ( - lalign_print_string s 20; - - let _ = match ptp with - | Some pxp -> sexp_print pxp; - | None -> print_string " " in - - print_string "\n"; - lalign_print_string s 20; - - let _ = match pxp with - | Some pxp -> sexp_print pxp; - | None -> print_string " " in - - print_string "\n") - | Lmcall((l, s), _ ) -> - print_string s; print_string "\n" - ) lst; - - ) merged)); - (* debug lexp parsing once merged *) print_string yellow; - let lexps, nctx = try Elab.lexp_p_decls pexps octx + let lexps, nctx = try Elab.lexp_p_decls nodes octx with e -> print_string reset; raise e in

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -371,7 +371,7 @@ and instantiate_implicit e t ctx = | Arrow ((Aerasable | Aimplicit) as ak, v, t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) - (match v with Some (_, name) -> name | _ -> "v") + (Eval.varname v) t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | _ -> (mkCall (e, List.rev args), t) @@ -821,25 +821,17 @@ and sexp_decls_macro_print sxp_decls = List.iter (fun sxp -> 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) = +and lexp_decls_macro (loc, mname) sargs ctx: sexp = 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 - let decls = match ret with - | Vsexp(sexp) -> sexp - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a sexp") in + match ret with + | Vsexp (sexp) -> sexp + | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a sexp")

- (* read as pexp_declaraton *) - (try pexp_p_decls decls, ctx - (* if an error occur print generated code to ease debugging *) - with e -> - error loc "An error occurred while expanding a macro"; - sexp_decls_macro_print decls; - raise e) - - with e -> - fatal loc ("Macro `" ^ mname ^ "`not found") + with e -> + fatal loc ("Macro `" ^ mname ^ "`not found")

and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) @@ -865,14 +857,14 @@ and lexp_check_decls (ectx : elab_context) (* External context. *)

and lexp_decls_1 - (pdecls : pdecl list) + (sdecls : sexp list) (ectx : elab_context) (* External ctx. *) (nctx : elab_context) (* New context. *) (pending_decls : (location * ltype) SMap.t) (* Pending type decls. *) (pending_defs : (vname * sexp * ltype) list) (* Pending definitions. *) - : (vname * lexp * ltype) list * pdecl list * elab_context = + : (vname * lexp * ltype) list * sexp list * elab_context =

- match pdecls with + match sdecls with | [] -> (if not (SMap.is_empty pending_decls) then let (s, (l, _)) = SMap.choose pending_decls in error l ("Variable `" ^ s ^ "` declared but not defined!") @@ -880,68 +872,88 @@ and lexp_decls_1 assert (pending_defs == [])); [], [], nctx

- | Ptype ((l, vname) as v, ptp) :: pdecls - -> let ltp = infer_type ptp (ectx_new_scope nctx) (Some v) in - if SMap.mem vname pending_decls then - (error l ("Variable `" ^ vname ^ "` declared twice!"); - lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) - else if List.exists (fun ((_, vname'), _, _) -> vname = vname') - pending_defs then - (error l ("Variable `" ^ vname ^ "` already defined!"); - lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) - else lexp_decls_1 pdecls ectx - (env_extend nctx v ForwardRef ltp) - (SMap.add vname (l, ltp) pending_decls) - pending_defs - - | Pexpr ((l, vname) as v, pexp) :: pdecls - when SMap.is_empty pending_decls - -> assert (pending_defs == []); - assert (ectx == nctx); - let (lexp, ltp) = infer pexp (ectx_new_scope nctx) in - (* Lexp decls are always recursive, so we have to shift by 1 to account - * for the extra var (ourselves). *) - [(v, mkSusp lexp (S.shift 1), ltp)], pdecls, - ctx_define nctx v lexp ltp - - | Pexpr ((l, vname) as v, pexp) :: pdecls - -> (try let (_, ltp) = SMap.find vname pending_decls in - let pending_decls = SMap.remove vname pending_decls in - let pending_defs = ((v, pexp, ltp) :: pending_defs) in - if SMap.is_empty pending_decls then - let nctx = ectx_new_scope nctx in - let decls, nctx = lexp_check_decls ectx nctx pending_defs in - decls, pdecls, nctx - else - lexp_decls_1 pdecls ectx nctx pending_decls pending_defs - - with Not_found -> - error l ("`" ^ vname ^ "` defined but not declared!"); - lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) - - | Pmcall ((l, _) as v, sargs) :: pdecls - -> ((* expand macro and get the generated declarations *) - let pdecls', nctx' = lexp_decls_macro v sargs nctx in - - if nctx == nctx' then - (* Plain macro expansion! *) - lexp_decls_1 (List.append pdecls' pdecls) ectx nctx - pending_decls pending_defs - - else if ectx == nctx then - (assert (SMap.is_empty pending_decls); - assert (pending_defs = []); - - lexp_decls_1 (List.append pdecls' pdecls) ectx nctx' - pending_decls pending_defs) - - else fatal l "Context changed in already changed context") - - -and lexp_p_decls pdecls ctx: ((vname * lexp * ltype) list list * elab_context) = - if pdecls = [] then [], ctx else - let decls, pdecls, nctx = lexp_decls_1 pdecls ctx ctx SMap.empty [] in - let declss, nnctx = lexp_p_decls pdecls nctx in + | Symbol (_, "") :: sdecls + -> lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + + | Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls') :: sdecls + -> lexp_decls_1 (List.append sdecls' sdecls) + ectx nctx pending_decls pending_defs + + | Node (Symbol (l, "_:_"), args) :: sdecls + (* FIXME: Move this to a "special form"! *) + -> (match args with + | [Symbol ((l, vname) as v); stp] + -> let ltp = infer_type stp (ectx_new_scope nctx) (Some v) in + if SMap.mem vname pending_decls then + (error l ("Variable `" ^ vname ^ "` declared twice!"); + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + else if List.exists (fun ((_, vname'), _, _) -> vname = vname') + pending_defs then + (error l ("Variable `" ^ vname ^ "` already defined!"); + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + else lexp_decls_1 sdecls ectx + (env_extend nctx v ForwardRef ltp) + (SMap.add vname (l, ltp) pending_decls) + pending_defs + | _ -> error l "Invalid type declaration syntax"; + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + + | Node (Symbol (l, "_=_") as head, args) :: sdecls + (* FIXME: Move this to a "special form"! *) + -> (match args with + | [Symbol ((l, vname) as v); sexp] + when SMap.is_empty pending_decls + -> assert (pending_defs == []); + assert (ectx == nctx); + let (lexp, ltp) = infer sexp (ectx_new_scope nctx) in + (* Lexp decls are always recursive, so we have to shift by 1 to + * account for the extra var (ourselves). *) + [(v, mkSusp lexp (S.shift 1), ltp)], sdecls, + ctx_define nctx v lexp ltp + + | [Symbol ((l, vname) as v); sexp] + -> (try let (_, ltp) = SMap.find vname pending_decls in + let pending_decls = SMap.remove vname pending_decls in + let pending_defs = ((v, sexp, ltp) :: pending_defs) in + if SMap.is_empty pending_decls then + let nctx = ectx_new_scope nctx in + let decls, nctx = lexp_check_decls ectx nctx pending_defs in + decls, sdecls, nctx + else + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + + with Not_found -> + error l ("`" ^ vname ^ "` defined but not declared!"); + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + + | [Node (Symbol s, args) as d; body] + -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) + lexp_decls_1 ((Node (head, + [Symbol s; + Node (Symbol (sexp_location d, "lambda_->_"), + [sexp_u_list args; body])])) + :: sdecls) + ectx nctx pending_decls pending_defs + + | _ -> error l "Invalid definition syntax"; + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + + | Node (Symbol ((l, _) as v), sargs) :: sdecls + -> (* expand macro and get the generated declarations *) + let sdecl' = lexp_decls_macro v sargs nctx in + lexp_decls_1 (sdecl' :: sdecls) ectx nctx + pending_decls pending_defs + + | sexp :: sdecls + -> error (sexp_location sexp) "Invalid declaration syntax"; + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + +and lexp_p_decls (sdecls : sexp list) ctx + : ((vname * lexp * ltype) list list * elab_context) = + match sdecls with + | [] -> [], ctx + | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in + let declss, nnctx = lexp_p_decls sdecls nctx in decls :: declss, nnctx

and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = @@ -1219,8 +1231,7 @@ 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 declss, nctx = lexp_p_decls pdecls ctx in + -> let declss, nctx = lexp_p_decls [sdecls] ctx in (* FIXME: Use `elaborate`. *) let bdy, ltp = infer sbody (ectx_new_scope nctx) in let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in @@ -1308,8 +1319,7 @@ let default_ectx let pres = prelex_file file_name in let sxps = lex default_stt pres in let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in - let pxps = pexp_decls_all nods in - let _, lctx = lexp_p_decls pxps elctx + let _, lctx = lexp_p_decls nods elctx in lctx in

(* Register predef *) @@ -1368,8 +1378,8 @@ let lexp_expr_str str lctx = _lexp_expr_str str default_stt default_grammar (Some ";") lctx

let _lexp_decl_str (str: string) tenv grm limit ctx = - let pxps = _pexp_decl_str str tenv grm limit in - lexp_p_decls pxps ctx + let sdecls = _sexp_parse_str str tenv grm limit in + lexp_p_decls sdecls ctx

(* specialized version *) let lexp_decl_str str lctx =

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -380,13 +380,16 @@ let rec lexp_unparse lxp =

| Let (loc, ldecls, body) -> (* (vdef * lexp * ltype) list *) - let pdecls = List.fold_left + let sdecls = List.fold_left (fun acc (vdef, lxp, ltp) - -> Ptype (vdef, lexp_unparse ltp) - :: Pexpr(vdef, lexp_unparse lxp)::acc) + -> Node (Symbol (U.dummy_location, "_=_"), + [Symbol vdef; lexp_unparse ltp]) + :: Node (Symbol (U.dummy_location, "_=_"), + [Symbol vdef; lexp_unparse lxp]) + :: acc) [] ldecls in Node (Symbol (loc, "let_in_"), - [pexp_u_decls pdecls; + [Node (Symbol (U.dummy_location, "_;_"), sdecls); lexp_unparse body])

| Call(lxp, largs) -> (* (arg_kind * lexp) list *)

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

-and ppat = +type 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 sexp * (symbol option * ppat) list

-and pdecl = - | Ptype of symbol * sexp (* identifier : expr *) - | Pexpr of symbol * sexp (* identifier = expr *) - | Pmcall of symbol * sexp list (* identifier [sexp] *) - - let rec pexp_pat_location e = match e with | Ppatany l -> l | Ppatsym (l,_) -> l @@ -134,53 +128,6 @@ and pexp_u_pat (p : ppat) : sexp = match p with | Ppatsym s -> Symbol s | 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, t)] - | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr (s, t)] - | Node (Symbol (l, "_=_"), [Node (Symbol s, args) as d; t]) -> - (* FIXME: Hardcode "lambda_->_"! *) - [Pexpr (s, Node (Symbol (sexp_location d, "lambda_->_"), - [sexp_u_list 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 *) - | Node (Symbol (l, op), args) -> [Pmcall ((l, op), args)] - | _ -> - print_string ((sexp_name e) ^ ": ""); sexp_print e; print_string ""\n"; - pexp_error (sexp_location e) ("Unknown declaration"); [] - -and pexp_u_decl decl = - match decl with - | Pexpr (s, v) -> - Node (Symbol (dummy_location, "_=_"), [Symbol s; v]) - - | Ptype (s, v) -> - Node (Symbol (dummy_location, "_:_"), [Symbol s; v]) - - | Pmcall(s, args) -> - Node (Symbol s, args) - -and pexp_u_decls (ds: pdecl list) = - match ds with - | [] -> dummy_epsilon - | [d] -> pexp_u_decl d - | _ -> Node (Symbol (dummy_location, "_;_"), - List.map pexp_u_decl ds) - -let pexp_decls_all (nodes: sexp list): pdecl list = - let rec loop nodes acc = - match nodes with - | [] -> acc - | hd::tl -> - let r = pexp_p_decls hd in - let nacc = List.append acc r in - loop tl nacc in - loop nodes [] - (* String Parsing * --------------------------------------------------------- *)

@@ -192,12 +139,3 @@ let _pexp_expr_str (str: string) (tenv: token_env) (* specialized version *) let pexp_expr_str str = _pexp_expr_str str default_stt default_grammar (Some ";") - -let _pexp_decl_str (str: string) tenv grm limit = - let sxps = _sexp_parse_str str tenv grm limit in - pexp_decls_all sxps - -(* specialized version *) -let pexp_decl_str str = - _pexp_decl_str str default_stt default_grammar (Some ";") -

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

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/e060bdbadf9b5c64892f86f5b3d071a088cc... You're receiving this email because of your account on gitlab.com.