Jean-Alexandre Barszcz pushed to branch depelim 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

- - - - - 371c37d4 by Jean-Alexandre Barszcz at 2020-09-19T23:59:22-04:00 Big ints in sexps and for int literals

* Change the sexp datatype to have Zarith big integers instead of plain Ocaml `int`s. * Change the type of integer literals to `Integer` instead of `Int`. * Add the `Integer->Int` builtin. * Add overflow checking to the `Int` builtin operators.

- - - - - 12076610 by Jean-Alexandre Barszcz at 2020-09-20T00:01:57-04:00 Improve quoting

- - - - - 695d98c7 by Jean-Alexandre Barszcz at 2020-09-20T00:01:57-04:00 Add a macro for dependent elimination

- - - - -

26 changed files:

- README.md - btl/builtins.typer - btl/case.typer - + btl/depelim.typer - btl/do.typer - btl/list.typer - btl/pervasive.typer - btl/plain-let.typer - btl/polyfun.typer - btl/tuple.typer - src/debug.ml - src/elab.ml - src/eval.ml - + src/float.ml - + src/int.ml - src/lexer.ml - src/lexp.ml - src/opslexp.ml - + src/option.ml - src/sexp.ml - src/util.ml - tests/elab_test.ml - tests/eval_test.ml - tests/macro_test.ml - tests/unify_test.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 -

===================================== btl/builtins.typer ===================================== @@ -108,11 +108,6 @@ Int_- = Built-in "Int.-" : Int -> Int -> Int; Int_* = Built-in "Int.*" : Int -> Int -> Int; Int_/ = Built-in "Int./" : Int -> Int -> Int;

-_+_ = Int_+; -_-_ = Int_-; -_*_ = Int_*; -_/_ = Int_/; - %% modulo Int_mod = Built-in "Int.mod" : Int -> Int -> Int;

@@ -133,7 +128,15 @@ Int_>= = Built-in "Int.>=" : Int -> Int -> Bool; %% bitwise negation Int_not = Built-in "Int.not" : Int -> Int;

+%% `Int` and `Integer` are conceptually isomorphic in that they both +%% represent unbounded integers, but in reality, both are bounded. +%% `Int` is implemented with `int` type in ocaml (31 or 63 bits), and +%% `Integer` is implemented with big integers (ultimately limited by +%% available memory). Both cause runtime errors at their limits, so no +%% overflows are allowed. Here are the functions that witness the +%% isomorphism: Int->Integer = Built-in "Int->Integer" : Int -> Integer; +Integer->Int = Built-in "Integer->Int" : Integer -> Int;

Int->String = Built-in "Int->String" : Int -> String;

@@ -142,6 +145,11 @@ Integer_- = Built-in "Integer.-" : Integer -> Integer -> Integer; Integer_* = Built-in "Integer.*" : Integer -> Integer -> Integer; Integer_/ = Built-in "Integer./" : Integer -> Integer -> Integer;

+_+_ = Integer_+; +_-_ = Integer_-; +_*_ = Integer_*; +_/_ = Integer_/; + Integer_< = Built-in "Integer.<" : Integer -> Integer -> Bool; Integer_> = Built-in "Integer.>" : Integer -> Integer -> Bool; Integer_eq = Built-in "Integer.=" : Integer -> Integer -> Bool;

===================================== btl/case.typer ===================================== @@ -156,7 +156,7 @@ get-branches vars sexps = let to-case sexp = let

tup-exprs : Sexp -> List Sexp; - tup-exprs sexp = if (Int_eq (List_length vars) 1) then + tup-exprs sexp = if (Int_eq (List_length vars) (Integer->Int 1)) then (cons (expand-tuple-ctor sexp) nil) else (List_map expand-tuple-ctor (get-tup-exprs sexp)); @@ -165,7 +165,7 @@ get-branches vars sexps = let

(lambda s ss -> case (Sexp_eq (Sexp_symbol "_=>_") s) %% expecting a Sexp_node as second argument to _=>_ - | true => pair (tup-exprs (List_nth 0 ss Pat_error)) (List_nth 1 ss Code_error) + | true => pair (tup-exprs (List_nth (Integer->Int 0) ss Pat_error)) (List_nth (Integer->Int 1) ss Code_error) | false => pair (cons Pat_error nil) Code_error)

perr perr perr perr perr; @@ -232,10 +232,11 @@ kinds pat = let mf : Elab_Context -> Sexp -> Int -> Bool; mf env arg i = Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_:=_")) then - ( if (Sexp_eq (List_nth 0 ss Sexp_error) dflt-var) then + ( if (Sexp_eq (List_nth (Integer->Int 0) ss Sexp_error) dflt-var) then (Elab_is-nth-erasable ctor i env) else - (Elab_is-arg-erasable ctor (str_of_sym (List_nth 0 ss Sexp_error)) env) ) + (Elab_is-arg-erasable ctor + (str_of_sym (List_nth (Integer->Int 0) ss Sexp_error)) env) ) else (false)) (lambda _ -> false) @@ -313,7 +314,7 @@ renamed-pat pat names = let %% I expect it to not compile... (Sexp_node sym ss) else - (Sexp_node sym (cons (List_nth 0 ss Sexp_error) (cons (List_nth i names Sexp_error) nil))) + (Sexp_node sym (cons (List_nth (Integer->Int 0) ss Sexp_error) (cons (List_nth i names Sexp_error) nil))) else if tup then %% tuples argument are all implicit so we must take special care of those (Sexp_node (Sexp_symbol "_:=_") @@ -407,7 +408,7 @@ introduced-vars pat = let %% %% error used in Sexp_dispatch %% - serr = lambda _ -> IO_return (pair 0 nil); + serr = lambda _ -> IO_return (pair (Integer->Int 0) nil);

