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

git.iko.soy/Idris-dev

Distinguish parameters and indices internally in data types

This doesn't do anything, yet, but will become important soon!

commit2a13be4e1635a423f67f35628084d906f950a217 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 5 Feb 2013, 14:40 (14 years ago) parente5706d3

7 files changed+86−13

compare with master

unifiedsplit

CHANGELOG+11 src/Idris/AbsSyntaxTree.hs+3−1 src/Idris/Coverage.hs+4−4 src/Idris/ElabDecls.hs+58−2 src/Idris/ElabTerm.hs+2−2 src/Idris/IBC.hs+6−4 src/Idris/REPL.hs+2

CHANGELOG+11

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

112New in 0.9.6:

213-------------

314

src/Idris/AbsSyntaxTree.hs+3−1

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

579579!-}

580580

581581

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

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

583+ codata :: Bool,

584+ param_pos :: [Int] }

583585 deriving Show

584586{-!

585587deriving instance Binary TypeInfo

src/Idris/Coverage.hs+4−4

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

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

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

112112 case lookupCtxt Nothing tyn (idris_datatypes i) of

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

114− return $ addAlts ps (altsFor all) all

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

114+ return $ addAlts ps (altsFor all) all

115115 _ -> return all

116116 where

117117 altsFor [] = []

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

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

226226 let tyn = getTy n (tt_ctxt i)

227227 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])

229229 _ -> [p]

230230 ops fc n arg o = return Placeholder

231231

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

300300 cotype ty

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

302302 = case lookupCtxt Nothing t (idris_datatypes i) of

303− [TI _ True] -> True

303+ [TI _ True _] -> True

304304 _ -> False

305305 | otherwise = False

306306

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

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

6868 let corec = case t of

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

70− [TI _ True] -> True

70+ [TI _ True _] -> True

7171 _ -> False

7272 _ -> False

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

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

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

142142 ttag <- getName

143143 i <- get

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

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

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

145148 (idris_datatypes i) })

146149 addIBC (IBCDef n)

147150 addIBC (IBCData n)

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

150153 collapseCons n cons

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

152155 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

153179

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

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

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

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

912938 [c] -> return c

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

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

914941 let iname = case expn of

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

916943 Just nm -> nm

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

957984 iLOG (show idecls)

958985 mapM (elabDecl EAll info) idecls

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

960991 where

961992 intInst = case ps of

962993 [PConstant IType] -> True

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

10481079 = decorate ns iname m == decorate ns iname m'

10491080 clauseFor m iname ns _ = False

10501081

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+

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

10521108decorateid decorate (PClauses f o n cs)

10531109 = 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

356356 ps' <- get_probs

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

358358 -- i.e. no holes in them

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

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

360360 mapM_ (\n -> do focus n

361361 g <- goal

362362 env <- get_env

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

612612 args <- apply (Var n) imps

613613 ps' <- get_probs

614614 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) $

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

617617 t' <- goal

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

src/Idris/IBC.hs+6−4

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

2121import Paths_idris

2222

2323ibcVersion :: Word8

24−ibcVersion = 24

24+ibcVersion = 25

2525

2626data IBCFile = IBCFile { ver :: Word8,

2727 sourcefile :: FilePath,

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

15221522 return (Optimise x1 x2 x3)

15231523

15241524instance Binary TypeInfo where

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

1526− put x2

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

1526+ put x2

1527+ put x3

15271528 get = do x1 <- get

15281529 x2 <- get

1529− return (TI x1 x2)

1530+ x3 <- get

1531+ return (TI x1 x2 x3)

15301532

15311533instance Binary SynContext where

15321534 put x

src/Idris/REPL.hs+2

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

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

241241 let si = lookupCtxt Nothing n (idris_statics i)

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

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

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

243245 let d = lookupDef Nothing n (tt_ctxt i)

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

245247 do print (head d)