git.iko.soy/Idris-dev
on master help sign in
Fix parameter identification in data declarations
442d8c8Edwin Brady
CHANGELOG+1
compare with master
unifiedsplit
@@ -14,6 +14,7 @@ User visible changes:
14
14
15Internal changes:
15Internal changes:
16
16
17+* Fix non-linear pattern checking
17* Improved name disambiguation
18* Improved name disambiguation
18* More flexible unification and elaboration of lambdas
19* More flexible unification and elaboration of lambdas
19* Various unification and totality checking bug fixes
20* Various unification and totality checking bug fixes
lib/Decidable/Equality.idr+1−1
@@ -75,7 +75,7 @@ total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _
75leftNotRight refl impossible
75leftNotRight refl impossible
76
76
77instance (DecEq a, DecEq b) => DecEq (Either a b) where
77instance (DecEq a, DecEq b) => DecEq (Either a b) where
78− decEq {b=b} (Left x') (Left y') with (decEq x' y')
78+ decEq (Left x') (Left y') with (decEq x' y')
79 | Yes p = Yes $ cong p
79 | Yes p = Yes $ cong p
80 | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h
80 | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h
81 decEq (Right x') (Right y') with (decEq x' y')
81 decEq (Right x') (Right y') with (decEq x' y')
src/Idris/ElabDecls.hs+48−27
@@ -147,7 +147,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
147 ttag <- getName
147 ttag <- getName
148 i <- getIState
148 i <- getIState
149 let as = map (const Nothing) (getArgTys cty)
149 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)
151 logLvl 2 $ "Parameters : " ++ show params
151 logLvl 2 $ "Parameters : " ++ show params
152 putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)
152 putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)
153 (idris_datatypes i) })
153 (idris_datatypes i) })
@@ -161,32 +161,53 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
161 where
161 where
162 -- parameters are names which are unchanged across the structure,
162 -- parameters are names which are unchanged across the structure,
163 -- which appear exactly once in the return type of a constructor
163 -- which appear exactly once in the return type of a constructor
164− findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]
164+
165− findParams ps [] = mapMaybe (\ ((x, y), n) ->
165+ -- First, find all applications of the constructor, then check over
166− if y then Just n else Nothing)
166+ -- them for repeated arguments
167− (zip ps [0..])
167+
168− findParams ps (t : ts) = findParams (updateParams ps t) ts
168+ findParams :: [Type] -> [Int]
169−
169+ findParams ts = let allapps = concatMap getDataApp ts in
170− updateParams ps (Bind n (Pi t) sc)
170+ paramPos allapps
171− = updateParams (updateParams ps (instantiate (P Bound n t) sc)) t
171+
172− updateParams ps tm@(App f a)
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 _ _)
173− | (P _ fn _, args) <- unApply tm
193+ | (P _ d _, args) <- unApply f
174− = if fn == n
194+ = if (d == n) then [mParam args args] else []
175− then updateParamsA ps args (tail args)
195+ getDataApp (Bind n (Pi t) sc)
176− else updateParams (updateParams ps f) a
196+ = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)
177− | otherwise = updateParams (updateParams ps f) a
197+ getDataApp _ = []
178− updateParams ps _ = ps
198+
179−
199+ -- keep the arguments which are single names, which don't appear
180− updateParamsA ((mn, _) : ns) (p@(P _ n' _) : args) all
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)
181− | n' `elem` concatMap freeNames all
208+ | n `elem` freeNames t = 1 + count n ts
182− = (mn, False) : updateParamsA ns args (p : all)
209+ | otherwise = count n ts
183− updateParamsA ((Nothing, b) : ns) (p@(P _ n' _) : args) all
210+ mParam args (_ : rest) = Nothing : mParam args rest
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
190
211
191-- | Elaborate a type provider
212-- | Elaborate a type provider
192elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
213elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()