%% %% List of kind of pattern argument @@ -440,11 +441,12 @@ introduced-vars pat = let ks <- ks; if (Sexp_eq s (Sexp_symbol "_:=_")) then if (List_nth i ks false) then - (IO_return (pair (i + 1) (List_concat o (cons dflt-var nil)))) + (IO_return (pair (Int_+ i (Integer->Int 1)) (List_concat o (cons dflt-var nil)))) else - (IO_return (pair (i + 1) (List_concat o (cons (List_nth 1 ss Var_error) nil)))) + (IO_return (pair (Int_+ i (Integer->Int 1)) + (List_concat o (cons (List_nth (Integer->Int 1) ss Var_error) nil)))) else - (IO_return (pair (i + 1) (List_concat o (cons dflt-var nil)))); + (IO_return (pair (Int_+ i (Integer->Int 1)) (List_concat o (cons dflt-var nil)))); }) (lambda s -> do { o <- o; % bind @@ -452,15 +454,15 @@ introduced-vars pat = let sym <- IO_return (Sexp_symbol s); b <- is-pat sym; if (b) then - (IO_return (pair (i + 1) (List_concat o (cons dflt-var nil)))) + (IO_return (pair (Int_+ i (Integer->Int 1)) (List_concat o (cons dflt-var nil)))) else - (IO_return (pair (i + 1) (List_concat o (cons sym nil)))); + (IO_return (pair (Int_+ i (Integer->Int 1)) (List_concat o (cons sym nil)))); }) serr serr serr serr;

in Sexp_dispatch pat (lambda _ ss -> do { - p <- (List_foldl ff (IO_return (pair 0 nil)) ss); + p <- (List_foldl ff (IO_return (pair (Integer->Int 0) nil)) ss); IO_return (case p | pair _ xs => xs); }) @@ -492,7 +494,7 @@ head-pats ps = let %% mf : Pair Pats Code -> Pat; mf p = case p - | pair pats _ => (List_nth 0 pats Pat_error); + | pair pats _ => (List_nth (Integer->Int 0) pats Pat_error);

in List_map mf ps;

