text:
module Main

import Data.String
import Data.List

maxByThird : Ord c => List (a, b, c) -> (a, b, c)
maxByThird = foldr1 (\(ax, ay, av), (x, y, v) => if v > av then (x, y, v) else (ax, ay, av))

cell : Integer -> Integer -> Integer -> Integer
cell x y serial = (mod (div ((((x + 10) * y) + serial) * (x + 10)) 100) 10) - 5

grid : Integer -> List (List Integer)
grid serial = [[cell x y serial | y <- [1..300]] | x <- [1..300]]

squareCell : Integer -> Integer -> Integer -> List (List Integer) -> Integer
squareCell size x y g = if (x + size - 1) > 300 || (y + size - 1) > 300 then 0 else
    sum
    . map (
        sum
        . List.take (fromIntegerNat size)
        . List.drop (fromIntegerNat (y - 1))
        )
    . List.take (fromIntegerNat size)
    . List.drop (fromIntegerNat (x - 1))
    $ g

square : Integer -> List (List Integer) -> (Integer, Integer, Integer)
square size g = maxByThird [(x, y, squareCell size x y g) | x <- [1..300 - (size - 2)], y <- [1..300 - (size - 2)]]

part1 : List (List Integer) -> (Integer, Integer, Integer)
part1 = square 3

part2 : List (List Integer) -> (Integer, Integer, Integer)
part2 g = maxByThird [square size g | size <- [1..10]]

main : IO()
main = do
    (Right str) <- readFile "11.in"
    let (Just serial) = String.parseInteger str
    let g = grid serial
    putStrLn "(x, (y, power)"
    printLn $ square 1 g
    printLn $ square 2 g
    putStrLn "Solution for part 1:"
    printLn $ square 3 g
    printLn $ square 4 g
    printLn $ square 5 g
    printLn $ square 6 g
    printLn $ square 7 g
    printLn $ square 8 g
    printLn $ square 9 g
    printLn $ square 10 g
    printLn $ square 11 g
    printLn $ square 12 g
    printLn $ square 13 g
    printLn $ square 14 g
    printLn $ square 15 g
    printLn $ square 16 g
    printLn $ square 17 g
    printLn $ square 18 g
    printLn $ square 19 g
    printLn $ square 20 g
    printLn $ square 21 g
    printLn $ square 22 g
    printLn $ square 23 g
    printLn $ square 24 g
    printLn $ square 25 g
    printLn $ square 26 g
    printLn $ square 27 g
    printLn $ square 28 g
    printLn $ square 29 g

    -- I do not want to optimize this right now, so... it works so it's good.
    -- You just take the biggest power, seems to be between 13 and 20 all the time.
    -- Starts at one, the size is the line number, not counting the info lines.

-- Solution part 1: 235,87
-- Solution part 2: 234,272,18

max_stars_repo_name: vypxl/aoc

max_issues_repo_name: vypxl/aoc

max_forks_repo_name: vypxl/aoc


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 2

-- exercise 1
val1 : (String, String, String)
val1 = ("A", "B", "C")
val2 : List String
val2 = ["A", "B", "C"]
val3 : ((String, String), String)
val3 = (("A", "B"), "C")

-- exercise 2
palindrome : String -> Bool
palindrome x = x == reverse x

-- exercise 3
palindrome2_1 : String -> Bool
palindrome2_1 x = let x' = toLower x in x' == reverse x'

palindrome2_2 : String -> Bool
palindrome2_2 x = palindrome (toLower x)

palindrome2_3 : String -> Bool
palindrome2_3 x = x' == (reverse x')
  where
    x' : String
    x' = toLower x

palindrome2_4 : String -> Bool
palindrome2_4 x = palindrome $ toLower x -- using $ instead of ()s

-- exercise 4
palindrome3_1 : String -> Bool
palindrome3_1 x = case length x >= 10 of
                        False => False
                        True => palindrome2_1 x

palindrome3_2 : String -> Bool
palindrome3_2 x = if length x >= 10
                      then palindrome2_1 x
                      else False

palindrome3_3 : String -> Bool
palindrome3_3 x = (length x >= 10) && palindrome2_1 x

-- exercise 5
palindrome4_1 : Nat -> String -> Bool
palindrome4_1 n x = case length x >= n of
                        False => False
                        True => palindrome2_1 x

palindrome4_2 : Nat -> String -> Bool
palindrome4_2 n x = if length x >= n
                      then palindrome2_1 x
                      else False

palindrome4_3 : Nat -> String -> Bool
palindrome4_3 n x = (length x >= n) && palindrome2_1 x

-- exercise 6
counts : String -> (Nat, Nat)
counts str = (length (words str), length str)

-- exercise 7
top_ten_1 : Ord a => List a -> List a
top_ten_1 xs = take 10 (reverse (sort xs))

top_ten_2 : Ord a => List a -> List a
top_ten_2 xs = take 10 $ reverse $ sort xs -- using $ instead of ()s

top_ten_3 : Ord a => List a -> List a
top_ten_3 xs = (Prelude.List.take 10) . reverse . sort $ xs -- using .

top_ten_4 : Ord a => List a -> List a
top_ten_4 = (Prelude.List.take 10) . reverse . sort -- using . & eta-reduction

-- exercise 8
over_length_1 : Nat -> List String -> Nat
over_length_1 k [] = 0
over_length_1 k (x :: xs) = case length x > k of
                               False => over_length_1 k xs
                               True => 1 + over_length_1 k xs

over_length_2 : Nat -> List String -> Nat
over_length_2 k xs = length (filter lengthMoreThanK xs) -- using filtering
                      where
                        lengthMoreThanK : String -> Bool
                        lengthMoreThanK str = length str > k

over_length_3 : Nat -> List String -> Nat
over_length_3 k xs = length (filter (\x => length x > k) xs) -- using lambda

over_length_4 : Nat -> List String -> Nat
over_length_4 k xs = let ls = map length xs in -- using map and filtering
                      length $ filter (> k) ls

-- exercise 9
-- run with ":exec ex9_1" or ":exec ex9_2" (or use a function main in a module Main)
ex9_1 : IO ()
ex9_1 = repl "Enter a string: " show_palindrome2_1
  where
    show_palindrome2_1 str = show (palindrome2_1 str) ++ "\n"

ex9_2 : IO ()
ex9_2 = repl "Enter a string: " show_counts
  where
    show_counts str = show (counts str) ++ "\n"

ext: idr

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Control.Permutation

import public Data.Group
import public Control.Permutation.Types
import public Control.Permutation.Mod
import public Control.Permutation.Proofs

max_stars_repo_name: vmchale/permutations

max_issues_repo_name: marcosh/permutations

max_forks_repo_name: marcosh/permutations


text:
TupleVect : Nat -> Type -> Type
TupleVect Z ty = ()
TupleVect (S k) ty = (ty, TupleVect k ty)

test : TupleVect 4 Nat
test = (1, 2, 3, 4, ())


text:
module Main

import public Data.Fin

%default total

{-
Terminology: parameters and indices

Vec defines a family of types.
- indexed by length
- parameterized by element type

Distinction between parameters and indices:
- parameter is unchanged across the entire structure (e.g, every element of the vector has the same type)
- index may change across a structure (e.g., every subvector has a different length)

Distinction useful when looking at function type
- specific value of a parameter can play no part in a function’s definition
- index might change definition
-}

infixr 7 :>

data Vec : Nat -> Type -> Type where
    V0   :                              Vec  Z    a
    (:>) : (x : a) -> (xs : Vec k a) -> Vec (S k) a

%name Vec xs, ys, zs

append : Vec n elem -> Vec m elem -> Vec (n + m) elem
append       V0  ys = ys
append (x :> xs) ys = x :> append xs ys

zip : Vec n a -> Vec n b -> Vec n (a, b)
zip       V0        V0  = V0
zip (x :> xs) (y :> ys) = (x, y) :> zip xs ys

{-
Fin n : unsigned number with non-inclusive upper bound of n.
name "Fin" says number is finitely bounded.

FZ and FS are constructors of Fin, corresponding to Z and S Nat constructors.
Can use numeric literals, as with Nat.
-}
index : Fin n -> Vec n a -> a
index  FZ    (x :>  _) = x
index (FS i) (_ :> ys) = index i ys

tryIndex' : Integer -> Vec n a -> Maybe a
tryIndex' _       V0  = Nothing
tryIndex' 0 (x :>  _) = Just x
tryIndex' i (_ :> xs) = tryIndex' (i - 1) xs

tryIndex : Integer -> Vec n a -> Maybe a
tryIndex {n} i xs =
    case integerToFin i n of
        Nothing    => Nothing
        (Just idx) => Just (index idx xs)

vectTake : (m : Nat) -> Vec (m + n) a -> Vec m a
vectTake  Z           _  = V0
vectTake (S k) (x :> xs) = x :> vectTake k xs

tvt : Vec (S Z) Integer
tvt = vectTake (S Z) (1:>2:>3:>4:>5:>6:>7:>V0)

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module Meriv.Core.Interfaces.Unifiable

-- interface Unifiable a with

max_stars_repo_name: Sintrastes/meriv-idr-prototype

max_issues_repo_name: Sintrastes/meriv-idr-prototype

max_forks_repo_name: Sintrastes/meriv-idr-prototype


text:
import Data.Vect

fourInts: Vect 4 Int
fourInts = [0, 1, 2, 3]

sixInts : Vect 6 Int
sixInts = [4, 5, 6, 7, 8, 9]

tenInts : Vect 10 Int
tenInts = fourInts ++ sixInts

allLengths : Vect len String -> Vect len Nat
allLengths [] = []
allLengths (word :: words) = length word :: allLengths words

insert : Ord elem => (x : elem) -> (xsSorted : Vect len elem) -> Vect (S len) elem
insert x [] = [x]
insert x (y :: xs) = case x < y of
                          False => y :: insert x xs
                          True =>  x :: y :: xs

insSort : Ord elem =>  Vect n elem -> Vect n elem
insSort [] = []
insSort (x :: xs) = let xsSorted = insSort xs in
                        insert x xsSorted


text:
module Main

import Data.Vect

test : Vect ?vlen String
test = ["Scala","Prolog","Haskell","Idris","Curry"]

vlen = %runElab

main : IO ()
main = putStrLn (show "Found length: \n" ++ ?vlen)

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
foo5 : Int -> Int
foo5 x with (x + 1)
foo5 x | y = y + x

foo6 : Int
foo6 = 52


text:
||| Logging utilities for the LSP server implementation.
|||
||| (C) The Idris Community, 2021
module Server.Log

import Core.Core
import Core.Context.Context
import Core.Directory
import Server.Configuration
import Server.Utils
import System.Directory
import System.File
import System.Path

%default total

||| Type for the severity of logging messages.
||| Levels are roughly categorised as follow:
||| - Debug    Messages targeted only for developing purposes
||| - Info     Messages for progress without unexpected behaviour or errors
||| - Warning  Messages for unsupported requests or wrong configurations
||| - Error    Messages for either server or compiler error which are unexpected but recoverable
||| - Critical Messages for error that require immediate stopping of the server
public export
data Severity = Debug | Info | Warning | Error | Critical

Cast Severity Integer where
  cast Debug    = 0
  cast Info     = 1
  cast Warning  = 2
  cast Error    = 3
  cast Critical = 4

export
Eq Severity where
  Debug    == Debug    = True
  Info     == Info     = True
  Warning  == Warning  = True
  Error    == Error    = True
  Critical == Critical = True
  _ == _ = False

export
Show Severity where
  show Debug    = "DEBUG"
  show Info     = "INFO"
  show Warning  = "WARNING"
  show Error    = "ERROR"
  show Critical = "CRITICAL"

export
Ord Severity where
  compare x y = compare (cast {to = Integer} x) (cast y)

public export
data Topic
  = AddClause
  | Browse
  | CaseSplit
  | Channel
  | CodeAction
  | Configuration
  | Diagnostic
  | DocumentHighlight
  | DocumentSymbol
  | ExprSearch
  | GenerateDef
  | GotoDefinition
  | Hover
  | MakeCase
  | MakeLemma
  | MakeWith
  | Metavars
  | QuickFix
  | RefineHole
  | SemanticTokens
  | Server
  | SignatureHelp

