
  0 | module TTImp.Interactive.Intro
  1 | 
  2 | import Core.Env
  3 | import Core.Metadata
  4 | import Core.TT.Views
  5 | import Core.Unify
  6 | 
  7 | import Idris.Desugar
  8 | import Idris.REPL.Opts
  9 | import Idris.Resugar
 10 | import Idris.Syntax
 11 | 
 12 | import TTImp.Elab
 13 | import TTImp.Elab.Check
 14 | import TTImp.TTImp
 15 | import TTImp.Unelab
 16 | import TTImp.Utils
 17 | 
 18 | import Libraries.Data.NatSet
 19 | 
 20 | %default covering
 21 | 
 22 | parameters
 23 |   {lhsCtxt : _ }
 24 |   {auto c : Ref Ctxt Defs}
 25 |   {auto s : Ref Syn SyntaxInfo}
 26 |   {auto m : Ref MD Metadata}
 27 |   {auto u : Ref UST UState}
 28 |   {auto r : Ref ROpts REPLOpts}
 29 |   (hidx : Int)
 30 |   (hole : Name)
 31 |   (env : Env Term lhsCtxt)
 32 | 
 33 |   introLam : Name -> RigCount -> Term lhsCtxt -> Core IRawImp
 34 |   introLam x rig ty = do
 35 |     ty <- unelab env ty
 36 |     defs <- get Ctxt
 37 |     new_hole <- uniqueHoleName defs [] (nameRoot hole)
 38 |     let iintrod = ILam replFC rig Explicit (Just x) ty (IHole replFC new_hole)
 39 |     pure iintrod
 40 | 
 41 |   introCon : Name -> Term lhsCtxt -> Core (List IRawImp)
 42 |   introCon n ty = do
 43 |     defs <- get Ctxt
 44 |     ust <- get UST
 45 |     Just gdef <- lookupCtxtExact n (gamma defs)
 46 |       | _ => pure []
 47 |     -- for now we only handle types with a unique constructor
 48 |     let TCon _ _ _ _ _ cs _ = definition gdef
 49 |       | _ => pure []
 50 |     let gty = gnf env ty
 51 |     ics <- for (fromMaybe [] cs) $ \ cons => do
 52 |       Just gdef <- lookupCtxtExact cons (gamma defs)
 53 |         | _ => pure Nothing
 54 |       let nargs = lengthExplicitPi $ fst $ snd $ underPis (-1) Env.empty (type gdef)
 55 |       new_hole_names <- uniqueHoleNames defs nargs (nameRoot hole)
 56 |       let new_holes = PHole replFC True <$> new_hole_names
 57 |       let pcons = papply replFC (PRef replFC cons) new_holes
 58 |       res <- catch
 59 |         (do -- We're desugaring it to the corresponding TTImp
 60 |             icons <- desugar AnyExpr (toList lhsCtxt) pcons
 61 |             ccons <- checkTerm hidx {-is this correct?-} InExpr [] (MkNested []) env icons gty
 62 |             newdefs <- get Ctxt
 63 |             ncons <- normaliseHoles newdefs env ccons
 64 |             icons <- unelab env ncons
 65 |             pure (Just icons))
 66 |         (\ _ => pure Nothing)
 67 |       put Ctxt defs -- reset the context, we don't want any updates
 68 |       put UST ust
 69 |       pure res
 70 |     pure (catMaybes ics)
 71 | 
 72 |   export
 73 |   intro : Term lhsCtxt -> Core (List IRawImp)
 74 |   -- structural cases
 75 |   intro (Bind _ x (Let _ _ ty val) sc) = toList <$> intro (subst val sc)
 76 |   intro (TDelayed _ _ t) = intro t
 77 |   -- interesting ones
 78 |   intro (Bind _ x (Pi _ rig Explicit ty) _) = pure <$> introLam x rig ty
 79 |   intro t = case getFnArgs t of
 80 |     (Ref _ (TyCon ar) n, _) => introCon n t
 81 |     _ => pure []
 82 |