@@ -681,7 +683,7 @@ partition-branches branches = let (List_concat tt (cons tail nil))) (ff parts p)) % This line sometimes produce too many patterns else - (if (similar? pat (List_nth 0 ps Pat_error)) then + (if (similar? pat (List_nth (Integer->Int 0) ps Pat_error)) then (case part | pair pp tt => cons (pair (List_concat pp (cons pat nil)) (List_concat tt (cons tail nil))) @@ -711,7 +713,7 @@ partition-branches branches = let mf : pre-part-type -> IO part-type; mf p = case p | pair pp tt => do { - pat <- IO_return (List_nth 0 pp Pat_error); + pat <- IO_return (List_nth (Integer->Int 0) pp Pat_error); ivars <- introduced-vars pat; rvars <- gen-vars ivars; rpat <- renamed-pat pat rvars; @@ -819,20 +821,20 @@ adjust-len branches = let else (n);

- in List_foldl ff 0 branches; + in List_foldl ff (Integer->Int 0) branches;

preppend-dflt : Int -> Pair Pats Code -> Pair Pats Code; preppend-dflt n branch = let

sup : Int -> Pats; sup n = - if (Int_eq n 0) then + if (Int_eq n (Integer->Int 0)) then (nil) else - (cons dflt-var (sup (n - 1))); + (cons dflt-var (sup (Int_- n (Integer->Int 1))));

in case branch | pair pats code => - pair (List_concat (sup (n - (List_length pats))) pats) code; + pair (List_concat (sup (Int_- n (List_length pats))) pats) code;

in List_map (preppend-dflt max-len) branches;

@@ -852,7 +854,7 @@ in List_map (preppend-dflt max-len) branches; compile-case : List Var -> List (Pair Pats Code) -> IO Code; compile-case subjects branches = let

- subject = (List_nth 0 subjects Var_error); + subject = (List_nth (Integer->Int 0) subjects Var_error);

%% %% Get partition of branches @@ -1025,7 +1027,7 @@ case-impl args = let

%% Expecting only one Sexp_node containing a case with arguments

-in (Sexp_dispatch (List_nth 0 args Sexp_error) +in (Sexp_dispatch (List_nth (Integer->Int 0) args Sexp_error) case1 err err err err err);

case-macro = macro case-impl;

===================================== btl/depelim.typer ===================================== @@ -0,0 +1,111 @@ +%%% depelim --- A macro for dependent elimination + +%% Copyright (C) 2020 Free Software Foundation, Inc. +%% +%% Author: Jean-Alexandre Barszcz jean-alexandre.barszcz@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/. + +%%% Description + +%% In Typer, the branch bodies of a `case` expression must all have +%% the same type. In order to write proofs that depend the +%% constructor, Typer adds a proof in the environment of each branch: +%% the equality between the branch's head and the case target. This +%% equality can be eliminated in each branch using `Eq_cast` to go +%% from a branch-dependent type to a target-dependent type. The +%% following macro eases this process by eliminating the boilerplate. + +%% The macro extends the builtin `case` syntax to +%% `case_as_return_`. The `as` and `return` clauses are used to build +%% Eq_cast's `f` argument (a lambda). The `as` clause should contain a +%% symbol (the variable binding the case target or branch head), and +%% is optional if the target is itself a symbol. The `return` clause +%% is `f`'s body, i.e. the return type of the case, using the variable +%% from the `as` clause to refer to the target or branch head. + +%%% Example usage + +%% type Nat +%% | Z +%% | S Nat; +%% +%% Nat_induction : +%% (P : Nat -> Type_ ?l) ≡> +%% P Z -> +%% ((n : Nat) -> P n -> P (S n)) -> +%% ((n : Nat) -> P n); +%% Nat_induction base step n = +%% case n return (P n) %% <-- `as` clause omitted: the target is a var.. +%% | Z => base +%% | S n' => (step n' (Nat_induction (P := P) base step n')); + +%%% Grammar + +%% This macro was written for the following operators (the precedence +%% level 42 is chosen to match that of the builtin case): +%% +%% define-operator "as" 42 42; +%% define-operator "return" 42 42; + +case_as_return_impl args = + let impl target_sexp var_sexp ret_and_branches_sexp = + case Sexp_wrap ret_and_branches_sexp + | node hd (cons ret_sexp branches) => + %% TODO Check that var_sexp is a variable. + %% TODO Check that hd is the symbol `_|_`. + let + on_branch branch_sexp = + case Sexp_wrap branch_sexp + | node arrow_sexp (cons head_sexp (cons body_sexp nil)) => + %% TODO Check that arrow_sexp is `=>`. + Sexp_node + arrow_sexp + (cons head_sexp + (cons (quote (##Eq.cast + (x := uquote head_sexp) + (y := uquote target_sexp) + (p := ##DeBruijn 0) + (f := lambda (uquote var_sexp) -> + uquote ret_sexp) + (uquote body_sexp))) + nil)) + | _ => Sexp_error; %% FIXME improve error reporting + new_branches = List_map on_branch branches; + in %% We extend the builtin case, so nested patterns don't work + quote (##case_ + (uquote (Sexp_node (Sexp_symbol "_|_") + (cons target_sexp new_branches)))) + | _ => Sexp_error; + in IO_return + case args + | cons target_sexp + (cons var_sexp + (cons ret_and_branches_sexp nil)) + => impl target_sexp var_sexp ret_and_branches_sexp + | cons target_sexp + (cons ret_and_branches_sexp nil) + => %% If the `as` clause is omitted, and the target is a + %% symbol, use it for `var_sexp` as well. + (case Sexp_wrap target_sexp + | symbol _ => impl target_sexp target_sexp ret_and_branches_sexp + | _ => Sexp_error) + | _ => Sexp_error; + +case_as_return_ = macro case_as_return_impl; +case_return_ = macro case_as_return_impl; +

===================================== btl/do.typer ===================================== @@ -33,7 +33,7 @@ get-sym sexp = let

in Sexp_dispatch sexp (lambda s ss -> if (Sexp_eq s assign) then - (List_nth 0 ss Sexp_error) + (List_nth (Integer->Int 0) ss Sexp_error) else (dflt-sym ())) dflt-sym dflt-sym dflt-sym @@ -57,7 +57,7 @@ get-op sexp = let helper = (lambda sexp -> Sexp_dispatch sexp

( lambda s ss -> if (Sexp_eq s assign) then - (Sexp_node (List_nth 1 ss Sexp_error) (List_tail (List_tail ss))) + (Sexp_node (List_nth (Integer->Int 1) ss Sexp_error) (List_tail (List_tail ss))) else (Sexp_node s ss) ) @@ -80,7 +80,7 @@ get-decl ctx args = let

%% Expecting a Block of command separated by ";"

- node = Sexp_dispatch (List_nth 0 args Sexp_error) + node = Sexp_dispatch (List_nth (Integer->Int 0) args Sexp_error)

(K err) err err err err

===================================== btl/list.typer ===================================== @@ -28,15 +28,15 @@ %% helper : (a : Type) ≡> Int -> List a -> Int; %% helper len xs = case xs %% | nil => len -%% | cons hd tl => helper (len + 1) tl; -%% in helper 0 xs; +%% | cons hd tl => helper (Int_+ len (Integer->Int 1)) tl; +%% in helper (Integer->Int 0) xs; %% %% length : (a : Type) ≡> List a -> Int; length xs = case xs - | nil => 0 + | nil => (Integer->Int 0) | cons hd tl => - (1 + (length tl)); + (Int_+ (Integer->Int 1) (length tl));

%% %% ML's typical `head` function is not total, so can't be defined @@ -88,8 +88,8 @@ mapi = lambda f -> lambda xs -> let helper : (a -> Int -> b) -> Int -> List a -> List b; helper = lambda f -> lambda i -> lambda xs -> case xs | nil => nil - | cons x xs => cons (f x i) (helper f (i + 1) xs); -in helper f 0 xs; + | cons x xs => cons (f x i) (helper f (Int_+ i (Integer->Int 1)) xs); +in helper f (Integer->Int 0) xs;

%% %% As `map` but with 2 list at the same time @@ -110,8 +110,8 @@ foldli = lambda f -> lambda o -> lambda xs -> let helper : (a -> b -> Int -> a) -> Int -> a -> List b -> a; helper = lambda f -> lambda i -> lambda o -> lambda xs -> case xs | nil => o - | cons x xs => helper f (i + 1) (f o x i) xs; -in helper f 0 o xs; + | cons x xs => helper f (Int_+ i (Integer->Int 1)) (f o x i) xs; +in helper f (Integer->Int 0) o xs;

%% %% Fold 2 List as long as both List are non-empty @@ -148,9 +148,9 @@ nth : (a : Type) ≡> Int -> List a -> a -> a; nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d | cons x xs - => case Int_<= n 0 + => case Int_<= n (Integer->Int 0) | true => x - | false => nth (n - 1) xs d; + | false => nth (Int_- n (Integer->Int 1)) xs d;

%% %% Reverse the element of a list @@ -223,7 +223,7 @@ in map mf xs; empty? : (a : Type) ≡> List a -> Bool; %% %% O(N): -%% empty? = lambda xs -> Int_eq (length xs) 0; +%% empty? = lambda xs -> Int_eq (length xs) (Integer->Int 0); %% %% O(1): empty? = lambda xs -> case xs

===================================== btl/pervasive.typer ===================================== @@ -40,9 +40,9 @@ none = datacons Option none;

List_length : List ?a -> Int; % Recursive defs aren't generalized :-( List_length xs = case xs - | nil => 0 + | nil => (Integer->Int 0) | cons hd tl => - (1 + (List_length tl)); + (Int_+ (Integer->Int 1) (List_length tl));

%% ML's typical `head` function is not total, so can't be defined %% as-is in Typer. There are several workarounds: @@ -80,9 +80,9 @@ List_nth : Int -> List ?a -> ?a -> ?a; List_nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d | cons x xs - => case Int_<= n 0 + => case Int_<= n (Integer->Int 0) | true => x - | false => List_nth (n - 1) xs d; + | false => List_nth (Int_- n (Integer->Int 1)) xs d;

%%%% A more flexible `lambda`

@@ -155,8 +155,8 @@ List_mapi f xs = let helper : (a -> Int -> b) -> Int -> List a -> List b; helper f i xs = case xs | nil => nil - | cons x xs => cons (f x i) (helper f (i + 1) xs); -in helper f 0 xs; + | cons x xs => cons (f x i) (helper f (Int_+ i (Integer->Int 1)) xs); +in helper f (Integer->Int 0) xs;

List_map2 : (?a -> ?b -> ?c) -> List ?a -> List ?b -> List ?c; List_map2 f xs ys = case xs @@ -175,7 +175,7 @@ List_fold2 f o xs ys = case xs

%% Is argument List empty? List_empty : List ?a -> Bool; -List_empty xs = Int_eq (List_length xs) 0; +List_empty xs = Int_eq (List_length xs) (Integer->Int 0);

%%% Good 'ol combinators

@@ -203,21 +203,30 @@ K x y = x; %% which will construct an Sexp equivalent to `x` at run-time. %% This is basically *cross stage persistence* for Sexp. quote1 : Sexp -> Sexp; -quote1 x = let k = K x; +quote1 x = let qlist : List Sexp -> Sexp; qlist xs = case xs | nil => Sexp_symbol "nil" | cons x xs => Sexp_node (Sexp_symbol "cons") (cons (quote1 x) (cons (qlist xs) nil)); + make_app str sexp = + Sexp_node (Sexp_symbol str) (cons sexp nil); + node op y = case (Sexp_eq op (Sexp_symbol "uquote")) | true => List_head Sexp_error y | false => Sexp_node (Sexp_symbol "##Sexp.node") (cons (quote1 op) (cons (qlist y) nil)); - symbol s = Sexp_node (Sexp_symbol "##Sexp.symbol") - (cons (Sexp_string s) nil) - in Sexp_dispatch x node symbol k k k k; + symbol s = make_app "##Sexp.symbol" (Sexp_string s); + string s = make_app "##Sexp.string" (Sexp_string s); + integer i = make_app "##Sexp.integer" (Sexp_integer i); + float f = make_app "##Sexp.float" (Sexp_float f); + block sxp = + %% FIXME ##Sexp.block takes a string (and prelexes + %% it) but we have a sexp, what should we do? + Sexp_symbol "<error FIXME block quoting>"; + in Sexp_dispatch x node symbol string integer float block;

%% quote definition quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x))); @@ -302,7 +311,7 @@ type-impl = lambda (x : List Sexp) -> get-type sxp = Sexp_dispatch sxp (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_")) - | true => List_nth 1 ss Sexp_error + | true => List_nth (Integer->Int 1) ss Sexp_error | false => sxp) (lambda _ -> sxp) (lambda _ -> Sexp_error) @@ -464,8 +473,8 @@ Decidable = typecons (Decidable (prop : Type_ ?ℓ)) %% Testing generalization in inductive type constructors. LList : Type -> Int -> Type; %FIXME: `LList : ?` should be sufficient! type LList (a : Type) (n : Int) - | vnil (p ::: Eq n 0) - | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound! + | vnil (p ::: Eq n (Integer->Int 0)) + | vcons a (LList a ?n1) (p ::: Eq n (Int_+ ?n1 (Integer->Int 1)));

%%%% If

@@ -475,9 +484,9 @@ define-operator "else" 1 66;

if_then_else_ = macro (lambda args -> - let e1 = List_nth 0 args Sexp_error; - e2 = List_nth 1 args Sexp_error; - e3 = List_nth 2 args Sexp_error; + let e1 = List_nth (Integer->Int 0) args Sexp_error; + e2 = List_nth (Integer->Int 1) args Sexp_error; + e3 = List_nth (Integer->Int 2) args Sexp_error; in IO_return (quote (case uquote e1 | true => uquote e2 | false => uquote e3))); @@ -543,7 +552,7 @@ in case (String_eq r "_") %% Elab_arg-pos a b c = let r = Elab_arg-pos' a b c; -in case (Int_eq r (-1)) +in case (Int_eq r (Integer->Int -1)) | true => (none) | false => (some r);

@@ -634,6 +643,17 @@ plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; %% _|_ = let lib = load "btl/polyfun.typer" in lib._|_;

+%% +%% case_as_return_, case_return_ +%% A `case` for dependent elimination +%% + +define-operator "as" 42 42; +define-operator "return" 42 42; +depelim = load "btl/depelim.typer"; +case_as_return_ = depelim.case_as_return_; +case_return_ = depelim.case_return_; + %%%% Unit tests function for doing file

%% It's hard to do a primitive which execute test file @@ -656,7 +676,7 @@ Test_file = macro (lambda args -> let (cons (Sexp_symbol "unit") nil);

%% Expecting a String and nothing else -in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) +in IO_return (Sexp_dispatch (List_nth (Integer->Int 0) args Sexp_error) (lambda _ _ -> ret) (lambda _ -> ret) %% `load` is a special form and takes a Sexp rather than a real `String`

===================================== btl/plain-let.typer ===================================== @@ -47,7 +47,7 @@ impl args = let

in Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then - (rename (List_nth 0 ss Sexp_error)) else + (rename (List_nth (Integer->Int 0) ss Sexp_error)) else (IO_return Sexp_error)) io-serr io-serr io-serr io-serr io-serr;

@@ -55,7 +55,7 @@ impl args = let get-def : Sexp -> Sexp; get-def arg = Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then - (List_nth 1 ss Sexp_error) else + (List_nth (Integer->Int 1) ss Sexp_error) else (Sexp_error)) serr serr serr serr serr;

@@ -63,7 +63,7 @@ impl args = let get-var : Sexp -> Sexp; get-var arg = Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then - (List_nth 0 ss Sexp_error) else + (List_nth (Integer->Int 0) ss Sexp_error) else (Sexp_error)) serr serr serr serr serr;

@@ -138,8 +138,8 @@ impl args = let in do { %% get list of pair and use it to generate `plain-let`

- defs <- IO_return (get-decls (List_nth 0 args Sexp_error)); - body <- IO_return (List_nth 1 args Sexp_error); + defs <- IO_return (get-decls (List_nth (Integer->Int 0) args Sexp_error)); + body <- IO_return (List_nth (Integer->Int 1) args Sexp_error); sym-def <- get-sym-def defs; sym-def <- IO_return (List_reverse (List_tail sym-def) nil); var-sym <- get-var-sym defs sym-def;

===================================== btl/polyfun.typer ===================================== @@ -40,7 +40,7 @@ fun-args decl = Sexp_dispatch decl mf arg = Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_:_")) then - (List_nth 0 ss Sexp_error) + (List_nth (Integer->Int 0) ss Sexp_error) else (Sexp_node s ss)) (lambda s -> Sexp_symbol s) @@ -64,7 +64,7 @@ fun-cases args = let in Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=>_")) then - (pair (List_nth 0 ss Sexp_error) (List_nth 1 ss Sexp_error)) + (pair (List_nth (Integer->Int 0) ss Sexp_error) (List_nth (Integer->Int 1) ss Sexp_error)) else (err ())) err err err err err; @@ -84,14 +84,14 @@ cases-to-sexp vars cases = let (cons pat (cons body nil));

tup : Bool; - tup = Int_< 1 (List_length vars); + tup = Int_< (Integer->Int 1) (List_length vars);

in Sexp_node (Sexp_symbol "case_") (cons (Sexp_node (Sexp_symbol "_|_") (cons (if tup then (Sexp_node (Sexp_symbol "_,_") vars) else - (List_nth 0 vars Sexp_error)) + (List_nth (Integer->Int 0) vars Sexp_error)) (List_map mf cases))) nil);

%% @@ -103,7 +103,7 @@ _|_ = macro (lambda args -> let

%% function with argument (e.g. `f x y`) decl : Sexp; - decl = List_nth 0 args Sexp_error; + decl = List_nth (Integer->Int 0) args Sexp_error;

%% symbol to match fargs : List Sexp;

===================================== btl/tuple.typer ===================================== @@ -90,11 +90,11 @@ gen-deduce vars = List_map %% tuple-nth = macro (lambda args -> let

- nerr = lambda _ -> (Int->Integer (-1)); + nerr = lambda _ -> (-1);

%% argument `n` of this macro n : Integer; - n = Sexp_dispatch (List_nth 1 args Sexp_error) + n = Sexp_dispatch (List_nth (Integer->Int 1) args Sexp_error) (lambda _ _ -> nerr ()) nerr nerr (lambda n -> n) @@ -106,7 +106,7 @@ tuple-nth = macro (lambda args -> let

%% tuple, argument of this macro tup : Sexp; - tup = List_nth 0 args Sexp_error; + tup = List_nth (Integer->Int 0) args Sexp_error;

in IO_return (Sexp_node (Sexp_symbol "__.__") (cons tup (cons elem-sym nil))) ); @@ -145,8 +145,8 @@ assign-tuple = macro (lambda args -> let

in do { IO_return (Sexp_node (Sexp_symbol "_;_") (List_mapi - (mf (List_nth 1 args Sexp_error)) - (get-tup-elem (List_nth 0 args Sexp_error)))); + (mf (List_nth (Integer->Int 1) args Sexp_error)) + (get-tup-elem (List_nth (Integer->Int 0) args Sexp_error)))); });

%%

===================================== src/debug.ml ===================================== @@ -90,7 +90,7 @@ let rec debug_sexp_print sexp = print_string """; print_string str; print_string """

| Integer(loc, n) - -> print_info "Integer: " loc; print_int n + -> print_info "Integer: " loc; Z.print n

| Float(loc, x) -> print_info "Float: " loc; print_float x

===================================== src/elab.ml ===================================== @@ -278,7 +278,7 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = | [String (_, name); l; r] -> let level s = match s with | Symbol (_, "") -> None - | Integer (_, n) -> Some n + | Integer (_, n) -> Some (Z.to_int n) | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in let (grm, a, b, c) = ctx in (SMap.add name (level l, level r) grm, a, b, c) @@ -1596,7 +1596,7 @@ let sform_arrow kind ctx loc sargs ot = let sform_immediate ctx loc sargs ot = match sargs with | [(String _) as se] -> mkImm (se), Inferred DB.type_string - | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int + | [(Integer _) as se] -> mkImm (se), Inferred DB.type_integer | [(Float _) as se] -> mkImm (se), Inferred DB.type_float | [Block (sl, pts, el)] -> let grm = ectx_get_grammar ctx in @@ -1803,7 +1803,7 @@ let sform_type ctx loc sargs ot = let sform_debruijn ctx loc sargs ot = match sargs with | [Integer (l,i)] - -> if i < 0 || i > get_size ctx then + -> let i = Z.to_int i in if i < 0 || i > get_size ctx then (sexp_error l "##DeBruijn index out of bounds"; sform_dummy_ret ctx loc) else

===================================== src/eval.ml ===================================== @@ -151,17 +151,68 @@ let add_binary_iop name f = | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in add_builtin_function name f 2

-let _ = add_binary_iop "+" (+); - add_binary_iop "-" (-); - add_binary_iop "*" ( * ); - add_binary_iop "/" (/); +let add_binary_iop_with_loc name f = + let name = "Int." ^ name in + let f loc (depth : eval_debug_info) (args_val: value_type list) = + match args_val with + | [Vint (v); Vint (w)] -> Vint (f loc v w) + | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in + add_builtin_function name f 2 + +let add_with_overflow loc a b = + let c = a + b in + (* Check that signs of both args are diff. OR sign of result is the + same as the sign of the args. *) + if (a lxor b) lor (a lxor (lnot c)) < 0 + then c + else error loc "Overflow in `Int.+`" + +let sub_with_overflow loc a b = + let c = a - b in + (* Check that signs of both args are the same OR sign of result is + the same as the sign of the first arg. *) + if (a lxor (lnot b)) lor (a lxor (lnot c)) < 0 + then c + else error loc "Overflow in `Int.-`" + +let mul_with_overflow loc a b = + let c = a * b in + if b = 0 || not (c = min_int && b = -1) && a = c / b (* Simple but slow *) + then c + else error loc "Overflow in `Int.*`" + +let div_with_overflow loc a b = + if not (a = min_int && b = -1) + then a / b + else error loc "Overflow in `Int./`" + +let lsl_with_overflow loc a b = + if b < 0 || b > Sys.int_size + then error loc ("Invalid shift value `" ^ (string_of_int b) ^ "` in `Int.lsl`") + else a lsl b + +let lsr_with_overflow loc a b = + if b < 0 || b > Sys.int_size + then error loc ("Invalid shift value `" ^ (string_of_int b) ^ "` in `Int.lsr`") + else a lsr b + +let asr_with_overflow loc a b = + if b < 0 || b > Sys.int_size + then error loc ("Invalid shift value `" ^ (string_of_int b) ^ "` in `Int.asr`") + else a asr b + +let _ = add_binary_iop_with_loc "+" add_with_overflow; + add_binary_iop_with_loc "-" sub_with_overflow; + add_binary_iop_with_loc "*" mul_with_overflow; + add_binary_iop_with_loc "/" div_with_overflow; + + add_binary_iop_with_loc "lsl" lsl_with_overflow; + add_binary_iop_with_loc "lsr" lsr_with_overflow; + add_binary_iop_with_loc "asr" asr_with_overflow;

add_binary_iop "mod" (mod); add_binary_iop "and" (land); - add_binary_iop "or" (lor); - add_binary_iop "lsl" (lsl); - add_binary_iop "lsr" (lsr); - add_binary_iop "asr"(asr); + add_binary_iop "or" (lor); add_binary_iop "xor" (lxor)

let add_binary_bool_iop name f = @@ -221,6 +272,16 @@ let _ = add_binary_bool_biop "<" BI.lt; -> match args_val with | [Vint v] -> Vinteger (BI.of_int v) | _ -> error loc ("`" ^ name ^ "` expects 1 Int argument")) + 1; + let name = "Integer->Int" in + add_builtin_function + name + (fun loc (depth : eval_debug_info) (args_val: value_type list) + -> match args_val with + | [Vinteger v] -> + (try Vint (BI.to_int v) with + | Z.Overflow -> error loc ("Overflow in `" ^ name ^ "`")) + | _ -> error loc ("`" ^ name ^ "` expects 1 Integer argument")) 1