export
Show Topic where
  show AddClause = "Request.CodeAction.AddClause"
  show Browse = "Request.Command.Browse"
  show CaseSplit = "Request.CodeAction.CaseSplit"
  show Channel = "Communication.Channel"
  show CodeAction = "CodeAction"
  show Configuration = "Request.Configuration"
  show Diagnostic = "Notification.Diagnostic"
  show DocumentHighlight = "Request.DocumentHighlight"
  show DocumentSymbol = "Request.DocumentSymbol"
  show ExprSearch = "Request.CodeAction.ExprSearch"
  show GenerateDef = "Request.CodeAction.GenerateDef"
  show GotoDefinition = "Request.GotoDefinition"
  show Hover = "Request.Hover"
  show MakeCase = "Request.CodeAction.MakeCase"
  show MakeLemma = "Request.CodeAction.MakeLemma"
  show MakeWith = "Request.CodeAction.MakeWith"
  show Metavars = "Request.Command.Metavars"
  show QuickFix = "Request.CodeAction.QuickFix"
  show RefineHole = "Request.CodeAction.RefineHole"
  show SemanticTokens = "Notification.SemanticTokens"
  show Server = "Server"
  show SignatureHelp = "Request.SignatureHelp"

||| Logs a string with the provided severity level.
export
log : Ref LSPConf LSPConfiguration => Severity -> Topic -> String -> Core ()
log severity topic msg = do
  logHandle <- gets LSPConf logHandle
  coreLift_ $ fPutStrLn logHandle "LOG \{show severity}:\{show topic}: \{msg}"
  coreLift $ fflush logHandle

export
logD : Ref LSPConf LSPConfiguration => Topic -> String -> Core ()
logD = log Debug

export
logI : Ref LSPConf LSPConfiguration => Topic -> String -> Core ()
logI = log Info

export
logW : Ref LSPConf LSPConfiguration => Topic -> String -> Core ()
logW = log Warning

export
logE : Ref LSPConf LSPConfiguration => Topic -> String -> Core ()
logE = log Error

export
logC : Ref LSPConf LSPConfiguration => Topic -> String -> Core ()
logC = log Critical

||| Changes the log file location, if possible.
export covering
changeLogFile : Ref LSPConf LSPConfiguration => String -> Core ()
changeLogFile fname = do
  let True = isAbsolute fname
    | False => logE Configuration "Unable to change log file location: \{fname} is not an absolute path"
  whenJust (parent fname) $ \dir => do
    Right _ <- coreLift $ mkdirAll dir
      | Left err => logE Configuration "Unable to create directory \{dir}: \{show err}"
    logD Configuration "Created new directory \{dir} for log file \{fname}"
  Right handle <- coreLift $ openFile fname Append
    | Left err => logE Configuration "Unable to updated log file location \{fname}: \{show err}"
  update LSPConf ({ logHandle := handle })
  logI Configuration "Log file location updated to \{fname}"


text:
-- --------------------------------------------------------------- [ Day10.idr ]
-- Module      : Data.Advent.Day10
-- Description : My solution to the Day 10 puzzle of the 2016 Advent of Code.
-- Copyright   : Copyright (c) 2016, Eric Bailey
-- License     : MIT
-- Link        : https://adventofcode.com/2016/day/2
-- --------------------------------------------------------------------- [ EOH ]
||| Day 10: Balance Bots
module Data.Advent.Day10

import Data.Advent.Day

import public Data.SortedMap

import Effects
import Effect.State

%default total

-- -------------------------------------------------------------- [ Data Types ]

%access public export

Chip : Type
Chip = Nat

OutBin : Type
OutBin = Nat

BotID : Type
BotID = Nat

data Give = ToBot BotID
          | ToOutBin OutBin

data Instruction = Bot BotID Give Give
                 | GoesTo Chip BotID

-- ----------------------------------------------------------------- [ Parsers ]

%default partial

%access export

nat : Parser Nat
nat = fromIntegerNat <$> integer

toBot : Parser Give
toBot = ToBot <$> (string "bot " *> nat) <?> "bot n"

toOutBin : Parser Give
toOutBin = ToOutBin <$> (string "output " *> nat) <?> "output n"

to : Parser Give
to = toBot <|> toOutBin <?> "{bot,output} n"

value : Parser Instruction
value = [| GoesTo (string "value " *> nat) (string " goes to bot " *> nat) |]

bot : Parser Instruction
bot = [| Bot (string "bot " *> nat)
             (string " gives low to " *> to)
             (string " and high to " *> to) |]

instruction : Parser Instruction
instruction = bot <|> value

-- ------------------------------------------------------------------- [ State ]

%default total

BotResponsibilities : Type
BotResponsibilities = SortedMap BotID (List Chip)

implementation Default BotResponsibilities where default = empty

BotState : Type -> Type
BotState ty = Eff ty [STATE BotResponsibilities]

-- ------------------------------------------------------------------- [ Logic ]

getChips : BotID -> BotState (List Chip)
getChips b = fromMaybe [] . lookup b <$> get

consChip : BotID -> Chip -> BotState ()
consChip b c = update (insert b (c :: !(getChips b)))

giveChip : Give -> Chip -> BotState (List (OutBin, Chip))
giveChip (ToBot b) c    = consChip b c *> pure []
giveChip (ToOutBin o) c = pure [(o, c)]

%default partial

zoom : List Instruction -> BotState (List (OutBin, Chip))
zoom []                    = pure []
zoom (i@(GoesTo c b)::is)  = consChip b c *> zoom is
zoom (i@(Bot b lo hi)::is) =
    do [c1,c2] <- sort <$> getChips b
         | _ => zoom (is ++ [i])
       pure $ !(giveChip lo c1) ++ !(giveChip hi c2) ++ !(zoom is)

-- ----------------------------------------------------------------- [ Example ]

example : BotState (List (OutBin, Chip))
example = zoom [
            GoesTo 5 2,
            Bot 2 (ToBot 1) (ToBot 0),
            GoesTo 3 1,
            Bot 1 (ToOutBin 1) (ToBot 0),
            Bot 0 (ToOutBin 2) (ToOutBin 0),
            GoesTo 2 2
          ]

runExample : List (OutBin, Chip)
runExample = runPure example

-- ---------------------------------------------------------------- [ Part One ]

partOne : List Instruction -> Maybe BotID
partOne is = runPure $ zoom is *> go <$> get
  where
    go : BotResponsibilities -> Maybe BotID
    go st = fst <$> find (\(_,cs) => sort cs == [17,61]) (toList st)

-- ---------------------------------------------------------------- [ Part Two ]

partTwo : List Instruction -> Nat
partTwo is = foldl go 1 (runPure (zoom is))
  where
    go : Nat -> (OutBin, Chip) -> Nat
    go acc (o,c) = if List.elem o [0,1,2] then c * acc else acc

-- -------------------------------------------------------------------- [ Main ]

namespace Main

    main : IO ()
    main = runDay $ MkDay 10 (some (instruction <* newline))
                    (pure . show . partOne)
                    (pure . show . partTwo)

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: yurrriq/advent-of-code


text:
module Exercises.Chapter6

import Data.Vect

%access public export

-- Exercise 6.2.3.1

||| An `n` by `m` matrix.
Matrix : (n, m : Nat) -> Type
Matrix n m = Vect n (Vect m Double)

-- Exercise 6.2.3.2

data Format = Number     Format
            | Dbl        Format
            | Chr        Format
            | Str        Format
            | Lit String Format
            | End

PrintfType : Format -> Type
PrintfType (Number  fmt) = (i : Int)    -> PrintfType fmt
PrintfType (Dbl     fmt) = (i : Double) -> PrintfType fmt
PrintfType (Chr     fmt) = (c : Char)   -> PrintfType fmt
PrintfType (Str     fmt) = (s : String) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType  End          = String

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number  fmt) acc = printfFmt fmt . (acc ++) . show
printfFmt (Dbl     fmt) acc = printfFmt fmt . (acc ++) . show
printfFmt (Chr     fmt) acc = printfFmt fmt . (acc ++) . flip strCons ""
printfFmt (Str     fmt) acc = printfFmt fmt . (acc ++)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt  End          acc = acc

