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

miniidris.cabal+2−1

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

1818 Main-is: Main.hs

1919 hs-source-dirs: src

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

21− ProofState, CoreParser, ShellParser

21+ ProofState, CoreParser, ShellParser,

22+ Unify

2223

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

2425

src/Core.hs+39

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

2222 | CheckConv

2323 deriving Eq

2424

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+

2549-- RAW TERMS ----------------------------------------------------------------

2650

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

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

6084 }

6185 deriving Show

6286

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

88+ deriving Show

89+

6390data RDef = RFunction RawFun

6491 | RConst Raw

92+ | RData RawDatatype

6593 deriving Show

6694

6795type RProgram = [(Name, RDef)]

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

82110

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

84112

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+

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

86119

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

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

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

97130 no' i _ = True

98131

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+

99138type Term = TT Name

100139type Type = Term

101140

src/CoreParser.hs+12

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

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

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

4949 return (x, RConst ty)

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

51+ return (x, RData d)

5052

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

5254app = do whiteSpace ; return RApp

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

116118 <|> try (do x <- iName

117119 return (Var x))

118120

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 @@

22

33module Evaluate(normalise,

44 Fun(..), Def(..), Context,

5− emptyContext, addToCtxt, addConstant,

5+ emptyContext, addToCtxt, addConstant, addDatatype,

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

77

88import Debug.Trace

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

110110

111111emptyContext = []

112112

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

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

115+

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

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

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

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

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

116119

117120addConstant :: 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)

119134

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

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

src/ProofState.hs+1

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

55import Typecheck

66import Evaluate

77import Core

8+import Unify

89

910import Control.Monad.State

1011import Control.Applicative

src/Typecheck.hs+18−26

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

88import Core

99import Evaluate

1010

11−data TC a = OK a

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

13− deriving (Eq, Functor)

14−

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

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

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

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

14+-- indexed with 'finalise'

3415

3516converts :: 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))

3719 then return ()

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

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

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

173155

174156checkProgram :: Context -> RProgram -> TC Context

175157checkProgram ctxt [] = return ctxt

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

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

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

178160 isSet ctxt [] tt'

179161 checkProgram (addConstant n t' ctxt) xs

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

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

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

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

183165 isSet ctxt [] tyt'

184166 converts ctxt [] ty' valt'

185167 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+

186178

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;

66two : N = S (S O);

77three : N = S two;

88

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

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

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

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

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

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

1212

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