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

git.iko.soy/Idris-dev

Add %static annotation on functions

This marks a function as one which should be reduced by the partial evaluator whenever the evaluator encounters it (that is, the function is used for metaprogramming).

commit7c1a2c606b155a68c365f42dd00cda418a437a26 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 27 Aug 2016, 08:53 (10 years ago) parentff776da

4 files changed+25−3

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/Elab/Clause.hs+20−3 src/Idris/IBC.hs+2 src/Idris/Parser.hs+2

src/Idris/AbsSyntaxTree.hs+1

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

660660 | Constructor -- ^ Data constructor type

661661 | AutoHint -- ^ use in auto implicit search

662662 | PEGenerated -- ^ generated by partial evaluator

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

663664 deriving (Show, Eq, Generic)

664665{-!

665666deriving instance Binary FnOpt

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

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

397397 [Total _] -> 65536

398398 [Productive] -> 16

399399 _ -> 1

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

401+ (snd specapp)

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

403+

400404 let opts = [Specialise ((if pe_simple specdecl

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

402406 else []) ++

403− (n, Just maxred) :

404− mapMaybe (specName (pe_simple specdecl))

405− (snd specapp))]

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

408+ concat descs)]

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

407410 ++ " in " ++ show caller ++

408411 " with " ++ show opts

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

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

444447 specName simpl _ = Nothing

445448

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+

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

447464 Just s -> not (or s)

448465 _ -> True

src/Idris/IBC.hs+2

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

12231223 put x1

12241224 AutoHint -> putWord8 15

12251225 PEGenerated -> putWord8 16

1226+ StaticFn -> putWord8 17

12261227 get

12271228 = do i <- getWord8

12281229 case i of

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

12451246 return $ CExport x1

12461247 15 -> return AutoHint

12471248 16 -> return PEGenerated

1249+ 17 -> return StaticFn

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

12491251

12501252instance Binary Fixity where

src/Idris/Parser.hs+2

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

685685 return NoImplicit

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

687687 return Inlinable

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

689+ return StaticFn

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

689691 fc <- getFC

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