Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer

Commits: d3a9e581 by Jean-Alexandre Barszcz at 2020-09-25T22:26:59-04:00 * src/eval.ml: Add overflow checking to the Int builtin operators

* tests/eval_test.ml: Test that overflows cause runtime errors

- - - - - 7e07d97d by Jean-Alexandre Barszcz at 2020-09-25T22:33:21-04:00 * src/sexp.ml (sexp): Use Zarith's big integers in sexps.

* btl/builtins.typer: Add the builtin `Integer->Int`. * src/eval.ml: Implement it. (sexp_dispatch): Fix the value passed to the integer handler.

- - - - - 043275cd by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 * btl/pervasive.typer (quote1): Fix quoting for literals

- - - - - 8a7b7910 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 Add a macro for dependent elimination

* btl/depelim.typer: New file, implements the macro. * btl/pervasive.typer: Load the new macro. * tests/elab_test.ml: Test it.

- - - - - c722732e by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 * src/unification.ml: Clarify the order of the handlers

Try and impose some logic on the order in which the various unification cases are handled.

(unify'): Shuffle. (unify_*): Simplify accordingly. (unify_call): Handle calls of different length.

* tests/unify_test.ml: Rewrite and enable the tests.

- - - - - ad090c1f by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 * src/elab.ml (sform_lambda): Use unify instead of conv_p.

(unify_or_error): New function, extracted from check_inferred. (check_inferred): Use it.

- - - - -

13 changed files:

- btl/builtins.typer - + btl/depelim.typer - btl/pervasive.typer - src/debug.ml - src/elab.ml - src/eval.ml - src/lexer.ml - src/lexp.ml - src/sexp.ml - src/unification.ml - tests/elab_test.ml - tests/eval_test.ml - tests/unify_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -133,7 +133,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;

===================================== btl/depelim.typer ===================================== @@ -0,0 +1,110 @@ +%%% 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/pervasive.typer ===================================== @@ -203,21 +203,31 @@ 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" + (make_app "##Int->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))); @@ -634,6 +644,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

===================================== 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) @@ -694,6 +694,22 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = | _ -> OL.get_type (ectx_to_lctx ctx) e in check_inferred ctx e inferred_t t

+and unify_or_error lctx lxp ?lxp_name expect actual = + match Unif.unify expect actual lctx with + | ((ck, _ctx, t1, t2)::_) + -> lexp_error (lexp_location lxp) lxp + ("Type mismatch" + ^ (match ck with | Unif.CKimpossible -> "" + | Unif.CKresidual -> " (residue)") + ^ "! Context expected:\n " ^ lexp_string expect ^ "\nbut " + ^ (U.option_default "expression" lxp_name) ^ " has type:\n " + ^ lexp_string actual ^ "\ncan't unify:\n " + ^ lexp_string t1 + ^ "\nwith:\n " + ^ lexp_string t2); + assert (not (OL.conv_p lctx expect actual)) + | [] -> () + (* This is a crucial function: take an expression `e` of type `inferred_t` * and convert it into something of type `t`. Currently the only conversion * we use is to instantiate implicit arguments when needed, but we could/should @@ -704,20 +720,7 @@ and check_inferred ctx e inferred_t t = | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in - (match Unif.unify inferred_t t (ectx_to_lctx ctx) with - | ((ck, _ctx, t1, t2)::_) - -> lexp_error (lexp_location e) e - ("Type mismatch(" - ^ (match ck with | Unif.CKimpossible -> "impossible" - | Unif.CKresidual -> "residue") - ^ ")! Context expected:\n " - ^ lexp_string t ^ "\nbut expression has type:\n " - ^ lexp_string inferred_t ^ "\ncan't unify:\n " - ^ lexp_string t1 - ^ "\nwith:\n " - ^ lexp_string t2); - assert (not (OL.conv_p (ectx_to_lctx ctx) inferred_t t)) - | [] -> ()); + unify_or_error (ectx_to_lctx ctx) e t inferred_t; e

(* Lexp.case can sometimes be inferred, but we prefer to always check. *) @@ -1711,10 +1714,8 @@ let rec sform_lambda kind ctx loc sargs ot = -> (match olt1 with | None -> () | Some lt1' - -> if not (OL.conv_p (ectx_to_lctx ctx) lt1 lt1') - then lexp_error (lexp_location lt1') lt1' - ("Type mismatch! Context expected `" - ^ lexp_string lt1 ^ "`")); + -> unify_or_error (ectx_to_lctx ctx) lt1' + ~lxp_name:"parameter" lt1 lt1'); mklam lt1 (Some lt2)

