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

git.iko.soy/Idris-dev

Allow forward declaration of data structures

To support induction-recursion and mutual data definitions Syntax is as a normal data declaration, but without the 'where' or '=' sections

commit895b323bc1f5bf94e0c80a2637e437466bc4eae0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 30 Oct 2012, 20:19 (14 years ago) parent20030b5

10 files changed+104−48

compare with master

unifiedsplit

CHANGELOG+9 src/Core/TT.hs+4 src/Idris/AbsSyntax.hs+7 src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabDecls.hs+35−13 src/Idris/IBC.hs+19−8 src/Idris/Parser.hs+24−22 src/Idris/Primitives.hs+1−1 test/reg002/reg002.idr+1−1 test/test014/Resimp.idr+3−3

CHANGELOG+9

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

110New in 0.9.5:

211-------------

312

src/Core/TT.hs+4

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

199199tcname (NS n _) = tcname n

200200tcname _ = False

201201

202+implicitable (NS n _) = implicitable n

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

204+implicitable _ = False

205+

202206nsroot (NS n _) = n

203207nsroot n = n

204208

src/Idris/AbsSyntax.hs+7

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

160160 show n ++ " already defined"

161161 _ -> return ()

162162

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+

163170setContext :: Context -> Idris ()

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

165172

src/Idris/AbsSyntaxTree.hs+1

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

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

315315 d_tcon :: t,

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

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

317318 deriving Functor

318319{-!

319320deriving 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

7676 addIBC (IBCAccess n Frozen)

7777

7878elabData :: 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)

8080 = do iLOG (show fc)

8181 checkUndefined fc n

8282 ctxt <- getContext

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

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

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

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

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

95112 ttag <- getName

96113 i <- get

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

123140 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

124141 let implBinds = getImplB id cty'

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

127144 mapM_ (tryElabDecl info) (update_decls)

128145 where

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

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

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

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

545− mapM_ (elabDecl info) wb

562+ mapM_ (elabDecl EAll info) wb

546563

547564 -- rhs becomes: fname' ps wval

548565 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

628645 logLvl 5 $ "Building functions"

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

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

631− mapM_ (elabDecl info) (concat fns)

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

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

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

634− mapM_ (elabDecl info) (concat fns)

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

635652 -- add the default definitions

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

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

637654 i <- get

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

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

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

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

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

797814 iLOG (show idecls)

798− mapM (elabDecl info) idecls

815+ mapM (elabDecl EAll info) idecls

799816 addIBC (IBCInstance intInst n iname)

800817 where

801818 intInst = case ps of

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

915932data ElabWhat = ETypes | EDefns | EAll

916933 deriving (Show, Eq)

917934

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

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

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

921− setErrLine (getErrLine msg)

922− iputStrLn msg)

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

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

937+-- mapM_ (elabDecl EDefns info) ds

938+

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

940+elabDecl what info d

941+ = idrisCatch (elabDecl' what info d)

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

943+ setErrLine (getErrLine msg)

944+ iputStrLn msg)

923945

924946elabDecl' _ info (PFix _ _ _)

925947 = return () -- nothing to elaborate

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

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

966988 elabClass info s f cs n ps ds

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

968− | what /= EDefns

990+ | what /= ETypes

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

970992 elabInstance info s f cs n ps t expn ds

971993elabDecl' 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

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

10611061

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

1063− put (PDatadecl x1 x2 x3)

1064− = do put x1

1065− put x2

1066− put x3

1063+ put x

1064+ = case x of

1065+ PDatadecl x1 x2 x3 -> do putWord8 0

1066+ put x1

1067+ put x2

1068+ put x3

1069+ PLaterdecl x1 x2 -> do putWord8 1

1070+ put x1

1071+ put x2

10671072 get

1068− = do x1 <- get

1069− x2 <- get

1070− x3 <- get

1071− return (PDatadecl x1 x2 x3)

1073+ = do i <- getWord8

1074+ case i of

1075+ 0 -> do x1 <- get

1076+ x2 <- get

1077+ x3 <- get

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'"

10721083

10731084instance Binary PTerm where

10741085 put x

src/Idris/Parser.hs+24−22

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

104104 -- Now add all the declarations to the context

105105 v <- verbose

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

107− mapM_ (elabDecl toplevel) ds

107+ elabDecls toplevel ds

108108 i <- get

109109 -- simplify every definition do give the totality checker

110110 -- a better chance

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

11111111 tyn_in <- pfName

11121112 ty <- pTSig (impOK syn)

11131113 let tyn = expandNS syn tyn_in

1114− reserved "where"

1115− openBlock

1116− pushIndent

1117− cons <- many (do notEndBlock

1118− c <- pConstructor syn

1119− pKeepTerminator

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

1121− popIndent

1122− closeBlock

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

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

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

1115+ reserved "where"

1116+ openBlock

1117+ pushIndent

1118+ cons <- many (do notEndBlock

1119+ c <- pConstructor syn

1120+ pKeepTerminator

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

1122+ popIndent

1123+ closeBlock

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

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

11251126 <|> try (do pushIndent

11261127 acc <- pAccessibility

11271128 co <- pDataI

11281129 fc <- pfc

11291130 tyn_in <- pfName

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

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

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

1138− do let cty = bindArgs cargs conty

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

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

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

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)

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

1140+ do let cty = bindArgs cargs conty

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

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

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

11421144 where

11431145 mkPApp fc t [] = t

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

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

281281

282282elabPrims :: Idris ()

283−elabPrims = do mapM_ (elabDecl toplevel)

283+elabPrims = do mapM_ (elabDecl EAll toplevel)

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

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

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

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

2323S_inj Infinity Infinity refl = refl

2424

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

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

2626swap Nil = Nil

2727swap (x :: Nil) = x :: Nil

2828swap (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)

100100

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

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

103− (failure:Res (update gam p a) (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

103+ (failure:Res (update gam p a) (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

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

107107 Res gam gam (R ()) -> Res gam gam (R ())

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