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

git.iko.soy/Idris-dev

Added case analysis on types, but only when enabled with --typecase (since it breaks parametricity)

commit6757c477aa4d31f6a3a00eb161563f67fed25ad5 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 25 Oct 2011, 20:11 (15 years ago) parent95a558b

11 files changed+68−30

compare with master

unifiedsplit

lib/list.idr+1 lib/vect.idr+1−1 src/Core/CaseTree.hs+20−10 src/Core/Evaluate.hs+13−5 src/Core/TT.hs+2−1 src/Core/Typecheck.hs+2−2 src/Core/Unify.hs+1−1 src/Idris/AbsSyntax.hs+13−5 src/Idris/Compiler.hs+6−2 src/Idris/ElabDecls.hs+6−3 src/Main.hs+3

lib/list.idr+1

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

77 revAcc acc Nil = acc;

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

99 }

10+

lib/vect.idr+1−1

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

1010 VNil : Vect a O

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

1212

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

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

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

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

1616

src/Core/CaseTree.hs+20−10

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

2323type Clause = ([Pat], Term)

2424type CS = Int

2525

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

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

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

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

30− ns = take numargs args in

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

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

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

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

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

30+ ns = take numargs args in

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

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

3333

3434data Pat = PCon Name Int [Pat]

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

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

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

4242

43−toPats :: Term -> [Pat]

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

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

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

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

4646 getArgs _ = []

4747

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

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

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

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

5050 where

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

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

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

5464 if n `elem` ns

5565 then return PAny

src/Core/Evaluate.hs+13−5

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

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

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

124124 | 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)

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

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

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

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

142145

143146 findConst c [] = Nothing

144147 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

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

146154

147155 getValArgs tm = getValArgs' tm []

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

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

200208

201209addDatatype :: Datatype Name -> Context -> Context

202−addDatatype (Data n ty cons) ctxt

210+addDatatype (Data n tag ty cons) ctxt

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

204212 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)

206214 where

207215 addCons tag [] ctxt = ctxt

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

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

210218 addCons (tag+1) cons (addDef n

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

212220

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

214−addCasedef n ps ty ctxt

215− = case simpleCase ps of

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

222+addCasedef n tcase ps ty ctxt

223+ = case simpleCase tcase ps of

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

217225

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

src/Core/TT.hs+2−1

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

158158

159159-- WELL TYPED TERMS ---------------------------------------------------------

160160

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

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

162162 deriving (Show, Eq)

163163

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

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

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

173173

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

175+ d_typetag :: Int,

175176 d_type :: (TT n),

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

177178 deriving (Show, Functor, Eq)

src/Core/Typecheck.hs+2−2

@@ -169,9 +169,9 @@ checkProgram ctxt ((n, RData (RDatatype _ ty cons)) : xs)

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

170170 isSet ctxt [] tyt'

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

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

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

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

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

176176 return (n, cty')

177177

src/Core/Unify.hs+1−1

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

1717 Error e -> tfail $ CantUnify topx topy e

1818 where

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

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

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

2121 injective (App f a) = injective f

2222 injective _ = False

2323

src/Idris/AbsSyntax.hs+13−5

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

1313

1414import qualified Epic.Epic as E

1515

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

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

17+ opt_typecase :: Bool

18+ }

1719 deriving (Show, Eq)

1820

19−defaultOpts = IOption 0

21+defaultOpts = IOption 0 False

2022

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

2224-- without typechecking).

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

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

3638 }

3739

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

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

3941

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

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

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

102104iLOG :: String -> Idris ()

103105iLOG = logLvl 1

104106

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+

105113-- Commands in the REPL

106114

107115data Command = Quit | Help | Eval PTerm

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

173181 | PRef FC Name

174182 | PLam Name PTerm PTerm

175183 | PPi Plicity Name PTerm PTerm

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

184+ | PLet Name PTerm PTerm PTerm

177185 | PApp FC PTerm [PArg]

178186 | PTrue FC

179187 | PFalse FC

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

365373 (PRef bi inferTy)), bi)]

366374

367375infTerm 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)

369377

370378getInferTerm, getInferType :: Term -> Term

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

src/Idris/Compiler.hs+6−2

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

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

5353 = doForeign args

5454 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

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

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

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

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

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

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

101101 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

103107

104108instance ToEpic ([Name], SC) where

105109 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)

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

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

5454 cons <- mapM (elabCon info) dcons

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

55+ ttag <- getName

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

5657

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

5859elabCon info (n, t, fc)

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

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

7576 show l ++ " = " ++

7677 show r) pats))

77− let tree = simpleCase (map debind pats)

78+ ist <- get

79+ let tcase = opt_typecase (idris_options ist)

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

7881 logLvl 3 (show tree)

7982 ctxt <- getContext

8083 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)

8285 Nothing -> return ()

8386 where

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

src/Main.hs+3

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

3232 | NoPrelude

3333 | NoREPL

3434 | OLogging Int

35+ | TypeCase

3536 deriving Eq

3637

3738main = do xs <- getArgs

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

5152 when runrepl $ repl (mkPrompt mods)

5253 where

5354 makeOption (OLogging i) = setLogLevel i

55+ makeOption TypeCase = setTypeCase True

5456 makeOption _ = return ()

5557

5658mkPrompt [] = "Idris"

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

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

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

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

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

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

7679

7780{-