module Lib.ProcessDecl

import Prelude
import Data.IORef
import Data.String
import Lib.Common
import Lib.Elab

import Lib.Parser
import Lib.Syntax
import Data.SortedMap
import Lib.TopContext
import Lib.Eval
import Lib.Prettier
import Lib.Types
import Lib.Util
import Lib.Derive

dumpEnv : Context -> M String
dumpEnv ctx =
  unlines ∘ reverse <$> go (names ctx) 0 (reverse $ zip ctx.env ctx.types) Nil
  where
    isVar : Int -> Val -> Bool
    isVar k (VVar _ _ k' Lin) = k == k'
    isVar _ _ = False
    -- REVIEW consider moving the goal up for editors like Helix that truncate
    -- REVIEW should we hide/demphasize entries that aren't bound to names?
    go : List String -> Int -> List (Val × String × Val × Quant) -> List String -> M (List String)
    go _ _ Nil acc = pure acc
    -- don't show the = bit for now. Lean folds it. We could truncate or ... it so we know it's a def.
    go names k ((v, n, ty, q) :: xs) acc = do
        ty' <- quote ctx.lvl ty
        go names (1 + k) xs ("  \{show q}\{n} : \{render 90 $ pprint names ty'}":: acc)

    -- go names k ((v, n, ty) :: xs) acc = if isVar k v
    --   then do
    --     ty' <- quote ctx.lvl ty
    --     go names (1 + k) xs ("  \{n} : \{render 90 $ pprint names ty'}":: acc)
    --   else do
    --     v' <- quote ctx.lvl v
    --     ty' <- quote ctx.lvl ty
    --     go names (1 + k) xs ("  \{n} = \{render 90 $ pprint names v'} : \{render 90 $ pprint names ty'}":: acc)

logConstraints : M Unit
logConstraints = do
  top <- getTop
  for_ top.currentMod.modMetaCtx.mpost $ \case
    MkMc fc nms env ty' ty => addError $ E fc "Constraint: \{show ty'} =?= \{show ty} deps \{show nms}"

logMetas : List MetaEntry -> M Unit
logMetas Nil = pure MkUnit
logMetas (OutOfScope :: rest) = logMetas rest
logMetas (Solved fc k soln :: rest) = logMetas rest
logMetas (Unsolved fc k ctx ty User :: rest) = do
      ty' <- quote ctx.lvl ty
      let names = map fst ctx.types
      env <- dumpEnv ctx
      let msg = "\{env}\n  -----------\n  \{render 90 $ pprint names ty'}"
      info fc "User Hole\n\{msg}"
      logMetas rest
-- error is reported separately
logMetas (Unsolved fc k ctx ty ErrorHole :: rest) = logMetas rest
logMetas (Unsolved fc k ctx ty kind :: rest) = do
      ty' <- forceMeta ty
      tm <- quote ctx.lvl ty'
      top <- getTop
      tm <- zonk top 0 Nil tm
      let msg = "Unsolved meta \{show k} \{show kind} type \{render 90 $ pprint (names ctx) tm}"
      sols <- case kind of
        AutoSolve => do
          x <- quote ctx.lvl ty
          ty <- eval ctx.env x
          debug "AUTO ---> \{show ty}"
          -- we want the context here too.
          top <- getTop
          let (VRef _ tyname _) = ty | _ => pure Nil
          -- TODO maybe log matches from ctx, too
          let cands = fromMaybe Nil $ lookupMap' tyname top.hints
          matches <- findMatches ctx ty cands
          pure ("  \{show $ length' matches} Solutions: \{show matches}" :: Nil)

        _ => pure Nil

      addError $ E fc $ unlines ((msg :: Nil) ++ sols)
      logMetas rest


-- Used for Class and Record
getSigs : List Decl -> List (FC × Quant × String × Raw)
getSigs Nil = Nil
getSigs ((TypeSig _ q Nil _) :: xs) = getSigs xs
getSigs ((TypeSig fc q (nm :: nms) ty) :: xs) = (fc, q, nm, ty) :: getSigs xs
getSigs (_ :: xs) = getSigs xs

teleToPi : Telescope -> Raw -> Raw
teleToPi Nil end = end
teleToPi ((info, ty) :: tele) end = RPi (getFC info) info ty (teleToPi tele end)

