1e6c727 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Disallow proving of top-level declarations and other meta-variables, fixes idris-lang/Idris-dev#46

1e6c727Ahmad Salim Al-Sibahi13 years ago

src/Idris/AbsSyntax.hs+3−3

compare with master

unifiedsplit

@@ -281,11 +281,11 @@ addConstraints fc (v, cs)

281addDeferred = addDeferred' Ref

282addDeferredTyCon = addDeferred' (TCon 0 0)

283

284−addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type))] -> Idris ()

284+addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()

285addDeferred' nt ns

286− = do mapM_ (\(n, (i, _, t)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

286+ = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

287 i <- getIState

288− putIState $ i { idris_metavars = map (\(n, (i, top, _)) -> (n, (top, i))) ns ++

288+ putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

289 idris_metavars i }

290 where tidyNames used (Bind (MN i x) b sc)

291 = let n' = uniqueName (UN x) used in

src/Idris/AbsSyntaxTree.hs+1−1

@@ -102,7 +102,7 @@ data IState = IState {

102 idris_name :: Int,

103 idris_lineapps :: [((FilePath, Int), PTerm)],

104 -- ^ Full application LHS on source line

105− idris_metavars :: [(Name, (Maybe Name, Int))], -- ^ The currently defined but not proven metavariables

105+ idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables

106 idris_coercions :: [Name],

107 idris_transforms :: [(Term, Term)],

108 syntax_rules :: [Syntax],

src/Idris/Completion.hs+1−1

@@ -71,7 +71,7 @@ names = do i <- get

72metavars :: Idris [String]

73metavars = do i <- get

74− return . map (show . nsroot) $ map fst (idris_metavars i) \\ primDefs

74+ return . map (show . nsroot) $ map fst (filter (\(_, (_,_,t)) -> not t) (idris_metavars i)) \\ primDefs

77modules :: Idris [String]

src/Idris/Delaborate.hs+2−2

@@ -41,7 +41,7 @@ delabTy' ist imps tm fullname = de [] imps tm

41 | Just n' <- lookup n env = PRef un n'

42 | otherwise

43 = case lookup n (idris_metavars ist) of

44− Just (Just _, mi) -> mkMVApp (dens n) []

44+ Just (Just _, mi, _) -> mkMVApp (dens n) []

45 _ -> PRef un (dens n)

46 de env _ (Bind n (Lam ty) sc)

47 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

@@ -86,7 +86,7 @@ delabTy' ist imps tm fullname = de [] imps tm

86 (de env [] r)

87 deFn env (P _ n _) args

88 = case lookup n (idris_metavars ist) of

89− Just (Just _, mi) ->

89+ Just (Just _, mi, _) ->

90 mkMVApp (dens n) (drop mi (map (de env []) args))

91 _ -> mkPApp (dens n) (map (de env []) args)

92 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

src/Idris/ElabDecls.hs+20−10

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

63 tclift $ elaborate ctxt n (TType (UVal 0)) []

64 (errAt "type of " n (erun fc (build i info False n ty)))

65 ds <- checkDef fc defer

66+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

66− addDeferred ds

67+ addDeferred ds'

67 mapM_ (elabCaseBlock info opts) is

68 mapM_ (elabCaseBlock info opts) is

68 ctxt <- getContext

69 ctxt <- getContext

69 logLvl 5 $ "Rechecking"

70 logLvl 5 $ "Rechecking"

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

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

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

90 ds <- checkDef fc [(n, (-1, Nothing, nty))]

91 ds <- checkDef fc [(n, (-1, Nothing, nty))]

91 addIBC (IBCDef n)

92 addIBC (IBCDef n)

93+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

92− addDeferred ds

94+ addDeferred ds'

93 setFlags n opts'

95 setFlags n opts'

94 addDocStr n doc

96 addDocStr n doc

95 addIBC (IBCDoc n)

97 addIBC (IBCDoc n)

@@ -143,7 +145,8 @@ elabData info syn doc fc codata (PLaterdecl n t_in)

143 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

145 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

144 (erun fc (build i info False n t))

146 (erun fc (build i info False n t))

145 def' <- checkDef fc defer

147 def' <- checkDef fc defer

148+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

146− addDeferredTyCon def'

149+ addDeferredTyCon def''

147 mapM_ (elabCaseBlock info []) is

150 mapM_ (elabCaseBlock info []) is

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

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

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

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

@@ -160,7 +163,8 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

160 tclift $ elaborate ctxt n (TType (UVal 0)) []

163 tclift $ elaborate ctxt n (TType (UVal 0)) []

161 (errAt "data declaration " n (erun fc (build i info False n t)))

164 (errAt "data declaration " n (erun fc (build i info False n t)))

162 def' <- checkDef fc defer

165 def' <- checkDef fc defer

166+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

163− addDeferredTyCon def'

167+ addDeferredTyCon def''

164 mapM_ (elabCaseBlock info []) is

168 mapM_ (elabCaseBlock info []) is

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

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

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

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

@@ -507,7 +511,8 @@ elabCon info syn tn codata (doc, n, t_in, fc)

507 (errAt "constructor " n (erun fc (build i info False n t)))

511 (errAt "constructor " n (erun fc (build i info False n t)))

508 logLvl 2 $ "Rechecking " ++ show t'

512 logLvl 2 $ "Rechecking " ++ show t'

509 def' <- checkDef fc defer

513 def' <- checkDef fc defer

514+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

510− addDeferred def'

515+ addDeferred def''

511 mapM_ (elabCaseBlock info []) is

516 mapM_ (elabCaseBlock info []) is

512 ctxt <- getContext

517 ctxt <- getContext

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

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

@@ -858,7 +863,8 @@ elabValBind info aspat tm_in

858 let vtm = orderPats (getInferTerm tm')

863 let vtm = orderPats (getInferTerm tm')

859

864

860 def' <- checkDef (fileFC "(input)") defer

865 def' <- checkDef (fileFC "(input)") defer

866+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'

861− addDeferred def'

867+ addDeferred def''

862 mapM_ (elabCaseBlock info []) is

868 mapM_ (elabCaseBlock info []) is

863

869

864 logLvl 3 ("Value: " ++ show vtm)

870 logLvl 3 ("Value: " ++ show vtm)

@@ -978,7 +984,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

978 logLvl 2 $ "---> " ++ show rhs'

984 logLvl 2 $ "---> " ++ show rhs'

979 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

985 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

980 def' <- checkDef fc defer

986 def' <- checkDef fc defer

987+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

981− addDeferred def'

988+ addDeferred def''

982

989

983 -- Now the remaining deferred (i.e. no type declarations) clauses

990 -- Now the remaining deferred (i.e. no type declarations) clauses

984 -- from the where block

991 -- from the where block

@@ -1097,7 +1104,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1097 tt <- get_term

1104 tt <- get_term

1098 return (tt, d, is))

1105 return (tt, d, is))

1099 def' <- checkDef fc defer

1106 def' <- checkDef fc defer

1107+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

1100− addDeferred def'

1108+ addDeferred def''

1101 mapM_ (elabCaseBlock info opts) is

1109 mapM_ (elabCaseBlock info opts) is

1102 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

1110 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

1103 let cwvaltyN = explicitNames cwvalty

1111 let cwvaltyN = explicitNames cwvalty

@@ -1128,7 +1136,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1128 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

1136 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

1129 addIBC (IBCDef wname)

1137 addIBC (IBCDef wname)

1130 def' <- checkDef fc [(wname, (-1, Nothing, wtype))]

1138 def' <- checkDef fc [(wname, (-1, Nothing, wtype))]

1139+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

1131− addDeferred def'

1140+ addDeferred def''

1132

1141

1133 -- in the subdecls, lhs becomes:

1142 -- in the subdecls, lhs becomes:

1134 -- fname pats | wpat [rest]

1143 -- fname pats | wpat [rest]

@@ -1156,7 +1165,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1156 tt <- get_term

1165 tt <- get_term

1157 return (tt, d, is))

1166 return (tt, d, is))

1158 def' <- checkDef fc defer

1167 def' <- checkDef fc defer

1168+ let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

1159− addDeferred def'

1169+ addDeferred def''

1160 mapM_ (elabCaseBlock info opts) is

1170 mapM_ (elabCaseBlock info opts) is

1161 logLvl 5 ("Checked RHS " ++ show rhs')

1171 logLvl 5 ("Checked RHS " ++ show rhs')

1162 (crhs, crhsty) <- recheckC fc [] rhs'

1172 (crhs, crhsty) <- recheckC fc [] rhs'

src/Idris/REPL.hs+12−9

@@ -449,7 +449,7 @@ process h fn (Check (PRef _ n))

449 case lookupNames n ctxt of

450 ts@(t:_) ->

451 case lookup t (idris_metavars ist) of

452− Just (_, i) -> ihPrintResult h (showMetavarInfo c imp ist n i)

452+ Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)

453 Nothing -> ihPrintResult h $

454 concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++

455 showImp (Just ist) imp c (delabTy ist n)) $ ts

@@ -675,9 +675,9 @@ process h fn (DoProofSearch updatefile l n hints)

675 [] -> return n

676 ns -> ierror (CantResolveAlts (map show ns))

677 i <- getIState

678− let (top, envlen) = case lookup mn (idris_metavars i) of

678+ let (top, envlen, _) = case lookup mn (idris_metavars i) of

679− Just mi -> mi

679+ Just (t, e, False) -> (t, e, False)

680− _ -> (Nothing, 0)

680+ _ -> (Nothing, 0, True)

681 let fc = fileFC fn

682 let body t = PProof [Try (TSeq Intros (ProofSearch t n hints))

683 (ProofSearch t n hints)]

@@ -744,7 +744,7 @@ process h fn (RmProof n')

744 insertMetavar n =

745 do i <- getIState

746 let ms = idris_metavars i

747− putIState $ i { idris_metavars = (n, (Nothing, 0)) : ms }

747+ putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }

748

749process h fn' (AddProof prf)

750 = do fn <- do

@@ -786,10 +786,13 @@ process h fn (ShowProof n')

786process h fn (Prove n')

787 = do ctxt <- getContext

788 ist <- getIState

789− n <- case lookupNames n' ctxt of

789+ let ns = lookupNames n' ctxt

790− [x] -> return x

790+ let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns

791+ n <- case metavars of

792+ [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

791− [] -> return n'

793+ [(n, (_,_,False))] -> return n

794+ [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

792− ns -> ierror (CantResolveAlts (map show ns))

795+ ns -> ierror (CantResolveAlts (map show ns))

793 prover (lit fn) n

796 prover (lit fn) n

794 -- recheck totality

797 -- recheck totality

795 i <- getIState

798 i <- getIState