Jean-Alexandre Barszcz pushed to branch ja-barszcz 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.

- - - - - baaf1bb3 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 [WIP] experiments with Decidable and proofs

- - - - - ed9be0b5 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 [WIP] First draft of an instance search algorithm

- - - - - 16dca693 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 [WIP] Add a syntax for records

- - - - - 0475cc31 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 [WIP] Extend the Decidable sample with conjunction (dep on records)

- - - - - 8500a992 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 Resolve instances in the REPL (since exprs. are not generalized)

- - - - - 6fbb8054 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 Resolve instances for recursive definitions

- - - - - 35e4183d by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 [WIP] Do the set_getenv

IIRC these were missing to correctly handle the elab context for macro expansion and Elab_... primitives. Perhaps it would be simpler to call set_getenv once before macro expansion rather than everywhere where the context can change. Needs some experimentation and tests.

- - - - - 7c8cfdb0 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 Num class example

- - - - - 0bc46119 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 Num class (with records)

- - - - - e29cd513 by Jean-Alexandre Barszcz at 2020-09-25T23:18:39-04:00 Algebra classes sample with proofs for the additive monoid for Nats

- - - - -

24 changed files:

- btl/builtins.typer - + btl/depelim.typer - btl/pervasive.typer - + btl/records.typer - + samples/alg_classes.typer - + samples/decidable.typer - + samples/num_class.typer - + samples/num_class_recs.typer - src/REPL.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/eval.ml - + src/instances.ml - src/lexer.ml - src/lexp.ml - src/log.ml - src/myers.ml - src/opslexp.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;

@@ -363,6 +371,12 @@ Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> Bool; Elab_isconstructor = Built-in "Elab.isconstructor" : String -> Elab_Context -> Bool;

+%% +%% Check if a symbol is an inductive in a particular context +%% +Elab_isinductive = Built-in "Elab.isinductive" + : String -> Elab_Context -> Bool; + %% %% Check if the n'th field of a constructor is erasable %% If the constructor isn't defined it will always return false @@ -389,6 +403,20 @@ Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> Strin %% Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int;

+%% +%% Get the position of a field in a constructor +%% It return -1 in case the field isn't defined +%% see pervasive.typer for a more convenient function +%% +Elab_ind-ctor-arg-pos' = Built-in "Elab.ind-ctor-arg-pos" : String -> String -> String -> Elab_Context -> Int; + +%% +%% Get the number of fields in a constructor +%% It return -1 in case the field isn't defined +%% see pervasive.typer for a more convenient function +%% +Elab_count-ctor-args' = Built-in "Elab.count-ctor-args" : String -> String -> Elab_Context -> Int; + %% %% Get the docstring associated with a symbol %%

