@@ -33,6 +33,12 @@ import Data.List
3333import Data.Maybe
3434import Debug.Trace
3535
36+import qualified Data.Map as Map
37+import Data.Char(isLetter, toLower)
38+import Data.List.Split (splitOn)
39+
40+import Util.Pretty(pretty)
41+
3642recheckC fc env t
3743 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
3844 ctxt <- getContext
@@ -196,6 +202,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
196202 collapseCons n cons
197203 updateContext (addDatatype (Data n ttag cty cons))
198204 mapM_ (checkPositive n) cons
205+ if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
206+ else return ()
199207 where
200208 -- parameters are names which are unchanged across the structure,
201209 -- which appear exactly once in the return type of a constructor
@@ -247,6 +255,243 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
247255 | otherwise = count n ts
248256 mParam args (_ : rest) = Nothing : mParam args rest
249257
258+type EliminatorState = StateT (Map.Map String Int) Idris
259+
260+-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
261+elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC)] -> ElabInfo -> EliminatorState ()
262+elabEliminator paramPos n ty cons info = do
263+ elimLog $ "Elaborating eliminator"
264+ let (cnstrs, _) = splitPi ty
265+ let (splittedTy@(pms, idxs)) = splitPms cnstrs
266+ generalParams <- namePis False pms
267+ motiveIdxs <- namePis False idxs
268+ let motive = mkMotive n paramPos generalParams motiveIdxs
269+ consTerms <- mapM (\(c@(_,cnm,_,_)) -> do
270+ name <- freshName $ "elim_" ++ simpleName cnm
271+ consTerm <- extractConsTerm c generalParams
272+ return (name, expl, consTerm)) cons
273+ scrutineeIdxs <- namePis False idxs
274+ let motiveConstr = [(motiveName, expl, motive)]
275+ let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
276+ let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
277+ let eliminatorTyDecl = PTy (show n) defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
278+ let clauseConsElimArgs = map getPiName consTerms
279+ let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
280+ let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
281+ let elimSig = "-- eliminator signature: " ++ showImp Nothing True True eliminatorTy
282+ eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
283+ let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
284+ elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef
285+ Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
286+ -- Do not elaborate clauses if there aren't any
287+ case eliminatorClauses of
288+ [] -> return ()
289+ _ -> Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
290+ where elimLog :: String -> EliminatorState ()
291+ elimLog s = Control.Monad.State.lift (logLvl 2 s)
292+
293+ elimFC :: FC
294+ elimFC = fileFC "(eliminator)"
295+
296+ elimDeclName :: Name
297+ elimDeclName = SN $ ElimN n
298+
299+ applyNS :: Name -> [String] -> Name
300+ applyNS n [] = n
301+ applyNS n ns = NS n ns
302+
303+ splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
304+ splitPi = splitPi' []
305+ where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)
306+ splitPi' acc (PPi pl n tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr
307+ splitPi' acc t = (reverse acc, t)
308+
309+ splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])
310+ splitPms cnstrs = (map fst pms, map fst idxs)
311+ where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
312+
313+ isMachineGenerated :: Name -> Bool
314+ isMachineGenerated (MN _ _) = True
315+ isMachineGenerated _ = False
316+
317+ namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]
318+ namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms
319+ let oldNames = map fst names
320+ let params = map snd names
321+ return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params
322+
323+ mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))
324+ mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))
325+ mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg
326+ return (oldName, (name, pl, piarg))
327+ where keyOf :: PTerm -> String
328+ keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"
329+ keyOf (PApp _ tyf _) = keyOf tyf
330+ keyOf PType = "ty__"
331+ keyOf _ = "carg__"
332+ nameStart :: Name -> Char
333+ nameStart n = nameStart' (simpleName n)
334+ where nameStart' :: String -> Char
335+ nameStart' "" = ' '
336+ nameStart' ns = head ns
337+
338+ simpleName :: Name -> String
339+ simpleName (NS n _) = simpleName n
340+ simpleName (MN i n) = n ++ show i
341+ simpleName n = show n
342+
343+ nameSpaces :: Name -> [String]
344+ nameSpaces (NS _ ns) = ns
345+ nameSpaces _ = []
346+
347+ freshName :: String -> EliminatorState Name
348+ freshName key = do
349+ nameMap <- get
350+ let i = fromMaybe 0 (Map.lookup key nameMap)
351+ let name = key ++ show i ++ "__"
352+ put $ Map.insert key (i+1) nameMap
353+ return (MN i name)
354+
355+ scrutineeName :: Name
356+ scrutineeName = MN 0 "scrutinee"
357+
358+ scrutineeArgName :: Name
359+ scrutineeArgName = MN 0 "scrutineeArg"
360+
361+ motiveName :: Name
362+ motiveName = MN 0 "prop"
363+
364+ mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
365+ mkMotive n paramPos params indicies =
366+ let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))
367+ in piConstr (indicies ++ [scrutineeTy]) PType
368+
369+ piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm
370+ piConstr [] ty = ty
371+ piConstr ((n, pl, tyb):tyr) ty = PPi pl n tyb (piConstr tyr ty)
372+
373+ interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]
374+ interlievePos idxs [] l2 i = l2
375+ interlievePos idxs l1 [] i = l1
376+ interlievePos idxs (x:xs) l2 i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))
377+ interlievePos idxs l1 (y:ys) i = y:(interlievePos idxs l1 ys (i+1))
378+
379+ replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
380+ replaceParams paramPos params cns =
381+ let (_, cnsResTy) = splitPi cns
382+ in case cnsResTy of
383+ PApp _ _ args ->
384+ let oldParams = paramNamesOf 0 paramPos args
385+ in removeParamPis oldParams params cns
386+ _ -> cns
387+
388+ removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
389+ removeParamPis oldParams params (PPi pl n tyb tyr) =
390+ case findIndex (== n) oldParams of
391+ Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))
392+ Just i -> (removeParamPis oldParams params tyr)
393+ removeParamPis oldParams params (PRef _ n) =
394+ case findIndex (== n) oldParams of
395+ Nothing -> (PRef elimFC n)
396+ Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))
397+ removeParamPis oldParams params (PApp _ cns args) =
398+ PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args
399+ where replaceParamArgs :: [PArg] -> [PArg]
400+ replaceParamArgs [] = []
401+ replaceParamArgs (arg:args) =
402+ case extractName (getTm arg) of
403+ [] -> arg:replaceParamArgs args
404+ [n] ->
405+ case findIndex (== n) oldParams of
406+ Nothing -> arg:replaceParamArgs args
407+ Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC newname}:replaceParamArgs args
408+ removeParamPis oldParams params t = t
409+
410+ paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]
411+ paramNamesOf i paramPos [] = []
412+ paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args
413+
414+ extractName :: PTerm -> [Name]
415+ extractName (PRef _ n) = [n]
416+ extractName _ = []
417+
418+ splitArgPms :: PTerm -> ([PTerm], [PTerm])
419+ splitArgPms (PApp _ f args) = splitArgPms' args
420+ where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])
421+ splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)
422+ where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
423+ splitArgPms _ = ([],[])
424+
425+
426+ implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]
427+ implicitIndexes (cns@(doc, cnm, ty, fc)) = do
428+ i <- Control.Monad.State.lift getIState
429+ implargs' <- case lookupCtxt cnm (idris_implicits i) of
430+ [] -> do fail $ "Error while showing implicits for " ++ show cnm
431+ [args] -> do return args
432+ _ -> do fail $ "Ambigous name for " ++ show cnm
433+ let implargs = mapMaybe convertImplPi implargs'
434+ let (_, cnsResTy) = splitPi ty
435+ case cnsResTy of
436+ PApp _ _ args ->
437+ let oldParams = paramNamesOf 0 paramPos args
438+ in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
439+ _ -> return implargs
440+
441+ extractConsTerm :: (String, Name, PTerm, FC) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
442+ extractConsTerm (doc, cnm, ty, fc) generalParameters = do
443+ let cons' = replaceParams paramPos generalParameters ty
444+ let (args, resTy) = splitPi cons'
445+ implidxs <- implicitIndexes (doc, cnm, ty, fc)
446+ consArgs <- namePis True args
447+ let recArgs = findRecArgs consArgs
448+ let recMotives = map applyRecMotive recArgs
449+ let (_, consIdxs) = splitArgPms resTy
450+ return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
451+ where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
452+ applyRecMotive (n,_,ty) = (MN 0 $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))
453+ where (_, idxs) = splitArgPms ty
454+
455+ findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
456+ findRecArgs [] = []
457+ findRecArgs (ty@(_,_,PRef _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
458+ findRecArgs (ty@(_,_,PApp _ (PRef _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
459+ findRecArgs (ty:rs) = findRecArgs rs
460+
461+ applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm
462+ applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)
463+
464+ convertArg :: (Name, Plicity, PTerm) -> PArg
465+ convertArg (n, _, _) = pexp (PRef elimFC n)
466+
467+ applyMotive :: [PTerm] -> PTerm -> PTerm
468+ applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])
469+
470+ getPiName :: (Name, Plicity, PTerm) -> Name
471+ getPiName (name,_,_) = name
472+
473+ convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)
474+ convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
475+ convertImplPi _ = Nothing
476+
477+ generateEliminatorClauses :: (String, Name, PTerm, FC) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
478+ generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do
479+ let cons' = replaceParams paramPos generalParameters ty
480+ let (args, resTy) = splitPi cons'
481+ i <- Control.Monad.State.lift getIState
482+ implidxs <- implicitIndexes (doc, cnm, ty, fc)
483+ let (_, generalIdxs') = splitArgPms resTy
484+ let generalIdxs = map pexp generalIdxs'
485+ consArgs <- namePis True args
486+ let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
487+ let recArgs = findRecArgs consArgs
488+ let recElims = map applyRecElim recArgs
489+ let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)
490+ return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []
491+ where applyRecElim :: (Name, Plicity, PTerm) -> PArg
492+ applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])
493+ where (_, idxs) = splitArgPms recTy
494+
250495-- | Elaborate primitives
251496
252497elabPrims :: Idris ()
@@ -255,6 +500,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
255500 (zip
256501 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
257502 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
503+ elabDecl EAll toplevel elimDecl
258504 mapM_ elabPrim primitives
259505 -- Special case prim__believe_me because it doesn't work on just constants
260506 elabBelieveMe