| Arrow (ak2, v, lt1, _, lt2) when kind = Anormal @@ -1803,7 +1804,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_shift_check 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_shift_check 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_shift_check 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_shift_check; + add_binary_iop_with_loc "lsr" lsr_with_shift_check; + add_binary_iop_with_loc "asr" asr_with_shift_check;

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)) -> Vint (Z.to_int 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. *)

===================================== 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/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/unification.ml ===================================== @@ -171,10 +171,27 @@ let rec s_offset s = match s with

(** Dispatch to the right unifier.

- If (<code>unify_X X Y</code>) don't handle the case <b>(X, Y)</b>, it call (<code>unify Y X</code>) - - The metavar unifier is the end rule, it can't call unify with its parameter (changing their order) -*) + Unification has the side-effect of associating the metavariables + in a way that makes the Lexp arguments convertible, if possible. In + case of success, it returns the empty list. Otherwise, it returns + the cause of failure as a list of constraints of the following + kinds: + + 1. `CKimpossible` constraints: constraints that cannot be + satisfied, even if other metavars are associated, redexes are + reduced, and subtitutions are done. For example, an arrow could + never be unified with a lambda. + + 2. `CKresidual` constraints: pairs of subterms that cannot be + unified in the current context, but might eventually be sucessfully + unifiable. For instance, a pair of different variables cannot be + unified, unless another reduction eventually substitutes one for + the other. As another example, a metavariable could be used in the + head position of a call, blocking its reduction, but a later + instanciation might turn this metavariable into a lambda, thus + yielding a redex, possibly reducing the call to a term unifiable + with the other argument. + *) let rec unify (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) : return_type = @@ -191,28 +208,45 @@ and unify' (e1: lexp) (e2: lexp) if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in match (lexp_lexp' e1', lexp_lexp' e2') with - | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) - | (Var _, Var _)) + (* Both expressions are in WHNF: we don't have `Let`s nor `Susp`s. *) + + (* First, we handle the simple cases with no substructure. *) + | ((Imm _ | Builtin _), (Imm _ | Builtin _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] + + (* Then, we handle metavariables (aka. flexible-flexible and + Flexible-Rigid Equations). Reminder: WHNF implies that the + metavariables are not already instanciated. *) | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' - | (_, Call _) -> unify_call e2' e1' ctx vs' - (* | (l, (Case _ as r)) -> unify_case r l subst *) - | (Arrow _ , _) -> unify_arrow e1' e2' ctx vs' - | (Lambda _, _) -> unify_lambda e1' e2' ctx vs' - | (Call _, _) -> unify_call e1' e2' ctx vs' - (* | (Case _ as l, r) -> unify_case l r subst *) - (* | (Inductive _ as l, r) -> unify_induct l r subst *) - | (Sort _, _) -> unify_sort e1' e2' ctx vs' - | (SortLevel _, _) -> unify_sortlvl e1' e2' ctx vs' - | (Inductive (_loc1, label1, args1, consts1), - Inductive (_loc2, label2, args2, consts2)) - -> (* print_string ("Unifying inductives " - * ^ snd label1 - * ^ " and " - * ^ snd label2 - * ^ "\n"); *) - unify_inductive ctx vs' args1 args2 consts1 consts2 e1 e2 + + (* Otherwise, the equation is rigid-rigid. Let's start with the + cases that can leave residuals: 1. Variables, since they could + be substituted with further reduction; 2. Calls, because they + might become redexes; 3. Case expressions, for the same + reason. *) + | (_, Var _) -> unify_var e2' e1' ctx vs' + | (Var _, _) -> unify_var e1' e2' ctx vs' + | (_, Call _) -> unify_call e2' e1' ctx vs' + | (Call _, _) -> unify_call e1' e2' ctx vs' + (* FIXME: Handle `Case` expressions. *) + + (* We are left with the cases that are not affected by + substitutions, thus should not immediately lead to residual + constraints. *) + | (_, Arrow _) -> unify_arrow e2' e1' ctx vs' + | (Arrow _, _) -> unify_arrow e1' e2' ctx vs' + | (_, Lambda _) -> unify_lambda e2' e1' ctx vs' + | (Lambda _, _) -> unify_lambda e1' e2' ctx vs' + | (_, Sort _) -> unify_sort e2' e1' ctx vs' + | (Sort _, _) -> unify_sort e1' e2' ctx vs' + | (_, SortLevel _) -> unify_sortlvl e2' e1' ctx vs' + | (SortLevel _, _) -> unify_sortlvl e1' e2' ctx vs' + | (_, Inductive _) -> unify_inductive e2' e1' ctx vs' + | (Inductive _, _) -> unify_inductive e1' e2' ctx vs' + | (_, Cons _) -> unify_cons e2' e1' ctx vs' + | (Cons _, _) -> unify_cons e1' e2' ctx vs' + | _ -> (if OL.conv_p ctx e1' e2' then [] else ((* print_string "Unification failure on default\n"; *) [(CKresidual, ctx, e1, e2)])) @@ -223,7 +257,6 @@ and unify' (e1: lexp) (e2: lexp) - (Arrow, Arrow) -> if var_kind = var_kind then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) else None - - (Arrow, Var) -> Constraint - (_, _) -> None *) and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs @@ -236,19 +269,13 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs @(unify' lexp1 (srename v1 lexp2) (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) - else [(CKimpossible, ctx, arrow, lxp)] - | (Arrow _, Imm _) -> [(CKimpossible, ctx, arrow, lxp)] - | (Arrow _, Var _) -> ([(CKresidual, ctx, arrow, lxp)]) - | (Arrow _, _) -> unify' lxp arrow ctx vs + else [(CKimpossible, ctx, arrow, lxp)] | (_, _) -> [(CKimpossible, ctx, arrow, lxp)]

(** Unify a Lambda and a lexp if possible - - Lamda , Lambda -> if var_kind = var_kind + - Lambda , Lambda -> if var_kind = var_kind then UNIFY ltype & lxp else ERROR - - Lambda , Var -> CONSTRAINT - - Lambda , Call -> Constraint - - Lambda , Let -> Constraint - - Lambda , lexp -> unify lexp lambda subst + - Lambda , _ -> Impossible *) and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' lambda, lexp_lexp' lxp) with @@ -260,19 +287,12 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) else [(CKimpossible, ctx, lambda, lxp)] - | ((Lambda _, Var _) - | (Lambda _, Let _) - | (Lambda _, Call _)) -> [(CKresidual, ctx, lambda, lxp)] - | (Lambda _, Arrow _) - | (Lambda _, Imm _) -> [(CKimpossible, ctx, lambda, lxp)] - | (Lambda _, _) -> unify' lxp lambda ctx vs - | (_, _) -> [(CKimpossible, ctx, lambda, lxp)] + | (_, _) -> [(CKimpossible, ctx, lambda, lxp)]

