arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

create type assumptions for free varibales in TypeInferer

Browse Source 
for this add getFreeVaribales() in lambda term
and enum TypeVaribaleKind
This commit is contained in:
Johanna Stuber 2021-01-28 22:24:41 +01:00
parent 804dfb2c2f
commit 785ce3dcc8
18 changed files with 150 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/main/java/edu/kit/typicalc/model/Conclusion.java
View File

@ -25,7 +25,6 @@ public class Conclusion {
* @param type the type assigned to the lambda term in the conclusion
*/
protected Conclusion(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm, Type type) {
// TODO: null checks?
this.typeAssumptions = typeAssumptions;
this.lambdaTerm = lambdaTerm;
this.type = type;

1
src/main/java/edu/kit/typicalc/model/Constraint.java
View File

@ -17,7 +17,6 @@ public class Constraint {
* @param b second type
*/
public Constraint(Type a, Type b) {
// TODO: null checks?
this.a = a;
this.b = b;
}

1
src/main/java/edu/kit/typicalc/model/Substitution.java
View File

@ -19,7 +19,6 @@ public class Substitution {
* @param b type to insert
*/
public Substitution(TypeVariable a, Type b) {
// TODO: null checks?
this.a = a;
this.b = b;
}

8
src/main/java/edu/kit/typicalc/model/Tree.java
View File

@ -11,10 +11,7 @@ import edu.kit.typicalc.model.term.LambdaTerm;
import edu.kit.typicalc.model.term.LetTerm;
import edu.kit.typicalc.model.term.TermVisitorTree;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.FunctionType;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import edu.kit.typicalc.model.type.TypeVariable;
import edu.kit.typicalc.model.type.*;
import java.util.ArrayList;
import java.util.HashMap;
@ -45,7 +42,7 @@ public class Tree implements TermVisitorTree {
* @param lambdaTerm the lambda term to generate the tree for
*/
protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm) {
this(typeAssumptions, lambdaTerm, new TypeVariableFactory());
this(typeAssumptions, lambdaTerm, new TypeVariableFactory(TypeVaribaleKind.TREE));
}
/**
@ -61,7 +58,6 @@ public class Tree implements TermVisitorTree {
*/
protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm,
TypeVariableFactory typeVariableFactory) {
// TODO: null checks
this.typeVarFactory = typeVariableFactory;
this.constraints = new ArrayList<>();

21
src/main/java/edu/kit/typicalc/model/TypeInferer.java
View File

@ -5,9 +5,12 @@ import edu.kit.typicalc.model.term.LambdaTerm;
import edu.kit.typicalc.model.term.VarTerm;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import edu.kit.typicalc.model.type.TypeVaribaleKind;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;
/**
* The type inferer is responsible for the whole type inference of a given lambda term, taking
@ -32,8 +35,10 @@ public class TypeInferer implements TypeInfererInterface {
* @param typeAssumptions the type assumptions to consider when generating the tree
*/
protected TypeInferer(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions) {
// TODO: null checks
tree = new Tree(typeAssumptions, lambdaTerm);
Map<VarTerm, TypeAbstraction> completeTypeAss = createAssForFreeVariables(lambdaTerm);
completeTypeAss.putAll(typeAssumptions);
tree = new Tree(completeTypeAss, lambdaTerm);
// TODO: Abbrechen bei fehlgeschlagener let-Teilinferenz, evtl. getUnificationSteps() anpassen
unification = new Unification(tree.getConstraints());
@ -50,6 +55,18 @@ public class TypeInferer implements TypeInfererInterface {
typeInfResult = new TypeInferenceResult(substitutions, tree.getFirstTypeVariable());
}
private Map<VarTerm, TypeAbstraction> createAssForFreeVariables(LambdaTerm lambdaTerm) {
TypeVariableFactory typeVarFactory = new TypeVariableFactory(TypeVaribaleKind.GENERATED_TYPE_ASSUMPTION);
Set<VarTerm> freeVariables = lambdaTerm.getFreeVariables();
Map<VarTerm, TypeAbstraction> generatedTypeAss = new HashMap<>();
for (VarTerm varTerm : freeVariables) {
generatedTypeAss.put(varTerm, new TypeAbstraction(typeVarFactory.nextTypeVariable()));
}
return generatedTypeAss;
}
@Override
public InferenceStep getFirstInferenceStep() {

11
src/main/java/edu/kit/typicalc/model/TypeVariableFactory.java
View File

@ -1,6 +1,7 @@
package edu.kit.typicalc.model;
import edu.kit.typicalc.model.type.TypeVariable;
import edu.kit.typicalc.model.type.TypeVaribaleKind;
/**
* Provides unique type variables on demand.
@ -9,12 +10,16 @@ public class TypeVariableFactory {
private static final int FIRST_VARIABLE_INDEX = 1;
private final TypeVaribaleKind kind;
private int nextVariableIndex;
/**
* Initializes a new type variable factory.
* Initializes a new type variable factory for type variables of the given kind.
*
* @param kind the kind of the created type variables
*/
protected TypeVariableFactory() {
protected TypeVariableFactory(TypeVaribaleKind kind) {
this.kind = kind;
nextVariableIndex = FIRST_VARIABLE_INDEX;
}
@ -24,7 +29,7 @@ public class TypeVariableFactory {
* @return a new unique type variable
*/
public TypeVariable nextTypeVariable() {
TypeVariable nextTypeVariable = new TypeVariable(nextVariableIndex);
TypeVariable nextTypeVariable = new TypeVariable(kind, nextVariableIndex);
nextVariableIndex++;
return nextTypeVariable;
}

9
src/main/java/edu/kit/typicalc/model/term/AbsTerm.java
View File

@ -4,8 +4,10 @@ import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.HashSet;
import java.util.Map;
import java.util.Objects;
import java.util.Set;
/**
* Representation of an abstraction term with its two sub-lambda terms.
@ -44,6 +46,13 @@ public class AbsTerm extends LambdaTerm {
return body.hasLet();
}
@Override
public Set<VarTerm> getFreeVariables() {
Set<VarTerm> set = new HashSet<>(this.body.getFreeVariables());
set.remove(this.var);
return set;
}
@Override
public void accept(TermVisitor termVisitor) {
termVisitor.visit(this);

10
src/main/java/edu/kit/typicalc/model/term/AppTerm.java
View File

@ -4,8 +4,7 @@ import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
import java.util.Objects;
import java.util.*;
/**
* Representation of an application term consisting of a function and the parameter passed to it.
@ -43,6 +42,13 @@ public class AppTerm extends LambdaTerm {
return left.hasLet() || right.hasLet();
}
@Override
public Set<VarTerm> getFreeVariables() {
Set<VarTerm> set = new HashSet<>(this.left.getFreeVariables());
set.addAll(this.right.getFreeVariables());
return set;
}
@Override
public void accept(TermVisitor termVisitor) {
termVisitor.visit(this);

7
src/main/java/edu/kit/typicalc/model/term/ConstTerm.java
View File

@ -5,7 +5,9 @@ import edu.kit.typicalc.model.type.NamedType;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
/**
* Abstract representation of a constant lambda term that has a predetermined type and a value of that type.
@ -16,6 +18,11 @@ public abstract class ConstTerm extends LambdaTerm {
*/
public abstract NamedType getType();
@Override
public Set<VarTerm> getFreeVariables() {
return new HashSet<>();
}
@Override
public boolean hasLet() {
return false;

8
src/main/java/edu/kit/typicalc/model/term/LambdaTerm.java
View File

@ -5,6 +5,7 @@ import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
import java.util.Set;
/**
* Abstract representation of a lambda term.
@ -17,6 +18,12 @@ public abstract class LambdaTerm {
*/
public abstract boolean hasLet();
/**
* Returns a set of all free variables occurring in the lambda term.
* @return all free variables
*/
public abstract Set<VarTerm> getFreeVariables();
/**
* Calls exactly one method on the visitor depending on the lambda term type.
* @param termVisitor a visitor
@ -32,5 +39,4 @@ public abstract class LambdaTerm {
*/
public abstract InferenceStep accept(TermVisitorTree termVisitorTree,
Map<VarTerm, TypeAbstraction> assumptions, Type type);
}

10
src/main/java/edu/kit/typicalc/model/term/LetTerm.java
View File

@ -4,8 +4,10 @@ import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.HashSet;
import java.util.Map;
import java.util.Objects;
import java.util.Set;
/**
* Representation of a let term with its variable, the lambda term assigned
@ -33,6 +35,14 @@ public class LetTerm extends LambdaTerm {
return true;
}
@Override
public Set<VarTerm> getFreeVariables() {
Set<VarTerm> set = new HashSet<>(this.body.getFreeVariables());
set.remove(this.variable);
set.addAll(this.definition.getFreeVariables());
return set;
}
@Override
public void accept(TermVisitor termVisitor) {
termVisitor.visit(this);

8
src/main/java/edu/kit/typicalc/model/term/VarTerm.java
View File

@ -4,8 +4,7 @@ import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAbstraction;
import java.util.Map;
import java.util.Objects;
import java.util.*;
/**
* Representation of a variable term with its name.
@ -34,6 +33,11 @@ public class VarTerm extends LambdaTerm {
return false;
}
@Override
public Set<VarTerm> getFreeVariables() {
return new HashSet<>(Collections.singletonList(this));
}
@Override
public void accept(TermVisitor termVisitor) {
termVisitor.visit(this);

16
src/main/java/edu/kit/typicalc/model/type/FunctionType.java
View File

@ -68,11 +68,11 @@ public class FunctionType extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with
* Computes the necessary constraints (and substitution) to unify this type with
* another. This method uses the constrainEqualToFunction method on the other
* type.
* @param type the other type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
//TODO
@ -80,10 +80,10 @@ public class FunctionType extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* function type.
* @param type the function type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type) {
//TODO
@ -91,10 +91,10 @@ public class FunctionType extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* named type.
* @param type the named type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
//TODO
@ -102,10 +102,10 @@ public class FunctionType extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* type variable.
* @param type the type variable
* @return the unification steps neccessary, or an error if that is impossible
* @return the unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
//TODO

16
src/main/java/edu/kit/typicalc/model/type/NamedType.java
View File

@ -65,11 +65,11 @@ public class NamedType extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with
* Computes the necessary constraints (and substitution) to unify this type with
* another. This method uses the constrainEqualToNamedType method on the other
* type.
* @param type the other type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
//TODO
@ -77,10 +77,10 @@ public class NamedType extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* function type.
* @param type the function type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type) {
//TODO
@ -88,10 +88,10 @@ public class NamedType extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* named type.
* @param type the named type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
//TODO
@ -99,10 +99,10 @@ public class NamedType extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* type variable.
* @param type the type variable
* @return the unification steps neccessary, or an error if that is impossible
* @return the unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
//TODO

16
src/main/java/edu/kit/typicalc/model/type/Type.java
View File

@ -29,34 +29,34 @@ public abstract class Type {
public abstract void accept(TypeVisitor typeVisitor);
/**
* Computes the neccessary constraints (and substitution) to unify this type with
* Computes the necessary constraints (and substitution) to unify this type with
* another type.
* @param type the other type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public abstract Result<UnificationActions, UnificationError> constrainEqualTo(Type type);
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* function type.
* @param type the function type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public abstract Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type);
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* named type.
* @param type the named type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public abstract Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type);
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* type variable.
* @param type the type variable
* @return the unification steps neccessary, or an error if that is impossible
* @return the unification steps necessary, or an error if that is impossible
*/
public abstract Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type);

38
src/main/java/edu/kit/typicalc/model/type/TypeVariable.java
View File

@ -7,18 +7,32 @@ import edu.kit.typicalc.util.Result;
* Models a type variable
*/
public class TypeVariable extends Type {
private int index;
private final TypeVaribaleKind kind;
private final int index;
/**
* Initializes a new TypeVariable with the given index.
*
* @param kind the kind of type variable
* @param index the index of this variable
*/
public TypeVariable(int index) {
public TypeVariable(TypeVaribaleKind kind, int index) {
this.kind = kind;
this.index = index;
}
/**
* the index of the type variable as an integer
* @return index
* Returns the kind of the type variable.
* @return the variable's kind
*/
public TypeVaribaleKind getKind() {
return kind;
}
/**
* Returns the index of the type variable as an integer
* @return the variable's index
*/
public int getIndex() {
return index;
@ -53,11 +67,11 @@ public class TypeVariable extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with
* Computes the necessary constraints (and substitution) to unify this type with
* another. This method uses the constrainEqualToVariable method on the other
* type.
* @param type the other type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualTo(Type type) {
//TODO
@ -65,10 +79,10 @@ public class TypeVariable extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* function type.
* @param type the function type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToFunction(Type type) {
//TODO
@ -76,10 +90,10 @@ public class TypeVariable extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* named type.
* @param type the named type
* @return unification steps neccessary, or an error if that is impossible
* @return unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToNamedType(NamedType type) {
//TODO
@ -87,10 +101,10 @@ public class TypeVariable extends Type {
}
/**
* Computes the neccessary constraints (and substitution) to unify this type with a
* Computes the necessary constraints (and substitution) to unify this type with a
* type variable.
* @param type the type variable
* @return the unification steps neccessary, or an error if that is impossible
* @return the unification steps necessary, or an error if that is impossible
*/
public Result<UnificationActions, UnificationError> constrainEqualToVariable(TypeVariable type) {
//TODO

22
src/main/java/edu/kit/typicalc/model/type/TypeVaribaleKind.java Normal file
View File

@ -0,0 +1,22 @@
package edu.kit.typicalc.model.type;
/**
* Describes the kind of type variable (the context it was generated / it is used in).
*/
public enum TypeVaribaleKind {
/**
* Used if the type variable was created from user input.
*/
USER_INPUT,
/**
* Used if the type variable was generated while building the proof tree.
*/
TREE,
/**
* Used if the type variable was generated for a type assumption of a free variable in the input lambda term.
*/
GENERATED_TYPE_ASSUMPTION
}

4
src/main/java/edu/kit/typicalc/model/type/UnificationActions.java
View File

@ -7,7 +7,7 @@ import java.util.Collection;
import java.util.Optional;
/**
* Models the neccessary actions to process a constraint.
* Models the necessary actions to process a constraint.
*/
public class UnificationActions {
private Collection<Constraint> constraints;
@ -16,7 +16,7 @@ public class UnificationActions {
/**
* Initializes this object using the provided constraints and substitution.
* @param constraints added constraints, if any
* @param substitution neccessary substitution, if any
* @param substitution necessary substitution, if any
*/
protected UnificationActions(Collection<Constraint> constraints, Optional<Substitution> substitution) {
this.constraints = constraints;