6757c47 · Idris-dev · git.iko.soy

lib/list.idr+1

compare with master

unifiedsplit

@@ -7,3 +7,4 @@ rev xs = revAcc Nil xs

7 revAcc acc Nil = acc;

8 revAcc acc (Cons x xs) = revAcc (Cons x acc) xs;

9 }

10+

lib/vect.idr+1−1

@@ -10,7 +10,7 @@ data Vect : Set -> Nat -> Set where

10 VNil : Vect a O

11 | (::) : a -> Vect a k -> Vect a (S k);

12

13−vlookup : (i : Fin n) -> Vect a n -> a;

13+vlookup : Fin n -> Vect a n -> a;

14vlookup fO (x :: xs) = x;

15vlookup (fS k) (x :: xs) = vlookup k xs;

16

src/Core/CaseTree.hs+20−10

@@ -23,12 +23,12 @@ type CaseTree = SC

23type Clause = ([Pat], Term)

24type CS = Int

25

26−simpleCase :: [(Term, Term)] -> CaseDef

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

27−simpleCase [] = CaseDef [] (UnmatchedCase "No pattern clauses")

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

28−simpleCase cs = let pats = map (\ (l, r) -> (toPats l, r)) cs

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

29− numargs = length (fst (head pats))

29+ numargs = length (fst (head pats))

30− ns = take numargs args in

30+ ns = take numargs args in

31− CaseDef ns (evalState (match ns pats (UnmatchedCase "Error")) numargs)

31+ CaseDef ns (evalState (match ns pats (UnmatchedCase "Error")) numargs)

32 where args = map (\i -> MN i "e") [0..]

33

34data Pat = PCon Name Int [Pat]

@@ -40,16 +40,26 @@ data Pat = PCon Name Int [Pat]

40-- If there are repeated variables, take the *last* one (could be name shadowing

41-- in a where clause, so take the most recent).

42

43−toPats :: Term -> [Pat]

43+toPats :: Bool -> Term -> [Pat]

44−toPats f = reverse (toPat (getArgs f)) where

44+toPats tc f = reverse (toPat tc (getArgs f)) where

45 getArgs (App f a) = a : getArgs f

46 getArgs _ = []

47

48−toPat :: [Term] -> [Pat]

48+toPat :: Bool -> [Term] -> [Pat]

49−toPat tms = evalState (mapM (\x -> toPat' x []) tms) []

49+toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

50 where

51 toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args

52 return $ PCon n t args'

53+ -- Typecase

54+ toPat' (P (TCon t a) n _) args | tc

55+ = do args' <- mapM (\x -> toPat' x []) args

56+ return $ PCon n t args'

57+ toPat' (Constant IType) [] | tc = return $ PCon (UN ["Int"]) 1 []

58+ toPat' (Constant FlType) [] | tc = return $ PCon (UN ["Float"]) 2 []

59+ toPat' (Constant ChType) [] | tc = return $ PCon (UN ["Char"]) 3 []

60+ toPat' (Constant StrType) [] | tc = return $ PCon (UN ["String"]) 4 []

61+ toPat' (Constant PtrType) [] | tc = return $ PCon (UN ["Ptr"]) 5 []

62+

53 toPat' (P Bound n _) [] = do ns <- get

63 toPat' (P Bound n _) [] = do ns <- get

54 if n `elem` ns

64 if n `elem` ns

55 then return PAny

65 then return PAny

src/Core/Evaluate.hs+13−5

@@ -122,6 +122,9 @@ eval ctxt genv tm = ev [] tm where

122 chooseAlt _ (VP (DCon i a) _ _, args) alts amap

123 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)

124 | Just v <- findDefault alts = Just (amap, v)

125+ chooseAlt _ (VP (TCon i a) _ _, args) alts amap

126+ | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)

127+ | Just v <- findDefault alts = Just (amap, v)

125 chooseAlt _ (VConstant c, []) alts amap

128 chooseAlt _ (VConstant c, []) alts amap

126 | Just v <- findConst c alts = Just (amap, v)

129 | Just v <- findConst c alts = Just (amap, v)

127 | Just v <- findDefault alts = Just (amap, v)

130 | Just v <- findDefault alts = Just (amap, v)

@@ -142,6 +145,11 @@ eval ctxt genv tm = ev [] tm where

142

145

143 findConst c [] = Nothing

146 findConst c [] = Nothing

