[Typer] [Git][monnier/typer][ja-barszcz] 23 commits: Fix `lexp_whnf` for Case

Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer

Commits: ecf0604b by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 Fix `lexp_whnf` for Case

A substitution built with `cons`es happens all at once, in the sense that the terms in such a list are substituted independently, and thus should not be shifted one relative to another.

This commit removes such a shift that was made by mistake in the computation of the WHNF of a `Case` redex. The shift caused debruijn indexing errors in the body of branches with multiple fields.

Additionnally, this commit removes the arguments to the inductive type from the substitution applied to the branch, since they are not bound by the case.

- - - - - fc0eca14 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] Make unification symmetric

- - - - - 781bb80b by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] Handle variables earlier during unification

- - - - - 6a15b3d8 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] experiments with Decidable and proofs

- - - - - 32df061f by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] unify instead of conv_p in sform_lambda

- - - - - 03d9edec by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] proof of Decidable (a < b)

- - - - - a3b4be48 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] First draft of an instance search algorithm

- - - - - 6ebb745f by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 WIP WIP WIP

- - - - - 1c718ddf by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 WIP WIP getting there

- - - - - 265eb152 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] Add a set of typeclasses to the elab context

- - - - - 113e45b5 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] Add a syntax for records

- - - - - 9e65db64 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] Extend the Decidable sample with conjunction (dep on records)

- - - - - 9cd4cc78 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 Resolve instances in the REPL (since exprs. are not generalized)

- - - - - 7f6c7124 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 Resolve instances for recursive definitions

- - - - - bf2ab158 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-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.

- - - - - 777c472a by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 Num class example

- - - - - fc4cf72d by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 Num class (with records)

- - - - - 83432703 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 Allow non-inductives to be typeclasses (Eq for instance)

- - - - - 6291b3f5 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 Move the Eq builtin to debruijn.ml to make it available for elab.

- - - - - 189bd1af by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 Make Eq.refl available to the ocaml code

* src/debruijn.ml : Add a definition of the lexp for Eq.refl

* src/builtin.ml : Register the constant Eq.refl

* btl/builtins.typer (Eq_refl) : Use the builtin variable ##Eq.refl instead of registering the builtin with the `Built-in` form. This ensures that we have the right variable and type, and might help to keep things in sync between the ocaml and typer code.

- - - - - d9f84fc5 by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] Add Eq to case

- - - - - 402cde7b by Jean-Alexandre Barszcz at 2020-08-24T17:55:49-04:00 [WIP] Adding Eq to Case: mutual rec for (whnf & get_type) + conv_p of case?

- - - - - 7619fb6c by Jean-Alexandre Barszcz at 2020-08-24T19:47:59-04:00 Algebra classes sample with proofs for the additive monoid for Nats

- - - - -

21 changed files:

- btl/builtins.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/builtin.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - + src/instances.ml - src/inverse_subst.ml - src/lexp.ml - src/log.ml - src/myers.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml - tests/unify_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -48,7 +48,7 @@ Void = typecons Void; %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l Eq_refl : ((x : ?t) ≡> Eq x x); -Eq_refl = Built-in "Eq.refl"; +Eq_refl = ##Eq.refl;

Eq_cast : (x : ?) ≡> (y : ?) ≡> (p : Eq x y) @@ -363,6 +363,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 +395,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/pervasive.typer ===================================== @@ -394,7 +394,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 +411,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) @@ -458,7 +459,8 @@ Not prop = prop -> False; %% We don't use the `type` macro here because it would make these `true` %% and `false` constructors override `Bool`'s, and we currently don't %% want that. -Decidable = typecons (Decidable (prop : Type_ ?ℓ)) +%% FIXME generalize typecons formal arguments +Decidable = typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ)) (true (p ::: prop)) (false (p ::: Not prop));

%% Testing generalization in inductive type constructors. @@ -547,6 +549,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 +662,15 @@ plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro; %% _|_ = let lib = load "btl/polyfun.typer" in lib._|_;

+%% +%% 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,82 @@ +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 (i - 1) (n - 1))) + else (cons (Sexp_symbol "_") (arg_pats s (i - 1) (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; %% I was going for a syntax close to + %% Erlang's, but the # doesn't separate + %% tokens ... Meh. + +record (Pair (a : Type) (b : Type)) (fst : a) (snd : a);

===================================== samples/alg_classes.typer ===================================== @@ -0,0 +1,111 @@ +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 + | Zero => Eq_cast + (x := Zero) + (y := x) + (p := Eq_comm (instance ())) + (f := (lambda (Zx : Nat) -> Eq (plus (plus Zx y) z) (plus Zx (plus y z)))) + Eq_refl + | Succ x' => + Eq_cast + (x := Succ x') + (y := x) + (p := Eq_comm (instance ())) + (f := (lambda (sx'x : Nat) -> Eq (plus (plus sx'x y) z) (plus sx'x (plus y z)))) + (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 + | Zero => Eq_cast + (x := Zero) + (y := x) + (p := Eq_comm (instance ())) + (f := (lambda (Zx : Nat) -> + Eq (plus Zx Zero) Zx)) + Eq_refl + | Succ x' => Eq_cast + (x := Succ x') + (y := x) + (p := Eq_comm (instance ())) + (f := (lambda (Sx'x : Nat) -> + Eq (plus Sx'x Zero) Sx'x)) + (Eq_cong (p := zeroIsPlusRIdent x') Succ); + +natAdditiveMonoid : Monoid Nat; +natAdditiveMonoid = mkMonoid natAdditiveSemigroup Zero + (isIdent := pair zeroIsPlusLIdent zeroIsPlusRIdent);

===================================== samples/decidable.typer ===================================== @@ -0,0 +1,168 @@ +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); +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/builtin.ml ===================================== @@ -99,19 +99,6 @@ let dloc = DB.dloc let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, mkArrow (Anormal, (dloc, None), t, dloc, t))

-let type_eq = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, - DB.type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 1), dloc, - mkSort (dloc, Stype (mkVar (lv, 3))))))) - let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx

(* Typer list as seen during runtime. *) @@ -161,7 +148,9 @@ let register_builtin_csts () = add_builtin_cst "Integer" DB.type_integer; add_builtin_cst "Float" DB.type_float; add_builtin_cst "String" DB.type_string; - add_builtin_cst "Elab_Context" DB.type_elabctx + add_builtin_cst "Elab_Context" DB.type_elabctx; + add_builtin_cst "Eq" DB.type_eq; + add_builtin_cst "Eq.refl" DB.eq_refl

let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in @@ -175,7 +164,6 @@ let register_builtin_types () = "Array" (mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0)) in let _ = new_builtin_type "FileHandle" DB.type0 in - let _ = new_builtin_type "Eq" type_eq in ()

let _ = register_builtin_csts ();

===================================== src/debruijn.ml ===================================== @@ -94,6 +94,37 @@ let type_integer = mkBuiltin ((dloc, "Integer"), type0, None) let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None) let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0, None) +let type_eq_type = + let lv = (dloc, Some "l") in + let tv = (dloc, Some "t") in + mkArrow (Aerasable, lv, + type_level, dloc, + mkArrow (Aerasable, tv, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, + mkArrow (Anormal, (dloc, None), + mkVar (tv, 0), dloc, + mkArrow (Anormal, (dloc, None), + mkVar (tv, 1), dloc, + mkSort (dloc, Stype (mkVar (lv, 3))))))) +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type, None) +let eq_refl = + let lv = (dloc, Some "l") in + let tv = (dloc, Some "t") in + let xv = (dloc, Some "x") in + mkBuiltin ((dloc, "Eq.refl"), + mkArrow (Aerasable, lv, + type_level, dloc, + mkArrow (Aerasable, tv, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, + mkArrow (Aerasable, xv, + mkVar (tv, 0), dloc, + mkCall (type_eq, + [Aerasable, mkVar (lv, 2); + Aerasable, mkVar (tv, 1); + Anormal, mkVar (xv, 0); + Anormal, mkVar (xv, 0)])))), + None) +

(* easier to debug with type annotations *) type env_elem = (vname * varbind * ltype) @@ -112,26 +143,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 @@ -142,7 +176,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) @@ -150,7 +184,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 = @@ -189,11 +223,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

@@ -207,28 +241,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/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

