895b323 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow forward declaration of data structures

895b323Edwin Brady14 years ago

CHANGELOG+9

compare with master

unifiedsplit

@@ -1,3 +1,12 @@

1+New in 0.9.6:

3+User visible changes:

5+* Forward declarations of data allowed

6+ - supporting induction recursion and mutually recursive data

7+* Implicit arguments will be added automatically only if their initial

8+ letter is lower case, or they are in a using declaration

1New in 0.9.5:

10New in 0.9.5:

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

11-------------

src/Core/TT.hs+4

@@ -199,6 +199,10 @@ tcname (UN ('@':_)) = True

199tcname (NS n _) = tcname n

200tcname _ = False

201

202+implicitable (NS n _) = implicitable n

203+implicitable (UN (x:xs)) = isLower x

204+implicitable _ = False

205+

202nsroot (NS n _) = n

206nsroot (NS n _) = n

203nsroot n = n

207nsroot n = n

204

208

src/Idris/AbsSyntax.hs+7

@@ -160,6 +160,13 @@ checkUndefined fc n

160 show n ++ " already defined"

161 _ -> return ()

162

163+isUndefined :: FC -> Name -> Idris Bool

164+isUndefined fc n

165+ = do i <- getContext

166+ case lookupTy Nothing n i of

167+ (_:_) -> return False

168+ _ -> return True

169+

163setContext :: Context -> Idris ()

170setContext :: Context -> Idris ()

164setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

171setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

165

172

src/Idris/AbsSyntaxTree.hs+1

@@ -314,6 +314,7 @@ deriving instance Binary PClause'

314data PData' t = PDatadecl { d_name :: Name,

315 d_tcon :: t,

316 d_cons :: [(Name, t, FC)] }

317+ | PLaterdecl { d_name :: Name, d_tcon :: t }

317 deriving Functor

318 deriving Functor

318{-!

319{-!

319deriving instance Binary PData'

320deriving instance Binary PData'

src/Idris/ElabDecls.hs+35−13

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

76 addIBC (IBCAccess n Frozen)

78elabData :: ElabInfo -> SyntaxInfo -> FC -> Bool -> PData -> Idris ()

79−elabData info syn fc codata (PDatadecl n t_in dcons)

79+elabData info syn fc codata (PLaterdecl n t_in)

80 = do iLOG (show fc)

81 checkUndefined fc n

82 ctxt <- getContext

@@ -91,6 +91,23 @@ elabData info syn fc codata (PDatadecl n t_in dcons)

91 (cty, _) <- recheckC fc [] t'

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

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

94+

95+elabData info syn fc codata (PDatadecl n t_in dcons)

96+ = do iLOG (show fc)

97+ undef <- isUndefined fc n

98+ ctxt <- getContext

99+ i <- get

100+ t_in <- implicit syn n t_in

101+ let t = addImpl i t_in

102+ ((t', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

103+ (erun fc (build i info False n t))

104+ def' <- checkDef fc defer

105+ addDeferred def'

106+ mapM_ (elabCaseBlock info) is

107+ (cty, _) <- recheckC fc [] t'

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

109+ -- temporary, to check cons

110+ when undef $ updateContext (addTyDecl n cty)

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

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

95 ttag <- getName

112 ttag <- getName

96 i <- get

113 i <- get

@@ -123,7 +140,7 @@ elabRecord info syn fc tyn ty cn cty

123 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

140 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

124 let implBinds = getImplB id cty'

141 let implBinds = getImplB id cty'

125 update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..])

142 update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..])

126− mapM_ (elabDecl info) (concat proj_decls)

143+ mapM_ (elabDecl EAll info) (concat proj_decls)

127 mapM_ (tryElabDecl info) (update_decls)

144 mapM_ (tryElabDecl info) (update_decls)

128 where

145 where

129-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

146-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

@@ -542,7 +559,7 @@ elabClause info tcgen (PWith fc fname lhs_in withs wval_in withblock)

542 -- ==> fname' ps wpat [rest], match pats against toplevel for ps

559 -- ==> fname' ps wpat [rest], match pats against toplevel for ps

543 wb <- mapM (mkAuxC wname lhs (map fst bargs)) withblock

560 wb <- mapM (mkAuxC wname lhs (map fst bargs)) withblock

544 logLvl 5 ("with block " ++ show wb)

561 logLvl 5 ("with block " ++ show wb)

545− mapM_ (elabDecl info) wb

562+ mapM_ (elabDecl EAll info) wb

546

563

547 -- rhs becomes: fname' ps wval

564 -- rhs becomes: fname' ps wval

