mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Klassengerüst
This commit is contained in:
parent
c8564e14bd
commit
8700a83390
@ -1,5 +1,12 @@
|
|||||||
package edu.kit.typicalc.model;
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
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 java.util.Map;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Models the conclusion of an inference rule and consists of a list of type assumptions, a lambda term and a type.
|
* Models the conclusion of an inference rule and consists of a list of type assumptions, a lambda term and a type.
|
||||||
* This class is used in inference steps to represent the conclusion of that specific application of the inference rule.
|
* This class is used in inference steps to represent the conclusion of that specific application of the inference rule.
|
||||||
|
@ -1,5 +1,7 @@
|
|||||||
package edu.kit.typicalc.model;
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
import edu.kit.typicalc.model.type.Type;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Constrains two types to be equal.
|
* Constrains two types to be equal.
|
||||||
*/
|
*/
|
||||||
|
@ -1,5 +1,8 @@
|
|||||||
package edu.kit.typicalc.model;
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
import edu.kit.typicalc.model.type.Type;
|
||||||
|
import edu.kit.typicalc.model.type.TypeVariable;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* A substitution specifies that some type should be replaced by a different type.
|
* A substitution specifies that some type should be replaced by a different type.
|
||||||
*/
|
*/
|
||||||
|
@ -1,6 +1,13 @@
|
|||||||
package edu.kit.typicalc.model;
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
import edu.kit.typicalc.model.step.InferenceStep;
|
||||||
|
import edu.kit.typicalc.model.term.LambdaTerm;
|
||||||
|
import edu.kit.typicalc.model.term.TermVisitor;
|
||||||
|
import edu.kit.typicalc.model.term.VarTerm;
|
||||||
|
import edu.kit.typicalc.model.type.TypeAbstraction;
|
||||||
|
|
||||||
import java.util.List;
|
import java.util.List;
|
||||||
|
import java.util.Map;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Models the proof tree formed when the type of a lambda term is inferred.
|
* Models the proof tree formed when the type of a lambda term is inferred.
|
||||||
|
@ -1,5 +1,8 @@
|
|||||||
package edu.kit.typicalc.model;
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
import edu.kit.typicalc.model.type.Type;
|
||||||
|
import edu.kit.typicalc.model.type.TypeVariable;
|
||||||
|
|
||||||
import java.util.List;
|
import java.util.List;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -1,6 +1,13 @@
|
|||||||
package edu.kit.typicalc.model;
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
import edu.kit.typicalc.model.step.InferenceStep;
|
||||||
|
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 java.util.List;
|
import java.util.List;
|
||||||
|
import java.util.Map;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* The type inferer is responsible for the whole type inference of a given lambda term, taking
|
* The type inferer is responsible for the whole type inference of a given lambda term, taking
|
||||||
|
@ -1,5 +1,8 @@
|
|||||||
package edu.kit.typicalc.model;
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
import edu.kit.typicalc.model.step.InferenceStep;
|
||||||
|
import edu.kit.typicalc.model.type.Type;
|
||||||
|
|
||||||
import java.util.List;
|
import java.util.List;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -1,6 +1,11 @@
|
|||||||
package edu.kit.typicalc.model;
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
import edu.kit.typicalc.model.term.LambdaTerm;
|
||||||
|
import edu.kit.typicalc.model.term.VarTerm;
|
||||||
|
import edu.kit.typicalc.model.type.TypeAbstraction;
|
||||||
|
|
||||||
import java.util.List;
|
import java.util.List;
|
||||||
|
import java.util.Map;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Instances of this subclass of TypeInferer are used to execute the sub-inference starting in let steps.
|
* Instances of this subclass of TypeInferer are used to execute the sub-inference starting in let steps.
|
||||||
|
@ -1,5 +1,7 @@
|
|||||||
package edu.kit.typicalc.model;
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
import edu.kit.typicalc.model.type.TypeVariable;
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Provides unique type variables on demand.
|
* Provides unique type variables on demand.
|
||||||
*/
|
*/
|
||||||
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model;
|
||||||
|
|
||||||
|
public class UnificationStep {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.step;
|
||||||
|
|
||||||
|
public class InferenceStep {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.term;
|
||||||
|
|
||||||
|
public class LambdaTerm {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.term;
|
||||||
|
|
||||||
|
public interface TermVisitor {
|
||||||
|
}
|
4
src/main/java/edu/kit/typicalc/model/term/VarTerm.java
Normal file
4
src/main/java/edu/kit/typicalc/model/term/VarTerm.java
Normal file
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.term;
|
||||||
|
|
||||||
|
public class VarTerm {
|
||||||
|
}
|
4
src/main/java/edu/kit/typicalc/model/type/Type.java
Normal file
4
src/main/java/edu/kit/typicalc/model/type/Type.java
Normal file
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.type;
|
||||||
|
|
||||||
|
public abstract class Type {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.type;
|
||||||
|
|
||||||
|
public class TypeAbstraction {
|
||||||
|
}
|
@ -0,0 +1,4 @@
|
|||||||
|
package edu.kit.typicalc.model.type;
|
||||||
|
|
||||||
|
public class TypeVariable {
|
||||||
|
}
|
Loading…
Reference in New Issue
Block a user