Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[ derive, refactor, perf ] Refactor TypeApp, make derivation faster #203

Merged
merged 3 commits into from
Sep 25, 2024
Merged

[ derive, refactor, perf ] Refactor TypeApp, make derivation faster #203

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1189eab
[ refactor ] Move arguments dependencies calculation function up & nicen
buzden Sep 25, 2024
6904a9a
[ refactor, derive, perf ] Move `TypeApp` type out
buzden Sep 25, 2024
56b6a43
[ refactor ] Make `TypeApp` to be `record`
buzden Sep 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
77 changes: 39 additions & 38 deletions src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,41 @@ import public Deriving.DepTyCheck.Gen.Derive

%default total

record TypeApp (0 con : Con) where
constructor MkTypeApp
argHeadType : TypeInfo
{auto 0 argHeadTypeGood : AllTyArgsNamed argHeadType}
argApps : Vect argHeadType.args.length .| Either (Fin con.args.length) TTImp

getTypeApps : Elaboration m => NamesInfoInTypes => (con : Con) -> m $ Vect con.args.length $ TypeApp con
getTypeApps con = do
let conArgIdxs = SortedMap.fromList $ mapI con.args $ \idx, arg => (argName arg, idx)

-- Analyse that we can do subgeneration for each constructor argument
-- Fails using `Elaboration` if the given expression is not an application to a type constructor
let analyseTypeApp : TTImp -> m $ TypeApp con
analyseTypeApp expr = do
let (lhs, args) = unAppAny expr
ty <- case lhs of
IVar _ lhsName => do let Nothing = lookupType lhsName -- TODO to support `lhsName` to be a type parameter of type `Type`
| Just found => pure found
-- we didn't found, failing, there are at least two reasons
failAt (getFC lhs) $ if isNamespaced lhsName
then "Data type `\{lhsName}` is unavailable at the site of derivation (forgotten import?)"
else "Usupported applications to a non-concrete type `\{lhsName}`"
IPrimVal _ (PrT t) => pure $ typeInfoForPrimType t
IType _ => pure typeInfoForTypeOfTypes
lhs@(IPi {}) => failAt (getFC lhs) "Fields with function types are not supported in constructors"
lhs => failAt (getFC lhs) "Unsupported type of a constructor field: \{show lhs}"
let Yes lengthCorrect = decEq ty.args.length args.length
| No _ => failAt (getFC lhs) "INTERNAL ERROR: wrong count of unapp when analysing type application"
_ <- ensureTyArgsNamed ty
pure $ MkTypeApp ty $ rewrite lengthCorrect in args.asVect <&> \arg => case getExpr arg of
expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs
expr => Right expr

for con.args.asVect $ analyseTypeApp . type

-------------------------------------------------
--- Derivation of a generator for constructor ---
-------------------------------------------------
Expand Down Expand Up @@ -52,37 +87,11 @@ namespace NonObligatoryExts
-- Prepare intermediate data and functions using this data --
-------------------------------------------------------------

-- Get file position of the constructor definition (for better error reporting)
let conFC = getFC con.type

-- Build a map from constructor's argument name to its index
let conArgIdxs = SortedMap.fromList $ mapI con.args $ \idx, arg => (argName arg, idx)

-- Analyse that we can do subgeneration for each constructor argument
-- Fails using `Elaboration` if the given expression is not an application to a type constructor
let analyseTypeApp : TTImp -> m TypeApp
analyseTypeApp expr = do
let (lhs, args) = unAppAny expr
ty <- case lhs of
IVar _ lhsName => do let Nothing = lookupType lhsName -- TODO to support `lhsName` to be a type parameter of type `Type`
| Just found => pure found
-- we didn't found, failing, there are at least two reasons
failAt (getFC lhs) $ if isNamespaced lhsName
then "Data type `\{lhsName}` is unavailable at the site of derivation (forgotten import?)"
else "Usupported applications to a non-concrete type `\{lhsName}`"
IPrimVal _ (PrT t) => pure $ typeInfoForPrimType t
IType _ => pure typeInfoForTypeOfTypes
lhs@(IPi {}) => failAt (getFC lhs) "Fields with function types are not supported in constructors"
lhs => failAt (getFC lhs) "Unsupported type of a constructor field: \{show lhs}"
let Yes lengthCorrect = decEq ty.args.length args.length
| No _ => failAt (getFC lhs) "INTERNAL ERROR: wrong count of unapp when analysing type application"
_ <- ensureTyArgsNamed ty
pure $ MkTypeApp ty $ rewrite lengthCorrect in args.asVect <&> \arg => case getExpr arg of
expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs
expr => Right expr

