Simon Génier pushed to branch simon--sexp-node-location at Stefan / Typer

Commits: 8b7e3b1f by Simon Génier at 2023-02-19T14:08:42-05:00 Get rid of empty_args_are_not_args.

This configuration was used to toggle the behaviour of the sexp parser for a transition in syntax that was completed years ago. Today it is always false and we can get rid of it to simplify the maintenance of the parser.

- - - - - a61d6455 by Simon Génier at 2023-02-19T14:43:00-05:00 Merge branches for non-operators in the sexp parser.

There two ways to mark a symbol as a non-operator. * Simply not adding it to the grammar. * Adding to the grammar with neither a left nor right precedence.

The two cases were handled in the same way, but the code was duplicated. This patch merges them.

- - - - - e660eda7 by Simon Génier at 2023-02-19T16:08:58-05:00 Add locations to nodes.

- - - - - da30313c by Simon Génier at 2023-02-19T16:10:45-05:00 Track locations during parsing instead of recomputing them.

- - - - -

15 changed files:

- src/REPL.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/eval.ml - src/grammar.ml - src/lexer.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/sexp.ml - src/source.ml - + src/string.ml - tests/lexer_test.ml - tests/sexp_test.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -114,9 +114,9 @@ let eval_interactive | [] -> (List.rev decls, List.rev exprs) | sexp :: sexps -> (match sexp with - | Node (Symbol (_, ("_=_" | "_:_")), [Symbol _; _]) + | Node (_, Symbol (_, ("_=_" | "_:_")), [Symbol _; _]) -> loop sexps (sexp :: decls) exprs - | Node (Symbol (_, ("_=_")), [Node _; _]) + | Node (_, Symbol (_, ("_=_")), [Node _; _]) -> loop sexps (sexp :: decls) exprs | _ -> loop sexps decls (sexp :: exprs))

===================================== src/debruijn.ml ===================================== @@ -191,7 +191,7 @@ type typeclass_ctx (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context - = Grammar.grammar * senv_type * lexp_context * meta_scope * typeclass_ctx + = Grammar.t * senv_type * lexp_context * meta_scope * typeclass_ctx

(* Elab context getters *)

@@ -199,7 +199,7 @@ let get_size (ctx : elab_context) = let (_, (n, _), lctx, _, _) = ctx in assert (n = M.length lctx); n

-let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = +let ectx_get_grammar (ectx : elab_context) : Grammar.t = let (grm,_, _, _, _) = ectx in grm

let ectx_get_senv (ectx : elab_context) : senv_type = @@ -223,7 +223,7 @@ let ectx_to_tcctx (ectx : elab_context) : typeclass_ctx =

(* Functional updates *)

-let ectx_set_grammar (grm : Grammar.grammar) (ectx : elab_context) : elab_context = +let ectx_set_grammar (grm : Grammar.t) (ectx : elab_context) : elab_context = let (_, senv, lctx, sl, tcctx) = ectx in (grm, senv, lctx, sl, tcctx)

===================================== src/debug.ml ===================================== @@ -91,8 +91,8 @@ let debug_sexp_print sexp = | Float(loc, x) -> print_info "Float: " loc; print_float x

- | Node(f, args) - -> print_info "Node: " (sexp_location f); + | Node(location, f, args) + -> print_info "Node: " location; sexp_print f; print_string " ["; List.iter (fun sexp -> print_string " "; sexp_print sexp) args;

===================================== src/elab.ml ===================================== @@ -338,7 +338,7 @@ let sdform_define_operator (ctx : elab_context) loc sargs : elab_context = | Integer (_, n) -> Some (Z.to_int n) | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in let grm = ectx_get_grammar ctx in - ectx_set_grammar (SMap.add name (level l, level r) grm) ctx + ectx_set_grammar (Grammar.add name (level l, level r) grm) ctx | [o; _; _] -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ @@ -608,18 +608,18 @@ let rec elaborate ctx se ot = (* Rewrite SYM to `typer-identifier SYM`. *) | Symbol ((loc, name) as _id) -> if not (name = "typer-identifier") then - elaborate ctx (Node (Symbol (loc, "typer-identifier"), [se])) ot + elaborate ctx (Node (loc, Symbol (loc, "typer-identifier"), [se])) ot (* Break the inf-recursion! *) else elab_varref ctx (se, name)

(* Rewrite IMM to `typer-immediate IMM`. *) | (Integer _ | Float _ | String _ | Block _) -> let l = sexp_location se in - elaborate ctx (Node (Symbol (l, "typer-immediate"), [se])) ot + elaborate ctx (Node (l, Symbol (l, "typer-immediate"), [se])) ot

- | Node (se, []) -> elaborate ctx se ot + | Node (_, se, []) -> elaborate ctx se ot

- | Node (func, args) + | Node (_, func, args) -> let (f, t) as ft = infer func ctx in if (OL.conv_p (ectx_to_lctx ctx) t type_special_form) then elab_special_form ctx f args ot @@ -800,7 +800,7 @@ and check_case rtype (loc, target, ppatterns) ctx =

let uniqueness_warn pat = warning - ~loc:(sexp_location (pexp_pat_location pat)) + ~loc:(pexp_pat_location pat) "Pattern %s is a duplicate. It will override a previous pattern." (pat_string pat) in @@ -992,7 +992,7 @@ and check_case rtype (loc, target, ppatterns) ctx = add_branch (Symbol (sexp_location l, name)) [] else add_default var (* A named default branch. *)

- | Ppatcons (pctor, pargs) -> add_branch pctor pargs in + | Ppatcons (_, pctor, pargs) -> add_branch pctor pargs in

let (lpattern, dflt) = List.fold_left fold_fun (SMap.empty, None) ppatterns in @@ -1042,7 +1042,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (SMap.remove aname pending) (L.mkSusp ret_type (S.substitute larg))

- | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, + | Node (_, Symbol (_, "_:=_"), [Symbol (_, aname); sarg]) :: sargs, Arrow (_, ak, _, arg_type, ret_type) when (aname = "_") (* Explicit-implicit argument. *) @@ -1050,13 +1050,13 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = handle_fun_args ((ak, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg))

- | (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs, + | Node (_, Symbol (_, "_:=_"), [Symbol (l, aname); sarg]) :: sargs, Arrow _ -> if SMap.mem aname pending then sexp_error l {|Duplicate explicit arg "%s"|} aname; handle_fun_args largs sargs (SMap.add aname sarg pending) ltp

- | (Node (Symbol (_, "_:=_"), Symbol (l, aname) :: _)) :: sargs, _ + | Node (_, Symbol (_, "_:=_"), Symbol (l, aname) :: _) :: sargs, _ -> sexp_error l {|Explicit arg "%s" to non-function (type = %s)|} aname (lexp_string ltp); @@ -1327,10 +1327,10 @@ and lexp_decls_1 | Some (Symbol (_, "")) -> recur [] nctx pending_decls pending_defs

- | Some (Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls')) + | Some (Node (_, Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls')) -> recur sdecls' nctx pending_decls pending_defs

- | Some (Node (Symbol (loc, "_:_"), args) as thesexp) + | Some (Node (_, Symbol (loc, "_:_"), args) as thesexp) (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol (loc, vname); stp] @@ -1367,7 +1367,7 @@ and lexp_decls_1 (sexp_string thesexp); recur [] nctx pending_decls pending_defs)

