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.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616module Lib.Typesimport Preludeimport Lib.Commonimport Lib.Prettierimport Data.IORefimport Data.SnocListimport Data.SortedMapimport Data.Stringalias Name = Stringdata Icit = Implicit | Explicit | Autoderive Show Icitderive Eq Icitdata BD = Bound | Definedderive Eq BDderive Show BDdata Quant = Zero | Manyderive Eq Quantinstance Mul Quant where Zero * b = Zero a * Zero = Zero a * b = Many-- Used for pretty-printinginstance Show Quant where show Zero = "0 " show Many = ""data BindInfo : U where BI : (fc : FC) -> (name : Name) -> (icit : Icit) -> (quant : Quant) -> BindInfoinstance HasFC BindInfo where getFC (BI fc _ _ _) = fc0 Tm : Udata Literal = LString String | LInt Int | LChar Char | LBool Boolinstance Show Literal where show (LString str) = quoteString str show (LBool b) = if b then "true" else "false" show (LInt i) = show i show (LChar c) = "\{show c}"data CaseAlt : U where CaseDefault : Tm -> CaseAlt CaseCons : (name : QName) -> (args : List String) -> Tm -> CaseAlt CaseLit : Literal -> Tm -> CaseAlt0 Def : Uinstance Eq Literal where LString x == LString y = x == y LInt x == LInt y = x == y LChar x == LChar y = x == y _ == _ = Falsedata Tm : U where Bnd : FC -> Int -> Tm -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc. Ref : FC -> QName -> Tm Meta : FC -> QName -> Tm Lam : FC -> Name -> Icit -> Quant -> Tm -> Tm App : FC -> Tm -> Tm -> Quant -> Tm UU : FC -> Tm Pi : (fc : FC) -> (nm : Name) -> Icit -> Quant -> (a : Tm) -> (b : Tm) -> Tm Case : FC -> Tm -> List CaseAlt -> Tm -- need type? Let : FC -> Name -> Tm -> Tm -> Tm -- for desugaring where LetRec : FC -> Name -> (ty : Tm) -> (t : Tm) -> (u : Tm) -> Tm Lit : FC -> Literal -> Tm -- An erased value Erased : FC -> Tm Delay : FC → Tm → Tm Force : FC → Tm → Tminstance HasFC Tm where getFC (Bnd fc k) = fc getFC (Force fc _) = fc getFC (Delay fc _) = fc getFC (Ref fc str) = fc getFC (Meta fc k) = fc getFC (Lam fc str _ _ t) = fc getFC (App fc t u _) = fc getFC (UU fc) = fc getFC (Pi fc str icit quant t u) = fc getFC (Case fc t xs) = fc getFC (Lit fc _) = fc getFC (Let fc _ _ _) = fc getFC (LetRec fc _ _ _ _) = fc getFC (Erased fc) = fcshowCaseAlt : CaseAlt → Stringinstance Show Tm where show (Bnd _ k) = "(Bnd \{show k})" show (Force _ t) = "(Force \{show t})" show (Delay _ t) = "(Delay \{show t})" show (Ref _ str) = "(Ref \{show str})" show (Lam _ nm icit rig t) = "(\\ \{show rig}\{nm} => \{show t})" show (App _ t u _) = "(\{show t} \{show u})" show (Meta _ i) = "(Meta \{show i})" show (Lit _ l) = "(Lit \{show l})" show (UU _) = "U" show (Pi _ str Explicit rig t u) = "(Pi (\{show rig}\{str} : \{show t}) => \{show u})" show (Pi _ str Implicit rig t u) = "(Pi {\{show rig}\{str} : \{show t}} => \{show u})" show (Pi _ str Auto rig t u) = "(Pi {{\{show rig}\{str} : \{show t}}} => \{show u})" show (Case _ sc alts) = "(Case \{show sc} \{show $ map showCaseAlt alts})" show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})" show (LetRec _ nm ty t u) = "(LetRec \{nm} : \{show ty} \{show t} \{show u})" show (Erased _) = "ERASED"showCaseAlt (CaseDefault tm) = "_ => \{show tm}"showCaseAlt (CaseCons nm args tm) = "\{show nm} \{unwords args} => \{show tm}"showCaseAlt (CaseLit lit tm) = "\{show lit} => \{show tm}"instance Show CaseAlt where show = showCaseAlt-- TODO make it more readable-- Option to hide implicits-- Ahh, but App doesn't know...-- Restore infix operations e.g. (_::_ a b) => a _::_ b (but implicits!)pprint' : Int -> List String -> Tm -> DocpprintAlt : Int -> List String -> CaseAlt -> DocpprintAlt p names (CaseDefault t) = text "_" <+> text "=>" <+> pprint' p ("_" :: names) tpprintAlt p names (CaseCons name args t) = text (show name) <+> spread (map text args) <+> (nest 2 $ text "=>" <+/> pprint' p (reverse args ++ names) t)-- `;` is not in surface syntax, but sometimes we print on one linepprintAlt p names (CaseLit lit t) = text (show lit) <+> (nest 2 $ text "=>" <+/> pprint' p names t ++ text ";")parens : Int -> Int -> Doc -> Docparens a b doc = if a < b then text "(" ++ doc ++ text ")" else docpprint' p names (Bnd _ k) = case getAt (cast k) names of -- Either a bug or we're printing without names Nothing => text "BND:\{show k}" Just nm => text "\{nm}:\{show k}"pprint' p names (Force _ t) = text "%force" <+> pprint' p names tpprint' p names (Delay _ t) = parens 0 p $ text "%delay" <+> pprint' 0 names tpprint' p names (Ref _ qn) = text $ show qnpprint' p names (Ref _ (QN qns baseName)) = text baseNamepprint' p names (Meta _ (QN qns baseName)) = text "?\{baseName}"pprint' p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{nm} =>" <+/> pprint' 0 (nm :: names) t-- TODO would be nice to make Meta app prettier, we could funArgs it, but might not be able-- to drop them because we do want to show if the meta is applied to _extra_ argspprint' p names (App _ t u _) = parens 0 p $ pprint' 0 names t <+> pprint' 1 names upprint' p names (UU _) = text "U"pprint' p names (Pi _ nm Auto rig t u) = parens 0 p $ text "{{" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t <+> text "}}" <+> text "->" <+> pprint' 0 (nm :: names) upprint' p names (Pi _ nm Implicit rig t u) = parens 0 p $ text "{" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t <+> text "}" <+> text "->" <+> pprint' 0 (nm :: names) upprint' p names (Pi _ "_" Explicit Many t u) = parens 0 p $ pprint' 1 names t <+> text "->" <+> pprint' 0 ("_" :: names) upprint' p names (Pi _ nm Explicit rig t u) = parens 0 p $ text "(" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t ++ text ")" <+> text "->" <+> pprint' 0 (nm :: names) upprint' p names (Case _ sc alts) = parens 0 p $ text "case" <+> pprint' 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (pprintAlt 0 names) alts)))pprint' p names (Lit _ lit) = text (show lit)pprint' p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> text ":=" <+> pprint' 0 names t <+> text "in" </> (nest 2 $ pprint' 0 (nm :: names) u)pprint' p names (LetRec _ nm ty t u) = parens 0 p $ text "letrec" <+> text nm <+> text ":" <+> pprint' 0 names ty <+> text ":=" <+> pprint' 0 names t <+> text "in" </> (nest 2 $ pprint' 0 (nm :: names) u)pprint' p names (Erased _) = text "ERASED"-- Pretty printer for Tm.pprint : List String -> Tm -> Docpprint names tm = pprint' 0 names tm0 Val : U-- IS/TypeTheory.idr is calling this a Kripke function space-- Yaffle, IS/TypeTheory use a function here.-- Kovacs, Idris use Env and Tm-- in cctt kovacs refers to this choice as defunctionalization vs HOAS-- https://github.com/AndrasKovacs/cctt/blob/main/README.md#defunctionalization-- the tradeoff is access to internals of the function-- Yaffle is vars -> vars here0 Closure : U0 Env : U-- Constatine has Icit in here too, I'm considering that as not part of core,-- but I suspect I'll want it later. Maybe for diagnostics or reusing data.alias VSpine = SnocList (Val × Quant)data Val : U where VVar : FC -> (nm : String) -> (k : Int) -> (sp : VSpine) -> Val VRef : FC -> (nm : QName) -> (sp : VSpine) -> Val VCase : FC -> (sc : Val) -> Env -> List CaseAlt -> Val VMeta : FC -> QName -> (sp : VSpine) -> Val VLam : FC -> Name -> Icit -> Quant -> Closure -> Val VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val -- not substing let, like idris VLet : FC -> Name -> Val -> Closure -> Val VLetRec : FC -> Name -> Val -> Closure -> Closure -> Val VU : FC -> Val VErased : FC -> Val VLit : FC -> Literal -> Val VDelay : FC -> Val -> Val VForce : FC -> Val -> ValEnv = List Valdata Closure = MkClosure Env TmgetValFC : Val -> FCgetValFC (VVar fc _ _ _) = fcgetValFC (VForce fc _) = fcgetValFC (VDelay fc _) = fcgetValFC (VRef fc _ _) = fcgetValFC (VCase fc _ _ _) = fcgetValFC (VMeta fc _ _) = fcgetValFC (VLam fc _ _ _ _) = fcgetValFC (VPi fc _ _ _ a b) = fcgetValFC (VU fc) = fcgetValFC (VErased fc) = fcgetValFC (VLit fc _) = fcgetValFC (VLet fc _ _ _) = fcgetValFC (VLetRec fc _ _ _ _) = fcinstance HasFC Val where getFC = getValFCshowClosure : Closure → Stringinstance Show Val where show (VVar _ nm k Lin) = "\{show nm}:\{show k}" show (VForce _ t) = "(%force \{show t})" show (VDelay _ t) = "(%delay \{show t})" show (VVar _ nm k sp) = "(\{show nm}:\{show k} \{unwords $ map show $ map fst (sp <>> Nil)})" show (VRef _ nm Lin) = show nm show (VRef _ nm sp) = "(\{show nm} \{unwords $ map show $ map fst (sp <>> Nil)})" show (VMeta _ ix sp) = "(%meta \{show ix} [\{show $ snoclen sp} sp])" show (VLam _ str icit quant x) = "(%lam \{show quant}\{str} \{showClosure x})" show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show x}}. \{showClosure y})" show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show x}). \{showClosure y})" show (VPi fc str Auto rig x y) = "(%pi {{\{show rig} \{str} : \{show x}}}. \{showClosure y})" show (VCase fc sc env alts) = "(%case \{show sc} \{unwords $ map show alts})" show (VU _) = "U" show (VLit _ lit) = show lit show (VLet _ nm a (MkClosure env b)) = "(%let \{show nm} = \{show a} in \{show b}" show (VLetRec _ nm ty (MkClosure _ a) (MkClosure _ b)) = "(%letrec \{show nm} : \{show ty} = \{show a} in \{show b}" show (VErased _) = "ERASED"showClosure (MkClosure xs t) = "(%cl [\{show $ length xs} env] \{show t})"0 Context : Udata MetaKind = Normal | User | AutoSolve | ErrorHolederive Show MetaKindderive Eq MetaKindrpprint : List String → Tm → Stringrpprint names tm = render 90 $ pprint names tm-- In types so we can have Val / Tm / Contextdata Error = E FC String | ENotInScope FC String -- Postpone signals a meta that needs to be solved first | Postpone FC String | UnificationError FC (List String) Tm Tm Errorinstance HasFC Error where getFC (E x str) = x getFC (UnificationError fc _ _ _ _) = fc getFC (ENotInScope x _) = x getFC (Postpone x str) = x-- Non-pretty version, there is an in-monad prettyErrorMsg in Lib.ErrorerrorMsg : Error -> StringerrorMsg (E x str) = strerrorMsg (ENotInScope x nm) = "\{nm} not in scope"errorMsg (Postpone x str) = strerrorMsg (UnificationError fc names a b err) = "unification failure: \{errorMsg err}\n failed to unify \{show a}\n with \{show b}\n "instance Show Error where show err = "ERROR at \{show $ getFC err}: \{errorMsg err}\n"-- constrain meta applied to val to be a valdata MConstraint = MkMc FC (List QName) Env Val Valinstance Show MConstraint where show (MkMc fc ms env ty' ty) = "MkMC \{show fc} env \{show ty'} \{show ty}"data MetaEntry = Unsolved FC QName Context Val MetaKind | Solved FC QName Val | OutOfScopeinstance HasFC MetaEntry where getFC (Unsolved fc _ _ _ _) = fc getFC (Solved fc _ _) = fc getFC OutOfScope = emptyFC-- The purpose of this is to only check one level of constraints when trying an Auto solution-- The idea being we narrow it down to the likely solution, and let any consequent type error-- bubble up to the user, rather than have a type error wipe out all solutions.-- We also don't bother adding constraints if not in CheckAll modedata MetaMode = CheckAll | CheckFirst | NoCheckrecord MetaContext where constructor MC metas : SortedMap QName MetaEntry autos : List QName mpost : List MConstraint next : Int mcmode : MetaModederive Eq MetaModedata ConInfo = NormalCon | SuccCon | ZeroCon | EnumCon | TrueCon | FalseCon | NilCon | ConsConderive Eq ConInfoinstance Show ConInfo where show NormalCon = "" show ConsCon = "[C]" show NilCon = "[N]" show FalseCon = "[F]" show TrueCon = "[T]" show SuccCon = "[S]" show ZeroCon = "[Z]" show EnumCon = "[E]"data Def = Axiom | TCon (List Quant) (List QName) | DCon Nat ConInfo (List Quant) QName | Fn Tm | PrimTCon (List Quant) | PrimFn String (List Quant) (List QName)derive Show Defdata EFlag = Hint | Inline | Export | InstConderive Show EFlagderive Eq EFlagrecord TopEntry where constructor MkEntry fc : FC quant : Quant name : QName type : Tm def : Def eflags : List EFlaginstance Show TopEntry where show (MkEntry fc q name type def flags) = "\{show q}\{show name} : \{show type} := \{show def} \{show flags}"data EditorInfo = CaseSplit FC Context Int Val -- Not sure we need Context here? | MissingCases FC Context (List QName)record ModContext where constructor MkModCtx modName : String modSource : String modDefs : SortedMap QName TopEntry -- Do we need this if everything solved is zonked? modMetaCtx : MetaContext -- longer term maybe drop this, put the operator decls in ctxDefs and collect them on import modOps : Operators modDeps : List String modErrors : List Error modInfos : List EditorInfoemptyModCtx : String → String → ModContextemptyModCtx modName source = MkModCtx modName source emptyMap (MC emptyMap Nil Nil 0 NoCheck) emptyMap Nil Nil Nilalias HintTable = SortedMap QName (List (QName × Tm))-- DERIVE - HasFC would be an example of a user-defined derivedinstance HasFC EditorInfo where getFC (CaseSplit fc _ _ _) = fc getFC (MissingCases fc _ _) = fc-- InlineEval is used in inliningdata ElabMode = NormalEval | InlineEval-- modules are "modules"-- currentMod represents the current module (to save a map lookup)-- when we switch modules, load imports into ops and hints-- as we process the decls, update ops and currentMod.opsrecord TopContext where constructor MkTop modules : SortedMap String ModContext hints : HintTable -- current module currentMod : ModContext verbose : Int -- command line flag increments this ops : Operators freshIx : Int -- I didn't want to pass another argument through eval (maybe an auto?) -- used to switch behavior for inlining elabMode : ElabMode-- For erasure, is the erased marker present in the environmentdata Marker = Present | Absentderive Show Markerrecord Context where constructor MkCtx lvl : Int -- Kovacs splits this into multiple fields -- I was going to recombine them, but realized I'd have to regenerate env for eval env : Env -- Values in scope -- TODO add fc, maybe add BD and make this a proper type types : List (String × Val × Quant) -- types and names in scope -- so we'll try "bds" determines length of local context bds : List BD -- bound or defined -- FC to use for errors if we don't have a better option ctxFC : FC marker : Marker-- add a binding to environmentextend : Context -> String -> Val -> Quant → Contextextend (MkCtx lvl env types bds ctxFC mark) name ty quant = MkCtx (1 + lvl) (VVar emptyFC name lvl Lin :: env) ((name, ty, quant) :: types) (Bound :: bds) ctxFC mark-- add a def to the environmentdefine : Context -> String -> Val -> Val → Quant -> Contextdefine (MkCtx lvl env types bds ctxFC mark) name val ty quant = MkCtx (1 + lvl) (val :: env) ((name, ty, quant) :: types) (Defined :: bds) ctxFC markinstance Show MetaEntry where show (Unsolved pos k ctx ty kind) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds} cs" show (Solved _ k x) = "Solved \{show k} \{show x}" show OutOfScope = "OutOfScope"withPos : Context -> FC -> ContextwithPos ctx fc = { ctxFC := fc } ctxnames : Context -> List Stringnames ctx = map fst ctx.types-- Enter an erased sectionenterMarker : Context → ContextenterMarker = { marker := Present }enterMarker' : Quant → Context → ContextenterMarker' Zero = { marker := Present }enterMarker' Many ctx = ctxrecord M a where constructor MkM runM : TopContext -> IO (Either Error (TopContext × a))instance Functor M where map f (MkM run) = MkM $ \tc => do (Right (tc', a)) <- (run tc) | Left err => return $ Left err return $ Right (tc', f a)instance Applicative M where pure x = MkM $ \tc => return $ Right (tc, x) (MkM f) <*> (MkM x) = MkM $ \tc => do Right (tc', f') <- f tc | Left err => return $ Left err Right (tc'', x') <- x tc' | Left err => return $ Left err return $ Right (tc'', f' x')instance Monad M where return = pure bind (MkM x) f = MkM $ \tc => do (Right (tc', a)) <- x tc | Left err => return $ Left err .runM (f a) tc'instance HasIO M where liftIO io = MkM $ \tc => do result <- io return $ Right (tc, result)throwError : ∀ a. Error -> M athrowError err = MkM $ \_ => return $ Left errcatchError : ∀ a. M a -> (Error -> M a) -> M acatchError (MkM ma) handler = MkM $ \tc => do (Right (tc', a)) <- ma tc | Left err => .runM (handler err) tc return $ Right (tc', a)tryError : ∀ a. M a -> M (Either Error a)tryError ma = catchError (map Right ma) (return ∘ Left)filterM : ∀ a. (a → M Bool) → List a → M (List a)filterM pred Nil = return NilfilterM pred (x :: xs) = do check <- pred x if check then _::_ x <$> filterM pred xs else filterM pred xsgetTop : M TopContextgetTop = MkM $ \ tc => return $ Right (tc, tc)putTop : TopContext -> M UnitputTop tc = MkM $ \_ => return $ Right (tc, MkUnit)modifyTop : (TopContext -> TopContext) -> M UnitmodifyTop f = do tc <- getTop putTop (f tc)-- Force argument and print if verbose is truelog : Int -> Lazy String -> M Unitlog lvl x = do top <- getTop when (lvl <= top.verbose) $ putStrLn xlogM : Int → M String -> M UnitlogM lvl x = do top <- getTop when (lvl <= top.verbose) $ do msg <- x putStrLn msg-- deprecated for `log 2`debug : Lazy String -> M Unitdebug x = log 2 xinfo : FC -> String -> M Unitinfo fc msg = putStrLn "INFO at \{show fc}: \{msg}"-- Version of debug that makes monadic computation lazydebugM : M String -> M UnitdebugM x = logM 2 xinstance Show Context where show ctx = "Context \{show $ map fst $ ctx.types}"error : ∀ a. FC -> String -> M aerror fc msg = throwError $ E fc msgerror' : ∀ a. String -> M aerror' msg = throwError $ E emptyFC msglookupMeta : QName -> M MetaEntrylookupMeta ix@(QN ns nm) = do top <- getTop case lookupMap' ix top.currentMod.modMetaCtx.metas of Just meta => return meta Nothing => case lookupMap' ns top.modules of Nothing => do -- happens when printing an error because the top is reset debug "missing module: \{show ns} looking up meta \{show ix}" return OutOfScope Just mod => case lookupMap' ix mod.modMetaCtx.metas of Nothing => do -- happens for rolled back metas in error messages debug "meta not present: \{show ix}" return OutOfScope Just entry => return entrymkCtx : FC -> Quant -> ContextmkCtx fc q = MkCtx 0 Nil Nil Nil fc (if q == Many then Absent else Present)-- Used by Syntax and Elabdata Pattern = PatVar FC Icit Name | PatCon FC Icit QName (List Pattern) (Maybe Name) | PatWild FC Icit | PatLit FC Literal | PatImpossible FCgetIcit : Pattern -> IcitgetIcit (PatVar x icit str) = icitgetIcit (PatCon x icit str xs as) = icitgetIcit (PatWild x icit) = icitgetIcit (PatLit fc lit) = ExplicitgetIcit (PatImpossible _) = Explicitinstance HasFC Pattern where getFC (PatVar fc _ _) = fc getFC (PatCon fc _ _ _ _) = fc getFC (PatWild fc _) = fc getFC (PatLit fc lit) = fc getFC (PatImpossible fc) = fcinstance Show Pattern where show (PatVar _ icit str) = "(PatVar " ++ show icit ++ " " ++ show str ++ ")" show (PatImpossible _) = "PatImp" show (PatCon _ icit str xs as) = "(PatCon " ++ show icit ++ " " ++ show str ++ " " ++ show xs ++ " " ++ show as ++ ")" show (PatWild _ icit) = "(PatWild " ++ show icit ++ ")" show (PatLit _ lit) = "(PatLit " ++ show lit ++ ")"-- Lazy because `let` would do work at the top of a `M a`profile : ∀ a. String → Lazy (M a) → M aprofile desc work = do start <- getTime res <- work end <- getTime putStrLn "PROF \{desc} \{show $ end - start} ms" return res