Computation Model

full code

Idris1

||| Reflection of the well typed core language
data TT =
        ||| A reference to some name (P for Parameter)
        P NameType TTName TT |
        ||| de Bruijn variables
        V Int |
        ||| Bind a variable
        Bind TTName (Binder TT) TT |
        ||| Apply one term to another
        App TT TT |
        ||| Embed a constant
        TConst Const |
        ||| Erased terms
        Erased |
        ||| The type of types along (with universe constraints)
        TType TTUExp |
        ||| Alternative universes for dealing with uniqueness
        UType Universe

full code

Idris2

public export
data TT : List Name -> Type where
     Local : FC -> (idx : Nat) -> (n : Name) ->
             (0 prf : IsVar name idx vars) -> TT vars
     Ref : FC -> NameType -> Name -> TT vars
     Pi : FC -> Count -> PiInfo ->
          (x : Name) -> (argTy : TT vars) -> (retTy : TT (x :: vars)) ->
          TT vars
     Lam : FC -> Count -> PiInfo ->
           (x : Name) -> (argTy : TT vars) -> (scope : TT (x :: vars)) ->
           TT vars
     App : FC -> TT vars -> TT vars -> TT vars
     TDelayed : FC -> LazyReason -> TT vars -> TT vars
     TDelay : FC -> LazyReason -> (ty : TT vars) -> (arg : TT vars) -> TT vars
     TForce : FC -> TT vars -> TT vars
     PrimVal : FC -> Constant -> TT vars
     Erased : FC -> TT vars
     TType : FC -> TT vars

x

full code

Idris1

||| Types annotations for bound variables in different
||| binding contexts
|||
||| @ tmTy the terms that can occur inside the binder, as type
|||        annotations or bound values
data Binder : (tmTy : Type) -> Type where
  ||| Lambdas
  |||
  ||| @ ty the type of the argument
  Lam : (ty : a) -> Binder a

  ||| Function types.
  |||
  ||| @ kind The kind of arrow. Only relevant when dealing with
  |||        uniqueness, so you can usually pretend that this
  |||        field doesn't exist. For ordinary functions, use the
  |||        type of types here.
  Pi : (ty, kind : a) -> Binder a

  ||| A let binder
  |||
  ||| @ ty the type of the bound variable
  ||| @ val the bound value
  Let : (ty, val : a) -> Binder a

  ||| A hole that can occur during elaboration, and must be filled
  |||
  ||| @ ty the type of the value that will eventually be put into the hole
  Hole : (ty : a) -> Binder a

  ||| A hole that will later become a top-level metavariable
  GHole : (ty : a) -> Binder a

  ||| A hole with a solution in it. Computationally inert.
  |||
  ||| @ ty the type of the value in the hole
  ||| @ val the value in the hole
  Guess : (ty, val : a) -> Binder a

  ||| A pattern variable. These bindings surround the terms that make
  ||| up the left and right sides of pattern-matching definition
  ||| clauses.
  |||
  ||| @ ty the type of the pattern variable
  PVar : (ty : a) -> Binder a

  ||| The type of a pattern binding. This is to `PVar` as `Pi` is to
  ||| `Lam`.
  |||
  ||| @ ty the type of the pattern variable
  PVTy : (ty : a) -> Binder a

data PiInfo t = Implicit | Explicit | AutoImplicit | DefImplicit t

public export
data Binder : Type -> Type where
	   -- Lambda bound variables with their implicitness
     Lam : RigCount -> PiInfo type -> (ty : type) -> Binder type
		 -- Let bound variables with their value
     Let : RigCount -> (val : type) -> (ty : type) -> Binder type
		 -- Forall/pi bound variables with their implicitness
     Pi : RigCount -> PiInfo type -> (ty : type) -> Binder type
		 -- pattern bound variables. The PiInfo gives the implicitness at the
     -- point it was bound (Explicit if it was explicitly named in the
     -- program)
     PVar : RigCount -> PiInfo type -> (ty : type) -> Binder type
		 -- variable bound for an as pattern (Like a let, but no computational
     -- force, and only used on the lhs. Converted to a let on the rhs because
     -- we want the computational behaviour.)
     PLet : RigCount -> (val : type) -> (ty : type) -> Binder type
		 -- the type of pattern bound variables
     PVTy : RigCount -> (ty : type) -> Binder type

x

x

x