(* Floating point numers. *) @@ -283,7 +344,7 @@ let make_string loc depth args_val = match args_val with | _ -> error loc "Sexp.string expects one string as argument"

let make_integer loc depth args_val = match args_val with - | [Vinteger n] -> Vsexp (Integer (loc, BI.to_int n)) + | [Vinteger n] -> Vsexp (Integer (loc, n)) | _ -> error loc "Sexp.integer expects one integer as argument"

let make_float loc depth args_val = match args_val with @@ -373,7 +434,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) match lxp with (* Leafs *) (* ---------------- *) - | Imm(Integer (_, i)) -> Vint i + | Imm(Integer (_, i)) -> Vinteger i | Imm(String (_, s)) -> Vstring s | Imm(Float (_, n)) -> Vfloat n | Imm(sxp) -> Vsexp sxp @@ -567,7 +628,7 @@ and sexp_dispatch loc depth args = | 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 [Vint i] + | Integer (_ , i) -> eval_call it [Vinteger i] | Float (_ , f) -> eval_call flt [Vfloat f] | Block (_ , _, _) as b -> (* I think this code breaks what Blocks are. *) @@ -744,7 +805,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 +824,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 +844,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 +866,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/lexer.ml ===================================== @@ -58,7 +58,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos if bp >= String.length name then ((if np == NPint then Integer ({file;line;column=column+cpos;docstr=docstr}, - int_of_string (string_sub name bpos bp)) + Z.of_string (string_sub name bpos bp)) else Float ({file;line;column=column+cpos;docstr=docstr}, float_of_string (string_sub name bpos bp))), @@ -75,7 +75,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos | _ -> ((if np == NPint then Integer ({file;line;column=column+cpos;docstr=docstr}, - int_of_string (string_sub name bpos bp)) + Z.of_string (string_sub name bpos bp)) else Float ({file;line;column=column+cpos;docstr=docstr}, float_of_string (string_sub name bpos bp))),