===================================== 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))); @@ -394,7 +404,7 @@ BoolMod = (##datacons Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); pair = datacons Pair pair;

-__.__ = +dot-impl = let mksel o f = let constructor = Sexp_node (Sexp_symbol "##datacons") (cons (Sexp_symbol "?") @@ -411,14 +421,15 @@ __.__ = (cons (Sexp_node (Sexp_symbol "_|_") (cons o (cons branch nil))) nil) - in macro (lambda args - -> IO_return - case args - | cons o tail - => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error); + in (lambda args -> + IO_return case args + | cons o tail + => (case tail + | cons f _ => mksel o f + | nil => Sexp_error) + | nil => Sexp_error); + +__.__ = macro dot-impl;

%% Triplet (tuple with 3 values) type Triplet (a : Type) (b : Type) (c : Type) @@ -547,6 +558,32 @@ in case (Int_eq r (-1)) | true => (none) | false => (some r);

+%% +%% If `Elab_ind-ctor-arg-pos'` returns (-1) it means: +%% A- The constructor isn't defined, or +%% B- The constructor has no argument named like this +%% +%% So in those case this function returns `none` +%% +Elab_ind-ctor-arg-pos a b c d = let + r = Elab_ind-ctor-arg-pos' a b c d; +in case (Int_eq r -1) + | true => (none) + | false => (some r); + +%% +%% If `Elab_count-ctor-args'` returns (-1) it means: +%% A- The constructor isn't defined, or +%% B- The constructor has no argument named like this +%% +%% So in those case this function returns `none` +%% +Elab_count-ctor-args a b c = let + r = Elab_count-ctor-args' a b c; +in case (Int_eq r -1) + | true => (none) + | false => (some r); + %%%% %%%% Common library %%%% @@ -634,6 +671,26 @@ 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_; + +%% +%% records : a simple datatype when there is only one case +%% +define-operator "#" 200 (); +records = load "btl/records.typer"; +record = records.record; +__.__ = records.__.__; +_# = records._#; + %%%% Unit tests function for doing file

%% It's hard to do a primitive which execute test file

===================================== btl/records.typer ===================================== @@ -0,0 +1,80 @@ +record-impl : List Sexp -> IO Sexp; +record-impl args = + let + %% Get a name (symbol) from a sexp + %% - (name t) -> name + %% - name -> name + get-name : Sexp -> Sexp; + get-name sxp = + case Sexp_wrap sxp + | node op _ => get-name op + | symbol _ => sxp + | _ => Sexp_error; + + %% head is (Sexp_node type-name (arg list)) + name-args = List_head Sexp_error args; + fields = List_tail args; + + type-name = get-name name-args; + + %% Create the inductive type definition. + inductive = Sexp_node (Sexp_symbol "typecons") + (cons name-args + (cons (Sexp_node (Sexp_symbol "rec") fields) + nil)); + + decl = make-decl type-name inductive; + + in IO_return decl; + +record = macro record-impl; + +record-get-impl : List Sexp -> IO Sexp; +record-get-impl args = + let + get tc f idx nargs ectx = + let arg_pats : Sexp -> Int -> Int -> List Sexp; + arg_pats s i n = + if (Int_eq n 0) then nil + else (if (Int_eq i 0) + then (cons s (arg_pats s (Int_- i 1) (Int_- n 1))) + else (cons (Sexp_symbol "_") (arg_pats s (Int_- i 1) (Int_- n 1)))); + + pat = (Sexp_node (quote (datacons (uquote (Sexp_symbol tc)) rec)) + (arg_pats (Sexp_symbol "v") idx nargs)); + + branch = (quote ((uquote pat) => v)); + in + (quote (lambda rec -> (##case_ (_|_ rec (uquote branch))))); + + try-rec-get : List Sexp -> Elab_Context -> Option Sexp; + try-rec-get arg ectx = + case args + | (cons tc (cons f nil)) => + (case (Sexp_wrap tc, Sexp_wrap f) + | (symbol tcstr, symbol fstr) => + (case (Elab_count-ctor-args tcstr "rec" ectx, + Elab_ind-ctor-arg-pos tcstr "rec" fstr ectx) + | (some nargs, some idx) => some (get tcstr fstr idx nargs ectx) + | _ => none) + | _ => none) + | _ => none; + in + do { + ectx <- Elab_getenv (); + case try-rec-get args ectx + | some sxp => IO_return sxp + | _ => dot-impl args; %% Fallback on default dot implementation + }; + +__.__ = macro record-get-impl; + +record-make-impl : List Sexp -> IO Sexp; +record-make-impl args = + IO_return case args + | (cons tc nil) => (quote (datacons (uquote tc) rec)) + | _ => Sexp_error; + +_# = macro record-make-impl; + +record (Pair (a : Type) (b : Type)) (fst : a) (snd : a);

===================================== samples/alg_classes.typer ===================================== @@ -0,0 +1,88 @@ +case_ = ##case_; %% To ease debugging + +type Magma (α : Type) + | mkMagma (op : α -> α -> α); + +typeclass Magma; + +magma_op = + lambda magma_inst => + case magma_inst + | mkMagma op => op; + +Associativity (op : ?α -> ?α -> ?α) = + (x : ?α) -> (y : ?α) -> (z : ?α) -> Eq (op (op x y) z) (op x (op y z)); + +type Semigroup (α : Type) + | mkSemigroup (magma : Magma α) (assoc ::: Associativity magma_op); + +typeclass Semigroup; + +semigroup_magma = + lambda semigroup_inst => + case semigroup_inst + | mkSemigroup magma => magma; + +IsLeftIdentity (id : ?α) (op : ?α -> ?α -> ?α) = + (x : ?α) -> Eq (op id x) x; + +IsRightIdentity (id : ?α) (op : ?α -> ?α -> ?α) = + (x : ?α) -> Eq (op x id) x; + +IsIdentity (id : ?α) (op : ?α -> ?α -> ?α) = + (Pair (IsLeftIdentity id op) (IsRightIdentity id op)); + +type Monoid (α : Type) + | mkMonoid (semigroup : Semigroup α) + (identity : α) + (isIdent ::: IsIdentity identity magma_op); + +typeclass Monoid; + +type Nat + | Zero + | Succ Nat; + +plus : Nat -> Nat -> Nat; +plus x y = + case x + | Zero => y + | Succ x' => Succ (plus x' y); + +natAdditiveMagma = + mkMagma plus; + +Eq_cong : % not sure about levels here + (t : (Type_ ?ℓ)) ≡> (r : (Type_ ?ℓ)) ≡> + (x : t) ≡> (y : t) ≡> (p : (Eq x y)) ≡> + (f : (t -> r)) -> (Eq (f x) (f y)); +Eq_cong f = + Eq_cast (p := p) (f := lambda xy -> Eq (f x) (f xy)) Eq_refl; + +natPlusAssoc : Associativity plus; +natPlusAssoc x y z = + let + typeclass Eq + in + case x return (Eq (plus (plus x y) z) (plus x (plus y z))) + | Zero => Eq_refl + | Succ x' => (Eq_cong (p := natPlusAssoc x' y z) Succ); + +natAdditiveSemigroup : Semigroup Nat; +natAdditiveSemigroup = + mkSemigroup natAdditiveMagma (assoc := natPlusAssoc); + +zeroIsPlusLIdent : IsLeftIdentity Zero plus; +zeroIsPlusLIdent x = Eq_refl (x := x); + +zeroIsPlusRIdent : IsRightIdentity Zero plus; +zeroIsPlusRIdent x = + let + typeclass Eq; + in case x return (Eq (plus x Zero) x) + | Zero => Eq_refl + | Succ x' => (Eq_cong (p := zeroIsPlusRIdent x') Succ); + +natAdditiveMonoid : Monoid Nat; +natAdditiveMonoid = mkMonoid natAdditiveSemigroup Zero + (isIdent := pair zeroIsPlusLIdent zeroIsPlusRIdent);

===================================== samples/decidable.typer ===================================== @@ -0,0 +1,170 @@ +False = Void; +True = Unit; + +% FIXME improved "case" fails with no branches +exfalso : False -> ?a; +exfalso f = ##case_ f; + +%type Decidable (prop : Type) +% | yes (p ::: prop) +% | no (p ::: Not prop); +Decidable = typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ)) + (true (p ::: prop)) (false (p ::: Not prop)); +yes = datacons Decidable true; +no = datacons Decidable false; + +typeclass Decidable; + +Eq_trans : + (x : ?t) => (y : ?t) => (a : ?t) -> + (ax : Eq a x) => (ay : Eq a y) => Eq x y; +Eq_trans a = + lambda (ax : Eq a x) (ay : Eq a y) => + Eq_cast (f := lambda ax -> Eq ax y) ay; + +Eq_cong : % not sure about levels here + (t : (Type_ ?ℓ)) ≡> (r : (Type_ ?ℓ)) ≡> + (x : t) ≡> (y : t) ≡> (p : (Eq x y)) ≡> + (f : (t -> r)) -> (Eq (f x) (f y)); +Eq_cong f = + Eq_cast (p := p) (f := lambda xy -> Eq (f x) (f xy)) Eq_refl; + +discriminate_nocheck = + macro (lambda args -> + case args + | cons x (cons y nil) => + do { + sd <- gensym (); + sp <- gensym (); + IO_return + (quote ((lambda (uquote sp) -> + (Eq_cast (p := (uquote sp)) + (f := (lambda (uquote sd) -> + (case uquote sd + | (uquote x) => True + | _ => False))) + ())) : Not (Eq (uquote x) (uquote y)))) + } + | _ => IO_return Sexp_error); + +discriminate = + macro (lambda args -> + case args + | cons x (cons y nil) => + (case (Sexp_wrap x, Sexp_wrap y) + | (symbol sx, symbol sy) => % FIXME get the constructor even when its a call + do { + env <- Elab_getenv (); + if (and (Elab_isconstructor sx env) + (and (Elab_isconstructor sy env) + (not (Sexp_eq x y)))) + then + Macro_expand discriminate_nocheck args + else (IO_return Sexp_error) + } + | _ => IO_return Sexp_error) + | _ => IO_return Sexp_error); + +test : (Not (Eq true false)); +test = discriminate true false; + +absurd = + lambda (p : ?prop) -> + lambda (contra : (Not ?prop)) -> + contra p; + +% We can't (usefully) have a `Decidable Bool` because it's +% impossible to have a `Not Bool`. Instead, we can decide boolean +% equality: + +decideBoolEq : (a : Bool) => (b : Bool) => Decidable (Eq a b); +decideBoolEq = + lambda (a : Bool) (b : Bool) => + case (a, b) + | (false, false) => yes (p := Eq_trans false) + | (false, true) => no (p := lambda (p : Eq a b) -> + absurd (Eq_trans (ax := Eq_trans a) b) (discriminate false true)) + | (true, false) => no (p := lambda (p : Eq a b) -> + absurd (Eq_trans (ax := Eq_trans a) b) (discriminate true false)) + | (true, true) => yes (p := Eq_trans true); + +type Nat + | zero + | succ Nat; + +type even (a : Nat) + | eZ (p ::: Eq a zero) + | eSS (p :: even ?a) (pss ::: Eq a (succ (succ ?a))); + +decideEven : (a : Nat) => Decidable (even a); +decideEven = + lambda (a : Nat) => + case a + | zero => yes (p := eZ) + | succ zero => no (p := + lambda (p : even a) -> + case p + | eZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ zero)) + | eSS => absurd (Eq_trans a) (discriminate_nocheck (succ (succ ?)) (succ zero))) + | succ (succ a') => + case (decideEven : Decidable (even a')) + | yes => yes (p := eSS) + | no => no (p := + lambda (p : even a) -> + case p + | eZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ (succ ?))) + | eSS => absurd (? : even a') (? : Not (even a'))); + +type _<_ (a : Nat) (b : Nat) + | ltZ (pa ::: Eq a zero) (pb ::: Eq b (succ ?b)) + | ltS (p :: (?a < ?b)) (pa ::: Eq a (succ ?a)) (pb ::: Eq b (succ ?b)); + +decideLT : (a : Nat) => (b : Nat) => Decidable (a < b); +decideLT = + lambda a b => + case b + | zero => no (p := + lambda (p : (a < b)) -> + case p + | ltZ => absurd (Eq_trans b) (discriminate_nocheck zero (succ ?)) + | ltS => absurd (Eq_trans b) (discriminate_nocheck zero (succ ?))) + | succ b' => + case a + | zero => yes (p := ltZ) + | succ a' => + case (decideLT : (Decidable (a' < b'))) + | yes => yes (p := ltS) + | no => no (p := + lambda (p : (a < b)) -> + case p + | ltZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ ?)) + | ltS => absurd (? : (a' < b')) (? : Not (a' < b'))); + +define-operator "∧" 111 130; + +record ((a : Type) ∧ (b : Type)) (fst : a) (snd : b); + +decideAnd : (P : Type) ≡> (Q : Type) ≡> + (Decidable P) => (Decidable Q) => (Decidable (P ∧ Q)); +decideAnd = + lambda P Q ≡> + lambda (decP : Decidable P) (decQ : Decidable Q) => + case (decP, decQ) + | (yes (p := pP), yes (p := pQ)) => yes (p := _∧_ # pP pQ) + | (no (p := nP), _) => + no (p := (lambda (proofs : P ∧ Q) -> absurd (_∧_.fst proofs) nP)) + | (_, no (p := nQ)) => + no (p := (lambda (proofs : P ∧ Q) -> absurd (_∧_.snd proofs) nQ)); + +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; + in IO_return (quote (case (instance () : (Decidable (uquote e1))) + | yes => uquote e2 + | no => uquote e3))); + +test2 : Bool; +test2 = if ((even (succ zero)) ∧ (zero < zero)) then false else true; +

===================================== samples/num_class.typer ===================================== @@ -0,0 +1,39 @@ +type Num (α : Type) + | mkNum (Num_+ : α -> α -> α) + (Num_- : α -> α -> α) + (Num_* : α -> α -> α) + (Num_/ : α -> α -> α); + +typeclass Num; + +_+_ = lambda numInst => case numInst | mkNum _+_ _ _ _ => _+_; +_-_ = lambda numInst => case numInst | mkNum _ _-_ _ _ => _-_; +_*_ = lambda numInst => case numInst | mkNum _ _ _*_ _ => _*_; +_/_ = lambda numInst => case numInst | mkNum _ _ _ _/_ => _/_; + +IntNum : Num Int; +IntNum = + mkNum (Num_+ := Int_+) (Num_- := Int_-) (Num_* := Int_*) (Num_/ := Int_/); + +IntegerNum : Num Integer; +IntegerNum = + mkNum (Num_+ := Integer_+) (Num_- := Integer_-) + (Num_* := Integer_*) (Num_/ := Integer_/); + +FloatNum : Num Float; +FloatNum = + mkNum (Num_+ := Float_+) (Num_- := Float_-) + (Num_* := Float_*) (Num_/ := Float_/); + +type FromInt (α : Type) + | mkFromInt (FromInt_fromInt : Int -> α); + +typeclass FromInt; + +fromInt = lambda fromIntInst => case fromIntInst | mkFromInt fromInt => fromInt; + +IntFromInt : FromInt Int; +IntFromInt = mkFromInt (lambda x -> x); + +IntegerFromInt : FromInt Integer; +IntegerFromInt = mkFromInt Int->Integer;

===================================== samples/num_class_recs.typer ===================================== @@ -0,0 +1,33 @@ +record (Num (α : Type)) + (_+_ : α -> α -> α) + (_-_ : α -> α -> α) + (_*_ : α -> α -> α) + (_/_ : α -> α -> α); + +typeclass Num; + +_+_ = lambda numInst => Num._+_ numInst; +_-_ = lambda numInst => Num._-_ numInst; +_*_ = lambda numInst => Num._*_ numInst; +_/_ = lambda numInst => Num._/_ numInst; + +IntNum : Num Int; +IntNum = Num # Int_+ Int_- Int_* Int_/; + +IntegerNum : Num Integer; +IntegerNum = Num # Integer_+ Integer_- Integer_* Integer_/; + +FloatNum : Num Float; +FloatNum = Num # Float_+ Float_- Float_* Float_/; + +record (FromInt (α : Type)) (fromInt : Int -> α); + +typeclass FromInt; + +fromInt = lambda fromIntInst => FromInt.fromInt fromIntInst; + +IntFromInt : FromInt Int; +IntFromInt = FromInt # (lambda x -> x); + +IntegerFromInt : FromInt Integer; +IntegerFromInt = FromInt # Int->Integer;

===================================== src/REPL.ml ===================================== @@ -139,6 +139,7 @@ let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = unparsed tokens directly instead *) let ldecls, lctx = Elab.lexp_p_decls pdecls [] lctx in let lexprs = Elab.lexp_parse_all pexprs lctx in + List.iter Elab.resolve_instances lexprs; List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx lctx) lxp)) lexprs; (ldecls, lexprs), lctx

===================================== src/debruijn.ml ===================================== @@ -145,26 +145,29 @@ type meta_scope * lctx_length (* Length of ctx when the scope is added. *) * (meta_id SMap.t ref) (* Metavars already known in this scope. *)

+type typeclass_ctx + = (ltype * lctx_length) list (* FIXME make it a set of lexps ? *) + (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context - = Grammar.grammar * senv_type * lexp_context * meta_scope + = Grammar.grammar * senv_type * lexp_context * meta_scope * typeclass_ctx

let get_size (ctx : elab_context) - = let (_, (n, _), lctx, _) = ctx in + = let (_, (n, _), lctx, _, _) = ctx in assert (n = M.length lctx); n

let ectx_to_grm (ectx : elab_context) : Grammar.grammar = - let (grm,_, _, _) = ectx in grm + let (grm,_, _, _, _) = ectx in grm

(* Extract the lexp context from the context used during elaboration. *) let ectx_to_lctx (ectx : elab_context) : lexp_context = - let (_,_, lctx, _) = ectx in lctx + let (_,_, lctx, _, _) = ectx in lctx

-let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level +let ectx_to_scope_level ((_, _, _, (sl, _, _), _) : elab_context) : scope_level = sl

-let ectx_local_scope_size ((_, (n, _), _, (_, slen, _)) as ectx) : int +let ectx_local_scope_size ((_, (n, _), _, (_, slen, _), _) as ectx) : int = get_size ectx - slen

(* Public methods: DO USE @@ -175,7 +178,7 @@ let empty_lctx = M.nil

let empty_elab_context : elab_context = (Grammar.default_grammar, empty_senv, empty_lctx, - (0, 0, ref SMap.empty)) + (0, 0, ref SMap.empty), [])

(* senv_lookup caller were using Not_found exception *) exception Senv_Lookup_Fail of (string list) @@ -183,7 +186,7 @@ let senv_lookup_fail relateds = raise (Senv_Lookup_Fail relateds)

(* Return its current DeBruijn index. *) let senv_lookup (name: string) (ctx: elab_context): int = - let (_, (n, map), _, _) = ctx in + let (_, (n, map), _, _, _) = ctx in try n - (SMap.find name map) - 1 with Not_found -> let get_related_names (n : db_ridx) name map = @@ -222,11 +225,11 @@ let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) =

let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (loc, oname) = def in - let (grm, (n, map), env, sl) = ctx in + let (grm, (n, map), env, sl, tcctx) = ctx in let nmap = match oname with None -> map | Some name -> SMap.add name n map in (grm, (n + 1, nmap), lexp_ctx_cons env def v t, - sl) + sl, tcctx)

