f833918 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

(Experimental) Create deferred definitions by application

commitf8339180bc3d3506f3199c14392a64d4aef799a7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 28 Nov 2012, 18:06 (14 years ago) parente23c029

5 files changed+76−25

compare with master

unifiedsplit

src/Core/Elaborate.hs+4 src/Core/ProofState.hs+37−23 src/Idris/AbsSyntax.hs+4 src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabTerm.hs+30−2

src/Core/Elaborate.hs+4

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

266266defer n = do n' <- unique_hole n

267267 processTactic' (Defer n')

268268

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

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

271+ processTactic' (DeferType n' ty ns)

272+

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

270274instanceArg n = processTactic' (Instance n)

271275

src/Core/ProofState.hs+37−23

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

6565 | PatBind Name

6666 | Focus Name

6767 | Defer Name

68+ | DeferType Name Raw [Name]

6869 | Instance Name

6970 | MoveLast Name

7071 | ProofState

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

298299

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

300301

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+

301314regret :: RunTactic

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

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

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

577590 let (h, _) = unified ps

578591 tactic (Just h) solve_unified

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

580− where mktac Attack = attack

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

582− mktac (Exact r) = exact r

583− mktac (Fill r) = fill r

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

585− mktac CompleteFill = complete_fill

586− mktac Regret = regret

587− mktac Solve = solve

588− mktac (StartUnify n) = start_unify n

589− mktac Compute = compute

590− mktac (Intro n) = intro n

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

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

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

594− mktac (Rewrite t) = rewrite t

595− mktac (PatVar n) = patvar n

596− mktac (PatBind n) = patbind n

597− mktac (CheckIn r) = check_in r

598− mktac (EvalIn r) = eval_in r

599− mktac (Focus n) = focus n

600− mktac (Defer n) = defer n

601− mktac (Instance n) = instanceArg n

602− mktac (MoveLast n) = movelast n

593+ where mktac Attack = attack

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

595+ mktac (Exact r) = exact r

596+ mktac (Fill r) = fill r

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

598+ mktac CompleteFill = complete_fill

599+ mktac Regret = regret

600+ mktac Solve = solve

601+ mktac (StartUnify n) = start_unify n

602+ mktac Compute = compute

603+ mktac (Intro n) = intro n

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

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

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

607+ mktac (Rewrite t) = rewrite t

608+ mktac (PatVar n) = patvar n

609+ mktac (PatBind n) = patbind n

610+ mktac (CheckIn r) = check_in r

611+ mktac (EvalIn r) = eval_in r

612+ mktac (Focus n) = focus n

613+ mktac (Defer n) = defer n

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

615+ mktac (Instance n) = instanceArg n

616+ mktac (MoveLast n) = movelast n

603617

src/Idris/AbsSyntax.hs+4

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

776776 PDPair fc l' t' r'

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

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

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

780783 | not (f `elem` env)

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

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

10001003 _ -> LeftErr (a, b)

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

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

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

10031007 match (PQuote _) _ = return []

10041008 match (PProof _) _ = return []

10051009 match (PTactics _) _ = return []

src/Idris/AbsSyntaxTree.hs+1

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

894894showImp impl tm = se 10 tm where

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

896896 se p (PPatvar fc n) = show n

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

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

898899 else showbasic n

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

src/Idris/ElabTerm.hs+30−2

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

232232 elabE (True, a) val

233233 elabE (True, a) sc

234234 solve

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

236− = fail "Not implemented"

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

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+

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

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

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