@@ -280,8 +288,8 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = | Symbol (_, "") -> None | Integer (_, n) -> Some 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 | _ @@ -466,11 +474,11 @@ let rec meta_to_var ids (e : lexp) = -> let ncases = SMap.map (fun (l, fields, e) - -> (l, fields, loop (o + List.length fields) e)) + -> (l, fields, loop (o + List.length fields + 1) e)) cases in mkCase (l, loop o e, loop o t, ncases, match default with None -> None - | Some (v, e) -> Some (v, loop (1 + o) e)) + | Some (v, e) -> Some (v, loop (2 + o) e)) | Metavar (id, s, name) -> if IMap.mem id ids then mkVar (name, o + count - IMap.find id ids) @@ -625,12 +633,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 (Var (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 @@ -707,7 +786,8 @@ and check_inferred ctx e inferred_t t = -> lexp_error (lexp_location e) e ("Type mismatch(" ^ (match ck with | Unif.CKimpossible -> "impossible" - | Unif.CKresidual -> "residue") + | Unif.CKresidual -> "residue" + | _ -> failwith "impossible" ) ^ ")! Context expected:\n " ^ lexp_string t ^ "\nbut expression has type:\n " ^ lexp_string inferred_t ^ "\ncan't unify:\n " @@ -738,16 +818,16 @@ and check_case rtype (loc, target, ppatterns) ctx = let ltarget = ref tlxp in

let get_cs_as it' lctor = + let unify_ind expected actual = + match Unif.unify actual expected (ectx_to_lctx ctx) with + | (_::_) + -> lexp_error loc lctor + ("Expected pattern of type `" ^ lexp_string expected + ^ "` but got `" ^ lexp_string actual ^ "`") + | [] -> () in match !it_cs_as with | Some (it, cs, args) - -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with - | (_::_) - -> lexp_error loc lctor - ("Expected pattern of type `" - ^ lexp_string it ^ "` but got `" - ^ lexp_string it' ^ "`") - | [] -> () in - (cs, args) + -> unify_ind it it'; (cs, args) | None -> match OL.lexp_whnf it' (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) @@ -768,6 +848,7 @@ and check_case rtype (loc, target, ppatterns) ctx = with | Call (f, args) -> (f, args) | _ -> (e,[]) in let (it, targs) = call_split tltp in + unify_ind it it'; let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); @@ -776,14 +857,42 @@ and check_case rtype (loc, target, ppatterns) ctx = ("Can't `case` on objects of this type: " ^ lexp_string tltp); SMap.empty in + it_cs_as := Some (it, constructors, targs); (constructors, targs) in

(* Read patterns one by one *) let fold_fun (lbranches, dflt) (pat, pexp) =

+ let shift_to_extended_ctx nctx lexp = + mkSusp lexp (S.shift (M.length (ectx_to_lctx nctx) + - M.length (ectx_to_lctx ctx))) in + + let ctx_extend_with_eq nctx head_lexp = + (* Add a proof of equality between the target and the branch + head to the context *) + let tlxp' = shift_to_extended_ctx nctx tlxp in + let tltp' = shift_to_extended_ctx nctx tltp in + let tkind = OL.get_type (ectx_to_lctx nctx) tltp' in + let tlevel = (match OL.lexp_whnf tkind (ectx_to_lctx nctx) with + | Sort (_, Stype l) -> l + | _ -> error "HMMM"; DB.level0) in + let head_lexp_type = OL.get_type (ectx_to_lctx nctx) head_lexp in + (match Unif.unify tltp' head_lexp_type (ectx_to_lctx nctx) with + | [] -> () + | constraints -> Log.log_error "Unification failed for case Eq"); + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlevel); (* Typelevel *) + (Aerasable, tltp'); (* Inductive type *) + (Anormal, tlxp'); (* Target lexp *) + (Anormal, head_lexp)]) (* Lexp of the branch head *) + in ctx_extend nctx (loc, None) Variable eqty + in + let add_default v = (if dflt != None then uniqueness_warn pat); let nctx = ctx_extend ctx v Variable tltp in + let head_lexp = mkVar (v, 0) in + let nctx = ctx_extend_with_eq nctx head_lexp in let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - M.length (ectx_to_lctx ctx))) in let lexp = check pexp rtype' nctx in @@ -864,6 +973,15 @@ and check_case rtype (loc, target, ppatterns) ctx = make_nctx nctx (ssink var s) pargs cargs pe ((ak, var)::acc) in let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in + let head_lexp_ctor = + shift_to_extended_ctx nctx + (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in + let head_lexp_args = + List.mapi (fun i (ak, vname) -> + (* This is not pretty :( *) + (ak, mkVar (vname, List.length fargs - i - 1))) fargs in + let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in + let nctx = ctx_extend_with_eq nctx head_lexp in let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - M.length (ectx_to_lctx ctx))) in @@ -946,11 +1064,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)) | [], _ @@ -996,7 +1116,7 @@ and lexp_parse_inductive ctors ctx = (fun (ak, n, t) aa -> Arrow (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 -> Arrow (Aerasable, vname, t, l, e)) altacc in @@ -1110,9 +1230,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) -> @@ -1122,10 +1242,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 @@ -1161,7 +1282,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = | Arrow (ak, v, t1, l, t2) -> Arrow (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 @@ -1169,7 +1290,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)) @@ -1301,6 +1422,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 @@ -1329,10 +1454,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)

(* -------------------------------------------------------------------------- @@ -1657,10 +1784,21 @@ 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 ^ "`")); + -> (match Unif.unify lt1' lt1 (ectx_to_lctx ctx) with + | ((ck, _ctx, t1, t2)::_) + -> lexp_error (lexp_location lt1') lt1' + ("Type mismatch(" + ^ (match ck with | Unif.CKimpossible -> "impossible" + | Unif.CKresidual -> "residue" + | _ -> failwith "impossible") + ^ ")! Context expected:\n " + ^ lexp_string lt1 ^ "\nbut parameter has type:\n " + ^ lexp_string lt1' ^ "\ncan't unify:\n " + ^ lexp_string t1 + ^ "\nwith:\n " + ^ lexp_string t2); + assert (not (OL.conv_p (ectx_to_lctx ctx) lt1' lt1)) + | [] -> ())); mklam lt1 (Some lt2)

| Arrow (ak2, v, lt1, _, lt2) when kind = Anormal @@ -1824,6 +1962,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 @@ -1853,6 +2007,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 ===================================== @@ -744,6 +744,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 +829,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 +882,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 +1045,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,52 @@ +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 = + match OL.lexp_whnf t lctx with + | L.Call (head, _) -> head + | head -> head + + +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/inverse_subst.ml ===================================== @@ -300,11 +300,12 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, apply_inv_subst e s')) + let s'' = ssink (l, None) s' in + (l, cargs, apply_inv_subst e s'')) cases, match default with | None -> default - | Some (v,e) -> Some (v, apply_inv_subst e (ssink v s))) + | Some (v,e) -> Some (v, apply_inv_subst e (ssink (l, None) (ssink v s)))) | Metavar (id, s', name) -> match metavar_lookup id with | MVal e -> apply_inv_subst (push_susp e s') s

