77be0d0 · Idris-dev · git.iko.soy

miniidris.cabal+2−1

compare with master

unifiedsplit

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

18 Main-is: Main.hs

19 hs-source-dirs: src

20 Other-modules: Core, Evaluate, Typecheck, ProofState,

21− ProofState, CoreParser, ShellParser

21+ ProofState, CoreParser, ShellParser,

22+ Unify

22

23

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

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

24

25

src/Core.hs+39

@@ -22,6 +22,30 @@ data Option = SetInSet

22 | CheckConv

23 deriving Eq

24

25+data TC a = OK a

26+ | Error String -- TMP! Make this an informative data structure

27+ deriving (Eq, Functor)

28+

29+instance Show a => Show (TC a) where

30+ show (OK x) = show x

31+ show (Error str) = "Error: " ++ str

32+

33+-- at some point, this instance should also carry type checking options

34+-- (e.g. Set:Set)

35+

36+instance Monad TC where

37+ return = OK

38+ x >>= k = case x of

39+ OK v -> k v

40+ Error e -> Error e

41+ fail = Error

42+

43+instance MonadPlus TC where

44+ mzero = Error "Unknown error"

45+ (OK x) `mplus` _ = OK x

46+ _ `mplus` (OK y) = OK y

47+ err `mplus` _ = err

48+

25-- RAW TERMS ----------------------------------------------------------------

49-- RAW TERMS ----------------------------------------------------------------

26

50

27-- Names are hierarchies of strings, describing scope (so no danger of

51-- Names are hierarchies of strings, describing scope (so no danger of

@@ -60,8 +84,12 @@ data RawFun = RawFun { rtype :: Raw,

60 }

84 }

61 deriving Show

85 deriving Show

62

86

87+data RawDatatype = RDatatype Name Raw [(Name, Raw)]

88+ deriving Show

89+

63data RDef = RFunction RawFun

90data RDef = RFunction RawFun

64 | RConst Raw

91 | RConst Raw

92+ | RData RawDatatype

65 deriving Show

93 deriving Show

66

94

67type RProgram = [(Name, RDef)]

95type RProgram = [(Name, RDef)]

@@ -82,6 +110,11 @@ data TT n = P NameType n (TT n) -- embed type

82

110

83type EnvTT n = [(n, Binder (TT n))]

111type EnvTT n = [(n, Binder (TT n))]

84

112

113+data Datatype n = Data { d_typename :: n,

114+ d_type :: (TT n),

115+ d_cons :: [(n, TT n)] }

116+ deriving (Show, Functor, Eq)

117+

85-- Returns true if V 0 and bound name n do not occur in the term

118-- Returns true if V 0 and bound name n do not occur in the term

86

119

87noOccurrence :: Eq n => n -> TT n -> Bool

120noOccurrence :: Eq n => n -> TT n -> Bool

@@ -96,6 +129,12 @@ noOccurrence n t = no' 0 t

96 no' i (App f a) = no' i f && no' i a

129 no' i (App f a) = no' i f && no' i a

97 no' i _ = True

130 no' i _ = True

98

131

132+-- Return the arity of a (normalised) type

133+

134+arity :: TT n -> Int

135+arity (Bind n (Pi t) sc) = 1 + arity sc

136+arity _ = 0

137+

99type Term = TT Name

138type Term = TT Name

100type Type = Term

139type Type = Term

101

140

src/CoreParser.hs+12

@@ -47,6 +47,8 @@ pDef = try (do x <- iName; lchar ':'; ty <- pTerm

47 return (x, RFunction (RawFun ty tm)))

48 <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'

49 return (x, RConst ty)

50+ <|> do (x, d) <- pData

51+ return (x, RData d)

50

52

51app :: Parser (Raw -> Raw -> Raw)

53app :: Parser (Raw -> Raw -> Raw)

52app = do whiteSpace ; return RApp

54app = do whiteSpace ; return RApp

@@ -116,3 +118,13 @@ pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm

116 <|> try (do x <- iName

118 <|> try (do x <- iName

117 return (Var x))

119 return (Var x))

118

120

121+pData :: Parser (Name, RawDatatype)

122+pData = do reserved "data"; x <- iName; lchar ':'; ty <- pTerm; reserved "where"

123+ cs <- many pConstructor

124+ return (x, RDatatype x ty cs)

125+

126+pConstructor :: Parser (Name, Raw)

127+pConstructor = do lchar '|'

128+ c <- iName; lchar ':'; ty <- pTerm

129+ return (c, ty)

130+

src/Evaluate.hs+19−4

@@ -2,7 +2,7 @@

2

3module Evaluate(normalise,

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

5− emptyContext, addToCtxt, addConstant,

5+ emptyContext, addToCtxt, addConstant, addDatatype,

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

7

8import Debug.Trace

@@ -110,12 +110,27 @@ type Context = [(Name, Def)]

110

111emptyContext = []

112

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

114+addDef n d ctxt = (n, d) : ctxt

115+

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

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

114−addToCtxt n tm ty ctxt = (n, Function (Fun ty (eval ctxt [] ty)

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

115− tm (eval ctxt [] tm))) : ctxt

118+ tm (eval ctxt [] tm))) ctxt

116

119

117addConstant :: Name -> Type -> Context -> Context

120addConstant :: Name -> Type -> Context -> Context

118−addConstant n ty ctxt = (n, Constant Ref ty (eval ctxt [] ty)) : ctxt

121+addConstant n ty ctxt = addDef n (Constant Ref ty (eval ctxt [] ty)) ctxt

122+

123+addDatatype :: Datatype Name -> Context -> Context

124+addDatatype (Data n ty cons) ctxt

125+ = let ty' = normalise ctxt [] ty in