- | Some (Node (Symbol (loc, "_=_") as head, args) as thesexp) + | Some (Node (_, (Symbol (loc, "_=_") as head), args) as thesexp) (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol ((_l, vname)); sexp] @@ -1397,12 +1397,14 @@ and lexp_decls_1 (error ~loc {|"%s" defined but not declared!|} vname; recur [] nctx pending_decls pending_defs)

- | [Node (Symbol s, args) as d; body] + | [Node (location, Symbol s, args) as d; body] -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) - recur [Node (head, + recur [Node (location, + head, [Symbol s; - Node (Symbol (sexp_location d, "lambda_->_"), - [sexp_u_list args; body])])] + Node (location, + Symbol (sexp_location d, "lambda_->_"), + [sexp_u_list args location; body])])] nctx pending_decls pending_defs

| _ @@ -1413,7 +1415,7 @@ and lexp_decls_1 | Some sexp -> (* sdforms or macros *) let sxp, sargs = match sexp with - | Node (sxp, sargs) -> sxp, sargs + | Node (_, sxp, sargs) -> sxp, sargs | _ -> sexp, [] in let lctx = ectx_to_lctx nctx in let (f, t) = infer sxp nctx in @@ -1527,13 +1529,13 @@ let elab_colon_to_ak k = match k with | _ -> Anormal

let elab_datacons_arg s = match s with - | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol s; t]) + | Node (_, Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol s; t]) -> (elab_colon_to_ak k, elab_p_id s, t) | _ -> (Anormal, (s, None), s)

let elab_typecons_arg arg : (arg_kind * vname * sexp option) = match arg with - | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (_l,name); e]) + | Node (_, Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (_l,name); e]) -> (elab_colon_to_ak k, (arg, Some name), Some e) | Symbol (_l, name) -> (Anormal, (arg, Some name), None) @@ -1547,7 +1549,7 @@ let sform_typecons ctx loc sargs _ot = | [] -> sexp_error (sexp_location loc) "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) | formals :: constrs -> let (label, formals) = match formals with - | Node (label, formals) -> (label, formals) + | Node (_, label, formals) -> (label, formals) | _ -> (formals, []) in let label = match label with | Symbol label -> label @@ -1575,7 +1577,7 @@ let sform_typecons ctx loc sargs _ot = (fun case pcases -> match case with (* read Constructor name + args => Type ((Symbol * args) list) *) - | Node (Symbol s, cases) + | Node (_, Symbol s, cases) -> (s, List.map elab_datacons_arg cases)::pcases (* This is a constructor with no args *) | Symbol s -> (s, [])::pcases @@ -1600,7 +1602,7 @@ let sform_arrow kind ctx loc sargs _ot = match sargs with | [st1; st2] -> let (v, st1) = match st1 with - | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1) + | Node (_, Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1) | _ -> ((st1, None), st1) in let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in @@ -1705,7 +1707,7 @@ let rec sform_lambda kind ctx loc sargs ot = match sargs with | [sarg; sbody] -> let (arg, ost1) = match sarg with - | Node (Symbol (_, "_:_"), [Symbol arg; st]) -> (elab_p_id arg, Some st) + | Node (_, Symbol (_, "_:_"), [Symbol arg; st]) -> (elab_p_id arg, Some st) | Symbol arg -> (elab_p_id arg, None) | _ -> sexp_error (sexp_location sarg) "Unrecognized lambda argument"; @@ -1777,10 +1779,10 @@ let rec sform_lambda kind ctx loc sargs ot = | Aerasable -> "≡>"); sform_dummy_ret ctx loc

-let rec sform_case ctx loc sargs ot = match sargs with - | [Node (Symbol (_, "_|_"), se :: scases)] +let rec sform_case ctx sinfo sargs ot = match sargs with + | [Node (_, Symbol (_, "_|_"), se :: scases)] -> let parse_case branch = match branch with - | Node (Symbol (_, "_=>_"), [pat; code]) + | Node (_, Symbol (_, "_=>_"), [pat; code]) -> (pexp_p_pat pat, code) | _ -> let l = (sexp_location branch) in sexp_error l "Unrecognized simple case branch"; @@ -1788,14 +1790,17 @@ let rec sform_case ctx loc sargs ot = match sargs with let pcases = List.map parse_case scases in let t = match ot with | Some t -> t - | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc in - let le = check_case t (loc, se, pcases) ctx in + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) sinfo in + let le = check_case t (sinfo, se, 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 (sexp_location loc, "_|_"), sargs)] ot - | _ -> sexp_error (sexp_location loc) "Unrecognized case expression"; - sform_dummy_ret ctx loc + | [_e] + -> let loc = sexp_location sinfo in + sform_case ctx sinfo [Node (loc, Symbol (loc, "_|_"), sargs)] ot + | _ + -> sexp_error (sexp_location sinfo) "Unrecognized case expression"; + sform_dummy_ret ctx sinfo

let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] @@ -1829,9 +1834,9 @@ let rec infer_level ctx se : lexp = match se with | Symbol (_, "z") -> mkSortLevel SLz | Symbol _ -> check se type_level ctx - | Node (Symbol (_, "s"), [se]) + | Node (_, Symbol (_, "s"), [se]) -> mkSortLevel (SLsucc (infer_level ctx se)) - | Node (Symbol (_, "_∪_"), [se1; se2]) + | Node (_, Symbol (_, "_∪_"), [se1; se2]) -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) | _ -> let l = (sexp_location se) in (sexp_error l "Unrecognized TypeLevel: %s" (sexp_string se);

===================================== src/eval.ml ===================================== @@ -336,7 +336,7 @@ let make_node loc _depth args_val = match args_val with {|Sexp.node expects "List Sexp" second as arguments\n%s|} (trace_value v) in - Vsexp (Node (op, List.map unwrap_sexp args)) + Vsexp (Node (loc, op, List.map unwrap_sexp args))

| _ -> error loc "Sexp.node expects a `Sexp` and a `List Sexp`"

@@ -645,7 +645,7 @@ and sexp_dispatch loc depth args = in

match sxp with - | Node (op, s) -> eval_call nd [Vsexp op; o2v_list s] + | Node (_, op, s) -> eval_call nd [Vsexp op; o2v_list s] | Symbol (_ , s) -> eval_call sym [Vstring s] | String (_ , s) -> eval_call str [Vstring s] | Integer (_ , i) -> eval_call it [Vinteger i]

===================================== src/grammar.ml ===================================== @@ -36,7 +36,15 @@

open Util

-type grammar = (int option * int option) SMap.t +type t = Grammar of (int option * int option) SMap.t [@@unboxed] + +let add (name : string) (p : int option * int option) (Grammar (ps) : t) : t = + let ps' = SMap.add name p ps in + Grammar (ps') + +let find (name : string) (Grammar (ps) : t) : int option * int option = + try SMap.find name ps with + | Not_found -> (None, None)

(* A token_end array indicates the few chars which are separate tokens, * even if not surrounded by spaces, such as '(', ')', and ';'. @@ -63,7 +71,8 @@ let default_stt : token_env = (if (numberp (nth 2 x)) (format "Some %d" (nth 2 x)) "None") ");\n"))) *) -let default_grammar : grammar = +let default_grammar : t = + let precedences = List.fold_left (fun g (n, ll, rl) -> SMap.add n (ll, rl) g) SMap.empty [("^", Some 166, Some 153); @@ -101,3 +110,5 @@ let default_grammar : grammar = (* ("if", None, Some 2); *) ("(", None, Some 0) ] + in + Grammar (precedences)