===================================== src/lexp.ml ===================================== @@ -409,11 +409,11 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, mkSusp e s')) + (l, cargs, mkSusp e (ssink (l, None) s'))) cases, match default with | None -> default - | Some (v,e) -> Some (v, mkSusp e (ssink v s))) + | Some (v,e) -> Some (v, mkSusp e (ssink (l, None) (ssink v s)))) (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp @@ -475,11 +475,12 @@ let clean e = -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, clean s' e)) + let s'' = ssink (l, None) s' in + (l, cargs, clean s'' e)) cases, match default with | None -> default - | Some (v,e) -> Some (v, clean (ssink v s) e)) + | Some (v,e) -> Some (v, clean (ssink (l, None) (ssink v s)) e)) | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s)

===================================== 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 ===================================== @@ -38,6 +38,22 @@ module S = Subst (* module L = List *) module DB = Debruijn

+type set_plexp = (lexp * lexp) list +type sort_compose_result + = SortResult of ltype + | SortInvalid + | SortK1NotType + | SortK2NotType +type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t + (* Metavars that appear in non-erasable positions. *) + * unit IMap.t + +module LMap + (* Memoization table. FIXME: Ideally the keys should be "weak", but + * I haven't found any such functionality in OCaml's libs. *) + = Hashtbl.Make + (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) + let error_tc = Log.log_error ~section:"TC" let warning_tc = Log.log_warning ~section:"TC"

@@ -132,7 +148,7 @@ let lexp_close lctx e = * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let lexp_whnf e (ctx : DB.lexp_context) : lexp = +let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = match e with | Var v -> (match lookup_value ctx v with @@ -156,30 +172,45 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> let e' = lexp_whnf e ctx in - let reduce name aargs = + let get_refl e = + let etype = get_type ctx e in (* FIXME we should not need get_type here *) + let elevel = match lexp_whnf (get_type ctx etype) ctx with + | Sort (_, Stype l) -> l + | _ -> Log.internal_error "" in + mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in + let reduce it name aargs = + let targs = match (lexp_whnf it ctx) with + | Inductive (_,_,fargs,_) -> fargs + | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in try let (_, _, branch) = SMap.find name branches in let (subst, _) = List.fold_left - (fun (s,d) (_, arg) -> - (S.cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d)) s, - d + 1)) - (S.identity, 0) + (fun (s, targs) (_, arg) -> + match targs with + | [] -> (S.cons (lexp_whnf arg ctx) s, []) + | _targ::targs -> + (* Ignore the type arguments *) + (s, targs)) + (S.identity, targs) aargs in + (* Substitute case Eq variable by the proof (Eq.refl l t e') *) + let subst = S.cons (get_refl e') subst in lexp_whnf (push_susp branch subst) ctx with Not_found -> match default with | Some (v,default) - -> lexp_whnf (push_susp default (S.substitute e')) ctx + -> let subst = S.cons (get_refl e') (S.substitute e') in + lexp_whnf (push_susp default subst) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:l ("Unhandled constructor " ^ name ^ "in case expression"); mkCase (l, e, rt, branches, default) in (match e' with - | Cons (_, (_, name)) -> reduce name [] + | Cons (it, (_, name)) -> reduce it name [] | Call (f, aargs) -> (match lexp_whnf f ctx with - | Cons (_, (_, name)) -> reduce name aargs + | Cons (it, (_, name)) -> reduce it name aargs | _ -> mkCase (l, e, rt, branches, default)) | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _) @@ -198,9 +229,8 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp =

(** A very naive implementation of sets of pairs of lexps. *) -type set_plexp = (lexp * lexp) list -let set_empty : set_plexp = [] -let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool +and set_empty : set_plexp = [] +and set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool = assert (e1 == Lexp.hc e1); assert (e2 == Lexp.hc e2); try let _ = List.find (fun (e1', e2') @@ -208,14 +238,14 @@ let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool s in true with Not_found -> false -let set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp +and set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp = (* assert (not (set_member_p s e1 e2)); *) ((e1, e2) :: s) -let set_shift_n (s : set_plexp) (n : U.db_offset) +and set_shift_n (s : set_plexp) (n : U.db_offset) = List.map (let s = S.shift n in fun (e1, e2) -> (Lexp.push_susp e1 s, Lexp.push_susp e2 s)) s -let set_shift s : set_plexp = set_shift_n s 1 +and set_shift s : set_plexp = set_shift_n s 1

(********* Testing if two types are "convertible" aka "equivalent" *********)

@@ -225,7 +255,7 @@ let set_shift s : set_plexp = set_shift_n s 1 * `c` is the maximum "constant" level that occurs in `e` * and `m` maps variable indices to the maxmimum depth at which they were * found. *) -let level_canon e = +and level_canon e = let add_var_depth v d ((c,m) as acc) = let o = try IMap.find v m with Not_found -> -1 in if o < d then (c, IMap.add v d m) else acc in @@ -244,18 +274,21 @@ let level_canon e = | _ -> (max_int, m) in canon e 0 (0,IMap.empty)

-let level_leq (c1, m1) (c2, m2) = +and level_leq (c1, m1) (c2, m2) = c1 <= c2 && c1 != max_int && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false) m1

(* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) -let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = +and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in let e2' = lexp_whnf e2 ctx in + Log.log_debug ("conv_p : e1' = `" ^ (lexp_string e1') + ^ "`; e2' = `" ^ (lexp_string e2') ^ "`"); e1' == e2' || let changed = not (e1 == e1' && e2 == e2') in + Log.log_debug ("changed : " ^ string_of_bool changed); if changed && set_member_p vs e1' e2' then true else let vs' = if changed then set_add vs e1' e2' else vs in let conv_p = conv_p' ctx vs' in @@ -319,19 +352,119 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | _,_ -> false in l1 == l2 && conv_args ctx vs' args1 args2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 - (* I'm not sure to understand how to compare two Metavar * - * Should I do a `lookup`? Or is it that simple: *) - (*| (Metavar (id1,_,_), Metavar (id2,_,_)) -> id1 = id2*) - (* FIXME: Various missing cases, such as Case. *) - | (_, _) -> false - -let conv_p (ctx : DB.lexp_context) e1 e2 + | (Case (_, te1, r1, cases1, def1), Case (_, te2, r2, cases2, def2)) + -> Log.log_debug ("conv_p of case : e1' = `" ^ (lexp_string e1') + ^ "`; e2' = `" ^ (lexp_string e2') ^ "`"); + eq e1' e2' || + (Log.log_debug "subexpr"; conv_p te1 te2) && + (Log.log_debug "return"; conv_p r1 r2) && ( + Log.log_debug "branches"; + (* Compare the branches *) + (* 1. Get the inductive for the field types *) + let call_split e = match e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + (* We can arbitrarily use te1 since te1 and te2 are convertible *) + let etype = lexp_whnf (get_type ctx te1) ctx in + let it, aargs = call_split etype in + (* 2. Build the substitution for the inductive arguments *) + let fargs, ctors = + (match lexp_whnf it ctx with + | Inductive (_, _, fargs, constructors) + -> fargs, constructors + | _ -> Log.log_fatal ("Case of non-inductive in conv_p")) in + let fargs_subst = List.fold_left2 (fun s _farg (_, aarg) -> S.cons aarg s) + S.identity fargs aargs in + (* 3. Compare the branches *) + (* The map module doesn't have a function to compare two + maps with the key (which is needed to get the field + types from the inductive. Instead, we work with the + lists of associations. *) + (try + List.for_all2 (fun (l1, (_, fields1, e1)) (l2, (_, fields2, e2)) -> + l1 = l2 && + let fieldtypes = SMap.find l1 ctors in + let rec mkctx ctx args s i vdefs1 vdefs2 fieldtypes = + match vdefs1, vdefs2, fieldtypes with + | [], [], [] -> Some (ctx, List.rev args, s) + | (ak1, vdef1)::vdefs1, (ak2, vdef2)::vdefs2, + (ak', vdef', ftype)::fieldtypes + -> if ak1 = ak2 && ak2 = ak' then + (* FIXME Should we compare the variable names ? *) + mkctx + (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s)) + ((ak1, (mkVar (vdef1, i)))::args) + (ssink vdef1 s) + (i - 1) + vdefs1 vdefs2 fieldtypes + else None + | _,_,_ -> None in + match mkctx ctx [] fargs_subst (List.length fields1) + fields1 fields2 fieldtypes with + | None -> false + | Some (nctx, args, _subst) -> + (* TODO build head lexp the eq type *) + let offset = (List.length fields1) in + let subst = S.shift offset in + Log.log_debug "hlxp time"; + let tlxp = mkSusp te1 subst in + Log.log_debug ("tlxp : `" ^ (lexp_string tlxp) ^ "`"); + let tltp = mkSusp etype subst in + Log.log_debug ("etype : `" ^ (lexp_string etype) ^ "`"); + Log.log_debug ("subst : `" ^ (subst_string subst) ^ "`"); + Log.log_debug ("tltp : `" ^ (lexp_string tltp) ^ "`"); + let tlev = (match lexp_whnf (get_type nctx tltp) nctx with + | Sort (_, Stype l) -> l + | _ -> Log.log_error "HMMM"; DB.level0) in + let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)), aargs)) subst in + Log.log_debug ("ctor : `" ^ (lexp_string ctor) ^ "`"); + let hlxp = mkCall (ctor, args) in + Log.log_debug ("hlxp : `" ^ (lexp_string hlxp) ^ "`"); + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlev); (* Typelevel *) + (Aerasable, tltp); (* Inductive type *) + (Anormal, tlxp); (* Target lexp *) + (Anormal, hlxp)]) in (* Lexp of the branch head *) + let nctx = DB.lexp_ctx_cons nctx (DB.dloc, None) Variable eqty in + conv_p' nctx (set_shift_n vs' (offset + 1)) e1 e2 + ) (SMap.bindings cases1) (SMap.bindings cases2) + with + | Invalid_argument _ -> false (* If the lists have different length *) + ) + && (match (def1, def2) with + | (Some (v1, e1), Some (v2, e2)) -> + (* FIXME should we compare the variable names ? *) + Log.log_debug "default"; + let nctx = DB.lctx_extend ctx v1 Variable etype in + let subst = S.shift 1 in + let tlxp = mkSusp e1 subst in + let tltp = mkSusp etype subst in + let tlev = (match lexp_whnf (get_type nctx tltp) nctx with + | Sort (_, Stype l) -> l + | _ -> Log.log_error "HMMM"; DB.level0) in + let hlxp = mkVar ((DB.dloc, None), 0) in + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlev); (* Typelevel *) + (Aerasable, tltp); (* Inductive type *) + (Anormal, tlxp); (* Target lexp *) + (Anormal, hlxp)]) in (* Lexp of the branch head *) + let nctx = DB.lexp_ctx_cons nctx (DB.dloc, None) Variable eqty in + conv_p' nctx (set_shift_n vs' 2) e1 e2 + | None, None -> true + | _, _ -> false)) + (* I'm not sure to understand how to compare two Metavar * + * Should I do a `lookup`? Or is it that simple: *) + (*| (Metavar (id1,_,_), Metavar (id2,_,_)) -> id1 = id2*) + (* FIXME: Various missing cases, such as Case. *) + | (_, _) -> false + +and conv_p (ctx : DB.lexp_context) e1 e2 = if e1 == e2 then true else conv_p' ctx set_empty e1 e2

(********* Testing if a lexp is properly typed *********)

-let rec mkSLlub ctx e1 e2 = +and mkSLlub ctx e1 e2 = match (lexp_whnf e1 ctx, lexp_whnf e2 ctx) with | (SortLevel SLz, _) -> e2 | (_, SortLevel SLz) -> e1 @@ -344,13 +477,7 @@ let rec mkSLlub ctx e1 e2 = else if level_leq ce2 ce1 then e1 else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *)

