7b8f3b4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'feature/eliminators' of https://github.com/ahmadsalim/Idris-dev into ahmadsalim-feature/eliminators

7b8f3b4Edwin Brady13 years ago

libs/prelude/Prelude/List.idr+1−1

compare with master

unifiedsplit

@@ -15,7 +15,7 @@ import Prelude.Nat

15infixr 7 ::

16infixl 8 ++

18−data List a

18+%elim data List a

19 = Nil

20 | (::) a (List a)

libs/prelude/Prelude/Nat.idr+1−1

@@ -10,7 +10,7 @@ import Prelude.Classes

10%access public

11%default total

13−data Nat

13+%elim data Nat

14 = Z

15 | S Nat

libs/prelude/Prelude/Vect.idr+1−1

@@ -11,7 +11,7 @@ import Prelude.Nat

12infixr 7 ::

14−data Vect : Nat -> Type -> Type where

14+%elim data Vect : Nat -> Type -> Type where

15 Nil : Vect Z a

16 (::) : a -> Vect n a -> Vect (S n) a

src/Core/TT.hs+2

@@ -237,6 +237,7 @@ data SpecialName = WhereN Int Name Name

237 | ParentN Name String

238 | MethodN Name

239 | CaseN Name

240+ | ElimN Name

240 deriving (Eq, Ord)

241 deriving (Eq, Ord)

241{-!

242{-!

242deriving instance Binary SpecialName

243deriving instance Binary SpecialName

@@ -269,6 +270,7 @@ instance Show SpecialName where

269 show (MethodN m) = "method " ++ show m

270 show (MethodN m) = "method " ++ show m

270 show (ParentN p c) = show p ++ "#" ++ c

271 show (ParentN p c) = show p ++ "#" ++ c

271 show (CaseN n) = "case block in " ++ show n

272 show (CaseN n) = "case block in " ++ show n

273+ show (ElimN n) = "<<" ++ show n ++ " eliminator>>"

272

274

273-- Show a name in a way decorated for code generation, not human reading

275-- Show a name in a way decorated for code generation, not human reading

274showCG :: Name -> String

276showCG :: Name -> String

src/Idris/AbsSyntax.hs+13−1

@@ -634,6 +634,7 @@ inferDecl = PDatadecl inferTy

634 [("", inferCon, PPi impl (MN 0 "A") PType (

635 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))

636 (PRef bi inferTy)), bi)]

637+inferOpts = []

637

638

638infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]

639infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]

639infP = P (TCon 6 0) inferTy (TType (UVal 0))

640infP = P (TCon 6 0) inferTy (TType (UVal 0))

@@ -646,7 +647,7 @@ getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

646getInferType (Bind n b sc) = Bind n b $ getInferType sc

647getInferType (Bind n b sc) = Bind n b $ getInferType sc

647getInferType (App (App _ ty) _) = ty

648getInferType (App (App _ ty) _) = ty

648

649

649−-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign

650+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class

650

651

651primNames = [unitTy, unitCon,

652primNames = [unitTy, unitCon,

652 falseTy, pairTy, pairCon,

653 falseTy, pairTy, pairCon,

@@ -656,9 +657,11 @@ unitTy = MN 0 "__Unit"

656unitCon = MN 0 "__II"

657unitCon = MN 0 "__II"

657unitDecl = PDatadecl unitTy PType

658unitDecl = PDatadecl unitTy PType

658 [("", unitCon, PRef bi unitTy, bi)]

659 [("", unitCon, PRef bi unitTy, bi)]

660+unitOpts = [DefaultEliminator]

659

661

660falseTy = MN 0 "__False"

662falseTy = MN 0 "__False"

661falseDecl = PDatadecl falseTy PType []

663falseDecl = PDatadecl falseTy PType []

664+falseOpts = []

662

665

663pairTy = MN 0 "__Pair"

666pairTy = MN 0 "__Pair"

664pairCon = MN 0 "__MkPair"

667pairCon = MN 0 "__MkPair"

@@ -670,6 +673,7 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

670 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

673 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

671 pexp (PRef bi (n "B"))])))), bi)]

