2Module : Idris.Elab.Clause
3Description : Code to elaborate clauses.
6Maintainer : The Idris Community.
8{-# LANGUAGE PatternGuards #-}
9module Idris.Elab.Clause where
13import Idris.Core.CaseTree
14import Idris.Core.Elaborate hiding (Tactic(..))
15import Idris.Core.Evaluate
17import Idris.Core.Typecheck
21import Idris.DeepSeq ()
22import Idris.Delaborate
23import Idris.Docstrings hiding (Unchecked)
24import Idris.Elab.AsPat
26import Idris.Elab.Transform
28import Idris.Elab.Utils
31import Idris.Output (iWarn, pshow, sendHighlighting)
32import Idris.PartialEval
33import Idris.Termination
34import Idris.Transforms
36import Util.Pretty hiding ((<$>))
38import Prelude hiding (id, (.))
40import Control.Category
43import qualified Control.Monad.State.Lazy as LState
44import Control.Monad.State.Strict as State
47import qualified Data.Set as S
52-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
53-- top-level definition.
54elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
55elabClauses info' fc opts n_in cs =
56 do let n = liftname info n_in
57 info = info' { elabFC = Just fc }
60 optimise <- getOptimise
61 let petrans = PETransform `elem` optimise
62 inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)
64 -- Check n actually exists, with no definition yet
65 let tys = lookupTy n ctxt
66 let reflect = Reflection `elem` opts
67 when (reflect && FCReflection `notElem` idris_language_extensions ist) $
68 ierror $ At fc (Msg "You must turn on the FirstClassReflection extension to use %reflection")
70 unless (length tys > 1) $ do
72 [] -> -- TODO: turn into a CAF if there's no arguments
73 -- question: CAFs in where blocks?
74 tclift $ tfail $ At fc (NoTypeDecl n)
76 let atys_in = map snd (getArgTys (normalise ctxt [] fty))
77 let atys = map (\x -> (x, isCanonical x ctxt)) atys_in
78 cs_elab <- mapM (elabClause info opts)
81 -- pats_raw is the basic type checked version, no PE or forcing
82 let optinfo = idris_optimisation ist
83 let (pats_in, cs_full) = unzip cs_elab
84 let pats_raw = map (simple_lhs ctxt) pats_in
85 -- We'll apply forcing to the left hand side here, so that we don't
86 -- do any unnecessary case splits
87 let pats_forced = map (force_lhs optinfo) pats_raw
89 logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw
90 logElab 5 $ "Forced patterns:\n" ++ show pats_forced
94 -- just ensure that the structure exists
95 fmodifyState (ist_optimisation n) id
100 -- Don't apply rules if this is a partial evaluation definition,
101 -- or we'll make something that just runs itself!
102 let tpats = case specNames opts of
103 Nothing -> transformPats ist pats_in
106 -- If the definition is specialisable, this reduces the
108 pe_tm <- doPartialEval ist tpats
110 let pats_pe = if petrans
111 then map (force_lhs optinfo . simple_lhs ctxt) pe_tm
114 let tcase = opt_typecase (idris_options ist)
116 -- Look for 'static' names and generate new specialised
117 -- definitions for them, as well as generating rewrite rules
118 -- for partially evaluated definitions
119 newrules <- if petrans
120 then mapM (\ e -> case e of
122 Right (l, r) -> elabPE info fc n r) pats_pe
125 -- Redo transforms with the newly generated transformations, so
126 -- that the specialised application we've just made gets
127 -- used in place of the general one
129 let pats_transformed = if petrans
130 then transformPats ist pats_pe
133 -- Summary of what's about to happen: Definitions go:
135 -- pats_in -> pats -> pdef -> pdef'
137 -- addCaseDef builds case trees from <pdef> and <pdef'>
139 -- pdef is the compile-time pattern definition, after forcing
140 -- optimisation applied to LHS
141 let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $
142 map debind pats_forced
143 -- pdef_pe is the one which will get further optimised
144 -- for run-time, with no forcing optimisation of the LHS because
145 -- the affects erasure. Also, it's partially evaluated
146 let pdef_pe = map debind pats_transformed
148 logElab 5 $ "Initial typechecked patterns:\n" ++ show pats_raw
149 logElab 5 $ "Initial typechecked pattern def:\n" ++ show pdef
151 -- NOTE: Need to store original definition so that proofs which
152 -- rely on its structure aren't affected by any changes to the
153 -- inliner. Just use the inlined version to generate pdef' and to
154 -- help with later inlinings.
157 numArgs <- tclift $ sameLength pdef
159 case specNames opts of
161 do logElab 3 $ "Partially evaluated:\n" ++ show pats_pe
163 logElab 3 $ "Transformed:\n" ++ show pats_transformed
165 erInfo <- getErasureInfo <$> getIState
166 tree@(CaseDef scargs sc _) <- tclift $
167 simpleCase tcase (UnmatchedCase "Error") reflect CompileTime fc inacc atys pdef erInfo
170 if cov && not (hasDefault pats_raw)
171 then do -- Generate clauses from the given possible cases
172 missing <- genClauses fc n
173 (map (\ (ns,tm,_) -> (ns, tm)) pdef)
175 -- missing <- genMissing n scargs sc
176 missing' <- checkPossibles info fc True n missing
177 -- Filter out the ones which match one of the
178 -- given cases (including impossible ones)
179 logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++
180 showSep "\n" (map showTmImpls missing') ++
182 showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))
183 -- filter out anything in missing' which is
184 -- matched by any of clhs. This might happen since
185 -- unification may force a variable to take a
186 -- particular form, rather than force a case
188 return missing' -- (filter (noMatch ist clhs) missing')
190 let pcover = null pmissing
192 -- pdef' is the version that gets compiled for run-time,
193 -- so we start from the partially evaluated version
194 pdef_in' <- applyOpts $ map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) pdef_pe
196 let pdef' = map (simple_rt ctxt) pdef_in'
198 logElab 5 $ "After data structure transformations:\n" ++ show pdef'
201 let tot | pcover = Unchecked -- finish later
202 | AssertTotal `elem` opts = Total []
203 | PEGenerated `elem` opts = Generated
204 | otherwise = Partial NotCovering -- already know it's not total
207 CaseDef _ _ [] -> return ()
208 CaseDef _ _ xs -> mapM_ (\x ->
209 iWarn fc $ text "Unreachable case:" </> text (show (delab ist x))
211 let knowncovering = (pcover && cov) || AssertTotal `elem` opts
212 let defaultcase = if knowncovering
214 else UnmatchedCase $ "*** " ++
216 ":unmatched case in " ++ show n ++
219 tree' <- tclift $ simpleCase tcase defaultcase reflect
220 RunTime fc inacc atys pdef' erInfo
221 logElab 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree
222 logElab 3 $ "Optimised: " ++ show tree'
225 putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)
226 (idris_patdefs ist) })
227 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)
229 case lookupTyExact n ctxt of
231 do ctxt' <- do ctxt <- getContext
233 addCasedef n erInfo caseInfo
236 (AssertTotal `elem` opts)
247 when (not reflect && PEGenerated `notElem` opts) $
249 defer_totcheck (fc, n)
250 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
253 case lookupDef n ctxt of
254 (CaseOp _ _ _ _ _ cd : _) ->
255 let (scargs, sc) = cases_compiletime cd in
256 do let calls = map fst $ findCalls sc scargs
257 -- let scg = buildSCG i sc scargs
258 -- add SCG later, when checking totality
259 logElab 2 $ "Called names: " ++ show calls
260 -- if the definition is public, make sure
261 -- it only uses public names
262 nvis <- getFromHideList n
264 Just Public -> mapM_ (checkVisibility fc n Public Public) calls
267 let rig = if linearArg (whnfArgs ctxt [] ty)
270 updateContext (setRigCount n (minRig ctxt rig calls))
274 -- addIBC (IBCTotal n tot)
276 -- Check it's covering, if 'covering' option is used. Chase
277 -- all called functions, and fail if any of them are also
278 -- 'Partial NotCovering'
279 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
280 -- Add the 'AllGuarded' flag if it's guaranteed that every
281 -- 'Inf' argument will be guarded by constructors in the result
282 -- (allows productivity check to go under this function)
284 -- If this has %static arguments, cache the names of functions
285 -- it calls for partial evaluation later
287 let statics = case lookupCtxtExact n (idris_statics ist) of
290 when (or statics) $ do getAllNames n
294 checkUndefined n ctxt = case lookupDef n ctxt of
296 [TyDecl _ _] -> return ()
297 _ -> tclift $ tfail (At fc (AlreadyDefined n))
299 debind (Right (x, y)) = let (vs, x') = depat [] x
300 (_, y') = depat [] y in
302 debind (Left x) = let (vs, x') = depat [] x in
305 depat acc (Bind n (PVar rig t) sc) = depat ((n, t) : acc) (instantiate (P Bound n t) sc)
306 depat acc x = (acc, x)
309 getPVs (Bind x (PVar rig _) tm) = let (vs, tm') = getPVs tm
313 isPatVar vs (P Bound n _) = n `elem` vs
316 hasDefault cs | (Right (lhs, rhs) : _) <- reverse cs
317 , (pvs, tm) <- getPVs (explicitNames lhs)
318 , (f, args) <- unApply tm = all (isPatVar pvs) args
323 -- Simplify the left hand side of a definition, to remove any lets
324 -- that may have arisen during elaboration
325 simple_lhs ctxt (Right (x, y))
326 = Right (Idris.Core.Evaluate.simplify ctxt [] x, y)
327 simple_lhs ctxt t = t
329 force_lhs opts (Right (x, y)) = Right (forceWith opts x, y)
332 simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p
333 (rt_simplify ctxt [] y)))
335 specNames [] = Nothing
336 specNames (Specialise ns : _) = Just ns
337 specNames (_ : xs) = specNames xs
339 sameLength ((_, x, _) : xs)
340 = do l <- sameLength xs
341 let (_, as) = unApply x
342 if (null xs || l == length as) then return (length as)
343 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))
344 sameLength [] = return 0
346 -- Partially evaluate, if the definition is marked as specialisable
347 doPartialEval ist pats =
348 case specNames opts of
349 Nothing -> return pats
350 Just ns -> case partial_eval (tt_ctxt ist) ns pats of
352 Nothing -> ierror (At fc (Msg "No specialisation achieved"))
354 minRig :: Context -> RigCount -> [Name] -> RigCount
355 minRig c minr [] = minr
356 minRig c minr (r : rs) = case lookupRigCountExact r c of
357 Nothing -> minRig c minr rs
358 Just rc -> minRig c (min minr rc) rs
360forceWith :: Ctxt OptInfo -> Term -> Term
361forceWith opts lhs = -- trace (show lhs ++ "\n==>\n" ++ show (force lhs) ++ "\n----") $
364 -- If there's forced arguments, erase them
366 | (fn@(P _ c _), args) <- unApply ap,
367 Just copt <- lookupCtxtExact c opts
368 = let args' = eraseArg 0 (forceable copt) args in
369 mkApp fn (map force args')
371 = App t (force f) (force a)
372 -- We might have pat bindings, so go under them
373 force (Bind n b sc) = Bind n b (force sc)
374 -- Everything else, leave it alone
377 eraseArg i fs (n : ns) | i `elem` fs = Erased : eraseArg (i + 1) fs ns
378 | otherwise = n : eraseArg (i + 1) fs ns
382-- | Find 'static' applications in a term and partially evaluate them.
383-- Return any new transformation rules
384elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]
385-- Don't go deeper than 5 nested partially evaluated definitions in one go
386-- (make this configurable? It's a good limit for most cases, certainly for
387-- interfaces and polymorphic definitions, but maybe not for DSLs and
388-- interpreters in complicated cases.
389-- Possibly only worry about the limit if we've specialised the same function
390-- a number of times in one go.)
391elabPE info fc caller r | pe_depth info > 5 = return []
392elabPE info fc caller r =
394 let sa = filter (\ap -> fst ap /= caller) $ getSpecApps ist [] r
395 rules <- mapM mkSpecialised sa
396 return $ concat rules
398 -- Make a specialised version of the application, and
399 -- add a PTerm level transformation rule, which is basically the
400 -- new definition in reverse (before specialising it).
401 -- RHS => LHS where implicit arguments are left blank in the
404 -- Transformation rules are applied after every PClause elaboration
406 mkSpecialised :: (Name, [(PEArgType, Term)]) -> Idris [(Term, Term)]
407 mkSpecialised specapp_in = do
410 (specTy, specapp) <- getSpecTy ist specapp_in
411 let (n, newnm, specdecl) = getSpecClause ist specapp specTy
412 let lhs = pe_app specdecl
413 let rhs = pe_def specdecl
414 let undef = case lookupDefExact newnm ctxt of
417 logElab 5 $ show (newnm, undef, map (concreteArg ist) (snd specapp))
419 (if (undef && all (concreteArg ist) (snd specapp)) then do
420 cgns <- getAllNames n
421 -- on the RHS of the new definition, we should reduce
422 -- everything that's not itself static (because we'll
423 -- want to be a PE version of those next)
424 let cgns' = filter (\x -> x /= n &&
425 notStatic ist x) cgns
426 -- set small reduction limit on partial/productive things
427 let maxred = case lookupTotal n ctxt of
431 let specnames = mapMaybe (specName (pe_simple specdecl))
433 descs <- mapM getStaticsFrom (map fst specnames)
435 let opts = [Specialise ((if pe_simple specdecl
436 then map (\x -> (x, Nothing)) cgns'
438 (n, Just maxred) : specnames ++
440 logElab 3 $ "Specialising application: " ++ show specapp
441 ++ "\n in \n" ++ show caller ++
442 "\n with \n" ++ show opts
443 ++ "\nCalling: " ++ show cgns
444 logElab 3 $ "New name: " ++ show newnm
445 logElab 3 $ "PE definition type : " ++ (show specTy)
447 logElab 2 $ "PE definition " ++ show newnm ++ ":\n" ++
449 (map (\ (lhs, rhs) ->
450 (showTmImpls lhs ++ " = " ++
451 showTmImpls rhs)) (pe_clauses specdecl))
453 logElab 5 $ show n ++ " transformation rule: " ++
454 showTmImpls rhs ++ " ==> " ++ showTmImpls lhs
456 elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy
457 let def = map (\(lhs, rhs) ->
458 let lhs' = mapPT hiddenToPH $ stripUnmatchable ist lhs in
459 PClause fc newnm lhs' [] rhs [])
460 (pe_clauses specdecl)
461 trans <- elabTransform info fc False rhs lhs
462 elabClauses (info {pe_depth = pe_depth info + 1}) fc
463 (PEGenerated:opts) newnm def
466 -- if it doesn't work, just don't specialise. Could happen for lots
467 -- of valid reasons (e.g. local variables in scope which can't be
469 (\e -> do logElab 5 $ "Couldn't specialise: " ++ (pshow ist e)
472 hiddenToPH (PHidden _) = Placeholder
475 specName simpl (ImplicitS _, tm)
476 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
477 specName simpl (ExplicitS, tm)
478 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
479 specName simpl (ConstraintS, tm)
480 | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
481 specName simpl _ = Nothing
483 -- get the descendants of the name 'n' which are marked %static
484 -- Marking a function %static essentially means it's used to construct
485 -- programs, so should be evaluated by the partial evaluator
486 getStaticsFrom :: Name -> Idris [(Name, Maybe Int)]
487 getStaticsFrom n = do ns <- getAllNames n
489 let statics = filter (staticFn i) ns
490 return (map (\n -> (n, Nothing)) statics)
492 staticFn :: IState -> Name -> Bool
493 staticFn i n = case lookupCtxt n (idris_flags i) of
494 [opts] -> elem StaticFn opts
497 notStatic ist n = case lookupCtxtExact n (idris_statics ist) of
501 concreteArg ist (ImplicitS _, tm) = concreteTm ist tm
502 concreteArg ist (ExplicitS, tm) = concreteTm ist tm
503 concreteArg ist _ = True
505 concreteTm ist tm | (P _ n _, _) <- unApply tm =
506 case lookupTy n (tt_ctxt ist) of
509 concreteTm ist (Constant _) = True
510 concreteTm ist (Bind n (Lam _ _) sc) = True
511 concreteTm ist (Bind n (Pi _ _ _ _) sc) = True
512 concreteTm ist (Bind n (Let _ _ _) sc) = concreteTm ist sc
513 concreteTm ist _ = False
515 -- get the type of a specialised application
516 getSpecTy ist (n, args)
517 = case lookupTy n (tt_ctxt ist) of
518 [ty] -> let (specty_in, args') = specType args (explicitNames ty)
519 specty = normalise (tt_ctxt ist) [] (finalise specty_in)
520 t = mkPE_TyDecl ist args' (explicitNames specty) in
521 return (t, (n, args'))
522-- (normalise (tt_ctxt ist) [] (specType args ty))
523 _ -> ifail $ "Ambiguous name " ++ show n ++ " (getSpecTy)"
525 -- get the clause of a specialised application
526 getSpecClause ist (n, args) specTy
527 = let newnm = sUN ("PE_" ++ show (nsroot n) ++ "_" ++
528 qhash 5381 (showSep "_" (map showArg args))) in
529 -- UN (show n ++ show (map snd args)) in
530 (n, newnm, mkPE_TermDecl ist newnm n specTy args)
531 where showArg (ExplicitS, n) = qshow n
532 showArg (ImplicitS _, n) = qshow n
535 qshow (Bind _ _ _) = "fn"
536 qshow (App _ f a) = qshow f ++ qshow a
537 qshow (P _ n _) = show n
538 qshow (Constant c) = show c
541 -- Simple but effective string hashing...
542 -- Keep it to 32 bits for readability/debuggability
543 qhash :: Word64 -> String -> String
544 qhash hash [] = showHex (abs hash `mod` 0xffffffff) ""
545 qhash hash (x:xs) = qhash (hash * 33 + fromIntegral(fromEnum x)) xs
547-- | Checks if the clause is a possible left hand side.
548-- NOTE: A lot of this is repeated for reflected definitions in Idris.Elab.Term
549-- One day, these should be merged, but until then remember that if you edit
550-- this you might need to edit the other version...
551checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)
552checkPossible info fc tcgen fname lhs_in
553 = do ctxt <- getContext
555 let lhs = addImplPat i lhs_in
556 logElab 10 $ "Trying missing case: " ++ showTmImpls lhs
557 -- if the LHS type checks, it is possible
558 case elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
559 (erun fc (buildTC i info EImpossible [] fname
562 OK (ElabResult lhs' _ _ ctxt' newDecls highlights newGName, _) ->
564 processTacticDecls info newDecls
565 sendHighlighting highlights
566 updateIState $ \i -> i { idris_name = newGName }
567 let lhs_tm = normalise ctxt [] (orderPats (getInferTerm lhs'))
568 let emptyPat = hasEmptyPat ctxt (idris_datatypes i) lhs_tm
570 do logElab 10 $ "Empty type in pattern "
573 case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of
575 do logElab 10 $ "Valid " ++ show tm ++ "\n"
576 ++ " from " ++ show lhs
577 return (Just (delab' i tm True True))
578 err -> do logElab 10 $ "Conversion failure"
580 -- if it's a recoverable error, the case may become possible
581 Error err -> do logLvl 10 $ "Impossible case " ++ (pshow i err)
582 ++ "\n" ++ show (recoverableCoverage ctxt err,
583 validCoverageCase ctxt err)
584 -- tcgen means that it was generated by genClauses,
585 -- so only looking for an error. Otherwise, it
586 -- needs to be the right kind of error (a type mismatch
587 -- in the same family).
588 if tcgen then returnTm i err (recoverableCoverage ctxt err)
589 else returnTm i err (validCoverageCase ctxt err ||
590 recoverableCoverage ctxt err)
591 where returnTm i err True = do logLvl 10 $ "Possibly resolvable error on " ++
592 pshow i (fmap (normalise (tt_ctxt i) []) err)
593 ++ " on " ++ showTmImpls lhs_in
595 returnTm i err False = return $ Nothing
597-- Filter out the terms which are not well type left hand sides. Whenever we
598-- eliminate one, also eliminate later ones which match it without checking,
599-- because they're obviously going to have the same result
600checkPossibles :: ElabInfo -> FC -> Bool -> Name -> [PTerm] -> Idris [PTerm]
601checkPossibles info fc tcgen fname (lhs : rest)
602 = do ok <- checkPossible info fc tcgen fname lhs
604 -- Hypothesis: any we can remove will be within the next few, because
605 -- leftmost patterns tend to change less
606 -- Since the match could take a while if there's a lot of cases to
607 -- check, just remove from the next batch
608 let rest' = filter (\x -> not (qmatch x lhs)) (take 200 rest) ++ drop 200 rest
609 restpos <- checkPossibles info fc tcgen fname rest'
611 Nothing -> return restpos
612 Just lhstm -> return (lhstm : restpos)
614 qmatch _ Placeholder = True
615 qmatch (PApp _ f args) (PApp _ f' args')
616 | length args == length args'
617 = qmatch f f' && and (zipWith qmatch (map getTm args)
619 qmatch (PRef _ _ n) (PRef _ _ n') = n == n'
620 qmatch (PPair _ _ _ l r) (PPair _ _ _ l' r') = qmatch l l' && qmatch r r'
621 qmatch (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r')
622 = qmatch l l' && qmatch t t' && qmatch r r'
624checkPossibles _ _ _ _ [] = return []
626findUnique :: Context -> Env -> Term -> [Name]
627findUnique ctxt env (Bind n b sc)
628 = let rawTy = forgetEnv (map fstEnv env) (binderTy b)
629 uniq = case check ctxt env rawTy of
630 OK (_, UType UniqueType) -> True
631 OK (_, UType NullType) -> True
632 OK (_, UType AllTypes) -> True
634 if uniq then n : findUnique ctxt ((n, RigW, b) : env) sc
635 else findUnique ctxt ((n, RigW, b) : env) sc
638-- | Return the elaborated LHS/RHS, and the original LHS with implicits added
639elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
640 Idris (Either Term (Term, Term), PTerm)
641elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
642 = do let tcgen = Dictionary `elem` opts
644 let lhs = addImpl [] i lhs_in
645 b <- checkPossible info fc tcgen fname lhs_in
647 Just _ -> tclift $ tfail (At fc
648 (Msg $ show lhs_in ++ " is a valid case"))
649 Nothing -> do ptm <- mkPatTm lhs_in
650 logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++
652 return (Left ptm, lhs)
653elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock_as)
654 = do push_estack fname False
656 let (lhs_in, rhs_in, whereblock) = desugarAs lhs_in_as rhs_in_as whereblock_as
658 -- Build the LHS as an "Infer", and pull out its type and
661 inf <- isTyInferred fname
663 -- Check if we have extra "with" patterns
664 when (not $ null withs) $
665 ierror (At (fromMaybe NoFC $ highestFC lhs_in_as)
666 (Elaborating "left hand side of " fname Nothing
667 (Msg $ if isOutsideWith lhs_in
668 then "unexpected patterns outside of \"with\" block"
669 else "unexpected extra \"with\" patterns")))
671 -- get the parameters first, to pass through to any where block
672 let fn_ty = case lookupTy fname ctxt of
674 _ -> error "Can't happen (elabClause function type)"
675 let fn_is = case lookupCtxt fname (idris_implicits i) of
678 let norm_ty = normalise ctxt [] fn_ty
679 let params = getParamsInType i [] fn_is norm_ty
680 let tcparams = getTCParamsInType i [] fn_is norm_ty
682 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $
683 propagateParams i params norm_ty (allNamesIn lhs_in) (addImplPat i lhs_in)
685-- let lhs = mkLHSapp $
686-- propagateParams i params fn_ty (addImplPat i lhs_in)
687 logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))
688 logElab 5 ("LHS: " ++ show opts ++ "\n" ++ show fc ++ " " ++ showTmImpls lhs)
689 logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ showTmImpls lhs_in ++
690 "\n" ++ show (fn_ty, fn_is))
692 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-
693 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
694 (do res <- errAt "left hand side of " fname Nothing
695 (erun (fromMaybe NoFC $ highestFC lhs_in_as)
696 (buildTC i info ELHS opts fname
701 return (res, probs, inj))
703 processTacticDecls info newDecls
704 sendHighlighting highlights
705 updateIState $ \i -> i { idris_name = newGName }
707 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)
709 let lhs_tm = orderPats (getInferTerm lhs')
710 let lhs_ty = getInferType lhs'
711 let static_names = getStaticNames i lhs_tm
713 logElab 3 ("Elaborated: " ++ show lhs_tm)
714 logElab 3 ("Elaborated type: " ++ show lhs_ty)
715 logElab 5 ("Injective: " ++ show fname ++ " " ++ show inj)
717 -- If we're inferring metavariables in the type, don't recheck,
718 -- because we're only doing this to try to work out those metavariables
720 (clhs_c, clhsty) <- if not inf
721 then recheckC_borrowing False (PEGenerated `notElem` opts)
722 [] (constraintNS info) fc id [] lhs_tm
723 else return (lhs_tm, lhs_ty)
724 let clhs = normalise ctxt [] clhs_c
725 -- These are the names we're not allowed to use on the RHS, because
726 -- they're UniqueTypes and borrowed from another function.
727 let borrowed = borrowedNames [] clhs
729 logElab 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))
733 addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?
734 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
736 logElab 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
737 -- Elaborate where block
742 let decls = nub (concatMap declared whereblock)
743 let defs = nub (decls ++ concatMap defined whereblock)
744 let newargs_all = pvars ist lhs_tm
746 -- Unique arguments must be passed to the where block explicitly
747 -- (since we can't control "usage" easlily otherwise). Remove them
749 let uniqargs = findUnique ctxt [] lhs_tm
750 let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all
752 let winfo = (pinfo info newargs defs windex) { elabFC = Just fc }
753 let wb = map (mkStatic static_names) $
754 map (expandImplementationScope ist decorate newargs defs) $
755 map (expandParamsD False ist decorate newargs defs) whereblock
757 -- Split the where block into declarations with a type, and those
759 -- Elaborate those with a type *before* RHS, those without *after*
760 let (wbefore, wafter) = sepBlocks wb
762 logElab 5 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
763 mapM_ (rec_elabDecl info EAll winfo) wbefore
764 -- Now build the RHS, using the type of the LHS as the goal.
765 i <- getIState -- new implicits from where block
766 logElab 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
767 let rhs = rhs_trans info $
768 addImplBoundInf i (map fst newargs_all) (defs \\ decls)
769 (expandParams decorate newargs defs (defs \\ decls) rhs_in)
770 logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs
771 ctxt <- getContext -- new context with where block added
772 logElab 5 "STARTING CHECK"
773 ((rhsElab, defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-
774 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState
775 (do pbinds ist lhs_tm
776 -- proof search can use explicitly written names
777 mapM_ addPSname (allNamesIn lhs_in)
779 traceWhen ulog ("Setting injective: " ++ show (nub (tcparams ++ inj))) $
780 mapM_ setinj (nub (tcparams ++ inj))
782 (ElabResult _ _ is ctxt' newDecls highlights newGName) <-
783 errAt "right hand side of " fname (Just clhsty)
784 (erun fc (build i winfo ERHS opts fname rhs))
785 errAt "right hand side of " fname (Just clhsty)
786 (erun fc $ psolve lhs_tm)
789 let (tm, ds) = runState (collectDeferred (Just fname)
790 (map fst $ case_decls aux) ctxt tt) []
793 return (tm, ds, hs, is, probs, ctxt', newDecls, highlights, newGName))
795 processTacticDecls info newDecls
796 sendHighlighting highlights
797 updateIState $ \i -> i { idris_name = newGName }
799 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)
801 logElab 3 "DONE CHECK"
802 logElab 3 $ "---> " ++ show rhsElab
807 when (not (null defer)) $ logElab 2 $ "DEFERRED " ++
808 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
810 -- If there's holes, set the metavariables as undefinable
811 def' <- checkDef info fc (\n -> Elaborating "deferred type of " n Nothing) (null holes) defer
812 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, null holes))) def'
815 mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
817 when (not (null def')) $ do
818 mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')
820 -- Now the remaining deferred (i.e. no type declarations) clauses
821 -- from the where block
823 mapM_ (rec_elabDecl info EAll winfo) wafter
824 mapM_ (elabCaseBlock winfo opts) is
827 logElab 5 "Rechecking"
828 logElab 6 $ " ==> " ++ show (forget rhs')
830 (crhs, crhsty) -- if there's holes && deferred things, it's okay
831 -- but we'll need to freeze the definition and not
832 -- allow the deferred things to be definable
833 -- (this is just to allow users to inspect intermediate
835 <- if (null holes || null def') && not inf
836 then recheckC_borrowing True (PEGenerated `notElem` opts)
837 borrowed (constraintNS info) fc id [] rhs'
838 else return (rhs', clhsty)
840 logElab 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty
842 -- If there's holes, make sure this definition is frozen
843 when (not (null holes)) $ do
844 logElab 5 $ "Making " ++ show fname ++ " frozen due to " ++ show holes
845 setAccessibility fname Frozen
848 let constv = next_tvar ctxt
850 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of
851 OK (_, cs) -> when (PEGenerated `notElem` opts && not tit) $ do
853 mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)
854 logElab 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)
856 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))
858 checkInferred fc (delab' i crhs True True) rhs
859 -- if the function is declared '%error_reverse',
860 -- then we'll try running it in reverse to improve error messages
861 -- Also if the type is '%error_reverse' and the LHS is smaller than
863 let (ret_fam, _) = unApply (getRetTy crhsty)
864 rev <- case ret_fam of
866 case lookupCtxt rfamn (idris_datatypes i) of
867 [TI _ _ dopts _ _ _] ->
868 return (DataErrRev `elem` dopts &&
869 size clhs <= size crhs)
873 when (rev || ErrorReverse `elem` opts) $ do
874 addIBC (IBCErrRev (crhs, clhs))
875 addErrRev (crhs, clhs)
876 when (rev || ErrorReduce `elem` opts) $ do
877 addIBC (IBCErrReduce fname)
880 return (Right (clhs, crhs), lhs)
882 pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
884 = let newps = params info ++ ns
885 dsParams = map (\n -> (n, map fst newps)) ds
886 newb = addAlist dsParams (inblock info) in
887 info { params = newps,
889 liftname = id -- (\n -> case lookupCtxt n newb of
891 -- _ -> MN i (show n)) . l
894 -- Find the variable names which appear under a 'Ownership.Read' so that
895 -- we know they can't be used on the RHS
896 borrowedNames :: [Name] -> Term -> [Name]
897 borrowedNames env (App _ (App _ (P _ (NS (UN lend) [owner]) _) _) arg)
898 | owner == txt "Ownership" &&
899 (lend == txt "lend" || lend == txt "Read") = getVs arg
901 getVs (V i) = [env!!i]
902 getVs (App _ f a) = nub $ getVs f ++ getVs a
904 borrowedNames env (App _ f a) = nub $ borrowedNames env f ++ borrowedNames env a
905 borrowedNames env (Bind n b sc) = nub $ borrowedB b ++ borrowedNames (n:env) sc
906 where borrowedB (Let _ t v) = nub $ borrowedNames env t ++ borrowedNames env v
907 borrowedB b = borrowedNames env (binderTy b)
908 borrowedNames _ _ = []
910 mkLHSapp t@(PRef _ _ _) = PApp fc t []
914 = NS (SN (WhereN cnum fname x)) ns
916 = SN (WhereN cnum fname x)
918 sepBlocks bs = sepBlocks' [] bs where
919 sepBlocks' ns (d@(PTy _ _ _ _ _ n _ t) : bs)
920 = let (bf, af) = sepBlocks' (n : ns) bs in
922 sepBlocks' ns (d@(PClauses _ _ n _) : bs)
923 | not (n `elem` ns) = let (bf, af) = sepBlocks' ns bs in
925 sepBlocks' ns (b : bs) = let (bf, af) = sepBlocks' ns bs in
927 sepBlocks' ns [] = ([], [])
929 -- term is not within "with" block
930 isOutsideWith :: PTerm -> Bool
931 isOutsideWith (PApp _ (PRef _ _ (SN (WithN _ _))) _) = False
932 isOutsideWith _ = True
934elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
935 = do ctxt <- getContext
936 -- Build the LHS as an "Infer", and pull out its type and
939 -- get the parameters first, to pass through to any where block
940 let fn_ty = case lookupTy fname ctxt of
942 _ -> error "Can't happen (elabClause function type)"
943 let fn_is = case lookupCtxt fname (idris_implicits i) of
946 let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)
947 let lhs = stripLinear i $ stripUnmatchable i $
948 propagateParams i params fn_ty (allNamesIn lhs_in)
949 (addImplPat i lhs_in)
950 logElab 2 ("LHS: " ++ show lhs)
951 (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-
952 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
953 (errAt "left hand side of with in " fname Nothing
954 (erun (fromMaybe NoFC $ highestFC lhs_in)
955 (buildTC i info ELHS opts fname
959 processTacticDecls info newDecls
960 sendHighlighting highlights
961 updateIState $ \i -> i { idris_name = newGName }
964 let lhs_tm = orderPats (getInferTerm lhs')
965 let lhs_ty = getInferType lhs'
966 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))
967 let static_names = getStaticNames i lhs_tm
968 logElab 5 (show lhs_tm ++ "\n" ++ show static_names)
969 (clhs_c, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm
970 let clhs = normalise ctxt [] clhs_c
972 logElab 5 ("Checked " ++ show clhs)
973 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))
974 wval <- case wval_in of
975 Placeholder -> ierror $ At fc $
976 Msg "No expression for the with block to inspect.\nYou need to replace the _ with an expression."
979 addImplBound i (map fst bargs) wval_in
980 logElab 5 ("Checking " ++ showTmImpls wval)
981 -- Elaborate wval in this context
982 ((wvalElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-
983 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")
984 (bindTyArgs PVTy bargs infP) initEState
986 -- proof search can use explicitly written names
987 mapM_ addPSname (allNamesIn lhs_in)
989 -- TODO: may want where here - see winfo abpve
990 (ElabResult _ d is ctxt' newDecls highlights newGName) <- errAt "with value in " fname Nothing
991 (erun fc (build i info ERHS opts fname (infTerm wval)))
992 erun fc $ psolve lhs_tm
994 return (tt, d, is, ctxt', newDecls, highlights, newGName))
996 processTacticDecls info newDecls
997 sendHighlighting highlights
998 updateIState $ \i -> i { idris_name = newGName }
1000 def' <- checkDef info fc iderr True defer
1001 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
1003 mapM_ (elabCaseBlock info opts) is
1005 let wval' = wvalElab
1006 logElab 5 ("Checked wval " ++ show wval')
1009 (cwval, cwvalty) <- recheckC (constraintNS info) fc id [] (getInferTerm wval')
1010 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
1011 let cwvalN = explicitNames (normalise ctxt [] cwval)
1012 logElab 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
1013 -- We're going to assume the with type is not a function shortly,
1014 -- so report an error if it is (you can't match on a function anyway
1015 -- so this doesn't lose anything)
1016 case getArgTys cwvaltyN of
1018 (_:_) -> ierror $ At fc (WithFnType cwvalty)
1020 let pvars = map fst (getPBtys cwvalty)
1021 -- we need the unelaborated term to get the names it depends on
1022 -- rather than a de Bruijn index.
1023 let pdeps = usedNamesIn pvars i (delab i cwvalty)
1024 let (bargs_pre, bargs_post) = split pdeps bargs []
1026 let mpn = case pn_in of
1028 Just (n, nfc) -> Just (uniqueName n (map fst bargs))
1030 -- Highlight explicit proofs
1031 sendHighlighting $ S.fromList [(FC' fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]
1033 logElab 10 ("With type " ++ show (getRetTy cwvaltyN) ++
1034 " depends on " ++ show pdeps ++ " from " ++ show pvars)
1035 logElab 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)
1037 -- build a type declaration for the new function:
1038 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
1039 let wargval = getRetTy cwvalN
1040 let wargtype = getRetTy cwvaltyN
1041 let wargname = sMN windex "warg"
1043 logElab 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)
1044 let wtype = bindTyArgs (flip (Pi RigW Nothing) (TType (UVar [] 0))) (bargs_pre ++
1045 (wargname, wargtype) :
1046 map (abstract wargname wargval wargtype) bargs_post ++
1048 Just pn -> [(pn, mkApp (P Ref eqTy Erased)
1049 [wargtype, wargtype,
1050 P Bound wargname Erased, wargval])]
1052 (substTerm wargval (P Bound wargname wargtype) ret_ty)
1053 logElab 3 ("New function type " ++ show wtype)
1054 let wname = SN (WithN windex fname)
1056 let imps = getImps wtype -- add to implicits context
1057 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })
1058 let statics = getStatics static_names wtype
1059 logElab 5 ("Static positions " ++ show statics)
1061 putIState (i { idris_statics = addDef wname statics (idris_statics i) })
1063 addIBC (IBCDef wname)
1064 addIBC (IBCImp wname)
1065 addIBC (IBCStatic wname)
1067 def' <- checkDef info fc iderr True [(wname, (-1, Nothing, wtype, []))]
1068 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
1071 -- in the subdecls, lhs becomes:
1072 -- fname pats | wpat [rest]
1073 -- ==> fname' ps wpat [rest], match pats against toplevel for ps
1074 wb <- mapM (mkAuxC mpn wname lhs (map fst bargs_pre) (map fst bargs_post))
1076 logElab 3 ("with block " ++ show wb)
1077 setFlags wname [Inlinable]
1078 when (AssertTotal `elem` opts) $
1079 setFlags wname [Inlinable, AssertTotal]
1081 let rhstrans' = updateWithTerm i mpn wname lhs (map fst bargs_pre) (map fst (bargs_post))
1083 mapM_ (rec_elabDecl info EAll (info { rhs_trans = rhstrans' })) wb
1085 -- rhs becomes: fname' ps_pre wval ps_post Refl
1086 let rhs = PApp fc (PRef fc [] wname)
1087 (map (pexp . (PRef fc []) . fst) bargs_pre ++
1089 (map (pexp . (PRef fc []) . fst) bargs_post) ++
1092 Just _ -> [pexp (PApp NoFC (PRef NoFC [] eqCon)
1093 [ pimp (sUN "A") Placeholder False
1094 , pimp (sUN "x") Placeholder False
1096 logElab 5 ("New RHS " ++ showTmImpls rhs)
1097 ctxt <- getContext -- New context with block added
1099 ((rhsElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-
1100 tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState
1103 (ElabResult _ d is ctxt' newDecls highlights newGName) <-
1104 erun fc (build i info ERHS opts fname rhs)
1107 return (tt, d, is, ctxt', newDecls, highlights, newGName))
1110 processTacticDecls info newDecls
1111 sendHighlighting highlights
1112 updateIState $ \i -> i { idris_name = newGName }
1117 def' <- checkDef info fc iderr True defer
1118 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
1120 mapM_ (elabCaseBlock info opts) is
1121 logElab 5 ("Checked RHS " ++ show rhs')
1122 (crhs, crhsty) <- recheckC (constraintNS info) fc id [] rhs'
1123 return (Right (clhs, crhs), lhs)
1125 getImps (Bind n (Pi _ _ _ _) t) = pexp Placeholder : getImps t
1128 mkAuxC pn wname lhs ns ns' (PClauses fc o n cs)
1129 = do cs' <- mapM (mkAux pn wname lhs ns ns') cs
1130 return $ PClauses fc o wname cs'
1131 mkAuxC pn wname lhs ns ns' d = return d
1133 mkAux pn wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
1135 let tm = addImplPat i tm_in
1136 logElab 2 ("Matching " ++ showTmImpls tm ++ " against " ++
1138 case matchClause i toplhs tm of
1139 Left (a,b) -> ifail $ show fc ++ ":with clause does not match top level"
1141 do logElab 3 ("Match vars : " ++ show mvars)
1142 lhs <- updateLHS n pn wname mvars ns ns' (fullApp tm) w
1143 return $ PClause fc wname lhs ws rhs wheres
1144 mkAux pn wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval pn' withs)
1146 let tm = addImplPat i tm_in
1147 logElab 2 ("Matching " ++ showTmImpls tm ++ " against " ++
1149 withs' <- mapM (mkAuxC pn wname toplhs ns ns') withs
1150 case matchClause i toplhs tm of
1151 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")
1153 do lhs <- updateLHS n pn wname mvars ns ns' (fullApp tm) w
1154 return $ PWith fc wname lhs ws wval pn' withs'
1155 mkAux pn wname toplhs ns ns' c
1156 = ifail $ show fc ++ ":badly formed with clause"
1158 -- ns, arguments which don't depend on the with argument
1159 -- ns', arguments which do
1160 updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w
1161 = let ns = map (keepMvar (map fst mvars) fc') ns_in
1162 ns' = map (keepMvar (map fst mvars) fc') ns_in' in
1163 return $ substMatches mvars $
1164 PApp fc (PRef fc' [] wname)
1165 (map pexp ns ++ pexp w : (map pexp ns') ++
1168 Just pnm -> [pexp (PRef fc [] pnm)])
1169 updateLHS n pn wname mvars ns_in ns_in' tm w
1170 = updateLHS n pn wname mvars ns_in ns_in' (PApp fc tm []) w
1172 -- Only keep a var as a pattern variable in the with block if it's
1173 -- matched in the top level pattern
1174 keepMvar mvs fc v | v `elem` mvs = PRef fc [] v
1175 | otherwise = Placeholder
1177 updateWithTerm :: IState -> Maybe Name -> Name -> PTerm -> [Name] -> [Name] -> PTerm -> PTerm
1178 updateWithTerm ist pn wname toplhs ns_in ns_in' tm
1179 = mapPT updateApp tm
1181 currentFn fname (PAlternative _ _ as)
1182 | Just tm <- getApp as = tm
1183 where getApp (tm@(PApp _ (PRef _ _ f) _) : as)
1184 | f == fname = Just tm
1185 getApp (_ : as) = getApp as
1189 updateApp wtm@(PWithApp fcw tm_in warg) =
1190 let tm = currentFn fname tm_in in
1191 case matchClause ist toplhs tm of
1192 Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level "))
1194 let ns = map (keepMvar (map fst mvars) fcw) ns_in
1195 ns' = map (keepMvar (map fst mvars) fcw) ns_in'
1196 wty = lookupTyExact wname (tt_ctxt ist)
1197 res = substMatches mvars $
1198 PApp fcw (PRef fcw [] wname)
1199 (map pexp ns ++ pexp warg : (map pexp ns') ++
1202 Just pnm -> [pexp (PRef fc [] pnm)]) in
1204 Nothing -> res -- can't happen!
1205 Just ty -> addResolves ty res
1208 addResolves ty (PApp fc f args) = PApp fc f (addResolvesArgs fc ty args)
1209 addResolves ty tm = tm
1211 -- if an argument's type is an interface, and is otherwise to
1212 -- be inferred, then resolve it with implementation search
1213 -- This is something of a hack, because matching on the top level
1214 -- application won't find this information for us
1215 addResolvesArgs :: FC -> Term -> [PArg] -> [PArg]
1216 addResolvesArgs fc (Bind n (Pi _ _ ty _) sc) (a : args)
1217 | (P _ cn _, _) <- unApply ty,
1218 getTm a == Placeholder
1219 = case lookupCtxtExact cn (idris_interfaces ist) of
1220 Just _ -> a { getTm = PResolveTC fc } : addResolvesArgs fc sc args
1221 Nothing -> a : addResolvesArgs fc sc args
1222 addResolvesArgs fc (Bind n (Pi _ _ ty _) sc) (a : args)
1223 = a : addResolvesArgs fc sc args
1224 addResolvesArgs fc _ args = args
1226 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1229 split [] rest pre = (reverse pre, rest)
1230 split deps ((n, ty) : rest) pre
1231 | n `elem` deps = split (deps \\ [n]) rest ((n, ty) : pre)
1232 | otherwise = split deps rest ((n, ty) : pre)
1233 split deps [] pre = (reverse pre, [])
1235 abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)
1237-- | Apply a transformation to all RHSes and nested RHSs
1238mapRHS :: (PTerm -> PTerm) -> PClause -> PClause
1239mapRHS f (PClause fc n lhs args rhs ws)
1240 = PClause fc n lhs args (f rhs) (map (mapRHSdecl f) ws)
1241mapRHS f (PWith fc n lhs args warg prf ws)
1242 = PWith fc n lhs args (f warg) prf (map (mapRHSdecl f) ws)
1243mapRHS f (PClauseR fc args rhs ws)
1244 = PClauseR fc args (f rhs) (map (mapRHSdecl f) ws)
1245mapRHS f (PWithR fc args warg prf ws)
1246 = PWithR fc args (f warg) prf (map (mapRHSdecl f) ws)
1248mapRHSdecl :: (PTerm -> PTerm) -> PDecl -> PDecl
1249mapRHSdecl f (PClauses fc opt n cs)
1250 = PClauses fc opt n (map (mapRHS f) cs)
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list