-type sort_compose_result - = SortResult of ltype - | SortInvalid - | SortK1NotType - | SortK2NotType - -let sort_compose ctx1 ctx2 l ak k1 k2 = +and sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen * if `v` is a TypeLevel. *) match (lexp_whnf k1 ctx1, lexp_whnf k2 ctx2) with @@ -388,11 +515,11 @@ let sort_compose ctx1 ctx2 l ak k1 k2 = | (Sort (_, _), _) -> SortK2NotType | (_, _) -> SortK1NotType

-let dbset_push ak erased = +and dbset_push ak erased = let nerased = DB.set_sink 1 erased in if ak = P.Aerasable then DB.set_set 0 nerased else nerased

-let nerased_let defs erased = +and nerased_let defs erased = (* Let bindings are not erasable, with the important exception of * let-bindings of the form `x = y` where `y` is an erasable var. * This exception is designed so that macros like `case` which need to @@ -418,7 +545,7 @@ let nerased_let defs erased = erased es

(* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -let rec check'' erased ctx e = +and check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () @@ -610,24 +737,38 @@ let rec check'' erased ctx e = SMap.iter (fun name (l, vdefs, branch) -> let fieldtypes = SMap.find name constructors in - let rec mkctx erased ctx s vdefs fieldtypes = + let rec mkctx erased ctx s hlxp vdefs fieldtypes = match vdefs, fieldtypes with - | [], [] -> (erased, ctx) + | [], [] -> (erased, ctx, hlxp) (* FIXME: If ak is Aerasable, make sure the var only * appears in type annotations. *) | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) - (S.cons (mkVar (vdef, 0)) - (S.mkShift s 1)) + (ssink vdef s) + (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _,_ -> (error_tc ~loc:l "Wrong number of args to constructor!"; - (erased, ctx)) in - let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in + (erased, ctx, hlxp)) in + let hctor = mkCall (mkCons (it, (l, name)), aargs) in + let (nerased, nctx, hlxp) = + mkctx erased ctx s hctor vdefs fieldtypes in + (* Create Eq type between target and lexp matching the + branch head, and add it (erasable) to the context *) + let subst = S.shift (List.length vdefs) in + let tlxp = mkSusp e subst in + let tltp = mkSusp etype subst in + let eqty = mkCall (DB.type_eq, + [(Aerasable, DB.type0); (* Typelevel *) (* FIXME The real typelevel *) + (Aerasable, tltp); (* Inductive type *) + (Anormal, tlxp); (* Target lexp *) + (Anormal, hlxp)]) in (* Lexp of the branch head *) + let nerased = dbset_push Aerasable nerased in (* The eq proof is erasable *) + let nctx = DB.lexp_ctx_cons nctx (l, None) Variable eqty in assert_type nctx branch (check nerased nctx branch) - (mkSusp ret (S.shift (List.length fieldtypes)))) + (mkSusp ret (S.shift ((List.length fieldtypes) + 1)))) branches; let diff = SMap.cardinal constructors - SMap.cardinal branches in (match default with @@ -635,8 +776,21 @@ let rec check'' erased ctx e = -> if diff <= 0 then warning_tc ~loc:l "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in - assert_type nctx d (check (DB.set_sink 1 erased) nctx d) - (mkSusp ret (S.shift 1)) + let nerased = DB.set_sink 1 erased in + let subst = S.shift 1 in + (* FIXME DRY this code *) + let tlxp = mkSusp e subst in + let tltp = mkSusp etype subst in + let hlxp = mkVar ((l, None), 0) in + let eqty = mkCall (DB.type_eq, + [(Aerasable, DB.type0); (* Typelevel *) (* FIXME The real typelevel *) + (Aerasable, tltp); (* Inductive type *) + (Anormal, tlxp); (* Target lexp *) + (Anormal, hlxp)]) in (* Lexp of the branch head *) + let nerased = dbset_push Aerasable nerased in (* The eq proof is erasable *) + let nctx = DB.lexp_ctx_cons nctx (l, None) Variable eqty in + assert_type nctx d (check nerased nctx d) + (mkSusp ret (S.shift 2)) | None -> if diff > 0 then error_tc ~loc:l ("Non-exhaustive match: " @@ -682,24 +836,21 @@ let rec check'' erased ctx e = check erased ctx e | MVar (_, t, _) -> push_susp t s)

-let check' ctx e = +and check' ctx e = let res = check'' DB.set_empty ctx e in (Log.stop_on_error (); res)

-let check = check' +and check ctx e = check' ctx e

(** Compute the set of free (meta)variables. **)

-let rec list_union l1 l2 = match l1 with +and list_union l1 l2 = match l1 with | [] -> l2 | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2))

