76c46bb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More flexible holes

76c46bbEdwin Brady11 years ago

CHANGELOG+3

compare with master

unifiedsplit

@@ -60,6 +60,9 @@ Minor language changes

60* File Modes expanded: Append, ReadWriteTruncate, and ReadAppend added,

61 Write is deprecated and renamed to WriteTruncate.

62* C11 Extended Mode variations added to File Modes.

63+* More flexible holes.

64+ Holes can now depend on other holes in a term (such as implicit arguments

65+ which may be inferred from the definition of the hole).

64New in 0.10:

67New in 0.10:

65============

68============

src/Idris/AbsSyntax.hs+7−3

@@ -672,9 +672,13 @@ addDeferred' nt ns

672 Bind n' b $ tidyNames (S.insert n' used) sc

673 tidyNames used b = b

674

675−solveDeferred :: Name -> Idris ()

675+solveDeferred :: FC -> Name -> Idris ()

676−solveDeferred n = do i <- getIState

676+solveDeferred fc n

677+ = do i <- getIState

678+ case lookup n (idris_metavars i) of

679+ Just (_, _, _, _, False) ->

680+ throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")

677− putIState $ i { idris_metavars =

681+ _ -> putIState $ i { idris_metavars =

678 filter (\(n', _) -> n/=n')

682 filter (\(n', _) -> n/=n')

679 (idris_metavars i),

683 (idris_metavars i),

680 ibc_write =

684 ibc_write =

src/Idris/Elab/Clause.hs+28−12

@@ -87,7 +87,7 @@ elabClauses info' fc opts n_in cs =

87 let pats_raw = map (simple_lhs ctxt) pats_in

88 logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw

90− solveDeferred n

90+ solveDeferred fc n

92 -- just ensure that the structure exists

93 fmodifyState (ist_optimisation n) id

@@ -670,7 +670,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

670 logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

671 ctxt <- getContext -- new context with where block added

672 logElab 5 "STARTING CHECK"

673− ((rhs', defer, is, probs, ctxt', newDecls, highlights), _) <-

673+ ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights), _) <-

674 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState

675 (do pbinds ist lhs_tm

676 -- proof search can use explicitly written names

@@ -687,7 +687,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

687 let (tm, ds) = runState (collectDeferred (Just fname)

688 (map fst $ case_decls aux) ctxt tt) []

689 probs <- get_probs

690+ hs <- get_holes

690− return (tm, ds, is, probs, ctxt', newDecls, highlights))

691+ return (tm, ds, hs, is, probs, ctxt', newDecls, highlights))

691 setContext ctxt'

692 setContext ctxt'

692 processTacticDecls info newDecls

693 processTacticDecls info newDecls

693 sendHighlighting highlights

694 sendHighlighting highlights

@@ -698,9 +699,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

698 logElab 4 $ "---> " ++ show rhs'

699 logElab 4 $ "---> " ++ show rhs'

699 when (not (null defer)) $ logElab 1 $ "DEFERRED " ++

700 when (not (null defer)) $ logElab 1 $ "DEFERRED " ++

700 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)

701 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)

702+

703+ -- If there's holes, set the metavariables as undefinable

701− def' <- checkDef fc (\n -> Elaborating "deferred type of " n Nothing) defer

704+ def' <- checkDef fc (\n -> Elaborating "deferred type of " n Nothing) (null holes) defer

702− let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

705+ let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, null holes))) def'

703 addDeferred def''

706 addDeferred def''

707+

704 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

708 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''

705

709

