2a13be4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Distinguish parameters and indices internally in data types

2a13be4Edwin Brady14 years ago

CHANGELOG+11

compare with master

unifiedsplit

@@ -1,3 +1,14 @@

1+New in 0.9.7:

2+-------------

4+User visible changes:

6+Internal changes:

8+* Change unification so that it keeps track of failed constraints in case

9+ later information helps to resolve them

10+* Distinguishing parameters and indices in data types

11+

1New in 0.9.6:

12New in 0.9.6:

2-------------

13-------------

src/Idris/AbsSyntaxTree.hs+3−1

@@ -579,7 +579,9 @@ deriving instance Binary OptInfo

579!-}

580

581

582−data TypeInfo = TI { con_names :: [Name], codata :: Bool }

582+data TypeInfo = TI { con_names :: [Name],

583+ codata :: Bool,

584+ param_pos :: [Int] }

583 deriving Show

585 deriving Show

584{-!

586{-!

585deriving instance Binary TypeInfo

587deriving instance Binary TypeInfo

src/Idris/Coverage.hs+4−4

@@ -110,8 +110,8 @@ expandAlts i all@(ConCase n _ _ _ : alts) def

110 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)

111 = do let tyn = getTy n (tt_ctxt i)

112 case lookupCtxt Nothing tyn (idris_datatypes i) of

113− (TI ns _ : _) -> do let ps = map mkPat ns

113+ (TI ns _ _: _) -> do let ps = map mkPat ns

114− return $ addAlts ps (altsFor all) all

114+ return $ addAlts ps (altsFor all) all

115 _ -> return all

116 where

117 altsFor [] = []

@@ -225,7 +225,7 @@ genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of

225 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)

226 let tyn = getTy n (tt_ctxt i)

227 case lookupCtxt Nothing tyn (idris_datatypes i) of

228− (TI ns _ : _) -> p : map (mkPat fc) (ns \\ [n])

