
  0 | module TTImp.Interactive.MakeLemma
  1 | 
  2 | import Core.Env
  3 | import Core.Metadata
  4 | 
  5 | import Idris.Syntax
  6 | 
  7 | import TTImp.Unelab
  8 | import TTImp.TTImp
  9 | import TTImp.TTImp.Functor
 10 | import TTImp.Utils
 11 | 
 12 | %default covering
 13 | 
 14 | used : RigCount -> Bool
 15 | used = not . isErased
 16 | 
 17 | hiddenName : Name -> Bool
 18 | hiddenName (MN "_" _) = True
 19 | hiddenName _ = False
 20 | 
 21 | -- True if the variable appears guarded by a constructor in the term
 22 | bindable : Nat -> Term vars -> Bool
 23 | bindable p tm
 24 |     = case getFnArgs tm of
 25 |            (Ref _ (TyCon {}) n, args) => any (bindable p) args
 26 |            (Ref _ (DataCon {}) _, args) => any (bindable p) args
 27 |            (TDelayed _ _ t, args) => any (bindable p) (t :: args)
 28 |            (TDelay _ _ _ t, args) => any (bindable p) (t :: args)
 29 |            (TForce _ _ t, args) => any (bindable p) (t :: args)
 30 |            (Local _ _ p' _, []) => p == p'
 31 |            _ => False
 32 | 
 33 | bindableArg : Nat -> Term vars -> Bool
 34 | bindableArg p (Bind _ _ (Pi _ _ _ ty) sc)
 35 |    = bindable p ty || bindableArg (1 + p) sc
 36 | bindableArg p _ = False
 37 | 
 38 | getArgs : {vars : _} ->
 39 |           {auto c : Ref Ctxt Defs} ->
 40 |           {auto s : Ref Syn SyntaxInfo} ->
 41 |           Env Term vars -> Nat -> Term vars ->
 42 |           Core (List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp), RawImp)
 43 | getArgs {vars} env (S k) (Bind _ x b@(Pi _ c _ ty) sc)
 44 |     = do defs <- get Ctxt
 45 |          ty' <- map (map rawName) $ unelab env !(normalise defs env ty)
 46 |          let x' = UN $ Basic !(uniqueBasicName defs (toList $ map nameRoot vars) (nameRoot x))
 47 |          (sc', ty) <- getArgs (b :: env) k (compat {n = x'} sc)
 48 |          -- Don't need to use the name if it's not used in the scope type
 49 |          let mn = if c == top
 50 |                        then case shrink sc (Drop Refl) of
 51 |                                     Nothing => Just x'
 52 |                                     _ => Nothing
 53 |                        else Just x'
 54 |          let p' = if used c && not (bindableArg 0 sc) && not (hiddenName x)
 55 |                      then Explicit
 56 |                      else Implicit
 57 |          pure ((x, mn, p', c, ty') :: sc', ty)
 58 | getArgs env k ty
 59 |       = do defs <- get Ctxt
 60 |            ty' <- map (map rawName) $ unelab env !(normalise defs env ty)
 61 |            pure ([], ty')
 62 | 
 63 | mkType : FC -> List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp) ->
 64 |          RawImp -> RawImp
 65 | mkType loc [] ret = ret
 66 | mkType loc ((_, n, p, c, ty) :: rest) ret
 67 |     = IPi loc c p n ty (mkType loc rest ret)
 68 | 
 69 | mkApp : FC -> Name ->
 70 |         List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp) -> RawImp
 71 | mkApp loc n args
 72 |     = apply (IVar loc n) (mapMaybe getArg args)
 73 |   where
 74 |     getArg : (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp) ->
 75 |              Maybe RawImp
 76 |     getArg (x, _, Explicit, _, _) = Just (IVar loc x)
 77 |     getArg _ = Nothing
 78 | 
 79 | -- Return a top level type for the lemma, and an expression which applies
 80 | -- the lemma to solve a hole with 'locs' arguments
 81 | export
 82 | makeLemma : {auto c : Ref Ctxt Defs} ->
 83 |             {auto s : Ref Syn SyntaxInfo} ->
 84 |             FC -> Name -> Nat -> ClosedTerm ->
 85 |             Core (RawImp, RawImp)
 86 | makeLemma loc n nlocs ty
 87 |     = do defs <- get Ctxt
 88 |          (args, ret) <- getArgs Env.empty nlocs !(normalise defs Env.empty ty)
 89 |          pure (mkType loc args ret, mkApp loc n args)
 90 |