<commit_before>||| Primitives and tactics for elaborator reflection.
|||
||| Elaborator reflection allows Idris code to control Idris's
||| built-in elaborator, and re-use features like the unifier, the
||| type checker, and the hole mechanism.
module Language.Reflection.Elab

import Builtins
import Prelude.Applicative
import Prelude.Basics
import Prelude.Bool
import Prelude.Functor
import Prelude.List
import Prelude.Maybe
import Prelude.Monad
import Prelude.Nat
import Language.Reflection

data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat

||| Erasure annotations reflect Idris's idea of what is intended to be
||| erased.
data Erasure = Erased | NotErased

||| How an argument is provided in high-level Idris
data Plicity =
  ||| The argument is directly provided at the application site
  Explicit |
  ||| The argument is found by Idris at the application site
  Implicit |
  ||| The argument is solved using type class resolution
  Constraint

||| Function arguments
|||
||| These are the simplest representation of argument lists, and are
||| used for functions. Additionally, because a FunArg provides enough
||| information to build an application, a generic type lookup of a
||| top-level identifier will return its FunArgs, if applicable.
record FunArg where
  constructor MkFunArg
  name    : TTName
  type    : Raw
  plicity : Plicity
  erasure : Erasure

||| Type constructor arguments
|||
||| Each argument is identified as being either a parameter that is
||| consistent in all constructors, or an index that varies based on
||| which constructor is selected.
data TyConArg =
  ||| Parameters are uniform across the constructors
  TyConParameter FunArg |
  ||| Indices are not uniform
  TyConIndex FunArg

||| A type declaration
record TyDecl where
  constructor Declare

  ||| The name of the function being declared.
  name : TTName

  ||| Each argument is in the scope of the names of previous arguments.
  arguments : List FunArg

  ||| The return type is in the scope of all the argument names.
  returnType : Raw


-- Note: FunClause is not a record because impossible clauses may be
-- added at some point.
||| A single pattern-matching clause
data FunClause : Type where
  MkFunClause : (lhs, rhs : Raw) -> FunClause

||| A reflected function definition.
record FunDefn where
  constructor DefineFun
  name : TTName
  clauses : List FunClause


data CtorArg = CtorParameter FunArg | CtorField FunArg

||| A reflected datatype definition
record Datatype where
  constructor MkDatatype

  ||| The name of the type constructor
  name : TTName

  ||| The arguments to the type constructor
  tyConArgs : List TyConArg

  ||| The result of the type constructor
  tyConRes : Raw

  ||| The constructors for the family
  constructors : List (TTName, List CtorArg, Raw)

||| A reflected elaboration script.<commit_msg>Add MkImpossibleClause constructor to FunClause<commit_after>||| Primitives and tactics for elaborator reflection.
|||
||| Elaborator reflection allows Idris code to control Idris's
||| built-in elaborator, and re-use features like the unifier, the
||| type checker, and the hole mechanism.
module Language.Reflection.Elab

import Builtins
import Prelude.Applicative
import Prelude.Basics
import Prelude.Bool
import Prelude.Functor
import Prelude.List
import Prelude.Maybe
import Prelude.Monad
import Prelude.Nat
import Language.Reflection

data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat

||| Erasure annotations reflect Idris's idea of what is intended to be
||| erased.
data Erasure = Erased | NotErased

||| How an argument is provided in high-level Idris
data Plicity =
  ||| The argument is directly provided at the application site
  Explicit |
  ||| The argument is found by Idris at the application site
  Implicit |
  ||| The argument is solved using type class resolution
  Constraint

||| Function arguments
|||
||| These are the simplest representation of argument lists, and are
||| used for functions. Additionally, because a FunArg provides enough
||| information to build an application, a generic type lookup of a
||| top-level identifier will return its FunArgs, if applicable.
record FunArg where
  constructor MkFunArg
  name    : TTName
  type    : Raw
  plicity : Plicity
  erasure : Erasure

||| Type constructor arguments
|||
||| Each argument is identified as being either a parameter that is
||| consistent in all constructors, or an index that varies based on
||| which constructor is selected.
data TyConArg =
  ||| Parameters are uniform across the constructors
  TyConParameter FunArg |
  ||| Indices are not uniform
  TyConIndex FunArg

||| A type declaration
record TyDecl where
  constructor Declare

  ||| The name of the function being declared.
  name : TTName

  ||| Each argument is in the scope of the names of previous arguments.
  arguments : List FunArg

  ||| The return type is in the scope of all the argument names.
  returnType : Raw


||| A single pattern-matching clause
data FunClause : Type where
  MkFunClause : (lhs, rhs : Raw) -> FunClause
  MkImpossibleClause : (lhs : Raw) -> FunClause

||| A reflected function definition.
record FunDefn where
  constructor DefineFun
  name : TTName
  clauses : List FunClause


data CtorArg = CtorParameter FunArg | CtorField FunArg

||| A reflected datatype definition
record Datatype where
  constructor MkDatatype

  ||| The name of the type constructor
  name : TTName

  ||| The arguments to the type constructor
  tyConArgs : List TyConArg

  ||| The result of the type constructor
  tyConRes : Raw

  ||| The constructors for the family
  constructors : List (TTName, List CtorArg, Raw)

||| A reflected elaboration script.
{'fraction_non_alphanumeric': 0.06752241955336732, 'fraction_numerical': 0.0, 'mean_word_length': 4.156844968268359, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 6, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4029914', 'n_tokens_mistral': 1619, 'n_tokens_neox': 1574, 'n_words': 710}