228+ (TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

229 _ -> [p]

230 ops fc n arg o = return Placeholder

231

@@ -300,7 +300,7 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats

300 cotype ty

301 | (P _ t _, _) <- unApply (getRetTy ty)

302 = case lookupCtxt Nothing t (idris_datatypes i) of

303− [TI _ True] -> True

303+ [TI _ True _] -> True

304 _ -> False

305 | otherwise = False

306

src/Idris/ElabDecls.hs+58−2

@@ -67,7 +67,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

67 let (t, _) = unApply (getRetTy nty')

68 let corec = case t of

69 P _ rcty _ -> case lookupCtxt Nothing rcty (idris_datatypes i) of

70− [TI _ True] -> True

70+ [TI _ True _] -> True

71 _ -> False

72 _ -> False

73 let opts' = if corec then (Coinductive : opts) else opts

@@ -141,7 +141,10 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

141 cons <- mapM (elabCon info syn n codata) dcons

142 ttag <- getName

143 i <- get

144+ let as = map (const Nothing) (getArgTys cty)

145+ let params = findParams (zip as (repeat True)) (map snd cons)

146+ logLvl 2 $ "Parameters : " ++ show params

144− put (i { idris_datatypes = addDef n (TI (map fst cons) codata)

147+ put (i { idris_datatypes = addDef n (TI (map fst cons) codata params)

145 (idris_datatypes i) })

148 (idris_datatypes i) })

146 addIBC (IBCDef n)

149 addIBC (IBCDef n)

147 addIBC (IBCData n)

150 addIBC (IBCData n)

@@ -150,6 +153,29 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

150 collapseCons n cons

153 collapseCons n cons

151 updateContext (addDatatype (Data n ttag cty cons))

154 updateContext (addDatatype (Data n ttag cty cons))

152 mapM_ (checkPositive n) cons

155 mapM_ (checkPositive n) cons

156+ where findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]

157+ findParams ps [] = mapMaybe (\ ((x, y), n) ->

158+ if y then Just n else Nothing)

159+ (zip ps [0..])

160+ findParams ps (t : ts) = findParams (updateParams ps t) ts

161+

162+ updateParams ps (Bind n (Pi t) sc)

163+ = updateParams ps (instantiate (P Bound n t) sc)

164+ updateParams ps tm@(App f a)

165+ | (P _ fn _, args) <- unApply tm

166+ = if fn == n

167+ then updateParamsA ps args

168+ else updateParams (updateParams ps f) a

169+ | otherwise = updateParams (updateParams ps f) a

170+ updateParams ps _ = ps

171+

172+ updateParamsA ((Nothing, b) : ns) (P _ n' _ : args)

173+ = (Just n', b) : updateParamsA ns args

174+ updateParamsA ((Just p, b) : ns) (P _ n' _ : args)

175+ = (Just n', b && p == n') : updateParamsA ns args

176+ updateParamsA ((mn, _) : ns) (_ : args)

177+ = (mn, False) : updateParamsA ns args

178+ updateParamsA ps args = ps

153

179

154elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

180elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

155 PTerm -> String -> Name -> PTerm -> Idris ()

181 PTerm -> String -> Name -> PTerm -> Idris ()

@@ -911,6 +937,7 @@ elabInstance info syn fc cs n ps t expn ds

911 (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

937 (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

912 [c] -> return c

938 [c] -> return c

913 _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

939 _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

940+ let constraint = PApp fc (PRef fc n) (map pexp ps)

914 let iname = case expn of

941 let iname = case expn of

915 Nothing -> UN ('@':show n ++ "$" ++ show ps)

942 Nothing -> UN ('@':show n ++ "$" ++ show ps)

916 Just nm -> nm

943 Just nm -> nm

@@ -957,6 +984,10 @@ elabInstance info syn fc cs n ps t expn ds

957 iLOG (show idecls)

984 iLOG (show idecls)

958 mapM (elabDecl EAll info) idecls

985 mapM (elabDecl EAll info) idecls

959 addIBC (IBCInstance intInst n iname)

986 addIBC (IBCInstance intInst n iname)

987+-- -- for each constraint, build a top level function to chase it

988+-- logLvl 5 $ "Building functions"

989+-- fns <- mapM (cfun (instanceName ci) constraint syn idecls) cs

990+-- mapM_ (elabDecl EAll info) (concat fns)

960 where

991 where

961 intInst = case ps of

992 intInst = case ps of

962 [PConstant IType] -> True

993 [PConstant IType] -> True

@@ -1048,6 +1079,31 @@ elabInstance info syn fc cs n ps t expn ds

1048 = decorate ns iname m == decorate ns iname m'

1079 = decorate ns iname m == decorate ns iname m'

1049 clauseFor m iname ns _ = False

1080 clauseFor m iname ns _ = False

1050

1081

1082+{- This won't work yet. Can it ever, in this form?

1083+

1084+ cfun cn c syn all con

1085+ = do let cfn = UN ('@':'@':show cn ++ "#" ++ show con)

1086+ let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

1087+ let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

1088+ let lhs = PApp fc (PRef fc cfn) [pconst capp]

1089+ let rhs = PResolveTC (FC "HACK" 0)

1090+ let ty = PPi constraint (MN 0 "pc") c con

1091+ iLOG (showImp True ty)

1092+ iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

1093+ i <- get

1094+ let conn = case con of

1095+ PRef _ n -> n

1096+ PApp _ (PRef _ n) _ -> n

1097+ let conn' = case lookupCtxtName Nothing conn (idris_classes i) of

1098+ [(n, _)] -> n

1099+ _ -> conn

1100+ addInstance False conn' cfn

1101+ addIBC (IBCInstance False conn' cfn)

1102+ iputStrLn ("Added " ++ show (conn, cfn, ty) ++ "\n" ++ show (lhs, rhs))

1103+ return [PTy "" syn fc [] cfn ty,

1104+ PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]]

1105+-}

1106+

1051decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t

1107decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t

1052decorateid decorate (PClauses f o n cs)

1108decorateid decorate (PClauses f o n cs)

1053 = PClauses f o (decorate n) (map dc cs)

1109 = PClauses f o (decorate n) (map dc cs)

src/Idris/ElabTerm.hs+2−2

@@ -356,7 +356,7 @@ elab ist info pattern tcgen fn tm

356 ps' <- get_probs

357 -- Attempt to resolve any type classes which have 'complete' types,

358 -- i.e. no holes in them

359− when (not pattern || (ina && not tcgen)) $

359+ when (not pattern || (ina && not tcgen && not guarded)) $

360 mapM_ (\n -> do focus n

361 g <- goal

362 env <- get_env

@@ -612,7 +612,7 @@ resolveTC depth fn ist

612 args <- apply (Var n) imps

613 ps' <- get_probs

614 when (length ps < length ps') $ fail "Can't apply type class"

615− -- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

615+-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

616 mapM_ (\ (_,n) -> do focus n

617 t' <- goal

618 let (tc', ttype) = unApply t'

src/Idris/IBC.hs+6−4

@@ -21,7 +21,7 @@ import System.Directory

21import Paths_idris

23ibcVersion :: Word8

24−ibcVersion = 24

24+ibcVersion = 25

26data IBCFile = IBCFile { ver :: Word8,

27 sourcefile :: FilePath,

@@ -1522,11 +1522,13 @@ instance Binary OptInfo where

1522 return (Optimise x1 x2 x3)

1523

1524instance Binary TypeInfo where

1525− put (TI x1 x2) = do put x1

1525+ put (TI x1 x2 x3) = do put x1

1526− put x2

1526+ put x2

1527+ put x3

1527 get = do x1 <- get

1528 get = do x1 <- get

1528 x2 <- get

1529 x2 <- get

1530+ x3 <- get

1529− return (TI x1 x2)

1531+ return (TI x1 x2 x3)

1530

1532

1531instance Binary SynContext where

1533instance Binary SynContext where

1532 put x

1534 put x

src/Idris/REPL.hs+2

@@ -240,6 +240,8 @@ process fn (DebugInfo n)

240 when (not (null oi)) $ iputStrLn (show oi)

241 let si = lookupCtxt Nothing n (idris_statics i)

242 when (not (null si)) $ iputStrLn (show si)

243+ let di = lookupCtxt Nothing n (idris_datatypes i)

244+ when (not (null di)) $ iputStrLn (show di)

243 let d = lookupDef Nothing n (tt_ctxt i)

245 let d = lookupDef Nothing n (tt_ctxt i)

244 when (not (null d)) $ liftIO $

246 when (not (null d)) $ liftIO $

245 do print (head d)

247 do print (head d)