diff --git a/Class/MonadTC.agda b/Class/MonadTC.agda index 6bc3bb0..b2278d5 100644 --- a/Class/MonadTC.agda +++ b/Class/MonadTC.agda @@ -12,6 +12,8 @@ open import Reflection.Syntax open import Reflection.Debug +open import Class.Show +open import Class.DecEq open import Class.MonadReader open import Class.MonadError open import Class.Functor @@ -135,6 +137,61 @@ record MonadTC (M : ∀ {f} → Set f → Set f) where _ → error ("Not a record!" ∷ᵈ []) return $ con c args + isSolvedMeta : Term → M Bool + isSolvedMeta m@(meta x args) = do + r@(meta y _) ← reduce m + where _ → return true + return (x ≠ y) + isSolvedMeta _ = error ("Not a meta!" ∷ᵈ []) + + hasUnsolvedMetas : Term → M Bool + hasUnsolvedMetas' : List (Arg Term) → M Bool + hasUnsolvedMetasCl : List Clause → M Bool + hasUnsolvedMetasTel : Telescope → M Bool + + hasUnsolvedMetas (var x args) = hasUnsolvedMetas' args + hasUnsolvedMetas (con c args) = hasUnsolvedMetas' args + hasUnsolvedMetas (def f args) = hasUnsolvedMetas' args + hasUnsolvedMetas (lam v (abs _ t)) = hasUnsolvedMetas t + hasUnsolvedMetas (pat-lam cs args) = do + a ← hasUnsolvedMetasCl cs + b ← hasUnsolvedMetas' args + return (a ∨ b) + hasUnsolvedMetas (pi (arg _ a) (abs _ b)) = do + a ← hasUnsolvedMetas a + b ← hasUnsolvedMetas b + return (a ∨ b) + hasUnsolvedMetas (sort (set t)) = hasUnsolvedMetas t + hasUnsolvedMetas (sort (prop t)) = hasUnsolvedMetas t + hasUnsolvedMetas (sort unknown) = return true + hasUnsolvedMetas (sort _) = return false + hasUnsolvedMetas (lit l) = return false + hasUnsolvedMetas m@(meta x x₁) = not <$> isSolvedMeta m + hasUnsolvedMetas unknown = return false + + hasUnsolvedMetas' [] = return false + hasUnsolvedMetas' ((arg _ x) ∷ l) = do + a ← hasUnsolvedMetas x + b ← hasUnsolvedMetas' l + return (a ∨ b) + + hasUnsolvedMetasCl [] = return false + hasUnsolvedMetasCl (clause tel _ t ∷ cl) = do + a ← hasUnsolvedMetas t + b ← hasUnsolvedMetasTel tel + c ← hasUnsolvedMetasCl cl + return (a ∨ b ∨ c) + hasUnsolvedMetasCl (absurd-clause tel _ ∷ cl) = do + a ← hasUnsolvedMetasTel tel + b ← hasUnsolvedMetasCl cl + return (a ∨ b) + + hasUnsolvedMetasTel [] = return false + hasUnsolvedMetasTel ((_ , arg _ x) ∷ tel) = do + a ← hasUnsolvedMetas x + b ← hasUnsolvedMetasTel tel + return (a ∨ b) + -- this allows mutual recursion declareAndDefineFuns : List (Arg Name × Type × List Clause) → M ⊤ declareAndDefineFuns ds = do @@ -142,6 +199,20 @@ record MonadTC (M : ∀ {f} → Set f → Set f) traverse (λ where (arg _ n , _ , cs) → defineFun n cs) ds return _ + declareAndDefineFunsDebug : List (Arg Name × Type × List Clause) → M ⊤ + declareAndDefineFunsDebug ds = do + traverse (λ (n , t , _) → declareDef n t) ds + traverse (λ where (arg _ n , _ , _) → do + b ← getType n >>= hasUnsolvedMetas + if b then error [ strErr $ show n ] else return tt) ds + traverse (λ where (arg _ n , _ , cs) → defineFun n cs) ds + traverse (λ where (arg _ n , _ , _) → do + d@(function cs) ← getDefinition n + where _ → error [ strErr "Weird bug" ] + b ← hasUnsolvedMetasCl cs + if b then error [ strErr $ show d ] else return tt) ds + return _ + declareAndDefineFun : Arg Name → Type → List Clause → M ⊤ declareAndDefineFun n ty cls = declareAndDefineFuns [ (n , ty , cls) ] diff --git a/Reflection/Debug.agda b/Reflection/Debug.agda index 958b306..e67062d 100644 --- a/Reflection/Debug.agda +++ b/Reflection/Debug.agda @@ -33,6 +33,9 @@ instance IsErrorPart-Name : IsErrorPart Name IsErrorPart-Name .toErrorPart = ErrorPart.nameErr + IsErrorPart-Pattern : IsErrorPart Pattern + IsErrorPart-Pattern .toErrorPart = ErrorPart.pattErr + IsErrorPart-Clause : IsErrorPart Clause IsErrorPart-Clause .toErrorPart c = ErrorPart.termErr (pat-lam [ c ] []) diff --git a/Reflection/Utils.agda b/Reflection/Utils.agda index b4bb9bb..910f412 100644 --- a/Reflection/Utils.agda +++ b/Reflection/Utils.agda @@ -251,3 +251,9 @@ updateField fs rexp fn fexp = else clause [] [ vArg (proj f) ] (f ∙⟦ rexp ⟧) ) [] + +toTelescope : List (Abs (Arg Type)) → Telescope +toTelescope = map (λ where (abs n x) → (n , x)) + +fromTelescope : Telescope → List (Abs (Arg Type)) +fromTelescope = map (λ where (n , x) → (abs n x)) diff --git a/Reflection/Utils/TCI.agda b/Reflection/Utils/TCI.agda index efd8931..afae7a9 100644 --- a/Reflection/Utils/TCI.agda +++ b/Reflection/Utils/TCI.agda @@ -224,6 +224,9 @@ viewAndReduceTy ty = helper ty =<< (length ∘ proj₁ ∘ viewTy) <$> normalise getType' : Name → M TypeView getType' n = viewAndReduceTy =<< getType n +getTypeDB : ℕ → M TypeView +getTypeDB n = viewAndReduceTy =<< inferType (♯ n) + getDataDef : Name → M DataDef getDataDef n = inDebugPath "getDataDef" do debugLog ("Find details for datatype: " ∷ᵈ n ∷ᵈ []) @@ -268,11 +271,11 @@ isSort t = do where _ → return false return true -isNArySort : ℕ → Term → M Bool -isNArySort n t = do +isNArySort : Term → M (Bool × ℕ) +isNArySort t = do (tel , ty) ← viewAndReduceTy t b ← isSort ty - return (⌊ (length tel) ≟ n ⌋ ∧ b) + return (b , length tel) isDefT : Name → Term → M Bool isDefT n t = do @@ -293,8 +296,13 @@ withSafeReset x = runAndReset $ do debugLog ("In term: " ∷ᵈ t ∷ᵈ []) error1 "Unsolved metavariables remaining in withSafeReset!" --- apply a list of terms to a name, picking the correct constructor & visibility +-- apply a list of terms to a name, picking the correct constructor of the term datatype & visibility applyWithVisibility : Name → List Term → M Term applyWithVisibility n l = do (argTys , _) ← getType' n nameConstr n (zipWith (λ where (abs _ (arg i _)) → arg i) argTys l) + +applyWithVisibilityDB : ℕ → List Term → M Term +applyWithVisibilityDB n l = do + (argTys , _) ← getTypeDB n + return $ var n (zipWith (λ where (abs _ (arg i _)) → arg i) argTys l) diff --git a/Tactic/Assumption.agda b/Tactic/Assumption.agda index f92aa26..507e8e8 100644 --- a/Tactic/Assumption.agda +++ b/Tactic/Assumption.agda @@ -21,15 +21,6 @@ open import Reflection.Utils.TCI instance _ = Functor-M -solve : ⦃ TCOptions ⦄ → Term → Tactic -solve t = initTac $ runSpeculative $ do - inj₁ goal ← reader TCEnv.goal - where _ → error1 "solve: Goal is not a term!" - metas ← findMetas <$> checkType t goal - if null metas - then (_, true) <$> unify goal t - else (_, false) <$> error1 "Unsolved metavariables remaining!" - assumption' : ITactic assumption' = inDebugPath "assumption" do c ← getContext diff --git a/Tactic/ClauseBuilder.agda b/Tactic/ClauseBuilder.agda index 81b6bae..5eccb65 100644 --- a/Tactic/ClauseBuilder.agda +++ b/Tactic/ClauseBuilder.agda @@ -18,6 +18,7 @@ open SortingAlgorithm ≤-decTotalOrder (mergeSort ≤-decTotalOrder) public open import Reflection.Utils open import Reflection.Utils.TCI +open import Class.Show open import Class.DecEq open import Class.Functor open import Class.MonadError.Instances @@ -34,6 +35,8 @@ private variable a b : Level A : Set a +open import Data.String as S using (parens) + record ClauseBuilder (M : Set → Set) : Set₁ where field Base : Set → Set @@ -241,7 +244,7 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr -- 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 = markDontFail "specializeType" $ inDebugPath "specializeType" $ runAndReset do + 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)) ∷ @@ -261,7 +264,7 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr return (goalTy' , newCtx) ContextMonad-MonadTC : ContextMonad M - ContextMonad-MonadTC .introPatternM pat x = do + ContextMonad-MonadTC .introPatternM pat@(_ , arg _ p) x = do goalTy ← goalTy (newGoalTy , newContext) ← specializeType pat goalTy extendContext' newContext (runWithGoalTy newGoalTy x) diff --git a/Tactic/Derive.agda b/Tactic/Derive.agda index eb21f8a..889c104 100644 --- a/Tactic/Derive.agda +++ b/Tactic/Derive.agda @@ -34,39 +34,56 @@ open import Relation.Nullary.Decidable open import Tactic.ClauseBuilder open import Class.DecEq -open import Class.Monad -open import Class.Traversable open import Class.Functor +open import Class.Monad open import Class.MonadReader.Instances open import Class.MonadTC.Instances +open import Class.Show +open import Class.Traversable instance _ = ContextMonad-MonadTC _ = Functor-M + _ = Show-List open ClauseExprM +-- generate the type of the `className dName` instance genClassType : ℕ → Name → Maybe Name → TC Type genClassType arity dName wName = do params ← getParamsAndIndices dName - adjParams ← adjustParams $ take (length params ∸ arity) params + let params' = L.map (λ where (abs x y) → abs x (hide y)) $ take (length params ∸ arity) params + sorts ← collectRelevantSorts params' + debugLog1 ("Generate required instances at indices: " S.++ show (L.map proj₁ sorts)) + let adjustedDBs = L.zipWith (λ (i , tel) a → (i + a , tel)) sorts (upTo (length sorts)) + adjustedDBs' ← extendContext' (toTelescope params) $ genSortInstanceWithCtx adjustedDBs + let adjParams = params' ++ adjustedDBs' debugLog1 "AdjustedParams: " - logTelescope (L.map ((λ where (abs s x) → just s , x) ∘ proj₁) adjParams) - ty ← applyWithVisibility dName (L.map ♯ (trueIndices adjParams)) - return $ modifyClassType wName (L.map proj₁ adjParams , ty) + logTelescope (L.map ((λ where (abs s x) → just s , x)) adjParams) + ty ← applyWithVisibility dName (L.map (♯ ∘ (_+ length sorts)) (downFrom (length params))) + return $ modifyClassType wName (adjParams , ty) where - adjustParams : List (Abs (Arg Type)) → TC (List ((Abs (Arg Type)) × Bool)) - adjustParams [] = return [] - adjustParams (abs x (arg _ t) ∷ l) = do - a ← (if_then [ (abs "_" (iArg (className ∙⟦ ♯ 0 ⟧)) , false) ] else []) <$> isNArySort arity t - ps ← extendContext (x , hArg t) (adjustParams l) - let ps' = flip L.map ps λ where - (abs s (arg i t) , b) → (abs s (arg i (mapVars (_+ (if b then length a else 0)) t)) , b) - return (((abs x (hArg t) , true) ∷ a) ++ ps') - - trueIndices : {A : Set} → List (A × Bool) → List ℕ - trueIndices [] = [] - trueIndices (x ∷ l) = if proj₂ x then length l ∷ trueIndices l else trueIndices l + -- returns list of DB indices (at the end) and telescope of argument types + collectRelevantSorts : List (Abs (Arg Type)) → TC (List (ℕ × ℕ)) + collectRelevantSorts [] = return [] + collectRelevantSorts (abs x (arg _ t) ∷ l) = do + rec ← extendContext (x , hArg t) $ collectRelevantSorts l + (b , k) ← isNArySort t + return (if b then (length l , k) ∷ rec else rec) + + genSortInstance : ℕ → ℕ → ℕ → TC Term + genSortInstance k 0 i = do + res ← applyWithVisibilityDB (i + k) (L.map ♯ $ downFrom k) + return $ className ∙⟦ res ⟧ + genSortInstance k (suc a) i = do + res ← extendContext ("" , hArg unknown) $ genSortInstance k a i + return $ pi (hArg unknown) $ abs "_" res + + genSortInstanceWithCtx : List (ℕ × ℕ) → TC (List (Abs (Arg Term))) + genSortInstanceWithCtx [] = return [] + genSortInstanceWithCtx ((i , k) ∷ xs) = do + x' ← (abs "_" ∘ iArg) <$> (genSortInstance k k i) + (x' ∷_) <$> (extendContext ("", hArg unknown) $ genSortInstanceWithCtx xs) modifyClassType : Maybe Name → TypeView → Type modifyClassType nothing (tel , ty) = tyView (tel , className ∙⟦ ty ⟧) @@ -115,7 +132,7 @@ module _ (arity : ℕ) (genCe : (Name → Maybe Name) → List SinglePattern → derive-Class : ⦃ TCOptions ⦄ → List (Name × Name) → UnquoteDecl derive-Class l = initUnquoteWithGoal (className ∙) $ - declareAndDefineFuns =<< concat <$> traverse ⦃ Functor-List ⦄ helper l + declareAndDefineFuns =<< runAndReset (concat <$> traverse ⦃ Functor-List ⦄ helper l) where helper : Name × Name → TC (List (Arg Name × Type × List Clause)) helper (a , b) = do hs ← genMutualHelpers a ; deriveMulti (a , b , hs) diff --git a/Tactic/Derive/Show.agda b/Tactic/Derive/Show.agda index 326afe6..9cb9573 100644 --- a/Tactic/Derive/Show.agda +++ b/Tactic/Derive/Show.agda @@ -70,12 +70,15 @@ private open import Tactic.Derive.TestTypes import Data.Nat.Show open import Tactic.Defaults + open import Data.List.Relation.Binary.Pointwise.Base unquoteDecl Show-Bool Show-ℤ Show-List Show-Maybe Show-ℕ Show-Sign Show-⊤ = derive-Show ((quote Bool , Show-Bool) ∷ (quote ℤ , Show-ℤ) ∷ (quote List , Show-List) ∷ (quote Maybe , Show-Maybe) ∷ (quote ℕ , Show-ℕ) ∷ (quote Sign , Show-Sign) ∷ (quote ⊤ , Show-⊤) ∷ []) unquoteDecl Show-Fin = derive-Show [ (quote Fin , Show-Fin) ] unquoteDecl Show-Vec = derive-Show [ (quote Vec , Show-Vec) ] + unquoteDecl Show-Pointwise = derive-Show [ (quote Pointwise , Show-Pointwise) ] + unquoteDecl Show-These = derive-Show [ (quote These , Show-These) ] unquoteDecl Show-⊎ = derive-Show [ (quote _⊎_ , Show-⊎) ]