Implement BuiltinGoal::Implies

jackh726 · May 14, 2022 · bcc159a · bcc159a
1 parent ff96a93
commit bcc159a
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
diff --git a/src/cosld_solve.rs b/src/cosld_solve.rs
@@ -9,7 +9,11 @@ pub fn prove(env: Env, prove_stacks: ProveStacks, goal: Goal) -> Option<Env> {
         Goal::AtomicGoal(AtomicGoal::Relation(relation)) => todo!(),
         Goal::BuiltinGoal(BuiltinGoal::All(goals)) => prove_all(env, prove_stacks, *goals),
         Goal::BuiltinGoal(BuiltinGoal::Any(goals)) => todo!(),
-        Goal::BuiltinGoal(BuiltinGoal::Implies(hypotheses, goal)) => todo!(),
+        Goal::BuiltinGoal(BuiltinGoal::Implies(hypotheses, goal)) => {
+            let env_1 = utils::env_with_hypotheses(env.clone(), hypotheses);
+            let env_out = prove(env_1, prove_stacks, *goal)?;
+            Some(utils::reset(env, VarIds(vec![]), env_out))
+        }
         Goal::BuiltinGoal(BuiltinGoal::Quantified(quantifier, kinded_var_ids, goal)) => {
             let (env_1, goal_1, varids_new) =
                 instantiate::instantiate_qualified(env.clone(), quantifier, kinded_var_ids, *goal);

diff --git a/src/utils.rs b/src/utils.rs
@@ -58,3 +58,7 @@ pub fn env_with_vars_in_current_universe(
 ) -> Env {
     todo!()
 }
+
+pub fn env_with_hypotheses(env: Env, hypotheses: Hypotheses) -> Env {
+    todo!()
+}
-Original file line number
+Diff line change
@@ Expand Up / @@ -58,3 +58,7 @@ pub fn env_with_vars_in_current_universe( @@
     ) -> Env {
         todo!()
     }
+    pub fn env_with_hypotheses(env: Env, hypotheses: Hypotheses) -> Env {
+        todo!()
+    }