ffc64e3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add mechanism for simplification and function options

commitffc64e379f565d822b888375f5b1d28562336c8a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 9 Nov 2011, 18:54 (15 years ago) parentd676ca6

9 files changed+83−52

compare with master

unifiedsplit

src/Core/CaseTree.hs+6−1 src/Core/Evaluate.hs+39−22 src/Idris/AbsSyntax.hs+12−7 src/Idris/Compiler.hs+1−1 src/Idris/ElabDecls.hs+12−11 src/Idris/Parser.hs+8−8 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+3−1 src/Idris/REPLParser.hs+1

src/Core/CaseTree.hs+6−1

@@ -1,5 +1,5 @@

11module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree,

2− simpleCase) where

2+ simpleCase, small) where

44import Core.TT

@@ -23,6 +23,11 @@ type CaseTree = SC

2323type Clause = ([Pat], Term)

2424type CS = Int

2525

26+-- simple terms can be inlined trivially - good for primitives in particular

27+small :: SC -> Bool

28+small (STerm t) = True

29+small _ = False

30+

2631simpleCase :: Bool -> [(Term, Term)] -> CaseDef

2732simpleCase tc [] = CaseDef [] (UnmatchedCase "No pattern clauses")

2833simpleCase tc cs = let pats = map (\ (l, r) -> (toPats tc l, r)) cs

src/Core/Evaluate.hs+39−22

@@ -1,7 +1,7 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

22 PatternGuards #-}

4−module Core.Evaluate(normalise, normaliseC, specialise, hnf,

4+module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,

55 Fun(..), Def(..), Context,

66 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

77 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

@@ -16,7 +16,7 @@ import Core.CaseTree

1616type EvalState = ()

1717type Eval a = State EvalState a

1818

19−data EvalOpt = Spec | HNF

19+data EvalOpt = Spec | HNF | Simplify

2020 deriving (Show, Eq)

2121

2222-- VALUES (as HOAS) ---------------------------------------------------------

@@ -66,6 +66,14 @@ specialise ctxt statics t

6666 = evalState (do val <- eval ctxt statics [] (finalise t) [Spec]

6767 quote 0 val) ()

6868

69+-- Like normalise, but we only reduce functions that are marked as okay to

70+-- inline (and probably shouldn't reduce lets?)

71+

72+simplify :: Context -> Env -> TT Name -> TT Name

73+simplify ctxt env t

74+ = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [Simplify]

75+ quote 0 val) ()

76+

6977hnf :: Context -> Env -> TT Name -> TT Name

7078hnf ctxt env t

7179 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) [HNF]

@@ -92,17 +100,20 @@ unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

92100eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value

93101eval ctxt statics genv tm opts = ev True [] tm where

94102 spec = Spec `elem` opts

103+ simpl = Simplify `elem` opts

95104

96105 ev top env (P _ n ty)

97106 | Just (Let t v) <- lookup n genv = ev top env v

98107 ev top env (P Ref n ty) = case lookupDef n ctxt of

99108 Just (Function (Fun _ _ _ v)) -> return v

100109 Just (TyDecl nt ty hty) -> return $ VP nt n hty

101− Just (CaseOp _ _ [] tree) ->

102− do c <- evCase top env [] [] tree

103− case c of

104− (Nothing, _) -> liftM (VP Ref n) (ev top env ty)

105− (Just v, _) -> return v

110+ Just (CaseOp inl _ _ [] tree) ->

111+ if simpl && (not inl)

112+ then liftM (VP Ref n) (ev top env ty)

113+ else do c <- evCase top env [] [] tree

114+ case c of

115+ (Nothing, _) -> liftM (VP Ref n) (ev top env ty)

116+ (Just v, _) -> return v

106117 _ -> liftM (VP Ref n) (ev top env ty)

107118 ev top env (P nt n ty) = liftM (VP nt n) (ev top env ty)

108119 ev top env (V i) | i < length env = return $ env !! i

@@ -137,12 +148,13 @@ eval ctxt statics genv tm opts = ev True [] tm where

