36785b5 · Idris-dev · git.iko.soy

124 = do let loglvl = opt_logLevel (idris_options ist)

125 when (loglvl > 5) $ unifyLog True

126 compute -- expand type synonyms, etc

127− elabE (False, False, False) tm -- (in argument, guarded, in type)

127+ elabE (False, False, False, False) tm -- (in argument, guarded, in type, in qquote)

128 end_unify

129 when pattern -- convert remaining holes to pattern vars

130 (do update_term orderPats

158 -- and forces/delays. If you make a recursive call in elab', it is

159 -- normally correct to call elabE - the ones that don't are desugarings

160 -- typically

161− elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()

161+ elabE :: (Bool, Bool, Bool, Bool) -> PTerm -> ElabD ()

162 elabE ina t =

163 --do g <- goal

164 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $

210

211 -- "guarded" means immediately under a constructor, to help find patvars

212

213− elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)

213+ elab' :: (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a quasiquote)

214 -> PTerm -- ^ The term to elaborate

215 -> ElabD ()

216 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

239 [pimp (sMN 0 "A") Placeholder True,

240 pimp (sMN 0 "B") Placeholder False,

241 pexp l, pexp r])

242− elab' ina@(_, a, inty) (PPair fc _ l r)

242+ elab' ina@(_, a, inty, qq) (PPair fc _ l r)

243 = do hnf_compute

244 g <- goal

245 case g of

246− TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)

246+ TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)

247− [pexp l,pexp r])

247+ [pexp l,pexp r])

248− _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)

248+ _ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)

249− [pimp (sMN 0 "A") Placeholder True,

249+ [pimp (sMN 0 "A") Placeholder True,

250− pimp (sMN 0 "B") Placeholder True,

250+ pimp (sMN 0 "B") Placeholder True,

251− pexp l, pexp r])

251+ pexp l, pexp r])

252 elab' ina (PDPair fc p l@(PRef _ n) t r)

253 = case t of

254 Placeholder ->

294-- elab' (_, _, inty) (PRef fc f)

295-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

296-- = lift $ tfail (Msg "Typecase is not allowed")

297− elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)

297+ elab' (ina, guarded, inty, qq) (PRef fc n) | pattern && not (inparamBlock n)

298 = do ctxt <- get_context

299 let defined = case lookupTy n ctxt of

300 [] -> False

311 _ -> True

312 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

313 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

314− elab' ina@(_, a, inty) (PLam n Placeholder sc)

314+ elab' ina@(_, a, inty, qq) (PLam n Placeholder sc)

315 = do -- if n is a type constructor name, this makes no sense...

316 ctxt <- get_context

317 when (isTConName n ctxt) $

319 checkPiGoal n

320 attack; intro (Just n);

321 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

322− elabE (True, a, inty) sc; solve

322+ elabE (True, a, inty, qq) sc; solve

323− elab' ina@(_, a, inty) (PLam n ty sc)

323+ elab' ina@(_, a, inty, qq) (PLam n ty sc)

324 = do tyn <- getNameFrom (sMN 0 "lamty")

325 -- if n is a type constructor name, this makes no sense...

326 ctxt <- get_context

334 hs <- get_holes

335 introTy (Var tyn) (Just n)

336 focus tyn

337− elabE (True, a, True) ty

337+ elabE (True, a, True, qq) ty

338− elabE (True, a, inty) sc

338+ elabE (True, a, inty, qq) sc

339 solve

340− elab' ina@(_, a, _) (PPi _ n Placeholder sc)

340+ elab' ina@(_, a, _, qq) (PPi _ n Placeholder sc)

341− = do attack; arg n (sMN 0 "ty"); elabE (True, a, True) sc; solve

341+ = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) sc; solve

342− elab' ina@(_, a, _) (PPi _ n ty sc)

342+ elab' ina@(_, a, _, qq) (PPi _ n ty sc)

343 = do attack; tyn <- getNameFrom (sMN 0 "ty")

344 claim tyn RType

345 n' <- case n of

347 _ -> return n

348 forall n' (Var tyn)

349 focus tyn

350− elabE (True, a, True) ty

350+ elabE (True, a, True, qq) ty

351− elabE (True, a, True) sc

351+ elabE (True, a, True, qq) sc

352 solve

353− elab' ina@(_, a, inty) (PLet n ty val sc)

353+ elab' ina@(_, a, inty, qq) (PLet n ty val sc)

354 = do attack;

355 tyn <- getNameFrom (sMN 0 "letty")

356 claim tyn RType

362 Placeholder -> return ()

363 _ -> do focus tyn

364 explicit tyn

365− elabE (True, a, True) ty

365+ elabE (True, a, True, qq) ty

366 focus valn

367− elabE (True, a, True) val

367+ elabE (True, a, True, qq) val

368 env <- get_env

369− elabE (True, a, inty) sc

