Stefan pushed to branch master at Stefan / Typer
Commits:
e8a59f86 by Simon Génier at 2021-09-28T17:25:19-04:00
Replace raw offsets with points which also track line and column.
- - - - -
87882dea by Simon Génier at 2021-09-28T17:45:35-04:00
Compute location inside the source from the given point.
- - - - -
fce0fac4 by Simon Génier at 2021-09-28T18:16:00-04:00
Upgrade to OCaml 4.11.
* Update the README
* Remove a few functions that are now part of the standard library.
- - - - -
db1cf4da by Stefan Monnier at 2021-10-06T09:38:32-04:00
Merge remote-tracking branch 'gitlab/ocaml-4.11' into trunk
- - - - -
14 changed files:
- README.md
- debug_util.ml
- src/elab.ml
- − src/float.ml
- src/gambit.ml
- − src/int.ml
- src/lexer.ml
- src/listx.ml
- src/log.ml
- src/opslexp.ml
- − src/option.ml
- src/prelexer.ml
- src/source.ml
- src/util.ml
Changes:
=====================================
README.md
=====================================
@@ -8,7 +8,7 @@ Status []
## Requirement
-* Ocaml 4.05
+* Ocaml 4.11
* Dune 2.x
* Zarith
=====================================
debug_util.ml
=====================================
@@ -279,7 +279,7 @@ let main () =
(* Type erasure *)
let _, clean_lxp =
- Listx.fold_left_map OL.clean_decls (ectx_to_lctx nctx) lexps
+ List.fold_left_map OL.clean_decls (ectx_to_lctx nctx) lexps
in
(* Eval declaration *)
=====================================
src/elab.ml
=====================================
@@ -683,7 +683,7 @@ and unify_or_error lctx lxp ?lxp_name expect actual =
^ (match ck with | Unif.CKimpossible -> ""
| Unif.CKresidual -> " (residue)")
^ "! Context expected:\n " ^ lexp_string expect ^ "\nbut "
- ^ (U.option_default "expression" lxp_name) ^ " has type:\n "
+ ^ (Option.value ~default:"expression" lxp_name) ^ " has type:\n "
^ lexp_string actual ^ "\ncan't unify:\n "
^ lexp_string t1
^ "\nwith:\n "
@@ -1711,7 +1711,7 @@ let sform_letin ctx loc sargs ot = match sargs with
List.fold_left (fun (s, off) decls ->
(OL.lexp_defs_subst loc s decls, off + List.length decls))
(S.identity, 0) declss in
- let ot = U.option_map (fun t -> mkSusp t (S.shift off)) ot in
+ let ot = Option.map (fun t -> mkSusp t (S.shift off)) ot in
let bdy, ot = elaborate nctx sbody ot in
let ot = match ot with
| Inferred t -> Inferred (mkSusp t s)
@@ -1955,7 +1955,7 @@ let eval_expr_str str ectx rctx =
let eval_decl_str str ectx rctx =
let lxps, ectx' = lexp_decl_str str ectx in
let lctx = ectx_to_lctx ectx in
- let _, elxps = Listx.fold_left_map (OL.clean_decls) lctx lxps in
+ let _, elxps = List.fold_left_map (OL.clean_decls) lctx lxps in
(EV.eval_decls_toplevel elxps rctx), ectx'
let eval_file
=====================================
src/float.ml deleted
=====================================
@@ -1,25 +0,0 @@
-(* Copyright (C) 2020 Free Software Foundation, Inc.
- *
- * Author: Simon Génier <simon.genier(a)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/>. *)
-
-type t = float
-
-let equal (l : t) (r : t) : bool = l = r
-
-let compare (l : t) (r : t) : int = compare l r
=====================================
src/gambit.ml
=====================================
@@ -176,7 +176,7 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t =
then scheme_of_expr sctx body
else
let sctx, bindings =
- Listx.fold_left_map ScmContext.intro_binding sctx bindings
+ List.fold_left_map ScmContext.intro_binding sctx bindings
in
let scheme_of_binding (name, elexp) =
Scm.List [Scm.Symbol name; scheme_of_expr sctx elexp]
@@ -293,7 +293,7 @@ class gambit_compiler lctx output = object
method process_decls ldecls =
let lctx', eldecls = Opslexp.clean_decls lctx ldecls in
- let sctx', eldecls = Listx.fold_left_map ScmContext.intro_binding sctx eldecls in
+ let sctx', eldecls = List.fold_left_map ScmContext.intro_binding sctx eldecls in
let sdecls = Scm.List (Scm.begin' :: List.map (scheme_of_decl sctx') eldecls) in
sctx <- sctx';
=====================================
src/int.ml deleted
=====================================
@@ -1,25 +0,0 @@
-(* Copyright (C) 2020 Free Software Foundation, Inc.
- *
- * Author: Simon Génier <simon.genier(a)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/>. *)
-
-type t = int
-
-let equal (l : t) (r : t) : bool = l = r
-
-let compare (l : t) (r : t) : int = compare l r
=====================================
src/lexer.ml
=====================================
@@ -37,8 +37,8 @@ let unescape str =
let lex_number
(source : #Source.t)
- (start_location : Source.Location.t)
- (start_offset : int)
+ (start_point : Source.Point.t)
+ (doc : string)
: sexp =
let rec lex_exponent () =
@@ -48,8 +48,8 @@ let lex_number
lex_exponent ()
| _
- -> let source = source#slice start_offset in
- Float (start_location, float_of_string source)
+ -> let source, location = source#slice start_point doc in
+ Float (location, float_of_string source)
in
let lex_exponent_sign () =
@@ -60,8 +60,8 @@ let lex_number
(* TODO: error if there are no signs or digits after the 'e'? *)
| _
- -> let source = source#slice start_offset in
- Float (start_location, float_of_string source)
+ -> let source, location = source#slice start_point doc in
+ Float (location, float_of_string source)
in
let rec lex_fractional () =
@@ -75,8 +75,8 @@ let lex_number
lex_exponent_sign ()
| _
- -> let source = source#slice start_offset in
- Float (start_location, float_of_string source)
+ -> let source, location = source#slice start_point doc in
+ Float (location, float_of_string source)
in
let rec lex_integer () =
@@ -94,8 +94,8 @@ let lex_number
lex_exponent_sign ()
| _
- -> let source = source#slice start_offset in
- Integer (start_location, Z.of_string source)
+ -> let source, location = source#slice start_point doc in
+ Integer (location, Z.of_string source)
in
lex_integer ()
@@ -105,38 +105,37 @@ let lex_symbol
(token_env : token_env)
(source : #Source.t)
(doc : string)
- (start_location : Source.Location.t)
- (start_offset : int)
+ (start_point : Source.Point.t)
: sexp =
- let mksym start_location start_offset escaped =
- if Int.equal start_offset source#offset
- then epsilon start_location
+ let mksym start_point escaped =
+ if Source.Point.equal start_point source#point
+ then epsilon (Source.Location.of_point source#file start_point doc)
else
- let raw_name = source#slice start_offset in
+ let raw_name, location = source#slice start_point doc in
let name = if escaped then unescape raw_name else raw_name in
- hSymbol (start_location, name)
+ hSymbol (location, name)
in
- let rec loop start_location start_offset prec lf (escaped : bool) =
+ let rec loop start_point prec lf (escaped : bool) =
match source#peek with
| None
- -> lf (mksym start_location start_offset escaped)
+ -> lf (mksym start_point escaped)
| Some c
-> (match token_env.(Char.code c) with
| CKseparate
- -> lf (mksym start_location start_offset escaped)
+ -> lf (mksym start_point escaped)
| CKinner prec'
- -> let left = mksym start_location start_offset escaped in
+ -> let left = mksym start_point escaped in
let op_location = source#location doc in
(* To be considered `inner`, an operator char needs to have
something on its LHS or its RHS, otherwise, treat it as a
normal char. `.` can be the normal function composition
operator as well. *)
- let lhs_p = start_offset != source#offset in
+ let lhs_p = not (Source.Point.equal start_point source#point) in
source#advance;
let rhs_p =
(match source#peek with
@@ -151,9 +150,9 @@ let lex_symbol
then fun s -> lf (Node (op, [left; s]))
else fun s -> Node (op, [lf left; s])
in
- loop (source#location doc) source#offset prec' lf' false
+ loop source#point prec' lf' false
else
- loop start_location start_offset prec lf escaped
+ loop start_point prec lf escaped
| CKnormal
-> (source#advance;
@@ -165,11 +164,11 @@ let lex_symbol
leading byte, so it has to count as 1 as well ;-) *)
| '\\' when not is_last
-> source#advance;
- loop start_location start_offset prec lf true
+ loop start_point prec lf true
- | _ -> loop start_location start_offset prec lf escaped))
+ | _ -> loop start_point prec lf escaped))
in
- loop start_location start_offset 0 (fun s -> s) false
+ loop start_point 0 (fun s -> s) false
let split_presymbol
(token_env : token_env)
@@ -181,8 +180,7 @@ let split_presymbol
match source#peek with
| None -> List.rev acc
| Some (c)
- -> let start_offset = source#offset in
- let start_location = source#location doc in
+ -> let start_point = source#point in
let token =
match c with
(* A negative number literal, or a symbol starting with '-'. *)
@@ -190,21 +188,21 @@ let split_presymbol
-> (source#advance;
match source#peek with
| Some ('0' .. '9')
- -> lex_number source start_location start_offset
+ -> lex_number source start_point doc
| _
- -> lex_symbol token_env source doc start_location start_offset)
+ -> lex_symbol token_env source doc start_point)
| '0' .. '9'
-> (source#advance;
- lex_number source start_location start_offset)
+ lex_number source start_point doc)
| _ when token_env.(Char.code c) = CKseparate
-> source#advance;
- let name = source#slice start_offset in
- hSymbol (start_location, name)
+ let name, location = source#slice start_point doc in
+ hSymbol (location, name)
| _
- -> lex_symbol token_env source doc start_location start_offset
+ -> lex_symbol token_env source doc start_point
in
loop (token :: acc)
in
=====================================
src/listx.ml
=====================================
@@ -18,33 +18,6 @@
* You should have received a copy of the GNU General Public License along
* with this program. If not, see <http://www.gnu.org/licenses/>. *)
-(* Backport from 4.08. *)
-let filter_map (f : 'a -> 'b option) (xs : 'a list) : 'b list =
- let rec loop xs ys =
- match xs with
- | [] -> List.rev ys
- | x :: xs
- -> (match f x with
- | Some y -> loop xs (y :: ys)
- | None -> loop xs ys)
- in
- loop xs []
-
-(* Backport from 4.11. *)
-let fold_left_map
- (f : 'a -> 'b -> 'a * 'c)
- (i : 'a)
- (bs : 'b list)
- : 'a * 'c list =
-
- let rec loop fold_acc map_acc bs = match bs with
- | [] -> (fold_acc, List.rev map_acc)
- | b :: bs
- -> let fold_acc, new_element = f fold_acc b in
- loop fold_acc (new_element :: map_acc) bs
- in
- loop i [] bs
-
(* Backport from 4.12. *)
let rec equal (p : 'a -> 'a -> bool) (ls : 'a list) (rs : 'a list) : bool =
match ls, rs with
=====================================
src/log.ml
=====================================
@@ -114,9 +114,12 @@ let maybe_color_string color_opt str =
let string_of_log_entry {level; kind; section; loc; msg; _} =
let color = if typer_log_config.color then (level_color level) else None in
let parens s = "(" ^ s ^ ")" in
- (option_default "" (option_map Source.Location.to_string loc)
- ^ maybe_color_string color (option_default (string_of_level level) kind) ^ ":"
- ^ option_default "" (option_map parens section) ^ " "
+ (Option.value ~default:"" (Option.map Source.Location.to_string loc)
+ ^ maybe_color_string
+ color
+ (Option.value ~default:(string_of_level level) kind)
+ ^ ":"
+ ^ Option.value ~default:"" (Option.map parens section) ^ " "
^ msg)
let print_entry entry =
=====================================
src/opslexp.ml
=====================================
@@ -187,7 +187,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =
| Call (f', xs1) -> mkCall (f', List.append xs1 xs)
| Builtin ((_, name), _)
-> (match SMap.find_opt name (!reducible_builtins) with
- | Some f -> U.option_default e (f ctx args)
+ | Some f -> Option.value ~default:e (f ctx args)
| None -> e)
| _ -> e) (* Keep `e`, assuming it's more readable! *)
| Case (l, e, rt, branches, default) ->
@@ -1159,7 +1159,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp =
E.Let (l, edecls, erase_type lctx' body)
| L.Call (fct, args)
- -> E.Call (erase_type lctx fct, Listx.filter_map (clean_arg lctx) args)
+ -> E.Call (erase_type lctx fct, List.filter_map (clean_arg lctx) args)
| L.Case (location, target, _, branches, default)
-> let etarget = erase_type lctx target in
@@ -1227,7 +1227,7 @@ let erase_type lctx lxp =
~print_action:(fun () ->
IMap.iter (fun i (_, t, _, (l, n)) ->
print_endline ("\t" ^ (Source.Location.to_string l)
- ^ " ?" ^ (U.option_default "" n)
+ ^ " ?" ^ (Option.value ~default:"" n)
^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t))
) mvs)
("Metavariables in erase_type :");
=====================================
src/option.ml deleted
=====================================
@@ -1,47 +0,0 @@
-(* Copyright (C) 2020 Free Software Foundation, Inc.
- *
- * Author: Simon Génier <simon.genier(a)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/>. *)
-
-type 'a t = 'a option
-
-let equal (inner_equal : 'a -> 'a -> bool) (l : 'a t) (r : 'a t) : bool =
- match l, r with
- | Some l, Some r -> inner_equal l r
- | None, None -> true
- | _ -> false
-
-let get (o : 'a option) : 'a =
- match o with
- | Some v -> v
- | None -> invalid_arg "expected Some"
-
-let value ~(default : 'a) (o : 'a option) : 'a =
- match o with
- | Some v -> v
- | None -> default
-
-let is_some (o : 'a option) : bool =
- match o with
- | Some _ -> true
- | None -> false
-
-let is_none (o : 'a option) : bool =
- match o with
- | Some _ -> false
- | None -> true
=====================================
src/prelexer.ml
=====================================
@@ -61,7 +61,7 @@ end
(* FIXME: Handle multiline strings. *)
let rec consume_until_newline (source : #Source.t) : unit =
- match source#next_char with
+ match source#next with
| None | Some ('\n') -> ()
| Some _ -> consume_until_newline source
@@ -94,16 +94,16 @@ let prelex (source : #Source.t) : pretoken list =
(* line's bounds seems ok: String.sub line 1 0 == "" *)
| Some ('@')
-> source#advance;
- let start_offset = source#offset in
+ let start_point = source#point in
consume_until_newline source;
- let new_doc = String.trim (source#slice start_offset) in
- loop ctx acc (doc ^ "\n" ^ new_doc)
+ let new_doc, _ = source#slice start_point "" in
+ loop ctx acc (doc ^ "\n" ^ String.trim new_doc)
(* A string. *)
| Some ('"')
-> source#advance;
let rec prestring chars =
- match source#next_char with
+ match source#next with
| None | Some ('\n')
-> let location = source#location doc in
prelexer_error location "Unterminated string";
@@ -115,7 +115,7 @@ let prelex (source : #Source.t) : pretoken list =
loop ctx (pretoken :: acc) ""
| Some ('\\')
- -> (match source#next_char with
+ -> (match source#next with
| None | Some ('\n')
-> let location = source#location doc in
prelexer_error location "Unterminated escape sequence";
@@ -150,30 +150,30 @@ let prelex (source : #Source.t) : pretoken list =
(* A pretoken. *)
| Some _
- -> let start_offset = source#offset in
+ -> let start_point = source#point in
source#advance;
let rec pretok () =
match source#peek with
| None | Some ('%' | '"' | '{' | '}')
- -> let location = source#location doc in
- let text = source#slice start_offset in
+ -> let text, location = source#slice start_point doc in
loop ctx (Pretoken (location, text) :: acc) ""
| Some (c) when c <= ' '
- -> let location = source#location doc in
- let text = source#slice start_offset in
+ -> let text, location = source#slice start_point doc in
source#advance;
loop ctx (Pretoken (location, text) :: acc) ""
| Some ('\\')
-> source#advance;
- (match source#next_char with
+ (match source#next with
| Some _ -> pretok ()
| None
- -> let location = source#location doc in
+ -> let error_location = source#location doc in
source#advance;
- let text = source#slice start_offset in
- prelexer_error location ("Unterminated escape sequence in: " ^ text);
+ let text, location = source#slice start_point doc in
+ prelexer_error
+ error_location
+ ("Unterminated escape sequence in: " ^ text);
loop ctx (Pretoken (location, text) :: acc) "")
| Some _
=====================================
src/source.ml
=====================================
@@ -18,11 +18,29 @@
* 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
+
+ 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
+
module Location = struct
type t = {file : string; line : int; column : int; docstr : string}
let dummy = {file = ""; line = 0; column = 0; docstr = ""}
+ let of_point
+ (file : string)
+ (_, line, column : Point.t)
+ (docstr : string)
+ : t =
+
+ {file; line; column; docstr}
+
let to_string ({file; line; column; _} : t) : string =
Printf.sprintf "%s:%d:%d" file line column
@@ -59,16 +77,22 @@ object (self)
method location (docstr : string) : Location.t =
{file; line; column; docstr}
+ method point : Point.t =
+ (self#offset, line, column)
+
(* The current offset of the cursor in the file, in bytes. *)
- method virtual offset : int
+ method virtual private offset : int
- (* Slices the text, from (and including) a starting offset and to (and
+ (* Slices the text, from (and including) a starting point and to (and
excluding) the curent cursor offset.
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 virtual slice : int -> string
+ method slice (offset, line, column : Point.t) (docstr : string) : string * Location.t =
+ (self#slice_impl offset, {file; line; column; docstr})
+
+ method virtual private slice_impl : int -> string
(* Moves the cursor forward one byte *)
method advance : unit =
@@ -86,7 +110,7 @@ object (self)
method private virtual advance_impl : unit
(* Returns the char at the cursor, then advances it forward. *)
- method next_char : char option =
+ method next : char option =
let c = self#peek in
self#advance;
c
@@ -120,12 +144,12 @@ class source_file file_name = object (self)
with
| End_of_file -> None
- method advance_impl =
+ method private advance_impl =
offset <- offset + 1
- method offset = line_offset + offset
+ method private offset = line_offset + offset
- method slice start_offset =
+ method private slice_impl start_offset =
let relative_start_offset = start_offset - line_offset in
String.sub source_line relative_start_offset (offset - relative_start_offset)
end
@@ -146,11 +170,11 @@ object
then Some (source.[offset])
else None
- method advance_impl =
+ method private advance_impl =
offset <- offset + 1
- method offset = offset
+ method private offset = offset
- method slice start_offset =
+ method private slice_impl start_offset =
String.sub source start_offset (offset - start_offset)
end
=====================================
src/util.ml
=====================================
@@ -20,21 +20,8 @@ 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/>. *)
-(** Adds the update function to maps. This can be removed when we upgrade to
- OCaml >= 4.06 *)
-module UPDATABLE(Base : Map.S) = struct
- include Base
-
- let update key f map =
- let before = find_opt key map in
- match before, f before with
- | _, Some after -> add key after map
- | Some _before, None -> remove key map
- | None, None -> map
-end
-
-module SMap = UPDATABLE(Map.Make(String))
-module IMap = UPDATABLE(Map.Make(Int))
+module SMap = Map.Make(String)
+module IMap = Map.Make(Int)
type charpos = int
type bytepos = int
@@ -66,8 +53,6 @@ let get_vname_name vname =
let string_implode chars = String.concat "" (List.map (String.make 1) chars)
let string_sub str b e = String.sub str b (e - b)
-let opt_map f x = match x with None -> None | Some x -> Some (f x)
-
let str_split str sep =
let str = String.trim str in
let n = String.length str in
@@ -115,16 +100,6 @@ let padding_left (str: string ) (dim: int ) (char_: char) : string =
in let lpad = max diff 0
in (String.make lpad char_) ^ str
-let option_default (default : 'a) (opt : 'a option) : 'a =
- match opt with
- | None -> default
- | Some x -> x
-
-let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option =
- match opt with
- | None -> None
- | Some x -> Some (fn x)
-
(* It seemed good to use the prime number 31.
* FIXME: Pick another one ? *)
let combine_hash e1 e2 = (e1 * 31) lxor e2
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/aff91a5112bd6d143870e6fd5070cb23…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/aff91a5112bd6d143870e6fd5070cb23…
You're receiving this email because of your account on gitlab.com.