-type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t - (* Metavars that appear in non-erasable positions. *) - * unit IMap.t -let mv_set_empty : mv_set = (IMap.empty, IMap.empty) -let mv_set_add (ms, nes) id x : mv_set = (IMap.add id x ms, IMap.add id () nes) -let mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set +and mv_set_empty : mv_set = (IMap.empty, IMap.empty) +and mv_set_add (ms, nes) id x : mv_set = (IMap.add id x ms, IMap.add id () nes) +and mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set = (IMap.merge (fun _m oss1 oss2 -> match (oss1, oss2) with | (None, _) -> oss2 @@ -715,23 +866,19 @@ let mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set Some ss1) ms1 ms2, IMap.merge (fun _m _o1 _o2 -> Some ()) nes1 nes2) -let mv_set_erase (ms, _nes) = (ms, IMap.empty) +and mv_set_erase (ms, _nes) = (ms, IMap.empty)

-module LMap - (* Memoization table. FIXME: Ideally the keys should be "weak", but - * I haven't found any such functionality in OCaml's libs. *) - = Hashtbl.Make - (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) -let fv_memo = LMap.create 1000 +and fv_memo = LMap.create 1000 +and fv_flush () = LMap.clear fv_memo

-let fv_empty = (DB.set_empty, mv_set_empty) -let fv_union (fv1, mv1) (fv2, mv2) +and fv_empty = (DB.set_empty, mv_set_empty) +and fv_union (fv1, mv1) (fv2, mv2) = (DB.set_union fv1 fv2, mv_set_union mv1 mv2) -let fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) -let fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) -let fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs) +and fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) +and fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) +and fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs)

-let rec fv (e : lexp) : (DB.set * mv_set) = +and fv (e : lexp) : (DB.set * mv_set) = let fv' e = match e with | Imm _ -> fv_empty | SortLevel SLz -> fv_empty @@ -784,9 +931,9 @@ let rec fv (e : lexp) : (DB.set * mv_set) = -> let s = fv_union (fv e) (fv_erase (fv t)) in let s = match def with | None -> s - | Some (_, e) -> fv_union s (fv_hoist 1 (fv e)) in + | Some (_, e) -> fv_union s (fv_hoist 2 (fv e)) in SMap.fold (fun _ (_, fields, e) s - -> fv_union s (fv_hoist (List.length fields) (fv e))) + -> fv_union s (fv_hoist (List.length fields + 1) (fv e))) cases s | Metavar (id, s, name) -> (match metavar_lookup id with @@ -806,7 +953,7 @@ let rec fv (e : lexp) : (DB.set * mv_set) = (** Finding the type of a expression. **) (* This should never signal any warning/error. *)

-let rec get_type ctx e = +and get_type ctx e = match e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int @@ -933,7 +1080,7 @@ let rec erase_type (lxp: L.lexp): E.elexp =

| L.Case(l, target, _, cases, default) -> E.Case(l, (erase_type target), (clean_map cases), - (clean_maybe default)) + (clean_default default))

| L.Susp(l, s) -> erase_type (L.push_susp l s)

@@ -962,10 +1109,12 @@ and filter_arg_list lst = and clean_decls decls = List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls

-and clean_maybe lxp = - match lxp with - | Some (v, lxp) -> Some (v, erase_type lxp) - | None -> None +and clean_default lxp = + match lxp with + | Some (v, lxp) -> + Some (v, + erase_type (L.push_susp lxp (S.substitute DB.type0))) + | None -> None

and clean_map cases = let clean_arg_list lst = @@ -979,7 +1128,8 @@ and clean_map cases = clean_arg_list lst [] in

SMap.map (fun (l, args, expr) - -> (l, (clean_arg_list args), (erase_type expr))) + -> (l, (clean_arg_list args), + erase_type (L.push_susp expr (S.substitute DB.type0)))) cases

(** Turning a set of declarations into an object. **)