(** Unify a Metavar and a lexp if possible - - lexp , {metavar <-> none} -> UNIFY - - lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] - - metavar , metavar -> if Metavar = Metavar then OK else ERROR - - metavar , lexp -> OK + - metavar , metavar -> if Metavar = Metavar then intersect + - metavar , metavar -> inverse subst (try both sides) + - metavar , lexp -> inverse subst *) and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = @@ -384,6 +404,16 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | _ -> unif idx2 s2 lxp1) | _ -> unif idx s1 lxp2

+(** Unify a Var (var) and a lexp (lxp) + - Var , Var -> IF same var THEN ok ELSE constraint + - Var , lexp -> Constraint +*) +and unify_var (var: lexp) (lxp: lexp) ctx vs + : return_type = + match (lexp_lexp' var, lexp_lexp' lxp) with + | (Var _, Var _) when OL.conv_p ctx var lxp -> [] + | (_, _) -> [(CKresidual, ctx, var, lxp)] + (** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT @@ -393,13 +423,15 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs match (lexp_lexp' call, lexp_lexp' lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) when OL.conv_p ctx lxp_left lxp_right - -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) + -> (try List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then (unify' e1 e2 ctx vs)@op else [(CKimpossible, ctx, call, lxp)]) [] (List.combine lxp_list1 lxp_list2) - | (_, _) -> [(CKresidual, ctx, call, lxp)] + with Invalid_argument _ (* Lists of diff. length in combine. *) + -> [(CKresidual, ctx, call, lxp)]) + | (_, _) -> [(CKresidual, ctx, call, lxp)]

(** Unify a Case with a lexp - Case, Case -> try to unify @@ -468,11 +500,10 @@ and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = * more "canonicalized" otherwise it's too restrictive! *) (unify' l11 l21 ctx vs)@(unify' l12 l22 ctx vs) | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) - | _, _ -> [(CKresidual, ctx, sortlvl, lxp)] + | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]

(** Unify a Sort and a lexp - Sort, Sort -> if Sort ~= Sort then OK else ERROR - - Sort, Var -> Constraint - Sort, lexp -> ERROR *) and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = @@ -482,8 +513,7 @@ and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = | StypeOmega, StypeOmega -> [] | StypeLevel, StypeLevel -> [] | _, _ -> [(CKimpossible, ctx, sort_, lxp)]) - | Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)] - | _, _ -> [(CKimpossible, ctx, sort_, lxp)] + | _, _ -> [(CKimpossible, ctx, sort_, lxp)]