144 findConst c (ConstCase c' v : xs) | c == c' = Just v

147 findConst c (ConstCase c' v : xs) | c == c' = Just v

148+ findConst IType (ConCase n 1 [] v : xs) = Just v

149+ findConst FlType (ConCase n 2 [] v : xs) = Just v

150+ findConst ChType (ConCase n 3 [] v : xs) = Just v

151+ findConst StrType (ConCase n 4 [] v : xs) = Just v

152+ findConst PtrType (ConCase n 5 [] v : xs) = Just v

145 findConst c (_ : xs) = findConst c xs

153 findConst c (_ : xs) = findConst c xs

146

154

147 getValArgs tm = getValArgs' tm []

155 getValArgs tm = getValArgs' tm []

@@ -199,10 +207,10 @@ addTyDecl :: Name -> Type -> Context -> Context

199addTyDecl n ty ctxt = addDef n (TyDecl Ref ty (eval ctxt [] ty)) ctxt

207addTyDecl n ty ctxt = addDef n (TyDecl Ref ty (eval ctxt [] ty)) ctxt

200

208

201addDatatype :: Datatype Name -> Context -> Context

209addDatatype :: Datatype Name -> Context -> Context

202−addDatatype (Data n ty cons) ctxt

210+addDatatype (Data n tag ty cons) ctxt

203 = let ty' = normalise ctxt [] ty in

211 = let ty' = normalise ctxt [] ty in

204 addCons 0 cons (addDef n

212 addCons 0 cons (addDef n

205− (TyDecl (TCon (arity ty')) ty (eval ctxt [] ty)) ctxt)

213+ (TyDecl (TCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)

206 where

214 where

207 addCons tag [] ctxt = ctxt

215 addCons tag [] ctxt = ctxt

208 addCons tag ((n, ty) : cons) ctxt

216 addCons tag ((n, ty) : cons) ctxt

@@ -210,9 +218,9 @@ addDatatype (Data n ty cons) ctxt

210 addCons (tag+1) cons (addDef n

218 addCons (tag+1) cons (addDef n

211 (TyDecl (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)

219 (TyDecl (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)

212

220

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

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

214−addCasedef n ps ty ctxt

222+addCasedef n tcase ps ty ctxt

215− = case simpleCase ps of

223+ = case simpleCase tcase ps of

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

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

217

225

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

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

src/Core/TT.hs+2−1

@@ -158,7 +158,7 @@ type RProgram = [(Name, RDef)]

158

159-- WELL TYPED TERMS ---------------------------------------------------------

160

161−data NameType = Bound | Ref | DCon Int Int | TCon Int

161+data NameType = Bound | Ref | DCon Int Int | TCon Int Int

162 deriving (Show, Eq)

163

164data TT n = P NameType n (TT n) -- embed type

@@ -172,6 +172,7 @@ data TT n = P NameType n (TT n) -- embed type

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

173

174data Datatype n = Data { d_typename :: n,

175+ d_typetag :: Int,

175 d_type :: (TT n),

176 d_type :: (TT n),

176 d_cons :: [(n, TT n)] }

177 d_cons :: [(n, TT n)] }

177 deriving (Show, Functor, Eq)

178 deriving (Show, Functor, Eq)

src/Core/Typecheck.hs+2−2

@@ -169,9 +169,9 @@ 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

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

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

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

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

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

176 return (n, cty')

177

src/Core/Unify.hs+1−1

@@ -17,7 +17,7 @@ unify ctxt env topx topy

17 Error e -> tfail $ CantUnify topx topy e

18 where

19 injective (P (DCon _ _) _ _) = True

20− injective (P (TCon _) _ _) = True

20+ injective (P (TCon _ _) _ _) = True

21 injective (App f a) = injective f

22 injective _ = False

23

src/Idris/AbsSyntax.hs+13−5

@@ -13,10 +13,12 @@ import Debug.Trace

13

14import qualified Epic.Epic as E

15

16−data IOption = IOption { opt_logLevel :: Int }

16+data IOption = IOption { opt_logLevel :: Int,

17+ opt_typecase :: Bool

18+ }

17 deriving (Show, Eq)

19 deriving (Show, Eq)

18

20

19−defaultOpts = IOption 0

21+defaultOpts = IOption 0 False

20

22

21-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

23-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

22-- without typechecking).

24-- without typechecking).

@@ -35,7 +37,7 @@ data IState = IState { tt_ctxt :: Context,

35 idris_prims :: [(Name, ([E.Name], E.Term))]

37 idris_prims :: [(Name, ([E.Name], E.Term))]

36 }

38 }

37

39

38−idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] [] [] []

40+idrisInit = IState emptyContext [] emptyContext "" defaultOpts 6 [] [] [] []

39

41

40-- The monad for the main REPL - reading and processing files and updating

42-- The monad for the main REPL - reading and processing files and updating

41-- global state (hence the IO inner monad).

43-- global state (hence the IO inner monad).

@@ -102,6 +104,12 @@ logLvl l str = do i <- get

102iLOG :: String -> Idris ()

104iLOG :: String -> Idris ()

103iLOG = logLvl 1

105iLOG = logLvl 1

104

106

107+setTypeCase :: Bool -> Idris ()

108+setTypeCase t = do i <- get

109+ let opts = idris_options i

110+ let opt' = opts { opt_typecase = t }

111+ put (i { idris_options = opt' })

112+

105-- Commands in the REPL

113-- Commands in the REPL

106

114

107data Command = Quit | Help | Eval PTerm

115data Command = Quit | Help | Eval PTerm

@@ -173,7 +181,7 @@ data PTerm = PQuote Raw

173 | PRef FC Name

181 | PRef FC Name

174 | PLam Name PTerm PTerm

182 | PLam Name PTerm PTerm

175 | PPi Plicity Name PTerm PTerm

183 | PPi Plicity Name PTerm PTerm

176− | PLet Name PTerm PTerm PTerm -- not implemented yet

184+ | PLet Name PTerm PTerm PTerm

177 | PApp FC PTerm [PArg]

185 | PApp FC PTerm [PArg]

178 | PTrue FC

186 | PTrue FC

179 | PFalse FC

187 | PFalse FC

@@ -365,7 +373,7 @@ inferDecl = PDatadecl inferTy

365 (PRef bi inferTy)), bi)]

373 (PRef bi inferTy)), bi)]

366

374

367infTerm t = PApp bi (PRef bi inferCon) [PImp (MN 0 "A") Placeholder, PExp t]

375infTerm t = PApp bi (PRef bi inferCon) [PImp (MN 0 "A") Placeholder, PExp t]

368−infP = P (TCon 0) inferTy (Set 0)

376+infP = P (TCon 6 0) inferTy (Set 0)

369

377

370getInferTerm, getInferType :: Term -> Term

378getInferTerm, getInferType :: Term -> Term

371getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

379getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

src/Idris/Compiler.hs+6−2

@@ -52,7 +52,7 @@ instance ToEpic (TT Name) where

52 | (P _ (UN ["mkForeign"]) _, args) <- unApply tm

53 = doForeign args

54 epic' env (P (DCon t a) n _) = return $ con_ t

55− epic' env (P (TCon _) _ _) = return impossible

55+ epic' env (P (TCon t a) n _) = return $ con_ t

56 epic' env (P _ n _) = return $ ref (ename n)

57 epic' env (V i) = return $ ref (env!!i)

58 epic' env (Bind n (Lam _) sc)

@@ -99,7 +99,11 @@ instance ToEpic Const where

99 epic (Fl f) = return (float f)

100 epic (Str s) = return (str s)

101 epic (Ch c) = return (char c)

102− epic _ = return impossible

102+ epic IType = return $ con_ 1

103+ epic FlType = return $ con_ 2

104+ epic ChType = return $ con_ 3

105+ epic StrType = return $ con_ 4

106+ epic PtrType = return $ con_ 5

103

107

104instance ToEpic ([Name], SC) where

108instance ToEpic ([Name], SC) where

105 epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

109 epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

src/Idris/ElabDecls.hs+6−3

@@ -52,7 +52,8 @@ elabData info fc (PDatadecl n t dcons)

52 logLvl 2 $ "---> " ++ show cty

53 updateContext (addTyDecl n cty) -- temporary, to check cons

54 cons <- mapM (elabCon info) dcons

55+ ttag <- getName

55− setContext (addDatatype (Data n cty cons) ctxt)

56+ setContext (addDatatype (Data n ttag cty cons) ctxt)

56

57

57elabCon :: ElabInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

58elabCon :: ElabInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

58elabCon info (n, t, fc)

59elabCon info (n, t, fc)

@@ -74,11 +75,13 @@ elabClauses info fc n_in cs = let n = liftname info n_in in

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

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

75 show l ++ " = " ++

76 show l ++ " = " ++

76 show r) pats))

77 show r) pats))