===================================== src/lexer.ml ===================================== @@ -112,7 +112,7 @@ let lex_symbol else let raw_name, location = source#slice start_point in let name = if escaped then unescape raw_name else raw_name in - hSymbol (location, name) + Sexp.symbol ~location name in

let rec loop start_point prec lf (escaped : bool) = @@ -143,11 +143,20 @@ let lex_symbol if lhs_p || rhs_p || lf dummy_epsilon <> dummy_epsilon then let op_text, op_location = source#slice op_point in - let op = hSymbol (op_location, Printf.sprintf "__%s__" op_text) in + let op = + Sexp.symbol + ~location:op_location (Printf.sprintf "__%s__" op_text) + in + let location s = + s + |> sexp_location + |> Source.Location.extend op_location + |> Source.Location.extend (sexp_location left) + in let lf' = if prec' > prec - then fun s -> lf (Node (op, [left; s])) - else fun s -> Node (op, [lf left; s]) + then fun s -> lf (Node (location s, op, [left; s])) + else fun s -> Node (location s, op, [lf left; s]) in loop source#point prec' lf' false else @@ -197,7 +206,7 @@ let split_presymbol | _ when token_env.(Char.code c) = CKseparate -> source#advance; let name, location = source#slice start_point in - hSymbol (location, name) + Sexp.symbol ~location name

| _ -> lex_symbol token_env source start_point @@ -217,8 +226,8 @@ let lex (token_env : token_env) (pretokens : pretoken list) : sexp list = | Prestring (location, text) :: pretokens' -> loop pretokens' (String (location, text) :: acc)

- | Pretoken ({file; start_line = l; start_column = c; _}, name) :: pretokens' - -> let source = new Source.source_string ~file ~line:l ~column:c name in + | Pretoken ({file; start = {line; column; _}; _}, name) :: pretokens' + -> let source = new Source.source_string ~file ~line ~column name in let tokens = split_presymbol token_env source in loop pretokens' (List.rev_append tokens acc) in

===================================== src/lexp.ml ===================================== @@ -538,9 +538,8 @@ let rec lexp_sinfo s = | Proj (l,_,_) -> l

-let lexp_location e = - sexp_location (lexp_sinfo e) - +let lexp_location (e : lexp) : Source.Location.t = + e |> lexp_sinfo |> sexp_location

(********* Normalizing a term *********)

