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.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307module Lib.Syntaximport Preludeimport Lib.Commonimport Data.Stringimport Data.Listimport Lib.Prettierimport Lib.Typesdata Raw : U-- could be a pair, but I suspect stuff will be added?data RCaseAlt = MkAlt Raw (Maybe Raw)data UpdateClause = AssignField FC String Raw | ModifyField FC String Rawdata DoStmt : U where DoExpr : (fc : FC) -> Raw -> DoStmt DoLet : (fc : FC) -> String -> Raw -> DoStmt DoArrow : (fc : FC) -> (lhs : Raw) -> (rhs : Raw) -> (alts : List RCaseAlt) -> DoStmtinstance HasFC DoStmt where getFC (DoExpr fc _) = fc getFC (DoArrow fc _ _ _) = fc getFC (DoLet fc _ _) = fcdata Decl : Udata Raw : U where RVar : (fc : FC) -> (nm : Name) -> Raw RLam : (fc : FC) -> BindInfo -> (sc : Raw) -> Raw RApp : (fc : FC) -> (t : Raw) -> (u : Raw) -> (icit : Icit) -> Raw RU : (fc : FC) -> Raw RImpossible : (fc : FC) -> Raw RPi : (fc : FC) -> BindInfo -> (ty : Raw) -> (sc : Raw) -> Raw RLet : (fc : FC) -> (nm : Name) -> (ty : Raw) -> (v : Raw) -> (sc : Raw) -> Raw RLit : (fc : FC) -> Literal -> Raw RCase : (fc : FC) -> (scrut : Raw) -> (mty : Maybe Raw) -> (alts : List RCaseAlt) -> Raw RImplicit : (fc : FC) -> Raw RHole : (fc : FC) -> Raw RDo : (fc : FC) -> List DoStmt -> Raw RIf : (fc : FC) -> Raw -> Raw -> Raw -> Raw RWhere : (fc : FC) -> (List Decl) -> Raw -> Raw RAs : (fc : FC) -> Name -> Raw -> Raw -- has to be applied or we have to know its type as Foo → Foo to elaborate. -- I can bake the arg in here, or require an app in elab. RUpdateRec : (fc : FC) → List UpdateClause → Maybe Raw → Rawinstance HasFC Raw where getFC (RVar fc nm) = fc getFC (RLam fc _ ty) = fc getFC (RApp fc t u icit) = fc getFC (RU fc) = fc getFC (RPi fc _ ty sc) = fc getFC (RLet fc nm ty v sc) = fc getFC (RLit fc y) = fc getFC (RCase fc scrut mty alts) = fc getFC (RImplicit fc) = fc getFC (RHole fc) = fc getFC (RDo fc stmts) = fc getFC (RIf fc _ _ _) = fc getFC (RWhere fc _ _) = fc getFC (RAs fc _ _) = fc getFC (RUpdateRec fc _ _) = fc getFC (RImpossible fc) = fcdata Import = MkImport FC (FC × Name)alias Telescope = List (BindInfo × Raw)data Decl = TypeSig FC Quant (List Name) Raw | FunDef FC Name (List (Raw × Maybe Raw)) | DCheck FC Raw Raw | DDerive FC (FC × String) (FC × String) | DAlias FC (FC × String) Telescope Raw -- TODO maybe add Telescope (before `:`) and auto-add to constructors... | Data FC (FC × Name) Raw (Maybe $ List Decl) | ShortData FC Raw (List Raw) | PType FC Name (Maybe Raw) | PFunc FC Name (List String) Raw String | PMixFix FC (List Name) Int Fixity | Class FC (FC × Name) Telescope (List Decl) | Instance FC Raw (Maybe (List Decl)) | Record FC (FC × Name) Telescope (Maybe $ FC × Name) (List Decl) | Exports FC (List $ FC × Name)instance HasFC Decl where getFC (TypeSig x _ strs tm) = x getFC (DAlias x _ _ _) = x getFC (Exports x _) = x getFC (FunDef x str xs) = x getFC (DCheck x tm tm1) = x getFC (Data x str tm xs) = x getFC (ShortData x _ _) = x getFC (PType x str mtm) = x getFC (PFunc x str _ tm str1) = x getFC (PMixFix x strs k y) = x getFC (Class x str xs ys) = x getFC (Instance x tm xs) = x getFC (Record x str tm str1 xs) = x getFC (DDerive x _ _) = xrecord Module where constructor MkModule modname : Name imports : List Import decls : List Declinstance Show Rawderive Show Importderive Show BindInfoderive Show DoStmtderive Show Declderive Show Modulederive Show RCaseAltderive Show UpdateClausederive Show Raw-- TODO fill in pretty printing---- We want to be able to print the entire file back out and get something usable.---- Ideally, it would be usable as a formatter. That means we need to handle infix and possibly push-- some desugaring to later. String comprehension, case let in do, maybe `$` (but handle LHS of pattern matching)instance Pretty Literal where -- FIXME quote properly pretty (LString t) = text "\"\{t}\"" pretty (LBool b) = if b then text "true" else text "false" pretty (LInt i) = text $ show i pretty (LChar c) = text $ show cwrap : Icit -> Doc -> Docwrap Explicit x = text "(" ++ x ++ text ")"wrap Implicit x = text "{" ++ x ++ text "}"wrap Auto x = text "{{" ++ x ++ text "}}"instance Pretty Pattern where pretty (PatVar _ Implicit str) = text str pretty (PatImpossible _) = text "()" pretty (PatVar _ icit str) = wrap icit $ text str pretty (PatCon _ icit nm args Nothing) = text (show nm) <+> spread (map pretty args) pretty (PatCon _ icit nm args (Just as)) = text as ++ text "@(" ++ text (show nm) <+> spread (map pretty args) ++ text ")" pretty (PatWild _ icit) = text "_" pretty (PatLit _ lit) = pretty litinstance Pretty Raw where pretty = asDoc 0 where bindDoc : BindInfo -> Doc bindDoc (BI _ nm icit quant) = text "BINDDOC" paren : Int -> Int -> Doc -> Doc paren p p' d = if p' < p then text "(" ++ d ++ text ")" else d asDoc : Int -> Raw -> Doc asDoc p (RVar _ str) = text str asDoc p (RLam _ (BI _ nm icit q) x) = paren p 0 $ text "\\" ++ wrap icit (text nm) <+> text "=>" <+> asDoc 0 x -- This needs precedence and operators... asDoc p (RApp _ x y Explicit) = paren p 2 $ asDoc 2 x <+> asDoc 3 y asDoc p (RApp _ x y Implicit) = paren p 2 $ asDoc 2 x <+> text "{" ++ asDoc 0 y ++ text "}" asDoc p (RApp _ x y Auto) = paren p 2 $ asDoc 2 x <+> text "{{" ++ asDoc 0 y ++ text "}}" asDoc p (RU _) = text "U" asDoc p (RPi _ (BI _ "_" Explicit Many) ty scope) = paren p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope asDoc p (RPi _ (BI _ nm icit quant) ty scope) = paren p 1 $ wrap icit (text (show quant ++ nm) <+> text ":" <+> asDoc p ty ) <+> text "->" <+/> asDoc 1 scope asDoc p (RLet _ x v ty scope) = paren p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty <+> text "=" <+> asDoc p v <+/> text "in" <+> asDoc p scope asDoc p (RLit _ lit) = pretty lit asDoc p (RCase fc sc mty alts) = --text "TODO - Pretty RCase" text "case" <+> nest 2 (asDoc 0 sc) <+> text "of" ++ nest 2 (line ++ stack (map caseAltDoc alts)) where caseAltDoc : RCaseAlt → Doc -- TODO we want a <+/> after the "=>" caseAltDoc (MkAlt lhs (Just rhs)) = asDoc 0 lhs <+> text "=>" ++ (nest 2 (asDoc 0 rhs)) caseAltDoc (MkAlt lhs Nothing) = asDoc 0 lhs asDoc p (RImplicit _) = text "_" asDoc p (RImpossible _) = text "()" asDoc p (RHole _) = text "?" asDoc p (RDo _ stmts) = text "do" ++ nest 2 (line ++ stack (map prettyDoStmt stmts)) where prettyDoStmt : DoStmt → Doc prettyDoStmt (DoExpr fc t) = asDoc 0 t prettyDoStmt (DoLet fc n t) = text "let" <+> text n <+> text "=" <+/> nest 2 (asDoc 0 t) prettyDoStmt (DoArrow fc lhs rhs alts) = go alts $ asDoc 0 lhs <+> text "<-" <+/> nest 2 (asDoc 0 rhs) where go : List RCaseAlt → Doc → Doc go Nil acc = acc go ((MkAlt lhs (Just rhs)) :: alts) acc = go alts $ acc ++ nest 2 (line ++ text "|" <+> asDoc 0 lhs <+> text "=>" <+> nest 2 (asDoc 0 rhs)) go ((MkAlt lhs Nothing) :: alts) acc = go alts $ acc ++ nest 2 (line ++ text "|" <+> asDoc 0 lhs) asDoc p (RIf _ x y z) = paren p 0 $ text "if" <+> asDoc 0 x <+/> text "then" <+> asDoc 0 y <+/> text "else" <+> asDoc 0 z asDoc p (RWhere _ dd b) = text "TODO pretty RWhere" asDoc p (RAs _ nm x) = text nm ++ text "@(" ++ asDoc 0 x ++ text ")" asDoc p (RUpdateRec _ clauses tm) = text "{" <+> text "TODO RUpdateRec" <+> text "}"prettyBind : (BindInfo × Raw) -> DocprettyBind (BI _ nm icit quant, ty) = wrap icit (text (show quant ++ nm) <+> text ":" <+> pretty ty)pipeSep : List Doc -> DocpipeSep = folddoc (\a b => a <+/> text "|" <+> b)instance Pretty Decl where pretty (TypeSig _ q nm ty) = text (show q) ++ spread (map text nm) <+> text ":" <+> nest 2 (pretty ty) pretty (DAlias _ nm args tm) = text "alias" <+> text (snd nm) <+> spread (map prettyBind args) <+> text "=" <+> pretty tm pretty (DDerive _ x y) = text "derive" <+> text (snd x) <+> text (snd y) pretty (FunDef _ nm clauses) = stack $ map prettyPair clauses where prettyPair : Raw × Maybe Raw → Doc prettyPair (a, Nothing) = pretty a prettyPair (a, Just b) = pretty a <+> text "=" <+> pretty b pretty (Data _ (_,nm) x Nothing) = text "data" <+> text nm <+> text ":" <+> pretty x pretty (Data _ (_,nm) x (Just xs)) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" </> stack (map pretty xs)) pretty (DCheck _ x y) = text "#check" <+> pretty x <+> text ":" <+> pretty y pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => text ":" <+> pretty ty) ty) pretty (PFunc _ nm Nil ty src) = text "pfunc" <+> text nm <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src)) pretty (PFunc _ nm used ty src) = text "pfunc" <+> text nm <+> text "uses" <+> spread (map text used) <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src)) pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names) pretty (Record _ (_,nm) tele (cname) decls) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele) <+> (nest 2 $ text "where" </> stack (maybe empty (\ nm' => text "constructor" <+> text (snd nm')) cname :: map pretty decls)) pretty (Class _ (_,nm) tele decls) = text "class" <+> text nm <+> text ":" <+> spread (map prettyBind tele) <+> (nest 2 $ text "where" </> stack (map pretty decls)) pretty (Instance fc top Nothing) = text "instance" <+> pretty top pretty (Instance fc top (Just decls)) = text "instance" <+> pretty top <+> nest 2 (text "where" </> stack (map pretty decls)) pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> text "=" <+> pipeSep (map pretty sigs) pretty (Exports _ nms) = text "#export" <+> spread (map (text ∘ show ∘ snd) nms)lhsNames : Raw → List StringlhsNames tm = case tm of RVar fc n => n :: Nil RAs _ n tm => n :: lhsNames tm RApp _ t u _ => lhsNames t ++ lhsNames u -- the rest have no names or don't occur on LHS _ => Nil-- used for the projection type in dependent records, probably overkill, but maybe it will be useful elsewhere-- TODO unit tests on substRawsubstRaw : List (String × Raw) → Raw → RawsubstRaw ss t = case t of RVar fc n => fromMaybe t (lookup n ss) (RUpdateRec fc uc target) => RUpdateRec fc (map substUC uc) (map (substRaw ss) target) -- LHS only (RAs fc nm t) => RAs fc nm (substRaw ss t) (RIf fc c t e) => RIf fc (substRaw ss c) (substRaw ss t) (substRaw ss e) (RLet fc nm ty v sc) => RLet fc nm (substRaw ss ty) (substRaw ss v) (substRaw ss sc) (RPi fc info a b) => RPi fc info (substRaw ss a) (substRaw (filterBind info ss) b) (RApp fc t u icit) => RApp fc (substRaw ss t) (substRaw ss u) icit (RLam fc info sc) => RLam fc info (substRaw (filterBind info ss) sc) -- FIXME shadowing (RWhere fc ds body) => RWhere fc (map substDecl ds) (substRaw ss body) (RDo fc stmts) => RDo fc (substStmts ss stmts) (RCase fc scrut mdef alts) => RCase fc (substRaw ss scrut) (map (substRaw ss) mdef) (map substAlt alts) -- Enumerate to force consideration of new cases t@(RImpossible _) => t t@(RU _) => t t@(RHole fc) => t t@(RImplicit fc) => t t@(RLit _ _) => t where -- Need to handle shadowing! filter : ∀ a. List String → List (String × a) → List (String × a) filter nms Nil = Nil filter nms (x@(a,b) :: xs) = if elem a nms then filter nms xs else x :: filter nms xs filterBind : ∀ a. BindInfo → List (String × a) → List (String × a) filterBind (BI fc nm _ _) xs = filter (nm :: Nil) xs substUC : UpdateClause → UpdateClause substUC (AssignField fc nm t) = AssignField fc nm (substRaw ss t) substUC (ModifyField fc nm t) = ModifyField fc nm (substRaw ss t) substClause : Raw × Maybe Raw → Raw × Maybe Raw substClause (a,b) = (substRaw ss a, map (substRaw ss) b) substDecl : Decl → Decl substDecl (TypeSig fc q nms ty) = TypeSig fc q nms (substRaw ss ty) substDecl (FunDef fc nm clauses) = FunDef fc nm $ map substClause clauses substDecl d = d -- shouldn't happen substAlt : RCaseAlt → RCaseAlt substAlt (MkAlt a b) = MkAlt (substRaw ss a) (map (substRaw (filter (lhsNames a) ss)) b) substStmts : List (String × Raw) → List DoStmt → List DoStmt substStmts ss Nil = Nil substStmts ss (DoExpr fc t :: rest) = DoExpr fc (substRaw ss t) :: substStmts ss rest substStmts ss (DoArrow fc pat sc alts :: rest) = DoArrow fc (substRaw ss pat) (substRaw ss sc) (map (substAlt) alts) :: substStmts (filter (lhsNames pat) ss) rest substStmts ss (DoLet fc nm t :: rest) = DoLet fc nm (substRaw ss t) :: substStmts (filter (nm :: Nil) ss) restinstance Pretty Module where pretty (MkModule name imports decls) = text "module" <+> text name </> stack (map doImport imports) </> stack (map pretty decls) where doImport : Import -> Doc doImport (MkImport _ (_,nm)) = text "import" <+> text nm ++ line