Skip to content

Commit

Permalink
merge: #1002
Browse files Browse the repository at this point in the history
1002: Shape matcher code review r=ice1000 a=ice1000

xsajxnsakjnxsajkxnjksaxnjksanxjsknxakjs

Co-authored-by: HoshinoTented <hoshinotented@qq.com>
Co-authored-by: ice1000 <ice1000kotlin@foxmail.com>
Co-authored-by: imkiva <imkiva@islovely.icu>
  • Loading branch information
4 people authored Oct 20, 2023
2 parents c5be01e + 7d5ed05 commit f2bbdc4
Show file tree
Hide file tree
Showing 14 changed files with 614 additions and 248 deletions.
103 changes: 90 additions & 13 deletions base/src/main/java/org/aya/core/repr/AyaShape.java
Original file line number Diff line number Diff line change
Expand Up @@ -5,15 +5,21 @@
import kala.collection.immutable.ImmutableSeq;
import kala.collection.mutable.MutableLinkedHashMap;
import kala.collection.mutable.MutableMap;
import kala.control.Either;
import kala.control.Option;
import kala.tuple.Tuple;
import kala.tuple.Tuple2;
import org.aya.core.def.Def;
import org.aya.core.def.GenericDef;
import org.aya.util.Arg;
import org.jetbrains.annotations.NotNull;

import static org.aya.core.repr.CodeShape.CtorShape;
import static org.aya.core.repr.CodeShape.DataShape;
import static org.aya.core.repr.CodeShape.*;
import static org.aya.core.repr.CodeShape.GlobalId.*;
import static org.aya.core.repr.CodeShape.LocalId.LHS;
import static org.aya.core.repr.CodeShape.LocalId.RHS;
import static org.aya.core.repr.ParamShape.anyLicit;
import static org.aya.core.repr.ParamShape.explicit;

