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

Merge github.com:idris-lang/Idris2

Browse Source
This commit is contained in:
Edwin Brady 2020-07-26 17:39:00 +01:00
commit c860e5e690
24 changed files with 1223 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/base/Data/Either.idr
View File

@ -65,9 +65,11 @@ eitherToMaybe (Right x) = Just x
-- Injectivity of constructors
||| Left is injective
export
leftInjective : Left x = Left y -> x = y
leftInjective Refl = Refl
||| Right is injective
export
rightInjective : Right x = Right y -> x = y
rightInjective Refl = Refl

22
libs/base/Decidable/Equality.idr
View File

@ -1,6 +1,7 @@
module Decidable.Equality
import Data.Maybe
import Data.Either
import Data.Nat
import Data.List
@ -78,6 +79,27 @@ DecEq t => DecEq (Maybe t) where
decEq (Just x') (Just y') | No p
= No $ \h : Just x' = Just y' => p $ justInjective h
--------------------------------------------------------------------------------
-- Either
--------------------------------------------------------------------------------
Uninhabited (Left x = Right y) where
uninhabited Refl impossible
Uninhabited (Right x = Left y) where
uninhabited Refl impossible
export
(DecEq t, DecEq s) => DecEq (Either t s) where
decEq (Left x) (Left y) with (decEq x y)
decEq (Left x) (Left x) | Yes Refl = Yes Refl
decEq (Left x) (Left y) | No contra = No (contra . leftInjective)
decEq (Left x) (Right y) = No absurd
decEq (Right x) (Left y) = No absurd
decEq (Right x) (Right y) with (decEq x y)
decEq (Right x) (Right x) | Yes Refl = Yes Refl
decEq (Right x) (Right y) | No contra = No (contra . rightInjective)
--------------------------------------------------------------------------------
-- Tuple
--------------------------------------------------------------------------------

12
libs/contrib/Text/PrettyPrint/Prettyprinter.idr Normal file
View File

@ -0,0 +1,12 @@
||| A Idris port of the prettyprinter library [1] and
||| the ANSI terminal backend [2].
|||
||| [1] https://hackage.haskell.org/package/prettyprinter
||| [2] https://hackage.haskell.org/package/prettyprinter-ansi-terminal
module Text.PrettyPrint.Prettyprinter
import public Text.PrettyPrint.Prettyprinter.Doc
import public Text.PrettyPrint.Prettyprinter.Symbols
%default total

746
libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr Normal file
View File