(************************ Helper function ************************************)

@@ -533,7 +563,14 @@ and is_same arglist arglist2 = * | None -> test e subst) * ) None lst *)

-and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = +and unify_inductive lxp1 lxp2 ctx vs = + match lexp_lexp' lxp1, lexp_lexp' lxp2 with + | (Inductive (_loc1, label1, args1, consts1), + Inductive (_loc2, label2, args2, consts2)) + -> unify_inductive' ctx vs args1 args2 consts1 consts2 lxp1 lxp2 + | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)] + +and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = let unif_formals ctx vs args1 args2 = if not (List.length args1 == List.length args2) then (ctx, vs, [(CKimpossible, ctx, e1, e2)]) @@ -578,3 +615,8 @@ and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = * | _, _ -> None * in test l1 l2 subst *)

+and unify_cons lxp1 lxp2 ctx vs = + match lexp_lexp' lxp1, lexp_lexp' lxp2 with + | (Cons (it1, (_, l1)), Cons (it2, (_, l2))) when l1 = l2 + -> unify' it1 it2 ctx vs + | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)]

===================================== tests/elab_test.ml ===================================== @@ -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 ===================================== @@ -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 ^ " " ^ (string_of_int a) + ^ " " ^ (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/unify_test.ml ===================================== @@ -21,21 +21,18 @@ * * -------------------------------------------------------------------------- *)

-open Sexp -open Pexp + open Lexp open Unification

-open Utest_lib - open Fmt +open Utest_lib

-open Builtin -open Env - -open Str +module U = Util

-open Debug +(* default environment *) +let ectx = Elab.default_ectx +let rctx = Elab.default_rctx

type result = | Constraint @@ -43,10 +40,6 @@ type result = | Equivalent | Nothing

-type unif_res = (result * (constraints) * lexp * lexp) - -type triplet = string * string * string - let string_of_result r = match r with | Constraint -> "Constraint" @@ -54,179 +47,97 @@ let string_of_result r = | Equivalent -> "Equivalent" | Nothing -> "Nothing"

