d337b5d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Performance/compiler temporary hack: %erase

d337b5dEdwin Brady13 years ago

src/Idris/AbsSyntax.hs+6−6

compare with master

unifiedsplit

@@ -698,7 +698,7 @@ inferDecl = PDatadecl inferTy

698 PType

699 [("", inferCon, PPi impl (sMN 0 "iType") PType (

700 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

701− (PRef bi inferTy)), bi)]

701+ (PRef bi inferTy)), bi, [])]

702inferOpts = []

703

704infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

@@ -721,7 +721,7 @@ primNames = [unitTy, unitCon,

721unitTy = sMN 0 "__Unit"

722unitCon = sMN 0 "__II"

723unitDecl = PDatadecl unitTy PType

724− [("", unitCon, PRef bi unitTy, bi)]

724+ [("", unitCon, PRef bi unitTy, bi, [])]

725unitOpts = [DefaultEliminator]

726

727falseTy = sMN 0 "__False"

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

736 PPi expl (n "a") (PRef bi (n "A")) (

737 PPi expl (n "b") (PRef bi (n "B"))

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

739− pexp (PRef bi (n "B"))])))), bi)]

739+ pexp (PRef bi (n "B"))])))), bi, [])]

740 where n a = sMN 0 a

741pairOpts = []

742

@@ -750,7 +750,7 @@ eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

750 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

751 pimp (n "B") Placeholder False,

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

753− pexp (PRef bi (n "x"))])), bi)]

753+ pexp (PRef bi (n "x"))])), bi, [])]

754 where n a = sMN 0 a

755eqOpts = []

756

@@ -921,8 +921,8 @@ expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

921 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))

922 (map econ cons)

923 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

924− econ (doc, n, t, fc)

924+ econ (doc, n, t, fc, fs)

925− = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)

925+ = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

926expandParamsD rhs ist dec ps ns (PParams f params pds)

927 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

928 (map (expandParamsD True ist dec ps ns) pds)

src/Idris/AbsSyntaxTree.hs+5−5

@@ -478,7 +478,7 @@ deriving instance NFData PClause'

478-- | Data declaration

479data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

480 d_tcon :: t, -- ^ Type constructor

481− d_cons :: [(String, Name, t, FC)] -- ^ Constructors

481+ d_cons :: [(String, Name, t, FC, [Name])] -- ^ Constructors

482 }

483 -- ^ Data declaration

484 | PLaterdecl { d_name :: Name, d_tcon :: t }

@@ -505,7 +505,7 @@ declared (PPostulate _ _ _ _ n t) = [n]

505declared (PClauses _ _ n _) = [] -- not a declaration

506declared (PCAF _ n _) = [n]

507declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

508− where fstt (_, a, _, _) = a

508+ where fstt (_, a, _, _, _) = a

509declared (PData _ _ _ _ (PLaterdecl n _)) = [n]

510declared (PParams _ _ ds) = concatMap declared ds

511declared (PNamespace _ ds) = concatMap declared ds

@@ -525,7 +525,7 @@ tldeclared (PPostulate _ _ _ _ n t) = [n]

525tldeclared (PClauses _ _ n _) = [] -- not a declaration

526tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]

527tldeclared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

528− where fstt (_, a, _, _) = a

528+ where fstt (_, a, _, _, _) = a

529tldeclared (PParams _ _ ds) = []

530tldeclared (PMutual _ ds) = concatMap tldeclared ds

531tldeclared (PNamespace _ ds) = concatMap tldeclared ds

@@ -540,7 +540,7 @@ defined (PPostulate _ _ _ _ n t) = []

540defined (PClauses _ _ n _) = [n] -- not a declaration

541defined (PCAF _ n _) = [n]

542defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

543− where fstt (_, a, _, _) = a

543+ where fstt (_, a, _, _, _) = a

544defined (PData _ _ _ _ (PLaterdecl n _)) = []

545defined (PParams _ _ ds) = concatMap defined ds

546defined (PNamespace _ ds) = concatMap defined ds