/**
* @author kiva
Expand All @@ -23,14 +29,18 @@ public sealed interface AyaShape {

@NotNull AyaShape NAT_SHAPE = AyaIntShape.INSTANCE;
@NotNull AyaShape LIST_SHAPE = AyaListShape.INSTANCE;
@NotNull ImmutableSeq<AyaShape> LITERAL_SHAPES = ImmutableSeq.of(NAT_SHAPE, LIST_SHAPE);
@NotNull AyaShape PLUS_LEFT_SHAPE = AyaPlusFnLeftShape.INSTANCE;
@NotNull AyaShape PLUS_RIGHT_SHAPE = AyaPlusFnShape.INSTANCE;
@NotNull ImmutableSeq<AyaShape> LITERAL_SHAPES = ImmutableSeq.of(NAT_SHAPE, LIST_SHAPE, PLUS_RIGHT_SHAPE);

enum AyaIntShape implements AyaShape {
INSTANCE;

public static final @NotNull CodeShape DATA_NAT = new DataShape(ImmutableSeq.empty(), ImmutableSeq.of(
new CtorShape(CodeShape.MomentId.ZERO, ImmutableSeq.empty()),
new CtorShape(CodeShape.MomentId.SUC, ImmutableSeq.of(CodeShape.ParamShape.explicit(CodeShape.TermShape.Call.justCall(0))))
public static final @NotNull CodeShape DATA_NAT = new DataShape(
NAT,
ImmutableSeq.empty(), ImmutableSeq.of(
new CtorShape(ZERO, ImmutableSeq.empty()),
new CtorShape(SUC, ImmutableSeq.of(ParamShape.explicit(TermShape.NameCall.of(NAT))))
));

@Override public @NotNull CodeShape codeShape() {
Expand All @@ -41,21 +51,88 @@ enum AyaIntShape implements AyaShape {
enum AyaListShape implements AyaShape {
INSTANCE;

public static final @NotNull LocalId A = new LocalId("A");

public static final @NotNull CodeShape DATA_LIST = new DataShape(
ImmutableSeq.of(CodeShape.ParamShape.anyLicit(new CodeShape.TermShape.Sort(null, 0))),
LIST,
ImmutableSeq.of(explicit(A, new TermShape.Sort(null, 0))),
ImmutableSeq.of(
new CtorShape(CodeShape.MomentId.NIL, ImmutableSeq.empty()),
new CtorShape(CodeShape.MomentId.CONS, ImmutableSeq.of(
CodeShape.ParamShape.anyLicit(new CodeShape.TermShape.TeleRef(0, 0)), // A
CodeShape.ParamShape.anyLicit(new CodeShape.TermShape.Call(0, ImmutableSeq.of( // List A
new CodeShape.TermShape.TeleRef(0, 0))))))
new CtorShape(GlobalId.NIL, ImmutableSeq.empty()),
new CtorShape(GlobalId.CONS, ImmutableSeq.of(
explicit(TermShape.NameCall.of(A)),
explicit(new TermShape.NameCall(LIST, ImmutableSeq.of(new Arg<>(TermShape.NameCall.of(A), true))))
)) // List A
));

@Override public @NotNull CodeShape codeShape() {
return DATA_LIST;
}
}

enum AyaPlusFnShape implements AyaShape {
INSTANCE;

public static final @NotNull CodeShape FN_PLUS = new FnShape(
NAT_ADD,
// _ : Nat -> Nat -> Nat
ImmutableSeq.of(
explicit(new TermShape.ShapeCall(NAT, AyaIntShape.DATA_NAT, ImmutableSeq.empty())),
explicit(TermShape.NameCall.of(NAT))
),
TermShape.NameCall.of(NAT),
Either.right(ImmutableSeq.of(
// | a, 0 => a
new ClauseShape(ImmutableSeq.of(
new PatShape.Bind(LHS), PatShape.ShapedCtor.of(NAT, ZERO)
), TermShape.NameCall.of(LHS)),
// | a, suc b => suc (_ a b)
new ClauseShape(ImmutableSeq.of(
new PatShape.Bind(LHS), new PatShape.ShapedCtor(NAT, SUC, ImmutableSeq.of(new PatShape.Bind(RHS)))
), new TermShape.CtorCall(NAT, SUC, ImmutableSeq.of(new Arg<>(new TermShape.NameCall(NAT_ADD, ImmutableSeq.of(
new Arg<>(TermShape.NameCall.of(LHS), true), // TODO: licit
new Arg<>(TermShape.NameCall.of(RHS), true)
)), true))))
))
);

@Override
public @NotNull CodeShape codeShape() {
return FN_PLUS;
}
}

enum AyaPlusFnLeftShape implements AyaShape {
INSTANCE;

public static final @NotNull CodeShape FN_PLUS = new FnShape(
NAT_ADD,
// _ : Nat -> Nat -> Nat
ImmutableSeq.of(
explicit(new TermShape.ShapeCall(GlobalId.NAT, AyaIntShape.DATA_NAT, ImmutableSeq.empty())),
explicit(TermShape.NameCall.of(NAT))
),
TermShape.NameCall.of(NAT),
Either.right(ImmutableSeq.of(
// | 0, b => b
new ClauseShape(ImmutableSeq.of(
PatShape.ShapedCtor.of(NAT, ZERO), new PatShape.Bind(RHS)
), TermShape.NameCall.of(RHS)),
// | suc a, b => _ a (suc b)
new ClauseShape(ImmutableSeq.of(
new PatShape.ShapedCtor(NAT, SUC, ImmutableSeq.of(new PatShape.Bind(LHS))), new PatShape.Bind(RHS)
), new TermShape.CtorCall(NAT, SUC, ImmutableSeq.of(new Arg<>(new TermShape.NameCall(NAT_ADD, ImmutableSeq.of(
new Arg<>(TermShape.NameCall.of(LHS), true),
new Arg<>(TermShape.NameCall.of(RHS), true)
)), true))))
))
);

@Override
public @NotNull CodeShape codeShape() {
return FN_PLUS;
}
}

class Factory {
public @NotNull MutableMap<GenericDef, ShapeRecognition> discovered = MutableLinkedHashMap.of();

Expand All @@ -77,7 +154,7 @@ public void bonjour(@NotNull GenericDef def, @NotNull ShapeRecognition shape) {
/** Discovery of shaped literals */
public void bonjour(@NotNull GenericDef def) {
AyaShape.LITERAL_SHAPES.view()
.flatMap(shape -> ShapeMatcher.match(shape, def))
.flatMap(shape -> new ShapeMatcher().match(shape, def))
.forEach(shape -> bonjour(def, shape));
}