706 when (not (null def')) $ do

710 when (not (null def')) $ do

@@ -716,11 +720,23 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

716 logElab 5 $ "Rechecking"

720 logElab 5 $ "Rechecking"

717 logElab 6 $ " ==> " ++ show (forget rhs')

721 logElab 6 $ " ==> " ++ show (forget rhs')

718

722

719− (crhs, crhsty) <- if not inf

723+ (crhs, crhsty) -- if there's holes && deferred things, it's okay

724+ -- but we'll need to freeze the definition and not

725+ -- allow the deferred things to be definable

726+ -- (this is just to allow users to inspect intermediate

727+ -- things)

728+ <- if (null holes || null def') && not inf

720− then recheckC_borrowing True (PEGenerated `notElem` opts)

729+ then recheckC_borrowing True (PEGenerated `notElem` opts)

721− borrowed fc id [] rhs'

730+ borrowed fc id [] rhs'

722− else return (rhs', clhsty)

731+ else return (rhs', clhsty)

732+

723 logElab 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty

733 logElab 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty

734+

735+ -- If there's holes, make sure this definition is frozen

736+ when (not (null holes)) $ do

737+ logElab 5 $ "Making " ++ show fname ++ " frozen due to " ++ show holes

738+ setAccessibility fname Frozen

739+

724 ctxt <- getContext

740 ctxt <- getContext

725 let constv = next_tvar ctxt

741 let constv = next_tvar ctxt

726 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

742 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

@@ -861,7 +877,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

861 processTacticDecls info newDecls

877 processTacticDecls info newDecls

862 sendHighlighting highlights

878 sendHighlighting highlights

863

879

864− def' <- checkDef fc iderr defer

880+ def' <- checkDef fc iderr True defer

865 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

881 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

866 addDeferred def''

882 addDeferred def''

867 mapM_ (elabCaseBlock info opts) is

883 mapM_ (elabCaseBlock info opts) is

@@ -926,7 +942,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

926 addIBC (IBCImp wname)

942 addIBC (IBCImp wname)

927 addIBC (IBCStatic wname)

943 addIBC (IBCStatic wname)

928

944

929− def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype, []))]

945+ def' <- checkDef fc iderr True [(wname, (-1, Nothing, wtype, []))]

930 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

946 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

931 addDeferred def''

947 addDeferred def''

932

948

@@ -967,7 +983,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

967 processTacticDecls info newDecls

983 processTacticDecls info newDecls

968 sendHighlighting highlights

984 sendHighlighting highlights

969

985

970− def' <- checkDef fc iderr defer

986+ def' <- checkDef fc iderr True defer

971 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

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

972 addDeferred def''

988 addDeferred def''

973 mapM_ (elabCaseBlock info opts) is

989 mapM_ (elabCaseBlock info opts) is

src/Idris/Elab/Data.hs+1−1

@@ -355,7 +355,7 @@ elabCaseFun ind paramPos n ty cons info = do

355 (ierror . Elaborating "type declaration of " elimDeclName Nothing)

356 -- Do not elaborate clauses if there aren't any

357 case eliminatorClauses of

358− [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type

358+ [] -> State.lift $ solveDeferred emptyFC elimDeclName -- Remove meta-variable for type

359 _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)

360 (ierror . Elaborating "clauses of " elimDeclName Nothing)

361 where elimLog :: String -> EliminatorState ()

src/Idris/Elab/Term.hs+2−2

@@ -2508,7 +2508,7 @@ processTacticDecls info steps =

2508 updateIState $ \i -> i { idris_implicits =

2509 addDef n impls (idris_implicits i) }

2510 addIBC (IBCImp n)

2511− ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty, []))]

2511+ ds <- checkDef fc (\_ e -> e) True [(n, (-1, Nothing, ty, []))]

2512 addIBC (IBCDef n)

2513 ctxt <- getContext

2514 case lookupDef n ctxt of

@@ -2528,7 +2528,7 @@ processTacticDecls info steps =

2528 addIBC (IBCInstance False True className instName)

2529 RClausesInstrs n cs ->

2530 do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n

2531− solveDeferred n

2531+ solveDeferred emptyFC n

2532 let lhss = map (\(_, lhs, _) -> lhs) cs

2533 let fc = fileFC "elab_reflected"

2534 pmissing <-

src/Idris/Elab/Type.hs+4−4

@@ -78,7 +78,7 @@ buildType info syn fc opts n ty' = do

79 logElab 3 $ show ty ++ "\nElaborated: " ++ show tyT'

81− ds <- checkAddDef True False fc iderr defer

81+ ds <- checkAddDef True False fc iderr True defer

82 -- if the type is not complete, note that we'll need to infer

83 -- things later (for solving metavariables)

84 when (length ds > length is) -- more deferred than case blocks

@@ -173,7 +173,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

173 -- Productivity checking now via checking for guarded 'Delay'

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

175 let usety = if norm then nty' else nty

176− ds <- checkDef fc iderr [(n, (-1, Nothing, usety, []))]

176+ ds <- checkDef fc iderr True [(n, (-1, Nothing, usety, []))]

177 addIBC (IBCDef n)

178 addDefinedName n

179 let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True, True))) ds

