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

git.iko.soy/Idris-dev

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

commit1e6c727d4b41cc72d07bc4c6404682503439d26a authorAhmad Salim Al-Sibahi <asal@itu.dk> dateTue 19 Nov 2013, 18:31 (13 years ago) parent76a3fda

6 files changed+39−26

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+3−3 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Completion.hs+1−1 src/Idris/Delaborate.hs+2−2 src/Idris/ElabDecls.hs+20−10 src/Idris/REPL.hs+12−9

src/Idris/AbsSyntax.hs+3−3

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

281281addDeferred = addDeferred' Ref

282282addDeferredTyCon = addDeferred' (TCon 0 0)

283283

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

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

285285addDeferred' 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

287287 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 ++

289289 idris_metavars i }

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

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

src/Idris/AbsSyntaxTree.hs+1−1

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

102102 idris_name :: Int,

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

104104 -- ^ 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

106106 idris_coercions :: [Name],

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

108108 syntax_rules :: [Syntax],

src/Idris/Completion.hs+1−1

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

7171

7272metavars :: Idris [String]

7373metavars = 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

7575

7676

7777modules :: Idris [String]

src/Idris/Delaborate.hs+2−2

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

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

4242 | otherwise

4343 = case lookup n (idris_metavars ist) of

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

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

4545 _ -> PRef un (dens n)

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

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

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

8686 (de env [] r)

8787 deFn env (P _ n _) args

8888 = case lookup n (idris_metavars ist) of

89− Just (Just _, mi) ->

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

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

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

9292 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

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

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

6565 ds <- checkDef fc defer

66− addDeferred ds

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

67+ addDeferred ds'

6768 mapM_ (elabCaseBlock info opts) is

6869 ctxt <- getContext

6970 logLvl 5 $ "Rechecking"

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

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

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

9192 addIBC (IBCDef n)

92− addDeferred ds

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

94+ addDeferred ds'

9395 setFlags n opts'

9496 addDocStr n doc

9597 addIBC (IBCDoc n)

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

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

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

145147 def' <- checkDef fc defer

146− addDeferredTyCon def'

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

149+ addDeferredTyCon def''

147150 mapM_ (elabCaseBlock info []) is

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

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

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

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

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

162165 def' <- checkDef fc defer

163− addDeferredTyCon def'

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

167+ addDeferredTyCon def''

164168 mapM_ (elabCaseBlock info []) is

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

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

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

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

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

509513 def' <- checkDef fc defer

510− addDeferred def'

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

515+ addDeferred def''

511516 mapM_ (elabCaseBlock info []) is

512517 ctxt <- getContext

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

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

858863 let vtm = orderPats (getInferTerm tm')

859864

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

861− addDeferred def'

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

867+ addDeferred def''

862868 mapM_ (elabCaseBlock info []) is

863869

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

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

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

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

980986 def' <- checkDef fc defer

981− addDeferred def'

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

988+ addDeferred def''

982989

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

984991 -- from the where block

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

10971104 tt <- get_term

10981105 return (tt, d, is))

10991106 def' <- checkDef fc defer

1100− addDeferred def'

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

1108+ addDeferred def''

11011109 mapM_ (elabCaseBlock info opts) is

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

11031111 let cwvaltyN = explicitNames cwvalty

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

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

11291137 addIBC (IBCDef wname)

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

1131− addDeferred def'

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

1140+ addDeferred def''

11321141

11331142 -- in the subdecls, lhs becomes:

11341143 -- fname pats | wpat [rest]

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

11561165 tt <- get_term

11571166 return (tt, d, is))

11581167 def' <- checkDef fc defer

1159− addDeferred def'

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

1169+ addDeferred def''

11601170 mapM_ (elabCaseBlock info opts) is

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

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

src/Idris/REPL.hs+12−9

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

449449 case lookupNames n ctxt of

450450 ts@(t:_) ->

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

453453 Nothing -> ihPrintResult h $

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

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

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

675675 [] -> return n

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

677677 i <- getIState

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

679− Just mi -> mi

680− _ -> (Nothing, 0)

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

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

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

681681 let fc = fileFC fn

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

683683 (ProofSearch t n hints)]

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

744744 insertMetavar n =

745745 do i <- getIState

746746 let ms = idris_metavars i

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

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

748748

749749process h fn' (AddProof prf)

750750 = do fn <- do

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

786786process h fn (Prove n')

787787 = do ctxt <- getContext

788788 ist <- getIState

789− n <- case lookupNames n' ctxt of

790− [x] -> return x

791− [] -> return n'

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

789+ let ns = lookupNames n' ctxt

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

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

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

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

793796 prover (lit fn) n

794797 -- recheck totality

795798 i <- getIState