@@ -689,123 +688,164 @@ let rec lexp_unparse lxp = | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) | Var ((loc, name), _) -> Symbol (sexp_location loc, maybename name) - | Proj (l,lxp,(loc,str) ) - -> Node (Symbol (sexp_location l, "__.__"), - [(lexp_unparse lxp);(Symbol (loc,str))]) + | Proj (sinfo, lxp, (loc, str)) + -> let location = sexp_location sinfo in + Node (location, + Symbol (location, "__.__"), + [(lexp_unparse lxp); (Symbol (loc, str))]) | Cons (t, (l, name)) - -> Node (sdatacons, - [lexp_unparse t; Symbol (l, name)]) + -> Node (l, sdatacons, [lexp_unparse t; Symbol (l, name)]) | Lambda (kind, vdef, ltp, body) -> let l = lexp_location lxp in - let st = lexp_unparse ltp in - Node (Symbol (l, match kind with - | Anormal -> "lambda_->_" - | Aimplicit -> "lambda_=>_" - | Aerasable -> "lambda_≡>_"), - [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); - lexp_unparse body]) - | Arrow (loc, arg_kind, (l,oname), ltp1, ltp2) - -> let ut1 = lexp_unparse ltp1 in - Node (Symbol (sexp_location loc, match arg_kind with Anormal -> "_->_" - | Aimplicit -> "_=>_" - | Aerasable -> "_≡>_"), - [(match oname with None -> ut1 - | Some v -> Node (Symbol (sexp_location l, "_:_"), - [Symbol (sexp_location l,v); ut1])); - lexp_unparse ltp2]) - - | Let (loc, ldecls, body) - -> (* (vdef * lexp * ltype) list *) - let sdecls = List.fold_left - (fun acc (vdef, lxp, ltp) - -> Node (Symbol (U.dummy_location, "_=_"), - [Symbol (sname vdef); lexp_unparse ltp]) - :: Node (Symbol (U.dummy_location, "_=_"), - [Symbol (sname vdef); lexp_unparse lxp]) - :: acc) - [] ldecls in - Node (Symbol (sexp_location loc, "let_in_"), - [Node (Symbol (U.dummy_location, "_;_"), sdecls); - lexp_unparse body]) - - | Call(_, lxp, largs) -> (* (arg_kind * lexp) list *) - 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 *) - (* (arg_kind * pvar * pexp option) list *) - let pfargs = List.map (fun (kind, vdef, ltp) -> - (kind, sname vdef, Some (lexp_unparse ltp))) lfargs in - - Node (stypecons, - Node (Symbol label, List.map pexp_u_formal_arg pfargs) - :: List.map - (fun (name, types) - -> Node (Symbol (sexp_location loc, name), - List.map - (fun arg -> - match arg with - | (Anormal, (_,None), t) -> lexp_unparse t - | (ak, s, t) - -> let (l,_) as id = sname s in - Node (Symbol (l, match ak with - | Anormal -> "_:_" - | Aimplicit -> "_::_" - | Aerasable -> "_:::_"), - [Symbol id; lexp_unparse t])) - types)) - (SMap.bindings ctors)) - - | Case (loc, target, bltp, branches, default) -> - let bt = lexp_unparse bltp in - let pbranch = List.map (fun (str, (loc, args, bch)) -> - match args with - | [] -> Ppatsym (loc, Some str), lexp_unparse bch - | _ -> - let pat_args - = List.map (fun (_kind, ((l,oname) as name)) - -> match oname with - | Some vdef -> (Some (sexp_location l,vdef), name) - | None -> (None, name)) - args - (* FIXME: Rather than a Pcons we'd like to refer to an existing - * binding with that value! *) - in (Ppatcons (Node (sdatacons, - [bt; Symbol (sexp_location loc, str)]), - pat_args), - lexp_unparse bch) - ) (SMap.bindings branches) in - - let pbranch = match default with - | Some (v,dft) -> (Ppatsym v, - lexp_unparse dft)::pbranch - | None -> pbranch - in let e = lexp_unparse target in - Node (Symbol (sexp_location loc, "case_"), + let st = lexp_unparse ltp in + Node (l, + Symbol (l, match kind with + | Anormal -> "lambda_->_" + | Aimplicit -> "lambda_=>_" + | Aerasable -> "lambda_≡>_"), + [Node (l, Symbol (l, "_:_"), [Symbol (sname vdef); st]); + lexp_unparse body]) + + | Arrow (sinfo, arg_kind, (sinfo_v, oname), ltp1, ltp2) + -> let location = sexp_location sinfo in + let location_v = sexp_location sinfo_v in + let ut1 = lexp_unparse ltp1 in + Node (location, + Symbol (location, + match arg_kind with Anormal -> "_->_" + | Aimplicit -> "_=>_" + | Aerasable -> "_≡>_"), + [(match oname with + | None -> ut1 + | Some v -> Node (location, + Symbol (location_v, "_:_"), + [Symbol (location_v, v); ut1])); + lexp_unparse ltp2]) + + | Let (sinfo, ldecls, body) (* (vdef * lexp * ltype) list *) + -> let location = sexp_location sinfo in + let sdecls = List.fold_left + (fun acc (vdef, lxp, ltp) + -> Node (location, + Symbol (U.dummy_location, "_=_"), + [Symbol (sname vdef); lexp_unparse ltp]) + :: Node (location, + Symbol (U.dummy_location, "_=_"), + [Symbol (sname vdef); lexp_unparse lxp]) + :: acc) + [] ldecls in + Node (location, + Symbol (location, "let_in_"), + [Node (location, Symbol (U.dummy_location, "_;_"), sdecls); + lexp_unparse body]) + + + | Call (sinfo, lxp, largs) (* (arg_kind * lexp) list *) + -> let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem) largs in + Node (sexp_location sinfo, lexp_unparse lxp, sargs) + + (* (arg_kind * vdef * ltype) list *) + (* (arg_kind * pvar * pexp option) list *) + | Inductive (sinfo, label, lfargs, ctors) + -> let location = sexp_location sinfo in + let pfargs = + List.map + (fun (kind, vdef, ltp) + -> (kind, sname vdef, Some (lexp_unparse ltp))) + lfargs + in + Node (location, + stypecons, + Node (location, Symbol label, List.map pexp_u_formal_arg pfargs) + :: List.map + (fun (name, types) + -> Node (location, + Sexp.symbol ~location name, + List.map + (fun arg -> + match arg with + | (Anormal, (_, None), t) -> lexp_unparse t + | (ak, s, t) + -> let (l, _) as id = sname s in + Node (location, + Symbol (l, match ak with + | Anormal -> "_:_" + | Aimplicit -> "_::_" + | Aerasable -> "_:::_"), + [Symbol id; lexp_unparse t])) + types)) + (SMap.bindings ctors)) + + | Case (sinfo, target, bltp, branches, default) + -> let bt = lexp_unparse bltp in + let unparse_pbranch (str, (sinfo, args, bch)) = + let location = sexp_location sinfo in + match args with + | [] -> Ppatsym (sinfo, Some str), lexp_unparse bch + | _ -> + let pat_args + = List.map (fun (_kind, ((sinfo, oname) as name)) + -> let location = sexp_location sinfo in + match oname with + | Some vdef -> (Some (location, vdef), name) + | None -> (None, name)) + args + (* FIXME: Rather than a Pcons we'd like to refer to an existing + * binding with that value! *) + in + let pattern = + Ppatcons (location, + Node (location, + sdatacons, + [bt; Symbol (location, str)]), + pat_args) + in + (pattern, lexp_unparse bch) + in + let pbranch = List.map unparse_pbranch (SMap.bindings branches) in + + let pbranch = match default with + | Some (v,dft) -> (Ppatsym v, lexp_unparse dft) :: pbranch + | None -> pbranch + in + let e = lexp_unparse target in + let location = sexp_location sinfo in + Node (location, + Symbol (location, "case_"), e :: List.map (fun (pat, branch) -> - Node (Symbol (sexp_location (pexp_pat_location pat), "_=>_"), + Node (location, + Symbol (pexp_pat_location pat, "_=>_"), [pexp_u_pat pat; branch])) pbranch)

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

| SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") + | SortLevel (SLsucc l) - -> Node (Symbol (lexp_location l, "##TypeLevel.succ"), - [lexp_unparse l]) + -> let location = lexp_location l in + Node (location, Symbol (location, "##TypeLevel.succ"), [lexp_unparse l]) + | SortLevel (SLlub (l1, l2)) - -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), - [lexp_unparse l1; lexp_unparse l2]) + -> let location = + Source.Location.extend (lexp_location l1) (lexp_location l2) + in + Node (location, + Symbol (lexp_location l1, "##TypeLevel.∪"), + [lexp_unparse l1; lexp_unparse l2]) + | Sort (l, StypeOmega) -> Symbol (sexp_location l, "##Type_ω") + | Sort (l, StypeLevel) -> Symbol (sexp_location l, "##TypeLevel.Sort") - | Sort (_l, Stype sl) - -> Node (Symbol (lexp_location sl, "##Type_"), - [lexp_unparse sl]) + + | Sort (l, Stype sl) + -> Node (sexp_location l, + Symbol (lexp_location sl, "##Type_"), + [lexp_unparse sl])

(* FIXME: ¡Unify lexp_print and lexp_string! *) and lexp_string lxp = sexp_string (lexp_unparse lxp) @@ -831,7 +871,7 @@ and lexp_name e = type print_context_value = | Bool of bool | Int of int - | Predtl of grammar (* precedence table *) + | Predtl of Grammar.t (** precedence table *)

type print_context = print_context_value SMap.t

@@ -906,7 +946,7 @@ let get_binary_op_name name = String.sub name 1 ((String.length name) - 2)

let rec get_precedence expr ctx = - let lkp name = SMap.find name (pp_grammar ctx) in + let lkp name = Grammar.find name (pp_grammar ctx) in match lexp_lexp' expr with | Lambda _ -> lkp "lambda" | Case _ -> lkp "case"

===================================== src/opslexp.ml ===================================== @@ -633,7 +633,7 @@ and check'' erased ctx e = | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_integer | Imm (String (_, _)) -> DB.type_string - | Imm (Block (_, _) | Symbol _ | Node (_, _)) + | Imm (Block (_, _) | Symbol _ | Node (_, _, _)) -> (log_tc_error ~loc:(lexp_location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level @@ -1094,7 +1094,7 @@ and get_type ctx e = | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_integer | Imm (String (_, _)) -> DB.type_string - | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> DB.type_int + | Imm (Block (_, _) | Symbol _ | Node (_, _, _)) -> DB.type_int | Builtin (_, t) -> t | SortLevel _ -> DB.type_level | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e)))

===================================== src/pexp.ml ===================================== @@ -37,46 +37,50 @@ type pvar = symbol (* type tag = string *)

type ppat = - | Ppatsym of vname (* A named default pattern, or a 0-ary constructor. *) - | Ppatcons of sexp * (symbol option * vname) list + | Ppatsym of vname (** A named default pattern, or a 0-ary constructor. *) + | Ppatcons of Source.Location.t * sexp * (symbol option * vname) list

-let pexp_pat_location e = match e with - | Ppatsym (l,_) -> l - | Ppatcons (e, _) -> e +let pexp_pat_location : ppat -> Source.Location.t = function + | Ppatsym (l, _) -> sexp_location l + | Ppatcons (l, _, _) -> l

let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = match arg with | (Anormal, s, None) -> Symbol s | (ak, ((l,_) as s), t) - -> Node (Symbol (l, match ak with Aerasable -> ":::" - | Aimplicit -> "::" - | Anormal -> ":"), - [Symbol s; match t with Some e -> e - | None -> Symbol (l, "_")]) + -> let head = + Symbol (l, match ak with Aerasable -> ":::" + | Aimplicit -> "::" + | Anormal -> ":") + in + let ty = match t with Some e -> e | None -> Symbol (l, "_") in + let location = Source.Location.extend l (sexp_location ty) in + Node (location, head, [Symbol s; ty])

let pexp_p_pat_arg (s : sexp) = match s with | Symbol (_l , n) -> (None, (s, match n with "_" -> None | _ -> Some n)) - | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (_l,n)]) + | Node (_, Symbol (_, "_:=_"), [Symbol f; Symbol (_l,n)]) -> (Some f, (s, Some n)) | _ -> let loc = sexp_location s in - pexp_error loc "Unknown pattern arg"; - (None, (s, None)) + pexp_error loc "Unknown pattern arg"; + (None, (s, None))

