git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Elab/Data.hs
539 lines 25 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Data(elabData) where
4import Idris.AbsSyntax
5import Idris.ASTUtils
6import Idris.DSL
7import Idris.Error
8import Idris.Delaborate
9import Idris.Imports
10import Idris.ElabTerm
11import Idris.Coverage
12import Idris.DataOpts
13import Idris.Providers
14import Idris.Primitives
15import Idris.Inliner
16import Idris.PartialEval
17import Idris.DeepSeq
18import Idris.Output (iputStrLn, pshow, iWarn)
19import IRTS.Lang
21import Idris.Elab.Type
22import Idris.Elab.Utils
23import Idris.Elab.Value
25import Idris.Core.TT
26import Idris.Core.Elaborate hiding (Tactic(..))
27import Idris.Core.Evaluate
28import Idris.Core.Execute
29import Idris.Core.Typecheck
30import Idris.Core.CaseTree
32import Idris.Docstrings
34import Prelude hiding (id, (.))
35import Control.Category
37import Control.Applicative hiding (Const)
38import Control.DeepSeq
39import Control.Monad
40import Control.Monad.State.Strict as State
41import Data.List
42import Data.Maybe
43import Debug.Trace
45import qualified Data.Map as Map
46import qualified Data.Set as S
47import qualified Data.Text as T
48import Data.Char(isLetter, toLower)
49import Data.List.Split (splitOn)
51import Util.Pretty(pretty, text)
53elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()
54elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
55 = do let codata = Codata `elem` opts
56 iLOG (show (fc, doc))
57 checkUndefined fc n
58 (cty, _, t, inacc) <- buildType info syn fc [] n t_in
60 addIBC (IBCDef n)
61 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
63elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
64 = do let codata = Codata `elem` opts
65 iLOG (show fc)
66 undef <- isUndefined fc n
67 (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in
68 -- if n is defined already, make sure it is just a type declaration
69 -- with the same type we've just elaborated, and no constructors
70 -- yet
71 i <- getIState
72 checkDefinedAs fc n cty i
73 -- temporary, to check cons
74 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
75 let cnameinfo = cinfo info (map cname dcons)
76 let unique = case getRetTy cty of
77 UType UniqueType -> True
78 _ -> False
79 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons
80 ttag <- getName
81 i <- getIState
82 let as = map (const (Left (Msg ""))) (getArgTys cty)
83 let params = findParams (map snd cons)
84 logLvl 2 $ "Parameters : " ++ show params
85 -- TI contains information about mutually declared types - this will
86 -- be updated when the mutual block is complete
87 putIState (i { idris_datatypes =
88 addDef n (TI (map fst cons) codata opts params [n])
89 (idris_datatypes i) })
90 addIBC (IBCDef n)
91 addIBC (IBCData n)
92 checkDocs fc argDocs t
93 doc' <- elabDocTerms info doc
94 argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
95 return (n, d')) argDocs
96 addDocStr n doc' argDocs'
97 addIBC (IBCDoc n)
98 let metainf = DataMI params
99 addIBC (IBCMetaInformation n metainf)
100 -- TMP HACK! Make this a data option
101 updateContext (addDatatype (Data n ttag cty unique cons))
102 updateContext (setMetaInformation n metainf)
103 mapM_ totcheck (zip (repeat fc) (map fst cons))
104-- mapM_ (checkPositive n) cons
106 -- if there's exactly one constructor,
107 -- mark both the type and the constructor as detaggable
108 case cons of
109 [(cn,ct)] -> setDetaggable cn >> setDetaggable n
110 >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
111 _ -> return ()
113 -- create an eliminator
114 when (DefaultEliminator `elem` opts) $
115 evalStateT (elabCaseFun True params n t dcons info) Map.empty
116 -- create a case function
117 when (DefaultCaseFun `elem` opts) $
118 evalStateT (elabCaseFun False params n t dcons info) Map.empty
119 where
120 setDetaggable :: Name -> Idris ()
121 setDetaggable n = do
122 ist <- getIState
123 let opt = idris_optimisation ist
124 case lookupCtxt n opt of
125 [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
126 _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
128 checkDefinedAs fc n t i
129 = let defined = tclift $ tfail (At fc (AlreadyDefined n))
130 ctxt = tt_ctxt i in
131 case lookupDef n ctxt of
132 [] -> return ()
133 [TyDecl _ ty] ->
134 case converts ctxt [] t ty of
135 OK () -> case lookupCtxtExact n (idris_datatypes i) of
136 Nothing -> return ()
137 _ -> defined
138 _ -> defined
139 _ -> defined
140 -- parameters are names which are unchanged across the structure,
141 -- which appear exactly once in the return type of a constructor
143 -- First, find all applications of the constructor, then check over
144 -- them for repeated arguments
146 findParams :: [Type] -> [Int]
147 findParams ts = let allapps = map getDataApp ts
148 -- do each constructor separately, then merge the results (names
149 -- may change between constructors)
150 conParams = map paramPos allapps in
151 inAll conParams
153 inAll :: [[Int]] -> [Int]
154 inAll [] = []
155 inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x
157 paramPos [] = []
158 paramPos (args : rest)
159 = dropNothing $ keepSame (zip [0..] args) rest
161 dropNothing [] = []
162 dropNothing ((x, Nothing) : ts) = dropNothing ts
163 dropNothing ((x, _) : ts) = x : dropNothing ts
165 keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
166 [(Int, Maybe Name)]
167 keepSame as [] = as
168 keepSame as (args : rest) = keepSame (update as args) rest
169 where
170 update [] _ = []
171 update _ [] = []
172 update ((n, Just x) : as) (Just x' : args)
173 | x == x' = (n, Just x) : update as args
174 update ((n, _) : as) (_ : args) = (n, Nothing) : update as args
176 getDataApp :: Type -> [[Maybe Name]]
177 getDataApp f@(App _ _)
178 | (P _ d _, args) <- unApply f
179 = if (d == n) then [mParam args args] else []
180 getDataApp (Bind n (Pi _ t _) sc)
181 = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)
182 getDataApp _ = []
184 -- keep the arguments which are single names, which don't appear
185 -- elsewhere
187 mParam args [] = []
188 mParam args (P Bound n _ : rest)
189 | count n args == 1
190 = Just n : mParam args rest
191 where count n [] = 0
192 count n (t : ts)
193 | n `elem` freeNames t = 1 + count n ts
194 | otherwise = count n ts
195 mParam args (_ : rest) = Nothing : mParam args rest
197 cname (_, _, n, _, _, _) = n
199 -- Abuse of ElabInfo.
200 -- TODO Contemplate whether the ElabInfo type needs modification.
201 cinfo :: ElabInfo -> [Name] -> ElabInfo
202 cinfo info ds
203 = let newps = params info
204 dsParams = map (\n -> (n, [])) ds
205 newb = addAlist dsParams (inblock info)
206 l = liftname info in
207 info { params = newps,
208 inblock = newb,
209 liftname = id -- Is this appropriate?
210 }
212elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
213 Type -> -- for unique kind checking
214 Type -> -- data type's kind
215 (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->
216 Idris (Name, Type)
217elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)
218 = do checkUndefined fc n
219 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in
220 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
221 ctxt <- getContext
222 let cty' = normalise ctxt [] cty
223 checkUniqueKind ckind expkind
224 addDataConstraint ckind dkind
226 -- Check that the constructor type is, in fact, a part of the family being defined
227 tyIs n cty'
229 logLvl 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t
230 logLvl 5 $ "Inaccessible args: " ++ show inacc
231 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
233 -- Add to the context (this is temporary, so that later constructors
234 -- can be indexed by it)
235 updateContext (addTyDecl n (DCon 0 0 False) cty)
237 addIBC (IBCDef n)
238 checkDocs fc argDocs t
239 doc' <- elabDocTerms info doc
240 argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
241 return (n, d')) argDocs
242 addDocStr n doc' argDocs'
243 addIBC (IBCDoc n)
244 fputState (opt_inaccessible . ist_optimisation n) inacc
245 addIBC (IBCOpt n)
246 return (n, cty')
247 where
248 tyIs con (Bind n b sc) = tyIs con sc
249 tyIs con t | (P _ n' _, _) <- unApply t
250 = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show n' ++ " is not " ++ show tn))))
251 else return ()
252 tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))
254 mkLazy (PPi pl n ty sc)
255 = let ty' = if getTyName ty
256 then PApp fc (PRef fc (sUN "Lazy'"))
257 [pexp (PRef fc (sUN "LazyCodata")),
258 pexp ty]
259 else ty in
260 PPi pl n ty' (mkLazy sc)
261 mkLazy t = t
263 getTyName (PApp _ (PRef _ n) _) = n == nsroot tn
264 getTyName (PRef _ n) = n == nsroot tn
265 getTyName _ = False
268 getNamePos :: Int -> PTerm -> Name -> Maybe Int
269 getNamePos i (PPi _ n _ sc) x | n == x = Just i
270 | otherwise = getNamePos (i + 1) sc x
271 getNamePos _ _ _ = Nothing
273 -- if the constructor is a UniqueType, the datatype must be too
274 -- (Type* is fine, since that is checked for uniqueness too)
275 checkUniqueKind (UType NullType) (UType NullType) = return ()
276 checkUniqueKind (UType NullType) _
277 = tclift $ tfail (At fc (UniqueKindError NullType n))
278 checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()
279 checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()
280 checkUniqueKind (UType UniqueType) _
281 = tclift $ tfail (At fc (UniqueKindError UniqueType n))
282 checkUniqueKind (UType AllTypes) _ = return ()
283 checkUniqueKind _ _ = return ()
285 -- Constructor's kind must be <= expected kind
286 addDataConstraint (TType con) (TType exp)
287 = do ctxt <- getContext
288 let v = next_tvar ctxt
289 addConstraints fc (v, [ULT con exp])
290 addDataConstraint _ _ = return ()
292type EliminatorState = StateT (Map.Map String Int) Idris
294-- -- Issue #1616 in the issue tracker.
295-- https://github.com/idris-lang/Idris-dev/issues/1616
296--
297-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
298-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function
299-- rename to caseFun to match updated intend
300elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->
301 [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name])] ->
302 ElabInfo -> EliminatorState ()
303elabCaseFun ind paramPos n ty cons info = do
304 elimLog $ "Elaborating case function"
305 put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))
306 let (cnstrs, _) = splitPi ty
307 let (splittedTy@(pms, idxs)) = splitPms cnstrs
308 generalParams <- namePis False pms
309 motiveIdxs <- namePis False idxs
310 let motive = mkMotive n paramPos generalParams motiveIdxs
311 consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do
312 let casefunt = if ind then "elim_" else "case_"
313 name <- freshName $ casefunt ++ simpleName cnm
314 consTerm <- extractConsTerm c generalParams
315 return (name, expl, consTerm)) cons
316 scrutineeIdxs <- namePis False idxs
317 let motiveConstr = [(motiveName, expl, motive)]
318 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
319 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
320 let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
321 let clauseConsElimArgs = map getPiName consTerms
322 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
323 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
324 let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy
325 elimLog elimSig
326 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
327 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
328 elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
329 State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)
330 (ierror . Elaborating "type declaration of " elimDeclName)
331 -- Do not elaborate clauses if there aren't any
332 case eliminatorClauses of
333 [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
334 _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)
335 (ierror . Elaborating "clauses of " elimDeclName)
336 where elimLog :: String -> EliminatorState ()
337 elimLog s = State.lift (logLvl 2 s)
339 elimFC :: FC
340 elimFC = fileFC "(casefun)"
342 elimDeclName :: Name
343 elimDeclName = if ind then SN . ElimN $ n else SN . CaseN $ n
345 applyNS :: Name -> [String] -> Name
346 applyNS n [] = n
347 applyNS n ns = sNS n ns
349 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
350 splitPi = splitPi' []
351 where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)
352 splitPi' acc (PPi pl n tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr
353 splitPi' acc t = (reverse acc, t)
355 splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])
356 splitPms cnstrs = (map fst pms, map fst idxs)
357 where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
359 isMachineGenerated :: Name -> Bool
360 isMachineGenerated (MN _ _) = True
361 isMachineGenerated _ = False
363 namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]
364 namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms
365 let oldNames = map fst names
366 let params = map snd names
367 return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params
369 mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))
370 mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))
371 mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg
372 return (oldName, (name, pl, piarg))
373 where keyOf :: PTerm -> String
374 keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"
375 keyOf (PApp _ tyf _) = keyOf tyf
376 keyOf PType = "ty__"
377 keyOf _ = "carg__"
378 nameStart :: Name -> Char
379 nameStart n = nameStart' (simpleName n)
380 where nameStart' :: String -> Char
381 nameStart' "" = ' '
382 nameStart' ns = head ns
384 simpleName :: Name -> String
385 simpleName (NS n _) = simpleName n
386 simpleName (MN i n) = str n ++ show i
387 simpleName n = show n
389 nameSpaces :: Name -> [String]
390 nameSpaces (NS _ ns) = map str ns
391 nameSpaces _ = []
393 freshName :: String -> EliminatorState Name
394 freshName key = do
395 nameMap <- get
396 let i = fromMaybe 0 (Map.lookup key nameMap)
397 let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)
398 put $ Map.insert key (i+1) nameMap
399 return name
401 scrutineeName :: Name
402 scrutineeName = sUN "scrutinee"
404 scrutineeArgName :: Name
405 scrutineeArgName = sUN "scrutineeArg"
407 motiveName :: Name
408 motiveName = sUN "prop"
410 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
411 mkMotive n paramPos params indicies =
412 let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))
413 in piConstr (indicies ++ [scrutineeTy]) PType
415 piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm
416 piConstr [] ty = ty
417 piConstr ((n, pl, tyb):tyr) ty = PPi pl n tyb (piConstr tyr ty)
419 interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]
420 interlievePos idxs [] l2 i = l2
421 interlievePos idxs l1 [] i = l1
422 interlievePos idxs (x:xs) l2 i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))
423 interlievePos idxs l1 (y:ys) i = y:(interlievePos idxs l1 ys (i+1))
425 replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
426 replaceParams paramPos params cns =
427 let (_, cnsResTy) = splitPi cns
428 in case cnsResTy of
429 PApp _ _ args ->
430 let oldParams = paramNamesOf 0 paramPos args
431 in removeParamPis oldParams params cns
432 _ -> cns
434 removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
435 removeParamPis oldParams params (PPi pl n tyb tyr) =
436 case findIndex (== n) oldParams of
437 Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))
438 Just i -> (removeParamPis oldParams params tyr)
439 removeParamPis oldParams params (PRef _ n) =
440 case findIndex (== n) oldParams of
441 Nothing -> (PRef elimFC n)
442 Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))
443 removeParamPis oldParams params (PApp _ cns args) =
444 PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args
445 where replaceParamArgs :: [PArg] -> [PArg]
446 replaceParamArgs [] = []
447 replaceParamArgs (arg:args) =
448 case extractName (getTm arg) of
449 [] -> arg:replaceParamArgs args
450 [n] ->
451 case findIndex (== n) oldParams of
452 Nothing -> arg:replaceParamArgs args
453 Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC newname}:replaceParamArgs args
454 removeParamPis oldParams params t = t
456 paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]
457 paramNamesOf i paramPos [] = []
458 paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args
460 extractName :: PTerm -> [Name]
461 extractName (PRef _ n) = [n]
462 extractName _ = []
464 splitArgPms :: PTerm -> ([PTerm], [PTerm])
465 splitArgPms (PApp _ f args) = splitArgPms' args
466 where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])
467 splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)
468 where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
469 splitArgPms _ = ([],[])
472 implicitIndexes :: (Docstring (Either Err PTerm), Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
473 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
474 i <- State.lift getIState
475 implargs' <- case lookupCtxt cnm (idris_implicits i) of
476 [] -> do fail $ "Error while showing implicits for " ++ show cnm
477 [args] -> do return args
478 _ -> do fail $ "Ambigous name for " ++ show cnm
479 let implargs = mapMaybe convertImplPi implargs'
480 let (_, cnsResTy) = splitPi ty
481 case cnsResTy of
482 PApp _ _ args ->
483 let oldParams = paramNamesOf 0 paramPos args
484 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
485 _ -> return implargs
487 extractConsTerm :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
488 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
489 let cons' = replaceParams paramPos generalParameters ty
490 let (args, resTy) = splitPi cons'
491 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
492 consArgs <- namePis False args
493 let recArgs = findRecArgs consArgs
494 let recMotives = if ind then map applyRecMotive recArgs else []
495 let (_, consIdxs) = splitArgPms resTy
496 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
497 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
498 applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))
499 where (_, idxs) = splitArgPms ty
501 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
502 findRecArgs [] = []
503 findRecArgs (ty@(_,_,PRef _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
504 findRecArgs (ty@(_,_,PApp _ (PRef _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
505 findRecArgs (ty:rs) = findRecArgs rs
507 applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm
508 applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)
510 convertArg :: (Name, Plicity, PTerm) -> PArg
511 convertArg (n, _, _) = pexp (PRef elimFC n)
513 applyMotive :: [PTerm] -> PTerm -> PTerm
514 applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])
516 getPiName :: (Name, Plicity, PTerm) -> Name
517 getPiName (name,_,_) = name
519 convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)
520 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
521 convertImplPi _ = Nothing
523 generateEliminatorClauses :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
524 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
525 let cons' = replaceParams paramPos generalParameters ty
526 let (args, resTy) = splitPi cons'
527 i <- State.lift getIState
528 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
529 let (_, generalIdxs') = splitArgPms resTy
530 let generalIdxs = map pexp generalIdxs'
531 consArgs <- namePis False args
532 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
533 let recArgs = findRecArgs consArgs
534 let recElims = if ind then map applyRecElim recArgs else []
535 let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)
536 return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []
537 where applyRecElim :: (Name, Plicity, PTerm) -> PArg
538 applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])
539 where (_, idxs) = splitArgPms recTy