toFormat : (xs : List Char) -> Format
toFormat []                    = End
toFormat ('%' :: 'd' :: chars) = Number  (toFormat chars)
toFormat ('%' :: 'f' :: chars) = Dbl     (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Chr     (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str     (toFormat chars)
toFormat ('%'        :: chars) = Lit "%" (toFormat chars)
toFormat ( c         :: chars) with (toFormat chars)
  | (Lit lit chars') = Lit (strCons c lit) chars'
  |  fmt             = Lit (strCons c "")  fmt

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""

-- Exercise 6.2.3.3

TupleVect : (k : Nat) -> (a : Type) -> Type
TupleVect  Z    a = ()
TupleVect (S k) a = (a, TupleVect k a)

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Main

import Hardware
import Processor
import Examples

--------------------------------------------------
--                  main

main : IO ()
main = do printLn "Registers before: "
          printRegisters simpleLoop
          printLn "Registers after: "
          printRegisters $ evaluator simpleLoop
          printLn "Expected result is 6 in R1"
          printLn ""

max_stars_repo_name: nickgeoca/QVM

max_issues_repo_name: nickgeoca/QVM

max_forks_repo_name: nickgeoca/QVM


text:
module Main

data ListZ : Type -> Type where
  (::) : a -> Lazy (ListZ a) -> ListZ a
  Nil  : ListZ a

implementation Show a => Show (ListZ a) where
  show xs = "[" ++ show' "" xs ++ "]"
      where
        show' acc Nil        = acc
        show' acc (x :: Nil) = acc ++ show x
        show' acc (x :: xs)  = show' (acc ++ show x ++ ", ") xs

foo : ListZ Nat
foo = (1 :: 2 :: 3 :: Nil)

main : IO ()
main = printLn foo

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
> module Enumerated.Enumerated

> import Data.Vect

> %default total
> %auto_implicits off
> %access public export

> interface Enumerated (t : Type) (len : Nat) | t where
>   values : Vect len t
>   toFin  : t -> Fin len
>   values_match_toFin : map toFin values = range

> {-

> using (t : Type, len : Nat)
>   implementation Enumerated t len => Eq t where
>     x == y = toFin x == toFin y

> -}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Libraries.Data.List.Lazy

%default total

-- All functions here are public export
-- because their definitions are pretty much the specification.

public export
data LazyList : Type -> Type where
  Nil : LazyList a
  (::) : (1 x : a) -> (1 xs : Lazy (LazyList a)) -> LazyList a

public export
(++) : LazyList a -> Lazy (LazyList a) -> LazyList a
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

--- Interface implementations ---

public export
Semigroup (LazyList a) where
  [] <+> ys = ys
  (x :: xs) <+> ys = x :: (xs <+> ys)

public export
Monoid (LazyList a) where
  neutral = []

public export
Foldable LazyList where
  foldr op nil [] = nil
  foldr op nil (x :: xs) = x `op` foldr op nil xs

  foldl op acc [] = acc
  foldl op acc (x :: xs) = foldl op (acc `op` x) xs

  null []     = True
  null (_::_) = False

public export
Functor LazyList where
  map f [] = []
  map f (x :: xs) = f x :: map f xs

public export
Applicative LazyList where
  pure x = [x]
  fs <*> vs = concatMap (\f => map f vs) fs

public export
Alternative LazyList where
  empty = []
  xs <|> ys = xs ++ ys

public export
Monad LazyList where
  m >>= f = concatMap f m

-- There is no Traversable instance for lazy lists.
-- The result of a traversal will be a non-lazy list in general
-- (you can't delay the "effect" of an applicative functor).
public export
traverse : Applicative f => (a -> f b) -> LazyList a -> f (List b)
traverse g [] = pure []
traverse g (x :: xs) = [| g x :: traverse g xs |]

public export
sequence : Applicative f => LazyList (f a) -> f (List a)
sequence = traverse id

--- Lists creation ---

public export
fromList : List a -> LazyList a
fromList []      = []
fromList (x::xs) = x :: fromList xs

covering
public export
iterate : (f : a -> Maybe a) -> (x : a) -> LazyList a
iterate f x = x :: case f x of
  Nothing => []
  Just y  => iterate f y

covering
public export
unfoldr : (b -> Maybe (a, b)) -> b -> LazyList a
unfoldr f c = case f c of
  Nothing     => []
  Just (a, n) => a :: unfoldr f n

public export
iterateN : Nat -> (a -> a) -> a -> LazyList a
iterateN Z     _ _ = []
iterateN (S n) f x = x :: iterateN n f (f x)

public export
replicate : (n : Nat) -> (x : a) -> LazyList a
replicate Z     _ = []
replicate (S n) x = x :: replicate n x

--- Functions acquiring parts of list ---

public export
head' : LazyList a -> Maybe a
head' []     = Nothing
head' (x::_) = Just x

export
tail' : LazyList a -> Maybe (LazyList a)
tail' []      = Nothing
tail' (_::xs) = Just xs

--- Functions for acquiring different types of sublists ---

public export
take : Nat -> LazyList a -> LazyList a
take (S k) (x::xs) = x :: take k xs
take _ _ = []

public export
drop : Nat -> LazyList a -> LazyList a
drop Z     xs      = xs
drop (S _) []      = []
drop (S n) (_::xs) = drop n xs

public export
takeWhile : (a -> Bool) -> LazyList a -> LazyList a
takeWhile p []      = []
takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []

public export
dropWhile : (a -> Bool) -> LazyList a -> LazyList a
dropWhile p []      = []
dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs

public export
filter : (a -> Bool) -> LazyList a -> LazyList a
filter p []      = []
filter p (x::xs) = if p x then x :: filter p xs else filter p xs

public export
mapMaybe : (a -> Maybe b) -> LazyList a -> LazyList b
mapMaybe f []      = []
mapMaybe f (x::xs) = case f x of
  Nothing => mapMaybe f xs
  Just y  => y :: mapMaybe f xs


text:
test : () -> IO ()
test () = putStrLn "a test"
test _  = putStrLn "oopsie"

main : IO ()
main = do test ()
          putStrLn "foo" >>= test


text:
module Main

%access  public export
%default total

||| Given two strings, return the length of the longer one.
longerLength : String -> String -> Nat
longerLength = max `on` length
  where
    on : (b -> b -> c) -> (a -> b) -> a -> a -> c
    on g f x y = f x `g` f y

-- Exercise 5.1.4.1

namespace Do
  main : IO ()
  main = do
    putStr "String A: "
    stringA <- getLine
    putStr "String B: "
    stringB <- getLine
    printLn $ longerLength stringA stringB

-- Exercise 5.1.4.2

namespace Bind
  main : IO ()
  main =
    putStr "String A: " *> getLine >>= \stringA =>
    putStr "String B: " *> getLine >>= \stringB =>
    printLn $ longerLength stringA stringB


text:
||| Copyright 2016 Google Inc.
|||
||| Licensed under the Apache License, Version 2.0 (the "License");
||| you may not use this file except in compliance with the License.
||| You may obtain a copy of the License at
|||
|||     http://www.apache.org/licenses/LICENSE-2.0
|||
||| Unless required by applicable law or agreed to in writing, software
||| distributed under the License is distributed on an "AS IS" BASIS,
||| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
||| See the License for the specific language governing permissions and
||| limitations under the License.

module Test.Parser

import Test.UnitTest
import Test.Utils
import Protobuf.Core
import Protobuf.Parser
import Protobuf.Util

%access export

protoFileContents : String
protoFileContents = unlines [
  "message Person {",
  "  required string name = 0;",
  "  required int32 id = 1;",
  "  optional string email = 2;",
  "  message PhoneNumber {",
  "    required string number = 0;",
  "    enum PhoneType {MOBILE = 0; HOME = 1; WORK = 2;}",
  "    optional Person.PhoneNumber.PhoneType type = 1;",
  "  }",
  "  repeated Person.PhoneNumber phone = 3;",
  "}",
  ""
]

expectedFileDescriptor : (List MessageDescriptor, List EnumDescriptor)
expectedFileDescriptor = ([PhoneNumber, Person], [PhoneType])

allTests : IO ()
allTests = runTests (MkTestFixture "Parser" [
  MkTestCase "ParseFileDescriptor"
    (assertEq (parseFile protoFileContents) (Right expectedFileDescriptor))
])

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf


text:
module Main

%foreign "Dart:cantUseBool,lib.dart"
cantUseBool : Bool -> Int

main : IO ()
main = printLn (cantUseBool True)


text:
import DepPairs
import Do
import Hello
import Loops
import PrintLength
import ReadNum
import ReadVect


text:
module AOC.Day.Two

import AOC.Solution
import Data.String

%default total

----------------------------------------------------------------------------
-- Types -------------------------------------------------------------------
----------------------------------------------------------------------------

data Direction = Forward Integer
               | Up Integer
               | Down Integer

InputType : Type
InputType = List Direction

----------------------------------------------------------------------------
-- Interfaces --------------------------------------------------------------
----------------------------------------------------------------------------

-- These interfaces not strictly necessary, but are helpful for debugging.

partial
Cast String (Maybe Direction) where
    cast x = case (words x) of
        ("forward" :: (a :: [])) => Just (Forward (cast a))
        ("up" :: (a :: [])) => Just (Up (cast a))
        ("down" :: (a :: [])) => Just (Down (cast a))
        _ => Nothing

Show Direction where
    show (Forward x) = "forward " ++ (show x)
    show (Up x) = "up " ++ (show x)
    show (Down x) = "down " ++ (show x)

----------------------------------------------------------------------------
-- Helper Functions --------------------------------------------------------
----------------------------------------------------------------------------

direction_helper : (Integer, Integer) -> List Direction -> (Integer, Integer)
direction_helper vals [] = vals
direction_helper (f, ud) ((Forward x) :: dirs) = direction_helper (f + x, ud) dirs
direction_helper (f, ud) ((Up x) :: dirs) = direction_helper (f, ud - x) dirs
direction_helper (f, ud) ((Down x) :: dirs) = direction_helper (f, ud + x) dirs

direction : List Direction -> Integer
direction dirs = let
  (f, ud) = direction_helper (0, 0) dirs
  in f * ud

direction_helper2 : (Integer, Integer, Integer) -> List Direction -> (Integer, Integer, Integer)
direction_helper2 vals [] = vals
direction_helper2 (f, ud, aim) ((Forward x) :: dirs) = direction_helper2 (f + x, ud + aim * x, aim) dirs
direction_helper2 (f, ud, aim) ((Up x) :: dirs) = direction_helper2 (f, ud, aim - x) dirs
direction_helper2 (f, ud, aim) ((Down x) :: dirs) = direction_helper2 (f, ud, aim + x) dirs

direction2 : List Direction -> Integer
direction2 dirs = let
  (f, ud, aim) = direction_helper2 (0, 0, 0) dirs
  in f * ud

----------------------------------------------------------------------------
-- Solutions ---------------------------------------------------------------
----------------------------------------------------------------------------

part1 : InputType -> Integer
part1 = direction

part2 : InputType -> Integer
part2 = direction2

----------------------------------------------------------------------------
-- Interface for input/output ----------------------------------------------
----------------------------------------------------------------------------

-- Why is this partial?
partial
parser : String -> Maybe InputType
parser = sequence . map (the (Maybe Direction) . cast) . lines

partial
export
day2 : (inputType ** AOCSolution inputType)
day2 = solutionToDP (MkAOCSolution {
    day = 2
  , parser = parser
  , part1 = show . part1
  , part2 = show . part2
  })


text:
module Control.Applicative.Const

import Data.Contravariant
import Data.Bits

%default total

public export
record Const (a : Type) (b : Type) where
  constructor MkConst
  runConst : a

public export
Eq a => Eq (Const a b) where
  (==) = (==) `on` runConst

public export
Ord a => Ord (Const a b) where
  compare = compare `on` runConst

export
Show a => Show (Const a b) where
  showPrec p (MkConst v) = showCon p "MkConst" (showArg v)

public export
Semigroup a => Semigroup (Const a b) where
  MkConst x <+> MkConst y = MkConst (x <+> y)

public export
Monoid a => Monoid (Const a b) where
  neutral = MkConst neutral

public export
Num a => Num (Const a b) where
  MkConst x + MkConst y = MkConst (x + y)
  MkConst x * MkConst y = MkConst (x * y)
  fromInteger = MkConst . fromInteger

public export
Neg a => Neg (Const a b) where
  negate (MkConst x)    = MkConst (negate x)
  MkConst x - MkConst y = MkConst (x - y)

public export
Abs a => Abs (Const a b) where
  abs (MkConst x)    = MkConst (abs x)

public export
Fractional a => Fractional (Const a b) where
  recip (MkConst x)     = MkConst (recip x)
  MkConst x / MkConst y = MkConst (x / y)

public export
Integral a => Integral (Const a b) where
  MkConst x `div` MkConst y = MkConst (x `div` y)
  MkConst x `mod` MkConst y = MkConst (x `mod` y)

public export
Bits a => Bits (Const a b) where
  Index = Index {a}
  MkConst x .&. MkConst y = MkConst (x .&. y)
  MkConst x .|. MkConst y = MkConst (x .|. y)
  MkConst x `xor` MkConst y = MkConst (x `xor` y)
  shiftL (MkConst v) ix = MkConst (shiftL v ix)
  shiftR (MkConst v) ix = MkConst (shiftR v ix)
  bit = MkConst . bit
  zeroBits = MkConst zeroBits
  complement (MkConst v) = MkConst (complement v)
  oneBits = MkConst oneBits
  complementBit (MkConst v) ix = MkConst (complementBit v ix)
  clearBit (MkConst v) ix = MkConst (clearBit v ix)
  testBit (MkConst v) ix = testBit v ix
  setBit (MkConst v) ix = MkConst (setBit v ix)

public export
FromString a => FromString (Const a b) where
  fromString = MkConst . fromString

public export
Functor (Const a) where
  map _ (MkConst v) = MkConst v

public export
Contravariant (Const a) where
  contramap _ (MkConst v) = MkConst v

public export
Monoid a => Applicative (Const a) where
  pure _ = MkConst neutral
  MkConst x <*> MkConst y = MkConst (x <+> y)

public export
Foldable (Const a) where
  foldr _ acc _ = acc
  foldl _ acc _ = acc
  null _ = True
  toList _ = []
  foldMap _ _ = neutral

public export
Traversable (Const a) where
  traverse _ (MkConst v) = pure (MkConst v)

public export
Bifunctor Const where
  bimap f _ (MkConst v) = MkConst (f v)

public export
Bifoldable Const where
  bifoldr f _ acc (MkConst v) = f v acc
  bifoldl f _ acc (MkConst v) = f acc v
  binull _ = False

public export
Bitraversable Const where
  bitraverse f _ (MkConst v) = MkConst <$> f v


text:
-- --------------------------------------------------------------- [ Error.idr ]
-- Module    : Error.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

module Toolkit.Options.ArgParse.Error

import Data.List1
import Data.String

import System.File

import Toolkit.Data.Location

import Toolkit.Options.ArgParse.Model
import Toolkit.Options.ArgParse.Lexer
import Toolkit.Options.ArgParse.Parser

%default total

public export
data ArgParseError : Type where
  InvalidOption   : Arg -> ArgParseError
  MalformedOption : ParseError Token -> ArgParseError

export
Show a => Show (ParseFailure a) where
  show err
    = trim $ unlines [show (location err), (error err)]

export
Show a => Show (Run.ParseError a) where
  show (FError err)
    = trim $ unlines ["File Error: "
                     , show err]
  show (PError err)
    = trim $ unlines (forget (map show err))

  show (LError (MkLexFail l i))
    = trim $ unlines [show l, show i]

export
(Show Arg) => Show ArgParseError where
  show (InvalidOption o)
    = "Invalid Option " ++ show o
  show (MalformedOption err)
    = show err

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Options.Applicative.Test

import Options.Applicative

test1 : Either ParseError String
test1 = runParserFully p ["--hello", "there"]
  where
    p : Parser String
    p = strOption ( long "hello" )

test2 : String
test2 = show $ parserHelp p
    where
      p : Parser String
      p = strOption ( long "hello" )

public export covering
main : IO ()
main = case test1 of
  Left err => putStrLn "err"
  Right res => putStrLn res


text:
module Test

import Lambdapants.Command
import Lambdapants.Command.Parser
import Lambdapants.Term
import Lambdapants.Term.Parser
import Lambdapants.Term.Reduction
import Lightyear
import Lightyear.Strings

partial parseUnsafe_ : String -> Term
parseUnsafe_ input =
  case parse term input of
       Right t => t

export test : IO ()
test = do

  -- Test reductions

  putStrLn (show (isLeft (parse term "\\x.x )))")))
  putStrLn (show (isRight (parse term "\\x.x")))

  let t0 = parseUnsafe_ "(\\x.\\y.x y) y"
  putStrLn (show (parseUnsafe_ "\\z.y z" `alphaEq` nor t0))

  let t0_1 = parseUnsafe_ "(\\x.\\y.\\z.x y z) z"
  putStrLn (show (parseUnsafe_ "\\y.\\z0.z y z0" `alphaEq` nor t0_1))

  let t0_2 = parseUnsafe_ "(\\x.\\y.\\z.\\a.x y z a) (z a)"
  putStrLn (show (parseUnsafe_ "\\y.\\z0.\\a0.(z a) y z0 a0" `alphaEq` nor t0_2))

  let t1 = parseUnsafe_ "(\\a.\\b.a) c ((\\d.e) d)"
  let t2 = parseUnsafe_ "(\\b.c) ((\\d.e) d)"
  putStrLn (show (t2 `alphaEq` nor t1))
  let t3 = parseUnsafe_ "c"
  putStrLn (show (t3 `alphaEq` nor t2))
  --
  let t4 = parseUnsafe_ "(\\a.\\b.a) c ((\\d.e) d)"
  let t5 = parseUnsafe_ "(\\a.\\b.a) c e"
  putStrLn (show (t5 `alphaEq` aor t4))
  let t6 = parseUnsafe_ "(\\b.c) e"
  putStrLn (show (t6 `alphaEq` aor t5))
  putStrLn (show (t3 `alphaEq` aor t6))
  --
  let t7 = parseUnsafe_ "(\\x.a)((\\x.x x)(\\y.y y))"
  putStrLn (show (parseUnsafe_ "a" `alphaEq` nor t7))
  --
  let t8 = parseUnsafe_ "(\\x.a)((\\y.y y)(\\y.y y))"
  putStrLn (show (t8 `alphaEq` aor t7))
  --
  let t9 = parseUnsafe_ "((\\a.x) ((\\a.a a)(\\a.((\\b.a b) a))))"
  putStrLn (show (Var "x" `alphaEq` nor t9))
  --
  let t10 = parseUnsafe_ "(\\x.\\i0.y) c (\\z.(\\w.(\\b.(\\a.a) c) z) f)"
  let t11 = parseUnsafe_ "(\\x.y) (\\z.(\\w.(\\b.(\\a.a) c) z) f)"
  putStrLn (show (t11 `alphaEq` nor t10))
  putStrLn (show (Var "y" `alphaEq` nor t11))
  --
  let t12 = parseUnsafe_ "((\\a.x) ((\\a.a a) (\\a.a a)))"
  putStrLn (show (t12 `alphaEq` aor t9))
  putStrLn (show (t12 `alphaEq` aor (aor t9)))
  --
  let t13 = parseUnsafe_ "((\\x.\\x.y) c (\\z.(\\w.(\\b.(\\a.a) c) z) f))"
  let t14 = parseUnsafe_ "(\\x.\\i0.y) c (\\z.(\\b.(\\a.a) c) z)"
  putStrLn (show (t14 `alphaEq` aor t13))
  let t15 = parseUnsafe_ "(\\x.\\i0.y) c (\\z.(\\a.a) c)"
  putStrLn (show (t15 `alphaEq` aor t14))
  let t16 = parseUnsafe_ "(\\x.\\i0.y) c (\\z.c)"
  putStrLn (show (t16 `alphaEq` aor t15))
  let t17 = parseUnsafe_ "(\\x.y) (\\z.c)"
  putStrLn (show (t17 `alphaEq` aor t16))
  let t18 = parseUnsafe_ "y"
  putStrLn (show (t18 `alphaEq` aor t17))
  --

  -- Test repl expressions

  putStrLn (show (parseCmd "env"        == Right Env))
  putStrLn (show (parseCmd "env  "      == Right Env))
  putStrLn (show (isLeft (parseCmd "envxx")))
  putStrLn (show (isLeft (parseCmd "env mu")))
  putStrLn (show (isLeft (parseCmd "env   baz")))

  putStrLn (show (parseCmd "h "         == Right Help))
  putStrLn (show (parseCmd "h"          == Right Help))
  putStrLn (show (parseCmd "help  "     == Right Help))
  putStrLn (show (parseCmd "help"       == Right Help))
  putStrLn (show (isLeft (parseCmd "hp")))
  putStrLn (show (isLeft (parseCmd "helpo")))
  putStrLn (show (parseCmd "? "         == Right Help))
  putStrLn (show (parseCmd "?"          == Right Help))
  putStrLn (show (isLeft (parseCmd "?elp")))

  putStrLn (show (parseCmd "aq (\\x.x) Y" == Right (AlphaEq (Lam "x" (Var "x")) (Var "Y"))))
  putStrLn (show (parseCmd "aq X Y"     == Right (AlphaEq (Var "X") (Var "Y"))))
  putStrLn (show (isLeft (parseCmd "aqX Y")))
  putStrLn (show (parseCmd "aq X"       == Left "Usage is :aq <term> <term>"))
  putStrLn (show (parseCmd "aq"         == Left "Usage is :aq <term> <term>"))
  putStrLn (show (parseCmd "aq "        == Left "Usage is :aq <term> <term>"))
  putStrLn (show (parseCmd "aq (\\x.x)" == Left "Usage is :aq <term> <term>"))

  putStrLn (show (parseCmd "eq X Y"     == Right (Eq (Var "X") (Var "Y"))))
  putStrLn (show (isLeft (parseCmd "eqX Y")))
  putStrLn (show (parseCmd "eq X"       == Left "Usage is :eq <term> <term>"))

  putStrLn (show (parseCmd "reduce"     == Left "Usage is :reduce <term>"))
  putStrLn (show (parseCmd "reduce  "   == Left "Usage is :reduce <term>"))
  putStrLn (show (parseCmd "r"          == Left "Usage is :r <term>"))
  putStrLn (show (isLeft (parseCmd "reducex")))
  putStrLn (show (parseCmd "reduce X"   == Right (Reduce (Var "X"))))

  putStrLn (show (parseCmd "whatis"     == Left "Usage is :whatis <term>"))
  putStrLn (show (parseCmd "whatis  "   == Left "Usage is :whatis <term>"))
  putStrLn (show (parseCmd "w"          == Left "Usage is :w <term>"))
  putStrLn (show (isLeft (parseCmd "whatisx")))
  putStrLn (show (parseCmd "whatis X"     == Right (Whatis (Var "X"))))
  putStrLn (show (parseCmd "whatis (X Y)" == Right (Whatis (App (Var "X") (Var "Y")))))
  putStrLn (show (parseCmd "w (X Y)"      == Right (Whatis (App (Var "X") (Var "Y")))))

  putStrLn (show (parseCmd "unset "     == Left "Usage is :unset <symbol>"))
  putStrLn (show (parseCmd "unset"      == Left "Usage is :unset <symbol>"))
  putStrLn (show (parseCmd "unset  "    == Left "Usage is :unset <symbol>"))
  putStrLn (show (parseCmd "u "         == Left "Usage is :u <symbol>"))
  putStrLn (show (parseCmd "u"          == Left "Usage is :u <symbol>"))
  putStrLn (show (isLeft (parseCmd "uz")))
  putStrLn (show (isLeft (parseCmd "uns del")))
  putStrLn (show (isLeft (parseCmd "uns wat")))
  putStrLn (show (parseCmd "u baz"      == Right (Unset "baz")))
  putStrLn (show (parseCmd "unset baz"  == Right (Unset "baz")))
  putStrLn (show (parseCmd "unset fez_baz"
                                        == Right (Unset "fez_baz")))
  putStrLn (show (parseCmd "u fez_baz"  == Right (Unset "fez_baz")))

  putStrLn (show (parseCmd "limit 3"    == Right (Limit 3)))
  putStrLn (show (parseCmd "limit 300"  == Right (Limit 300)))
  putStrLn (show (parseCmd "limit"      == Left "Usage is :limit <number>"))
  putStrLn (show (parseCmd "limit "     == Left "Usage is :limit <number>"))
  putStrLn (show (parseCmd "limit foo"  == Left "Usage is :limit <number>"))
  putStrLn (show (parseCmd "limit 30x"  == Left "Usage is :limit <number>"))
  putStrLn (show (parseCmd "limit f3"   == Left "Usage is :limit <number>"))
  putStrLn (show (isLeft (parseCmd "limits")))

  putStrLn (show (parseCmd "q "         == Right Quit))
  putStrLn (show (parseCmd "q"          == Right Quit))
  putStrLn (show (parseCmd "quit "      == Right Quit))
  putStrLn (show (parseCmd "quit"       == Right Quit))
  putStrLn (show (isLeft (parseCmd "qu")))
  putStrLn (show (isLeft (parseCmd "quitquit")))

  putStrLn (show (isLeft (parseCmd "setup")))
  putStrLn (show (parseCmd "set"               == Left "Usage is :set <symbol> <term>"))
  putStrLn (show (parseCmd "set "              == Left "Usage is :set <symbol> <term>"))
  putStrLn (show (parseCmd "set baz"           == Left "Usage is :set <symbol> <term>"))
  putStrLn (show (parseCmd "set baz \\x.("     == Left "Usage is :set <symbol> <term>"))
  putStrLn (show (parseCmd "set foo foo"       == Right (Set "foo" (Var "foo"))))
  putStrLn (show (parseCmd "set id (\\x.x)"    == Right (Set "id" (Lam "x" (Var "x")))))
  putStrLn (show (parseCmd "set id    (\\x.x)" == Right (Set "id" (Lam "x" (Var "x")))))
  putStrLn (show (parseCmd "set x_x (A B)"     == Right (Set "x_x" (App (Var "A") (Var "B")))))
  putStrLn (show (parseCmd "set  why (\\g.(\\x.g (x x)) (\\x.g (x x)))"
                                               == Right (Set "why" (Lam "g" (App (Lam "x" (App (Var "g") (App (Var "x") (Var "x")))) (Lam "x" (App (Var "g") (App (Var "x") (Var "x")))))))))

max_stars_repo_name: laserpants/redex-reflex

max_issues_repo_name: laserpants/lambdapants

max_forks_repo_name: laserpants/lambdapants


text:
module Idris.Desugar

import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
import Core.Options
import Core.TT
import Core.Unify

import Data.Maybe

import Libraries.Data.List.Extra
import Libraries.Data.StringMap
import Libraries.Data.String.Extra
import Libraries.Data.ANameMap
import Libraries.Data.SortedMap

import Idris.Doc.String
import Idris.Syntax

import Idris.Elab.Implementation
import Idris.Elab.Interface

import Idris.Desugar.Mutual

import Parser.Lexer.Source

import TTImp.BindImplicits
import TTImp.Parser
import TTImp.TTImp
import TTImp.Utils

import Libraries.Data.IMaybe
import Libraries.Utils.Shunting

import Control.Monad.State
import Data.Maybe
import Data.List
import Data.List.Views
import Data.List1
import Data.String
import Libraries.Data.String.Extra

%hide Data.String.lines
%hide Data.String.lines'
%hide Data.String.unlines
%hide Data.String.unlines'

-- Convert high level Idris declarations (PDecl from Idris.Syntax) into
-- TTImp, recording any high level syntax info on the way (e.g. infix
-- operators)

-- Desugaring from high level Idris syntax to TTImp involves:

-- * Shunting infix operators into function applications according to precedence
-- * Replacing 'do' notating with applications of (>>=)
-- * Replacing string interpolation with concatenation by (++)
-- * Replacing pattern matching binds with 'case'
-- * Changing tuples to 'Pair/MkPair'
-- * List notation
-- * Replacing !-notation
-- * Dependent pair notation
-- * Idiom brackets

%default covering

public export
data Side = LHS | AnyExpr

export
Eq Side where
  LHS == LHS = True
  AnyExpr == AnyExpr = True
  _ == _ = False

export
extendSyn : {auto s : Ref Syn SyntaxInfo} ->
            {auto c : Ref Ctxt Defs} ->
            SyntaxInfo -> Core ()
extendSyn newsyn
    = do syn <- get Syn
         log "doc.module" 20 $ unlines
           [ "Old (" ++ unwords (map show $ saveMod syn) ++ "): "
              ++ show (modDocstrings syn)
           , "New (" ++ unwords (map show $ saveMod newsyn) ++ "): "
              ++ show (modDocstrings newsyn)
           ]
         put Syn (record { infixes $= mergeLeft (infixes newsyn),
                           prefixes $= mergeLeft (prefixes newsyn),
                           ifaces $= merge (ifaces newsyn),
                           modDocstrings $= mergeLeft (modDocstrings newsyn),
                           defDocstrings $= merge (defDocstrings newsyn),
                           bracketholes $= ((bracketholes newsyn) ++) }
                  syn)

mkPrec : Fixity -> Nat -> OpPrec
mkPrec InfixL p = AssocL p
mkPrec InfixR p = AssocR p
mkPrec Infix p = NonAssoc p
mkPrec Prefix p = Prefix p

toTokList : {auto s : Ref Syn SyntaxInfo} ->
            PTerm -> Core (List (Tok OpStr PTerm))
toTokList (POp fc opFC opn l r)
    = do syn <- get Syn
         let op = nameRoot opn
         case lookup op (infixes syn) of
              Nothing =>
                  if any isOpChar (fastUnpack op)
                     then throw (GenericMsg fc $ "Unknown operator '" ++ op ++ "'")
                     else do rtoks <- toTokList r
                             pure (Expr l :: Op fc opFC opn backtickPrec :: rtoks)
              Just (Prefix, _) =>
                      throw (GenericMsg fc $ "'" ++ op ++ "' is a prefix operator")
              Just (fix, prec) =>
                   do rtoks <- toTokList r
                      pure (Expr l :: Op fc opFC opn (mkPrec fix prec) :: rtoks)
  where
    backtickPrec : OpPrec
    backtickPrec = NonAssoc 1
toTokList (PPrefixOp fc opFC opn arg)
    = do syn <- get Syn
         let op = nameRoot opn
         case lookup op (prefixes syn) of
              Nothing =>
                   throw (GenericMsg fc $ "'" ++ op ++ "' is not a prefix operator")
              Just prec =>
                   do rtoks <- toTokList arg
                      pure (Op fc opFC opn (Prefix prec) :: rtoks)
toTokList t = pure [Expr t]

record BangData where
  constructor MkBangData
  nextName : Int
  bangNames : List (Name, FC, RawImp)
  mbNamespace : Maybe Namespace

initBangs : Maybe Namespace -> BangData
initBangs = MkBangData 0 []

addNS : Maybe Namespace -> Name -> Name
addNS (Just ns) n@(NS _ _) = n
addNS (Just ns) n = NS ns n
addNS _ n = n

bindFun : FC -> Maybe Namespace -> RawImp -> RawImp -> RawImp
bindFun fc ns ma f =
  let fc = virtualiseFC fc in
  IApp fc (IApp fc (IVar fc (addNS ns $ UN $ Basic ">>=")) ma) f

seqFun : FC -> Maybe Namespace -> RawImp -> RawImp -> RawImp
seqFun fc ns ma mb =
  let fc = virtualiseFC fc in
  IApp fc (IApp fc (IVar fc (addNS ns (UN $ Basic ">>"))) ma) mb

bindBangs : List (Name, FC, RawImp) -> Maybe Namespace -> RawImp -> RawImp
bindBangs [] ns tm = tm
bindBangs ((n, fc, btm) :: bs) ns tm
    = bindBangs bs ns
    $ bindFun fc ns btm
    $ ILam EmptyFC top Explicit (Just n) (Implicit fc False) tm

idiomise : FC -> RawImp -> RawImp
idiomise fc (IAlternative afc u alts)
  = IAlternative afc (mapAltType (idiomise afc) u) (idiomise afc <$> alts)
idiomise fc (IApp afc f a)
    = let fc = virtualiseFC fc in
      IApp fc (IApp fc (IVar fc (UN $ Basic "<*>"))
                       (idiomise afc f))
              a
idiomise fc fn
  = let fc = virtualiseFC fc in
    IApp fc (IVar fc (UN $ Basic "pure")) fn

pairname : Name
pairname = NS builtinNS (UN $ Basic "Pair")

mkpairname : Name
mkpairname = NS builtinNS (UN $ Basic "MkPair")

dpairname : Name
dpairname = NS dpairNS (UN $ Basic "DPair")

mkdpairname : Name
mkdpairname = NS dpairNS (UN $ Basic "MkDPair")

data Bang : Type where

mutual
  desugarB : {auto s : Ref Syn SyntaxInfo} ->
             {auto b : Ref Bang BangData} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             Side -> List Name -> PTerm -> Core RawImp
  desugarB side ps (PRef fc x) = pure $ IVar fc x
  desugarB side ps (PPi fc rig p mn argTy retTy)
      = let ps' = maybe ps (:: ps) mn in
            pure $ IPi fc rig !(traverse (desugar side ps') p)
                              mn !(desugarB side ps argTy)
                                 !(desugarB side ps' retTy)
  desugarB side ps (PLam fc rig p pat@(PRef prefFC n@(UN nm)) argTy scope)
      =  if isPatternVariable nm
           then do whenJust (isConcreteFC prefFC) $ \nfc
                     => addSemanticDecorations [(nfc, Bound, Just n)]
                   pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
                           (Just n) !(desugarB AnyExpr ps argTy)
                                    !(desugar AnyExpr (n :: ps) scope)
           else pure $ ILam EmptyFC rig !(traverse (desugar AnyExpr ps) p)
                   (Just (MN "lamc" 0)) !(desugarB AnyExpr ps argTy) $
                 ICase fc (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False)
                     [snd !(desugarClause ps True (MkPatClause fc pat scope []))]
  desugarB side ps (PLam fc rig p (PRef _ n@(MN _ _)) argTy scope)
      = pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
                           (Just n) !(desugarB AnyExpr ps argTy)
                                    !(desugar AnyExpr (n :: ps) scope)
  desugarB side ps (PLam fc rig p (PImplicit _) argTy scope)
      = pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
                           Nothing !(desugarB AnyExpr ps argTy)
                                   !(desugar AnyExpr ps scope)
  desugarB side ps (PLam fc rig p pat argTy scope)
      = pure $ ILam EmptyFC rig !(traverse (desugar AnyExpr ps) p)
                   (Just (MN "lamc" 0)) !(desugarB AnyExpr ps argTy) $
                 ICase fc (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False)
                     [snd !(desugarClause ps True (MkPatClause fc pat scope []))]
  desugarB side ps (PLet fc rig (PRef prefFC n) nTy nVal scope [])
      = do whenJust (isConcreteFC prefFC) $ \nfc =>
             addSemanticDecorations [(nfc, Bound, Just n)]
           pure $ ILet fc prefFC rig n !(desugarB side ps nTy) !(desugarB side ps nVal)
                                       !(desugar side (n :: ps) scope)
  desugarB side ps (PLet fc rig pat nTy nVal scope alts)
      = pure $ ICase fc !(desugarB side ps nVal) !(desugarB side ps nTy)
                        !(traverse (map snd . desugarClause ps True)
                            (MkPatClause fc pat scope [] :: alts))
  desugarB side ps (PCase fc x xs)
      = pure $ ICase fc !(desugarB side ps x)
                        (Implicit (virtualiseFC fc) False)
                        !(traverse (map snd . desugarClause ps True) xs)
  desugarB side ps (PLocal fc xs scope)
      = let ps' = definedIn xs ++ ps in
            pure $ ILocal fc (concat !(traverse (desugarDecl ps') xs))
                             !(desugar side ps' scope)
  desugarB side ps (PApp pfc (PUpdate fc fs) rec)
      = pure $ IUpdate pfc !(traverse (desugarUpdate side ps) fs)
                           !(desugarB side ps rec)
  desugarB side ps (PUpdate fc fs)
      = desugarB side ps
      $ let vfc = virtualiseFC fc in
      PLam vfc top Explicit (PRef vfc (MN "rec" 0)) (PImplicit vfc)
      $ PApp vfc (PUpdate fc fs) (PRef vfc (MN "rec" 0))
  desugarB side ps (PApp fc x y)
      = pure $ IApp fc !(desugarB side ps x) !(desugarB side ps y)
  desugarB side ps (PAutoApp fc x y)
      = pure $ IAutoApp fc !(desugarB side ps x) !(desugarB side ps y)
  desugarB side ps (PWithApp fc x y)
      = pure $ IWithApp fc !(desugarB side ps x) !(desugarB side ps y)
  desugarB side ps (PNamedApp fc x argn y)
      = pure $ INamedApp fc !(desugarB side ps x) argn !(desugarB side ps y)
  desugarB side ps (PDelayed fc r ty)
      = pure $ IDelayed fc r !(desugarB side ps ty)
  desugarB side ps (PDelay fc tm)
      = pure $ IDelay fc !(desugarB side ps tm)
  desugarB side ps (PForce fc tm)
      = pure $ IForce fc !(desugarB side ps tm)
  desugarB side ps (PEq fc l r)
      = do l' <- desugarB side ps l
           r' <- desugarB side ps r
           pure $ IAlternative fc FirstSuccess
                     [apply (IVar fc (UN $ Basic "===")) [l', r'],
                      apply (IVar fc (UN $ Basic "~=~")) [l', r']]
  desugarB side ps (PBracketed fc e) = desugarB side ps e
  desugarB side ps (POp fc opFC op l r)
      = do ts <- toTokList (POp fc opFC op l r)
           desugarTree side ps !(parseOps ts)
  desugarB side ps (PPrefixOp fc opFC op arg)
      = do ts <- toTokList (PPrefixOp fc opFC op arg)
           desugarTree side ps !(parseOps ts)
  desugarB side ps (PSectionL fc opFC op arg)
      = do syn <- get Syn
           -- It might actually be a prefix argument rather than a section
           -- so check that first, otherwise desugar as a lambda
           case lookup (nameRoot op) (prefixes syn) of
                Nothing =>
                   desugarB side ps (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
                               (POp fc opFC op (PRef fc (MN "arg" 0)) arg))
                Just prec => desugarB side ps (PPrefixOp fc opFC op arg)
  desugarB side ps (PSectionR fc opFC arg op)
      = desugarB side ps (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
                 (POp fc opFC op arg (PRef fc (MN "arg" 0))))
  desugarB side ps (PSearch fc depth) = pure $ ISearch fc depth
  desugarB side ps (PPrimVal fc (BI x))
      = case !fromIntegerName of
             Nothing =>
                pure $ IAlternative fc (UniqueDefault (IPrimVal fc (BI x)))
                                [IPrimVal fc (BI x),
                                 IPrimVal fc (I (fromInteger x))]
             Just fi =>
               let vfc = virtualiseFC fc in
               pure $ IApp vfc (IVar vfc fi) (IPrimVal fc (BI x))
  desugarB side ps (PPrimVal fc (Ch x))
      = case !fromCharName of
             Nothing =>
                pure $ IPrimVal fc (Ch x)
             Just f =>
               let vfc = virtualiseFC fc in
               pure $ IApp vfc (IVar vfc f) (IPrimVal fc (Ch x))
  desugarB side ps (PPrimVal fc (Db x))
      = case !fromDoubleName of
             Nothing =>
                pure $ IPrimVal fc (Db x)
             Just f =>
               let vfc = virtualiseFC fc in
               pure $ IApp vfc (IVar vfc f) (IPrimVal fc (Db x))
  desugarB side ps (PPrimVal fc x) = pure $ IPrimVal fc x
  desugarB side ps (PQuote fc tm)
      = pure $ IQuote fc !(desugarB side ps tm)
  desugarB side ps (PQuoteName fc n)
      = pure $ IQuoteName fc n
  desugarB side ps (PQuoteDecl fc x)
      = do xs <- traverse (desugarDecl ps) x
           pure $ IQuoteDecl fc (concat xs)
  desugarB side ps (PUnquote fc tm)
      = pure $ IUnquote fc !(desugarB side ps tm)
  desugarB side ps (PRunElab fc tm)
      = pure $ IRunElab fc !(desugarB side ps tm)
  desugarB side ps (PHole fc br holename)
      = do when br $
              do syn <- get Syn
                 put Syn (record { bracketholes $= ((UN (Basic holename)) ::) } syn)
           pure $ IHole fc holename
  desugarB side ps (PType fc) = pure $ IType fc
  desugarB side ps (PAs fc nameFC vname pattern)
      = pure $ IAs fc nameFC UseRight vname !(desugarB side ps pattern)
  desugarB side ps (PDotted fc x)
      = pure $ IMustUnify fc UserDotted !(desugarB side ps x)
  desugarB side ps (PImplicit fc) = pure $ Implicit fc True
  desugarB side ps (PInfer fc)
    = do when (side == LHS) $
           throw (GenericMsg fc "? is not a valid pattern")
         pure $ Implicit fc False
  desugarB side ps (PMultiline fc indent lines)
      = addFromString fc !(expandString side ps fc !(trimMultiline fc indent lines))

  -- We only add `fromString` if we are looking at a plain string literal.
  -- Interpolated string literals don't have a `fromString` call since they
  -- are always concatenated with other strings and therefore can never use
  -- another `fromString` implementation that differs from `id`.
  desugarB side ps (PString fc [])
      = addFromString fc (IPrimVal fc (Str ""))
  desugarB side ps (PString fc [StrLiteral fc' str])
      = addFromString fc (IPrimVal fc' (Str str))
  desugarB side ps (PString fc strs)
      = expandString side ps fc strs

  desugarB side ps (PDoBlock fc ns block)
      = expandDo side ps fc ns block
  desugarB side ps (PBang fc term)
      = do itm <- desugarB side ps term
           bs <- get Bang
           let bn = MN "bind" (nextName bs)
           put Bang (record { nextName $= (+1),
                              bangNames $= ((bn, fc, itm) ::)
                            } bs)
           pure (IVar EmptyFC bn)
  desugarB side ps (PIdiom fc term)
      = do itm <- desugarB side ps term
           logRaw "desugar.idiom" 10 "Desugaring idiom for" itm
           let val = idiomise fc itm
           logRaw "desugar.idiom" 10 "Desugared to" val
           pure val
  desugarB side ps (PList fc nilFC args)
      = expandList side ps nilFC args
  desugarB side ps (PSnocList fc nilFC args)
      = expandSnocList side ps nilFC (reverse args)
  desugarB side ps (PPair fc l r)
      = do l' <- desugarB side ps l
           r' <- desugarB side ps r
           let pval = apply (IVar fc mkpairname) [l', r']
           pure $ IAlternative fc (UniqueDefault pval)
                  [apply (IVar fc pairname) [l', r'], pval]
  desugarB side ps (PDPair fc opFC (PRef nameFC n@(UN _)) (PImplicit _) r)
      = do r' <- desugarB side ps r
           let pval = apply (IVar opFC mkdpairname) [IVar nameFC n, r']
           let vfc = virtualiseFC nameFC
           whenJust (isConcreteFC nameFC) $ \nfc =>
             addSemanticDefault (nfc, Bound, Just n)
           pure $ IAlternative fc (UniqueDefault pval)
                  [apply (IVar opFC dpairname)
                      [Implicit vfc False,
                       ILam nameFC top Explicit (Just n) (Implicit vfc False) r'],
                   pval]
  desugarB side ps (PDPair fc opFC (PRef namefc n@(UN _)) ty r)
      = do ty' <- desugarB side ps ty
           r' <- desugarB side ps r
           pure $ apply (IVar opFC dpairname)
                        [ty', ILam namefc top Explicit (Just n) ty' r']
  desugarB side ps (PDPair fc opFC l (PImplicit _) r)
      = do l' <- desugarB side ps l
           r' <- desugarB side ps r
           pure $ apply (IVar opFC mkdpairname) [l', r']
  desugarB side ps (PDPair fc opFC l ty r)
      = throw (GenericMsg fc "Invalid dependent pair type")
  desugarB side ps (PUnit fc)
      = pure $ IAlternative fc (UniqueDefault (IVar fc (UN $ Basic "MkUnit")))
               [IVar fc (UN $ Basic "Unit"),
                IVar fc (UN $ Basic "MkUnit")]
  desugarB side ps (PIfThenElse fc x t e)
      = let fc = virtualiseFC fc in
        pure $ ICase fc !(desugarB side ps x) (IVar fc (UN $ Basic "Bool"))
                   [PatClause fc (IVar fc (UN $ Basic "True")) !(desugar side ps t),
                    PatClause fc (IVar fc (UN $ Basic "False")) !(desugar side ps e)]
  desugarB side ps (PComprehension fc ret conds) = do
        let ns = mbNamespace !(get Bang)
        desugarB side ps (PDoBlock fc ns (map (guard ns) conds ++ [toPure ns ret]))
    where
      guard : Maybe Namespace -> PDo -> PDo
      guard ns (DoExp fc tm)
       = DoExp fc (PApp fc (PRef fc (mbApplyNS ns $ UN $ Basic "guard")) tm)
      guard ns d = d

      toPure : Maybe Namespace -> PTerm -> PDo
      toPure ns tm = DoExp fc (PApp fc (PRef fc (mbApplyNS ns $ UN $ Basic "pure")) tm)
  desugarB side ps (PRewrite fc rule tm)
      = pure $ IRewrite fc !(desugarB side ps rule) !(desugarB side ps tm)
  desugarB side ps (PRange fc start next end)
      = let fc = virtualiseFC fc in
        desugarB side ps $ case next of
           Nothing => papply fc (PRef fc (UN $ Basic "rangeFromTo")) [start,end]
           Just n  => papply fc (PRef fc (UN $ Basic "rangeFromThenTo")) [start, n, end]
  desugarB side ps (PRangeStream fc start next)
      = let fc = virtualiseFC fc in
        desugarB side ps $ case next of
           Nothing => papply fc (PRef fc (UN $ Basic "rangeFrom")) [start]
           Just n  => papply fc (PRef fc (UN $ Basic "rangeFromThen")) [start, n]
  desugarB side ps (PUnifyLog fc lvl tm)
      = pure $ IUnifyLog fc lvl !(desugarB side ps tm)
  desugarB side ps (PPostfixApp fc rec projs)
      = desugarB side ps
      $ foldl (\x, (fc, proj) => PApp fc (PRef fc proj) x) rec projs
  desugarB side ps (PPostfixAppPartial fc projs)
      = do let vfc = virtualiseFC fc
           let var = PRef vfc (MN "paRoot" 0)
           desugarB side ps $
             PLam fc top Explicit var (PImplicit vfc) $
               foldl (\r, (fc, proj) => PApp fc (PRef fc proj) r) var projs
  desugarB side ps (PWithUnambigNames fc ns rhs)
      = IWithUnambigNames fc ns <$> desugarB side ps rhs

  desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
                  {auto b : Ref Bang BangData} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto u : Ref UST UState} ->
                  {auto m : Ref MD Metadata} ->
                  Side -> List Name -> PFieldUpdate -> Core IFieldUpdate
  desugarUpdate side ps (PSetField p v)
      = pure (ISetField p !(desugarB side ps v))
  desugarUpdate side ps (PSetFieldApp p v)
      = pure (ISetFieldApp p !(desugarB side ps v))

  expandList : {auto s : Ref Syn SyntaxInfo} ->
               {auto b : Ref Bang BangData} ->
               {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto m : Ref MD Metadata} ->
               Side -> List Name ->
               (nilFC : FC) -> List (FC, PTerm) -> Core RawImp
  expandList side ps nilFC [] = pure (IVar nilFC (UN $ Basic "Nil"))
  expandList side ps nilFC ((consFC, x) :: xs)
      = pure $ apply (IVar consFC (UN $ Basic "::"))
                [!(desugarB side ps x), !(expandList side ps nilFC xs)]

  expandSnocList
             : {auto s : Ref Syn SyntaxInfo} ->
               {auto b : Ref Bang BangData} ->
               {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto m : Ref MD Metadata} ->
               Side -> List Name -> (nilFC : FC) -> List (FC, PTerm) -> Core RawImp
  expandSnocList side ps nilFC [] = pure (IVar nilFC (UN $ Basic "Lin"))
  expandSnocList side ps nilFC ((consFC, x) :: xs)
      = pure $ apply (IVar consFC (UN $ Basic ":<"))
                [!(expandSnocList side ps nilFC xs) , !(desugarB side ps x)]

  addFromString : {auto c : Ref Ctxt Defs} ->
                  FC -> RawImp -> Core RawImp
  addFromString fc tm
      = pure $ case !fromStringName of
                    Nothing => tm
                    Just f =>
                      let fc = virtualiseFC fc in
                      IApp fc (IVar fc f) tm

  expandString : {auto s : Ref Syn SyntaxInfo} ->
                 {auto b : Ref Bang BangData} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 Side -> List Name -> FC -> List PStr -> Core RawImp
  expandString side ps fc xs
    = do xs <- traverse toRawImp (filter notEmpty $ mergeStrLit xs)
         pure $ case xs of
           [] => IPrimVal fc (Str "")
           (_ :: _) => foldr1 concatStr xs
    where
      toRawImp : PStr -> Core RawImp
      toRawImp (StrLiteral fc str) = pure $ IPrimVal fc (Str str)
      toRawImp (StrInterp fc tm) = desugarB side ps tm

      -- merge neighbouring StrLiteral
      mergeStrLit : List PStr -> List PStr
      mergeStrLit xs
          = case List.spanBy (\case StrLiteral fc str => Just (fc, str); _ => Nothing) xs of
                 ([], []) => []
                 ([], x::xs) => x :: mergeStrLit xs
                 (lits@(_::_), xs) => (StrLiteral (fst $ head lits) (fastConcat $ snd <$> lits)) :: mergeStrLit xs

      notEmpty : PStr -> Bool
      notEmpty (StrLiteral _ str) = str /= ""
      notEmpty (StrInterp _ _) = True

      concatStr : RawImp -> RawImp -> RawImp
      concatStr a b =
        let aFC = virtualiseFC (getFC a)
            bFC = virtualiseFC (getFC b)
        in IApp aFC (IApp bFC (IVar bFC (UN $ Basic "++")) a) b

  trimMultiline : FC -> Nat -> List (List PStr) -> Core (List PStr)
  trimMultiline fc indent lines
      = if indent == 0
           then pure $ dropLastNL $ concat lines
           else do
             lines <- trimLast fc lines
             lines <- traverse (trimLeft indent) lines
             pure $ dropLastNL $ concat lines
    where
      trimLast : FC -> List (List PStr) -> Core (List (List PStr))
      trimLast fc lines with (snocList lines)
        trimLast fc [] | Empty = throw $ BadMultiline fc "Expected line wrap"
        trimLast _ (initLines `snoc` []) | Snoc [] initLines _ = pure lines
        trimLast _ (initLines `snoc` [StrLiteral fc str]) | Snoc [(StrLiteral _ _)] initLines _
            = if any (not . isSpace) (fastUnpack str)
                     then throw $ BadMultiline fc "Closing delimiter of multiline strings cannot be preceded by non-whitespace characters"
                     else pure initLines
        trimLast _ (initLines `snoc` xs) | Snoc xs initLines _
            = let fc = fromMaybe fc $ findBy isStrInterp xs in
                  throw $ BadMultiline fc "Closing delimiter of multiline strings cannot be preceded by non-whitespace characters"

      dropLastNL : List PStr -> List PStr
      dropLastNL pstrs with (snocList pstrs)
        dropLastNL [] | Empty = []
        dropLastNL (initLines `snoc` (StrLiteral fc str)) | Snoc (StrLiteral _ _) initLines _
            = initLines `snoc` (StrLiteral fc (fst $ break isNL str))
        dropLastNL pstrs | _ = pstrs

      trimLeft : Nat -> List PStr -> Core (List PStr)
      trimLeft indent [] = pure []
      trimLeft indent [(StrLiteral fc str)]
          = let (trimed, rest) = splitAt indent (fastUnpack str) in
                if any (not . isSpace) trimed
                   then throw $ BadMultiline fc "Line is less indented than the closing delimiter"
                   else pure $ [StrLiteral fc (fastPack rest)]
      trimLeft indent ((StrLiteral fc str)::xs)
          = let (trimed, rest) = splitAt indent (fastUnpack str) in
                if any (not . isSpace) trimed || length trimed < indent
                   then throw $ BadMultiline fc "Line is less indented than the closing delimiter"
                   else pure $ (StrLiteral fc (fastPack rest))::xs
      trimLeft indent xs = throw $ BadMultiline fc "Line is less indented than the closing delimiter"

  expandDo : {auto s : Ref Syn SyntaxInfo} ->
             {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto m : Ref MD Metadata} ->
             Side -> List Name -> FC -> Maybe Namespace -> List PDo -> Core RawImp
  expandDo side ps fc ns [] = throw (GenericMsg fc "Do block cannot be empty")
  expandDo side ps _ ns [DoExp fc tm] = desugarDo side ps ns tm
  expandDo side ps fc ns [e]
      = throw (GenericMsg (getLoc e)
                  "Last statement in do block must be an expression")
  expandDo side ps topfc ns (DoExp fc tm :: rest)
      = do tm' <- desugarDo side ps ns tm
           rest' <- expandDo side ps topfc ns rest
           gam <- get Ctxt
           pure $ seqFun fc ns tm' rest'
  expandDo side ps topfc ns (DoBind fc nameFC n tm :: rest)
      = do tm' <- desugarDo side ps ns tm
           rest' <- expandDo side ps topfc ns rest
           whenJust (isConcreteFC nameFC) $ \nfc => addSemanticDecorations [(nfc, Bound, Just n)]
           pure $ bindFun fc ns tm'
                $ ILam nameFC top Explicit (Just n)
                       (Implicit (virtualiseFC fc) False) rest'
  expandDo side ps topfc ns (DoBindPat fc pat exp alts :: rest)
      = do pat' <- desugarDo LHS ps ns pat
           (newps, bpat) <- bindNames False pat'
           exp' <- desugarDo side ps ns exp
           alts' <- traverse (map snd . desugarClause ps True) alts
           let ps' = newps ++ ps
           rest' <- expandDo side ps' topfc ns rest
           let fcOriginal = fc
           let fc = virtualiseFC fc
           pure $ bindFun fc ns exp'
                $ ILam EmptyFC top Explicit (Just (MN "_" 0))
                          (Implicit fc False)
                          (ICase fc (IVar EmptyFC (MN "_" 0))
                               (Implicit fc False)
                               (PatClause fcOriginal bpat rest'
                                  :: alts'))
  expandDo side ps topfc ns (DoLet fc lhsFC n rig ty tm :: rest)
      = do b <- newRef Bang (initBangs ns)
           tm' <- desugarB side ps tm
           ty' <- desugarDo side ps ns ty
           rest' <- expandDo side ps topfc ns rest
           whenJust (isConcreteFC lhsFC) $ \nfc => addSemanticDecorations [(nfc, Bound, Just n)]
           let bind = ILet fc (virtualiseFC lhsFC) rig n ty' tm' rest'
           bd <- get Bang
           pure $ bindBangs (bangNames bd) ns bind
  expandDo side ps topfc ns (DoLetPat fc pat ty tm alts :: rest)
      = do b <- newRef Bang (initBangs ns)
           pat' <- desugarDo LHS ps ns pat
           ty' <- desugarDo side ps ns ty
           (newps, bpat) <- bindNames False pat'
           tm' <- desugarB side ps tm
           alts' <- traverse (map snd . desugarClause ps True) alts
           let ps' = newps ++ ps
           rest' <- expandDo side ps' topfc ns rest
           bd <- get Bang
           let fc = virtualiseFC fc
           pure $ bindBangs (bangNames bd) ns $
                    ICase fc tm' ty'
                       (PatClause fc bpat rest'
                                  :: alts')
  expandDo side ps topfc ns (DoLetLocal fc decls :: rest)
      = do rest' <- expandDo side ps topfc ns rest
           decls' <- traverse (desugarDecl ps) decls
           pure $ ILocal fc (concat decls') rest'
  expandDo side ps topfc ns (DoRewrite fc rule :: rest)
      = do rest' <- expandDo side ps topfc ns rest
           rule' <- desugarDo side ps ns rule
           pure $ IRewrite fc rule' rest'

  desugarTree : {auto s : Ref Syn SyntaxInfo} ->
                {auto b : Ref Bang BangData} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {auto m : Ref MD Metadata} ->
                Side -> List Name -> Tree OpStr PTerm -> Core RawImp
  desugarTree side ps (Infix loc eqFC (UN $ Basic "=") l r) -- special case since '=' is special syntax
      = do l' <- desugarTree side ps l
           r' <- desugarTree side ps r
           pure (IAlternative loc FirstSuccess
                     [apply (IVar eqFC (UN $ Basic "===")) [l', r'],
                      apply (IVar eqFC (UN $ Basic "~=~")) [l', r']])
  desugarTree side ps (Infix loc _ (UN $ Basic "$") l r) -- special case since '$' is special syntax
      = do l' <- desugarTree side ps l
           r' <- desugarTree side ps r
           pure (IApp loc l' r')
  desugarTree side ps (Infix loc opFC op l r)
      = do l' <- desugarTree side ps l
           r' <- desugarTree side ps r
           pure (IApp loc (IApp loc (IVar opFC op) l') r')

  -- negation is a special case, since we can't have an operator with
  -- two meanings otherwise
  --
  -- Note: In case of negated signed integer literals, we apply the
  -- negation directly. Otherwise, the literal might be
  -- truncated to 0 before being passed on to `negate`.
  desugarTree side ps (Pre loc opFC (UN $ Basic "-") $ Leaf $ PPrimVal fc c)
    = let newFC    = fromMaybe EmptyFC (mergeFC loc fc)
          continue = desugarTree side ps . Leaf . PPrimVal newFC
       in case c of
            I   x => continue $ I (-x)
            I8  x => continue $ I8 (-x)
            I16 x => continue $ I16 (-x)
            I32 x => continue $ I32 (-x)
            I64 x => continue $ I64 (-x)
            BI  x => continue $ BI (-x)

            -- not a signed integer literal. proceed by desugaring
            -- and applying to `negate`.
            _     => do arg' <- desugarTree side ps (Leaf $ PPrimVal fc c)
                        pure (IApp loc (IVar opFC (UN $ Basic "negate")) arg')

  desugarTree side ps (Pre loc opFC (UN $ Basic "-") arg)
    = do arg' <- desugarTree side ps arg
         pure (IApp loc (IVar opFC (UN $ Basic "negate")) arg')

  desugarTree side ps (Pre loc opFC op arg)
      = do arg' <- desugarTree side ps arg
           pure (IApp loc (IVar opFC op) arg')
  desugarTree side ps (Leaf t) = desugarB side ps t

  desugarType : {auto s : Ref Syn SyntaxInfo} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {auto m : Ref MD Metadata} ->
                List Name -> PTypeDecl -> Core ImpTy
  desugarType ps (MkPTy fc nameFC n d ty)
      = do addDocString n d
           syn <- get Syn
           pure $ MkImpTy fc nameFC n !(bindTypeNames fc (usingImpl syn)
                                               ps !(desugar AnyExpr ps ty))

  -- Attempt to get the function name from a function pattern. For example,
  --   - given the pattern 'f x y', getClauseFn would return 'f'.
  --   - given the pattern 'x == y', getClausefn would return '=='.
  getClauseFn : RawImp -> Core Name
  getClauseFn (IVar _ n) = pure n
  getClauseFn (IApp _ f _) = getClauseFn f
  getClauseFn (IAutoApp _ f _) = getClauseFn f
  getClauseFn (INamedApp _ f _ _) = getClauseFn f
  getClauseFn tm = throw $ GenericMsg (getFC tm) "Head term in pattern must be a function name"

  desugarLHS : {auto s : Ref Syn SyntaxInfo} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               List Name -> (arg : Bool) -> PTerm ->
               Core (IMaybe (not arg) Name, List Name, RawImp)
                  -- ^ we only look for the head name of the expression...
                  --   if we are actually looking at a headed thing!
  desugarLHS ps arg lhs =
    do rawlhs <- desugar LHS ps lhs
       inm <- iunless arg $ getClauseFn rawlhs
       (bound, blhs) <- bindNames arg rawlhs
       iwhenJust inm $ \ nm =>
         when (nm `elem` bound) $ do
           let fc = getPTermLoc lhs
           throw $ GenericMsg fc $ concat $ the (List String)
             [ "Declaration name ("
             , show nm
             , ") shadowed by a pattern variable."
             ]

       pure (inm, bound, blhs)

  desugarClause : {auto s : Ref Syn SyntaxInfo} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto u : Ref UST UState} ->
                  {auto m : Ref MD Metadata} ->
                  List Name -> (arg : Bool) -> PClause ->
                  Core (IMaybe (not arg) Name, ImpClause)
  desugarClause ps arg (MkPatClause fc lhs rhs wheres)
      = do ws <- traverse (desugarDecl ps) wheres

           (nm, bound, lhs') <- desugarLHS ps arg lhs

           -- desugar rhs, putting where clauses as local definitions
           rhs' <- desugar AnyExpr (bound ++ ps) rhs
           let rhs' = case ws of
                        [] => rhs'
                        _ => ILocal fc (concat ws) rhs'

           pure (nm, PatClause fc lhs' rhs')

  desugarClause ps arg (MkWithClause fc lhs wval prf flags cs)
      = do cs' <- traverse (map snd . desugarClause ps arg) cs
           (nm, bound, lhs') <- desugarLHS ps arg lhs
           wval' <- desugar AnyExpr (bound ++ ps) wval
           pure (nm, WithClause fc lhs' wval' prf flags cs')

  desugarClause ps arg (MkImpossible fc lhs)
      = do (nm, _, lhs') <- desugarLHS ps arg lhs
           pure (nm, ImpossibleClause fc lhs')

  desugarData : {auto s : Ref Syn SyntaxInfo} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {auto m : Ref MD Metadata} ->
                List Name -> (doc : String) ->
                PDataDecl -> Core ImpData
  desugarData ps doc (MkPData fc n tycon opts datacons)
      = do addDocString n doc
           syn <- get Syn
           pure $ MkImpData fc n
                              !(bindTypeNames fc (usingImpl syn)
                                              ps !(desugar AnyExpr ps tycon))
                              opts
                              !(traverse (desugarType ps) datacons)
  desugarData ps doc (MkPLater fc n tycon)
      = do addDocString n doc
           syn <- get Syn
           pure $ MkImpLater fc n !(bindTypeNames fc (usingImpl syn)
                                                  ps !(desugar AnyExpr ps tycon))

  desugarField : {auto s : Ref Syn SyntaxInfo} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 {auto m : Ref MD Metadata} ->
                 List Name -> Namespace -> PField ->
                 Core IField
  desugarField ps ns (MkField fc doc rig p n ty)
      = do addDocStringNS ns n doc
           addDocStringNS ns (toRF n) doc
           syn <- get Syn
           pure (MkIField fc rig !(traverse (desugar AnyExpr ps) p )
                          n !(bindTypeNames fc (usingImpl syn)
                          ps !(desugar AnyExpr ps ty)))
        where
          toRF : Name -> Name
          toRF (UN (Basic n)) = UN (Field n)
          toRF n = n

  export
  desugarFnOpt : {auto s : Ref Syn SyntaxInfo} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 {auto m : Ref MD Metadata} ->
                 List Name -> PFnOpt -> Core FnOpt
  desugarFnOpt ps (IFnOpt f) = pure f
  desugarFnOpt ps (PForeign tms)
      = do tms' <- traverse (desugar AnyExpr ps) tms
           pure (ForeignFn tms')

  -- Given a high level declaration, return a list of TTImp declarations
  -- which process it, and update any necessary state on the way.
  export
  desugarDecl : {auto s : Ref Syn SyntaxInfo} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {auto m : Ref MD Metadata} ->
                List Name -> PDecl -> Core (List ImpDecl)
  desugarDecl ps (PClaim fc rig vis fnopts ty)
      = do opts <- traverse (desugarFnOpt ps) fnopts
           pure [IClaim fc rig vis opts !(desugarType ps ty)]
        where
          isTotalityOption : FnOpt -> Bool
          isTotalityOption (Totality _) = True
          isTotalityOption _            = False

  desugarDecl ps (PDef fc clauses)
  -- The clauses won't necessarily all be from the same function, so split
  -- after desugaring, by function name, using collectDefs from RawImp
      = do ncs <- traverse (desugarClause ps False) clauses
           defs <- traverse (uncurry $ toIDef . fromJust) ncs
           pure (collectDefs defs)
    where
      toIDef : Name -> ImpClause -> Core ImpDecl
      toIDef nm (PatClause fc lhs rhs)
          = pure $ IDef fc nm [PatClause fc lhs rhs]
      toIDef nm (WithClause fc lhs rhs prf flags cs)
          = pure $ IDef fc nm [WithClause fc lhs rhs prf flags cs]
      toIDef nm (ImpossibleClause fc lhs)
          = pure $ IDef fc nm [ImpossibleClause fc lhs]

  desugarDecl ps (PData fc doc vis ddecl)
      = pure [IData fc vis !(desugarData ps doc ddecl)]
  desugarDecl ps (PParameters fc params pds)
      = do pds' <- traverse (desugarDecl (ps ++ map fst params)) pds
           params' <- traverse (\(n, rig, i, ntm) => do tm' <- desugar AnyExpr ps ntm
                                                        i' <- traverse (desugar AnyExpr ps) i
                                                        pure (n, rig, i', tm')) params
           -- Look for implicitly bindable names in the parameters
           pnames <- ifThenElse (not !isUnboundImplicits) (pure [])
             $ map concat
             $ for (map (Builtin.snd . Builtin.snd . Builtin.snd) params')
             $ findUniqueBindableNames fc True (ps ++ map Builtin.fst params) []

           let paramsb = map (\(n, rig, info, tm) =>
                                 (n, rig, info, doBind pnames tm)) params'
           pure [IParameters fc paramsb (concat pds')]
  desugarDecl ps (PUsing fc uimpls uds)
      = do syn <- get Syn
           let oldu = usingImpl syn
           uimpls' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
                                            btm <- bindTypeNames fc oldu ps tm'
                                            pure (fst ntm, btm)) uimpls
           put Syn (record { usingImpl = uimpls' ++ oldu } syn)
           uds' <- traverse (desugarDecl ps) uds
           syn <- get Syn
           put Syn (record { usingImpl = oldu } syn)
           pure (concat uds')
  desugarDecl ps (PReflect fc tm)
      = throw (GenericMsg fc "Reflection not implemented yet")
--       pure [IReflect fc !(desugar AnyExpr ps tm)]
  desugarDecl ps (PInterface fc vis cons_in tn doc params det conname body)
      = do addDocString tn doc
           let paramNames = map fst params

           let cons = concatMap expandConstraint cons_in
           cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr (ps ++ paramNames)
                                                         (snd ntm)
                                          pure (fst ntm, tm')) cons
           params' <- traverse (\ (nm, (rig, tm)) =>
                         do tm' <- desugar AnyExpr ps tm
                            pure (nm, (rig, tm')))
                      params
           -- Look for bindable names in all the constraints and parameters
           let mnames = map dropNS (definedIn body)
           bnames <- ifThenElse (not !isUnboundImplicits) (pure [])
             $ map concat
             $ for (map Builtin.snd cons' ++ map (snd . snd) params')
             $ findUniqueBindableNames fc True (ps ++ mnames ++ paramNames) []

           let paramsb = map (\ (nm, (rig, tm)) =>
                                 let tm' = doBind bnames tm in
                                 (nm, (rig, tm')))
                         params'
           let consb = map (\ (nm, tm) => (nm, doBind bnames tm)) cons'

           body' <- traverse (desugarDecl (ps ++ mnames ++ paramNames)) body
           pure [IPragma (maybe [tn] (\n => [tn, n]) conname)
                         (\nest, env =>
                             elabInterface fc vis env nest consb
                                           tn paramsb det conname
                                           (concat body'))]
    where
      -- Turns pairs in the constraints to individual constraints. This
      -- is a bit of a hack, but it's necessary to build parent constraint
      -- chasing functions correctly
      pairToCons : PTerm -> List PTerm
      pairToCons (PPair _ l r) = pairToCons l ++ pairToCons r
      pairToCons t = [t]

      expandConstraint : (Maybe Name, PTerm) -> List (Maybe Name, PTerm)
      expandConstraint (Just n, t) = [(Just n, t)]
      expandConstraint (Nothing, p)
          = map (\x => (Nothing, x)) (pairToCons p)

  desugarDecl ps (PImplementation fc vis fnopts pass is cons tn params impln nusing body)
      = do opts <- traverse (desugarFnOpt ps) fnopts
           is' <- traverse (\ (n,c,tm) => do tm' <- desugar AnyExpr ps tm
                                             pure (n, c, tm')) is
           let _ = the (List (Name, RigCount, RawImp)) is'
           cons' <- traverse (\ (n, tm) => do tm' <- desugar AnyExpr ps tm
                                              pure (n, tm')) cons
           let _ = the (List (Maybe Name, RawImp)) cons'
           params' <- traverse (desugar AnyExpr ps) params
           let _ = the (List RawImp) params'
           -- Look for bindable names in all the constraints and parameters
           bnames <- ifThenElse (not !isUnboundImplicits) (pure [])
             $ map concat
             $ for (map snd cons' ++ params')
             $ findUniqueBindableNames fc True ps []

           let paramsb = map (doBind bnames) params'
           let isb = map (\ (n, r, tm) => (n, r, doBind bnames tm)) is'
           let _ = the (List (Name, RigCount, RawImp)) isb
           let consb = map (\(n, tm) => (n, doBind bnames tm)) cons'
           let _ = the (List (Maybe Name, RawImp)) consb

           body' <- maybe (pure Nothing)
                          (\b => do b' <- traverse (desugarDecl ps) b
                                    pure (Just (concat b'))) body
           -- calculate the name of the interface, if it's not explicitly
           -- given.
           let impname = maybe (mkImplName fc tn paramsb) id impln

           pure [IPragma [impname]
                         (\nest, env =>
                             elabImplementation fc vis opts pass env nest isb consb
                                                tn paramsb (isNamed impln)
                                                impname nusing
                                                body')]
    where
      isNamed : Maybe a -> Bool
      isNamed Nothing = False
      isNamed (Just _) = True

  desugarDecl ps (PRecord fc doc vis tn params conname_in fields)
      = do addDocString tn doc
           params' <- traverse (\ (n,c,p,tm) =>
                          do tm' <- desugar AnyExpr ps tm
                             p'  <- mapDesugarPiInfo ps p
                             pure (n, c, p', tm'))
                        params
           let _ = the (List (Name, RigCount, PiInfo RawImp, RawImp)) params'
           let fnames = map fname fields
           let _ = the (List Name) fnames
           -- Look for bindable names in the parameters

           let bnames = if !isUnboundImplicits
                        then concatMap (findBindableNames True
                                         (ps ++ fnames ++ map fst params) [])
                                       (map (\(_,_,_,d) => d) params')
                        else []
           let _ = the (List (String, String)) bnames

           let paramsb = map (\ (n, c, p, tm) => (n, c, p, doBind bnames tm)) params'
           let _ = the (List (Name, RigCount, PiInfo RawImp, RawImp)) paramsb
           let recName = nameRoot tn
           fields' <- traverse (desugarField (ps ++ map fname fields ++
                                              map fst params) (mkNamespace recName))
                               fields
           let _ = the (List IField) fields'
           let conname = maybe (mkConName tn) id conname_in
           let _ = the Name conname
           pure [IRecord fc (Just recName)
                         vis (MkImpRecord fc tn paramsb conname fields')]
    where
      fname : PField -> Name
      fname (MkField _ _ _ _ n _) = n

      mkConName : Name -> Name
      mkConName (NS ns (UN n))
        = let str = displayUserName n in
          NS ns (DN str (MN ("__mk" ++ str) 0))
      mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)

      mapDesugarPiInfo : List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
      mapDesugarPiInfo ps = traverse (desugar AnyExpr ps)

  desugarDecl ps (PFixity fc Prefix prec (UN (Basic n)))
      = do syn <- get Syn
           put Syn (record { prefixes $= insert n prec } syn)
           pure []
  desugarDecl ps (PFixity fc fix prec (UN (Basic n)))
      = do syn <- get Syn
           put Syn (record { infixes $= insert n (fix, prec) } syn)
           pure []
  desugarDecl ps (PFixity fc _ _ _)
      = throw (GenericMsg fc "Fixity declarations must be for unqualified names")
  desugarDecl ps (PMutual fc ds)
      = do let (tys, defs) = splitMutual ds
           mds' <- traverse (desugarDecl ps) (tys ++ defs)
           pure (concat mds')
  desugarDecl ps (PNamespace fc ns decls)
      = withExtendedNS ns $ do
           ds <- traverse (desugarDecl ps) decls
           pure [INamespace fc ns (concat ds)]
  desugarDecl ps (PTransform fc n lhs rhs)
      = do (bound, blhs) <- bindNames False !(desugar LHS ps lhs)
           rhs' <- desugar AnyExpr (bound ++ ps) rhs
           pure [ITransform fc (UN $ Basic n) blhs rhs']
  desugarDecl ps (PRunElabDecl fc tm)
      = do tm' <- desugar AnyExpr ps tm
           pure [IRunElabDecl fc tm']
  desugarDecl ps (PDirective fc d)
      = case d of
             Hide n => pure [IPragma [] (\nest, env => hide fc n)]
             Logging i => pure [ILog ((\ i => (topics i, verbosity i)) <$> i)]
             LazyOn a => pure [IPragma [] (\nest, env => lazyActive a)]
             UnboundImplicits a => do
               setUnboundImplicits a
               pure [IPragma [] (\nest, env => setUnboundImplicits a)]
             PrefixRecordProjections b => do
               pure [IPragma [] (\nest, env => setPrefixRecordProjections b)]
             AmbigDepth n => pure [IPragma [] (\nest, env => setAmbigLimit n)]
             AutoImplicitDepth n => pure [IPragma [] (\nest, env => setAutoImplicitLimit n)]
             NFMetavarThreshold n => pure [IPragma [] (\nest, env => setNFThreshold n)]
             SearchTimeout n => pure [IPragma [] (\nest, env => setSearchTimeout n)]
             PairNames ty f s => pure [IPragma [] (\nest, env => setPair fc ty f s)]
             RewriteName eq rw => pure [IPragma [] (\nest, env => setRewrite fc eq rw)]
             PrimInteger n => pure [IPragma [] (\nest, env => setFromInteger n)]
             PrimString n => pure [IPragma [] (\nest, env => setFromString n)]
             PrimChar n => pure [IPragma [] (\nest, env => setFromChar n)]
             PrimDouble n => pure [IPragma [] (\nest, env => setFromDouble n)]
             CGAction cg dir => pure [IPragma [] (\nest, env => addDirective cg dir)]
             Names n ns => pure [IPragma [] (\nest, env => addNameDirective fc n ns)]
             StartExpr tm => pure [IPragma [] (\nest, env => throw (InternalError "%start not implemented"))] -- TODO!
             Overloadable n => pure [IPragma [] (\nest, env => setNameFlag fc n Overloadable)]
             Extension e => pure [IPragma [] (\nest, env => setExtension e)]
             DefaultTotality tot => pure [IPragma [] (\_, _ => setDefaultTotalityOption tot)]
  desugarDecl ps (PBuiltin fc type name) = pure [IBuiltin fc type name]

  export
  desugarDo : {auto s : Ref Syn SyntaxInfo} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              Side -> List Name -> Maybe Namespace -> PTerm -> Core RawImp
  desugarDo s ps doNamespace tm
      = do b <- newRef Bang (initBangs doNamespace)
           tm' <- desugarB s ps tm
           bd <- get Bang
           pure $ bindBangs (bangNames bd) doNamespace tm'

  export
  desugar : {auto s : Ref Syn SyntaxInfo} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            Side -> List Name -> PTerm -> Core RawImp
  desugar s ps tm = desugarDo s ps Nothing tm


text:
module Example

import Data.Schema.Restricted
import Data.Schema
import Data.Schema.Data

%default total

-- [ Example Predicates on Data ]
data IsUpperC : Char -> Type where
  YesIUC : (isUpper c = True) -> IsUpperC c

data IsUpperCS : List Char -> Type where
  E : IsUpperCS Nil
  C : IsUpperC c -> IsUpperCS cs -> IsUpperCS (c::cs)

data IsUpperStr : String -> Type where
  S : IsUpperCS (unpack s) -> IsUpperStr s

data Name
  = Employee
  | PersonInfo
  | FullName
  | Firstname
  | Lastname
  | Address
  | FirstLine
  | City
  | Country
  | PostCode

||| An Example Schema to describe Employees.
|||
||| The corresponding XSD Schema would potentially be:
|||
||| ```xsd
||| <xs:element name="employee" type="fullpersoninfo"/>
||| <xs:complexType name="personinfo">
|||   <xs:sequence>
|||     <xs:element name="firstname" type="xs:string"/>
|||     <xs:element name="lastname" type="xs:string"/>
|||   </xs:sequence>
||| </xs:complexType>
||| <xs:complexType name="fullpersoninfo">
|||   <xs:complexContent>
|||     <xs:extension base="personinfo">
|||       <xs:sequence>
|||         <xs:element name="address" type="xs:string"/>
|||         <xs:element name="city" type="xs:string"/>
|||         <xs:element name="country" type="xs:string"/>
|||       </xs:sequence>
|||     </xs:extension>
|||   </xs:complexContent>
||| </xs:complexType>
||| ```
|||
EmployeeSchema : Schema Name
EmployeeSchema
  = Complex Employee
      (Complex PersonInfo
          (concat [Complex FullName (concat [Simple $ MkAtom Firstname String RestrictedNot IsString
                                            ,Simple $ MkAtom Lastname  String RestrictedNot IsString
                                            ])
                  ,select [Simple $ MkAtom Address String RestrictedNot IsString
                          ,(concat [Simple $ MkAtom FirstLine String RestrictedNot           IsString
                                   ,Simple $ MkAtom City      String RestrictedNot           IsString
                                   ,Simple $ MkAtom Country   String (Restricted IsUpperStr) IsString
                                   ,Simple $ MkAtom PostCode  String RestrictedNot           IsString
                                   ])]]))

-- [ Example Data ]

||| One employee
employee0 : Data EmployeeSchema
employee0
  = Branch Employee
      (Branch PersonInfo
        (SeqEmpty (Branch FullName (SeqEmpty (Leaf Firstname "Thor" RestrictedNot)
                                   (SeqEmpty (Leaf Lastname "Odinson" RestrictedNot)
                                             Empty)))
        (SeqEmpty (This (Leaf Address "Asgard" RestrictedNot))
                  Empty)))

||| Another Employee
employee1 : Data EmployeeSchema
employee1
  = Branch Employee
      (Branch PersonInfo
        (SeqEmpty (Branch FullName (SeqEmpty (Leaf Firstname "Loki" RestrictedNot)
                                   (SeqEmpty (Leaf Lastname "Laufison" RestrictedNot)
                                             Empty)))
        (SeqEmpty (That (SeqEmpty (Leaf FirstLine "The Frost Palace" RestrictedNot)
                        (SeqEmpty (Leaf City      "Jotun City"       RestrictedNot)
                        (SeqEmpty (Leaf Country "JH" (Restricted (S (C (YesIUC Refl) (C (YesIUC Refl) E)))))
                        (SeqEmpty (Leaf PostCode "JH01" (RestrictedNot))
                                  Empty)))))
                  Empty)))

-- [ EOF ]

max_stars_repo_name: jfdm/idris-shaped

max_issues_repo_name: jfdm/idris-shaped

max_forks_repo_name: jfdm/idris-shaped