137148 apply False env f args

138149 | spec = return $ unload env f args

139150 apply top env (VP Ref n ty) args

140− | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt

151+ | Just (CaseOp inl _ _ ns tree) <- lookupDef n ctxt

141152 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

142− do c <- evCase top env ns args tree

143− case c of

144− (Nothing, _) -> return $ unload env (VP Ref n ty) args

145− (Just v, rest) -> evApply top env rest v

153+ if simpl && (not inl) then return $ unload env (VP Ref n ty) args

154+ else do c <- evCase top env ns args tree

155+ case c of

156+ (Nothing, _) -> return $ unload env (VP Ref n ty) args

157+ (Just v, rest) -> evApply top env rest v

146158 | Just (Operator _ i op) <- lookupDef n ctxt

147159 = if (i <= length args)

148160 then case op (take i args) of

@@ -282,7 +294,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

282294 ev env (P Ref n ty) = case lookupDef n ctxt of

283295 Just (Function (Fun _ _ t _)) -> ev env t

284296 Just (TyDecl nt ty hty) -> return $ HP nt n ty

285− Just (CaseOp _ _ [] tree) ->

297+ Just (CaseOp inl _ _ [] tree) ->

286298 do c <- evCase env [] [] tree

287299 case c of

288300 (Nothing, _, _) -> return $ HP Ref n ty

@@ -312,7 +324,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

312324 app <- apply env sc' as

313325 wknH (-1) app

314326 apply env (HP Ref n ty) args

315− | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt

327+ | Just (CaseOp _ _ _ ns tree) <- lookupDef n ctxt

316328 = do c <- evCase env ns args tree

317329 case c of

318330 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

@@ -415,13 +427,14 @@ data Fun = Fun Type Value Term Value

415427data Def = Function Fun

416428 | TyDecl NameType Type Value

417429 | Operator Type Int ([Value] -> Maybe Value)

418− | CaseOp Type [(Term, Term)] [Name] SC

430+ | CaseOp Bool Type [(Term, Term)] [Name] SC -- Bool for inlineable

419431

420432instance Show Def where

421433 show (Function f) = "Function: " ++ show f

422434 show (TyDecl nt ty val) = "TyDecl: " ++ show nt ++ " " ++ show ty

423435 show (Operator ty _ _) = "Operator: " ++ show ty

424− show (CaseOp ty _ ns sc) = "Case: " ++ show ns ++ " " ++ show sc

436+ show (CaseOp _ ty ps ns sc) = "Case: " ++ show ps ++ "\n" ++

437+ show ns ++ " " ++ show sc

425438

426439-------

427440

@@ -448,10 +461,14 @@ addDatatype (Data n tag ty cons) ctxt