===================================== 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 @@ -174,13 +176,15 @@ let rec s_offset s = match s with

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) +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 @@ -190,20 +194,26 @@ 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 (e1', e2') with - | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) - | (Var _, Var _)) + | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] - | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l - | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r - | (l, (Call _ as r)) -> unify_call r l ctx vs' - (* | (l, (Case _ as r)) -> unify_case r l subst *) - | (Arrow _ as l, r) -> unify_arrow l r ctx vs' - | (Lambda _ as l, r) -> unify_lambda l r ctx vs' - | (Call _ as l, r) -> unify_call l r ctx vs' - (* | (Case _ as l, r) -> unify_case l r subst *) - (* | (Inductive _ as l, r) -> unify_induct l r subst *) - | (Sort _ as l, r) -> unify_sort l r ctx vs' - | (SortLevel _ as l, r) -> unify_sortlvl l r ctx vs' + | (l, (Metavar (idx, s, _) as r)) -> unify_metavar c ctx idx s r l + | ((Metavar (idx, s, _) as l), r) -> unify_metavar c ctx idx s l r + | (l, (Call _ as r)) -> unify_call c r l ctx vs' + | ((Call _ as l), r) -> unify_call c l r ctx vs' + | (l, (Var _ as r)) -> unify_var r l ctx vs' + | ((Var _ as l), r) -> unify_var l r ctx vs' + | (l, (Arrow _ as r)) -> unify_arrow c r l ctx vs' + | ((Arrow _ as l), r) -> unify_arrow c l r ctx vs' + | (l, (Lambda _ as r)) -> unify_lambda c r l ctx vs' + | ((Lambda _ as l), r) -> unify_lambda c l r ctx vs' + (* | (l, (Case _ as r)) -> unify_case r l subst *) + (* | ((Case _ as l), r) -> unify_case l r subst *) + (* | (l, (Inductive _ as r)) -> unify_induct r l subst *) + (* | ((Inductive _ as l), r) -> unify_induct l r subst *) + | (l, (Sort _ as r)) -> unify_sort c r l ctx vs' + | ((Sort _ as l), r) -> unify_sort c l r ctx vs' + | (l, (SortLevel _ as r)) -> unify_sortlvl c r l ctx vs' + | ((SortLevel _ as l), r) -> unify_sortlvl c l r ctx vs' | (Inductive (_loc1, label1, args1, consts1), Inductive (_loc2, label2, args2, consts2)) -> (* print_string ("Unifying inductives " @@ -211,7 +221,7 @@ and unify' (e1: lexp) (e2: lexp) * ^ " and " * ^ snd label2 * ^ "\n"); *) - unify_inductive ctx vs' args1 args2 consts1 consts2 e1 e2 + unify_inductive c ctx vs' args1 args2 consts1 consts2 e1 e2 | _ -> (if OL.conv_p ctx e1' e2' then [] else ((* print_string "Unification failure on default\n"; *) [(CKresidual, ctx, e1, e2)])) @@ -222,87 +232,77 @@ 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 (arrow, 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 (lambda, 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 (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); - 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 + -> match checking with + | Some l when l >= sl -> [(CKassoc, ctx, lxp1, lxp2)] + | _ -> ( + associate idx lxp'; + 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 match 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 ! @@ -353,7 +353,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 @@ -364,18 +364,28 @@ 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 (var, 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 (call, 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)) -> 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) @@ -438,31 +448,29 @@ 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 sortlvl, 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)]

(** 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 sort_, 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)]

(************************ Helper function ************************************) @@ -513,7 +521,7 @@ 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) 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)]) @@ -522,7 +530,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

===================================== tests/elab_test.ml ===================================== @@ -51,8 +51,24 @@ let generate_tests (name: string) (test input_gen fmt tester)

(* let input = "y = lambda x -> x + 1;" *) -let input = "id = lambda (α : Type) ≡> lambda (x : α) -> x; -res = id 3;" +let inputs = + [("identity", {| +id = lambda (α : Type) ≡> lambda (x : α) -> x; +res = id 3; + |}); + ("whnf of case", {| +Box = (typecons (Box (l : TypeLevel) (t : Type_ l)) (box t)); +box = (datacons Box box); +unbox b = ##case_ (b | box inside => inside); +alwaysbool b = ##case_ (b | box _ => Bool); + +example1 : unbox (box (lambda x -> Bool)) 1; +example1 = true; + +example2 : alwaysbool (box Int); +example2 = true; + |}); + ]

let generate_lexp_from_str str = List.hd ((fun (lst, _) -> @@ -63,9 +79,22 @@ let generate_lexp_from_str str =

let _ = generate_tests "TYPECHECK" - (fun () -> [generate_lexp_from_str input]) - (fun x -> List.map lexp_string x) - (fun x -> (x, true)) + (fun () -> inputs) + (fun x -> x) + (fun (name, input) -> + let result = + try + let ectx = Elab.default_ectx in + let pres = Prelexer.prelex_string input in + let sxps = Lexer.lex Grammar.default_stt pres in + let _lxps, _ectx = Elab.lexp_p_decls [] sxps ectx in + Log.stop_on_error(); + true + with + | Log.Stop_Compilation _ -> (Log.print_and_clear_log (); false) + | Log.Internal_error _ -> (Log.print_and_clear_log (); false) in + (name, result) + )

let lctx = Elab.default_ectx (* let _ = (add_test "TYPECHEK_LEXP" "lexp_print" (fun () ->

===================================== tests/unify_test.ml ===================================== @@ -199,6 +199,7 @@ let test_input (lxp1: lexp) (lxp2: lexp): unif_res = else (Unification, res, lxp1, lxp2) | (CKresidual, _, _, _)::_ -> (Constraint, res, lxp1, lxp2) | (CKimpossible, _, _, _)::_ -> (Nothing, res, lxp1, lxp2) + | _ -> failwith "impossible"

let check (lxp1: lexp) (lxp2: lexp) (res: result): bool = let r, _, _, _ = test_input lxp1 lxp2

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