@@ -147,7 +147,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
147147 ttag <- getName
148148 i <- getIState
149149 let as = map (const Nothing) (getArgTys cty)
150− let params = findParams (zip as (repeat True)) (map snd cons)
150+ let params = findParams (map snd cons)
151151 logLvl 2 $ "Parameters : " ++ show params
152152 putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)
153153 (idris_datatypes i) })
@@ -161,32 +161,53 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
161161 where
162162 -- parameters are names which are unchanged across the structure,
163163 -- which appear exactly once in the return type of a constructor
164− findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]
165− findParams ps [] = mapMaybe (\ ((x, y), n) ->
166− if y then Just n else Nothing)
167− (zip ps [0..])
168− findParams ps (t : ts) = findParams (updateParams ps t) ts
169−
170− updateParams ps (Bind n (Pi t) sc)
171− = updateParams (updateParams ps (instantiate (P Bound n t) sc)) t
172− updateParams ps tm@(App f a)
173− | (P _ fn _, args) <- unApply tm
174− = if fn == n
175− then updateParamsA ps args (tail args)
176− else updateParams (updateParams ps f) a
177− | otherwise = updateParams (updateParams ps f) a
178− updateParams ps _ = ps
179−
180− updateParamsA ((mn, _) : ns) (p@(P _ n' _) : args) all
181− | n' `elem` concatMap freeNames all
182− = (mn, False) : updateParamsA ns args (p : all)
183− updateParamsA ((Nothing, b) : ns) (p@(P _ n' _) : args) all
184− = (Just n', b) : updateParamsA ns args (p : all)
185− updateParamsA ((Just p, b) : ns) (tm@(P _ n' _) : args) all
186− = (Just n', b && p == n') : updateParamsA ns args (tm : all)
187− updateParamsA ((mn, _) : ns) (p : args) all
188− = (mn, False) : updateParamsA ns args (p : all)
189− updateParamsA ps args all = ps
164+
165+ -- First, find all applications of the constructor, then check over
166+ -- them for repeated arguments
167+
168+ findParams :: [Type] -> [Int]
169+ findParams ts = let allapps = concatMap getDataApp ts in
170+ paramPos allapps
171+
172+ paramPos [] = []
173+ paramPos (args : rest)
174+ = dropNothing $ keepSame (zip [0..] args) rest
175+
176+ dropNothing [] = []
177+ dropNothing ((x, Nothing) : ts) = dropNothing ts
178+ dropNothing ((x, _) : ts) = x : dropNothing ts
179+
180+ keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
181+ [(Int, Maybe Name)]
182+ keepSame as [] = as
183+ keepSame as (args : rest) = keepSame (update as args) rest
184+ where
185+ update [] _ = []
186+ update _ [] = []
187+ update ((n, Just x) : as) (Just x' : args)
188+ | x == x' = (n, Just x) : update as args
189+ update ((n, _) : as) (_ : args) = (n, Nothing) : update as args
190+
191+ getDataApp :: Type -> [[Maybe Name]]
192+ getDataApp f@(App _ _)
193+ | (P _ d _, args) <- unApply f
194+ = if (d == n) then [mParam args args] else []
195+ getDataApp (Bind n (Pi t) sc)
196+ = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)
197+ getDataApp _ = []
198+
199+ -- keep the arguments which are single names, which don't appear
200+ -- elsewhere
201+
202+ mParam args [] = []
203+ mParam args (P Bound n _ : rest)
204+ | count n args == 1
205+ = Just n : mParam args rest
206+ where count n [] = 0
207+ count n (t : ts)
208+ | n `elem` freeNames t = 1 + count n ts
209+ | otherwise = count n ts
210+ mParam args (_ : rest) = Nothing : mParam args rest
190211
191212-- | Elaborate a type provider
192213elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()