text:
namespace Foo

  public export
  data T
    = A Int
    | B T

  export
  Show T where
    show (A n) = "[A " ++ show n ++ "]"
    show (B t) = "[B " ++ show t ++ "]"

namespace Bar

  %hide Foo.T

  public export
  data T
    = A Int
    | B T
    | C Bool

  export
  Show T where
    show (A n) = "{A " ++ show n ++ "}"
    show (B t) = "{B " ++ show t ++ "}"
    show (C b) = "{C " ++ show b ++ "}"

  %unhide Foo.T

foo : Foo.T
foo = B (A 5)

bar : Bar.T
bar = B (A 6)

main : IO ()
main = do
  printLn foo
  printLn bar

ext: idr


text:
zeroNotSucc : (0 = S k) -> Void
zeroNotSucc Refl impossible

succNotZero : (S k = 0) -> Void
succNotZero Refl impossible

noRec : (contra : (k = j) -> Void) -> (S k = S j) -> Void
noRec contra Refl = contra Refl

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
checkEqNat Z Z = Yes Refl
checkEqNat Z (S k) = No zeroNotSucc
checkEqNat (S k) Z = No succNotZero
checkEqNat (S k) (S j) = case checkEqNat k j of
                            Yes prf => Yes (cong prf)
                            No contra => No (noRec contra)

data Vect : Nat -> Type -> Type where
     Nil  : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

headUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
    (contra : (x = y) -> Void) -> (x :: xs) = (y :: ys) -> Void
headUnequal contra Refl = contra Refl

tailUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
    (contra : (xs = ys) -> Void) -> (x :: xs) = (y :: ys) -> Void
tailUnequal contra Refl = contra Refl

DecEq a => DecEq (Vect n a) where
    decEq [] [] = Yes Refl
    decEq (x :: xs) (y :: ys) =
        case decEq x y of
            No contra => No (headUnequal contra)
            Yes Refl => case decEq xs ys of
                Yes Refl => Yes Refl
                No contra => No (tailUnequal contra)


text:
import Data.Vect

x : Int
x = 5

ErrorOrNat : (n:Nat) -> Type
ErrorOrNat Z = String
ErrorOrNat (S k) = Nat

divide : (dividend:Nat) -> (divisor:Nat) -> ErrorOrNat divisor
divide dividend Z = "Division by zero"
divide dividend (S k) = div dividend (S k)

length : List Int -> Int
length [] = 0
length (x :: xs) = 1 + length xs

xs : List Int
xs = [1,2,3]

ys : Vect 3 Int
ys = [1,2,3]

vtake : (n:Nat) -> Vect (n+m) t -> Vect n t
vtake Z xs = []
vtake (S k) (x :: xs) = x :: vtake k xs

zs : String
zs = show ( vtake 3 [1,2,3,4,5] )

vconcat : Vect n t -> Vect m t -> Vect (n+m) t
vconcat [] ys = ys
vconcat (x :: xs) ys = x :: vconcat xs ys


text:
module Network.Curl.Types.Code

||| Providing a mapping from constructor to Int.
public export
interface ToCode a where
  total
  toCode : a -> Int

||| Providing a mapping from Int to constructor.
||| Two ways in case you are certain the Int has a mapping
public export
interface FromCode a where
  unsafeFromCode : Int -> a
  total
  fromCode : Int -> Maybe a


text:
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

Eq Shape where
  (==) (Triangle a b) (Triangle j k) = a == j && b == k
  (==) (Rectangle a b) (Rectangle j k) = a == j && b == k
  (==) (Circle a) (Circle b) = a == b
  (==) _ _ = False

Ord Shape where
  compare shape_l shape_r = compare (area shape_l) (area shape_r)

testShapes : List Shape
testShapes = [Circle 3, Triangle 3 9, Rectangle 2 6, Circle 4, Rectangle 2 7]


text:
-- test that defs from String are available.
import Data.String

-- same signature as a function pulled in from above import
sameSig : Char -> String
sameSig = singleton


text:
||| A predicate p on a type t is a partial function from
||| t to Type. A refinement of t under p is the domain of p,
||| that is, the subset of values in t for which p is defined.
|||
||| Idris2 provides data type `Subset` for modelling invariants
||| about values, with the guarantee that these invariants
||| will be erased at runtime. We use this data type in this
||| library as a proof that a value has been properly validated
||| (refined) at runtime.
|||
||| The majority of predicates defined in this module are
||| boolean predicates: Proofs that a runtime check returned
||| `True` most of the time. However, some other combinators
||| exist, and these can be used with other typelevel
||| propositions as well.
|||
||| This module only provides a large set of predefined
||| predicates. For an interface to check these predicates
||| at runtime, see module `Data.Subset.Interfaces`.
|||
||| Note: With function names starting with a lowercase letter,
|||       Idris2 often fails to treat them as predicate functions
|||       and considers them as type paramters. This can lead
|||       to unexpected behavior. For instance, the following will
|||       not compile:
|||
|||       ```idris example
|||       alpha : Subset Char $ Is isAlpha
|||       alpha = refine 'z'
|||       ```
|||
|||       Whereas the following version compiles just fine:
|||
|||       ```idris example
|||       IsAlpha : Char -> Type
|||       IsAlpha = Is isAlpha
|||
|||       alpha : Subset Char IsAlpha
|||       alpha = refine 'z'
|||       ```
module Data.Subset.Predicates

import public Data.DPair

%default total

--------------------------------------------------------------------------------
--          Predicate Combinators
--------------------------------------------------------------------------------

||| Proof that the given boolean predicate `pred` holds for `v`
||| (that is, `pred v` returns `True`).
|||
||| Probably the workhorse of this module. Allows us to
||| conveniently specify short boolean predicates through
||| anonymous functions.
|||
||| ```idris example
||| IsShortString : String -> Type
||| IsShortString = Is \s => length s <= 20
||| ```
public export
data Is : (pred : t -> Bool) -> (v : t) -> Type where
  ItIs : (prf : pred v = True) -> Is {t = t} pred v

||| Proof that the given predicate `p` holds for the image
||| of value `v` under function `f`.
|||
||| This is especially useful if `p` is actually a list of predicates.
|||
||| ```idris example
||| IsShortNonEmptyString : String -> Type
||| IsShortNonEmptyString = Via {a = String} length $ And [GT 0, LEQ 20]
||| ```
public export
data Via : (0 f : a -> b) -> (0 p : b -> Type) -> (v : a) -> Type where
  Go : (v : a) -> (prf : p (f v)) -> Via f p v

||| Proof that all predicates in list `ps`
||| hold for the given value `v`
public export
data And : (0 ps : List (t -> Type)) -> (v : t) -> Type where
  Nil  : And [] v
  (::) : (prf : p v) -> And ps v -> And {t = t} (p :: ps) v

||| Proof that at least one predicate in a list `ps`
||| of predicates holds for the given value `v`.
public export
data Or : (0 ps : List (t -> Type)) -> (v : t) -> Type where
  Z : (prf : p v) -> Or {t = t} (p :: ps) v
  S : Or ps v    -> Or {t = t} (p :: ps) v

||| Proof that the given predicate `p` does not hold for `v`.
public export
data Neg : (0 p : t -> Type) -> (v : t) -> Type where
  IsNeg : (contra : p v -> Void) -> Neg {t = t} p v

--------------------------------------------------------------------------------
--          EqOrd Predicates
--------------------------------------------------------------------------------

||| Alias for `Is (a ==)`
public export
EQ : Eq a => a -> a -> Type
EQ a = Is (a ==)

||| Alias for `Is (a /=)`
public export
NEQ : Eq a => a -> a -> Type
NEQ a = Is (a /=)

||| Alias for `Is (> a)`
public export
GT : Ord a => a -> a -> Type
GT a = Is (> a)

||| Alias for `Is (< a)`
public export
LT : Ord a => a -> a -> Type
LT a = Is (< a)

||| Alias for `Is (>= a)`
public export
GEQ : Ord a => a -> a -> Type
GEQ a = Is (>= a)

||| Alias for `Is (<= a)`
public export
LEQ : Ord a => a -> a -> Type
LEQ a = Is (<= a)

||| Inclusive interval of numbers
public export
FromTo : Ord a => a -> a -> a -> Type
FromTo mi ma = And [GEQ mi, LEQ ma]

--------------------------------------------------------------------------------
--          Numeric Predicates
--------------------------------------------------------------------------------

||| Alias for `GT 0`
public export
IsPositive : Ord a => Num a => a -> Type
IsPositive = GT 0

||| Alias for `LT 0`
public export
IsNegative : Ord a => Num a => a -> Type
IsNegative = LT 0

||| Alias for `GEQ 0`
public export
IsNonNegative : Ord a => Num a => a -> Type
IsNonNegative = GEQ 0

||| Alias for `LEQ 0`
public export
IsNonPositive : Ord a => Num a => a -> Type
IsNonPositive = LEQ 0

||| Values in the interval [0,1]
public export
IsUnit : Ord a => Num a => a -> Type
IsUnit = FromTo 0 1

infixl 9 `divides`

public export
divides : Eq a => Integral a => a -> a -> Bool
divides x y = x /= 0 && y `mod` x == 0

||| Alias for `Is (a `divides`)`
public export
IsDivisibleBy : Eq a => Integral a => a -> a -> Type
IsDivisibleBy a = Is (a `divides`)

||| Alias for `IsDivisibleBy 2`
public export
IsEven : Eq a => Integral a => a -> Type
IsEven = IsDivisibleBy 2

||| Alias for `Is (not $ a `divides`)`
public export
IsNotDivisibleBy : Eq a => Integral a => a -> a -> Type
IsNotDivisibleBy a = Is (\b => not $ a `divides` b)

||| Alias for `IsNotDivisibleBy 2`
public export
IsOdd : Eq a => Integral a => a -> Type
IsOdd = IsNotDivisibleBy 2

--------------------------------------------------------------------------------
--          Numeric Subsets
--------------------------------------------------------------------------------

||| Subset of positive numbers.
|||
||| ```idris example
||| anInt : Positive Int
||| anInt = 12
||| ```
public export
Positive : (t : Type) -> Ord t => Num t => Type
Positive t = Subset t IsPositive

||| Subset of non-negative numbers.
|||
||| ```idris example
||| zero : NonNegative Int
||| zero = 0
||| ```
public export
NonNegative : (t : Type) -> Ord t => Num t => Type
NonNegative t = Subset t IsNonNegative

||| Subset of negative numbers.
|||
||| ```idris example
||| minusOne : Negative Int
||| minusOne = -1
||| ```
public export
Negative : (t : Type) -> Ord t => Num t => Type
Negative t = Subset t IsNegative

||| Subset of non-positive numbers.
|||
||| ```idris example
||| zero : NonPositive Int
||| zero = 0
||| ```
public export
NonPositive : (t : Type) -> Ord t => Num t => Type
NonPositive t = Subset t IsNonPositive

||| Subset of numbers in the inclusive range [0,1].
|||
||| ```idris example
||| pointFive : Unit Double
||| pointFive = 0.5
||| ```
public export
Unit : (t : Type) -> Ord t => Num t => Type
Unit t = Subset t IsUnit

||| Subset of even integers.
|||
||| ```idris example
||| fourteen : Even Int
||| fourteen = 14
||| ```
public export
Even : (t : Type) -> Eq t => Integral t => Type
Even t = Subset t IsEven

||| Subset of odd integers.
|||
||| ```idris example
||| seven : Odd Int
||| seven = 7
||| ```
public export
Odd : (t : Type) -> Eq t => Integral t => Type
Odd t = Subset t IsOdd

--------------------------------------------------------------------------------
--          Char Predicates
--------------------------------------------------------------------------------

||| Alias fo `Is isUpper`.
public export
IsUpper : Char -> Type
IsUpper = Is isUpper

||| Alias fo `Is isLower`.
public export
IsLower : Char -> Type
IsLower = Is isLower

||| Alias fo `Is isAlpha`.
public export
IsAlpha : Char -> Type
IsAlpha = Is isAlpha

||| Alias fo `Is isDigit`.
public export
IsDigit : Char -> Type
IsDigit = Is isDigit

||| Alias fo `Is isAlphaNum`.
public export
IsAlphaNum : Char -> Type
IsAlphaNum = Is isAlphaNum

||| Alias fo `Is isSpace`.
public export
IsSpace : Char -> Type
IsSpace = Is isSpace

||| Alias fo `Is isNL`.
public export
IsNL : Char -> Type
IsNL = Is isNL

||| Alias fo `Is isHexDigit`.
public export
IsHexDigit : Char -> Type
IsHexDigit = Is isHexDigit

||| Alias fo `Is isHexDigit`.
public export
IsOctDigit : Char -> Type
IsOctDigit = Is isOctDigit

||| Alias fo `Is isControl`.
public export
IsControl : Char -> Type
IsControl = Is isControl

--------------------------------------------------------------------------------
--          Character Subsets
--------------------------------------------------------------------------------

||| Subset of upper case characters (range 'A'-'Z').
public export
Upper : Type
Upper = Subset Char IsUpper

||| Subset of lower case characters (range 'a'-'z').
public export
Lower : Type
Lower = Subset Char IsLower

||| Subset of characters in the ranges 'a'-'z' and 'A'-'Z'.
public export
Alpha : Type
Alpha = Subset Char IsAlpha

