fc6eb53 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Bug fixes; checking type names in data decls

fc6eb53Edwin Brady15 years ago

src/Core/Evaluate.hs+11−10

compare with master

unifiedsplit

@@ -472,14 +472,15 @@ instance Binary (a -> b) where

472data Accessibility = Public | Frozen | Hidden

473 deriving (Show, Eq)

474

475+data Totality = Total [Int] -- well-founded arguments

475−data Totality = Total | Partial PReason

476+ | Partial PReason

476 deriving Eq

477 deriving Eq

477

478

478−data PReason = Other [Name] | Itself | NotCovering | NotPositive

479+data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

479 deriving (Show, Eq)

480 deriving (Show, Eq)

480

481

481instance Show Totality where

482instance Show Totality where

482− show Total = "Total"

483+ show (Total args)= "Total, " ++ show args ++ " decreasing arguments"

483 show (Partial Itself) = "not total as it is not well founded"

484 show (Partial Itself) = "not total as it is not well founded"

484 show (Partial NotCovering) = "not total as there are missing cases"

485 show (Partial NotCovering) = "not total as there are missing cases"

485 show (Partial NotPositive) = "not strictly positive"

486 show (Partial NotPositive) = "not strictly positive"

@@ -511,7 +512,7 @@ veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

511addToCtxt :: Name -> Term -> Type -> Context -> Context

512addToCtxt :: Name -> Term -> Type -> Context -> Context

512addToCtxt n tm ty uctxt

513addToCtxt n tm ty uctxt

513 = let ctxt = definitions uctxt

514 = let ctxt = definitions uctxt

514− ctxt' = addDef n (Function ty tm, Public, Total) ctxt in

515+ ctxt' = addDef n (Function ty tm, Public, Total []) ctxt in