===================================== src/lexp.ml ===================================== @@ -962,7 +962,7 @@ and lexp_str ctx (exp : lexp) : string = match lexp_lexp' exp with | Imm(value) -> (match value with | String (_, s) -> tval (""" ^ s ^ """) - | Integer(_, s) -> tval (string_of_int s) + | Integer(_, s) -> tval (Z.to_string s) | Float (_, s) -> tval (string_of_float s) | e -> sexp_string e)

===================================== src/opslexp.ml ===================================== @@ -566,7 +566,7 @@ and check'' erased ctx e = s in match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float - | Imm (Integer (_, _)) -> DB.type_int + | Imm (Integer (_, _)) -> DB.type_integer | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; @@ -960,7 +960,7 @@ and fv (e : lexp) : (DB.set * mv_set) = and get_type ctx e = match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float - | Imm (Integer (_, _)) -> DB.type_int + | Imm (Integer (_, _)) -> DB.type_integer | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t, _) -> t

===================================== 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/sexp.ml ===================================== @@ -27,16 +27,13 @@ open Grammar let sexp_error ?print_action loc msg = Log.log_error ~section:"SEXP" ?print_action ~loc msg

-type integer = (* Num.num *) int +type integer = Z.t type symbol = location * string

type sexp = (* Syntactic expression, kind of like Lisp. *) | Block of location * pretoken list * location | Symbol of symbol | String of location * string - (* FIXME: It would make a lof of sense to use a bigint here, but `compare` - * burps on Big_int objects, and `compare` is used for hash-consing of lexp - * objects which contain sexp objects as well. *) | Integer of location * integer | Float of location * float | Node of sexp * sexp list @@ -76,7 +73,7 @@ let rec sexp_string sexp = | Symbol(_, "") -> "()" (* Epsilon *) | Symbol(_, name) -> name | String(_, str) -> """ ^ str ^ """ - | Integer(_, n) -> string_of_int n + | Integer(_, n) -> Z.to_string n | Float(_, x) -> string_of_float x | Node(f, args) -> let str = "(" ^ (sexp_string f) in

