module Idris.AbsSyntaxTree where
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Typecheck
import Idris.Docstrings
import IRTS.Lang
import IRTS.CodegenCommon
import Util.Pretty
import Util.DynamicLinker
import Idris.Colours
import System.Console.Haskeline
import System.IO
import Control.Monad.Trans.State.Strict
import Control.Monad.Trans.Error
import Data.List hiding (group)
import Data.Char
import qualified Data.Map as M
import qualified Data.Text as T
import qualified Data.Map as M
import Data.Either
import qualified Data.Set as S
import Data.Word (Word)
import Data.Maybe (fromMaybe, mapMaybe)
import Data.Traversable (Traversable)
import Data.Foldable (Foldable)
import Debug.Trace
import Text.PrettyPrint.Annotated.Leijen
data ElabWhat = ETypes | EDefns | EAll
deriving (Show, Eq)
data ElabInfo = EInfo { params :: [(Name, PTerm)],
inblock :: Ctxt [Name],
liftname :: Name -> Name,
namespace :: Maybe [String],
rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->
Idris () }
toplevel :: ElabInfo
toplevel = EInfo [] emptyContext id Nothing (\_ _ _ -> fail "Not implemented")
eInfoNames :: ElabInfo -> [Name]
eInfoNames info = map fst (params info) ++ M.keys (inblock info)
data IOption = IOption { opt_logLevel :: Int,
opt_typecase :: Bool,
opt_typeintype :: Bool,
opt_coverage :: Bool,
opt_showimp :: Bool,
opt_errContext :: Bool,
opt_repl :: Bool,
opt_verbose :: Bool,
opt_nobanner :: Bool,
opt_quiet :: Bool,
opt_codegen :: Codegen,
opt_outputTy :: OutputType,
opt_ibcsubdir :: FilePath,
opt_importdirs :: [FilePath],
opt_triple :: String,
opt_cpu :: String,
opt_cmdline :: [Opt],
opt_origerr :: Bool,
opt_autoSolve :: Bool,
opt_autoImport :: [FilePath],
opt_optimise :: [Optimisation]
}
deriving (Show, Eq)
defaultOpts = IOption { opt_logLevel = 0
, opt_typecase = False
, opt_typeintype = False
, opt_coverage = True
, opt_showimp = False
, opt_errContext = False
, opt_repl = True
, opt_verbose = True
, opt_nobanner = False
, opt_quiet = False
, opt_codegen = Via "c"
, opt_outputTy = Executable
, opt_ibcsubdir = ""
, opt_importdirs = []
, opt_triple = ""
, opt_cpu = ""
, opt_cmdline = []
, opt_origerr = False
, opt_autoSolve = True
, opt_autoImport = []
, opt_optimise = defaultOptimise
}
data PPOption = PPOption {
ppopt_impl :: Bool
} deriving (Show)
data Optimisation = PETransform
deriving (Show, Eq)
defaultOptimise = [PETransform]
defaultPPOption :: PPOption
defaultPPOption = PPOption { ppopt_impl = False }
verbosePPOption :: PPOption
verbosePPOption = PPOption { ppopt_impl = True }
ppOption :: IOption -> PPOption
ppOption opt = PPOption {
ppopt_impl = opt_showimp opt
}
ppOptionIst :: IState -> PPOption
ppOptionIst = ppOption . idris_options
data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
data OutputMode = RawOutput Handle
| IdeSlave Integer Handle
deriving Show
data ConsoleWidth = InfinitelyWide
| ColsWide Int
| AutomaticWidth
data IState = IState {
tt_ctxt :: Context,
idris_constraints :: [(UConstraint, FC)],
idris_infixes :: [FixDecl],
idris_implicits :: Ctxt [PArg],
idris_statics :: Ctxt [Bool],
idris_classes :: Ctxt ClassInfo,
idris_dsls :: Ctxt DSL,
idris_optimisation :: Ctxt OptInfo,
idris_datatypes :: Ctxt TypeInfo,
idris_namehints :: Ctxt [Name],
idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]),
idris_flags :: Ctxt [FnOpt],
idris_callgraph :: Ctxt CGInfo,
idris_calledgraph :: Ctxt [Name],
idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
idris_tyinfodata :: Ctxt TIData,
idris_fninfo :: Ctxt FnInfo,
idris_transforms :: Ctxt [(Term, Term)],
idris_totcheck :: [(FC, Name)],
idris_defertotcheck :: [(FC, Name)],
idris_totcheckfail :: [(FC, String)],
idris_options :: IOption,
idris_name :: Int,
idris_lineapps :: [((FilePath, Int), PTerm)],
idris_metavars :: [(Name, (Maybe Name, Int, Bool))],
idris_coercions :: [Name],
idris_errRev :: [(Term, Term)],
syntax_rules :: [Syntax],
syntax_keywords :: [String],
imported :: [FilePath],
idris_scprims :: [(Name, (Int, PrimFn))],
idris_objs :: [(Codegen, FilePath)],
idris_libs :: [(Codegen, String)],
idris_cgflags :: [(Codegen, String)],
idris_hdrs :: [(Codegen, String)],
idris_imported :: [FilePath],
proof_list :: [(Name, [String])],
errSpan :: Maybe FC,
parserWarnings :: [(FC, Err)],
lastParse :: Maybe Name,
indent_stack :: [Int],
brace_stack :: [Maybe Int],
lastTokenSpan :: Maybe FC,
idris_parsedSpan :: Maybe FC,
hide_list :: [(Name, Maybe Accessibility)],
default_access :: Accessibility,
default_total :: Bool,
ibc_write :: [IBCWrite],
compiled_so :: Maybe String,
idris_dynamic_libs :: [DynamicLib],
idris_language_extensions :: [LanguageExt],
idris_outputmode :: OutputMode,
idris_colourRepl :: Bool,
idris_colourTheme :: ColourTheme,
idris_errorhandlers :: [Name],
idris_nameIdx :: (Int, Ctxt (Int, Name)),
idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)),
module_aliases :: M.Map [T.Text] [T.Text],
idris_consolewidth :: ConsoleWidth,
idris_postulates :: S.Set Name,
idris_whocalls :: Maybe (M.Map Name [Name]),
idris_callswho :: Maybe (M.Map Name [Name]),
idris_repl_defs :: [Name]
}
instance Show IState where
show = const "{internal state}"
data SizeChange = Smaller | Same | Bigger | Unknown
deriving (Show, Eq)
type SCGEntry = (Name, [Maybe (Int, SizeChange)])
type UsageReason = (Name, Int)
data CGInfo = CGInfo { argsdef :: [Name],
calls :: [(Name, [[Name]])],
scg :: [SCGEntry],
argsused :: [Name],
usedpos :: [(Int, [UsageReason])] }
deriving Show
primDefs = [sUN "unsafePerformPrimIO",
sUN "mkLazyForeignPrim",
sUN "mkForeignPrim",
sUN "void"]
data IBCWrite = IBCFix FixDecl
| IBCImp Name
| IBCStatic Name
| IBCClass Name
| IBCInstance Bool Name Name
| IBCDSL Name
| IBCData Name
| IBCOpt Name
| IBCMetavar Name
| IBCSyntax Syntax
| IBCKeyword String
| IBCImport FilePath
| IBCImportDir FilePath
| IBCObj Codegen FilePath
| IBCLib Codegen String
| IBCCGFlag Codegen String
| IBCDyLib String
| IBCHeader Codegen String
| IBCAccess Name Accessibility
| IBCMetaInformation Name MetaInformation
| IBCTotal Name Totality
| IBCFlags Name [FnOpt]
| IBCFnInfo Name FnInfo
| IBCTrans Name (Term, Term)
| IBCErrRev (Term, Term)
| IBCCG Name
| IBCDoc Name
| IBCCoercion Name
| IBCDef Name
| IBCNameHint (Name, Name)
| IBCLineApp FilePath Int PTerm
| IBCErrorHandler Name
| IBCFunctionErrorHandler Name Name Name
| IBCPostulate Name
| IBCTotCheckErr FC String
| IBCParsedRegion FC
deriving Show
idrisInit :: IState
idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
emptyContext emptyContext emptyContext emptyContext
emptyContext emptyContext emptyContext emptyContext
emptyContext emptyContext emptyContext emptyContext
[] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []
[] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
(RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
AutomaticWidth S.empty Nothing Nothing []
type Idris = StateT IState (ErrorT Err IO)
data Codegen = Via String
| Bytecode
deriving (Show, Eq)
data Command = Quit
| Help
| Eval PTerm
| NewDefn [PDecl]
| Undefine [Name]
| Check PTerm
| DocStr (Either Name Const)
| TotCheck Name
| Reload
| Load FilePath (Maybe Int)
| ChangeDirectory FilePath
| ModImport String
| Edit
| Compile Codegen String
| Execute
| ExecVal PTerm
| Metavars
| Prove Name
| AddProof (Maybe Name)
| RmProof Name
| ShowProof Name
| Proofs
| Universes
| LogLvl Int
| Spec PTerm
| HNF PTerm
| TestInline PTerm
| Defn Name
| Missing Name
| DynamicLink FilePath
| ListDynamic
| Pattelab PTerm
| DebugInfo Name
| Search PTerm
| CaseSplitAt Bool Int Name
| AddClauseFrom Bool Int Name
| AddProofClauseFrom Bool Int Name
| AddMissing Bool Int Name
| MakeWith Bool Int Name
| MakeLemma Bool Int Name
| DoProofSearch Bool Bool Int Name [Name]
| SetOpt Opt
| UnsetOpt Opt
| NOP
| SetColour ColourType IdrisColour
| ColourOn
| ColourOff
| ListErrorHandlers
| SetConsoleWidth ConsoleWidth
| Apropos String
| WhoCalls Name
| CallsWho Name
| MakeDoc String
| Warranty
| PrintDef Name
| PPrint OutputFmt Int PTerm
| TransformInfo Name
data OutputFmt = HTMLOutput | LaTeXOutput
data Opt = Filename String
| Quiet
| NoBanner
| ColourREPL Bool
| Ideslave
| IdeslaveSocket
| ShowLibs
| ShowLibdir
| ShowIncs
| NoBasePkgs
| NoPrelude
| NoBuiltins
| NoREPL
| OLogging Int
| Output String
| TypeCase
| TypeInType
| DefaultTotal
| DefaultPartial
| WarnPartial
| WarnReach
| NoCoverage
| ErrContext
| ShowImpl
| Verbose
| Port String
| IBCSubDir String
| ImportDir String
| PkgBuild String
| PkgInstall String
| PkgClean String
| PkgCheck String
| PkgREPL String
| PkgMkDoc String
| PkgTest String
| WarnOnly
| Pkg String
| BCAsm String
| DumpDefun String
| DumpCases String
| UseCodegen Codegen
| OutputTy OutputType
| Extension LanguageExt
| InterpretScript String
| EvalExpr String
| TargetTriple String
| TargetCPU String
| OptLevel Int
| AddOpt Optimisation
| RemoveOpt Optimisation
| Client String
| ShowOrigErr
| AutoWidth
| AutoSolve
deriving (Show, Eq)
data Fixity = Infixl { prec :: Int }
| Infixr { prec :: Int }
| InfixN { prec :: Int }
| PrefixN { prec :: Int }
deriving Eq
instance Show Fixity where
show (Infixl i) = "infixl " ++ show i
show (Infixr i) = "infixr " ++ show i
show (InfixN i) = "infix " ++ show i
show (PrefixN i) = "prefix " ++ show i
data FixDecl = Fix Fixity String
deriving Eq
instance Show FixDecl where
show (Fix f s) = show f ++ " " ++ s
instance Ord FixDecl where
compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
data Static = Static | Dynamic
deriving (Show, Eq)
data Plicity = Imp { pargopts :: [ArgOpt],
pstatic :: Static,
pparam :: Bool }
| Exp { pargopts :: [ArgOpt],
pstatic :: Static,
pparam :: Bool }
| Constraint { pargopts :: [ArgOpt],
pstatic :: Static }
| TacImp { pargopts :: [ArgOpt],
pstatic :: Static,
pscript :: PTerm }
deriving (Show, Eq)
impl = Imp [] Dynamic False
expl = Exp [] Dynamic False
expl_param = Exp [] Dynamic True
constraint = Constraint [] Static
tacimpl t = TacImp [] Dynamic t
data FnOpt = Inlinable
| TotalFn | PartialFn | CoveringFn
| Coinductive | AssertTotal
| Dictionary
| Implicit
| NoImplicit
| CExport String
| ErrorHandler
| ErrorReverse
| Reflection
| Specialise [(Name, Maybe Int)]
| Constructor
deriving (Show, Eq)
type FnOpts = [FnOpt]
inlinable :: FnOpts -> Bool
inlinable = elem Inlinable
dictionary :: FnOpts -> Bool
dictionary = elem Dictionary
data DataOpt = Codata
| DefaultEliminator
| DefaultCaseFun
| DataErrRev
deriving (Show, Eq)
type DataOpts = [DataOpt]
data ProvideWhat' t = ProvTerm t t
| ProvPostulate t
deriving (Show, Eq, Functor)
type ProvideWhat = ProvideWhat' PTerm
data PDecl' t
= PFix FC Fixity [String]
| PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t
| PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t
| PClauses FC FnOpts Name [PClause' t]
| PCAF FC Name t
| PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t)
| PParams FC [(Name, t)] [PDecl' t]
| PNamespace String [PDecl' t]
| PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t
| PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
[t]
Name
[(Name, t)]
[(Name, Docstring (Either Err PTerm))]
[PDecl' t]
| PInstance SyntaxInfo FC [t]
Name
[t]
t
(Maybe Name)
[PDecl' t]
| PDSL Name (DSL' t)
| PSyntax FC Syntax
| PMutual FC [PDecl' t]
| PDirective (Idris ())
| PProvider SyntaxInfo FC (ProvideWhat' t) Name
| PTransform FC Bool t t
deriving Functor
type ElabD a = Elab' [PDecl] a
data PClause' t = PClause FC Name t [t] t [PDecl' t]
| PWith FC Name t [t] t [PDecl' t]
| PClauseR FC [t] t [PDecl' t]
| PWithR FC [t] t [PDecl' t]
deriving Functor
data PData' t = PDatadecl { d_name :: Name,
d_tcon :: t,
d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])]
}
| PLaterdecl { d_name :: Name, d_tcon :: t }
deriving Functor
type PDecl = PDecl' PTerm
type PData = PData' PTerm
type PClause = PClause' PTerm
declared :: PDecl -> [Name]
declared (PFix _ _ _) = []
declared (PTy _ _ _ _ _ n t) = [n]
declared (PPostulate _ _ _ _ n t) = [n]
declared (PClauses _ _ n _) = []
declared (PCAF _ n _) = [n]
declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
where fstt (_, _, a, _, _, _) = a
declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
declared (PParams _ _ ds) = concatMap declared ds
declared (PNamespace _ ds) = concatMap declared ds
declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
declared (PInstance _ _ _ _ _ _ _ _) = []
declared (PDSL n _) = [n]
declared (PSyntax _ _) = []
declared (PMutual _ ds) = concatMap declared ds
declared (PDirective _) = []
tldeclared :: PDecl -> [Name]
tldeclared (PFix _ _ _) = []
tldeclared (PTy _ _ _ _ _ n t) = [n]
tldeclared (PPostulate _ _ _ _ n t) = [n]
tldeclared (PClauses _ _ n _) = []
tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
where fstt (_, _, a, _, _, _) = a
tldeclared (PParams _ _ ds) = []
tldeclared (PMutual _ ds) = concatMap tldeclared ds
tldeclared (PNamespace _ ds) = concatMap tldeclared ds
tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
tldeclared (PInstance _ _ _ _ _ _ _ _) = []
tldeclared _ = []
defined :: PDecl -> [Name]
defined (PFix _ _ _) = []
defined (PTy _ _ _ _ _ n t) = []
defined (PPostulate _ _ _ _ n t) = []
defined (PClauses _ _ n _) = [n]
defined (PCAF _ n _) = [n]
defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
where fstt (_, _, a, _, _, _) = a
defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
defined (PParams _ _ ds) = concatMap defined ds
defined (PNamespace _ ds) = concatMap defined ds
defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
defined (PInstance _ _ _ _ _ _ _ _) = []
defined (PDSL n _) = [n]
defined (PSyntax _ _) = []
defined (PMutual _ ds) = concatMap defined ds
defined (PDirective _) = []
updateN :: [(Name, Name)] -> Name -> Name
updateN ns n | Just n' <- lookup n ns = n'
updateN _ n = n
updateNs :: [(Name, Name)] -> PTerm -> PTerm
updateNs [] t = t
updateNs ns t = mapPT updateRef t
where updateRef (PRef fc f) = PRef fc (updateN ns f)
updateRef t = t
data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
data PTerm = PQuote Raw
| PRef FC Name
| PInferRef FC Name
| PPatvar FC Name
| PLam Name PTerm PTerm
| PPi Plicity Name PTerm PTerm
| PLet Name PTerm PTerm PTerm
| PTyped PTerm PTerm
| PApp FC PTerm [PArg]
| PAppBind FC PTerm [PArg]
| PMatchApp FC Name
| PCase FC PTerm [(PTerm, PTerm)]
| PTrue FC PunInfo
| PRefl FC PTerm
| PResolveTC FC
| PEq FC PTerm PTerm PTerm PTerm
| PRewrite FC PTerm PTerm (Maybe PTerm)
| PPair FC PunInfo PTerm PTerm
| PDPair FC PunInfo PTerm PTerm PTerm
| PAlternative Bool [PTerm]
| PHidden PTerm
| PType
| PUniverse Universe
| PGoal FC PTerm Name PTerm
| PConstant Const
| Placeholder
| PDoBlock [PDo]
| PIdiom FC PTerm
| PReturn FC
| PMetavar Name
| PProof [PTactic]
| PTactics [PTactic]
| PElabError Err
| PImpossible
| PCoerced PTerm
| PDisamb [[T.Text]] PTerm
| PUnifyLog PTerm
| PNoImplicits PTerm
| PQuasiquote PTerm (Maybe PTerm)
| PUnquote PTerm
deriving Eq
mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
mapPT f t = f (mpt t) where
mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
(fmap (mapPT f) g)
mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
mpt (PHidden t) = PHidden (mapPT f t)
mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
mpt x = x
data PTactic' t = Intro [Name] | Intros | Focus Name
| Refine Name [Bool] | Rewrite t | DoUnify
| Induction t
| CaseTac t
| Equiv t
| MatchRefine Name
| LetTac Name t | LetTacTy Name t t
| Exact t | Compute | Trivial | TCInstance
| ProofSearch Bool Bool Int (Maybe Name) [Name]
| Solve
| Attack
| ProofState | ProofTerm | Undo
| Try (PTactic' t) (PTactic' t)
| TSeq (PTactic' t) (PTactic' t)
| ApplyTactic t
| ByReflection t
| Reflect t
| Fill t
| GoalType String (PTactic' t)
| TCheck t
| TEval t
| TDocStr (Either Name Const)
| TSearch t
| Skip
| TFail [ErrorReportPart]
| Qed | Abandon
deriving (Show, Eq, Functor, Foldable, Traversable)
instance Sized a => Sized (PTactic' a) where
size (Intro nms) = 1 + size nms
size Intros = 1
size (Focus nm) = 1 + size nm
size (Refine nm bs) = 1 + size nm + length bs
size (Rewrite t) = 1 + size t
size (Induction t) = 1 + size t
size (LetTac nm t) = 1 + size nm + size t
size (Exact t) = 1 + size t
size Compute = 1
size Trivial = 1
size Solve = 1
size Attack = 1
size ProofState = 1
size ProofTerm = 1
size Undo = 1
size (Try l r) = 1 + size l + size r
size (TSeq l r) = 1 + size l + size r
size (ApplyTactic t) = 1 + size t
size (Reflect t) = 1 + size t
size (Fill t) = 1 + size t
size Qed = 1
size Abandon = 1
size Skip = 1
size (TFail ts) = 1 + size ts
type PTactic = PTactic' PTerm
data PDo' t = DoExp FC t
| DoBind FC Name t
| DoBindP FC t t [(t,t)]
| DoLet FC Name t t
| DoLetP FC t t
deriving (Eq, Functor)
instance Sized a => Sized (PDo' a) where
size (DoExp fc t) = 1 + size fc + size t
size (DoBind fc nm t) = 1 + size fc + size nm + size t
size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
size (DoLetP fc l r) = 1 + size fc + size l + size r
type PDo = PDo' PTerm
data PArg' t = PImp { priority :: Int,
machine_inf :: Bool,
argopts :: [ArgOpt],
pname :: Name, getTm :: t }
| PExp { priority :: Int,
argopts :: [ArgOpt],
pname :: Name,
getTm :: t }
| PConstraint { priority :: Int,
argopts :: [ArgOpt],
pname :: Name,
getTm :: t }
| PTacImplicit { priority :: Int,
argopts :: [ArgOpt],
pname :: Name,
getScript :: t,
getTm :: t }
deriving (Show, Eq, Functor)
data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
deriving (Show, Eq)
instance Sized a => Sized (PArg' a) where
size (PImp p _ l nm trm) = 1 + size nm + size trm
size (PExp p l nm trm) = 1 + size nm + size trm
size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
pimp n t mach = PImp 1 mach [] n t
pexp t = PExp 1 [] (sMN 0 "arg") t
pconst t = PConstraint 1 [] (sMN 0 "carg") t
ptacimp n s t = PTacImplicit 2 [] n s t
type PArg = PArg' PTerm
data ClassInfo = CI { instanceName :: Name,
class_methods :: [(Name, (FnOpts, PTerm))],
class_defaults :: [(Name, (Name, PDecl))],
class_default_superclasses :: [PDecl],
class_params :: [Name],
class_instances :: [Name] }
deriving Show
data TIData = TIPartial
| TISolution [Term]
deriving Show
data FnInfo = FnInfo { fn_params :: [Int] }
deriving Show
data OptInfo = Optimise { inaccessible :: [(Int,Name)],
detaggable :: Bool }
deriving Show
data TypeInfo = TI { con_names :: [Name],
codata :: Bool,
data_opts :: DataOpts,
param_pos :: [Int],
mutual_types :: [Name] }
deriving Show
data DSL' t = DSL { dsl_bind :: t,
dsl_return :: t,
dsl_apply :: t,
dsl_pure :: t,
dsl_var :: Maybe t,
index_first :: Maybe t,
index_next :: Maybe t,
dsl_lambda :: Maybe t,
dsl_let :: Maybe t,
dsl_pi :: Maybe t
}
deriving (Show, Functor)
type DSL = DSL' PTerm
data SynContext = PatternSyntax | TermSyntax | AnySyntax
deriving Show
data Syntax = Rule [SSymbol] PTerm SynContext
deriving Show
syntaxNames :: Syntax -> [Name]
syntaxNames (Rule syms _ _) = mapMaybe ename syms
where ename (Keyword n) = Just n
ename _ = Nothing
data SSymbol = Keyword Name
| Symbol String
| Binding Name
| Expr Name
| SimpleExpr Name
deriving Show
initDSL = DSL (PRef f (sUN ">>="))
(PRef f (sUN "return"))
(PRef f (sUN "<$>"))
(PRef f (sUN "pure"))
Nothing
Nothing
Nothing
Nothing
Nothing
Nothing
where f = fileFC "(builtin)"
data Using = UImplicit Name PTerm
| UConstraint Name [Name]
deriving (Show, Eq)
data SyntaxInfo = Syn { using :: [Using],
syn_params :: [(Name, PTerm)],
syn_namespace :: [String],
no_imp :: [Name],
decoration :: Name -> Name,
inPattern :: Bool,
implicitAllowed :: Bool,
maxline :: Maybe Int,
mut_nesting :: Int,
dsl_info :: DSL,
syn_in_quasiquote :: Int }
deriving Show
defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
expandNS :: SyntaxInfo -> Name -> Name
expandNS syn n@(NS _ _) = n
expandNS syn n = case syn_namespace syn of
[] -> n
xs -> sNS n xs
bi = fileFC "builtin"
inferTy = sMN 0 "__Infer"
inferCon = sMN 0 "__infer"
inferDecl = PDatadecl inferTy
PType
[(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
(PRef bi inferTy)), bi, [])]
inferOpts = []
infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
infP = P (TCon 6 0) inferTy (TType (UVal 0))
getInferTerm, getInferType :: Term -> Term
getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
getInferTerm (App (App _ _) tm) = tm
getInferTerm tm = tm
getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
where toTy (Lam t) = Pi t (TType (UVar 0))
toTy (PVar t) = PVTy t
toTy b = b
getInferType (App (App _ ty) _) = ty
primNames = [eqTy, eqCon, inferTy, inferCon]
unitTy = sUN "Unit"
unitCon = sUN "MkUnit"
falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
"The empty type, also known as the trivially false proposition." ++
"\n\n" ++
"Use `void` or `absurd` to prove anything if you have a variable " ++
"of type `Void` in scope."
falseTy = sUN "Void"
pairTy = sUN "Pair"
pairCon = sUN "MkPair"
eqTy = sUN "="
eqCon = sUN "Refl"
eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
"The propositional equality type. A proof that `x` = `y`." ++
"\n\n" ++
"To use such a proof, pattern-match on it, and the two equal things will " ++
"then need to be the _same_ pattern." ++
"\n\n" ++
"**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
"is possible to state equalities between values of potentially different " ++
"types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
"\n\n" ++
"You may need to use `(~=~)` to explicitly request heterogeneous equality."
eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
(piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
PType))
[(reflDoc, reflParamDoc,
eqCon, PPi impl (n "A") PType (
PPi impl (n "x") (PRef bi (n "A"))
(PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
pimp (n "B") Placeholder False,
pexp (PRef bi (n "x")),
pexp (PRef bi (n "x"))])), bi, [])]
where n a = sUN a
reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
"A proof that `x` in fact equals `x`. To construct this, you must have already " ++
"shown that both sides are in fact equal."
reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
(n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
(n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
]
where n a = sUN a
eqOpts = []
sigmaTy = sUN "Sigma"
existsCon = sUN "MkSigma"
piBind :: [(Name, PTerm)] -> PTerm -> PTerm
piBind = piBindp expl
piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
piBindp p [] t = t
piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
instance Show PTerm where
showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
instance Show PDecl where
showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
instance Show PClause where
showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
instance Show PData where
showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
instance Pretty PTerm OutputAnnotation where
pretty = prettyImp defaultPPOption
consoleDecorate :: IState -> OutputAnnotation -> String -> String
consoleDecorate ist _ | not (idris_colourRepl ist) = id
consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
in if constIsType c
then colouriseType theme
else colouriseData theme
consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
theme = idris_colourTheme ist
in case () of
_ | isDConName n ctxt -> colouriseData theme
_ | isFnName n ctxt -> colouriseFun theme
_ | isTConName n ctxt -> colouriseType theme
_ | isPostulateName n ist -> colourisePostulate theme
_ | otherwise -> id
consoleDecorate ist (AnnFC _) = id
consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
where colour BoldText = IdrisColour Nothing True False True False
colour UnderlineText = IdrisColour Nothing True True False False
colour ItalicText = IdrisColour Nothing True False False True
consoleDecorate ist (AnnTerm _ _) = id
consoleDecorate ist (AnnSearchResult _) = id
consoleDecorate ist (AnnErr _) = id
isPostulateName :: Name -> IState -> Bool
isPostulateName n ist = S.member n (idris_postulates ist)
prettyImp :: PPOption
-> PTerm
-> Doc OutputAnnotation
prettyImp impl = pprintPTerm impl [] [] []
prettyIst :: IState -> PTerm -> Doc OutputAnnotation
prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
pprintPTerm :: PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
where
prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
prettySe p bnd (PQuote r) =
text "![" <> pretty r <> text "]"
prettySe p bnd (PPatvar fc n) = pretty n
prettySe p bnd e
| Just str <- slist p bnd e = str
| Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
prettySe p bnd (PLam n ty sc) =
bracket p 2 . group . align . hang 2 $
text "\\" <> bindingOf n False <+> text "=>" <$>
prettySe 10 ((n, False):bnd) sc
prettySe p bnd (PLet n ty v sc) =
bracket p 2 . group . align $
kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
prettySe p bnd (PPi (Exp l s _) n ty sc)
| n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
bracket p 2 . group $
enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
| otherwise =
bracket p 2 . group $
group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
where
st =
case s of
Static -> text "[static]" <> space
_ -> empty
prettySe p bnd (PPi (Imp l s _) n ty sc)
| ppopt_impl ppo =
bracket p 2 $
lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
st <> text "->" </> prettySe 10 ((n, True):bnd) sc
| otherwise = prettySe 10 ((n, True):bnd) sc
where
st =
case s of
Static -> text "[static]" <> space
_ -> empty
prettySe p bnd (PPi (Constraint _ _) n ty sc) =
bracket p 2 $
prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
bracket p 2 $
lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
prettySe p bnd (PApp _ (PRef _ f) args)
| UN nm <- basename f
, not (ppopt_impl ppo) && null (getShowArgs args) =
prettyName True (ppopt_impl ppo) bnd f
prettySe p bnd (PAppBind _ (PRef _ f) [])
| not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
prettySe p bnd (PApp _ (PRef _ op) args)
| UN nm <- basename op
, not (tnull nm) &&
(not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
case getShowArgs args of
[] -> opName True
[x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
[l,r] -> let precedence = fromMaybe 20 (fmap prec f)
in bracket p precedence $ inFix (getTm l) (getTm r)
(l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
bracket p 1 $
enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
align (group (vsep (map (prettyArgS bnd) rest)))
as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
f = getFixity (opStr op)
left l = case f of
Nothing -> prettySe (1) bnd l
Just (Infixl p') -> prettySe p' bnd l
Just f' -> prettySe (prec f'1) bnd l
right r = case f of
Nothing -> prettySe (1) bnd r
Just (Infixr p') -> prettySe p' bnd r
Just f' -> prettySe (prec f'1) bnd r
inFix l r = align . group $
(left l <+> opName False) <$> group (right r)
prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
| PConstant (Idris.Core.TT.Str str) <- getTm tm,
f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
prettySe p bnd (PApp _ f as) =
let args = getShowArgs as
fp = prettySe 1 bnd f
in
bracket p 1 . group $
if ppopt_impl ppo
then if null as
then fp
else fp <+> align (vsep (map (prettyArgS bnd) as))
else if null args
then fp
else fp <+> align (vsep (map (prettyArgS bnd) args))
prettySe p bnd (PCase _ scr opts) =
kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
where
prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
prettySe p bnd (PResolveTC _) = text "resolvetc"
prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
prettySe p bnd (PEq _ lt rt l r)
| ppopt_impl ppo =
bracket p 1 $
enclose lparen rparen eq <+>
align (group (vsep (map (prettyArgS bnd)
[PImp 0 False [] (sUN "A") lt,
PImp 0 False [] (sUN "B") rt,
PExp 0 [] (sUN "x") l,
PExp 0 [] (sUN "y") r])))
| otherwise =
bracket p 2 . align . group $
prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
where eq = annName eqTy (text "=")
prettySe p bnd (PRewrite _ l r _) =
bracket p 2 $
text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
prettySe p bnd (PTyped l r) =
lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
prettySe p bnd pair@(PPair _ pun _ _)
| Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
align . group . vsep . punctuate (ann comma) $
map (prettySe 10 bnd) elts
where ann = case pun of
TypeOrTerm -> id
IsType -> annName pairTy
IsTerm -> annName pairCon
prettySe p bnd (PDPair _ TypeOrTerm l t r) =
lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
annName sigmaTy lparen <>
bindingOf n False <+>
annName sigmaTy (text "**") <+>
prettySe 10 ((n, False):bnd) r <>
annName sigmaTy rparen
prettySe p bnd (PDPair _ IsType l t r) =
annName sigmaTy lparen <>
prettySe 10 bnd l <+>
annName sigmaTy (text "**") <+>
prettySe 10 bnd r <>
annName sigmaTy rparen
prettySe p bnd (PDPair _ IsTerm l t r) =
annName existsCon lparen <>
prettySe 10 bnd l <+>
annName existsCon (text "**") <+>
prettySe 10 bnd r <>
annName existsCon rparen
prettySe p bnd (PAlternative a as) =
lparen <> text "|" <> prettyAs <> text "|" <> rparen
where
prettyAs =
foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
prettySe p bnd (PProof ts) =
text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
prettySe p bnd (PTactics ts) =
text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
prettySe p bnd (PMetavar n) = text "?" <> pretty n
prettySe p bnd (PReturn f) = kwd "return"
prettySe p bnd PImpossible = kwd "impossible"
prettySe p bnd Placeholder = text "_"
prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
prettySe p bnd (PCoerced t) = prettySe p bnd t
prettySe p bnd (PElabError s) = pretty s
prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
prettySe p bnd _ = text "missing pretty-printer for term"
prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
prettyArgSe bnd arg = prettySe 0 bnd arg
prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
annName n = annotate (AnnName n Nothing Nothing Nothing)
opStr :: Name -> String
opStr (NS n _) = opStr n
opStr (UN n) = T.unpack n
basename :: Name -> Name
basename (NS n _) = basename n
basename n = n
slist' p bnd (PApp _ (PRef _ nil) _)
| not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
slist' p bnd (PRef _ nil)
| not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
slist' p bnd (PApp _ (PRef _ cons) args)
| nsroot cons == sUN "::",
(PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
all isImp imps,
Just tl' <- slist' p bnd tl
= Just (hd:tl')
where
isImp (PImp {}) = True
isImp _ = False
slist' _ _ tm = Nothing
slist p bnd e | Just es <- slist' p bnd e = Just $
case es of [] -> annotate (AnnData "" "") $ text "[]"
[x] -> enclose left right . group $
prettySe p bnd x
xs -> (enclose left right .
align . group . vsep .
punctuate comma .
map (prettySe p bnd)) xs
where left = (annotate (AnnData "" "") (text "["))
right = (annotate (AnnData "" "") (text "]"))
comma = (annotate (AnnData "" "") (text ","))
slist _ _ _ = Nothing
pairElts :: PTerm -> Maybe [PTerm]
pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
| otherwise = Just [x, y]
pairElts _ = Nothing
natns = "Prelude.Nat."
snat p (PRef _ z)
| show z == (natns++"Z") || show z == "Z" = Just 0
snat p (PApp _ s [PExp {getTm=n}])
| show s == (natns++"S") || show s == "S",
Just n' <- snat p n
= Just $ 1 + n'
snat _ _ = Nothing
bracket outer inner doc
| inner > outer = lparen <> doc <> rparen
| otherwise = doc
kwd = annotate AnnKeyword . text
fixities :: M.Map String Fixity
fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
getFixity :: String -> Maybe Fixity
getFixity = flip M.lookup fixities
bindingOf :: Name
-> Bool
-> Doc OutputAnnotation
bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
prettyName
:: Bool
-> Bool
-> [(Name, Bool)]
-> Name
-> Doc OutputAnnotation
prettyName infixParen showNS bnd n
| Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
| otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
where fullName = text nameSpace <> parenthesise (text (baseName n))
baseName (UN n) = T.unpack n
baseName (NS n ns) = baseName n
baseName (MN i s) = T.unpack s
baseName other = show other
nameSpace = case n of
(NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
_ -> ""
isInfix = case baseName n of
"" -> False
(c : _) -> not (isAlpha c)
parenthesise = if isInfix && infixParen then enclose lparen rparen else id
showCImp :: PPOption -> PClause -> Doc OutputAnnotation
showCImp ppo (PClause _ n l ws r w)
= prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
<+> text "where" <+> text (show w)
where
showWs [] = empty
showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
showCImp ppo (PWith _ n l ws r w)
= prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
<+> braces (text (show w))
where
showWs [] = empty
showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
showDImp :: PPOption -> PData -> Doc OutputAnnotation
showDImp ppo (PDatadecl n ty cons)
= text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
(indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
showDecls o ds = vsep (map (showDeclImp o) ds)
showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
indent 2 (vsep (map (showCImp o) cs))
showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
showDeclImp o (PClass _ _ _ cs n ps _ ds)
= text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
showDeclImp o (PInstance _ _ cs n _ t _ ds)
= text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
showDeclImp _ _ = text "..."
instance Show (Doc OutputAnnotation) where
show = flip (displayS . renderCompact) ""
getImps :: [PArg] -> [(Name, PTerm)]
getImps [] = []
getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
getImps (_ : xs) = getImps xs
getExps :: [PArg] -> [PTerm]
getExps [] = []
getExps (PExp _ _ _ tm : xs) = tm : getExps xs
getExps (_ : xs) = getExps xs
getShowArgs :: [PArg] -> [PArg]
getShowArgs [] = []
getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
getShowArgs (_ : xs) = getShowArgs xs
getConsts :: [PArg] -> [PTerm]
getConsts [] = []
getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
getConsts (_ : xs) = getConsts xs
getAll :: [PArg] -> [PTerm]
getAll = map getTm
showName :: Maybe IState
-> [(Name, Bool)]
-> PPOption
-> Bool
-> Name
-> String
showName ist bnd ppo colour n = case ist of
Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
Nothing -> showbasic n
where name = if ppopt_impl ppo then show n else showbasic n
showbasic n@(UN _) = showCG n
showbasic (MN i s) = str s
showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
showbasic (SN s) = show s
fst3 (x, _, _) = x
colourise n t = let ctxt' = fmap tt_ctxt ist in
case ctxt' of
Nothing -> name
Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
else colouriseBound t name
| isDConName n ctxt -> colouriseData t name
| isFnName n ctxt -> colouriseFun t name
| isTConName n ctxt -> colouriseType t name
| otherwise -> colouriseImplicit t name
showTm :: IState
-> PTerm
-> String
showTm ist = displayDecorated (consoleDecorate ist) .
renderPretty 0.8 100000 .
prettyImp (ppOptionIst ist)
showTmImpls :: PTerm -> String
showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
instance Sized PTerm where
size (PQuote rawTerm) = size rawTerm
size (PRef fc name) = size name
size (PLam name ty bdy) = 1 + size ty + size bdy
size (PPi plicity name ty bdy) = 1 + size ty + size bdy
size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
size (PTyped trm ty) = 1 + size trm + size ty
size (PApp fc name args) = 1 + size args
size (PAppBind fc name args) = 1 + size args
size (PCase fc trm bdy) = 1 + size trm + size bdy
size (PTrue fc _) = 1
size (PRefl fc _) = 1
size (PResolveTC fc) = 1
size (PEq fc _ _ left right) = 1 + size left + size right
size (PRewrite fc left right _) = 1 + size left + size right
size (PPair fc _ left right) = 1 + size left + size right
size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
size (PAlternative a alts) = 1 + size alts
size (PHidden hidden) = size hidden
size (PUnifyLog tm) = size tm
size (PDisamb _ tm) = size tm
size (PNoImplicits tm) = size tm
size PType = 1
size (PUniverse _) = 1
size (PConstant const) = 1 + size const
size Placeholder = 1
size (PDoBlock dos) = 1 + size dos
size (PIdiom fc term) = 1 + size term
size (PReturn fc) = 1
size (PMetavar name) = 1
size (PProof tactics) = size tactics
size (PElabError err) = size err
size PImpossible = 1
size _ = 0
getPArity :: PTerm -> Int
getPArity (PPi _ _ _ sc) = 1 + getPArity sc
getPArity _ = 0
allNamesIn :: PTerm -> [Name]
allNamesIn tm = nub $ ni [] tm
where
ni env (PRef _ n)
| not (n `elem` env) = [n]
ni env (PPatvar _ n) = [n]
ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
ni env (PHidden tm) = ni env tm
ni env (PEq _ _ _ l r) = ni env l ++ ni env r
ni env (PRewrite _ l r _) = ni env l ++ ni env r
ni env (PTyped l r) = ni env l ++ ni env r
ni env (PPair _ _ l r) = ni env l ++ ni env r
ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
ni env (PAlternative a ls) = concatMap (ni env) ls
ni env (PUnifyLog tm) = ni env tm
ni env (PDisamb _ tm) = ni env tm
ni env (PNoImplicits tm) = ni env tm
ni env _ = []
niTacImp env (TacImp _ _ scr) = ni env scr
niTacImp _ _ = []
boundNamesIn :: PTerm -> [Name]
boundNamesIn tm = nub $ ni tm
where
ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
ni (PLam n ty sc) = n : (ni ty ++ ni sc)
ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
ni (PEq _ _ _ l r) = ni l ++ ni r
ni (PRewrite _ l r _) = ni l ++ ni r
ni (PTyped l r) = ni l ++ ni r
ni (PPair _ _ l r) = ni l ++ ni r
ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
ni (PAlternative a as) = concatMap (ni) as
ni (PHidden tm) = ni tm
ni (PUnifyLog tm) = ni tm
ni (PDisamb _ tm) = ni tm
ni (PNoImplicits tm) = ni tm
ni _ = []
niTacImp (TacImp _ _ scr) = ni scr
niTacImp _ = []
implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
implicitNamesIn uvars ist tm = nub $ ni [] tm
where
ni env (PRef _ n)
| not (n `elem` env)
= case lookupTy n (tt_ctxt ist) of
[] -> [n]
_ -> if n `elem` uvars then [n] else []
ni env (PApp _ f@(PRef _ n) as)
| n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
| otherwise = concatMap (ni env) (map getTm as)
ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
ni env (PCase _ c os) = ni env c ++
(nub (concatMap (ni env) (map snd os))
\\ nub (concatMap (ni env) (map fst os)))
ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
ni env (PEq _ _ _ l r) = ni env l ++ ni env r
ni env (PRewrite _ l r _) = ni env l ++ ni env r
ni env (PTyped l r) = ni env l ++ ni env r
ni env (PPair _ _ l r) = ni env l ++ ni env r
ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
ni env (PAlternative a as) = concatMap (ni env) as
ni env (PHidden tm) = ni env tm
ni env (PUnifyLog tm) = ni env tm
ni env (PDisamb _ tm) = ni env tm
ni env (PNoImplicits tm) = ni env tm
ni env _ = []
namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
namesIn uvars ist tm = nub $ ni [] tm
where
ni env (PRef _ n)
| not (n `elem` env)
= case lookupTy n (tt_ctxt ist) of
[] -> [n]
_ -> if n `elem` (map fst uvars) then [n] else []
ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
ni env (PCase _ c os) = ni env c ++
(nub (concatMap (ni env) (map snd os))
\\ nub (concatMap (ni env) (map fst os)))
ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
ni env (PEq _ _ _ l r) = ni env l ++ ni env r
ni env (PRewrite _ l r _) = ni env l ++ ni env r
ni env (PTyped l r) = ni env l ++ ni env r
ni env (PPair _ _ l r) = ni env l ++ ni env r
ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
ni env (PAlternative a as) = concatMap (ni env) as
ni env (PHidden tm) = ni env tm
ni env (PUnifyLog tm) = ni env tm
ni env (PDisamb _ tm) = ni env tm
ni env (PNoImplicits tm) = ni env tm
ni env _ = []
niTacImp env (TacImp _ _ scr) = ni env scr
niTacImp _ _ = []
usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
usedNamesIn vars ist tm = nub $ ni [] tm
where
ni env (PRef _ n)
| n `elem` vars && not (n `elem` env)
= case lookupDefExact n (tt_ctxt ist) of
Nothing -> [n]
_ -> []
ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
ni env (PEq _ _ _ l r) = ni env l ++ ni env r
ni env (PRewrite _ l r _) = ni env l ++ ni env r
ni env (PTyped l r) = ni env l ++ ni env r
ni env (PPair _ _ l r) = ni env l ++ ni env r
ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
ni env (PAlternative a as) = concatMap (ni env) as
ni env (PHidden tm) = ni env tm
ni env (PUnifyLog tm) = ni env tm
ni env (PDisamb _ tm) = ni env tm
ni env (PNoImplicits tm) = ni env tm
ni env _ = []
niTacImp env (TacImp _ _ scr) = ni env scr
niTacImp _ _ = []
getErasureInfo :: IState -> Name -> [Int]
getErasureInfo ist n =
case lookupCtxtExact n (idris_optimisation ist) of
Just (Optimise inacc detagg) -> map fst inacc
Nothing -> []