@@ -113,59 +113,6 @@ genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of
113113
114114upd p' p = p { getTm = p' }
115115
116−-- recursive calls are well-founded if one of their argument positions is
117−-- always decreasing. Return a list of arguments which are either not used
118−-- recursively, or always decreasing recursively
119−
120−-- If we encounter a non-total name, we'll fail
121−
122−wellFounded :: IState -> Name -> SC -> Totality
123−wellFounded i n sc = case wff [] sc of
124− RightOK smaller_args ->
125− -- is there a number in every list?
126− -- trace (show (n, smaller_args)) $
127− case smaller_args of
128− [] -> Total []
129− (x : xs) -> let args = foldl intersect x xs in
130− if (null args) then Partial Itself
131− else Total args
132− LeftErr x -> Partial (Other x)
133− where
134− wff :: [Name] -> SC -> EitherErr [Name] [[Int]]
135− wff ns (Case n as) = do is <- mapM (wffC ns) as
136− return $ concat is
137− where wffC ns (ConCase n i ns' sc) = do checkOK n
138− wff (ns ++ ns') sc
139− wffC ns (ConstCase _ sc) = wff ns sc
140− wffC ns (DefaultCase sc) = wff ns sc
141− wff ns (STerm t) = argPos ns t
142− wff ns _ = return []
143−
144− checkOK n' = case lookupTotal n' (tt_ctxt i) of
145− [Partial _] -> LeftErr [n']
146− [Total _] -> RightOK ()
147− x -> RightOK ()
148−
149− argPos ns ap@(App f' a')
150− | (P _ f _, args) <- unApply ap
151− = if f == n then
152− do aa <- argPos ns a'
153− return $ chkArgs 0 ns args : aa
154− else do checkOK f
155− argPos ns a'
156− argPos ns (App f a) = do f' <- argPos ns f
157− a' <- argPos ns a
158− return (f' ++ a')
159− argPos ns (Bind n (Let t v) sc) = do v' <- argPos ns v
160− sc' <- argPos ns sc
161− return (v' ++ sc')
162− argPos ns (Bind n _ sc) = argPos ns sc
163− argPos ns _ = return []
164−
165− chkArgs i ns [] = []
166− chkArgs i ns (P _ n _ : xs) | n `elem` ns = i : chkArgs (i + 1) ns xs
167− chkArgs i ns (_ : xs) = chkArgs (i+1) ns xs
168−
169116-- Check if, in a given type n, the constructor cn : ty is strictly positive,
170117-- and update the context accordingly
171118