===================================== 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/elab_test.ml ===================================== @@ -51,7 +51,7 @@ let add_elab_test_decl = let _ = add_elab_test_expr "Instanciate implicit arguments" ~setup:{| -f : (i : Int) -> Eq i i -> Int; +f : (i : Integer) -> Eq i i -> Integer; f = lambda i -> lambda eq -> i; |} ~expected:"f 4 (Eq_refl (x := 4));" @@ -107,6 +107,24 @@ plus x y = Eq_refl); |}

+let _ = add_elab_test_decl + "depelim macro" + {| +type Nat + | Z + | S Nat; + +Nat_induction : + (P : Nat -> Type_ ?l) ≡> + P Z -> + ((n : Nat) -> P n -> P (S n)) -> + ((n : Nat) -> P n); +Nat_induction base step n = + case n return (P n) + | Z => base + | S n' => (step n' (Nat_induction (P := P) base step n')); + |} + let _ = add_elab_test_decl "case conversion" {|

===================================== tests/eval_test.ml ===================================== @@ -112,7 +112,7 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Lambda"

- "sqr : Int -> Int; + "sqr : Integer -> Integer; sqr = lambda x -> x * x;"

"sqr 4;" (* == *) "16" @@ -120,10 +120,10 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Nested Lambda"

- "sqr : Int -> Int; + "sqr : Integer -> Integer; sqr = lambda x -> x * x;

- cube : Int -> Int; + cube : Integer -> Integer; cube = lambda x -> x * (sqr x);"

"cube 4" (* == *) "64" @@ -148,7 +148,7 @@ let _ = test_eval_eqv_named b = (ctr2 (ctr2 ctr0)); z = 3; c = (ctr3 (ctr2 ctr0)); w = 4;

- test_fun : idt -> Int; + test_fun : idt -> Integer; test_fun = lambda k -> case k | ctr1 l => 1 | ctr2 l => 2 @@ -166,7 +166,7 @@ let nat_decl = " zero = datacons Nat zero; succ = datacons Nat succ;

- to-num : Nat -> Int; + to-num : Nat -> Integer; to-num = lambda (x : Nat) -> case x | (succ y) => (1 + (to-num y)) | zero => 0;" @@ -210,8 +210,8 @@ let _ = test_eval_eqv_named two = succ one; three = succ two;

- even : Nat -> Int; - odd : Nat -> Int; + even : Nat -> Integer; + odd : Nat -> Integer;

odd = lambda (n : Nat) -> case n | zero => 0 @@ -229,7 +229,7 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Partial Application"

- "add : Int -> Int -> Int; + "add : Integer -> Integer -> Integer; add = lambda x y -> (x + y);

inc1 = add 1; @@ -260,12 +260,12 @@ let _ = test_eval_eqv_named list.head my_list; list.head (list.tail my_list)"

- "4; some 1; some 2" + "(Integer->Int 4); some 1; some 2"

(* * Special forms *) -let _ = test_eval_eqv "w = 2" "decltype w" "Int" +let _ = test_eval_eqv "w = 2" "decltype w" "Integer" let _ = test_eval_eqv "w = 2" "declexpr w" "2"

let _ = (add_test "EVAL" "Monads" (fun () -> @@ -288,9 +288,9 @@ let _ = (add_test "EVAL" "Monads" (fun () -> let _ = test_eval_eqv_named "Argument Reordering"

- "fun = lambda (x : Int) => - lambda (y : Int) -> - lambda (z : Int) -> x * y + z;" + "fun = lambda (x : Integer) => + lambda (y : Integer) -> + lambda (z : Integer) -> x * y + z;"

"fun (x := 3) 2 1; fun (x := 3) (z := 1) 4; @@ -312,7 +312,7 @@ let _ = test_eval_eqv_named "Metavars" let _ = test_eval_eqv_named "Explicit field patterns" "Triplet = typecons Triplet - (triplet (a ::: Int) (b :: Float) (c : String) (d :: Int)); + (triplet (a ::: Integer) (b :: Float) (c : String) (d :: Integer)); triplet = datacons Triplet triplet; t = triplet (b := 5.0) (a := 3) (d := 7) (c := "hello");"

@@ -330,7 +330,7 @@ let _ = test_eval_eqv_named "Implicit Arguments"

{| - fun = lambda (x : Int) => + fun = lambda (x : Integer) => lambda (p : Eq x x) -> x; |} @@ -344,7 +344,7 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Equalities"

- "f : (α : Type) ≡> (p : Eq Int α) -> Int -> α; + "f : (α : Type) ≡> (p : Eq Integer α) -> Integer -> α; f = lambda α ≡> lambda p x -> Eq_cast (f := lambda v -> v) (p := p) x"

@@ -364,7 +364,7 @@ let _ = test_eval_eqv_named

Pair = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b));

- ptest : Pair Int String; + ptest : Pair Integer String; ptest = (##datacons Pair cons) (x := 4) (y := "hello");

px = case ptest | (##datacons ? cons) (x := v) => v; @@ -445,4 +445,36 @@ nil≠l = |} "head l nil≠l" "0"

+let _ = + add_test "EVAL" "int overflows" (fun () -> + let check_op op biop a b = + let a' = Z.of_int a in + let b' = Z.of_int b in + let expect' = biop a' b' in + let str = "(Int_" ^ op ^ " (Integer->Int " ^ (string_of_int a) ^ ")" + ^ " (Integer->Int " ^ (string_of_int b) ^ "))" in + let lxp = List.hd (Elab.lexp_expr_str str ectx) in + let elxp = OL.erase_type lxp in + assert (Log.error_count () == 0); + + if Z.fits_int expect' then + let actual = eval elxp rctx in + expect_equal_values [actual] [Vint (Z.to_int expect')] + else + (* The result should overflow *) + try let result = (eval elxp rctx) in + ut_string2 ("EXPECTED overflow for `" ^ str ^ "`\n"); + ut_string2 ("GOT: " ^ (value_string result) ^ "\n"); + failure + with + | Log.Internal_error _ -> Log.clear_log (); success in + let arith_ops = [("+", Z.add); ("-", Z.sub); ("*", Z.mul); ("/", Z.div)] in + let vals = [min_int; -1; 0; 1; max_int] in + let sum_for ls fn = List.fold_left (+) 0 (List.map fn ls) in + sum_for arith_ops (fun (op, biop) -> + sum_for vals (fun a -> + sum_for vals (fun b -> + if op = "/" && b = 0 then success else + check_op op biop a b)))) + let _ = run_all ()

===================================== tests/macro_test.ml ===================================== @@ -57,10 +57,10 @@ let _ = (add_test "MACROS" "macros base" (fun () ->

let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in

- let ecode = "(lambda (x : Int) -> sqr 3) 5;" in + let ecode = "(lambda (x : Integer) -> sqr 3) 5;" in

let ret = Elab.eval_expr_str ecode ectx rctx in - expect_equal_values ret [Vint(3 * 3)])) + expect_equal_values ret [Vinteger (Z.of_int (3 * 3))]))

let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " @@ -68,9 +68,9 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> let chain-decl : Sexp -> Sexp -> Sexp; chain-decl a b = Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil)) in

- let make-decl : String -> Int -> Sexp; + let make-decl : String -> Integer -> Sexp; make-decl name val = - (Sexp_node (Sexp_symbol "_=_") (cons (Sexp_symbol name) (cons (Sexp_integer (Int->Integer val)) nil))) in + (Sexp_node (Sexp_symbol "_=_") (cons (Sexp_symbol name) (cons (Sexp_integer val) nil))) in

let d1 = make-decl "a" 1 in let d2 = make-decl "b" 2 in @@ -85,7 +85,7 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> let ecode = "a; b;" in

let ret = Elab.eval_expr_str ecode ectx rctx in - expect_equal_values ret [Vint(1); Vint(2)])) + expect_equal_values ret [Vinteger(Z.of_int 1); Vinteger(Z.of_int 2)]))

(* run all tests *) let _ = run_all ()

===================================== tests/unify_test.ml ===================================== @@ -82,14 +82,14 @@ let str_int_4 = "i = 4" let str_case = "i = case true | true => 2 | false => 42" -let str_case2 = "i = case nil(a := Int) +let str_case2 = "i = case nil(a := Integer) | nil => 12 | _ => 24" let str_let = "i = let a = 5 in a + 1" let str_let2 = "j = let b = 5 in b" -let str_lambda = "sqr = lambda (x : Int) -> x * x;" -let str_lambda2 = "sqr = lambda (x : Int) -> x * x;" -let str_lambda3 = "sqr = lambda (x : Int) -> lambda (y : Int) -> x * y;" +let str_lambda = "sqr = lambda (x : Integer) -> x * x;" +let str_lambda2 = "sqr = lambda (x : Integer) -> x * x;" +let str_lambda3 = "sqr = lambda (x : Integer) -> lambda (y : Integer) -> x * y;" let str_type = "i = let j = decltype(Type) in decltype(j);" let str_type2 = "j = let i = Int -> Int in decltype(i);"

@@ -128,11 +128,11 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = ( mkLambda ((Anormal), (Util.dummy_location, Some "L1"), mkVar((Util.dummy_location, Some "z"), 3), - mkImm (Integer (Util.dummy_location, 3))), + mkImm (Integer (Util.dummy_location, Z.of_int 3))), mkLambda ((Anormal), (Util.dummy_location, Some "L2"), mkVar((Util.dummy_location, Some "z"), 4), - mkImm (Integer (Util.dummy_location, 3))), Nothing ) + mkImm (Integer (Util.dummy_location, Z.of_int 3))), Nothing )

::(input_induct , input_induct , Equivalent) (* 2 *) ::(input_int_4 , input_int_4 , Equivalent) (* 3 *)

===================================== 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/c21079e759d495ac1ae331ab0e58dadb7...