||| Subset of characters in the range '0'-'9'
public export
Digit : Type
Digit = Subset Char IsDigit

||| Subset of alphanumeric characters.
public export
AlphaNum : Type
AlphaNum = Subset Char IsAlphaNum

||| Subset of space characters.
public export
Space : Type
Space = Subset Char IsSpace

||| Subset of newline characters.
public export
NL : Type
NL = Subset Char IsNL

||| Subset of hexadecimal digits.
public export
HexDigit : Type
HexDigit = Subset Char IsHexDigit

||| Digits in the range '0'-'7'.
public export
OctDigit : Type
OctDigit = Subset Char IsOctDigit

||| Subset of control characters.
public export
Control : Type
Control = Subset Char IsControl

--------------------------------------------------------------------------------
--          String Predicates
--------------------------------------------------------------------------------

||| Proof that a String is actually the empty string.
||| This is often useful in combination with `Or`.
|||
||| As an example, consider a predicate `IsEmail` for valid
||| email addresses, and an optional "eMail" field in a GUI
||| that accepts either a valid email or an empty string.
|||
||| It's refinement type might be defined as follows:
|||
||| ```idris example
||| OptionalEmail : Type
||| OptionalEmail = Subset String $ Or [IsEmptyString, IsEmail]
||| ```
public export
IsEmptyString : String -> Type
IsEmptyString = Is \s => length s == 0

||| Proof that a String is non-empty.
public export
IsNonEmptyString : String -> Type
IsNonEmptyString = Is \s => length s > 0

||| Proof that a String's length does not
||| exceed the given value.
public export
MaxStringLength : Nat -> String -> Type
MaxStringLength n = Is \s => length s <= n

||| Proof that a String's length is at least
||| the given value.
public export
MinStringLength : Nat -> String -> Type
MinStringLength n = Is \s => length s >= n

||| Proof that the given boolean predicate holds for all
||| characters in a String
public export
AllChars : (pred : Char -> Bool) -> String -> Type
AllChars pred = Is $ all pred . unpack

||| Proof that the given boolean predicate holds for at least
||| one character in a String
public export
AnyChar : (pred : Char -> Bool) -> String -> Type
AnyChar pred = Is $ any pred . unpack

||| Proof that a string has no line breaks
public export
NoLinebreak : String -> Type
NoLinebreak = AllChars (not . isNL)

||| Proof that a string has no control characters
public export
NoControlChars : String -> Type
NoControlChars = AllChars (not . isControl)

--------------------------------------------------------------------------------
--          String Subsets
--------------------------------------------------------------------------------

||| Subset of non-empty Strings.
public export
NonEmptyString : Type
NonEmptyString = Subset String IsNonEmptyString

||| Subset of Strings consisting only of alphanumeric characters
||| in the ranges 'a'-'z', 'A'-'Z', '0'-'9'.
public export
AlphaNumString : Type
AlphaNumString = Subset String $ AllChars isAlphaNum

||| Subset of Strings without line breaks
public export
Line : Type
Line = Subset String NoLinebreak

||| Subset of Strings without control characters
public export
PlainString : Type
PlainString = Subset String NoControlChars

--------------------------------------------------------------------------------
--          Foldable Predicates
--------------------------------------------------------------------------------

||| Proof that the given predicate holds for all values
||| in a `Foldable` structure.
public export
Forall : Foldable f => (pred : a -> Bool) -> f a -> Type
Forall pred = Is $ all pred

||| Proof that the given predicate holds for at least one value
||| in a `Foldable` structure.
public export
Exists : Foldable f => (pred : a -> Bool) -> f a -> Type
Exists pred = Is $ any pred


text:
module Average

export
average : List Nat -> Double
average elems = let summed = sum elems
                    len = length elems in
                    cast summed / cast len

||| averages the length of each word splitting on spaces
||| @str a string containing words seperated by whitespaces
export
averageWordLen : (str: String) -> Double
averageWordLen = average . map length . words


text:
module Main

record Point where
  constructor MkPoint
  x : Double
  y : Double

-- a record creates two projections:
-- x : Point -> Double
-- y : Point -> Double

record Rect where
  constructor MkRect
  topLeft : Point
  bottomRight : Point

pt : Point
pt = MkPoint 4.2 6.6

rect : Rect
rect =
  MkRect
    (MkPoint 1.1 2.5)
    (MkPoint 4.3 6.3)

-- Foo.bar.baz with uppercase F is one lexeme: DotSepIdent ["baz", "bar", "Foo"]
-- foo.bar.baz with lowercase f is three lexemes: foo, .bar, .baz
-- .foo.bar.baz is three lexemes: .foo, .bar, .baz
--
-- If you want Constructor.field, you have to write (Constructor).field.

add : Num a => a -> a -> a
add x y = x + y

oopFoldl : List a -> b -> (b -> a -> b) -> b
oopFoldl xs z f = foldl f z xs

bad : Double
bad =
  rect.x.topLeft        -- should not throw errors
  + rect.(x . topLeft)  -- disallowed without %language PostfixProjections

bad2 : Double
bad2 = (.oopFoldl 0 (+))  -- disallowed without %language PostfixProjections

%language PostfixProjections
-- from now on, we can use complex projections


text:
module Toml.Data

import Data.String
import Data.List

import Extra.String

mutual
  public export
  data Value : Type where
    Str : String -> Value
    Num : Int -> Value
    Lst : List Value -> Value
    ArrTab : List Toml -> Value

  public export
  Toml : Type
  Toml = List (List String, Value)

toList : Toml -> List (List String, Value)
toList = id

export covering
Show Value where
  show (Str str) = (quote str)
  show (Num x) = (show x)
  show (Lst els) = (showList show els)
  show (ArrTab t) = show t

export covering
Eq Value where
  (Str s0) == (Str s1) = s0 == s1
  (Num x0) == (Num x1) = x0 == x1
  (Lst x0) == (Lst x1) = x0 == x1
  (ArrTab x0) == (ArrTab x1) = x0 == x1
  _ == _ = False

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Quicksort

import Data.Vect

total
partitionVect : Ord elem => (pivot : elem) -> (Vect n elem) -> (l1 : Nat ** l2 : Nat ** (Vect l1 elem, Vect l2 elem, n = (l1 + l2)))
partitionVect pivot [] = (0 ** 0 ** ([], [],Refl))
partitionVect pivot (x :: xs) with (partitionVect pivot xs)
  partitionVect pivot (x :: xs) | (l1 ** l2 ** ( v1, v2, equality)) = if (x <= pivot) then (S (l1) ** l2 ** ((x :: v1), v2, cong {f = S} equality)) else
    (l1 ** S (l2) ** (v1, x :: v2, trans (cong {f = S} equality) (plusSuccRightSucc l1 l2)))

-- qsort : Ord elem => Vect n elem -> (l1 ** l2 ** (Vect (l1 + l2) elem, (l1 + l2) = n))


text:
module Control.Optics.Pair

import public Control.Optics.Lens
import public Control.Optics.Getter
import public Control.Optics.Setter

export
lfst : Lens (a, c) (b, c) a b
lfst = lens fst (flip (mapFst . const))

export
lsnd : Lens (c, a) (c, b) a b
lsnd = lens snd (flip (mapSnd . const))

export
paired : {a, b : _} -> Simple Lens s a -> Simple Lens s b -> Simple Lens s (a, b)
paired l r = lens (\s => (view l s, view r s)) (\s, (a, b) => set l a $ set r b $ s)


text:
import Data.String

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
     then pure (Just (stringToNatOrZ input))
     else pure Nothing

readNumbers_v1 : IO (Maybe (Nat, Nat))
readNumbers_v1 =
  do num1 <- readNumber
     case num1 of
          Nothing => pure Nothing
          Just num1_ok =>
               do num2 <- readNumber
                  case num2 of
                       Nothing => pure Nothing
                       Just num2_ok => pure (Just (num1_ok, num2_ok))

readPair : IO (String, String)
readPair = do str1 <- getLine
              str2 <- getLine
              pure (str1, str2)

partial
readNumbers_v2 : IO (Maybe (Nat, Nat))
readNumbers_v2 =
  do Just num1_ok <- readNumber
     Just num2_ok <- readNumber
     pure (Just (num1_ok, num2_ok))

readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
  do Just num1_ok <- readNumber | Nothing => pure Nothing
     Just num2_ok <- readNumber | Nothing => pure Nothing
     pure (Just (num1_ok, num2_ok))


text:
module Erlang.Types

%default total

-- This module contains data types that have special handling in the Erlang
-- code generator. Even if these data types have special handling, you can
-- use them like any other Idris data types. For example: You can use pattern
-- matching to obtain the contained values.
--
-- When calling an Erlang function you can pass these data types and assume
-- that they have the expected representation in Erlang. Similarly, when
-- retrieving values from Erlang (in the case of `erlUnsafeCall`), you should
-- be careful to choose the correct type. If you are unsure or if the returned
-- value can have one of many possible types, then you should specify `ErlTerm`.

||| Represents any Erlang term.
|||
||| An `ErlTerm` can be converted to a typed value using
||| `Erlang.Decode.erlDecode` and friends.
export
data ErlTerm : Type where [external]

||| Represents a value that have no meaning to Erlang.
|||
||| Some of the Erlang interop functions require that the value is a member of
||| `ErlType`. If you still want to pass the Idris value to Erlang, you can
||| wrap it in the `Raw` type.
|||
||| `Raw a` is compiled to `a`.
public export
data Raw a = MkRaw a

-- ATOMS

||| Represents an Erlang atom.
|||
||| | Idris                    | Erlang            |
||| | ------------------------ | ----------------- |
||| | `MkAtom "ok"`            | `ok`              |
||| | `MkAtom "Elixir.String"` | `'Elixir.String'` |
public export
data ErlAtom : Type where
  [noNewtype]
  MkAtom : String -> ErlAtom

-- CHARLISTS

||| Represents an Erlang charlist.
|||
||| | Idris                 | Erlang                  |
||| | --------------------- | ----------------------- |
||| | `MkCharlist "abc"`    | `"abc"`, `[97, 98, 99]` |
||| | `MkCharlist ""`       | `""`, `[]`              |
public export
data ErlCharlist : Type where
  [noNewtype]
  MkCharlist : String -> ErlCharlist

-- LISTS

namespace MaybeImproperList
  ||| Represents the Erlang empty list.
  |||
  ||| | Idris            | Erlang |
  ||| | ---------------- | ------ |
  ||| | `the ErlNil Nil` | `[]`   |
  public export
  data ErlNil = Nil

  ||| Represents the head and tail of an Erlang list.
  |||
  ||| `ErlCons` can be used to create improper lists. Combine with `ErlNil`
  ||| to create a proper list.
  |||
  ||| | Idris                                  | Erlang              |
  ||| | -------------------------------------- | ------------------- |
  ||| | `the (ErlCons Int Double) (3 :: 7.5)`  | `[3 | 7.5]`         |
  ||| | `the (ErlCons Int ErlNil) (42 :: Nil)` | `[42 | []]`, `[42]` |
  public export
  data ErlCons a b = (::) a b

namespace ProperList
  ||| Represents an Erlang list where each element has a separate type.
  |||
  ||| `ErlList` can only represent proper lists.
  |||
  ||| Note that `Prelude.List` is also converted to an Erlang list. The
  ||| difference between `ErlList` and `List` is that `List` require that
  ||| all elements have the same type.
  |||
  ||| | Idris                                  | Erlang              |
  ||| | -------------------------------------- | ------------------- |
  ||| | `the (ErlCons Int Int) (3 :: 7)`       | `[3 | 7]`           |
  ||| | `the (ErlCons Int ErlNil) (42 :: Nil)` | `[42 | []]`, `[42]` |
  public export
  data ErlList : List Type -> Type where
    Nil : ErlList []
    (::) : x -> ErlList xs -> ErlList (x :: xs)

-- MAPS

||| A data type to describe an entry in an Erlang map.
|||
||| This data type is a helper type for `ErlMapSubset` and does not
||| represent anything specific in Erlang.
public export
data ErlMapEntry : Type where
  MkMapEntry : key -> (valueTy : Type) -> ErlMapEntry

infix 0 :=

||| A convenience operator to describe an entry in an Erlang map.
|||
||| `"name" := String` is equivalent to `MkMapEntry "name" String`.
public export
(:=) : key -> (valueTy : Type) -> ErlMapEntry
(:=) = MkMapEntry

||| Represents an Erlang map containing at least the entries specified in
||| its type. The Erlang map may still contain other entries.
|||
||| As an example: `ErlMapSubset [MkAtom "name" := String, MkAtom "age" := Int]`
||| represents any Erlang map that contains both of these entries (and possibly
||| more entries). Thus, the following Erlang values matches this specification:
||| - `#{name => <<"Christian">>, age => 33}`
||| - `#{name => <<"Christian">>, age => 33, other_field => true}`
|||
||| See module `Erlang.Types.Map` for Map-related functions.
export
data ErlMapSubset : List ErlMapEntry -> Type where [external]

||| Represents any Erlang maps.
|||
||| At compile-time one does not know which keys are available
||| in the map.
|||
||| See module `Erlang.Types.Map` for Map-related functions.
public export
ErlAnyMap : Type
ErlAnyMap = ErlMapSubset []

-- REFERENCE TYPES

||| Represents an Erlang process ID.
export
data ErlPid : Type where [external]