impTele : Telescope -> Telescope
impTele tele = map foo tele
  where
    foo : BindInfo × Raw → BindInfo × Raw
    foo (BI fc nm _ _ , ty) = (BI fc nm Implicit Zero, ty)


checkAlreadyDef : FC → Name → M Unit
checkAlreadyDef fc nm = do
  top <- getTop
  case lookup (QN top.currentMod.modName nm) top of
    Nothing => pure MkUnit
    Just entry => error fc "\{show nm} is already defined at \{show entry.fc}"


processDecl :  String -> Decl -> M Unit

processTypeSig :  String → FC → Quant → List Name → Raw → M Unit
processTypeSig ns fc q names tm = do
  log 1 "-----"
  top <- getTop
  traverse (checkAlreadyDef fc) names
  ty <- check (mkCtx fc Zero) tm (VU fc)
  log 1 "TypeSig \{unwords names} : \{render 90 $ pprint Nil ty}"
  ignore $ for names $ \nm => setDef (QN ns nm) fc q ty Axiom Nil


processPrimType : String → FC → Name → Maybe Raw → M Unit
processPrimType ns fc nm ty = do
  log 1 "Ptype \{show nm} : \{show ty}"
  top <- getTop
  ty' <- check (mkCtx fc Zero) (maybe (RU fc) id ty) (VU fc)
  let arity = piArity ty'
  setDef (QN ns nm) fc Zero ty' (PrimTCon arity) Nil


processPrimFn :  String → FC → String → List String → Raw → String → M Unit
processPrimFn ns fc nm used ty src = do
  top <- getTop
  ty <- check (mkCtx fc Zero) ty (VU fc)
  ty' <- nf Nil ty
  log 1 "pfunc \{nm} : \{render 90 $ pprint Nil ty'} = \{show src}"
  -- TODO wire through fc for not in scope error
  used' <- for used $ \ name => case lookupRaw name top of
    Nothing => error fc "\{name} not in scope"
    Just entry => pure entry.name
  let arity = piArity ty'
  setDef (QN ns nm) fc Many ty' (PrimFn src arity used') Nil

-- identity, lambdas in front of ref, application of args, unprocessed
-- we'd like to pick up String ++ and identity functions at least
-- important that we don't inline emptyTop - it has a lambda inside it (not top level)
-- which picks up the locals and leaks memory
shouldInline : Tm → Bool
shouldInline (Lam _ _ _ _ sc) = shouldInline sc
shouldInline (Bnd _ _) = True
shouldInline (Ref _ _) = True
shouldInline (App _ t u Zero) = shouldInline t
shouldInline (App _ t (Bnd _ _) Many) = shouldInline t
shouldInline _ = False

