[Typer] [Git][monnier/typer][ja-barszcz] 26 commits: Apply the instantiated metavariable substs when displaying lexps

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

Commits: ac4cc3a5 by Jean-Alexandre Barszcz at 2020-08-20T15:01:14-04:00 Apply the instantiated metavariable substs when displaying lexps

- - - - - f0b33b28 by Jean-Alexandre Barszcz at 2020-08-20T15:01:36-04:00 Replace instantiated metavars when checking syntactic equality

- - - - - dc78ba24 by Jean-Alexandre Barszcz at 2020-08-21T18:04:30-04:00 Test WHNF of case

- - - - - 28fd1c84 by Jean-Alexandre Barszcz at 2020-08-21T18:04:56-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.

- - - - - ae72b840 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] Make unification symmetric

- - - - - 2d50e3b8 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] Handle variables earlier during unification

- - - - - 490090a5 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] experiments with Decidable and proofs

- - - - - 85ed613c by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] unify instead of conv_p in sform_lambda

- - - - - 81b757c3 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] proof of Decidable (a < b)

- - - - - e357e46a by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] First draft of an instance search algorithm

- - - - - 033b3837 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 WIP WIP WIP

- - - - - f19d4d84 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 WIP WIP getting there

- - - - - f394fb30 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] Add a set of typeclasses to the elab context

- - - - - 2ef581db by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] Add a syntax for records

- - - - - d0ec2a80 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] Extend the Decidable sample with conjunction (dep on records)

- - - - - 33d9c63c by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 Resolve instances in the REPL (since exprs. are not generalized)

- - - - - d0678ad7 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 Resolve instances for recursive definitions

- - - - - b54e3e6a by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-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.

- - - - - 86624799 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 Num class example

- - - - - 27b776e3 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 Num class (with records)

- - - - - ec0bb7e6 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 Allow non-inductives to be typeclasses (Eq for instance)

- - - - - 016b580a by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 Move the Eq builtin to debruijn.ml to make it available for elab.

- - - - - 56b2ecb8 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-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.

- - - - - 9e5aa5d1 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] Add Eq to case

- - - - - 7e8b3db1 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 [WIP] Adding Eq to Case: mutual rec for (whnf & get_type) + conv_p of case?

- - - - - 333bc9e9 by Jean-Alexandre Barszcz at 2020-08-21T18:05:32-04:00 Algebra classes sample with proof of associativity of +

- - - - -

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,84 @@ +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);

===================================== 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) @@ -805,7 +806,7 @@ and lexp_str ctx (exp : lexp) : string = | Metavar (idx, subst, (loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with - | MVal e -> lexp_str ctx e + | MVal e -> lexp_str ctx (push_susp e subst) | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx))

| Let (_, decls, body) -> @@ -993,7 +994,19 @@ let rec eq e1 e2 = | (Some (_, e1), Some (_, e2)) -> eq e1 e2 | _ -> def1 = def2) | (Metavar (i1, s1, _), Metavar (i2, s2, _)) - -> i1 = i2 && subst_eq s1 s2 + -> if i1 == i2 then subst_eq s1 s2 else + (match (metavar_lookup i1, metavar_lookup i2) with + | (MVal l, _) -> eq (push_susp l s1) e2 + | (_, MVal l) -> eq e1 (push_susp l s2) + | _ -> false) + | (Metavar (i1, s1, _), _) + -> (match metavar_lookup i1 with + | MVal l -> eq (push_susp l s1) e2 + | _ -> false) + | (_, Metavar (i2, s2, _)) + -> (match metavar_lookup i2 with + | MVal l -> eq e1 (push_susp l s2) + | _ -> false) | _ -> false

and subst_eq s1 s2 =

===================================== 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,21 +172,28 @@ 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 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 name aargs = try let (_, _, branch) = SMap.find name branches in - let (subst, _) + 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) (_, arg) -> S.cons (lexp_whnf arg ctx) s) + S.identity 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"); @@ -198,9 +221,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 +230,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 +247,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 +266,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 +344,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 +469,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 +507,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 +537,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 +729,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 +768,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 +828,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 +858,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 +923,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 +945,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 +1072,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 +1101,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 +1120,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,21 @@ 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); + +%% unbox twice to compute something in a branch +example : unbox (unbox (box (box Bool))); +example = true; + |}); + ]

let generate_lexp_from_str str = List.hd ((fun (lst, _) -> @@ -63,9 +76,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/e68491a11f17e63d891831b8c6cbe037a...