674 pexp (PRef bi (n "B"))])))), bi)]

672 where n a = MN 0 a

675 where n a = MN 0 a

676+pairOpts = []

673

677

674eqTy = UN "="

678eqTy = UN "="

675eqCon = UN "refl"

679eqCon = UN "refl"

@@ -683,6 +687,14 @@ eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),

683 pexp (PRef bi (n "x")),

687 pexp (PRef bi (n "x")),

684 pexp (PRef bi (n "x"))])), bi)]

688 pexp (PRef bi (n "x"))])), bi)]

685 where n a = MN 0 a

689 where n a = MN 0 a

690+eqOpts = []

691+

692+elimName = UN "__Elim"

693+elimMethElimTy = UN "__elimTy"

694+elimMethElim = UN "elim"

695+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(UN "scrutineeType", PType)]

696+ [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

697+ PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

686

698

687-- Defined in builtins.idr

699-- Defined in builtins.idr

688sigmaTy = UN "Exists"

700sigmaTy = UN "Exists"

src/Idris/AbsSyntaxTree.hs+9−1

@@ -392,6 +392,14 @@ inlinable = elem Inlinable

392dictionary :: FnOpts -> Bool

393dictionary = elem Dictionary

394

395+

396+-- | Data declaration options

397+data DataOpt = Codata -- Set if the the data-type is coinductive

398+ | DefaultEliminator -- Set if an eliminator should be generated for data type

399+ deriving (Show, Eq)

400+

401+type DataOpts = [DataOpt]

402+

395-- | Top-level declarations such as compiler directives, definitions,

403-- | Top-level declarations such as compiler directives, definitions,

396-- datatypes and typeclasses.

404-- datatypes and typeclasses.

397data PDecl' t

405data PDecl' t

@@ -400,7 +408,7 @@ data PDecl' t

400 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

408 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

401 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

409 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

402 | PCAF FC Name t -- ^ Top level constant

410 | PCAF FC Name t -- ^ Top level constant

403− | PData String SyntaxInfo FC Bool (PData' t) -- ^ Data declaration. The Bool argument is True for codata.

411+ | PData String SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

404 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

412 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

405 | PNamespace String [PDecl' t] -- ^ New namespace

413 | PNamespace String [PDecl' t] -- ^ New namespace

406 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

414 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

src/Idris/DeepSeq.hs+5

@@ -31,6 +31,7 @@ instance NFData SpecialName where

31 rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

32 rnf (MethodN x1) = rnf x1 `seq` ()

33 rnf (CaseN x1) = rnf x1 `seq` ()

34+ rnf (ElimN x1) = rnf x1 `seq` ()

35instance NFData IntTy where

36instance NFData IntTy where

36 rnf (ITFixed x1) = rnf x1 `seq` ()

37 rnf (ITFixed x1) = rnf x1 `seq` ()

@@ -164,6 +165,10 @@ instance NFData FnOpt where

164 rnf Reflection = ()

165 rnf Reflection = ()

165 rnf (Specialise x1) = rnf x1 `seq` ()

166 rnf (Specialise x1) = rnf x1 `seq` ()

166

167

168+instance NFData DataOpt where

169+ rnf Codata = ()

170+ rnf DefaultEliminator = ()

171+

167instance (NFData t) => NFData (PDecl' t) where

172instance (NFData t) => NFData (PDecl' t) where

168 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

173 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

169 rnf (PTy x1 x2 x3 x4 x5 x6)

174 rnf (PTy x1 x2 x3 x4 x5 x6)

src/Idris/ElabDecls.hs+260−10

@@ -33,6 +33,12 @@ import Data.List

33import Data.Maybe

34import Debug.Trace

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+

36recheckC fc env t

42recheckC fc env t

37 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

43 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

38 ctxt <- getContext

44 ctxt <- getContext

@@ -143,9 +149,10 @@ elabPostulate info syn doc fc opts n ty

143 -- remove it from the deferred definitions list

149 -- remove it from the deferred definitions list

144 solveDeferred n

150 solveDeferred n

145

151

146−elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()

152+elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()

147−elabData info syn doc fc codata (PLaterdecl n t_in)

153+elabData info syn doc fc opts (PLaterdecl n t_in)

154+ = do let codata = Codata `elem` opts

148− = do iLOG (show (fc, doc))

155+ iLOG (show (fc, doc))

149 checkUndefined fc n

156 checkUndefined fc n

150 ctxt <- getContext

157 ctxt <- getContext

151 i <- getIState

158 i <- getIState

@@ -161,8 +168,9 @@ elabData info syn doc fc codata (PLaterdecl n t_in)

161 logLvl 2 $ "---> " ++ show cty

168 logLvl 2 $ "---> " ++ show cty

162 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

169 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

163

170

164−elabData info syn doc fc codata (PDatadecl n t_in dcons)

171+elabData info syn doc fc opts (PDatadecl n t_in dcons)

172+ = do let codata = Codata `elem` opts

165− = do iLOG (show fc)

173+ iLOG (show fc)

166 undef <- isUndefined fc n

174 undef <- isUndefined fc n

167 ctxt <- getContext

175 ctxt <- getContext

168 i <- getIState

176 i <- getIState

@@ -194,6 +202,8 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

194 collapseCons n cons

202 collapseCons n cons

195 updateContext (addDatatype (Data n ttag cty cons))

203 updateContext (addDatatype (Data n ttag cty cons))

196 mapM_ (checkPositive n) cons

204 mapM_ (checkPositive n) cons

205+ if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

206+ else return ()

197 where

207 where

198 -- parameters are names which are unchanged across the structure,

208 -- parameters are names which are unchanged across the structure,

199 -- which appear exactly once in the return type of a constructor

209 -- which appear exactly once in the return type of a constructor

@@ -245,12 +255,252 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

245 | otherwise = count n ts

255 | otherwise = count n ts

246 mParam args (_ : rest) = Nothing : mParam args rest

256 mParam args (_ : rest) = Nothing : mParam args rest

247

257

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+

248-- | Elaborate primitives

495-- | Elaborate primitives

249

496

250elabPrims :: Idris ()

497elabPrims :: Idris ()

251elabPrims = do mapM_ (elabDecl EAll toplevel)

498elabPrims = do mapM_ (elabDecl EAll toplevel)

252− (map (PData "" defaultSyntax (fileFC "builtin") False)

499+ (map (\(opt, decl) -> PData "" defaultSyntax (fileFC "builtin") opt decl)

500+ (zip

501+ [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

253− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

502+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

503+ elabDecl EAll toplevel elimDecl

254 mapM_ elabPrim primitives

504 mapM_ elabPrim primitives

255 -- Special case prim__believe_me because it doesn't work on just constants

505 -- Special case prim__believe_me because it doesn't work on just constants

256 elabBelieveMe

506 elabBelieveMe

@@ -400,7 +650,7 @@ elabTransform info fc safe lhs_in rhs_in

400elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

650elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

401 PTerm -> String -> Name -> PTerm -> Idris ()

651 PTerm -> String -> Name -> PTerm -> Idris ()

402elabRecord info syn doc fc tyn ty cdoc cn cty

652elabRecord info syn doc fc tyn ty cdoc cn cty

403− = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])

653+ = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc)])

404 cty' <- implicit syn cn cty

654 cty' <- implicit syn cn cty

405 i <- getIState

655 i <- getIState

406 cty <- case lookupTy cn (tt_ctxt i) of

656 cty <- case lookupTy cn (tt_ctxt i) of

@@ -1286,7 +1536,7 @@ elabClass info syn doc fc constraints tn ps ds

1286 let cons = [("", cn, cty, fc)]

1536 let cons = [("", cn, cty, fc)]

1287 let ddecl = PDatadecl tn tty cons

1537 let ddecl = PDatadecl tn tty cons

1288 logLvl 5 $ "Class data " ++ showDImp True ddecl

1538 logLvl 5 $ "Class data " ++ showDImp True ddecl

1289− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl

1539+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl

1290 -- for each constraint, build a top level function to chase it

1540 -- for each constraint, build a top level function to chase it

1291 logLvl 5 $ "Building functions"

1541 logLvl 5 $ "Building functions"

1292 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

1542 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

@@ -1709,7 +1959,7 @@ elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

1709 elabRecord info s doc f tyn ty cdoc cn cty

1959 elabRecord info s doc f tyn ty cdoc cn cty

1710 | otherwise

1960 | otherwise

1711 = do iLOG $ "Elaborating [type of] " ++ show tyn

1961 = do iLOG $ "Elaborating [type of] " ++ show tyn

1712− elabData info s doc f False (PLaterdecl tyn ty)

1962+ elabData info s doc f [] (PLaterdecl tyn ty)

1713elabDecl' _ info (PDSL n dsl)

1963elabDecl' _ info (PDSL n dsl)

1714 = do i <- getIState

1964 = do i <- getIState

1715 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

1965 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

src/Idris/IBC.hs+13−1

@@ -23,7 +23,7 @@ import Debug.Trace

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 44

26+ibcVersion = 45

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -410,6 +410,7 @@ instance Binary SpecialName where

410 MethodN x1 -> do putWord8 3

411 put x1

412 CaseN x1 -> do putWord8 4; put x1

413+ ElimN x1 -> do putWord8 5; put x1

413 get

414 get

414 = do i <- getWord8

415 = do i <- getWord8

415 case i of

416 case i of

@@ -427,6 +428,8 @@ instance Binary SpecialName where

427 return (MethodN x1)

428 return (MethodN x1)

428 4 -> do x1 <- get

429 4 -> do x1 <- get

429 return (CaseN x1)

430 return (CaseN x1)

431+ 5 -> do x1 <- get

432+ return (ElimN x1)

430 _ -> error "Corrupted binary data for SpecialName"

433 _ -> error "Corrupted binary data for SpecialName"

431

434

432

435

@@ -931,6 +934,15 @@ instance Binary IBCFile where

931 return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27)

934 return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27)

932 else return (initIBC { ver = x1 })

935 else return (initIBC { ver = x1 })

933

936

937+instance Binary DataOpt where

938+ put x = case x of

939+ Codata -> putWord8 0

940+ DefaultEliminator -> putWord8 1

941+ get = do i <- getWord8

942+ case i of

943+ 0 -> return Codata

944+ 1 -> return DefaultEliminator

945+

934instance Binary FnOpt where

946instance Binary FnOpt where

935 put x

947 put x

936 = case x of

948 = case x of

src/Idris/ParseData.hs+22−12

@@ -70,13 +70,19 @@ record syn = do (doc, acc) <- try (do

70{- | Parses data declaration type (normal or codata)

71DataI ::= 'data' | 'codata';

72-}

73−dataI :: IdrisParser Bool

73+dataI :: IdrisParser DataOpts

74−dataI = do reserved "data"; return False

74+dataI = do reserved "data"; return []

75− <|> do reserved "codata"; return True

75+ <|> do reserved "codata"; return [Codata]

76+

77+{- | Parses if a data should not have a default eliminator

78+DefaultEliminator ::= 'noelim'?

79+ -}

80+defaultEliminator :: IdrisParser DataOpts

81+defaultEliminator = do option [] (do reserved "%elim"; return [DefaultEliminator])

77{- | Parses a data type declaration

83{- | Parses a data type declaration

78−Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?

84+Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

79− | DocComment? Accessibility? DataI FnName Name* DataRest?

85+ | DocComment? Accessibility? DataI DefaultEliminator FnName Name* DataRest?

80 ;

86 ;

81Constructor' ::= Constructor KeepTerminator;

87Constructor' ::= Constructor KeepTerminator;

82ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;

88ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;

@@ -90,29 +96,31 @@ SimpleConstructorList ::=

90 ;

96 ;

91-}

97-}

92data_ :: SyntaxInfo -> IdrisParser PDecl

98data_ :: SyntaxInfo -> IdrisParser PDecl

93−data_ syn = do (doc, acc, co) <- try (do

99+data_ syn = do (doc, acc, dataOpts) <- try (do

94 doc <- option "" (docComment '|')

100 doc <- option "" (docComment '|')

95 pushIndent

101 pushIndent

96 acc <- optional accessibility

102 acc <- optional accessibility

103+ elim <- defaultEliminator

97 co <- dataI

104 co <- dataI

105+ let dataOpts = combineDataOpts(elim ++ co)

98− return (doc, acc, co))

106+ return (doc, acc, dataOpts))

99 fc <- getFC

107 fc <- getFC

100 tyn_in <- fnName

108 tyn_in <- fnName

101 (do try (lchar ':')

109 (do try (lchar ':')

102 popIndent

110 popIndent

103 ty <- typeExpr (allowImp syn)

111 ty <- typeExpr (allowImp syn)

104 let tyn = expandNS syn tyn_in

112 let tyn = expandNS syn tyn_in

105− option (PData doc syn fc co (PLaterdecl tyn ty)) (do

113+ option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do

106 reserved "where"

114 reserved "where"

107 cons <- indentedBlock (constructor syn)

115 cons <- indentedBlock (constructor syn)

108 accData acc tyn (map (\ (_, n, _, _) -> n) cons)

116 accData acc tyn (map (\ (_, n, _, _) -> n) cons)

109− return $ PData doc syn fc co (PDatadecl tyn ty cons))) <|> (do

117+ return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

110 args <- many name

118 args <- many name

111 let ty = bindArgs (map (const PType) args) PType

119 let ty = bindArgs (map (const PType) args) PType

112 let tyn = expandNS syn tyn_in

120 let tyn = expandNS syn tyn_in

113− option (PData doc syn fc co (PLaterdecl tyn ty)) (do

121+ option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do

114 try (lchar '=') <|> do reserved "where"

122 try (lchar '=') <|> do reserved "where"

115− let kw = (if co then "co" else "") ++ "data "

123+ let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

116 let n = show tyn_in ++ " "

124 let n = show tyn_in ++ " "

117 let s = kw ++ n

125 let s = kw ++ n

118 let as = concat (intersperse " " $ map show args) ++ " "

126 let as = concat (intersperse " " $ map show args) ++ " "

@@ -129,7 +137,7 @@ data_ syn = do (doc, acc, co) <- try (do

129 do let cty = bindArgs cargs conty

137 do let cty = bindArgs cargs conty

130 return (doc, x, cty, cfc)) cons

138 return (doc, x, cty, cfc)) cons

131 accData acc tyn (map (\ (_, n, _, _) -> n) cons')

139 accData acc tyn (map (\ (_, n, _, _) -> n) cons')

132− return $ PData doc syn fc co (PDatadecl tyn ty cons')))

140+ return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons')))

133 <?> "data type declaration"

141 <?> "data type declaration"

134 where

142 where

135 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

143 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

@@ -137,6 +145,8 @@ data_ syn = do (doc, acc, co) <- try (do

137 mkPApp fc t xs = PApp fc t (map pexp xs)

145 mkPApp fc t xs = PApp fc t (map pexp xs)

138 bindArgs :: [PTerm] -> PTerm -> PTerm

146 bindArgs :: [PTerm] -> PTerm -> PTerm

139 bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs

147 bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs

148+ combineDataOpts :: DataOpts -> DataOpts

149+ combineDataOpts opts = if Codata `elem` opts then delete DefaultEliminator opts else opts

140

150

141

151

142{- | Parses a type constructor declaration

152{- | Parses a type constructor declaration

src/Idris/ParseExpr.hs+1

@@ -267,6 +267,7 @@ simpleExpr syn =

267 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';

268 return t)

269 return (PRefl fc tm)

270+ <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))

270 <|> proofExpr syn

271 <|> proofExpr syn

271 <|> tacticsExpr syn

272 <|> tacticsExpr syn

272 <|> caseExpr syn

273 <|> caseExpr syn