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

TermVisitorTree

Browse Source
This commit is contained in:
Arne Keller 2021-01-27 21:21:16 +01:00
parent f2cd4370cf
commit f3fd6d0696
2 changed files with 83 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

79
src/main/java/edu/kit/typicalc/model/term/TermVisitorTree.java Normal file
View File

@ -0,0 +1,79 @@
package edu.kit.typicalc.model.term;
import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.type.Type;
import edu.kit.typicalc.model.type.TypeAssumption;
import java.util.List;
public interface TermVisitorTree {
/**
* Returns an {@link edu.kit.typicalc.model.step.AppStep} suiting the given application (lambda term)
* to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list.
* @param appTerm the application (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.AppStep}
*/
InferenceStep visit(AppTerm appTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.AbsStep} suiting the given abstraction (lambda term)
* to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list.
* @param absTerm the abstraction (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.AbsStep}
*/
InferenceStep visit(AbsTerm absTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.LetStep} suiting the given let expression (lambda term)
* to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list.
* @param letTerm the let expression (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.LetStep}
*/
InferenceStep visit(LetTerm letTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.ConstStep} suiting the given constant
* to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list.
* @param constTerm the constant to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.ConstStep}
*/
InferenceStep visit(ConstTerm constTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
/**
* Returns an {@link edu.kit.typicalc.model.step.VarStep} suiting the given variable (lambda term)
* to type-infer and the type assumptions to consider.
* Simultaneously assembles the tree's constraint list.
* @param varTerm the variable (lambda term) to build the inference step structure for,
* i.e. the lambda term in the conclusion of the returned inference step
* @param typeAssumptions the type assumptions to consider,
* i.e. the type assumptions in the conclusion of the returned inference step
* @param conclusionType the type that the lambda term in the conclusion
* of the returned inference step will be assigned
* @return an {@link edu.kit.typicalc.model.step.VarStep}
*/
InferenceStep visit(VarTerm varTerm, List<TypeAssumption> typeAssumptions, Type conclusionType);
}

4
src/main/java/edu/kit/typicalc/model/type/TypeAssumption.java Normal file
View File

@ -0,0 +1,4 @@
package edu.kit.typicalc.model.type;
public class TypeAssumption {
}