Skip to content

Commit

Permalink
merge: data -> inductive (#1070)
Browse files Browse the repository at this point in the history 
Fix #1069
  • Loading branch information
@ice1000
ice1000 authored May 31, 2024
2 parents 49d5e4a + 0989da4 commit 2015fd5
Show file tree
Hide file tree
Showing 39 changed files with 238 additions and 404 deletions.
4 changes: 2 additions & 2 deletions base/src/main/java/org/aya/resolve/ResolvingStmt.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,12 @@
* postulate
* Context : Set
*
* data Stmt : Set where
* inductive Stmt : Set where
* FnDecl : Stmt
* DataDecl : Stmt
* DataCon : Stmt
*
* data ExtInfo : Stmt -> Set where
* inductive ExtInfo : Stmt -> Set where
* ExtData : Context -> ExtInfo DataDecl
* ExtFn : Context -> ExtInfo FnDecl
* -- trivial extra info
Expand Down
28 changes: 14 additions & 14 deletions base/src/test/java/org/aya/tyck/PatternTyckTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
public class PatternTyckTest {
@Test public void elim0() {
var result = tyck("""
open data Nat | O | S Nat
open inductive Nat | O | S Nat
def lind (a b : Nat) : Nat elim a
| 0 => b
| S a' => S (lind a' b)
Expand All @@ -28,8 +28,8 @@ def lind (a b : Nat) : Nat elim a

@Test public void test1() {
var result = tyck("""
open data Nat | O | S Nat
open data Vec Nat Type
open inductive Nat | O | S Nat
open inductive Vec Nat Type
| 0, A => vnil
| S n, A => infixr vcons A (Vec n A)
Expand All @@ -52,7 +52,7 @@ def unwrap (A : Type) (v : Vec 1 A) : A elim v

@Test public void test2() {
var result = tyck("""
open data Nat | O | S Nat
open inductive Nat | O | S Nat
prim I : ISet
prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
Expand All @@ -79,7 +79,7 @@ def pmap (f : A -> B) {a b : A} (p : a = b) : f a = f b => \\i => f (p i)

@Test public void test3() {
var result = tyck("""
open data Nat | O | S Nat
open inductive Nat | O | S Nat
prim I : ISet
prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
Expand All @@ -94,7 +94,7 @@ prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
| a, S b => S (a +' b)
tighter =
open data Int
open inductive Int
| pos Nat | neg Nat
| zro : pos 0 = neg 0
Expand All @@ -114,8 +114,8 @@ prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type

@Test public void test4() {
assertTrue(tyck("""
open data Nat | O | S Nat
open data Fin Nat
open inductive Nat | O | S Nat
open inductive Fin Nat
| 1 => fzero
| S n => fsucc (Fin n)
Expand All @@ -125,8 +125,8 @@ def exfalso (A : Type) (x : Fin 0) : A elim x | ()

@Test public void issue630() {
assertTrue(tyck("""
open data Nat | O | S Nat
open data INat (n : Nat)
open inductive Nat | O | S Nat
open inductive INat (n : Nat)
| O => zero
| S n' => +-one
| S (S n') => +-two
Expand All @@ -140,12 +140,12 @@ open data INat (n : Nat)
@Test
public void test5() {
@Language("Aya") var code = """
open data Nat | O | S Nat
open data Vec Type Nat
open inductive Nat | O | S Nat
open inductive Vec Type Nat
| A, O => vnil
| A, S n => vcons A (Vec A n)
open data MatchMe (n : Nat) (Vec Nat n)
open inductive MatchMe (n : Nat) (Vec Nat n)
| S n', vcons v xs => matched
def checkMe {n : Nat} (m : Nat) {v : Vec Nat n} (MatchMe n v) : Nat
Expand Down
144 changes: 15 additions & 129 deletions base/src/test/java/org/aya/tyck/TyckTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,37 +3,21 @@
package org.aya.tyck;

import kala.collection.immutable.ImmutableSeq;
import kala.collection.immutable.primitive.ImmutableIntSeq;
import org.aya.normalize.Normalizer;
import org.aya.primitive.PrimFactory;
import org.aya.resolve.ResolveInfo;
import org.aya.resolve.module.ModuleCallback;
import org.aya.syntax.SyntaxTestUtil;
import org.aya.syntax.core.Closure;
import org.aya.syntax.core.def.*;
import org.aya.syntax.core.term.LamTerm;
import org.aya.syntax.core.term.Term;
import org.aya.syntax.core.term.call.DataCall;
import org.aya.syntax.core.term.call.FnCall;
import org.aya.syntax.core.term.repr.IntegerTerm;
import org.aya.syntax.core.term.repr.ListTerm;
import org.aya.syntax.literate.CodeOptions;
import org.aya.syntax.core.def.TyckDef;
import org.intellij.lang.annotations.Language;
import org.jetbrains.annotations.NotNull;
import org.junit.jupiter.api.Test;

import java.util.Random;
import java.util.function.Function;
import java.util.function.IntFunction;

import static org.junit.jupiter.api.Assertions.assertNotNull;
import static org.junit.jupiter.api.Assertions.assertTrue;

public class TyckTest {
@Test public void test0() {
var result = tyck("""
data Nat | O | S Nat
data FreeMonoid (A : Type) | e | cons A (FreeMonoid A)
inductive Nat | O | S Nat
inductive FreeMonoid (A : Type) | e | cons A (FreeMonoid A)
def id {A : Type} (a : A) => a
def lam (A : Type) : Fn (a : A) -> Type => fn a => A
Expand All @@ -47,7 +31,7 @@ def letExample (A : Type) (B : A -> Type) (f : Fn (a : A) -> B a) (a : A) : B a

@Test public void test1() {
var result = tyck("""
open data Unit | unit
open inductive Unit | unit
variable A : Type
def foo {value : A} : A => value
def what : Unit => foo {value := unit}
Expand All @@ -57,7 +41,7 @@ def letExample (A : Type) (B : A -> Type) (f : Fn (a : A) -> B a) (a : A) : B a

@Test public void path0() {
var result = tyck("""
data Nat
inductive Nat
| O : Nat
| S (x : Nat) : Nat
prim I : ISet
Expand All @@ -73,14 +57,14 @@ def coeFill0 (A : I -> Type) (u : A 0) : Path A u (transp A u) => \\i => coe 0 i

@Test public void path1() {
var result = tyck("""
data Nat | O | S Nat
inductive Nat | O | S Nat
prim I : ISet
prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
prim coe
variable A : Type
def infix = (a b : A) => Path (\\i => A) a b
def refl {a : A} : a = a => \\i => a
open data Int
open inductive Int
| pos Nat | neg Nat
| zro : pos 0 = neg 0
example def testZro0 : zro 0 = pos 0 => refl
Expand All @@ -96,9 +80,9 @@ def funExt (A B : Type) (f g : A -> B) (p : Fn (a : A) -> f a = g a) : f = g =>
/*@Test*/
public void issue768() {
var result = tyck("""
open data Unit | unit
data Nat | O | S Nat
open data SomeDT Nat
open inductive Unit | unit
inductive Nat | O | S Nat
open inductive SomeDT Nat
| m => someDT
def how' {m : Nat} (a : Nat) (b : SomeDT m) : Nat => 0
def what {A : Nat -> Type} (B : Fn (n : Nat) -> A n -> Nat) : Unit => unit
Expand All @@ -109,8 +93,8 @@ public void issue768() {

@Test public void test2() {
var result = tyck("""
open data Nat | O | S Nat
open data Bool | true | false
open inductive Nat | O | S Nat
open inductive Bool | true | false
def not Bool : Bool | true => false | false => true
def even Nat : Bool
| 0 => true
Expand All @@ -124,113 +108,15 @@ public void issue768() {

@Test public void test3() {
assertTrue(tyck("""
open data Nat | O | S Nat
open data Natt | OO | SS Nat
open inductive Nat | O | S Nat
open inductive Natt | OO | SS Nat
def infix = {A : Type} (a b : A) => Type
// Disambiguate by type checking
def test (a : Nat) => a = 114514
""").defs.isNotEmpty());
}

@Test
public void sort() {
var result = tyck("""
open data Nat | O | S Nat
open data Bool | True | False
open data List Type
| nil
| A => infixr cons A (List A)
open data Color | red | black
def Decider (A : Type) => Fn (x y : A) -> Bool
variable A : Type
open data RBTree (A : Type) : Type
| rbLeaf
| rbNode Color (RBTree A) A (RBTree A)
def rbTreeToList (rb : RBTree A) (r : List A) : List A elim rb
| rbLeaf => r
| rbNode x t1 a t2 => rbTreeToList t1 (a cons rbTreeToList t2 r)
def repaint (RBTree A) : RBTree A
| rbNode c l a r => rbNode black l a r
| rbLeaf => rbLeaf
def le (x y : Nat) : Bool
| O, _ => True
| S _, O => False
| S a, S b => le a b
def balanceLeft Color (RBTree A) A (RBTree A) : RBTree A
| black, rbNode red (rbNode red a x b) y c, v, r =>
rbNode red (rbNode black a x b) y (rbNode black c v r)
| black, rbNode red a x (rbNode red b y c), v, r =>
rbNode red (rbNode black a x b) y (rbNode black c v r)
| c, a, v, r => rbNode c a v r
def balanceRight Color (RBTree A) A (RBTree A) : RBTree A
| black, l, v, rbNode red (rbNode red b y c) z d =>
rbNode red (rbNode black l v b) y (rbNode black c z d)
| black, l, v, rbNode red b y (rbNode red c z d) =>
rbNode red (rbNode black l v b) y (rbNode black c z d)
| c, l, v, b => rbNode c l v b
def insert_lemma (dec_le : Decider A) (a a1 : A) (c : Color) (l1 l2 : RBTree A) (b : Bool) : RBTree A elim b
| True => balanceRight c l1 a1 (insert a l2 dec_le)
| False => balanceLeft c (insert a l1 dec_le) a1 l2
def insert (a : A) (node : RBTree A) (dec_le : Decider A) : RBTree A elim node
| rbLeaf => rbNode red rbLeaf a rbLeaf
| rbNode c l1 a1 l2 => insert_lemma dec_le a a1 c l1 l2 (dec_le a1 a)
private def aux (l : List A) (r : RBTree A) (dec_le : Decider A) : RBTree A elim l
| nil => r
| a cons l => aux l (repaint (insert a r dec_le)) dec_le
def tree_sort (dec_le : Decider A) (l : List A) => rbTreeToList (aux l rbLeaf dec_le) nil
""");

var defs = result.defs;

var Nat = (DataDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("Nat")).get());
var O = (ConDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("O")).get());
var S = (ConDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("S")).get());
var List = (DataDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("List")).get());
var nil = (ConDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("nil")).get());
var cons = (ConDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("cons")).get());
var le = (FnDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("le")).get());
var tree_sort = (FnDefLike) TyckAnyDef.make(defs.find(x -> x.ref().name().equals("tree_sort")).get());

var NatCall = new DataCall(Nat, 0, ImmutableSeq.empty());
var ListNatCall = new DataCall(List, 0, ImmutableSeq.of(NatCall));

IntFunction<Term> mkInt = i -> new IntegerTerm(i, O, S, NatCall);

Function<ImmutableIntSeq, Term> mkList = xs -> new ListTerm(xs.mapToObj(mkInt::apply), nil, cons, ListNatCall);

var leCall = new LamTerm(new Closure.Jit(x ->
new LamTerm(new Closure.Jit(y ->
new FnCall(le, 0, ImmutableSeq.of(x, y))))));

var seed = 114514L;
var random = new Random(seed);
var largeList = mkList.apply(ImmutableIntSeq.fill(50, () -> Math.abs(random.nextInt()) % 100));
var args = ImmutableSeq.of(NatCall, leCall, largeList);

var beginTime = System.currentTimeMillis();
var sortResult = new Normalizer(new TyckState(result.info().shapeFactory(), new PrimFactory()))
.normalize(new FnCall(tree_sort, 0, args), CodeOptions.NormalizeMode.FULL);
var endTime = System.currentTimeMillis();
assertNotNull(sortResult);

System.out.println(STR."Done in \{(endTime - beginTime)}");
System.out.println(sortResult.debuggerOnlyToString());
}

public record TyckResult(@NotNull ImmutableSeq<TyckDef> defs, @NotNull ResolveInfo info) {

}
public record TyckResult(@NotNull ImmutableSeq<TyckDef> defs, @NotNull ResolveInfo info) { }

public static TyckResult tyck(@Language("Aya") @NotNull String code) {
var moduleLoader = SyntaxTestUtil.moduleLoader();
Expand Down
8 changes: 4 additions & 4 deletions cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,12 +38,12 @@ public class ReplCompilerTest {

@Test public void issue382() {
// success cases, we can find the definition in the context
compile("data Nat | zero | suc Nat");
compile("inductive Nat | zero | suc Nat");
var nat = findContext("Nat");
assertNotNull(nat);

// failure cases, the context is unchanged
assertThrows(Throwable.class, () -> compile("data Nat ="));
assertThrows(Throwable.class, () -> compile("inductive Nat ="));
var newNat = findContext("Nat");
assertEquals(nat, newNat);

Expand All @@ -54,9 +54,9 @@ public class ReplCompilerTest {
/** <a href="https://ice1000.jetbrains.space/im/group/4DLh053zIix6?message=2db0002db&channel=4DLh053zIix6">Bug report</a> */
@Test public void reportedInSpace() {
// success cases, we can find the definition in the context
compile("data Unit | unit");
compile("inductive Unit | unit");
assertNotNull(findContext("Unit"));
compile("data What | what");
compile("inductive What | what");
assertNotNull(findContext("What"));
assertNotNull(findContext("Unit"));
}
Expand Down
10 changes: 5 additions & 5 deletions cli-impl/src/test/java/org/aya/test/fixtures/ExprTyckError.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,14 +34,14 @@ prim Path (A : I -> Type) (a b : A)
""";

@Language("Aya") String testPiDom = """
data X : Set
data Test : Type | con X
inductive X : Set
inductive Test : Type | con X
""";

@Language("Aya") String testPiDomMeta = """
data X : Set
data infix = (a b : X) : Type
data Test : Type
inductive X : Set
inductive infix = (a b : X) : Type
inductive Test : Type
| con (x : _) (y : X) (x = y)
""";
}
Loading

0 comments on commit 2015fd5

Please sign in to comment.