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

git.iko.soy/Idris-dev

More flexible holes

Holes can now depend on other holes (e.g. hole bindings in a term which will be inferred from the solution of the hole). However, holes with dependencies can only be inspected, not defined later, since the later definition won't solve those remaining implicit arguments.

commit76c46bb770b8de187200516923b00ee5bfd1f5f9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 25 Feb 2016, 13:28 (11 years ago) parentbe0ff0f

10 files changed+59−34

compare with master

unifiedsplit

CHANGELOG+3 src/Idris/AbsSyntax.hs+7−3 src/Idris/Elab/Clause.hs+28−12 src/Idris/Elab/Data.hs+1−1 src/Idris/Elab/Term.hs+2−2 src/Idris/Elab/Type.hs+4−4 src/Idris/Elab/Utils.hs+11−9 src/Idris/Elab/Value.hs+1−1 src/Idris/IBC.hs+1−1 src/Idris/Prover.hs+1−1

CHANGELOG+3

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

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

6161 Write is deprecated and renamed to WriteTruncate.

6262* 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).

6366

6467New in 0.10:

6568============

src/Idris/AbsSyntax.hs+7−3

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

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

673673 tidyNames used b = b

674674

675−solveDeferred :: Name -> Idris ()

676−solveDeferred n = do i <- getIState

677− putIState $ i { idris_metavars =

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

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

681+ _ -> putIState $ i { idris_metavars =

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

679683 (idris_metavars i),

680684 ibc_write =

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

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

8787 let pats_raw = map (simple_lhs ctxt) pats_in

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

8989

90− solveDeferred n

90+ solveDeferred fc n

9191

9292 -- just ensure that the structure exists

9393 fmodifyState (ist_optimisation n) id

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

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

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

672672 logElab 5 "STARTING CHECK"

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

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

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

675675 (do pbinds ist lhs_tm

676676 -- 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

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

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

689689 probs <- get_probs

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

690+ hs <- get_holes

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

691692 setContext ctxt'

692693 processTacticDecls info newDecls

693694 sendHighlighting highlights

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

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

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

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

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

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

702+

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

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

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

703706 addDeferred def''

707+

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

705709

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

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

716720 logElab 5 $ "Rechecking"

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

718722

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

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

721− borrowed fc id [] rhs'

722− else return (rhs', clhsty)

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

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

730+ borrowed fc id [] rhs'

731+ else return (rhs', clhsty)

732+

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

724740 ctxt <- getContext

725741 let constv = next_tvar ctxt

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

861877 processTacticDecls info newDecls

862878 sendHighlighting highlights

863879

864− def' <- checkDef fc iderr defer

880+ def' <- checkDef fc iderr True defer

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

866882 addDeferred def''

867883 mapM_ (elabCaseBlock info opts) is

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

926942 addIBC (IBCImp wname)

927943 addIBC (IBCStatic wname)

928944

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

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

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

931947 addDeferred def''

932948

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

967983 processTacticDecls info newDecls

968984 sendHighlighting highlights

969985

970− def' <- checkDef fc iderr defer

986+ def' <- checkDef fc iderr True defer

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

972988 addDeferred def''

973989 mapM_ (elabCaseBlock info opts) is

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

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

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

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

357357 case eliminatorClauses of

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

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

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

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

361361 where elimLog :: String -> EliminatorState ()

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

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

25082508 updateIState $ \i -> i { idris_implicits =

25092509 addDef n impls (idris_implicits i) }

25102510 addIBC (IBCImp n)

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

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

25122512 addIBC (IBCDef n)

25132513 ctxt <- getContext

25142514 case lookupDef n ctxt of

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

25282528 addIBC (IBCInstance False True className instName)

25292529 RClausesInstrs n cs ->

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

2531− solveDeferred n

2531+ solveDeferred emptyFC n

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

25332533 let fc = fileFC "elab_reflected"

25342534 pmissing <-

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

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

7878

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

8080

81− ds <- checkAddDef True False fc iderr defer

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

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

8383 -- things later (for solving metavariables)

8484 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

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

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

175175 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, []))]

177177 addIBC (IBCDef n)

178178 addDefinedName n

179179 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

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

256256

257257 -- remove it from the deferred definitions list

258− solveDeferred n

258+ solveDeferred fc n

259259

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

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

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

268268 addIBC (IBCExtern (n, arity))

269269

270270 -- 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

5656iderr :: Name -> Err -> Err

5757iderr _ e = e

5858

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

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

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

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

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

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

62+checkDef fc mkerr definable ns

63+ = checkAddDef False True fc mkerr definable ns

6264

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

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

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

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

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

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

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

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

6870 = do ctxt <- getContext

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

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

7072 (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))]

7274 addIBC (IBCDef n)

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

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

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

7577

7678-- | 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

7575

7676 let vtm = orderPats (getInferTerm tm')

7777

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

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

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

8080 addDeferred def''

8181 mapM_ (elabCaseBlock info []) is

src/Idris/IBC.hs+1−1

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

533533 case d' of

534534 TyDecl _ _ -> return ()

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

536− solveDeferred n

536+ solveDeferred emptyFC n

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

538538 ) ds

539539 where

src/Idris/Prover.hs+1−1

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

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

125125 ctxt

126126 setContext ctxt'

127− solveDeferred n

127+ solveDeferred emptyFC n

128128 case idris_outputmode i of

129129 IdeMode n h ->

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