From c58a4bfafdca11b80ef92a0ed4be5ed0b3bfaa0d Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sun, 13 Oct 2019 17:50:02 -0400 Subject: [PATCH] [ clause ] Move `ProblemEq`. Maybe it's time to release a newer version? --- src/check/rules/clause.rs | 13 ++++++++++++- src/syntax/abs/decl.rs | 12 ------------ 2 files changed, 12 insertions(+), 13 deletions(-) diff --git a/src/check/rules/clause.rs b/src/check/rules/clause.rs index 4bb8564..e3b12d7 100644 --- a/src/check/rules/clause.rs +++ b/src/check/rules/clause.rs @@ -1,7 +1,18 @@ use crate::check::monad::{TCM, TCS}; -use crate::syntax::abs::{AbsClause, AbsCopat, ProblemEq}; +use crate::syntax::abs::{AbsClause, AbsCopat}; use crate::syntax::core::{Clause, Pat, Tele, Term, Val}; +/// A user pattern and a core term that they should equal +/// after splitting is complete. +/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Abstract.html#ProblemEq). +#[derive(Debug, PartialEq, Eq, Clone)] +pub struct ProblemEq { + /// The pattern causes this problem. + in_pat: AbsCopat, + inst: Term, + ty: Term, +} + /// User patterns we still have to split on. /// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.LHS.Problem.html#Problem). #[derive(Debug, Clone)] diff --git a/src/syntax/abs/decl.rs b/src/syntax/abs/decl.rs index b033166..1e8a44b 100644 --- a/src/syntax/abs/decl.rs +++ b/src/syntax/abs/decl.rs @@ -2,8 +2,6 @@ use voile_util::level::Level; use voile_util::loc::{Ident, Loc, ToLoc}; use voile_util::uid::GI; -use crate::syntax::core::Term; - use super::{Abs, AbsCopat, AbsTele}; /// Declaration. @@ -131,16 +129,6 @@ impl ToLoc for AbsDecl { } } -/// A user pattern and a core term that they should equal -/// after splitting is complete. -/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Abstract.html#ProblemEq). -#[derive(Debug, PartialEq, Eq, Clone)] -pub struct ProblemEq { - in_pat: AbsCopat, - inst: Term, - ty: Term, -} - /// Clause information in abstract syntax. /// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Abstract.html#Clause%27). #[derive(Debug, PartialEq, Eq, Clone)]