78+ ist <- get

79+ let tcase = opt_typecase (idris_options ist)

77− let tree = simpleCase (map debind pats)

80+ let tree = simpleCase tcase (map debind pats)

78 logLvl 3 (show tree)

81 logLvl 3 (show tree)

79 ctxt <- getContext

82 ctxt <- getContext

80 case lookupTy n ctxt of

83 case lookupTy n ctxt of

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

84+ Just ty -> updateContext (addCasedef n tcase (map debind pats) ty)

82 Nothing -> return ()

85 Nothing -> return ()

83 where

86 where

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

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

src/Main.hs+3

@@ -32,6 +32,7 @@ data Opt = Filename String

32 | NoPrelude

33 | NoREPL

34 | OLogging Int

35+ | TypeCase

35 deriving Eq

36 deriving Eq

36

37

37main = do xs <- getArgs

38main = do xs <- getArgs

@@ -51,6 +52,7 @@ runIdris opts =

51 when runrepl $ repl (mkPrompt mods)

52 when runrepl $ repl (mkPrompt mods)

52 where

53 where

53 makeOption (OLogging i) = setLogLevel i

54 makeOption (OLogging i) = setLogLevel i

55+ makeOption TypeCase = setTypeCase True

54 makeOption _ = return ()

56 makeOption _ = return ()

55

57

56mkPrompt [] = "Idris"

58mkPrompt [] = "Idris"

@@ -72,6 +74,7 @@ parseArgs [] = return []

72parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)

74parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)

73parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)

75parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)

74parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)

76parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)

77+parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

75parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

78parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

76

79

77{-

80{-