Derive.Refined

This module derives functionality for refinement type. In general,
a refinement type is of the following shape:

```idris
record Percent where
  constructor MkPercent
  value : Double
  0 prf : IsPercent value
```

That is, a value paired with a predicate on that value. The
predicate can be an explicit or implicit argument of any
quantity.

Reexports

Definitions

data AppVar : PArg n -> Name -> Type

  Proof that a constructor argument `arg` is a dependent type
  on a second argument of name `name`, that is, `arg` is
  of type `p nm` for some predicate `p`.

Totality: total
Visibility: public export
Constructors:

HereApp : (0 _ : n1 == n2 = True) -> AppVar (PApp p (PVar n2)) n1

HereNamedApp : (0 _ : n1 == n2 = True) -> AppVar (PNamedApp p n3 (PVar n2)) n1

ThereApp : AppVar p n1 -> AppVar (PApp p p2) n1

ThereNamedApp : AppVar p n1 -> AppVar (PNamedApp p n2 p2) n1

appVar : (nm : Name) -> (arg : PArg n) -> Maybe (AppVar arg nm)

  Tests if `arg` is a dependent type on a value with name `nm`.

Totality: total
Visibility: public export

data ProofInfo : PiInfo TTImp -> Type

  A proof (value of a predicate) in a refined type must be
  an explicit or auto-implicit argument of that type.

Totality: total
Visibility: public export
Constructors:

PIAuto : ProofInfo AutoImplicit

PIExplicit : ProofInfo ExplicitArg

proofInfo : (pi : PiInfo TTImp) -> Maybe (ProofInfo pi)

  Tests if `pi` is explicit or auto-implicit

Totality: total
Visibility: public export

data RefinedArgs : Vect m (ConArg n) -> Type

  Proof that the argument list of a data constructor
  consists of erased implicits followed by a single
  explicit value, followed by an explicit or auto-implicit
  predicate on the value.

Totality: total
Visibility: public export
Constructors:

RArgs : ProofInfo pi -> AppVar t2 nm -> RefinedArgs [CArg (Just nm) MW ExplicitArg t1, CArg mn c pi t2]

RImplicit : RefinedArgs as -> RefinedArgs (ParamArg ix t :: as)

refinedArgs : (as : Vect m (ConArg n)) -> Maybe (RefinedArgs as)

  Tests if the arguments of a data constructor are valid
  arguments of a refined type.

Totality: total
Visibility: public export

proofType : Vect n Name -> (as : Vect m (ConArg n)) -> RefinedArgs as -> TTImp

  Extracts the predicate from the constructor of a refined type.

Totality: total
Visibility: export

isErased : (as : Vect m (ConArg n)) -> RefinedArgs as -> Bool

  Extracts the predicate from the constructor of a refined type.

Totality: total
Visibility: export

valType : Vect n Name -> (as : Vect m (ConArg n)) -> RefinedArgs as -> TTImp

  Extracts the value type from the constructor of a refined type.

Totality: total
Visibility: export

valName : (as : Vect m (ConArg n)) -> RefinedArgs as -> Name

  Extracts the field name from the constructor of a refined type

Totality: total
Visibility: export

appCon : TTImp -> (c : ParamCon n) -> RefinedArgs (c .args) -> TTImp

  Applies the data constructor of a refinement type to a
  refined value. We assume that a proof of validity of
  the correct count is already in scope.
  
  In case of an explicit proof argument, we pass the argument
  by invoking `%search`, in case of an auto-implicit proof argument,
  proof search will do this for us automatically.

Totality: total
Visibility: export

data RefinedInfo : ParamTypeInfo -> Type

  Proof that a data type is a refinement type: A data type with a single
  data constructor taking an arbitrary number or erased implicit arguments,
  a single explicit value argument of quantity "any" and an explict or
  auto-implicit predicate on the value.

Totality: total
Visibility: public export
Constructor: 

RI : RefinedArgs (c .args) -> RefinedInfo (MkParamTypeInfo ti p ns [c] s)

refinedInfo : (p : ParamTypeInfo) -> Res (RefinedInfo p)

Totality: total
Visibility: export

refineClaim : Name -> (p : ParamTypeInfo) -> RefinedInfo p -> Decl

  Function for refining a value at runtime. This returns a `Maybe` of
  the refinement type.

Totality: total
Visibility: export

refineDef : Name -> (p : ParamTypeInfo) -> RefinedInfo p -> Decl

Totality: total
Visibility: export

refineTL : Name -> (p : ParamTypeInfo) -> RefinedInfo p -> TopLevel

Totality: total
Visibility: export

fromIntTL : Visibility -> (p : ParamTypeInfo) -> RefinedInfo p -> TopLevel

Totality: total
Visibility: export

fromDblTL : Visibility -> (p : ParamTypeInfo) -> RefinedInfo p -> TopLevel

Totality: total
Visibility: export

fromStrTL : Visibility -> (p : ParamTypeInfo) -> RefinedInfo p -> TopLevel

Totality: total
Visibility: export

refineName : Named a => a -> Name

Totality: total
Visibility: export

Refined : List Name -> ParamTypeInfo -> Res (List TopLevel)

Totality: total
Visibility: export

RefinedIntegerVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)

Totality: total
Visibility: export

RefinedInteger : List Name -> ParamTypeInfo -> Res (List TopLevel)

Totality: total
Visibility: export

RefinedDoubleVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)

Totality: total
Visibility: export

RefinedDouble : List Name -> ParamTypeInfo -> Res (List TopLevel)

Totality: total
Visibility: export

RefinedStringVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)

Totality: total
Visibility: export

RefinedString : List Name -> ParamTypeInfo -> Res (List TopLevel)

Totality: total
Visibility: export