Skip to content

Commit

Permalink
Fix a bug with ext meta
Browse files Browse the repository at this point in the history
  • Loading branch information
@valis
valis committed Mar 3, 2024
1 parent e9abd43 commit 818c480
Show file tree
Hide file tree
Showing 3 changed files with 24 additions and 15 deletions.
27 changes: 15 additions & 12 deletions meta/src/main/java/org/arend/lib/meta/ExtMeta.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ private TypedExpression hidingIRef(ConcreteExpression expr, CoreExpression type)
return binding == null ? typechecker.typecheck(expr, type) : checkGoals(typechecker.withFreeBindings(new FreeBindingsModifier().remove(binding), tc -> tc.typecheck(expr, type)));
}

private ConcreteExpression makeCoeLambda(CoreParameter typeParams, CoreBinding paramBinding, Set<CoreBinding> used, Map<CoreBinding, PathExpression> sigmaRefs, ConcreteFactory factory) {
private ConcreteExpression makeCoeLambda(CoreParameter typeParams, CoreBinding paramBinding, CoreExpression paramType, Set<CoreBinding> used, Map<CoreBinding, PathExpression> sigmaRefs, ConcreteFactory factory) {
ArendRef coeRef = factory.local("i");
return factory.lam(Collections.singletonList(factory.param(coeRef)), factory.meta("ext_coe", new MetaDefinition() {
@Override
Expand All @@ -170,7 +170,7 @@ private ConcreteExpression makeCoeLambda(CoreParameter typeParams, CoreBinding p
substitution.add(new SubstitutionPair(param.getBinding(), sigmaRefs.get(param.getBinding()).applyAt(coeRef, factory, ext)));
}
}
CoreExpression result = typechecker.substitute(paramBinding.getTypeExpr().normalize(NormalizationMode.WHNF), LevelSubstitution.EMPTY, substitution);
CoreExpression result = typechecker.substitute((paramType == null ? paramBinding.getTypeExpr() : paramType).normalize(NormalizationMode.WHNF), LevelSubstitution.EMPTY, substitution);
return result == null ? null : result.computeTyped(true);
}
}));
Expand Down Expand Up @@ -239,12 +239,15 @@ private ConcreteExpression generate(ConcreteExpression arg, CoreExpression type,
}