processDef :  String → FC → String → List (Raw × Maybe Raw) → M Unit
processDef ns fc nm clauses = do
  log 1 "-----"
  log 1 "Def \{show nm}"
  top <- getTop
  let mc = top.currentMod.modMetaCtx
  let (Just entry) = lookup (QN ns nm) top
    | Nothing => throwError $ E fc "No declaration for \{nm}"
  let (MkEntry fc q name ty Axiom _) = entry
    | _ => throwError $ E fc "\{nm} already defined at \{show entry.fc}"

  log 1 "check \{nm} at \{render 90 $ pprint Nil ty}"
  vty <- eval Nil ty

  debug "\{nm} vty is \{show vty}"

  clauses' <- traverse makeClause clauses
  tm <- buildTree (mkCtx fc q) (MkProb clauses' vty)

  -- We might want to freeze the autos after this
  -- TODO look at what is not solved at this point and see if we can catch it earlier
  solveAutos

  debug "Add def \{nm} \{render 90 $ pprint Nil tm} : \{render 90 $ pprint Nil ty}"
  updateDef (QN ns nm) fc ty (Fn tm)
  let name = show $ QN ns nm
  if shouldInline tm
     || name == "Prelude.Prelude.Monad Prelude.IO,bind"
     || name == "Prelude._>>=_"
     -- || name == "Prelude.Prelude.Concat Prim.String,_++_"
    then do
      debug "inline flag \{name}"
      setFlag (QN ns nm) fc Inline
    else pure MkUnit

processCheck :  String → FC → Raw → Raw → M Unit
processCheck ns fc tm ty = do
  log 1 "----- DCheck"
  top <- getTop

  info fc "check \{show tm} at \{show ty}"
  ty' <- check (mkCtx fc Zero) ty (VU fc)
  putStrLn "  got type \{render 90 $ pprint Nil ty'}"
  vty <- eval Nil ty'
  res <- check (mkCtx fc Many) tm vty
  putStrLn "  got \{render 90 $ pprint Nil res}"
  norm <- nf Nil res
  putStrLn "  NF \{render 90 $ pprint Nil norm}"


processClass :  String → FC → (FC × String) → Telescope → List Decl → M Unit
processClass ns classFC (nameFC, nm) tele decls = do
  -- REVIEW maybe we can leverage Record for this
  -- a couple of catches, we don't want the dotted accessors and
  -- the self argument should be an auto-implicit
  log 1 "-----"
  log 1 "Class \{nm}"
  let fields = getSigs decls
  -- We'll need names for the telescope
  let dcName = "Mk\{nm}"
  let tcType = teleToPi tele (RU classFC)
  let tail = foldl mkApp (RVar classFC nm) tele
  let dcType = teleToPi (impTele tele) $ foldr mkPi tail fields

  log 1 "tcon type \{render 90 $ pretty tcType}"
  log 1 "dcon type \{render 90 $ pretty dcType}"
  let decl = Data classFC (nameFC, nm) tcType (Just $ TypeSig classFC Many [dcName] dcType :: Nil)
  log 1 "Decl:"
  log 1 $ render 90 $ pretty decl
  processDecl ns decl
  ignore $ for fields $ \case
    (fc,q,name,ty) => do
      let funType = teleToPi (impTele tele) $ RPi fc (BI fc "_" Auto Many) tail ty
      let autoPat = foldl mkAutoApp (RVar classFC dcName) fields
      let lhs = makeLHS (RVar fc name) tele
      let lhs = RApp classFC lhs autoPat Auto
      let decl = FunDef fc name ((lhs, (Just $ RVar fc name)) :: Nil)

      log 1 "\{name} : \{render 90 $ pretty funType}"
      log 1 "\{render 90 $ pretty decl}"
      processDecl ns $ TypeSig fc q [name] funType
      setFlag (QN ns name) fc Inline
      processDecl ns decl
  where
    makeLHS : Raw → Telescope → Raw
    makeLHS acc ((BI fc' nm icit quant,  _) :: tele) = RApp fc' (makeLHS acc tele) (RVar fc' nm) Implicit
    makeLHS acc Nil = acc

    -- TODO probably should just do the fold ourselves then.
    mkAutoApp : Raw → FC × Quant × String × Raw → Raw
    mkAutoApp acc (fc, q, nm, ty) = RApp fc acc (RVar fc nm) Explicit

    mkPi : FC × Quant × String × Raw → Raw → Raw
    mkPi (fc, q, nm, ty) acc = RPi fc (BI fc nm Explicit q) ty acc

    mkApp : Raw → BindInfo × Raw → Raw
    mkApp acc (BI fc nm icit _, _) = RApp fc acc (RVar fc nm) icit

processInstance :  String → FC → Raw → Maybe (List Decl) → M Unit
processInstance ns instfc rawty decls = do
  log 1 "-----"
  log 1 "Instance \{render 90 $ pretty rawty}"
  top <- getTop
  let tyFC = getFC rawty

  let emptyCtx = mkCtx tyFC Zero
  ty <- check emptyCtx rawty (VU instfc)
  -- Here `tele` holds arguments to the instance
  let (codomain, tele) = splitTele ty
  -- env represents the environment of those arguments
  let env = tenv (length tele)
  debug "codomain \{render 90 $ pprint Nil codomain}"
  debug "tele is \{show tele}"

  -- a hack for a unique name
  let instname = render 90 $ pprint Nil codomain
  let sigDecl = TypeSig instfc Many (instname :: Nil) rawty
  -- The instance needs to be declared before processing the defs, but the defs need to be
  -- defined before this - side effect is that a duplicate def is noted at the first
  -- member
  case lookup (QN ns instname) top of
    Just entry => do
      vty' <- eval Nil entry.type
      vty <- eval Nil ty
      unifyCatch tyFC emptyCtx vty vty'
    Nothing => do
      -- only add once
      processDecl ns sigDecl
      setFlag (QN ns instname) instfc Hint
      addHint (QN ns instname)

  let (Just decls) = collectDecl <$> decls
    | _ => do
      debug "Forward declaration \{show sigDecl}"

  let (Ref _ tconName, args) = funArgs codomain
    | (tm, _) => error tyFC "\{render 90 $ pprint Nil codomain} doesn't appear to be a TCon application"
  let (Just (MkEntry _ _ name type (TCon _ cons) _)) = lookup tconName top
    | _ => error tyFC "\{show tconName} is not a type constructor"
  let (con :: Nil) = cons
    | _ => error tyFC "\{show tconName} has multiple constructors \{show cons}"
  let (Just (MkEntry _ _ _ dcty (DCon _ _ _ _) _)) = lookup con top
    | _ => error tyFC "can't find constructor \{show con}"
  vdcty@(VPi _ nm icit rig a b) <- eval Nil dcty
    | x => error (getFC x) "dcty not Pi"
  debug "dcty \{render 90 $ pprint Nil dcty}"
  -- let (_,args) = funArgs codomain

  let args = map fst args
  debug "traverse \{show $ map show args}"
  -- This is a little painful because we're reverse engineering the
  -- individual types back out from the composite type
  args' <- traverse (eval env) args
  debug "args' is \{show args'}"
  appty <- apply vdcty args'
  conTele <- getFields appty env Nil
  -- declare individual functions, collect their defs
  defs <- for conTele $ \case
     (MkBinder fc nm Explicit rig ty) => do
       let ty' = foldr (\ x acc => case x : Binder of (MkBinder fc nm' icit rig ty') => Pi fc nm' icit rig ty' acc) ty tele
       let nm' = "\{instname},\{nm}"
       -- we're working with a Tm, so we define directly instead of processDecl
       let (Just (FunDef fc name xs)) = find (\x => case x : Decl of
              (FunDef y name xs) => name == nm
              _ => False) decls
                | _ => error instfc "no definition for \{nm}"

       -- REVIEW if we want to Hint this
       setDef (QN ns nm') fc Many ty' Axiom Nil
       let decl = (FunDef fc nm' xs)
       log 1 "***"
       log 1 "«\{nm'}» : \{render 90 $ pprint Nil ty'}"
       log 1 $ render 80 $ pretty decl
       pure $ Just decl
     _ => pure Nothing

  for (mapMaybe id defs) $ \decl => do
    -- debug because already printed above, but nice to have it near processing
    debug $ render 80 $ pretty decl
    processDecl ns decl
  let (QN _ con') = con
  let decl = FunDef instfc instname ((RVar instfc instname, (Just $ mkRHS instname conTele (RVar instfc con'))) :: Nil)
  log 1 "SIGDECL"
  log 1 "\{render 90 $ pretty sigDecl}"
  log 1 $ render 80 $ pretty decl
  processDecl ns decl
  setFlag (QN ns instname) instfc InstCon
  where
    -- try to extract types of individual fields from the typeclass dcon
    -- We're assuming they don't depend on each other.
    getFields : Val -> Env -> List Binder -> M (List Binder)
    getFields tm@(VPi fc nm Explicit rig ty sc) env bnds = do
      bnd <- MkBinder fc nm Explicit rig <$> quote (length' env) ty
      appsc <- sc $$ VVar fc nm (length' env) Lin
      getFields appsc env (bnd :: bnds)
    getFields tm@(VPi fc nm _ rig ty sc) env bnds = do
      appsc <- sc $$ VVar fc nm (length' env) Lin
      getFields appsc env bnds
    getFields tm xs bnds = pure $ reverse bnds

    tenv : Nat -> Env
    tenv Z = Nil
    tenv (S k) = (VVar emptyFC "_" (cast k) Lin :: tenv k)

    mkRHS : String -> List Binder -> Raw -> Raw
    mkRHS instName (MkBinder fc nm Explicit rig ty :: bs) tm = mkRHS instName bs (RApp fc tm (RVar fc "\{instName},\{nm}") Explicit)
    mkRHS instName (b :: bs) tm = mkRHS instName bs tm
    mkRHS instName Nil tm = tm

    apply : Val -> List Val -> M Val
    apply x Nil = pure x
    apply (VPi fc nm icit rig a b) (x :: xs) = do
      bx <- b $$ x
      apply bx xs
    apply x (y :: xs) = error instfc "expected pi type \{show x}"

-- desugars to Data and processes it
processShortData :  String → FC → Raw → List Raw → M Unit
processShortData ns fc lhs sigs = do
  (nameFC, nm,args) <- getArgs lhs Nil
  let ty = foldr mkPi (RU fc) args
  cons <- traverse (mkDecl args Nil) sigs
  let dataDecl = Data fc (nameFC, nm) ty (Just cons)
  log 1 "SHORTDATA"
  log 1 "\{render 90 $ pretty dataDecl}"
  processDecl ns dataDecl
  where
    mkPi : FC × Name → Raw → Raw
    mkPi (fc,n) a = RPi fc (BI fc n Explicit Zero) (RU fc) a

    getArgs : Raw -> List (FC × String) -> M (FC × String × List (FC × String))
    getArgs (RVar fc1 nm) acc = pure (fc1, nm, acc)
    getArgs (RApp _ t (RVar fc' nm) _) acc = getArgs t ((fc', nm) :: acc)
    getArgs tm _ = error (getFC tm) "Expected contructor application, got: \{show tm}"

    mkDecl : List (FC × Name) -> List Raw -> Raw -> M Decl
    mkDecl args acc (RVar fc' name) = do
      let base = foldr (\ ty acc => RPi (getFC ty) (BI (getFC ty) "_" Explicit Many) ty acc) lhs acc
      let ty = foldr mkPi base args
      pure $ TypeSig fc' Many (name :: Nil) ty
      where
        mkPi : FC × String → Raw → Raw
        mkPi (fc,nm) acc = RPi fc (BI fc nm Implicit Zero) (RU fc) acc

    mkDecl args acc (RApp fc' t u icit) = mkDecl args (u :: acc) t
    mkDecl args acc tm = error (getFC tm) "Expected contructor application, got: \{show tm}"

-- Identify Nat-like, enum-like, etc
populateConInfo : List TopEntry → List TopEntry
populateConInfo entries =
  let (Nothing) = traverse checkEnum entries
      -- Boolean
      | Just (a :: b :: Nil) => (setInfo a FalseCon :: setInfo b TrueCon :: Nil)
      | Just entries => entries in
  case entries of
    a :: Nil => case countFields a of
      0 => setInfo a NilCon :: Nil
      2 => setInfo a ConsCon :: Nil
      _ => entries
    a :: b :: Nil =>
      fromMaybe entries $ checkNat entries <|> checkCons entries
    _ => entries
  where
    countFields : TopEntry → Int
    countFields (MkEntry fc _ name type def eflags) = go type
     where
       go : Tm → Int
       go (Pi fc nm _ Zero a b) = go b
       go (Pi fc nm _ Many a b) = 1 + go b
       go _ = 0
    countFields _ = 0

    runtimeFields : Tm → List Tm × Tm
    runtimeFields type = go type Lin
      where
        go : Tm → SnocList Tm → List Tm × Tm
        go (Pi fc nm _ Zero a b) tele = go b tele
        go (Pi fc nm _ Many a b) tele = go b (tele :< a)
        go tl tele = (tele <>> Nil, tl)

    splitApp : Tm → Tm × List Tm
    splitApp tm = go tm Lin
      where
        go : Tm → SnocList Tm → Tm × List Tm
        go (App _ t u Zero) tele = go t tele
        go (App _ t u Many) tele = go t (tele :< u)
        go tm tele = (tm, tele <>> Nil)

    setInfo : TopEntry → ConInfo → TopEntry
    setInfo (MkEntry fc q nm dty (DCon ix _ arity hn) flags) info = MkEntry fc q nm dty (DCon ix info arity hn) flags
    setInfo x _ = x

    checkEnum : TopEntry → Maybe TopEntry
    checkEnum entry = case countFields entry of
       0 => Just $ setInfo entry EnumCon
       _ => Nothing

    isZero : TopEntry → Bool
    isZero entry = countFields entry == 0

    isSucc : TopEntry → Bool
    isSucc entry@(MkEntry fc _ nm dty@(Pi _ _ _ _ _ b) (DCon _ _ _ hn) _)  = case runtimeFields dty of
      ([a],b) => case (splitApp a, splitApp b) of
        ((Ref _ a, _), (Ref _ b, _)) => a == b
        (a,b) => False
      _ => False
    isSucc _ = False

    -- assumes we've filtered down to two entries
    checkNat : List TopEntry → Maybe (List TopEntry)
    checkNat entries = do
      zero <- find isZero entries
      succ <- find isSucc entries
      pure $ setInfo zero ZeroCon :: setInfo succ SuccCon :: Nil

    -- assumes we've filtered down to two entries
    checkCons : List TopEntry → Maybe (List TopEntry)
    checkCons entries = do
      nil <- find (\ x => countFields x == 0) entries
      cons <- find (\x => countFields x == 2) entries
      pure $ setInfo nil NilCon :: setInfo cons ConsCon :: Nil

processData : String → FC → FC × String → Raw → List Decl → M Unit
processData ns fc (nameFC, nm) ty cons = do
  log 1 "-----"
  log 1 "Data \{nm}"
  top <- getTop
  let mc = top.currentMod.modMetaCtx
  let emptyCtx = mkCtx fc Zero
  tyty <- check emptyCtx ty (VU fc)
  case lookup (QN ns nm) top of
    Just (MkEntry fdeclFC q name type Axiom _) => do
      let (Zero) = q | _ => error fdeclFC "Type constructor forward declaration at wrong quantity"
      tyty' <- eval Nil tyty
      type' <- eval Nil type
      unifyCatch fc emptyCtx tyty' type'
    Just _ => error nameFC "\{show nm} already declared"
    Nothing => setDef (QN ns nm) fc Zero tyty Axiom Nil
  -- check cons, return list of type,con
  allCons <- join <$> (for cons $ \x => case x of
      (TypeSig fc q names tm) => do
          traverse (checkAlreadyDef fc) names
          debug "check dcon \{show names} \{show tm}"
          dty <- check (mkCtx fc Zero) tm (VU fc)
          debug "dty \{show names} is \{render 90 $ pprint Nil dty}"

          -- We only check that codomain used the right type constructor
          -- We know it's in U because it's part of a checked Pi type
          let (codomain, tele) = splitTele dty
          -- for printing
          let tnames = reverse $ map binderName tele
          let (Ref _ hn, args) = funArgs codomain
            | (tm, _) => error (getFC tm) "expected \{nm} got \{render 90 $ pprint tnames tm}"
          when (hn /= QN ns nm) $
            error (getFC codomain) "Constructor codomain is \{render 90 $ pprint tnames codomain} rather than \{nm}"
          pure $ map (_,_ dty) names
      decl => throwError $ E (getFC decl) "expected constructor declaration")
  -- type level autos like _++_
  solveAutos

  let entries = populateConInfo $ map makeConEntry $ enumerate allCons
  for entries $ \case (MkEntry fc q name dty def flags) => setDef name fc q dty def flags
  let cnames = map (\x => x.name) entries

  log 1 "setDef \{nm}  TCon \{show cnames}"
  let arity = piArity tyty
  updateDef (QN ns nm) fc tyty (TCon arity cnames)
  where
    makeConEntry : (Nat × Tm × String) → TopEntry
    makeConEntry (ix, dty, nm') = MkEntry fc Many (QN ns nm') dty (DCon ix NormalCon (getArity dty) (QN ns nm)) Nil

    binderName : Binder → Name
    binderName (MkBinder _ nm _ _ _) = nm

    checkDeclType : Tm -> M Unit
    checkDeclType (UU _) = pure MkUnit
    checkDeclType (Pi _ str icit rig t u) = checkDeclType u
    checkDeclType _ = error fc "data type doesn't return U"


processRecord :  String → FC → FC × String → Telescope → Maybe (FC × Name) → List Decl → M Unit
processRecord ns recordFC (nameFC, nm) tele cname decls = do
  log 1 "-----"
  log 1 "Record"
  let fields = getSigs decls
  let (dcFC,dcName) = fromMaybe (nameFC,"Mk\{show nm}") cname
  let tcType = teleToPi tele (RU recordFC)
  let tail = foldl (\ acc bi => case bi : BindInfo × Raw of (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar nameFC nm) tele
  let dcType = teleToPi (impTele tele) $
        foldr (\ x acc => case x : FC × Quant × String × Raw of (fc, q, nm, ty) =>  RPi fc (BI fc nm Explicit q) ty acc  ) tail fields

  log 1 "tcon type \{render 90 $ pretty tcType}"
  log 1 "dcon type \{render 90 $ pretty dcType}"
  let decl = Data recordFC (nameFC,nm) tcType (Just $ TypeSig recordFC Many [dcName] dcType :: Nil)
  log 1 "Decl:"
  log 1 $ render 90 $ pretty decl
  processDecl ns decl
  -- pattern to peel out fields on LHS
  let autoPat = foldl (\acc x => case x : FC × Quant × String × Raw of (fc,q,nm,ty) => RApp fc acc (RVar nameFC nm) Explicit) (RVar nameFC dcName) fields
  processFields autoPat tail Nil fields
  where
    processFields : Raw → Raw → List (String × Raw) → List (FC × Quant × String × Raw) → M Unit
    processFields _ _ _ Nil = pure MkUnit
    processFields autoPat tail deps ((fc,q,name,ty) :: rest) = do
      let funType = substRaw deps $ teleToPi (impTele tele) $ RPi fc (BI fc "$self" Explicit Many) tail ty

      -- `.fieldName`
      let pname = "." ++ name
      let lhs = foldl (\acc x => case x : BindInfo × Raw of (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc pname) tele
      let lhs = RApp recordFC lhs autoPat Explicit
      let pdecl = FunDef fc pname ((lhs, (Just $ RVar fc name)) :: Nil)
      log 1 "\{pname} : \{render 90 $ pretty funType}"
      log 1 "\{render 90 $ pretty pdecl}"
      processDecl ns $ TypeSig fc Many (pname :: Nil) funType
      processDecl ns pdecl
      setFlag (QN ns pname) fc Inline
      let deps = ((name, RApp fc (RVar fc pname) (RVar fc "$self") Explicit) :: deps)
      processFields autoPat tail deps rest

processDerive : String → FC → FC × String → (FC × String) → M Unit
processDerive ns fc (clFC, clName) (fc, name) = do
  case clName of
    "Eq" => do
        decls <- deriveEq fc name
        for_ decls $ processDecl ns
    "Show" => do
        decls <- deriveShow fc name
        for_ decls $ processDecl ns
    _ => error fc "derive \{clName} is not supported"

processAlias : FC → FC × String → Telescope → Raw → M Unit
processAlias fc (fc', nm) args rhs = do
  top <- getTop
  let ns = top.currentMod.modName
  let ty = mkty args
  processTypeSig ns fc Zero [nm] ty
  let lhs = mklhs args
  processDef ns fc (nm) [(lhs, Just rhs)]
  pure MkUnit
  where
    mklhs : Telescope → Raw
    mklhs Nil = RVar fc' nm
    mklhs ((BI fc name icit quant, _) :: rest) =
      RApp fc (mklhs rest) (RVar fc name) Explicit

    mkty : Telescope → Raw
    mkty Nil = RU fc
    mkty ((bi, ty) :: ns) = RPi (getFC bi) bi ty $ mkty ns


processExports : String → FC → List (FC × String) → M Unit
processExports ns fc names = do
  top <- getTop
  traverse_ (setExport top) names
  where
    setExport : TopContext → FC × String → M Unit
    setExport top (fc, name) = do
      let (Just entry) = lookupRaw name top | _ => error fc "\{name} not in scope"
      setFlag entry.name fc Export

-- currently mixfix registration is handled in the parser
-- since we now run a decl at a time we could do it here.
processDecl ns (PMixFix _ _ _ _)  = pure MkUnit
processDecl ns (DAlias fc nm args rhs)  = processAlias fc nm args rhs
processDecl ns (DDerive fc tclass name)  = processDerive ns fc tclass name
processDecl ns (TypeSig fc q names tm) = processTypeSig ns fc q names tm
processDecl ns (PType fc nm ty) = processPrimType ns fc nm ty
processDecl ns (PFunc fc nm used ty src) = processPrimFn ns fc nm used ty src
processDecl ns (FunDef fc nm clauses) = processDef ns fc nm clauses
processDecl ns (DCheck fc tm ty) = processCheck ns fc tm ty
processDecl ns (Class classFC nm tele decls) = processClass ns classFC nm tele decls
processDecl ns (Instance instfc ty decls) = processInstance ns instfc ty decls
processDecl ns (ShortData fc lhs sigs) = processShortData ns fc lhs sigs
processDecl ns (Data fc nm ty (Just cons)) = processData ns fc nm ty cons
-- TODO distinguish from function signatures
processDecl ns (Data fc (_, nm) ty Nothing) = processTypeSig ns fc Zero [nm] ty
processDecl ns (Record recordFC nm tele cname decls) = processRecord ns recordFC nm tele cname decls
processDecl ns (Exports fc names) = processExports ns fc names