-let max_dim (lst: (string * string * string * string) list): (int * int * int *int) = - let max i l = max i (String.length l) - in List.fold_left - (fun (la, ca1, ca2, ra) (l, c1, c2, r) -> ((max la l), (max ca1 c1), (max ca2 c2), (max ra r))) - (0, 0, 0, 0) - lst - -let fmt (lst: (lexp * lexp * result * result) list): string list = - let str_lst = List.map - (fun (l1, l2, r1, r2) -> ((lexp_string l1), (lexp_string l2), (string_of_result r1), (string_of_result r2))) - lst - in let l, c1, c2, r = max_dim str_lst - in List.map (fun (l1, l2, r1, r2) -> (U.padding_right l1 l ' ') - ^ ", " - ^ (U.padding_right l2 c1 ' ') - ^ " -> got: " - ^ (U.padding_right r2 r ' ') - ^ " expected: " - ^ (U.padding_right r1 c2 ' ') - ) str_lst - -(* Inputs for the test *) -let str_induct = "Nat : Type; Nat = typecons (dNat) (zero) (succ Nat)" -let str_int_3 = "i = 3" -let str_int_4 = "i = 4" -let str_case = "i = case true -| true => 2 -| false => 42" -let str_case2 = "i = case nil(a := Int) -| 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_type = "i = let j = decltype(Type) in decltype(j);" -let str_type2 = "j = let i = Int -> Int in decltype(i);" - -let generate_ltype_from_str str = - List.hd ((fun (lst, _) -> - (List.map - (fun (_, _, ltype) -> ltype)) - (List.flatten lst)) - (Elab.lexp_decl_str str Elab.default_ectx)) - -let generate_lexp_from_str str = - List.hd ((fun (lst, _) -> - (List.map - (fun (_, lxp, _) -> lxp)) - (List.flatten lst)) - (Elab.lexp_decl_str str Elab.default_ectx)) - -let input_induct = generate_lexp_from_str str_induct -let input_int_4 = generate_lexp_from_str str_int_4 -let input_int_3 = generate_lexp_from_str str_int_3 -let input_case = generate_lexp_from_str str_case -let input_case2 = generate_lexp_from_str str_case2 -let input_let = generate_lexp_from_str str_let -let input_let2 = generate_lexp_from_str str_let -let input_lambda = generate_lexp_from_str str_lambda -let input_lambda2 = generate_lexp_from_str str_lambda2 -let input_lambda3 = generate_lexp_from_str str_lambda3 -let input_arrow = generate_ltype_from_str str_lambda -let input_arrow2 = generate_ltype_from_str str_lambda2 -let input_arrow3 = generate_ltype_from_str str_lambda3 -let input_type = generate_ltype_from_str str_type -let input_type_t = generate_ltype_from_str str_type2 - -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))), - mkLambda ((Anormal), - (Util.dummy_location, Some "L2"), - mkVar((Util.dummy_location, Some "z"), 4), - mkImm (Integer (Util.dummy_location, 3))), Nothing ) - - ::(input_induct , input_induct , Equivalent) (* 2 *) - ::(input_int_4 , input_int_4 , Equivalent) (* 3 *) - ::(input_int_3 , input_int_4 , Nothing) (* 4 *) - ::(input_case , input_int_4 , Constraint) (* 5 *) - ::(input_case , input_induct , Constraint) (* 6 *) - ::(input_case , input_case , Equivalent) (* 7 *) - ::(input_case , input_case2 , Nothing) (* 8 *) - - ::(input_let , input_induct , Constraint) (* 9 *) - ::(input_let , input_int_4 , Constraint) (* 10 *) - ::(input_let , input_case , Constraint) (* 11 *) - ::(input_let , input_let , Equivalent) (* 12 *) - ::(input_let2 , input_let , Equivalent) (* 13 *) - ::(input_let2 , input_let2 , Equivalent) (* 14 *) - - ::(input_lambda , input_int_4 , Nothing) (* 15 *) - ::(input_lambda , input_induct , Nothing) (* 16 *) - ::(input_lambda , input_case , Constraint) (* 17 *) - ::(input_lambda , input_case2 , Constraint) (* 18 *) - ::(input_lambda , input_let , Constraint) (* 19 *) - ::(input_lambda , input_induct , Nothing) (* 20 *) - ::(input_lambda , input_lambda , Equivalent) (* 21 *) - - ::(input_lambda2 , input_int_4 , Nothing) (* 22 *) - ::(input_lambda2 , input_induct , Nothing) (* 23 *) - ::(input_lambda2 , input_case , Constraint) (* 24 *) - ::(input_lambda2 , input_case2 , Constraint) (* 25 *) - ::(input_lambda2 , input_let , Constraint) (* 26 *) - ::(input_lambda2 , input_induct , Nothing) (* 27 *) - ::(input_lambda2 , input_lambda , Equivalent) (* 28 *) - ::(input_lambda2 , input_lambda2 , Equivalent) (* 29 *) - ::(input_lambda2 , input_lambda3 , Constraint) (* 30 *) - ::(input_lambda3 , input_lambda3 , Equivalent) (* 31 *) - - ::(input_arrow2 , input_int_4 , Unification) (* 32 *) - ::(input_arrow2 , input_induct , Unification) (* 33 *) - ::(input_arrow2 , input_case , Constraint) (* 34 *) - ::(input_arrow2 , input_case2 , Constraint) (* 35 *) - ::(input_arrow2 , input_let , Constraint) (* 36 *) - ::(input_arrow2 , input_induct , Unification) (* 37 *) - ::(input_arrow2 , input_lambda , Unification) (* 38 *) - ::(input_arrow2 , input_lambda2 , Unification) (* 39 *) - ::(input_arrow2 , input_arrow3 , Unification) (* 40 *) - ::(input_arrow3 , input_arrow , Unification) (* 41 *) - ::(input_arrow2 , input_arrow , Unification) (* 42 *) - ::(input_arrow3 , input_arrow3 , Equivalent) (* 43 *) - - ::(input_type , input_type_t , Equivalent) (* 44 *) - - ::(mkMetavar (0, S.identity, (Util.dummy_location, Some "M")), - mkVar ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *) - - ::[] - -let test_input (lxp1: lexp) (lxp2: lexp): unif_res = +let unif_output (lxp1: lexp) (lxp2: lexp) ctx = let orig_subst = !metavar_table in - let res = unify lxp1 lxp2 Myers.nil in - match res with + let constraints = unify lxp1 lxp2 ctx in + match constraints with | [] -> let new_subst = !metavar_table in if orig_subst == new_subst - then (Equivalent, res, lxp1, lxp2) - else (Unification, res, lxp1, lxp2) - | (CKresidual, _, _, _)::_ -> (Constraint, res, lxp1, lxp2) - | (CKimpossible, _, _, _)::_ -> (Nothing, res, lxp1, lxp2) - -let check (lxp1: lexp) (lxp2: lexp) (res: result): bool = - let r, _, _, _ = test_input lxp1 lxp2 - in if r = res then true else false - -let test_if (input: lexp list) sample_generator checker : bool = - let rec test_if_ samples checker = - match samples with - | (l1, l2, res)::t -> if checker l1 l2 res then test_if_ t checker else false - | [] -> true - in test_if_ (sample_generator input) checker - -let unifications = List.map - (fun (l1, l2, res) -> - let r, _, _, _ = test_input l1 l2 - in (l1, l2, res, r)) - (* FIXME: Skip failure for now. *) - [] (* (generate_testable []) *) - -let idx = ref 0 -let _ = List.map - (fun (str, (l1, l2, expected, res)) -> - idx := !idx + 1; - add_test "UNIFICATION" - ((if !idx < 10 then "0" else "") ^ (string_of_int !idx) ^ " " ^ str ) - (fun () -> if expected = res then success else failure)) - (List.combine (fmt unifications) unifications ) + then (Equivalent, constraints) + else (Unification, constraints) + | (CKresidual, _, _, _)::_ -> (Constraint, constraints) + | (CKimpossible, _, _, _)::_ -> (Nothing, constraints) + +let add_unif_test name ?(ectx=ectx) lxp_a lxp_b expected = + add_test "UNIFICATION" name (fun () -> + let (r, cstrts) = unif_output lxp_a lxp_b (DB.ectx_to_lctx ectx) in + + if r = expected then + success + else ( + ut_string2 (red ^ "EXPECTED: " ^ reset ^ (string_of_result expected) ^ "\n"); + ut_string2 (red ^ "GOT: " ^ reset ^ (string_of_result r ) ^ "\n"); + ut_string2 ("During the unification of:\n\t" ^ (lexp_string lxp_a) + ^ "\nand\n\t" ^ (lexp_string lxp_b) ^ "\n"); + failure + )) + +let add_unif_test_s name ?(setup="") ?(ectx=ectx) input_a input_b expected = + let _, ectx = Elab.lexp_decl_str setup ectx in + + let lxp_a = List.hd (Elab.lexp_expr_str input_a ectx) in + let lxp_b = List.hd (Elab.lexp_expr_str input_b ectx) in + + add_unif_test name ~ectx lxp_a lxp_b expected + +let _ = + (* Let's have some variables in context to block the reduction of + elimination forms. The variables are manually added to the + context (and not given a value) to make sure that they cannot be + reduced. *) + let _, ectx = Elab.lexp_decl_str + {| type Nat + | Z + | S (Nat); |} ectx in + let dloc = U.dummy_location in + let nat = mkVar ((dloc, Some "Nat"), 2) in + let shift l i = mkSusp l (S.shift i) in + let ectx, _ = + List.fold_left + (fun (ectx, i) (name, lexp) -> + Elab.ctx_extend ectx (dloc, Some name) Variable (shift lexp i), i + 1) + (ectx, 0) + [("f", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); + ("g", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); + ("h", (mkArrow (Anormal, (dloc, Some "x"), nat, dloc, + mkArrow (Anormal, (dloc, Some "y"), shift nat 1, + dloc, shift nat 2)))); + ("a", nat); + ("b", nat)] in + + add_unif_test_s "same integer" "4" "4" Equivalent; + add_unif_test_s "diff. integers" "3" "4" Nothing; + add_unif_test_s "int and builtin" "3" "##Int" Nothing; + add_unif_test_s "same var" ~ectx "a" "a" Equivalent; + add_unif_test_s "diff. var" ~ectx "a" "b" Constraint; + add_unif_test_s "var and integer" ~ectx "a" "1" Constraint; + add_unif_test_s "same call" ~ectx "f a" "f a" Equivalent; + add_unif_test_s "calls with inconvertible heads" ~ectx "f a" "g a" Constraint; + add_unif_test_s "calls with diff. num. of args" ~ectx "h a" "h a b" Constraint; + add_unif_test_s "calls with residue in args" ~ectx "f a" "f b" Constraint; + add_unif_test_s "same case" ~ectx + "case a | Z => false | S n => true" + "case a | Z => false | S n => true" + Equivalent; + add_unif_test_s "diff. case" ~ectx + "case a | Z => false | S n => true" + "case a | Z => true | S n => false" + (* 'Nothing' would be a more accurate result here. This would + require implementing unification for case exprs. *) + Constraint; + + add_unif_test_s "datacons/inductive" ~ectx + "Z" + "(datacons (typecons Nat Z (S Nat)) Z)" + (* Not recursive! Refers to the previous def of Nat. *) + Equivalent; + + (* Metavariables *) + add_unif_test_s "same metavar" "?m" "?m" Equivalent; + add_unif_test_s "diff. metavar" "?m1" "?m2" Unification; + add_unif_test_s "metavar and int" "?m" "5" Unification; + + ()

let _ = run_all () - -

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