369+ elabE (True, a, inty, qq) sc

370 -- HACK: If the name leaks into its type, it may leak out of

371 -- scope outside, so substitute in the outer scope.

372 expandLet n (case lookup n env of

373 Just (Let t v) -> v)

374 solve

375− elab' ina@(_, a, inty) (PGoal fc r n sc) = do

375+ elab' ina@(_, a, inty, qq) (PGoal fc r n sc) = do

376 rty <- goal

377 attack

378 tyn <- getNameFrom (sMN 0 "letty")

381 claim valn (Var tyn)

382 letbind n (Var tyn) (Var valn)

383 focus valn

384− elabE (True, a, True) (PApp fc r [pexp (delab ist rty)])

384+ elabE (True, a, True, qq) (PApp fc r [pexp (delab ist rty)])

385 env <- get_env

386 computeLet n

387− elabE (True, a, inty) sc

387+ elabE (True, a, inty, qq) sc

388 solve

389-- elab' ina (PLet n Placeholder

390-- (PApp fc r [pexp (delab ist rty)]) sc)

440 _ -> lift $ tfail (NoSuchVariable fn)

441 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

442 solve

443− elab' (_, _, inty) (PApp fc (PRef _ f) args')

443+ elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')

444− | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

444+ | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

445 = lift $ tfail (Msg "Typecase is not allowed")

446 -- if f is local, just do a simple_app

447− elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)

447+ elab' (ina, g, inty, qq) tm@(PApp fc (PRef _ f) args)

448 = do env <- get_env

449 if (f `elem` map fst env && length args == 1)

450 then -- simple app, as below

451− do simple_app (elabE (ina, g, inty) (PRef fc f))

451+ do simple_app (elabE (ina, g, inty, qq) (PRef fc f))

452− (elabE (True, g, inty) (getTm (head args)))

452+ (elabE (True, g, inty, qq) (getTm (head args)))

453 (show tm)

454 solve

455 else

475 -- Sort so that the implicit tactics and alternatives go last

476 let (ns', eargs) = unzip $

477 sortBy cmpArg (zip ns args)

478− elabArgs ist (ina || not isinf, guarded, inty)

478+ elabArgs ist (ina || not isinf, guarded, inty, qq)

479 [] fc False f ns'

480 (f == sUN "Force")

481 (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg

549 setInjective (PApp _ (PRef _ n) _) = setinj n

550 setInjective _ = return ()

551

552− elab' ina@(_, a, inty) tm@(PApp fc f [arg])

552+ elab' ina@(_, a, inty, qq) tm@(PApp fc f [arg])

553 = erun fc $

554− do simple_app (elabE ina f) (elabE (True, a, inty) (getTm arg))

554+ do simple_app (elabE ina f) (elabE (True, a, inty, qq) (getTm arg))

555 (show tm)

556 solve

557 elab' ina Placeholder = do (h : hs) <- get_holes

600 elab' ina sc

601 elab' ina (PRef fc letn)

602 solve

603− elab' ina@(_, a, inty) c@(PCase fc scr opts)

603+ elab' ina@(_, a, inty, qq) c@(PCase fc scr opts)

604 = do attack

605 tyn <- getNameFrom (sMN 0 "scty")

606 claim tyn RType

609 claim valn (Var tyn)

610 letbind scvn (Var tyn) (Var valn)

611 focus valn

612− elabE (True, a, inty) scr

612+ elabE (True, a, inty, qq) scr

613 args <- get_env

614 cname <- unique_hole' True (mkCaseName fn)

615 let cname' = mkN cname

636 elab' ina (PUnifyLog t) = do unifyLog True

637 elab' ina t

638 unifyLog False

639− elab' ina (PQuasiquote t)

639+ elab' (ina, g, inty, qq) (PQuasiquote t)

640 = do -- First elaborate the unquoted subterms, replacing them with

641 -- fresh names in the quasiquoted term

642 (t, unq) <- extractUnquotes t

651 newProof (sMN 0 "q") ctxt $

652 P Ref tt Erased)

653

654− -- Re-add the unquotes, letting Idris infer the types

654+ -- Re-add the unquotes, letting Idris infer the (fictional) types

655 mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")

656 claim ty RType

657 movelast ty

674 movelast qTy

675 -- Elaborate the quasiquoted term into the hole

676 focus qTm

677− elabE ina t

677+ elabE (ina, g, inty, True) t

678 end_unify

679 -- We now have an elaborated term. Reflect it and solve the

680 -- original goal

691

692 elabUnquote (n, tm)

693 = do focus n

694− elabE ina tm

694+ elabE (ina, g, inty, False) tm

695

696

697 elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"

786

787 -- | Elaborate the arguments to a function

788 elabArgs :: IState -- ^ The current Idris state

789− -> (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)

789+ -> (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a qquote)

790 -> [Bool]

791 -> FC -- ^ Source location

792 -> Bool