Expand Down
123 changes: 25 additions & 98 deletions base/src/main/java/org/aya/core/repr/CodeShape.java
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,8 @@
package org.aya.core.repr;

import kala.collection.immutable.ImmutableSeq;
import org.aya.core.term.DataCall;
import org.aya.core.term.Term;
import org.aya.generic.SortKind;
import org.jetbrains.annotations.Contract;
import kala.control.Either;
import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;

import java.io.Serializable;

Expand All @@ -17,113 +13,44 @@
*/
public sealed interface CodeShape {
/** A capture group, see {@link CodeShape.CtorShape} and {@link ShapeMatcher#captures()} */
sealed interface Moment {
sealed interface Moment permits CtorShape, DataShape, FnShape, ParamShape.Licit, PatShape.Bind, TermShape.ShapeCall {
@NotNull MomentId name();
}

/** Typed capture name, rather than plain strings */
enum MomentId implements Serializable {
sealed interface MomentId {
}

enum GlobalId implements MomentId, Serializable {
ZERO, SUC, NIL, CONS,
NAT, LIST,
NAT_ADD,
}

record LocalId(@NotNull String name) implements MomentId {
public static final @NotNull LocalId IGNORED = new LocalId("_");
public static final @NotNull LocalId LHS = new LocalId("lhs");
public static final @NotNull LocalId RHS = new LocalId("rhs");
}

record FnShape(
@NotNull ImmutableSeq<ParamShape> tele
) implements CodeShape {}
@NotNull MomentId name,
@NotNull ImmutableSeq<ParamShape> tele,
@NotNull TermShape result,
@NotNull Either<TermShape, ImmutableSeq<ClauseShape>> body
) implements CodeShape, Moment {}

record ClauseShape(@NotNull ImmutableSeq<PatShape> pats, @NotNull TermShape body) implements CodeShape {
}

record DataShape(
@NotNull MomentId name,
@NotNull ImmutableSeq<ParamShape> tele,
@NotNull ImmutableSeq<CtorShape> ctors
) implements CodeShape {}

record StructShape(
@NotNull ImmutableSeq<ParamShape> tele,
@NotNull ImmutableSeq<FieldShape> fields
) implements CodeShape {}
) implements CodeShape, Moment {}

record CtorShape(
@NotNull MomentId name,
@NotNull GlobalId name,
@NotNull ImmutableSeq<ParamShape> tele
) implements CodeShape, Moment {}

record FieldShape(
@NotNull ImmutableSeq<ParamShape> tele
) implements CodeShape {}

/**
* @author kiva
*/
sealed interface TermShape {
enum Any implements TermShape {
INSTANCE;
}

/**
* @param superLevel the data def reference
* @param args corresponds to {@link DataCall#args()}
*/
record Call(int superLevel, @NotNull ImmutableSeq<TermShape> args) implements TermShape {
@Contract("_ -> new") public static @NotNull Call justCall(int superLevel) {
return new Call(superLevel, ImmutableSeq.empty());
}
}

record TeleRef(int superLevel, int nth) implements TermShape {}

/**
* The shape to Sort term, I am not very work well at type theory, so improve this feel free!
*
* @param kind the SortKind, null if accept any kind of sort. see {@link ShapeMatcher#matchTerm(TermShape, Term)}
* @param ulift the lower bound of the type level.
* @author hoshino
*/
record Sort(@Nullable SortKind kind, int ulift) implements TermShape {}
}

/**
* @author kiva
*/
sealed interface PatShape {
enum Any implements PatShape {
INSTANCE;
}
}

/**
* @author kiva
*/
sealed interface ParamShape {
enum Any implements ParamShape {
INSTANCE;
}

record Licit(@NotNull CodeShape.TermShape type, Kind kind) implements ParamShape {
enum Kind {
Any, Ex, Im
}
}

record Optional(@NotNull CodeShape.ParamShape param) implements ParamShape {}

static @NotNull CodeShape.ParamShape explicit(@NotNull CodeShape.TermShape type) {
return new Licit(type, Licit.Kind.Ex);
}

static @NotNull CodeShape.ParamShape implicit(@NotNull CodeShape.TermShape type) {
return new Licit(type, Licit.Kind.Im);
}

static @NotNull CodeShape.ParamShape anyLicit(@NotNull CodeShape.TermShape type) {
return new Licit(type, Licit.Kind.Any);
}

static @NotNull CodeShape.ParamShape anyEx() {
return explicit(TermShape.Any.INSTANCE);
}

static @NotNull CodeShape.ParamShape anyIm() {
return implicit(TermShape.Any.INSTANCE);
}

// anyLicit(TermShape.Any) would be equivalent to ParamShape.Any
}
}
54 changes: 54 additions & 0 deletions base/src/main/java/org/aya/core/repr/ParamShape.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
package org.aya.core.repr;

