in base/src/main/java/org/arend/prelude/Prelude.java [98:243]
public static void update(Definition definition) {
switch (definition.getReferable().textRepresentation()) {
case "Nat" -> {
NAT = (DataDefinition) definition;
ZERO = NAT.getConstructor("zero");
SUC = NAT.getConstructor("suc");
DIV_MOD_TYPE = new SigmaExpression(Sort.SET0, parameter(true, Arrays.asList(null, null), Nat()));
}
case "Fin" -> {
FIN = (DataDefinition) definition;
FIN.setSort(Sort.SET0);
if (FIN.getConstructors().isEmpty()) {
FIN_ZERO = new Constructor(new LocatedReferableImpl(AccessModifier.PUBLIC, Precedence.DEFAULT, "zero", FIN.getRef(), GlobalReferable.Kind.CONSTRUCTOR), FIN);
DependentLink binding = new TypedDependentLink(true, "n", ExpressionFactory.Nat(), EmptyDependentLink.getInstance());
List<ExpressionPattern> patterns = Collections.singletonList(new ConstructorExpressionPattern(new ConCallExpression(SUC, Levels.EMPTY, Collections.emptyList(), Collections.emptyList()), Collections.singletonList(new BindingPattern(binding))));
FIN_ZERO.setPatterns(patterns);
FIN_ZERO.setParameters(EmptyDependentLink.getInstance());
FIN_ZERO.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
FIN_ZERO.getReferable().setTypechecked(FIN_ZERO);
FIN.addConstructor(FIN_ZERO);
FIN_SUC = new Constructor(new LocatedReferableImpl(AccessModifier.PUBLIC, Precedence.DEFAULT, "suc", FIN.getRef(), GlobalReferable.Kind.CONSTRUCTOR), FIN);
FIN_SUC.setPatterns(patterns);
FIN_SUC.setParameters(new TypedDependentLink(true, null, DataCallExpression.make(FIN, Levels.EMPTY, new SingletonList<>(new ReferenceExpression(binding))), EmptyDependentLink.getInstance()));
FIN_SUC.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
FIN_SUC.getReferable().setTypechecked(FIN_SUC);
FIN.addConstructor(FIN_SUC);
} else {
FIN_ZERO = FIN.getConstructor("zero");
FIN_SUC = FIN.getConstructor("suc");
}
}
case "+" -> PLUS = (FunctionDefinition) definition;
case "-" -> MINUS = (FunctionDefinition) definition;
case "*" -> MUL = (FunctionDefinition) definition;
case "Int" -> {
INT = (DataDefinition) definition;
POS = INT.getConstructor("pos");
NEG = INT.getConstructor("neg");
}
case "String" -> STRING = (DataDefinition) definition;
case "I" -> {
INTERVAL = (DataDefinition) definition;
INTERVAL.setSort(new Sort(new Level(0), Level.INFINITY));
LEFT = INTERVAL.getConstructor("left");
RIGHT = INTERVAL.getConstructor("right");
}
case "squeeze" -> {
SQUEEZE = (FunctionDefinition) definition;
SQUEEZE.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "squeezeR" -> {
SQUEEZE_R = (FunctionDefinition) definition;
SQUEEZE_R.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "Path" -> {
PATH = (DataDefinition) definition;
PATH.setSort(new Sort(new Level(LevelVariable.PVAR), new Level(LevelVariable.HVAR, -1)));
PATH.setCovariant(1, false);
PATH.setCovariant(2, false);
PATH_CON = PATH.getConstructor("path");
}
case "=" -> {
PATH_INFIX = (FunctionDefinition) definition;
PATH_INFIX.setResultType(new UniverseExpression(new Sort(new Level(LevelVariable.PVAR), new Level(LevelVariable.HVAR, -1))));
DataCallExpression dataCall = (DataCallExpression) PATH_INFIX.getBody();
assert dataCall != null;
PATH_INFIX.setBody(DataCallExpression.make(dataCall.getDefinition(), dataCall.getLevels(), Arrays.asList(new LamExpression(new Sort(new Level(LevelVariable.PVAR, 1), Level.INFINITY), UnusedIntervalDependentLink.INSTANCE, ((LamExpression) dataCall.getDefCallArguments().get(0)).getBody()), dataCall.getDefCallArguments().get(1), dataCall.getDefCallArguments().get(2))));
}
case "idp" -> {
IDP = (DConstructor) definition;
List<Expression> args = new ArrayList<>(2);
args.add(new ReferenceExpression(IDP.getParameters()));
args.add(new ReferenceExpression(IDP.getParameters().getNext()));
IDP.setPattern(new ConstructorExpressionPattern(FunCallExpression.makeFunCall(IDP, LevelPair.STD, args), Collections.emptyList()));
IDP.setNumberOfParameters(2);
IDP.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
PathExpression pathExpr = (PathExpression) IDP.getBody();
assert pathExpr != null;
Sort sort = new Sort(new Level(LevelVariable.PVAR), Level.INFINITY);
IDP.setBody(new PathExpression(pathExpr.getLevels(), new LamExpression(sort, UnusedIntervalDependentLink.INSTANCE, args.get(0)), new LamExpression(sort, UnusedIntervalDependentLink.INSTANCE, ((LamExpression) pathExpr.getArgument()).getBody())));
}
case "@" -> {
AT = (FunctionDefinition) definition;
AT.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "coe" -> {
COERCE = (FunctionDefinition) definition;
COERCE.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "coe2" -> {
COERCE2 = (FunctionDefinition) definition;
COERCE2.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "iso" -> {
ISO = (FunctionDefinition) definition;
ISO.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "fromNat" -> {
FIN_FROM_NAT = (FunctionDefinition) definition;
FIN_FROM_NAT.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "divMod" -> {
DIV_MOD = (FunctionDefinition) definition;
DIV_MOD.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "div" -> {
DIV = (FunctionDefinition) definition;
DIV.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "mod" -> {
MOD = (FunctionDefinition) definition;
MOD.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "divModProp" -> {
DIV_MOD_PROPERTY = (FunctionDefinition) definition;
DIV_MOD_PROPERTY.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "DArray" -> {
DEP_ARRAY = (ClassDefinition) definition;
ARRAY_ELEMENTS_TYPE = DEP_ARRAY.getPersonalFields().get(1);
ARRAY_LENGTH = DEP_ARRAY.getPersonalFields().get(0);
ARRAY_AT = DEP_ARRAY.getPersonalFields().get(2);
}
case "Array" -> {
ARRAY = (FunctionDefinition) definition;
if (ARRAY.getRef() instanceof TypedLocatedReferable) {
((TypedLocatedReferable) ARRAY.getRef()).setBodyReference(DEP_ARRAY.getRef());
}
}
case "nil" -> {
EMPTY_ARRAY = (DConstructor) definition;
EMPTY_ARRAY.setPattern(new ConstructorExpressionPattern(FunCallExpression.makeFunCall(EMPTY_ARRAY, LevelPair.STD, Collections.emptyList()), Collections.singletonList(new BindingPattern(EMPTY_ARRAY.getParameters()))));
EMPTY_ARRAY.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "::" -> {
ARRAY_CONS = (DConstructor) definition;
ARRAY_CONS.setPattern(new ConstructorExpressionPattern(FunCallExpression.makeFunCall(ARRAY_CONS, LevelPair.STD, Collections.emptyList()), Arrays.asList(new BindingPattern(ARRAY_CONS.getParameters()), new BindingPattern(ARRAY_CONS.getParameters().getNext()), new BindingPattern(ARRAY_CONS.getParameters().getNext().getNext()), new BindingPattern(ARRAY_CONS.getParameters().getNext().getNext().getNext()))));
ARRAY_CONS.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
case "!!" -> {
ARRAY_INDEX = (FunctionDefinition) definition;
ARRAY_INDEX.setBody(null);
}
default -> throw new IllegalStateException();
}
}