fc6eb53 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Bug fixes; checking type names in data decls

commitfc6eb53c49fd1ae40e44e73946aaf7e4f1d7f6b7 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 25 Jan 2012, 16:04 (15 years ago) parentde6bb41

4 files changed+44−37

compare with master

unifiedsplit

src/Core/Evaluate.hs+11−10 src/Idris/Coverage.hs+13−9 src/Idris/ElabDecls.hs+16−16 src/Idris/IBC.hs+4−2

src/Core/Evaluate.hs+11−10

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

472472data Accessibility = Public | Frozen | Hidden

473473 deriving (Show, Eq)

474474

475−data Totality = Total | Partial PReason

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

476+ | Partial PReason

476477 deriving Eq

477478

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

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

479480 deriving (Show, Eq)

480481

481482instance Show Totality where

482− show Total = "Total"

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

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

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

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

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

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

512513addToCtxt n tm ty uctxt

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

515516 uctxt { definitions = ctxt' }

516517

517518setAccess :: Name -> Accessibility -> Context -> Context

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

528529

529530addCtxtDef :: Name -> Def -> Context -> Context

530531addCtxtDef 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

532533 c { definitions = ctxt' }

533534

534535addTyDecl :: Name -> Type -> Context -> Context

535536addTyDecl n ty uctxt

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

538539 uctxt { definitions = ctxt' }

539540

540541addDatatype :: Datatype Name -> Context -> Context

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

542543 = let ctxt = definitions uctxt

543544 ty' = normalise uctxt [] ty

544545 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

546547 uctxt { definitions = ctxt' }

547548 where

548549 addCons tag [] ctxt = ctxt

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

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

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

553554

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

555556 Type -> Context -> Context

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

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

562563 let inl = alwaysInline in

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

564− Public, Total) ctxt in

565+ Public, Total []) ctxt in

565566 uctxt { definitions = ctxt' }

566567 where simpl [] = []

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

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

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

570571addOperator n ty a op uctxt

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

573574 uctxt { definitions = ctxt' }

574575

575576tfst (a, _, _) = a

src/Idris/Coverage.hs+13−9

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

9898upd p' p = p { getTm = p' }

9999

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

102103

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

104105

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

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

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

107108 RightOK smaller_args ->

108109 -- is there a number in every list?

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

110111 case smaller_args of

111− [] -> Right True

112+ [] -> Total []

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

113− Right $ not (null args)

114− LeftErr x -> Left x

114+ if (null args) then Partial Itself

115+ else Total args

116+ LeftErr x -> Partial (Other x)

115117 where

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

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

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

125127

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

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

128− [Total] -> RightOK ()

130+ [Total _] -> RightOK ()

129131 x -> RightOK ()

130−-- checkOK n = RightOK ()

131132

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

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

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

153154checkPositive n (cn, ty)

154155 = do let p = cp ty

155156 i <- getIState

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

157− (tt_ctxt i)

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

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

158159 putIState (i { tt_ctxt = ctxt' })

160+ addIBC (IBCTotal cn tot)

159161 where

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

163+

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

161165 cp t = True

162166

src/Idris/ElabDecls.hs+16−16

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

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

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

2+ PatternGuards #-}

34module Idris.ElabDecls where

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

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

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

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

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

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

7677 ttag <- getName

7778 i <- get

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

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

8889elabRecord info syn fc tyn ty cn cty

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

9091

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

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

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

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

9394 = do checkUndefined fc n

9495 ctxt <- getContext

9596 i <- get

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

104105 mapM_ (elabCaseBlock info) is

105106 ctxt <- getContext

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

108+ tyIs cty

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

108110 addIBC (IBCDef n)

109111 forceArgs n cty

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

111119

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

113121elabClauses 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

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

135143 ist <- get

136144 let wf = wellFounded ist n sc

137− tot <- if pcover

138− then case wf of

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

145+ let tot = if pcover

146+ then wf

147+ else Partial NotCovering

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

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

150150 then case tot of

151− Total -> return ()

151+ Total _ -> return ()

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

153153 else return ()

154154 _ -> return ()

src/Idris/IBC.hs+4−2

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

614614instance Binary Totality where

615615 put x

616616 = case x of

617− Total -> putWord8 0

617+ Total x1 -> do putWord8 0

618+ put x1

618619 Partial x1 -> do putWord8 1

619620 put x1

620621 get

621622 = do i <- getWord8

622623 case i of

623− 0 -> return Total

624+ 0 -> do x1 <- get

625+ return (Total x1)

624626 1 -> do x1 <- get

625627 return (Partial x1)

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