Add goal to test

jackh726 · May 13, 2022 · 5163fa8 · 5163fa8
1 parent ff44d19
commit 5163fa8
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 9 deletions.
diff --git a/src/logic_grammar.rs b/src/logic_grammar.rs
@@ -25,9 +25,6 @@ pub struct VarBinder(VarId, ParameterKind, Quantifier, Universe);
 
 pub struct VarInequalities(pub Vec<VarInequality>);
 
-pub struct KindedVarIds(pub Vec<KindedVarId>);
-pub struct KindedVarId(pub Parameter, pub VarId);
-
 pub struct Parameters(pub Vec<Parameter>);
 
 pub struct Predicates(pub Vec<Predicate>);
@@ -71,7 +68,7 @@ pub struct Invariants(pub Vec<Invariant>);
 pub struct Invariant(KindedVarIds, Predicate, Predicate); // ForAll KindedVarIds (Implies (Predicate) Predicate))
 
 pub struct Relations(pub Vec<Relation>);
-pub struct Relation(Parameter, RelationOp, Parameter);
+pub struct Relation(pub Parameter, pub RelationOp, pub Parameter);
 pub enum RelationOp {
     Equals,
     InequalityOp(InequalityOp),

diff --git a/src/tests/ty_test_subtyping.rs b/src/tests/ty_test_subtyping.rs
@@ -11,7 +11,7 @@ fn test_subtyping() {
         VarInequalities(vec![]),
         Hypotheses(vec![
             Hypothesis::ForAll(
-                logic_grammar::KindedVarIds(vec![KindedVarId(
+                ty_grammar::KindedVarIds(vec![KindedVarId(
                     Parameter::Ty(Ty::VarId(VarId("T".into()))),
                     VarId("T".into()),
                 )]),
@@ -23,7 +23,7 @@ fn test_subtyping() {
                 ))),
             ),
             Hypothesis::ForAll(
-                logic_grammar::KindedVarIds(vec![KindedVarId(
+                ty_grammar::KindedVarIds(vec![KindedVarId(
                     Parameter::Ty(Ty::VarId(VarId("T".into()))),
                     VarId("T".into()),
                 )]),
@@ -38,4 +38,15 @@ fn test_subtyping() {
             ),
         ]),
     );
+
+    let goal: Goal = Goal::AtomicGoal(AtomicGoal::Relation(
+        Relation(
+            Parameter::Ty(Ty::PredicateTy(PredicateTy::ForAllTy(ForAllTy(ty_grammar::KindedVarIds(vec![ty_grammar::KindedVarId(
+                ty_grammar::Parameter::Ty(Ty::VarId(VarId("T".into()))),
+                VarId("T".into()),
+            )]), Box::new(Ty::VarId(VarId("T".into()))))))),
+            RelationOp::InequalityOp(InequalityOp::SubtypeOp(SubtypeOp::Subset)),
+            Parameter::Ty(Ty::RigidTy(RigidTy(RigidName::ScalarId(ScalarId::U32), ty_grammar::Parameters(vec![])))),
+        ),
+    ));
 }
diff --git a/src/ty_grammar.rs b/src/ty_grammar.rs
@@ -46,7 +46,7 @@ pub enum Ty {
     VarId(VarId),
 }
 
-pub struct RigidTy(RigidName, Parameters);
+pub struct RigidTy(pub RigidName, pub Parameters);
 
 pub enum RigidName {
     AdtId(AdtId),
@@ -68,7 +68,7 @@ pub enum PredicateTy {
     ImplicationTy(ImplicationTy),
     EnsuresTy(EnsuresTy),
 }
-pub struct ForAllTy(KindedVarIds, Box<Ty>);
+pub struct ForAllTy(pub KindedVarIds, pub Box<Ty>);
 pub struct ImplicationTy(WhereClauses, Box<Ty>);
 pub struct ExistsTy(KindedVarIds, Box<Ty>);
 pub struct EnsuresTy(Box<Ty>, WhereClauses);
@@ -129,7 +129,8 @@ pub struct AssociatedTyId(pub String);
 pub struct TyAliasId(pub String);
 pub struct VarId(pub String);
 
-pub struct KindedVarIds;
+pub struct KindedVarIds(pub Vec<KindedVarId>);
+pub struct KindedVarId(pub Parameter, pub VarId);
 
 pub struct Generics(GenericParameters, WhereClauses);
 pub struct GenericParameters(pub Vec<GenericParameter>);