@@ -945,7 +945,7 @@ showDImp :: Bool -> PData -> String

945showDImp impl (PDatadecl n ty cons)

946 = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"

947 ++ showSep "\n\t| "

948− (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)

948+ (map (\ (_, n, t, _, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)

949

950getImps :: [PArg] -> [(Name, PTerm)]

951getImps [] = []

src/Idris/DataOpts.hs+6−3

@@ -18,14 +18,16 @@ type ForceMap = M.IntMap Forceability

19-- Calculate the forceable arguments to a constructor

20-- and update the set of optimisations.

21−forceArgs :: Name -> Name -> Type -> Idris ()

21+forceArgs :: Name -> Name -> [Int] -> Type -> Idris ()

22−forceArgs typeName n t = do

22+forceArgs typeName n expforce t = do

23 ist <- getIState

24 let fargs = getForcedArgs ist typeName t

25 copt = case lookupCtxt n (idris_optimisation ist) of

26 [] -> Optimise False False [] []

27 op:_ -> op

28− opts = addDef n (copt { forceable = M.toList fargs }) (idris_optimisation ist)

28+ opts = addDef n (copt { forceable = M.toList fargs ++

29+ zip expforce (repeat Unconditional) })

30+ (idris_optimisation ist)

29 putIState (ist { idris_optimisation = opts })

31 putIState (ist { idris_optimisation = opts })

30 addIBC (IBCOpt n)

32 addIBC (IBCOpt n)

31 iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t

33 iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t

@@ -319,3 +321,4 @@ applyDataOptRT oi n tag arity args

319 where

321 where

320 ctor' = (P (DCon tag (arity - forcedCnt forceMap)) n Erased)

322 ctor' = (P (DCon tag (arity - forcedCnt forceMap)) n Erased)

321 args' = [t | (f, t) <- zip (forcedArgSeq oi) args, f /= Just Unconditional]

323 args' = [t | (f, t) <- zip (forcedArgSeq oi) args, f /= Just Unconditional]

324+

src/Idris/ElabDecls.hs+24−15

@@ -304,7 +304,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

304type EliminatorState = StateT (Map.Map String Int) Idris

305

306-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

307−elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC)] -> ElabInfo -> EliminatorState ()

307+elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC, [Name])] ->

308+ ElabInfo -> EliminatorState ()

308elabEliminator paramPos n ty cons info = do

309elabEliminator paramPos n ty cons info = do

309 elimLog $ "Elaborating eliminator"

310 elimLog $ "Elaborating eliminator"

310 let (cnstrs, _) = splitPi ty

311 let (cnstrs, _) = splitPi ty

@@ -312,7 +313,7 @@ elabEliminator paramPos n ty cons info = do

312 generalParams <- namePis False pms

313 generalParams <- namePis False pms

313 motiveIdxs <- namePis False idxs

314 motiveIdxs <- namePis False idxs

314 let motive = mkMotive n paramPos generalParams motiveIdxs

315 let motive = mkMotive n paramPos generalParams motiveIdxs

315− consTerms <- mapM (\(c@(_,cnm,_,_)) -> do

316+ consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do

316 name <- freshName $ "elim_" ++ simpleName cnm

317 name <- freshName $ "elim_" ++ simpleName cnm

317 consTerm <- extractConsTerm c generalParams

318 consTerm <- extractConsTerm c generalParams

318 return (name, expl, consTerm)) cons

319 return (name, expl, consTerm)) cons

@@ -469,8 +470,8 @@ elabEliminator paramPos n ty cons info = do

469 splitArgPms _ = ([],[])

470 splitArgPms _ = ([],[])

470

471

472

472− implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]

473+ implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

473− implicitIndexes (cns@(doc, cnm, ty, fc)) = do

474+ implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do

474 i <- State.lift getIState

475 i <- State.lift getIState

475 implargs' <- case lookupCtxt cnm (idris_implicits i) of

476 implargs' <- case lookupCtxt cnm (idris_implicits i) of

476 [] -> do fail $ "Error while showing implicits for " ++ show cnm

477 [] -> do fail $ "Error while showing implicits for " ++ show cnm

@@ -484,11 +485,11 @@ elabEliminator paramPos n ty cons info = do

484 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

485 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

485 _ -> return implargs

486 _ -> return implargs

486

487

487− extractConsTerm :: (String, Name, PTerm, FC) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

488+ extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

488− extractConsTerm (doc, cnm, ty, fc) generalParameters = do

489+ extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do

489 let cons' = replaceParams paramPos generalParameters ty

490 let cons' = replaceParams paramPos generalParameters ty

490 let (args, resTy) = splitPi cons'

491 let (args, resTy) = splitPi cons'

491− implidxs <- implicitIndexes (doc, cnm, ty, fc)

492+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

492 consArgs <- namePis True args

493 consArgs <- namePis True args

493 let recArgs = findRecArgs consArgs

494 let recArgs = findRecArgs consArgs

494 let recMotives = map applyRecMotive recArgs

495 let recMotives = map applyRecMotive recArgs

@@ -520,12 +521,12 @@ elabEliminator paramPos n ty cons info = do

520 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

521 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

521 convertImplPi _ = Nothing

522 convertImplPi _ = Nothing

522

523

523− generateEliminatorClauses :: (String, Name, PTerm, FC) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

524+ generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

524− generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do

525+ generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

525 let cons' = replaceParams paramPos generalParameters ty

526 let cons' = replaceParams paramPos generalParameters ty

526 let (args, resTy) = splitPi cons'

527 let (args, resTy) = splitPi cons'

527 i <- State.lift getIState

528 i <- State.lift getIState

528− implidxs <- implicitIndexes (doc, cnm, ty, fc)

529+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

529 let (_, generalIdxs') = splitArgPms resTy

530 let (_, generalIdxs') = splitArgPms resTy

530 let generalIdxs = map pexp generalIdxs'

531 let generalIdxs = map pexp generalIdxs'

531 consArgs <- namePis True args

532 consArgs <- namePis True args

@@ -698,7 +699,7 @@ elabTransform info fc safe lhs_in rhs_in

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

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

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

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

700elabRecord info syn doc fc tyn ty cdoc cn cty

701elabRecord info syn doc fc tyn ty cdoc cn cty

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

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

702 cty' <- implicit syn cn cty

703 cty' <- implicit syn cn cty

703 i <- getIState

704 i <- getIState

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

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

@@ -805,8 +806,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

805 return (pn, pfnTy, PClauses fc [] setname [pclause])

806 return (pn, pfnTy, PClauses fc [] setname [pclause])

806

807

807elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

808elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

808− (String, Name, PTerm, FC) -> Idris (Name, Type)

809+ (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)

809−elabCon info syn tn codata (doc, n, t_in, fc)

810+elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

810 = do checkUndefined fc n

811 = do checkUndefined fc n

811 ctxt <- getContext

812 ctxt <- getContext

812 i <- getIState

813 i <- getIState

@@ -829,7 +830,10 @@ elabCon info syn tn codata (doc, n, t_in, fc)

829 addIBC (IBCDef n)

830 addIBC (IBCDef n)

830 addDocStr n doc

831 addDocStr n doc

831 addIBC (IBCDoc n)

832 addIBC (IBCDoc n)

833+ let fs = map (getNamePos 0 t) forcenames

834+ -- FIXME: 'forcenames' is an almighty hack! Need a better way of

835+ -- erasing non-forceable things

832− forceArgs tn n cty'

836+ forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'

833 return (n, cty')

837 return (n, cty')

834 where

838 where

835 tyIs (Bind n b sc) = tyIs sc

839 tyIs (Bind n b sc) = tyIs sc

@@ -841,6 +845,11 @@ elabCon info syn tn codata (doc, n, t_in, fc)

841 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

845 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

842 mkLazy t = t

846 mkLazy t = t

843

847

848+ getNamePos :: Int -> PTerm -> Name -> Maybe Int

849+ getNamePos i (PPi _ n _ sc) x | n == x = Just i

850+ | otherwise = getNamePos (i + 1) sc x

851+ getNamePos _ _ _ = Nothing

852+

844-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

853-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

845-- top-level definition.

854-- top-level definition.

846elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

855elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

@@ -1628,7 +1637,7 @@ elabClass info syn doc fc constraints tn ps ds

1628 let cty = impbind ps $ conbind constraints

1637 let cty = impbind ps $ conbind constraints

1629 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1638 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1630 constraint

1639 constraint

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

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

1632 let ddecl = PDatadecl tn tty cons

1641 let ddecl = PDatadecl tn tty cons

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

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

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

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

src/Idris/ParseData.hs+13−9

@@ -49,7 +49,7 @@ record syn = do (doc, acc) <- try (do

49 ty <- typeExpr (allowImp syn)

50 let tyn = expandNS syn tyn_in

51 reserved "where"

52− (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)

52+ (cdoc, cn, cty, _, _) <- indentedBlockS (constructor syn)

53 accData acc tyn [cn]

54 let rsyn = syn { syn_namespace = show (nsroot tyn) :

55 syn_namespace syn }

@@ -113,7 +113,7 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

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

114 reserved "where"

115 cons <- indentedBlock (constructor syn)

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

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

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

118 args <- many name

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

@@ -133,10 +133,10 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

133 cons <- sepBy1 (simpleConstructor syn) (lchar '|')

134 terminator

135 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

136− cons' <- mapM (\ (doc, x, cargs, cfc) ->

136+ cons' <- mapM (\ (doc, x, cargs, cfc, fs) ->

137 do let cty = bindArgs cargs conty

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

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

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

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

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

141 <?> "data type declaration"

142 where

@@ -152,20 +152,24 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

152{- | Parses a type constructor declaration

153 Constructor ::= DocComment? FnName TypeSig;

154-}

155−constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)

155+constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC, [Name])

156constructor syn

157 = do doc <- option "" (docComment '|')

158 cn_in <- fnName; fc <- getFC

159 let cn = expandNS syn cn_in

160 lchar ':'

161+ -- FIXME: 'forcenames' is an almighty hack! Need a better way of

162+ -- erasing non-forceable things

163+ fs <- option [] (do lchar '%'; reserved "erase"

164+ sepBy1 name (lchar ','))

161 ty <- typeExpr (allowImp syn)

165 ty <- typeExpr (allowImp syn)

162− return (doc, cn, ty, fc)

166+ return (doc, cn, ty, fc, fs)

163 <?> "constructor"

167 <?> "constructor"

164

168

165{- | Parses a constructor for simple discriminative union data types

169{- | Parses a constructor for simple discriminative union data types

166 SimpleConstructor ::= FnName SimpleExpr* DocComment?

170 SimpleConstructor ::= FnName SimpleExpr* DocComment?

167-}

171-}

168−simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)

172+simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC, [Name])

169simpleConstructor syn

173simpleConstructor syn

170 = do cn_in <- fnName

174 = do cn_in <- fnName

171 let cn = expandNS syn cn_in

175 let cn = expandNS syn cn_in

@@ -173,7 +177,7 @@ simpleConstructor syn

173 args <- many (do notEndApp

177 args <- many (do notEndApp

174 simpleExpr syn)

178 simpleExpr syn)

175 doc <- option "" (docComment '^')

179 doc <- option "" (docComment '^')

176− return (doc, cn, args, fc)

180+ return (doc, cn, args, fc, [])

177 <?> "constructor"

181 <?> "constructor"

178

182

179{- | Parses a dsl block declaration

183{- | Parses a dsl block declaration

src/Idris/ParseExpr.hs+1−1

@@ -580,7 +580,7 @@ implicitArg syn = do lchar '{'

580 v <- option (PRef fc n) (do lchar '='

581 expr syn)

582 lchar '}'

583− return (pimp n v False)

583+ return (pimp n v True)

584 <?> "implicit function argument"

585

586{-| Parses a constraint argument (for selecting a named type class instance)