01078f2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #641 from ahmadsalim/feature/metavarprooffix

Disallow proving of top-level declarations and other meta-variables, fix...

commit01078f25d7d8c8f13749230b08820fed0747fbdb authorEdwin Brady <edwin.brady@gmail.com> dateTue 19 Nov 2013, 12:34 (13 years ago) parent27a6ec7 1e6c727

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'

@@ -860,7 +865,8 @@ elabValBind info aspat tm_in

860865 let vtm = orderPats (getInferTerm tm')

861866

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

863− addDeferred def'

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

869+ addDeferred def''

864870 mapM_ (elabCaseBlock info []) is

865871

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

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

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

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

982988 def' <- checkDef fc defer

983− addDeferred def'

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

990+ addDeferred def''

984991

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

986993 -- from the where block

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

10991106 tt <- get_term

11001107 return (tt, d, is))

11011108 def' <- checkDef fc defer

1102− addDeferred def'

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

1110+ addDeferred def''

11031111 mapM_ (elabCaseBlock info opts) is

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

11051113 let cwvaltyN = explicitNames cwvalty

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

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

11311139 addIBC (IBCDef wname)

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

1133− addDeferred def'

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

1142+ addDeferred def''

11341143

11351144 -- in the subdecls, lhs becomes:

11361145 -- fname pats | wpat [rest]

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

11581167 tt <- get_term

11591168 return (tt, d, is))

11601169 def' <- checkDef fc defer

1161− addDeferred def'

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

1171+ addDeferred def''

11621172 mapM_ (elabCaseBlock info opts) is

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

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

src/Idris/REPL.hs+12−9

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

447447 case lookupNames n ctxt of

448448 ts@(t:_) ->

449449 case lookup t (idris_metavars ist) of

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

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

451451 Nothing -> ihPrintResult h $

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

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

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

673673 [] -> return n

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

675675 i <- getIState

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

677− Just mi -> mi

678− _ -> (Nothing, 0)

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

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

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

679679 let fc = fileFC fn

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

681681 (ProofSearch t n hints)]

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

742742 insertMetavar n =

743743 do i <- getIState

744744 let ms = idris_metavars i

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

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

746746

747747process h fn' (AddProof prf)

748748 = do fn <- do

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

784784process h fn (Prove n')

785785 = do ctxt <- getContext

786786 ist <- getIState

787− n <- case lookupNames n' ctxt of

788− [x] -> return x

789− [] -> return n'

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

787+ let ns = lookupNames n' ctxt

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

789+ n <- case metavars of

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

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

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

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

791794 prover (lit fn) n

792795 -- recheck totality

793796 i <- getIState