Language.Reflection.Syntax

Some utilities for defining and manipulating TTImp values
for writing elaborator scripts.

Some notes: Use quotes whenever possible:

Names can be quoted like so: `{ AName }, `{ In.Namespace.AName }.
Both examples are of type Language.Reflection.TT.Name.

Expressions can be quoted like so: `(\x => x * x)

Definitions

isNil : Name -> Bool

  True if the given name ends on (`Basic $ UN "Nil")

Totality: total
Visibility: public export

isLin : Name -> Bool

  True if the given name ends on (`Basic $ UN "Lin")

Totality: total
Visibility: public export

isCons : Name -> Bool

  True if the given name ends on (`Basic $ UN "::")

Totality: total
Visibility: public export

isSnoc : Name -> Bool

  True if the given name ends on (`Basic $ UN ":<")

Totality: total
Visibility: public export

camelCase : Name -> String

  Takes a (probably fully qualified name) and generates a
  identifier from this without the dots.
  
  Example : camelCase "Data.List1.List1" = "DataList1List1"

Totality: total
Visibility: export

nameStr : Name -> String

  Convert a `Name` to a simple string dropping some of its context
  like its namespace (if any).
  
  Use this to get access to a simple variable name or to print the
  un-prefixed name of a data- or type constructor.

Totality: total
Visibility: export

interface Named : Type -> Type

  An interface for things with a `Name`.
  
  This comes with several utility function strewn across this module
  for creating variables from names and printing a name as a string.
  All these make use of dot syntax, so they can be used like record
  projections.

Parameters: a
Methods:

.getName : a -> Name

  Extract the `Name` from a value.
  
  We call this `(.getName)` instead
  of just `(.name)`, because `name` is a commonly used record field name.

Implementations:

Named a => Named (Subset a p)

Named Name

Named (Con n vs)

Named TypeInfo

Named (ParamCon n)

Named ParamTypeInfo

.getName : Named a => a -> Name

  Extract the `Name` from a value.
  
  We call this `(.getName)` instead
  of just `(.name)`, because `name` is a commonly used record field name.

Totality: total
Visibility: public export

.nameStr : Named a => a -> String

  Use `nameStr` to convert the name of a value to a simple string.

Totality: total
Visibility: public export

var : Name -> TTImp

  Creates a variable from the given name
  
  Names are best created using quotes: `{ AName },
  `{ In.Namespacs.Name }.
  
  Likewise, if the name is already known at the time of
  writing, use quotes for defining variables directly: `(AName)

Totality: total
Visibility: public export

.nameVar : Named a => a -> TTImp

  Creates a variable with the name of the given value.

Totality: total
Visibility: public export

varStr : String -> TTImp

  Alias for `var . fromString`

Totality: total
Visibility: public export

bindVar : Name -> TTImp

  Binds a new variable, for instance in a pattern match.
  
  This is an alias for `IBindVar EmptyFC`.

Totality: total
Visibility: public export

.bindVar : Named a => a -> TTImp

  Bind a named value to a variable. This uses `nameStr` for
  the variable's name.

Totality: total
Visibility: public export

implicitTrue : TTImp

  Implicit value bound if unsolved
  
  This is an alias for `Implicit EmptyFC True`

Totality: total
Visibility: public export

implicitFalse : TTImp

  Implicitly typed value unbound if unsolved
  
  This is an alias for `Implicit EmptyFC False`

Totality: total
Visibility: public export

primVal : Constant -> TTImp

  Primitive values.
  
  This is an alias for `IPrimVal EmptyFC`

Totality: total
Visibility: public export

.namePrim : Named a => a -> TTImp

  Creates a string constant from a named value. Uses
  `nameStr` to convert the name to a string.

Totality: total
Visibility: public export

type : TTImp

  The type `Type`.
  
  This is an alias for `IType EmptyFC`.

Totality: total
Visibility: public export

hole : String -> TTImp

  A named hole.
  
  This is an alias for `IHole EmptyFC`.

Totality: total
Visibility: public export

unVar : TTImp -> Maybe Name

  Tries to extract a variable name from a `TTImp`.
  
  Returns `Nothing` if not an `IVar`.

Totality: total
Visibility: public export

iSearch : Nat -> TTImp

  Proof search
  
  This is an alias for `ISearch EmptyFC`

Totality: total
Visibility: public export

app : TTImp -> TTImp -> TTImp

  Function application.
  
  This is an alias for `IApp EmptyFC`.
  
  Example: ```app (var "Just") (var "x")```
           is equivalent to `(Just x)

Totality: total
Visibility: public export

unApp : TTImp -> (TTImp, List TTImp)

Totality: total
Visibility: export

appAll : Name -> List TTImp -> TTImp

  Applies a list of variables to a function.
  
  See `appNames` for an example

Totality: total
Visibility: public export

appNames : Name -> List Name -> TTImp

  Applies a list of variable names to a function.
  
  Example: appNames "either" ["f","g","val"]
           is equivalent to ~(either f g val)

Totality: total
Visibility: public export

bindAll : Name -> List Name -> TTImp

  Binds a list of parameters to a data constructor in
  a pattern match.
  
  Example: bindAll "MkPair" ["a","b"]
           is the same as `(MkPair a b)

Totality: total
Visibility: public export

bindHere : BindMode -> TTImp -> TTImp

  Alias for `IBindHere EmptyFC`

Totality: total
Visibility: public export

mustUnify : DotReason -> TTImp -> TTImp

  Alias for `IMustUnify EmptyFC`

Totality: total
Visibility: public export

iAs : UseSide -> Name -> TTImp -> TTImp

  Alias for `IAs EmptyFC EmptyFC`

Totality: total
Visibility: public export

autoApp : TTImp -> TTImp -> TTImp

  Applying an auto-implicit.
  
  This is an alias for `IAutoApp EmptyFC`.
  
  Example: `autoApp (var "traverse") (var "MyApp")`
           is equivalent to `(traverse @{MyApp})

Totality: total
Visibility: public export

(.@) : TTImp -> TTImp -> TTImp

  Infix version of `autoApp`

Totality: total
Visibility: public export

withApp : TTImp -> TTImp -> TTImp

  Application in a `with` expression
  
  This is an alias for `IWithApp EmptyFC`.

Totality: total
Visibility: public export

namedApp : TTImp -> Name -> TTImp -> TTImp

  Named function application.
  
  This is an alias for `INamedApp EmptyFC`.
  
  Example: `namedApp (var "traverse") "f" (var "MyApp")`
           is equivalent to `(traverse {f = MyApp})

Totality: total
Visibility: public export

bindAny : Named a => a -> TTImp

  Catch-all pattern match on a data constructor.
  
  Example: `bindAny "Person"`
           is the same as `(Person {})
  ```

Totality: total
Visibility: public export

alternative : AltType -> List TTImp -> TTImp

  Alias for `IAlternative EmptyFC`

Totality: total
Visibility: public export

record Arg : Type

  A function argument, typically extracted from pi-types or used
  to define pi-types.

Totality: total
Visibility: public export
Constructor: 

MkArg : Count -> PiInfo TTImp -> Maybe Name -> TTImp -> Arg

Projections:

.count : Arg -> Count

.name : Arg -> Maybe Name

.piInfo : Arg -> PiInfo TTImp

.type : Arg -> TTImp

Hint: 

Named (Con n vs)

.count : Arg -> Count

Totality: total
Visibility: public export

count : Arg -> Count

Totality: total
Visibility: public export

.piInfo : Arg -> PiInfo TTImp

Totality: total
Visibility: public export

piInfo : Arg -> PiInfo TTImp

Totality: total
Visibility: public export

.name : Arg -> Maybe Name

Totality: total
Visibility: public export

name : Arg -> Maybe Name

Totality: total
Visibility: public export

.type : Arg -> TTImp

Totality: total
Visibility: public export

type : Arg -> TTImp

Totality: total
Visibility: public export

arg : TTImp -> Arg

  Creates an explicit unnamed argument of the given type.

Totality: total
Visibility: public export

erasedArg : TTImp -> Arg

  Creates an explicit, unnamed, zero-quantity
  argument of the given type.

Totality: total
Visibility: public export

lambdaArg : Named a => a -> Arg

  Creates an explicit argument of the given name
  to be used in a lambda.

Totality: total
Visibility: public export

erasedImplicit : Named a => a -> Arg

  Creates an erased implicit argument of the given name.

Totality: total
Visibility: public export

isExplicit : Arg -> Bool

  True if the given argument is an explicit argument.

Totality: total
Visibility: public export

isErased : Arg -> Bool

  True if the given argument has quantity zero.

Totality: total
Visibility: public export

isExplicitUnerased : Arg -> Bool

  True if the given argument is explicit and does not have
  quantity zero.

Totality: total
Visibility: public export

unPi : TTImp -> (List Arg, TTImp)

  Extracts the arguments from a function type.

Totality: total
Visibility: export

unLambda : TTImp -> (List Arg, TTImp)

  Extracts the arguments from a lambda.

Totality: total
Visibility: export

lam : Arg -> TTImp -> TTImp

  Defines an anonymous function (lambda).
  
  This passes the fields of `Arg` to `ILam EmptyFC`

Totality: total
Visibility: public export

pi : Arg -> TTImp -> TTImp

  Defines a function type.
  
  This passes the fields of `Arg` to `IPi EmptyFC`

Totality: total
Visibility: public export

piAll : TTImp -> List Arg -> TTImp

  Defines a function type taking the given arguments.

Totality: total
Visibility: public export

piAllImplicit : TTImp -> List Name -> TTImp

  Defines a function type taking implicit arguments of the
  given names.

Totality: total
Visibility: public export

piAllAuto : TTImp -> List TTImp -> TTImp

  Defines a function type taking the given auto-implicit arguments.

Totality: total
Visibility: public export

impossibleClause : TTImp -> Clause

  An impossible clause in a pattern match.
  
  This is an alias for `ImpossibleClause EmptyFC`.

Totality: total
Visibility: public export

patClause : TTImp -> TTImp -> Clause

  A pattern clause consisting of the left-hand and
  right-hand side of the pattern arrow "=>".
  
  This is an alias for `PatClause EmptyFC`.

Totality: total
Visibility: public export

withClause : TTImp -> Count -> TTImp -> Maybe (Count, Name) -> List WithFlag -> List Clause -> Clause

  A with clause.
  
  This is an alias for `WithClause EmptyFC`.

Totality: total
Visibility: public export

iCase : TTImp -> TTImp -> List Clause -> TTImp

  A case expression.
  
  This is an alias for `ICase EmptyFC []`.

Totality: total
Visibility: public export

as : Name -> TTImp -> TTImp

  "as"-pattern.
  
  This is an alias for `IAs EmptyFC UseLeft`.

Totality: total
Visibility: public export

mkTy : Name -> TTImp -> ITy

  Named type.
  
  This is an alias for `MkTyp EmptyFC`.

Totality: total
Visibility: public export

claim : Count -> Visibility -> List FnOpt -> Name -> TTImp -> Decl

  Type declaration of a function.
  
  `claim c v opts n tp` is an alias for
  `IClaim EmptyFC c v opts (MkTy EmptyFC n tp)`.

Totality: total
Visibility: public export

simpleClaim : Visibility -> Name -> TTImp -> Decl

  `simpleClaim v n t` is an alias for `claim MW v [] (mkTy n t)`

Totality: total
Visibility: public export

public' : Name -> TTImp -> Decl

  Alias for `simpleClaim Public`

Totality: total
Visibility: public export

private' : Name -> TTImp -> Decl

  Alias for `simpleClaim Private``

Totality: total
Visibility: public export

export' : Name -> TTImp -> Decl

  Alias for `simpleClaim Export`

Totality: total
Visibility: public export

directHint : Visibility -> Name -> TTImp -> Decl

  `directHint v` is an alias for `claim MW v [Hint True]`

Totality: total
Visibility: public export

interfaceHintOpts : Visibility -> List FnOpt -> Name -> TTImp -> Decl

  `interfaceHint v opts` is an alias for `claim MW v (Hint False :: opts)`

Totality: total
Visibility: public export

interfaceHint : Visibility -> Name -> TTImp -> Decl

  `interfaceHint v` is an alias for `claim MW v [Hint False]`

Totality: total
Visibility: public export

def : Name -> List Clause -> Decl

  Function definition (implementation)
  
  This is an alias for `IDef EmptyFC`.

Totality: total
Visibility: public export

iLet : Count -> Name -> TTImp -> TTImp -> TTImp -> TTImp

  Let bindings.
  
  This is an alias for `ILet EmptyFC`.

Totality: total
Visibility: public export

local : List Decl -> TTImp -> TTImp

  Local definitions
  
  This is an alias for `ILocal EmptyFC`.

Totality: total
Visibility: public export

update : List IFieldUpdate -> TTImp -> TTImp

  Field updates
  
  This is an alias for `IUpdate EmptyFC`.

Totality: total
Visibility: public export

iData : Visibility -> Name -> TTImp -> List DataOpt -> List ITy -> Decl

  Data declaration.
  
  This merges constructors `IData` and `MkData`.

Totality: total
Visibility: public export

iDataLater : Visibility -> Name -> TTImp -> Decl

  Data claim.
  
  This merges constructors `IData` and `MkLater`.

Totality: total
Visibility: public export

simpleData : Visibility -> Name -> List ITy -> Decl

  Simple data declaration of type `Type` (no options, no parameters,
  no indices).
  
  `simpleData v n` is an alias for `iData v n type []`.

Totality: total
Visibility: public export

simpleDataPublic : Name -> List ITy -> Decl

  Alias for `simpleData Public`

Totality: total
Visibility: public export

simpleDataExport : Name -> List ITy -> Decl

  Alias for `simpleData Export`

Totality: total
Visibility: public export

iRewrite : TTImp -> TTImp -> TTImp

  Alias for `IRewrite EmptyFC`

Totality: total
Visibility: public export

iDelayed : LazyReason -> TTImp -> TTImp

  Alias for `IDelayed EmptyFC`

Totality: total
Visibility: public export

iDelay : TTImp -> TTImp

  Alias for `IDelay EmptyFC`

Totality: total
Visibility: public export

iForce : TTImp -> TTImp

  Alias for `IForce EmptyFC`

Totality: total
Visibility: public export

quote : TTImp -> TTImp

  Alias for `IQuote EmptyFC`

Totality: total
Visibility: public export

quoteName : Name -> TTImp

  Alias for `IQuoteName EmptyFC`

Totality: total
Visibility: public export

quoteDecl : List Decl -> TTImp

  Alias for `IQuoteDecl EmptyFC`

Totality: total
Visibility: public export

unquote : TTImp -> TTImp

  Alias for `IUnquote EmptyFC`

Totality: total
Visibility: public export

rec : List Name -> TTImp -> Bool

  Checks if one of the given names makes an appearance in the
  given type.

Totality: total
Visibility: export

assertIfRec : List Name -> TTImp -> TTImp -> TTImp

  Prefixes the given expression with `assert_total`, if
  one of the names listed makes an appearance in the given type.

Totality: total
Visibility: export

listOf : Foldable t => t TTImp -> TTImp

  Constructs a `TTImp` from the given arguments, which
  wraps them in unqualified list constructors.
  
  For instance, `listOf [var "x", var "y"]` generates
  an expression corresponding to `x :: y :: Nil`

Totality: total
Visibility: public export

lookupName : Elaboration m => Name -> m (Name, TTImp)

  Looks up a name in the current namespace.

Totality: total
Visibility: export