ac25f15 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Changed contexts to Data.Map

ac25f15Edwin Brady15 years ago

miniidris.cabal+2−1

compare with master

unifiedsplit

@@ -21,7 +21,8 @@ Executable miniidris

21 ProofState, CoreParser, ShellParser,

22 Unify, Elaborate

24− Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline

24+ Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

25+ containers

26 Extensions: MultiParamTypeClasses, FunctionalDependencies,

27 Extensions: MultiParamTypeClasses, FunctionalDependencies,

27 FlexibleInstances

28 FlexibleInstances

src/Core.hs+1−1

@@ -54,7 +54,7 @@ instance MonadPlus TC where

55data Name = UN [String]

56 | MN Int String

57− deriving Eq

57+ deriving (Eq, Ord)

59instance Show Name where

60 show (UN [n]) = n

src/Elaborate.hs+8−21

@@ -191,24 +191,11 @@ arg n tyhole = do ty <- unique_hole tyhole

191 claim ty (RSet 0)

192 forall n (Var ty)

193

194−-- patarg :: Name -> Name -> Elab ()

195−-- patarg n tyhole = do ty <- unique_hole tyhole

196−-- claim ty (RSet 0)

197−-- patvar n (Var ty)

198−

199−-- Some combinators on elaborations

200−

201−-- Sequencing

202−-- infixr 5 ==>

203−

204−-- (==>) :: Elab -> Elab -> Elab

205−-- (==>) t1 t2 ps = do (ps', log') <- t1 ps

206−-- (ps'', log'') <- t2 ps'

207−-- return (ps'', log' ++ log')

208−--

209−-- -- Try a tactic, if it fails, try another

194+-- Try a tactic, if it fails, try another

210−-- try :: Elab -> Elab -> Elab

195+try :: Elab a -> Elab a -> Elab a

211−-- try t1 t2 ps = case t1 ps of

196+try t1 t2 = do s <- get

197+ case runStateT t1 s of

198+ OK (v, s') -> do put s'

212−-- OK v -> return v

199+ return v

213−-- _ -> t2 ps

200+ _ -> t2

214−--

201+

src/Evaluate.hs+25−5

@@ -1,10 +1,11 @@

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

3module Evaluate(normalise,

4− Fun(..), Def(..), Context,

4+ Fun(..), Def(..), Context, toAlist,

5 emptyContext, addToCtxt, addConstant, addDatatype,

6 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where

8+import qualified Data.Map as Map

8import Debug.Trace

9import Debug.Trace

9import Core

10import Core

@@ -97,6 +98,7 @@ data Def = Function Fun

97 | Constant NameType Type Value

98 | Constant NameType Type Value

98 deriving Show

99 deriving Show

100

101+{-

100type Context = [(Name, Def)]

102type Context = [(Name, Def)]

101

103

102emptyContext = []

104emptyContext = []

@@ -104,6 +106,24 @@ emptyContext = []

104addDef :: Name -> Def -> Context -> Context

106addDef :: Name -> Def -> Context -> Context

105addDef n d ctxt = (n, d) : ctxt

107addDef n d ctxt = (n, d) : ctxt

106

108

109+lookupCtxt :: Name -> Context -> Maybe Def

110+lookupCtxt n c = lookup n c

111+-}

112+

113+type Context = Map.Map Name Def

114+emptyContext = Map.empty

115+

116+addDef :: Name -> Def -> Context -> Context

117+addDef = Map.insert

118+

119+lookupCtxt :: Name -> Context -> Maybe Def

120+lookupCtxt = Map.lookup

121+

122+toAlist :: Context -> [(Name, Def)]

123+toAlist = Map.toList

124+

125+-------

126+

107addToCtxt :: Name -> Term -> Type -> Context -> Context

127addToCtxt :: Name -> Term -> Type -> Context -> Context

108addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)

128addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)

109 tm (eval ctxt [] tm))) ctxt

129 tm (eval ctxt [] tm))) ctxt

@@ -124,28 +144,28 @@ addDatatype (Data n ty cons) ctxt

124 (Constant (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)

144 (Constant (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)

125

145

126lookupTy :: Name -> Context -> Maybe Type

146lookupTy :: Name -> Context -> Maybe Type

127−lookupTy n ctxt = do def <- lookup n ctxt

147+lookupTy n ctxt = do def <- lookupCtxt n ctxt

128 case def of

148 case def of

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

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

130 (Constant _ ty _) -> return ty

150 (Constant _ ty _) -> return ty

131

151

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

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

133lookupP n ctxt

153lookupP n ctxt

134− = do def <- lookup n ctxt

154+ = do def <- lookupCtxt n ctxt

135 case def of

155 case def of

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

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

137 (Constant nt ty hty) -> return (P nt n ty)

157 (Constant nt ty hty) -> return (P nt n ty)

138

158

139lookupDef :: Name -> Context -> Maybe Term

159lookupDef :: Name -> Context -> Maybe Term

140lookupDef n ctxt

160lookupDef n ctxt

141− = do def <- lookup n ctxt

161+ = do def <- lookupCtxt n ctxt

142 case def of

162 case def of

143 (Function (Fun ty _ tm _)) -> return tm

163 (Function (Fun ty _ tm _)) -> return tm

144 (Constant nt ty hty) -> return (P nt n ty)

164 (Constant nt ty hty) -> return (P nt n ty)

145

165

146lookupVal :: Name -> Context -> Maybe Value

166lookupVal :: Name -> Context -> Maybe Value

147lookupVal n ctxt

167lookupVal n ctxt

148− = do def <- lookup n ctxt

168+ = do def <- lookupCtxt n ctxt

149 case def of

169 case def of

150 (Function (Fun _ _ _ htm)) -> return htm

170 (Function (Fun _ _ _ htm)) -> return htm

151 (Constant nt ty hty) -> return (VP nt n hty)

171 (Constant nt ty hty) -> return (VP nt n hty)

src/Main.hs+3−2

@@ -5,14 +5,15 @@ import ShellParser

5import Core

6import Typecheck

7import ProofShell

8+import Evaluate

9main = do f <- readFile "test.mi"

10main = do f <- readFile "test.mi"

10 case parseFile f of

11 case parseFile f of

11 Left err -> print err

12 Left err -> print err

12 Right defs -> do

13 Right defs -> do

13 print defs

14 print defs

14− case checkProgram [] defs of

15+ case checkProgram emptyContext defs of

15− OK ctxt -> do print ctxt

16+ OK ctxt -> do print (toAlist ctxt)

16 runShell (initState ctxt)

17 runShell (initState ctxt)

17 return ()

18 return ()

18 err -> print err

19 err -> print err