548 let rhs = PApp fc (PRef fc wname) (map (pexp . (PRef fc) . fst) bargs ++

565 let rhs = PApp fc (PRef fc wname) (map (pexp . (PRef fc) . fst) bargs ++

@@ -628,12 +645,12 @@ elabClass info syn fc constraints tn ps ds

628 logLvl 5 $ "Building functions"

645 logLvl 5 $ "Building functions"

629 let usyn = syn { using = ps ++ using syn }

646 let usyn = syn { using = ps ++ using syn }

630 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints

647 fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints

631− mapM_ (elabDecl info) (concat fns)

648+ mapM_ (elabDecl EAll info) (concat fns)

632 -- for each method, build a top level function

649 -- for each method, build a top level function

633 fns <- mapM (tfun cn constraint usyn (map fst imethods)) imethods

650 fns <- mapM (tfun cn constraint usyn (map fst imethods)) imethods

634− mapM_ (elabDecl info) (concat fns)

651+ mapM_ (elabDecl EAll info) (concat fns)

635 -- add the default definitions

652 -- add the default definitions

636− mapM_ (elabDecl info) (concat (map (snd.snd) defs))

653+ mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

637 i <- get

654 i <- get

638 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

655 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

639 addClass tn (CI cn imethods defaults (map fst ps) [])

656 addClass tn (CI cn imethods defaults (map fst ps) [])

@@ -795,7 +812,7 @@ elabInstance info syn fc cs n ps t expn ds

795 let idecls = [PClauses fc [Inlinable, TCGen] iname

812 let idecls = [PClauses fc [Inlinable, TCGen] iname

796 [PClause fc iname lhs [] rhs wb]]

813 [PClause fc iname lhs [] rhs wb]]

797 iLOG (show idecls)

814 iLOG (show idecls)

798− mapM (elabDecl info) idecls

815+ mapM (elabDecl EAll info) idecls

799 addIBC (IBCInstance intInst n iname)

816 addIBC (IBCInstance intInst n iname)

800 where

817 where

801 intInst = case ps of

818 intInst = case ps of

@@ -915,11 +932,16 @@ pvars ist _ = []

915data ElabWhat = ETypes | EDefns | EAll

932data ElabWhat = ETypes | EDefns | EAll

916 deriving (Show, Eq)

933 deriving (Show, Eq)

917

934

935+elabDecls :: ElabInfo -> [PDecl] -> Idris ()

936+elabDecls info ds = do mapM_ (elabDecl EAll info) ds

937+-- mapM_ (elabDecl EDefns info) ds

938+

918−elabDecl :: ElabInfo -> PDecl -> Idris ()

939+elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()

940+elabDecl what info d

919−elabDecl info d = idrisCatch (elabDecl' EAll info d)

941+ = idrisCatch (elabDecl' what info d)

920− (\e -> do let msg = show e

942+ (\e -> do let msg = show e

921− setErrLine (getErrLine msg)

943+ setErrLine (getErrLine msg)

922− iputStrLn msg)

944+ iputStrLn msg)

923

945

924elabDecl' _ info (PFix _ _ _)

946elabDecl' _ info (PFix _ _ _)

925 = return () -- nothing to elaborate

947 = return () -- nothing to elaborate

@@ -965,7 +987,7 @@ elabDecl' what info (PClass s f cs n ps ds)

965 = do iLOG $ "Elaborating class " ++ show n

987 = do iLOG $ "Elaborating class " ++ show n

966 elabClass info s f cs n ps ds

988 elabClass info s f cs n ps ds

967elabDecl' what info (PInstance s f cs n ps t expn ds)

989elabDecl' what info (PInstance s f cs n ps t expn ds)

968− | what /= EDefns

990+ | what /= ETypes

969 = do iLOG $ "Elaborating instance " ++ show n

991 = do iLOG $ "Elaborating instance " ++ show n

970 elabInstance info s f cs n ps t expn ds

992 elabInstance info s f cs n ps t expn ds

971elabDecl' what info (PRecord s f tyn ty cn cty)

993elabDecl' what info (PRecord s f tyn ty cn cty)

src/Idris/IBC.hs+19−8

@@ -1060,15 +1060,26 @@ instance (Binary t) => Binary (PClause' t) where

1060 _ -> error "Corrupted binary data for PClause'"

1061

1062instance (Binary t) => Binary (PData' t) where

1063− put (PDatadecl x1 x2 x3)

1063+ put x

1064+ = case x of

1065+ PDatadecl x1 x2 x3 -> do putWord8 0

1064− = do put x1

1066+ put x1

1065− put x2

1067+ put x2

1066− put x3

1068+ put x3

1069+ PLaterdecl x1 x2 -> do putWord8 1

1070+ put x1

1071+ put x2

1067 get

1072 get

1073+ = do i <- getWord8

1074+ case i of

1068− = do x1 <- get

1075+ 0 -> do x1 <- get

1069− x2 <- get

1076+ x2 <- get

1070− x3 <- get

1077+ x3 <- get

1071− return (PDatadecl x1 x2 x3)

1078+ return (PDatadecl x1 x2 x3)

1079+ 1 -> do x1 <- get

1080+ x2 <- get

1081+ return (PLaterdecl x1 x2)

1082+ _ -> error "Corrupted binary data for PData'"

1072

1083

1073instance Binary PTerm where

1084instance Binary PTerm where

1074 put x

1085 put x

src/Idris/Parser.hs+24−22

@@ -104,7 +104,7 @@ loadSource lidr f

104 -- Now add all the declarations to the context

105 v <- verbose

106 when v $ iputStrLn $ "Type checking " ++ f

107− mapM_ (elabDecl toplevel) ds

107+ elabDecls toplevel ds

108 i <- get

109 -- simplify every definition do give the totality checker

110 -- a better chance

@@ -1111,34 +1111,36 @@ pData syn = try (do acc <- pAccessibility

1111 tyn_in <- pfName

1112 ty <- pTSig (impOK syn)

1113 let tyn = expandNS syn tyn_in

1114+ option (PData syn fc co (PLaterdecl tyn ty)) (do

1114− reserved "where"

1115+ reserved "where"

1115− openBlock

1116+ openBlock

1116− pushIndent

1117+ pushIndent

1117− cons <- many (do notEndBlock

1118+ cons <- many (do notEndBlock

1118− c <- pConstructor syn

1119+ c <- pConstructor syn

1119− pKeepTerminator

1120+ pKeepTerminator

1120− return c) -- (lchar '|')

1121+ return c) -- (lchar '|')

1121− popIndent

1122+ popIndent

1122− closeBlock

1123+ closeBlock

1123− accData acc tyn (map (\ (n, _, _) -> n) cons)

1124+ accData acc tyn (map (\ (n, _, _) -> n) cons)

1124− return $ PData syn fc co (PDatadecl tyn ty cons))

1125+ return $ PData syn fc co (PDatadecl tyn ty cons)))

1125 <|> try (do pushIndent

1126 <|> try (do pushIndent

1126 acc <- pAccessibility

1127 acc <- pAccessibility

1127 co <- pDataI

1128 co <- pDataI

1128 fc <- pfc

1129 fc <- pfc

1129 tyn_in <- pfName

1130 tyn_in <- pfName

1130 args <- many pName

1131 args <- many pName

1131− let tyn = expandNS syn tyn_in

1132− lchar '='

1133− cons <- sepBy1 (pSimpleCon syn) (lchar '|')

1134− pTerminator

1135− let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

1136 let ty = bindArgs (map (const PSet) args) PSet

1132 let ty = bindArgs (map (const PSet) args) PSet

1133+ let tyn = expandNS syn tyn_in

1134+ option (PData syn fc co (PLaterdecl tyn ty)) (do

1135+ lchar '='

1136+ cons <- sepBy1 (pSimpleCon syn) (lchar '|')

1137+ pTerminator

1138+ let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

1137− cons' <- mapM (\ (x, cargs, cfc) ->

1139+ cons' <- mapM (\ (x, cargs, cfc) ->

1138− do let cty = bindArgs cargs conty

1140+ do let cty = bindArgs cargs conty

1139− return (x, cty, cfc)) cons

1141+ return (x, cty, cfc)) cons

1140− accData acc tyn (map (\ (n, _, _) -> n) cons')

1142+ accData acc tyn (map (\ (n, _, _) -> n) cons')

1141− return $ PData syn fc co (PDatadecl tyn ty cons'))

1143+ return $ PData syn fc co (PDatadecl tyn ty cons')))

1142 where

1144 where

1143 mkPApp fc t [] = t

1145 mkPApp fc t [] = t

1144 mkPApp fc t xs = PApp fc t (map pexp xs)

1146 mkPApp fc t xs = PApp fc t (map pexp xs)

src/Idris/Primitives.hs+1−1

@@ -280,7 +280,7 @@ elabPrim (Prim n ty i def sc tot)

280 putIState i { idris_scprims = (n, sc) : idris_scprims i }

281

282elabPrims :: Idris ()

283−elabPrims = do mapM_ (elabDecl toplevel)

283+elabPrims = do mapM_ (elabDecl EAll toplevel)

284 (map (PData defaultSyntax (FC "builtin" 0) False)

285 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

286 mapM_ elabPrim primitives

test/reg002/reg002.idr+1−1

@@ -22,7 +22,7 @@ S_inj (Co n) Infinity p = FalseElim (S_Co_not_Inf p)

22S_inj Infinity (Co m) p = FalseElim (S_Co_not_Inf (sym p))

23S_inj Infinity Infinity refl = refl

25−swap : {n : Nat} -> Vect A n -> Vect A n

25+swap : {n : Nat} -> Vect a n -> Vect a n

26swap Nil = Nil

27swap (x :: Nil) = x :: Nil

28swap (x :: y :: xs) = (y :: x :: (swap xs))

test/test014/Resimp.idr+3−3

@@ -100,9 +100,9 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

100

101 Lift : IO a -> Res gam gam (R a)

102 Check : (p:HasType gam i (Choice (interpTy a) (interpTy b))) ->

103− (failure:Res (update gam p a) (update gam p c) T) ->

103+ (failure:Res (update gam p a) (update gam p c) t) ->

104− (success:Res (update gam p b) (update gam p c) T) ->

104+ (success:Res (update gam p b) (update gam p c) t) ->

105− Res gam (update gam p c) T

105+ Res gam (update gam p c) t

106 While : Res gam gam (R Bool) ->

107 Res gam gam (R ()) -> Res gam gam (R ())

108 Return : a -> Res gam gam (R a)