Simon Génier pushed to branch master at Stefan / Typer

Commits: eb1741eb by Simon Génier at 2020-09-16T09:21:42-04:00 Update the requirements for building typer.

* Add tools and libraries. * Bump OCaml version to the latest one on Debian stable.

- - - - - bcb53b2c by Simon Génier at 2020-09-16T09:21:42-04:00 Use Map.S.find_opt.

- - - - - b36d30ac by Simon Génier at 2020-09-16T09:21:42-04:00 Oops: fix broken tests on OCaml 4.05.0.

- - - - - 1fb4ed6c by Simon Génier at 2020-09-16T09:23:33-04:00 Merge branch 'update-requirements' into HEAD

- - - - -

7 changed files:

- README.md - src/eval.ml - + src/float.ml - + src/int.ml - + src/option.ml - src/util.ml - tests/utest_lib.ml

Changes:

===================================== README.md ===================================== @@ -8,7 +8,11 @@ Status []

## Requirement

-* Ocaml 4.01 +* Ocaml 4.05 +* Ocamlfind +* Ocamlbuild +* Findlib +* Zarith

## Build

@@ -29,4 +33,3 @@ By default ocamlbuild creates a '_build' folder which holds all the compiled fil # Emacs files

/typer-mode.el -

===================================== src/eval.ml ===================================== @@ -744,7 +744,7 @@ let constructor_p name ectx = with Senv_Lookup_Fail _ -> false

let erasable_p name nth ectx = - let is_erasable ctors = match (smap_find_opt name ctors) with + let is_erasable ctors = match (SMap.find_opt name ctors) with | (Some args) -> if (nth < (List.length args) && nth >= 0) then ( match (List.nth args nth) with @@ -763,7 +763,7 @@ let erasable_p name nth ectx =

let erasable_p2 t name ectx = let is_erasable ctors = - match (smap_find_opt t ctors) with + match (SMap.find_opt t ctors) with | Some args -> (List.exists (fun (k, oname, _) @@ -783,7 +783,7 @@ let erasable_p2 t name ectx = with Senv_Lookup_Fail _ -> false

let nth_ctor_arg name nth ectx = - let find_nth ctors = match (smap_find_opt name ctors) with + let find_nth ctors = match (SMap.find_opt name ctors) with | Some args -> (match (List.nth args nth) with | (_, (_, Some n), _) -> n @@ -805,7 +805,7 @@ let ctor_arg_pos name arg ectx = | [] -> None | (_, (_, Some x), _)::xs -> if x = arg then Some n else find_opt xs (n + 1) | _::xs -> find_opt xs (n + 1) in - let find_arg ctors = match (smap_find_opt name ctors) with + let find_arg ctors = match (SMap.find_opt name ctors) with | (Some args) -> ( match (find_opt args 0) with | None -> (-1)

===================================== src/float.ml ===================================== @@ -0,0 +1,25 @@ +(* 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/int.ml ===================================== @@ -0,0 +1,25 @@ +(* 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/option.ml ===================================== @@ -0,0 +1,27 @@ +(* 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

===================================== src/util.ml ===================================== @@ -1,6 +1,6 @@ (* util.ml --- Misc definitions for Typer. -*- coding: utf-8 -*-

-Copyright (C) 2011-2018 Free Software Foundation, Inc. +Copyright (C) 2011-2020 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -20,12 +20,21 @@ 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/. *)

-module SMap = Map.Make (String) -(* Apparently OCaml-4.02 doesn't have find_opt and Debian stable still - * uses 4.02. *) -let smap_find_opt s m = try Some (SMap.find s m) with Not_found -> None - -module IMap = Map.Make (struct type t = int let compare = compare end) +(** 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))

type charpos = int type bytepos = int

===================================== tests/utest_lib.ml ===================================== @@ -31,12 +31,10 @@ * --------------------------------------------------------------------------- *)

open Fmt - -module StringMap = - Map.Make (struct type t = string let compare = String.compare end) +open Util

type test_fun = unit -> int -type section = test_fun StringMap.t * string list +type section = test_fun SMap.t * string list

let success = 0 let failure = -1 @@ -48,7 +46,7 @@ let failure = -1 * "Lambda" - "Base Case" * "Lambda" - "Nested" *) -let global_sections = ref StringMap.empty +let global_sections = ref SMap.empty let insertion_order = ref [] let ret_code = ref 0 let number_test = ref 0 @@ -201,21 +199,21 @@ let add_test section_name test_name test_fun = let update_sections section = let updated_entry = match section with | Some (tests, order) - -> StringMap.update test_name update_tests tests, test_name :: order + -> SMap.update test_name update_tests tests, test_name :: order | None -> (insertion_order := section_name :: !insertion_order; - StringMap.singleton test_name test_fun, [test_name]) + SMap.singleton test_name test_fun, [test_name]) in Some updated_entry in - global_sections := StringMap.update section_name update_sections !global_sections + global_sections := SMap.update section_name update_sections !global_sections

(* sk : Section Key * tmap: test_name -> tmap * tk : Test Key *) let for_all_tests sk tmap tk = if (must_run_title tk) then ( - let tv = StringMap.find tk tmap in + let tv = SMap.find tk tmap in flush stdout; Log.clear_log (); try @@ -236,7 +234,7 @@ let for_all_tests sk tmap tk = unexpected_throw sk tk e) else ()

let for_all_sections sk = - let tmap, tst = StringMap.find sk (!global_sections) in + let tmap, tst = SMap.find sk (!global_sections) in let tst = List.rev tst in if must_run_section sk then (

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