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

git.iko.soy/Idris-dev

on master help sign in

Add %static annotation on functions

7c1a2c6Edwin Brady10 years ago

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -660,6 +660,7 @@ data FnOpt = Inlinable -- ^ always evaluate when simplifying

660 | Constructor -- ^ Data constructor type

661 | AutoHint -- ^ use in auto implicit search

662 | PEGenerated -- ^ generated by partial evaluator

663+ | StaticFn -- ^ Marked static, to be evaluated by partial evaluator

663 deriving (Show, Eq, Generic)

664 deriving (Show, Eq, Generic)

664{-!

665{-!

665deriving instance Binary FnOpt

666deriving instance Binary FnOpt

src/Idris/Elab/Clause.hs+20−3

@@ -397,12 +397,15 @@ elabPE info fc caller r =

397 [Total _] -> 65536

398 [Productive] -> 16

399 _ -> 1

400+ let specnames = mapMaybe (specName (pe_simple specdecl))

401+ (snd specapp)

402+ descs <- mapM getStaticsFrom (map fst specnames)

403+

400 let opts = [Specialise ((if pe_simple specdecl

404 let opts = [Specialise ((if pe_simple specdecl

401 then map (\x -> (x, Nothing)) cgns'

405 then map (\x -> (x, Nothing)) cgns'

402 else []) ++

406 else []) ++

403− (n, Just maxred) :

407+ (n, Just maxred) : specnames ++

404− mapMaybe (specName (pe_simple specdecl))

408+ concat descs)]

405− (snd specapp))]

406 logElab 3 $ "Specialising application: " ++ show specapp

409 logElab 3 $ "Specialising application: " ++ show specapp

407 ++ " in " ++ show caller ++

410 ++ " in " ++ show caller ++

408 " with " ++ show opts

411 " with " ++ show opts

@@ -443,6 +446,20 @@ elabPE info fc caller r =

443 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

446 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

444 specName simpl _ = Nothing

447 specName simpl _ = Nothing

445

448

449+ -- get the descendants of the name 'n' which are marked %static

450+ -- Marking a function %static essentially means it's used to construct

451+ -- programs, so should be evaluated by the partial evaluator

452+ getStaticsFrom :: Name -> Idris [(Name, Maybe Int)]

453+ getStaticsFrom n = do ns <- getAllNames n

454+ i <- getIState

455+ let statics = filter (staticFn i) ns

456+ return (map (\n -> (n, Nothing)) statics)

457+

458+ staticFn :: IState -> Name -> Bool

459+ staticFn i n = case lookupCtxt n (idris_flags i) of

460+ [opts] -> elem StaticFn opts

461+ _ -> False

462+

446 notStatic ist n = case lookupCtxtExact n (idris_statics ist) of

463 notStatic ist n = case lookupCtxtExact n (idris_statics ist) of

447 Just s -> not (or s)

464 Just s -> not (or s)

448 _ -> True

465 _ -> True

src/Idris/IBC.hs+2

@@ -1223,6 +1223,7 @@ instance Binary FnOpt where

1223 put x1

1224 AutoHint -> putWord8 15

1225 PEGenerated -> putWord8 16

1226+ StaticFn -> putWord8 17

1226 get

1227 get

1227 = do i <- getWord8

1228 = do i <- getWord8

1228 case i of

1229 case i of

@@ -1245,6 +1246,7 @@ instance Binary FnOpt where

1245 return $ CExport x1

1246 return $ CExport x1

1246 15 -> return AutoHint

1247 15 -> return AutoHint

1247 16 -> return PEGenerated

1248 16 -> return PEGenerated

1249+ 17 -> return StaticFn

1248 _ -> error "Corrupted binary data for FnOpt"

1250 _ -> error "Corrupted binary data for FnOpt"

1249

1251

1250instance Binary Fixity where

1252instance Binary Fixity where

src/Idris/Parser.hs+2

@@ -685,6 +685,8 @@ fnOpt = do reservedHL "total"; return TotalFn

685 return NoImplicit

686 <|> do try (lchar '%' *> reserved "inline");

687 return Inlinable

688+ <|> do try (lchar '%' *> reserved "static");

689+ return StaticFn

688 <|> do try (lchar '%' *> reserved "assert_total");

690 <|> do try (lchar '%' *> reserved "assert_total");

689 fc <- getFC

691 fc <- getFC

690 parserWarning fc Nothing (Msg "%assert_total is deprecated. Use the 'assert_total' function instead.")

692 parserWarning fc Nothing (Msg "%assert_total is deprecated. Use the 'assert_total' function instead.")