let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t

@@ -240,28 +243,33 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = ctx

let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = - let (grm, (n, senv), lctx, sl) = ctx in + let (grm, (n, senv), lctx, sl, tcctx) = ctx in let senv', _ = List.fold_left (fun (senv, i) ((_, oname), _, _) -> (match oname with None -> senv | Some name -> SMap.add name i senv), i + 1) (senv, n) defs in - (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl) + (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl, tcctx)

let ectx_new_scope (ectx : elab_context) : elab_context = - let (grm, senv, lctx, (scope, _, rmmap)) = ectx in - (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap))) + let (grm, senv, lctx, (scope, _, rmmap), tcctx) = ectx in + (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap)), tcctx)

let ectx_get_scope (ectx : elab_context) : meta_scope = - let (_, _, _, sl) = ectx in sl + let (_, _, _, sl, _) = ectx in sl

let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = - let (grm, _, _, _) = ectx in grm + let (grm, _, _, _, _) = ectx in grm

let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx

+let env_add_typeclass (ectx : elab_context) (t : ltype) : elab_context = + let (grm, senv, lctx, sl, tcctx) = ectx in + let ntcctx = ((t, get_size ectx) :: tcctx) in + (grm, senv, lctx, sl, ntcctx) + (* Print context *) let print_lexp_ctx_n (ctx : lexp_context) start = let n = (M.length ctx) - 1 in