-- Compute left-to-right need of generation when there are non-trivial types at the left
argsTypeApps <- for con.args.asVect $ analyseTypeApp . type
argsTypeApps <- getTypeApps con

-- Get dependencies of constructor's arguments
let rawDeps' = argDeps con.args
Expand All @@ -107,7 +116,7 @@ namespace NonObligatoryExts
genForOrder order = map (foldr apply callCons) $ evalStateT givs $ for order $ \genedArg => do

-- Get info for the `genedArg`
let MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ TypeApp) argsTypeApps
let MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ $ TypeApp con) argsTypeApps

-- Acquire the set of arguments that are already present
presentArguments <- get
Expand Down Expand Up @@ -161,14 +170,14 @@ namespace NonObligatoryExts
-------------------------------------------------

-- Determine which arguments need to be generated in a left-to-right manner
let (leftToRightArgsTypeApp, leftToRightArgs) = unzip $ filter (\((MkTypeApp _ as), _) => any isRight as) $ toListI argsTypeApps
let (leftToRightArgsTypeApp, leftToRightArgs) = unzip $ filter (\(ta, _) => any isRight ta.argApps) $ toListI argsTypeApps

--------------------------------------------------------------------------------
-- Preparation of input for the left-to-right phase (1st right-to-left phase) --
--------------------------------------------------------------------------------

-- Acquire those variables that appear in non-trivial type expressions, i.e. those which needs to be generated before the left-to-right phase
let preLTR = leftToRightArgsTypeApp >>= \(MkTypeApp _ as) => rights (toList as) >>= allVarNames
let preLTR = leftToRightArgsTypeApp >>= \ta => rights (toList ta.argApps) >>= allVarNames
let preLTR = SortedSet.fromList $ mapMaybe (lookup' conArgIdxs) preLTR

-- Find rightmost arguments among `preLTR`
Expand Down Expand Up @@ -218,14 +227,6 @@ namespace NonObligatoryExts
Foldable f => Interpolation (f $ Fin con.args.length) where
interpolate = ("[" ++) . (++ "]") . joinBy ", " . map interpolate . toList

-- TODO make this to be a `record` as soon as #2177 is fixed
data TypeApp : Type where
MkTypeApp :
(type : TypeInfo) ->
(0 _ : AllTyArgsNamed type) =>
(argTypes : Vect type.args.length .| Either (Fin con.args.length) TTImp) ->
TypeApp

||| Best effort non-obligatory tactic tries to use as much external generators as possible
||| but discards some there is a conflict between them.
||| All possible non-conflicting layouts may be produced in the generated values list.
Expand Down
24 changes: 12 additions & 12 deletions src/Deriving/DepTyCheck/Util/Reflection.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -389,6 +389,18 @@ export
allVarNames : TTImp -> List Name
allVarNames = SortedSet.toList . allVarNames'

public export
0 ArgDeps : Nat -> Type
ArgDeps n = DVect n $ SortedSet . Fin . Fin.finToNat

export
argDeps : (args : List Arg) -> ArgDeps args.length
argDeps args = do
let nameToIndices = SortedMap.fromList $ mapI args $ \i, arg => (argName arg, SortedSet.singleton i)
let args = Vect.fromList args <&> \arg => allVarNames arg.type |> map (fromMaybe empty . lookup' nameToIndices)
flip upmapI args $ \i, deps => flip concatMap deps $ \candidates =>
maybe empty singleton $ last' $ mapMaybe tryToFit $ SortedSet.toList candidates

export
record NamesInfoInTypes where
constructor Names
Expand Down Expand Up @@ -612,15 +624,3 @@ genTypeName g = do
let (IVar _ genTy, _) = unApp genTy
| (genTy, _) => failAt (getFC genTy) "Expected a type name"
pure genTy

----------------------------------------------
--- Analyzing dependently typed signatures ---
----------------------------------------------

export
argDeps : (args : List Arg) -> DVect args.length $ SortedSet . Fin . Fin.finToNat
argDeps args = do
let nameToIndices = SortedMap.fromList $ mapI args $ \i, arg => (argName arg, SortedSet.singleton i)
let args = Vect.fromList args <&> \arg => allVarNames arg.type |> map (fromMaybe empty . lookup' nameToIndices)
flip upmapI args $ \i, argDeps => flip concatMap argDeps $ \candidates =>
maybe empty singleton $ last' $ mapMaybe tryToFit $ SortedSet.toList candidates