f833918 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

(Experimental) Create deferred definitions by application

f833918Edwin Brady14 years ago

src/Core/Elaborate.hs+4

compare with master

unifiedsplit

@@ -266,6 +266,10 @@ defer :: Name -> Elab' aux ()

266defer n = do n' <- unique_hole n

267 processTactic' (Defer n')

268

269+deferType :: Name -> Raw -> [Name] -> Elab' aux ()

270+deferType n ty ns = do n' <- unique_hole n

271+ processTactic' (DeferType n' ty ns)

272+

269instanceArg :: Name -> Elab' aux ()

273instanceArg :: Name -> Elab' aux ()

270instanceArg n = processTactic' (Instance n)

274instanceArg n = processTactic' (Instance n)

271

275

src/Core/ProofState.hs+37−23

@@ -65,6 +65,7 @@ data Tactic = Attack

65 | PatBind Name

66 | Focus Name

67 | Defer Name

68+ | DeferType Name Raw [Name]

68 | Instance Name

69 | Instance Name

69 | MoveLast Name

70 | MoveLast Name

70 | ProofState

71 | ProofState

@@ -298,6 +299,18 @@ defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

298

299

299 getP (n, b) = P Bound n (binderTy b)

300 getP (n, b) = P Bound n (binderTy b)

300

301

302+-- as defer, but build the type and application explicitly

303+deferType :: Name -> Raw -> [Name] -> RunTactic

304+deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

305+ do (fty, _) <- lift $ check ctxt env fty_in

306+ action (\ps -> let hs = holes ps in

307+ ps { holes = hs \\ [x] })

308+ return (Bind n (GHole fty)

309+ (mkApp (P Ref n ty) (map getP args)))

310+ where

311+ getP n = case lookup n env of

312+ Just b -> P Bound n (binderTy b)

313+

301regret :: RunTactic

314regret :: RunTactic

302regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

315regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