||| Represents an Erlang reference.
export
data ErlReference : Type where [external]

||| Represents an Erlang port.
export
data ErlPort : Type where [external]

-- TUPLES

||| Represents an Erlang tuple of size 0.
|||
||| | Idris      | Erlang |
||| | ---------- | ------ |
||| | `MkTuple0` | `{}`   |
public export
data ErlTuple0 : Type where
  MkTuple0 : ErlTuple0

||| Represents an Erlang tuple of size 1.
|||
||| | Idris         | Erlang |
||| | ------------- | ------ |
||| | `MkTuple1 42` | `{42}` |
public export
data ErlTuple1 : Type -> Type where
  [noNewtype]
  MkTuple1 : a -> ErlTuple1 a

||| Represents an Erlang tuple of size 2.
|||
||| | Idris             | Erlang      |
||| | ----------------- | ----------- |
||| | `MkTuple2 42 7.5` | `{42, 7.5}` |
public export
data ErlTuple2 : Type -> Type -> Type where
  MkTuple2 : a -> b -> ErlTuple2 a b

||| Represents an Erlang tuple of size 3.
public export
data ErlTuple3 : Type -> Type -> Type -> Type where
  MkTuple3 : a -> b -> c -> ErlTuple3 a b c

||| Represents an Erlang tuple of size 4.
public export
data ErlTuple4 : Type -> Type -> Type -> Type -> Type where
  MkTuple4 : a -> b -> c -> d -> ErlTuple4 a b c d

||| Represents an Erlang tuple of size 5.
public export
data ErlTuple5 : Type -> Type -> Type -> Type -> Type -> Type where
  MkTuple5 : a -> b -> c -> d -> e -> ErlTuple5 a b c d e

||| Represents an Erlang tuple of size 6.
public export
data ErlTuple6 : Type -> Type -> Type -> Type -> Type -> Type -> Type where
  MkTuple6 : a -> b -> c -> d -> e -> f -> ErlTuple6 a b c d e f

||| Represents an Erlang tuple of size 7.
public export
data ErlTuple7 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where
  MkTuple7 : a -> b -> c -> d -> e -> f -> g -> ErlTuple7 a b c d e f g

||| Represents an Erlang tuple of size 8.
public export
data ErlTuple8 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where
  MkTuple8 : a -> b -> c -> d -> e -> f -> g -> h -> ErlTuple8 a b c d e f g h

-- FUNCTIONS

||| Represents an Erlang function of arity 0.
|||
||| `ErlFun/N` is a series of data types that can be used to convert a pure
||| Idris function to an Erlang function of a given arity, or to convert an
||| Erlang function to a pure Idris function.
|||
||| Note that `ErlFun/N` should only be used when the Erlang function does not
||| perform any side-effects. If the Erlang function performs any side-effects,
||| you should instead use one of the `ErlIOFun/N` data types.
public export
data ErlFun0 : Type -> Type where
  [noNewtype]
  MkFun0 : ret -> ErlFun0 ret

||| Represents an Erlang function of arity 1.
|||
||| See the documentation of `ErlFun0` for more details.
public export
data ErlFun1 : Type -> Type -> Type where
  [noNewtype]
  MkFun1 : (a -> ret) -> ErlFun1 a ret

||| Represents an Erlang function of arity 2.
|||
||| See the documentation of `ErlFun0` for more details.
public export
data ErlFun2 : Type -> Type -> Type -> Type where
  [noNewtype]
  MkFun2 : (a -> b -> ret) -> ErlFun2 a b ret

||| Represents an Erlang function of arity 3.
|||
||| See the documentation of `ErlFun0` for more details.
public export
data ErlFun3 : Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkFun3 : (a -> b -> c -> ret) -> ErlFun3 a b c ret

||| Represents an Erlang function of arity 4.
|||
||| See the documentation of `ErlFun0` for more details.
public export
data ErlFun4 : Type -> Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkFun4 : (a -> b -> c -> d -> ret) -> ErlFun4 a b c d ret

||| Represents an Erlang function of arity 5.
|||
||| See the documentation of `ErlFun0` for more details.
public export
data ErlFun5 : Type -> Type -> Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkFun5 : (a -> b -> c -> d -> e -> ret) -> ErlFun5 a b c d e ret

||| Represents an Erlang function of arity 6.
|||
||| See the documentation of `ErlFun0` for more details.
public export
data ErlFun6 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkFun6 : (a -> b -> c -> d -> e -> f -> ret) -> ErlFun6 a b c d e f ret

||| Represents an Erlang function of arity 7.
|||
||| See the documentation of `ErlFun0` for more details.
public export
data ErlFun7 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkFun7 : (a -> b -> c -> d -> e -> f -> g -> ret) -> ErlFun7 a b c d e f g ret

||| Represents an Erlang function of arity 8.
|||
||| See the documentation of `ErlFun0` for more details.
public export
data ErlFun8 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkFun8 : (a -> b -> c -> d -> e -> f -> g -> h -> ret) -> ErlFun8 a b c d e f g h ret

||| Represents an Erlang function of arity 0.
|||
||| `ErlIOFun/N` is a series of data types that can be used to convert an Idris
||| function that performs side-effects to an Erlang function of a given arity,
||| or to convert an Erlang function to an Idris function that performs
||| side-effects.
|||
||| If you are certain that the Erlang function is pure, then you can consider
||| using one of the `ErlFun/N` data types.
public export
data ErlIOFun0 : Type -> Type where
  [noNewtype]
  MkIOFun0  : IO ret -> ErlIOFun0 ret

||| Represents an Erlang function of arity 1.
|||
||| See the documentation of `ErlIOFun0` for more details.
public export
data ErlIOFun1 : Type -> Type -> Type where
  [noNewtype]
  MkIOFun1  : (a -> IO ret) -> ErlIOFun1 a ret

||| Represents an Erlang function of arity 2.
|||
||| See the documentation of `ErlIOFun0` for more details.
public export
data ErlIOFun2 : Type -> Type -> Type -> Type where
  [noNewtype]
  MkIOFun2  : (a -> b -> IO ret) -> ErlIOFun2 a b ret

||| Represents an Erlang function of arity 3.
|||
||| See the documentation of `ErlIOFun0` for more details.
public export
data ErlIOFun3 : Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkIOFun3  : (a -> b -> c -> IO ret) -> ErlIOFun3 a b c ret

||| Represents an Erlang function of arity 4.
|||
||| See the documentation of `ErlIOFun0` for more details.
public export
data ErlIOFun4 : Type -> Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkIOFun4  : (a -> b -> c -> d -> IO ret) -> ErlIOFun4 a b c d ret

||| Represents an Erlang function of arity 5.
|||
||| See the documentation of `ErlIOFun0` for more details.
public export
data ErlIOFun5 : Type -> Type -> Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkIOFun5  : (a -> b -> c -> d -> e -> IO ret) -> ErlIOFun5 a b c d e ret

||| Represents an Erlang function of arity 6.
|||
||| See the documentation of `ErlIOFun0` for more details.
public export
data ErlIOFun6 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkIOFun6  : (a -> b -> c -> d -> e -> f -> IO ret) -> ErlIOFun6 a b c d e f ret

||| Represents an Erlang function of arity 7.
|||
||| See the documentation of `ErlIOFun0` for more details.
public export
data ErlIOFun7 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkIOFun7  : (a -> b -> c -> d -> e -> f -> g -> IO ret) -> ErlIOFun7 a b c d e f g ret

||| Represents an Erlang function of arity 8.
|||
||| See the documentation of `ErlIOFun0` for more details.
public export
data ErlIOFun8 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where
  [noNewtype]
  MkIOFun8  : (a -> b -> c -> d -> e -> f -> g -> h -> IO ret) -> ErlIOFun8 a b c d e f g h ret

-- ERLANG TYPE PREDICATE

mutual
  ||| `ErlType` describes all data types that have a natural representation
  ||| in Erlang. `ErlType` can help prevent mistakes such as trying to pass
  ||| invalid values to Erlang functions.
  |||
  ||| All Idris values must have a representation in Erlang, but it is not
  ||| always clear what that representation should be. For example: How
  ||| should the value `Just 42` be represented in Erlang? It could be `{ok, 42}`,
  ||| `{just, 42}` or something else.
  |||
  ||| If you need to pass an Idris value to Erlang that is not present in this
  ||| data type, you can always wrap the value in the `Raw` type.
  public export
  data ErlType : Type -> Type where
    ETInt           : ErlType Int
    ETInteger       : ErlType Integer
    ETDouble        : ErlType Double
    ETString        : ErlType String
    ETChar          : ErlType Char
    ETList          : ErlType a => ErlType (List a)

    ETRaw           : ErlType (Raw a)     -- Can contain any Idris value
    ETErlTerm       : ErlType ErlTerm     -- Can contain any Erlang term

    -- Data types that bridge to native Erlang data types
    ETErlAtom       : ErlType ErlAtom
    ETErlCharlist   : ErlType ErlCharlist
    ETErlNil        : ErlType ErlNil
    ETErlCons       : (ErlType a, ErlType b) => ErlType (ErlCons a b)
    ETErlList       : ErlTypes xs => ErlType (ErlList xs)
    ETErlMapSubset  : ErlMapTypes xs => ErlType (ErlMapSubset xs)
    ETErlPid        : ErlType ErlPid
    ETErlReference  : ErlType ErlReference
    ETErlPort       : ErlType ErlPort
    ETErlTuple0     : ErlType ErlTuple0
    ETErlTuple1     : ErlTypes [a]                           => ErlType (ErlTuple1 a)
    ETErlTuple2     : ErlTypes [a, b]                        => ErlType (ErlTuple2 a b)
    ETErlTuple3     : ErlTypes [a, b, c]                     => ErlType (ErlTuple3 a b c)
    ETErlTuple4     : ErlTypes [a, b, c, d]                  => ErlType (ErlTuple4 a b c d)
    ETErlTuple5     : ErlTypes [a, b, c, d, e]               => ErlType (ErlTuple5 a b c d e)
    ETErlTuple6     : ErlTypes [a, b, c, d, e, f]            => ErlType (ErlTuple6 a b c d e f)
    ETErlTuple7     : ErlTypes [a, b, c, d, e, f, g]         => ErlType (ErlTuple7 a b c d e f g)
    ETErlTuple8     : ErlTypes [a, b, c, d, e, f, g, h]      => ErlType (ErlTuple8 a b c d e f g h)
    ETErlFun0       : ErlTypes [ret]                         => ErlType (ErlFun0 ret)
    ETErlFun1       : ErlTypes [a, ret]                      => ErlType (ErlFun1 a ret)
    ETErlFun2       : ErlTypes [a, b, ret]                   => ErlType (ErlFun2 a b ret)
    ETErlFun3       : ErlTypes [a, b, c, ret]                => ErlType (ErlFun3 a b c ret)
    ETErlFun4       : ErlTypes [a, b, c, d, ret]             => ErlType (ErlFun4 a b c d ret)
    ETErlFun5       : ErlTypes [a, b, c, d, e, ret]          => ErlType (ErlFun5 a b c d e ret)
    ETErlFun6       : ErlTypes [a, b, c, d, e, f, ret]       => ErlType (ErlFun6 a b c d e f ret)
    ETErlFun7       : ErlTypes [a, b, c, d, e, f, g, ret]    => ErlType (ErlFun7 a b c d e f g ret)
    ETErlFun8       : ErlTypes [a, b, c, d, e, f, g, h, ret] => ErlType (ErlFun8 a b c d e f g h ret)
    ETErlIOFun0     : ErlTypes [ret]                         => ErlType (ErlIOFun0 ret)
    ETErlIOFun1     : ErlTypes [a, ret]                      => ErlType (ErlIOFun1 a ret)
    ETErlIOFun2     : ErlTypes [a, b, ret]                   => ErlType (ErlIOFun2 a b ret)
    ETErlIOFun3     : ErlTypes [a, b, c, ret]                => ErlType (ErlIOFun3 a b c ret)
    ETErlIOFun4     : ErlTypes [a, b, c, d, ret]             => ErlType (ErlIOFun4 a b c d ret)
    ETErlIOFun5     : ErlTypes [a, b, c, d, e, ret]          => ErlType (ErlIOFun5 a b c d e ret)
    ETErlIOFun6     : ErlTypes [a, b, c, d, e, f, ret]       => ErlType (ErlIOFun6 a b c d e f ret)
    ETErlIOFun7     : ErlTypes [a, b, c, d, e, f, g, ret]    => ErlType (ErlIOFun7 a b c d e f g ret)
    ETErlIOFun8     : ErlTypes [a, b, c, d, e, f, g, h, ret] => ErlType (ErlIOFun8 a b c d e f g h ret)

  ||| A variant of `ErlType` that takes a list of types.
  public export
  data ErlTypes : List Type -> Type where
    ETErlTypesNil   : ErlTypes []
    ETErlTypesCons  : (ErlType x, ErlTypes xs) => ErlTypes (x :: xs)

  ||| A variant of `ErlType` that takes a list of map entries.
  public export
  data ErlMapTypes : List ErlMapEntry -> Type where
    EMTNil : ErlMapTypes []
    EMTCons : (ErlType keyTy, ErlType valueTy) => (key : keyTy) -> ErlMapTypes xs -> ErlMapTypes (MkMapEntry key valueTy :: xs)