@ -0,0 +1,746 @@
module Text.PrettyPrint.Prettyprinter.Doc
import Data.List
import Data.Maybe
import Data.Strings
import Data.String.Extra
%default total
export
textSpaces : Int -> String
textSpaces n = replicate (integerToNat $ cast n) ' '
||| Maximum number of characters that fit in one line.
public export
data PageWidth : Type where
||| The `Int` is the number of characters, including whitespace, that fit in a line.
||| The `Double` is the ribbon, the fraction of the toal page width that can be printed on.
AvailablePerLine : Int -> Double -> PageWidth
||| The layouters should not introduce line breaks.
Unbounded : PageWidth
data FlattenResult : Type -> Type where
Flattened : a -> FlattenResult a
AlreadyFlat : FlattenResult a
NeverFlat : FlattenResult a
Functor FlattenResult where
map f (Flattened a) = Flattened (f a)
map _ AlreadyFlat = AlreadyFlat
map _ NeverFlat = NeverFlat
||| Fusion depth parameter.
public export
data FusionDepth : Type where
||| Do not dive deep into nested documents.
Shallow : FusionDepth
||| Recurse into all parts of the `Doc`. May impact performace.
Deep : FusionDepth
||| This data type represents pretty documents that have
||| been annotated with an arbitrary data type `ann`.
public export
data Doc : Type -> Type where
Empty : Doc ann
Chara : (c : Char) -> Doc ann -- Invariant: not '\n'
Text : (len : Int) -> (text : String) -> Doc ann -- Invariant: at least two characters long and no '\n'
Line : Doc ann
FlatAlt : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
Cat : Doc ann -> Doc ann -> Doc ann
Nest : (i : Int) -> Doc ann -> Doc ann
Union : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann -- Invariant: the first line of the first document should be
-- longer than the first lines of the second one
Column : (Int -> Doc ann) -> Doc ann
WithPageWidth : (PageWidth -> Doc ann) -> Doc ann
Nesting : (Int -> Doc ann) -> Doc ann
Annotated : ann -> Doc ann -> Doc ann
export
Semigroup (Doc ann) where
(<+>) = Cat
export
Monoid (Doc ann) where
neutral = Empty
||| Layout a document depending on which column it starts at.
export
column : (Int -> Doc ann) -> Doc ann
column = Column
||| Lays out a document with the current nesting level increased by `i`.
export
nest : Int -> Doc ann -> Doc ann
nest 0 x = x
nest i x = Nest i x
||| Layout a document depending on the current nesting level.
export
nesting : (Int -> Doc ann) -> Doc ann
nesting = Nesting
||| Lays out a document, and makes the column width of it available to a function.
export
width : Doc ann -> (Int -> Doc ann) -> Doc ann
width doc f = column (\colStart => doc <+> column (\colEnd => f (colEnd - colStart)))
||| Layout a document depending on the page width, if one has been specified.
export
pageWidth : (PageWidth -> Doc ann) -> Doc ann
pageWidth = WithPageWidth
||| Lays out a document with the nesting level set to the current column.
export
align : Doc ann -> Doc ann
align d = column (\k => nesting (\i => nest (k - i) d))
||| Lays out a document with a nesting level set to the current column plus `i`.
||| Negative values are allowed, and decrease the nesting level accordingly.
export
hang : Int -> Doc ann -> Doc ann
hang i d = align (nest i d)
||| Insert a number of spaces.
export
spaces : Int -> Doc ann
spaces n = if n <= 0
then Empty
else if n == 1
then Chara ' '
else Text n (textSpaces n)
||| Indents a document with `i` spaces, starting from the current cursor position.
export
indent : Int -> Doc ann -> Doc ann
indent i d = hang i (spaces i <+> d)
||| Lays out a document. It then appends spaces until the width is equal to `i`.
||| If the width is already larger, nothing is appended.
export
fill : Int -> Doc ann -> Doc ann
fill n doc = width doc (\w => spaces $ n - w)
infixr 6 <++>
||| Concatenates two documents with a space in between.
export
(<++>) : Doc ann -> Doc ann -> Doc ann
x <++> y = x <+> Chara ' ' <+> y
||| The empty document behaves like `pretty ""`, so it has a height of 1.
export
emptyDoc : Doc ann
emptyDoc = Empty
||| Behaves like `space` if the resulting output fits the page, otherwise like `line`.
export
softline : Doc ann
softline = Union (Chara ' ') Line
||| Like `softline`, but behaves like `neutral` if the resulting output does not fit
||| on the page.
export
softline' : Doc ann
softline' = Union neutral Line
||| A line break, even when grouped.
export
hardline : Doc ann
hardline = Line
flatten : Doc ann -> Doc ann
flatten Empty = Empty
flatten (Chara x) = Chara x
flatten (Text len x) = Text len x
flatten Line = Empty
flatten (FlatAlt _ y) = flatten y
flatten (Cat x y) = Cat (flatten x) (flatten y)
flatten (Nest i x) = Nest i (flatten x)
flatten (Union x _) = flatten x
flatten (Column f) = Column (\x => flatten $ f x)
flatten (WithPageWidth f) = WithPageWidth (\x => flatten $ f x)
flatten (Nesting f) = Nesting (\x => flatten $ f x)
flatten (Annotated ann x) = Annotated ann (flatten x)
changesUponFlattening : Doc ann -> FlattenResult (Doc ann)
changesUponFlattening Empty = AlreadyFlat
changesUponFlattening (Chara x) = AlreadyFlat
changesUponFlattening (Text x y) = AlreadyFlat
changesUponFlattening Line = NeverFlat
changesUponFlattening (FlatAlt _ y) = Flattened (flatten y)
changesUponFlattening (Cat x y) = case (changesUponFlattening x, changesUponFlattening y) of
(NeverFlat, _) => NeverFlat
(_, NeverFlat) => NeverFlat
(Flattened x', Flattened y') => Flattened (Cat x' y')
(Flattened x', AlreadyFlat) => Flattened (Cat x' y)
(AlreadyFlat , Flattened y') => Flattened (Cat x y')
(AlreadyFlat , AlreadyFlat) => AlreadyFlat
changesUponFlattening (Nest i x) = map (Nest i) (changesUponFlattening x)
changesUponFlattening (Union x _) = Flattened x
changesUponFlattening (Column f) = Flattened (Column (flatten . f))
changesUponFlattening (WithPageWidth f) = Flattened (WithPageWidth (flatten . f))
changesUponFlattening (Nesting f) = Flattened (Nesting (flatten . f))
changesUponFlattening (Annotated ann x) = map (Annotated ann) (changesUponFlattening x)
||| Tries laying out a document into a single line by removing the contained
||| line breaks; if this does not fit the page, or has an `hardline`, the document
||| is laid out without changes.
export
group : Doc ann -> Doc ann
group (Union x y) = Union x y
group (FlatAlt x y) = case changesUponFlattening y of
Flattened y' => Union y' x
AlreadyFlat => Union y x
NeverFlat => x
group x = case changesUponFlattening x of
Flattened x' => Union x' x
AlreadyFlat => x
NeverFlat => x
||| By default renders the first document, When grouped renders the second, with
||| the first as fallback when there is not enough space.
export
flatAlt : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
flatAlt = FlatAlt
||| Advances to the next line and indents to the current nesting level.
export
line : Doc ann
line = FlatAlt Line (Chara ' ')
||| Like `line`, but behaves like `neutral` if the line break is undone by `group`.
export
line' : Doc ann
line' = FlatAlt Line Empty
||| First lays out the document. It then appends spaces until the width is equal to `i`.
||| If the width is already larger than `i`, the nesting level is decreased by `i`
||| and a line is appended.
export
fillBreak : Int -> Doc ann -> Doc ann
fillBreak f x = width x (\w => if w > f
then nest f line'
else spaces $ f - w)
||| Concatenate all documents element-wise with a binary function.
export
concatWith : (Doc ann -> Doc ann -> Doc ann) -> List (Doc ann) -> Doc ann
concatWith f [] = neutral
concatWith f (x :: xs) = foldl f x xs
||| Concatenates all documents horizontally with `(<++>)`.
export
hsep : List (Doc ann) -> Doc ann
hsep = concatWith (<++>)
||| Concatenates all documents above each other. If a `group` undoes the line breaks,
||| the documents are separated with a space instead.
export
vsep : List (Doc ann) -> Doc ann
vsep = concatWith (\x, y => x <+> line <+> y)
||| Concatenates the documents horizontally with `(<++>)` as long as it fits the page,
||| then inserts a line and continues.
export
fillSep : List (Doc ann) -> Doc ann
fillSep = concatWith (\x, y => x <+> softline <+> y)
||| Tries laying out the documents separated with spaces and if this does not fit,
||| separates them with newlines.
export
sep : List (Doc ann) -> Doc ann
sep = group . vsep
||| Concatenates all documents horizontally with `(<+>)`.
export
hcat : List (Doc ann) -> Doc ann
hcat = concatWith (<+>)
||| Vertically concatenates the documents. If it is grouped, the line breaks are removed.
export
vcat : List (Doc ann) -> Doc ann
vcat = concatWith (\x, y => x <+> line' <+> y)
||| Concatenates documents horizontally with `(<+>)` as log as it fits the page, then
||| inserts a line and continues.
export
fillCat : List (Doc ann) -> Doc ann
fillCat = concatWith (\x, y => x <+> softline' <+> y)
||| Tries laying out the documents separated with nothing, and if it does not fit the page,
||| separates them with newlines.
export
cat : List (Doc ann) -> Doc ann
cat = group . vcat
||| Appends `p` to all but the last document.
export
punctuate : Doc ann -> List (Doc ann) -> List (Doc ann)
punctuate _ [] = []
punctuate _ [d] = [d]
punctuate p (d :: ds) = (d <+> p) :: punctuate p ds
export
plural : (Num amount, Eq amount) => doc -> doc -> amount -> doc
plural one multiple n = if n == 1 then one else multiple
||| Encloses the document between two other documents using `(<+>)`.
export
enclose : Doc ann -> Doc ann -> Doc ann -> Doc ann
enclose l r x = l <+> x <+> r
||| Reordering of `encloses`.
||| Example: concatWith (surround (pretty ".")) [pretty "Text", pretty "PrettyPrint", pretty "Doc"]
||| Text.PrettyPrint.Doc
export
surround : Doc ann -> Doc ann -> Doc ann -> Doc ann
surround x l r = l <+> x <+> r
||| Concatenates the documents separated by `s` and encloses the resulting document by `l` and `r`.
export
encloseSep : Doc ann -> Doc ann -> Doc ann -> List (Doc ann) -> Doc ann
encloseSep l r s [] = l <+> r
encloseSep l r s [d] = l <+> d <+> r
encloseSep l r s ds = cat (zipWith (<+>) (l :: replicate (length ds `minus` 1) s) ds) <+> r
unsafeTextWithoutNewLines : String -> Doc ann
unsafeTextWithoutNewLines str = case strM str of
StrNil => Empty
StrCons c cs => if cs == ""
then Chara c
else Text (cast $ length str) str
||| Adds an annotation to a document.
export
annotate : ann -> Doc ann -> Doc ann
annotate = Annotated
||| Changes the annotations of a document. Individual annotations can be removed,
||| changed, or replaced by multiple ones.
export
alterAnnotations : (ann -> List ann') -> Doc ann -> Doc ann'
alterAnnotations re Empty = Empty
alterAnnotations re (Chara c) = Chara c
alterAnnotations re (Text l t) = Text l t
alterAnnotations re Line = Line
alterAnnotations re (FlatAlt x y) = FlatAlt (alterAnnotations re x) (alterAnnotations re y)
alterAnnotations re (Cat x y) = Cat (alterAnnotations re x) (alterAnnotations re y)
alterAnnotations re (Nest i x) = Nest i (alterAnnotations re x)
alterAnnotations re (Union x y) = Union (alterAnnotations re x) (alterAnnotations re y)
alterAnnotations re (Column f) = Column (\x => alterAnnotations re $ f x)
alterAnnotations re (WithPageWidth f) = WithPageWidth (\x => alterAnnotations re $ f x)
alterAnnotations re (Nesting f) = Nesting (\x => alterAnnotations re $ f x)
alterAnnotations re (Annotated ann x) = foldr Annotated (alterAnnotations re x) (re ann)
||| Removes all annotations.
export
unAnnotate : Doc ann -> Doc xxx
unAnnotate = alterAnnotations (const [])
||| Changes the annotations of a document.
export
reAnnotate : (ann -> ann') -> Doc ann -> Doc ann'
reAnnotate re = alterAnnotations (pure . re)
||| Alter the document's annotations.
export
Functor Doc where
map = reAnnotate
||| Overloaded converison to `Doc`.
public export
interface Pretty a where
pretty : a -> Doc ann
pretty x = prettyPrec Open x
prettyPrec : Prec -> a -> Doc ann
prettyPrec _ x = pretty x
export
Pretty String where
pretty = vsep . map unsafeTextWithoutNewLines . lines
||| Variant of `encloseSep` with braces and comma as separator.
export
list : List (Doc ann) -> Doc ann
list = group . encloseSep (flatAlt (pretty "[ ") (pretty "["))
(flatAlt (pretty " ]") (pretty "]"))
(pretty ", ")
||| Variant of `encloseSep` with parentheses and comma as separator.
export
tupled : List (Doc ann) -> Doc ann
tupled = group . encloseSep (flatAlt (pretty "( ") (pretty "("))
(flatAlt (pretty " )") (pretty ")"))
(pretty ", ")
export
Pretty a => Pretty (List a) where
pretty = align . list . map pretty
export
[prettyListMaybe] Pretty a => Pretty (List (Maybe a)) where
pretty = pretty . catMaybes
where catMaybes : List (Maybe a) -> List a
catMaybes [] = []
catMaybes (Nothing :: xs) = catMaybes xs
catMaybes ((Just x) :: xs) = x :: catMaybes xs
export
Pretty () where
pretty _ = pretty "()"
export
Pretty Bool where
pretty True = pretty "True"
pretty False = pretty "False"
export
Pretty Char where
pretty '\n' = line
pretty c = Chara c
export Pretty Nat where pretty = unsafeTextWithoutNewLines . show
export Pretty Int where pretty = unsafeTextWithoutNewLines . show
export Pretty Integer where pretty = unsafeTextWithoutNewLines . show
export Pretty Double where pretty = unsafeTextWithoutNewLines . show
export Pretty Bits8 where pretty = unsafeTextWithoutNewLines . show
export Pretty Bits16 where pretty = unsafeTextWithoutNewLines . show
export Pretty Bits32 where pretty = unsafeTextWithoutNewLines . show
export Pretty Bits64 where pretty = unsafeTextWithoutNewLines . show
export
(Pretty a, Pretty b) => Pretty (a, b) where
pretty (x, y) = tupled [pretty x, pretty y]
export
Pretty a => Pretty (Maybe a) where
pretty = maybe neutral pretty
||| Combines text nodes so they can be rendered more efficiently.
export
fuse : FusionDepth -> Doc ann -> Doc ann
fuse depth (Cat Empty x) = fuse depth x
fuse depth (Cat x Empty) = fuse depth x
fuse depth (Cat (Chara c1) (Chara c2)) = Text 2 (strCons c1 (strCons c2 ""))
fuse depth (Cat (Text lt t) (Chara c)) = Text (lt + 1) (t ++ singleton c)
fuse depth (Cat (Chara c) (Text lt t)) = Text (lt + 1) (strCons c t)
fuse depth (Cat (Text l1 t1) (Text l2 t2)) = Text (l1 + l2) (t1 ++ t2)
fuse depth (Cat (Chara x) (Cat (Chara y) z)) =
let sub = Text 2 (strCons x (strCons y "")) in
fuse depth $ assert_smaller (Cat (Chara x) (Cat (Chara y) z)) (Cat sub z)
fuse depth (Cat (Text lx x) (Cat (Chara y) z)) =
let sub = Text (lx + 1) (x ++ singleton y) in
fuse depth $ assert_smaller (Cat (Text lx x) (Cat (Chara y) z)) (Cat sub z)
fuse depth (Cat (Chara x) (Cat (Text ly y) z)) =
let sub = Text (ly + 1) (strCons x y) in
fuse depth $ assert_smaller (Cat (Chara x) (Cat (Text ly y) z)) (Cat sub z)
fuse depth (Cat (Text lx x) (Cat (Text ly y) z)) =
let sub = Text (lx + ly) (x ++ y) in
fuse depth $ assert_smaller (Cat (Text lx x) (Cat (Text ly y) z)) (Cat sub z)
fuse depth (Cat (Cat x (Chara y)) z) =
let sub = fuse depth (Cat (Chara y) z) in
assert_total $ fuse depth (Cat x sub)
fuse depth (Cat (Cat x (Text ly y)) z) =
let sub = fuse depth (Cat (Text ly y) z) in
assert_total $ fuse depth (Cat x sub)
fuse depth (Cat x y) = Cat (fuse depth x) (fuse depth y)
fuse depth (Nest i (Nest j x)) = fuse depth $ assert_smaller (Nest i (Nest j x)) (Nest (i + j) x)
fuse depth (Nest _ Empty) = Empty
fuse depth (Nest _ (Text lx x)) = Text lx x
fuse depth (Nest _ (Chara x)) = Chara x
fuse depth (Nest 0 x) = fuse depth x
fuse depth (Nest i x) = Nest i (fuse depth x)
fuse depth (Annotated ann x) = Annotated ann (fuse depth x)
fuse depth (FlatAlt x y) = FlatAlt (fuse depth x) (fuse depth y)
fuse depth (Union x y) = Union (fuse depth x) (fuse depth y)
fuse Shallow (Column f) = Column f
fuse depth (Column f) = Column (\x => fuse depth $ f x)
fuse Shallow (WithPageWidth f) = WithPageWidth f
fuse depth (WithPageWidth f) = WithPageWidth (\x => fuse depth $ f x)
fuse Shallow (Nesting f) = Nesting f
fuse depth (Nesting f) = Nesting (\x => fuse depth $ f x)
fuse depth x = x
||| This data type represents laid out documents and is used by the display functions.
public export
data SimpleDocStream : Type -> Type where
SEmpty : SimpleDocStream ann
SChar : (c : Char) -> (rest : Lazy (SimpleDocStream ann)) -> SimpleDocStream ann
SText : (len : Int) -> (text : String) -> (rest : Lazy (SimpleDocStream ann)) -> SimpleDocStream ann
SLine : (i : Int) -> (rest : SimpleDocStream ann) -> SimpleDocStream ann
SAnnPush : ann -> (rest : SimpleDocStream ann) -> SimpleDocStream ann
SAnnPop : (rest : SimpleDocStream ann) -> SimpleDocStream ann
internalError : SimpleDocStream ann
internalError = let msg = "<internal pretty printing error>" in
SText (cast $ length msg) msg SEmpty
data AnnotationRemoval = Remove | DontRemove
||| Changes the annotation of a document to a different annotation or none.
export
alterAnnotationsS : (ann -> Maybe ann') -> SimpleDocStream ann -> SimpleDocStream ann'
alterAnnotationsS re = fromMaybe internalError . go []
where
go : List AnnotationRemoval -> SimpleDocStream ann -> Maybe (SimpleDocStream ann')
go stack SEmpty = pure SEmpty
go stack (SChar c rest) = SChar c . delay <$> go stack rest
go stack (SText l t rest) = SText l t . delay <$> go stack rest
go stack (SLine l rest) = SLine l <$> go stack rest
go stack (SAnnPush ann rest) = case re ann of
Nothing => go (Remove :: stack) rest
Just ann' => SAnnPush ann' <$> go (DontRemove :: stack) rest
go stack (SAnnPop rest) = case stack of
[] => Nothing
DontRemove :: stack' => SAnnPop <$> go stack' rest
Remove :: stack' => go stack' rest
||| Removes all annotations.
export
unAnnotateS : SimpleDocStream ann -> SimpleDocStream xxx
unAnnotateS SEmpty = SEmpty
unAnnotateS (SChar c rest) = SChar c (unAnnotateS rest)
unAnnotateS (SText l t rest) = SText l t (unAnnotateS rest)
unAnnotateS (SLine l rest) = SLine l (unAnnotateS rest)
unAnnotateS (SAnnPush ann rest) = unAnnotateS rest
unAnnotateS (SAnnPop rest) = unAnnotateS rest
||| Changes the annotation of a document.
export
reAnnotateS : (ann -> ann') -> SimpleDocStream ann -> SimpleDocStream ann'
reAnnotateS re SEmpty = SEmpty
reAnnotateS re (SChar c rest) = SChar c (reAnnotateS re rest)
reAnnotateS re (SText l t rest) = SText l t (reAnnotateS re rest)
reAnnotateS re (SLine l rest) = SLine l (reAnnotateS re rest)
reAnnotateS re (SAnnPush ann rest) = SAnnPush (re ann) (reAnnotateS re rest)
reAnnotateS re (SAnnPop rest) = SAnnPop (reAnnotateS re rest)
export
Functor SimpleDocStream where
map = reAnnotateS
||| Collects all annotations from a document.
export
collectAnnotations : Monoid m => (ann -> m) -> SimpleDocStream ann -> m
collectAnnotations f SEmpty = neutral
collectAnnotations f (SChar c rest) = collectAnnotations f rest
collectAnnotations f (SText l t rest) = collectAnnotations f rest
collectAnnotations f (SLine l rest) = collectAnnotations f rest
collectAnnotations f (SAnnPush ann rest) = f ann <+> collectAnnotations f rest
collectAnnotations f (SAnnPop rest) = collectAnnotations f rest
||| Transform a document based on its annotations.
export
traverse : Applicative f => (ann -> f ann') -> SimpleDocStream ann -> f (SimpleDocStream ann')
traverse f SEmpty = pure SEmpty
traverse f (SChar c rest) = SChar c . delay <$> traverse f rest
traverse f (SText l t rest) = SText l t . delay <$> traverse f rest
traverse f (SLine l rest) = SLine l <$> traverse f rest
traverse f (SAnnPush ann rest) = SAnnPush <$> f ann <*> traverse f rest
traverse f (SAnnPop rest) = SAnnPop <$> traverse f rest
data WhitespaceStrippingState = AnnotationLevel Int | RecordedWithespace (List Int) Int
dropWhileEnd : (a -> Bool) -> List a -> List a
dropWhileEnd p = foldr (\x, xs => if p x && isNil xs then [] else x :: xs) []
||| Removes all trailing space characters.
export
removeTrailingWhitespace : SimpleDocStream ann -> SimpleDocStream ann
removeTrailingWhitespace = fromMaybe internalError . go (RecordedWithespace [] 0)
where
prependEmptyLines : List Int -> SimpleDocStream ann -> SimpleDocStream ann
prependEmptyLines is sds0 = foldr (\_, sds => SLine 0 sds) sds0 is
commitWhitespace : List Int -> Int -> SimpleDocStream ann -> SimpleDocStream ann
commitWhitespace [] 0 sds = sds
commitWhitespace [] 1 sds = SChar ' ' sds
commitWhitespace [] n sds = SText n (textSpaces n) sds
commitWhitespace (i :: is) n sds = prependEmptyLines is (SLine (i + n) sds)
go : WhitespaceStrippingState -> SimpleDocStream ann -> Maybe (SimpleDocStream ann)
go (AnnotationLevel _) SEmpty = pure SEmpty
go l@(AnnotationLevel _) (SChar c rest) = SChar c . delay <$> go l rest
go l@(AnnotationLevel _) (SText lt text rest) = SText lt text . delay <$> go l rest
go l@(AnnotationLevel _) (SLine i rest) = SLine i <$> go l rest
go (AnnotationLevel l) (SAnnPush ann rest) = SAnnPush ann <$> go (AnnotationLevel (l + 1)) rest
go (AnnotationLevel l) (SAnnPop rest) =
if l > 1
then SAnnPop <$> go (AnnotationLevel (l - 1)) rest
else SAnnPop <$> go (RecordedWithespace [] 0) rest
go (RecordedWithespace _ _) SEmpty = pure SEmpty
go (RecordedWithespace lines spaces) (SChar ' ' rest) = go (RecordedWithespace lines (spaces + 1)) rest
go (RecordedWithespace lines spaces) (SChar c rest) =
do rest' <- go (RecordedWithespace [] 0) rest
pure $ commitWhitespace lines spaces (SChar c rest')
go (RecordedWithespace lines spaces) (SText l text rest) =
let stripped = pack $ dropWhileEnd (== ' ') $ unpack text
strippedLength = cast $ length stripped
trailingLength = l - strippedLength in
if strippedLength == 0
then go (RecordedWithespace lines (spaces + l)) rest
else do rest' <- go (RecordedWithespace [] trailingLength) rest
pure $ commitWhitespace lines spaces (SText strippedLength stripped rest')
go (RecordedWithespace lines spaces) (SLine i rest) = go (RecordedWithespace (i :: lines) 0) rest
go (RecordedWithespace lines spaces) (SAnnPush ann rest) =
do rest' <- go (AnnotationLevel 1) rest
pure $ commitWhitespace lines spaces (SAnnPush ann rest')
go (RecordedWithespace lines spaces) (SAnnPop _) = Nothing
public export
FittingPredicate : Type -> Type
FittingPredicate ann = Int -> Int -> Maybe Int -> SimpleDocStream ann -> Bool
data LayoutPipeline ann = Nil | Cons Int (Doc ann) (LayoutPipeline ann) | UndoAnn (LayoutPipeline ann)
export
defaultPageWidth : PageWidth
defaultPageWidth = AvailablePerLine 80 1
round : Double -> Int
round x = if x > 0
then if x - floor x < 0.5 then cast $ floor x else cast $ ceiling x
else if ceiling x - x < 0.5 then cast $ ceiling x else cast $ floor x
||| The remaining width on the current line.
remainingWidth : Int -> Double -> Int -> Int -> Int
remainingWidth lineLength ribbonFraction lineIndent currentColumn =
let columnsLeftInLine = lineLength - currentColumn
ribbonWidth = (max 0 . min lineLength . round) (cast lineLength * ribbonFraction)
columnsLeftInRibbon = lineIndent + ribbonWidth - currentColumn in
min columnsLeftInLine columnsLeftInRibbon
public export
record LayoutOptions where
constructor MkLayoutOptions
layoutPageWidth : PageWidth
export
defaultLayoutOptions : LayoutOptions
defaultLayoutOptions = MkLayoutOptions defaultPageWidth
||| The Wadler/Leijen layout algorithm.
export
layoutWadlerLeijen : FittingPredicate ann -> PageWidth -> Doc ann -> SimpleDocStream ann
layoutWadlerLeijen fits pageWidth_ doc = best 0 0 (Cons 0 doc Nil)
where
initialIndentation : SimpleDocStream ann -> Maybe Int
initialIndentation (SLine i _) = Just i
initialIndentation (SAnnPush _ s) = initialIndentation s
initialIndentation (SAnnPop s) = initialIndentation s
initialIndentation _ = Nothing
selectNicer : Int -> Int -> SimpleDocStream ann -> Lazy (SimpleDocStream ann) -> SimpleDocStream ann
selectNicer lineIndent currentColumn x y =
if fits lineIndent currentColumn (initialIndentation y) x then x else y
best : Int -> Int -> LayoutPipeline ann -> SimpleDocStream ann
best _ _ Nil = SEmpty
best nl cc (UndoAnn ds) = SAnnPop (best nl cc ds)
best nl cc (Cons i Empty ds) = best nl cc ds
best nl cc (Cons i (Chara c) ds) = SChar c (best nl (cc + 1) ds)
best nl cc (Cons i (Text l t) ds) = SText l t (best nl (cc + l) ds)
best nl cc (Cons i Line ds) = let x = best i i ds
i' = case x of
SEmpty => 0
SLine _ _ => 0
_ => i in
SLine i' x
best nl cc c@(Cons i (FlatAlt x y) ds) = best nl cc $ assert_smaller c (Cons i x ds)
best nl cc (Cons i (Cat x y) ds) = assert_total $ best nl cc (Cons i x (Cons i y ds))
best nl cc c@(Cons i (Nest j x) ds) = best nl cc $ assert_smaller c (Cons (i + j) x ds)
best nl cc c@(Cons i (Union x y) ds) = let x' = best nl cc $ assert_smaller c (Cons i x ds)
y' = delay $ best nl cc $ assert_smaller c (Cons i y ds) in
selectNicer nl cc x' y'
best nl cc c@(Cons i (Column f) ds) = best nl cc $ assert_smaller c (Cons i (f cc) ds)
best nl cc c@(Cons i (WithPageWidth f) ds) = best nl cc $ assert_smaller c (Cons i (f pageWidth_) ds)
best nl cc c@(Cons i (Nesting f) ds) = best nl cc $ assert_smaller c (Cons i (f i) ds)
best nl cc c@(Cons i (Annotated ann x) ds) = SAnnPush ann $ best nl cc $ assert_smaller c (Cons i x (UndoAnn ds))
||| Layout a document with unbounded page width.
export
layoutUnbounded : Doc ann -> SimpleDocStream ann
layoutUnbounded = layoutWadlerLeijen (\_, _, _, sdoc => True) Unbounded
fits : Int -> SimpleDocStream ann -> Bool
fits w s = if w < 0 then False
else case s of
SEmpty => True
SChar _ x => fits (w - 1) x
SText l _ x => fits (w - l) x
SLine i x => True
SAnnPush _ x => fits w x
SAnnPop x => fits w x
||| The default layout algorithm.
export
layoutPretty : LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty (MkLayoutOptions pageWidth_@(AvailablePerLine lineLength ribbonFraction)) =
layoutWadlerLeijen (\lineIndent, currentColumn, _, sdoc =>
fits (remainingWidth lineLength ribbonFraction lineIndent currentColumn) sdoc) pageWidth_
layoutPretty (MkLayoutOptions Unbounded) = layoutUnbounded
||| Layout algorithm with more lookahead than layoutPretty.
export
layoutSmart : LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutSmart (MkLayoutOptions pageWidth_@(AvailablePerLine lineLength ribbonFraction)) =
layoutWadlerLeijen fits pageWidth_
where
fits : Int -> Int -> Maybe Int -> SimpleDocStream ann -> Bool
fits lineIndent currentColumn initialIndentY sdoc = go availableWidth sdoc
where
availableWidth : Int
availableWidth = remainingWidth lineLength ribbonFraction lineIndent currentColumn
minNestingLevel : Int
minNestingLevel = case initialIndentY of
Just i => min i currentColumn
Nothing => currentColumn
go : Int -> SimpleDocStream ann -> Bool
go w s = if w < 0
then False
else case s of
SEmpty => True
SChar _ x => go (w - 1) $ assert_smaller s x
SText l _ x => go (w - l) $ assert_smaller s x
SLine i x => if minNestingLevel < i
then go (lineLength - i) $ assert_smaller s x
else True
SAnnPush _ x => go w x
SAnnPop x => go w x
layoutSmart (MkLayoutOptions Unbounded) = layoutUnbounded
||| Lays out the document without adding any indentation. This layouter is very fast.
export
layoutCompact : Doc ann -> SimpleDocStream ann
layoutCompact doc = scan 0 [doc]
where
scan : Int -> List (Doc ann) -> SimpleDocStream ann
scan _ [] = SEmpty
scan col (Empty :: ds) = scan col ds
scan col ((Chara c) :: ds) = SChar c (scan (col + 1) ds)
scan col ((Text l t) :: ds) = SText l t (scan (col + l) ds)
scan col s@((FlatAlt x _) :: ds) = scan col $ assert_smaller s (x :: ds)
scan col (Line :: ds) = SLine 0 (scan 0 ds)
scan col s@((Cat x y) :: ds) = scan col $ assert_smaller s (x :: y :: ds)
scan col s@((Nest _ x) :: ds) = scan col $ assert_smaller s (x :: ds)
scan col s@((Union _ y) :: ds) = scan col $ assert_smaller s (y :: ds)
scan col s@((Column f) :: ds) = scan col $ assert_smaller s (f col :: ds)
scan col s@((WithPageWidth f) :: ds) = scan col $ assert_smaller s (f Unbounded :: ds)
scan col s@((Nesting f) :: ds) = scan col $ assert_smaller s (f 0 :: ds)
scan col s@((Annotated _ x) :: ds) = scan col $ assert_smaller s (x :: ds)
export
renderShow : SimpleDocStream ann -> (String -> String)
renderShow SEmpty = id
renderShow (SChar c x) = (strCons c) . renderShow x
renderShow (SText _ t x) = (t ++) . renderShow x
renderShow (SLine i x) = ((strCons '\n' $ textSpaces i) ++) . renderShow x
renderShow (SAnnPush _ x) = renderShow x
renderShow (SAnnPop x) = renderShow x
export
Show (Doc ann) where
show doc = renderShow (layoutPretty defaultLayoutOptions doc) ""

32
libs/contrib/Text/PrettyPrint/Prettyprinter/Render/String.idr Normal file
View File

@ -0,0 +1,32 @@
module Text.PrettyPrint.Prettyprinter.Render.String
import Data.Strings
import Data.String.Extra
import Text.PrettyPrint.Prettyprinter.Doc
%default total
export
renderString : SimpleDocStream ann -> String
renderString SEmpty = neutral
renderString (SChar c rest) = singleton c <+> renderString rest
renderString (SText l t rest) = t <+> renderString rest
renderString (SLine l rest) = singleton '\n' <+> textSpaces l <+> renderString rest
renderString (SAnnPush ann rest) = renderString rest
renderString (SAnnPop rest) = renderString rest
export
renderIO : SimpleDocStream ann -> IO ()
renderIO SEmpty = pure ()
renderIO (SChar c rest) = do putChar c; renderIO rest
renderIO (SText l t rest) = do putStr t; renderIO rest
renderIO (SLine l rest) = do putChar '\n'
putStr (textSpaces l)
renderIO rest
renderIO (SAnnPush ann rest) = renderIO rest
renderIO (SAnnPop rest) = renderIO rest
||| Prettyprints a document to standard output, using default options.
export
putDoc : Doc ann -> IO ()
putDoc = renderIO . layoutPretty defaultLayoutOptions

98
libs/contrib/Text/PrettyPrint/Prettyprinter/Render/Terminal.idr Normal file
View File

@ -0,0 +1,98 @@
module Text.PrettyPrint.Prettyprinter.Render.Terminal
import Data.Maybe
import Data.Strings
import Control.ANSI
import Control.Monad.ST
import Text.PrettyPrint.Prettyprinter.Doc
%default covering
public export
AnsiStyle : Type
AnsiStyle = List SGR
export
color : Color -> AnsiStyle
color c = pure $ SetForeground c
export
bgColor : Color -> AnsiStyle
bgColor c = pure $ SetBackground c
export
bold : AnsiStyle
bold = pure $ SetStyle Bold
export
italic : AnsiStyle
italic = pure $ SetStyle Italic
export
underline : AnsiStyle
underline = pure $ SetStyle SingleUnderline
export
strike : AnsiStyle
strike = pure $ SetStyle Striked
export
renderString : SimpleDocStream AnsiStyle -> String
renderString sdoc = fromMaybe "<internal pretty printing error>" $ runST $ do
styleStackRef <- newSTRef {a = List (List SGR)} [neutral]
outputRef <- newSTRef {a = String} neutral
go styleStackRef outputRef sdoc
readSTRef styleStackRef >>= \case
[] => pure Nothing
[_] => Just <$> readSTRef outputRef
_ => pure Nothing
where
push : STRef s (List AnsiStyle) -> List SGR -> ST s ()
push stack x = modifySTRef stack (x ::)
peek : STRef s (List AnsiStyle) -> ST s (Maybe AnsiStyle)
peek stack = do
(x :: _) <- readSTRef stack | [] => pure Nothing
pure (Just x)
pop : STRef s (List AnsiStyle) -> ST s (Maybe AnsiStyle)
pop stack = do
(x :: xs) <- readSTRef stack | [] => pure Nothing
writeSTRef stack xs
pure (Just x)
writeOutput : STRef s String -> String -> ST s ()
writeOutput out x = modifySTRef out (<+> x)
go : STRef s (List AnsiStyle) -> STRef s String -> SimpleDocStream AnsiStyle -> ST s ()
go stack out SEmpty = pure ()
go stack out (SChar c rest) = do
writeOutput out (singleton c)
go stack out rest
go stack out (SText l t rest) = do
writeOutput out t
go stack out rest
go stack out (SLine l rest) = do
writeOutput out (singleton '\n' <+> textSpaces l)
go stack out rest
go stack out (SAnnPush style rest) = do
Just currentStyle <- peek stack
| Nothing => writeSTRef stack []
let newStyle = style <+> currentStyle
push stack newStyle
writeOutput out (escapeSGR newStyle)
go stack out rest
go stack out (SAnnPop rest) = do
_ <- pop stack
Just newStyle <- peek stack
| Nothing => writeSTRef stack []
writeOutput out (escapeSGR (Reset :: newStyle))
go stack out rest
export
renderIO : SimpleDocStream AnsiStyle -> IO ()
renderIO = putStrLn . renderString
export
putDoc : Doc AnsiStyle -> IO ()
putDoc = renderIO . layoutPretty defaultLayoutOptions

95
libs/contrib/Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr Normal file
View File

@ -0,0 +1,95 @@
module Text.PrettyPrint.Prettyprinter.SimpleDocTree
import Text.PrettyPrint.Prettyprinter.Doc
import Text.Parser
%default total
||| Tree-like structure more suitable for rendering to a structured
||| format such as HTML.
public export
data SimpleDocTree : Type -> Type where
STEmpty : SimpleDocTree ann
STChar : (c : Char) -> SimpleDocTree ann
STText : (len : Int) -> (text : String) -> SimpleDocTree ann
STLine : (i : Int) -> SimpleDocTree ann
STAnn : ann -> (rest : SimpleDocTree ann) -> SimpleDocTree ann
STConcat : List (SimpleDocTree ann) -> SimpleDocTree ann
||| Changes the annotation of a document, or none at all.
export
alterAnnotationsST : (ann -> List ann') -> SimpleDocTree ann -> SimpleDocTree ann'
alterAnnotationsST re STEmpty = STEmpty
alterAnnotationsST re (STChar c) = STChar c
alterAnnotationsST re (STText len text) = STText len text
alterAnnotationsST re (STLine i) = STLine i
alterAnnotationsST re (STAnn ann rest) = foldr STAnn (alterAnnotationsST re rest) (re ann)
alterAnnotationsST re (STConcat xs) = assert_total $ STConcat (map (alterAnnotationsST re) xs)
||| Changes the annotation of a document.
export
reAnnotateST : (ann -> ann') -> SimpleDocTree ann -> SimpleDocTree ann'
reAnnotateST f = alterAnnotationsST (pure . f)
||| Removes all annotations.
export
unAnnotateST : SimpleDocTree ann -> SimpleDocTree xxx
unAnnotateST = alterAnnotationsST (const [])
||| Collects all annotations from a document.
export
collectAnnotations : Monoid m => (ann -> m) -> SimpleDocTree ann -> m
collectAnnotations f STEmpty = neutral
collectAnnotations f (STChar c) = neutral
collectAnnotations f (STText len text) = neutral
collectAnnotations f (STLine i) = neutral
collectAnnotations f (STAnn ann rest) = f ann <+> collectAnnotations f rest
collectAnnotations f (STConcat xs) = assert_total $ concat $ map (collectAnnotations f) xs
||| Transform a document based on its annotations.
export
traverse : Applicative f => (ann -> f ann') -> SimpleDocTree ann -> f (SimpleDocTree ann')
traverse f STEmpty = pure STEmpty
traverse f (STChar c) = pure $ STChar c
traverse f (STText len text) = pure $ STText len text
traverse f (STLine i) = pure $ STLine i
traverse f (STAnn ann rest) = STAnn <$> f ann <*> traverse f rest
traverse f (STConcat xs) = assert_total $ STConcat <$> Prelude.traverse (traverse f) xs
sdocToTreeParser : SimpleDocStream ann -> (Maybe (SimpleDocTree ann), Maybe (SimpleDocStream ann))
sdocToTreeParser SEmpty = (Just STEmpty, Nothing)
sdocToTreeParser (SChar c rest) = case sdocToTreeParser rest of
(Just tree, rest') => (Just $ STConcat [STChar c, tree], rest')
(Nothing, rest') => (Just $ STChar c, rest')
sdocToTreeParser (SText len text rest) = case sdocToTreeParser rest of
(Just tree, rest') => (Just $ STConcat [STText len text, tree], rest')
(Nothing, rest') => (Just $ STText len text, rest')
sdocToTreeParser (SLine i rest) = case sdocToTreeParser rest of
(Just tree, rest') => (Just $ STConcat [STLine i, tree], rest')
(Nothing, rest') => (Just $ STLine i, rest')
sdocToTreeParser (SAnnPush ann rest) = case sdocToTreeParser rest of
(tree, Nothing) => (Nothing, Nothing)
(Just tree, Nothing) => (Just $ STAnn ann tree, Nothing)
(Just tree, Just rest') => case sdocToTreeParser rest' of
(Just tree', rest'') => (Just $ STConcat [STAnn ann tree, tree'], rest'')
(Nothing, rest'') => (Just $ STAnn ann tree, rest'')
(Nothing, Just rest') => assert_total $ sdocToTreeParser rest'
(Nothing, Nothing) => (Nothing, Nothing)
sdocToTreeParser (SAnnPop rest) = (Nothing, Just rest)
export
fromStream : SimpleDocStream ann -> SimpleDocTree ann
fromStream sdoc = case sdocToTreeParser sdoc of
(Just tree, Nothing) => flatten tree
_ => internalError
where
flatten : SimpleDocTree ann -> SimpleDocTree ann
flatten (STConcat [x, STEmpty]) = flatten x
flatten (STConcat [x, STConcat xs]) = case flatten (STConcat xs) of
(STConcat xs') => STConcat (x :: xs')
y => y
flatten x = x
internalError : SimpleDocTree ann
internalError = let msg = "<internal pretty printing error>" in
STText (cast $ length msg) msg

105
libs/contrib/Text/PrettyPrint/Prettyprinter/Symbols.idr Normal file
View File

@ -0,0 +1,105 @@
module Text.PrettyPrint.Prettyprinter.Symbols
import Text.PrettyPrint.Prettyprinter.Doc
%default total
export
squote : Doc ann
squote = pretty '\''
export
dquote : Doc ann
dquote = pretty '"'
export
lparen : Doc ann
lparen = pretty '('
export
rparen : Doc ann
rparen = pretty ')'
export
langle : Doc ann
langle = pretty '<'
export
rangle : Doc ann
rangle = pretty '>'
export
lbracket : Doc ann
lbracket = pretty '['
export
rbracket : Doc ann
rbracket = pretty ']'
export
lbrace : Doc ann
lbrace = pretty '{'
export
rbrace : Doc ann
rbrace = pretty '}'
export
semi : Doc ann
semi = pretty ';'
export
colon : Doc ann
colon = pretty ':'
export
comma : Doc ann
comma = pretty ','
export
space : Doc ann
space = pretty ' '
export
dot : Doc ann
dot = pretty '.'
export
slash : Doc ann
slash = pretty '/'
export
backslash : Doc ann
backslash = pretty '\\'
export
equals : Doc ann
equals = pretty '='
export
pipe : Doc ann
pipe = pretty '|'
export
squotes : Doc ann -> Doc ann
squotes = enclose squote squote
export
dquotes : Doc ann -> Doc ann
dquotes = enclose dquote dquote
export
parens : Doc ann -> Doc ann
parens = enclose lparen rparen
export
angles : Doc ann -> Doc ann
angles = enclose langle rangle
export
brackets : Doc ann -> Doc ann
brackets = enclose lbracket rbracket
export
braces : Doc ann -> Doc ann
braces = enclose lbrace rbrace

31
libs/contrib/Text/PrettyPrint/Prettyprinter/Util.idr Normal file
View File

@ -0,0 +1,31 @@
module Text.PrettyPrint.Prettyprinter.Util
import Data.List
import Data.Strings
import Text.PrettyPrint.Prettyprinter.Doc
import Text.PrettyPrint.Prettyprinter.Render.String
%default total
||| Split an input into word-sized `Doc`.
export
words : String -> List (Doc ann)
words s = map pretty $ map pack (helper (unpack s))
where
helper : List Char -> List (List Char)
helper s =
case dropWhile isSpace s of
[] => []
s' => let (w, s'') = break isSpace s' in
w :: helper (assert_smaller s s'')
||| Insert soft linebreaks between words, so that text is broken into multiple
||| lines when it exceeds the available width.
export
reflow : String -> Doc ann
reflow = fillSep . words
||| Renders a document with a certain width.
export
putDocW : Nat -> Doc ann -> IO ()
putDocW w = renderIO . layoutPretty (record { layoutPageWidth = AvailablePerLine (cast w) 1 } defaultLayoutOptions)

7
libs/contrib/contrib.ipkg
View File

@ -54,6 +54,13 @@ modules = Control.ANSI,
Text.Lexer,
Text.Parser.Core,
Text.Lexer.Core,
Text.PrettyPrint.Prettyprinter,
Text.PrettyPrint.Prettyprinter.Doc,
Text.PrettyPrint.Prettyprinter.Symbols,
Text.PrettyPrint.Prettyprinter.Util,
Text.PrettyPrint.Prettyprinter.SimpleDocTree,
Text.PrettyPrint.Prettyprinter.Render.String,
Text.PrettyPrint.Prettyprinter.Render.Terminal,
System.Random,
System.Path,

8
libs/prelude/Prelude/EqOrd.idr
View File

@ -19,6 +19,10 @@ interface Eq ty where
x == y = not (x /= y)
x /= y = not (x == y)
public export
Eq Void where
_ == _ impossible
public export
Eq () where
_ == _ = True
@ -102,6 +106,10 @@ interface Eq ty => Ord ty where
min : ty -> ty -> ty
min x y = if (x < y) then x else y
public export
Ord Void where
compare _ _ impossible
public export
Ord () where
compare _ _ = EQ

2
samples/ffi/Small.idr
View File

@ -1,5 +1,5 @@
libsmall : String -> String
libsmall fn = "C:" ++ fn ++ ",libsmall"
libsmall fn = "C:" ++ fn ++ ",libsmallc"
%foreign (libsmall "add")
add : Int -> Int -> Int

2
samples/ffi/Struct.idr
View File

@ -1,7 +1,7 @@
import System.FFI
libsmall : String -> String
libsmall fn = "C:" ++ fn ++ ",libsmall"
libsmall fn = "C:" ++ fn ++ ",libsmallc"
Point : Type
Point = Struct "point" [("x", Int), ("y", Int)]

10
samples/ffi/smallc.c
View File

@ -1,3 +1,12 @@
// To compile this file for the samples `sample/ffi/Small.dir` and `sample/ffi/Struct.idr`, you will
// need to manually compile and link it into a `.so` file, and place it in a location where the
// resulting exectuable can find it. For example:
// gcc -c -fPIC smallc.c -o smallc.o
// gcc smallc.o -shared -o libsmallc.so
// idris2 Small.idr
// For an example of using Idris packages to build external (FFI) libraries, see the `FFI-readline`
// sample, and specifically `readline.ipkg`
#include <stdlib.h>
#include <stdio.h>
@ -36,4 +45,3 @@ point* mkPoint(int x, int y) {
void freePoint(point* pt) {
free(pt);
}

1
src/Core/CaseBuilder.idr
View File

@ -601,6 +601,7 @@ sameType {ns} fc phase fn env (p :: xs)
firstPat (pinf :: _) = pat pinf
headEq : NF ns -> NF ns -> Phase -> Bool
headEq (NBind _ _ (Pi _ _ _) _) (NBind _ _ (Pi _ _ _) _) _ = True
headEq (NTCon _ n _ _ _) (NTCon _ n' _ _ _) _ = n == n'
headEq (NPrimVal _ c) (NPrimVal _ c') _ = c == c'
headEq (NType _) (NType _) _ = True

5
src/Core/Context.idr
View File

@ -113,7 +113,7 @@ data Def : Type where
(constraints : List Int) -> Def
ImpBind : Def -- global name temporarily standing for an implicitly bound name
-- A delayed elaboration. The elaborators themselves are stored in the
-- unifiation state
-- unification state
Delayed : Def
export
@ -1726,7 +1726,8 @@ getDirectives : {auto c : Ref Ctxt Defs} ->
CG -> Core (List String)
getDirectives cg
= do defs <- get Ctxt
pure (mapMaybe getDir (cgdirectives defs))
pure $ defs.options.session.directives ++
mapMaybe getDir (cgdirectives defs)
where
getDir : (CG, String) -> Maybe String
getDir (x', str) = if cg == x' then Just str else Nothing

6
src/Core/Options.idr
View File

@ -123,6 +123,7 @@ record Session where
nobanner : Bool
findipkg : Bool
codegen : CG
directives : List String
logLevel : Nat
logTimings : Bool
debugElabCheck : Bool -- do conversion check to verify results of elaborator
@ -174,8 +175,9 @@ defaultPPrint = MkPPOpts False True False
export
defaultSession : Session
defaultSession = MkSessionOpts False False False Chez 0 False False
Nothing Nothing Nothing Nothing
defaultSession = MkSessionOpts False False False Chez [] 0
False False Nothing Nothing
Nothing Nothing
export
defaultElab : ElabDirectives

4
src/Idris/CommandLine.idr
View File

@ -51,6 +51,8 @@ data CLOpt
ExecFn String |
||| Use a specific code generator
SetCG String |
||| Pass a directive to the code generator
Directive String |
||| Don't implicitly import Prelude
NoPrelude |
||| Set source directory
@ -160,6 +162,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just "Don't implicitly import Prelude"),
MkOpt ["--codegen", "--cg"] [Required "backend"] (\f => [SetCG f])
(Just $ "Set code generator " ++ showDefault (codegen defaultSession)),
MkOpt ["--directive"] [Required "directive"] (\d => [Directive d])
(Just $ "Pass a directive to the current code generator"),
MkOpt ["--package", "-p"] [Required "package"] (\f => [PkgPath f])
(Just "Add a package as a dependency"),
MkOpt ["--source-dir"] [Required "dir"] (\d => [SourceDir d])

22
src/Idris/IDEMode/Commands.idr
View File

@ -34,6 +34,7 @@ data IDECommand
| MakeCase Integer String
| MakeWith Integer String
| DocsFor String (Maybe DocMode)
| Directive String
| Apropos String
| Metavariables Integer
| WhoCalls String
@ -75,7 +76,7 @@ getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n])
= Just $ CaseSplit l 0 n
getIDECommand (SExpList [SymbolAtom "add-clause", IntegerAtom l, StringAtom n])
= Just $ AddClause l n
getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
= Just $ AddMissing line n
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n])
= Just $ ExprSearch l n [] False
@ -105,9 +106,11 @@ getIDECommand (SExpList (SymbolAtom "docs-for" :: StringAtom n :: modeTail))
[SymbolAtom "overview"] => Just $ Just Overview
[SymbolAtom "full" ] => Just $ Just Full
_ => Nothing
Just $ DocsFor n modeOpt
Just $ DocsFor n modeOpt
getIDECommand (SExpList [SymbolAtom "apropos", StringAtom n])
= Just $ Apropos n
getIDECommand (SExpList [SymbolAtom "directive", StringAtom n])
= Just $ Directive n
getIDECommand (SExpList [SymbolAtom "metavariables", IntegerAtom n])
= Just $ Metavariables n
getIDECommand (SExpList [SymbolAtom "who-calls", StringAtom n])
@ -116,13 +119,13 @@ getIDECommand (SExpList [SymbolAtom "calls-who", StringAtom n])
= Just $ CallsWho n
getIDECommand (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
= Just $ BrowseNamespace ns
getIDECommand (SExpList [SymbolAtom "normalise-term", StringAtom tm])
getIDECommand (SExpList [SymbolAtom "normalise-term", StringAtom tm])
= Just $ NormaliseTerm tm
getIDECommand (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
= Just $ ShowTermImplicits tm
getIDECommand (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
= Just $ HideTermImplicits tm
getIDECommand (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
getIDECommand (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
= Just $ ElaborateTerm tm
getIDECommand (SExpList [SymbolAtom "print-definition", StringAtom n])
= Just $ PrintDefinition n
@ -151,7 +154,7 @@ putIDECommand (GenerateDef line n) = (SExpList [SymbolAtom "generate-
putIDECommand (MakeLemma line n) = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])
putIDECommand (MakeCase line n) = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
putIDECommand (MakeWith line n) = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])
putIDECommand (DocsFor n modeOpt) = let modeTail = case modeOpt of
putIDECommand (DocsFor n modeOpt) = let modeTail = case modeOpt of
Nothing => []
Just Overview => [SymbolAtom "overview"]
Just Full => [SymbolAtom "full"] in
@ -161,12 +164,13 @@ putIDECommand (Metavariables n) = (SExpList [SymbolAtom "metavaria
putIDECommand (WhoCalls n) = (SExpList [SymbolAtom "who-calls", StringAtom n])
putIDECommand (CallsWho n) = (SExpList [SymbolAtom "calls-who", StringAtom n])
putIDECommand (BrowseNamespace ns) = (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
putIDECommand (NormaliseTerm tm) = (SExpList [SymbolAtom "normalise-term", StringAtom tm])
putIDECommand (ShowTermImplicits tm) = (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
putIDECommand (HideTermImplicits tm) = (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
putIDECommand (ElaborateTerm tm) = (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
putIDECommand (NormaliseTerm tm) = (SExpList [SymbolAtom "normalise-term", StringAtom tm])
putIDECommand (ShowTermImplicits tm) = (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
putIDECommand (HideTermImplicits tm) = (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
putIDECommand (ElaborateTerm tm) = (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
putIDECommand (PrintDefinition n) = (SExpList [SymbolAtom "print-definition", StringAtom n])
putIDECommand (ReplCompletions n) = (SExpList [SymbolAtom "repl-completions", StringAtom n])
putIDECommand (Directive n) = (SExpList [SymbolAtom "directive", StringAtom n])
putIDECommand GetOptions = (SExpList [SymbolAtom "get-options"])
putIDECommand Version = SymbolAtom "version"

3
src/Idris/IDEMode/REPL.idr
View File

@ -182,6 +182,9 @@ process (DocsFor n modeOpt)
process (Apropos n)
= do todoCmd "apropros"
pure $ REPL $ Printed []
process (Directive n)
= do todoCmd "directive"
pure $ REPL $ Printed []
process (WhoCalls n)
= do todoCmd "who-calls"
pure $ NameList []

18
src/Idris/Parser.idr
View File

@ -1764,6 +1764,9 @@ data CmdArg : Type where
||| The command takes a module.
ModuleArg : CmdArg
||| The command takes a string
StringArg : CmdArg
||| The command takes multiple arguments.
Args : List CmdArg -> CmdArg
@ -1777,6 +1780,7 @@ Show CmdArg where
show OptionArg = "<option>"
show FileArg = "<file>"
show ModuleArg = "<module>"
show StringArg = "<module>"
show (Args args) = showSep " " (map show args)
export
@ -1826,6 +1830,19 @@ nameArgCmd parseCmd command doc = (names, NameArg, doc, parse)
n <- name
pure (command n)
stringArgCmd : ParseCmd -> (String -> REPLCmd) -> String -> CommandDefinition
stringArgCmd parseCmd command doc = (names, StringArg, doc, parse)
where
names : List String
names = extractNames parseCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
s <- strLit
pure (command s)
moduleArgCmd : ParseCmd -> (List String -> REPLCmd) -> String -> CommandDefinition
moduleArgCmd parseCmd command doc = (names, ModuleArg, doc, parse)
where
@ -1918,6 +1935,7 @@ parserCommandsForHelp =
, optArgCmd (ParseIdentCmd "unset") SetOpt False "Unset an option"
, compileArgsCmd (ParseREPLCmd ["c", "compile"]) Compile "Compile to an executable"
, exprArgCmd (ParseIdentCmd "exec") Exec "Compile to an executable and run"
, stringArgCmd (ParseIdentCmd "directive") CGDirective "Set a codegen-specific directive"
, noArgCmd (ParseREPLCmd ["r", "reload"]) Reload "Reload current file"
, noArgCmd (ParseREPLCmd ["e", "edit"]) Edit "Edit current file using $EDITOR or $VISUAL"
, nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing "Show missing clauses"

3
src/Idris/REPL.idr
View File

@ -727,6 +727,9 @@ process (Editing cmd)
res <- processEdit cmd
setPPrint ppopts
pure $ Edited res
process (CGDirective str)
= do setSession (record { directives $= (str::) } !getSession)
pure Done
process Quit
= pure Exited
process NOP

3
src/Idris/SetOptions.idr
View File

@ -71,6 +71,9 @@ preOptions (SetCG e :: opts)
coreLift $ putStrLn $ "Code generators available: " ++
showSep ", " (map fst (availableCGs (options defs)))
coreLift $ exitWith (ExitFailure 1)
preOptions (Directive d :: opts)
= do setSession (record { directives $= (d::) } !getSession)
preOptions opts
preOptions (PkgPath p :: opts)
= do addPkgDir p
preOptions opts

3
src/Idris/Syntax.idr
View File

@ -392,7 +392,7 @@ data EditCmd : Type where
public export
data REPLCmd : Type where
NewDefn : List PDecl -> REPLCmd
NewDefn : List PDecl -> REPLCmd
Eval : PTerm -> REPLCmd
Check : PTerm -> REPLCmd
PrintDef : Name -> REPLCmd
@ -407,6 +407,7 @@ data REPLCmd : Type where
DebugInfo : Name -> REPLCmd
SetOpt : REPLOpt -> REPLCmd
GetOpts : REPLCmd
CGDirective : String -> REPLCmd
CD : String -> REPLCmd
CWD: REPLCmd
Missing : Name -> REPLCmd