9a89a8d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Eliminators working for some type - still experimental. Will create a way to make them work with the elim type class

9a89a8dAhmad Salim Al-Sibahi13 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+4−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

@@ -252,14 +253,14 @@ instance Sized Name where

252instance Pretty Name where

253instance Pretty Name where

253 pretty (UN n) = text n

254 pretty (UN n) = text n

254 pretty (NS n s) = pretty n

255 pretty (NS n s) = pretty n

255− pretty (MN i s) = lbrace <+> text s <+> (text . show $ i) <+> rbrace

256+ pretty (MN i s) = text "«" <+> text s <+> (text . show $ i) <+> text "»"

256 pretty (SN s) = text (show s)

257 pretty (SN s) = text (show s)

257

258

258instance Show Name where

259instance Show Name where

259 show (UN n) = n

260 show (UN n) = n

260 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n

261 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n

261 show (MN _ "underscore") = "_"

262 show (MN _ "underscore") = "_"

262− show (MN i s) = "{" ++ s ++ show i ++ "}"

263+ show (MN i s) = "«" ++ s ++ show i ++ "»"

263 show (SN s) = show s

264 show (SN s) = show s

264 show NErased = "_"

265 show NErased = "_"

265

266

@@ -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+8−2

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

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

620getInferType (App (App _ ty) _) = ty

621

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

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

623

624primNames = [unitTy, unitCon,

625 falseTy, pairTy, pairCon,

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

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

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

647 where n a = MN 0 a

648−pairOpts = [DefaultEliminator]

648+pairOpts = []

649

650eqTy = UN "="

651eqCon = UN "refl"

@@ -661,6 +661,12 @@ eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),

661 where n a = MN 0 a

662eqOpts = []

663

664+elimName = UN "__Elim"

665+elimMethElimTy = UN "__elimTy"

666+elimMethElim = UN "elim"

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

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

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

664

670

665-- Defined in builtins.idr

671-- Defined in builtins.idr

666sigmaTy = UN "Exists"

672sigmaTy = UN "Exists"

src/Idris/AbsSyntaxTree.hs+2−2

@@ -940,7 +940,7 @@ prettyImp impl = prettySe 10

940 prettyBasic n

941 where

942 prettyBasic n@(UN _) = pretty n

943− prettyBasic (MN _ s) = text s

943+ prettyBasic n@(MN _ _) = pretty n

944 prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n

945 prettyBasic (SN sn) = text (show sn)

946 prettySe p (PLam n ty sc) =

@@ -1126,7 +1126,7 @@ showName ist bnd impl colour n = case ist of

1126 Nothing -> showbasic n

1127 where name = if impl then show n else showbasic n

1128 showbasic n@(UN _) = show n

1129− showbasic (MN _ s) = s

1129+ showbasic n@(MN _ _) = show n

1130 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

1131 showbasic (SN s) = show s

1132 fst3 (x, _, _) = x

src/Idris/DeepSeq.hs+1

@@ -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` ()

src/Idris/ElabDecls.hs+246

@@ -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

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

196 collapseCons n cons

202 collapseCons n cons

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

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

198 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 ()

199 where

207 where

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

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

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

209 -- 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)

247 | otherwise = count n ts

255 | otherwise = count n ts

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

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

249

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+

250-- | Elaborate primitives

495-- | Elaborate primitives

251

496

252elabPrims :: Idris ()

497elabPrims :: Idris ()

@@ -255,6 +500,7 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

255 (zip

500 (zip

256 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

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

257 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

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

503+ elabDecl EAll toplevel elimDecl

258 mapM_ elabPrim primitives

504 mapM_ elabPrim primitives

259 -- 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

260 elabBelieveMe

506 elabBelieveMe

src/Idris/IBC.hs+3

@@ -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

src/Idris/ParseData.hs+1−1

@@ -78,7 +78,7 @@ dataI = do reserved "data"; return []

78DefaultEliminator ::= 'noelim'?

79 -}

80defaultEliminator :: IdrisParser DataOpts

81−defaultEliminator = do option [DefaultEliminator] (do reserved "%noelim"; return [])

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

83{- | Parses a data type declaration

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

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