text:
||| A `Source` is a monadic streaming function that produces
||| values independently of the input value.
module Rhone.JS.Source

import Control.Category
import Control.Monad.Dom
import Data.MSF
import JS
import Text.Html
import Web.Dom
import Web.Html

%default total

--------------------------------------------------------------------------------
--          Value
--------------------------------------------------------------------------------

public export
interface SafeCast t => HasValue t where
  getValue' : t -> JSIO String

public export
HasValue HTMLButtonElement where
  getValue' = to value

public export
HasValue HTMLDataElement where
  getValue' = to value

public export
HasValue HTMLInputElement where
  getValue' = to value

public export
HasValue HTMLOptionElement where
  getValue' = to value

public export
HasValue HTMLOutputElement where
  getValue' = to value

public export
HasValue HTMLParamElement where
  getValue' = to value

public export
HasValue HTMLSelectElement where
  getValue' = to value

public export
HasValue HTMLTextAreaElement where
  getValue' = to value

public export
HasValue RadioNodeList where
  getValue' = to value

export
getValue : LiftJSIO m => HasValue t => t -> m String
getValue = liftJSIO . getValue'

export
value : LiftJSIO m => HasValue t => MSF m (ElemRef t) String
value = arrM $ \r => getElementByRef r >>= getValue

export %inline
valueOf : LiftJSIO m => HasValue t => ElemRef t -> MSF m i String
valueOf r = const r >>> value

export
meterValue : LiftJSIO m => MSF m (ElemRef HTMLMeterElement) Double
meterValue = arrM $ \r => liftJSIO (getElementByRef r >>= to value)

export %inline
meterValueOf : LiftJSIO m => ElemRef HTMLMeterElement -> MSF m i Double
meterValueOf r = const r >>> meterValue

export
progressValue : LiftJSIO m => MSF m (ElemRef HTMLProgressElement) Double
progressValue = arrM $ \r => liftJSIO (getElementByRef r >>= to value)

export %inline
progressValueOf : LiftJSIO m => ElemRef HTMLProgressElement -> MSF m i Double
progressValueOf r = const r >>> progressValue

--------------------------------------------------------------------------------
--          Checked
--------------------------------------------------------------------------------

export
getChecked : LiftJSIO m => HTMLInputElement -> m Bool
getChecked el = liftJSIO $ get el checked

export
checked : LiftJSIO m => MSF m (ElemRef HTMLInputElement) Bool
checked = arrM getElementByRef >>! getChecked

export %inline
checkedAt : LiftJSIO m => ElemRef HTMLInputElement -> MSF m i Bool
checkedAt r = const r >>> checked

--------------------------------------------------------------------------------
--          Routing
--------------------------------------------------------------------------------

export
windowLocation : LiftJSIO m => MSF m i Location
windowLocation = constM $ liftJSIO (window >>= location)

export
windowHash : LiftJSIO m => MSF m i String
windowHash = windowLocation >>! (liftJSIO . to Location.hash)


text:
module TTImp.ProcessRunElab

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Options
import Core.Normalise
import Core.Reflect
import Core.UnifyState
import Core.Value

import TTImp.Elab
import TTImp.Elab.Check
import TTImp.Elab.RunElab
import TTImp.TTImp

%default covering

export
processRunElab : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
                 RawImp -> Core ()
processRunElab eopts nest env fc tm
    = do defs <- get Ctxt
         unless (isExtension ElabReflection defs) $
             throw (GenericMsg fc "%language ElabReflection not enabled")
         tidx <- resolveName (UN $ Basic "[elaborator script]")
         let n = NS reflectionNS (UN $ Basic "Elab")
         unit <- getCon fc defs (builtin "Unit")
         exp <- appCon fc defs n [unit]

         stm <- checkTerm tidx InExpr eopts nest env tm (gnf env exp)
         ignore $ elabScript fc nest env !(nfOpts withAll defs env stm) Nothing


text:
module CH06

import Data.Vect

Matrix : Nat -> Nat -> Type
Matrix x y = Vect x (Vect y Int)

testMatrix : Matrix 2 3
testMatrix = [[0,0,0], [0,0,0]]

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

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


text:
-- To be type-checked by Idris 2 --
-- Idea origin: @greenest_pig

module MonoidRegardingToFunction

import Data.Nat

--- Interfaces for lawful semigroup and monoid ---

interface S (a : Type) (op : a -> a -> a) where
  opAssoc : (x, y, z : a) -> x `op` (y `op` z) = (x `op` y) `op` z

interface S a op => M (a : Type) (op : a -> a -> a) where
  neu  : a
  neuL : (x : a) -> neu `op` x = x
  neuR : (x : a) -> x `op` neu = x

--- Additive monoid for naturals ---

S Nat (+) where
  opAssoc = plusAssociative

M Nat (+) where
  neu = 0
  neuL _ = Refl
  neuR n = rewrite plusZeroRightNeutral n in Refl

--- Multiplicative monoid for naturals ---

S Nat (*) where
  opAssoc = multAssociative

M Nat (*) where
  neu = 1
  neuL n = rewrite plusZeroRightNeutral n in Refl
  neuR n = rewrite multOneRightNeutral n in Refl

--- Usage example ---

fold : (op : a -> a -> a) -> M a op => List a -> a
fold op [] = neu {a} {op}
fold op (x::xs) = x `op` fold op xs

--- Running example ---

testList : List Nat
testList = [1, 2, 3, 4]

testSum : Nat
testSum = fold (+) testList
-- it is 10!

testMul : Nat
testMul = fold (*) testList
-- it is 24!

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Idris.Syntax

import public Core.Binary
import public Core.Context
import public Core.Context.Log
import public Core.Core
import public Core.FC
import public Core.Normalise
import public Core.Options
import public Core.TTC
import public Core.TT

import TTImp.TTImp

import Libraries.Data.ANameMap
import Data.List
import Data.Maybe
import Data.String
import Libraries.Data.NameMap
import Libraries.Data.SortedMap
import Libraries.Data.String.Extra
import Libraries.Data.StringMap
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Text.PrettyPrint.Prettyprinter.Render.String

import Parser.Lexer.Source

%default covering

public export
data Fixity = InfixL | InfixR | Infix | Prefix

export
Show Fixity where
  show InfixL = "infixl"
  show InfixR = "infixr"
  show Infix  = "infix"
  show Prefix = "prefix"

public export
OpStr' : Type -> Type
OpStr' nm = nm

public export
OpStr : Type
OpStr = OpStr' Name

