d337b5d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Performance/compiler temporary hack: %erase

This is a (temporary!) annotation for erasing implicit constructor arguments which are not forceable, and would otherwise remain in compiled code. e.g.: data Binary : (width : Nat) -> (value : Nat) -> Type where zero : Binary Z Z num : %erase bit, v Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v) This would erase 'bit' and 'v' from the num constructor (w is already forceable). If bit or v is required for any reason, compilation will fail. This is a TEMPORARY HACK (no, honestly, it is) until we have more general erasure of implicit arguments (which is coming) but this is a placeholder which is required for some existing examples. Use at your own risk! Note that any code which abuses this will fail to compile, so it is at least sound...

commitd337b5d75a4735e038f35b551cf7790b970851a2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 19 Jan 2014, 20:16 (13 years ago) parent32b66c5

6 files changed+55−39

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6−6 src/Idris/AbsSyntaxTree.hs+5−5 src/Idris/DataOpts.hs+6−3 src/Idris/ElabDecls.hs+24−15 src/Idris/ParseData.hs+13−9 src/Idris/ParseExpr.hs+1−1

src/Idris/AbsSyntax.hs+6−6

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

698698 PType

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

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

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

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

702702inferOpts = []

703703

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

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

721721unitTy = sMN 0 "__Unit"

722722unitCon = sMN 0 "__II"

723723unitDecl = PDatadecl unitTy PType

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

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

725725unitOpts = [DefaultEliminator]

726726

727727falseTy = sMN 0 "__False"

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

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

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

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

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

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

740740 where n a = sMN 0 a

741741pairOpts = []

742742

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

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

751751 pimp (n "B") Placeholder False,

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

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

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

754754 where n a = sMN 0 a

755755eqOpts = []

756756

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

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

922922 (map econ cons)

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

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

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

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

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

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

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

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

src/Idris/AbsSyntaxTree.hs+5−5

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

478478-- | Data declaration

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

480480 d_tcon :: t, -- ^ Type constructor

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

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

482482 }

483483 -- ^ Data declaration

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

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

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

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

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

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

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

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

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

511511declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

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

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

529529tldeclared (PParams _ _ ds) = []

530530tldeclared (PMutual _ ds) = concatMap tldeclared ds

531531tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

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

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

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

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

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

546546defined (PNamespace _ ds) = concatMap defined ds

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

945945showDImp impl (PDatadecl n ty cons)

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

947947 ++ 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)

949949

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

951951getImps [] = []

src/Idris/DataOpts.hs+6−3

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

1818

1919-- Calculate the forceable arguments to a constructor

2020-- and update the set of optimisations.

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

22−forceArgs typeName n t = do

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

22+forceArgs typeName n expforce t = do

2323 ist <- getIState

2424 let fargs = getForcedArgs ist typeName t

2525 copt = case lookupCtxt n (idris_optimisation ist) of

2626 [] -> Optimise False False [] []

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

2931 putIState (ist { idris_optimisation = opts })

3032 addIBC (IBCOpt n)

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

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

319321 where

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

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

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

305305

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

308309elabEliminator paramPos n ty cons info = do

309310 elimLog $ "Elaborating eliminator"

310311 let (cnstrs, _) = splitPi ty

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

312313 generalParams <- namePis False pms

313314 motiveIdxs <- namePis False idxs

314315 let motive = mkMotive n paramPos generalParams motiveIdxs

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

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

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

317318 consTerm <- extractConsTerm c generalParams

318319 return (name, expl, consTerm)) cons

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

469470 splitArgPms _ = ([],[])

470471

471472

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

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

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

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

474475 i <- State.lift getIState

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

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

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

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

485486 _ -> return implargs

486487

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

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

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

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

489490 let cons' = replaceParams paramPos generalParameters ty

490491 let (args, resTy) = splitPi cons'

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

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

492493 consArgs <- namePis True args

493494 let recArgs = findRecArgs consArgs

494495 let recMotives = map applyRecMotive recArgs

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

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

521522 convertImplPi _ = Nothing

522523

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

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

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

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

525526 let cons' = replaceParams paramPos generalParameters ty

526527 let (args, resTy) = splitPi cons'

527528 i <- State.lift getIState

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

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

529530 let (_, generalIdxs') = splitArgPms resTy

530531 let generalIdxs = map pexp generalIdxs'

531532 consArgs <- namePis True args

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

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

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

700701elabRecord 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, [])])

702703 cty' <- implicit syn cn cty

703704 i <- getIState

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

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

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

806807

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

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

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

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

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

810811 = do checkUndefined fc n

811812 ctxt <- getContext

812813 i <- getIState

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

829830 addIBC (IBCDef n)

830831 addDocStr n doc

831832 addIBC (IBCDoc n)

832− forceArgs tn n cty'

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

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

833837 return (n, cty')

834838 where

835839 tyIs (Bind n b sc) = tyIs sc

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

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

842846 mkLazy t = t

843847

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+

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

845854-- top-level definition.

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

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

16281637 let cty = impbind ps $ conbind constraints

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

16301639 constraint

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

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

16321641 let ddecl = PDatadecl tn tty cons

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

16341643 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

4949 ty <- typeExpr (allowImp syn)

5050 let tyn = expandNS syn tyn_in

5151 reserved "where"

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

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

5353 accData acc tyn [cn]

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

5555 syn_namespace syn }

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

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

114114 reserved "where"

115115 cons <- indentedBlock (constructor syn)

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

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

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

118118 args <- many name

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

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

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

134134 terminator

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

137137 do let cty = bindArgs cargs conty

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

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

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

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

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

141141 <?> "data type declaration"

142142 where

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

152152{- | Parses a type constructor declaration

153153 Constructor ::= DocComment? FnName TypeSig;

154154-}

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

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

156156constructor syn

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

158158 cn_in <- fnName; fc <- getFC

159159 let cn = expandNS syn cn_in

160160 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 ','))

161165 ty <- typeExpr (allowImp syn)

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

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

163167 <?> "constructor"

164168

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

166170 SimpleConstructor ::= FnName SimpleExpr* DocComment?

167171-}

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

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

169173simpleConstructor syn

170174 = do cn_in <- fnName

171175 let cn = expandNS syn cn_in

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

173177 args <- many (do notEndApp

174178 simpleExpr syn)

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

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

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

177181 <?> "constructor"

178182

179183{- | Parses a dsl block declaration

src/Idris/ParseExpr.hs+1−1

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

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

581581 expr syn)

582582 lchar '}'

583− return (pimp n v False)

583+ return (pimp n v True)

584584 <?> "implicit function argument"

585585

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