126+ addCons 0 cons (addDef n

127+ (Constant (TCon (arity ty')) ty (eval ctxt [] ty)) ctxt)

128+ where

129+ addCons tag [] ctxt = ctxt

130+ addCons tag ((n, ty) : cons) ctxt

131+ = let ty' = normalise ctxt [] ty in

132+ addCons (tag+1) cons (addDef n

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

119

134

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

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

121lookupTy n ctxt = do def <- lookup n ctxt

136lookupTy n ctxt = do def <- lookup n ctxt

src/ProofState.hs+1

@@ -5,6 +5,7 @@ module ProofState where

5import Typecheck

6import Evaluate

7import Core

8+import Unify

8

9

9import Control.Monad.State

10import Control.Monad.State

10import Control.Applicative

11import Control.Applicative

src/Typecheck.hs+18−26

@@ -8,32 +8,14 @@ import Debug.Trace

8import Core

9import Evaluate

10

11−data TC a = OK a

11+-- To check conversion, normalise each term wrt the current environment.

12− | Error String -- TMP! Make this an informative data structure

12+-- Since we haven't converted everything to de Bruijn indices yet, we'll have to

13− deriving (Eq, Functor)

13+-- deal with alpha conversion - we do this by making each inner term de Bruijn

14−

14+-- indexed with 'finalise'

15−instance Show a => Show (TC a) where

16− show (OK x) = show x

17− show (Error str) = "Error: " ++ str

18−

19−-- at some point, this instance should also carry type checking options

20−-- (e.g. Set:Set)

21−

22−instance Monad TC where

23− return = OK

24− x >>= k = case x of

25− OK v -> k v

26− Error e -> Error e

27− fail = Error

28−

29−instance MonadPlus TC where

30− mzero = Error "Unknown error"

31− (OK x) `mplus` _ = OK x

32− _ `mplus` (OK y) = OK y

33− err `mplus` _ = err

34

15

35converts :: Context -> Env -> Term -> Term -> TC ()

16converts :: Context -> Env -> Term -> Term -> TC ()

36−converts ctxt env x y = if (normalise ctxt env x == normalise ctxt env y)

17+converts ctxt env x y = if (finalise (normalise ctxt env x) ==

18+ finalise (normalise ctxt env y))

37 then return ()

19 then return ()

38 else fail ("Can't convert between " ++

20 else fail ("Can't convert between " ++

39 showEnv env (normalise ctxt env x) ++ " and " ++

21 showEnv env (normalise ctxt env x) ++ " and " ++

@@ -173,14 +155,24 @@ finalise t = t

173

155

174checkProgram :: Context -> RProgram -> TC Context

156checkProgram :: Context -> RProgram -> TC Context

175checkProgram ctxt [] = return ctxt

157checkProgram ctxt [] = return ctxt

176−checkProgram ctxt ((n, RConst t):xs)

158+checkProgram ctxt ((n, RConst t) : xs)

177 = do (t', tt') <- trace (show n) $ check ctxt [] t

159 = do (t', tt') <- trace (show n) $ check ctxt [] t

178 isSet ctxt [] tt'

160 isSet ctxt [] tt'

179 checkProgram (addConstant n t' ctxt) xs

161 checkProgram (addConstant n t' ctxt) xs

180−checkProgram ctxt ((n, RFunction (RawFun ty val)):xs)

162+checkProgram ctxt ((n, RFunction (RawFun ty val)) : xs)

181 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

163 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

182 (val', valt') <- check ctxt [] val

164 (val', valt') <- check ctxt [] val

183 isSet ctxt [] tyt'

165 isSet ctxt [] tyt'

184 converts ctxt [] ty' valt'

166 converts ctxt [] ty' valt'

185 checkProgram (addToCtxt n val' ty' ctxt) xs

167 checkProgram (addToCtxt n val' ty' ctxt) xs

168+checkProgram ctxt ((n, RData (RDatatype _ ty cons)) : xs)

169+ = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

170+ isSet ctxt [] tyt'

171+ -- add the tycon temporarily so we can check constructors

172+ let ctxt' = addDatatype (Data n ty' []) ctxt

173+ cons' <- mapM (checkCon ctxt') cons

174+ checkProgram (addDatatype (Data n ty' cons') ctxt) xs

175+ where checkCon ctxt (n, cty) = do (cty', ctyt') <- check ctxt [] cty

176+ return (n, cty')

177+

186

178

src/Unify.hsnew file+26

@@ -0,0 +1,26 @@

1+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}

2+

3+module Unify(unify) where

4+

5+import Core

6+import Evaluate

7+

8+-- Unification is applied inside the theorem prover. We're looking for holes

9+-- which can be filled in, by matching one term's normal form against another.

10+-- Returns a list of hole names paired with the term which solves them.

11+

12+unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

13+unify ctxt env x y

14+ = case un' [] x y of

15+ OK v -> return v

16+ _ -> fail $ "Can't unify " ++ showEnv env x ++ " and " ++ showEnv env y

17+ where

18+ un' bnames (P Bound x _) (P Bound y _) | (x,y) `elem` bnames = return []

19+ un' bnames x y | x == y = return []

20+ | otherwise = fail "Can't unify"

21+

22+holeIn :: Env -> Name -> Bool

23+holeIn env n = case lookup n env of

24+ Just (Hole _) -> True

25+ _ -> False

26+

src/test.mi+3−3

@@ -6,8 +6,8 @@ one : N = S O;

6two : N = S (S O);

7three : N = S two;

8

9−Vect : (A:Set 0) -> (n:N) -> Set 0;

9+data Vect : (A:Set 0) -> (n:N) -> Set 0 where

10−Nil : (A:Set 0) -> (Vect A O);

10+ Nil : (A:Set 0) -> (Vect A O)

11−Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));

11+ | Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));

12

13vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);