-let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = - let pname = Symbol (sexp_location l, match oname with None -> "_" | Some n -> n) in +let pexp_u_pat_arg (okn, (l, oname) : symbol option * vname) : sexp = + let oname_text = match oname with None -> "_" | Some n -> n in + let pname = Sexp.symbol ~location:(sexp_location l) oname_text in match okn with | None -> pname - | Some ((l,_) as n) -> - Node (Symbol (l, "_:=_"), [Symbol n; pname]) + | Some ((l, _) as n) -> Node (l, Symbol (l, "_:=_"), [Symbol n; pname])

let pexp_p_pat (s : sexp) : ppat = match s with | Symbol (_l, n) -> Ppatsym (s, match n with "_" -> None | _ -> Some n) - | Node (c, args) - -> Ppatcons (c, List.map pexp_p_pat_arg args) - | _ -> let l = sexp_location s in - pexp_error l "Unknown pattern"; Ppatsym (s, None) + | Node (location, c, args) + -> Ppatcons (location, c, List.map pexp_p_pat_arg args) + | _ + -> pexp_error (sexp_location s) "Unknown pattern"; + Ppatsym (s, None)

let pexp_u_pat (p : ppat) : sexp = match p with | Ppatsym (l, None) -> Symbol (sexp_location l, "_") | Ppatsym (l, Some n) -> Symbol (sexp_location l, n) - | Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args) + | Ppatcons (location, c, args) -> Node (location, c, List.map pexp_u_pat_arg args)

===================================== src/sexp.ml ===================================== @@ -22,31 +22,82 @@ this program. If not, see http://www.gnu.org/licenses/. *)

open Util open Prelexer -open Grammar

let sexp_error ?print_action loc fmt = Log.log_error ~section:"SEXP" ?print_action ~loc fmt

type integer = Z.t -type symbol = location * string - -type sexp = (* Syntactic expression, kind of like Lisp. *) - | Block of location * pretoken list - | Symbol of symbol - | String of location * string - | Integer of location * integer - | Float of location * float - | Node of sexp * sexp list + +module Sym = struct + type t = Source.Location.t * string + + let intern : location : Source.Location.t -> string -> t = + let module SHash = Hashtbl.Make(String) in + let shash = SHash.create 1000 in + fun ~location name -> + let name' = + try SHash.find shash name with + | Not_found -> SHash.add shash name name; name + in + (location, name') + + let location : t -> location = + fst + + let name : t -> string = + snd + + let equal (l : t) (r : t) : bool = + name l = name r + + let same (l : t) (r : t) : bool = + Source.Location.same (location l) (location r) + && name l = name r +end +type symbol = Sym.t + +(** Syntactic expression, kind of like Lisp. *) +type t = + | Block of Source.Location.t * pretoken list + | Symbol of Sym.t + | String of Source.Location.t * string + | Integer of Source.Location.t * integer + | Float of Source.Location.t * float + | Node of Source.Location.t * t * t list +type sexp = t type token = sexp type sinfo = sexp

-let epsilon l = Symbol (l, "") -let dummy_epsilon = epsilon dummy_location +let location : sexp -> location = function + | Block (l, _) -> l + | Symbol (l, _) -> l + | String (l, _) -> l + | Integer (l, _) -> l + | Float (l, _) -> l + | Node (l, _, _) -> l +let sexp_location = location + +let symbol ~(location : Source.Location.t) (name : string) : t = + Symbol (Sym.intern ~location name) + +let node (head : t) (tail : t list) : t = + let location = + List.fold_left + (fun l e -> Source.Location.extend l (location e)) + (location head) + tail + in + Node (location, head, tail)

+let epsilon (location : Source.Location.t) : sexp = + Symbol (Sym.intern ~location "") + +let dummy_epsilon = epsilon dummy_location let dummy_sinfo = epsilon dummy_location

type vname = sinfo * string option type vref = vname * db_index + (********************** Sexp tests **********************)

let pred_symbol s pred = @@ -54,44 +105,21 @@ let pred_symbol s pred = | Symbol (_, n) -> pred n | _ -> false

-let is_symbol e = pred_symbol e (fun _e -> true) - -(**************** Hash-consing symbols *********************) - -module SHash = Hashtbl.Make (struct type t = string - let equal = (=) - let hash = Hashtbl.hash - end) -let shash = SHash.create 1000 -let hString (name) = try SHash.find shash name - with Not_found - -> SHash.add shash name name; name -let hSymbol (l, name) = Symbol (l, hString name) -(* let toplevel = hString "TopLevel" *) -let emptyString = hString "" - (*************** The Sexp Printer *********************)