303 do action (\ps -> let hs = holes ps in

316 do action (\ps -> let hs = holes ps in

@@ -577,27 +590,28 @@ process EndUnify _

577 let (h, _) = unified ps

590 let (h, _) = unified ps

578 tactic (Just h) solve_unified

591 tactic (Just h) solve_unified

579process t h = tactic (Just h) (mktac t)

592process t h = tactic (Just h) (mktac t)

580− where mktac Attack = attack

593+ where mktac Attack = attack

581− mktac (Claim n r) = claim n r

594+ mktac (Claim n r) = claim n r

582− mktac (Exact r) = exact r

595+ mktac (Exact r) = exact r

583− mktac (Fill r) = fill r

596+ mktac (Fill r) = fill r

584− mktac (PrepFill n ns) = prep_fill n ns

597+ mktac (PrepFill n ns) = prep_fill n ns

585− mktac CompleteFill = complete_fill

598+ mktac CompleteFill = complete_fill

586− mktac Regret = regret

599+ mktac Regret = regret

587− mktac Solve = solve

600+ mktac Solve = solve

588− mktac (StartUnify n) = start_unify n

601+ mktac (StartUnify n) = start_unify n

589− mktac Compute = compute

602+ mktac Compute = compute

590− mktac (Intro n) = intro n

603+ mktac (Intro n) = intro n

591− mktac (IntroTy ty n) = introTy ty n

604+ mktac (IntroTy ty n) = introTy ty n

592− mktac (Forall n t) = forall n t

605+ mktac (Forall n t) = forall n t

593− mktac (LetBind n t v) = letbind n t v

606+ mktac (LetBind n t v) = letbind n t v

594− mktac (Rewrite t) = rewrite t

607+ mktac (Rewrite t) = rewrite t

595− mktac (PatVar n) = patvar n

608+ mktac (PatVar n) = patvar n

596− mktac (PatBind n) = patbind n

609+ mktac (PatBind n) = patbind n

597− mktac (CheckIn r) = check_in r

610+ mktac (CheckIn r) = check_in r

598− mktac (EvalIn r) = eval_in r

611+ mktac (EvalIn r) = eval_in r

599− mktac (Focus n) = focus n

612+ mktac (Focus n) = focus n

600− mktac (Defer n) = defer n

613+ mktac (Defer n) = defer n

614+ mktac (DeferType n t a) = deferType n t a

601− mktac (Instance n) = instanceArg n

615+ mktac (Instance n) = instanceArg n

602− mktac (MoveLast n) = movelast n

616+ mktac (MoveLast n) = movelast n

603

617

src/Idris/AbsSyntax.hs+4

@@ -776,6 +776,9 @@ addImpl' inpat env ist ptm = ai env ptm

776 PDPair fc l' t' r'

777 ai env (PAlternative a as) = let as' = map (ai env) as in

778 PAlternative a as'

779+ ai env (PApp fc (PInferRef _ f) as)

780+ = let as' = map (fmap (ai env)) as in

781+ PApp fc (PInferRef fc f) as'

779 ai env (PApp fc (PRef _ f) as)

782 ai env (PApp fc (PRef _ f) as)

780 | not (f `elem` env)

783 | not (f `elem` env)

781 = let as' = map (fmap (ai env)) as in

784 = let as' = map (fmap (ai env)) as in

@@ -1000,6 +1003,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1000 _ -> LeftErr (a, b)

1003 _ -> LeftErr (a, b)

1001 match (PCase _ _ _) _ = return [] -- lifted out

1004 match (PCase _ _ _) _ = return [] -- lifted out

1002 match (PMetavar _) _ = return [] -- modified

1005 match (PMetavar _) _ = return [] -- modified

1006+ match (PInferRef _ _) _ = return [] -- modified

1003 match (PQuote _) _ = return []

1007 match (PQuote _) _ = return []

1004 match (PProof _) _ = return []

1008 match (PProof _) _ = return []

1005 match (PTactics _) _ = return []

1009 match (PTactics _) _ = return []

src/Idris/AbsSyntaxTree.hs+1

@@ -894,6 +894,7 @@ showImp :: Bool -> PTerm -> String

894showImp impl tm = se 10 tm where

895 se p (PQuote r) = "![" ++ show r ++ "]"

896 se p (PPatvar fc n) = show n

897+ se p (PInferRef fc n) = show n -- ++ "[" ++ show fc ++ "]"

897 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"

898 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"

898 else showbasic n

899 else showbasic n

899 where showbasic n@(UN _) = show n

900 where showbasic n@(UN _) = show n

src/Idris/ElabTerm.hs+30−2

@@ -232,8 +232,36 @@ elab ist info pattern tcgen fn tm

232 elabE (True, a) val

233 elabE (True, a) sc

234 solve

235− elab' (ina, g) tm@(PApp fc (PInferRef _ f) args')

235+ elab' ina tm@(PApp fc (PInferRef _ f) args)

236− = fail "Not implemented"

236+ = do rty <- goal

237+ -- make a function type a -> b -> c -> ... -> rty for the

238+ -- new function name

239+ argTys <- claimArgTys args

240+ fn <- unique_hole (MN 0 "inf_fn")

241+ let fty = fnTy argTys rty

242+-- trace (show (ptm, map fst argTys)) $ focus fn

243+ -- build and defer the function application

244+ attack; deferType f fty (map fst argTys); solve

245+ -- elaborate the arguments, to unify their types. They all have to

246+ -- be explicit.

247+ mapM_ elabIArg (zip argTys args)

248+ where claimArgTys [] = return []

249+ claimArgTys (arg : xs) | PRef _ n <- getTm arg

250+ = do nty <- get_type (Var n)

251+ ans <- claimArgTys xs

252+ return ((n, (False, forget nty)) : ans)

253+ claimArgTys (_ : xs) = do an <- unique_hole (MN 0 "inf_argTy")

254+ aval <- unique_hole (MN 0 "inf_arg")

255+ claim an RSet

256+ claim aval (Var an)

257+ ans <- claimArgTys xs

258+ return ((aval, (True, (Var an))) : ans)

259+ fnTy [] ret = forget ret

260+ fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi xt) (fnTy xs ret)

261+

262+ elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)

263+ elabIArg _ = return () -- already done, just a name

264+

237 elab' (ina, g) tm@(PApp fc (PRef _ f) args')

265 elab' (ina, g) tm@(PApp fc (PRef _ f) args')

238 = do let args = {- case lookupCtxt f (inblock info) of

266 = do let args = {- case lookupCtxt f (inblock info) of

239 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

267 Just ps -> (map (pexp . (PRef fc)) ps ++ args')