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@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@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@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/aff91a5112bd6d143870e6fd5070cb23b...