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

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #641 from ahmadsalim/feature/metavarprooffix

01078f2Edwin Brady13 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'

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

860 let vtm = orderPats (getInferTerm tm')

865 let vtm = orderPats (getInferTerm tm')

861

866

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

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

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

863− addDeferred def'

869+ addDeferred def''

864 mapM_ (elabCaseBlock info []) is

870 mapM_ (elabCaseBlock info []) is

865

871

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

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

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

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

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

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

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

982 def' <- checkDef fc defer

988 def' <- checkDef fc defer

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

983− addDeferred def'

990+ addDeferred def''

984

991

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

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

986 -- from the where block

993 -- from the where block

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

1099 tt <- get_term

1106 tt <- get_term

1100 return (tt, d, is))

1107 return (tt, d, is))

1101 def' <- checkDef fc defer

1108 def' <- checkDef fc defer

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

1102− addDeferred def'

1110+ addDeferred def''

1103 mapM_ (elabCaseBlock info opts) is

1111 mapM_ (elabCaseBlock info opts) is

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

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

1105 let cwvaltyN = explicitNames cwvalty

1113 let cwvaltyN = explicitNames cwvalty

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

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

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

1131 addIBC (IBCDef wname)

1139 addIBC (IBCDef wname)

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

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

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

1133− addDeferred def'

1142+ addDeferred def''

1134

1143

1135 -- in the subdecls, lhs becomes:

1144 -- in the subdecls, lhs becomes:

1136 -- fname pats | wpat [rest]

1145 -- fname pats | wpat [rest]

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

1158 tt <- get_term

1167 tt <- get_term

1159 return (tt, d, is))

1168 return (tt, d, is))

1160 def' <- checkDef fc defer

1169 def' <- checkDef fc defer

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

1161− addDeferred def'

1171+ addDeferred def''

1162 mapM_ (elabCaseBlock info opts) is

1172 mapM_ (elabCaseBlock info opts) is

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

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

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

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

src/Idris/REPL.hs+12−9

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

447 case lookupNames n ctxt of

448 ts@(t:_) ->

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

451 Nothing -> ihPrintResult h $

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

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

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

673 [] -> return n

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

675 i <- getIState

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

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

677− Just mi -> mi

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

678− _ -> (Nothing, 0)

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

679 let fc = fileFC fn

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

681 (ProofSearch t n hints)]

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

742 insertMetavar n =

743 do i <- getIState

744 let ms = idris_metavars i

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

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

746

747process h fn' (AddProof prf)

748 = do fn <- do

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

784process h fn (Prove n')

785 = do ctxt <- getContext

786 ist <- getIState

787− n <- case lookupNames n' ctxt of

787+ let ns = lookupNames n' ctxt

788− [x] -> return x

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

789− [] -> return n'

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

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

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

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

791 prover (lit fn) n

794 prover (lit fn) n

792 -- recheck totality

795 -- recheck totality

793 i <- getIState

796 i <- getIState