-let rec sexp_location (s : sexp) : location = - match s with - | Block (l, _) -> l - | Symbol (l, _) -> l - | String (l, _) -> l - | Integer (l, _) -> l - | Float (l, _) -> l - | Node (s, _) -> sexp_location s - (* Converts a sexp to a string, optionally printing locations as a list preceded by a Racket-style reader comment (#;). *) let rec sexp_string ?(print_locations = false) sexp = (if print_locations then let open Source.Location in - let {file; start_line; start_column; end_line; end_column} = - sexp_location sexp + let {file; start; end'} = sexp_location sexp in Printf.sprintf - "#;("%s" %d %d %d %d) " file start_line start_column end_line end_column + "#;("%s" %d %d %d %d %d %d) " + file + start.offset start.line start.column + end'.offset end'.line end'.column else "") ^ match sexp with | Block(_, pts) -> "{" ^ (pretokens_string pts) ^ " }" @@ -100,7 +128,7 @@ let rec sexp_string ?(print_locations = false) sexp = | String(_, str) -> """ ^ str ^ """ | Integer(_, n) -> Z.to_string n | Float(_, x) -> string_of_float x - | Node(f, args) -> + | Node(_, f, args) -> let str = "(" ^ (sexp_string ~print_locations f) in (List.fold_left (fun str sxp -> str ^ " " ^ (sexp_string ~print_locations sxp)) str args) ^ ")" @@ -119,27 +147,9 @@ let sexp_name s =

(*************** The Sexp Parser *********************)

- -(* If true, infix symbols like "_;_" will be turned into ";_" or "_;" - * if they had no right or left argument. - * If false, "_;_" will stay as it is, and receive Epsilon arguments - * as appropriate. *) -let empty_args_are_not_args = false - -(* `op' is the operator being parsed. E.g. for let...in... - * it would be either ["let"] or ["in";"let"] depending on which - * part we've parsed already. - * `largs' are the args to the left of the latest infix; they belong to `op'. - * `rargs' are the sexps that compose the arg to the right of the latest - * infix symbol. They may belong to `op' or to a later infix operator - * we haven't seen yet which binds more tightly. *) -let rec sexp_parse (g : grammar) (rest : sexp list) - (level : int) - (op : symbol list) - (largs : sexp list) - (rargs : sexp list) - : (sexp * sexp list) = - let sexp_parse = sexp_parse g in +let sexp_parse + (g : Grammar.t) (tokens : sexp list) (level : int) + : sexp * sexp list =

let compose_symbol (ss : symbol list) = match ss with | [] -> (Log.internal_error "empty operator!") @@ -148,115 +158,139 @@ let rec sexp_parse (g : grammar) (rest : sexp list)

let push_largs largs rargs closer = match List.rev rargs with | [] -> if closer then dummy_epsilon :: largs else largs - | e::es -> (match es with [] -> e | _ -> Node (e, es)) :: largs in + | e :: [] -> e :: largs + | e :: es -> node e es :: largs + in

- let mk_node op largs rargs closer = + let make_node op largs rargs closer = let args = List.rev (push_largs largs rargs closer) in - match op with - | [] -> (match args with [] -> dummy_epsilon - | [e] -> e - | e::es -> Node (e, es)) - | ss -> let headname = compose_symbol ss in - match (headname, args) with - (* FIXME: While it's uaulyl good to strip away parens, - * this makes assumptions about the grammar (i.e. there's - * a rule « exp ::= '(' exp ')' » ), and this is sometimes - * not desired (e.g. to distinguish "a b ⊢ c d" from - * "(a b) ⊢ (c d)"). *) - | ((_,"(_)"), [arg]) -> arg (* Strip away parens. *) - | _ -> Node (hSymbol (headname), args) in - - match rest with - | (((Symbol ((l,name) as s)) as e)::rest') -> - (try match SMap.find name g with - | (None, None) -> sexp_parse rest' level op largs (e::rargs) - | (None, Some rl) (* Open paren or prefix. *) - -> let (e, rest) = sexp_parse rest' rl [s] [] [] - in sexp_parse rest level op largs (e::rargs) + match op, args with + | [], [] -> dummy_epsilon + | [], [e] -> e + | [], e :: es -> node e es + | ss, _ + -> let head_location, head_name = compose_symbol ss in + match head_name, args with + (* FIXME: While it's usualy good to strip away parens, this makes + assumptions about the grammar (i.e. there's a rule + « exp ::= '(' exp ')' »), and this is sometimes not desired (e.g. to + distinguish "a b ⊢ c d" from "(a b) ⊢ (c d)"). *) + | "(_)", [arg] -> arg (* Strip away parens. *) + | _ + -> let head = symbol ~location:head_location head_name in + node head args + in + + (* `op' is the operator being parsed. E.g. for let...in... it would be either + ["let"] or ["in";"let"] depending on which part we've parsed already. + + `largs' are the args to the left of the latest infix; they belong to `op'. + + `rargs' are the sexps that compose the arg to the right of the latest infix + symbol. They may belong to `op' or to a later infix operator we haven't + seen yet which binds more tightly. *) + let rec recur rest level op largs rargs = + match rest with + | (Symbol ((l, name) as s) as e) :: rest' + -> begin match Grammar.find name g with + | (None, None) + -> recur rest' level op largs (e :: rargs) + + (* Open paren or prefix. *) + | (None, Some rl) + -> let (e, rest) = recur rest' rl [s] [] [] + in recur rest level op largs (e :: rargs) + + (* A symbol that closes the currently parsed element. *) | (Some ll, _) when ll < level - (* A symbol that closes the currently parsed element. *) - -> ((if empty_args_are_not_args then - mk_node (match rargs with [] -> op | _ -> ((l,"")::op)) - largs rargs false - else - mk_node ((l,"")::op) largs rargs true), - rest) + -> let node = make_node ((l, "") :: op) largs rargs true in + (node, rest) + + (* A closer without matching opener or a postfix symbol that binds very + tightly. Previously, we signaled an error (assuming the former), but + it prevented the use tightly binding postfix operators. + + For example, it signaled spurious errors when parsing expressions with + a tightly binding postfix # operator that implemented record + construction by taking an inductive as argument and returning the + inductive's only constructor. *) | (Some ll, None) when ll > level - (* A closer without matching opener or a postfix symbol - that binds very tightly. Previously, we signaled an - error (assuming the former), but it prevented the use - tightly binding postfix operators. - - For example, it signaled spurious errors when parsing - expressions with a tightly binding postfix # operator - that implemented record construction by taking an - inductive as argument and returning the inductive's only - constructor. *) - -> sexp_parse rest' level op largs - [mk_node [(l,name);(l,"")] [] rargs true] + -> let rarg = make_node [(l, name); (l, "")] [] rargs true in + recur rest' level op largs [rarg] + + (* A new infix which binds more tightly, i.e. does not close the + current `op' but takes its `rargs' instead. *) | (Some ll, Some rl) when ll > level - (* A new infix which binds more tightly, i.e. does not close - * the current `op' but takes its `rargs' instead. *) - -> let (e, rest) - = if empty_args_are_not_args then - sexp_parse rest' rl - (match rargs with [] -> [s] | _ -> [s;(l,"")]) - (push_largs [] rargs false) [] - else - sexp_parse rest' rl [s;(l,"")] - (push_largs [] rargs true) [] - in sexp_parse rest level op largs [e] + -> let largs' = push_largs [] rargs true in + let (e, rest'') = recur rest' rl [s; (l, "")] largs' [] in + recur rest'' level op largs [e] + | (Some ll, Some rl) - -> sexp_parse rest' rl - (if ll == rl - && match op with (_,name')::_ -> name = name' - | _ -> false - then op else (s::op)) - (push_largs largs rargs true) [] + -> let op' = + (* Having the same left and right precedence means it is a + separator such as ‘;’ or ‘|’. In that case, only add it the + operator name if it is not present. For example, adding ‘|’ to + ‘case_’ yields ‘case_|’, but adding another ‘|’ to ‘case_|’ + also yields ‘case_|’. *) + if + ll == rl + && match op with (_, name') :: _ -> name = name' | _ -> false + then op + else s :: op + in + recur rest' rl op' (push_largs largs rargs true) [] + | (Some _ll, None) - -> (mk_node (s::op) largs rargs true, rest') - with Not_found -> - sexp_parse rest' level op largs (e::rargs)) - | e::rest -> sexp_parse rest level op largs (e::rargs) - | [] -> (mk_node (match rargs with [] -> op - | _ -> ((dummy_location,"")::op)) - largs rargs false, - []) + -> let node = make_node (s :: op) largs rargs true in + (node, rest') + end + + | e :: rest -> recur rest level op largs (e :: rargs) + + | [] + -> let op' = match rargs with [] -> op | _ -> (dummy_location, "") :: op in + let node = make_node op' largs rargs false in + (node, []) + in + recur tokens level [] [] []

let sexp_parse_all grm tokens limit : sexp * token list = - let level = match limit with + let level = + match limit with | None -> min_int | Some token -> - match SMap.find token grm with - | (Some ll, Some _) -> ll + 1 - | _ -> Log.internal_error {|Can't find level of "%s"|} token - in let (e, rest) = sexp_parse grm tokens level [] [] [] in - let se = match e with - | Node (Symbol (_, ""), [e]) -> e - | Node (Symbol (_, ""), e::es) -> Node (e, es) - | _ -> (Log.internal_error "Didn't find a toplevel") in - match rest with - | [] -> (se,rest) - | Symbol (l,t) :: rest - -> if not (Some t = limit) - then sexp_error l {|Stray closing token: "%s"|} t; - (se,rest) - | _ -> (Log.internal_error "Stopped parsing before the end!") + match Grammar.find token grm with + | (Some ll, Some _) -> ll + 1 + | _ -> Log.internal_error {|Can't find level of "%s"|} token + in + let (e, rest) = sexp_parse grm tokens level in + let se = match e with + | Node (_, Symbol (_, ""), [e]) -> e + | Node (location, Symbol (_, ""), e :: es) -> Node (location, e, es) + | _ -> Log.internal_error "Didn't find a toplevel" + in + match rest with + | [] -> (se,rest) + | Symbol (l,t) :: rest + -> if not (Some t = limit) + then sexp_error l {|Stray closing token: "%s"|} t; + (se,rest) + | _ -> (Log.internal_error "Stopped parsing before the end!")

(* "sexp_p" is for "parsing" and "sexp_u" is for "unparsing". *)

let sexp_p_list (s : sexp) (exceptions : string list) : sexp list = match s with | Symbol (_, "") -> [] - | Node (Symbol (_, head), _tail) when List.mem head exceptions -> [s] - | Node (head, tail) -> head :: tail + | Node (_, Symbol (_, head), _tail) when List.mem head exceptions -> [s] + | Node (_, head, tail) -> head :: tail | _ -> [s]

-let sexp_u_list (ss : sexp list) : sexp = +let sexp_u_list (ss : sexp list) (location : Source.Location.t) : sexp = match ss with | [] -> dummy_epsilon | [s] -> s - | (s :: ss) -> Node (s, ss) + | (s :: ss) -> Node (location, s, ss)

(* Parse all the Sexp *) let sexp_parse_all_to_list grm tokens limit : sexp list = @@ -269,19 +303,36 @@ let sexp_parse_all_to_list grm tokens limit : sexp list = sexp_parse_impl grm rest limit (sxp :: acc) in sexp_parse_impl grm tokens limit []

-(* Sexp comparison, ignoring source-line-number info, used for tests. *) +(** Sexp comparison, ignoring source-line-number info, used for tests. *) let rec sexp_equal s1 s2 = match s1, s2 with | Block (_, ps1), Block (_, ps2) -> pretokens_eq_list ps1 ps2 | Symbol (_, s1), Symbol (_, s2) -> s1 = s2 | String (_, s1), String (_, s2) -> s1 = s2 | Integer (_, n1), Integer (_, n2) -> n1 = n2 | Float (_, n1), Float (_, n2) -> n1 = n2 - | Node (s1, ss1), Node (s2, ss2) -> - sexp_equal s1 s2 && sexp_eq_list ss1 ss2 + | Node (_, s1, ss1), Node (_, s2, ss2) + -> sexp_equal s1 s2 && Listx.equal sexp_equal ss1 ss2 | _ -> false

-and sexp_eq_list ss1 ss2 = match ss1, ss2 with - | [], [] -> true - | (s1 :: ss1), (s2 :: ss2) -> - sexp_equal s1 s2 && sexp_eq_list ss1 ss2 - | _ -> false +(** Sexp comparison, *with* source-line-number info, used for tests. *) +let rec same l r = + match l, r with + | Block (l_location, l_pretokens), Block (r_location, r_pretokens) + -> Source.Location.same l_location r_location + && Listx.equal pretokens_equal l_pretokens r_pretokens + | Symbol (l_sym), Symbol (r_sym) + -> Sym.same l_sym r_sym + | String (l_location, l_value), String (r_location, r_value) + -> Source.Location.same l_location r_location + && l_value = r_value + | Integer (l_location, l_value), Integer (r_location, r_value) + -> Source.Location.same l_location r_location + && l_value = r_value + | Float (l_location, l_value), Float (r_location, r_value) + -> Source.Location.same l_location r_location + && l_value = r_value + | Node (l_location, l_head, l_tail), Node (r_location, r_head, r_tail) + -> Source.Location.same l_location r_location + && same l_head r_head + && Listx.equal same l_tail r_tail + | _, _ -> false

===================================== src/source.ml ===================================== @@ -18,90 +18,103 @@ * You should have received a copy of the GNU General Public License along * with this program. If not, see http://www.gnu.org/licenses/. *)

-module Point = struct - (* offset * line * column *) - type t = int * int * int +(** Traditionally, line numbers start at 1… *) +let first_line_of_file : int = 1

- let equal (l, _, _ : t) (r, _, _ : t) : bool = - (* The line and column are metadata, only the offset is necessary for - determining equality. *) - Int.equal l r -end +let first_column_of_line : int = 0

-module Location = struct - type t = - { - file : string; - start_line : int; - start_column : int; - end_line : int; - end_column : int; - } +(** A point is a position within a source file. *) +module Point = struct + type t = {offset : int; line : int; column : int}

- let dummy = + let zero : t = { - file = ""; - start_line = 0; - start_column = 0; - end_line = 0; - end_column = 0; + offset = 0; + line = first_line_of_file; + column = first_column_of_line; }

- (* Creates a zero-width location around the given point. *) - let of_point (file : string) (_, line, column : Point.t) : t = - { - file; - start_line = line; - start_column = column; - end_line = line; - end_column = column; - } + (** Two points are equal if they refer to the same offset in a givent file. + The line and column are metadata and do not participate in determining + equality. *) + let equal (l : t) (r : t) : bool = + l.offset = r.offset + + (** Like [equal], but also checks the line and column. *) + let same (l : t) (r : t) : bool = + l.offset = r.offset + && l.line = r.line + && l.column = r.column + + let min (l : t) (r : t) : t = + if l.offset < r.offset + then l + else r + + let max (l : t) (r : t) : t = + if l.offset < r.offset + then r + else l + + let (<=) (l : t) (r : t) : bool = + l.offset <= r.offset +end + +(** A location is an open interval of characters within a source file. *) +module Location = struct + type t = {file : string; start : Point.t; end' : Point.t}

- let to_string - ({file; start_line; start_column; end_line; end_column} : t) - : string = + (** Creates a zero-width location around the given point. *) + let of_point (file : string) (point : Point.t) : t = + {file; start = point; end' = point}

- if Int.equal start_line end_line && Int.equal start_column end_column - then Printf.sprintf "%s:%d:%d" file start_line start_column + (** An empty location at the beginning of an empty file. *) + let dummy = of_point "" Point.zero + + let to_string (l : t) : string = + if l.start.offset = l.end'.offset + then Printf.sprintf "%s:%d:%d" l.file l.start.line l.start.column else Printf.sprintf - "%s:%d:%d-%d:%d" file start_line start_column end_line end_column + "%s:%d:%d-%d:%d" + l.file l.start.line l.start.column l.end'.line l.end'.column

let equal (l : t) (r : t) = - let - { - file = l_file; - start_line = l_start_line; - start_column = l_start_column; - end_line = l_end_line; - end_column = l_end_column; - } = l - in - let - { - file = r_file; - start_line = r_start_line; - start_column = r_start_column; - end_line = r_end_line; - end_column = r_end_column; - } = r - in - - String.equal l_file r_file - && Int.equal l_start_line r_start_line - && Int.equal l_start_column r_start_column - && Int.equal l_end_line r_end_line - && Int.equal l_end_column r_end_column + String.equal l.file r.file + && Point.equal l.start r.start + && Point.equal l.end' r.end' + + let same (l : t) (r : t) = + String.equal l.file r.file + && Point.same l.start r.start + && Point.same l.end' r.end' + + (** Locations form a partial order where one is smaller than another iff it is + entirely contained in the latter. *) + let (<=) (l : t) (r : t) : bool = + if l.file <> r.file + then false + else Point.(<=) r.start l.start && Point.(<=) l.end' r.end' + + (** Returns the least upper bound of two locations, i.e. the smallest location + that covers both. If the locations do not belong to the same file, simply + returns the first one. *) + let extend (l : t) (r : t) : t = + if l.file <> r.file + then l + else if l == dummy + then r + else if r == dummy + then l + else + let start = Point.min l.start r.start in + let end' = Point.max l.end' r.end' in + {file = l.file; start; end'} end

-(* Traditionally, line numbers start at 1… *) -let first_line_of_file = 1 -(* … and so do column numbers :-( *) -let first_column_of_line = 1 - -(* A source object is text paired with a cursor. The text can be lazily loaded - as it is accessed byte by byte, but it must be retained for future reference - by error messages. *) +(** A source object is text paired with a cursor. The text can be lazily loaded + as it is accessed byte by byte, but it must be retained for future reference + by error messages. *) class virtual t (base_line : int) (base_column : int) (file : string) = object (self) val mutable line = base_line @@ -116,15 +129,15 @@ object (self)

(* The current point of the cursor. *) method point : Point.t = - (self#offset, line, column) + {offset = self#offset; line; column}

(* The current offset of the cursor in the file, in bytes. *) method virtual private offset : int

(* Makes a location starting at the given point and ending at the current cursor position. *) - method make_location (_, start_line, start_column : Point.t) : Location.t = - {file; start_line; start_column; end_line = line; end_column = column} + method make_location (start : Point.t) : Location.t = + {file; start; end' = self#point}

(* Slices the text, from (and including) a starting point and to (and excluding) the curent cursor offset. @@ -132,8 +145,8 @@ object (self) Note that the source is required only to buffer the last line read and may raise an Invalid_argument if the slice extends before the start of the line. *) - method slice (offset, _, _ as point : Point.t) : string * Location.t = - (self#slice_impl offset, self#make_location point) + method slice (point : Point.t) : string * Location.t = + (self#slice_impl point.offset, self#make_location point)

method virtual private slice_impl : int -> string

===================================== src/string.ml ===================================== @@ -0,0 +1,24 @@ +(* Copyright (C) 2023 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. *) + +include Stdlib.String + +(* Backport from 5.0. *) +let hash : t -> int = Hashtbl.hash

===================================== tests/lexer_test.ml ===================================== @@ -23,30 +23,11 @@ open Utest_lib

open Prelexer open Sexp -open Source

let test_lex name pretokens expected = - (* Unlike the version in the Sexp module, this version of equality considers - locations. *) - let rec sexp_equal actual expected = - match actual, expected with - | Sexp.Block (actual_location, actual_pretokens), - Sexp.Block (expected_location, expected_pretokens) - -> Location.equal actual_location expected_location - && Listx.equal Pretoken.equal actual_pretokens expected_pretokens - | Sexp.Symbol (actual_location, actual_name), - Sexp.Symbol (expected_location, expected_name) - -> Location.equal actual_location expected_location - && String.equal actual_name expected_name - | Sexp.Node (actual_head, actual_tail), - Sexp.Node (expected_head, expected_tail) - -> sexp_equal actual_head expected_head - && Listx.equal sexp_equal actual_tail expected_tail - | _, _ -> false - in let lex () = let actual = Lexer.lex Grammar.default_stt pretokens in - if Listx.equal sexp_equal actual expected + if Listx.equal Sexp.same actual expected then success else ((* Only print locations if the Sexp are otherwise identical so its easier @@ -65,43 +46,42 @@ let test_lex name pretokens expected = in add_test "LEXER" name lex

-let l : Source.Location.t = +let l os ls cs oe le ce : Source.Location.t = { file = "test.typer"; - start_line = 1; - start_column = 1; - end_line = 1; - end_column = 1; + start = {offset = os; line = ls; column = cs}; + end' = {offset = oe; line = le; column = ce}; }

let () = test_lex "Inner operator inside a presymbol" - [Pretoken (l, "a.b")] - [Node (Symbol ({l with start_column = 2; end_column = 3}, "__.__"), - [Symbol ({l with start_column = 1; end_column = 2}, "a"); - Symbol ({l with start_column = 3; end_column = 4}, "b")])] + [Pretoken (l 0 1 0 3 1 3, "a.b")] + [Node (l 0 1 0 3 1 3, + Symbol (l 1 1 1 2 1 2, "__.__"), + [Symbol (l 0 1 0 1 1 1, "a"); Symbol (l 2 1 2 3 1 3, "b")])]

let () = test_lex "Inner operators at the beginning of a presymbol" - [Pretoken (l, ".b")] - [Node (Symbol ({l with start_column = 1; end_column = 2}, "__.__"), - [epsilon {l with start_column = 1; end_column = 1}; - Symbol ({l with start_column = 2; end_column = 3}, "b")])] + [Pretoken (l 0 1 0 2 1 2, ".b")] + [Node (l 0 1 0 2 1 2, + Symbol (l 0 1 0 1 1 1, "__.__"), + [epsilon (l 0 1 0 0 1 0); Symbol (l 1 1 1 2 1 2, "b")])]

let () = test_lex "Inner operators at the end of a presymbol" - [Pretoken (l, "a.")] - [Node (Symbol ({l with start_column = 2; end_column = 3}, "__.__"), - [Symbol ({l with start_column = 1; end_column = 2}, "a"); - epsilon {l with start_column = 3; end_column = 3}])] + [Pretoken (l 0 1 0 2 1 2, "a.")] + [Node (l 0 1 0 2 1 2, + Symbol (l 1 1 1 2 1 2, "__.__"), + [Symbol (l 0 1 0 1 1 1, "a"); + epsilon (l 2 1 2 2 1 2)])]

let () = test_lex "An inner operator by itself is a simple symbol" - [Pretoken (l, ".")] - [Symbol ({l with start_column = 1; end_column = 2}, ".")] + [Pretoken (l 0 1 0 1 1 1, ".")] + [Symbol (l 0 1 0 1 1 1, ".")]

let () = run_all ()

===================================== tests/sexp_test.ml ===================================== @@ -43,17 +43,19 @@ let test_sexp_add dcode testfun =

let _ = test_sexp_add "lambda x -> x + x" (fun ret -> match ret with - | [Node(Symbol(_, "lambda_->_"), + | [Node(_, + Symbol(_, "lambda_->_"), [Symbol(_, "x"); - Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")])])] + Node(_, Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")])])] -> success | _ -> failure )

let _ = test_sexp_add "x * x * x" (fun ret -> match ret with - | [Node(Symbol(_, "_*_"), - [Node(Symbol(_, "_*_"), [Symbol(_, "x"); Symbol(_, "x")]); + | [Node(_, + Symbol(_, "_*_"), + [Node(_, Symbol(_, "_*_"), [Symbol(_, "x"); Symbol(_, "x")]); Symbol(_, "x")])] -> success | _ -> failure

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a8f40b1a6ec3f0d6f0d5bf474b8b3ae4b...