===================================== 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 ===================================== @@ -57,6 +57,7 @@ open Grammar module BI = Builtin

module Unif = Unification +module Inst = Instances

module OL = Opslexp module EL = Elexp @@ -257,6 +258,13 @@ let newMetavar (ctx : lexp_context) sl name t = let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.identity, name)

+let newInstanceMetavar (ctx : elab_context) name t = + let lctx = ectx_to_lctx ctx in + let sl = ectx_to_scope_level ctx in + let meta = Unif.create_metavar lctx sl t in + Inst.add_instance_metavar meta ctx (fst name); + mkMetavar (meta, S.identity, name) + let newMetalevel (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level

@@ -278,10 +286,10 @@ 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) + let (grm, a, b, c, d) = ctx in + (SMap.add name (level l, level r) grm, a, b, c, d) | [o; _; _] -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ @@ -626,12 +634,83 @@ and get_implicit_arg ctx loc oname t = and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with + | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) when Inst.is_typeclass ctx t1 + -> let arg = newInstanceMetavar ctx (lexp_location e, v) t1 in + instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | _ -> (mkCall (e, List.rev args), t) in instantiate t []

+and myers_filter_map_index (f : int -> 'a -> 'b option) (m : 'a M.myers) + : ('b M.myers) + = snd (M.fold_right + (fun x (i, l') -> + match (f i x) with + | Some y -> (i - 1, M.cons y l') + | None -> (i - 1, l')) + m (M.length m - 1, M.nil)) + +and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp option = + Log.log_debug ~loc ("Searching for t = `" ^ (lexp_string t) ^ "`"); + let ctx = ectx_new_scope ctx in + let lctx = (ectx_to_lctx ctx) in + let sl = (ectx_to_scope_level ctx) in + let env_elem_match (i : int) (elem : DB.env_elem) : (int * DB.env_elem * lexp * ltype) option = + let ((_, namopt), _, t') = elem in + let var = mkVar ((loc,namopt), i) in + let t' = mkSusp t' (S.shift (i + 1)) in + let (e, t') = instantiate_implicit var t' ctx in + (* All candidates should have a type that is a typeclass *) + if not (Inst.is_typeclass ctx t') then None else + match Inst.check_typeclass_match t t' lctx sl with + | (Impossible | Possible) -> None + (* | Possible -> None *) + | (Match) -> Some (i, elem, e, t') in + let candidates = + myers_filter_map_index env_elem_match lctx in + Log.log_debug ("Candidates for instance of type `" ^ lexp_string t ^ "`:") + ~print_action:(fun () -> + M.iter (fun (i, ((_, so),_,t'),_, _) -> + lalign_print_int i 4; + lalign_print_string (match so with | Some s -> s | None -> "<none>") 10; + print_endline (lexp_string t')) candidates); + match M.safe_car candidates with + | None -> None + | Some (i, (vname, _, t'),e,t) -> + let t' = mkSusp t' (S.shift (i + 1)) in + Log.log_debug ~loc + ("Found candidate at index " ^ (string_of_int i) ^ ": `" ^ + (lexp_string (mkVar (vname, i))) ^ " : " ^ (lexp_string t') ^ "`"); + Some e + +and resolve_instances e = + let (_, (fv_map, _)) = OL.fv e in + U.IMap.iter (fun i (sl, t, cl, vn) -> + match Inst.instance_metavar_lookup i with + | Some (ctx, loc) -> + (match search_instance ctx loc t with + | Some e -> Unif.associate i e; resolve_instances e + | None -> + error ~loc ("No instance found for type `" ^ (lexp_string t) ^ "`") + ) + | None -> () + ) fv_map + + +and resolve_instances_and_generalize ctx e = + resolve_instances e; + generalize ctx e + +and sdform_typeclass (ctx : elab_context) loc sargs _ot : elab_context = + match sargs with + | [se] -> + let (t, _) = infer se ctx in + Inst.add_typeclass ctx t + | _ + -> sexp_error loc "typeclass expects 1 argument"; ctx + and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated @@ -694,6 +773,23 @@ 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)" + | _ -> failwith "impossible") + ^ "! 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 +800,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. *) @@ -983,11 +1066,13 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (* Don't instantiate after the last explicit arg: the rest is done, * when needed in infer_and_check (via instantiate_implicit). *) when not (sargs = [] && SMap.is_empty pending) - -> let larg = get_implicit_arg - ctx (match sargs with - | [] -> loc - | sarg::_ -> sexp_location sarg) - v arg_type in + -> let larg = if Inst.is_typeclass ctx arg_type + then newInstanceMetavar ctx (loc, v) arg_type + else get_implicit_arg + ctx (match sargs with + | [] -> loc + | sarg::_ -> sexp_location sarg) + v arg_type in handle_fun_args ((ak, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) | [], _ @@ -1033,7 +1118,7 @@ and lexp_parse_inductive ctors ctx = (fun (ak, n, t) aa -> mkArrow (ak, n, t, dummy_location, aa)) acc impossible in - let g = generalize nctx altacc in + let g = resolve_instances_and_generalize nctx altacc in let altacc' = g (fun _ne vname t l e -> mkArrow (Aerasable, vname, t, l, e)) altacc in @@ -1148,9 +1233,9 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (* FIXME: Generalize when/where possible, so things like `map` can be defined without type annotations! *) (* Preserve the new operators added to nctx. *) - let ectx = let (_, a, b, c) = ectx in - let (grm, _, _, _) = nctx in - (grm, a, b, c) in + let ectx = let (_, a, b, c, _) = ectx in + let (grm, _, _, _, tcctx) = nctx in + (grm, a, b, c, tcctx) in let (declmap, nctx) = List.fold_right (fun ((l, vname), pexp) (map, nctx) -> @@ -1160,10 +1245,11 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) | (v', ForwardRef, t) -> let adjusted_t = push_susp t (S.shift (i + 1)) in let e = check pexp adjusted_t nctx in - let (grm, ec, lc, sl) = nctx in + resolve_instances e; + let (grm, ec, lc, sl, tcctx) = nctx in let d = (v', LetDef (i + 1, e), t) in (IMap.add i ((l, Some vname), e, t) map, - (grm, ec, Myers.set_nth i d lc, sl)) + (grm, ec, Myers.set_nth i d lc, sl, tcctx)) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in @@ -1201,7 +1287,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = -> mkArrow (ak, v, t1, l, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in - let g = generalize nctx (strip_rettype t) in + let g = resolve_instances_and_generalize nctx (strip_rettype t) in g (fun _ne name t l e -> mkArrow (Aerasable, name, t, l, e)) t @@ -1209,7 +1295,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in let (e,t) = infer se nctx in - let g = generalize nctx e in + let g = resolve_instances_and_generalize nctx e in let e' = g (fun ne vname t l e -> mkLambda ((if ne then Aimplicit else Aerasable), vname, t, e)) @@ -1341,6 +1427,10 @@ and lexp_decls_1 -> recur [] (sdform_define_operator nctx l args None) pending_decls pending_defs

+ | Some (Node (Symbol (l, "typeclass"), args)) + -> recur [] (sdform_typeclass nctx l args None) + pending_decls pending_defs + | Some (Node (Symbol ((l, _) as v), sargs)) -> (* expand macro and get the generated declarations *) let sdecl' = lexp_decls_macro v sargs nctx in @@ -1369,10 +1459,12 @@ and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) impl sdecls tokens ctx

and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = + Eval.set_getenv ctx; let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in (Log.stop_on_error (); res)

and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = + Eval.set_getenv ctx; let e, _ = infer e ctx in (Log.stop_on_error (); e)

(* -------------------------------------------------------------------------- @@ -1711,10 +1803,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 +1893,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 @@ -1878,6 +1968,22 @@ let sform_load usr_elctx loc sargs ot =

(tuple',Lazy)

+(** + Draft of a special form "instance" that gets refers to a variable + of the requested type in the context. + **) +let sform_instance ctx loc sargs ot = + match sargs, ot with + | ([se; _], _) -> (* Dummy param to trigger the special form *) + let t = infer_type se ctx (loc, None) in + let mv = newInstanceMetavar ctx (loc, Some "instance") t in + (mv, Inferred t) + | ([_], Some t) -> (* Dummy param to trigger the special form *) + let mv = newInstanceMetavar ctx (loc, Some "instance") t in + (mv, Checked) + | _ -> (sexp_error loc "##instance expects a type argument if not checked"; + sform_dummy_ret ctx loc) + (* Register special forms. *) let register_special_forms () = List.iter add_special_form @@ -1907,6 +2013,7 @@ let register_special_forms () = (* FIXME: These should be functions! *) ("decltype", sform_decltype); ("declexpr", sform_declexpr); + ("instance", sform_instance); ]

(* Default context with builtin types

===================================== 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. *) @@ -743,6 +804,14 @@ let constructor_p name ectx = | _ -> false with Senv_Lookup_Fail _ -> false

+let inductive_p name ectx = + try let idx = senv_lookup name ectx in + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) with + | Inductive _ -> true + | _ -> false + with Senv_Lookup_Fail _ -> false + let erasable_p name nth ectx = let is_erasable ctors = match (SMap.find_opt name ctors) with | (Some args) -> @@ -821,10 +890,43 @@ let ctor_arg_pos name arg ectx = | _ -> (-1) with Senv_Lookup_Fail _ -> (-1)

+let ind_ctor_arg_pos indname ctorname arg ectx = + let rec find_opt xs n = match xs with + | [] -> None + | (_, (_, Some x), _)::xs -> if x = arg then Some n else find_opt xs (n + 1) + | _::xs -> find_opt xs (n + 1) in + try let idx = senv_lookup indname ectx in + match OL.lexp'_whnf (mkVar ((dummy_location, Some indname), idx)) + (ectx_to_lctx ectx) with + | Inductive (_, _, _, ctors) -> + (match SMap.find_opt ctorname ctors with + | (Some args) -> + (match (find_opt args 0) with + | None -> (-1) + | Some n -> n) + | _ -> (-1)) + | _ -> (-1) + with Senv_Lookup_Fail _ -> (-1) + +let count_ctor_args indname ctorname ectx = + try let idx = senv_lookup indname ectx in + match OL.lexp'_whnf (mkVar ((dummy_location, Some indname), idx)) + (ectx_to_lctx ectx) with + | Inductive (_,_,_,ctors) -> + (match SMap.find_opt ctorname ctors with + | Some args -> List.length args + | None -> (-1)) + | _ -> (-1) + with Senv_Lookup_Fail _ -> (-1) + let is_constructor loc depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx) | _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments"

+let is_inductive loc depth args_val = match args_val with + | [Vstring name; Velabctx ectx] -> o2v_bool (inductive_p name ectx) + | _ -> error loc "Elab.isinductive takes a String and an Elab_Context as arguments" + let is_nth_erasable loc depth args_val = match args_val with | [Vstring name; Vint nth_arg; Velabctx ectx] -> o2v_bool (erasable_p name nth_arg ectx) | _ -> error loc "Elab.is-nth-erasable takes a String, an Int and an Elab_Context as arguments" @@ -841,6 +943,14 @@ let arg_pos loc depth args_val = match args_val with | [Vstring t; Vstring a; Velabctx ectx] -> Vint (ctor_arg_pos t a ectx) | _ -> error loc "Elab.arg-pos takes two String and an Elab_Context as arguments"

+let ind_ctor_arg_pos loc depth args_val = match args_val with + | [Vstring ind; Vstring ctor; Vstring field; Velabctx ectx] -> Vint (ind_ctor_arg_pos ind ctor field ectx) + | _ -> error loc "Elab.ind-ctor-arg-pos takes three String and an Elab_Context as arguments" + +let count_ctor_args loc depth args_val = match args_val with + | [Vstring ind; Vstring ctor; Velabctx ectx] -> Vint (count_ctor_args ind ctor ectx) + | _ -> error loc "Elab.count-ctor-args takes two String and an Elab_Context as arguments" + let array_append loc depth args_val = match args_val with | [v; Varray a] -> Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v)) @@ -996,10 +1106,13 @@ let register_builtin_functions () = ("Elab.debug-doc", debug_doc, 2); ("Elab.isbound" , is_bound, 2); ("Elab.isconstructor", is_constructor, 2); + ("Elab.isinductive", is_inductive, 2); ("Elab.is-nth-erasable", is_nth_erasable, 3); ("Elab.is-arg-erasable", is_arg_erasable, 3); ("Elab.nth-arg" , nth_arg, 3); ("Elab.arg-pos" , arg_pos, 3); + ("Elab.ind-ctor-arg-pos", ind_ctor_arg_pos, 4); + ("Elab.count-ctor-args", count_ctor_args, 3); ("Array.append" , array_append,2); ("Array.create" , array_create,2); ("Array.length" , array_length,1);

===================================== src/instances.ml ===================================== @@ -0,0 +1,53 @@ +module Unif = Unification +module U = Util +module DB = Debruijn +module L = Lexp +module S = Subst +module OL = Opslexp + +(* FIXME Is it possible to have multiple references to the same + instance metavar? It would break the following code *) +let instance_metavar_table = ref (U.IMap.empty : (DB.elab_context * U.location) U.IMap.t) +let instance_metavar_lookup (id : L.meta_id) : (DB.elab_context * U.location) option + = U.IMap.find_opt id (!instance_metavar_table) +let add_instance_metavar (id : L.meta_id) (ctx : DB.elab_context) (loc : U.location) : unit + = instance_metavar_table := U.IMap.add id (ctx, loc) !instance_metavar_table + +let env_is_typeclass (ectx : DB.elab_context) (t : L.ltype) : bool = + let (_, _, _, _, tcctx) = ectx in + let cl = DB.get_size ectx in + List.exists (fun (t', cl') -> + let i = cl - cl' in + let t' = L.mkSusp t' (S.shift i) in + OL.conv_p (DB.ectx_to_lctx ectx) t t' + (*(Unif.unify ~checking:(max_int (* FIXME *)) t t' (DB.ectx_to_lctx ectx)) = []*) + ) tcctx + + +let get_head (lctx : DB.lexp_context) (t : L.ltype) : L.ltype = + let whnft = OL.lexp_whnf t lctx in + match L.lexp_lexp' whnft with + | L.Call (head, _) -> head + | _ -> whnft + + +let is_typeclass (ctx : DB.elab_context) (t : L.ltype) = + let lctx = DB.ectx_to_lctx ctx in + let head = get_head lctx t in + env_is_typeclass ctx head + +let add_typeclass (ctx : DB.elab_context) (t : L.ltype) : DB.elab_context = + let lctx = DB.ectx_to_lctx ctx in + let head = get_head lctx t in + DB.env_add_typeclass ctx head + +type match_res = Impossible | Possible | Match + +let check_typeclass_match t1 t2 lctx sl = + match Unif.unify ~checking:sl t1 t2 lctx with + | [] -> Match + | constraints when List.exists (function | (Unif.CKimpossible,_,_,_) -> true + | _ -> false) + constraints -> Impossible + | _ -> Possible +

===================================== 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/log.ml ===================================== @@ -133,11 +133,13 @@ let print_entry entry = let log_entry (entry : log_entry) = if (entry.level <= typer_log_config.level) then ( - log_push entry; - if (typer_log_config.print_at_log) + if (typer_log_config.print_at_log || + entry.level >= Debug) then (print_entry entry; flush stdout) + else + log_push entry )

let count_msgs (lvlp : log_level -> bool) =

===================================== src/myers.ml ===================================== @@ -54,11 +54,21 @@ let car l = | Mnil -> raise Not_found | Mcons (x, _, _, _) -> x

+let safe_car l = + match l with + | Mnil -> None + | Mcons (x, _, _, _) -> Some x + let cdr l = match l with | Mnil -> Mnil | Mcons (_, l, _, _) -> l

+let safe_cdr l = + match l with + | Mnil -> None + | Mcons (_, l, _, _) -> Some l + let case l n c = match l with | Mnil -> n () @@ -136,3 +146,6 @@ let rec fold_right f l i = match l with let map f l = fold_right (fun x l' -> cons (f x) l') l nil

let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l + +let iter (f : 'a -> unit) (l : 'a myers) : unit + = fold_left (fun _ x -> f x; ()) () l

===================================== src/opslexp.ml ===================================== @@ -874,6 +874,7 @@ and mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set and mv_set_erase (ms, _nes) = (ms, IMap.empty)

and fv_memo = LMap.create 1000 +and fv_flush () = LMap.clear fv_memo

and fv_empty = (DB.set_empty, mv_set_empty) and fv_union (fv1, mv1) (fv2, mv2)

===================================== 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 ===================================== @@ -46,6 +46,7 @@ let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) type constraint_kind = | CKimpossible (* Unification is simply impossible. *) | CKresidual (* We failed to find a unifier. *) + | CKassoc (* Couldn't associate because of checking mode *) (* FIXME: Each constraint should additionally come with a description of how it relates to its "top-level" or some other info which might let us fix the problem (e.g. by introducing coercions). *) @@ -54,8 +55,9 @@ type constraints = (constraint_kind * DB.lexp_context * lexp * lexp) list type return_type = constraints

(** Alias for VMap.add*) -let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst - = U.IMap.add id (MVal lxp) subst +let associate (id: meta_id) (lxp: lexp) : unit + = metavar_table := U.IMap.add id (MVal lxp) (!metavar_table); + OL.fv_flush ()

let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | MVal _ -> Log.internal_error @@ -171,17 +173,36 @@ 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) -*) -let rec unify (e1: lexp) (e2: lexp) + 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 ?checking + (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) : return_type = - unify' e1 e2 ctx OL.set_empty + unify' e1 e2 ctx OL.set_empty checking

and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) + (c : scope_level option) (* checking mode scope level *) : return_type = if e1 == e2 then [] else let e1' = OL.lexp_whnf e1 ctx in @@ -191,28 +212,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)] - | (_, 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 + + (* 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 c ctx idx s e2' e1' + | (Metavar (idx, s, _), _) -> unify_metavar c ctx idx s 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 c e2' e1' ctx vs' + | (Call _, _) -> unify_call c 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 c e2' e1' ctx vs' + | (Arrow _, _) -> unify_arrow c e1' e2' ctx vs' + | (_, Lambda _) -> unify_lambda c e2' e1' ctx vs' + | (Lambda _, _) -> unify_lambda c e1' e2' ctx vs' + | (_, Sort _) -> unify_sort c e2' e1' ctx vs' + | (Sort _, _) -> unify_sort c e1' e2' ctx vs' + | (_, SortLevel _) -> unify_sortlvl c e2' e1' ctx vs' + | (SortLevel _, _) -> unify_sortlvl c e1' e2' ctx vs' + | (_, Inductive _) -> unify_inductive c e2' e1' ctx vs' + | (Inductive _, _) -> unify_inductive c e1' e2' ctx vs' + | (_, Cons _) -> unify_cons c e2' e1' ctx vs' + | (Cons _, _) -> unify_cons c 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,106 +261,96 @@ 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 +and unify_arrow (checking : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' arrow, lexp_lexp' lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 - then (unify' ltype1 ltype2 ctx vs) + then (unify' ltype1 ltype2 ctx vs checking) @(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 + (OL.set_shift vs) checking) + 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 = +and unify_lambda (checking : scope_level option) (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lexp_lexp' lambda, lexp_lexp' lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 - then (unify' ltype1 ltype2 ctx vs) + then (unify' ltype1 ltype2 ctx vs checking) @(unify' lexp1 lexp2 (DB.lexp_ctx_cons ctx v1 Variable ltype1) - (OL.set_shift vs)) + (OL.set_shift vs) checking) 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) +and unify_metavar (checking : scope_level option) ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = - let t = match metavar_lookup idx with + let t, sl = match metavar_lookup idx with | MVal _ -> Log.internal_error "`lexp_whnf` returned an instantiated metavar!!" - | MVar (_, t, _) -> push_susp t s in + | MVar (_, t, sl) -> push_susp t s, sl in match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible - -> log_info ?loc:None ("Unification of metavar failed:\n " - ^ "?[" ^ subst_string s ^ "]" - ^ "\nAgainst:\n " - ^ lexp_string lxp ^ "\n"); + -> log_info ~loc:(lexp_location lxp) + ("Unification of metavar failed:\n " + ^ "?[" ^ subst_string s ^ "]" + ^ "\nAgainst:\n " + ^ lexp_string lxp ^ "\n"); [(CKresidual, ctx, lxp1, lxp2)] | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' - -> metavar_table := associate idx lxp' (!metavar_table); - let type_unif_residue = - match unify t (OL.get_type ctx lxp) ctx with - | [] as r -> r - (* FIXME: Let's ignore the error for now. *) - | _ - -> log_info ?loc:None - ("Unification of metavar type failed:\n " - ^ lexp_string t ^ " != " - ^ lexp_string (OL.get_type ctx lxp) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - [(CKresidual, ctx, lxp1, lxp2)] in - (* FIXME Here, we unify lxp1 with lxp2 again, because that - the metavariables occuring in the associated term might - have different substitutions from the corresponding - metavariables on the other side (due to subst inversion - not being a perfect inverse of subtitution application). - - For example, when unifying `?τ↑1[114]` with `(List[56] - ?ℓ↑0[117] ?a↑0[118])`, we associate the metavar ?τ[114] - with the lexp `(List[55] ?ℓ() · ↑0[117] ?a() · ↑0[118])` - (after applying the inverse substitution of ↑1), and the - lexp (?τ↑1[114]) becomes `(List[56] ?ℓ(↑1 () · ↑0)[117] - ?a(↑1 () · ↑0)[118])`, which is not exactly the same as - the right-hand side. My solution/kludge to this problem is - to do a second unification to fix the metavar - substitutions on the right-hand side, but there is - probably a cleaner way to solve this. *) - let second_unif_residue = unify lxp1 lxp2 ctx in - List.append type_unif_residue second_unif_residue in + -> match checking with + | Some l when l >= sl -> [(CKassoc, ctx, lxp1, lxp2)] + | _ -> ( + associate idx lxp'; + let type_unif_residue = + match unify t (OL.get_type ctx lxp) ctx with + | [] as r -> r + (* FIXME: Let's ignore the error for now. *) + | _ + -> log_info ?loc:None + ("Unification of metavar type failed:\n " + ^ lexp_string t ^ " != " + ^ lexp_string (OL.get_type ctx lxp) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + [(CKresidual, ctx, lxp1, lxp2)] in + (* FIXME Here, we unify lxp1 with lxp2 again, because that + the metavariables occuring in the associated term might + have different substitutions from the corresponding + metavariables on the other side (due to subst inversion + not being a perfect inverse of subtitution application). + + For example, when unifying `?τ↑1[114]` with `(List[56] + ?ℓ↑0[117] ?a↑0[118])`, we associate the metavar ?τ[114] + with the lexp `(List[55] ?ℓ() · ↑0[117] ?a() · ↑0[118])` + (after applying the inverse substitution of ↑1), and the + lexp (?τ↑1[114]) becomes `(List[56] ?ℓ(↑1 () · ↑0)[117] + ?a(↑1 () · ↑0)[118])`, which is not exactly the same as + the right-hand side. My solution/kludge to this problem + is to do a second unification to fix the metavar + substitutions on the right-hand side, but there is + probably a cleaner way to solve this. *) + let second_unif_residue = unify lxp1 lxp2 ctx in + List.append type_unif_residue second_unif_residue) in match lexp_lexp' lxp2 with | Metavar (idx2, s2, name) - -> if idx = idx2 then + -> if idx = idx2 && checking == None then match common_subset ctx s1 s2 with | S.Identity 0 -> [] (* Optimization! *) (* ¡ s1 != s2 ! @@ -373,7 +401,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) * ^ "\n =\n " * ^ subst_string (scompose s s2) * ^ "\n"); *) - metavar_table := associate idx lexp (!metavar_table); + associate idx lexp; assert (OL.conv_p ctx lxp1 lxp2); [] else @@ -384,22 +412,34 @@ 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 *) -and unify_call (call: lexp) (lxp: lexp) ctx vs +and unify_call (checking : scope_level option) (call: lexp) (lxp: lexp) ctx vs : return_type = 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 + (unify' e1 e2 ctx vs checking)@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 @@ -458,32 +498,30 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - SortLevel, _ -> ERROR *) -and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = +and unify_sortlvl (checking : scope_level option) (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = match lexp_lexp' sortlvl, lexp_lexp' lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> [] - | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs + | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs checking | SLlub (l11, l12), SLlub (l21, l22) -> (* FIXME: This SLlub representation needs to be * more "canonicalized" otherwise it's too restrictive! *) - (unify' l11 l21 ctx vs)@(unify' l12 l22 ctx vs) + (unify' l11 l21 ctx vs checking)@(unify' l12 l22 ctx vs checking) | _, _ -> [(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 = +and unify_sort (checking : scope_level option) (sort_: lexp) (lxp: lexp) ctx vs : return_type = match lexp_lexp' sort_, lexp_lexp' lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with - | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs + | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs checking | 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 +571,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 (checking : scope_level option) lxp1 lxp2 ctx vs = + match lexp_lexp' lxp1, lexp_lexp' lxp2 with + | (Inductive (_loc1, label1, args1, consts1), + Inductive (_loc2, label2, args2, consts2)) + -> unify_inductive' (checking : scope_level option) ctx vs args1 args2 consts1 consts2 lxp1 lxp2 + | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)] + +and unify_inductive' (checking : scope_level option) 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)]) @@ -542,7 +587,7 @@ and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = -> (DB.lexp_ctx_cons ctx v1 Variable t1, OL.set_shift vs, if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] - else (unify' t1 t2 ctx vs) @ residue)) + else (unify' t1 t2 ctx vs checking) @ residue)) (ctx, vs, []) (List.combine args1 args2) in let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in @@ -578,3 +623,8 @@ and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = * | _, _ -> None * in test l1 l2 subst *)

+and unify_cons (checking : scope_level option) 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 checking + | _, _ -> [(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,98 @@ 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) + | _ -> failwith "impossible" + +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/5b458959d3c5209c907ab368f96d82caa...