From c1ebc0535d868c7108b76a265fe09a9184b4253c Mon Sep 17 00:00:00 2001 From: "G. Allais" Date: Fri, 13 Aug 2021 16:00:54 +0100 Subject: [PATCH] [ new ] semantic highlighting in REPL & holes (#1836) --- idris2api.ipkg | 1 + src/Core/Metadata.idr | 15 + src/Core/TT.idr | 9 + src/Idris/Doc/String.idr | 138 +++--- src/Idris/Elab/Implementation.idr | 3 +- src/Idris/Error.idr | 3 +- src/Idris/IDEMode/CaseSplit.idr | 7 +- src/Idris/IDEMode/Holes.idr | 4 +- src/Idris/Parser.idr | 15 +- src/Idris/Pretty.idr | 119 +++-- src/Idris/REPL.idr | 47 +- src/Idris/REPL/Common.idr | 8 +- src/Idris/Resugar.idr | 140 +++--- src/Idris/Syntax.idr | 653 +++++++++++++++------------ src/Parser/Lexer/Source.idr | 6 +- src/TTImp/Elab/RunElab.idr | 9 +- src/TTImp/Interactive/CaseSplit.idr | 5 +- src/TTImp/Interactive/ExprSearch.idr | 5 +- src/TTImp/Interactive/MakeLemma.idr | 5 +- src/TTImp/PartialEval.idr | 13 +- src/TTImp/ProcessDef.idr | 2 + src/TTImp/ProcessRecord.idr | 3 +- src/TTImp/TTImp.idr | 285 +++++++----- src/TTImp/TTImp/Functor.idr | 160 +++++++ src/TTImp/Unelab.idr | 60 +-- tests/idris2/coverage004/expected | 2 +- tests/idris2/docs001/expected | 9 +- tests/idris2/docs002/expected | 3 - tests/idris2/docs003/expected | 2 +- tests/idris2/interactive030/expected | 2 + tests/idris2/perf005/expected | 9 +- tests/idris2/pretty001/expected | 6 +- tests/idris2/reflection002/expected | 2 +- 33 files changed, 1094 insertions(+), 656 deletions(-) create mode 100644 src/TTImp/TTImp/Functor.idr diff --git a/idris2api.ipkg b/idris2api.ipkg index ee4e397ad..0ef1ad721 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -199,6 +199,7 @@ modules = TTImp.ProcessType, TTImp.Reflect, TTImp.TTImp, + TTImp.TTImp.Functor, TTImp.Unelab, TTImp.Utils, TTImp.WithClause, diff --git a/src/Core/Metadata.idr b/src/Core/Metadata.idr index 60cb8819c..c218ad7d5 100644 --- a/src/Core/Metadata.idr +++ b/src/Core/Metadata.idr @@ -34,6 +34,21 @@ nameTypeDecoration Func = Function nameTypeDecoration (DataCon _ _) = Data nameTypeDecoration (TyCon _ _ ) = Typ +export +defDecoration : Def -> Maybe Decoration +defDecoration None = Nothing +defDecoration (PMDef {}) = Just Function +defDecoration (ExternDef {}) = Just Function +defDecoration (ForeignDef {}) = Just Function +defDecoration (Builtin {}) = Just Function +defDecoration (DCon {}) = Just Data +defDecoration (TCon {}) = Just Typ +defDecoration (Hole {}) = Just Function +defDecoration (BySearch {}) = Nothing +defDecoration (Guess {}) = Nothing +defDecoration ImpBind = Just Bound +defDecoration Delayed = Nothing + public export ASemanticDecoration : Type ASemanticDecoration = (NonEmptyFC, Decoration, Maybe Name) diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 7081fdcfa..d1138583d 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -29,6 +29,15 @@ isCon (DataCon t a) = Just (t, a) isCon (TyCon t a) = Just (t, a) isCon _ = Nothing +public export +record KindedName where + constructor MkKindedName + nameKind : Maybe NameType + rawName : Name + +export +Show KindedName where show = show . rawName + public export data Constant = I Int diff --git a/src/Idris/Doc/String.idr b/src/Idris/Doc/String.idr index ea1aa4bc0..ac738e500 100644 --- a/src/Idris/Doc/String.idr +++ b/src/Idris/Doc/String.idr @@ -4,6 +4,7 @@ import Core.Context import Core.Context.Log import Core.Core import Core.Env +import Core.Metadata import Core.TT import Idris.Pretty @@ -13,6 +14,7 @@ import Idris.Resugar import Idris.Syntax import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Elab.Prim import Data.List @@ -50,6 +52,7 @@ styleAnn (TCon _) = color BrightBlue styleAnn DCon = color BrightRed styleAnn (Fun _) = color BrightGreen styleAnn Header = underline +styleAnn (Syntax syn) = syntaxAnn syn styleAnn _ = [] export @@ -99,17 +102,51 @@ addDocStringNS ns n_in doc put Syn (record { docstrings $= addName n' doc, saveDocstrings $= insert n' () } syn) +prettyTerm : IPTerm -> Doc IdrisDocAnn +prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm + +showCategory : GlobalDef -> Doc IdrisDocAnn -> Doc IdrisDocAnn +showCategory d = case defDecoration (definition d) of + Nothing => id + Just decor => annotate (Syntax $ SynDecor decor) + +prettyName : Name -> Doc IdrisDocAnn +prettyName n = + let root = nameRoot n in + if isOpName n then parens (pretty root) else pretty root + export getDocsForPrimitive : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Constant -> Core (List String) + Constant -> Core (Doc IdrisDocAnn) getDocsForPrimitive constant = do let (_, type) = checkPrim EmptyFC constant - let typeString = show constant ++ " : " ++ show !(resugar [] type) - pure [typeString ++ "\n\tPrimitive"] + let typeString = pretty (show constant) + <++> colon <++> prettyTerm !(resugar [] type) + pure (typeString <+> Line <+> indent 2 "Primitive") -prettyTerm : PTerm -> Doc IdrisDocAnn -prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm +data Config : Type where + ||| Configuration of the printer for a name + ||| @ longNames Do we print qualified names? + ||| @ dropFirst Do we drop the first argument in the type? + ||| @ getTotality Do we print the totality status of the function? + MkConfig : {default True longNames : Bool} -> + {default False dropFirst : Bool} -> + {default True getTotality : Bool} -> + Config + +||| Printer configuration for interface methods +||| * longNames turned off for interface methods because the namespace is +||| already spelt out for the interface itself +||| * dropFirst turned on for interface methods because the first argument +||| is always the interface constraint +||| * totality turned off for interface methods because the methods themselves +||| are just projections out of a record and so are total +methodsConfig : Config +methodsConfig + = MkConfig {longNames = False} + {dropFirst = True} + {getTotality = False} export getDocsForName : {auto o : Ref ROpts REPLOpts} -> @@ -127,10 +164,12 @@ getDocsForName fc n | _ => undefinedName fc n let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn)) all | [] => pure $ pretty ("No documentation for " ++ show n) - docs <- traverse showDoc ns + docs <- traverse (showDoc MkConfig) ns pure $ vcat (punctuate Line docs) where + showDoc : Config -> (Name, String) -> Core (Doc IdrisDocAnn) + -- Avoid generating too much whitespace by not returning a single empty line reflowDoc : String -> List (Doc IdrisDocAnn) reflowDoc "" = [] @@ -142,11 +181,6 @@ getDocsForName fc n Unchecked => "" _ => header "Totality" <++> pretty tot - prettyName : Name -> Doc IdrisDocAnn - prettyName n = - let root = nameRoot n in - if isOpName n then parens (pretty root) else pretty root - getDConDoc : Name -> Core (Doc IdrisDocAnn) getDConDoc con = do defs <- get Ctxt @@ -156,12 +190,13 @@ getDocsForName fc n syn <- get Syn ty <- resugar [] =<< normaliseHoles defs [] (type def) let conWithTypeDoc = annotate (Decl con) (hsep [dCon (prettyName con), colon, prettyTerm ty]) - let [(n, str)] = lookupName con (docstrings syn) - | _ => pure conWithTypeDoc - pure $ vcat - [ conWithTypeDoc - , annotate DocStringBody $ vcat $ reflowDoc str - ] + case lookupName con (docstrings syn) of + [(n, "")] => pure conWithTypeDoc + [(n, str)] => pure $ vcat + [ conWithTypeDoc + , annotate DocStringBody $ vcat $ reflowDoc str + ] + _ => pure conWithTypeDoc getImplDoc : Name -> Core (List (Doc IdrisDocAnn)) getImplDoc n @@ -174,16 +209,9 @@ getDocsForName fc n getMethDoc : Method -> Core (List (Doc IdrisDocAnn)) getMethDoc meth = do syn <- get Syn - let [(n, str)] = lookupName meth.name (docstrings syn) + let [nstr] = lookupName meth.name (docstrings syn) | _ => pure [] - ty <- pterm meth.type - let nm = prettyName meth.name - pure $ pure $ vcat [ - annotate (Decl meth.name) (hsep [fun (meth.name) nm, colon, prettyTerm ty]) - , annotate DocStringBody $ vcat ( - toList (indent 2 . pretty . show <$> meth.totalReq) - ++ reflowDoc str) - ] + pure <$> showDoc methodsConfig nstr getInfixDoc : Name -> Core (List (Doc IdrisDocAnn)) getInfixDoc n @@ -217,9 +245,12 @@ getDocsForName fc n [] => [] ps => [hsep (header "Parameters" :: punctuate comma (map (pretty . show) ps))] let constraints = - case !(traverse pterm (parents iface)) of + case !(traverse (pterm . map (MkKindedName Nothing)) (parents iface)) of [] => [] ps => [hsep (header "Constraints" :: punctuate comma (map (pretty . show) ps))] + let icon = case dropNS (iconstructor iface) of + DN _ _ => [] -- machine inserted + nm => [hsep [header "Constructor", dCon (prettyName nm)]] mdocs <- traverse getMethDoc (methods iface) let meths = case concat mdocs of [] => [] @@ -233,7 +264,7 @@ getDocsForName fc n [doc] => [header "Implementation" <++> annotate Declarations doc] docs => [vcat [header "Implementations" , annotate Declarations $ vcat $ map (indent 2) docs]] - pure (vcat (params ++ constraints ++ meths ++ insts)) + pure (vcat (params ++ constraints ++ icon ++ meths ++ insts)) getFieldDoc : Name -> Core (Doc IdrisDocAnn) getFieldDoc nm @@ -243,7 +274,7 @@ getDocsForName fc n -- should never happen, since we know that the DCon exists: | Nothing => pure Empty ty <- resugar [] =<< normaliseHoles defs [] (type def) - let prettyName = pretty (nameRoot nm) + let prettyName = prettyName nm let projDecl = annotate (Decl nm) $ hsep [ fun nm prettyName, colon, prettyTerm ty ] case lookupName nm (docstrings syn) of [(_, "")] => pure projDecl @@ -290,26 +321,24 @@ getDocsForName fc n pure (tot ++ cdoc) _ => pure [] - showCategory : GlobalDef -> Doc IdrisDocAnn -> Doc IdrisDocAnn - showCategory d = case definition d of - TCon _ _ _ _ _ _ _ _ => tCon (fullname d) - DCon _ _ _ => dCon - PMDef _ _ _ _ _ => fun (fullname d) - ForeignDef _ _ => fun (fullname d) - Builtin _ => fun (fullname d) - _ => id - - showDoc : (Name, String) -> Core (Doc IdrisDocAnn) - showDoc (n, str) + showDoc (MkConfig {longNames, dropFirst, getTotality}) (n, str) = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | Nothing => undefinedName fc n ty <- resugar [] =<< normaliseHoles defs [] (type def) + -- when printing e.g. interface methods there is no point in + -- repeating the interface's name + let ty = ifThenElse (not dropFirst) ty $ case ty of + PPi _ _ AutoImplicit _ _ sc => sc + _ => ty let cat = showCategory def nm <- aliasName n - let docDecl = annotate (Decl n) (hsep [cat (pretty (show nm)), colon, prettyTerm ty]) + -- when printing e.g. interface methods there is no point in + -- repeating the namespace the interface lives in + let nm = if longNames then pretty (show nm) else prettyName nm + let docDecl = annotate (Decl n) (hsep [cat nm, colon, prettyTerm ty]) let docText = reflowDoc str - extra <- getExtra n def + extra <- ifThenElse getTotality (getExtra n def) (pure []) fixes <- getFixityDoc n let docBody = annotate DocStringBody $ vcat $ docText ++ (map (indent 2) (extra ++ fixes)) pure (vcat [docDecl, docBody]) @@ -320,7 +349,8 @@ getDocsForPTerm : {auto o : Ref ROpts REPLOpts} -> {auto s : Ref Syn SyntaxInfo} -> PTerm -> Core (List String) getDocsForPTerm (PRef fc name) = pure $ [!(render styleAnn !(getDocsForName fc name))] -getDocsForPTerm (PPrimVal _ constant) = getDocsForPrimitive constant +getDocsForPTerm (PPrimVal _ constant) + = pure [!(render styleAnn !(getDocsForPrimitive constant))] getDocsForPTerm (PType _) = pure ["Type : Type\n\tThe type of all types is Type. The type of Type is Type."] getDocsForPTerm (PString _ _) = pure ["String Literal\n\tDesugars to a fromString call"] getDocsForPTerm (PList _ _ _) = pure ["List Literal\n\tDesugars to (::) and Nil"] @@ -332,24 +362,26 @@ getDocsForPTerm pterm = pure ["Docs not implemented for " ++ show pterm ++ " yet summarise : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Name -> Core String + Name -> Core (Doc IdrisDocAnn) summarise n -- n is fully qualified = do syn <- get Syn defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | _ => pure "" - let doc = case lookupName n (docstrings syn) of - [(_, doc)] => case Extra.lines doc of - ("" ::: _) => Nothing - (d ::: _) => Just d - _ => Nothing + -- let doc = case lookupName n (docstrings syn) of + -- [(_, doc)] => case Extra.lines doc of + -- ("" ::: _) => Nothing + -- (d ::: _) => Just d + -- _ => Nothing ty <- normaliseHoles defs [] (type def) - pure (nameRoot n ++ " : " ++ show !(resugar [] ty) ++ - maybe "" ((++) "\n\t") doc) + pure $ showCategory def (prettyName n) + <++> colon <++> hang 0 (prettyTerm !(resugar [] ty)) +-- <+> maybe "" ((Line <+>) . indent 2 . pretty) doc) -- Display all the exported names in the given namespace export -getContents : {auto c : Ref Ctxt Defs} -> +getContents : {auto o : Ref ROpts REPLOpts} -> + {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> Namespace -> Core (List String) getContents ns @@ -359,7 +391,7 @@ getContents ns ns <- allNames (gamma defs) let allNs = filter inNS ns allNs <- filterM (visible defs) allNs - traverse summarise (sort allNs) + traverse (\ ns => render styleAnn !(summarise ns)) (sort allNs) where visible : Defs -> Name -> Core Bool visible defs n diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index 45c73890f..74770b3a5 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -17,6 +17,7 @@ import TTImp.Elab import TTImp.Elab.Check import TTImp.ProcessDecls import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Unelab import TTImp.Utils @@ -101,7 +102,7 @@ getMethImps : {vars : _} -> Env Term vars -> Term vars -> Core (List (Name, RigCount, RawImp)) getMethImps env (Bind fc x (Pi fc' c Implicit ty) sc) - = do rty <- unelabNoSugar env ty + = do rty <- map (map rawName) $ unelabNoSugar env ty ts <- getMethImps (Pi fc' c Implicit ty :: env) sc pure ((x, c, rty) :: ts) getMethImps env tm = pure [] diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index ee98b0185..0f7f3cfb4 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -4,6 +4,7 @@ import Core.CaseTree import Core.Core import Core.Context import Core.Env +import Core.Metadata import Core.Options import Core.Value @@ -38,7 +39,7 @@ import System.File %default covering keyword : Doc IdrisAnn -> Doc IdrisAnn -keyword = annotate (Syntax SynKeyword) +keyword = annotate (Syntax $ SynDecor Keyword) -- | Add binding site information if the term is simply a machine-inserted name pShowMN : {vars : _} -> Term vars -> Env t vars -> Doc IdrisAnn -> Doc IdrisAnn diff --git a/src/Idris/IDEMode/CaseSplit.idr b/src/Idris/IDEMode/CaseSplit.idr index 02ebe665a..8fc2b2811 100644 --- a/src/Idris/IDEMode/CaseSplit.idr +++ b/src/Idris/IDEMode/CaseSplit.idr @@ -12,6 +12,7 @@ import Parser.Unlit import TTImp.Interactive.CaseSplit import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Utils import Idris.IDEMode.TokenLine @@ -44,10 +45,10 @@ toStrUpdate : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> (Name, RawImp) -> Core Updates toStrUpdate (UN n, term) - = do clause <- pterm term + = do clause <- pterm (map (MkKindedName Nothing) term) -- hack pure [(n, show (bracket clause))] where - bracket : PTerm -> PTerm + bracket : PTerm' nm -> PTerm' nm bracket tm@(PRef _ _) = tm bracket tm@(PList _ _ _) = tm bracket tm@(PSnocList _ _ _) = tm @@ -146,7 +147,7 @@ showImpossible : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> (indent : Nat) -> RawImp -> Core String showImpossible indent lhs - = do clause <- pterm lhs + = do clause <- pterm (map (MkKindedName Nothing) lhs) -- hack pure (fastPack (replicate indent ' ') ++ show clause ++ " impossible") -- Given a list of updates and a line and column, find the relevant line in diff --git a/src/Idris/IDEMode/Holes.idr b/src/Idris/IDEMode/Holes.idr index cb5b94b61..a4c0c894a 100644 --- a/src/Idris/IDEMode/Holes.idr +++ b/src/Idris/IDEMode/Holes.idr @@ -18,7 +18,7 @@ public export record HolePremise where constructor MkHolePremise name : Name - type : PTerm + type : IPTerm multiplicity : RigCount isImplicit : Bool @@ -27,7 +27,7 @@ public export record HoleData where constructor MkHoleData name : Name - type : PTerm + type : IPTerm context : List HolePremise ||| If input is a hole, return number of locals in scope at binding diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index aeaf23ec4..6dc928571 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1093,12 +1093,13 @@ simpleData : OriginDesc -> WithBounds t -> simpleData fname start tyName indents = do b <- bounds (do params <- many (bounds $ decorate fname Bound name) tyend <- bounds (decoratedSymbol fname "=") - let tyfc = boundToFC fname (mergeBounds start tyend) - let tyCon = PRef (boundToFC fname tyName) tyName.val - let toPRef = \ t => PRef (boundToFC fname t) t.val - let conRetTy = papply tyfc tyCon (map toPRef params) - cons <- sepBy1 (decoratedSymbol fname "|") (simpleCon fname conRetTy indents) - pure (params, tyfc, forget cons)) + mustWork $ do + let tyfc = boundToFC fname (mergeBounds start tyend) + let tyCon = PRef (boundToFC fname tyName) tyName.val + let toPRef = \ t => PRef (boundToFC fname t) t.val + let conRetTy = papply tyfc tyCon (map toPRef params) + cons <- sepBy1 (decoratedSymbol fname "|") (simpleCon fname conRetTy indents) + pure (params, tyfc, forget cons)) (params, tyfc, cons) <- pure b.val pure (MkPData (boundToFC fname (mergeBounds start b)) tyName.val (mkTyConType fname tyfc params) [] cons) @@ -1126,7 +1127,7 @@ dataBody fname mincol start n indents ty gadtData : OriginDesc -> Int -> WithBounds t -> WithBounds Name -> IndentInfo -> Rule PDataDecl gadtData fname mincol start tyName indents - = do decoratedSymbol fname ":" + = do mustWork $ decoratedSymbol fname ":" commit ty <- typeExpr pdef fname indents dataBody fname mincol start tyName.val indents ty diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index c734f4a85..0201f97ca 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -1,5 +1,6 @@ module Idris.Pretty +import Core.Metadata import Data.List import Data.Maybe import Data.String @@ -21,7 +22,7 @@ import Idris.Syntax public export data IdrisSyntax = SynHole - | SynKeyword + | SynDecor Decoration | SynPragma | SynRef Name @@ -35,6 +36,21 @@ data IdrisAnn | Meta | Syntax IdrisSyntax +export +decorAnn : Decoration -> AnsiStyle +decorAnn Keyword = color BrightWhite +decorAnn Typ = color BrightBlue +decorAnn Data = color BrightRed +decorAnn Function = color BrightGreen +decorAnn Bound = italic + +export +syntaxAnn : IdrisSyntax -> AnsiStyle +syntaxAnn SynHole = color BrightGreen +syntaxAnn (SynDecor decor) = decorAnn decor +syntaxAnn SynPragma = color BrightMagenta +syntaxAnn (SynRef _) = [] + export colorAnn : IdrisAnn -> AnsiStyle colorAnn Warning = color Yellow <+> bold @@ -43,10 +59,7 @@ colorAnn ErrorDesc = bold colorAnn FileCtxt = color BrightBlue colorAnn Code = color Magenta colorAnn Meta = color Green -colorAnn (Syntax SynHole) = color Green -colorAnn (Syntax SynKeyword) = color Red -colorAnn (Syntax SynPragma) = color BrightMagenta -colorAnn (Syntax (SynRef _)) = [] +colorAnn (Syntax syn) = syntaxAnn syn export warning : Doc IdrisAnn -> Doc IdrisAnn @@ -66,7 +79,7 @@ fileCtxt = annotate FileCtxt export keyword : Doc IdrisSyntax -> Doc IdrisSyntax -keyword = annotate SynKeyword +keyword = annotate (SynDecor Keyword) export meta : Doc IdrisAnn -> Doc IdrisAnn @@ -124,7 +137,7 @@ prettyRig = elimSemi (pretty '0' <+> space) (const emptyDoc) mutual - prettyAlt : PClause -> Doc IdrisSyntax + prettyAlt : PClause' KindedName -> Doc IdrisSyntax prettyAlt (MkPatClause _ lhs rhs _) = space <+> pipe <++> prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs <+> semi prettyAlt (MkWithClause _ lhs wval prf flags cs) = @@ -132,7 +145,7 @@ mutual prettyAlt (MkImpossible _ lhs) = space <+> pipe <++> prettyTerm lhs <++> impossible_ <+> semi - prettyCase : PClause -> Doc IdrisSyntax + prettyCase : PClause' KindedName -> Doc IdrisSyntax prettyCase (MkPatClause _ lhs rhs _) = prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs prettyCase (MkWithClause _ lhs rhs prf flags _) = @@ -140,11 +153,11 @@ mutual prettyCase (MkImpossible _ lhs) = prettyTerm lhs <++> impossible_ - prettyString : PStr -> Doc IdrisSyntax + prettyString : PStr' KindedName -> Doc IdrisSyntax prettyString (StrLiteral _ str) = pretty str prettyString (StrInterp _ tm) = prettyTerm tm - prettyDo : PDo -> Doc IdrisSyntax + prettyDo : PDo' KindedName -> Doc IdrisSyntax prettyDo (DoExp _ tm) = prettyTerm tm prettyDo (DoBind _ _ n tm) = pretty n <++> pretty "<-" <++> prettyTerm tm prettyDo (DoBindPat _ l tm alts) = @@ -157,14 +170,17 @@ mutual let_ <++> braces (angles (angles (pretty "definitions"))) prettyDo (DoRewrite _ rule) = rewrite_ <+> prettyTerm rule - prettyUpdate : PFieldUpdate -> Doc IdrisSyntax + prettyUpdate : PFieldUpdate' KindedName -> Doc IdrisSyntax prettyUpdate (PSetField path v) = concatWith (surround dot) (pretty <$> path) <++> equals <++> prettyTerm v prettyUpdate (PSetFieldApp path v) = concatWith (surround dot) (pretty <$> path) <++> pretty '$' <+> equals <++> prettyTerm v + prettyBinder : Name -> Doc IdrisSyntax + prettyBinder = annotate (SynDecor Bound) . pretty + export - prettyTerm : PTerm -> Doc IdrisSyntax + prettyTerm : IPTerm -> Doc IdrisSyntax prettyTerm = go Open where startPrec : Prec @@ -178,47 +194,68 @@ mutual then annotate (SynRef op) $ pretty op else Chara '`' <+> annotate (SynRef op) (pretty op) <+> Chara '`' - go : Prec -> PTerm -> Doc IdrisSyntax - go d (PRef _ n) = annotate (SynRef n) $ pretty n + go : Prec -> IPTerm -> Doc IdrisSyntax + go d (PRef _ (MkKindedName mnt n)) + = maybe id (annotate . SynDecor . nameTypeDecoration) mnt + $ annotate (SynRef n) $ pretty n go d (PPi _ rig Explicit Nothing arg ret) = parenthesise (d > startPrec) $ group $ branchVal (go startPrec arg <++> "->" <++> go startPrec ret) - (parens (prettyRig rig <+> "_" <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret) + (parens (prettyRig rig <+> "_" <++> colon <++> go startPrec arg) + <++> "->" <+> softline <+> go startPrec ret) rig go d (PPi _ rig Explicit (Just n) arg ret) = parenthesise (d > startPrec) $ group $ - parens (prettyRig rig <+> pretty n <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret + parens (prettyRig rig <+> prettyBinder n + <++> colon <++> go startPrec arg) + <++> "->" <+> softline <+> go startPrec ret go d (PPi _ rig Implicit Nothing arg ret) = parenthesise (d > startPrec) $ group $ - braces (prettyRig rig <+> pretty '_' <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret + braces (prettyRig rig <+> pretty '_' + <++> colon <++> go startPrec arg) + <++> "->" <+> softline <+> go startPrec ret go d (PPi _ rig Implicit (Just n) arg ret) = parenthesise (d > startPrec) $ group $ - braces (prettyRig rig <+> pretty n <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret + braces (prettyRig rig <+> prettyBinder n + <++> colon <++> go startPrec arg) + <++> "->" <+> softline <+> go startPrec ret go d (PPi _ rig AutoImplicit Nothing arg ret) = parenthesise (d > startPrec) $ group $ branchVal - (go startPrec arg <++> "=>" <+> line <+> go startPrec ret) - (braces (auto_ <++> prettyRig rig <+> "_" <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret) + (go startPrec arg <++> "=>" <+> softline <+> go startPrec ret) + (braces (auto_ <++> prettyRig rig <+> "_" + <++> colon <++> go startPrec arg) + <++> "->" <+> softline <+> go startPrec ret) rig go d (PPi _ rig AutoImplicit (Just n) arg ret) = parenthesise (d > startPrec) $ group $ - braces (auto_ <++> prettyRig rig <+> pretty n <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret + braces (auto_ <++> prettyRig rig <+> prettyBinder n + <++> colon <++> go startPrec arg) + <++> "->" <+> softline <+> go startPrec ret go d (PPi _ rig (DefImplicit t) Nothing arg ret) = parenthesise (d > startPrec) $ group $ - braces (default_ <++> go appPrec t <++> prettyRig rig <+> "_" <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret + braces (default_ <++> go appPrec t <++> prettyRig rig <+> "_" + <++> colon <++> go startPrec arg) + <++> "->" <+> softline <+> go startPrec ret go d (PPi _ rig (DefImplicit t) (Just n) arg ret) = parenthesise (d > startPrec) $ group $ - braces (default_ <++> go appPrec t <++> prettyRig rig <+> pretty n <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret + braces (default_ <++> go appPrec t + <++> prettyRig rig <+> prettyBinder n + <++> colon <++> go startPrec arg) + <++> "->" <+> softline <+> go startPrec ret go d (PLam _ rig _ n ty sc) = let (ns, sc) = getLamNames [(rig, n, ty)] sc in - parenthesise (d > startPrec) $ group $ align $ hang 2 $ - backslash <+> prettyBindings ns <++> "=>" <+> line <+> go startPrec sc + parenthesise (d > startPrec) $ group $ + backslash <+> prettyBindings ns <++> "=>" <+> softline <+> go startPrec sc where - getLamNames : List (RigCount, PTerm, PTerm) -> PTerm -> (List (RigCount, PTerm, PTerm), PTerm) + getLamNames : List (RigCount, IPTerm, IPTerm) -> + IPTerm -> + (List (RigCount, IPTerm, IPTerm), IPTerm) getLamNames acc (PLam _ rig _ n ty sc) = getLamNames ((rig, n, ty) :: acc) sc getLamNames acc sc = (reverse acc, sc) - prettyBindings : List (RigCount, PTerm, PTerm) -> Doc IdrisSyntax + + prettyBindings : List (RigCount, IPTerm, IPTerm) -> Doc IdrisSyntax prettyBindings [] = neutral prettyBindings [(rig, n, (PImplicit _))] = prettyRig rig <+> go startPrec n prettyBindings [(rig, n, ty)] = prettyRig rig <+> go startPrec n <++> colon <++> go startPrec ty @@ -254,8 +291,8 @@ mutual let_ <++> (group $ align $ hang 2 $ prettyRig rig <+> go startPrec n <++> equals <+> line <+> go startPrec val) <+> line <+> in_ <++> (group $ align $ hang 2 $ continuation) - getPRefName : PTerm -> Maybe Name - getPRefName (PRef _ n) = Just n + getPRefName : IPTerm -> Maybe Name + getPRefName (PRef _ n) = Just (rawName n) getPRefName _ = Nothing go d (PLet _ rig n ty val sc alts) = @@ -276,7 +313,7 @@ mutual in parenthesise (d > appPrec) $ group $ case f of (PRef _ n) => - if isJust (isRF n) + if isJust (isRF $ rawName n) then go leftAppPrec a <++> go appPrec f else catchall _ => catchall @@ -289,9 +326,9 @@ mutual parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> "@" <+> braces (go startPrec a) go d (PNamedApp _ f n (PRef _ a)) = parenthesise (d > appPrec) $ group $ - if n == a + if n == rawName a then go leftAppPrec f <++> braces (pretty n) - else go leftAppPrec f <++> braces (pretty n <++> equals <++> pretty a) + else go leftAppPrec f <++> braces (pretty n <++> equals <++> pretty a.rawName) go d (PNamedApp _ f n a) = parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> braces (pretty n <++> equals <++> go d a) go d (PSearch _ _) = pragma "%search" @@ -300,13 +337,15 @@ mutual go d (PQuoteDecl _ tm) = parenthesise (d > appPrec) $ "`" <+> brackets (angles (angles (pretty "declaration"))) go d (PUnquote _ tm) = parenthesise (d > appPrec) $ "~" <+> parens (go startPrec tm) go d (PRunElab _ tm) = parenthesise (d > appPrec) $ pragma "%runElab" <++> go startPrec tm - go d (PPrimVal _ c) = pretty c + go d (PPrimVal _ c) = + let decor = if isPrimType c then Typ else Data in + annotate (SynDecor decor) $ pretty c go d (PHole _ _ n) = hole (pretty (strCons '?' n)) - go d (PType _) = pretty "Type" + go d (PType _) = annotate (SynDecor Typ) "Type" go d (PAs _ _ n p) = pretty n <+> "@" <+> go d p go d (PDotted _ p) = dot <+> go d p go d (PImplicit _) = "_" - go d (PInfer _) = "?" + go d (PInfer _) = annotate SynHole $ "?" go d (POp _ _ op x y) = parenthesise (d > appPrec) $ group $ go startPrec x <++> prettyOp op <++> go startPrec y go d (PPrefixOp _ _ op x) = parenthesise (d > appPrec) $ pretty op <+> go startPrec x go d (PSectionL _ _ op x) = parens (prettyOp op <++> go startPrec x) @@ -331,12 +370,14 @@ mutual go d (PComprehension _ ret es) = group $ brackets (go startPrec (dePure ret) <++> pipe <++> vsep (punctuate comma (prettyDo . deGuard <$> es))) where - dePure : PTerm -> PTerm - dePure tm@(PApp _ (PRef _ n) arg) = if dropNS n == UN "pure" then arg else tm + dePure : IPTerm -> IPTerm + dePure tm@(PApp _ (PRef _ n) arg) + = if dropNS (rawName n) == UN "pure" then arg else tm dePure tm = tm - deGuard : PDo -> PDo - deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg)) = if dropNS n == UN "guard" then DoExp fc arg else tm + deGuard : PDo' KindedName -> PDo' KindedName + deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg)) + = if dropNS (rawName n) == UN "guard" then DoExp fc arg else tm deGuard tm = tm go d (PRewrite _ rule tm) = parenthesise (d > appPrec) $ group $ rewrite_ <++> go startPrec rule <+> line <+> in_ <++> go startPrec tm diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 0ebf157a7..bdcd28197 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -48,6 +48,7 @@ import Idris.Version import public Idris.REPL.Common import Idris.REPL.FuzzySearch +import TTImp.TTImp.Functor import TTImp.Elab import TTImp.Elab.Check import TTImp.Elab.Local @@ -110,7 +111,7 @@ showInfo (n, idx, d) coreLift_ $ putStrLn $ "Size change: " ++ showSep ", " scinfo -prettyTerm : PTerm -> Doc IdrisAnn +prettyTerm : IPTerm -> Doc IdrisAnn prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm displayType : {auto c : Ref Ctxt Defs} -> @@ -119,7 +120,10 @@ displayType : {auto c : Ref Ctxt Defs} -> Core (Doc IdrisAnn) displayType defs (n, i, gdef) = maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef)) - pure (pretty !(aliasName (fullname gdef)) <++> colon <++> prettyTerm tm)) + nm <- aliasName (fullname gdef) + let ann = maybe id (annotate . Syntax . SynDecor) + $ defDecoration $ definition gdef + pure (ann (pretty nm) <++> colon <++> prettyTerm tm)) (\num => reAnnotate Syntax <$> prettyHole defs [] n num (type gdef)) (isHole gdef) @@ -215,12 +219,12 @@ printClause : {auto c : Ref Ctxt Defs} -> Maybe String -> Nat -> ImpClause -> Core String printClause l i (PatClause _ lhsraw rhsraw) - = do lhs <- pterm lhsraw - rhs <- pterm rhsraw + = do lhs <- pterm $ map (MkKindedName Nothing) lhsraw -- hack + rhs <- pterm $ map (MkKindedName Nothing) rhsraw -- hack pure (relit l (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs)) printClause l i (WithClause _ lhsraw wvraw prf flags csraw) - = do lhs <- pterm lhsraw - wval <- pterm wvraw + = do lhs <- pterm $ map (MkKindedName Nothing) lhsraw -- hack + wval <- pterm $ map (MkKindedName Nothing) wvraw -- hack cs <- traverse (printClause l (i + 2)) csraw pure (relit l ((pack (replicate i ' ') ++ show lhs @@ -229,7 +233,7 @@ printClause l i (WithClause _ lhsraw wvraw prf flags csraw) ++ "\n")) ++ showSep "\n" cs) printClause l i (ImpossibleClause _ lhsraw) - = do lhs <- pterm lhsraw + = do lhs <- pterm $ map (MkKindedName Nothing) lhsraw -- hack pure (relit l (pack (replicate i ' ') ++ show lhs ++ " impossible")) @@ -340,7 +344,7 @@ nextGenDef reject Z => pure (Just (line, res)) S k => nextGenDef k -dropLams : Nat -> RawImp -> RawImp +dropLams : Nat -> RawImp' nm -> RawImp' nm dropLams Z tm = tm dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc dropLams _ tm = tm @@ -424,8 +428,8 @@ processEdit (ExprSearch upd line name hints) Just (_, restm) <- nextProofSearch | Nothing => pure $ EditError "No search results" let tm' = dropLams locs restm - itm <- pterm tm' - let itm' : PTerm = if brack then addBracket replFC itm else itm + itm <- pterm $ map (MkKindedName Nothing) tm' -- hack + let itm' = ifThenElse brack (addBracket replFC itm) itm if upd then updateFile (proofSearch name (show itm') (integerToNat (cast (line - 1)))) else pure $ DisplayEdit (prettyTerm itm') @@ -435,7 +439,7 @@ processEdit (ExprSearch upd line name hints) SolvedHole locs => do let (_ ** (env, tm')) = dropLamsTm locs [] !(normaliseHoles defs [] tm) itm <- resugar env tm' - let itm' : PTerm = if brack then addBracket replFC itm else itm + let itm'= ifThenElse brack (addBracket replFC itm) itm if upd then updateFile (proofSearch name (show itm') (integerToNat (cast (line - 1)))) else pure $ DisplayEdit (prettyTerm itm') @@ -450,8 +454,8 @@ processEdit ExprSearchNext | _ => pure $ EditError "Not a searchable hole" let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn) let tm' = dropLams locs restm - itm <- pterm tm' - let itm' : PTerm = if brack then addBracket replFC itm else itm + itm <- pterm $ map (MkKindedName Nothing) tm' + let itm' = ifThenElse brack (addBracket replFC itm) itm pure $ DisplayEdit (prettyTerm itm') processEdit (GenerateDef upd line name rej) @@ -494,12 +498,12 @@ processEdit (MakeLemma upd line name) case !(lookupDefTyName name (gamma defs)) of [(n, nidx, Hole locs _, ty)] => do (lty, lapp) <- makeLemma replFC name locs ty - pty <- pterm lty - papp <- pterm lapp + pty <- pterm $ map (MkKindedName Nothing) lty -- hack + papp <- pterm $ map (MkKindedName Nothing) lapp -- hack opts <- get ROpts - let pappstr = show (the PTerm (if brack - then addBracket replFC papp - else papp)) + let pappstr = show (ifThenElse brack + (addBracket replFC papp) + papp) Just srcLine <- getSourceLine line | Nothing => pure (EditError "Source line not found") let (markM,_) = isLitLine srcLine @@ -1070,9 +1074,9 @@ mutual {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core () displayResult (REPLError err) = printError err displayResult (Evaluated x Nothing) = printResult $ prettyTerm x - displayResult (Evaluated x (Just y)) = printResult (prettyTerm x <++> colon <++> code (prettyTerm y)) + displayResult (Evaluated x (Just y)) = printResult (prettyTerm x <++> colon <++> prettyTerm y) displayResult (Printed xs) = printResult xs - displayResult (TermChecked x y) = printResult (prettyTerm x <++> colon <++> code (prettyTerm y)) + displayResult (TermChecked x y) = printResult (prettyTerm x <++> colon <++> prettyTerm y) displayResult (FileLoaded x) = printResult (reflow "Loaded file" <++> pretty x) displayResult (ModuleLoaded x) = printResult (reflow "Imported module" <++> pretty x) displayResult (ErrorLoadingModule x err) = printResult (reflow "Error loading module" <++> pretty x <+> colon <++> !(perror err)) @@ -1100,7 +1104,8 @@ mutual displayResult (Edited (DisplayEdit Empty)) = pure () displayResult (Edited (DisplayEdit xs)) = printResult xs displayResult (Edited (EditError x)) = printError x - displayResult (Edited (MadeLemma lit name pty pappstr)) = printResult $ pretty (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr) + displayResult (Edited (MadeLemma lit name pty pappstr)) + = printResult $ pretty (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr) displayResult (Edited (MadeWith lit wapp)) = printResult $ pretty $ showSep "\n" (map (relit lit) wapp) displayResult (Edited (MadeCase lit cstr)) = printResult $ pretty $ showSep "\n" (map (relit lit) cstr) displayResult (OptionsSet opts) = printResult (vsep (pretty <$> opts)) diff --git a/src/Idris/REPL/Common.idr b/src/Idris/REPL/Common.idr index f30078201..04ac3ccca 100644 --- a/src/Idris/REPL/Common.idr +++ b/src/Idris/REPL/Common.idr @@ -175,7 +175,7 @@ public export data EditResult : Type where DisplayEdit : Doc IdrisAnn -> EditResult EditError : Doc IdrisAnn -> EditResult - MadeLemma : Maybe String -> Name -> PTerm -> String -> EditResult + MadeLemma : Maybe String -> Name -> IPTerm -> String -> EditResult MadeWith : Maybe String -> List String -> EditResult MadeCase : Maybe String -> List String -> EditResult @@ -191,9 +191,9 @@ data REPLResult : Type where REPLError : Doc IdrisAnn -> REPLResult Executed : PTerm -> REPLResult RequestedHelp : REPLResult - Evaluated : PTerm -> (Maybe PTerm) -> REPLResult + Evaluated : IPTerm -> Maybe IPTerm -> REPLResult Printed : Doc IdrisAnn -> REPLResult - TermChecked : PTerm -> PTerm -> REPLResult + TermChecked : IPTerm -> IPTerm -> REPLResult FileLoaded : String -> REPLResult ModuleLoaded : String -> REPLResult ErrorLoadingModule : String -> Error -> REPLResult @@ -203,7 +203,7 @@ data REPLResult : Type where CurrentDirectory : String -> REPLResult CompilationFailed: REPLResult Compiled : String -> REPLResult - ProofFound : PTerm -> REPLResult + ProofFound : IPTerm -> REPLResult Missed : List MissedResult -> REPLResult CheckedTotal : List (Name, Totality) -> REPLResult FoundHoles : List HoleData -> REPLResult diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index c688fd226..af7e65513 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -8,6 +8,7 @@ import Core.Options import Idris.Syntax import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Unelab import TTImp.Utils @@ -24,25 +25,26 @@ import Libraries.Data.StringMap -- type check (in fact it probably won't due to tidying up names for -- readability). -unbracketApp : PTerm -> PTerm +unbracketApp : PTerm' nm -> PTerm' nm unbracketApp (PBracketed _ tm@(PApp _ _ _)) = tm unbracketApp tm = tm -- TODO: Deal with precedences mkOp : {auto s : Ref Syn SyntaxInfo} -> - PTerm -> Core PTerm -mkOp tm@(PApp fc (PApp _ (PRef opFC n) x) y) + IPTerm -> Core IPTerm +mkOp tm@(PApp fc (PApp _ (PRef opFC kn) x) y) = do syn <- get Syn + let n = rawName kn case StringMap.lookup (nameRoot n) (infixes syn) of Nothing => pure tm Just _ => pure (POp fc opFC n (unbracketApp x) (unbracketApp y)) mkOp tm = pure tm export -addBracket : FC -> PTerm -> PTerm +addBracket : FC -> PTerm' nm -> PTerm' nm addBracket fc tm = if needed tm then PBracketed fc tm else tm where - needed : PTerm -> Bool + needed : PTerm' nm -> Bool needed (PBracketed _ _) = False needed (PRef _ _) = False needed (PPair _ _ _) = False @@ -51,11 +53,16 @@ addBracket fc tm = if needed tm then PBracketed fc tm else tm needed (PComprehension _ _ _) = False needed (PList _ _ _) = False needed (PSnocList _ _ _) = False + needed (PRange{}) = False + needed (PRangeStream{}) = False needed (PPrimVal _ _) = False + needed (PIdiom{}) = False + needed (PBang{}) = False needed tm = True bracket : {auto s : Ref Syn SyntaxInfo} -> - (outer : Nat) -> (inner : Nat) -> PTerm -> Core PTerm + (outer : Nat) -> (inner : Nat) -> + IPTerm -> Core IPTerm bracket outer inner tm = do tm' <- mkOp tm if outer > inner @@ -92,21 +99,22 @@ fullNamespace = do pp <- getPPrint pure (fullNamespace pp) -unbracket : PTerm -> PTerm +unbracket : PTerm' nm -> PTerm' nm unbracket (PBracketed _ tm) = tm unbracket tm = tm ||| Attempt to extract a constant natural number -extractNat : Nat -> PTerm -> Maybe Nat +extractNat : Nat -> IPTerm -> Maybe Nat extractNat acc tm = case tm of - PRef _ (NS ns (UN n)) => + PRef _ (MkKindedName _ (NS ns (UN n))) => do guard (n == "Z") guard (ns == typesNS || ns == preludeNS) pure acc - PApp _ (PRef _ (NS ns (UN n))) k => do - do guard (n == "S") - guard (ns == typesNS || ns == preludeNS) - extractNat (1 + acc) k + PApp _ (PRef _ (MkKindedName _ (NS ns (UN n)))) k => case n of + "S" => do guard (ns == typesNS || ns == preludeNS) + extractNat (1 + acc) k + "fromInteger" => extractNat acc k + _ => Nothing PPrimVal _ (BI n) => pure (acc + integerToNat n) PBracketed _ k => extractNat acc k _ => Nothing @@ -115,8 +123,12 @@ mutual ||| Put the special names (Nil, ::, Pair, Z, S, etc) back as syntax ||| Returns `Nothing` in case there was nothing to resugar. - sugarAppM : PTerm -> Maybe PTerm - sugarAppM (PApp fc (PApp _ (PRef opFC (NS ns nm)) l) r) = + sugarAppM : IPTerm -> Maybe IPTerm + sugarAppM (PApp fc (PApp _ (PApp _ (PRef opFC (MkKindedName nt (NS ns nm))) l) m) r) = + case nameRoot nm of + "rangeFromThenTo" => pure $ PRange fc (unbracket l) (Just $ unbracket m) (unbracket r) + _ => Nothing + sugarAppM (PApp fc (PApp _ (PRef opFC (MkKindedName nt (NS ns nm))) l) r) = if builtinNS == ns then case nameRoot nm of "Pair" => pure $ PPair fc (unbracket l) (unbracket r) @@ -137,13 +149,16 @@ mutual -- use a snoc list here in a future version (xs ++ [(opFC, unbracketApp l)]) _ => Nothing + "rangeFromTo" => pure $ PRange fc (unbracket l) Nothing (unbracket r) + "rangeFromThen" => pure $ PRangeStream fc (unbracket l) (Just $ unbracket r) + _ => Nothing sugarAppM tm = -- refolding natural numbers if the expression is a constant case extractNat 0 tm of Just k => pure $ PPrimVal (getPTermLoc tm) (BI (cast k)) Nothing => case tm of - PRef fc (NS ns nm) => + PRef fc (MkKindedName nt (NS ns nm)) => if builtinNS == ns then case nameRoot nm of "Unit" => pure $ PUnit fc @@ -153,11 +168,15 @@ mutual "Nil" => pure $ PList fc fc [] "Lin" => pure $ PSnocList fc fc [] _ => Nothing + PApp fc (PRef _ (MkKindedName nt (NS ns nm))) arg => + case nameRoot nm of + "rangeFrom" => pure $ PRangeStream fc (unbracket arg) Nothing + _ => Nothing _ => Nothing ||| Put the special names (Nil, ::, Pair, Z, S, etc.) back as syntax - sugarApp : PTerm -> PTerm + sugarApp : IPTerm -> IPTerm sugarApp tm = fromMaybe tm (sugarAppM tm) export @@ -167,24 +186,24 @@ sugarName (PV n _) = sugarName n sugarName (DN n _) = n sugarName x = show x -toPRef : FC -> Name -> Core PTerm -toPRef fc nm = case nm of - MN n _ => pure (sugarApp (PRef fc (UN n))) - PV n _ => pure (sugarApp (PRef fc n)) - DN n _ => pure (sugarApp (PRef fc (UN n))) - Nested _ n => toPRef fc n - _ => pure (sugarApp (PRef fc nm)) +toPRef : FC -> KindedName -> Core IPTerm +toPRef fc kn@(MkKindedName nt nm) = case nm of + MN n _ => pure (sugarApp (PRef fc (MkKindedName nt $ UN n))) + PV n _ => pure (sugarApp (PRef fc (MkKindedName nt $ n))) + DN n _ => pure (sugarApp (PRef fc (MkKindedName nt $ UN n))) + Nested _ n => toPRef fc (MkKindedName nt n) + _ => pure (sugarApp (PRef fc kn)) mutual toPTerm : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - (prec : Nat) -> RawImp -> Core PTerm + (prec : Nat) -> IRawImp -> Core IPTerm toPTerm p (IVar fc nm) = do t <- if fullNamespace !(getPPrint) then pure $ PRef fc nm else toPRef fc nm log "resugar.var" 70 $ - unwords [ "Resugaring", show @{Raw} nm, "to", show t] + unwords [ "Resugaring", show @{Raw} nm.rawName, "to", show t] pure t toPTerm p (IPi fc rig Implicit n arg ret) = do imp <- showImplicits @@ -200,7 +219,8 @@ mutual where needsBind : Maybe Name -> Bool needsBind (Just (UN t)) - = let ns = findBindableNames False [] [] ret + = let ret = map rawName ret + ns = findBindableNames False [] [] ret allNs = findAllNames [] ret in ((UN t) `elem` allNs) && not (t `elem` (map Builtin.fst ns)) needsBind _ = False @@ -218,15 +238,16 @@ mutual else pure (PImplicit fc) sc' <- toPTerm startPrec sc pt' <- traverse (toPTerm argPrec) pt - bracket p startPrec (PLam fc rig pt' (PRef fc n) arg' sc') + let var = PRef fc (MkKindedName (Just Bound) n) + bracket p startPrec (PLam fc rig pt' var arg' sc') toPTerm p (ILet fc lhsFC rig n ty val sc) = do imp <- showImplicits ty' <- if imp then toPTerm startPrec ty else pure (PImplicit fc) val' <- toPTerm startPrec val sc' <- toPTerm startPrec sc - bracket p startPrec (PLet fc rig (PRef lhsFC n) - ty' val' sc' []) + let var = PRef lhsFC (MkKindedName (Just Bound) n) + bracket p startPrec (PLet fc rig var ty' val' sc' []) toPTerm p (ICase fc sc scty [PatClause _ lhs rhs]) = do sc' <- toPTerm startPrec sc lhs' <- toPTerm startPrec lhs @@ -238,10 +259,11 @@ mutual alts' <- traverse toPClause alts bracket p startPrec (mkIf (PCase fc sc' alts')) where - mkIf : PTerm -> PTerm + mkIf : IPTerm -> IPTerm mkIf tm@(PCase loc sc [MkPatClause _ (PRef _ tval) t [], MkPatClause _ (PRef _ fval) f []]) - = if dropNS tval == UN "True" && dropNS fval == UN "False" + = if dropNS (rawName tval) == UN "True" + && dropNS (rawName fval) == UN "False" then PIfThenElse loc sc t f else tm mkIf tm = tm @@ -282,7 +304,7 @@ mutual toPTerm p (IPrimVal fc c) = pure (PPrimVal fc c) toPTerm p (IHole fc str) = pure (PHole fc False str) toPTerm p (IType fc) = pure (PType fc) - toPTerm p (IBindVar fc v) = pure (PRef fc (UN v)) + toPTerm p (IBindVar fc v) = pure (PRef fc (MkKindedName (Just Bound) (UN v))) toPTerm p (IBindHere fc _ tm) = toPTerm p tm toPTerm p (IAs fc nameFC _ n pat) = pure (PAs fc nameFC n !(toPTerm argPrec pat)) toPTerm p (IMustUnify fc r pat) = pure (PDotted fc !(toPTerm argPrec pat)) @@ -307,7 +329,9 @@ mutual mkApp : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - PTerm -> List (FC, Maybe (Maybe Name), PTerm) -> Core PTerm + IPTerm -> + List (FC, Maybe (Maybe Name), IPTerm) -> + Core IPTerm mkApp fn [] = pure fn mkApp fn ((fc, Nothing, arg) :: rest) = do let ap = sugarApp (PApp fc fn arg) @@ -324,8 +348,8 @@ mutual toPTermApp : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - RawImp -> List (FC, Maybe (Maybe Name), PTerm) -> - Core PTerm + IRawImp -> List (FC, Maybe (Maybe Name), IPTerm) -> + Core IPTerm toPTermApp (IApp fc f a) args = do a' <- toPTerm argPrec a toPTermApp f ((fc, Nothing, a') :: args) @@ -334,7 +358,7 @@ mutual toPTermApp f ((fc, Just (Just n), a') :: args) toPTermApp fn@(IVar fc n) args = do defs <- get Ctxt - case !(lookupCtxtExact n (gamma defs)) of + case !(lookupCtxtExact (rawName n) (gamma defs)) of Nothing => do fn' <- toPTerm appPrec fn mkApp fn' args Just def => do fn' <- toPTerm appPrec fn @@ -350,7 +374,7 @@ mutual toPFieldUpdate : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - IFieldUpdate -> Core PFieldUpdate + IFieldUpdate' KindedName -> Core (PFieldUpdate' KindedName) toPFieldUpdate (ISetField p v) = do v' <- toPTerm startPrec v pure (PSetField p v') @@ -360,7 +384,7 @@ mutual toPClause : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - ImpClause -> Core PClause + ImpClause' KindedName -> Core (PClause' KindedName) toPClause (PatClause fc lhs rhs) = pure (MkPatClause fc !(toPTerm startPrec lhs) !(toPTerm startPrec rhs) @@ -376,13 +400,13 @@ mutual toPTypeDecl : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - ImpTy -> Core PTypeDecl + ImpTy' KindedName -> Core (PTypeDecl' KindedName) toPTypeDecl (MkImpTy fc nameFC n ty) = pure (MkPTy fc nameFC n "" !(toPTerm startPrec ty)) toPData : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - ImpData -> Core PDataDecl + ImpData' KindedName -> Core (PDataDecl' KindedName) toPData (MkImpData fc n ty opts cs) = pure (MkPData fc n !(toPTerm startPrec ty) opts !(traverse toPTypeDecl cs)) @@ -391,7 +415,7 @@ mutual toPField : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - IField -> Core PField + IField' KindedName -> Core (PField' KindedName) toPField (MkIField fc c p n ty) = do ty' <- toPTerm startPrec ty p' <- traverse (toPTerm startPrec) p @@ -399,8 +423,11 @@ mutual toPRecord : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - ImpRecord -> - Core (Name, List (Name, RigCount, PiInfo PTerm, PTerm), Maybe Name, List PField) + ImpRecord' KindedName -> + Core ( Name + , List (Name, RigCount, PiInfo IPTerm, IPTerm) + , Maybe Name + , List (PField' KindedName)) toPRecord (MkImpRecord fc n ps con fs) = do ps' <- traverse (\ (n, c, p, ty) => do ty' <- toPTerm startPrec ty @@ -409,7 +436,7 @@ mutual fs' <- traverse toPField fs pure (n, ps', Just con, fs') where - mapPiInfo : PiInfo RawImp -> Core (PiInfo PTerm) + mapPiInfo : PiInfo IRawImp -> Core (PiInfo IPTerm) mapPiInfo Explicit = pure Explicit mapPiInfo Implicit = pure Implicit mapPiInfo AutoImplicit = pure AutoImplicit @@ -417,7 +444,7 @@ mutual toPFnOpt : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - FnOpt -> Core PFnOpt + FnOpt' KindedName -> Core (PFnOpt' KindedName) toPFnOpt (ForeignFn cs) = do cs' <- traverse (toPTerm startPrec) cs pure (PForeign cs') @@ -425,7 +452,7 @@ mutual toPDecl : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - ImpDecl -> Core (Maybe PDecl) + ImpDecl' KindedName -> Core (Maybe (PDecl' KindedName)) toPDecl (IClaim fc rig vis opts ty) = do opts' <- traverse toPFnOpt opts pure (Just (PClaim fc rig vis opts' !(toPTypeDecl ty))) @@ -459,7 +486,7 @@ mutual export cleanPTerm : {auto c : Ref Ctxt Defs} -> - PTerm -> Core PTerm + IPTerm -> Core IPTerm cleanPTerm ptm = do ns <- fullNamespace if ns then pure ptm else mapPTermM cleanNode ptm @@ -476,9 +503,12 @@ cleanPTerm ptm RF n => pure (RF n) _ => UN <$> prettyName nm - cleanNode : PTerm -> Core PTerm + cleanKindedName : KindedName -> Core KindedName + cleanKindedName (MkKindedName nt nm) = MkKindedName nt <$> cleanName nm + + cleanNode : IPTerm -> Core IPTerm cleanNode (PRef fc nm) = - PRef fc <$> cleanName nm + PRef fc <$> cleanKindedName nm cleanNode (POp fc opFC op x y) = (\ op => POp fc opFC op x y) <$> cleanName op cleanNode (PPrefixOp fc opFC op x) = @@ -487,11 +517,13 @@ cleanPTerm ptm (\ op => PSectionL fc opFC op x) <$> cleanName op cleanNode (PSectionR fc opFC x op) = PSectionR fc opFC x <$> cleanName op + cleanNode (PPi fc rig vis (Just n) arg ret) = + (\ n => PPi fc rig vis (Just n) arg ret) <$> cleanName n cleanNode tm = pure tm toCleanPTerm : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - (prec : Nat) -> RawImp -> Core PTerm + (prec : Nat) -> IRawImp -> Core IPTerm toCleanPTerm prec tti = do ptm <- toPTerm prec tti cleanPTerm ptm @@ -500,7 +532,7 @@ export resugar : {vars : _} -> {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Env Term vars -> Term vars -> Core PTerm + Env Term vars -> Term vars -> Core IPTerm resugar env tm = do tti <- unelab env tm toCleanPTerm startPrec tti @@ -509,7 +541,7 @@ export resugarNoPatvars : {vars : _} -> {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Env Term vars -> Term vars -> Core PTerm + Env Term vars -> Term vars -> Core IPTerm resugarNoPatvars env tm = do tti <- unelabNoPatvars env tm toCleanPTerm startPrec tti @@ -517,5 +549,5 @@ resugarNoPatvars env tm export pterm : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - RawImp -> Core PTerm + IRawImp -> Core IPTerm pterm raw = toCleanPTerm startPrec raw diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 63e4739b4..c0f6ca5f7 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -41,88 +41,101 @@ OpStr : Type OpStr = Name mutual - -- The full high level source language - -- This gets desugared to RawImp (TTImp.TTImp), then elaborated to - -- Term (Core.TT) + + ||| Source language as produced by the parser public export - data PTerm : Type where + PTerm : Type + PTerm = PTerm' Name + + ||| Internal PTerm + ||| Source language as produced by the unelaboration of core Terms + ||| KindedNames carry extra information about the nature of the variable + public export + IPTerm : Type + IPTerm = PTerm' KindedName + + ||| The full high level source language + ||| This gets desugared to RawImp (TTImp.TTImp), + ||| then elaborated to Term (Core.TT) + public export + data PTerm' : Type -> Type where -- Direct (more or less) translations to RawImp - PRef : FC -> Name -> PTerm - PPi : FC -> RigCount -> PiInfo PTerm -> Maybe Name -> - (argTy : PTerm) -> (retTy : PTerm) -> PTerm - PLam : FC -> RigCount -> PiInfo PTerm -> PTerm -> - (argTy : PTerm) -> (scope : PTerm) -> PTerm - PLet : FC -> RigCount -> (pat : PTerm) -> - (nTy : PTerm) -> (nVal : PTerm) -> (scope : PTerm) -> - (alts : List PClause) -> PTerm - PCase : FC -> PTerm -> List PClause -> PTerm - PLocal : FC -> List PDecl -> (scope : PTerm) -> PTerm - PUpdate : FC -> List PFieldUpdate -> PTerm - PApp : FC -> PTerm -> PTerm -> PTerm - PWithApp : FC -> PTerm -> PTerm -> PTerm - PNamedApp : FC -> PTerm -> Name -> PTerm -> PTerm - PAutoApp : FC -> PTerm -> PTerm -> PTerm + PRef : FC -> nm -> PTerm' nm + PPi : FC -> RigCount -> PiInfo (PTerm' nm) -> Maybe Name -> + (argTy : PTerm' nm) -> (retTy : PTerm' nm) -> PTerm' nm + PLam : FC -> RigCount -> PiInfo (PTerm' nm) -> PTerm' nm -> + (argTy : PTerm' nm) -> (scope : PTerm' nm) -> PTerm' nm + PLet : FC -> RigCount -> (pat : PTerm' nm) -> + (nTy : PTerm' nm) -> (nVal : PTerm' nm) -> (scope : PTerm' nm) -> + (alts : List (PClause' nm)) -> PTerm' nm + PCase : FC -> PTerm' nm -> List (PClause' nm) -> PTerm' nm + PLocal : FC -> List (PDecl' nm) -> (scope : PTerm' nm) -> PTerm' nm + PUpdate : FC -> List (PFieldUpdate' nm) -> PTerm' nm + PApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm + PWithApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm + PNamedApp : FC -> PTerm' nm -> Name -> PTerm' nm -> PTerm' nm + PAutoApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm - PDelayed : FC -> LazyReason -> PTerm -> PTerm - PDelay : FC -> PTerm -> PTerm - PForce : FC -> PTerm -> PTerm + PDelayed : FC -> LazyReason -> PTerm' nm -> PTerm' nm + PDelay : FC -> PTerm' nm -> PTerm' nm + PForce : FC -> PTerm' nm -> PTerm' nm - PSearch : FC -> (depth : Nat) -> PTerm - PPrimVal : FC -> Constant -> PTerm - PQuote : FC -> PTerm -> PTerm - PQuoteName : FC -> Name -> PTerm - PQuoteDecl : FC -> List PDecl -> PTerm - PUnquote : FC -> PTerm -> PTerm - PRunElab : FC -> PTerm -> PTerm - PHole : FC -> (bracket : Bool) -> (holename : String) -> PTerm - PType : FC -> PTerm - PAs : FC -> (nameFC : FC) -> Name -> (pattern : PTerm) -> PTerm - PDotted : FC -> PTerm -> PTerm - PImplicit : FC -> PTerm - PInfer : FC -> PTerm + PSearch : FC -> (depth : Nat) -> PTerm' nm + PPrimVal : FC -> Constant -> PTerm' nm + PQuote : FC -> PTerm' nm -> PTerm' nm + PQuoteName : FC -> Name -> PTerm' nm + PQuoteDecl : FC -> List (PDecl' nm) -> PTerm' nm + PUnquote : FC -> PTerm' nm -> PTerm' nm + PRunElab : FC -> PTerm' nm -> PTerm' nm + PHole : FC -> (bracket : Bool) -> (holename : String) -> PTerm' nm + PType : FC -> PTerm' nm + PAs : FC -> (nameFC : FC) -> Name -> (pattern : PTerm' nm) -> PTerm' nm + PDotted : FC -> PTerm' nm -> PTerm' nm + PImplicit : FC -> PTerm' nm + PInfer : FC -> PTerm' nm -- Operators - POp : (full, opFC : FC) -> OpStr -> PTerm -> PTerm -> PTerm - PPrefixOp : (full, opFC : FC) -> OpStr -> PTerm -> PTerm - PSectionL : (full, opFC : FC) -> OpStr -> PTerm -> PTerm - PSectionR : (full, opFC : FC) -> PTerm -> OpStr -> PTerm - PEq : FC -> PTerm -> PTerm -> PTerm - PBracketed : FC -> PTerm -> PTerm + POp : (full, opFC : FC) -> OpStr -> PTerm' nm -> PTerm' nm -> PTerm' nm + PPrefixOp : (full, opFC : FC) -> OpStr -> PTerm' nm -> PTerm' nm + PSectionL : (full, opFC : FC) -> OpStr -> PTerm' nm -> PTerm' nm + PSectionR : (full, opFC : FC) -> PTerm' nm -> OpStr -> PTerm' nm + PEq : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm + PBracketed : FC -> PTerm' nm -> PTerm' nm -- Syntactic sugar - PString : FC -> List PStr -> PTerm - PMultiline : FC -> (indent : Nat) -> List (List PStr) -> PTerm - PDoBlock : FC -> Maybe Namespace -> List PDo -> PTerm - PBang : FC -> PTerm -> PTerm - PIdiom : FC -> PTerm -> PTerm - PList : (full, nilFC : FC) -> List (FC, PTerm) -> PTerm + PString : FC -> List (PStr' nm) -> PTerm' nm + PMultiline : FC -> (indent : Nat) -> List (List (PStr' nm)) -> PTerm' nm + PDoBlock : FC -> Maybe Namespace -> List (PDo' nm) -> PTerm' nm + PBang : FC -> PTerm' nm -> PTerm' nm + PIdiom : FC -> PTerm' nm -> PTerm' nm + PList : (full, nilFC : FC) -> List (FC, PTerm' nm) -> PTerm' nm -- ^ v location of the conses/snocs - PSnocList : (full, nilFC : FC) -> List ((FC, PTerm)) -> PTerm - PPair : FC -> PTerm -> PTerm -> PTerm - PDPair : (full, opFC : FC) -> PTerm -> PTerm -> PTerm -> PTerm - PUnit : FC -> PTerm - PIfThenElse : FC -> PTerm -> PTerm -> PTerm -> PTerm - PComprehension : FC -> PTerm -> List PDo -> PTerm - PRewrite : FC -> PTerm -> PTerm -> PTerm + PSnocList : (full, nilFC : FC) -> List ((FC, PTerm' nm)) -> PTerm' nm + PPair : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm + PDPair : (full, opFC : FC) -> PTerm' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm + PUnit : FC -> PTerm' nm + PIfThenElse : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm + PComprehension : FC -> PTerm' nm -> List (PDo' nm) -> PTerm' nm + PRewrite : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -- A list range [x,y..z] - PRange : FC -> PTerm -> Maybe PTerm -> PTerm -> PTerm + PRange : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm -> PTerm' nm -- A stream range [x,y..] - PRangeStream : FC -> PTerm -> Maybe PTerm -> PTerm + PRangeStream : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm -- r.x.y - PPostfixApp : FC -> PTerm -> List (FC, Name) -> PTerm + PPostfixApp : FC -> PTerm' nm -> List (FC, Name) -> PTerm' nm -- .x.y - PPostfixAppPartial : FC -> List (FC, Name) -> PTerm + PPostfixAppPartial : FC -> List (FC, Name) -> PTerm' nm -- Debugging - PUnifyLog : FC -> LogLevel -> PTerm -> PTerm + PUnifyLog : FC -> LogLevel -> PTerm' nm -> PTerm' nm -- with-disambiguation - PWithUnambigNames : FC -> List Name -> PTerm -> PTerm + PWithUnambigNames : FC -> List Name -> PTerm' nm -> PTerm' nm export - getPTermLoc : PTerm -> FC + getPTermLoc : PTerm' nm -> FC getPTermLoc (PRef fc _) = fc getPTermLoc (PPi fc _ _ _ _ _) = fc getPTermLoc (PLam fc _ _ _ _ _) = fc @@ -177,27 +190,39 @@ mutual getPTermLoc (PWithUnambigNames fc _ _) = fc public export - data PFieldUpdate : Type where - PSetField : (path : List String) -> PTerm -> PFieldUpdate - PSetFieldApp : (path : List String) -> PTerm -> PFieldUpdate + PFieldUpdate : Type + PFieldUpdate = PFieldUpdate' Name public export - data PDo : Type where - DoExp : FC -> PTerm -> PDo - DoBind : FC -> (nameFC : FC) -> Name -> PTerm -> PDo - DoBindPat : FC -> PTerm -> PTerm -> List PClause -> PDo - DoLet : FC -> (lhs : FC) -> Name -> RigCount -> PTerm -> PTerm -> PDo - DoLetPat : FC -> PTerm -> PTerm -> PTerm -> List PClause -> PDo - DoLetLocal : FC -> List PDecl -> PDo - DoRewrite : FC -> PTerm -> PDo + data PFieldUpdate' : Type -> Type where + PSetField : (path : List String) -> PTerm' nm -> PFieldUpdate' nm + PSetFieldApp : (path : List String) -> PTerm' nm -> PFieldUpdate' nm public export - data PStr : Type where - StrLiteral : FC -> String -> PStr - StrInterp : FC -> PTerm -> PStr + PDo : Type + PDo = PDo' Name + + public export + data PDo' : Type -> Type where + DoExp : FC -> PTerm' nm -> PDo' nm + DoBind : FC -> (nameFC : FC) -> Name -> PTerm' nm -> PDo' nm + DoBindPat : FC -> PTerm' nm -> PTerm' nm -> List (PClause' nm) -> PDo' nm + DoLet : FC -> (lhs : FC) -> Name -> RigCount -> PTerm' nm -> PTerm' nm -> PDo' nm + DoLetPat : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -> List (PClause' nm) -> PDo' nm + DoLetLocal : FC -> List (PDecl' nm) -> PDo' nm + DoRewrite : FC -> PTerm' nm -> PDo' nm + + public export + PStr : Type + PStr = PStr' Name + + public export + data PStr' : Type -> Type where + StrLiteral : FC -> String -> PStr' nm + StrInterp : FC -> PTerm' nm -> PStr' nm export - getLoc : PDo -> FC + getLoc : PDo' nm -> FC getLoc (DoExp fc _) = fc getLoc (DoBind fc _ _ _) = fc getLoc (DoBindPat fc _ _ _) = fc @@ -207,38 +232,51 @@ mutual getLoc (DoRewrite fc _) = fc export - papply : FC -> PTerm -> List PTerm -> PTerm + papply : FC -> PTerm' nm -> List (PTerm' nm) -> PTerm' nm papply fc f [] = f papply fc f (a :: as) = papply fc (PApp fc f a) as public export - data PTypeDecl : Type where - MkPTy : FC -> (nameFC : FC) -> (n : Name) -> (doc: String) -> (type : PTerm) -> PTypeDecl + PTypeDecl : Type + PTypeDecl = PTypeDecl' Name + + public export + data PTypeDecl' : Type -> Type where + MkPTy : FC -> (nameFC : FC) -> (n : Name) -> + (doc: String) -> (type : PTerm' nm) -> PTypeDecl' nm export - getPTypeDeclLoc : PTypeDecl -> FC + getPTypeDeclLoc : PTypeDecl' nm -> FC getPTypeDeclLoc (MkPTy fc _ _ _ _) = fc public export - data PDataDecl : Type where - MkPData : FC -> (tyname : Name) -> (tycon : PTerm) -> + PDataDecl : Type + PDataDecl = PDataDecl' Name + + public export + data PDataDecl' : Type -> Type where + MkPData : FC -> (tyname : Name) -> (tycon : PTerm' nm) -> (opts : List DataOpt) -> - (datacons : List PTypeDecl) -> PDataDecl - MkPLater : FC -> (tyname : Name) -> (tycon : PTerm) -> PDataDecl + (datacons : List (PTypeDecl' nm)) -> PDataDecl' nm + MkPLater : FC -> (tyname : Name) -> (tycon : PTerm' nm) -> PDataDecl' nm export - getPDataDeclLoc : PDataDecl -> FC + getPDataDeclLoc : PDataDecl' nm -> FC getPDataDeclLoc (MkPData fc _ _ _ _) = fc getPDataDeclLoc (MkPLater fc _ _) = fc public export - data PClause : Type where - MkPatClause : FC -> (lhs : PTerm) -> (rhs : PTerm) -> - (whereblock : List PDecl) -> PClause - MkWithClause : FC -> (lhs : PTerm) -> - (wval : PTerm) -> (prf : Maybe Name) -> - List WithFlag -> List PClause -> PClause - MkImpossible : FC -> (lhs : PTerm) -> PClause + PClause : Type + PClause = PClause' Name + + public export + data PClause' : Type -> Type where + MkPatClause : FC -> (lhs : PTerm' nm) -> (rhs : PTerm' nm) -> + (whereblock : List (PDecl' nm)) -> PClause' nm + MkWithClause : FC -> (lhs : PTerm' nm) -> + (wval : PTerm' nm) -> (prf : Maybe Name) -> + List WithFlag -> List (PClause' nm) -> PClause' nm + MkImpossible : FC -> (lhs : PTerm' nm) -> PClause' nm export getPClauseLoc : PClause -> FC @@ -261,7 +299,7 @@ mutual PrimDouble : Name -> Directive CGAction : String -> String -> Directive Names : Name -> List String -> Directive - StartExpr : PTerm -> Directive + StartExpr : PTerm' nm -> Directive Overloadable : Name -> Directive Extension : LangExt -> Directive DefaultTotality : TotalReq -> Directive @@ -321,9 +359,13 @@ mutual "%search_timeout ms" public export - data PField : Type where - MkField : FC -> (doc : String) -> RigCount -> PiInfo PTerm -> - Name -> (ty : PTerm) -> PField + PField : Type + PField = PField' Name + + public export + data PField' : Type -> Type where + MkField : FC -> (doc : String) -> RigCount -> PiInfo (PTerm' nm) -> + Name -> (ty : PTerm' nm) -> PField' nm -- For noting the pass we're in when desugaring a mutual block -- TODO: Decide whether we want mutual blocks! @@ -346,59 +388,70 @@ mutual defPass p = p == Single || p == AsDef public export - data PFnOpt : Type where - IFnOpt : FnOpt -> PFnOpt - PForeign : List PTerm -> PFnOpt + PFnOpt : Type + PFnOpt = PFnOpt' Name public export - data PDecl : Type where - PClaim : FC -> RigCount -> Visibility -> List PFnOpt -> PTypeDecl -> PDecl - PDef : FC -> List PClause -> PDecl - PData : FC -> (doc : String) -> Visibility -> PDataDecl -> PDecl - PParameters : FC -> List (Name, RigCount, PiInfo PTerm, PTerm) -> List PDecl -> PDecl - PUsing : FC -> List (Maybe Name, PTerm) -> List PDecl -> PDecl - PReflect : FC -> PTerm -> PDecl + data PFnOpt' : Type -> Type where + IFnOpt : FnOpt' nm -> PFnOpt' nm + PForeign : List (PTerm' nm) -> PFnOpt' nm + + public export + PDecl : Type + PDecl = PDecl' Name + + public export + data PDecl' : Type -> Type where + PClaim : FC -> RigCount -> Visibility -> List (PFnOpt' nm) -> PTypeDecl' nm -> PDecl' nm + PDef : FC -> List (PClause' nm) -> PDecl' nm + PData : FC -> (doc : String) -> Visibility -> PDataDecl' nm -> PDecl' nm + PParameters : FC -> + List (Name, RigCount, PiInfo (PTerm' nm), PTerm' nm) -> + List (PDecl' nm) -> PDecl' nm + PUsing : FC -> List (Maybe Name, PTerm' nm) -> + List (PDecl' nm) -> PDecl' nm + PReflect : FC -> PTerm' nm -> PDecl' nm PInterface : FC -> Visibility -> - (constraints : List (Maybe Name, PTerm)) -> + (constraints : List (Maybe Name, PTerm' nm)) -> Name -> (doc : String) -> - (params : List (Name, (RigCount, PTerm))) -> + (params : List (Name, (RigCount, PTerm' nm))) -> (det : List Name) -> (conName : Maybe Name) -> - List PDecl -> - PDecl + List (PDecl' nm) -> + PDecl' nm PImplementation : FC -> Visibility -> List PFnOpt -> Pass -> - (implicits : List (Name, RigCount, PTerm)) -> - (constraints : List (Maybe Name, PTerm)) -> + (implicits : List (Name, RigCount, PTerm' nm)) -> + (constraints : List (Maybe Name, PTerm' nm)) -> Name -> - (params : List PTerm) -> + (params : List (PTerm' nm)) -> (implName : Maybe Name) -> (nusing : List Name) -> - Maybe (List PDecl) -> - PDecl + Maybe (List (PDecl' nm)) -> + PDecl' nm PRecord : FC -> (doc : String) -> Visibility -> Name -> - (params : List (Name, RigCount, PiInfo PTerm, PTerm)) -> + (params : List (Name, RigCount, PiInfo (PTerm' nm), PTerm' nm)) -> (conName : Maybe Name) -> - List PField -> - PDecl + List (PField' nm) -> + PDecl' nm -- TODO: PPostulate -- TODO: POpen (for opening named interfaces) - PMutual : FC -> List PDecl -> PDecl - PFixity : FC -> Fixity -> Nat -> OpStr -> PDecl - PNamespace : FC -> Namespace -> List PDecl -> PDecl - PTransform : FC -> String -> PTerm -> PTerm -> PDecl - PRunElabDecl : FC -> PTerm -> PDecl - PDirective : FC -> Directive -> PDecl - PBuiltin : FC -> BuiltinType -> Name -> PDecl + PMutual : FC -> List (PDecl' nm) -> PDecl' nm + PFixity : FC -> Fixity -> Nat -> OpStr -> PDecl' nm + PNamespace : FC -> Namespace -> List (PDecl' nm) -> PDecl' nm + PTransform : FC -> String -> PTerm' nm -> PTerm' nm -> PDecl' nm + PRunElabDecl : FC -> PTerm' nm -> PDecl' nm + PDirective : FC -> Directive -> PDecl' nm + PBuiltin : FC -> BuiltinType -> Name -> PDecl' nm export - getPDeclLoc : PDecl -> FC + getPDeclLoc : PDecl' nm -> FC getPDeclLoc (PClaim fc _ _ _ _) = fc getPDeclLoc (PDef fc _) = fc getPDeclLoc (PData fc _ _ _) = fc @@ -559,178 +612,193 @@ record Module where documentation : String decls : List PDecl -mutual - showAlt : PClause -> String - showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";" - showAlt (MkWithClause _ lhs wval prf flags cs) = " | <>;" - showAlt (MkImpossible _ lhs) = " | " ++ show lhs ++ " impossible;" +parameters {0 nm : Type} (toName : nm -> Name) - showDo : PDo -> String - showDo (DoExp _ tm) = show tm - showDo (DoBind _ _ n tm) = show n ++ " <- " ++ show tm + showAlt : PClause' nm -> String + showDo : PDo' nm -> String + showPStr : PStr' nm -> String + showUpdate : PFieldUpdate' nm -> String + showPTermPrec : Prec -> PTerm' nm -> String + showOpPrec : Prec -> OpStr -> String + + showPTerm : PTerm' nm -> String + showPTerm = showPTermPrec Open + + showAlt (MkPatClause _ lhs rhs _) = + " | " ++ showPTerm lhs ++ " => " ++ showPTerm rhs ++ ";" + showAlt (MkWithClause _ lhs wval prf flags cs) = " | <>;" + showAlt (MkImpossible _ lhs) = " | " ++ showPTerm lhs ++ " impossible;" + + showDo (DoExp _ tm) = showPTerm tm + showDo (DoBind _ _ n tm) = show n ++ " <- " ++ showPTerm tm showDo (DoBindPat _ l tm alts) - = show l ++ " <- " ++ show tm ++ concatMap showAlt alts - showDo (DoLet _ _ l rig _ tm) = "let " ++ show l ++ " = " ++ show tm + = showPTerm l ++ " <- " ++ showPTerm tm ++ concatMap showAlt alts + showDo (DoLet _ _ l rig _ tm) = "let " ++ show l ++ " = " ++ showPTerm tm showDo (DoLetPat _ l _ tm alts) - = "let " ++ show l ++ " = " ++ show tm ++ concatMap showAlt alts + = "let " ++ showPTerm l ++ " = " ++ showPTerm tm ++ concatMap showAlt alts showDo (DoLetLocal _ ds) -- We'll never see this when displaying a normal form... = "let { << definitions >> }" showDo (DoRewrite _ rule) - = "rewrite " ++ show rule + = "rewrite " ++ showPTerm rule - export - Show PStr where - show (StrLiteral _ str) = show str - show (StrInterp _ tm) = show tm + showPStr (StrLiteral _ str) = show str + showPStr (StrInterp _ tm) = showPTerm tm - showUpdate : PFieldUpdate -> String - showUpdate (PSetField p v) = showSep "." p ++ " = " ++ show v - showUpdate (PSetFieldApp p v) = showSep "." p ++ " $= " ++ show v + showUpdate (PSetField p v) = showSep "." p ++ " = " ++ showPTerm v + showUpdate (PSetFieldApp p v) = showSep "." p ++ " $= " ++ showPTerm v - export - Show PTerm where - showPrec d (PRef _ n) = showPrec d n - showPrec d (PPi _ rig Explicit Nothing arg ret) - = showPrec d arg ++ " -> " ++ showPrec d ret - showPrec d (PPi _ rig Explicit (Just n) arg ret) - = "(" ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d arg ++ ") -> " ++ showPrec d ret - showPrec d (PPi _ rig Implicit Nothing arg ret) -- shouldn't happen - = "{" ++ showCount rig ++ "_ : " ++ showPrec d arg ++ "} -> " ++ showPrec d ret - showPrec d (PPi _ rig Implicit (Just n) arg ret) - = "{" ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d arg ++ "} -> " ++ showPrec d ret - showPrec d (PPi _ top AutoImplicit Nothing arg ret) - = showPrec d arg ++ " => " ++ showPrec d ret - showPrec d (PPi _ rig AutoImplicit (Just n) arg ret) - = "{auto " ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d arg ++ "} -> " ++ showPrec d ret - showPrec d (PPi _ rig (DefImplicit t) Nothing arg ret) -- shouldn't happen - = "{default " ++ showPrec App t ++ " " ++ showCount rig ++ "_ : " ++ showPrec d arg ++ "} -> " ++ showPrec d ret - showPrec d (PPi _ rig (DefImplicit t) (Just n) arg ret) - = "{default " ++ showPrec App t ++ " " ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d arg ++ "} -> " ++ showPrec d ret - showPrec d (PLam _ rig _ n (PImplicit _) sc) - = "\\" ++ showCount rig ++ showPrec d n ++ " => " ++ showPrec d sc - showPrec d (PLam _ rig _ n ty sc) - = "\\" ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d ty ++ " => " ++ showPrec d sc - showPrec d (PLet _ rig n (PImplicit _) val sc alts) - = "let " ++ showCount rig ++ showPrec d n ++ " = " ++ showPrec d val ++ " in " ++ showPrec d sc - showPrec d (PLet _ rig n ty val sc alts) - = "let " ++ showCount rig ++ showPrec d n ++ " : " ++ showPrec d ty ++ " = " - ++ showPrec d val ++ concatMap showAlt alts ++ - " in " ++ showPrec d sc + showPTermPrec d (PRef _ n) = showPrec d (toName n) + showPTermPrec d (PPi _ rig Explicit Nothing arg ret) + = showPTermPrec d arg ++ " -> " ++ showPTermPrec d ret + showPTermPrec d (PPi _ rig Explicit (Just n) arg ret) + = "(" ++ showCount rig ++ showPrec d n + ++ " : " ++ showPTermPrec d arg ++ ") -> " + ++ showPTermPrec d ret + showPTermPrec d (PPi _ rig Implicit Nothing arg ret) -- shouldn't happen + = "{" ++ showCount rig ++ "_ : " ++ showPTermPrec d arg ++ "} -> " + ++ showPTermPrec d ret + showPTermPrec d (PPi _ rig Implicit (Just n) arg ret) + = "{" ++ showCount rig ++ showPrec d n ++ " : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret + showPTermPrec d (PPi _ top AutoImplicit Nothing arg ret) + = showPTermPrec d arg ++ " => " ++ showPTermPrec d ret + showPTermPrec d (PPi _ rig AutoImplicit (Just n) arg ret) + = "{auto " ++ showCount rig ++ showPrec d n ++ " : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret + showPTermPrec d (PPi _ rig (DefImplicit t) Nothing arg ret) -- shouldn't happen + = "{default " ++ showPTermPrec App t ++ " " ++ showCount rig ++ "_ : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret + showPTermPrec d (PPi _ rig (DefImplicit t) (Just n) arg ret) + = "{default " ++ showPTermPrec App t ++ " " ++ showCount rig ++ showPrec d n ++ " : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret + showPTermPrec d (PLam _ rig _ n (PImplicit _) sc) + = "\\" ++ showCount rig ++ showPTermPrec d n ++ " => " ++ showPTermPrec d sc + showPTermPrec d (PLam _ rig _ n ty sc) + = "\\" ++ showCount rig ++ showPTermPrec d n ++ " : " ++ showPTermPrec d ty ++ " => " ++ showPTermPrec d sc + showPTermPrec d (PLet _ rig n (PImplicit _) val sc alts) + = "let " ++ showCount rig ++ showPTermPrec d n ++ " = " ++ showPTermPrec d val ++ " in " ++ showPTermPrec d sc + showPTermPrec d (PLet _ rig n ty val sc alts) + = "let " ++ showCount rig ++ showPTermPrec d n ++ " : " ++ showPTermPrec d ty ++ " = " + ++ showPTermPrec d val ++ concatMap showAlt alts ++ + " in " ++ showPTermPrec d sc where - showAlt : PClause -> String - showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";" + showAlt : PClause' nm -> String + showAlt (MkPatClause _ lhs rhs _) = " | " ++ showPTerm lhs ++ " => " ++ showPTerm rhs ++ ";" showAlt (MkWithClause _ lhs rhs prf flags _) = " | <>" - showAlt (MkImpossible _ lhs) = " | " ++ show lhs ++ " impossible;" - showPrec _ (PCase _ tm cs) - = "case " ++ show tm ++ " of { " ++ + showAlt (MkImpossible _ lhs) = " | " ++ showPTerm lhs ++ " impossible;" + showPTermPrec _ (PCase _ tm cs) + = "case " ++ showPTerm tm ++ " of { " ++ showSep " ; " (map showCase cs) ++ " }" where - showCase : PClause -> String - showCase (MkPatClause _ lhs rhs _) = show lhs ++ " => " ++ show rhs + showCase : PClause' nm -> String + showCase (MkPatClause _ lhs rhs _) = showPTerm lhs ++ " => " ++ showPTerm rhs showCase (MkWithClause _ lhs rhs _ flags _) = " | <>" - showCase (MkImpossible _ lhs) = show lhs ++ " impossible" - showPrec d (PLocal _ ds sc) -- We'll never see this when displaying a normal form... - = "let { << definitions >> } in " ++ showPrec d sc - showPrec d (PUpdate _ fs) + showCase (MkImpossible _ lhs) = showPTerm lhs ++ " impossible" + showPTermPrec d (PLocal _ ds sc) -- We'll never see this when displaying a normal form... + = "let { << definitions >> } in " ++ showPTermPrec d sc + showPTermPrec d (PUpdate _ fs) = "record { " ++ showSep ", " (map showUpdate fs) ++ " }" - showPrec d (PApp _ f a) = - let catchall : Lazy String := showPrec App f ++ " " ++ showPrec App a in + showPTermPrec d (PApp _ f a) = + let catchall : Lazy String := showPTermPrec App f ++ " " ++ showPTermPrec App a in case f of PRef _ n => - if isJust (isRF n) - then showPrec App a ++ " " ++ showPrec App f + if isJust (isRF (toName n)) + then showPTermPrec App a ++ " " ++ showPTermPrec App f else catchall _ => catchall - showPrec d (PWithApp _ f a) = showPrec d f ++ " | " ++ showPrec d a - showPrec d (PAutoApp _ f a) - = showPrec d f ++ " @{" ++ showPrec d a ++ "}" - showPrec d (PDelayed _ LInf ty) - = showCon d "Inf" $ showArg ty - showPrec d (PDelayed _ _ ty) - = showCon d "Lazy" $ showArg ty - showPrec d (PDelay _ tm) - = showCon d "Delay" $ showArg tm - showPrec d (PForce _ tm) - = showCon d "Force" $ showArg tm - showPrec d (PNamedApp _ f n (PRef _ a)) - = if n == a - then showPrec d f ++ " {" ++ showPrec d n ++ "}" - else showPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d a ++ "}" - showPrec d (PNamedApp _ f n a) - = showPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d a ++ "}" - showPrec _ (PSearch _ _) = "%search" - showPrec d (PQuote _ tm) = "`(" ++ showPrec d tm ++ ")" - showPrec d (PQuoteName _ n) = "`{" ++ showPrec d n ++ "}" - showPrec d (PQuoteDecl _ tm) = "`[ <> ]" - showPrec d (PUnquote _ tm) = "~(" ++ showPrec d tm ++ ")" - showPrec d (PRunElab _ tm) = "%runElab " ++ showPrec d tm - showPrec d (PPrimVal _ c) = showPrec d c - showPrec _ (PHole _ _ n) = "?" ++ n - showPrec _ (PType _) = "Type" - showPrec d (PAs _ _ n p) = showPrec d n ++ "@" ++ showPrec d p - showPrec d (PDotted _ p) = "." ++ showPrec d p - showPrec _ (PImplicit _) = "_" - showPrec _ (PInfer _) = "?" - showPrec d (POp _ _ op x y) = showPrec d x ++ " " ++ showPrecOp d op ++ " " ++ showPrec d y - showPrec d (PPrefixOp _ _ op x) = showPrec d op ++ showPrec d x - showPrec d (PSectionL _ _ op x) = "(" ++ showPrecOp d op ++ " " ++ showPrec d x ++ ")" - showPrec d (PSectionR _ _ x op) = "(" ++ showPrec d x ++ " " ++ showPrecOp d op ++ ")" - showPrec d (PEq fc l r) = showPrec d l ++ " = " ++ showPrec d r - showPrec d (PBracketed _ tm) = "(" ++ showPrec d tm ++ ")" - showPrec d (PString _ xs) = join " ++ " $ show <$> xs - showPrec d (PMultiline _ indent xs) = "multiline (" ++ (join " ++ " $ show <$> concat xs) ++ ")" - showPrec d (PDoBlock _ ns ds) + showPTermPrec d (PWithApp _ f a) = showPTermPrec d f ++ " | " ++ showPTermPrec d a + showPTermPrec d (PAutoApp _ f a) + = showPTermPrec d f ++ " @{" ++ showPTermPrec d a ++ "}" + showPTermPrec d (PDelayed _ LInf ty) + = showParens (d >= App) $ "Inf " ++ showPTermPrec App ty + showPTermPrec d (PDelayed _ _ ty) + = showParens (d >= App) $ "Lazy " ++ showPTermPrec App ty + showPTermPrec d (PDelay _ tm) + = showParens (d >= App) $ "Delay " ++ showPTermPrec App tm + showPTermPrec d (PForce _ tm) + = showParens (d >= App) $ "Force " ++ showPTermPrec App tm + showPTermPrec d (PNamedApp _ f n (PRef _ a)) + = if n == (toName a) + then showPTermPrec d f ++ " {" ++ showPrec d n ++ "}" + else showPTermPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d (toName a) ++ "}" + showPTermPrec d (PNamedApp _ f n a) + = showPTermPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPTermPrec d a ++ "}" + showPTermPrec _ (PSearch _ _) = "%search" + showPTermPrec d (PQuote _ tm) = "`(" ++ showPTermPrec d tm ++ ")" + showPTermPrec d (PQuoteName _ n) = "`{" ++ showPrec d n ++ "}" + showPTermPrec d (PQuoteDecl _ tm) = "`[ <> ]" + showPTermPrec d (PUnquote _ tm) = "~(" ++ showPTermPrec d tm ++ ")" + showPTermPrec d (PRunElab _ tm) = "%runElab " ++ showPTermPrec d tm + showPTermPrec d (PPrimVal _ c) = showPrec d c + showPTermPrec _ (PHole _ _ n) = "?" ++ n + showPTermPrec _ (PType _) = "Type" + showPTermPrec d (PAs _ _ n p) = showPrec d n ++ "@" ++ showPTermPrec d p + showPTermPrec d (PDotted _ p) = "." ++ showPTermPrec d p + showPTermPrec _ (PImplicit _) = "_" + showPTermPrec _ (PInfer _) = "?" + showPTermPrec d (POp _ _ op x y) = showPTermPrec d x ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d y + showPTermPrec d (PPrefixOp _ _ op x) = showPrec d op ++ showPTermPrec d x + showPTermPrec d (PSectionL _ _ op x) = "(" ++ showOpPrec d op ++ " " ++ showPTermPrec d x ++ ")" + showPTermPrec d (PSectionR _ _ x op) = "(" ++ showPTermPrec d x ++ " " ++ showOpPrec d op ++ ")" + showPTermPrec d (PEq fc l r) = showPTermPrec d l ++ " = " ++ showPTermPrec d r + showPTermPrec d (PBracketed _ tm) = "(" ++ showPTermPrec d tm ++ ")" + showPTermPrec d (PString _ xs) = join " ++ " $ showPStr <$> xs + showPTermPrec d (PMultiline _ indent xs) = "multiline (" ++ (join " ++ " $ showPStr <$> concat xs) ++ ")" + showPTermPrec d (PDoBlock _ ns ds) = "do " ++ showSep " ; " (map showDo ds) - showPrec d (PBang _ tm) = "!" ++ showPrec d tm - showPrec d (PIdiom _ tm) = "[|" ++ showPrec d tm ++ "|]" - showPrec d (PList _ _ xs) - = "[" ++ showSep ", " (map (showPrec d . snd) xs) ++ "]" - showPrec d (PSnocList _ _ xs) - = "[<" ++ showSep ", " (map (showPrec d . snd) xs) ++ "]" - showPrec d (PPair _ l r) = "(" ++ showPrec d l ++ ", " ++ showPrec d r ++ ")" - showPrec d (PDPair _ _ l (PImplicit _) r) = "(" ++ showPrec d l ++ " ** " ++ showPrec d r ++ ")" - showPrec d (PDPair _ _ l ty r) = "(" ++ showPrec d l ++ " : " ++ showPrec d ty ++ - " ** " ++ showPrec d r ++ ")" - showPrec _ (PUnit _) = "()" - showPrec d (PIfThenElse _ x t e) = "if " ++ showPrec d x ++ " then " ++ showPrec d t ++ - " else " ++ showPrec d e - showPrec d (PComprehension _ ret es) - = "[" ++ showPrec d (dePure ret) ++ " | " ++ + showPTermPrec d (PBang _ tm) = "!" ++ showPTermPrec d tm + showPTermPrec d (PIdiom _ tm) = "[|" ++ showPTermPrec d tm ++ "|]" + showPTermPrec d (PList _ _ xs) + = "[" ++ showSep ", " (map (showPTermPrec d . snd) xs) ++ "]" + showPTermPrec d (PSnocList _ _ xs) + = "[<" ++ showSep ", " (map (showPTermPrec d . snd) xs) ++ "]" + showPTermPrec d (PPair _ l r) = "(" ++ showPTermPrec d l ++ ", " ++ showPTermPrec d r ++ ")" + showPTermPrec d (PDPair _ _ l (PImplicit _) r) = "(" ++ showPTermPrec d l ++ " ** " ++ showPTermPrec d r ++ ")" + showPTermPrec d (PDPair _ _ l ty r) = "(" ++ showPTermPrec d l ++ " : " ++ showPTermPrec d ty ++ + " ** " ++ showPTermPrec d r ++ ")" + showPTermPrec _ (PUnit _) = "()" + showPTermPrec d (PIfThenElse _ x t e) = "if " ++ showPTermPrec d x ++ " then " ++ showPTermPrec d t ++ + " else " ++ showPTermPrec d e + showPTermPrec d (PComprehension _ ret es) + = "[" ++ showPTermPrec d (dePure ret) ++ " | " ++ showSep ", " (map (showDo . deGuard) es) ++ "]" where - dePure : PTerm -> PTerm + dePure : PTerm' nm -> PTerm' nm dePure tm@(PApp _ (PRef _ n) arg) - = if dropNS n == UN "pure" then arg else tm + = if dropNS (toName n) == UN "pure" then arg else tm dePure tm = tm - deGuard : PDo -> PDo + deGuard : PDo' nm -> PDo' nm deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg)) - = if dropNS n == UN "guard" then DoExp fc arg else tm + = if dropNS (toName n) == UN "guard" then DoExp fc arg else tm deGuard tm = tm - showPrec d (PRewrite _ rule tm) - = "rewrite " ++ showPrec d rule ++ " in " ++ showPrec d tm - showPrec d (PRange _ start Nothing end) - = "[" ++ showPrec d start ++ " .. " ++ showPrec d end ++ "]" - showPrec d (PRange _ start (Just next) end) - = "[" ++ showPrec d start ++ ", " ++ showPrec d next ++ " .. " ++ showPrec d end ++ "]" - showPrec d (PRangeStream _ start Nothing) - = "[" ++ showPrec d start ++ " .. ]" - showPrec d (PRangeStream _ start (Just next)) - = "[" ++ showPrec d start ++ ", " ++ showPrec d next ++ " .. ]" - showPrec d (PUnifyLog _ _ tm) = showPrec d tm - showPrec d (PPostfixApp fc rec fields) - = showPrec d rec ++ concatMap (\n => "." ++ show n) fields - showPrec d (PPostfixAppPartial fc fields) + showPTermPrec d (PRewrite _ rule tm) + = "rewrite " ++ showPTermPrec d rule ++ " in " ++ showPTermPrec d tm + showPTermPrec d (PRange _ start Nothing end) + = "[" ++ showPTermPrec d start ++ " .. " ++ showPTermPrec d end ++ "]" + showPTermPrec d (PRange _ start (Just next) end) + = "[" ++ showPTermPrec d start ++ ", " ++ showPTermPrec d next ++ " .. " ++ showPTermPrec d end ++ "]" + showPTermPrec d (PRangeStream _ start Nothing) + = "[" ++ showPTermPrec d start ++ " .. ]" + showPTermPrec d (PRangeStream _ start (Just next)) + = "[" ++ showPTermPrec d start ++ ", " ++ showPTermPrec d next ++ " .. ]" + showPTermPrec d (PUnifyLog _ _ tm) = showPTermPrec d tm + showPTermPrec d (PPostfixApp fc rec fields) + = showPTermPrec d rec ++ concatMap (\n => "." ++ show n) fields + showPTermPrec d (PPostfixAppPartial fc fields) = concatMap (\n => "." ++ show n) fields - showPrec d (PWithUnambigNames fc ns rhs) - = "with " ++ show ns ++ " " ++ showPrec d rhs + showPTermPrec d (PWithUnambigNames fc ns rhs) + = "with " ++ show ns ++ " " ++ showPTermPrec d rhs - showPrecOp : Prec -> OpStr -> String - showPrecOp d op = if isOpName op + showOpPrec d op = if isOpName op then showPrec d op else "`" ++ showPrec d op ++ "`" +export +Show PTerm where + showPrec = showPTermPrec id + +export +Show IPTerm where + showPrec = showPTermPrec rawName + public export record Method where constructor MkMethod @@ -923,12 +991,12 @@ withSyn : {auto s : Ref Syn SyntaxInfo} -> Core a -> Core a withSyn = wrapRef Syn (\_ => pure ()) export -mapPTermM : (PTerm -> Core PTerm) -> PTerm -> Core PTerm +mapPTermM : (PTerm' nm -> Core (PTerm' nm)) -> PTerm' nm -> Core (PTerm' nm) mapPTermM f = goPTerm where mutual - goPTerm : PTerm -> Core PTerm + goPTerm : PTerm' nm -> Core (PTerm' nm) goPTerm t@(PRef _ _) = f t goPTerm (PPi fc x info z argTy retTy) = PPi fc x <$> goPiInfo info @@ -1098,15 +1166,15 @@ mapPTermM f = goPTerm where PWithUnambigNames fc ns <$> goPTerm rhs >>= f - goPFieldUpdate : PFieldUpdate -> Core PFieldUpdate + goPFieldUpdate : PFieldUpdate' nm -> Core (PFieldUpdate' nm) goPFieldUpdate (PSetField p t) = PSetField p <$> goPTerm t goPFieldUpdate (PSetFieldApp p t) = PSetFieldApp p <$> goPTerm t - goPStr : PStr -> Core PStr + goPStr : PStr' nm -> Core (PStr' nm) goPStr (StrInterp fc t) = StrInterp fc <$> goPTerm t goPStr x = pure x - goPDo : PDo -> Core PDo + goPDo : PDo' nm -> Core (PDo' nm) goPDo (DoExp fc t) = DoExp fc <$> goPTerm t goPDo (DoBind fc nameFC n t) = DoBind fc nameFC n <$> goPTerm t goPDo (DoBindPat fc t u cls) = @@ -1124,7 +1192,7 @@ mapPTermM f = goPTerm where goPDo (DoLetLocal fc decls) = DoLetLocal fc <$> goPDecls decls goPDo (DoRewrite fc t) = DoRewrite fc <$> goPTerm t - goPClause : PClause -> Core PClause + goPClause : PClause' nm -> Core (PClause' nm) goPClause (MkPatClause fc lhs rhs wh) = MkPatClause fc <$> goPTerm lhs <*> goPTerm rhs @@ -1137,7 +1205,7 @@ mapPTermM f = goPTerm where <*> goPClauses cls goPClause (MkImpossible fc lhs) = MkImpossible fc <$> goPTerm lhs - goPDecl : PDecl -> Core PDecl + goPDecl : PDecl' nm -> Core (PDecl' nm) goPDecl (PClaim fc c v opts tdecl) = PClaim fc c v <$> goPFnOpts opts <*> goPTypeDecl tdecl @@ -1179,95 +1247,96 @@ mapPTermM f = goPTerm where goPDecl p@(PBuiltin _ _ _) = pure p - goPTypeDecl : PTypeDecl -> Core PTypeDecl + goPTypeDecl : PTypeDecl' nm -> Core (PTypeDecl' nm) goPTypeDecl (MkPTy fc nameFC n d t) = MkPTy fc nameFC n d <$> goPTerm t - goPDataDecl : PDataDecl -> Core PDataDecl + goPDataDecl : PDataDecl' nm -> Core (PDataDecl' nm) goPDataDecl (MkPData fc n t opts tdecls) = MkPData fc n <$> goPTerm t <*> pure opts <*> goPTypeDecls tdecls goPDataDecl (MkPLater fc n t) = MkPLater fc n <$> goPTerm t - goPField : PField -> Core PField + goPField : PField' nm -> Core (PField' nm) goPField (MkField fc doc c info n t) = MkField fc doc c <$> goPiInfo info <*> pure n <*> goPTerm t - goPiInfo : PiInfo PTerm -> Core (PiInfo PTerm) + goPiInfo : PiInfo (PTerm' nm) -> Core (PiInfo (PTerm' nm)) goPiInfo (DefImplicit t) = DefImplicit <$> goPTerm t goPiInfo t = pure t - goPFnOpt : PFnOpt -> Core PFnOpt + goPFnOpt : PFnOpt' nm -> Core (PFnOpt' nm) goPFnOpt o@(IFnOpt _) = pure o goPFnOpt (PForeign ts) = PForeign <$> goPTerms ts -- Traversable stuff. Inlined for termination checking. - goMPTerm : Maybe PTerm -> Core (Maybe PTerm) + goMPTerm : Maybe (PTerm' nm) -> Core (Maybe $ PTerm' nm) goMPTerm Nothing = pure Nothing goMPTerm (Just t) = Just <$> goPTerm t - goPTerms : List PTerm -> Core (List PTerm) + goPTerms : List (PTerm' nm) -> Core (List $ PTerm' nm) goPTerms [] = pure [] goPTerms (t :: ts) = (::) <$> goPTerm t <*> goPTerms ts - goPairedPTerms : List (a, PTerm) -> Core (List (a, PTerm)) + goPairedPTerms : List (x, PTerm' nm) -> Core (List (x, PTerm' nm)) goPairedPTerms [] = pure [] goPairedPTerms ((a, t) :: ts) = (::) . MkPair a <$> goPTerm t <*> goPairedPTerms ts - go3TupledPTerms : List (a, b, PTerm) -> Core (List (a, b, PTerm)) + go3TupledPTerms : List (x, y, PTerm' nm) -> Core (List (x, y, PTerm' nm)) go3TupledPTerms [] = pure [] go3TupledPTerms ((a, b, t) :: ts) = (::) . (\ c => (a, b, c)) <$> goPTerm t <*> go3TupledPTerms ts - go4TupledPTerms : List (a, b, PiInfo PTerm, PTerm) -> Core (List (a, b, PiInfo PTerm, PTerm)) + go4TupledPTerms : List (x, y, PiInfo (PTerm' nm), PTerm' nm) -> + Core (List (x, y, PiInfo (PTerm' nm), PTerm' nm)) go4TupledPTerms [] = pure [] go4TupledPTerms ((a, b, p, t) :: ts) = (\ p, d, ts => (a, b, p, d) :: ts) <$> goPiInfo p <*> goPTerm t <*> go4TupledPTerms ts - goPStringLines : List (List PStr) -> Core (List (List PStr)) + goPStringLines : List (List (PStr' nm)) -> Core (List (List (PStr' nm))) goPStringLines [] = pure [] goPStringLines (line :: lines) = (::) <$> goPStrings line <*> goPStringLines lines - goPStrings : List PStr -> Core (List PStr) + goPStrings : List (PStr' nm) -> Core (List (PStr' nm)) goPStrings [] = pure [] goPStrings (str :: strs) = (::) <$> goPStr str <*> goPStrings strs - goPDos : List PDo -> Core (List PDo) + goPDos : List (PDo' nm) -> Core (List (PDo' nm)) goPDos [] = pure [] goPDos (d :: ds) = (::) <$> goPDo d <*> goPDos ds - goPClauses : List PClause -> Core (List PClause) + goPClauses : List (PClause' nm) -> Core (List (PClause' nm)) goPClauses [] = pure [] goPClauses (cl :: cls) = (::) <$> goPClause cl <*> goPClauses cls - goMPDecls : Maybe (List PDecl) -> Core (Maybe (List PDecl)) + goMPDecls : Maybe (List (PDecl' nm)) -> Core (Maybe (List (PDecl' nm))) goMPDecls Nothing = pure Nothing goMPDecls (Just ps) = Just <$> goPDecls ps - goPDecls : List PDecl -> Core (List PDecl) + goPDecls : List (PDecl' nm) -> Core (List (PDecl' nm)) goPDecls [] = pure [] goPDecls (d :: ds) = (::) <$> goPDecl d <*> goPDecls ds - goPFieldUpdates : List PFieldUpdate -> Core (List PFieldUpdate) + goPFieldUpdates : List (PFieldUpdate' nm) -> Core (List (PFieldUpdate' nm)) goPFieldUpdates [] = pure [] goPFieldUpdates (fu :: fus) = (::) <$> goPFieldUpdate fu <*> goPFieldUpdates fus - goPFields : List PField -> Core (List PField) + goPFields : List (PField' nm) -> Core (List (PField' nm)) goPFields [] = pure [] goPFields (f :: fs) = (::) <$> goPField f <*> goPFields fs - goPFnOpts : List PFnOpt -> Core (List PFnOpt) + goPFnOpts : List (PFnOpt' nm) -> Core (List (PFnOpt' nm)) goPFnOpts [] = pure [] goPFnOpts (o :: os) = (::) <$> goPFnOpt o <*> goPFnOpts os - goPTypeDecls : List PTypeDecl -> Core (List PTypeDecl) + goPTypeDecls : List (PTypeDecl' nm) -> Core (List (PTypeDecl' nm)) goPTypeDecls [] = pure [] goPTypeDecls (t :: ts) = (::) <$> goPTypeDecl t <*> goPTypeDecls ts diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index d48991687..0b7e36def 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -247,7 +247,11 @@ export ||| Test whether a user name begins with an operator symbol. isOpName : Name -> Bool isOpName n = fromMaybe False $ do - n <- userNameRoot n + -- NB: we can't use userNameRoot because that'll prefix `RF` + -- names with a `.` which means that record fields will systematically + -- be declared to be operators. + guard (isUserName n) + let n = nameRoot n c <- fst <$> strUncons n guard (isOpChar c) pure True diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index 2bc7d79fc..6b6f125a3 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/src/TTImp/Elab/RunElab.idr @@ -17,6 +17,7 @@ import TTImp.Elab.Check import TTImp.Elab.Delayed import TTImp.Reflect import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Unelab import TTImp.Utils @@ -100,7 +101,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp = do tm' <- evalClosure defs tm defs <- get Ctxt empty <- clearDefs defs - scriptRet !(unelabUniqueBinders env !(quote empty env tm')) + scriptRet $ map rawName !(unelabUniqueBinders env !(quote empty env tm')) elabCon defs "Lambda" [x, _, scope] = do empty <- clearDefs defs NBind bfc x (Lam fc' c p ty) sc <- evalClosure defs scope @@ -127,7 +128,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp | Nothing => nfOpts withAll defs env !(reflect fc defs False env (the (Maybe RawImp) Nothing)) ty <- getTerm gty - scriptRet (Just !(unelabUniqueBinders env ty)) + scriptRet (Just $ map rawName $ !(unelabUniqueBinders env ty)) elabCon defs "LocalVars" [] = scriptRet vars elabCon defs "GenSym" [str] @@ -145,7 +146,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp where unelabType : (Name, Int, ClosedTerm) -> Core (Name, RawImp) unelabType (n, _, ty) - = pure (n, !(unelabUniqueBinders [] ty)) + = pure (n, map rawName !(unelabUniqueBinders [] ty)) elabCon defs "GetLocalType" [n] = do n' <- evalClosure defs n n <- reify defs n' @@ -153,7 +154,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp Just (MkIsDefined rigb lv) => do let binder = getBinder lv env let bty = binderType binder - scriptRet !(unelabUniqueBinders env bty) + scriptRet $ map rawName !(unelabUniqueBinders env bty) _ => throw (GenericMsg fc (show n ++ " is not a local variable")) elabCon defs "GetCons" [n] = do n' <- evalClosure defs n diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index 65504b13e..d8fed61fd 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/src/TTImp/Interactive/CaseSplit.idr @@ -16,6 +16,7 @@ import TTImp.Elab.Check import TTImp.ProcessDef import TTImp.ProcessDecls import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Unelab import TTImp.Utils @@ -354,7 +355,7 @@ mkCase {c} {u} fn orig lhs_raw setAllPublic False put Ctxt defs -- reset the context, we don't want any updates put UST ust - lhs' <- unelabNoSugar [] lhs + lhs' <- map (map rawName) $ unelabNoSugar [] lhs log "interaction.casesplit" 3 $ "Original LHS: " ++ show orig log "interaction.casesplit" 3 $ "New LHS: " ++ show lhs' @@ -401,7 +402,7 @@ getSplitsLHS fc envlen lhs_in n OK (fn, tyn, cons) <- findCons n lhs | SplitFail err => pure (SplitFail err) - rawlhs <- unelabNoSugar [] lhs + rawlhs <- map (map rawName) $ unelabNoSugar [] lhs trycases <- traverse (\c => newLHS fc envlen usedns n c rawlhs) cons let Just idx = getNameID fn (gamma defs) diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index 4c95199cb..8db591df8 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/src/TTImp/Interactive/ExprSearch.idr @@ -26,6 +26,7 @@ import Core.Value import TTImp.Elab.Check import TTImp.Interactive.CaseSplit import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Unelab import TTImp.Utils @@ -862,7 +863,7 @@ firstLinearOK fc (Result (t, ds) next) defs <- get Ctxt nft <- normaliseHoles defs [] t raw <- unelab [] !(toFullNames nft) - pure (Result raw (firstLinearOK fc !next))) + pure (Result (map rawName raw) (firstLinearOK fc !next))) (\err => do next' <- next firstLinearOK fc next') @@ -882,7 +883,7 @@ exprSearchOpts opts fc n_in hints let Hole _ _ = definition gdef | PMDef pi [] (STerm _ tm) _ _ => do raw <- unelab [] !(toFullNames !(normaliseHoles defs [] tm)) - one raw + one (map rawName raw) | _ => throw (GenericMsg fc "Name is already defined") lhs <- findHoleLHS !(getFullName (Resolved idx)) log "interaction.search" 10 $ "LHS hole data " ++ show (n, lhs) diff --git a/src/TTImp/Interactive/MakeLemma.idr b/src/TTImp/Interactive/MakeLemma.idr index e050fe835..fadf454f9 100644 --- a/src/TTImp/Interactive/MakeLemma.idr +++ b/src/TTImp/Interactive/MakeLemma.idr @@ -9,6 +9,7 @@ import Core.Value import TTImp.Unelab import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Utils import Data.List @@ -45,7 +46,7 @@ getArgs : {vars : _} -> Core (List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp), RawImp) getArgs {vars} env (S k) (Bind _ x b@(Pi _ c _ ty) sc) = do defs <- get Ctxt - ty' <- unelab env !(normalise defs env ty) + ty' <- map (map rawName) $ unelab env !(normalise defs env ty) let x' = UN !(uniqueName defs (map nameRoot vars) (nameRoot x)) (sc', ty) <- getArgs (b :: env) k (renameTop x' sc) -- Don't need to use the name if it's not used in the scope type @@ -60,7 +61,7 @@ getArgs {vars} env (S k) (Bind _ x b@(Pi _ c _ ty) sc) pure ((x, mn, p', c, ty') :: sc', ty) getArgs env k ty = do defs <- get Ctxt - ty' <- unelab env !(normalise defs env ty) + ty' <- map (map rawName) $ unelab env !(normalise defs env ty) pure ([], ty') mkType : FC -> List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp) -> diff --git a/src/TTImp/PartialEval.idr b/src/TTImp/PartialEval.idr index 8154ad083..56c84f0fc 100644 --- a/src/TTImp/PartialEval.idr +++ b/src/TTImp/PartialEval.idr @@ -13,6 +13,7 @@ import Core.UnifyState import TTImp.Elab.Check import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Unelab import Libraries.Utils.Hex @@ -150,12 +151,12 @@ getSpecPats fc pename fn stk fnty args sargs pats = do defs <- get Ctxt sc' <- sc defs (toClosure defaultOpts [] (Erased fc False)) tm' <- unelabNoSugar [] tm - mkRHSargs sc' (IApp fc app tm') as ds + mkRHSargs sc' (IApp fc app (map rawName tm')) as ds mkRHSargs (NBind _ x (Pi _ _ _ _) sc) app as ((_, Static tm) :: ds) = do defs <- get Ctxt sc' <- sc defs (toClosure defaultOpts [] (Erased fc False)) tm' <- unelabNoSugar [] tm - mkRHSargs sc' (INamedApp fc app x tm') as ds + mkRHSargs sc' (INamedApp fc app x (map rawName tm')) as ds -- Type will depend on the value here (we assume a variadic function) but -- the argument names are still needed mkRHSargs ty app (a :: as) ((_, Dynamic) :: ds) @@ -182,17 +183,17 @@ getSpecPats fc pename fn stk fnty args sargs pats Core ImpClause unelabPat pename (_ ** (env, lhs, rhs)) = do lhsapp <- unelabNoSugar env lhs - let lhs' = dropArgs pename lhsapp + let lhs' = dropArgs pename (map rawName lhsapp) defs <- get Ctxt rhsnf <- normaliseArgHoles defs env rhs rhs' <- unelabNoSugar env rhsnf - pure (PatClause fc lhs' rhs') + pure (PatClause fc lhs' (map rawName rhs')) unelabLHS : Name -> (vs ** (Env Term vs, Term vs, Term vs)) -> Core RawImp unelabLHS pename (_ ** (env, lhs, rhs)) = do lhsapp <- unelabNoSugar env lhs - pure $ dropArgs pename lhsapp + pure $ dropArgs pename (map rawName lhsapp) -- Get the reducible names in a function to be partially evaluated. In practice, -- that's all the functions it refers to @@ -308,7 +309,7 @@ mkSpecDef {vars} fc gdef pename sargs fn stk defs <- get Ctxt rhsnf <- normaliseArgHoles defs env rhs rhs' <- unelabNoSugar env rhsnf - pure (PatClause fc lhs' rhs') + pure (PatClause fc (map rawName lhs') (map rawName rhs')) showPat : ImpClause -> String showPat (PatClause _ lhs rhs) = show lhs ++ " = " ++ show rhs diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 6f22c70a7..e8fbfb6bd 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -23,6 +23,7 @@ import TTImp.Elab.Utils import TTImp.Impossible import TTImp.PartialEval import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Unelab import TTImp.Utils import TTImp.WithClause @@ -959,6 +960,7 @@ processDef opts nest env fc n_in cs_in Core (Maybe ClosedTerm) checkImpossible n mult tm = do itm <- unelabNoPatvars [] tm + let itm = map rawName itm handleUnify (do ctxt <- get Ctxt log "declare.def.impossible" 3 $ "Checking for impossibility: " ++ show itm diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index 7680d72e2..8b0a03208 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/src/TTImp/ProcessRecord.idr @@ -13,6 +13,7 @@ import TTImp.BindImplicits import TTImp.Elab import TTImp.Elab.Check import TTImp.TTImp +import TTImp.TTImp.Functor import TTImp.Unelab import TTImp.Utils @@ -143,7 +144,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields (names nest) nestDrop <- traverse (\ (n, ns) => pure (!(toFullNames n), ns)) nestDrop ty <- unelabNest nestDrop tyenv ty_chk - let ty' = substNames vars upds ty + let ty' = substNames vars upds $ map rawName ty log "declare.record.field" 5 $ "Field type: " ++ show ty' let rname = MN "rec" 0 diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 63b3a6767..881236f92 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -46,88 +46,105 @@ public export data BindMode = PI RigCount | PATTERN | NONE mutual + public export - data RawImp : Type where - IVar : FC -> Name -> RawImp - IPi : FC -> RigCount -> PiInfo RawImp -> Maybe Name -> - (argTy : RawImp) -> (retTy : RawImp) -> RawImp - ILam : FC -> RigCount -> PiInfo RawImp -> Maybe Name -> - (argTy : RawImp) -> (lamTy : RawImp) -> RawImp + RawImp : Type + RawImp = RawImp' Name + + public export + IRawImp : Type + IRawImp = RawImp' KindedName + + public export + data RawImp' : Type -> Type where + IVar : FC -> nm -> RawImp' nm + IPi : FC -> RigCount -> PiInfo (RawImp' nm) -> Maybe Name -> + (argTy : RawImp' nm) -> (retTy : RawImp' nm) -> RawImp' nm + ILam : FC -> RigCount -> PiInfo (RawImp' nm) -> Maybe Name -> + (argTy : RawImp' nm) -> (lamTy : RawImp' nm) -> RawImp' nm ILet : FC -> (lhsFC : FC) -> RigCount -> Name -> - (nTy : RawImp) -> (nVal : RawImp) -> - (scope : RawImp) -> RawImp - ICase : FC -> RawImp -> (ty : RawImp) -> - List ImpClause -> RawImp - ILocal : FC -> List ImpDecl -> RawImp -> RawImp + (nTy : RawImp' nm) -> (nVal : RawImp' nm) -> + (scope : RawImp' nm) -> RawImp' nm + ICase : FC -> RawImp' nm -> (ty : RawImp' nm) -> + List (ImpClause' nm) -> RawImp' nm + ILocal : FC -> List (ImpDecl' nm) -> RawImp' nm -> RawImp' nm -- Local definitions made elsewhere, but that we're pushing -- into a case branch as nested names. -- An appearance of 'uname' maps to an application of -- 'internalName' to 'args'. ICaseLocal : FC -> (uname : Name) -> (internalName : Name) -> - (args : List Name) -> RawImp -> RawImp + (args : List Name) -> RawImp' nm -> RawImp' nm - IUpdate : FC -> List IFieldUpdate -> RawImp -> RawImp + IUpdate : FC -> List (IFieldUpdate' nm) -> RawImp' nm -> RawImp' nm - IApp : FC -> RawImp -> RawImp -> RawImp - IAutoApp : FC -> RawImp -> RawImp -> RawImp - INamedApp : FC -> RawImp -> Name -> RawImp -> RawImp - IWithApp : FC -> RawImp -> RawImp -> RawImp + IApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm + IAutoApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm + INamedApp : FC -> RawImp' nm -> Name -> RawImp' nm -> RawImp' nm + IWithApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm - ISearch : FC -> (depth : Nat) -> RawImp - IAlternative : FC -> AltType -> List RawImp -> RawImp - IRewrite : FC -> RawImp -> RawImp -> RawImp - ICoerced : FC -> RawImp -> RawImp + ISearch : FC -> (depth : Nat) -> RawImp' nm + IAlternative : FC -> AltType' nm -> List (RawImp' nm) -> RawImp' nm + IRewrite : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm + ICoerced : FC -> RawImp' nm -> RawImp' nm -- Any implicit bindings in the scope should be bound here, using -- the given binder - IBindHere : FC -> BindMode -> RawImp -> RawImp + IBindHere : FC -> BindMode -> RawImp' nm -> RawImp' nm -- A name which should be implicitly bound - IBindVar : FC -> String -> RawImp + IBindVar : FC -> String -> RawImp' nm -- An 'as' pattern, valid on the LHS of a clause only - IAs : FC -> (nameFC : FC) -> UseSide -> Name -> RawImp -> RawImp + IAs : FC -> (nameFC : FC) -> UseSide -> Name -> RawImp' nm -> RawImp' nm -- A 'dot' pattern, i.e. one which must also have the given value -- by unification - IMustUnify : FC -> DotReason -> RawImp -> RawImp + IMustUnify : FC -> DotReason -> RawImp' nm -> RawImp' nm -- Laziness annotations - IDelayed : FC -> LazyReason -> RawImp -> RawImp -- the type - IDelay : FC -> RawImp -> RawImp -- delay constructor - IForce : FC -> RawImp -> RawImp + IDelayed : FC -> LazyReason -> RawImp' nm -> RawImp' nm -- the type + IDelay : FC -> RawImp' nm -> RawImp' nm -- delay constructor + IForce : FC -> RawImp' nm -> RawImp' nm -- Quasiquoting - IQuote : FC -> RawImp -> RawImp - IQuoteName : FC -> Name -> RawImp - IQuoteDecl : FC -> List ImpDecl -> RawImp - IUnquote : FC -> RawImp -> RawImp - IRunElab : FC -> RawImp -> RawImp + IQuote : FC -> RawImp' nm -> RawImp' nm + IQuoteName : FC -> Name -> RawImp' nm + IQuoteDecl : FC -> List (ImpDecl' nm) -> RawImp' nm + IUnquote : FC -> RawImp' nm -> RawImp' nm + IRunElab : FC -> RawImp' nm -> RawImp' nm - IPrimVal : FC -> (c : Constant) -> RawImp - IType : FC -> RawImp - IHole : FC -> String -> RawImp + IPrimVal : FC -> (c : Constant) -> RawImp' nm + IType : FC -> RawImp' nm + IHole : FC -> String -> RawImp' nm - IUnifyLog : FC -> LogLevel -> RawImp -> RawImp + IUnifyLog : FC -> LogLevel -> RawImp' nm -> RawImp' nm -- An implicit value, solved by unification, but which will also be -- bound (either as a pattern variable or a type variable) if unsolved -- at the end of elaborator - Implicit : FC -> (bindIfUnsolved : Bool) -> RawImp + Implicit : FC -> (bindIfUnsolved : Bool) -> RawImp' nm -- with-disambiguation - IWithUnambigNames : FC -> List Name -> RawImp -> RawImp + IWithUnambigNames : FC -> List Name -> RawImp' nm -> RawImp' nm public export - data IFieldUpdate : Type where - ISetField : (path : List String) -> RawImp -> IFieldUpdate - ISetFieldApp : (path : List String) -> RawImp -> IFieldUpdate + IFieldUpdate : Type + IFieldUpdate = IFieldUpdate' Name public export - data AltType : Type where - FirstSuccess : AltType - Unique : AltType - UniqueDefault : RawImp -> AltType + data IFieldUpdate' : Type -> Type where + ISetField : (path : List String) -> RawImp' nm -> IFieldUpdate' nm + ISetFieldApp : (path : List String) -> RawImp' nm -> IFieldUpdate' nm + + public export + AltType : Type + AltType = AltType' Name + + public export + data AltType' : Type -> Type where + FirstSuccess : AltType' nm + Unique : AltType' nm + UniqueDefault : RawImp' nm -> AltType' nm export - Show RawImp where + Show nm => Show (RawImp' nm) where show (IVar fc n) = show n show (IPi fc c p n arg ret) = "(%pi " ++ show c ++ " " ++ show p ++ " " ++ @@ -185,35 +202,39 @@ mutual show (IWithUnambigNames fc ns rhs) = "(%with " ++ show ns ++ " " ++ show rhs ++ ")" export - Show IFieldUpdate where + Show nm => Show (IFieldUpdate' nm) where show (ISetField p val) = showSep "->" p ++ " = " ++ show val show (ISetFieldApp p val) = showSep "->" p ++ " $= " ++ show val public export - data FnOpt : Type where - Inline : FnOpt - TCInline : FnOpt - -- Flag means the hint is a direct hint, not a function which might - -- find the result (e.g. chasing parent interface dictionaries) - Hint : Bool -> FnOpt - -- Flag means to use as a default if all else fails - GlobalHint : Bool -> FnOpt - ExternFn : FnOpt - -- Defined externally, list calling conventions - ForeignFn : List RawImp -> FnOpt - -- assume safe to cancel arguments in unification - Invertible : FnOpt - Totality : TotalReq -> FnOpt - Macro : FnOpt - SpecArgs : List Name -> FnOpt + FnOpt : Type + FnOpt = FnOpt' Name public export - isTotalityReq : FnOpt -> Bool + data FnOpt' : Type -> Type where + Inline : FnOpt' nm + TCInline : FnOpt' nm + -- Flag means the hint is a direct hint, not a function which might + -- find the result (e.g. chasing parent interface dictionaries) + Hint : Bool -> FnOpt' nm + -- Flag means to use as a default if all else fails + GlobalHint : Bool -> FnOpt' nm + ExternFn : FnOpt' nm + -- Defined externally, list calling conventions + ForeignFn : List (RawImp' nm) -> FnOpt' nm + -- assume safe to cancel arguments in unification + Invertible : FnOpt' nm + Totality : TotalReq -> FnOpt' nm + Macro : FnOpt' nm + SpecArgs : List Name -> FnOpt' nm + + public export + isTotalityReq : FnOpt' nm -> Bool isTotalityReq (Totality _) = True isTotalityReq _ = False export - Show FnOpt where + Show nm => Show (FnOpt' nm) where show Inline = "%inline" show TCInline = "%tcinline" show (Hint t) = "%hint " ++ show t @@ -242,11 +263,15 @@ mutual _ == _ = False public export - data ImpTy : Type where - MkImpTy : FC -> (nameFC : FC) -> (n : Name) -> (ty : RawImp) -> ImpTy + ImpTy : Type + ImpTy = ImpTy' Name + + public export + data ImpTy' : Type -> Type where + MkImpTy : FC -> (nameFC : FC) -> (n : Name) -> (ty : RawImp' nm) -> ImpTy' nm export - Show ImpTy where + Show nm => Show (ImpTy' nm) where show (MkImpTy fc _ n ty) = "(%claim " ++ show n ++ " " ++ show ty ++ ")" public export @@ -267,14 +292,18 @@ mutual (==) _ _ = False public export - data ImpData : Type where - MkImpData : FC -> (n : Name) -> (tycon : RawImp) -> + ImpData : Type + ImpData = ImpData' Name + + public export + data ImpData' : Type -> Type where + MkImpData : FC -> (n : Name) -> (tycon : RawImp' nm) -> (opts : List DataOpt) -> - (datacons : List ImpTy) -> ImpData - MkImpLater : FC -> (n : Name) -> (tycon : RawImp) -> ImpData + (datacons : List (ImpTy' nm)) -> ImpData' nm + MkImpLater : FC -> (n : Name) -> (tycon : RawImp' nm) -> ImpData' nm export - Show ImpData where + Show nm => Show (ImpData' nm) where show (MkImpData fc n tycon _ cons) = "(%data " ++ show n ++ " " ++ show tycon ++ " " ++ show cons ++ ")" @@ -282,25 +311,38 @@ mutual = "(%datadecl " ++ show n ++ " " ++ show tycon ++ ")" public export - data IField : Type where - MkIField : FC -> RigCount -> PiInfo RawImp -> Name -> RawImp -> - IField + IField : Type + IField = IField' Name public export - data ImpRecord : Type where + data IField' : Type -> Type where + MkIField : FC -> RigCount -> PiInfo (RawImp' nm) -> Name -> RawImp' nm -> + IField' nm + + -- TODO: turn into a proper datatype + public export + ImpParameter' : Type -> Type + ImpParameter' nm = (Name, RigCount, PiInfo (RawImp' nm), RawImp' nm) + + public export + ImpRecord : Type + ImpRecord = ImpRecord' Name + + public export + data ImpRecord' : Type -> Type where MkImpRecord : FC -> (n : Name) -> - (params : List (Name, RigCount, PiInfo RawImp, RawImp)) -> + (params : List (ImpParameter' nm)) -> (conName : Name) -> - (fields : List IField) -> - ImpRecord + (fields : List (IField' nm)) -> + ImpRecord' nm export - Show IField where + Show nm => Show (IField' nm) where show (MkIField _ c Explicit n ty) = show n ++ " : " ++ show ty show (MkIField _ c _ n ty) = "{" ++ show n ++ " : " ++ show ty ++ "}" export - Show ImpRecord where + Show nm => Show (ImpRecord' nm) where show (MkImpRecord _ n params con fields) = "record " ++ show n ++ " " ++ show params ++ " " ++ show con ++ "\n\t" ++ @@ -315,16 +357,24 @@ mutual Syntactic == Syntactic = True public export - data ImpClause : Type where - PatClause : FC -> (lhs : RawImp) -> (rhs : RawImp) -> ImpClause - WithClause : FC -> (lhs : RawImp) -> - (wval : RawImp) -> (prf : Maybe Name) -> + ImpClause : Type + ImpClause = ImpClause' Name + + public export + IImpClause : Type + IImpClause = ImpClause' KindedName + + public export + data ImpClause' : Type -> Type where + PatClause : FC -> (lhs : RawImp' nm) -> (rhs : RawImp' nm) -> ImpClause' nm + WithClause : FC -> (lhs : RawImp' nm) -> + (wval : RawImp' nm) -> (prf : Maybe Name) -> (flags : List WithFlag) -> - List ImpClause -> ImpClause - ImpossibleClause : FC -> (lhs : RawImp) -> ImpClause + List (ImpClause' nm) -> ImpClause' nm + ImpossibleClause : FC -> (lhs : RawImp' nm) -> ImpClause' nm export - Show ImpClause where + Show nm => Show (ImpClause' nm) where show (PatClause fc lhs rhs) = show lhs ++ " = " ++ show rhs show (WithClause fc lhs wval prf flags block) @@ -336,30 +386,35 @@ mutual = show lhs ++ " impossible" public export - data ImpDecl : Type where - IClaim : FC -> RigCount -> Visibility -> List FnOpt -> - ImpTy -> ImpDecl - IData : FC -> Visibility -> ImpData -> ImpDecl - IDef : FC -> Name -> List ImpClause -> ImpDecl - IParameters : FC -> List (Name, RigCount, PiInfo RawImp, RawImp) -> - List ImpDecl -> ImpDecl + ImpDecl : Type + ImpDecl = ImpDecl' Name + + public export + data ImpDecl' : Type -> Type where + IClaim : FC -> RigCount -> Visibility -> List (FnOpt' nm) -> + ImpTy' nm -> ImpDecl' nm + IData : FC -> Visibility -> ImpData' nm -> ImpDecl' nm + IDef : FC -> Name -> List (ImpClause' nm) -> ImpDecl' nm + IParameters : FC -> + List (ImpParameter' nm) -> + List (ImpDecl' nm) -> ImpDecl' nm IRecord : FC -> Maybe String -> -- nested namespace - Visibility -> ImpRecord -> ImpDecl - INamespace : FC -> Namespace -> List ImpDecl -> ImpDecl - ITransform : FC -> Name -> RawImp -> RawImp -> ImpDecl - IRunElabDecl : FC -> RawImp -> ImpDecl + Visibility -> ImpRecord' nm -> ImpDecl' nm + INamespace : FC -> Namespace -> List (ImpDecl' nm) -> ImpDecl' nm + ITransform : FC -> Name -> RawImp' nm -> RawImp' nm -> ImpDecl' nm + IRunElabDecl : FC -> RawImp' nm -> ImpDecl' nm IPragma : List Name -> -- pragmas might define names that wouldn't -- otherwise be spotted in 'definedInBlock' so they -- can be flagged here. ({vars : _} -> NestedNames vars -> Env Term vars -> Core ()) -> - ImpDecl - ILog : Maybe (List String, Nat) -> ImpDecl - IBuiltin : FC -> BuiltinType -> Name -> ImpDecl + ImpDecl' nm + ILog : Maybe (List String, Nat) -> ImpDecl' nm + IBuiltin : FC -> BuiltinType -> Name -> ImpDecl' nm export - Show ImpDecl where + Show nm => Show (ImpDecl' nm) where show (IClaim _ c _ opts ty) = show opts ++ " " ++ show c ++ " " ++ show ty show (IData _ _ d) = show d show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")" @@ -382,7 +437,7 @@ mutual show (IBuiltin _ type name) = "%builtin " ++ show type ++ " " ++ show name export -isIPrimVal : RawImp -> Maybe Constant +isIPrimVal : RawImp' nm -> Maybe Constant isIPrimVal (IPrimVal _ c) = Just c isIPrimVal _ = Nothing @@ -400,7 +455,7 @@ data ImpREPL : Type where Quit : ImpREPL export -mapAltType : (RawImp -> RawImp) -> AltType -> AltType +mapAltType : (RawImp' nm -> RawImp' nm) -> AltType' nm -> AltType' nm mapAltType f (UniqueDefault x) = UniqueDefault (f x) mapAltType _ u = u @@ -432,7 +487,7 @@ lhsInCurrentNS nest (IVar loc n) lhsInCurrentNS nest tm = pure tm export -findIBinds : RawImp -> List String +findIBinds : RawImp' nm -> List String findIBinds (IPi fc rig p mn aty retty) = findIBinds aty ++ findIBinds retty findIBinds (ILam fc rig p n aty sc) @@ -466,7 +521,7 @@ findIBinds (IBindVar _ n) = [n] findIBinds tm = [] export -findImplicits : RawImp -> List String +findImplicits : RawImp' nm -> List String findImplicits (IPi fc rig p (Just (UN mn)) aty retty) = mn :: findImplicits aty ++ findImplicits retty findImplicits (IPi fc rig p mn aty retty) @@ -679,7 +734,7 @@ definedInBlock ns decls = defName _ _ = [] export -getFC : RawImp -> FC +getFC : RawImp' nm -> FC getFC (IVar x _) = x getFC (IPi x _ _ _ _ _) = x getFC (ILam x _ _ _ _ _) = x @@ -718,7 +773,7 @@ getFC (IWithUnambigNames x _ _) = x namespace ImpDecl public export - getFC : ImpDecl -> FC + getFC : ImpDecl' nm -> FC getFC (IClaim fc _ _ _ _) = fc getFC (IData fc _ _) = fc getFC (IDef fc _ _) = fc @@ -732,24 +787,24 @@ namespace ImpDecl getFC (IBuiltin fc _ _) = fc export -apply : RawImp -> List RawImp -> RawImp +apply : RawImp' nm -> List (RawImp' nm) -> RawImp' nm apply f [] = f apply f (x :: xs) = let fFC = getFC f in apply (IApp (fromMaybe fFC (mergeFC fFC (getFC x))) f x) xs export -gapply : RawImp -> List (Maybe Name, RawImp) -> RawImp +gapply : RawImp' nm -> List (Maybe Name, RawImp' nm) -> RawImp' nm gapply f [] = f gapply f (x :: xs) = gapply (uncurry (app f) x) xs where - app : RawImp -> Maybe Name -> RawImp -> RawImp + app : RawImp' nm -> Maybe Name -> RawImp' nm -> RawImp' nm app f Nothing x = IApp (getFC f) f x app f (Just nm) x = INamedApp (getFC f) f nm x export -getFn : RawImp -> RawImp +getFn : RawImp' nm -> RawImp' nm getFn (IApp _ f _) = getFn f getFn (IWithApp _ f _) = getFn f getFn (INamedApp _ f _ _) = getFn f diff --git a/src/TTImp/TTImp/Functor.idr b/src/TTImp/TTImp/Functor.idr new file mode 100644 index 000000000..cd5d3c7cc --- /dev/null +++ b/src/TTImp/TTImp/Functor.idr @@ -0,0 +1,160 @@ +module TTImp.TTImp.Functor + +import Core.TT +import TTImp.TTImp + +%default covering + +mutual + + export + Functor RawImp' where + map f (IVar fc nm) = IVar fc (f nm) + map f (IPi fc rig info nm a sc) + = IPi fc rig (map (map f) info) nm (map f a) (map f sc) + map f (ILam fc rig info nm a sc) + = ILam fc rig (map (map f) info) nm (map f a) (map f sc) + map f (ILet fc lhsFC rig nm ty val sc) + = ILet fc lhsFC rig nm (map f ty) (map f val) (map f sc) + map f (ICase fc sc ty cls) + = ICase fc (map f sc) (map f ty) (map (map f) cls) + map f (ILocal fc ds sc) + = ILocal fc (map (map f) ds) (map f sc) + map f (ICaseLocal fc userN intN args sc) + = ICaseLocal fc userN intN args (map f sc) + map f (IUpdate fc upds rec) + = IUpdate fc (map (map f) upds) (map f rec) + map f (IApp fc fn t) + = IApp fc (map f fn) (map f t) + map f (IAutoApp fc fn t) + = IAutoApp fc (map f fn) (map f t) + map f (INamedApp fc fn nm t) + = INamedApp fc (map f fn) nm (map f t) + map f (IWithApp fc fn t) + = IWithApp fc (map f fn) (map f t) + map f (ISearch fc n) + = ISearch fc n + map f (IAlternative fc alt ts) + = IAlternative fc (map f alt) (map (map f) ts) + map f (IRewrite fc e t) + = IRewrite fc (map f e) (map f t) + map f (ICoerced fc e) + = ICoerced fc (map f e) + map f (IBindHere fc bd t) + = IBindHere fc bd (map f t) + map f (IBindVar fc str) + = IBindVar fc str + map f (IAs fc nmFC side nm t) + = IAs fc nmFC side nm (map f t) + map f (IMustUnify fc reason t) + = IMustUnify fc reason (map f t) + map f (IDelayed fc reason t) + = IDelayed fc reason (map f t) + map f (IDelay fc t) + = IDelay fc (map f t) + map f (IForce fc t) + = IForce fc (map f t) + map f (IQuote fc t) + = IQuote fc (map f t) + map f (IQuoteName fc nm) + = IQuoteName fc nm + map f (IQuoteDecl fc ds) + = IQuoteDecl fc (map (map f) ds) + map f (IUnquote fc t) + = IUnquote fc (map f t) + map f (IRunElab fc t) + = IRunElab fc (map f t) + map f (IPrimVal fc c) + = IPrimVal fc c + map f (IType fc) + = IType fc + map f (IHole fc str) + = IHole fc str + map f (IUnifyLog fc lvl t) + = IUnifyLog fc lvl (map f t) + map f (Implicit fc b) + = Implicit fc b + map f (IWithUnambigNames fc ns t) + = IWithUnambigNames fc ns (map f t) + + export + Functor ImpClause' where + map f (PatClause fc lhs rhs) + = PatClause fc (map f lhs) (map f rhs) + map f (WithClause fc lhs wval prf flags xs) + = WithClause fc (map f lhs) (map f wval) prf flags (map (map f) xs) + map f (ImpossibleClause fc lhs) + = ImpossibleClause fc (map f lhs) + + export + Functor ImpDecl' where + map f (IClaim fc rig vis opts ty) + = IClaim fc rig vis (map (map f) opts) (map f ty) + map f (IData fc vis dt) + = IData fc vis (map f dt) + map f (IDef fc nm cls) + = IDef fc nm (map (map f) cls) + map f (IParameters fc ps ds) + = IParameters fc (map (map {f = ImpParameter'} f) ps) (map (map f) ds) + map f (IRecord fc cs vis rec) + = IRecord fc cs vis (map f rec) + map f (INamespace fc ns ds) + = INamespace fc ns (map (map f) ds) + map f (ITransform fc n lhs rhs) + = ITransform fc n (map f lhs) (map f rhs) + map f (IRunElabDecl fc t) + = IRunElabDecl fc (map f t) + map f (IPragma xs k) = IPragma xs k + map f (ILog x) = ILog x + map f (IBuiltin fc ty n) = IBuiltin fc ty n + + export + Functor FnOpt' where + map f Inline = Inline + map f TCInline = TCInline + map f (Hint b) = Hint b + map f (GlobalHint b) = GlobalHint b + map f ExternFn = ExternFn + map f (ForeignFn ts) = ForeignFn (map (map f) ts) + map f Invertible = Invertible + map f (Totality tot) = Totality tot + map f Macro = Macro + map f (SpecArgs ns) = SpecArgs ns + + export + Functor ImpTy' where + map f (MkImpTy fc nameFC n ty) + = MkImpTy fc nameFC n (map f ty) + + export + Functor ImpData' where + map f (MkImpData fc n tycon opts datacons) + = MkImpData fc n (map f tycon) opts (map (map f) datacons) + map f (MkImpLater fc n tycon) + = MkImpLater fc n (map f tycon) + + export + Functor IField' where + map f (MkIField fc rig info n t) + = MkIField fc rig (map (map f) info) n (map f t) + + export + Functor ImpRecord' where + map f (MkImpRecord fc n params conName fields) + = MkImpRecord fc n (map (map {f = ImpParameter'} f) params) + conName (map (map f) fields) + + export + Functor ImpParameter' where + map f (nm, rig, info, t) = (nm, rig, map (map f) info, map f t) + + export + Functor IFieldUpdate' where + map f (ISetField path t) = ISetField path (map f t) + map f (ISetFieldApp path t) = ISetFieldApp path (map f t) + + export + Functor AltType' where + map f FirstSuccess = FirstSuccess + map f Unique = Unique + map f (UniqueDefault t) = UniqueDefault (map f t) diff --git a/src/TTImp/Unelab.idr b/src/TTImp/Unelab.idr index 458405669..0d2ed0c65 100644 --- a/src/TTImp/Unelab.idr +++ b/src/TTImp/Unelab.idr @@ -33,11 +33,11 @@ used idx (TForce _ _ tm) = used idx tm used idx _ = False data IArg - = Exp FC RawImp - | Auto FC RawImp - | Named FC Name RawImp + = Exp FC IRawImp + | Auto FC IRawImp + | Named FC Name IRawImp -unIArg : IArg -> RawImp +unIArg : IArg -> IRawImp unIArg (Exp _ t) = t unIArg (Auto _ t) = t unIArg (Named _ _ t) = t @@ -47,7 +47,7 @@ Show IArg where show (Auto fc t) = "@{" ++ show t ++ "}" show (Named fc n t) = "{" ++ show n ++ " = " ++ show t ++ "}" -getFnArgs : RawImp -> List IArg -> (RawImp, List IArg) +getFnArgs : IRawImp -> List IArg -> (IRawImp, List IArg) getFnArgs (IApp fc f arg) args = getFnArgs f (Exp fc arg :: args) getFnArgs (INamedApp fc f n arg) args = getFnArgs f (Named fc n arg :: args) getFnArgs (IAutoApp fc f arg) args = getFnArgs f (Auto fc arg :: args) @@ -67,8 +67,8 @@ Eq UnelabMode where mutual unelabCase : {auto c : Ref Ctxt Defs} -> List (Name, Nat) -> - Name -> List IArg -> RawImp -> - Core RawImp + Name -> List IArg -> IRawImp -> + Core IRawImp unelabCase nest n args orig = do defs <- get Ctxt Just glob <- lookupCtxtExact n (gamma defs) @@ -103,7 +103,7 @@ mutual mkClause : FC -> Nat -> (vs ** (Env Term vs, Term vs, Term vs)) -> - Core ImpClause + Core IImpClause mkClause fc dropped (vs ** (env, lhs, rhs)) = do let pat = nthArg fc dropped lhs logTerm "unelab.case" 20 "Unelaborating LHS" pat @@ -114,7 +114,7 @@ mutual pure (PatClause fc (fst lhs') (fst rhs')) mkCase : List (vs ** (Env Term vs, Term vs, Term vs)) -> - Nat -> Nat -> List IArg -> Core RawImp + Nat -> Nat -> List IArg -> Core IRawImp mkCase pats (S k) dropped (_ :: args) = mkCase pats k (S dropped) args mkCase pats Z dropped (Exp fc tm :: _) = do pats' <- traverse (mkClause fc dropped) pats @@ -124,14 +124,14 @@ mutual unelabSugar : {auto c : Ref Ctxt Defs} -> (umode : UnelabMode) -> (nest : List (Name, Nat)) -> - (RawImp, Glued vars) -> - Core (RawImp, Glued vars) + (IRawImp, Glued vars) -> + Core (IRawImp, Glued vars) unelabSugar (NoSugar _) nest res = pure res unelabSugar ImplicitHoles nest res = pure res unelabSugar _ nest (tm, ty) = let (f, args) = getFnArgs tm [] in case f of - IVar fc (NS ns (CaseBlock n i)) => + IVar fc (MkKindedName _ (NS ns (CaseBlock n i))) => do log "unelab.case" 20 $ unlines [ "Unelaborating case " ++ show (n, i) , "with arguments: " ++ show args @@ -142,17 +142,17 @@ mutual _ => pure (tm, ty) dropParams : {auto c : Ref Ctxt Defs} -> - List (Name, Nat) -> (RawImp, Glued vars) -> - Core (RawImp, Glued vars) + List (Name, Nat) -> (IRawImp, Glued vars) -> + Core (IRawImp, Glued vars) dropParams nest (tm, ty) = case getFnArgs tm [] of (IVar fc n, args) => - case lookup n nest of + case lookup (rawName n) nest of Nothing => pure (tm, ty) Just i => pure $ (apply (IVar fc n) (drop i args), ty) _ => pure (tm, ty) where - apply : RawImp -> List IArg -> RawImp + apply : IRawImp -> List IArg -> IRawImp apply tm [] = tm apply tm (Exp fc a :: args) = apply (IApp fc tm a) args apply tm (Auto fc a :: args) = apply (IAutoApp fc tm a) args @@ -168,7 +168,7 @@ mutual (umode : UnelabMode) -> (nest : List (Name, Nat)) -> Env Term vars -> Term vars -> - Core (RawImp, Glued vars) + Core (IRawImp, Glued vars) unelabTy umode nest env tm = unelabSugar umode nest !(dropParams nest !(unelabTy' umode nest env tm)) @@ -177,18 +177,18 @@ mutual (umode : UnelabMode) -> (nest : List (Name, Nat)) -> Env Term vars -> Term vars -> - Core (RawImp, Glued vars) + Core (IRawImp, Glued vars) unelabTy' umode nest env (Local fc _ idx p) = do let nm = nameAt p log "unelab.case" 20 $ "Found local name: " ++ show nm let ty = gnf env (binderType (getBinder p env)) - pure (IVar fc nm, ty) + pure (IVar fc (MkKindedName (Just Bound) nm), ty) unelabTy' umode nest env (Ref fc nt n) = do defs <- get Ctxt Just ty <- lookupTyExact n (gamma defs) | Nothing => case umode of ImplicitHoles => pure (Implicit fc True, gErased fc) - _ => pure (IVar fc n, gErased fc) + _ => pure (IVar fc (MkKindedName (Just nt) n), gErased fc) fn <- getFullName n n' <- case umode of NoSugar _ => pure fn @@ -199,7 +199,7 @@ mutual , "sugared to", show n' ] - pure (IVar fc n', gnf env (embed ty)) + pure (IVar fc (MkKindedName (Just nt) n'), gnf env (embed ty)) unelabTy' umode nest env (Meta fc n i args) = do defs <- get Ctxt let mkn = nameRoot n @@ -250,7 +250,7 @@ mutual case p' of IVar _ n => case umode of - NoSugar _ => pure (IAs fc (getLoc p) s n tm', ty) + NoSugar _ => pure (IAs fc (getLoc p) s n.rawName tm', ty) _ => pure (tm', ty) _ => pure (tm', ty) -- Should never happen! unelabTy' umode nest env (TDelayed fc r tm) @@ -277,7 +277,7 @@ mutual (umode : UnelabMode) -> (nest : List (Name, Nat)) -> Env Term vars -> PiInfo (Term vars) -> - Core (PiInfo RawImp) + Core (PiInfo IRawImp) unelabPi umode nest env Explicit = pure Explicit unelabPi umode nest env Implicit = pure Implicit unelabPi umode nest env AutoImplicit = pure AutoImplicit @@ -291,8 +291,8 @@ mutual (nest : List (Name, Nat)) -> FC -> Env Term vars -> (x : Name) -> Binder (Term vars) -> Term (x :: vars) -> - RawImp -> Term (x :: vars) -> - Core (RawImp, Glued vars) + IRawImp -> Term (x :: vars) -> + Core (IRawImp, Glued vars) unelabBinder umode nest fc env x (Lam fc' rig p ty) sctm sc scty = do (ty', _) <- unelabTy umode nest env ty p' <- unelabPi umode nest env p @@ -334,7 +334,7 @@ mutual export unelabNoSugar : {vars : _} -> {auto c : Ref Ctxt Defs} -> - Env Term vars -> Term vars -> Core RawImp + Env Term vars -> Term vars -> Core IRawImp unelabNoSugar env tm = do tm' <- unelabTy (NoSugar False) [] env tm pure $ fst tm' @@ -342,7 +342,7 @@ unelabNoSugar env tm export unelabUniqueBinders : {vars : _} -> {auto c : Ref Ctxt Defs} -> - Env Term vars -> Term vars -> Core RawImp + Env Term vars -> Term vars -> Core IRawImp unelabUniqueBinders env tm = do tm' <- unelabTy (NoSugar True) [] env tm pure $ fst tm' @@ -350,7 +350,7 @@ unelabUniqueBinders env tm export unelabNoPatvars : {vars : _} -> {auto c : Ref Ctxt Defs} -> - Env Term vars -> Term vars -> Core RawImp + Env Term vars -> Term vars -> Core IRawImp unelabNoPatvars env tm = do tm' <- unelabTy ImplicitHoles [] env tm pure $ fst tm' @@ -360,7 +360,7 @@ unelabNest : {vars : _} -> {auto c : Ref Ctxt Defs} -> List (Name, Nat) -> Env Term vars -> - Term vars -> Core RawImp + Term vars -> Core IRawImp unelabNest nest env (Meta fc n i args) = do let mkn = nameRoot n ++ showScope args pure (IHole fc mkn) @@ -384,5 +384,5 @@ export unelab : {vars : _} -> {auto c : Ref Ctxt Defs} -> Env Term vars -> - Term vars -> Core RawImp + Term vars -> Core IRawImp unelab = unelabNest [] diff --git a/tests/idris2/coverage004/expected b/tests/idris2/coverage004/expected index 9493332a0..d3246b856 100644 --- a/tests/idris2/coverage004/expected +++ b/tests/idris2/coverage004/expected @@ -1,5 +1,5 @@ 1/1: Building Cover (Cover.idr) -Error: While processing left hand side of bad. Can't match on Just (fromInteger 0) as it must have a polymorphic type. +Error: While processing left hand side of bad. Can't match on Just 0 as it must have a polymorphic type. Cover:14:6--14:12 10 | diff --git a/tests/idris2/docs001/expected b/tests/idris2/docs001/expected index 47413c3aa..571924be6 100644 --- a/tests/idris2/docs001/expected +++ b/tests/idris2/docs001/expected @@ -22,11 +22,12 @@ Main> Prelude.List : Type -> Type Main> Prelude.Show : Type -> Type Things that have a canonical `String` representation. Parameters: ty + Constructor: MkShow Methods: - show : (x : ty) -> String + show : ty -> String Convert a value to its `String` representation. @ x the value to convert - showPrec : (d : Prec) -> (x : ty) -> String + showPrec : Prec -> ty -> String Convert a value to its `String` representation in a certain precedence context. @@ -69,9 +70,11 @@ Main> Prelude.show : Show ty => ty -> String Main> Prelude.Monad : (Type -> Type) -> Type Parameters: m Constraints: Applicative m + Constructor: MkMonad Methods: (>>=) : m a -> (a -> m b) -> m b Also called `bind`. + Fixity Declaration: infixl operator, level 1 join : m (m a) -> m a Also called `flatten` or mu. Implementations: @@ -81,5 +84,5 @@ Main> Prelude.Monad : (Type -> Type) -> Type Monad (Either e) Monad List Main> 1 : Integer - Primitive + Primitive Main> Bye for now! diff --git a/tests/idris2/docs002/expected b/tests/idris2/docs002/expected index e98ea8f89..964c072f2 100644 --- a/tests/idris2/docs002/expected +++ b/tests/idris2/docs002/expected @@ -6,16 +6,13 @@ WrappedInt : Type a : SimpleRec -> Int b : SimpleRec -> String hello : Int -> Int - Hello! world : Nat -> Nat - World! Doc> Doc.NS.NestedNS.Foo : Type A type of Foo Doc> Doc.WrappedInt : Type Totality: total Constructor: MkWrappedInt : Int -> WrappedInt - Doc> Doc.SimpleRec : Type Totality: total Constructor: MkSimpleRec : Int -> String -> SimpleRec diff --git a/tests/idris2/docs003/expected b/tests/idris2/docs003/expected index 8341707a4..e49072d8a 100644 --- a/tests/idris2/docs003/expected +++ b/tests/idris2/docs003/expected @@ -14,6 +14,6 @@ RecordDoc> RecordDoc.Singleton : a -> Type Totality: total Constructor: __mkSingleton : _ Projections: - equal : ({rec:0} : Singleton v) -> value rec = v + equal : (rec : Singleton v) -> value rec = v value : Singleton v -> a RecordDoc> Bye for now! diff --git a/tests/idris2/interactive030/expected b/tests/idris2/interactive030/expected index fd31eef88..2c780018c 100644 --- a/tests/idris2/interactive030/expected +++ b/tests/idris2/interactive030/expected @@ -21,9 +21,11 @@ Main> Prelude.<$> : Functor f => (a -> b) -> f a -> f b Main> Prelude.Monad : (Type -> Type) -> Type Parameters: m Constraints: Applicative m + Constructor: MkMonad Methods: (>>=) : m a -> (a -> m b) -> m b Also called `bind`. + Fixity Declaration: infixl operator, level 1 join : m (m a) -> m a Also called `flatten` or mu. Implementations: diff --git a/tests/idris2/perf005/expected b/tests/idris2/perf005/expected index d9e659f1f..9b3f3ffc6 100644 --- a/tests/idris2/perf005/expected +++ b/tests/idris2/perf005/expected @@ -12,14 +12,15 @@ Lambda:62:3--88:9 67 | (Func 1/1: Building Bad1 (Bad1.idr) -Error: Couldn't parse declaration. +Error: Couldn't parse any alternatives: +1: Not the end of a block entry. -Bad1:3:1--3:5 +Bad1:3:20--3:21 1 | module Bad1 2 | 3 | data Bad = BadDCon (x : Nat) - ^^^^ - + ^ +... (2 others) 1/1: Building Bad2 (Bad2.idr) Error: Cannot return a named argument. diff --git a/tests/idris2/pretty001/expected b/tests/idris2/pretty001/expected index fae943ebb..149b114bd 100644 --- a/tests/idris2/pretty001/expected +++ b/tests/idris2/pretty001/expected @@ -30,10 +30,10 @@ def1 m n = m `div` n Issue1328A> Issue1328A.def2 : Integer -> Integer -> Integer def2 m n = m `div` n Issue1328A> Issue1328A.inDef0 : Nat -inDef0 = fromInteger 42 + fromInteger 21 +inDef0 = 42 + 21 Issue1328A> Issue1328A.inDef1 : Nat -inDef1 = fromInteger 42 + fromInteger 21 +inDef1 = 42 + 21 Issue1328A> Issue1328A.inDef2 : Nat -inDef2 = fromInteger 42 + fromInteger 21 +inDef2 = 42 + 21 Issue1328A> Bye for now! diff --git a/tests/idris2/reflection002/expected b/tests/idris2/reflection002/expected index a08ce16a8..fdb4e62bf 100644 --- a/tests/idris2/reflection002/expected +++ b/tests/idris2/reflection002/expected @@ -1,6 +1,6 @@ 1/1: Building power (power.idr) Main> Main.cube : Nat -> Nat -cube = \x => mult x (mult x (mult x (const (fromInteger 1) x))) +cube = \x => mult x (mult x (mult x (const 1 x))) Main> 27 Main> Main.cube' : Nat -> Nat cube' = \x => mult (mult (plus x 0) x) x