mutual

  ||| Source language as produced by the parser
  public export
  PTerm : Type
  PTerm = PTerm' Name

  ||| Internal PTerm
  ||| Source language as produced by the unelaboration of core Terms
  ||| KindedNames carry extra information about the nature of the variable
  public export
  IPTerm : Type
  IPTerm = PTerm' KindedName

  ||| The full high level source language
  ||| This gets desugared to RawImp (TTImp.TTImp),
  ||| then elaborated to Term (Core.TT)
  public export
  data PTerm' : Type -> Type where
       -- Direct (more or less) translations to RawImp

       PRef : FC -> nm -> PTerm' nm
       PPi : FC -> RigCount -> PiInfo (PTerm' nm) -> Maybe Name ->
             (argTy : PTerm' nm) -> (retTy : PTerm' nm) -> PTerm' nm
       PLam : FC -> RigCount -> PiInfo (PTerm' nm) -> PTerm' nm ->
              (argTy : PTerm' nm) -> (scope : PTerm' nm) -> PTerm' nm
       PLet : FC -> RigCount -> (pat : PTerm' nm) ->
              (nTy : PTerm' nm) -> (nVal : PTerm' nm) -> (scope : PTerm' nm) ->
              (alts : List (PClause' nm)) -> PTerm' nm
       PCase : FC -> PTerm' nm -> List (PClause' nm) -> PTerm' nm
       PLocal : FC -> List (PDecl' nm) -> (scope : PTerm' nm) -> PTerm' nm
       PUpdate : FC -> List (PFieldUpdate' nm) -> PTerm' nm
       PApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
       PWithApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
       PNamedApp : FC -> PTerm' nm -> Name -> PTerm' nm -> PTerm' nm
       PAutoApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm

       PDelayed : FC -> LazyReason -> PTerm' nm -> PTerm' nm
       PDelay : FC -> PTerm' nm -> PTerm' nm
       PForce : FC -> PTerm' nm -> PTerm' nm

       PSearch : FC -> (depth : Nat) -> PTerm' nm
       PPrimVal : FC -> Constant -> PTerm' nm
       PQuote : FC -> PTerm' nm -> PTerm' nm
       PQuoteName : FC -> Name -> PTerm' nm
       PQuoteDecl : FC -> List (PDecl' nm) -> PTerm' nm
       PUnquote : FC -> PTerm' nm -> PTerm' nm
       PRunElab : FC -> PTerm' nm -> PTerm' nm
       PHole : FC -> (bracket : Bool) -> (holename : String) -> PTerm' nm
       PType : FC -> PTerm' nm
       PAs : FC -> (nameFC : FC) -> Name -> (pattern : PTerm' nm) -> PTerm' nm
       PDotted : FC -> PTerm' nm -> PTerm' nm
       PImplicit : FC -> PTerm' nm
       PInfer : FC -> PTerm' nm

       -- Operators

       POp : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
       PPrefixOp : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm
       PSectionL : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm
       PSectionR : (full, opFC : FC) -> PTerm' nm -> OpStr' nm -> PTerm' nm
       PEq : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
       PBracketed : FC -> PTerm' nm -> PTerm' nm

       -- Syntactic sugar
       PString : FC -> List (PStr' nm) -> PTerm' nm
       PMultiline : FC -> (indent : Nat) -> List (List (PStr' nm)) -> PTerm' nm
       PDoBlock : FC -> Maybe Namespace -> List (PDo' nm) -> PTerm' nm
       PBang : FC -> PTerm' nm -> PTerm' nm
       PIdiom : FC -> PTerm' nm -> PTerm' nm
       PList : (full, nilFC : FC) -> List (FC, PTerm' nm) -> PTerm' nm
                                        -- ^   v location of the conses/snocs
       PSnocList : (full, nilFC : FC) -> List ((FC, PTerm' nm)) -> PTerm' nm
       PPair : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
       PDPair : (full, opFC : FC) -> PTerm' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
       PUnit : FC -> PTerm' nm
       PIfThenElse : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
       PComprehension : FC -> PTerm' nm -> List (PDo' nm) -> PTerm' nm
       PRewrite : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
       -- A list range  [x,y..z]
       PRange : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm -> PTerm' nm
       -- A stream range [x,y..]
       PRangeStream : FC -> PTerm' nm -> Maybe (PTerm' nm) -> PTerm' nm
       -- r.x.y
       PPostfixApp : FC -> PTerm' nm -> List (FC, Name) -> PTerm' nm
       -- .x.y
       PPostfixAppPartial : FC -> List (FC, Name) -> PTerm' nm

       -- Debugging
       PUnifyLog : FC -> LogLevel -> PTerm' nm -> PTerm' nm

       -- with-disambiguation
       PWithUnambigNames : FC -> List Name -> PTerm' nm -> PTerm' nm

  export
  getPTermLoc : PTerm' nm -> FC
  getPTermLoc (PRef fc _) = fc
  getPTermLoc (PPi fc _ _ _ _ _) = fc
  getPTermLoc (PLam fc _ _ _ _ _) = fc
  getPTermLoc (PLet fc _ _ _ _ _ _) = fc
  getPTermLoc (PCase fc _ _) = fc
  getPTermLoc (PLocal fc _ _) = fc
  getPTermLoc (PUpdate fc _) = fc
  getPTermLoc (PApp fc _ _) = fc
  getPTermLoc (PWithApp fc _ _) = fc
  getPTermLoc (PAutoApp fc _ _) = fc
  getPTermLoc (PNamedApp fc _ _ _) = fc
  getPTermLoc (PDelayed fc _ _) = fc
  getPTermLoc (PDelay fc _) = fc
  getPTermLoc (PForce fc _) = fc
  getPTermLoc (PSearch fc _) = fc
  getPTermLoc (PPrimVal fc _) = fc
  getPTermLoc (PQuote fc _) = fc
  getPTermLoc (PQuoteName fc _) = fc
  getPTermLoc (PQuoteDecl fc _) = fc
  getPTermLoc (PUnquote fc _) = fc
  getPTermLoc (PRunElab fc _) = fc
  getPTermLoc (PHole fc _ _) = fc
  getPTermLoc (PType fc) = fc
  getPTermLoc (PAs fc _  _ _) = fc
  getPTermLoc (PDotted fc _) = fc
  getPTermLoc (PImplicit fc) = fc
  getPTermLoc (PInfer fc) = fc
  getPTermLoc (POp fc _ _ _ _) = fc
  getPTermLoc (PPrefixOp fc _ _ _) = fc
  getPTermLoc (PSectionL fc _ _ _) = fc
  getPTermLoc (PSectionR fc _ _ _) = fc
  getPTermLoc (PEq fc _ _) = fc
  getPTermLoc (PBracketed fc _) = fc
  getPTermLoc (PString fc _) = fc
  getPTermLoc (PMultiline fc _ _) = fc
  getPTermLoc (PDoBlock fc _ _) = fc
  getPTermLoc (PBang fc _) = fc
  getPTermLoc (PIdiom fc _) = fc
  getPTermLoc (PList fc _ _) = fc
  getPTermLoc (PSnocList fc _ _) = fc
  getPTermLoc (PPair fc _ _) = fc
  getPTermLoc (PDPair fc _ _ _ _) = fc
  getPTermLoc (PUnit fc) = fc
  getPTermLoc (PIfThenElse fc _ _ _) = fc
  getPTermLoc (PComprehension fc _ _) = fc
  getPTermLoc (PRewrite fc _ _) = fc
  getPTermLoc (PRange fc _ _ _) = fc
  getPTermLoc (PRangeStream fc _ _) = fc
  getPTermLoc (PPostfixApp fc _ _) = fc
  getPTermLoc (PPostfixAppPartial fc _) = fc
  getPTermLoc (PUnifyLog fc _ _) = fc
  getPTermLoc (PWithUnambigNames fc _ _) = fc

  public export
  PFieldUpdate : Type
  PFieldUpdate = PFieldUpdate' Name

  public export
  data PFieldUpdate' : Type -> Type where
       PSetField : (path : List String) -> PTerm' nm -> PFieldUpdate' nm
       PSetFieldApp : (path : List String) -> PTerm' nm -> PFieldUpdate' nm

  public export
  PDo : Type
  PDo = PDo' Name

  public export
  data PDo' : Type -> Type where
       DoExp : FC -> PTerm' nm -> PDo' nm
       DoBind : FC -> (nameFC : FC) -> Name -> PTerm' nm -> PDo' nm
       DoBindPat : FC -> PTerm' nm -> PTerm' nm -> List (PClause' nm) -> PDo' nm
       DoLet : FC -> (lhs : FC) -> Name -> RigCount -> PTerm' nm -> PTerm' nm -> PDo' nm
       DoLetPat : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm -> List (PClause' nm) -> PDo' nm
       DoLetLocal : FC -> List (PDecl' nm) -> PDo' nm
       DoRewrite : FC -> PTerm' nm -> PDo' nm

  public export
  PStr : Type
  PStr = PStr' Name

  public export
  data PStr' : Type -> Type where
       StrLiteral : FC -> String -> PStr' nm
       StrInterp : FC -> PTerm' nm -> PStr' nm

  export
  getLoc : PDo' nm -> FC
  getLoc (DoExp fc _) = fc
  getLoc (DoBind fc _ _ _) = fc
  getLoc (DoBindPat fc _ _ _) = fc
  getLoc (DoLet fc _ _ _ _ _) = fc
  getLoc (DoLetPat fc _ _ _ _) = fc
  getLoc (DoLetLocal fc _) = fc
  getLoc (DoRewrite fc _) = fc

  export
  papply : FC -> PTerm' nm -> List (PTerm' nm) -> PTerm' nm
  papply fc f [] = f
  papply fc f (a :: as) = papply fc (PApp fc f a) as

  export
  applyArgs : PTerm' nm -> List (FC, PTerm' nm) -> PTerm' nm
  applyArgs f [] = f
  applyArgs f ((fc, a) :: args) = applyArgs (PApp fc f a) args

  public export
  PTypeDecl : Type
  PTypeDecl = PTypeDecl' Name

  public export
  data PTypeDecl' : Type -> Type where
       MkPTy : FC -> (nameFC : FC) -> (n : Name) ->
               (doc: String) -> (type : PTerm' nm) -> PTypeDecl' nm

  export
  getPTypeDeclLoc : PTypeDecl' nm -> FC
  getPTypeDeclLoc (MkPTy fc _ _ _ _) = fc

  public export
  PDataDecl : Type
  PDataDecl = PDataDecl' Name

  public export
  data PDataDecl' : Type -> Type where
       MkPData : FC -> (tyname : Name) -> (tycon : PTerm' nm) ->
                 (opts : List DataOpt) ->
                 (datacons : List (PTypeDecl' nm)) -> PDataDecl' nm
       MkPLater : FC -> (tyname : Name) -> (tycon : PTerm' nm) -> PDataDecl' nm

  export
  getPDataDeclLoc : PDataDecl' nm -> FC
  getPDataDeclLoc (MkPData fc _ _ _ _) = fc
  getPDataDeclLoc (MkPLater fc _ _) = fc

  public export
  PClause : Type
  PClause = PClause' Name

  public export
  data PClause' : Type -> Type where
       MkPatClause : FC -> (lhs : PTerm' nm) -> (rhs : PTerm' nm) ->
                     (whereblock : List (PDecl' nm)) -> PClause' nm
       MkWithClause : FC -> (lhs : PTerm' nm) ->
                      (wval : PTerm' nm) -> (prf : Maybe Name) ->
                      List WithFlag -> List (PClause' nm) -> PClause' nm
       MkImpossible : FC -> (lhs : PTerm' nm) -> PClause' nm

  export
  getPClauseLoc : PClause -> FC
  getPClauseLoc (MkPatClause fc _ _ _) = fc
  getPClauseLoc (MkWithClause fc _ _ _ _ _) = fc
  getPClauseLoc (MkImpossible fc _) = fc

  public export
  data Directive : Type where
       Hide : Name -> Directive
       Logging : Maybe LogLevel -> Directive
       LazyOn : Bool -> Directive
       UnboundImplicits : Bool -> Directive
       AmbigDepth : Nat -> Directive
       PairNames : Name -> Name -> Name -> Directive
       RewriteName : Name -> Name -> Directive
       PrimInteger : Name -> Directive
       PrimString : Name -> Directive
       PrimChar : Name -> Directive
       PrimDouble : Name -> Directive
       CGAction : String -> String -> Directive
       Names : Name -> List String -> Directive
       StartExpr : PTerm' nm -> Directive
       Overloadable : Name -> Directive
       Extension : LangExt -> Directive
       DefaultTotality : TotalReq -> Directive
       PrefixRecordProjections : Bool -> Directive
       AutoImplicitDepth : Nat -> Directive
       NFMetavarThreshold : Nat -> Directive
       SearchTimeout : Integer -> Directive

  directiveList : List Directive
  directiveList =
      [ (Hide ph), (Logging Nothing), (LazyOn False)
      , (UnboundImplicits False), (AmbigDepth 0)
      , (PairNames ph ph ph), (RewriteName ph ph)
      , (PrimInteger ph), (PrimString ph), (PrimChar ph)
      , (PrimDouble ph), (CGAction "" ""), (Names ph [])
      , (StartExpr (PRef EmptyFC ph)), (Overloadable ph)
      , (Extension ElabReflection), (DefaultTotality PartialOK)
      , (PrefixRecordProjections True), (AutoImplicitDepth 0)
      , (NFMetavarThreshold 0), (SearchTimeout 0)
      ]

      where
        -- placeholder
        ph : Name
        ph = UN $ Basic ""

  isPragma : Directive -> Bool
  isPragma (CGAction _ _) = False
  isPragma _              = True

  export
  pragmaTopics : String
  pragmaTopics =
    show $ vsep $ map (((<++>) "+") . pretty {ann=()} . showDirective) $ filter isPragma directiveList
    where
      showDirective : Directive -> String
      showDirective (Hide _)             = "%hide name"
      showDirective (Logging _)          = "%logging [topic] lvl"
      showDirective (LazyOn _)           = "%auto_lazy on|off"
      showDirective (UnboundImplicits _) = "%unbound_implicits"
      showDirective (AmbigDepth _)       = "%ambiguity_depth n"
      showDirective (PairNames _ _ _)    = "%pair ty f s"
      showDirective (RewriteName _ _)    = "%rewrite eq rw"
      showDirective (PrimInteger _)      = "%integerLit n"
      showDirective (PrimString _)       = "%stringLit n"
      showDirective (PrimChar _)         = "%charLit n"
      showDirective (PrimDouble _)       = "%doubleLit n"
      showDirective (CGAction _ _)       = "--directive d"
      showDirective (Names _ _)          = "%name ty ns"
      showDirective (StartExpr _)        = "%start expr"
      showDirective (Overloadable _)     = "%allow_overloads"
      showDirective (Extension _)        = "%language"
      showDirective (DefaultTotality _)  =
        "%default partial|total|covering"
      showDirective (PrefixRecordProjections _) =
        "%prefix_record_projections on|off"
      showDirective (AutoImplicitDepth _) =
        "%auto_implicit_depth n"
      showDirective (NFMetavarThreshold _) =
        "%nf_metavar_threshold n"
      showDirective (SearchTimeout _) =
        "%search_timeout ms"

  public export
  PField : Type
  PField = PField' Name

  public export
  data PField' : Type -> Type where
       MkField : FC -> (doc : String) -> RigCount -> PiInfo (PTerm' nm) ->
                 Name -> (ty : PTerm' nm) -> PField' nm

  -- For noting the pass we're in when desugaring a mutual block
  -- TODO: Decide whether we want mutual blocks!
  public export
  data Pass = Single | AsType | AsDef

  export
  Eq Pass where
    Single == Single = True
    AsType == AsType = True
    AsDef == AsDef = True
    _ == _ = False

  export
  typePass : Pass -> Bool
  typePass p = p == Single || p == AsType

  export
  defPass : Pass -> Bool
  defPass p = p == Single || p == AsDef

  public export
  PFnOpt : Type
  PFnOpt = PFnOpt' Name

  public export
  data PFnOpt' : Type -> Type where
       IFnOpt : FnOpt' nm -> PFnOpt' nm
       PForeign : List (PTerm' nm) -> PFnOpt' nm

  public export
  PDecl : Type
  PDecl = PDecl' Name

  public export
  data PDecl' : Type -> Type where
       PClaim : FC -> RigCount -> Visibility -> List (PFnOpt' nm) -> PTypeDecl' nm -> PDecl' nm
       PDef : FC -> List (PClause' nm) -> PDecl' nm
       PData : FC -> (doc : String) -> Visibility -> PDataDecl' nm -> PDecl' nm
       PParameters : FC ->
                     List (Name, RigCount, PiInfo (PTerm' nm), PTerm' nm) ->
                     List (PDecl' nm) -> PDecl' nm
       PUsing : FC -> List (Maybe Name, PTerm' nm) ->
                List (PDecl' nm) -> PDecl' nm
       PReflect : FC -> PTerm' nm -> PDecl' nm
       PInterface : FC ->
                    Visibility ->
                    (constraints : List (Maybe Name, PTerm' nm)) ->
                    Name ->
                    (doc : String) ->
                    (params : List (Name, (RigCount, PTerm' nm))) ->
                    (det : List Name) ->
                    (conName : Maybe Name) ->
                    List (PDecl' nm) ->
                    PDecl' nm
       PImplementation : FC ->
                         Visibility -> List PFnOpt -> Pass ->
                         (implicits : List (Name, RigCount, PTerm' nm)) ->
                         (constraints : List (Maybe Name, PTerm' nm)) ->
                         Name ->
                         (params : List (PTerm' nm)) ->
                         (implName : Maybe Name) ->
                         (nusing : List Name) ->
                         Maybe (List (PDecl' nm)) ->
                         PDecl' nm
       PRecord : FC ->
                 (doc : String) ->
                 Visibility ->
                 Name ->
                 (params : List (Name, RigCount, PiInfo (PTerm' nm), PTerm' nm)) ->
                 (conName : Maybe Name) ->
                 List (PField' nm) ->
                 PDecl' nm

       -- TODO: PPostulate
       -- TODO: POpen (for opening named interfaces)
       PMutual : FC -> List (PDecl' nm) -> PDecl' nm
       PFixity : FC -> Fixity -> Nat -> OpStr -> PDecl' nm
       PNamespace : FC -> Namespace -> List (PDecl' nm) -> PDecl' nm
       PTransform : FC -> String -> PTerm' nm -> PTerm' nm -> PDecl' nm
       PRunElabDecl : FC -> PTerm' nm -> PDecl' nm
       PDirective : FC -> Directive -> PDecl' nm
       PBuiltin : FC -> BuiltinType -> Name -> PDecl' nm

  export
  getPDeclLoc : PDecl' nm -> FC
  getPDeclLoc (PClaim fc _ _ _ _) = fc
  getPDeclLoc (PDef fc _) = fc
  getPDeclLoc (PData fc _ _ _) = fc
  getPDeclLoc (PParameters fc _ _) = fc
  getPDeclLoc (PUsing fc _ _) = fc
  getPDeclLoc (PReflect fc _) = fc
  getPDeclLoc (PInterface fc _ _ _ _ _ _ _ _) = fc
  getPDeclLoc (PImplementation fc _ _ _ _ _ _ _ _ _ _) = fc
  getPDeclLoc (PRecord fc _ _ _ _ _ _) = fc
  getPDeclLoc (PMutual fc _) = fc
  getPDeclLoc (PFixity fc _ _ _) = fc
  getPDeclLoc (PNamespace fc _ _) = fc
  getPDeclLoc (PTransform fc _ _ _) = fc
  getPDeclLoc (PRunElabDecl fc _) = fc
  getPDeclLoc (PDirective fc _) = fc
  getPDeclLoc (PBuiltin fc _ _) = fc

export
isStrInterp : PStr -> Maybe FC
isStrInterp (StrInterp fc _) = Just fc
isStrInterp (StrLiteral _ _) = Nothing

export
isPDef : PDecl -> Maybe (FC, List PClause)
isPDef (PDef annot cs) = Just (annot, cs)
isPDef _ = Nothing

definedInData : PDataDecl -> List Name
definedInData (MkPData _ n _ _ cons) = n :: map getName cons
  where
    getName : PTypeDecl -> Name
    getName (MkPTy _ _ n _ _) = n
definedInData (MkPLater _ n _) = [n]

export
definedIn : List PDecl -> List Name
definedIn [] = []
definedIn (PClaim _ _ _ _ (MkPTy _ _ n _ _) :: ds) = n :: definedIn ds
definedIn (PData _ _ _ d :: ds) = definedInData d ++ definedIn ds
definedIn (PParameters _ _ pds :: ds) = definedIn pds ++ definedIn ds
definedIn (PUsing _ _ pds :: ds) = definedIn pds ++ definedIn ds
definedIn (PNamespace _ _ ns :: ds) = definedIn ns ++ definedIn ds
definedIn (_ :: ds) = definedIn ds

public export
data REPLEval : Type where
     EvalTC : REPLEval -- Evaluate as if part of the typechecker
     NormaliseAll : REPLEval -- Normalise everything (default)
     Execute : REPLEval -- Evaluate then pass to an executer

export
Show REPLEval where
  show EvalTC = "typecheck"
  show NormaliseAll = "normalise"
  show Execute = "execute"

export
Pretty REPLEval where
  pretty EvalTC = pretty "typecheck"
  pretty NormaliseAll = pretty "normalise"
  pretty Execute = pretty "execute"

public export
data REPLOpt : Type where
     ShowImplicits : Bool -> REPLOpt
     ShowNamespace : Bool -> REPLOpt
     ShowTypes : Bool -> REPLOpt
     EvalMode : REPLEval -> REPLOpt
     Editor : String -> REPLOpt
     CG : String -> REPLOpt
     Profile : Bool -> REPLOpt

export
Show REPLOpt where
  show (ShowImplicits impl) = "showimplicits = " ++ show impl
  show (ShowNamespace ns) = "shownamespace = " ++ show ns
  show (ShowTypes typs) = "showtypes = " ++ show typs
  show (EvalMode mod) = "eval = " ++ show mod
  show (Editor editor) = "editor = " ++ show editor
  show (CG str) = "cg = " ++ str
  show (Profile p) = "profile = " ++ show p

export
Pretty REPLOpt where
  pretty (ShowImplicits impl) = pretty "showimplicits" <++> equals <++> pretty impl
  pretty (ShowNamespace ns) = pretty "shownamespace" <++> equals <++> pretty ns
  pretty (ShowTypes typs) = pretty "showtypes" <++> equals <++> pretty typs
  pretty (EvalMode mod) = pretty "eval" <++> equals <++> pretty mod
  pretty (Editor editor) = pretty "editor" <++> equals <++> pretty editor
  pretty (CG str) = pretty "cg" <++> equals <++> pretty str
  pretty (Profile p) = pretty "profile" <++> equals <++> pretty p

public export
data EditCmd : Type where
     TypeAt : Int -> Int -> Name -> EditCmd
     CaseSplit : Bool -> Int -> Int -> Name -> EditCmd
     AddClause : Bool -> Int -> Name -> EditCmd
     ExprSearch : Bool -> Int -> Name -> List Name -> EditCmd
     ExprSearchNext : EditCmd
     GenerateDef : Bool -> Int -> Name -> Nat -> EditCmd
     GenerateDefNext : EditCmd
     MakeLemma : Bool -> Int -> Name -> EditCmd
     MakeCase : Bool -> Int -> Name -> EditCmd
     MakeWith : Bool -> Int -> Name -> EditCmd

public export
data REPLCmd : Type where
     NewDefn : List PDecl -> REPLCmd
     Eval : PTerm -> REPLCmd
     Check : PTerm -> REPLCmd
     CheckWithImplicits : PTerm -> REPLCmd
     PrintDef : Name -> REPLCmd
     Reload : REPLCmd
     Load : String -> REPLCmd
     ImportMod : ModuleIdent -> REPLCmd
     Edit : REPLCmd
     Compile : PTerm -> String -> REPLCmd
     Exec : PTerm -> REPLCmd
     Help : REPLCmd
     TypeSearch : PTerm -> REPLCmd
     FuzzyTypeSearch : PTerm -> REPLCmd
     DebugInfo : Name -> REPLCmd
     SetOpt : REPLOpt -> REPLCmd
     GetOpts : REPLCmd
     CGDirective : String -> REPLCmd
     CD : String -> REPLCmd
     CWD: REPLCmd
     Missing : Name -> REPLCmd
     Total : Name -> REPLCmd
     Doc : PTerm -> REPLCmd
     Browse : Namespace -> REPLCmd
     SetLog : Maybe LogLevel -> REPLCmd
     SetConsoleWidth : Maybe Nat -> REPLCmd
     SetColor : Bool -> REPLCmd
     Metavars : REPLCmd
     Editing : EditCmd -> REPLCmd
     RunShellCommand : String -> REPLCmd
     ShowVersion : REPLCmd
     Quit : REPLCmd
     NOP : REPLCmd
     ImportPackage : String -> REPLCmd

public export
record Import where
  constructor MkImport
  loc : FC
  reexport : Bool
  path : ModuleIdent
  nameAs : Namespace

public export
record Module where
  constructor MkModule
  headerLoc : FC
  moduleNS : ModuleIdent
  imports : List Import
  documentation : String
  decls : List PDecl

parameters {0 nm : Type} (toName : nm -> Name)

  showAlt : PClause' nm -> String
  showDo : PDo' nm -> String
  showPStr : PStr' nm -> String
  showUpdate : PFieldUpdate' nm -> String
  showPTermPrec : Prec -> PTerm' nm -> String
  showOpPrec : Prec -> OpStr' nm -> String

  showPTerm : PTerm' nm -> String
  showPTerm = showPTermPrec Open

  showAlt (MkPatClause _ lhs rhs _) =
    " | " ++ showPTerm lhs ++ " => " ++ showPTerm rhs ++ ";"
  showAlt (MkWithClause _ lhs wval prf flags cs) = " | <<with alts not possible>>;"
  showAlt (MkImpossible _ lhs) = " | " ++ showPTerm lhs ++ " impossible;"

  showDo (DoExp _ tm) = showPTerm tm
  showDo (DoBind _ _ n tm) = show n ++ " <- " ++ showPTerm tm
  showDo (DoBindPat _ l tm alts)
      = showPTerm l ++ " <- " ++ showPTerm tm ++ concatMap showAlt alts
  showDo (DoLet _ _ l rig _ tm) = "let " ++ show l ++ " = " ++ showPTerm tm
  showDo (DoLetPat _ l _ tm alts)
      = "let " ++ showPTerm l ++ " = " ++ showPTerm tm ++ concatMap showAlt alts
  showDo (DoLetLocal _ ds)
      -- We'll never see this when displaying a normal form...
      = "let { << definitions >>  }"
  showDo (DoRewrite _ rule)
      = "rewrite " ++ showPTerm rule

  showPStr (StrLiteral _ str) = show str
  showPStr (StrInterp _ tm) = showPTerm tm

  showUpdate (PSetField p v) = showSep "." p ++ " = " ++ showPTerm v
  showUpdate (PSetFieldApp p v) = showSep "." p ++ " $= " ++ showPTerm v

  showPTermPrec d (PRef _ n) = showPrec d (toName n)
  showPTermPrec d (PPi _ rig Explicit Nothing arg ret)
        = showPTermPrec d arg ++ " -> " ++ showPTermPrec d ret
  showPTermPrec d (PPi _ rig Explicit (Just n) arg ret)
        = "(" ++ showCount rig ++ showPrec d n
         ++ " : " ++ showPTermPrec d arg ++ ") -> "
         ++ showPTermPrec d ret
  showPTermPrec d (PPi _ rig Implicit Nothing arg ret) -- shouldn't happen
        = "{" ++ showCount rig ++ "_ : " ++ showPTermPrec d arg ++ "} -> "
          ++ showPTermPrec d ret
  showPTermPrec d (PPi _ rig Implicit (Just n) arg ret)
        = "{" ++ showCount rig ++ showPrec d n ++ " : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret
  showPTermPrec d (PPi _ top AutoImplicit Nothing arg ret)
        = showPTermPrec d arg ++ " => " ++ showPTermPrec d ret
  showPTermPrec d (PPi _ rig AutoImplicit (Just n) arg ret)
        = "{auto " ++ showCount rig ++ showPrec d n ++ " : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret
  showPTermPrec d (PPi _ rig (DefImplicit t) Nothing arg ret) -- shouldn't happen
        = "{default " ++ showPTermPrec App t ++ " " ++ showCount rig ++ "_ : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret
  showPTermPrec d (PPi _ rig (DefImplicit t) (Just n) arg ret)
        = "{default " ++ showPTermPrec App t ++ " " ++ showCount rig ++ showPrec d n ++ " : " ++ showPTermPrec d arg ++ "} -> " ++ showPTermPrec d ret
  showPTermPrec d (PLam _ rig _ n (PImplicit _) sc)
        = "\\" ++ showCount rig ++ showPTermPrec d n ++ " => " ++ showPTermPrec d sc
  showPTermPrec d (PLam _ rig _ n ty sc)
        = "\\" ++ showCount rig ++ showPTermPrec d n ++ " : " ++ showPTermPrec d ty ++ " => " ++ showPTermPrec d sc
  showPTermPrec d (PLet _ rig n (PImplicit _) val sc alts)
        = "let " ++ showCount rig ++ showPTermPrec d n ++ " = " ++ showPTermPrec d val ++ " in " ++ showPTermPrec d sc
  showPTermPrec d (PLet _ rig n ty val sc alts)
        = "let " ++ showCount rig ++ showPTermPrec d n ++ " : " ++ showPTermPrec d ty ++ " = "
                 ++ showPTermPrec d val ++ concatMap showAlt alts ++
                 " in " ++ showPTermPrec d sc
      where
        showAlt : PClause' nm -> String
        showAlt (MkPatClause _ lhs rhs _) = " | " ++ showPTerm lhs ++ " => " ++ showPTerm rhs ++ ";"
        showAlt (MkWithClause _ lhs rhs prf flags _) = " | <<with alts not possible>>"
        showAlt (MkImpossible _ lhs) = " | " ++ showPTerm lhs ++ " impossible;"
  showPTermPrec _ (PCase _ tm cs)
        = "case " ++ showPTerm tm ++ " of { " ++
            showSep " ; " (map showCase cs) ++ " }"
      where
        showCase : PClause' nm -> String
        showCase (MkPatClause _ lhs rhs _) = showPTerm lhs ++ " => " ++ showPTerm rhs
        showCase (MkWithClause _ lhs rhs _ flags _) = " | <<with alts not possible>>"
        showCase (MkImpossible _ lhs) = showPTerm lhs ++ " impossible"
  showPTermPrec d (PLocal _ ds sc) -- We'll never see this when displaying a normal form...
        = "let { << definitions >>  } in " ++ showPTermPrec d sc
  showPTermPrec d (PUpdate _ fs)
        = "record { " ++ showSep ", " (map showUpdate fs) ++ " }"
  showPTermPrec d (PApp _ f a) =
      let catchall : Lazy String := showPTermPrec App f ++ " " ++ showPTermPrec App a in
      case f of
        PRef _ n =>
          if isJust (isRF (toName n))
          then showPTermPrec App a ++ " " ++ showPTermPrec App f
          else catchall
        _ => catchall
  showPTermPrec d (PWithApp _ f a) = showPTermPrec d f ++ " | " ++ showPTermPrec d a
  showPTermPrec d (PAutoApp _ f a)
        = showPTermPrec d f ++ " @{" ++ showPTermPrec d a ++ "}"
  showPTermPrec d (PDelayed _ LInf ty)
        = showParens (d >= App) $ "Inf " ++ showPTermPrec App ty
  showPTermPrec d (PDelayed _ _ ty)
        = showParens (d >= App) $ "Lazy " ++ showPTermPrec App ty
  showPTermPrec d (PDelay _ tm)
        = showParens (d >= App) $ "Delay " ++ showPTermPrec App tm
  showPTermPrec d (PForce _ tm)
        = showParens (d >= App) $ "Force " ++ showPTermPrec App tm
  showPTermPrec d (PNamedApp _ f n (PRef _ a))
        = if n == (toName a)
             then showPTermPrec d f ++ " {" ++ showPrec d n ++ "}"
             else showPTermPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d (toName a) ++ "}"
  showPTermPrec d (PNamedApp _ f n a)
        = showPTermPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPTermPrec d a ++ "}"
  showPTermPrec _ (PSearch _ _) = "%search"
  showPTermPrec d (PQuote _ tm) = "`(" ++ showPTermPrec d tm ++ ")"
  showPTermPrec d (PQuoteName _ n) = "`{" ++ showPrec d n ++ "}"
  showPTermPrec d (PQuoteDecl _ tm) = "`[ <<declaration>> ]"
  showPTermPrec d (PUnquote _ tm) = "~(" ++ showPTermPrec d tm ++ ")"
  showPTermPrec d (PRunElab _ tm) = "%runElab " ++ showPTermPrec d tm
  showPTermPrec d (PPrimVal _ c) = showPrec d c
  showPTermPrec _ (PHole _ _ n) = "?" ++ n
  showPTermPrec _ (PType _) = "Type"
  showPTermPrec d (PAs _ _ n p) = showPrec d n ++ "@" ++ showPTermPrec d p
  showPTermPrec d (PDotted _ p) = "." ++ showPTermPrec d p
  showPTermPrec _ (PImplicit _) = "_"
  showPTermPrec _ (PInfer _) = "?"
  showPTermPrec d (POp _ _ op x y) = showPTermPrec d x ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d y
  showPTermPrec d (PPrefixOp _ _ op x) = showOpPrec d op ++ showPTermPrec d x
  showPTermPrec d (PSectionL _ _ op x) = "(" ++ showOpPrec d op ++ " " ++ showPTermPrec d x ++ ")"
  showPTermPrec d (PSectionR _ _ x op) = "(" ++ showPTermPrec d x ++ " " ++ showOpPrec d op ++ ")"
  showPTermPrec d (PEq fc l r) = showPTermPrec d l ++ " = " ++ showPTermPrec d r
  showPTermPrec d (PBracketed _ tm) = "(" ++ showPTermPrec d tm ++ ")"
  showPTermPrec d (PString _ xs) = join " ++ " $ showPStr <$> xs
  showPTermPrec d (PMultiline _ indent xs) = "multiline (" ++ (join " ++ " $ showPStr <$> concat xs) ++ ")"
  showPTermPrec d (PDoBlock _ ns ds)
        = "do " ++ showSep " ; " (map showDo ds)
  showPTermPrec d (PBang _ tm) = "!" ++ showPTermPrec d tm
  showPTermPrec d (PIdiom _ tm) = "[|" ++ showPTermPrec d tm ++ "|]"
  showPTermPrec d (PList _ _ xs)
        = "[" ++ showSep ", " (map (showPTermPrec d . snd) xs) ++ "]"
  showPTermPrec d (PSnocList _ _ xs)
        = "[<" ++ showSep ", " (map (showPTermPrec d . snd) xs) ++ "]"
  showPTermPrec d (PPair _ l r) = "(" ++ showPTermPrec d l ++ ", " ++ showPTermPrec d r ++ ")"
  showPTermPrec d (PDPair _ _ l (PImplicit _) r) = "(" ++ showPTermPrec d l ++ " ** " ++ showPTermPrec d r ++ ")"
  showPTermPrec d (PDPair _ _ l ty r) = "(" ++ showPTermPrec d l ++ " : " ++ showPTermPrec d ty ++
                                 " ** " ++ showPTermPrec d r ++ ")"
  showPTermPrec _ (PUnit _) = "()"
  showPTermPrec d (PIfThenElse _ x t e) = "if " ++ showPTermPrec d x ++ " then " ++ showPTermPrec d t ++
                                 " else " ++ showPTermPrec d e
  showPTermPrec d (PComprehension _ ret es)
        = "[" ++ showPTermPrec d (dePure ret) ++ " | " ++
                 showSep ", " (map (showDo . deGuard) es) ++ "]"
      where
        dePure : PTerm' nm -> PTerm' nm
        dePure tm@(PApp _ (PRef _ n) arg)
            = if dropNS (toName n) == UN (Basic "pure") then arg else tm
        dePure tm = tm

        deGuard : PDo' nm -> PDo' nm
        deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg))
            = if dropNS (toName n) == UN (Basic "guard") then DoExp fc arg else tm
        deGuard tm = tm
  showPTermPrec d (PRewrite _ rule tm)
        = "rewrite " ++ showPTermPrec d rule ++ " in " ++ showPTermPrec d tm
  showPTermPrec d (PRange _ start Nothing end)
        = "[" ++ showPTermPrec d start ++ " .. " ++ showPTermPrec d end ++ "]"
  showPTermPrec d (PRange _ start (Just next) end)
        = "[" ++ showPTermPrec d start ++ ", " ++ showPTermPrec d next ++ " .. " ++ showPTermPrec d end ++ "]"
  showPTermPrec d (PRangeStream _ start Nothing)
        = "[" ++ showPTermPrec d start ++ " .. ]"
  showPTermPrec d (PRangeStream _ start (Just next))
        = "[" ++ showPTermPrec d start ++ ", " ++ showPTermPrec d next ++ " .. ]"
  showPTermPrec d (PUnifyLog _ _ tm) = showPTermPrec d tm
  showPTermPrec d (PPostfixApp fc rec fields)
        = showPTermPrec d rec ++ concatMap (\n => "." ++ show n) fields
  showPTermPrec d (PPostfixAppPartial fc fields)
        = concatMap (\n => "." ++ show n) fields
  showPTermPrec d (PWithUnambigNames fc ns rhs)
        = "with " ++ show ns ++ " " ++ showPTermPrec d rhs

  showOpPrec d op = let op = toName op in
    if isOpName op
    then        showPrec d op
    else "`" ++ showPrec d op ++ "`"

export
Show PTerm where
  showPrec = showPTermPrec id

export
Show IPTerm where
  showPrec = showPTermPrec rawName

public export
record Method where
  constructor MkMethod
  name     : Name
  count    : RigCount
  totalReq : Maybe TotalReq
  type     : RawImp

export
Show Method where
  show (MkMethod n c treq ty)
    = "[" ++ show treq ++ "] " ++ show c ++ " " ++ show n ++ " : " ++ show ty

public export
record IFaceInfo where
  constructor MkIFaceInfo
  iconstructor : Name
  implParams : List Name
  params : List Name
  parents : List RawImp
  methods : List Method
     -- ^ name, whether a data method, and desugared type (without constraint)
  defaults : List (Name, List ImpClause)

export
TTC Method where
  toBuf b (MkMethod nm c treq ty)
      = do toBuf b nm
           toBuf b c
           toBuf b treq
           toBuf b ty

  fromBuf b
      = do nm <- fromBuf b
           c <- fromBuf b
           treq <- fromBuf b
           ty <- fromBuf b
           pure (MkMethod nm c treq ty)

export
TTC IFaceInfo where
  toBuf b (MkIFaceInfo ic impps ps cs ms ds)
      = do toBuf b ic
           toBuf b impps
           toBuf b ps
           toBuf b cs
           toBuf b ms
           toBuf b ds

  fromBuf b
      = do ic <- fromBuf b
           impps <- fromBuf b
           ps <- fromBuf b
           cs <- fromBuf b
           ms <- fromBuf b
           ds <- fromBuf b
           pure (MkIFaceInfo ic impps ps cs ms ds)

-- If you update this, update 'extendSyn' in Desugar to keep it up to date
-- when reading imports
public export
record SyntaxInfo where
  constructor MkSyntax
  -- Keep infix/prefix, then we can define operators which are both
  -- (most obviously, -)
  infixes : StringMap (Fixity, Nat)
  prefixes : StringMap Nat
  -- info about modules
  saveMod : List ModuleIdent -- current module name
  modDocstrings : SortedMap ModuleIdent String
  -- info about interfaces
  saveIFaces : List Name -- interfaces defined in current session, to save
                         -- to ttc
  ifaces : ANameMap IFaceInfo
  -- info about definitions
  saveDocstrings : NameMap () -- names defined in current session
  defDocstrings : ANameMap String
  bracketholes : List Name -- hole names in argument position (so need
                           -- to be bracketed when solved)
  usingImpl : List (Maybe Name, RawImp)
  startExpr : RawImp

export
TTC Fixity where
  toBuf b InfixL = tag 0
  toBuf b InfixR = tag 1
  toBuf b Infix = tag 2
  toBuf b Prefix = tag 3

  fromBuf b
      = case !getTag of
             0 => pure InfixL
             1 => pure InfixR
             2 => pure Infix
             3 => pure Prefix
             _ => corrupt "Fixity"

export
TTC SyntaxInfo where
  toBuf b syn
      = do toBuf b (StringMap.toList (infixes syn))
           toBuf b (StringMap.toList (prefixes syn))
           toBuf b (filter (\n => elemBy (==) (fst n) (saveMod syn))
                           (SortedMap.toList $ modDocstrings syn))
           toBuf b (filter (\n => fst n `elem` saveIFaces syn)
                           (ANameMap.toList (ifaces syn)))
           toBuf b (filter (\n => isJust (lookup (fst n) (saveDocstrings syn)))
                           (ANameMap.toList (defDocstrings syn)))
           toBuf b (bracketholes syn)
           toBuf b (startExpr syn)

  fromBuf b
      = do inf <- fromBuf b
           pre <- fromBuf b
           moddstr <- fromBuf b
           ifs <- fromBuf b
           defdstrs <- fromBuf b
           bhs <- fromBuf b
           start <- fromBuf b
           pure $ MkSyntax (fromList inf) (fromList pre)
                   [] (fromList moddstr)
                   [] (fromList ifs)
                   empty (fromList defdstrs)
                   bhs
                   [] start

HasNames IFaceInfo where
  full gam iface
      = do -- coreLift $ printLn (iconstructor iface)
           -- coreLift $ printLn (methods iface)
           pure iface

  resolved gam iface = pure iface

HasNames a => HasNames (ANameMap a) where
  full gam nmap
      = insertAll empty (toList nmap)
    where
      insertAll : ANameMap a -> List (Name, a) -> Core (ANameMap a)
      insertAll ms [] = pure ms
      insertAll ms ((k, v) :: ns)
          = insertAll (addName !(full gam k) !(full gam v) ms) ns

  resolved gam nmap
      = insertAll empty (toList nmap)
    where
      insertAll : ANameMap a -> List (Name, a) -> Core (ANameMap a)
      insertAll ms [] = pure ms
      insertAll ms ((k, v) :: ns)
          = insertAll (addName !(resolved gam k) !(resolved gam v) ms) ns

export
HasNames SyntaxInfo where
  full gam syn
      = pure $ record { ifaces = !(full gam (ifaces syn)),
                        bracketholes = !(traverse (full gam) (bracketholes syn))
                      } syn
  resolved gam syn
      = pure $ record { ifaces = !(resolved gam (ifaces syn)),
                        bracketholes = !(traverse (resolved gam) (bracketholes syn))
                      } syn

export
initSyntax : SyntaxInfo
initSyntax
    = MkSyntax initInfix
               initPrefix
               []
               empty
               []
               empty
               initSaveDocStrings
               initDocStrings
               []
               []
               (IVar EmptyFC (UN $ Basic "main"))

  where

    initInfix : StringMap (Fixity, Nat)
    initInfix = insert "=" (Infix, 0) empty

    initPrefix : StringMap Nat
    initPrefix = fromList
      [ ("-", 10)
      , ("negate", 10) -- for documentation purposes
      ]

    initDocStrings : ANameMap String
    initDocStrings = empty

    initSaveDocStrings : NameMap ()
    initSaveDocStrings = empty

-- A label for Syntax info in the global state
export
data Syn : Type where

export
withSyn : {auto s : Ref Syn SyntaxInfo} -> Core a -> Core a
withSyn = wrapRef Syn (\_ => pure ())

export
mapPTermM : (PTerm' nm -> Core (PTerm' nm)) -> PTerm' nm -> Core (PTerm' nm)
mapPTermM f = goPTerm where

  mutual

    goPTerm : PTerm' nm -> Core (PTerm' nm)
    goPTerm t@(PRef _ _) = f t
    goPTerm (PPi fc x info z argTy retTy) =
      PPi fc x <$> goPiInfo info
               <*> pure z
               <*> goPTerm argTy
               <*> goPTerm retTy
      >>= f
    goPTerm (PLam fc x info z argTy scope) =
      PLam fc x <$> goPiInfo info
                <*> pure z
                <*> goPTerm argTy
                <*> goPTerm scope
      >>= f
    goPTerm (PLet fc x pat nTy nVal scope alts) =
      PLet fc x <$> goPTerm pat
                <*> goPTerm nTy
                <*> goPTerm nVal
                <*> goPTerm scope
                <*> goPClauses alts
      >>= f
    goPTerm (PCase fc x xs) =
      PCase fc <$> goPTerm x
               <*> goPClauses xs
      >>= f
    goPTerm (PLocal fc xs scope) =
      PLocal fc <$> goPDecls xs
                <*> goPTerm scope
      >>= f
    goPTerm (PUpdate fc xs) =
      PUpdate fc <$> goPFieldUpdates xs
      >>= f
    goPTerm (PApp fc x y) =
      PApp fc <$> goPTerm x
              <*> goPTerm y
      >>= f
    goPTerm (PWithApp fc x y) =
      PWithApp fc <$> goPTerm x
                  <*> goPTerm y
      >>= f
    goPTerm (PAutoApp fc x y) =
      PAutoApp fc <$> goPTerm x
                         <*> goPTerm y
      >>= f
    goPTerm (PNamedApp fc x n y) =
      PNamedApp fc <$> goPTerm x
                   <*> pure n
                   <*> goPTerm y
      >>= f
    goPTerm (PDelayed fc x y) =
      PDelayed fc x <$> goPTerm y
      >>= f
    goPTerm (PDelay fc x) =
      PDelay fc <$> goPTerm x
      >>= f
    goPTerm (PForce fc x) =
      PForce fc <$> goPTerm x
      >>= f
    goPTerm t@(PSearch _ _) = f t
    goPTerm t@(PPrimVal _ _) = f t
    goPTerm (PQuote fc x) =
      PQuote fc <$> goPTerm x
      >>= f
    goPTerm t@(PQuoteName _ _) = f t
    goPTerm (PQuoteDecl fc x) =
      PQuoteDecl fc <$> traverse goPDecl x
      >>= f
    goPTerm (PUnquote fc x) =
      PUnquote fc <$> goPTerm x
      >>= f
    goPTerm (PRunElab fc x) =
      PRunElab fc <$> goPTerm x
      >>= f
    goPTerm t@(PHole _ _ _) = f t
    goPTerm t@(PType _) = f t
    goPTerm (PAs fc nameFC x pat) =
      PAs fc nameFC x <$> goPTerm pat
      >>= f
    goPTerm (PDotted fc x) =
      PDotted fc <$> goPTerm x
      >>= f
    goPTerm t@(PImplicit _) = f t
    goPTerm t@(PInfer _) = f t
    goPTerm (POp fc opFC x y z) =
      POp fc opFC x <$> goPTerm y
                    <*> goPTerm z
      >>= f
    goPTerm (PPrefixOp fc opFC x y) =
      PPrefixOp fc opFC x <$> goPTerm y
      >>= f
    goPTerm (PSectionL fc opFC x y) =
      PSectionL fc opFC x <$> goPTerm y
      >>= f
    goPTerm (PSectionR fc opFC x y) =
      PSectionR fc opFC <$> goPTerm x
                   <*> pure y
      >>= f
    goPTerm (PEq fc x y) =
      PEq fc <$> goPTerm x
             <*> goPTerm y
      >>= f
    goPTerm (PBracketed fc x) =
      PBracketed fc <$> goPTerm x
      >>= f
    goPTerm (PString fc xs) =
      PString fc <$> goPStrings xs
      >>= f
    goPTerm (PMultiline fc x ys) =
      PMultiline fc x <$> goPStringLines ys
      >>= f
    goPTerm (PDoBlock fc ns xs) =
      PDoBlock fc ns <$> goPDos xs
      >>= f
    goPTerm (PBang fc x) =
      PBang fc <$> goPTerm x
      >>= f
    goPTerm (PIdiom fc x) =
      PIdiom fc <$> goPTerm x
      >>= f
    goPTerm (PList fc nilFC xs) =
      PList fc nilFC <$> goPairedPTerms xs
      >>= f
    goPTerm (PSnocList fc nilFC xs) =
      PSnocList fc nilFC <$> goPairedPTerms xs
      >>= f
    goPTerm (PPair fc x y) =
      PPair fc <$> goPTerm x
               <*> goPTerm y
      >>= f
    goPTerm (PDPair fc opFC x y z) =
      PDPair fc opFC
                <$> goPTerm x
                <*> goPTerm y
                <*> goPTerm z
      >>= f
    goPTerm t@(PUnit _) = f t
    goPTerm (PIfThenElse fc x y z) =
      PIfThenElse fc <$> goPTerm x
                     <*> goPTerm y
                     <*> goPTerm z
      >>= f
    goPTerm (PComprehension fc x xs) =
      PComprehension fc <$> goPTerm x
                        <*> goPDos xs
      >>= f
    goPTerm (PRewrite fc x y) =
      PRewrite fc <$> goPTerm x
                  <*> goPTerm y
      >>= f
    goPTerm (PRange fc x y z) =
      PRange fc <$> goPTerm x
                <*> goMPTerm y
                <*> goPTerm z
      >>= f
    goPTerm (PRangeStream fc x y) =
      PRangeStream fc <$> goPTerm x
                      <*> goMPTerm y
      >>= f
    goPTerm (PUnifyLog fc k x) =
      PUnifyLog fc k <$> goPTerm x
      >>= f
    goPTerm (PPostfixApp fc rec fields) =
      PPostfixApp fc <$> goPTerm rec <*> pure fields
      >>= f
    goPTerm (PPostfixAppPartial fc fields) =
      f (PPostfixAppPartial fc fields)
    goPTerm (PWithUnambigNames fc ns rhs) =
      PWithUnambigNames fc ns <$> goPTerm rhs
      >>= f

    goPFieldUpdate : PFieldUpdate' nm -> Core (PFieldUpdate' nm)
    goPFieldUpdate (PSetField p t)    = PSetField p <$> goPTerm t
    goPFieldUpdate (PSetFieldApp p t) = PSetFieldApp p <$> goPTerm t

    goPStr : PStr' nm -> Core (PStr' nm)
    goPStr (StrInterp fc t) = StrInterp fc <$> goPTerm t
    goPStr x                = pure x

    goPDo : PDo' nm -> Core (PDo' nm)
    goPDo (DoExp fc t) = DoExp fc <$> goPTerm t
    goPDo (DoBind fc nameFC n t) = DoBind fc nameFC n <$> goPTerm t
    goPDo (DoBindPat fc t u cls) =
      DoBindPat fc <$> goPTerm t
                   <*> goPTerm u
                   <*> goPClauses cls
    goPDo (DoLet fc lhsFC n c t scope) =
       DoLet fc lhsFC n c <$> goPTerm t
                          <*> goPTerm scope
    goPDo (DoLetPat fc pat t scope cls) =
       DoLetPat fc <$> goPTerm pat
                   <*> goPTerm t
                   <*> goPTerm scope
                   <*> goPClauses cls
    goPDo (DoLetLocal fc decls) = DoLetLocal fc <$> goPDecls decls
    goPDo (DoRewrite fc t) = DoRewrite fc <$> goPTerm t

    goPClause : PClause' nm -> Core (PClause' nm)
    goPClause (MkPatClause fc lhs rhs wh) =
      MkPatClause fc <$> goPTerm lhs
                     <*> goPTerm rhs
                     <*> goPDecls wh
    goPClause (MkWithClause fc lhs wVal prf flags cls) =
      MkWithClause fc <$> goPTerm lhs
                      <*> goPTerm wVal
                      <*> pure prf
                      <*> pure flags
                      <*> goPClauses cls
    goPClause (MkImpossible fc lhs) = MkImpossible fc <$> goPTerm lhs

    goPDecl : PDecl' nm -> Core (PDecl' nm)
    goPDecl (PClaim fc c v opts tdecl) =
      PClaim fc c v <$> goPFnOpts opts
                    <*> goPTypeDecl tdecl
    goPDecl (PDef fc cls) = PDef fc <$> goPClauses cls
    goPDecl (PData fc doc v d) = PData fc doc v <$> goPDataDecl d
    goPDecl (PParameters fc nts ps) =
      PParameters fc <$> go4TupledPTerms nts
                     <*> goPDecls ps
    goPDecl (PUsing fc mnts ps) =
      PUsing fc <$> goPairedPTerms mnts
                <*> goPDecls ps
    goPDecl (PReflect fc t) = PReflect fc <$> goPTerm t
    goPDecl (PInterface fc v mnts n doc nrts ns mn ps) =
      PInterface fc v <$> goPairedPTerms mnts
                      <*> pure n
                      <*> pure doc
                      <*> go3TupledPTerms nrts
                      <*> pure ns
                      <*> pure mn
                      <*> goPDecls ps
    goPDecl (PImplementation fc v opts p is cs n ts mn ns mps) =
      PImplementation fc v opts p <$> go3TupledPTerms is
                                  <*> goPairedPTerms cs
                                  <*> pure n
                                  <*> goPTerms ts
                                  <*> pure mn
                                  <*> pure ns
                                  <*> goMPDecls mps
    goPDecl (PRecord fc doc v n nts mn fs) =
      PRecord fc doc v n <$> go4TupledPTerms nts
                         <*> pure mn
                         <*> goPFields fs
    goPDecl (PMutual fc ps) = PMutual fc <$> goPDecls ps
    goPDecl p@(PFixity _ _ _ _) = pure p
    goPDecl (PNamespace fc strs ps) = PNamespace fc strs <$> goPDecls ps
    goPDecl (PTransform fc n a b) = PTransform fc n <$> goPTerm a <*> goPTerm b
    goPDecl (PRunElabDecl fc a) = PRunElabDecl fc <$> goPTerm a
    goPDecl p@(PDirective _ _) = pure p
    goPDecl p@(PBuiltin _ _ _) = pure p

    goPTypeDecl : PTypeDecl' nm -> Core (PTypeDecl' nm)
    goPTypeDecl (MkPTy fc nameFC n d t) = MkPTy fc nameFC n d <$> goPTerm t

    goPDataDecl : PDataDecl' nm -> Core (PDataDecl' nm)
    goPDataDecl (MkPData fc n t opts tdecls) =
      MkPData fc n <$> goPTerm t
                   <*> pure opts
                   <*> goPTypeDecls tdecls
    goPDataDecl (MkPLater fc n t) = MkPLater fc n <$> goPTerm t

    goPField : PField' nm -> Core (PField' nm)
    goPField (MkField fc doc c info n t) =
      MkField fc doc c <$> goPiInfo info
                       <*> pure n
                       <*> goPTerm t

    goPiInfo : PiInfo (PTerm' nm) -> Core (PiInfo (PTerm' nm))
    goPiInfo (DefImplicit t) = DefImplicit <$> goPTerm t
    goPiInfo t = pure t

    goPFnOpt : PFnOpt' nm -> Core (PFnOpt' nm)
    goPFnOpt o@(IFnOpt _) = pure o
    goPFnOpt (PForeign ts) = PForeign <$> goPTerms ts

    -- Traversable stuff. Inlined for termination checking.

    goMPTerm : Maybe (PTerm' nm) -> Core (Maybe $ PTerm' nm)
    goMPTerm Nothing  = pure Nothing
    goMPTerm (Just t) = Just <$> goPTerm t

    goPTerms : List (PTerm' nm) -> Core (List $ PTerm' nm)
    goPTerms []        = pure []
    goPTerms (t :: ts) = (::) <$> goPTerm t <*> goPTerms ts

    goPairedPTerms : List (x, PTerm' nm) -> Core (List (x, PTerm' nm))
    goPairedPTerms []             = pure []
    goPairedPTerms ((a, t) :: ts) =
       (::) . MkPair a <$> goPTerm t
                       <*> goPairedPTerms ts

    go3TupledPTerms : List (x, y, PTerm' nm) -> Core (List (x, y, PTerm' nm))
    go3TupledPTerms [] = pure []
    go3TupledPTerms ((a, b, t) :: ts) =
      (::) . (\ c => (a, b, c)) <$> goPTerm t
                                <*> go3TupledPTerms ts

    go4TupledPTerms : List (x, y, PiInfo (PTerm' nm), PTerm' nm) ->
                      Core (List (x, y, PiInfo (PTerm' nm), PTerm' nm))
    go4TupledPTerms [] = pure []
    go4TupledPTerms ((a, b, p, t) :: ts) =
      (\ p, d, ts => (a, b, p, d) :: ts) <$> goPiInfo p
                                         <*> goPTerm t
                                         <*> go4TupledPTerms ts

    goPStringLines : List (List (PStr' nm)) -> Core (List (List (PStr' nm)))
    goPStringLines []        = pure []
    goPStringLines (line :: lines) = (::) <$> goPStrings line <*> goPStringLines lines

    goPStrings : List (PStr' nm) -> Core (List (PStr' nm))
    goPStrings []        = pure []
    goPStrings (str :: strs) = (::) <$> goPStr str <*> goPStrings strs

    goPDos : List (PDo' nm) -> Core (List (PDo' nm))
    goPDos []        = pure []
    goPDos (d :: ds) = (::) <$> goPDo d <*> goPDos ds

    goPClauses : List (PClause' nm) -> Core (List (PClause' nm))
    goPClauses []          = pure []
    goPClauses (cl :: cls) = (::) <$> goPClause cl <*> goPClauses cls

    goMPDecls : Maybe (List (PDecl' nm)) -> Core (Maybe (List (PDecl' nm)))
    goMPDecls Nothing   = pure Nothing
    goMPDecls (Just ps) = Just <$> goPDecls ps

    goPDecls : List (PDecl' nm) -> Core (List (PDecl' nm))
    goPDecls []          = pure []
    goPDecls (d :: ds) = (::) <$> goPDecl d <*> goPDecls ds

    goPFieldUpdates : List (PFieldUpdate' nm) -> Core (List (PFieldUpdate' nm))
    goPFieldUpdates []          = pure []
    goPFieldUpdates (fu :: fus) = (::) <$> goPFieldUpdate fu <*> goPFieldUpdates fus

    goPFields : List (PField' nm) -> Core (List (PField' nm))
    goPFields []        = pure []
    goPFields (f :: fs) = (::) <$> goPField f <*> goPFields fs

    goPFnOpts : List (PFnOpt' nm) -> Core (List (PFnOpt' nm))
    goPFnOpts []        = pure []
    goPFnOpts (o :: os) = (::) <$> goPFnOpt o <*> goPFnOpts os

    goPTypeDecls : List (PTypeDecl' nm) -> Core (List (PTypeDecl' nm))
    goPTypeDecls []        = pure []
    goPTypeDecls (t :: ts) = (::) <$> goPTypeDecl t <*> goPTypeDecls ts


text:
||| Compiling an Idris2 interface and implementations
module Main

import Cairo

interface I a where
  f : a -> Felt

I Felt where
  f = id

I Bool where
  f False = 0
  f True = 1

%noinline
main : Cairo ()
main = do
    output $ f True
    output $ f (the Felt 42)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
||| Spec: http://webassembly.github.io/spec/core/syntax/types.html#result-types
module WebAssembly.Structure.Types.ResultTypes

import WebAssembly.Structure.Types.ValueTypes

public export
ResultType : Type
ResultType = List ValType

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly