Deriving.DepTyCheck.Util.DeepConsApp

Reexports

import public Control.Monad.Writer.Interface
import public Data.Fin.Split
import public Data.List.Ex
import public Data.List.Map
import public Data.List.Set
import public Data.SortedSet
import public Data.Vect.Ex
import public Language.Reflection.Compat.TypeInfo

Definitions

data ConsDetermInfo : Type

Totality: total
Visibility: public export
Constructors:

DeterminedByType : ConsDetermInfo
NotDeterminedByType : ConsDetermInfo
MustDecEqWith : TTImp -> ConsDetermInfo

Hints:

Cast Bool ConsDetermInfo
Cast ConsDetermInfo Bool
Monoid ConsDetermInfo
Semigroup ConsDetermInfo
Show ConsDetermInfo

ShowConsDetermInfo : Show ConsDetermInfo

Totality: total
Visibility: export

determineMustDecEqs : ConsDetermInfo -> ConsDetermInfo

Totality: total
Visibility: public export

BindExprFun : Nat -> Type

Totality: total
Visibility: public export

DeepConsAnalysisRes : Bool -> Type

Totality: total
Visibility: public export

analyseDeepConsApp : NamesInfoInTypes => MonadWriter (List String) m => (collectConsDetermInfo : Bool) -> SortedSet Name -> TTImp -> m (DeepConsAnalysisRes collectConsDetermInfo)

  Analyses whether the given expression can be an expression of free variables applied (maybe deeply) to a number of data constructors.
  
  Returns which of given free names are actually used in the given expression, in order of appearance in the expression.
  Notice that applied free names may repeat as soon as one name is used several times in the given expression.
  
  Also, a function returning a bind expression (an expression replacing all free names with bind names (`IBindVar`))
  is also returned.
  This function requires bind variable names as input.
  It returns correct bind expression only when all given bind names are different.

Totality: total
Visibility: export