515 uctxt { definitions = ctxt' }

516 uctxt { definitions = ctxt' }

516

517

517setAccess :: Name -> Accessibility -> Context -> Context

518setAccess :: Name -> Accessibility -> Context -> Context

@@ -528,13 +529,13 @@ setTotal n t uctxt

528

529

529addCtxtDef :: Name -> Def -> Context -> Context

530addCtxtDef :: Name -> Def -> Context -> Context

530addCtxtDef n d c = let ctxt = definitions c

531addCtxtDef n d c = let ctxt = definitions c

531− ctxt' = addDef n (d, Public, Total) ctxt in

532+ ctxt' = addDef n (d, Public, Total []) ctxt in

532 c { definitions = ctxt' }

533 c { definitions = ctxt' }

533

534

534addTyDecl :: Name -> Type -> Context -> Context

535addTyDecl :: Name -> Type -> Context -> Context

535addTyDecl n ty uctxt

536addTyDecl n ty uctxt

536 = let ctxt = definitions uctxt

537 = let ctxt = definitions uctxt

537− ctxt' = addDef n (TyDecl Ref ty, Public, Total) ctxt in

538+ ctxt' = addDef n (TyDecl Ref ty, Public, Total []) ctxt in

538 uctxt { definitions = ctxt' }

539 uctxt { definitions = ctxt' }

539

540

540addDatatype :: Datatype Name -> Context -> Context

541addDatatype :: Datatype Name -> Context -> Context

@@ -542,14 +543,14 @@ addDatatype (Data n tag ty cons) uctxt

542 = let ctxt = definitions uctxt

543 = let ctxt = definitions uctxt

543 ty' = normalise uctxt [] ty

544 ty' = normalise uctxt [] ty

544 ctxt' = addCons 0 cons (addDef n

545 ctxt' = addCons 0 cons (addDef n

545− (TyDecl (TCon tag (arity ty')) ty, Public, Total) ctxt) in

546+ (TyDecl (TCon tag (arity ty')) ty, Public, Total []) ctxt) in

546 uctxt { definitions = ctxt' }

547 uctxt { definitions = ctxt' }

547 where

548 where

548 addCons tag [] ctxt = ctxt

549 addCons tag [] ctxt = ctxt

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

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

550 = let ty' = normalise uctxt [] ty in

551 = let ty' = normalise uctxt [] ty in

551 addCons (tag+1) cons (addDef n

552 addCons (tag+1) cons (addDef n

552− (TyDecl (DCon tag (arity ty')) ty, Public, Total) ctxt)

553+ (TyDecl (DCon tag (arity ty')) ty, Public, Total []) ctxt)

553

554

554addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->

555addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->

555 Type -> Context -> Context

556 Type -> Context -> Context

@@ -561,7 +562,7 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt

561 (CaseDef args sc _, CaseDef args' sc' _) ->

562 (CaseDef args sc _, CaseDef args' sc' _) ->

562 let inl = alwaysInline in

563 let inl = alwaysInline in

563 addDef n (CaseOp inl ty ps args sc args' sc',

564 addDef n (CaseOp inl ty ps args sc args' sc',

564− Public, Total) ctxt in

565+ Public, Total []) ctxt in

565 uctxt { definitions = ctxt' }

566 uctxt { definitions = ctxt' }

566 where simpl [] = []

567 where simpl [] = []

567 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

568 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

@@ -569,7 +570,7 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt

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

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

570addOperator n ty a op uctxt

571addOperator n ty a op uctxt

571 = let ctxt = definitions uctxt

572 = let ctxt = definitions uctxt

572− ctxt' = addDef n (Operator ty a op, Public, Total) ctxt in

573+ ctxt' = addDef n (Operator ty a op, Public, Total []) ctxt in

573 uctxt { definitions = ctxt' }

574 uctxt { definitions = ctxt' }

574

575

575tfst (a, _, _) = a

576tfst (a, _, _) = a

src/Idris/Coverage.hs+13−9

@@ -98,20 +98,22 @@ genAll i args = concatMap otherPats (nub args)

98upd p' p = p { getTm = p' }

100-- recursive calls are well-founded if one of their argument positions is

101−-- always decreasing.

101+-- always decreasing. Return a list of arguments which are either not used

102+-- recursively, or always decreasing recursively

102

103

103-- If we encounter a non-total name, we'll fail

104-- If we encounter a non-total name, we'll fail

104

105

105−wellFounded :: IState -> Name -> SC -> Either [Name] Bool

106+wellFounded :: IState -> Name -> SC -> Totality

106wellFounded i n sc = case wff [] sc of

107wellFounded i n sc = case wff [] sc of

107 RightOK smaller_args ->

108 RightOK smaller_args ->

108 -- is there a number in every list?

109 -- is there a number in every list?

109 -- trace (show (n, smaller_args)) $

110 -- trace (show (n, smaller_args)) $

110 case smaller_args of

111 case smaller_args of

111− [] -> Right True

112+ [] -> Total []

112 (x : xs) -> let args = foldl intersect x xs in

113 (x : xs) -> let args = foldl intersect x xs in

113− Right $ not (null args)

114+ if (null args) then Partial Itself

115+ else Total args

114− LeftErr x -> Left x

116+ LeftErr x -> Partial (Other x)

115 where

117 where

116 wff :: [Name] -> SC -> EitherErr [Name] [[Int]]

118 wff :: [Name] -> SC -> EitherErr [Name] [[Int]]

117 wff ns (Case n as) = do is <- mapM (wffC ns) as

119 wff ns (Case n as) = do is <- mapM (wffC ns) as

@@ -125,9 +127,8 @@ wellFounded i n sc = case wff [] sc of

125

127

126 checkOK n' = case lookupTotal n' (tt_ctxt i) of

128 checkOK n' = case lookupTotal n' (tt_ctxt i) of

127 [Partial _] -> LeftErr [n']

129 [Partial _] -> LeftErr [n']

128− [Total] -> RightOK ()

130+ [Total _] -> RightOK ()

129 x -> RightOK ()

131 x -> RightOK ()

130−-- checkOK n = RightOK ()

131

132

132 argPos ns ap@(App f' a')

133 argPos ns ap@(App f' a')

133 | (P _ f _, args) <- unApply ap

134 | (P _ f _, args) <- unApply ap

@@ -153,10 +154,13 @@ checkPositive :: Name -> (Name, Type) -> Idris ()

153checkPositive n (cn, ty)

154checkPositive n (cn, ty)

154 = do let p = cp ty

155 = do let p = cp ty

155 i <- getIState

156 i <- getIState

156− let ctxt' = setTotal cn (if p then Total else Partial NotPositive)

157+ let tot = if p then Total (args ty) else Partial NotPositive

157− (tt_ctxt i)

158+ let ctxt' = setTotal cn tot (tt_ctxt i)

158 putIState (i { tt_ctxt = ctxt' })

159 putIState (i { tt_ctxt = ctxt' })

160+ addIBC (IBCTotal cn tot)

159 where

161 where

162+ args t = [0..length (getArgTys t)-1]

163+

160 cp (Bind n (Pi aty) sc) = posArg aty && cp sc

164 cp (Bind n (Pi aty) sc) = posArg aty && cp sc

161 cp t = True

165 cp t = True

162

166

src/Idris/ElabDecls.hs+16−16

@@ -1,4 +1,5 @@

1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}

1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

2+ PatternGuards #-}

3module Idris.ElabDecls where

4module Idris.ElabDecls where

@@ -72,7 +73,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

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

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

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

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

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

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

75− cons <- mapM (elabCon info syn) dcons

76+ cons <- mapM (elabCon info syn n) dcons

76 ttag <- getName

77 ttag <- getName

77 i <- get

78 i <- get

78 put (i { idris_datatypes = addDef n (TI (map fst cons))

79 put (i { idris_datatypes = addDef n (TI (map fst cons))

@@ -88,8 +89,8 @@ elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->

88elabRecord info syn fc tyn ty cn cty

89elabRecord info syn fc tyn ty cn cty

89 = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])

90 = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])

91−elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

92+elabCon :: ElabInfo -> SyntaxInfo -> Name -> (Name, PTerm, FC) -> Idris (Name, Type)

92−elabCon info syn (n, t_in, fc)

93+elabCon info syn tn (n, t_in, fc)

93 = do checkUndefined fc n

94 = do checkUndefined fc n

94 ctxt <- getContext

95 ctxt <- getContext

95 i <- get

96 i <- get

@@ -104,10 +105,17 @@ elabCon info syn (n, t_in, fc)

104 mapM_ (elabCaseBlock info) is

105 mapM_ (elabCaseBlock info) is

105 ctxt <- getContext

106 ctxt <- getContext

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

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

108+ tyIs cty

107 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

109 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

108 addIBC (IBCDef n)

110 addIBC (IBCDef n)

109 forceArgs n cty

111 forceArgs n cty

110 return (n, cty)

112 return (n, cty)

113+ where

114+ tyIs (Bind n b sc) = tyIs sc

115+ tyIs t | (P _ n' _, _) <- unApply t

116+ = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))

117+ else return ()

118+ tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

111

119

112elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

120elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

113elabClauses info fc opts n_in cs = let n = liftname info n_in in

121elabClauses info fc opts n_in cs = let n = liftname info n_in in

@@ -134,21 +142,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

134 let tree@(CaseDef _ sc _) = simpleCase tcase pcover pdef

142 let tree@(CaseDef _ sc _) = simpleCase tcase pcover pdef

135 ist <- get

143 ist <- get

136 let wf = wellFounded ist n sc

144 let wf = wellFounded ist n sc

137− tot <- if pcover

145+ let tot = if pcover

138− then case wf of

146+ then wf

139− Left ns -> do logLvl 2 $ show n ++ " not well founded due to "

140− ++ show ns

141− return $ Partial (Other ns)

142− Right False -> do logLvl 2 $ show n ++ " not well founded"

143− return $ Partial Itself

144− Right True -> do logLvl 2 $ show n ++ " well founded"

145− return Total

146− else do logLvl 2 $ show n ++ " does not cover all cases"

147− return $ Partial NotCovering

147+ else Partial NotCovering

148 case lookupCtxt (namespace info) n (idris_flags ist) of

149 [fs] -> if TotalFn `elem` fs

150 then case tot of

151− Total -> return ()

151+ Total _ -> return ()

152 t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

153 else return ()

154 _ -> return ()

src/Idris/IBC.hs+4−2

@@ -614,13 +614,15 @@ instance Binary PReason where

614instance Binary Totality where

615 put x

616 = case x of

617− Total -> putWord8 0

617+ Total x1 -> do putWord8 0

618+ put x1

618 Partial x1 -> do putWord8 1

619 Partial x1 -> do putWord8 1

619 put x1

620 put x1

620 get

621 get

621 = do i <- getWord8

622 = do i <- getWord8

622 case i of

623 case i of

624+ 0 -> do x1 <- get

623− 0 -> return Total

625+ return (Total x1)

624 1 -> do x1 <- get

626 1 -> do x1 <- get

625 return (Partial x1)

627 return (Partial x1)

626 _ -> error "Corrupted binary data for Totality"

628 _ -> error "Corrupted binary data for Totality"