448461 addCons (tag+1) cons (addDef n

449462 (TyDecl (DCon tag (arity ty')) ty (veval ctxt [] ty)) ctxt)

450463

451−addCasedef :: Name -> Bool -> [(Term, Term)] -> Type -> Context -> Context

452−addCasedef n tcase ps ty ctxt

453− = case simpleCase tcase ps of

454− CaseDef args sc -> addDef n (CaseOp ty ps args sc) ctxt

464+addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

465+addCasedef n alwaysInline tcase ps ty ctxt

466+ = let ps' = simpl ps in

467+ case simpleCase tcase ps' of

468+ CaseDef args sc -> let inl = alwaysInline in

469+ addDef n (CaseOp inl ty ps args sc) ctxt

470+ where simpl [] = []

471+ simpl ((l,r) : xs) = (l, simplify ctxt [] r) : simpl xs

455472

456473addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

457474addOperator n ty a op ctxt

@@ -463,7 +480,7 @@ lookupTy n ctxt = do def <- lookupCtxt n ctxt

463480 (Function (Fun ty _ _ _)) -> return ty

464481 (TyDecl _ ty _) -> return ty

465482 (Operator ty _ _) -> return ty

466− (CaseOp ty _ _ _) -> return ty

483+ (CaseOp _ ty _ _ _) -> return ty

467484

468485lookupP :: Name -> Context -> Maybe Term

469486lookupP n ctxt

@@ -471,7 +488,7 @@ lookupP n ctxt

471488 case def of

472489 (Function (Fun ty _ tm _)) -> return (P Ref n ty)

473490 (TyDecl nt ty hty) -> return (P nt n ty)

474− (CaseOp ty _ _ _) -> return (P Ref n ty)

491+ (CaseOp _ ty _ _ _) -> return (P Ref n ty)

475492 (Operator ty _ _) -> return (P Ref n ty)

476493

477494lookupDef :: Name -> Context -> Maybe Def

src/Idris/AbsSyntax.hs+12−7

146146 | Compile String | Execute String

147147 | Metavars | Prove Name

148148 | TTShell

149− | LogLvl Int | Spec PTerm | HNF PTerm

149+ | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

150150 | NOP

151151

152152-- Parsed declarations

@@ -186,9 +186,14 @@ impl = Imp False Dynamic

186186expl = Exp False Dynamic

187187constraint = Constraint False Static

188188

189+type FnOpts = Bool -- just inlinable, for now

190+

191+inlinable :: FnOpts -> Bool

192+inlinable x = x

193+

189194data PDecl' t = PFix FC Fixity [String] -- fixity declaration

190195 | PTy SyntaxInfo FC Name t -- type declaration

191− | PClauses FC Name [PClause' t] -- pattern clause

196+ | PClauses FC FnOpts Name [PClause' t] -- pattern clause

192197 | PData SyntaxInfo FC (PData' t) -- data declaration

193198 | PParams FC [(Name, t)] [PDecl' t] -- params block

194199 | PClass SyntaxInfo FC

@@ -225,7 +230,7 @@ type PClause = PClause' PTerm

225230declared :: PDecl -> [Name]

226231declared (PFix _ _ _) = []

227232declared (PTy _ _ n t) = [n]

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

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

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

230235 where fstt (a, _, _) = a

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

@@ -369,7 +374,7 @@ instance Show PTerm where

369374instance Show PDecl where

370375 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

371376 show (PTy _ _ n ty) = show n ++ " : " ++ show ty

372− show (PClauses _ n c) = showSep "\n" (map show c)

377+ show (PClauses _ _ n c) = showSep "\n" (map show c)

373378 show (PData _ _ d) = show d

374379

375380instance Show PClause where

@@ -611,9 +616,9 @@ expandParamsD ist dec ps ns (PTy syn fc n ty)

611616 = if n `elem` ns

612617 then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))

613618 else PTy syn fc n (expandParams dec ps ns ty)

614−expandParamsD ist dec ps ns (PClauses fc n cs)

619+expandParamsD ist dec ps ns (PClauses fc opts n cs)

615620 = let n' = if n `elem` ns then dec n else n in

616− PClauses fc n' (map expandParamsC cs)

621+ PClauses fc opts n' (map expandParamsC cs)

617622 where

618623 expandParamsC (PClause n lhs ws rhs ds)

619624 = let ps' = updateps True (namesIn ist rhs) (zip ps [0..])

@@ -859,7 +864,7 @@ dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

859864

860865dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

861866dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

862−dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

867+dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

863868dumpDecl (PData _ _ d) = showDImp True d

864869dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

865870dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

src/Idris/Compiler.hs+1−1

@@ -46,7 +46,7 @@ impossible = int 42424242

4646

4747instance ToEpic Def where

4848 epic (Function (Fun _ _ tm _)) = epic tm

49− epic (CaseOp _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising

49+ epic (CaseOp _ _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising

5050 epic _ = return impossible

5151

5252instance ToEpic (TT Name) where

src/Idris/ElabDecls.hs+12−11

@@ -85,8 +85,8 @@ elabCon info syn (n, t_in, fc)

8585 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

8686 return (n, cty)

8787

88−elabClauses :: ElabInfo -> FC -> Name -> [PClause] -> Idris ()

89−elabClauses info fc n_in cs = let n = liftname info n_in in

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

89+elabClauses info fc opts n_in cs = let n = liftname info n_in in

9090 do solveDeferred n

9191 pats <- mapM (elabClause info fc) cs

9292 logLvl 3 (showSep "\n" (map (\ (l,r) ->

@@ -98,7 +98,8 @@ elabClauses info fc n_in cs = let n = liftname info n_in in

9898 logLvl 3 (show tree)

9999 ctxt <- getContext

100100 case lookupTy n ctxt of

101− Just ty -> updateContext (addCasedef n tcase (map debind pats) ty)

101+ Just ty -> updateContext (addCasedef n (inlinable opts)

102+ tcase (map debind pats) ty)

102103 Nothing -> return ()

103104 where

104105 debind (x, y) = (depat x, depat y)

@@ -249,9 +250,9 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

249250 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

250251 getImps _ = []

251252

252− mkAuxC wname lhs ns (PClauses fc n cs)

253+ mkAuxC wname lhs ns (PClauses fc o n cs)

253254 | n == fname = do cs' <- mapM (mkAux wname lhs ns) cs

254− return $ PClauses fc wname cs'

255+ return $ PClauses fc o wname cs'

255256 | otherwise = fail $ "with clause uses wrong function name " ++ show n

256257 mkAuxC wname lhs ns d = return $ d

257258

@@ -313,7 +314,7 @@ elabClass info syn fc constraints tn ps ds

313314 tdecl (PTy syn _ n t) = do t' <- implicit syn n t

314315 return ( (n, (toExp (map fst ps) Exp t')),

315316 (n, (toExp (map fst ps) Imp t')) )

316− tdecl (PClauses _ _ _) = fail "No default definitions allowed yet"

317+ tdecl (PClauses _ _ _ _) = fail "No default definitions allowed yet"

317318 tdecl _ = fail "Not allowed in a class declaration"

318319

319320 tfun cn c syn all (m, ty)

@@ -328,7 +329,7 @@ elabClass info syn fc constraints tn ps ds

328329 iLOG (show (m, ty', capp, margs))

329330 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

330331 return [PTy syn fc m ty',

331− PClauses fc m [PClause m lhs [] rhs []]]

332+ PClauses fc True m [PClause m lhs [] rhs []]]

332333

333334 getMArgs (PPi (Imp _ _) n ty sc) = False : getMArgs sc

334335 getMArgs (PPi (Exp _ _) n ty sc) = True : getMArgs sc

@@ -374,7 +375,7 @@ elabInstance info syn fc cs n ps t ds

374375 let lhs = PRef fc iname

375376 let rhs = PApp fc (PRef fc (instanceName ci))

376377 (map (pexp . mkMethApp) mtys)

377− let idecl = PClauses fc iname [PClause iname lhs [] rhs wb]

378+ let idecl = PClauses fc True iname [PClause iname lhs [] rhs wb]

378379 iLOG (show idecl)

379380 elabDecl info idecl

380381 where

@@ -394,7 +395,7 @@ elabInstance info syn fc cs n ps t ds

394395 papp fc f as = PApp fc f as

395396 decorate (UN (n:ns)) = UN (('!':n) : ns)

396397 decorateid (PTy s f n t) = PTy s f (decorate n) t

397− decorateid (PClauses f n cs) = PClauses f (decorate n) (map dc cs)

398+ decorateid (PClauses f o n cs) = PClauses f o (decorate n) (map dc cs)

398399 where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds

399400 dc (PWith n t as w ds) = PWith (decorate n) (dappname t) as w ds

400401 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

@@ -442,8 +443,8 @@ elabDecl' info (PTy s f n ty) = do iLOG $ "Elaborating type decl " ++ show n

442443 elabType info s f n ty

443444elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d)

444445 elabData info s f d

445−elabDecl' info d@(PClauses f n ps) = do iLOG $ "Elaborating clause " ++ show n

446− elabClauses info f n ps

446+elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n

447+ elabClauses info f o n ps

447448elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

448449 where

449450 pinfo = let ds = concatMap declared ps

src/Idris/Parser.hs+8−8

@@ -132,17 +132,17 @@ parseProg syn fname input pos

132132-- Collect PClauses with the same function name

133133

134134collect :: [PDecl] -> [PDecl]

135−collect (c@(PClauses _ _ _) : ds)

135+collect (c@(PClauses _ o _ _) : ds)

136136 = clauses (cname c) [] (c : ds)

137− where clauses n acc (PClauses fc _ [PClause n' l ws r w] : ds)

137+ where clauses n acc (PClauses fc _ _ [PClause n' l ws r w] : ds)

138138 | n == n' = clauses n (PClause n' l ws r (collect w) : acc) ds

139− clauses n acc (PClauses fc _ [PWith n' l ws r w] : ds)

139+ clauses n acc (PClauses fc _ _ [PWith n' l ws r w] : ds)

140140 | n == n' = clauses n (PWith n' l ws r (collect w) : acc) ds

141− clauses n acc xs = PClauses (getfc c) n (reverse acc) : collect xs

141+ clauses n acc xs = PClauses (getfc c) o n (reverse acc) : collect xs

142142

143− cname (PClauses fc _ [PClause n _ _ _ _]) = n

144− cname (PClauses fc _ [PWith n _ _ _ _]) = n

145− getfc (PClauses fc _ _) = fc

143+ cname (PClauses fc _ _ [PClause n _ _ _ _]) = n

144+ cname (PClauses fc _ _ [PWith n _ _ _ _]) = n

145+ getfc (PClauses fc _ _ _) = fc

146146

147147collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

148148collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'

@@ -591,7 +591,7 @@ pSimpleCon syn

591591pPattern :: SyntaxInfo -> IParser PDecl

592592pPattern syn = do clause <- pClause syn

593593 fc <- pfc

594− return (PClauses fc (MN 2 "_") [clause]) -- collect together later

594+ return (PClauses fc False (MN 2 "_") [clause]) -- collect together later

595595

596596whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo

597597whereSyn n syn args = let ns = concatMap allNamesIn args

src/Idris/Prover.hs+1−1

@@ -38,7 +38,7 @@ prove ctxt n ty

3838 let tree = simpleCase False [(P Ref n ty, tm)]

3939 logLvl 3 (show tree)

4040 (ptm, pty) <- tclift $ recheck ctxt [] tm

41− updateContext (addCasedef n False [(P Ref n ty, ptm)] ty)

41+ updateContext (addCasedef n True False [(P Ref n ty, ptm)] ty)

4242 solveDeferred n

4343

4444elabStep :: ElabState -> Elab a -> Idris (a, ElabState)

src/Idris/REPL.hs+3−1

@@ -92,6 +92,8 @@ process _ (Check t) = do (tm, ty) <- elabVal toplevel False t

9292 let ty' = normaliseC ctxt [] ty

9393 iputStrLn (show (delab ist tm) ++ " : " ++

9494 show (delab ist ty'))

95+process _ (Defn n) = do ctxt <- getContext

96+ lift $ print (lookupDef n ctxt)

9597process _ (Spec t) = do (tm, ty) <- elabVal toplevel False t

9698 ctxt <- getContext

9799 ist <- get

@@ -101,7 +103,7 @@ process _ (Prove n) = prover n

101103process _ (HNF t) = do (tm, ty) <- elabVal toplevel False t

102104 ctxt <- getContext

103105 ist <- get

104− let tm' = hnf ctxt [] tm

106+ let tm' = simplify ctxt [] tm

105107 iputStrLn (show (delab ist tm'))

106108process _ TTShell = do ist <- get

107109 let shst = initState (tt_ctxt ist)

src/Idris/REPLParser.hs+1

@@ -32,6 +32,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

3232 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

3333 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

3434 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

35+ <|> try (do cmd ["d", "def"]; n <- pName; eof; return (Defn n))

3536 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

3637 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

3738 <|> do eof; return NOP