From 865f27dd1989cdcedc2dc3f4a1493217db90343d Mon Sep 17 00:00:00 2001 From: WhatisRT Date: Thu, 28 Nov 2024 09:44:14 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20agda/agd?= =?UTF-8?q?a-stdlib-meta@4125a767c99a2b8be773ed87d0a2f05b54fd555f=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Tactic.Case.html | 14 +- Tactic.ClauseBuilder.html | 623 +++++++++++++++++++------------------- Tactic.Derive.DecEq.html | 12 +- Tactic.Derive.Show.html | 8 +- Tactic.Derive.html | 12 +- typecheck.time | 30 +- 6 files changed, 344 insertions(+), 355 deletions(-) diff --git a/Tactic.Case.html b/Tactic.Case.html index 77deeb0..ca1b665 100644 --- a/Tactic.Case.html +++ b/Tactic.Case.html @@ -22,17 +22,17 @@ instance _ = MonadTC-TCI - _ = ContextMonad-MonadTC + _ = ContextMonad-MonadTC _ = Functor-M -open ClauseExprM +open ClauseExprM -matchInductive : Type → (SinglePattern → TC (ClauseExpr ⊎ Maybe Term)) → TC ClauseExpr +matchInductive : Type → (SinglePattern → TC (ClauseExpr ⊎ Maybe Term)) → TC ClauseExpr matchInductive ty rhs = do - ps ← constructorPatterns' ty - matchExprM (map (λ p → p , rhs p) ps) + ps ← constructorPatterns' ty + matchExprM (map (λ p → p , rhs p) ps) -genMatchingClauses : Type → TC Term → TC ClauseExpr +genMatchingClauses : Type → TC Term → TC ClauseExpr genMatchingClauses ty x = matchInductive ty (λ _ → (inj₂ ∘ just) <$> x) -- apply tac to all holes @@ -40,7 +40,7 @@ case a tac = inDebugPath "case" do t ← quoteTC a ty ← inferType t - unifyWithGoal =<< caseMatch t (genMatchingClauses ty (withGoalHole tac)) + unifyWithGoal =<< caseMatch t (genMatchingClauses ty (withGoalHole tac)) private module Test (A B : Set) where diff --git a/Tactic.ClauseBuilder.html b/Tactic.ClauseBuilder.html index b93cbf6..edb95af 100644 --- a/Tactic.ClauseBuilder.html +++ b/Tactic.ClauseBuilder.html @@ -38,321 +38,310 @@ open import Data.String as S using (parens) -showPattern : Pattern → String -showPattern (con c []) = "con" <+> show c -showPattern (con c ps) = parens ("con" <+> show c <+> show ps) -showPattern (dot t) = "." S.++ parens (show t) -showPattern (var x) = "pat-var" <+> show x -showPattern (lit l) = show l -showPattern (proj f) = show f -showPattern (absurd _) = "()" - - -record ClauseBuilder (M : Set → Set) : Set₁ where - field - Base : Set → Set - liftBase : Base A → M A - addPattern : List (String × Arg Type) → Arg Pattern → M A → M A - toClause : M (Maybe Term) → Base Clause - -open ClauseBuilder {{...}} public - -SinglePattern : Set -SinglePattern = List (String × Arg Type) × Arg Pattern - -typedVarSinglePattern : String → Arg Type → SinglePattern -typedVarSinglePattern n t@(arg i _) = ([ n , t ] , arg i (` 0)) - -varSinglePattern : Arg String → SinglePattern -varSinglePattern (arg i n) = ([ n , arg i unknown ] , arg i (` 0)) - -multiSinglePattern : List String → Arg Pattern → SinglePattern -multiSinglePattern s p = ((_, vArg unknown) <$> s) , p - -findIndexDefault : List ℕ → ℕ → ℕ → ℕ -findIndexDefault l d a with filter (λ where (i , x) → x ≟ a) (zipWithIndex _,_ l) -... | [] = d -... | (i , _) ∷ _ = i - -singlePatternFromPattern : Arg Pattern → SinglePattern -singlePatternFromPattern (arg i p) = - replicate (length (appearingIndices p)) ("" , vArg unknown) , arg i (replacePatternIndex p) - where - appearingIndices : Pattern → List ℕ - appearingIndicesHelper : List (Arg Pattern) → List ℕ - - appearingIndices (Pattern.con c ps) = appearingIndicesHelper ps - appearingIndices (Pattern.dot t) = [] -- TODO: this is probably wrong - appearingIndices (` x) = [ x ] - appearingIndices (Pattern.lit l) = [] - appearingIndices (Pattern.proj f) = [] - appearingIndices (Pattern.absurd x) = [] - - appearingIndicesHelper [] = [] - appearingIndicesHelper (arg _ p ∷ ps) = appearingIndices p ++ appearingIndicesHelper ps - - normalisedIndexList : List ℕ - normalisedIndexList = sort $ deduplicate _≟_ $ appearingIndices p - - replacePatternIndex : Pattern → Pattern - replacePatternIndexHelper : List (Arg Pattern) → List (Arg Pattern) - - replacePatternIndex (Pattern.con c ps) = Pattern.con c (replacePatternIndexHelper ps) - replacePatternIndex (Pattern.dot t) = Pattern.dot t - replacePatternIndex (` x) = ` findIndexDefault normalisedIndexList 0 x - replacePatternIndex (Pattern.lit l) = Pattern.lit l - replacePatternIndex (Pattern.proj f) = Pattern.proj f - replacePatternIndex (Pattern.absurd x) = Pattern.absurd x - - replacePatternIndexHelper [] = [] - replacePatternIndexHelper (arg i p ∷ ps) = (arg i (replacePatternIndex p)) ∷ (replacePatternIndexHelper ps) - -module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ where - - instance _ = Functor-M {M = M} - - ctxSinglePatterns : M (List SinglePattern) - ctxSinglePatterns = do - ctx ← getContext - return (singlePatternFromPattern <$> zipWithIndex (λ where k (_ , (arg i _)) → arg i (` k)) ctx) - - -- TODO: add the ability to match initial hidden arguments - -- TODO: add dot patterns - constrToPattern : Name → Type → M SinglePattern - constrToPattern n ty = do - (introTel , _) ← viewTy <$> (runAndReset $ local (λ env → record env { normalisation = true }) $ inferType (n ◆)) - let patternTel = zipWith (λ where (abs _ (arg i _)) k → arg i (` k)) introTel $ downFrom $ length introTel - return (((λ where (abs s (arg i t)) → (s , arg i unknown)) <$> introTel) , (vArg $ Pattern.con n patternTel)) - - -- like constrToPattern, but applied to parameters - constrToPatternTyped : Name → List Term → M SinglePattern - constrToPatternTyped n ps = do - t ← applyWithVisibility n ps - debugLogᵐ (t ᵛⁿ ∷ᵈᵐ []ᵐ) - (introTel , _) ← viewTy <$> (local (λ env → record env { normalisation = true }) $ inferType t) - let patternTel = zipWith (λ where (abs _ (arg i _)) k → arg i (` k)) introTel $ downFrom $ length introTel - return (((λ where (abs s (arg i t)) → (s , arg i t)) <$> introTel) , (vArg $ Pattern.con n patternTel)) - - -- all possible patterns for an inductive type - constructorPatterns : Arg Type → M (List SinglePattern) - constructorPatterns (arg i ty) = do - constrs ← getConstrsForType ty - return $ constrs <&> λ where - (n , t) → let argInfo = proj₁ $ viewTy t - in (((λ where (abs n' t') → n' , t') <$> argInfo) - , arg i (Pattern.con n (zipWithIndex (λ where k (abs _ (arg i _)) → arg i (` (length argInfo ∸ ℕ.suc k))) argInfo))) - - -- all possible patterns for an inductive type - constructorPatterns' : Type → M (List SinglePattern) - constructorPatterns' ty = do - constrs ← getConstrsForType ty - traverse (λ (n , _) → constrToPattern n ty) constrs - - -- all possible patterns for an inductive type - constructorPatternsTyped : Type → List Type → M (List SinglePattern) - constructorPatternsTyped ty ps = do - constrs ← getConstrsForType ty - traverse (λ (n , _) → constrToPatternTyped n ps) constrs - -ClauseInfo : Set -ClauseInfo = List SinglePattern - -data ClauseExpr : Set where - MatchExpr : List (SinglePattern × (ClauseExpr ⊎ Maybe Term)) → ClauseExpr - -multiClauseExpr : List (NE.List⁺ SinglePattern × (ClauseExpr ⊎ Maybe Term)) → ClauseExpr -multiClauseExpr = MatchExpr ∘ Data.List.map helper - where - helper' : (List SinglePattern × (ClauseExpr ⊎ Maybe Term)) → ClauseExpr ⊎ Maybe Term - helper' ([] , e) = e - helper' (p ∷ ps , e) = inj₁ (MatchExpr [ p , helper' (ps , e) ]) - - helper : (NE.List⁺ SinglePattern × (ClauseExpr ⊎ Maybe Term)) → SinglePattern × (ClauseExpr ⊎ Maybe Term) - helper (p NE.∷ ps , e) = p , helper' (ps , e) - -clauseExprToClauseInfo : ClauseExpr → List (ClauseInfo × Maybe Term) -clauseExprToClauseInfo (MatchExpr []) = [] -clauseExprToClauseInfo (MatchExpr ((p , inj₁ e) ∷ xs)) = - (map₁ (p ∷_) <$> clauseExprToClauseInfo e) ++ clauseExprToClauseInfo (MatchExpr xs) -clauseExprToClauseInfo (MatchExpr ((p , inj₂ t) ∷ xs)) = ([ p ] , t) ∷ clauseExprToClauseInfo (MatchExpr xs) - -clauseInfoToClauseArgs : ClauseInfo → List (String × Arg Type) × List (Arg Pattern) -clauseInfoToClauseArgs i = - case helper 0 i of λ where (tel , ps , _) → (tel , ps) - where - helper : ℕ → ClauseInfo → List (String × Arg Type) × List (Arg Pattern) × ℕ - helper k [] = ([] , [] , k) - helper k ((tel' , arg h p) ∷ i) with helper k i - ... | (tel , ps , k') = (tel' ++ tel , arg h (mapVariables (_+ k') p) ∷ ps , length tel' + k') - -clauseInfoToClause : ClauseInfo → Maybe Term → Clause -clauseInfoToClause i t with clauseInfoToClauseArgs i | t -... | tel , ps | just x = Clause.clause tel ps x -... | tel , ps | nothing = Clause.absurd-clause tel ps - -clauseExprToClauses : ClauseExpr → List Clause -clauseExprToClauses e = (λ { (i , t) → clauseInfoToClause i t }) <$> clauseExprToClauseInfo e - -nonBindingClause : Term → Clause -nonBindingClause = Clause.clause [] [] - -clauseExprToPatLam : ClauseExpr → Term -clauseExprToPatLam e = pat-lam (clauseExprToClauses e) [] - -record ContextMonad (M : ∀ {a} → Set a → Set a) ⦃ _ : Monad M ⦄ : Setω where - field - introPatternM : SinglePattern → M A → M A - - extendContextM : Arg Type → M A → M A - extendContextM l x = introPatternM (typedVarSinglePattern "" l) x - -open ContextMonad ⦃...⦄ - -Monad-Id : Monad id -Monad-Id .return = id -Monad-Id ._>>=_ = flip _$_ - --- No context -ContextMonad-Id : ContextMonad id ⦃ Monad-Id ⦄ -ContextMonad-Id .introPatternM _ a = a - -module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ where - - instance _ = Functor-M {M = M} - - refineWithSingle : (Term → Term) → M Term → M Term - refineWithSingle ref x = do - goalTy ← goalTy - m ← newMeta unknown - res ← checkType (ref m) goalTy - x' ← runWithHole m x - unify m x' - return $ ref x' - - caseMatch : Term → M ClauseExpr → M Term - caseMatch t expr = debugLog ("Match" ∷ᵈ t ∷ᵈ []) >> (refineWithSingle (quote case_of_ ∙⟦ t ∣_⟧) $ - (λ expr' → pat-lam (clauseExprToClauses expr') []) <$> expr) - - currentTyConstrPatterns : M (List SinglePattern) - currentTyConstrPatterns = do - (ty ∷ _ , _) ← viewTy′ <$> goalTy - where _ → error1 "currentTyConstrPatterns: Goal type is not a forall!" - constructorPatterns' (unArg ty) - -stripMetaLambdas : Term → Term -stripMetaLambdas = helper 0 - where - helper : ℕ → Term → Term - helper k (lam _ (abs _ t)) = helper (k + 1) t - helper k (meta x as) = meta x $ map-Args (mapVars (_∸ k)) $ take (length as ∸ k) as - helper _ _ = unknown - -module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ where - - isProj : Pattern → Bool - isProj (Pattern.proj _) = true - isProj _ = false - - -- if the goal is of type (a : A) → B, return the type of the branch of pattern p and new context - specializeType : SinglePattern → Type → M (Type × Telescope) - specializeType p@(t , arg i p') goalTy = inDebugPath "specializeType" $ runAndReset do - debugLog ("Goal type to specialize: " ∷ᵈ goalTy ∷ᵈ []) - cls@((Clause.clause tel _ _) ∷ _) ← return $ clauseExprToClauses $ MatchExpr $ - (p , inj₂ (just unknown)) ∷ - (if isProj p' then [] else [ varSinglePattern (arg i "_") , inj₂ (just unknown) ]) - where _ → error1 "BUG" - debugLog ("With pattern: " ∷ᵈ cls ∷ᵈ []) - debugLog (showPattern p' ∷ᵈ []) - (pat-lam (cl@(Clause.clause tel' _ (meta x ap)) ∷ _) []) ← checkType (pat-lam cls []) goalTy - where t → debugLog ("BUG in specializeType:" ∷ᵈ t ∷ᵈ "\nWith pattern:" ∷ᵈ cls - ∷ᵈ "\nWith type:" ∷ᵈ goalTy ∷ᵈ "\nSinglePattern:" -- ∷ᵈ {!p!} - ∷ᵈ []) >> error1 "BUG" - let varsToUnbind = 0 - let newCtx = tel' - let m = meta x (map-Args (mapVars (_∸ varsToUnbind)) $ take (length ap ∸ varsToUnbind) ap) - debugLog1 "New context:" - logContext newCtx - goalTy' ← extendContext' newCtx $ inferType m - return (goalTy' , newCtx) - - ContextMonad-MonadTC : ContextMonad M - ContextMonad-MonadTC .introPatternM pat@(_ , arg _ p) x = do - goalTy ← goalTy - (newGoalTy , newContext) ← specializeType pat goalTy - extendContext' newContext (runWithGoalTy newGoalTy x) - -module ClauseExprM {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ _ : ContextMonad M ⦄ where - - instance _ = Functor-M {M = M} - - -- Construct a ClauseExpr in M and extend the context appropriately - matchExprM : List (SinglePattern × M (ClauseExpr ⊎ Maybe Term)) → M ClauseExpr - matchExprM = _<$>_ MatchExpr ∘ traverse (λ (a , b) → (a ,_) <$> introPatternM a b) - - multiMatchExprM : List (NE.List⁺ SinglePattern × M (ClauseExpr ⊎ Maybe Term)) → M ClauseExpr - multiMatchExprM = matchExprM ∘ Data.List.map helper - where - helper' : (List SinglePattern × M (ClauseExpr ⊎ Maybe Term)) → M (ClauseExpr ⊎ Maybe Term) - helper' ([] , e) = e - helper' (p ∷ ps , e) = inj₁ <$> (matchExprM [ p , helper' (ps , e) ]) - - helper : (NE.List⁺ SinglePattern × M (ClauseExpr ⊎ Maybe Term)) → SinglePattern × M (ClauseExpr ⊎ Maybe Term) - helper (p NE.∷ ps , e) = (p , helper' (ps , e)) - - singleMatchExpr : SinglePattern → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr - singleMatchExpr p x = matchExprM [ p , x ] - - singleTelescopeMatchExpr : NE.List⁺ SinglePattern → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr - singleTelescopeMatchExpr (p NE.∷ ps) x = helper p ps x - where - helper : SinglePattern → List SinglePattern → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr - helper p [] x = singleMatchExpr p x - helper p (p' ∷ ps) x = singleMatchExpr p $ inj₁ <$> helper p' ps x - - introExpr : Arg String → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr - introExpr n x = singleMatchExpr (varSinglePattern n) x - - introsExpr : NE.List⁺ (Arg String) → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr - introsExpr (p NE.∷ ps) x = helper p ps x - where - helper : Arg String → List (Arg String) → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr - helper n [] x = introExpr n x - helper n (n' ∷ ns) x = introExpr n $ inj₁ <$> helper n ns x - - contMatch : M ClauseExpr → M (ClauseExpr ⊎ Maybe Term) - contMatch expr = inj₁ <$> expr - - finishMatch : M Term → M (ClauseExpr ⊎ Maybe Term) - finishMatch t = (inj₂ ∘ just) <$> t - - bindCtxMatchExpr : ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ - → M ClauseExpr → M ClauseExpr - bindCtxMatchExpr x = do - e ← ctxSinglePatterns - case NE.fromList e of λ where - (just e') → singleTelescopeMatchExpr e' $ contMatch x - nothing → x - -clauseTelescope : Clause → List (String × Arg Type) -clauseTelescope (Clause.clause tel _ _) = tel -clauseTelescope (Clause.absurd-clause tel _) = tel - -module _ where - open ClauseExprM ⦃ Monad-Id ⦄ ⦃ ContextMonad-Id ⦄ - - instanciatePattern : SinglePattern → List (Arg Type) - instanciatePattern p = proj₂ <$> - (clauseTelescope $ from-just $ head $ clauseExprToClauses $ singleMatchExpr p $ finishMatch unknown) - - instanciatePatterns : List SinglePattern → Term → List Clause - instanciatePatterns [] t = [ Clause.clause [] [] t ] - instanciatePatterns (x ∷ ps) t = - clauseExprToClauses $ singleTelescopeMatchExpr (x NE.∷ ps) (finishMatch t) - -ctxBindingClause : Term → TC Clause -ctxBindingClause t = do - pats ← ctxSinglePatterns - (c ∷ _) ← return $ instanciatePatterns (reverse pats) t - where _ → error1 "Bug in ctxBindingClause" - return c +record ClauseBuilder (M : Set → Set) : Set₁ where + field + Base : Set → Set + liftBase : Base A → M A + addPattern : List (String × Arg Type) → Arg Pattern → M A → M A + toClause : M (Maybe Term) → Base Clause + +open ClauseBuilder {{...}} public + +SinglePattern : Set +SinglePattern = List (String × Arg Type) × Arg Pattern + +typedVarSinglePattern : String → Arg Type → SinglePattern +typedVarSinglePattern n t@(arg i _) = ([ n , t ] , arg i (` 0)) + +varSinglePattern : Arg String → SinglePattern +varSinglePattern (arg i n) = ([ n , arg i unknown ] , arg i (` 0)) + +multiSinglePattern : List String → Arg Pattern → SinglePattern +multiSinglePattern s p = ((_, vArg unknown) <$> s) , p + +findIndexDefault : List ℕ → ℕ → ℕ → ℕ +findIndexDefault l d a with filter (λ where (i , x) → x ≟ a) (zipWithIndex _,_ l) +... | [] = d +... | (i , _) ∷ _ = i + +singlePatternFromPattern : Arg Pattern → SinglePattern +singlePatternFromPattern (arg i p) = + replicate (length (appearingIndices p)) ("" , vArg unknown) , arg i (replacePatternIndex p) + where + appearingIndices : Pattern → List ℕ + appearingIndicesHelper : List (Arg Pattern) → List ℕ + + appearingIndices (Pattern.con c ps) = appearingIndicesHelper ps + appearingIndices (Pattern.dot t) = [] -- TODO: this is probably wrong + appearingIndices (` x) = [ x ] + appearingIndices (Pattern.lit l) = [] + appearingIndices (Pattern.proj f) = [] + appearingIndices (Pattern.absurd x) = [] + + appearingIndicesHelper [] = [] + appearingIndicesHelper (arg _ p ∷ ps) = appearingIndices p ++ appearingIndicesHelper ps + + normalisedIndexList : List ℕ + normalisedIndexList = sort $ deduplicate _≟_ $ appearingIndices p + + replacePatternIndex : Pattern → Pattern + replacePatternIndexHelper : List (Arg Pattern) → List (Arg Pattern) + + replacePatternIndex (Pattern.con c ps) = Pattern.con c (replacePatternIndexHelper ps) + replacePatternIndex (Pattern.dot t) = Pattern.dot t + replacePatternIndex (` x) = ` findIndexDefault normalisedIndexList 0 x + replacePatternIndex (Pattern.lit l) = Pattern.lit l + replacePatternIndex (Pattern.proj f) = Pattern.proj f + replacePatternIndex (Pattern.absurd x) = Pattern.absurd x + + replacePatternIndexHelper [] = [] + replacePatternIndexHelper (arg i p ∷ ps) = (arg i (replacePatternIndex p)) ∷ (replacePatternIndexHelper ps) + +module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ where + + instance _ = Functor-M {M = M} + + ctxSinglePatterns : M (List SinglePattern) + ctxSinglePatterns = do + ctx ← getContext + return (singlePatternFromPattern <$> zipWithIndex (λ where k (_ , (arg i _)) → arg i (` k)) ctx) + + -- TODO: add the ability to match initial hidden arguments + -- TODO: add dot patterns + constrToPattern : Name → Type → M SinglePattern + constrToPattern n ty = do + (introTel , _) ← viewTy <$> (runAndReset $ local (λ env → record env { normalisation = true }) $ inferType (n ◆)) + let patternTel = zipWith (λ where (abs _ (arg i _)) k → arg i (` k)) introTel $ downFrom $ length introTel + return (((λ where (abs s (arg i t)) → (s , arg i unknown)) <$> introTel) , (vArg $ Pattern.con n patternTel)) + + -- like constrToPattern, but applied to parameters + constrToPatternTyped : Name → List Term → M SinglePattern + constrToPatternTyped n ps = do + t ← applyWithVisibility n ps + debugLogᵐ (t ᵛⁿ ∷ᵈᵐ []ᵐ) + (introTel , _) ← viewTy <$> (local (λ env → record env { normalisation = true }) $ inferType t) + let patternTel = zipWith (λ where (abs _ (arg i _)) k → arg i (` k)) introTel $ downFrom $ length introTel + return (((λ where (abs s (arg i t)) → (s , arg i t)) <$> introTel) , (vArg $ Pattern.con n patternTel)) + + -- all possible patterns for an inductive type + constructorPatterns : Arg Type → M (List SinglePattern) + constructorPatterns (arg i ty) = do + constrs ← getConstrsForType ty + return $ constrs <&> λ where + (n , t) → let argInfo = proj₁ $ viewTy t + in (((λ where (abs n' t') → n' , t') <$> argInfo) + , arg i (Pattern.con n (zipWithIndex (λ where k (abs _ (arg i _)) → arg i (` (length argInfo ∸ ℕ.suc k))) argInfo))) + + -- all possible patterns for an inductive type + constructorPatterns' : Type → M (List SinglePattern) + constructorPatterns' ty = do + constrs ← getConstrsForType ty + traverse (λ (n , _) → constrToPattern n ty) constrs + + -- all possible patterns for an inductive type + constructorPatternsTyped : Type → List Type → M (List SinglePattern) + constructorPatternsTyped ty ps = do + constrs ← getConstrsForType ty + traverse (λ (n , _) → constrToPatternTyped n ps) constrs + +ClauseInfo : Set +ClauseInfo = List SinglePattern + +data ClauseExpr : Set where + MatchExpr : List (SinglePattern × (ClauseExpr ⊎ Maybe Term)) → ClauseExpr + +multiClauseExpr : List (NE.List⁺ SinglePattern × (ClauseExpr ⊎ Maybe Term)) → ClauseExpr +multiClauseExpr = MatchExpr ∘ Data.List.map helper + where + helper' : (List SinglePattern × (ClauseExpr ⊎ Maybe Term)) → ClauseExpr ⊎ Maybe Term + helper' ([] , e) = e + helper' (p ∷ ps , e) = inj₁ (MatchExpr [ p , helper' (ps , e) ]) + + helper : (NE.List⁺ SinglePattern × (ClauseExpr ⊎ Maybe Term)) → SinglePattern × (ClauseExpr ⊎ Maybe Term) + helper (p NE.∷ ps , e) = p , helper' (ps , e) + +clauseExprToClauseInfo : ClauseExpr → List (ClauseInfo × Maybe Term) +clauseExprToClauseInfo (MatchExpr []) = [] +clauseExprToClauseInfo (MatchExpr ((p , inj₁ e) ∷ xs)) = + (map₁ (p ∷_) <$> clauseExprToClauseInfo e) ++ clauseExprToClauseInfo (MatchExpr xs) +clauseExprToClauseInfo (MatchExpr ((p , inj₂ t) ∷ xs)) = ([ p ] , t) ∷ clauseExprToClauseInfo (MatchExpr xs) + +clauseInfoToClauseArgs : ClauseInfo → List (String × Arg Type) × List (Arg Pattern) +clauseInfoToClauseArgs i = + case helper 0 i of λ where (tel , ps , _) → (tel , ps) + where + helper : ℕ → ClauseInfo → List (String × Arg Type) × List (Arg Pattern) × ℕ + helper k [] = ([] , [] , k) + helper k ((tel' , arg h p) ∷ i) with helper k i + ... | (tel , ps , k') = (tel' ++ tel , arg h (mapVariables (_+ k') p) ∷ ps , length tel' + k') + +clauseInfoToClause : ClauseInfo → Maybe Term → Clause +clauseInfoToClause i t with clauseInfoToClauseArgs i | t +... | tel , ps | just x = Clause.clause tel ps x +... | tel , ps | nothing = Clause.absurd-clause tel ps + +clauseExprToClauses : ClauseExpr → List Clause +clauseExprToClauses e = (λ { (i , t) → clauseInfoToClause i t }) <$> clauseExprToClauseInfo e + +nonBindingClause : Term → Clause +nonBindingClause = Clause.clause [] [] + +clauseExprToPatLam : ClauseExpr → Term +clauseExprToPatLam e = pat-lam (clauseExprToClauses e) [] + +record ContextMonad (M : ∀ {a} → Set a → Set a) ⦃ _ : Monad M ⦄ : Setω where + field + introPatternM : SinglePattern → M A → M A + + extendContextM : Arg Type → M A → M A + extendContextM l x = introPatternM (typedVarSinglePattern "" l) x + +open ContextMonad ⦃...⦄ + +Monad-Id : Monad id +Monad-Id .return = id +Monad-Id ._>>=_ = flip _$_ + +-- No context +ContextMonad-Id : ContextMonad id ⦃ Monad-Id ⦄ +ContextMonad-Id .introPatternM _ a = a + +module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ where + + instance _ = Functor-M {M = M} + + refineWithSingle : (Term → Term) → M Term → M Term + refineWithSingle ref x = do + goalTy ← goalTy + m ← newMeta unknown + res ← checkType (ref m) goalTy + x' ← runWithHole m x + unify m x' + return $ ref x' + + caseMatch : Term → M ClauseExpr → M Term + caseMatch t expr = debugLog ("Match" ∷ᵈ t ∷ᵈ []) >> (refineWithSingle (quote case_of_ ∙⟦ t ∣_⟧) $ + (λ expr' → pat-lam (clauseExprToClauses expr') []) <$> expr) + + currentTyConstrPatterns : M (List SinglePattern) + currentTyConstrPatterns = do + (ty ∷ _ , _) ← viewTy′ <$> goalTy + where _ → error1 "currentTyConstrPatterns: Goal type is not a forall!" + constructorPatterns' (unArg ty) + +stripMetaLambdas : Term → Term +stripMetaLambdas = helper 0 + where + helper : ℕ → Term → Term + helper k (lam _ (abs _ t)) = helper (k + 1) t + helper k (meta x as) = meta x $ map-Args (mapVars (_∸ k)) $ take (length as ∸ k) as + helper _ _ = unknown + +module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ where + + isProj : Pattern → Bool + isProj (Pattern.proj _) = true + isProj _ = false + + -- if the goal is of type (a : A) → B, return the type of the branch of pattern p and new context + specializeType : SinglePattern → Type → M (Type × Telescope) + specializeType p@(t , arg i p') goalTy = inDebugPath "specializeType" $ runAndReset do + debugLog ("Goal type to specialize: " ∷ᵈ goalTy ∷ᵈ []) + cls@((Clause.clause tel _ _) ∷ _) ← return $ clauseExprToClauses $ MatchExpr $ + (p , inj₂ (just unknown)) ∷ + (if isProj p' then [] else [ varSinglePattern (arg i "_") , inj₂ (just unknown) ]) + where _ → error1 "BUG" + debugLog ("With pattern: " ∷ᵈ cls ∷ᵈ []) + (pat-lam (cl@(Clause.clause tel' _ (meta x ap)) ∷ _) []) ← checkType (pat-lam cls []) goalTy + where t → debugLog ("BUG in specializeType:" ∷ᵈ t ∷ᵈ "\nWith pattern:" ∷ᵈ cls + ∷ᵈ "\nWith type:" ∷ᵈ goalTy ∷ᵈ "\nSinglePattern:" -- ∷ᵈ {!p!} + ∷ᵈ []) >> error1 "BUG" + let varsToUnbind = 0 + let newCtx = tel' + let m = meta x (map-Args (mapVars (_∸ varsToUnbind)) $ take (length ap ∸ varsToUnbind) ap) + debugLog1 "New context:" + logContext newCtx + goalTy' ← extendContext' newCtx $ inferType m + return (goalTy' , newCtx) + + ContextMonad-MonadTC : ContextMonad M + ContextMonad-MonadTC .introPatternM pat@(_ , arg _ p) x = do + goalTy ← goalTy + (newGoalTy , newContext) ← specializeType pat goalTy + extendContext' newContext (runWithGoalTy newGoalTy x) + +module ClauseExprM {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ _ : ContextMonad M ⦄ where + + instance _ = Functor-M {M = M} + + -- Construct a ClauseExpr in M and extend the context appropriately + matchExprM : List (SinglePattern × M (ClauseExpr ⊎ Maybe Term)) → M ClauseExpr + matchExprM = _<$>_ MatchExpr ∘ traverse (λ (a , b) → (a ,_) <$> introPatternM a b) + + multiMatchExprM : List (NE.List⁺ SinglePattern × M (ClauseExpr ⊎ Maybe Term)) → M ClauseExpr + multiMatchExprM = matchExprM ∘ Data.List.map helper + where + helper' : (List SinglePattern × M (ClauseExpr ⊎ Maybe Term)) → M (ClauseExpr ⊎ Maybe Term) + helper' ([] , e) = e + helper' (p ∷ ps , e) = inj₁ <$> (matchExprM [ p , helper' (ps , e) ]) + + helper : (NE.List⁺ SinglePattern × M (ClauseExpr ⊎ Maybe Term)) → SinglePattern × M (ClauseExpr ⊎ Maybe Term) + helper (p NE.∷ ps , e) = (p , helper' (ps , e)) + + singleMatchExpr : SinglePattern → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr + singleMatchExpr p x = matchExprM [ p , x ] + + singleTelescopeMatchExpr : NE.List⁺ SinglePattern → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr + singleTelescopeMatchExpr (p NE.∷ ps) x = helper p ps x + where + helper : SinglePattern → List SinglePattern → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr + helper p [] x = singleMatchExpr p x + helper p (p' ∷ ps) x = singleMatchExpr p $ inj₁ <$> helper p' ps x + + introExpr : Arg String → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr + introExpr n x = singleMatchExpr (varSinglePattern n) x + + introsExpr : NE.List⁺ (Arg String) → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr + introsExpr (p NE.∷ ps) x = helper p ps x + where + helper : Arg String → List (Arg String) → M (ClauseExpr ⊎ Maybe Term) → M ClauseExpr + helper n [] x = introExpr n x + helper n (n' ∷ ns) x = introExpr n $ inj₁ <$> helper n ns x + + contMatch : M ClauseExpr → M (ClauseExpr ⊎ Maybe Term) + contMatch expr = inj₁ <$> expr + + finishMatch : M Term → M (ClauseExpr ⊎ Maybe Term) + finishMatch t = (inj₂ ∘ just) <$> t + + bindCtxMatchExpr : ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ + → M ClauseExpr → M ClauseExpr + bindCtxMatchExpr x = do + e ← ctxSinglePatterns + case NE.fromList e of λ where + (just e') → singleTelescopeMatchExpr e' $ contMatch x + nothing → x + +clauseTelescope : Clause → List (String × Arg Type) +clauseTelescope (Clause.clause tel _ _) = tel +clauseTelescope (Clause.absurd-clause tel _) = tel + +module _ where + open ClauseExprM ⦃ Monad-Id ⦄ ⦃ ContextMonad-Id ⦄ + + instanciatePattern : SinglePattern → List (Arg Type) + instanciatePattern p = proj₂ <$> + (clauseTelescope $ from-just $ head $ clauseExprToClauses $ singleMatchExpr p $ finishMatch unknown) + + instanciatePatterns : List SinglePattern → Term → List Clause + instanciatePatterns [] t = [ Clause.clause [] [] t ] + instanciatePatterns (x ∷ ps) t = + clauseExprToClauses $ singleTelescopeMatchExpr (x NE.∷ ps) (finishMatch t) + +ctxBindingClause : Term → TC Clause +ctxBindingClause t = do + pats ← ctxSinglePatterns + (c ∷ _) ← return $ instanciatePatterns (reverse pats) t + where _ → error1 "Bug in ctxBindingClause" + return c \ No newline at end of file diff --git a/Tactic.Derive.DecEq.html b/Tactic.Derive.DecEq.html index a3988bb..f64d614 100644 --- a/Tactic.Derive.DecEq.html +++ b/Tactic.Derive.DecEq.html @@ -35,9 +35,9 @@ open import Tactic.Derive (quote DecEq) (quote _≟_) instance - _ = ContextMonad-MonadTC + _ = ContextMonad-MonadTC -open ClauseExprM +open ClauseExprM `yes `no : Term → Term `yes x = quote _because_ ◆⟦ quote true ◆ ∣ quote ofʸ ◆⟦ x ⟧ ⟧ @@ -60,12 +60,12 @@ ... | nothing = quote _≟_ ∙⟦ t ∣ t' ⟧ eqFromTerm _ t t' = quote _≟_ ∙⟦ t ∣ t' ⟧ - toDecEqName : SinglePattern → List (Term → Term → Term) + toDecEqName : SinglePattern → List (Term → Term → Term) toDecEqName (l , _) = L.map (λ where (_ , arg _ t) → eqFromTerm t) l -- on the diagonal we have one pattern, outside we don't care -- assume that the types in the pattern are properly normalized - mapDiag : Maybe SinglePattern → TC Term + mapDiag : Maybe SinglePattern → TC Term mapDiag nothing = return $ `no `λ⦅ [ ("" , vArg?) ] ⦆∅ mapDiag (just p@(l , _)) = let k = length l in do typeList ← traverse ⦃ Functor-List ⦄ inferType (applyDownFrom ♯ (length l)) @@ -87,9 +87,9 @@ reflTerm 0 = quote tt ◆ reflTerm (suc n) = quote _,_ ◆⟦ reflTerm n ∣ quote refl ◆ ⟧ - toMapDiag : SinglePattern → SinglePattern → NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term) + toMapDiag : SinglePattern → SinglePattern → NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term) toMapDiag p@(_ , arg _ p₁) p'@(_ , arg _ p₂) = - (p NE.∷ [ p' ] , finishMatch (if ⌊ p₁ ≟-Pattern p₂ ⌋ then mapDiag (just p) else mapDiag nothing)) + (p NE.∷ [ p' ] , finishMatch (if ⌊ p₁ ≟-Pattern p₂ ⌋ then mapDiag (just p) else mapDiag nothing)) module _ ⦃ _ : TCOptions ⦄ where derive-DecEq : List (Name × Name) → UnquoteDecl diff --git a/Tactic.Derive.Show.html b/Tactic.Derive.Show.html index 24f95a0..c48e8c2 100644 --- a/Tactic.Derive.Show.html +++ b/Tactic.Derive.Show.html @@ -28,9 +28,9 @@ open import Tactic.Derive (quote Show) (quote show) instance - _ = ContextMonad-MonadTC + _ = ContextMonad-MonadTC -open ClauseExprM +open ClauseExprM sLit = Term.lit ∘ Agda.Builtin.Reflection.Literal.string @@ -57,8 +57,8 @@ genShow n [] = sLit (showName n) genShow n (x ∷ l) = quote _<+>_ ∙⟦ genShow n l ∣ genPars x ⟧ - patternToClause : SinglePattern → NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term) - patternToClause p@(l , arg _ (Pattern.con n _)) = NE.[ p ] , finishMatch do + patternToClause : SinglePattern → NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term) + patternToClause p@(l , arg _ (Pattern.con n _)) = NE.[ p ] , finishMatch do typeList ← traverse ⦃ Functor-List ⦄ (λ t → do T ← inferType t; return (T , t)) (applyDownFrom ♯ (length l)) return $ genShow n (L.map (uncurry showFromTerm) $ reverse typeList) patternToClause p = NE.[ p ] , error1 "Error: not a con!" diff --git a/Tactic.Derive.html b/Tactic.Derive.html index 427b57c..3c4cd2b 100644 --- a/Tactic.Derive.html +++ b/Tactic.Derive.html @@ -43,11 +43,11 @@ open import Class.Traversable instance - _ = ContextMonad-MonadTC + _ = ContextMonad-MonadTC _ = Functor-M _ = Show-List -open ClauseExprM +open ClauseExprM -- generate the type of the `className dName` instance genClassType : ℕ → Name → Maybe Name → TC Type @@ -106,7 +106,7 @@ then just n' else nothing helper _ = nothing -module _ (arity : ℕ) (genCe : (Name → Maybe Name) → List SinglePattern → List (NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term))) where +module _ (arity : ℕ) (genCe : (Name → Maybe Name) → List SinglePattern → List (NE.List⁺ SinglePattern × TC (ClauseExpr ⊎ Maybe Term))) where -- Generate the declaration & definition of a particular derivation. -- -- Takes a dictionary (for mutual recursion), a wrapper (also for @@ -116,14 +116,14 @@ deriveSingle transName dName iName wName = inDebugPath "DeriveSingle" do debugLog ("For: " ∷ᵈ dName ∷ᵈ []) goalTy ← genClassType arity dName wName - ps ← constructorPatterns' (fromMaybe dName wName ∙) + ps ← constructorPatterns' (fromMaybe dName wName ∙) -- TODO: find a good way of printing this --debugLogᵐ ("Constrs: " ∷ᵈᵐ ps ᵛⁿ ∷ᵈᵐ []ᵐ) cs ← local (λ c → record c { goal = inj₂ goalTy }) $ - singleMatchExpr ([] , iArg (Pattern.proj projName)) $ contMatch $ multiMatchExprM $ + singleMatchExpr ([] , iArg (Pattern.proj projName)) $ contMatch $ multiMatchExprM $ genCe (lookupName transName) ps let defName = maybe (maybe vArg (iArg iName) ∘ lookupName transName) (iArg iName) wName - return (defName , goalTy , clauseExprToClauses cs) + return (defName , goalTy , clauseExprToClauses cs) deriveMulti : Name × Name × List Name → TC (List (Arg Name × Type × List Clause)) deriveMulti (dName , iName , hClasses) = do diff --git a/typecheck.time b/typecheck.time index b25a7a3..68025c6 100644 --- a/typecheck.time +++ b/typecheck.time @@ -1,11 +1,11 @@ -TOTAL: 3m17s -Algebra/Function: 0m9s -Meta/Prelude: 1m14s -Class/MonadError: 0m46s -Class/MonadReader: 0m0s +TOTAL: 0m38s +Algebra/Function: 0m1s +Meta/Prelude: 0m4s +Class/MonadError: 0m3s +Class/MonadReader: 0m1s Reflection/Syntax: 0m0s Reflection/Debug: 0m0s -Class/MonadTC: 0m11s +Class/MonadTC: 0m2s Reflection/TCI: 0m0s Meta/Init: 0m0s Reflection/Tactic: 0m0s @@ -14,9 +14,9 @@ Reflection/Utils/Debug: 0m0s Class/MonadError/Instances: 0m0s Class/MonadReader/Instances: 0m0s Class/MonadTC/Instances: 0m0s -Reflection/Utils/TCI: 0m3s +Reflection/Utils/TCI: 0m4s Reflection/Utils/TCM: 0m0s -Reflection/AlphaEquality: 0m1s +Reflection/AlphaEquality: 0m0s Reflection/AntiUnification: 0m0s Tactic/Try: 0m1s Tactic/Rewrite: 0m1s @@ -24,18 +24,18 @@ Tactic/Extra: 0m1s Tactic/Existentials: 0m0s Tactic/ByEq: 0m0s Tactic/AnyOf: 0m0s -Tactic/Defaults: 0m0s +Tactic/Defaults: 0m1s Tactic/Assumption: 0m0s -Tactic/ClauseBuilder: 0m32s +Tactic/ClauseBuilder: 0m3s Tactic/Case: 0m0s Tactic/Constrs: 0m0s Tactic/EquationalReasoning: 0m1s Tactic/Eta: 0m0s -Tactic/Intro: 0m1s -Tactic/ReduceDec: 0m0s +Tactic/Intro: 0m0s +Tactic/ReduceDec: 0m1s Tactic/Derive: 0m1s -Tactic/Derive/TestTypes: 0m1s -Tactic/Derive/DecEq: 0m7s -Tactic/Derive/Show: 0m2s +Tactic/Derive/TestTypes: 0m0s +Tactic/Derive/DecEq: 0m6s +Tactic/Derive/Show: 0m3s Tactic: 0m0s standard-library-meta: 0m0s