Something went wrong. Try again.
Newt - a dependent typed programming language
This is a mirror of the main github repository. newt.cloakedarrow.com
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638module Lib.ProcessDeclimport Preludeimport Data.IORefimport Data.Stringimport Lib.Commonimport Lib.Elabimport Lib.Parserimport Lib.Syntaximport Data.SortedMapimport Lib.TopContextimport Lib.Evalimport Lib.Prettierimport Lib.Typesimport Lib.Utilimport Lib.DerivedumpEnv : Context -> M StringdumpEnv 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 UnitlogConstraints = 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 UnitlogMetas Nil = pure MkUnitlogMetas (OutOfScope :: rest) = logMetas restlogMetas (Solved fc k soln :: rest) = logMetas restlogMetas (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 separatelylogMetas (Unsolved fc k ctx ty ErrorHole :: rest) = logMetas restlogMetas (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 RecordgetSigs : List Decl -> List (FC × Quant × String × Raw)getSigs Nil = NilgetSigs ((TypeSig _ q Nil _) :: xs) = getSigs xsgetSigs ((TypeSig fc q (nm :: nms) ty) :: xs) = (fc, q, nm, ty) :: getSigs xsgetSigs (_ :: xs) = getSigs xsteleToPi : Telescope -> Raw -> RawteleToPi Nil end = endteleToPi ((info, ty) :: tele) end = RPi (getFC info) info ty (teleToPi tele end)impTele : Telescope -> TelescopeimpTele 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 UnitcheckAlreadyDef 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 UnitprocessTypeSig : String → FC → Quant → List Name → Raw → M UnitprocessTypeSig 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 NilprocessPrimType : String → FC → Name → Maybe Raw → M UnitprocessPrimType 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) NilprocessPrimFn : String → FC → String → List String → Raw → String → M UnitprocessPrimFn 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 memoryshouldInline : Tm → BoolshouldInline (Lam _ _ _ _ sc) = shouldInline scshouldInline (Bnd _ _) = TrueshouldInline (Ref _ _) = TrueshouldInline (App _ t u Zero) = shouldInline tshouldInline (App _ t (Bnd _ _) Many) = shouldInline tshouldInline _ = FalseprocessDef : String → FC → String → List (Raw × Maybe Raw) → M UnitprocessDef 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 MkUnitprocessCheck : String → FC → Raw → Raw → M UnitprocessCheck 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 UnitprocessClass 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) icitprocessInstance : String → FC → Raw → Maybe (List Decl) → M UnitprocessInstance 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 itprocessShortData : String → FC → Raw → List Raw → M UnitprocessShortData 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, etcpopulateConInfo : List TopEntry → List TopEntrypopulateConInfo 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 :: NilprocessData : String → FC → FC × String → Raw → List Decl → M UnitprocessData 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 UnitprocessRecord 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 restprocessDerive : String → FC → FC × String → (FC × String) → M UnitprocessDerive 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 UnitprocessAlias 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 nsprocessExports : String → FC → List (FC × String) → M UnitprocessExports 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 MkUnitprocessDecl ns (DAlias fc nm args rhs) = processAlias fc nm args rhsprocessDecl ns (DDerive fc tclass name) = processDerive ns fc tclass nameprocessDecl ns (TypeSig fc q names tm) = processTypeSig ns fc q names tmprocessDecl ns (PType fc nm ty) = processPrimType ns fc nm typrocessDecl ns (PFunc fc nm used ty src) = processPrimFn ns fc nm used ty srcprocessDecl ns (FunDef fc nm clauses) = processDef ns fc nm clausesprocessDecl ns (DCheck fc tm ty) = processCheck ns fc tm typrocessDecl ns (Class classFC nm tele decls) = processClass ns classFC nm tele declsprocessDecl ns (Instance instfc ty decls) = processInstance ns instfc ty declsprocessDecl ns (ShortData fc lhs sigs) = processShortData ns fc lhs sigsprocessDecl ns (Data fc nm ty (Just cons)) = processData ns fc nm ty cons-- TODO distinguish from function signaturesprocessDecl ns (Data fc (_, nm) ty Nothing) = processTypeSig ns fc Zero [nm] typrocessDecl ns (Record recordFC nm tele cname decls) = processRecord ns recordFC nm tele cname declsprocessDecl ns (Exports fc names) = processExports ns fc names