|
| 1 | +open import Agda.Core.Prelude |
| 2 | +open import Agda.Core.Name |
| 3 | +open import Agda.Core.Syntax |
| 4 | +open import Agda.Core.Reduce |
| 5 | +open import Agda.Core.Rules.Conversion |
| 6 | +open import Agda.Core.Rules.Typing |
| 7 | +open import Agda.Core.TCM.Instances |
| 8 | +open import Agda.Core.Checkers.Converter |
| 9 | + |
| 10 | + |
| 11 | +module Agda.Core.Checkers.Terminate |
| 12 | + {{@0 globals : Globals}} |
| 13 | + {{@0 sig : Signature}} |
| 14 | + where |
| 15 | + |
| 16 | +private open module @0 G = Globals globals |
| 17 | + |
| 18 | +private variable |
| 19 | + @0 x : Name |
| 20 | + @0 α : Scope Name |
| 21 | + @0 rβ : RScope Name |
| 22 | + |
| 23 | +data SubTermContext : @0 Scope Name → Set where |
| 24 | + StCtxEmpty : SubTermContext mempty |
| 25 | + StCtxExtend : (@0 x : Name) → Maybe (NameIn α) → SubTermContext α → SubTermContext (α ▸ x) -- here x, is a subterm of y. |
| 26 | +{-# COMPILE AGDA2HS SubTermContext #-} |
| 27 | + |
| 28 | +private -- it should use a RScope instead of β and then could be public |
| 29 | + raiseNameIn : {@0 α β : Scope Name} → Singleton β → NameIn α → NameIn (α <> β) |
| 30 | + raiseNameIn r n = weakenNameIn (subJoinDrop r subRefl) n |
| 31 | + {-# COMPILE AGDA2HS raiseNameIn #-} |
| 32 | + |
| 33 | + |
| 34 | +lookupSt : (Γ : SubTermContext α) (x : NameIn α) → Maybe (NameIn α) |
| 35 | +lookupSt StCtxEmpty x = nameInEmptyCase x |
| 36 | +lookupSt (StCtxExtend namesubterm nameparent c) name = case (nameInBindCase name |
| 37 | + (λ q → lookupSt c (⟨ _ ⟩ q)) |
| 38 | + (λ _ → nameparent)) of λ where |
| 39 | + (Just n) → Just (raiseNameIn (sing _) n) |
| 40 | + Nothing → Nothing |
| 41 | +{-# COMPILE AGDA2HS lookupSt #-} |
| 42 | + |
| 43 | +checkSubtermVar : SubTermContext α → NameIn α → NameIn α → Bool |
| 44 | +checkSubtermVar ctx (⟨ _ ⟩ ( param ⟨ _ ⟩)) arg = case (lookupSt ctx arg) of λ where |
| 45 | + (Just (⟨ _ ⟩ ( parent ⟨ _ ⟩))) → case (param == parent) of λ where |
| 46 | + True → True |
| 47 | + False → False -- this needs eventually to check recursively |
| 48 | + Nothing → False |
| 49 | +{-# COMPILE AGDA2HS checkSubtermVar #-} |
| 50 | + |
| 51 | +checkSubterm : SubTermContext α → NameIn α → Term α → Bool |
| 52 | +checkSubterm con param (TVar arg) = checkSubtermVar con param arg |
| 53 | +checkSubterm con name term = False |
| 54 | +{-# COMPILE AGDA2HS checkSubterm #-} |
| 55 | + |
| 56 | + |
| 57 | +-- At some point make the lists vecs for more security |
| 58 | +compareArgsToParams : SubTermContext α → List (NameIn α) → List (Term α) → List Bool |
| 59 | +compareArgsToParams con (param ∷ params) (arg ∷ args) = checkSubterm con param arg ∷ compareArgsToParams con params args |
| 60 | +compareArgsToParams _ _ _ = [] |
| 61 | +{-# COMPILE AGDA2HS compareArgsToParams #-} |
| 62 | + |
| 63 | +opaque |
| 64 | + unfolding RScope extScope |
| 65 | + updateEnv : SubTermContext α → (cs : RScope Name) → NameIn α → SubTermContext (extScope α cs) |
| 66 | + updateEnv env [] _ = env |
| 67 | + updateEnv env (Erased x ∷ s) name = updateEnv (StCtxExtend x (Just name) env) s (weakenNameIn (subWeaken subRefl) name) |
| 68 | + {-# COMPILE AGDA2HS updateEnv #-} |
| 69 | + |
| 70 | +{-# NON_TERMINATING #-} -- need to find a way to not need those |
| 71 | +handleBranches : ∀ {@0 d : NameData} {@0 cs : RScope (NameCon d)} → SubTermContext α → NameIn defScope → List (NameIn α) → NameIn α → (bs : Branches α d cs) → List Bool |
| 72 | + |
| 73 | +getDecreasingArgs : SubTermContext α → NameIn defScope → List (NameIn α) → Term α → List Bool |
| 74 | + |
| 75 | +handleBranches con funName params name BsNil = map (λ _ → True) params |
| 76 | +handleBranches {α} con funName params name (BsCons (BBranch (c ⟨ w ⟩ ) (fields ⟨ p ⟩ ) clause) branches) = |
| 77 | + zipWith (λ x y → x && y) |
| 78 | + (getDecreasingArgs (updateEnv con fields name) funName |
| 79 | + (map (weakenNameIn (subExtScope (sing fields) subRefl)) params) |
| 80 | + ( subst0 (λ f → Term (α ◂▸ f)) p clause )) |
| 81 | + (handleBranches con funName params name branches) |
| 82 | + |
| 83 | +{-# COMPILE AGDA2HS handleBranches #-} |
| 84 | + |
| 85 | + |
| 86 | +getDecreasingArgs con funName params (TApp u v) = case unApps (TApp u v) of λ where |
| 87 | + (fun , args) → zipWith (λ x y → x && y) (foldr (zipWith (λ x y → x && y)) (map (λ _ → True) params) (map (getDecreasingArgs con funName params) args)) (case fun of λ where |
| 88 | + (TDef d) → case (d == funName) of λ where |
| 89 | + True → compareArgsToParams con params args |
| 90 | + False → map (λ _ → True) params |
| 91 | + x → getDecreasingArgs con funName params x) |
| 92 | +getDecreasingArgs con funName params (TLam name body) = |
| 93 | + getDecreasingArgs (StCtxExtend name Nothing con) funName (map (weakenNameIn (subWeaken subRefl)) params) body |
| 94 | +getDecreasingArgs con funName params (TLet name body1 body2) = |
| 95 | + zipWith (λ x y → x && y) (getDecreasingArgs con funName params body1) |
| 96 | + (getDecreasingArgs (StCtxExtend name Nothing con) funName (map (weakenNameIn (subWeaken subRefl)) params) body2) |
| 97 | +getDecreasingArgs con funName params (TCase _ _ (TVar nameVar) branches _) = -- we only accept pattern matching on variable for now. |
| 98 | + handleBranches con funName params nameVar branches |
| 99 | +getDecreasingArgs _ _ params _ = map (λ _ → True) params |
| 100 | +{-# COMPILE AGDA2HS getDecreasingArgs #-} |
| 101 | + |
| 102 | +checkTermination : SubTermContext α → NameIn defScope → List (NameIn α) → Term α → Bool |
| 103 | +-- unfold the function to get all the arguments and build the env |
| 104 | +checkTermination c def params (TLam x body) = checkTermination (StCtxExtend x Nothing c) def ((map (weakenNameIn (subWeaken subRefl)) params) ++ ((⟨ x ⟩ Zero ⟨ IsZero refl ⟩) ∷ [])) body |
| 105 | +checkTermination c def params body = any id (getDecreasingArgs c def params body) |
| 106 | +{-# COMPILE AGDA2HS checkTermination #-} |
0 commit comments