import org.jetbrains.annotations.NotNull;

/**
* @author kiva
*/
sealed public interface ParamShape {
enum Any implements ParamShape {
INSTANCE;
}

record Licit(
@NotNull CodeShape.MomentId name,
@NotNull TermShape type,
Licit.Kind kind
) implements ParamShape, CodeShape.Moment {
enum Kind {
Any, Ex, Im
}
}

static @NotNull ParamShape explicit(@NotNull TermShape type) {
return explicit(CodeShape.LocalId.IGNORED, type);
}

static @NotNull ParamShape explicit(@NotNull CodeShape.LocalId name, @NotNull TermShape type) {
return new Licit(name, type, Licit.Kind.Ex);
}

static @NotNull ParamShape implicit(@NotNull TermShape type) {
return new Licit(CodeShape.LocalId.IGNORED, type, Licit.Kind.Im);
}

static @NotNull ParamShape anyLicit(@NotNull CodeShape.MomentId name, @NotNull TermShape type) {
return new Licit(name, type, Licit.Kind.Any);
}

static @NotNull ParamShape anyLicit(@NotNull TermShape type) {
return anyLicit(CodeShape.LocalId.IGNORED, type);
}

static @NotNull ParamShape anyEx() {
return explicit(TermShape.Any.INSTANCE);
}

static @NotNull ParamShape anyIm() {
return implicit(TermShape.Any.INSTANCE);
}

// anyLicit(TermShape.Any) would be equivalent to ParamShape.Any
}
40 changes: 40 additions & 0 deletions base/src/main/java/org/aya/core/repr/PatShape.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
package org.aya.core.repr;

import kala.collection.immutable.ImmutableSeq;
import org.jetbrains.annotations.NotNull;

// TODO[h]: Licit, we can use generalized ParamShape

/**
* @author kiva
*/
public sealed interface PatShape {
enum Any implements PatShape {
INSTANCE;
}

record Bind(@NotNull CodeShape.MomentId name) implements PatShape, CodeShape.Moment {
}

sealed interface CtorLike extends PatShape permits Ctor, ShapedCtor {
@NotNull ImmutableSeq<PatShape> innerPats();
}

record Ctor(@NotNull ImmutableSeq<PatShape> innerPats) implements CtorLike {
}

/**
* Expecting a certain ctor, {@link ShapeMatcher} will crash if the {@param name} is invalid (such as undefined or not a DataShape)
*
* @param dataId a reference to a {@link CodeShape.DataShape}d term
* @param ctorId the {@link CodeShape.MomentId} to the ctor
*/
record ShapedCtor(@NotNull CodeShape.MomentId dataId, @NotNull CodeShape.GlobalId ctorId,
@NotNull ImmutableSeq<PatShape> innerPats) implements CtorLike {
public static @NotNull ShapedCtor of(@NotNull CodeShape.MomentId name, @NotNull CodeShape.GlobalId id) {
return new ShapedCtor(name, id, ImmutableSeq.empty());
}
}
}
Loading

0 comments on commit f2bbdc4

Please sign in to comment.