@@ -255,7 +255,7 @@ elabPostulate info syn doc fc nfc opts n ty = do

255 sendHighlighting [(nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]

256

257 -- remove it from the deferred definitions list

258− solveDeferred n

258+ solveDeferred fc n

259

260elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

261 FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()

@@ -268,4 +268,4 @@ elabExtern info syn doc fc nfc opts n ty = do

268 addIBC (IBCExtern (n, arity))

269

270 -- remove it from the deferred definitions list

271− solveDeferred n

271+ solveDeferred fc n

src/Idris/Elab/Utils.hs+11−9

@@ -56,21 +56,23 @@ checkDeprecated fc n

56iderr :: Name -> Err -> Err

57iderr _ e = e

59+checkDef :: FC -> (Name -> Err -> Err) -> Bool ->

59−checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type, [Name]))]

60+ [(Name, (Int, Maybe Name, Type, [Name]))] ->

60− -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

61+ Idris [(Name, (Int, Maybe Name, Type, [Name]))]

62+checkDef fc mkerr definable ns

61−checkDef fc mkerr ns = checkAddDef False True fc mkerr ns

63+ = checkAddDef False True fc mkerr definable ns

63−checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)

65+checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err) -> Bool

64 -> [(Name, (Int, Maybe Name, Type, [Name]))]

66 -> [(Name, (Int, Maybe Name, Type, [Name]))]

65 -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

67 -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

66−checkAddDef add toplvl fc mkerr [] = return []

68+checkAddDef add toplvl fc mkerr def [] = return []

67−checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns)

69+checkAddDef add toplvl fc mkerr definable ((n, (i, top, t, psns)) : ns)

68 = do ctxt <- getContext

70 = do ctxt <- getContext

69− logElab 5 $ "Rechecking deferred name " ++ show (n, t)

71+ logElab 5 $ "Rechecking deferred name " ++ show (n, t, definable)

70 (t', _) <- recheckC fc (mkerr n) [] t

72 (t', _) <- recheckC fc (mkerr n) [] t

71− when add $ do addDeferred [(n, (i, top, t, psns, toplvl, True))]

73+ when add $ do addDeferred [(n, (i, top, t, psns, toplvl, definable))]

72 addIBC (IBCDef n)

74 addIBC (IBCDef n)

73− ns' <- checkAddDef add toplvl fc mkerr ns

75+ ns' <- checkAddDef add toplvl fc mkerr definable ns

74 return ((n, (i, top, t', psns)) : ns')

76 return ((n, (i, top, t', psns)) : ns')

76-- | Get the list of (index, name) of inaccessible arguments from an elaborated

78-- | Get the list of (index, name) of inaccessible arguments from an elaborated

src/Idris/Elab/Value.hs+1−1

@@ -75,7 +75,7 @@ elabValBind info aspat norm tm_in

76 let vtm = orderPats (getInferTerm tm')

78− def' <- checkDef (fileFC "(input)") iderr defer

78+ def' <- checkDef (fileFC "(input)") iderr True defer

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

80 addDeferred def''

81 mapM_ (elabCaseBlock info []) is

src/Idris/IBC.hs+1−1

@@ -533,7 +533,7 @@ pDefs reexp ds

533 case d' of

534 TyDecl _ _ -> return ()

535 _ -> do logIBC 1 $ "SOLVING " ++ show n

536− solveDeferred n

536+ solveDeferred emptyFC n

537 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

538 ) ds

539 where

src/Idris/Prover.hs+1−1

@@ -124,7 +124,7 @@ prove mode opt ctxt lit n ty

124 [([], P Ref n ty, ptm')] ty

125 ctxt

126 setContext ctxt'

127− solveDeferred n

127+ solveDeferred emptyFC n

128 case idris_outputmode i of

129 IdeMode n h ->

130 runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n