idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 10:41:59 +03:00
Code Issues Projects Releases Wiki Activity

[ new ] semantic highlighting in REPL & holes (#1836)

Browse Source
This commit is contained in:
G. Allais 2021-08-13 16:00:54 +01:00 committed by GitHub
parent 82796b3936
commit c1ebc0535d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
33 changed files with 1094 additions and 656 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
idris2api.ipkg
View File

@ -199,6 +199,7 @@ modules =
TTImp.ProcessType,
TTImp.Reflect,
TTImp.TTImp,
TTImp.TTImp.Functor,
TTImp.Unelab,
TTImp.Utils,
TTImp.WithClause,

15
src/Core/Metadata.idr
View File

@ -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)

9
src/Core/TT.idr
View File

@ -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

138
src/Idris/Doc/String.idr
View File

@ -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

3
src/Idris/Elab/Implementation.idr
View File

@ -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 []

3
src/Idris/Error.idr
View File

@ -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

7
src/Idris/IDEMode/CaseSplit.idr
View File

@ -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

4
src/Idris/IDEMode/Holes.idr
View File

@ -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

15
src/Idris/Parser.idr
View File

@ -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

119
src/Idris/Pretty.idr
View File

@ -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

47
src/Idris/REPL.idr
View File

@ -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))

8
src/Idris/REPL/Common.idr
View File

@ -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

140
src/Idris/Resugar.idr
View File

@ -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

653
src/Idris/Syntax.idr
View File

@ -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) = " | <<with alts not possible>>;"
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) = " | <<with alts not possible>>;"
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 _) = " | <<with alts not possible>>"
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 _) = " | <<with alts not possible>>"
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) = "`[ <<declaration>> ]"
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) = "`[ <<declaration>> ]"
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

6
src/Parser/Lexer/Source.idr
View File

@ -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

9
src/TTImp/Elab/RunElab.idr
View File

@ -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

5
src/TTImp/Interactive/CaseSplit.idr
View File

@ -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)

5
src/TTImp/Interactive/ExprSearch.idr
View File

@ -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)

5
src/TTImp/Interactive/MakeLemma.idr
View File

@ -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) ->

13
src/TTImp/PartialEval.idr
View File

@ -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

2
src/TTImp/ProcessDef.idr
View File

@ -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

3
src/TTImp/ProcessRecord.idr
View File

@ -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

285
src/TTImp/TTImp.idr
View File

@ -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

160
src/TTImp/TTImp/Functor.idr Normal file
View File

@ -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)

60
src/TTImp/Unelab.idr
View File

@ -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 []

2
tests/idris2/coverage004/expected
View File

@ -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 |

9
tests/idris2/docs001/expected
View File

@ -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!

3
tests/idris2/docs002/expected
View File

@ -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

2
tests/idris2/docs003/expected
View File

@ -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!

2
tests/idris2/interactive030/expected
View File

@ -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:

9
tests/idris2/perf005/expected
View File

@ -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.

6
tests/idris2/pretty001/expected
View File

@ -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!

2
tests/idris2/reflection002/expected
View File

@ -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