Set<CoreClassField> propFields = new HashSet<>();
Set<CoreBinding> propBindings = new HashSet<>();
Map<CoreBinding, CoreExpression> propBindings = new HashMap<>();
int i = 0;
for (CoreParameter param = typeParams; param.hasNext(); param = param.getNext(), i++) {
boolean isProp = classFields != null && classFields.get(i).isProperty() || Utils.isProp(param.getTypeExpr());
if (isProp) {
propBindings.add(param.getBinding());
CoreExpression propType = classFields != null && classFields.get(i).isProperty() ? param.getTypeExpr() : null;
if (propType == null) {
propType = Utils.minimizeToProp(param.getTypeExpr());
}
if (propType != null) {
propBindings.put(param.getBinding(), propType);
if (classFields != null) {
propFields.add(classFields.get(i));
}
Expand Down Expand Up @@ -353,7 +356,7 @@ private ConcreteExpression generate(ConcreteExpression arg, CoreExpression type,
for (CoreParameter param = typeParams; param.hasNext(); param = param.getNext(), i++) {
Set<CoreBinding> used = new HashSet<>();
CoreBinding paramBinding = param.getBinding();
boolean isProp = propBindings.contains(paramBinding);
boolean isProp = propBindings.containsKey(paramBinding);
if (!bindings.isEmpty()) {
if (param.getTypeExpr().processSubexpression(e -> {
if (!(e instanceof CoreReferenceExpression)) {
Expand All @@ -362,7 +365,7 @@ private ConcreteExpression generate(ConcreteExpression arg, CoreExpression type,
CoreBinding binding = ((CoreReferenceExpression) e).getBinding();
if (bindings.contains(binding)) {
if (!isProp) {
if (propBindings.contains(binding)) {
if (propBindings.containsKey(binding)) {
typechecker.getErrorReporter().report(new TypecheckingError("Non-propositional fields cannot depend on propositional ones", marker));
return CoreExpression.FindAction.STOP;
}
Expand Down Expand Up @@ -453,7 +456,7 @@ private ConcreteExpression generate(ConcreteExpression arg, CoreExpression type,
CoreBinding binding = used.size() > 1 ? null : used.iterator().next();
PathExpression pathExpr = binding == null ? null : sigmaRefs.get(binding);
if (pathExpr == null || !pathExpr.getClass().equals(PathExpression.class)) {
leftExpr = factory.app(factory.ref(ext.prelude.getCoerce().getRef()), true, Arrays.asList(makeCoeLambda(typeParams, paramBinding, used, sigmaRefs, factory), leftExpr, factory.ref(ext.prelude.getRight().getRef())));
leftExpr = factory.app(factory.ref(ext.prelude.getCoerce().getRef()), true, Arrays.asList(makeCoeLambda(typeParams, paramBinding, propBindings.get(paramBinding), used, sigmaRefs, factory), leftExpr, factory.ref(ext.prelude.getRight().getRef())));
} else {
leftExpr = factory.app(factory.ref(ext.transport.getRef()), true, Arrays.asList(SubstitutionMeta.makeLambda(paramBinding.getTypeExpr(), binding, factory), pathExpr.pathExpression, leftExpr));
}
Expand Down Expand Up @@ -588,8 +591,8 @@ public void solve(@NotNull ExpressionTypechecker typechecker, @NotNull ConcreteG
ArendRef pRef = factory.local("i");
field = applyPath(pRef, pathExpr.applyAt(pRef, factory, ext));
useLet = false;
} else if (propBindings.contains(paramBinding)) {
field = factory.app(factory.ref(ext.propDPI.getRef()), true, Arrays.asList(makeCoeLambda(typeParams, paramBinding, usedList.get(i), fieldsMap, factory), makeProj(factory, left, i, classFields), makeProj(factory, right, i, classFields)));
} else if (propBindings.containsKey(paramBinding)) {
field = factory.app(factory.ref(ext.propDPI.getRef()), true, Arrays.asList(makeCoeLambda(typeParams, paramBinding, propBindings.get(paramBinding), usedList.get(i), fieldsMap, factory), makeProj(factory, left, i, classFields), makeProj(factory, right, i, classFields)));
useLet = true;
} else {
boolean isDependent = dependentBindings.contains(paramBinding);
Expand Down Expand Up @@ -664,7 +667,7 @@ public void solve(@NotNull ExpressionTypechecker typechecker, @NotNull ConcreteG
}
}

field = isDependent ? factory.appBuilder(factory.ref(ext.pathOver.getRef())).app(makeCoeLambda(typeParams, paramBinding, usedList.get(i), fieldsMap, factory), false).app(proj).build() : proj;
field = isDependent ? factory.appBuilder(factory.ref(ext.pathOver.getRef())).app(makeCoeLambda(typeParams, paramBinding, propBindings.get(paramBinding), usedList.get(i), fieldsMap, factory), false).app(proj).build() : proj;
i1++;
}

Expand Down
8 changes: 7 additions & 1 deletion meta/src/main/java/org/arend/lib/util/Utils.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -306,10 +306,16 @@ public static boolean safeCompare(ExpressionTypechecker typechecker, UncheckedEx
}

public static boolean isProp(CoreExpression type) {
CoreExpression typeType = type.normalize(NormalizationMode.WHNF).computeType(true).normalize(NormalizationMode.WHNF);
CoreExpression typeType = type.normalize(NormalizationMode.WHNF).computeType().normalize(NormalizationMode.WHNF);
return typeType instanceof CoreUniverseExpression && ((CoreUniverseExpression) typeType).getSort().isProp();
}

public static CoreExpression minimizeToProp(CoreExpression type) {
type = type.normalize(NormalizationMode.WHNF).minimizeLevels();
CoreExpression typeType = type.computeType().normalize(NormalizationMode.WHNF);
return typeType instanceof CoreUniverseExpression && ((CoreUniverseExpression) typeType).getSort().isProp() ? type : null;
}

public static List<CoreClassField> getNotImplementedField(CoreClassCallExpression classCall) {
List<CoreClassField> classFields = new ArrayList<>();
for (CoreClassField field : classCall.getDefinition().getNotImplementedFields()) {
Expand Down
4 changes: 2 additions & 2 deletions src/Algebra/Ring/Poly.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,8 +80,8 @@
| :: a l, padd p e => \lam s => pmap2 padd (gfunc l p (qadd_cons s).2) (qadd_cons {_} {e} {a} {toQPoly p} {l} s).1
| :: a l, peq => pathOver $ coe_pi *> ext (\lam s => coe_path (path peq) _ idp *> pmap (inv (path peq) *>) (pmap2 (\lam x => pmap2 padd (gfunc l pzero x)) prop-pi set-pi))

\func toQPoly-equiv {R : AddPointed} : Equiv (toQPoly {R})
=> contrFibers=>Equiv $ \case \elim __ \with {
\lemma toQPoly-equiv {R : AddPointed} : Equiv (toQPoly {R})
=> contrFibers=>Equiv \case \elim __ \with {
| in~ l => \new Contr {
| center => (fromArray l, cfunc l)
| contraction t => ext (inv (gfunc l t.1 t.2))
Expand Down

0 comments on commit 818c480

Please sign in to comment.